Isomorph

A bounded equivalence verifier for C#. Give it two implementations of a function and it proves they behave identically for all inputs (up to a bound), or hands back the exact input that tells them apart. Built on Roslyn and the Z3 SMT solver.

Paste in two versions of a function and Isomorph answers a question tests can only sample: are these the same for all inputs (up to a bound)? If they are, it returns a proof of equivalence. If they aren't, it returns a concrete distinguishing input (the array, the number, the flag) that makes them differ. It's a take on regression verification: catching the subtle overflow or off-by-one that a refactor slipped in, with a witness you can drop straight into a debugger.

using Isomorph;

Expr a = new Var("a");

// Proven equivalent over all 32-bit inputs — including wraparound:
EquivalenceChecker.Check(a + a, a * 2).AreEquivalent;      // true

// Not equivalent — with the exact witness:
var r = EquivalenceChecker.Check(a * a, a + a);           // a² vs 2a
r.AreEquivalent;                                          // false
r.Counterexample!["a"];                                   // e.g. 3  (9 != 6)

// …or paste in real C# and let Roslyn read it:
EquivalenceChecker.CheckMethods(
    "int Twice(int x) => x * 2;",
    "int Twice(int x) => x + x;").AreEquivalent;          // true

var bug = EquivalenceChecker.CheckMethods(
    "int F(int x) => x * 3;",
    "int F(int x) => x << 1;");                           // a "shift optimization" gone wrong
bug.AreEquivalent;                                        // false
bug.Counterexample!["x"];                                 // the input that proves it

Platform

CI runs on Windows. On a Linux runner the managed Microsoft.Z3 wrapper resolves against a system libz3 instead of the one the NuGet package ships, and the version mismatch fails every equivalence test with Unable to find an entry point named 'Z3_enable_concurrent_dec_ref'. Forcing native resolution to the package's runtimes/ directory would fix it; that has not been done, so the badge reflects Windows only. The code itself has nothing platform-specific in it.

Scope

This is bounded equivalence checking in the lineage of regression verification (SymDiff, Alive2, CBMC's equivalence mode). It isn't novel research and makes no world-first claim; the value is a clean, correct build with legible counterexamples.

The encoding is overflow-sound: values are two's-complement 32-bit bit-vectors, so a + a and a * 2 are proven equal including their wraparound, an equivalence a naive integer model gets wrong.

The core is a small expression language. From there it grows through a Roslyn front end for a C# subset, SSA, symbolic execution with bounded loop unrolling, and SMT arrays. Each layer carries its own bounds, spelled out in the status list below.

How it works

two expressions ──▶ encode to Z3 bit-vectors ──▶ assert (e₁ ≠ e₂) ──▶ Z3
                                                                        │
                    UNSAT → equivalent                                  │
                    SAT   → decode model → distinguishing input  ◀──────┘

Equivalence is the unsatisfiability of "there exists an input where they differ." When that formula is satisfiable, the model is a concrete counterexample, decoded back into signed 32-bit values.

Status & roadmap

• Expression core. A small integer language (Const, Var, +, −, ×, unary −) encoded to 32-bit bit-vectors. EquivalenceChecker.Check returns equivalent or a decoded distinguishing input, overflow-sound, with property tests (commutativity, associativity, distributivity, a+a == a*2, and a witness that separates a² from 2a)
• Bitwise & shifts. & | ^ ~ << >> (arithmetic, sign-extending; shift counts masked to 5 bits like C#), where overflow-soundness bites: proven a*2 ≡ a<<1, ~a ≡ -a-1, De Morgan, a^a ≡ 0; distinguished a*3 ≢ a<<1 and (a>>1)<<1 ≢ a
• Roslyn front end. Parse a real C# method (a pure int method, expression- or single-return-bodied) into the IR via the Roslyn compiler, so you check equivalence of source you paste in; unsupported syntax raises a clear error. EquivalenceChecker.CheckMethods(src1, src2) parses both and compares.
• Conditionals & comparisons. The ternary c ? t : e and signed comparisons (== != < <= > >=), encoded with Z3's if-then-else. Proves two max / abs / sign implementations equivalent (a>b?a:b ≡ a<b?b:a, and abs even at int.MinValue where both overflow identically), and catches a min-disguised-as-max with a witness.
• Local variables & straight-line SSA. Block bodies with int t = …; declarations, plain and compound assignments (= += -= *= &= |= ^= <<= >>=), and a final return, resolved by substitution, so only the parameters reach the solver. Handles reassignment and a swap-through-a-temp; a bug buried in a block is caught with a witness.
• Control flow (if/else). Symbolic execution over branches: an if duplicates the code after it into both arms (so each arm's assignments flow on and an early return skips the rest) and joins them with a ternary. Proves an imperative max/sign/clamp equal to its ternary form, merges a variable assigned in both branches, and catches a flipped branch with a witness; a path that can fall off the end without returning is rejected.
• Bounded loops. for/while (straight-line bodies) unrolled to a fixed depth (16). A constant-trip loop is checked exactly; a data-dependent loop is checked soundly under a path-guarded assumption that it terminates within the bound (¬(reached ∧ still-looping)), so a loop in one branch never constrains other paths and the checked domain is never silently collapsed. Proves a summation loop equals its closed form, count-up vs count-down loops equal, and catches an off-by-one trip count with a witness.
• Arrays. int[] parameters and a[i] indexing modelled as SMT arrays, over any array and any (symbolic) index. Proves array-access commutativity, a[i]*2 == a[i]+a[i], and (arrays and loops together) a fixed-length summation loop equal to its unrolled form; catches reading the wrong index.
• CLI. isomorph <file1.cs> <file2.cs> prints whether the two methods are equivalent or a distinguishing input, with exit codes (0 equivalent, 1 not, 2 usage/error, 3 unknown)

Soundness

An earlier version had a real soundness hole in the dangerous direction. The bounded-loop termination assumption was asserted as a global constraint built from the post-cutoff state, which for a non-monotonic condition, a divergent loop in one branch, or a conditionally-reached loop silently shrank the checked input domain and reported non-equivalent methods as equivalent. The assumption is now path-guarded, ¬(reached ∧ still-looping), so it only ever excludes inputs that actually reach the loop and overrun it. A pathologically deep expression now raises a catchable error instead of a stack overflow. Each fix carries a regression test.

Command line

Put each method in its own file and ask:

$ isomorph max_a.cs max_b.cs
✓ equivalent — the two methods agree on all inputs (within the analysis bounds)

$ isomorph fast.cs slow.cs
✗ not equivalent — a distinguishing input:
    x = -845571686

Exit codes: 0 equivalent, 1 not equivalent, 2 usage/error, 3 unknown, so it drops into a CI gate.

dotnet run --project src/Isomorph.Cli -- file1.cs file2.cs

Building & testing

dotnet test

Requires the .NET 9 SDK; the Z3 solver comes in via the Microsoft.Z3 NuGet package (native, x64).

License

MIT