[Layer 3] Prove conditional (if) statement equivalence

[Th0rgal]

Statement Type

Statement: Conditional (if)
Theorem: conditional_equiv
File: Compiler/Proofs/YulGeneration/StatementEquivalence.lean:187

Description

Prove that executing conditional (if) statements in IR matches executing them in Yul when states are aligned.

IR Semantics: See Compiler/Proofs/IRGeneration/IRInterpreter.lean
Yul Semantics: See Compiler/Proofs/YulGeneration/Semantics.lean

Proof Strategy

See theorem stub in StatementEquivalence.lean for detailed proof strategy and the worked example (variable assignment) for proof pattern.

Difficulty & Effort

• Difficulty: Medium-High
• Estimated Effort: 4-8h
• Dependencies: Recursive equivalence for branches

Acceptance Criteria

• Replace sorry in theorem stub with complete proof
• Add tests in Compiler/Proofs/YulGeneration/SmokeTests.lean demonstrating equivalence
• Update roadmap progress table (docs/ROADMAP.md) to mark as ✅ Complete
• CI passes (all proofs check, no new sorries)
• PR review approved

References

• Roadmap: docs/ROADMAP.md - Layer 3 section
• IR Semantics: Compiler/Proofs/IRGeneration/IRInterpreter.lean
• Yul Semantics: Compiler/Proofs/YulGeneration/Semantics.lean
• Equivalence Definitions: Compiler/Proofs/YulGeneration/Equivalence.lean
• Theorem Stub: Compiler/Proofs/YulGeneration/StatementEquivalence.lean:187
• Preservation Theorem: Compiler/Proofs/YulGeneration/Preservation.lean

Getting Started

1. Read the roadmap context in docs/ROADMAP.md
2. Review the theorem stub in StatementEquivalence.lean:187
3. Study the worked example (variable assignment) for proof patterns
4. Review IR and Yul semantics for this statement type
5. Replace sorry with your proof
6. Add smoke tests to verify your proof works
7. Submit PR referencing this issue

Questions?

Ask in the PR or open a discussion. See Compiler/Proofs/README.md for proof development guide.

---

Part of: Layer 3 (IR → Yul) verification completion
Blocks: End-to-end verification EDSL → Bytecode
Related: All 8 statement proofs must be completed before composition theorem

[Th0rgal]

📌 Important Prerequisite

Before working on this proof, note that there's a helper lemma that needs to be proven first:

evalIRExpr_eq_evalYulExpr (line 92 in StatementEquivalence.lean)

lemma evalIRExpr_eq_evalYulExpr (selector : Nat) (irState : IRState) (expr : YulExpr) :
    evalIRExpr irState expr = evalYulExpr (yulStateOfIR selector irState) expr := by
  sorry  -- ← Currently admitted

Why it matters: This lemma is used by assign_equiv and will likely be needed by most other statement proofs. It shows that IR and Yul expression evaluation are identical when states are aligned.

Status: Being worked on in PR #27. Check there for updates before starting this proof.

Alternative: If you want to start this proof now, you can use the lemma (with sorry) and it will work once the lemma is proven.

[Th0rgal]

🟡 Partially Complete

Status: The theorem structure is proven, but has one sorry for the recursive case.

File: Compiler/Proofs/YulGeneration/StatementEquivalence.lean:208-233

What's Proven ✅:

• Condition evaluation equivalence
• False branch (condition = 0) equivalence
• Structure and pattern established

What Remains ⚠️:

• True branch (condition ≠ 0) requires recursive call to execIRStmtsFuel / execYulStmtsFuel
• This will be resolved by the composition theorem (stmtList_equiv)
• One sorry on line 232

Next Steps:

