[Preview] Contradictory constant pins are lost during simplification

[NullWitnessZK]

Fork-local preview only. Not submitted to iden3/circom.

Minimal reproducer

Save as conflicting_pins.circom:

pragma circom 2.0.0;

template T() {
    signal input a;
    signal input b;
    signal output o;
    signal x;

    x <== a + b;
    x === 3;
    x === 5;
    o <== x + a;
}

component main = T();

Compile at each optimization level with Circom master at a100fae:

for level in 0 1 2; do
  mkdir -p "/tmp/circom-o${level}"
  circom conflicting_pins.circom --O${level} --r1cs --sym \
    -p goldilocks -o "/tmp/circom-o${level}"
done

Observed constraint counts:

--O0: 4 linear constraints   # contradiction preserved
--O1: 2 linear constraints   # x === 3 is gone
--O2: 0 constraints          # every witness satisfies the R1CS

Expected

x === 3 and x === 5 are contradictory. Every optimization level must preserve an unsatisfiable system, for example by keeping both pins or emitting 1 = 0.

Actual

At -O1, the first pin disappears. At -O2, simplification emits an empty constraint system and turns an unsatisfiable source circuit into a satisfiable R1CS.

Why it happens

Each constant pin becomes a substitution. Fast substitutions are stored in a HashMap keyed by signal, so the later x = 5 substitution overwrites x = 3; the consumed first constraint is never re-emitted.

Impact: underconstraint/soundness for contradictory source circuits. Normal witness generation with sanity checks may still reject, but the exported relation is weaker than the source.

Proposed fix

fix/contradictory-constant-pins at 2c23b2e detects repeated substitutions for the same signal and preserves a contradiction when their constants disagree.

Focused validation:

cargo test contradictory_constant_pins_are_not_overwritten

The regression passes, and git diff --check is clean. Repository-wide formatting was not applied because the upstream checkout has unrelated pre-existing formatting differences.