Semantic Equivalence Verifier

→ behavior-preservation-checker tests on a sample; this skill proves over the full input space. Use when "we ran it on 500 inputs" isn't enough.

When proof beats testing

Proof strategies — pick by code shape

Step-by-step — SMT-backed equivalence (common case)

1. Translate both fragments to a common logical form. Same input variable names, same state model.
2. Assert the preconditions: assume(pre(x)).
3. Assert inequivalence of outputs: assert(old_out != new_out).
4. Solve. If UNSAT → no input makes them differ → equivalent. If SAT → the model is a counterexample.

For loops: replace the loop with its invariant. You need the invariant to be the same for both versions (or for one to imply the other).

Worked example

Old:

int abs_old(int x) {
    if (x < 0) return -x;
    return x;
}

New (branchless):

int abs_new(int x) {
    int mask = x >> 31;
    return (x + mask) ^ mask;
}

Encode (SMT-LIB, bitvector theory):

(declare-const x (_ BitVec 32))
(define-fun old () (_ BitVec 32)
  (ite (bvslt x #x00000000) (bvneg x) x))
(define-fun new () (_ BitVec 32)
  (let ((mask (bvashr x #x0000001f)))
    (bvxor (bvadd x mask) mask)))
(assert (not (= old new)))
(check-sat)

Solve: unsat. Equivalent for all 32-bit inputs. ∎

But wait — what about INT_MIN? -INT_MIN overflows in C (UB). The SMT encoding uses modular arithmetic, so bvneg(INT_MIN) = INT_MIN, and both versions return INT_MIN. Equivalent, including at the UB point — they both return the wrong thing. The proof shows equivalence, not correctness. If you need correctness, add (assume (not (= x INT_MIN))) or prove against the spec result ≥ 0.

When proof fails

Limits — when to fall back to testing

• Heavy heap mutation → state space explodes
• Floating point → solvers handle it but slowly and with surprising edge cases (NaN, -0.0)
• External calls → can't symbolically execute what you don't have the body of
• Code > ~500 lines → decompose or give up on full proof; → behavior-preservation-checker with heavy fuzzing

Do not

• Do not claim equivalence without stating the precondition. "Equivalent for all inputs" and "equivalent for non-null inputs" are different theorems.
• Do not confuse "equivalent" with "correct." Two functions can be identically wrong. Equivalence is A↔B; correctness is A↔spec.
• Do not trust a proof of a hand-translation. If you translated the code to SMT-LIB by hand, the bug might be in the translation. Use a trusted frontend (→ python-to-dafny-translator, CBMC's C frontend) when possible.

Output format

## Claim
old: <fragment>
new: <fragment>
Equivalent under precondition: <P(x)>

## Proof strategy
<SMT | induction | simulation>

## Result
<PROVEN EQUIVALENT | COUNTEREXAMPLE: x=<val>, old=<o>, new=<n> | UNKNOWN — <why>>

## Trust base
<what the proof relies on: solver correctness, translation fidelity, axioms assumed>