Frame rule, footprint computation, and coupling invariants for the IR interpreter

[Th0rgal]

Generic frame infrastructure for the IR interpreter (frame rule, footprint computation, coupling invariants)

Context

The SPHINCS- retro-verification work (lfglabs-dev/SPHINCS-, pinned at e62d833a) proves that hand-transcribed Yul models refine functional specs by symbolically executing execStmt/execStmts over RuntimeState (Compiler/Proofs/IRGeneration/SourceSemantics.lean). The proofs blow up to 20-30 GB RSS, and three composition steps could not be elaborated under a 32 GB cap at all; they remain axioms on that repo's main (discharge attempt: lfglabs-dev/SPHINCS-#9).

The root cause is structural, not incidental: the transcribed Yul is one flat block, so every lemma about a code segment must describe the full concrete interpreter state at its boundary (a memory layout of 0x5A0+ bytes with symbolic contents). Pinning a generic lemma to such a state triggers huge defeq/unification problems, and the elaborator keeps every intermediate goal alive until the theorem closes.

The SPHINCS- repo worked around this with hand-rolled, per-statement, per-state-field frame lemmas: SphincsMinusVerifiers/MemoryFrame.lean, StateFrame.lean, BindingFrame.lean, RootFrame.lean, MemoryKit.lean. These are prototypes of infrastructure that belongs in Verity itself. This issue specifies that infrastructure.

What to add

All of the following is generic over Stmt/Expr/RuntimeState and should live under Compiler/Proofs/ in this repo. Nothing here mentions SPHINCS or any particular contract.

1. A resource algebra over RuntimeState

A type Resource describing disjoint pieces of interpreter state, at minimum:

• mem (lo hi : Nat): the byte range [lo, hi) of world.memory
• binding (name : String): one named local in bindings
• static: the read-only fields (selector, world.calldata)

with a disjointness predicate Disjoint : Resource -> Resource -> Prop and a satisfaction predicate OwnedEq (r : Resource) (st st' : RuntimeState) : Prop stating that st and st' agree on r. This replaces the current ad hoc PreservesSelectorCalldata, per-cell (s'.world.memory addr).val = (st.world.memory addr).val, etc.

2. A footprint function with a soundness theorem

def Stmt.writeFootprint : Stmt -> Option (List Resource)

returning an over-approximation of the resources a statement may write (none when not syntactically analyzable, e.g. a store at a fully dynamic offset). Most offsets in assembly-style models are literals or affine in a loop counter, so the function should evaluate offsets through a partial constant/affine evaluator over Expr.

Soundness theorem (the frame rule), proved once by induction on execStmt/execStmts:

theorem frame_rule
    (prog : List Stmt) (st s' : RuntimeState) (r : Resource)
    (hfp : Stmt.writeFootprint-based disjointness of r from prog)
    (h : execStmts [] st prog = .continue s') :
    OwnedEq r st s'

Acceptance criterion: "this 40-statement segment does not touch scratch cell 0x40" must be dischargeable by decide-style computation on the footprint plus one application of frame_rule, with no per-statement manual lemma. This single theorem subsumes the entire cartesian product currently spelled out by hand in the SPHINCS- repo (statement kind x state field).

3. Coupling invariants as first-class objects

A simulation interface for refinement proofs:

structure Coupling (Abs : Type) where
  Inv : RuntimeState -> Abs -> Prop

def SegmentSim (c : Coupling Abs) (prog : List Stmt) (f : Abs -> Abs) : Prop :=
  forall st a s', c.Inv st a -> execStmts [] st prog = .continue s' -> c.Inv s' (f a)

with composition lemmas:

• sequential: SegmentSim c p f -> SegmentSim c q g -> SegmentSim c (p ++ q) (g ∘ f)
• loop: a forEach/loop rule lifting a body simulation to the whole loop with the iteration count threaded through f
• weakening/strengthening between couplings, and a rule combining SegmentSim on owned resources with frame_rule on the rest

This lets a retro-verification state its cutpoint lemmas as small Inv before -> Inv after simulations instead of equalities between full concrete states, which is where the elaboration cost currently concentrates.

4. Tactic support

A tactic (or simp set plus macro) frame that, given a goal of the form OwnedEq r st s' or a hypothesis execStmts [] st prog = .continue s', computes the footprint, discharges the disjointness side conditions by decide/norm_num, and applies frame_rule. The analogue of Iris's iFrame, scoped to this interpreter.

Validation target

Port one of the three residual SPHINCS- composition steps (for example c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0, see lfglabs-dev/SPHINCS-#9 for its statement) to the new interface and confirm it elaborates within the 32 GB cap. The hand-rolled *Frame modules in that repo should become deletable once this lands.

Non-goals

• No change to execStmt/evalExpr semantics or to the EVMYulLean builtin backend.
• No full separation logic with magic wands or step-indexing; plain disjointness over a first-order resource type is sufficient for assembly-style straight-line code with static offsets.
• Proof-by-reflection of whole-program execution is a separate (complementary) track, not this issue.

[Th0rgal]

Re-scoping proposal based on the 2026-06-12 Morpho fidelity analysis (Th0rgal/morpho-verity): this issue now has a concrete acceptance test.

Target: Morpho Blue Proofs/Disciplines.lean local-axiom count → 0. The axioms a frame rule + footprint computation must be able to discharge:

• MonotoneDiscipline / GuardedDiscipline (generated-body field movement)
• AccrueInterestIdentityFor
• ExecutableMarketIdReadAligned / ExecutableOraclePriceReadAligned
• LocalNoOverflowFor ×4 — tracked separately in feat(Codegen,Proofs): automatic checked-arithmetic obligations (solc 0.8 overflow semantics) #1993 (auto-derived overflow obligations)
• Loc.slot_inj — tracked separately in proof: discharge Loc.slot_inj keccak non-collision axiom via layout certificates #2001 (layout-certificate discharge)

Suggested split to keep PRs reviewable:

1. Frame rule over the IR interpreter, building on the PreservesBindingsExcept/PreservesSelectorCalldata combinators just merged in Add minimal generic EVM Frames for climb/loop proofs (least surface) #1983 (Compiler/Proofs/Frames.lean).
2. Footprint computation (syntactic read/write set per generated body) + soundness theorem.
3. Coupling invariants consuming 1+2.

The consumer issue is #1994 (generated-body execution summaries); #1895 covers the annotation half. Anchoring each piece to a named Blue axiom should prevent scope drift.