Metadata-Version: 2.4
Name: congruent-eq
Version: 0.0.1
Summary: Prove behavioral equivalence between an original function and an AI-rewritten one within bounds, or return the concrete input that breaks it.
Author: Satchel Hamilton
License: MIT
License-File: LICENSE
Keywords: ai-codegen,bounded-model-checking,equivalence-checking,formal-methods,smt,symbolic-execution,verification,z3
Classifier: Development Status :: 2 - Pre-Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Software Development :: Quality Assurance
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.11
Requires-Dist: z3-solver>=4.12
Provides-Extra: c
Requires-Dist: pycparser>=2.21; extra == 'c'
Provides-Extra: cross-check
Requires-Dist: cvc5>=1.1; extra == 'cross-check'
Provides-Extra: dev
Requires-Dist: hypothesis>=6.100; extra == 'dev'
Requires-Dist: mypy>=1.10; extra == 'dev'
Requires-Dist: pytest>=8.0; extra == 'dev'
Requires-Dist: ruff>=0.5; extra == 'dev'
Provides-Extra: llm
Requires-Dist: anthropic>=0.40; extra == 'llm'
Provides-Extra: oracle
Requires-Dist: numpy>=1.26; extra == 'oracle'
Description-Content-Type: text/markdown

# Congruent

> Given an original function and an AI-rewritten one, **prove** behavioral equivalence within bounds, return the concrete input that breaks it — or admit it doesn't know.

Coding agents refactor, migrate, and "optimize" code constantly. The honest answer to *"did this preserve behavior?"* is usually tests plus vibes. Congruent gives a real answer for a deliberately narrow slice of the problem: **`EQUIVALENT up to bound N`**, **`COUNTEREXAMPLE: <concrete input>`**, or an honest **`UNKNOWN`** — never a guess dressed up as a proof.

It's equivalence checking (the EDA/formal-methods kind) pointed at the problem of trusting AI-generated code.

![Congruent catching a midpoint-overflow bug in an AI refactor](docs/demo.svg)

---

## Scope (read this first)

The credibility of this tool is its honesty about what it does and doesn't do. v1 is intentionally small.

| In scope (v1) | Out of scope (v1 — see [ROADMAP.md](ROADMAP.md)) |
| --- | --- |
| Pure, deterministic functions (no I/O, no global mutation) | Side effects, I/O, concurrency |
| Bounded inputs: machine ints, bools, fixed-length lists, bounded strings | Floating-point exactness |
| Integer/boolean arithmetic, comparisons, branches | Recursion / function calls; unbounded loops (loops are bounded, unrolled to depth `k`) |
| Bounded loops (`return`/`break`/`continue`), unrolled to depth `k` | Heap aliasing, full object semantics |
| A **Python** subset, plus a **C** subset front end | Full language semantics |

Verdicts:

- **`EQUIVALENT up to bound N`** — no diverging input exists within the bound (proven by the symbolic stage; for the current loop-free subset this is complete over all inputs at the chosen width).
- **`COUNTEREXAMPLE: <input>`** — a concrete input where the two functions disagree, with both outputs.
- **`UNKNOWN`** — no counterexample found, but equivalence not proven (e.g. the symbolic stage declined to model something — see below). Never silently upgraded to `EQUIVALENT`.

Congruent never claims unconditional soundness. Every verdict carries its bound and assumptions.

---

## How it works

Cheap checks first, expensive proof only when needed:

1. **Differential testing** (`difftest.py`) — property-based random + boundary inputs. Kills obvious non-equivalence in milliseconds. A counterexample here ends the run.
2. **Symbolic execution → SMT** (`symbolic.py` + `solver.py`) — translate both functions' bounded behavior into logical constraints, assert *inputs equal ∧ outputs differ*, and ask [Z3](https://github.com/Z3Prover/z3). `UNSAT` = equivalent within bound; `SAT` = the model decodes back to a concrete counterexample.
3. **Bounded model checking** — unroll loops to depth `k`, verify up to that bound, report the bound. (Recursion / function calls are out of scope.)

