Skip to content

fix: fold boolean OR complements to true - #252

Draft
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/cfold-or-complement
Draft

fix: fold boolean OR complements to true#252
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/cfold-or-complement

Conversation

@NullWitnessZK

Copy link
Copy Markdown

Fixes #247.

Minimal reproducer

Save as main.pl:

main(A: private bool, R: public u8) :-
    !A;
    A;
    R = 0x05.

The three cases form (!A) OR A OR (R == 5). Because !A OR A is always true, source semantics accept every R, including R = 6.

Compile through the normal Datalog proof pipeline at 271f911 and evaluate with R = 6:

raw source relation:       accepts R = 6
optimized IR:              (= R #x05)
pre/post R1CS and artifact: reject R = 6; accept R = 5

Expected

The entire disjunction folds to true.

Actual

The complementary pair is deleted, leaving only R == 5. A source-valid public input is rejected.

Why it happens

The wide BoolNaryOp::Or constant folder removes x and !x from its child set instead of returning true. Frontends can reach this n-ary form because Opt::Flatten runs before the final constant-fold pass.

Impact: overconstraint/completeness only.

Proposed fix

fix/cfold-or-complement at 65a9c14 returns true immediately when either ordering of a complementary pair is found.

The branch contains a self-contained regression:

cargo test b_or_complement

It checks both or(x, !x) and or(!x, x).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Boolean OR complement folding deletes a tautology

1 participant