chore: bump to Lean v4.30.0-rc2

lean/CoreModels/FunsExternal.lean

@@ -914,38 +914,31 @@ def rust_primitives.arithmetic.to_be_bytes_u128 : Std.U128 → Result (Array Std
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_usize"]
 def rust_primitives.arithmetic.to_be_bytes_usize : Std.Usize → Result (Array Std.U8 8#usize) :=
-  fun x => ok ⟨ (x.bv.setWidth 64).toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (8 * 8)] ⟩
+  fun x => ok ⟨ (x.bv.setWidth 64).toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_i8"]
 def rust_primitives.arithmetic.to_be_bytes_i8 : Std.I8 → Result (Array Std.U8 1#usize) :=
-  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (1 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_i16"]
 def rust_primitives.arithmetic.to_be_bytes_i16 : Std.I16 → Result (Array Std.U8 2#usize) :=
-  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (2 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_i32"]
 def rust_primitives.arithmetic.to_be_bytes_i32 : Std.I32 → Result (Array Std.U8 4#usize) :=
-  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (4 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_i64"]
 def rust_primitives.arithmetic.to_be_bytes_i64 : Std.I64 → Result (Array Std.U8 8#usize) :=
-  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (8 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_i128"]
 def rust_primitives.arithmetic.to_be_bytes_i128 : Std.I128 → Result (Array Std.U8 16#usize) :=
-  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (16 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_be_bytes_isize"]
 def rust_primitives.arithmetic.to_be_bytes_isize : Std.Isize → Result (Array Std.U8 8#usize) :=
-  fun x => ok ⟨ (x.bv.setWidth 64).toBEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toBEBytes_length (8 * 8)] ⟩
+  fun x => ok ⟨ (x.bv.setWidth 64).toBEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_u8"]
 def rust_primitives.arithmetic.to_le_bytes_u8 : Std.U8 → Result (Array Std.U8 1#usize) :=
@@ -969,38 +962,31 @@ def rust_primitives.arithmetic.to_le_bytes_u128 : Std.U128 → Result (Array Std
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_usize"]
 def rust_primitives.arithmetic.to_le_bytes_usize : Std.Usize → Result (Array Std.U8 8#usize) :=
-  fun x => ok ⟨ (x.bv.setWidth 64).toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (8 * 8)] ⟩
+  fun x => ok ⟨ (x.bv.setWidth 64).toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_i8"]
 def rust_primitives.arithmetic.to_le_bytes_i8 : Std.I8 → Result (Array Std.U8 1#usize) :=
-  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (1 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_i16"]
 def rust_primitives.arithmetic.to_le_bytes_i16 : Std.I16 → Result (Array Std.U8 2#usize) :=
-  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (2 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_i32"]
 def rust_primitives.arithmetic.to_le_bytes_i32 : Std.I32 → Result (Array Std.U8 4#usize) :=
-  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (4 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_i64"]
 def rust_primitives.arithmetic.to_le_bytes_i64 : Std.I64 → Result (Array Std.U8 8#usize) :=
-  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (8 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_i128"]
 def rust_primitives.arithmetic.to_le_bytes_i128 : Std.I128 → Result (Array Std.U8 16#usize) :=
-  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (16 * 8)] ⟩
+  fun x => ok ⟨ x.bv.toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::to_le_bytes_isize"]
 def rust_primitives.arithmetic.to_le_bytes_isize : Std.Isize → Result (Array Std.U8 8#usize) :=
-  fun x => ok ⟨ (x.bv.setWidth 64).toLEBytes.map UScalar.mk, by
-    simp only [List.length_map, UScalar.ofNatCore_val_eq, @BitVec.toLEBytes_length (8 * 8)] ⟩
+  fun x => ok ⟨ (x.bv.setWidth 64).toLEBytes.map UScalar.mk, by grind [BitVec.toBEBytes_length] ⟩
 
 @[rust_fun "rust_primitives::arithmetic::abs_i8"]
 def rust_primitives.arithmetic.abs_i8 : Std.I8 → Result Std.I8 :=

lean/CoreModels/Types.lean

@@ -760,7 +760,7 @@ structure ops.try_trait.FromResidual (Self : Type) (R : Type) where
 structure ops.try_trait.Try (Self : Type) (Self_Output : Type) (Self_Residual :
   Type) where
   from_output : Self_Output → Result Self
-  branch : Self → Result (ops.control_flow.ControlFlow Self_Residual
+  «branch» : Self → Result (ops.control_flow.ControlFlow Self_Residual
     Self_Output)
 
 /-- Trait declaration: [core_models::ops::deref::Deref]

lean/lake-manifest.json

@@ -1,31 +1,31 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/abentkamp/aeneas",
    "type": "git",
    "subDir": "backends/lean",
    "scope": "",
-   "rev": "4e02d6d8e1421562e6ab4a9737fae159ba602d8b",
+   "rev": "14dff64073df177210e5335bed1a5cb62d13274e",
    "name": "aeneas",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4e02d6d8e1421562e6ab4a9737fae159ba602d8b",
+   "inputRev": "14dff64073df177210e5335bed1a5cb62d13274e",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
+   "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
+   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,51 +55,52 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.86",
+   "inputRev": "v0.0.98",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
+   "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
+   "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "CoreModels",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lean/lakefile.toml

@@ -8,4 +8,4 @@ name = "CoreModels"
 [[require]]
 name = "aeneas"
 git = { url = "https://github.com/abentkamp/aeneas", subDir = "backends/lean" }
-rev = "4e02d6d8e1421562e6ab4a9737fae159ba602d8b"
+rev = "14dff64073df177210e5335bed1a5cb62d13274e"

lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.28.0-rc1
+leanprover/lean4:v4.30.0-rc2

patch_lean.py

@@ -225,6 +225,13 @@ def rewrite_phantom_data(text: str) -> str:
         text, ["core_models::marker::PhantomData"],
         trailer="replaced by core_models.Phantom (see rewrite_alloc_phantom_data)",
     )
+
+def escape_keywords(text: str) -> str:
+    """Aeneas introduces `branch` as a keyword, so we need to escape it.
+    https://github.com/AeneasVerif/aeneas/issues/1023
+    """
+    return re.sub(r"(?<![A-Za-z0-9])branch(?![A-Za-z0-9])", "«branch»", text)
+
 
 def desugar_pure_num_bound_binds(text: str) -> str:
     """The generated `Funs.lean` uses monadic bind syntax to fetch numeric
@@ -497,6 +504,7 @@ def main() -> int:
         text = read(path)
         text = rewrite_imports_and_opens(text)
         text = rewrite_phantom_data(text)
+        text = escape_keywords(text)
         if path == funs_path:
             text = fix_fail_panic(text)
             text = add_funs_prologue_import(text)

tests/lean/lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",
@@ -12,27 +12,27 @@
    "type": "git",
    "subDir": "backends/lean",
    "scope": "",
-   "rev": "4e02d6d8e1421562e6ab4a9737fae159ba602d8b",
+   "rev": "14dff64073df177210e5335bed1a5cb62d13274e",
    "name": "aeneas",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4e02d6d8e1421562e6ab4a9737fae159ba602d8b",
+   "inputRev": "14dff64073df177210e5335bed1a5cb62d13274e",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
+   "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
+   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,51 +62,52 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.86",
+   "inputRev": "v0.0.98",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
+   "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
+   "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Tests",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

tests/lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.28.0-rc1
+leanprover/lean4:v4.30.0-rc2