Move Boole dialect to the StrataBoole package

.github/workflows/ci.yml

@@ -65,6 +65,9 @@ jobs:
           git diff --exit-code editors/vscode/syntaxes/ editors/emacs/
       - name: Build and run strata verify
         run: lake exe strata verify Examples/SimpleProc.core.st
+      - name: Build StrataBoole
+        run: lake build StrataBoole StrataBooleTest
+        working-directory: StrataBoole
       - name: Build BoogieToStrata
         run: dotnet build -warnaserror ${SOLUTION}
       - name: Test BoogieToStrata

Strata.lean

@@ -38,8 +38,6 @@ import Strata.Transform.Specification
 
 /- Strata Languages — additional -/
 import Strata.Languages.B3
-import Strata.Languages.Boole.Boole
-import Strata.Languages.Boole.Verify
 import Strata.Languages.C_Simp.C_Simp
 import Strata.Languages.C_Simp.Verify
 import Strata.Languages.Core.EntryPoint

Strata/MetaVerifier.lean

@@ -7,13 +7,11 @@ module
 
 import Strata.Transform.LoopElim
 import Strata.Languages.Core.ObligationExtraction
-public import Strata.Languages.Boole.Boole
 public import Strata.Languages.C_Simp.C_Simp
 public import Strata.Languages.Core.SMTEncoder
 import Std.Tactic.BVDecide.Normalize.Prop
 import Strata.DL.Lambda.Denote.LExprAnnotated
 import Strata.DL.SMT.Denote
-import Strata.Languages.Boole.Verify
 import Strata.Languages.C_Simp.DDMTransform.Translate
 import Strata.Languages.C_Simp.Verify
 import Strata.Languages.Core.Core
@@ -98,19 +96,14 @@ def genVCs (program : Strata.C_Simp.Program) (options : Core.VerifyOptions := .d
 
 end C_Simp
 
-namespace Boole
-
-def genVCs (program : Strata.Boole.Program) (gctx : Strata.GlobalContext) (options : Core.VerifyOptions := .default) : Option Core.coreVCs := do
-  let program ← (Strata.Boole.toCoreProgram program gctx).toOption
-  Core.genVCs program options
-
-end Boole
-
 namespace Strata
 
 /--
 Generate verification conditions for a `Strata.Program` by translating it to the
 appropriate frontend verifier and collecting its deferred proof obligations.
+
+Note that this can be extended to new dialects by using
+`unsafe/@[implemented_by]` as in `StrataBoole.MetaVerifier`.
 -/
 def genCoreVCs (program : Program) : Option Core.coreVCs := do
   if program.dialect == "Core" then
@@ -119,11 +112,6 @@ def genCoreVCs (program : Program) : Option Core.coreVCs := do
   else if program.dialect == "C_Simp" then
     let (program, #[]) := C_Simp.TransM.run default (C_Simp.translateProgram program.commands) | none
     C_Simp.genVCs program { (default : Core.VerifyOptions) with verbose := .quiet : Core.VerifyOptions }
-  else if program.dialect == "Boole" then
-    match Boole.getProgram program with
-    | .ok booleProgram =>
-      Boole.genVCs booleProgram program.globalContext { (default : Core.VerifyOptions) with verbose := .quiet : Core.VerifyOptions }
-    | .error _ => none
   else
     none
 

StrataBoole/.gitignore

@@ -0,0 +1 @@
+.lake

StrataBoole/StrataBoole.lean

@@ -0,0 +1,9 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import StrataBoole.Boole
+import StrataBoole.Grammar
+import StrataBoole.MetaVerifier
+import StrataBoole.Verify

Strata/Languages/Boole/Boole.lean → StrataBoole/StrataBoole/Boole.lean

@@ -5,7 +5,7 @@
 -/
 module
 
-public import Strata.Languages.Boole.Grammar -- shake: keep
+public import StrataBoole.Grammar -- shake: keep
 import Strata.DDM.Integration.Lean.Gen -- shake: keep
 
 public section

StrataBoole/StrataBoole/MetaVerifier.lean

@@ -0,0 +1,118 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.MetaVerifier -- shake: keep
+public import StrataBoole.Verify
+meta import Lean.Meta.Eval
+import Lean.Meta.Eval -- shake: keep
+import Lean.Meta.Tactic.Rewrite -- shake: keep
+meta import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Unfold -- shake: keep
+meta import Lean.Meta.Tactic.Unfold
+
+/-!
+# Boole MetaVerifier
+
+Extends `Strata.MetaVerifier` with Boole dialect support for `genCoreVCs` and
+`smtVCsCorrect`. Test files in the `StrataBoole` package should import this
+module instead of `Strata.MetaVerifier` directly.
+-/
+
+public section
+
+namespace Strata.Boole
+
+def genVCs (program : Strata.Boole.Program) (gctx : Strata.GlobalContext) (options : Core.VerifyOptions := .default) : Option Core.coreVCs := do
+  let program ← (Strata.Boole.toCoreProgram program gctx).toOption
+  Core.genVCs program options
+
+end Strata.Boole
+
+namespace Strata
+
+/--
+Generate verification conditions for a `Strata.Program`, with Boole support.
+Extends `Strata.genCoreVCs` to handle the Boole dialect.
+-/
+def genCoreVCsBoole (program : Program) : Option Core.coreVCs := do
+  if program.dialect == "Boole" then
+    match Boole.getProgram program with
+    | .ok booleProgram =>
+      Boole.genVCs booleProgram program.globalContext { (default : Core.VerifyOptions) with verbose := .quiet : Core.VerifyOptions }
+    | .error _ => none
+  else
+    genCoreVCs program
+
+/--
+Generate SMT verification conditions for a `Strata.Program`, with Boole support.
+-/
+def genSMTVCsBoole (program : Program) : Option SMT.SMTVCs := do
+  let coreVCs ← genCoreVCsBoole program
+  toSMTVCs coreVCs
+
+/--
+State semantic correctness of the SMT verification conditions generated for a
+program, with Boole dialect support.
+-/
+def smtVCsCorrectBoole (program : Program) : Prop :=
+  match genSMTVCsBoole program with
+  | some vcs => (denoteQueries vcs).getD False
+  | none     => False
+
+end Strata
+
+namespace Strata.Meta
+
+open Lean hiding Options
+
+private unsafe def genSMTVCsBooleUnsafe (mv : MVarId) : MetaM (List MVarId) := do
+  let type ← mv.getType
+  let some program := type.app1? ``Strata.smtVCsCorrectBoole | throwError "Expected a Strata.smtVCsCorrectBoole goal"
+  trace[debug] m!"Generating SMT VCs for {program}"
+  let mv ← Meta.unfoldTarget mv ``Strata.smtVCsCorrectBoole
+  let ovcs := .app (.const ``Strata.genSMTVCsBoole []) program
+  let ovcsType := .app (.const ``Option [0]) (.const ``Strata.SMT.SMTVCs [])
+  let some evcs ← Meta.evalExpr (Option Strata.SMT.SMTVCs) ovcsType ovcs
+    | throwError "Failed to generate VCs"
+  trace[debug] m!"Generated {repr evcs}"
+  let rhs := toExpr (some evcs)
+  let eqVCs := mkApp3 (.const ``Eq [1]) ovcsType ovcs rhs
+  let hEQVCs ← nativeDecide eqVCs
+  let r ← mv.rewrite (← mv.getType) hEQVCs
+  let mv ← mv.replaceTargetEq r.eNew r.eqProof
+  let mvs ← evcs.mapM SMT.createGoal
+  trace[debug] m!"Created {mvs.length} SMT VC goals: {mvs}"
+  let ps ← mvs.mapM MVarId.getType
+  let hP := andNIntro (List.zip ps (mvs.map Expr.mvar))
+  mv.assign hP
+  return mvs
+
+@[implemented_by genSMTVCsBooleUnsafe]
+meta opaque genSMTVCsBoole (mv : MVarId) : MetaM (List MVarId)
+
+end Strata.Meta
+
+namespace Strata.Tactic
+
+open Lean Elab Tactic in
+/--
+Generate one Lean goal per SMT verification condition in a goal of the form
+`Strata.smtVCsCorrectBoole program`. Boole-aware variant of `gen_smt_vcs`.
+-/
+syntax (name := genSMTVCsBoole) "gen_smt_vcs_boole" : tactic
+
+open Lean Elab Tactic in
+@[tactic genSMTVCsBoole] meta def evalGenSMTVCsBoole : Tactic := fun stx => do
+  match stx with
+  | `(tactic| gen_smt_vcs_boole) =>
+    let mvs ← Meta.genSMTVCsBoole (← Tactic.getMainGoal)
+    Tactic.replaceMainGoal mvs
+  | _ => throwUnsupportedSyntax
+
+end Strata.Tactic
+
+end -- public section

Strata/Languages/Boole/Verify.lean → StrataBoole/StrataBoole/Verify.lean

@@ -5,7 +5,7 @@
 -/
 module
 
-public import Strata.Languages.Boole.Boole
+public import StrataBoole.Boole
 public import Strata.Languages.Core.Verifier
 import Strata.Languages.Core.Core
 import Strata.Util.Tactics

StrataBoole/StrataBooleTest.lean

@@ -0,0 +1,46 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import StrataBooleTest.array_2d
+import StrataBooleTest.array_assignment
+import StrataBooleTest.bit_vectors
+import StrataBooleTest.code_expression
+import StrataBooleTest.demo
+import StrataBooleTest.deterministic
+import StrataBooleTest.find_max
+import StrataBooleTest.find_max_verus
+import StrataBooleTest.format_program
+import StrataBooleTest.function_definitions
+import StrataBooleTest.global_readonly_call
+import StrataBooleTest.grammar_extensions
+import StrataBooleTest.insertion_sort
+import StrataBooleTest.loop_simple
+import StrataBooleTest.procedure_signatures
+import StrataBooleTest.square_matrix_multiply
+import StrataBooleTest.stack_array_based
+import StrataBooleTest.string_operators
+import StrataBooleTest.top_level_block_selection
+import StrataBooleTest.verification_coverage
+import StrataBooleTest.FeatureRequests.abstract_types_and_stubs
+import StrataBooleTest.FeatureRequests.bitvector_ops
+import StrataBooleTest.FeatureRequests.bitvector_proof_mode
+import StrataBooleTest.FeatureRequests.choose_operator
+import StrataBooleTest.FeatureRequests.datatypes_and_selectors
+import StrataBooleTest.FeatureRequests.decreases_metadata
+import StrataBooleTest.FeatureRequests.early_return
+import StrataBooleTest.FeatureRequests.higher_order_encoding
+import StrataBooleTest.FeatureRequests.horner_poly_eval
+import StrataBooleTest.FeatureRequests.lambda_closure
+import StrataBooleTest.FeatureRequests.map_extensionality
+import StrataBooleTest.FeatureRequests.mutual_recursion
+import StrataBooleTest.FeatureRequests.nat_int_boundary
+import StrataBooleTest.FeatureRequests.opaque_reveal_hide
+import StrataBooleTest.FeatureRequests.option_matches
+import StrataBooleTest.FeatureRequests.overflow_guard
+import StrataBooleTest.FeatureRequests.reveal_with_fuel
+import StrataBooleTest.FeatureRequests.seq_slicing
+import StrataBooleTest.FeatureRequests.struct_field_access
+import StrataBooleTest.FeatureRequests.trait_spec_methods
+import StrataBooleTest.FeatureRequests.widening_casts

StrataTest/Languages/Boole/FeatureRequests/abstract_types_and_stubs.lean → StrataBoole/StrataBooleTest/FeatureRequests/abstract_types_and_stubs.lean

@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.MetaVerifier
+import StrataBoole.MetaVerifier
 
 open Strata
 
@@ -55,6 +55,6 @@ spec {
 #guard_msgs (drop info) in
 #eval Strata.Boole.verify "cvc5" abstractTypesAndStubsSeed
 
-example : Strata.smtVCsCorrect abstractTypesAndStubsSeed := by
-  gen_smt_vcs
+example : Strata.smtVCsCorrectBoole abstractTypesAndStubsSeed := by
+  gen_smt_vcs_boole
   all_goals (try grind)

StrataTest/Languages/Boole/FeatureRequests/bitvector_ops.lean → StrataBoole/StrataBooleTest/FeatureRequests/bitvector_ops.lean

@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.MetaVerifier
+import StrataBoole.MetaVerifier
 
 open Strata
 
@@ -46,8 +46,8 @@ spec {
 #guard_msgs (drop info) in
 #eval Strata.Boole.verify "cvc5" bitvectorOpsSeed (options := .quiet)
 
-example : Strata.smtVCsCorrect bitvectorOpsSeed := by
-  gen_smt_vcs
+example : Strata.smtVCsCorrectBoole bitvectorOpsSeed := by
+  gen_smt_vcs_boole
   all_goals (first | grind | decide)
 
 -- Exercises ~, ^, >>, << (bit extraction, conditional swap, nibble ops).
@@ -81,8 +81,8 @@ spec {
 #guard_msgs (drop info) in
 #eval Strata.Boole.verify "cvc5" bitvectorShiftXorSeed (options := .quiet)
 
-example : Strata.smtVCsCorrect bitvectorShiftXorSeed := by
-  gen_smt_vcs
+example : Strata.smtVCsCorrectBoole bitvectorShiftXorSeed := by
+  gen_smt_vcs_boole
   all_goals (first | grind | decide)
 
 -- Exercises >>s (arithmetic/signed right shift): vacated bits are filled with
@@ -107,6 +107,6 @@ spec {
 #guard_msgs (drop info) in
 #eval Strata.Boole.verify "cvc5" bitvectorSShrSeed (options := .quiet)
 
-example : Strata.smtVCsCorrect bitvectorSShrSeed := by
-  gen_smt_vcs
+example : Strata.smtVCsCorrectBoole bitvectorSShrSeed := by
+  gen_smt_vcs_boole
   all_goals (first | grind | decide)

StrataTest/Languages/Boole/FeatureRequests/bitvector_proof_mode.lean → StrataBoole/StrataBooleTest/FeatureRequests/bitvector_proof_mode.lean

@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.MetaVerifier
+import StrataBoole.MetaVerifier
 
 open Strata
 

StrataTest/Languages/Boole/FeatureRequests/choose_operator.lean → StrataBoole/StrataBooleTest/FeatureRequests/choose_operator.lean

@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.MetaVerifier
+import StrataBoole.MetaVerifier
 
 open Strata
 
@@ -48,13 +48,15 @@ spec {
 };
 #end
 
-/-- info:
-Obligation: choose_seed_ensures_1_1077
+/--
+info:
+Obligation: choose_seed_ensures_1_1082
 Property: assert
-Result: ✅ pass-/
+Result: ✅ pass
+-/
 #guard_msgs in
 #eval Strata.Boole.verify "cvc5" chooseOperatorSeed (options :=.quiet)
 
-example : Strata.smtVCsCorrect chooseOperatorSeed := by
-  gen_smt_vcs
+example : Strata.smtVCsCorrectBoole chooseOperatorSeed := by
+  gen_smt_vcs_boole
   all_goals (try grind)