feat(evm): F4c observation and frame lemmas

[Th0rgal]

Summary

Adds EvmYul/EVM/Proof/Observation.lean: the observation and frame lemmas a later Ξ correspondence proof consumes. Builds on the X decomposition landed in #5 (F4a).

A correspondence proof rarely needs a whole post-state — it needs to know what an instruction can be observed to change, and far more often what it cannot. Both halves are supplied for the instructions whose effects are localized: SSTORE, MSTORE, MSTORE8, LOG0–LOG4, RETURN, REVERT.

What's in it

• Ordering instances for UInt256 keys. Storage is Std.TreeMap UInt256 UInt256 compare, but the derived Ord UInt256 carries no lawfulness instances, so no Std.TreeMap lookup lemma applied to it. OrientedCmp/TransCmp/ReflCmp/LawfulEqCmp (plus LawfulBEq) are discharged by reducing compare on UInt256 to compare on its Fin value. Without these, no statement about a single storage key is provable at all.
• Storage key locality. Account.updateStorage is not a plain insert — writing zero erases the key, keeping storage in the canonical form the state root is computed from. Both branches are shown key-local, and both agree with lookupStorage at the key written, which is what makes the distinction invisible to an observer.
• SSTORE frames. sstore writes the key, warms (Iₐ, k) and moves the refund counter at once; only the first is observable as storage. Hence storageAt_sstore_self, storageAt_sstore_of_ne_key, storageAt_sstore_of_ne_addr, lookupAccount_sstore_of_ne, and sstore_logSeries / sstore_executionEnv / sstore_σ₀.
• Unrelated accounts. lookupAccount_setAccount_of_ne is the frame that makes "unrelated accounts are untouched" provable; State.storageAt names the observation an SLOAD would make.
• Step equations + frames for the memory, state and log combinators, factored through three named post-states (afterMachineOp, afterStateOp, afterLogOp) so each frame is proved once per family rather than once per opcode.
• X-level consequences. X_RETURN / X_REVERT fix X's result outright, with the returned bytes a named slice of the pre-state's memory rather than an existential. xStepAt_* for SSTORE, MSTORE, MSTORE8 and LOG0–LOG4 give the non-halting iterations.

Notes

• The step equations are stated for a state written { pre with stack := … } rather than an arbitrary pre constrained by pre.stack = …. That is not cosmetic: with the stack a literal, the popₙ in the operation's implementation reduces and the equation closes by rfl; behind a hypothesis it does not reduce and the proof has to fight X's CREATE/CALL branches. The hypothesis form callers want is derived from it.
• sstore's refund arithmetic is deliberately not pinned down — none of the observations depends on it.
• No sorry, no new axiom. #print axioms on the headline lemmas reports only propext, Classical.choice, Quot.sound.

Scope stops short of the full Ξ correspondence; this is the lemma set F4d/R1 build on.

Test plan

• lake build EvmYul.EVM.Proof.Observation — green
• lake build (full, 1120 jobs) — green
• #print axioms on storageAt_sstore_of_ne_key, storageAt_sstore_of_ne_addr, lookupAccount_sstore_of_ne, storageAt_sstore_self, sstore_logSeries, X_RETURN, X_REVERT, xStepAt_SSTORE, xStepAt_LOG4, afterLogOp_logSeries — standard axioms only