1. Complete the composition theorem ([Compiler Enhancement] External function linking for production cryptographic libraries #36 - not yet created)
2. Use it to prove the recursive case
3. Remove the sorry

Difficulty: The hard part (pattern matching, case analysis) is done. The remaining piece is straightforward once composition is proven.

Keeping open until fully complete (no sorry).

[Th0rgal]

Status Update: Nearly Complete! 🎉

Progress: 95% complete (25/26 lines proven, 1 sorry remaining)

✅ What's Proven

All base cases of the conditional are fully proven with no sorries:

• ✅ Condition evaluation fails → both IR and Yul revert
• ✅ Condition evaluates to 0 (false) → both continue without executing body
• 🔵 Condition evaluates to non-zero (true) → both execute body (has 1 sorry)

🔵 Remaining Work

The recursive case (when condition is true and body executes) has 1 sorry that requires:

1. Universal statement dispatcher (all_stmts_equiv) - 2-4 hours

   • Pattern match on statement types
   • Dispatch to appropriate theorem (assign_equiv, storageLoad_equiv, etc.)
   • Handles circular dependency with well-founded recursion

2. Apply composition theorem - 1-2 hours (once all_stmts_equiv exists)

   • Use existing execIRStmtsFuel_equiv_execYulStmtsFuel_of_stmt_equiv (Equivalence.lean:403)
   • Proves body execution is equivalent
   • Completes the proof!

📍 Current Code

Location: Compiler/Proofs/YulGeneration/StatementEquivalence.lean:304-337

The Sorry:

· -- Condition is true (non-zero), both execute body
  simp [hc]
  -- Both call execIRStmtsFuel/execYulStmtsFuel on the body
  -- Apply the composition theorem to prove bodies are equivalent
  -- Requires: universal statement equivalence proof (see all_stmts_equiv below)
  sorry  -- Apply: execIRStmtsFuel_equiv_execYulStmtsFuel_of_stmt_equiv all_stmts_equiv

🎯 Implementation Strategy

Documented in StatementEquivalence.lean starting at line ~415:

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 _ => sorry  -- Trivial
  | let_ name value => exact assign_equiv ...
  | assign name value => exact assign_equiv ...
  | expr e => cases e with
      | call "sload" => exact storageLoad_equiv ...
      | call "sstore" => exact storageStore_equiv ...
      | call "return" => exact return_equiv ...
      | call "revert" => exact revert_equiv ...
      | ... -- All 7 proven theorems
  | if_ cond body => exact conditional_equiv ...  -- Circular\! Need mutual/WF recursion
  | ...

🏗️ Why This Structure

The circular dependency (conditional needs composition, composition needs conditional) is resolved by:

• Option 1: Mutual recursion (define both together)
• Option 2: Well-founded recursion on statement structure size

This is a well-understood pattern in Lean with clear solution paths.

📊 Impact

Completing this proof:

• ✅ Finishes 8/8 individual statement proofs
• ✅ Enables full use of composition theorem
• ✅ Completes Layer 3 to 100%
• ✅ Unblocks end-to-end EDSL → Bytecode verification

Total Effort Remaining: 3-6 hours
Difficulty: Medium (pattern matching + mutual recursion setup)

---

Related: PR #27 has all the infrastructure in place. The composition theorem exists and is proven (Equivalence.lean:403). All 7 other statement proofs are complete.

Next Steps: Implement all_stmts_equiv with pattern matching, apply to conditional proof, done!

[Th0rgal]

Status Update: Ready for Final Push!

Current Progress: 95% complete (25/26 lines proven)

With PR #27 merged, all infrastructure is in place. This issue is now unblocked and ready to complete!

✅ What's Done

All base cases proven with NO sorries:

• ✅ Condition evaluation fails → both revert
• ✅ Condition = 0 (false) → both continue without executing body

🎯 What Remains (1 sorry)

Recursive case: When condition is true (non-zero), both execute body

• Location: StatementEquivalence.lean:337
• Blocker: Needs universal statement dispatcher ([Layer 3] Implement universal statement dispatcher (all_stmts_equiv) #37)
• Effort: 1-2 hours once [Layer 3] Implement universal statement dispatcher (all_stmts_equiv) #37 is complete

📋 Implementation Path

After #37 is complete:

· -- Condition is true (non-zero), both execute body
  simp [hc]
  -- Apply composition theorem to prove body execution is equivalent
  have h_body : execResultsAligned selector
      (execIRStmtsFuel fuel' irState body)
      (execYulStmtsFuel fuel' yulState body) := by
    -- Use the composition theorem with all_stmts_equiv
    exact execIRStmtsFuel_equiv_execYulStmtsFuel_of_stmt_equiv 
          all_stmts_equiv selector fuel' body irState yulState halign
  exact h_body

🔗 Dependencies

Blocked by: #37 (universal statement dispatcher)
Blocks: Layer 3 100% completion

🎉 Impact

Completing this proof:

• ✅ Removes last sorry in Layer 3
• ✅ Completes 8/8 individual statement equivalence proofs
• ✅ Enables full use of composition theorem
• ✅ Completes Layer 3 to 100%!

📝 Implementation Notes

The circular dependency is resolved by defining all_stmts_equiv and conditional_equiv mutually (see #37).

Once #37 is done, finishing this proof should take 1-2 hours max - it's just applying the theorem!

---

Ready to tackle after #37 is complete!

[Th0rgal]

This issue has been resolved by PR #42, which implemented both conditional_equiv and all_stmts_equiv using mutual recursion.

The conditional_equiv theorem is now fully proven (lines 308-343 in StatementEquivalence.lean) with:

• ✅ Complete implementation (no sorry statements)
• ✅ Proper handling of condition evaluation
• ✅ Case splitting on condition value (zero vs non-zero)
• ✅ Application of composition theorem for the body when condition is true
• ✅ All CI checks passing

The mutual recursion with all_stmts_equiv resolved the circular dependency cleanly.