Skip to content

Boolean OR complement folding deletes a tautology #247

Description

@NullWitnessZK

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).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions