From 254160cb9f2963dcfa590bd6c34ee9680e5e99e8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 21 May 2026 13:49:37 -0700 Subject: [PATCH 1/3] Move Boole dialect to the StrataBoole package --- .github/workflows/ci.yml | 21 ++++ Strata.lean | 2 - Strata/MetaVerifier.lean | 15 --- StrataBoole/.gitignore | 1 + StrataBoole/StrataBoole.lean | 4 + .../StrataBoole}/Boole.lean | 2 +- .../StrataBoole}/Grammar.lean | 0 StrataBoole/StrataBoole/MetaVerifier.lean | 118 ++++++++++++++++++ .../StrataBoole}/Verify.lean | 2 +- StrataBoole/StrataBooleTest.lean | 41 ++++++ .../abstract_types_and_stubs.lean | 6 +- .../FeatureRequests/bitvector_ops.lean | 14 +-- .../FeatureRequests/bitvector_proof_mode.lean | 2 +- .../FeatureRequests/choose_operator.lean | 14 ++- .../datatypes_and_selectors.lean | 20 +-- .../FeatureRequests/decreases_metadata.lean | 14 ++- .../FeatureRequests/early_return.lean | 11 +- .../higher_order_encoding.lean | 14 ++- .../FeatureRequests/horner_poly_eval.lean | 6 +- .../FeatureRequests/lambda_closure.lean | 6 +- .../FeatureRequests/map_extensionality.lean | 8 +- .../FeatureRequests/mutual_recursion.lean | 6 +- .../FeatureRequests/nat_int_boundary.lean | 6 +- .../FeatureRequests/opaque_reveal_hide.lean | 6 +- .../FeatureRequests/option_matches.lean | 2 +- .../FeatureRequests/overflow_guard.lean | 18 +-- .../FeatureRequests/reveal_with_fuel.lean | 6 +- .../FeatureRequests/seq_slicing.lean | 2 +- .../FeatureRequests/struct_field_access.lean | 2 +- .../FeatureRequests/trait_spec_methods.lean | 2 +- .../FeatureRequests/widening_casts.lean | 6 +- .../StrataBooleTest}/array_2d.lean | 6 +- .../StrataBooleTest}/array_assignment.lean | 6 +- .../StrataBooleTest}/bit_vectors.lean | 6 +- .../StrataBooleTest}/code_expression.lean | 6 +- .../StrataBooleTest}/demo.lean | 10 +- .../StrataBooleTest}/deterministic.lean | 16 +-- .../StrataBooleTest}/find_max.lean | 15 ++- .../StrataBooleTest}/find_max_verus.lean | 24 ++-- .../StrataBooleTest}/format_program.lean | 2 +- .../function_definitions.lean | 13 +- .../global_readonly_call.lean | 26 ++-- .../StrataBooleTest}/grammar_extensions.lean | 6 +- .../StrataBooleTest}/insertion_sort.lean | 6 +- .../StrataBooleTest}/loop_simple.lean | 6 +- .../procedure_signatures.lean | 2 +- .../square_matrix_multiply.lean | 6 +- .../StrataBooleTest}/stack_array_based.lean | 56 ++++----- .../StrataBooleTest}/string_operators.lean | 32 ++--- .../top_level_block_selection.lean | 6 +- .../verification_coverage.lean | 46 +++---- StrataBoole/lake-manifest.json | 22 ++++ StrataBoole/lakefile.toml | 13 ++ StrataBoole/lean-toolchain | 1 + StrataMainLib.lean | 8 +- 55 files changed, 470 insertions(+), 247 deletions(-) create mode 100644 StrataBoole/.gitignore create mode 100644 StrataBoole/StrataBoole.lean rename {Strata/Languages/Boole => StrataBoole/StrataBoole}/Boole.lean (89%) rename {Strata/Languages/Boole => StrataBoole/StrataBoole}/Grammar.lean (100%) create mode 100644 StrataBoole/StrataBoole/MetaVerifier.lean rename {Strata/Languages/Boole => StrataBoole/StrataBoole}/Verify.lean (99%) create mode 100644 StrataBoole/StrataBooleTest.lean rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/abstract_types_and_stubs.lean (93%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/bitvector_ops.lean (92%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/bitvector_proof_mode.lean (97%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/choose_operator.lean (87%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/datatypes_and_selectors.lean (83%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/decreases_metadata.lean (90%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/early_return.lean (86%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/higher_order_encoding.lean (86%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/horner_poly_eval.lean (92%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/lambda_closure.lean (90%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/map_extensionality.lean (95%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/mutual_recursion.lean (95%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/nat_int_boundary.lean (92%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/opaque_reveal_hide.lean (94%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/option_matches.lean (98%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/overflow_guard.lean (83%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/reveal_with_fuel.lean (94%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/seq_slicing.lean (97%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/struct_field_access.lean (98%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/trait_spec_methods.lean (98%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/FeatureRequests/widening_casts.lean (92%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/array_2d.lean (78%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/array_assignment.lean (83%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/bit_vectors.lean (83%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/code_expression.lean (93%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/demo.lean (93%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/deterministic.lean (78%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/find_max.lean (79%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/find_max_verus.lean (87%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/format_program.lean (97%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/function_definitions.lean (74%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/global_readonly_call.lean (87%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/grammar_extensions.lean (92%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/insertion_sort.lean (90%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/loop_simple.lean (87%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/procedure_signatures.lean (99%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/square_matrix_multiply.lean (94%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/stack_array_based.lean (82%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/string_operators.lean (89%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/top_level_block_selection.lean (83%) rename {StrataTest/Languages/Boole => StrataBoole/StrataBooleTest}/verification_coverage.lean (86%) create mode 100644 StrataBoole/lake-manifest.json create mode 100644 StrataBoole/lakefile.toml create mode 100644 StrataBoole/lean-toolchain diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6fc9cc26de..b36f670d23 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -97,6 +97,27 @@ jobs: working-directory: StrataTest/Languages/Python/Regex run: python diff_test.py + build_strata_boole: + needs: build_and_test_lean + name: Build StrataBoole + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v6 + - name: Restore lake cache + uses: ./.github/actions/restore-lake-cache + with: + fail-on-cache-miss: "true" + use-restore-keys: "false" + - name: Install Lean + uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + - name: Build StrataBoole + run: lake build StrataBoole StrataBooleTest + working-directory: StrataBoole + check_pending_python: needs: build_and_test_lean name: Check pending Python tests diff --git a/Strata.lean b/Strata.lean index e1428c20c5..1d73306335 100644 --- a/Strata.lean +++ b/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 diff --git a/Strata/MetaVerifier.lean b/Strata/MetaVerifier.lean index 910831d9a4..1d61bb1570 100644 --- a/Strata/MetaVerifier.lean +++ b/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,14 +96,6 @@ 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 /-- @@ -119,11 +109,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 diff --git a/StrataBoole/.gitignore b/StrataBoole/.gitignore new file mode 100644 index 0000000000..2b00952692 --- /dev/null +++ b/StrataBoole/.gitignore @@ -0,0 +1 @@ +.lake diff --git a/StrataBoole/StrataBoole.lean b/StrataBoole/StrataBoole.lean new file mode 100644 index 0000000000..9d21ce8979 --- /dev/null +++ b/StrataBoole/StrataBoole.lean @@ -0,0 +1,4 @@ +import StrataBoole.Boole +import StrataBoole.Grammar +import StrataBoole.MetaVerifier +import StrataBoole.Verify diff --git a/Strata/Languages/Boole/Boole.lean b/StrataBoole/StrataBoole/Boole.lean similarity index 89% rename from Strata/Languages/Boole/Boole.lean rename to StrataBoole/StrataBoole/Boole.lean index e733208d2e..0734f4a729 100644 --- a/Strata/Languages/Boole/Boole.lean +++ b/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 diff --git a/Strata/Languages/Boole/Grammar.lean b/StrataBoole/StrataBoole/Grammar.lean similarity index 100% rename from Strata/Languages/Boole/Grammar.lean rename to StrataBoole/StrataBoole/Grammar.lean diff --git a/StrataBoole/StrataBoole/MetaVerifier.lean b/StrataBoole/StrataBoole/MetaVerifier.lean new file mode 100644 index 0000000000..38ad58cecb --- /dev/null +++ b/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 diff --git a/Strata/Languages/Boole/Verify.lean b/StrataBoole/StrataBoole/Verify.lean similarity index 99% rename from Strata/Languages/Boole/Verify.lean rename to StrataBoole/StrataBoole/Verify.lean index 911f096294..40536e4c62 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/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 diff --git a/StrataBoole/StrataBooleTest.lean b/StrataBoole/StrataBooleTest.lean new file mode 100644 index 0000000000..728d78bd51 --- /dev/null +++ b/StrataBoole/StrataBooleTest.lean @@ -0,0 +1,41 @@ +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 diff --git a/StrataTest/Languages/Boole/FeatureRequests/abstract_types_and_stubs.lean b/StrataBoole/StrataBooleTest/FeatureRequests/abstract_types_and_stubs.lean similarity index 93% rename from StrataTest/Languages/Boole/FeatureRequests/abstract_types_and_stubs.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/abstract_types_and_stubs.lean index 803eca6087..39e6d22e1f 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/abstract_types_and_stubs.lean +++ b/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) diff --git a/StrataTest/Languages/Boole/FeatureRequests/bitvector_ops.lean b/StrataBoole/StrataBooleTest/FeatureRequests/bitvector_ops.lean similarity index 92% rename from StrataTest/Languages/Boole/FeatureRequests/bitvector_ops.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/bitvector_ops.lean index 2bb64eb7fd..3f8036cd64 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/bitvector_ops.lean +++ b/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) diff --git a/StrataTest/Languages/Boole/FeatureRequests/bitvector_proof_mode.lean b/StrataBoole/StrataBooleTest/FeatureRequests/bitvector_proof_mode.lean similarity index 97% rename from StrataTest/Languages/Boole/FeatureRequests/bitvector_proof_mode.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/bitvector_proof_mode.lean index 44219536b6..d1b7294095 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/bitvector_proof_mode.lean +++ b/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 diff --git a/StrataTest/Languages/Boole/FeatureRequests/choose_operator.lean b/StrataBoole/StrataBooleTest/FeatureRequests/choose_operator.lean similarity index 87% rename from StrataTest/Languages/Boole/FeatureRequests/choose_operator.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/choose_operator.lean index 52a7a0724e..cb3e1e9fcb 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/choose_operator.lean +++ b/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) diff --git a/StrataTest/Languages/Boole/FeatureRequests/datatypes_and_selectors.lean b/StrataBoole/StrataBooleTest/FeatureRequests/datatypes_and_selectors.lean similarity index 83% rename from StrataTest/Languages/Boole/FeatureRequests/datatypes_and_selectors.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/datatypes_and_selectors.lean index a2ad320a41..146321c578 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/datatypes_and_selectors.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/datatypes_and_selectors.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -48,16 +48,17 @@ spec { }; #end -/-- info: -Obligation: assert_1_1159 +/-- +info: +Obligation: assert_1_1164 Property: assert Result: ✅ pass -Obligation: assert_assert_2_1190_calls_OptionInt..val_0 +Obligation: assert_assert_2_1195_calls_OptionInt..val_0 Property: assert Result: ✅ pass -Obligation: assert_2_1190 +Obligation: assert_2_1195 Property: assert Result: ✅ pass @@ -65,12 +66,13 @@ Obligation: set_ok_calls_OptionInt..val_0 Property: assert Result: ✅ pass -Obligation: datatype_selector_seed_ensures_0_1103 +Obligation: datatype_selector_seed_ensures_0_1108 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" datatypeSelectorsSeed (options := .quiet) -example : Strata.smtVCsCorrect datatypeSelectorsSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole datatypeSelectorsSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/decreases_metadata.lean b/StrataBoole/StrataBooleTest/FeatureRequests/decreases_metadata.lean similarity index 90% rename from StrataTest/Languages/Boole/FeatureRequests/decreases_metadata.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/decreases_metadata.lean index dbb14255ab..66221dfb7d 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/decreases_metadata.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/decreases_metadata.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -57,7 +57,8 @@ spec { }; #end -/-- info: +/-- +info: Obligation: entry_invariant_0_0 Property: assert Result: ✅ pass @@ -74,12 +75,13 @@ Obligation: arbitrary_iter_maintain_invariant_0_1 Property: assert Result: ✅ pass -Obligation: loop_measure_seed_ensures_1_1174 +Obligation: loop_measure_seed_ensures_1_1179 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" decreasesMetadataSeed (options:=.quiet) -example : Strata.smtVCsCorrect decreasesMetadataSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole decreasesMetadataSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/early_return.lean b/StrataBoole/StrataBooleTest/FeatureRequests/early_return.lean similarity index 86% rename from StrataTest/Languages/Boole/FeatureRequests/early_return.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/early_return.lean index acef8f5b9e..03da210783 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/early_return.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/early_return.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -39,14 +39,15 @@ spec { }; #end -/-- info: -Obligation: abs_seed_ensures_0_797 +/-- +info: +Obligation: abs_seed_ensures_0_802 Property: assert Result: ✅ pass -/ #guard_msgs in #eval Strata.Boole.verify "cvc5" earlyReturnSeed (options := .quiet) -example : Strata.smtVCsCorrect earlyReturnSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole earlyReturnSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/higher_order_encoding.lean b/StrataBoole/StrataBooleTest/FeatureRequests/higher_order_encoding.lean similarity index 86% rename from StrataTest/Languages/Boole/FeatureRequests/higher_order_encoding.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/higher_order_encoding.lean index ce9c2f9570..a229db44ea 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/higher_order_encoding.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/higher_order_encoding.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -42,13 +42,15 @@ spec { }; #end -/-- info: -Obligation: higher_order_seed_ensures_0_983 +/-- +info: +Obligation: higher_order_seed_ensures_0_988 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" higherOrderSeed (options:=.quiet) -example : Strata.smtVCsCorrect higherOrderSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole higherOrderSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/horner_poly_eval.lean b/StrataBoole/StrataBooleTest/FeatureRequests/horner_poly_eval.lean similarity index 92% rename from StrataTest/Languages/Boole/FeatureRequests/horner_poly_eval.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/horner_poly_eval.lean index c8a553b957..53b60e0b02 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/horner_poly_eval.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/horner_poly_eval.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier ------------------------------------------------------------ namespace Strata @@ -57,6 +57,6 @@ spec #guard_msgs in #eval Strata.Boole.verify "cvc5" hornerPgm (options := .quiet) -example : Strata.smtVCsCorrect hornerPgm := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole hornerPgm := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/lambda_closure.lean b/StrataBoole/StrataBooleTest/FeatureRequests/lambda_closure.lean similarity index 90% rename from StrataTest/Languages/Boole/FeatureRequests/lambda_closure.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/lambda_closure.lean index 4a131e5342..9d445ad559 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/lambda_closure.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/lambda_closure.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -54,6 +54,6 @@ procedure use_lambda() returns () #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" lambdaClosureSeed -example : Strata.smtVCsCorrect lambdaClosureSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole lambdaClosureSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean b/StrataBoole/StrataBooleTest/FeatureRequests/map_extensionality.lean similarity index 95% rename from StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/map_extensionality.lean index e5406a653b..554d7eb7d3 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/map_extensionality.lean @@ -4,8 +4,8 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier -import Strata.Languages.Boole.Verify +import StrataBoole.MetaVerifier +import StrataBoole.Verify open Strata open Lambda @@ -53,8 +53,8 @@ spec { #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" mapExtensionalitySeed -example : Strata.smtVCsCorrect mapExtensionalitySeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole mapExtensionalitySeed := by + gen_smt_vcs_boole all_goals intro Map inst select a b hPointwise i exact hPointwise i diff --git a/StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean b/StrataBoole/StrataBooleTest/FeatureRequests/mutual_recursion.lean similarity index 95% rename from StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/mutual_recursion.lean index 548cb37a50..17a4e985c2 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/mutual_recursion.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -67,8 +67,8 @@ spec { #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" mutualRecursionSeed -example : Strata.smtVCsCorrect mutualRecursionSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole mutualRecursionSeed := by + gen_smt_vcs_boole all_goals (try grind) -- Still open: mutual recursion over int requires a decreases clause. diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_int_boundary.lean b/StrataBoole/StrataBooleTest/FeatureRequests/nat_int_boundary.lean similarity index 92% rename from StrataTest/Languages/Boole/FeatureRequests/nat_int_boundary.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/nat_int_boundary.lean index c049a99945..fe9e9cf79e 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/nat_int_boundary.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/nat_int_boundary.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -51,6 +51,6 @@ spec { #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" natIntBoundarySeed -example : Strata.smtVCsCorrect natIntBoundarySeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole natIntBoundarySeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/opaque_reveal_hide.lean b/StrataBoole/StrataBooleTest/FeatureRequests/opaque_reveal_hide.lean similarity index 94% rename from StrataTest/Languages/Boole/FeatureRequests/opaque_reveal_hide.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/opaque_reveal_hide.lean index e3ed888a99..6a6eb71553 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/opaque_reveal_hide.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/opaque_reveal_hide.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -60,6 +60,6 @@ procedure opaque_reveal_hide_seed(x: int) returns () #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" opaqueRevealHideSeed -example : Strata.smtVCsCorrect opaqueRevealHideSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole opaqueRevealHideSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/option_matches.lean b/StrataBoole/StrataBooleTest/FeatureRequests/option_matches.lean similarity index 98% rename from StrataTest/Languages/Boole/FeatureRequests/option_matches.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/option_matches.lean index 1035da7573..4930a7d76e 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/option_matches.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/option_matches.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata diff --git a/StrataTest/Languages/Boole/FeatureRequests/overflow_guard.lean b/StrataBoole/StrataBooleTest/FeatureRequests/overflow_guard.lean similarity index 83% rename from StrataTest/Languages/Boole/FeatureRequests/overflow_guard.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/overflow_guard.lean index 264b8bae5f..7e5fc81b24 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/overflow_guard.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/overflow_guard.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -46,21 +46,23 @@ spec { }; #end -/-- info: -Obligation: assert_6_1175 +/-- +info: +Obligation: assert_6_1180 Property: assert Result: ✅ pass -Obligation: overflow_guard_seed_ensures_4_1112 +Obligation: overflow_guard_seed_ensures_4_1117 Property: assert Result: ✅ pass -Obligation: overflow_guard_seed_ensures_5_1134 +Obligation: overflow_guard_seed_ensures_5_1139 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" overflowGuardSeed (options := .quiet) -example : Strata.smtVCsCorrect overflowGuardSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole overflowGuardSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/reveal_with_fuel.lean b/StrataBoole/StrataBooleTest/FeatureRequests/reveal_with_fuel.lean similarity index 94% rename from StrataTest/Languages/Boole/FeatureRequests/reveal_with_fuel.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/reveal_with_fuel.lean index d41a37e3bd..ce5ea8a59d 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/reveal_with_fuel.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/reveal_with_fuel.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -61,6 +61,6 @@ spec { #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" revealWithFuelSeed -example : Strata.smtVCsCorrect revealWithFuelSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole revealWithFuelSeed := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean b/StrataBoole/StrataBooleTest/FeatureRequests/seq_slicing.lean similarity index 97% rename from StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/seq_slicing.lean index e69a0d205c..606bfba32d 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/seq_slicing.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata diff --git a/StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean b/StrataBoole/StrataBooleTest/FeatureRequests/struct_field_access.lean similarity index 98% rename from StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/struct_field_access.lean index b263203015..2b6a4febde 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/struct_field_access.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata diff --git a/StrataTest/Languages/Boole/FeatureRequests/trait_spec_methods.lean b/StrataBoole/StrataBooleTest/FeatureRequests/trait_spec_methods.lean similarity index 98% rename from StrataTest/Languages/Boole/FeatureRequests/trait_spec_methods.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/trait_spec_methods.lean index 6ba4d1f467..923c7cba2f 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/trait_spec_methods.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/trait_spec_methods.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata diff --git a/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean b/StrataBoole/StrataBooleTest/FeatureRequests/widening_casts.lean similarity index 92% rename from StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean rename to StrataBoole/StrataBooleTest/FeatureRequests/widening_casts.lean index 8ce2ca7f1e..5b9e44060a 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean +++ b/StrataBoole/StrataBooleTest/FeatureRequests/widening_casts.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -48,8 +48,8 @@ spec { #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" wideningCastsSeed -example : Strata.smtVCsCorrect wideningCastsSeed := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole wideningCastsSeed := by + gen_smt_vcs_boole all_goals intro Map inst n bv32_to_int_u select v hNonneg hn i hi exact hNonneg (select v i) diff --git a/StrataTest/Languages/Boole/array_2d.lean b/StrataBoole/StrataBooleTest/array_2d.lean similarity index 78% rename from StrataTest/Languages/Boole/array_2d.lean rename to StrataBoole/StrataBooleTest/array_2d.lean index b40e988876..980a752cee 100644 --- a/StrataTest/Languages/Boole/array_2d.lean +++ b/StrataBoole/StrataBooleTest/array_2d.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -24,6 +24,6 @@ procedure array_2d_write_read(i: int, j: int, v: int) returns () #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" array_2d -example : Strata.smtVCsCorrect array_2d := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole array_2d := by + gen_smt_vcs_boole all_goals grind diff --git a/StrataTest/Languages/Boole/array_assignment.lean b/StrataBoole/StrataBooleTest/array_assignment.lean similarity index 83% rename from StrataTest/Languages/Boole/array_assignment.lean rename to StrataBoole/StrataBooleTest/array_assignment.lean index d8c870255b..504d5460c3 100644 --- a/StrataTest/Languages/Boole/array_assignment.lean +++ b/StrataBoole/StrataBooleTest/array_assignment.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -36,6 +36,6 @@ procedure matrix_transpose (A: Matrix, m: int, n: int) returns (B: Matrix) #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" matrix_transpose_example -theorem matrix_transpose_smt_vcs_correct : Strata.smtVCsCorrect matrix_transpose_example := by - gen_smt_vcs +theorem matrix_transpose_smt_vcs_correct : Strata.smtVCsCorrectBoole matrix_transpose_example := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/bit_vectors.lean b/StrataBoole/StrataBooleTest/bit_vectors.lean similarity index 83% rename from StrataTest/Languages/Boole/bit_vectors.lean rename to StrataBoole/StrataBooleTest/bit_vectors.lean index 0b567ab526..c07976ee28 100644 --- a/StrataTest/Languages/Boole/bit_vectors.lean +++ b/StrataBoole/StrataBooleTest/bit_vectors.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier private def bit_vectors := #strata @@ -37,6 +37,6 @@ spec { #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" bit_vectors -example : Strata.smtVCsCorrect bit_vectors := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole bit_vectors := by + gen_smt_vcs_boole all_goals grind diff --git a/StrataTest/Languages/Boole/code_expression.lean b/StrataBoole/StrataBooleTest/code_expression.lean similarity index 93% rename from StrataTest/Languages/Boole/code_expression.lean rename to StrataBoole/StrataBooleTest/code_expression.lean index 722df809cd..15369bc56c 100644 --- a/StrataTest/Languages/Boole/code_expression.lean +++ b/StrataBoole/StrataBooleTest/code_expression.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -70,6 +70,6 @@ procedure D(a : (Map int T), n : int) returns () #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" code_expression -example : Strata.smtVCsCorrect code_expression := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole code_expression := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/demo.lean b/StrataBoole/StrataBooleTest/demo.lean similarity index 93% rename from StrataTest/Languages/Boole/demo.lean rename to StrataBoole/StrataBooleTest/demo.lean index 0d0b710e00..c50a0aa9cf 100644 --- a/StrataTest/Languages/Boole/demo.lean +++ b/StrataBoole/StrataBooleTest/demo.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -36,11 +36,11 @@ spec { open Strata.SMT -theorem loopSimple_smtVCsCorrect : smtVCsCorrect loopSimple := by - gen_smt_vcs +theorem loopSimple_smtVCsCorrectBoole : smtVCsCorrectBoole loopSimple := by + gen_smt_vcs_boole all_goals (try grind) -/-- info: 'loopSimple_smtVCsCorrect' depends on axioms: [propext, +/-- info: 'loopSimple_smtVCsCorrectBoole' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, @@ -97,4 +97,4 @@ theorem loopSimple_smtVCsCorrect : smtVCsCorrect loopSimple := by Core.bv8SafeUNegFunc._native.native_decide.ax_1✝, Core.bv8SafeUSubFunc._native.native_decide.ax_1✝]-/ #guard_msgs in -#print axioms loopSimple_smtVCsCorrect +#print axioms loopSimple_smtVCsCorrectBoole diff --git a/StrataTest/Languages/Boole/deterministic.lean b/StrataBoole/StrataBooleTest/deterministic.lean similarity index 78% rename from StrataTest/Languages/Boole/deterministic.lean rename to StrataBoole/StrataBooleTest/deterministic.lean index c45c756007..a5f1a55315 100644 --- a/StrataTest/Languages/Boole/deterministic.lean +++ b/StrataBoole/StrataBooleTest/deterministic.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -44,17 +44,19 @@ procedure Check(x1:int, x2:int) returns () #end -/-- info: -Obligation: Foo_ensures_0_251 +/-- +info: +Obligation: Foo_ensures_0_256 Property: assert Result: ✅ pass -Obligation: assert_1_557 +Obligation: assert_1_562 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" deterministic (options := .quiet) -example : Strata.smtVCsCorrect deterministic := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole deterministic := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/find_max.lean b/StrataBoole/StrataBooleTest/find_max.lean similarity index 79% rename from StrataTest/Languages/Boole/find_max.lean rename to StrataBoole/StrataBooleTest/find_max.lean index 3e28f93b5d..01fe508750 100644 --- a/StrataTest/Languages/Boole/find_max.lean +++ b/StrataBoole/StrataBooleTest/find_max.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -33,7 +33,9 @@ spec }; #end -/-- info: Obligation: entry_invariant_0_0 +/-- +info: +Obligation: entry_invariant_0_0 Property: assert Result: ✅ pass @@ -49,12 +51,13 @@ Obligation: arbitrary_iter_maintain_invariant_0_1 Property: assert Result: ✅ pass -Obligation: FindMax_ensures_1_313 +Obligation: FindMax_ensures_1_318 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" find_max_program (options := .quiet) -theorem find_max_program_smt_vcs_correct : Strata.smtVCsCorrect find_max_program := by - gen_smt_vcs +theorem find_max_program_smt_vcs_correct : Strata.smtVCsCorrectBoole find_max_program := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/find_max_verus.lean b/StrataBoole/StrataBooleTest/find_max_verus.lean similarity index 87% rename from StrataTest/Languages/Boole/find_max_verus.lean rename to StrataBoole/StrataBooleTest/find_max_verus.lean index 24f04fab89..e03d69de3b 100644 --- a/StrataTest/Languages/Boole/find_max_verus.lean +++ b/StrataBoole/StrataBooleTest/find_max_verus.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -93,8 +93,9 @@ spec { }; #end -/-- info: -Obligation: witnessOccurs_ensures_2_1229 +/-- +info: +Obligation: witnessOccurs_ensures_2_1234 Property: assert Result: ✅ pass @@ -122,28 +123,29 @@ Obligation: arbitrary_iter_maintain_invariant_0_2 Property: assert Result: ✅ pass -Obligation: assert_7_1950 +Obligation: assert_7_1955 Property: assert Result: ✅ pass -Obligation: callElimAssert_witnessOccurs_requires_0_1166_4 +Obligation: callElimAssert_witnessOccurs_requires_0_1171_4 Property: assert Result: ✅ pass -Obligation: callElimAssert_witnessOccurs_requires_1_1198_5 +Obligation: callElimAssert_witnessOccurs_requires_1_1203_5 Property: assert Result: ✅ pass -Obligation: findMax_ensures_5_1448 +Obligation: findMax_ensures_5_1453 Property: assert Result: ✅ pass -Obligation: findMax_ensures_6_1508 +Obligation: findMax_ensures_6_1513 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" findMax (options := .quiet) -example : Strata.smtVCsCorrect findMax := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole findMax := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/format_program.lean b/StrataBoole/StrataBooleTest/format_program.lean similarity index 97% rename from StrataTest/Languages/Boole/format_program.lean rename to StrataBoole/StrataBooleTest/format_program.lean index 88e4602842..d5795f41b3 100644 --- a/StrataTest/Languages/Boole/format_program.lean +++ b/StrataBoole/StrataBooleTest/format_program.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.Languages.Boole.Verify +import StrataBoole.Verify import Strata.DDM.Elab /-! diff --git a/StrataTest/Languages/Boole/function_definitions.lean b/StrataBoole/StrataBooleTest/function_definitions.lean similarity index 74% rename from StrataTest/Languages/Boole/function_definitions.lean rename to StrataBoole/StrataBooleTest/function_definitions.lean index f9ecc4d9fb..2ae6568afc 100644 --- a/StrataTest/Languages/Boole/function_definitions.lean +++ b/StrataBoole/StrataBooleTest/function_definitions.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -31,12 +31,15 @@ spec { #end -/-- info: Obligation: test_ensures_0_318 +/-- +info: +Obligation: test_ensures_0_323 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" function_definitions (options := .quiet) -example : Strata.smtVCsCorrect function_definitions := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole function_definitions := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/global_readonly_call.lean b/StrataBoole/StrataBooleTest/global_readonly_call.lean similarity index 87% rename from StrataTest/Languages/Boole/global_readonly_call.lean rename to StrataBoole/StrataBooleTest/global_readonly_call.lean index a0445f8753..5e60a48d37 100644 --- a/StrataTest/Languages/Boole/global_readonly_call.lean +++ b/StrataBoole/StrataBooleTest/global_readonly_call.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier /-! Test that read-only globals are correctly threaded through procedure headers @@ -141,41 +141,41 @@ spec { VCs: -Label: inc_ensures_1_2418 +Label: inc_ensures_1_2423 Property: assert Assumptions: -inc_requires_0_2400: z@1 > 0 +inc_requires_0_2405: z@1 > 0 Obligation: true -Label: callElimAssert_inc_requires_0_2400_6 +Label: callElimAssert_inc_requires_0_2405_6 Property: assert Assumptions: -main_caller_requires_2_2534: z@3 == 10 -main_caller_requires_3_2554: g@3 == 0 +main_caller_requires_2_2539: z@3 == 10 +main_caller_requires_3_2559: g@3 == 0 Obligation: z@3 > 0 -Label: main_caller_ensures_4_2573 +Label: main_caller_ensures_4_2578 Property: assert Assumptions: -main_caller_requires_2_2534: z@3 == 10 -main_caller_requires_3_2554: g@3 == 0 -callElimAssume_inc_ensures_1_2418_7: g@5 == g@3 + 5 + z@5 +main_caller_requires_2_2539: z@3 == 10 +main_caller_requires_3_2559: g@3 == 0 +callElimAssume_inc_ensures_1_2423_7: g@5 == g@3 + 5 + z@5 Obligation: g@5 == 15 --- info: -Obligation: inc_ensures_1_2418 +Obligation: inc_ensures_1_2423 Property: assert Result: ✅ pass -Obligation: callElimAssert_inc_requires_0_2400_6 +Obligation: callElimAssert_inc_requires_0_2405_6 Property: assert Result: ✅ pass -Obligation: main_caller_ensures_4_2573 +Obligation: main_caller_ensures_4_2578 Property: assert Result: ❓ unknown Model: diff --git a/StrataTest/Languages/Boole/grammar_extensions.lean b/StrataBoole/StrataBooleTest/grammar_extensions.lean similarity index 92% rename from StrataTest/Languages/Boole/grammar_extensions.lean rename to StrataBoole/StrataBooleTest/grammar_extensions.lean index 5d8f3337e4..200360ea77 100644 --- a/StrataTest/Languages/Boole/grammar_extensions.lean +++ b/StrataBoole/StrataBooleTest/grammar_extensions.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -90,6 +90,6 @@ procedure test_arrays () returns () #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" grammarExtensions -example : Strata.smtVCsCorrect grammarExtensions := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole grammarExtensions := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/insertion_sort.lean b/StrataBoole/StrataBooleTest/insertion_sort.lean similarity index 90% rename from StrataTest/Languages/Boole/insertion_sort.lean rename to StrataBoole/StrataBooleTest/insertion_sort.lean index 9c734c2082..b5f5605fff 100644 --- a/StrataTest/Languages/Boole/insertion_sort.lean +++ b/StrataBoole/StrataBooleTest/insertion_sort.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -53,6 +53,6 @@ spec #guard_msgs (drop info) in #eval Strata.Boole.verify "cvc5" insertionSortPgm -example : Strata.smtVCsCorrect insertionSortPgm := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole insertionSortPgm := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/loop_simple.lean b/StrataBoole/StrataBooleTest/loop_simple.lean similarity index 87% rename from StrataTest/Languages/Boole/loop_simple.lean rename to StrataBoole/StrataBooleTest/loop_simple.lean index 0a07e49930..f116cc1709 100644 --- a/StrataTest/Languages/Boole/loop_simple.lean +++ b/StrataBoole/StrataBooleTest/loop_simple.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -53,6 +53,6 @@ Result: ✅ pass-/ open Strata.SMT -theorem loop_simple_smt_vcs_correct : smtVCsCorrect loop_simple_program := by - gen_smt_vcs +theorem loop_simple_smt_vcs_correct : smtVCsCorrectBoole loop_simple_program := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/procedure_signatures.lean b/StrataBoole/StrataBooleTest/procedure_signatures.lean similarity index 99% rename from StrataTest/Languages/Boole/procedure_signatures.lean rename to StrataBoole/StrataBooleTest/procedure_signatures.lean index 744111a23c..a0ecaf635e 100644 --- a/StrataTest/Languages/Boole/procedure_signatures.lean +++ b/StrataBoole/StrataBooleTest/procedure_signatures.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier /-! Test accepted and rejected procedure signature forms in Boole. diff --git a/StrataTest/Languages/Boole/square_matrix_multiply.lean b/StrataBoole/StrataBooleTest/square_matrix_multiply.lean similarity index 94% rename from StrataTest/Languages/Boole/square_matrix_multiply.lean rename to StrataBoole/StrataBooleTest/square_matrix_multiply.lean index fd07b73fee..2564c7eacc 100644 --- a/StrataTest/Languages/Boole/square_matrix_multiply.lean +++ b/StrataBoole/StrataBooleTest/square_matrix_multiply.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier namespace Strata @@ -103,6 +103,6 @@ Result: ✅ pass -/ #guard_msgs in #eval Strata.Boole.verify "cvc5" squareMatrixMult (options := .quiet) -example : Strata.smtVCsCorrect squareMatrixMult := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole squareMatrixMult := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/stack_array_based.lean b/StrataBoole/StrataBooleTest/stack_array_based.lean similarity index 82% rename from StrataTest/Languages/Boole/stack_array_based.lean rename to StrataBoole/StrataBooleTest/stack_array_based.lean index 9af09256a0..bcd6fbeecc 100644 --- a/StrataTest/Languages/Boole/stack_array_based.lean +++ b/StrataBoole/StrataBooleTest/stack_array_based.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier ------------------------------------------------------------ namespace Strata @@ -169,21 +169,21 @@ spec { VCs: -Label: StackInit_ensures_1_1066 +Label: StackInit_ensures_1_1071 Property: assert Assumptions: -StackInit_requires_0_1015: cap@1 >= 0 +StackInit_requires_0_1020: cap@1 >= 0 Obligation: true -Label: StackInit_ensures_2_1086 +Label: StackInit_ensures_2_1091 Property: assert Assumptions: -StackInit_requires_0_1015: cap@1 >= 0 +StackInit_requires_0_1020: cap@1 >= 0 Obligation: true -Label: StackEmpty_ensures_3_1205 +Label: StackEmpty_ensures_3_1210 Property: assert Assumptions: : if top@3 == 0 then top@3 == 0 else true @@ -191,7 +191,7 @@ Assumptions: Obligation: if top@3 == 0 then true else false ==> top@3 == 0 -Label: StackEmpty_ensures_4_1233 +Label: StackEmpty_ensures_4_1238 Property: assert Assumptions: : if top@3 == 0 then top@3 == 0 else true @@ -199,82 +199,82 @@ Assumptions: Obligation: top@3 == 0 ==> if top@3 == 0 then true else false -Label: Push_ensures_6_1494 +Label: Push_ensures_6_1499 Property: assert Assumptions: -Push_requires_5_1443: top@4 < n@4 +Push_requires_5_1448: top@4 < n@4 Obligation: true -Label: Push_ensures_7_1525 +Label: Push_ensures_7_1530 Property: assert Assumptions: -Push_requires_5_1443: top@4 < n@4 +Push_requires_5_1448: top@4 < n@4 Obligation: (S@3[top@4 + 1:=x@1])[top@4 + 1] == x@1 -Label: Push_ensures_8_1583 +Label: Push_ensures_8_1588 Property: assert Assumptions: -Push_requires_5_1443: top@4 < n@4 +Push_requires_5_1448: top@4 < n@4 Obligation: forall __q0 : int :: 1 <= __q0 && __q0 <= top@4 ==> (S@3[top@4 + 1:=x@1])[__q0] == S@3[__q0] -Label: Pop_ensures_10_1840 +Label: Pop_ensures_10_1845 Property: assert Assumptions: -Pop_requires_9_1803: top@6 > 0 +Pop_requires_9_1808: top@6 > 0 Obligation: true -Label: Pop_ensures_11_1871 +Label: Pop_ensures_11_1876 Property: assert Assumptions: -Pop_requires_9_1803: top@6 > 0 +Pop_requires_9_1808: top@6 > 0 Obligation: true --- info: -Obligation: StackInit_ensures_1_1066 +Obligation: StackInit_ensures_1_1071 Property: assert Result: ✅ pass -Obligation: StackInit_ensures_2_1086 +Obligation: StackInit_ensures_2_1091 Property: assert Result: ✅ pass -Obligation: StackEmpty_ensures_3_1205 +Obligation: StackEmpty_ensures_3_1210 Property: assert Result: ✅ pass -Obligation: StackEmpty_ensures_4_1233 +Obligation: StackEmpty_ensures_4_1238 Property: assert Result: ✅ pass -Obligation: Push_ensures_6_1494 +Obligation: Push_ensures_6_1499 Property: assert Result: ✅ pass -Obligation: Push_ensures_7_1525 +Obligation: Push_ensures_7_1530 Property: assert Result: ✅ pass -Obligation: Push_ensures_8_1583 +Obligation: Push_ensures_8_1588 Property: assert Result: ✅ pass -Obligation: Pop_ensures_10_1840 +Obligation: Pop_ensures_10_1845 Property: assert Result: ✅ pass -Obligation: Pop_ensures_11_1871 +Obligation: Pop_ensures_11_1876 Property: assert Result: ✅ pass -/ #guard_msgs in #eval Strata.Boole.verify "cvc5" stackArrayPgm -example : Strata.smtVCsCorrect stackArrayPgm := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole stackArrayPgm := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/string_operators.lean b/StrataBoole/StrataBooleTest/string_operators.lean similarity index 89% rename from StrataTest/Languages/Boole/string_operators.lean rename to StrataBoole/StrataBooleTest/string_operators.lean index 441ca693b4..30bf034d08 100644 --- a/StrataTest/Languages/Boole/string_operators.lean +++ b/StrataBoole/StrataBooleTest/string_operators.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier namespace Strata @@ -118,49 +118,51 @@ procedure main() returns () { #end - /-- info: -Obligation: assert_19_3035 + /-- +info: +Obligation: assert_19_3040 Property: assert Result: ✅ pass -Obligation: assert_20_3077 +Obligation: assert_20_3082 Property: assert Result: ✅ pass -Obligation: assert_21_3125 +Obligation: assert_21_3130 Property: assert Result: ✅ pass -Obligation: assert_22_3159 +Obligation: assert_22_3164 Property: assert Result: ✅ pass -Obligation: assert_23_3206 +Obligation: assert_23_3211 Property: assert Result: ✅ pass -Obligation: assert_24_3242 +Obligation: assert_24_3247 Property: assert Result: ✅ pass -Obligation: assert_25_3272 +Obligation: assert_25_3277 Property: assert Result: ✅ pass -Obligation: assert_26_3302 +Obligation: assert_26_3307 Property: assert Result: ✅ pass -Obligation: assert_27_3332 +Obligation: assert_27_3337 Property: assert Result: ✅ pass -Obligation: assert_28_3386 +Obligation: assert_28_3391 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" basicOp (options := .quiet) -theorem basicOp_smt_vcs_correct : Strata.smtVCsCorrect basicOp := by - gen_smt_vcs +theorem basicOp_smt_vcs_correct : Strata.smtVCsCorrectBoole basicOp := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/top_level_block_selection.lean b/StrataBoole/StrataBooleTest/top_level_block_selection.lean similarity index 83% rename from StrataTest/Languages/Boole/top_level_block_selection.lean rename to StrataBoole/StrataBooleTest/top_level_block_selection.lean index 7f7aab3cc8..9d14b29b2c 100644 --- a/StrataTest/Languages/Boole/top_level_block_selection.lean +++ b/StrataBoole/StrataBooleTest/top_level_block_selection.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -36,6 +36,6 @@ Result: ✅ pass (proceduresToVerify := (some [Strata.Boole.topLevelBlockProcedureName])) (options := .quiet) -example : Strata.smtVCsCorrect topLevelBlockSelection := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole topLevelBlockSelection := by + gen_smt_vcs_boole all_goals (try grind) diff --git a/StrataTest/Languages/Boole/verification_coverage.lean b/StrataBoole/StrataBooleTest/verification_coverage.lean similarity index 86% rename from StrataTest/Languages/Boole/verification_coverage.lean rename to StrataBoole/StrataBooleTest/verification_coverage.lean index 885d9e287b..f65c06197e 100644 --- a/StrataTest/Languages/Boole/verification_coverage.lean +++ b/StrataBoole/StrataBooleTest/verification_coverage.lean @@ -4,7 +4,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ -import Strata.MetaVerifier +import StrataBoole.MetaVerifier open Strata @@ -161,12 +161,13 @@ spec #end -/-- info: -Obligation: assert_2_406 +/-- +info: +Obligation: assert_2_411 Property: assert Result: ✅ pass -Obligation: assert_3_509 +Obligation: assert_3_514 Property: assert Result: ✅ pass @@ -194,68 +195,69 @@ Obligation: arbitrary_iter_maintain_invariant_0_2 Property: assert Result: ✅ pass -Obligation: sum_ensures_5_652 +Obligation: sum_ensures_5_657 Property: assert Result: ✅ pass -Obligation: assert_10_1185 +Obligation: assert_10_1190 Property: assert Result: ✅ pass -Obligation: assert_12_1419 +Obligation: assert_12_1424 Property: assert Result: ✅ pass -Obligation: assert_16_1684 +Obligation: assert_16_1689 Property: assert Result: ✅ pass -Obligation: assert_18_1820 +Obligation: assert_18_1825 Property: assert Result: ✅ pass -Obligation: testEnsuresCallee_ensures_20_1983 +Obligation: testEnsuresCallee_ensures_20_1988 Property: assert Result: ✅ pass -Obligation: testEnsuresCallee_ensures_21_2025 +Obligation: testEnsuresCallee_ensures_21_2030 Property: assert Result: ✅ pass -Obligation: callElimAssert_testEnsuresCallee_requires_19_1941_7 +Obligation: callElimAssert_testEnsuresCallee_requires_19_1946_7 Property: assert Result: ✅ pass -Obligation: callElimAssert_testEnsuresCallee_requires_19_1941_2 +Obligation: callElimAssert_testEnsuresCallee_requires_19_1946_2 Property: assert Result: ✅ pass -Obligation: assert_24_2458 +Obligation: assert_24_2463 Property: assert Result: ✅ pass -Obligation: testEnsuresCaller_ensures_23_2219 +Obligation: testEnsuresCaller_ensures_23_2224 Property: assert Result: ✅ pass -Obligation: obviouslyUnconstrainedCode_ensures_27_2723 +Obligation: obviouslyUnconstrainedCode_ensures_27_2728 Property: assert Result: ✅ pass -Obligation: contradictoryEnsuresClause_ensures_29_3049 +Obligation: contradictoryEnsuresClause_ensures_29_3054 Property: assert Result: ✅ pass -Obligation: callElimAssert_contradictoryEnsuresClause_requires_28_2979_12 +Obligation: callElimAssert_contradictoryEnsuresClause_requires_28_2984_12 Property: assert Result: ✅ pass -Obligation: usesSomeInteger_ensures_32_3711 +Obligation: usesSomeInteger_ensures_32_3716 Property: assert -Result: ✅ pass-/ +Result: ✅ pass +-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" verification_coverage (options := .quiet) -example : Strata.smtVCsCorrect verification_coverage := by - gen_smt_vcs +example : Strata.smtVCsCorrectBoole verification_coverage := by + gen_smt_vcs_boole all_goals grind diff --git a/StrataBoole/lake-manifest.json b/StrataBoole/lake-manifest.json new file mode 100644 index 0000000000..ece503ad20 --- /dev/null +++ b/StrataBoole/lake-manifest.json @@ -0,0 +1,22 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "Strata", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "..", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4bdad1f417437e3331492708ce8320aec350280a", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "bump_to_v4.29.0-rc8", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "StrataBoole", + "lakeDir": ".lake"} diff --git a/StrataBoole/lakefile.toml b/StrataBoole/lakefile.toml new file mode 100644 index 0000000000..8c41aee1a9 --- /dev/null +++ b/StrataBoole/lakefile.toml @@ -0,0 +1,13 @@ +name = "StrataBoole" +version = "0.1.0" +defaultTargets = ["StrataBoole"] + +[[require]] +name = "Strata" +path = ".." + +[[lean_lib]] +name = "StrataBoole" + +[[lean_lib]] +name = "StrataBooleTest" diff --git a/StrataBoole/lean-toolchain b/StrataBoole/lean-toolchain new file mode 100644 index 0000000000..33e0c08893 --- /dev/null +++ b/StrataBoole/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.29.1 diff --git a/StrataMainLib.lean b/StrataMainLib.lean index 9f345497cd..23ef0bf597 100644 --- a/StrataMainLib.lean +++ b/StrataMainLib.lean @@ -18,8 +18,6 @@ import Strata.Languages.B3.Verifier.Program import Strata.Languages.Laurel.LaurelCompilationPipeline import Strata.Pipeline.Diagnostic import Strata.Pipeline.PyAnalyzeLaurel -import Strata.Languages.Boole.Boole -import Strata.Languages.Boole.Verify import Strata.Languages.C_Simp.DDMTransform.Parse import Strata.Languages.Python.Python import Strata.Languages.Python.Specs.IdentifyOverloads @@ -138,7 +136,6 @@ def buildDialectFileMap (pflags : ParsedFlags) : IO Strata.DialectFileMap := do |>.addDialect! Strata.Python.Python |>.addDialect! Strata.Python.Specs.DDM.PythonSpecs |>.addDialect! Strata.Core - |>.addDialect! Strata.Boole |>.addDialect! Strata.Laurel.Laurel |>.addDialect! Strata.smtReservedKeywordsDialect |>.addDialect! Strata.SMTCore @@ -318,7 +315,6 @@ private def readStrataProgram (file : String) let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file) let dctx := Elab.LoadedDialects.builtin let dctx := dctx.addDialect! Core - let dctx := dctx.addDialect! Boole let dctx := dctx.addDialect! C_Simp let dctx := dctx.addDialect! B3CST let leanEnv ← Lean.mkEmptyEnvironment 0 @@ -1296,8 +1292,6 @@ def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Com if opts.typeCheckOnly then let ans := if file.endsWith ".csimp.st" then C_Simp.typeCheck pgm opts - else if pgm.dialect == "Boole" then - Boole.typeCheck pgm opts else typeCheck inputCtx pgm opts match ans with @@ -1331,7 +1325,7 @@ def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Com IO.println s!" {marker} {desc}" pure #[] else if pgm.dialect == "Boole" then - Boole.verify opts.solver pgm inputCtx proceduresToVerify opts + throw <| IO.Error.userError "Boole dialect support requires the StrataBoole package" else verify pgm inputCtx proceduresToVerify opts (mkDischarge := mkDischarge) catch e => From 484a028d40a8732703f9b506e7d7dada44ebed88 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 21 May 2026 15:18:07 -0700 Subject: [PATCH 2/3] fix(ci): Add copyright headers and inline StrataBoole build step Add missing copyright headers to StrataBoole.lean and StrataBooleTest.lean to fix the lint check. Move the StrataBoole build into the main build_and_test_lean job instead of a separate job. --- .github/workflows/ci.yml | 24 +++--------------------- StrataBoole/StrataBoole.lean | 5 +++++ StrataBoole/StrataBooleTest.lean | 5 +++++ 3 files changed, 13 insertions(+), 21 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b36f670d23..b4b3879a73 100644 --- a/.github/workflows/ci.yml +++ b/.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 @@ -97,27 +100,6 @@ jobs: working-directory: StrataTest/Languages/Python/Regex run: python diff_test.py - build_strata_boole: - needs: build_and_test_lean - name: Build StrataBoole - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v6 - - name: Restore lake cache - uses: ./.github/actions/restore-lake-cache - with: - fail-on-cache-miss: "true" - use-restore-keys: "false" - - name: Install Lean - uses: leanprover/lean-action@v1 - with: - auto-config: false - build: false - - name: Build StrataBoole - run: lake build StrataBoole StrataBooleTest - working-directory: StrataBoole - check_pending_python: needs: build_and_test_lean name: Check pending Python tests diff --git a/StrataBoole/StrataBoole.lean b/StrataBoole/StrataBoole.lean index 9d21ce8979..be705c09df 100644 --- a/StrataBoole/StrataBoole.lean +++ b/StrataBoole/StrataBoole.lean @@ -1,3 +1,8 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ import StrataBoole.Boole import StrataBoole.Grammar import StrataBoole.MetaVerifier diff --git a/StrataBoole/StrataBooleTest.lean b/StrataBoole/StrataBooleTest.lean index 728d78bd51..06eefaa8af 100644 --- a/StrataBoole/StrataBooleTest.lean +++ b/StrataBoole/StrataBooleTest.lean @@ -1,3 +1,8 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ import StrataBooleTest.array_2d import StrataBooleTest.array_assignment import StrataBooleTest.bit_vectors From dd8d096bac09040ff5042985011f9da842664cfe Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 21 May 2026 15:43:15 -0700 Subject: [PATCH 3/3] Add some comments explaining Boole removals --- Strata/MetaVerifier.lean | 3 +++ StrataMainLib.lean | 2 ++ 2 files changed, 5 insertions(+) diff --git a/Strata/MetaVerifier.lean b/Strata/MetaVerifier.lean index 1d61bb1570..9e5002df34 100644 --- a/Strata/MetaVerifier.lean +++ b/Strata/MetaVerifier.lean @@ -101,6 +101,9 @@ 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 diff --git a/StrataMainLib.lean b/StrataMainLib.lean index 23ef0bf597..e836df93d0 100644 --- a/StrataMainLib.lean +++ b/StrataMainLib.lean @@ -1325,6 +1325,8 @@ def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Com IO.println s!" {marker} {desc}" pure #[] else if pgm.dialect == "Boole" then + -- TODO: this will be restored once StrataMainLib is in a separate + -- package that can depend on the StrataBoole package. throw <| IO.Error.userError "Boole dialect support requires the StrataBoole package" else verify pgm inputCtx proceduresToVerify opts (mkDischarge := mkDischarge)