chore: Update Lean to v4.34.1

Benchmarks/Catalog/RelocFixtureA/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.1

Benchmarks/Catalog/RelocFixtureB/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.1

Benchmarks/Compile/TruthMines/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.1

Benchmarks/Compile/lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.1",
+   "inputRev": "v4.34.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/TauCetiProject/TauCeti",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "45eb9afc55ce36516fc98ba10618c010fdced7dc",
+   "rev": "43420557744f04b5b62d74ac5c7b63eccf2cb7cd",
    "name": "flt",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"type": "path",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,7 +92,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -102,7 +102,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "e928b72544873815af278d38681b31c0293588e3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -112,7 +112,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -122,7 +122,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -132,7 +132,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -142,7 +142,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -172,40 +172,40 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
+   "rev": "a5621ecfe6416360d4e310c0ed40f3e79ae0710e",
    "name": "lean4lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
+   "inputRev": "a5621ecfe6416360d4e310c0ed40f3e79ae0710e",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/argumentcomputer/Blake3.lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
+   "rev": "3f8b805614a0bae1c033469ff893a8f0ee85f601",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
+   "inputRev": "3f8b805614a0bae1c033469ff893a8f0ee85f601",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e780f4188c9649aef988270f4d126651460ca9c4",
+   "rev": "d8eb3e0d9a8e33fc116e6700df0418a1d8114508",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e780f4188c9649aef988270f4d126651460ca9c4",
+   "inputRev": "d8eb3e0d9a8e33fc116e6700df0418a1d8114508",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/leansqlite",

Benchmarks/Compile/lakefile.toml

@@ -42,7 +42,7 @@ path = "../.."
 [[require]]
 name = "flt"
 git = "https://github.com/ImperialCollegeLondon/FLT"
-rev = "v4.33.0"
+rev = "v4.34.0"
 
 [[require]]
 name = "flt_e2e"
@@ -74,4 +74,4 @@ rev = "afb1aacb3632d3236eee756ea1683290c07270a3"
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.33.1"
+rev = "v4.34.1"

Benchmarks/Compile/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.1

Benchmarks/TruthMines/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.1

Ix/Compile/Verify/Audit/Statements.lean

@@ -83,8 +83,12 @@ def roots : Array RootAllowance := #[
   { root := ``Ix.Compile.Verify.ExprTableWF.mono },
   { root := ``Ix.Compile.Verify.Catalog.empty_wf,
     standardAxioms := standard, nativeAxioms := blake3Native },
+  -- `Std.HashMap`'s well-formedness proof reaches core's `Nat.le_iff_lt_add_one`
+  -- and `Nat.pow_lt_pow_iff_right`, which are classical as of Lean v4.34, so
+  -- any statement over `Ixon.Env` (hash-map fields) now carries
+  -- `Classical.choice` regardless of its own proof.
   { root := ``Ix.Compile.Verify.Catalog.ofEnv_finite,
-    standardAxioms := noChoice },
+    standardAxioms := standard },
   { root := ``Ix.Compile.Verify.BlockState.internRef_wf,
     standardAxioms := standard },
   { root := ``Ix.Compile.Verify.BlockState.internUniv_wf,
@@ -141,8 +145,10 @@ def roots : Array RootAllowance := #[
   { root :=
       ``Ix.Compile.Verify.PreseedCollectionCovers.compileExprRef_of_indexed,
     standardAxioms := standard, nativeAxioms := blake3Native },
+  -- Over hash-map state: carries `Classical.choice` for the reason given at
+  -- `Catalog.ofEnv_finite` above.
   { root := ``Ix.Compile.Verify.BlockWireTablesWF.of_preseed,
-    standardAxioms := noChoice },
+    standardAxioms := standard },
   { root := ``Ix.Compile.Verify.preseedExprTables_singleton_run_ready,
     standardAxioms := standard, nativeAxioms := blake3Native },
   { root := ``Ix.Compile.Verify.preseedExprTables_singleton_run_ready_wireWF,
@@ -477,7 +483,7 @@ def roots : Array RootAllowance := #[
   -- Compiled component search (`@[csimp]`): the loop of `searchComponents`
   -- runs the area- and closure-local search.
   { root := ``Ix.Sharing.Exact.searchComponents_eq_via,
-    standardAxioms := noChoice },
+    standardAxioms := standard },
   { root := ``Ix.Sharing.Exact.searchComponentsWith_eq_fast,
     standardAxioms := standard },
   { root := ``Ix.Compile.Verify.Tiered.canonicalTieredCore_select,
@@ -586,7 +592,7 @@ def roots : Array RootAllowance := #[
   { root := ``Ix.Sharing.Exact.propagateCounts_eq_fast,
     standardAxioms := noChoice },
   { root := ``Ix.Sharing.Exact.SCtx.phiE_eq_fast,
-    standardAxioms := noChoice },
+    standardAxioms := standard },
   { root := ``Ix.Sharing.Exact.csBase_eq_fast,
     standardAxioms := noChoice }
 ]

