G2 / Class B: lift E2-E7 + F2-F7 + true S8 to unconditional via per-BridgedStraightStmt observation framework

[Th0rgal]

Context

Follow-up to merged #1857 (which closed #1737 — the EVMYulLean transition itself). After #1857, the trust boundary is established and the native EvmYul.Yul.callDispatcher is the sole runtime authority for the supported fragment. The legacy reference-oracle stack is removed. Concrete deployed contracts (Storage.sol, SimpleStorage.sol, etc.) are verified unconditionally.

The work that remains is lifting a class of internal helper theorems from conditional to unconditional form. This does not change the trust boundary or the public surface — concrete contract correctness is already unconditional in #1857 — but it removes hypotheses from internal building blocks so that future user-body shapes drop out automatically without manual continuation provision.

Theorems that are currently conditional

In Compiler/Proofs/EndToEnd.lean:

• NativeGeneratedSelectorHitSuccessBridge.of_leave_body (E2) — takes hCont : LeaveAwareCallDispatcherContinuation
• NativeGeneratedSelectorHitSuccessBridge.of_block_leave (E4) — same
• NativeGeneratedSelectorHitSuccessBridge.of_nativePreservableStraightStmts_leave (E6, degenerate) — same
• NativeGeneratedSelectorHitSuccessBridge.of_bridgedStraightStmts_falling_through E7 — same
• NativeGeneratedSelectorHitSuccessBridge.of_leave_body_with_label_prefix (F2)
• NativeGeneratedSelectorHitSuccessBridge.of_block_leave_with_label_prefix (F4)
• NativeGeneratedSelectorHitSuccessBridge.of_nativePreservableStraightStmts_leave_with_label_prefix (F6, degenerate)
• F7 (degenerate, delegates to F2)
• True S8: compile_preserves_native_evmYulLean_of_compile_ok_supported_generated_callDispatcher still has hUserBodyHalt premise. The strengthened private _via_result variant already takes the unified Result bridge.

All of these compile and are correct under their hypotheses. They are not yet useful for new dispatcher-emitted body shapes without manual continuation provision.

Why it's blocked

The LeaveAwareCallDispatcherContinuation provider needs to discharge the _revived form of NativeBlockPreservesWord on the user-body, including Leave-ending bodies. The OLD-form NativeBlockPreservesWord provider in nativeGeneratedCallDispatcherResult_selector_hit_ok_matchesIR_forall_of_compile_ok_supported works for Ok-shaped finals but fails for Checkpoint-Leave finals (because final[name]! returns default for Checkpoint states — see memory yul-state-lookup-bracket-vs-lookup). The _revived form via final.reviveJump[name]! succeeds on Checkpoint Leave but proving it directly requires the per-BridgedStraightStmt IR↔native observation-equivalence framework which does not exist yet.

Scope estimate

• Framework: ~300–500 LoC, ~2–4 weeks.
• Parallel _revived dispatcher continuation provider: ~700 LoC, ~3–7 days once framework lands (mirrors nativeGeneratedCallDispatcherResult_selector_hit_ok_matchesIR_forall_of_compile_ok_supported).
• Wiring E2-E7 + F2-F7 + true S8 to drop LeaveAwareCallDispatcherContinuation / hUserBodyHalt: ~1–3 days.

Design path

See memory entry per-stmt-observation-framework-design.md (in .claude/projects/-workspaces-mission-de9e924b/memory/) and related design notes:

