[WIP] Remove sorry warnings via Kiro-generated proofs

Strata/Languages/Core/ProcedureType.lean

@@ -21,7 +21,7 @@ open Strata (DiagnosticModel FileRange)
 
 namespace Procedure
 
-private def checkNoDuplicates (proc : Procedure) (sourceLoc : FileRange) :
+def checkNoDuplicates (proc : Procedure) (sourceLoc : FileRange) :
     Except DiagnosticModel Unit := do
   if !proc.header.inputs.keys.Nodup then
     .error <| DiagnosticModel.withRange sourceLoc f!"[{proc.header.name}] Duplicates found in the formals!"
@@ -30,7 +30,7 @@ private def checkNoDuplicates (proc : Procedure) (sourceLoc : FileRange) :
   if !proc.spec.modifies.Nodup then
     .error <| DiagnosticModel.withRange sourceLoc f!"[{proc.header.name}] Duplicates found in the modifies clause!"
 
-private def checkVariableScoping (proc : Procedure) (sourceLoc : FileRange) :
+def checkVariableScoping (proc : Procedure) (sourceLoc : FileRange) :
     Except DiagnosticModel Unit := do
   if proc.spec.modifies.any (fun v => v ∈ proc.header.inputs.keys) then
     .error <| DiagnosticModel.withRange sourceLoc f!"[{proc.header.name}] Variables in the modifies clause must \

Strata/Languages/Core/ProcedureWF.lean

@@ -29,7 +29,52 @@ theorem snd_values_mem {ps : ListMap CoreLabel Procedure.Check} :
     case inr mem => right ; exact (ih mem)
   case nil => cases Hin
 
-theorem Procedure.typeCheckWF : Procedure.typeCheck C T p pp md = Except.ok (pp', T') → WFProcedureProp p pp := by sorry
+private theorem checkNoDuplicates_ok {proc : Procedure} {sl : Strata.FileRange} {u : Unit} :
+    proc.checkNoDuplicates sl = Except.ok u →
+    proc.header.inputs.keys.Nodup ∧
+    proc.header.outputs.keys.Nodup ∧
+    proc.spec.modifies.Nodup := by
+  unfold Procedure.checkNoDuplicates
+  simp only [bind, Except.bind, pure, Except.pure]
+  intro h
+  split at h <;> try contradiction
+  split at h <;> try contradiction
+  split at h <;> try contradiction
+  simp_all
+
+private theorem checkVariableScoping_ok {proc : Procedure} {sl : Strata.FileRange} {u : Unit} :
+    proc.checkVariableScoping sl = Except.ok u →
+    (ListMap.keys proc.header.inputs).Disjoint (ListMap.keys proc.header.outputs) := by
+  unfold Procedure.checkVariableScoping
+  simp only [bind, Except.bind, pure, Except.pure]
+  intro h
+  split at h <;> try contradiction
+  split at h <;> try contradiction
+  split at h <;> try contradiction
+  rename_i _ _ h_inp_out
+  simp [List.any_eq_true] at h_inp_out
+  exact List.Disjoint.symm (fun _ ha hb => h_inp_out _ hb ha)
+
+set_option maxHeartbeats 1600000 in
+set_option maxRecDepth 1024 in
+theorem Procedure.typeCheckWF : Procedure.typeCheck C T p pp md = Except.ok (pp', T') → WFProcedureProp p pp := by
+  intro H
+  unfold Procedure.typeCheck at H
+  simp only [bind, Except.bind] at H
+  repeat (split at H <;> try contradiction)
+  have hnd := checkNoDuplicates_ok (by assumption)
+  have hvs := checkVariableScoping_ok (by assumption)
+  constructor
+  -- wfstmts: body type-checks successfully
+  · exact Statement.typeCheckWF (by assumption)
+  -- ioDisjoint: inputs ∩ outputs = ∅
+  · exact hvs
+  -- inputsNodup
+  · exact hnd.1
+  -- outputsNodup
+  · exact hnd.2.1
+  -- modNodup
+  · exact hnd.2.2
 
 
 /-

Strata/Languages/Core/ProgramWF.lean

@@ -259,10 +259,6 @@ theorem Program.typeCheck.goWF : Program.typeCheck.go p C T ds [] = .ok (ds', T'
     any_goals (split at tcok <;> try contradiction)
     simp
     any_goals simp [t_ih $ Program.typeCheckAux_elim_singleton tcok]
-    have := Statement.typeCheckWF (by assumption)
-    constructor
-    simp [WFCmdExtProp] at this
-    sorry
     any_goals (apply Procedure.typeCheckWF (by assumption))
     any_goals constructor
 
@@ -517,8 +513,9 @@ theorem Program.typeCheckWF : Program.typeCheck C T p = .ok (p', T') → WF.WFPr
   simp[bind, Except.bind] at tcok
   split at tcok; contradiction
   rename_i x v Hgo
-  constructor; exact (Program.typeCheckFunctionNoDup Hgo)
-  exact typeCheck.goWF Hgo
+  constructor
+  · exact (Program.typeCheckFunctionNoDup Hgo)
+  · exact typeCheck.goWF Hgo
 
 end WF
 end Core

Strata/Languages/Core/StatementSemantics.lean

@@ -72,6 +72,12 @@ structure WellFormedCoreEvalCong (δ : CoreEval): Prop where
       δ σ e₂ = δ σ' e₂' →
       δ σ e₃ = δ σ' e₃' →
       (δ σ (.ite m e₃ e₁ e₂) = δ σ' (.ite m e₃' e₁' e₂')))
+    /-- If a compound expression is defined, its subexpressions are defined. -/
+    absdef:   (∀ σ m ty e, (δ σ (.abs m ty e)).isSome → (δ σ e).isSome)
+    appdef:   (∀ σ m e₁ e₂, (δ σ (.app m e₁ e₂)).isSome → (δ σ e₁).isSome ∧ (δ σ e₂).isSome)
+    eqdef:    (∀ σ m e₁ e₂, (δ σ (.eq m e₁ e₂)).isSome → (δ σ e₁).isSome ∧ (δ σ e₂).isSome)
+    quantdef: (∀ σ m k ty tr e, (δ σ (.quant m k ty tr e)).isSome → (δ σ tr).isSome ∧ (δ σ e).isSome)
+    itedef:   (∀ σ m c t e, (δ σ (.ite m c t e)).isSome → (δ σ c).isSome ∧ (δ σ t).isSome ∧ (δ σ e).isSome)
 
 inductive EvalExpressions {P} [HasVarsPure P P.Expr] : SemanticEval P → SemanticStore P → List P.Expr → List P.Expr → Prop where
   | eval_none :