feat: adding asynchronous execution of solver tactics for generated VCs (#33)

* feat: implement asynchronous tactic execution in Loom

This commit introduces several functions for executing tactics asynchronously, allowing for parallel processing of goals. Key additions include `wrapTactic`, `asyncRunTactic`, and `allGoalsAsync`, which facilitate running tactics on multiple goals concurrently. The implementation also includes helper functions for managing task priorities and cancellation tokens, enhancing the overall efficiency of tactic execution in Loom.

* feat: enhance Loom tactics with asynchronous capabilities

This commit adds new syntax for asynchronous tactics, including `loom_solve_async` and `loom_solve_async!`, allowing for improved parallel processing of goals. It introduces helper functions to manage asynchronous execution and provides warnings for potential mismatches in task numbers. Additionally, the previous `Loom.Tactic` file has been removed in favor of `Loom.TacticAsync`, streamlining the tactic execution process.

* feat: add a case study for async

* refactor: use grind in SerachSubstring

* chore: bump to v4.24.0

* fix one case study

* clean up

Author: volodeyka

CaseStudies/Tactic.lean

@@ -6,7 +6,8 @@ import Loom.MonadAlgebras.WP.Attr
 import Loom.MonadAlgebras.WP.Tactic
 -- import Loom.MonadAlgebras.WP.DoNames'
 import Loom.MonadAlgebras.WP.Gen
-import Loom.Tactic
+-- import Loom.Tactic
+import Loom.TacticAsync
 import Loom.SMT
 
 import CaseStudies.Extension
@@ -58,6 +59,8 @@ def getAssertionStx : TacticM (Option Term) := withMainContext do
 
 declare_syntax_cat loom_solve_tactic
 syntax "loom_solve" : loom_solve_tactic
+syntax "loom_solve_async" (num)? : loom_solve_tactic
+syntax "loom_solve_async!" (num)? : loom_solve_tactic
 syntax "loom_solve?" : loom_solve_tactic
 syntax "loom_solve!" : loom_solve_tactic
 syntax loom_solve_tactic : tactic
@@ -67,6 +70,16 @@ syntax "loom_unfold" : tactic
 syntax "loom_auto" : tactic
 syntax "loom_solver" : tactic
 
+def loomSolveAsync? : TSyntax `loom_solve_tactic -> Option (Option Nat)
+  | `(loom_solve_tactic| loom_solve_async $n ?)
+  | `(loom_solve_tactic| loom_solve_async! $n ?) => some (n.map (·.getNat))
+  | _ => none
+
+def loomSolveIsReporting : TSyntax `loom_solve_tactic -> Bool
+  | `(loom_solve_tactic| loom_solve_async! $_ ?)
+  | `(loom_solve_tactic| loom_solve!) => true
+  | _ => false
+
 elab_rules : tactic
   | `(tactic| loom_goals_intro) => withMainContext do
     let vlsIntro <- `(tactic| (
@@ -115,31 +128,31 @@ elab_rules : tactic
     else
       let vlsIntro ← `(tactic| loom_goals_intro)
       let vlsUnfold ← `(tactic| loom_unfold)
-      let vlsSolve ← `(tactic| loom_solver)
+      let vlsSolve ← `(tactic| try solve | loom_unfold; loom_solver)
       evalTactic vlsIntro
-      let res <- anyGoalsWithTag fun _mvarId => do
-        let stx_res <- getAssertionStx
+      let goals <- getUnsolvedGoals
+      if let some n := loomSolveAsync? vls then
+        if goals.length < n.getD 0 then
+          logWarningAt vls m!"This method has only {goals.length} Verification Conditions, but `loom_solve_async` is called with {n.get!} asynchronous tasks"
+        allGoalsAsync (numTasks := n.map (·.min goals.length)) do
+          evalTactic vlsSolve
+        logWarningAt vls m!
+        "`loom_solve_async` uses sorry to admit all the solved goals for now, consider running `loom_solve` once proof is complete to get the proof term"
+      else
+        allGoals do evalTactic vlsSolve
+      let mut unsolved := #[]
+      for mvarId in <- getUnsolvedGoals do
+        setGoals [mvarId]
+        let stx <- getAssertionStx
         evalTactic vlsUnfold
-        let mvarId <- getMainGoal
-        evalTactic vlsSolve
-        if (<- getUnsolvedGoals).length > 0 then
-          match stx_res with
-          | some stx =>
-            return some (.mkSimple stx.raw.prettyPrint.pretty, (mvarId, some stx))
-          | none =>
-            return some (`unnamed, (mvarId, none))
-        else return none
-      let tryVlsSolve ← `(tactic| all_goals try loom_solver)
-      let tryVlsUnfold ← `(tactic| all_goals try loom_unfold)
-      evalTactic tryVlsSolve
-      evalTactic tryVlsUnfold
-      match vls with
-      | `(loom_solve_tactic| loom_solve!) =>
-        for (mvarId, stx_res) in res do
-          match stx_res with
-          | some stx => logErrorAt stx $ m!"Failed to prove assertion\n{mvarId}"
-          | none => logError m!"Failed to prove nameless assertion\n{mvarId}"
-      | _ => pure ()
+        if let some stx := stx then
+          (<- getMainGoal).setTag <| .mkSimple stx.raw.prettyPrint.pretty
+          if loomSolveIsReporting vls then
+            logErrorAt stx $ m!"Failed to prove assertion\n{mvarId}"
+        else if loomSolveIsReporting vls then
+          logErrorAt vls m!"Failed to prove nameless assertion\n{mvarId}"
+        unsolved := unsolved.append (← getUnsolvedGoals).toArray
+      setGoals unsolved.toList
 
 elab "loom_solve?" : tactic => withMainContext do
   let ctx := (<- solverHints.get)
@@ -175,7 +188,7 @@ elab_rules : tactic
       | "grind" =>
         /- In case of `grind` solver, we need  to fetch the number of splits from the options first. -/
         let splits := Lean.Syntax.mkNatLit <| (opts.getNat (defVal := 20) `loom.solver.grind.splits)
-        evalTactic $ <- `(tactic| try grind ($(mkIdent `splits):ident := $splits))
+        evalTactic $ <- `(tactic| grind ($(mkIdent `splits):ident := $splits))
       | "custom" =>
         evalTactic $ <- `(tactic| fail "Custom solver is not specified")
       | _ => evalTactic $ <- `(tactic| loom_auto)

CaseStudies/Theory.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Ring.Int.Defs
 import Loom.MonadAlgebras.NonDetT.Extract
 import Loom.MonadAlgebras.Instances.Basic
 import Loom.MonadAlgebras.WP.Tactic
-import Loom.Tactic
+import Loom.Meta
 
 import CaseStudies.Extension
 variable {m τ l} [Monad m] [LawfulMonad m] [Nonempty τ] [CompleteBooleanAlgebra l]

CaseStudies/Velvet/VelvetExamples/Recursion.lean

@@ -201,4 +201,3 @@ method pow2 (n: Nat) return (res: Nat)
 
 prove_correct pow2 by
   loom_solve
-  rw [if_pos]; rfl

CaseStudies/Velvet/VelvetExamples/SubstringSearch.lean

@@ -4,7 +4,7 @@ import CaseStudies.TestingUtil
 set_option loom.semantics.termination "total"
 set_option loom.semantics.choice "demonic"
 set_option loom.solver "cvc5"
-set_option loom.solver.smt.timeout 5
+set_option loom.solver.smt.timeout 4
 
 --this will ne our answer type
 structure SubstringResult where
@@ -14,7 +14,7 @@ structure SubstringResult where
 deriving Repr, Inhabited
 
 --predicate for substring all characters of which satisfy the predicate
-@[loomAbstractionSimp]
+@[grind, loomAbstractionSimp]
 def CorrectSubstring (s : Array Char) (p : Char -> Bool) (l r : Nat) : Prop :=
   l ≤ r ∧ r < s.size ∧
   (∀ i, l ≤ i ∧ i ≤ r → p s[i]!)
@@ -76,8 +76,9 @@ do
       pnt := pnt + 1
     return ⟨l_ans, r_ans, ans > 0⟩
 
+#time
 prove_correct SubstringSearch by
-  loom_solve
+  loom_solve_async
 
 --prove theorem not about the monadic computation but the actual
 --extract result

CaseStudies/Velvet/VelvetExamples/SubstringSearchAsync.lean

@@ -0,0 +1,101 @@
+import Auto
+import Lean
+
+import CaseStudies.Velvet.Std
+import CaseStudies.TestingUtil
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+--this will ne our answer type
+structure SubstringResult where
+  l : Nat
+  r : Nat
+  flag: Bool
+deriving Repr, Inhabited
+
+--predicate for substring all characters of which satisfy the predicate
+@[grind]
+def CorrectSubstring (s : Array Char) (p : Char -> Bool) (l r : Nat) : Prop :=
+  l ≤ r ∧ r < s.size ∧
+  (∀ i, l ≤ i ∧ i ≤ r → p s[i]!)
+
+--actual method
+--  if there are no substrings,
+--  flag is false and all characters do not satisfy the predicate
+method SubstringSearch (s: Array Char) (p: Char -> Bool) return (res: SubstringResult)
+--postconditions, don't need any preconditions.
+ensures (res.l ≤ res.r)
+ensures 0 < s.size → res.r < s.size
+ensures res.flag → CorrectSubstring s p res.l res.r
+ensures res.flag →
+  (∀ l₁ r₁, CorrectSubstring s p l₁ r₁ →
+    r₁ - l₁ + 1 = res.r - res.l + 1 ∧ res.r ≤ r₁ ∨
+    r₁ - l₁ + 1 < res.r - res.l + 1)
+ensures ¬res.flag → ∀ i < s.size, ¬p s[i]!
+do
+    if s.size = 0 then
+      --basic case with an empty string
+      return ⟨0, 0, false⟩
+    let mut cnt := 0
+    let mut pnt := 0
+    let mut ans := 0
+    let mut l_ans := 0
+    let mut r_ans := 0
+    while pnt < s.size
+    --loop invariants
+    invariant 0 ≤ cnt
+    invariant cnt ≤ pnt
+    invariant pnt ≤ s.size
+    invariant l_ans ≤ r_ans
+    invariant r_ans < s.size
+    invariant cnt ≤ ans
+    invariant r_ans ≤ pnt
+    invariant ∀ j, pnt - cnt ≤ j ∧ j < pnt → p s[j]!
+    invariant ans > 0 →
+        ans = r_ans - l_ans + 1 ∧
+        CorrectSubstring s p l_ans r_ans
+    invariant ans = 0 → (∀ i, i < pnt → ¬p s[i]!)
+    invariant cnt < pnt → ¬p s[pnt - cnt - 1]!
+    invariant ∀ l₁ r₁,
+        CorrectSubstring s p l₁ r₁ ∧ r₁ < pnt →
+        r₁ - l₁ + 1 = ans ∧ r_ans ≤ r₁ ∨ r₁ - l₁ + 1 < ans
+    --value decreases by 1 with each iteration,
+    --therefore time complexity is O(size s), as other parts
+    --take constant time
+    decreasing s.size - pnt
+    do
+      --loop body
+      if p s[pnt]! then
+        cnt := cnt + 1
+        if ans < cnt then
+          l_ans := pnt + 1 - cnt
+          r_ans := pnt
+          ans := cnt
+      else
+        cnt := 0
+      pnt := pnt + 1
+    return ⟨l_ans, r_ans, ans > 0⟩
+
+/--
+warning: `loom_solve_async` uses sorry to admit all the solved goals for now, consider running `loom_solve` once proof is complete to get the proof term
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+prove_correct SubstringSearch by
+  loom_solve_async
+
+--prove theorem not about the monadic computation but the actual
+--extract result
+theorem finalCorrectnessTheorem (s : Array Char) (p : Char → Bool) :
+  let res := SubstringSearch s p |>.extract
+  (res.flag = false → ∀ i < s.size, p s[i]! = false) ∧
+  (res.flag = true →
+    (∀ l₁ r₁, CorrectSubstring s p l₁ r₁ →
+  r₁ - l₁ + 1 = res.r - res.l + 1 ∧ res.r ≤ r₁ ∨
+  r₁ - l₁ + 1 < res.r - res.l + 1)) ∧
+  (res.flag = true → CorrectSubstring s p res.l res.r) ∧
+  (0 < s.size → res.r < s.size) ∧
+  (res.l ≤ res.r) := by
+    grind [VelvetM.extract_spec, SubstringSearch_correct]

CaseStudies/Velvet/VelvetTheory.lean

@@ -55,7 +55,7 @@ lemma wp_mono_part (x : NonDetT DivM α) (post₁ post₂ : α -> Prop) :
 lemma VelvetM.total_decompose {α : Type} (x : VelvetM α) (post₁ post₂ : α -> Prop):
   [totl| wp x post₁] ⊓ [part| wp x post₂] = [totl| wp x (post₁ ⊓ post₂)] := by
     unhygienic induction x <;> try simp [loomLogicSimp]
-    { simp [DivM.total_decompose]
+    { --simp [DivM.total_decompose]
       simp [[totl|DivM.wp_eq]]
       split
       { simp }

Loom/MonadAlgebras/Instances/Gen.lean

@@ -8,11 +8,12 @@ open Plausible
 
 universe u
 
+-- TODO: Fix this instance
 /- Ordered Monad Algebra instance for Gen -/
-instance MAlgGenInst : MAlgOrdered Gen (ULift Nat -> ULift StdGen -> Prop) :=
-  inferInstanceAs
-    (MAlgOrdered
-      (ReaderT (ULift Nat)
-        (StateT (ULift StdGen) Id))
-      (ULift Nat ->
-        ULift StdGen -> Prop))
+-- instance MAlgGenInst : MAlgOrdered Gen (ULift Nat -> ULift StdGen -> Prop) :=
+--   inferInstanceAs
+--     (MAlgOrdered
+--       (ReaderT (ULift Nat)
+--         (StateT (ULift StdGen) Id))
+--       (ULift Nat ->
+--         ULift StdGen -> Prop))

Loom/MonadAlgebras/WP/Basic.lean

@@ -500,11 +500,12 @@ section Gen
 
 open Plausible
 
+-- TODO: Fix this instance
 /- WP for rand in Gen -/
-lemma Gen.wp_rand {α : Type} (c : Gen α) :
-  triple ⊤ c (fun _ => ⊤) := by
-    simp [triple, MAlgGenInst, ReaderT.wp_eq, StateT.wp_eq]
-    simp [wp, liftM, monadLift, MAlg.lift, MAlgOrdered.μ]; rfl
+-- lemma Gen.wp_rand {α : Type} (c : Gen α) :
+--   triple ⊤ c (fun _ => ⊤) := by
+--     simp [triple, MAlgGenInst, ReaderT.wp_eq, StateT.wp_eq]
+--     simp [wp, liftM, monadLift, MAlg.lift, MAlgOrdered.μ]; rfl
 
 end Gen