• yul-state-lookup-bracket-vs-lookup
• revived-chain-universal-discharge (closed in G1 S5-S8 stage 2: D1/D2 + E2-E7 success bridges + S8 dispatcher refactor #1857)
• leave-preservation-blocker
• per-stmt-observation-framework-design (open)

Phase 1: Define statesAligned : IRState → Yul.State → Prop and resultsAligned : IRExecResultWithInternals → Except Yul.Exception Yul.State → Prop. These currently do not exist as top-level abstractions — alignment is woven case-by-case through existing proofs.

Phase 2: Define NativeStraightStmtObserved (stmt : YulStmt) (codeOverride : Option YulContract) : Prop and prove for each of the ~20 constructors of NativePreservableStraightStmt (Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean:18510):

• Easy (~30 LoC each, ~5 constructors): comment, expr_stop, expr_return, expr_revert.
• Medium (~50 LoC each, ~10 constructors): let_, assign, expr_sstore, expr_mstore, expr_tstore, expr_mstore8, expr_log0..log4.
• Hard (~80 LoC each, ~5 constructors): letMany, expr_calldatacopy, expr_returndatacopy, generic expr_call.

Phase 3: Inductive step over NativePreservableStraightStmts.

Phase 4: Use the framework to discharge D1/D2/E6/E7 narrowing, then build the parallel _revived dispatcher continuation provider, then drop hCont / hUserBodyHalt from the affected theorems.

Success criteria

• Every NativeGeneratedSelectorHitSuccessBridge.of_* constructor in EndToEnd.lean is unconditional (no hCont / hExecBridge / LeaveAwareCallDispatcherContinuation hypothesis).
• compile_preserves_native_evmYulLean_of_compile_ok_supported_generated_callDispatcher (true S8) lands without hUserBodyHalt.
• git grep -n LeaveAwareCallDispatcherContinuation returns only the definition + the framework's provider (no leftover hypothesis sites).
• All sorry/axiom counts unchanged or reduced.
• lake clean && lake build green; make check green; full CI green.

Related

• Follows up Target native EVMYulLean runtime for generated Yul #1737 (closed by G1 S5-S8 stage 2: D1/D2 + E2-E7 success bridges + S8 dispatcher refactor #1857)
• Stacked on G1 S5-S8 stage 2: D1/D2 + E2-E7 success bridges + S8 dispatcher refactor #1857 merged commit (look for branch native-evmyullean-g1-s5-s8-stage2)
• Related memory entries in .claude/projects/-workspaces-mission-de9e924b/memory/

[Th0rgal]

Status update from interrupted Codex run:

• Checked out existing local branch issue-1884-observation-framework at stacked base origin/native-evmyullean-g1-s5-s8-stage2 (34f45b95).
• Read Compiler/Proofs/EndToEnd.lean around LeaveAwareCallDispatcherContinuation, E2/E4/E6/E7/F2/F4/F6/F7, and true S8, plus the design memories per-stmt-observation-framework-design, yul-state-lookup-bracket-vs-lookup, leave-preservation-blocker, and revived-chain-universal-discharge.
• Found an existing Phase 1 scaffold in Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean defining stateVarsAligned, stateStorageAligned, statesAligned, resultsAligned, NativeStraightStmtObserved, and NativeStraightStmtsObserved.
• The scaffold initially did not typecheck (GetElem? inference on revived state lookup and unopened execIRStmtWithInternals / execIRStmtsWithInternals). I fixed those local issues; lake env lean Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean now completes, with only pre-existing unused-simp warnings.

I am stopping here rather than opening an incomplete PR: Phases 2-4 are still not implemented. In particular, no per-constructor NativeStraightStmtObserved proofs, no list induction over NativePreservableStraightStmts, no revived dispatcher continuation provider, and no removal of hCont / hUserBodyHalt from EndToEnd.lean have landed. The current state therefore does not meet the issue DoD and has not been pushed as a PR.

[Th0rgal]

Status update from the observation-framework attempt:

I got as far as proving out the needed lower dispatcher direction conceptually, but the current revived-store approach hits a semantic blocker in the native switch lowering.

The missing layer is a revived analogue of the generated switch/case/default execution chain in Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean, needed so LeaveAwareCallDispatcherContinuation can be provided internally instead of passed as an assumption. A worker patch attempted this, but the key suffix/default skip lemmas are not true under the current interpreter semantics:

• NativeBlockPreservesWord_revived observes final.reviveJump[matchedName]!, which correctly sees the inner store of Checkpoint (.Leave shared store).
• The generated suffix/default guards execute after the selected body and evaluate raw state[matchedName]!, not state.reviveJump[matchedName]!.
• For Checkpoint, raw GetElem! is governed by State.store = default / checkpoint lookup behavior, while reviveJump reads the saved inner store.
• Therefore a body ending in Leave can preserve the matched flag in the revived predicate but still does not justify the later generated switch guards skipping.

Concrete failed proof points in the attempted patch were revived versions of:

• exec_nativeSwitchCaseIfs_matched_fuel
• exec_nativeSwitchCaseIfs_with_default_matched_fuel

A broad helper like state.reviveJump[name]! = state[name]! is false for Checkpoint, so the proof cannot be repaired by rewriting revived lookup back to ordinary lookup.

No PR was opened from this attempt, and the main feature branch was left clean. The likely next design step is to avoid executing generated suffix/default guards after a selected body has produced a checkpoint, or add a lower-level theorem that treats checkpoint results as terminal for these generated switch tails instead of requiring raw matched-flag guard evaluation after the checkpoint.

[Th0rgal]

Additional validation after the earlier status note:

I checked whether a narrower proof-only terminal-tail lemma could avoid the raw matched lookup after Leave. The existing switch-tail theorem stack does not support that:

• exec_nativeSwitchCaseIfs_head_hit_fuel, exec_nativeSwitchCaseIfs_prefix_hit_fuel, exec_nativeSwitchCaseIfs_find_hit_fuel, exec_nativeSwitchDefaultIf_matched_fuel, and exec_nativeSwitchCaseIfs_with_default_matched_fuel all require raw final[matchedName]! = 1.
• The closest lower wrapper, exec_lowerNativeSwitchBlock_selector_find_hit_finalMatched_store_fuel, also requires an explicit raw final matched fact.
• The revived preservation lemmas correctly handle Leave, but only through final.reviveJump[matchedName]!, not raw final[matchedName]!.

This is not just a missing bridge theorem: NativeStmtPreservesWord_revived_leave already documents the core reason the old/raw form is structurally false. For Checkpoint (.Leave shared store), raw bracket lookup follows the checkpoint/default-store path, while reviveJump reads the saved inner store. So deriving the raw matched fact needed by the generated switch suffix/default guards from revived preservation would be unsound.

I also verified with a tiny interpreter reduction that Leave followed by a later Let leaves the checkpoint unchanged, but raw bracket lookup on a checkpoint variable goes through Lean's GetElem! invalid path rather than the saved store. That matches the proof failure and rules out a clean proof-only terminal-tail lemma over the current generated guards.

At this point the remaining viable fixes appear to require a semantic/lowering design decision outside the current DoD shape, such as changing how block execution treats checkpoints or changing the native switch lowering so selected-body Leave cannot be followed by generated guard evaluation. I have not made such a change because it would be broader than the requested proof/framework lift and risks crossing the current public trust-boundary constraints.

[Th0rgal]

Status update after resuming on latest origin/main (edd145e6, includes #1883/#1886/#1887/#1888):

• Rechecked the G2 / Class B: lift E2-E7 + F2-F7 + true S8 to unconditional via per-BridgedStraightStmt observation framework #1884 proof path around LeaveAwareCallDispatcherContinuation, NativeBlockPreservesWord_revived, and the generated native switch-tail lemmas in Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean / Compiler/Proofs/EndToEnd.lean.
• The old blocker still appears to be the decisive one: LeaveAwareCallDispatcherContinuation is intentionally stated over NativeBlockPreservesWord_revived, so the selected body can be observed through final.reviveJump[...] after Leave; however the generated switch suffix/default machinery still requires raw matched-flag facts like final[matchedName]! = 1 via lemmas such as exec_nativeSwitchCaseIfs_matched_fuel and exec_nativeSwitchCaseIfs_with_default_matched_fuel.
• For checkpoint/leave states, a general bridge from final.reviveJump[matchedName]! = 1 to raw final[matchedName]! = 1 is not sound. This matches the earlier failed revived switch-tail attempts and means the requested unconditional provider cannot be completed as a proof-only observation-framework lift without changing the native switch-tail semantics/lowering or adding a terminal checkpoint-aware dispatcher theorem.
• I did not open a PR or merge the partial Phase 1 scaffold, because the DoD requires removing the continuation hypotheses and true S8 premise, and this blocker prevents that under the current design constraints.

Stopping here per the issue goal instruction: if blocked, post status and stop.

[Th0rgal]

Closing this broad proof-observation issue as superseded by the narrower blocker in #1890.

The latest proof investigation showed the important obstacle is not the full generic observation framework; it is checkpoint-aware native switch-tail semantics/lowering, specifically raw matched-flag lookup after Leave checkpoints. #1890 captures that smaller proof/code contract directly. Once #1890 lands, the remaining E/F/S unconditional-lifting work should be small enough to track as follow-up proof cleanup instead of keeping this umbrella open.

[Th0rgal]

Blocker found while implementing the reviveJump observation-boundary stack.

I tested the existing WIP approach that adds exec_nativeSwitchCaseIfs_*_revived lemmas and routes exec_lowerNativeSwitchBlock_selector_find_hit_* through NativeBlockPreservesWord_revived. The first required skip lemma has this shape:

state.reviveJump[matchedName]! = 1 ->
  exec ... (.Block (nativeSwitchCaseIfs discrName matchedName cases)) ... state = .ok state

For state = Checkpoint (.Leave shared store), this cannot be discharged by the existing raw matched skip lemma. Lean reduces the revived premise to lookup in the carried store, while the raw guard path required by the existing switch executor reduces to lookup through the checkpoint state's raw/default store. In other words, proving the skip by feeding reviveJump[matchedName] to a raw state[matchedName] theorem is exactly the unsound revived-to-raw adapter the issue says not to add.

Concrete failed point:

• Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean
• attempted revived variants around exec_nativeSwitchCaseIfs_matched_fuel / exec_nativeSwitchCaseIfs_with_default_matched_fuel
• failure: hMatched : (Ok shared store)[matchedName]! = 1 from reviveJump, but the raw skip theorem needs (Checkpoint (.Leave shared store))[matchedName]! = 1, which simplifies through the checkpoint/default raw lookup and is not derivable.

So the current lower-native switch execution stack still needs a different observation-boundary lemma: one that does not require proving raw switch/default guard skip after a Leave checkpoint, or a semantics-level lemma showing block execution after the checkpoint is observationally irrelevant before projecting via final.reviveJump. I backed out the failed patch and left the worktree clean rather than landing a theorem that smuggles revived state into raw lookup.

[Th0rgal]

Blocked while implementing the reviveJump observation-boundary design. The remaining blocker is in the native switch suffix/default proof layer: after a selected body returns a checkpoint, the revived observation premise is the right statement, but the switch theorem stack needs a separate lemma showing generated case suffixes and generated default tails execute as no-ops on checkpoint states, plus an invariant excluding from the selected-body endpoint. A raw adapter is not valid here because raw on checkpoint states follows the default/out-of-bounds path, which is exactly the public proof boundary #1884 is trying to remove. I stopped without opening a PR; local branch changes were reverted.

[Th0rgal]

Correction/expanded blocker details from the reviveJump observation-boundary implementation attempt:

The remaining blocker is in the native switch suffix/default proof layer. After a selected body returns a checkpoint, the revived observation premise is the right statement, but the switch theorem stack still needs separate lemmas showing generated case suffixes and generated default tails execute as no-ops on checkpoint states, plus an invariant excluding .OutOfFuel from the .ok final selected-body endpoint.

A raw adapter from final.reviveJump[matched] = 1 to final[matched] = 1 is not valid here: raw [name]! on checkpoint states follows the default/out-of-bounds path, which is exactly why #1884 needs the revived observation boundary. I stopped without opening a PR; local branch changes were reverted.

[Th0rgal]

Status after resuming on latest origin/main (7f9859d6) and branch issue-1884-observation-framework:

I rechecked the reviveJump/checkpoint-aware switch-tail path against the current tree and the prior WIP patches. The blocker remains the one now split out to #1890: the existing native switch suffix/default stack still reasons through raw state[matchedName]!, while the only sound selected-body observation after Leave is final.reviveJump[matchedName]!. Trying to reuse the raw skip lemmas fails exactly at the checkpoint boundary: Lean reduces the revived premise through the carried checkpoint store, but raw bracket lookup on Checkpoint goes through the checkpoint state's default/out-of-bounds GetElem! path. Adding a revived-to-raw adapter would violate #1884's constraint.

I also tested the larger revived-switch worker draft after rebasing; it still fails in the checkpoint no-op layer unless it smuggles revived lookup into raw lookup. So this is not ready for a PR that removes hCont, hExecBridge, or hUserBodyHalt while preserving the current trust boundary. I stopped without modifying the main worktree or opening a PR. The next productive task is #1890's narrower semantic/lowering contract for checkpoint-aware native switch tails; after that lands, #1884's unconditional bridge cleanup can be reopened as proof plumbing.