Add Strata example Eh I'll hold back on updating the Lean version for now

Changes

3 changed files (+84/-17)

• Strata.lean (new)
  • @@ -0,0 +1,53 @@
    + -- https://github.com/strata-org/Strata/blob/main/StrataTest/Languages/Boole/insertion_sort.lean + import Strata.MetaVerifier + + open Strata + + private def insertionSortPgm := + #strata + program Boole; + + type Array := Map int int; + + var A : Array; + var n : int; + + procedure InsertionSort() returns () + spec + { + modifies A; + requires 0 <= n; + requires n <= 1; + ensures ∀ i:int, j:int . 0 <= i && i <= j && j < n ==> A[i] <= A[j]; + } + { + var j : int; + var key : int; + + // for-loop syntax + array assignment syntax + quantifier syntax + for i : int := 1 to (n - 1) by 1 + invariant 1 <= i && i <= n + 1 + invariant ∀ p:int, q:int . 0 <= p && p <= q && q < i ==> A[p] <= A[q] + { + key := A[i]; + j := i - 1; + + while (j >= 0 && A[j] > key) + invariant (-1 <= j && j < i) + invariant (∀ p:int, q:int . 0 <= p && p <= q && q < i ==> A[p] <= A[q]) + { + A[j + 1] := A[j]; + j := j - 1; + } + + A[j + 1] := key; + } + }; + #end + + #guard_msgs (drop info) in + #eval Strata.Boole.verify "cvc5" insertionSortPgm + + example : Strata.smtVCsCorrect insertionSortPgm := by + gen_smt_vcs + all_goals (try grind)
• lake-manifest.json
  • @@ -1,11 +1,21 @@
    {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/bergmannjg/leanCurl", + [{"url": "https://github.com/strata-org/Strata", + "type": "git", + "subDir": null, + "scope": "strata-org", + "rev": "6ac407384ccc39b18eb91fa197b12c1a860e9be6", + "name": "Strata", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/bergmannjg/leanCurl", "type": "git", "subDir": null, "scope": "bergmannjg", - "rev": "5ef9a480e51eaa082784a73c1aa574584d09990f", + "rev": "d725fede14f67acc746c18eaec962f6461dee5cb", "name": "Curl", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -15,27 +25,27 @@ {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "32d24245c7a12ded17325299fd41d412022cd3fe", + "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/plausible.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a", + "scope": "", + "rev": "a0098f9ff17f6f003a238903a42ebdd81e08b7fb", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "bump_to_v4.27.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "19e5f5cc9c21199be466ef99489e3acab370f079", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -45,7 +55,7 @@ {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -55,17 +65,17 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.84", + "inputRev": "v0.0.87", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fb12f5535c80e40119286d9575c9393562252d21", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -75,7 +85,7 @@ {"url": "https://github.com/leanprover-community/quote4",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -85,7 +95,7 @@ {"url": "https://github.com/leanprover-community/batteries",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -95,10 +105,10 @@ {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", + "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "evolution",
• lakefile.toml
  • @@ -15,3 +15,7 @@
    [[require]] name = "Curl" scope = "bergmannjg" + + [[require]] + name = "Strata" + scope = "strata-org"