feat(Boole): add verified algorithm examples#369
feat(Boole): add verified algorithm examples#369Robertboy18 wants to merge 2 commits intoleanprover:Boole-sandboxfrom
Conversation
Adds new verified Boole examples: selection sort, insertion sort, linear search, prefix sums, Euclid GCD, and two-sum. Also updates the Strata pin in lake-manifest.json because the previously pinned commit is no longer available upstream.
There was a problem hiding this comment.
Pull request overview
This PR adds verified algorithm examples to the Boole language examples directory, demonstrating program verification using the Strata/Boole framework. The PR promotes insertion sort from feature requests to examples after fixing verification issues, and adds five new verified examples (selection sort, linear search, prefix sums, Euclid's GCD, and two-sum).
Changes:
- Updated Strata dependency to a commit that is available upstream
- Promoted and fixed insertion sort implementation with strengthened invariants
- Added five new verified algorithm examples with Lean-based proofs
Reviewed changes
Copilot reviewed 8 out of 8 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| lake-manifest.json | Updates Strata revision to available upstream commit |
| feature_requests/quantifier_syntax/insertion_sort.lean | Removed buggy version that had incorrect VCs |
| examples/insertion_sort.lean | Added corrected and verified insertion sort with stronger invariants |
| examples/selection_sort.lean | Added verified selection sort with adjacent-order sortedness spec |
| examples/linear_search.lean | Added verified linear search with completeness and soundness properties |
| examples/prefix_sums.lean | Added verified prefix sums using uninterpreted function with axioms |
| examples/euclid_gcd.lean | Added verified Euclid's GCD using free ensures helper pattern |
| examples/two_sum.lean | Added verified two-sum with soundness-only specification |
| set_option maxHeartbeats 1000000 in | ||
| example : Strata.smtVCsCorrect insertionSortPgm := by | ||
| gen_smt_vcs | ||
| all_goals grind |
There was a problem hiding this comment.
Missing end Strata at the end of the file. All other example files in the directory end with end Strata to close the namespace.
| all_goals grind | |
| all_goals grind | |
| end Strata |
| @@ -0,0 +1,102 @@ | |||
| import Strata.MetaVerifier | |||
|
|
|||
| --------------------------------------------------------------------- | |||
There was a problem hiding this comment.
The separator line has 69 dashes, but the convention in other example files is to use 60 dashes (as seen in find_max.lean, stack_array_based.lean, and all other new examples in this PR).
| --------------------------------------------------------------------- | |
| ------------------------------------------------------------ |
|
Follow-up: I pushed commit 5693c20 to address Copilot’s notes in
|
Summary
Excited to be contributing to CsLib! I think there is a lot we can do: )! So here is what I did
feature_requests/intoexamples/after strengthening invariants/spec.lake-manifest.jsonStrata pin (the previously pinned Strata commit is no longer available upstream, which breakslake update).Files
Cslib/Languages/Boole/examples/insertion_sort.leanCslib/Languages/Boole/examples/selection_sort.leanCslib/Languages/Boole/examples/linear_search.leanCslib/Languages/Boole/examples/prefix_sums.leanCslib/Languages/Boole/examples/euclid_gcd.lean(uses afree ensureshelperGCDProperties)Cslib/Languages/Boole/examples/two_sum.lean(soundness-only spec)Cslib/Languages/Boole/feature_requests/quantifier_syntax/insertion_sort.leanAll new/updated examples include a Lean-based proof like other examples?!
example : Strata.smtVCsCorrect ... := by gen_smt_vcs; all_goals grind