```
input: fn_original, fn_candidate (source) + bound config
  ├─ parse → normalized typed IR        (ir.py)
  ├─ Stage 1: differential tester ──► counterexample? ─► REPORT   (difftest.py)
  ├─ Stage 2: symbolic engine                                     (symbolic.py)
  │     • symbolically execute each fn over fresh symbolic inputs
  │     • collect path constraints + output expressions
  │     • build (inputs equal) ∧ (outputs differ) → Z3 solve      (solver.py)
  │           • UNSAT → EQUIVALENT up to bound N
  │           • SAT   → decode model → COUNTEREXAMPLE
  └─ REPORT (verdict, bound, counterexample, solver stats, caveats)  (report.py)
```

---

## The demo it's built to land

An LLM "simplifies" a midpoint calculation:

```python
# original (correct under fixed-width ints)
def mid(lo: int, hi: int) -> int:
    return lo + (hi - lo) // 2

# candidate (AI "simplification")
def mid(lo: int, hi: int) -> int:
    return (lo + hi) // 2
```

Congruent catches it:

```console
$ congruent original.py:mid candidate.py:mid --bound 8 --int-width 32
COUNTEREXAMPLE  (stage: difftest)
  inputs:    lo = 1, hi = 2147483647
  original:  1073741824
  candidate: -1073741824        # 32-bit overflow in (lo + hi)
  note: 32-bit two's-complement integers
```

And it *proves* the honest rewrites correct — distributivity over modular arithmetic, here, via Z3:

```console
$ congruent original.py:f candidate.py:g          # (x+y)*2  vs  x*2 + y*2
EQUIVALENT  (stage: symbolic, 0.00s)
  equivalent (complete — no bound needed)
  note: 32-bit two's-complement integers
  note: complete: agree on all 32-bit inputs (no loops to bound)
```

Note what that verdict does *not* say: there is no loop and no list here, so the
bound never binds — the pair is decided over the entire 32-bit input space. A
result that genuinely is complete says so, rather than hiding behind a bound.

One screenshot of *proof-or-counterexample on a real AI refactor* communicates the whole value.

It also handles bounded loops. A reversed-accumulation refactor is proven equivalent up to the unroll bound:

```console
$ congruent original.py:f candidate.py:g --bound 8   # sum i  vs  sum (n-1-i)
EQUIVALENT  (stage: symbolic, 0.01s)
  equivalent up to bound 8
  note: 32-bit two's-complement integers
  note: holds within bound: loops up to 8 iterations
```

And you can scope the question with a **precondition** — equivalence often only holds on part of the input domain:

```console
$ congruent ident.py:f abs.py:g                  # x  vs  (x if x>=0 else -x)
COUNTEREXAMPLE  (stage: difftest)
  inputs: x = -1                                 # they disagree on negatives
$ congruent ident.py:f abs.py:g --assume 'x >= 0'
EQUIVALENT  (stage: symbolic, 0.00s)
  note: precondition: x >= 0
```

Declare a precondition inline with a leading `assume(...)` in the reference function, or pass `--assume` on the CLI.

And it reasons about `list[int]` inputs — here it proves a hand-written count equals `len`, for every list up to the length bound:

```console
$ congruent original.py:f candidate.py:g          # len(xs)  vs  count loop
EQUIVALENT  (stage: symbolic, 0.00s)
  note: holds within bound: lists/strings up to length 8, loops up to 8 iterations
```

