proof: add structural WithInternals head witnesses

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. -/

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

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)