[Layer 3] Implement universal statement dispatcher (all_stmts_equiv)

[Th0rgal]

Overview

Implement the universal statement dispatcher that enables completing Layer 3 to 100%.

Status: Foundation complete, clear implementation path documented
Effort: 2-4 hours
Difficulty: Medium (pattern matching + mutual recursion)
Impact: Unblocks finishing conditional_equiv and completes Layer 3

Background

All 7 individual statement equivalence theorems are proven:

• ✅ assign_equiv
• ✅ storageLoad_equiv
• ✅ storageStore_equiv
• ✅ mappingLoad_equiv
• ✅ mappingStore_equiv
• ✅ return_equiv
• ✅ revert_equiv

The composition theorem exists and is fully proven (Equivalence.lean:403).

What's missing: A universal proof that ALL statements (any type) are equivalent.

What to Implement

theorem all_stmts_equiv : ∀ selector fuel stmt irState yulState,
    execIRStmt_equiv_execYulStmt_goal selector fuel stmt irState yulState := by
  intros selector fuel stmt irState yulState halign
  cases stmt with
  | comment _ => 
      -- Trivial: both no-op
      unfold execResultsAligned statesAligned at *
      rfl
  | let_ name value => 
      exact assign_equiv selector fuel name value irState yulState halign
  | assign name value => 
      exact assign_equiv selector fuel name value irState yulState halign
  | expr e =>
      cases e with
      | call "sload" [slotExpr] => 
          exact storageLoad_equiv selector fuel ... halign
      | call "sstore" [slotExpr, valExpr] => 
          exact storageStore_equiv selector fuel ... halign
      | call "return" [offsetExpr, sizeExpr] => 
          exact return_equiv selector fuel offsetExpr sizeExpr irState yulState halign
      | call "revert" [offsetExpr, sizeExpr] => 
          exact revert_equiv selector fuel offsetExpr sizeExpr irState yulState halign
      | call "mappingSlot" args =>
          -- Handle mapping operations
          sorry
      | _ => 
          -- Other expressions are no-ops
          sorry
  | if_ cond body => 
      -- Circular dependency\! Needs mutual/well-founded recursion
      exact conditional_equiv selector fuel cond body irState yulState halign
  | switch expr cases default => 
      -- Similar to conditional
      sorry
  | block stmts => 
      -- Recursive: apply composition theorem
      sorry
  | funcDef _ _ _ _ => 
      -- No-op
      unfold execResultsAligned statesAligned at *
      rfl

Circular Dependency Resolution

The circular dependency (conditional needs dispatcher, dispatcher needs conditional) can be resolved by:

Option 1: Mutual Recursion

mutual
  theorem all_stmts_equiv : ...
  theorem conditional_equiv : ...
end

Option 2: Well-Founded Recursion
Define on statement structure size (statements with smaller bodies come first).

Implementation Strategy

1. Start with non-recursive cases (assign, storage ops, return, revert)

   • These directly call the proven theorems
   • Should work immediately

2. Add trivial cases (comment, funcDef)

   • Both are no-ops, prove with rfl

3. Handle circular dependency

   • Use mutual recursion with conditional_equiv
   • OR use well-founded recursion on statement size

4. Test the theorem

   • Apply to simple statement lists
   • Verify composition theorem works with it

Files to Modify

• Primary: Compiler/Proofs/YulGeneration/StatementEquivalence.lean

  • Replace axiom all_stmts_equiv with actual implementation
  • May need to make conditional_equiv mutual

• Reference: Compiler/Proofs/YulGeneration/Equivalence.lean

  • See composition theorem at line 403 for how it's used

Acceptance Criteria

• Replace axiom all_stmts_equiv with proven theorem
• All pattern match cases covered
• Circular dependency resolved (mutual or WF recursion)
• Project builds successfully (lake build)
• No new sorries introduced
• Can be used by composition theorem

Once Complete

This theorem enables:

1. Finishing conditional_equiv (remove last sorry)
2. Using composition theorem for statement lists
3. Completing Layer 3 to 100%!

References

• Roadmap: docs/ROADMAP.md - Layer 3 section
• Implementation guide: Compiler/Proofs/YulGeneration/StatementEquivalence.lean:415+
• Existing proofs: Lines 70-402 in StatementEquivalence.lean
• Composition theorem: Equivalence.lean:403-491

Questions?

See PR #27 for full context and discussion. The structure is fully documented - this is "just" implementation!