Contradictory constant pins are lost during simplification

[NullWitnessZK]

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:

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 on master at a100fae:

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

Expected behavior

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

Actual behavior

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

Root cause

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.

This weakens the exported relation for contradictory source circuits. Normal witness generation with sanity checks may still reject, but the R1CS itself no longer represents the source constraints.

Proposed fix

Draft PR #424 detects repeated substitutions for the same signal and preserves a contradiction when their constants disagree. It includes a focused regression.

Validation:

cargo test contradictory_constant_pins_are_not_overwritten
git diff --check

The focused test passes and git diff --check is clean.