proof(ir): guarded-pipeline inversion lemmas (lane 2.2 pipeline closure)

Compiler/Proofs/IRGeneration/GuardedCompile.lean

@@ -0,0 +1,64 @@
+import Compiler.Proofs.IRGeneration.SpliceSimulation
+
+/-!
+# Inversion lemmas for the guarded compilation pipeline
+
+Make `attachNonReentrantGuard_exec` mechanically consumable from
+`compileGuardedFunctionSpec`: the compiled function body always has the
+loads-then-body shape (by construction of `compileFunctionSpec`), and the
+guarded pipeline is exactly compile-then-attach.
+-/
+namespace Compiler.Proofs.IRGeneration
+
+open Compiler.Yul
+open Compiler.CompilationModel
+open Verity.Core.Intrinsics (HardFork)
+
+/-- `compileFunctionSpec` output always has the loads-then-body shape. -/
+theorem compileFunctionSpec_body_shape (fields : List Field)
+    (events : List EventDef) (errors : List ErrorDef)
+    (adtTypes : List AdtTypeDef) (selector : Nat) (spec : FunctionSpec)
+    (targetFork : HardFork) (internalFunctions : List FunctionSpec)
+    (irFn : IRFunction)
+    (h : compileFunctionSpec fields events errors adtTypes selector spec
+      targetFork internalFunctions = .ok irFn) :
+    ∃ bodyStmts, irFn.body = genParamLoads spec.params ++ bodyStmts := by
+  unfold compileFunctionSpec at h
+  cases hv : validateFunctionSpec spec with
+  | error e => rw [hv] at h; cases h
+  | ok _ =>
+      rw [hv] at h
+      cases hr : functionReturns spec with
+      | error e => rw [hr] at h; cases h
+      | ok returns =>
+          rw [hr] at h
+          cases hb : compileStmtListWithFork fields events errors .calldata [] false
+              (spec.params.map (·.name)) adtTypes targetFork spec.body
+              internalFunctions with
+          | error e => rw [hb] at h; cases h
+          | ok bodyStmts =>
+              rw [hb] at h
+              refine ⟨bodyStmts, ?_⟩
+              have := Except.ok.inj h
+              rw [← this]
+
+/-- The guarded pipeline is exactly compile-then-attach. -/
+theorem compileGuardedFunctionSpec_inv (fields : List Field)
+    (events : List EventDef) (errors : List ErrorDef)
+    (adtTypes : List AdtTypeDef) (internalFunctions : List FunctionSpec)
+    (sel : Nat) (spec : FunctionSpec) (targetFork : HardFork)
+    (fn : IRFunction)
+    (h : compileGuardedFunctionSpec fields events errors adtTypes
+      internalFunctions sel spec targetFork = .ok fn) :
+    ∃ irFn, compileFunctionSpec fields events errors adtTypes sel spec
+        targetFork internalFunctions = .ok irFn ∧
+      attachNonReentrantGuard fields spec irFn = .ok fn := by
+  unfold compileGuardedFunctionSpec at h
+  cases hc : compileFunctionSpec fields events errors adtTypes sel spec
+      targetFork internalFunctions with
+  | error e => rw [hc] at h; cases h
+  | ok irFn =>
+      rw [hc] at h
+      exact ⟨irFn, rfl, h⟩
+
+end Compiler.Proofs.IRGeneration

PrintAxioms.lean

@@ -73,6 +73,7 @@ import Compiler.Proofs.IRGeneration.GenericInduction.ResultRelation
 import Compiler.Proofs.IRGeneration.GenericInduction.Scope
 import Compiler.Proofs.IRGeneration.GenericInduction.Storage
 import Compiler.Proofs.IRGeneration.GenericInduction.StorageWord
+import Compiler.Proofs.IRGeneration.GuardedCompile
 import Compiler.Proofs.IRGeneration.HelperBodyBridge
 import Compiler.Proofs.IRGeneration.HelperBodyShape
 import Compiler.Proofs.IRGeneration.HelperSummaryEvidence
@@ -3527,6 +3528,10 @@ end Verity.AxiomAudit
   -- Compiler.Proofs.IRGeneration.compiledStmtStep_setStorageWord_singleSlot_preserves  -- private
   Compiler.Proofs.IRGeneration.compiledStmtStep_setStorageWord_singleSlot
 
+  -- Compiler/Proofs/IRGeneration/GuardedCompile.lean
+  Compiler.Proofs.IRGeneration.compileFunctionSpec_body_shape
+  Compiler.Proofs.IRGeneration.compileGuardedFunctionSpec_inv
+
   -- Compiler/Proofs/IRGeneration/HelperBodyBridge.lean
   Compiler.Proofs.IRGeneration.execIRInternalFunctionWithInternals_obeys_internal_helper_summary
   -- Compiler.Proofs.IRGeneration.helperBridge_internalFunctionYulName_head  -- private
@@ -6692,4 +6697,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6250 theorems/lemmas (4382 public, 1868 private, 0 sorry'd)
+-- Total: 6252 theorems/lemmas (4384 public, 1868 private, 0 sorry'd)