Ix/Compile/Verify/Codec.lean

@@ -63,7 +63,7 @@ theorem Reads.checkCount {getm : Ixon.GetM α} {bytes : ByteArray} {value : α}
     unfold Ixon.checkCount
     change (EStateM.bind EStateM.get _) _ = _
     simp only [EStateM.bind, EStateM.get]
-    rw [if_neg hremaining]
+    rw [ite_eq_right hremaining]
     rfl
   change (EStateM.bind (Ixon.checkCount count minBytes) _) _ = _
   rw [EStateM.bind, hcheck]
@@ -102,7 +102,7 @@ theorem getU8_reads (byte : UInt8) :
     bytes := before ++ [byte].toByteArray ++ after
   } : Ixon.GetState) = _
   simp only [EStateM.bind, EStateM.get]
-  rw [if_pos (by
+  rw [ite_eq_left (by
     simp only [ByteArray.size_append, List.size_toByteArray, List.length_cons,
       List.length_nil]
     omega)]
@@ -372,79 +372,79 @@ theorem getTagN_reads (f : Nat) (hf : f = 0 ∨ f = 2 ∨ f = 4) (flag : UInt8)
   unfold tagNBytes Ixon.getTagN
   simp only
   by_cases h1 : value.toNat < Ixon.tagNEnd1 f
-  · rw [if_pos h1, ← ByteArray.append_empty (b := [_].toByteArray)]
+  · rw [ite_eq_left h1, ← ByteArray.append_empty (b := [_].toByteArray)]
     refine Reads.bind (getU8_reads _) ?_
     obtain ⟨hdiv, hmod⟩ := tagNHeader_fields f hf flag hflag value.toNat (by omega)
     simp only [hdiv, hmod]
-    rw [if_pos (by omega)]
+    rw [ite_eq_left (by omega)]
     exact Reads.pure_of_eq (tagN_mk_eq rfl rfl)
   by_cases h2 : value.toNat < Ixon.tagNEnd2 f
-  · rw [if_neg h1, if_pos h2]
+  · rw [ite_eq_right h1, ite_eq_left h2]
     refine Reads.bind (getU8_reads _) ?_
     obtain ⟨hdiv, hmod⟩ := tagNHeader_fields f hf flag hflag
       (2 ^ (8 - f - 1) + (value.toNat - Ixon.tagNEnd1 f) / 256) (by omega)
     simp only [hdiv, hmod]
-    rw [if_neg (by omega), if_pos (by omega), ← ByteArray.append_empty (b := [_].toByteArray)]
+    rw [ite_eq_right (by omega), ite_eq_left (by omega), ← ByteArray.append_empty (b := [_].toByteArray)]
     refine Reads.bind (getU8_reads _) ?_
     exact Reads.pure_of_eq (tagN_mk_eq rfl (by simp; omega))
   by_cases h3 : value.toNat < Ixon.tagNEnd3 f
-  · rw [if_neg h1, if_neg h2, if_pos h3]
+  · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_left h3]
     refine Reads.bind (getU8_reads _) ?_
     obtain ⟨hdiv, hmod⟩ := tagNHeader_fields f hf flag hflag
       (2 ^ (8 - f - 1) + 2 ^ (8 - f - 2)) (by omega)
     simp only [hdiv, hmod]
-    rw [if_neg (by omega), if_neg (by omega)]
+    rw [ite_eq_right (by omega), ite_eq_right (by omega)]
     unfold Ixon.getTagNWide
-    rw [if_pos (by omega), ← ByteArray.append_empty (b := trimmedBytes _ _)]
+    rw [ite_eq_left (by omega), ← ByteArray.append_empty (b := trimmedBytes _ _)]
     have hx : ((value.toNat - Ixon.tagNEnd2 f).toUInt64).toNat =
         value.toNat - Ixon.tagNEnd2 f := by simp; omega
     refine Reads.bind (getU64TrimmedLEAux_reads _ 2
       (shiftBytes_eq_zero_of_lt _ _ (by rw [hx]; omega))) ?_
     exact Reads.pure_of_eq (tagN_mk_eq rfl (by rw [hx]; omega))
   by_cases h4 : value.toNat < Ixon.tagNEnd4 f
-  · rw [if_neg h1, if_neg h2, if_neg h3, if_pos h4]
+  · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_right h3, ite_eq_left h4]
     refine Reads.bind (getU8_reads _) ?_
     obtain ⟨hdiv, hmod⟩ := tagNHeader_fields f hf flag hflag
       (2 ^ (8 - f - 1) + 2 ^ (8 - f - 2) + 1) (by omega)
     simp only [hdiv, hmod]
