Node R1: Represents — packed EVM world to Model.State relation

[Th0rgal]

What this is

Node R1 of the correspondence DAG: the state relation, and nothing else.

Eip8282.Audit.Represents.Represents : Kind → EvmYul.EVM.State → Model.State → Prop

Represents kind s m holds when the world s carries, at the pinned predeploy address for kind, an account that

• runs the pinned runtime bytes (Correspondence.runtimeCode kind),
• whose packed storage is WellFormed (control slots 0–3 plus a dense [QUEUE_HEAD, QUEUE_TAIL) item window), and
• abstracts under WellFormed.toModel to exactly m, balance included.

toModel was already the abstraction function the three registered parents use on a bare Storage. R1 lifts it to a whole EvmYul.EVM.State.

Why it strengthens the three registered parents

P-SUBMIT-1, P-DRAIN-1 and P-CONTROL-1 each quantify over {σ : Storage} (_ : CallHyp kind σ). Nothing in-tree could say which world state a given σ was the storage of. Represents.callHyp closes that gap: a Represents witness supplies the CallHyp kind σ the parents already require, at the predeploy's own storage, so σ can now be named as a real world's predeploy storage instead of a free variable.

No new parent IDs. No changes to audit/guarantees.yaml or audit/assumptions.yaml.

What this is explicitly NOT

R1 relates states, not steps. Nothing here says that if Represents kind s m and Ξ carries s to s', then Represents kind s' (Model.step m k). That ∀-transport is a later node.

Consequently A-ABSTRACT-TX is not closed and not reduced by this PR. The relation now exists and is proved functional and inhabited, but the Ξ ↔ Model.userCall/systemCall step correspondence it would have to be preserved by is still absent. Supplying a hypothesis is not transporting a conclusion.

Non-vacuity

A relation that nothing satisfies would prove anything downstream, so the module carries inhabitation witnesses rather than just the definition:

• represents_packed_deposit / represents_packed_exit — a ∀ over every WellFormed packed image at any predeploy balance, not a single ground world.
• represents_liveStorage, represents_altStorage, represents_inhibitedStorage, represents_depositQueue65, represents_default_storage — the concrete images the registered parents already run against, so Represents is inhabited exactly where the guarantees live.
• Represents.unique — a world abstracts to at most one Model.State. Without this the relation would be useless as a specification.

Honesty marker

default_storage_not_initialExit is proved and kept deliberately: the exits predeploy is specified to start inhibited (Model.initialExit.storedExcess = inhibitor), but an all-zero storage image abstracts to storedExcess = 0. So represents_default_storage at .exit is not a witness that the deployed world starts in Model.initialExit — that needs the constructor image, which is P-CONTROL-1's ctor fragment, not R1.

Receipts

The relation never runs Ξ, so it carries no native_decide receipt. Every new theorem reports only the three foundational axioms, and Trust.lean now checks this:

'…represents_of_lookup'             depends on axioms: [propext, Classical.choice, Quot.sound]
'…Represents.unique'                depends on axioms: [propext, Classical.choice, Quot.sound]
'…Represents.fields'                depends on axioms: [propext, Classical.choice, Quot.sound]
'…Represents.queue_length'          depends on axioms: [propext, Classical.choice, Quot.sound]
'…Represents.inhibited_iff'         depends on axioms: [propext, Classical.choice, Quot.sound]
'…represents_packed_deposit'        depends on axioms: [propext, Classical.choice, Quot.sound]
'…represents_packed_exit'           depends on axioms: [propext, Classical.choice, Quot.sound]
'…represents_liveStorage'           depends on axioms: [propext, Classical.choice, Quot.sound]
'…represents_depositQueue65'        depends on axioms: [propext, Classical.choice, Quot.sound]
'…represents_default_storage'       depends on axioms: [propext, Classical.choice, Quot.sound]
'…default_storage_not_initialExit'  depends on axioms: [propext, Classical.choice, Quot.sound]

No sorry, no project axiom, no native_decide axiom.

python3 scripts/audit_metadata.py → audit-check ok.

make prove receipt is being appended as a follow-up comment; the new module itself builds clean (lake build Eip8282.Audit.Represents → Built Eip8282.Audit.Represents).

Notes for review

• Branched from main 72047231af294022298c86d1c0d7e0f9aff8aaa6; EVMYulLean pin untouched.
• Draft — do not merge.