From 1cbc08ae74c19decfec6ccbbecd0a915b4216621 Mon Sep 17 00:00:00 2001 From: Thomas Marchand Date: Tue, 7 Jul 2026 01:12:23 +0200 Subject: [PATCH] proof: package structural WithInternals heads --- Compiler/Proofs/HelperStepProofs.lean | 72 +++++++++++++++++++ .../GenericInduction/InterfaceAssembly.lean | 28 ++++++++ PrintAxioms.lean | 4 +- 3 files changed, 103 insertions(+), 1 deletion(-) diff --git a/Compiler/Proofs/HelperStepProofs.lean b/Compiler/Proofs/HelperStepProofs.lean index 6ca470f4a..2f1748263 100644 --- a/Compiler/Proofs/HelperStepProofs.lean +++ b/Compiler/Proofs/HelperStepProofs.lean @@ -2214,6 +2214,78 @@ theorem stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_of_compi intro _ exact ⟨compiledIR, hstep⟩ +/-- Concrete `WithInternals` structural witness for an `ite` head. The caller +supplies the exact spec-functions compiled-step proof for the recursive +statement form, and this packages it into the structural helper interface +without falling back to the legacy empty-helper compiler world. -/ +theorem stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_ite_of_compiledStep + {runtimeContract : IRContract} + {spec : CompilationModel} + {fields : List Field} + {scope : List String} + {cond : Expr} + {thenBranch elseBranch : List Stmt} + {compiledIR : List YulStmt} + {rest : List Stmt} + (hstep : + CompiledStmtStepWithHelpersAndHelperIRWithInternals + runtimeContract spec fields scope + (Stmt.ite cond thenBranch elseBranch) compiledIR) + (hrest : + StmtListStructuralInternalHelperStepInterfaceWithInternals + runtimeContract spec fields + (stmtNextScope scope (Stmt.ite cond thenBranch elseBranch)) rest) : + StmtListStructuralInternalHelperStepInterfaceWithInternals + runtimeContract spec fields scope + (Stmt.ite cond thenBranch elseBranch :: rest) := by + exact + stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_of_compiledStep + (runtimeContract := runtimeContract) + (spec := spec) + (fields := fields) + (scope := scope) + (stmt := Stmt.ite cond thenBranch elseBranch) + (compiledIR := compiledIR) + (rest := rest) + hstep + hrest + +/-- Concrete `WithInternals` structural witness for a `forEach` head. The exact +head step compiles against `spec.functions`, so the recursive structural case +can participate in the phase-17 mixed-list assembly route directly. -/ +theorem stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_forEach_of_compiledStep + {runtimeContract : IRContract} + {spec : CompilationModel} + {fields : List Field} + {scope : List String} + {varName : String} + {count : Expr} + {body : List Stmt} + {compiledIR : List YulStmt} + {rest : List Stmt} + (hstep : + CompiledStmtStepWithHelpersAndHelperIRWithInternals + runtimeContract spec fields scope + (Stmt.forEach varName count body) compiledIR) + (hrest : + StmtListStructuralInternalHelperStepInterfaceWithInternals + runtimeContract spec fields + (stmtNextScope scope (Stmt.forEach varName count body)) rest) : + StmtListStructuralInternalHelperStepInterfaceWithInternals + runtimeContract spec fields scope + (Stmt.forEach varName count body :: rest) := by + exact + stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_of_compiledStep + (runtimeContract := runtimeContract) + (spec := spec) + (fields := fields) + (scope := scope) + (stmt := Stmt.forEach varName count body) + (compiledIR := compiledIR) + (rest := rest) + hstep + hrest + /-- Assemble the spec-functions structural-helper interface from exact `WithInternals` head steps for the structural-helper heads that occur in the statement list. -/ diff --git a/Compiler/Proofs/IRGeneration/GenericInduction/InterfaceAssembly.lean b/Compiler/Proofs/IRGeneration/GenericInduction/InterfaceAssembly.lean index 146346384..5cd9cbfce 100644 --- a/Compiler/Proofs/IRGeneration/GenericInduction/InterfaceAssembly.lean +++ b/Compiler/Proofs/IRGeneration/GenericInduction/InterfaceAssembly.lean @@ -1048,6 +1048,34 @@ theorem (ih (fun stmt' hmem => hallDirect stmt' (List.mem_cons_of_mem stmt hmem))) +/-- Spec-functions-aware structural-helper list bridge. Structural helper heads +supplied by the `WithInternals` interface assemble directly into the +`StmtListGenericWithHelpersAndHelperIRWithInternals` seam. This is intentionally +narrow: every head in the list must be a recursive structural helper head. -/ +theorem + stmtListGenericWithHelpersAndHelperIRWithInternals_of_structuralInternalHelperStepInterfaceWithInternals + {runtimeContract : IRContract} + {spec : CompilationModel} + {fields : List Field} + {scope : List String} + {stmts : List Stmt} + (hstruct : + StmtListStructuralInternalHelperStepInterfaceWithInternals + runtimeContract spec fields scope stmts) + (hallStructural : + ∀ stmt ∈ stmts, stmtTouchesStructuralInternalHelperSurface stmt = true) : + StmtListGenericWithHelpersAndHelperIRWithInternals + runtimeContract spec fields scope stmts := by + induction hstruct with + | nil => + exact .nil + | @cons scope stmt rest hhead htail ih => + rcases hhead (hallStructural stmt List.mem_cons_self) with + ⟨compiledIR, hcompiled⟩ + exact .cons hcompiled + (ih (fun stmt' hmem => + hallStructural stmt' (List.mem_cons_of_mem stmt hmem))) + /-- Spec-functions-aware mixed helper-list bridge. Helper-free heads and helper-positive heads both provide exact `compileStmt ... spec.functions` witnesses, so the assembled list lands directly in diff --git a/PrintAxioms.lean b/PrintAxioms.lean index 59e1c6591..ddb7d4b63 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -1824,6 +1824,8 @@ end Verity.AxiomAudit Compiler.Proofs.HelperStepProofs.stmtListExprInternalHelperStepInterface_cons_of_exprHeadStepBridge Compiler.Proofs.HelperStepProofs.stmtListExprInternalHelperStepInterface_of_exprHeadStepBridges Compiler.Proofs.HelperStepProofs.stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_of_compiledStep + Compiler.Proofs.HelperStepProofs.stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_ite_of_compiledStep + Compiler.Proofs.HelperStepProofs.stmtListStructuralInternalHelperStepInterfaceWithInternals_cons_forEach_of_compiledStep Compiler.Proofs.HelperStepProofs.stmtListStructuralInternalHelperStepInterfaceWithInternals_of_structuralHeadStepsWithInternals Compiler.Proofs.HelperStepProofs.fullHelperAwareListWitnessWithInternals_of_allInterfaces Compiler.Proofs.HelperStepProofs.allHelperInterfacesSatisfied_of_helperSurfaceClosed @@ -5899,4 +5901,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 5529 theorems/lemmas (3827 public, 1702 private, 0 sorry'd) +-- Total: 5531 theorems/lemmas (3829 public, 1702 private, 0 sorry'd)