-    rw [if_neg (by omega), if_neg (by omega)]
+    rw [ite_eq_right (by omega), ite_eq_right (by omega)]
     unfold Ixon.getTagNWide
-    rw [if_neg (by omega), if_pos (by omega),
+    rw [ite_eq_right (by omega), ite_eq_left (by omega),
       ← ByteArray.append_empty (b := trimmedBytes _ _)]
     have hx : ((value.toNat - Ixon.tagNEnd3 f).toUInt64).toNat =
         value.toNat - Ixon.tagNEnd3 f := by simp; omega
     refine Reads.bind (getU64TrimmedLEAux_reads _ 3
       (shiftBytes_eq_zero_of_lt _ _ (by rw [hx]; omega))) ?_
     exact Reads.pure_of_eq (tagN_mk_eq rfl (by rw [hx]; omega))
   by_cases h5 : value.toNat < Ixon.tagNEnd5 f
-  · rw [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_pos h5]
+  · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_right h3, ite_eq_right h4, ite_eq_left h5]
     refine Reads.bind (getU8_reads _) ?_
     obtain ⟨hdiv, hmod⟩ := tagNHeader_fields f hf flag hflag
       (2 ^ (8 - f - 1) + 2 ^ (8 - f - 2) + 2) (by omega)
     simp only [hdiv, hmod]
-    rw [if_neg (by omega), if_neg (by omega)]
+    rw [ite_eq_right (by omega), ite_eq_right (by omega)]
     unfold Ixon.getTagNWide
-    rw [if_neg (by omega), if_neg (by omega), if_pos (by omega),
+    rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_left (by omega),
       ← ByteArray.append_empty (b := trimmedBytes _ _)]
     have hx : ((value.toNat - Ixon.tagNEnd4 f).toUInt64).toNat =
         value.toNat - Ixon.tagNEnd4 f := by simp; omega
     refine Reads.bind (getU64TrimmedLEAux_reads _ 4
       (shiftBytes_eq_zero_of_lt _ _ (by rw [hx]; omega))) ?_
     exact Reads.pure_of_eq (tagN_mk_eq rfl (by rw [hx]; omega))
-  · rw [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5]
+  · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_right h3, ite_eq_right h4, ite_eq_right h5]
     refine Reads.bind (getU8_reads _) ?_
     obtain ⟨hdiv, hmod⟩ := tagNHeader_fields f hf flag hflag
       (2 ^ (8 - f - 1) + 2 ^ (8 - f - 2) + 3) (by omega)
     simp only [hdiv, hmod]
-    rw [if_neg (by omega), if_neg (by omega)]
+    rw [ite_eq_right (by omega), ite_eq_right (by omega)]
     unfold Ixon.getTagNWide
-    rw [if_neg (by omega), if_neg (by omega), if_neg (by omega), if_pos (by omega),
+    rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_left (by omega),
       ← ByteArray.append_empty (b := trimmedBytes _ _)]
     have hx : ((value.toNat - Ixon.tagNEnd5 f).toUInt64).toNat =
         value.toNat - Ixon.tagNEnd5 f := by simp; omega
     refine Reads.bind (getU64TrimmedLEAux_reads _ 8
       (shiftBytes_eq_zero_of_lt _ _ (by rw [hx]; omega))) ?_
-    rw [if_pos (by rw [hx]; omega)]
+    rw [ite_eq_left (by rw [hx]; omega)]
     exact Reads.pure_of_eq (tagN_mk_eq rfl (by rw [hx]; omega))
 
 /-- A read law gives the exact full-buffer decode. -/
@@ -513,7 +513,7 @@ theorem tag2Bytes_small (flag : UInt8) (size : UInt64)
   have hs : size.toNat < Ixon.tagNEnd1 2 := by
     simpa [UInt64.lt_iff_toNat_lt, show Ixon.tagNEnd1 2 = 32 by decide] using hsize
   unfold tag2Bytes tagNBytes
-  simp only [if_pos hs]
+  simp only [ite_eq_left hs]
   congr 1
   rcases uint8_cases4 flag hflag with rfl | rfl | rfl | rfl <;>
     rcases uint64_cases32 size hsize with