Language-soundness metatheory (src/abi/Lang/*): follow-ons toward verified extraction

[hyperpolymath]

Context

PRs #73–#77 landed a machine-checked metatheory of the constrained form under src/abi/Lang/ — a faithful Idris2 model of lib/ast.ml / lib/eval.ml / lib/constrained_check.ml, all idris2 --build-verified with zero escape hatches (no believe_me/postulate/assert_total/partial/holes):

Module	Proved
Lang.Eval	termination — the evaluator is total: call-free (Slice 1), then full language via the rank-stratified evalLevel over the acyclic call graph (Slice 2)
Lang.Checker	checker soundness — a Ranking rules out direct & mutual recursion (Slice 3)
Lang.Reversible	inverse is an involution on incr/decr/swap; assign is the irreversible echo[A,B] boundary (Slice 4)
Lang.Resource	static resource budget = accountability-trace length, both total (Slice 5)

This closes the gap identified earlier — the constrained form's four advertised guarantees (termination, static resource bounds, reversibility, accountability) are now proven, not just checked — over the model.

Follow-ons (model → the OCaml itself)

• 3b — checker completeness. Mechanize the OCaml DFS cycle-detector and prove validate_program p = [] ⇒ Ranking p (the existence of a ranking from acceptance, via topological sort). Slice 3 proved the dual (Ranking ⇒ no recursion); the forward construction is open (graph-algorithm reasoning).
• 4b — general semantic reversibility. Lift the concrete reversibility witnesses to a general (all-variable) theorem over a lawful / DecEq-keyed store. Blocked for primitive String names (x == x doesn't reduce for a variable x); holds for any DecEq-reducing name type / lawful store interface.
• 5b — runtime-trace faithfulness. A trace-producing evaluator whose emitted trace realizes staticTrace (with the one-branch-per-if refinement), tying oblibeny --dump-trace to the static skeleton already proved.
• Verified extraction (research-scale). Relate the OCaml lib/* to the Idris2 model — translation validation or codegen — closing the model-fidelity gap entirely. The honest endpoint; not a single slice.

Refs

Modules Lang.{Eval,Checker,Reversible,Resource,Syntax}; PRs #73, #74, #75, #76, #77.