Chapter 18 — The Verification Loop

A contract is a specification the machine understands. Once you have that, the compiler can do three things with it.

--emit=check: fuzz your contracts automatically

Your contract says what should be true. So the compiler can go looking for an input that makes it false. inglec --emit=check generates many inputs that satisfy a function’s requires, runs the function, and reports the first input that violates an ensures (or an assert) — as a concrete counterexample.

Point it at the (correct) contracts example and everything passes:

inglec --emit=check examples/07_contracts.ig

check gcd: ok (300 cases)
check clamp: ok (300 cases)
checked 2 function(s): 2 passed, 0 failed

Now write a contract that’s a little too hopeful — claiming doubling a number always makes it bigger (false for zero and negatives) — and watch the compiler find the hole:

fn dbl(x: int) -> int
    ensures result > x
{
    return x + x
}

inglec --emit=check bad.ig

check dbl: FAILED
  counterexample: dbl(0)  =>  postcondition failed in 'dbl' (ensures, line 2)
checked 1 function(s): 0 passed, 1 failed

It didn’t just say “this is wrong” — it handed you dbl(0), the simplest input that breaks it. A few things worth knowing: requires defines the valid domain (inputs that fail a precondition are out of scope, not failures); struct and array parameters get fuzzed too; counterexamples are shrunk toward the simplest failing case; and generation is deterministic (a fixed seed), so you get the same counterexample every run — perfect for a regression test, or for a colleague to reproduce.

--emit=prove: prove there’s no counterexample

Fuzzing can find a bug; it can’t certify the absence of one. For contracts in a decidable fragment — linear integer arithmetic over a function’s integer parameters — Ingle can prove the postcondition holds for all inputs, with no external solver:

fn add_nonneg(a: int, b: int) -> int
    requires a >= 0
    requires b >= 0
    ensures result >= 0
{
    return a + b
}

inglec --emit=prove add_nonneg.ig

prove add_nonneg: ensures @line 5 — PROVED
proved 1 of 1 ensures clause(s); 0 to check

The prover is sound and never optimistic: anything outside its fragment (branches, multiplication of variables, calls, non-integer parameters) is reported as not proved and politely handed off to --check. It will never call a false contract proved. Run it on the GCD example, whose loop and % are well outside linear arithmetic, and it says so honestly:

prove gcd: ensures @line 17 — not proved (use --check)

So the workflow is a hierarchy: prove what’s decidable, fuzz the rest, and — next — replay anything that fails.

--emit=replay: make any run reproducible

The bane of debugging is the bug you can’t reproduce. Ingle’s nondeterminism comes from a small, known set of sources — random(), the clock, external reads, and C calls — so the runtime can record every nondeterministic value a run consumes and replay them to reproduce that run exactly. --emit=replay runs your program twice (once recording, once replaying) and checks the two runs are byte-for-byte identical:

inglec --emit=replay program.ig

replay: deterministic — 5 nondeterministic event(s) recorded (5 random, 0 clock, 0 read_line, 0 read_file, 0 ffi); both runs identical

If the two runs disagree, the program has a source of nondeterminism the runtime doesn’t yet capture — which is itself a useful thing to discover. Concurrency comes along for free: replay uses the deterministic serial scheduler, so even a nursery/spawn/channel program replays identically.

Put the three together — prove, check, replay — and you have a closed correctness loop: state what the code should do, have the machine prove it or hunt counterexamples, and reproduce any failure on demand. Plenty of languages offer one or two of these; having all three hang off the same executable contract, in one toolchain, is what Ingle is reaching for.

Fireside trivia. The prover’s engine is Fourier–Motzkin elimination, a method for deciding systems of linear inequalities that Joseph Fourier sketched in the 1820s — yes, the heat-equation, the-frequencies-of-the-universe Fourier — and that Theodore Motzkin rediscovered and formalised in his 1936 thesis. It sat as a piece of pure mathematics for the better part of a century before turning out to be exactly the tool for proving little integer contracts in a programming language two hundred years later. You never know what the maths is for when it’s written down.