chore: Prove worklistRun

SSA/Experimental/Bits/AutoStructs/Basic.lean

@@ -457,12 +457,9 @@ where go (st0 : worklist.St A S) : RawCNFA A :=
   | none => st0.m -- never happens
   termination_by st0.meas
 
-def worklistRun (final : S → Bool) (inits : Array S)
-    (hinits : inits.toList.Nodup) (f : S → Array (BitVec n × S)) : CNFA n :=
-  ⟨worklistRun' _ S final inits hinits f, by sorry⟩
-
 -- Correctness of the algorithm
 variable (final : S → Bool) (f : S → Array (A × S)) (inits : Array S)
+variable (hinits : inits.toList.Nodup)
 variable (M : NFA A σ)
 variable (corr : S → σ)
 variable (corr_inj : Function.Injective corr)
@@ -760,7 +757,6 @@ def processOneElem_inv {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) :
 
 seal GetElem.getElem in
 seal GetElem?.getElem? in
-
 set_option debug.skipKernelTC true in -- deterministic timeout
 def processOneElem_spec {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) :
     ∀ a sa', (f sa)[k]? = some (a, sa') →
@@ -984,7 +980,7 @@ def processOneElem_spec {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) :
 -- TODO: improve this proof, make it faster
 def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
     inv.sim A S M corr →
-    (worklistRun'.go A S final f st |>.Sim M) := by
+     (worklistRun'.go A S final f st).WF ∧ (worklistRun'.go A S final f st |>.Sim M) := by
   induction st using worklistRun'.go.induct _ _ final f with
   | case4 st hnemp sa? hsa? => -- trivial case that's impossible
       simp [sa?, Array.back?] at hsa?
@@ -1000,7 +996,9 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
   | case1 st hemp => -- exit case, prove that the invariant + empty worklist implies the postcondition
     have : st.worklist = #[] := by
       simp only [Array.isEmpty] at hemp; apply Array.eq_empty_of_size_eq_zero; simp_all only [decide_eq_true_eq]
-    intros hsim; unfold worklistRun'.go; simp_all; apply sim_closed_set _ _ _ _ _ _ (by simp_all) hsim
+    intros hsim; unfold worklistRun'.go; simp_all; constructor
+    · exact inv.wf
+    apply sim_closed_set _ _ _ _ _ _ (by simp_all) hsim
     simp [NFA.closed_set]; constructor
     { intros q hq; simp [worklist.St.R]
       obtain ⟨s, hmap, _⟩ := hsim.initial_all q hq
@@ -1032,7 +1030,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
             ext sa'; simp_all; rintro rfl k hge hsome
             suffices hccl : (f sa'.1)[k]? = none by simp_all
             apply Array.getElem?_size_le; assumption
-          simp_all only [ge_iff_le, st2]
+          simp_all only [ge_iff_le, Prod.mk.eta, and_self, st2]
         apply Array.foldl_induction
         simp only [st1, wl']
         { unfold processOneElem_mot
@@ -1098,7 +1096,8 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
       have : st.worklist.size = 0 := by omega
       simp_all
 
-def worklistRun'_spec : (worklistRun' A S final inits hinits f |>.Sim M) := by
+
+def worklistRun'_spec : (worklistRun' A S final inits hinits f).WF ∧ (worklistRun' A S final inits hinits f |>.Sim M) := by
   unfold worklistRun'
   simp
   have hh : StInv' ∅ (worklist.initState A S inits hinits final) := by
@@ -1112,6 +1111,7 @@ section worklist_good
 
 variable (S : Type) [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S]
 variable (final : S → Bool) (f : S → Array (BitVec n × S)) (inits : Array S)
+variable (hinits : inits.toList.Nodup)
 variable (M : NFA' n)
 variable (corr : S → M.σ)
 variable (corr_inj : Function.Injective corr)
@@ -1121,8 +1121,11 @@ variable (hinit₂ : ∀ q ∈  M.M.start, ∃ sa, corr sa = q ∧ sa ∈ inits)
 variable (hf₁: ∀ sa q' a, q' ∈ M.M.step (corr sa) a → ∃ sa', corr sa' = q' ∧ (a, sa') ∈ f sa)
 variable (hf₂: ∀ sa a sa', (a, sa') ∈ f sa → corr sa' ∈ M.M.step (corr sa) a)
 
-def worklistRun_spec : (worklistRun S final inits hinits f |>.Sim M) :=
-  worklistRun'_spec (BitVec n) S final f inits M.M corr corr_inj final_corr hf₁ hf₂
+def worklistRun : CNFA n :=
+  ⟨worklistRun' _ S final inits hinits f, (worklistRun'_spec _ _ final f inits hinits M.M corr corr_inj final_corr hf₁ hf₂).1⟩
+
+def worklistRun_spec : (worklistRun S final f inits hinits M corr corr_inj final_corr hf₁ hf₂ |>.Sim M) :=
+  worklistRun'_spec (BitVec n) S final f inits hinits M.M corr corr_inj final_corr hf₁ hf₂ |>.2
 
 end worklist_good