Skip to content

fix: preserve contradictory constant pin constraints - #424

Draft
NullWitnessZK wants to merge 1 commit into
iden3:masterfrom
NullWitnessZK:fix/contradictory-constant-pins
Draft

fix: preserve contradictory constant pin constraints#424
NullWitnessZK wants to merge 1 commit into
iden3:masterfrom
NullWitnessZK:fix/contradictory-constant-pins

Conversation

@NullWitnessZK

@NullWitnessZK NullWitnessZK commented Aug 4, 2026

Copy link
Copy Markdown

Summary

Preserve an explicit contradiction when constant-pin simplification encounters different constants for the same signal.

Given:

signal x;
x <== a + b;
x === 3;
x === 5;

the source constraint system is unsatisfiable. Before this change, fast substitutions were inserted into a map keyed by signal, so the later x = 5 substitution overwrote x = 3. -O1 dropped one pin and -O2 could emit zero constraints.

Expected versus current behavior:

       current       expected
-O0    4 constraints  contradiction preserved
-O1    2 constraints  contradiction preserved
-O2    0 constraints  contradiction preserved

Fixes #425. The upstream issue contains the complete standalone reproducer and observed compiler output.

Changes

  • Detect multiple substitutions for the same signal while encoding fast substitutions.
  • If the constants disagree, preserve a contradictory constraint rather than overwriting the first substitution.
  • Add a regression covering the conflicting-pin case.

Validation

cargo test contradictory_constant_pins_are_not_overwritten
git diff --check

The focused test passes. Repository-wide formatting was not applied because the upstream checkout has unrelated pre-existing formatting differences.

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.

Contradictory constant pins are lost during simplification

1 participant