lean-refine

A Lean 4 port of Lammich's monadic refinement calculus — the nondeterminism-with-failure monad nres, ordered so that m ≤ SPEC Φ is the total-correctness Hoare triple, with data refinement ⇓R over coupling relations, and the rules that let an abstract algorithm's correctness proof be an artifact separate from — and reusable across — the representations that implement it.

The namespace is Refine; the reference is Peter Lammich's Isabelle/HOL Refine_Monadic (AFP). Mathlib is the only dependency.

Extracted from zip-2005-asm, where it was built as the L3 layer above a Myreen-style decompilation of a RISC-V guest, and where its first consumer still lives.

lake exe cache get                    # Mathlib oleans; without it, an hour
lake build                            # 446 jobs, zero warnings
scripts/check-axioms.sh               # 104 declarations, three classical axioms
scripts/check-forbidden-tactics.sh

ROADMAP.md is the queue and the honest list of what is missing. This file is the contract.

What is here

Module	What it is
Refine.Nres	The monad. Nres, fail/res/succeed, spec, ret, bind, nofail, Mem; le_spec_iff and its two regressions; bind_mono, bind_le_spec; assert/assume'.
Refine.Algebra	The monad laws and the completeness of the VCG rule: bind_le_spec_iff, bind_ret_right, bind_assoc, and the iSup_res characterization they rest on.
Refine.DataRefine	Data refinement. conc (notation ⇓), conc_mono, conc_conc, le_conc_spec_iff; coupling relations br, with build_rel_spec_conv and three non-vacuity witnesses.
Refine.While	The total-correctness loop. whileT, the fixpoint equation whileT_eq, whileT_rule and its Nat-measure form, terminates_of_measure. No fuel.
Refine.Rules	The refinement rules: bind_refine (heterogeneous, reachability-restricted) and whileT_refine (no termination hypothesis on either side).

RefineTools is build-time tooling — the axiom gate — and no theorem imports it.

The one thing to get right

m ≤ m' means m refines m': m is the more defined, more deterministic one. So FAIL is the top element — a computation that may fail is the least informative, not the most. Under that order

m ≤ SPEC Φ   ⟺   m does not fail, and every result of m satisfies Φ

which is the total-correctness triple. Refine.le_spec_iff is that sentence as a theorem.

This is the one thing that would be silently catastrophic to get backwards. If the order were flipped, FAIL ≤ SPEC Φ would hold, every triple would be provable, and every later lemma in the development would still typecheck. fail_not_le_spec and fail_not_le_spec_true are the standing regressions — the second because a flipped order is most likely to survive scrutiny at Φ = fun _ => True, the case where "every result satisfies Φ" says nothing and only nofail is doing work.

What the layer buys

Refining a specification is one inequality: ⇓R plus monotonicity. Refining a program is the thing worth having — take an abstract algorithm, replace its state by a concrete representation, replace each step by a concrete step, and conclude that the concrete program refines the abstract one without redoing the abstract correctness proof. That is what bind_refine and whileT_refine are for, and it is why Lammich's case studies can "reuse the existing abstract algorithms and correctness proofs unchanged".

Two shape decisions in those rules were forced rather than chosen, and are worth knowing before you use them:

• bind_refine is heterogeneous — the two continuations may return different types, coupled by a second relation. A homogeneous version cannot refine a loop, whose two sides carry their own state types.
• Its continuation obligation is restricted to reachable abstract values. In whileT_refine the induction hypothesis is available exactly for the abstract successors, not for arbitrary states; quantifying over all of them would be a premise no caller could supply. The AFP restricts it for the same reason. bind_refine_all is the unrestricted form for callers who can supply it.

whileT_refine needs no termination hypothesis on either side. The induction runs on the abstract loop's termination derivation, so the concrete loop's termination is a conclusion — the usable direction, since a concrete loop over a limb representation has no obvious well-founded relation of its own. The abstract side needs none either: a non-terminating abstract loop is FAIL, ⇓R FAIL is FAIL, and everything refines FAIL.

No fuel

Termination is carried by a well-founded relation, never by a step budget. whileT_rule takes a WellFounded R, an invariant preserved by the body, and a body that decreases R; whileT_rule_measure is the Nat-measure form a decompiled loop actually arrives in.

Threading fuel through a calculus is a mistake that is expensive to undo, and a data-dependent trip count cannot be written as a literal anyway. Note also that one well-founded induction proves termination and the postcondition together: a caller does not discharge termination separately from correctness, and nofail (f s) falls out of the body's ≤ SPEC obligation via le_spec_iff rather than being a side condition.

Trust

lake build is clean at 446 jobs with zero warnings. scripts/check-axioms.sh audits 104 declarations, of which 84 rest on some axiom, and the set is exactly Lean's three classical axioms:

propext            84 declarations
Classical.choice   80
Quot.sound         82
offenders           0

No sorry, no axiom, no native_decide, no bv_decide. The axiom gate is a policy gate rather than a name baseline, and it earns its keep here specifically because Mathlib is the dependency: Mathlib rests on the same three axioms, but that is a property of Mathlib rather than a promise it makes to us, so a bump that changed it fails the build here instead of being discovered downstream.

What is not reduced: the correctness of Lean and of Mathlib's order library, and the faithfulness of the port itself to the AFP entry — which is prose and a correspondence table (ROADMAP.md), not a theorem.

Building on it

The calculus deliberately stops short of the machine. hn_refine — the code-facing predicate that lands a refinement on a machine-code triple — cannot be stated without naming a machine, so it belongs in the consumer. zip-2005-asm's RefineAsm.hnrAsm is the first, landing on a Decomp.cpsTotal from riscv-decomp.

The shape a downstream project instantiates:

1. State the algorithm abstractly in Nres, over whatever types are convenient. Prove it meets its specification: m ≤ spec Φ.
2. Choose the concrete representation and write the coupling relation, usually br abs I — an abstraction function plus a concrete invariant, neither total nor surjective.
3. Refine step by step with bind_refine and whileT_refine, obtaining mc ≤ ⇓R m. The step-1 proof is not touched.
4. Compose: conc_mono and conc_conc carry it, and build_rel_spec_conv is the lemma the specification boundary needs.
5. Land it on whatever your machine layer is, with your own hn_refine.

Steps 1 and 3 being independently checkable artifacts is the entire point; if a slice ends up proving one theorem that mentions both the machine and the abstract postcondition, the abstraction has collapsed.

Provenance

Written as milestone M6 of zip-2005-asm and extracted here at that repository's 10c8cc6. The library arrived in four reviewed pull requests plus their review responses, and the review commits are worth finding, because three of them changed a definition rather than a comment:

upstream PR	commits	what landed
#34	dd9242f	the monad, the order, ⇓R/br, le_spec_iff
#35	3cefea9, 4c04283	whileT and its rule; then the actual fixpoint equation, after review found the first one characterized an exit set and had been named for a lemma it was not
#36	8265830, a1d3025, 3409a53	VCG completeness and the monad laws; bind_ret corrected from rfl to simp
#37	6983852, e508901	the refinement rules; then the termination premise on whileT_refine dropped as slack, and the witness rewritten after review showed the invariant was not load-bearing

References

Cite these, not refine_tutorial.html — it is a landing page with no technical text.

• ITP'15, Refinement to Imperative/HOL
• AFP, Refine_Monadic
• AFP, Refine_Imperative_HOL
• refine_slides.pdf

Licence

None yet — ask before depending on this.