> **Status: M0–M7 complete, plus the LLM closed-loop stretch.** The differential stage catches counterexamples
> (overflow included) under a fixed-width integer model; the symbolic stage lowers
> both functions to Z3 bitvector expressions and returns `EQUIVALENT` (UNSAT), a
> `COUNTEREXAMPLE` (SAT, decoded to concrete inputs), or `UNKNOWN`. Supported:
> ints/bools, branches, `for ... in range(...)` and `for x in xs` loops (bounded
> model checking) with `return`/`break`/`continue`, `assume(...)` preconditions, and bounded
> `list[int]` both as inputs (`len`, iteration, `xs[i]`) and as **outputs** (build
> and return a list via literals + `+`), and bounded **`str`** (literals, `len`,
> `==`, `+`, indexing incl. Python negative indices, iteration). Out-of-bounds
> access and divide-by-zero are modeled as runtime errors (a rewrite that crashes
> where the original didn't is a counterexample); *falling off the end without
> returning* yields Python's `None` — a value distinct from both a raised
> exception and any returned value. Counterexamples are minimized to the smallest
> failing input. An optional `--cross-check` re-decides each query with CVC5. Benchmarks
> pass with zero unsound verdicts. See [PROGRESS.md](PROGRESS.md) and
> [ROADMAP.md](ROADMAP.md).

---

## Install

Congruent is distributed on PyPI as **`congruent-eq`**; you still `import congruent`
and run the `congruent` CLI.

```bash
pip install congruent-eq
```

Or from source:

```bash
git clone <repo-url> congruent
cd congruent
python -m pip install -e ".[dev]"
```

Requires Python 3.11+. The solver backend is `z3-solver`.

## Usage

```bash
congruent path/to/original.py:func_name path/to/candidate.py:func_name --bound 8
```

| Flag | Default | Meaning |
| --- | --- | --- |
| `--bound N` | `8` | Loop unroll depth and list/string-length bound |
| `--int-width W` | `32` | Bit width for the fixed-width integer model |
| `--assume EXPR` | — | Precondition on the inputs, e.g. `--assume 'n >= 0'` (repeatable) |
| `--no-minimize` | off | Report the first counterexample found, not the smallest |
| `--cross-check` | off | Re-decide with CVC5 and flag any disagreement (needs `pip install "congruent-eq[cross-check]"`) |
| `--timeout S` | `300` | Give up on the solver after `S` seconds and report `UNKNOWN` (`0` = no limit) |

Some queries are genuinely intractable — multiplying unknowns by unknowns in a
loop (a polynomial with symbolic coefficients) is the classic one. `--timeout`
bounds them: the verdict degrades to an honest `UNKNOWN`, never a hang and never
a false `EQUIVALENT`. See [benchmarks/README.md](benchmarks/README.md#the-scaling-edge-measured).

## Layout

```
src/congruent/
  ir.py         # Python AST → normalized typed IR
  cfront.py     # C front end (pycparser → the same IR)
  difftest.py   # differential prefilter + fixed-width concrete interpreter (Stage 1)
  symbolic.py   # symbolic interpreter → Z3 exprs (Stage 2)
  solver.py     # equivalence query, model decoding, minimization
  backends.py   # CVC5 cross-check (independent second opinion)
  equiv.py      # orchestration, escalation, Verdict data model
  report.py     # verdict formatting
  refine.py     # the LLM closed loop (AI proposes → Congruent verifies → feedback)
  cli.py        # `congruent a.py:f b.py:g --bound 8`
tests/          # 229 tests incl. fuzz + oracle soundness guards
examples/       # gallery of realistic AI-refactor pairs (Python + C), runner,
                #   closed_loop_demo.py (offline/--live), live_rewrite.py (your code)
benchmarks/     # recall gate, timing-vs-bound, self-validating fuzzer,
                #   realpy_fuzz.py (semantics oracle), numpy_oracle.py (wrapping oracle)
docs/demo.svg   # the README demo image
docs/live_run.md # captured live-model sessions (caught, corrected, proven)
```

## Gallery

[`examples/`](examples/) holds realistic AI-refactor pairs — faithful rewrites
and subtly broken ones — with Congruent's verdict on each (binary-search
midpoint, clamping, list maximum, sum-to-n, counting). The largest entry,
[`water_bill.py`](examples/water_bill.py), is a ~50-line tiered-billing routine
whose candidate was written by a live model and accepted only after proof; a
second, [`polyval.py`](examples/polyval.py), is **numpy's own Horner loop**
seed-optimized by a live model — both captured in
[docs/live_run.md](docs/live_run.md). Run them all:

```bash
python examples/run_gallery.py
```

## Closed loop: AI proposes, Congruent verifies

The stretch feature ([`refine.py`](src/congruent/refine.py)) closes the loop: an
LLM proposes a rewrite, Congruent checks it, and any counterexample is fed back
so the model can fix its own mistake — repeating until the rewrite is *proven*
equivalent within the bound. **The loop never accepts an unverified rewrite.**

```bash
python examples/closed_loop_demo.py          # offline, deterministic (a scripted LLM)
python examples/closed_loop_demo.py --live   # a real model via the Anthropic API
python examples/live_rewrite.py FILE.py:func # point the live loop at your own code
```

The demo shows Congruent catching a plausible-but-wrong refactor and guiding the
fix — e.g. an agent "simplifies" a midpoint to `(a + b) // 2`, Congruent returns
the exact overflowing input, and the next attempt reverts to the safe form and is
proven equivalent. **This is not hypothetical:** in a live run, a real model
(`claude-opus-4-8`) made exactly that mistake, was handed the overflowing input,
and came back with the proven-safe form — the unedited transcript is in
[docs/live_run.md](docs/live_run.md). The rewriter is pluggable via a `Rewriter`
protocol: `ScriptedRewriter` (offline, used by the demo and tests) or
`AnthropicRewriter` (`pip install "congruent-eq[llm]"`, reads `ANTHROPIC_API_KEY`).

## Benchmarks

```bash
python benchmarks/bench_recall.py     # verdict vs. expectation over the eval set
python benchmarks/bench_scaling.py    # solver time vs. --bound
python benchmarks/fuzz.py             # random pairs, each verdict re-checked
python benchmarks/realpy_fuzz.py      # interpreter vs. real Python (semantics oracle)
python benchmarks/numpy_oracle.py     # wrapping vs. numpy fixed-width ints (overflow oracle)
```

`numpy_oracle.py` needs the `oracle` extra: `pip install "congruent-eq[oracle]"`
(from source: `python -m pip install -e ".[dev,oracle]"`). Everything else in that
block runs on the core install.

`bench_recall.py` exits non-zero if any verdict is unsound (a false `EQUIVALENT`
or false `COUNTEREXAMPLE`), so it doubles as a soundness gate. `fuzz.py` is the
deepest check: it generates random function pairs, asks Congruent, and then
*independently re-validates* each verdict against the concrete interpreter — so a
false verdict fails loudly. It re-verifies clean on the current code (3,000 random
pairs, 0 unsound, at its default settings), and tens of thousands more passed
across seven adversarial audit rounds (plus Z3↔CVC5 cross-checks); a small
deterministic batch runs in the test suite.

Two more oracles validate the interpreter every other check trusts, each against
a reference that shares no code with Congruent — one per half of the fixed-width
model. `realpy_fuzz.py` unparses generated IR back to real Python and diffs the
behavior (this caught the negative-indexing bug both stages shared); it runs wide
so nothing overflows, isolating *semantics*. `numpy_oracle.py` covers the other
half — the two's-complement **wrapping** itself — by re-evaluating random integer
functions with numpy's C fixed-width scalars at small widths where overflow is
the common case; it agrees with the interpreter across 8/16/32/64 (and matches
Congruent's arithmetic *exhaustively* over every 8-bit operand pair, overflow
edges included). Both run a deterministic slice in the test suite.

The measured operating envelope — solver time out to bound 1024, where the
cliff is, and why the default bound is 8 — is documented in
[benchmarks/README.md](benchmarks/README.md#the-scaling-edge-measured).

## Roadmap & progress

- [ROADMAP.md](ROADMAP.md) — milestones M0→M7 and the out-of-scope list as future work.
- [PROGRESS.md](PROGRESS.md) — current state, M0 checklist, and open design decisions.

## License

MIT — see [LICENSE](LICENSE).
