chore: Update to Lean v4.26.0 and Rust 1.92 (#290)

* chore: Update lean4-nix

* Update

* (WIP) chore: Update Lean to v4.26.0

* Update lean4-nix and Rust 1.92

* Fix lints

* Update Blake3.lean

Author: samuelburnham

.github/workflows/nix.yml

@@ -26,7 +26,7 @@ jobs:
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
       # Ix CLI
       - run: nix build --print-build-logs --accept-flake-config
-      - run: nix run .#default -- --help
+      - run: nix run .#ix -- --help
       # Ix benches
       - run: nix build .#bench-aiur --print-build-logs --accept-flake-config
       - run: nix build .#bench-blake3 --print-build-logs --accept-flake-config

Ix/Address.lean

@@ -60,7 +60,7 @@ def natOfHex : Char -> Option Nat
 def hexOfByte (b : UInt8) : String :=
   let hi := hexOfNat (UInt8.toNat (b >>> 4))
   let lo := hexOfNat (UInt8.toNat (b &&& 0xF))
-  String.mk [hi.get!, lo.get!]
+  String.ofList [hi.get!, lo.get!]
 
 /-- Convert a ByteArray to a big-endian hexadecimal string. -/
 def hexOfBytes (ba : ByteArray) : String :=

Ix/Benchmark/Bench.lean

@@ -333,10 +333,10 @@ def padWhitespace (input : String) (width : Nat) : String :=
   let padWidth := width - input.length 
   let leftPad := padWidth / 2
   let rightPad := padWidth - leftPad
-  String.mk (List.replicate leftPad ' ') ++ input ++ (String.mk (List.replicate rightPad ' '))
+  String.ofList (List.replicate leftPad ' ') ++ input ++ (String.ofList (List.replicate rightPad ' '))
 
 def padDashes (width : Nat) : String :=
-  String.mk (List.replicate width '-')
+  String.ofList (List.replicate width '-')
 
 def mkReportPretty' (columnWidths : ColumnWidths) (reportPretty : String) (row : BenchReport) : String :=
   let functionStr := padWhitespace row.function columnWidths.function

Ix/Common.lean

@@ -38,8 +38,8 @@ deriving instance BEq, Repr, Ord, Hashable for Lean.QuotKind
 deriving instance BEq, Repr, Ord, Hashable for Lean.ReducibilityHints
 deriving instance BEq, Repr, Ord, Hashable for Lean.DefinitionSafety
 deriving instance BEq, Repr, Ord, Hashable for ByteArray
-deriving instance BEq, Repr, Ord, Hashable for String.Pos
-deriving instance BEq, Repr, Ord, Hashable for Substring
+deriving instance BEq, Repr, Ord, Hashable for String.Pos.Raw
+deriving instance BEq, Repr, Ord, Hashable for Substring.Raw
 deriving instance BEq, Repr, Ord, Hashable for Lean.SourceInfo
 deriving instance BEq, Repr, Ord, Hashable for Lean.Syntax.Preresolved
 deriving instance BEq, Repr, Ord, Hashable for Lean.Syntax

Ix/CompileM.lean

@@ -227,7 +227,7 @@ def compileLevel (lvl: Lean.Level): CompileM MetaAddress := do
       | none   => do throw <| .levelNotFound (<- read).current n lvls s!"compileLevel"
     | l@(.mvar ..) => throw $ .levelMetavariable l
 
-def compileSubstring : Substring -> CompileM Ixon.Substring
+def compileSubstring : Substring.Raw -> CompileM Ixon.Substring
 | ⟨str, startPos, stopPos⟩ => do
     pure ⟨<- storeString str, startPos.byteIdx, stopPos.byteIdx⟩
 

Ix/Store.lean

@@ -43,9 +43,11 @@ def storeDir : StoreIO FilePath := do
 def storePath (addr: Address): StoreIO FilePath := do
   let store <- storeDir
   let hex := hexOfBytes addr.hash
-  let dir1 := String.mk [(hex.get ⟨0⟩), (hex.get ⟨1⟩)]
-  let dir2 := String.mk [(hex.get ⟨2⟩), (hex.get ⟨3⟩)]
-  let dir3 := String.mk [(hex.get ⟨4⟩), (hex.get ⟨5⟩)]
+  -- TODO: Use Slice API once it matures
+  let hexChars := hex.toSlice.chars.toList
+  let dir1 := String.ofList [hexChars[0]!, hexChars[1]!]
+  let dir2 := String.ofList [hexChars[2]!, hexChars[3]!]
+  let dir3 := String.ofList [hexChars[4]!, hexChars[5]!]
   let file := hex.drop 6
   let path := store / dir1 / dir2 / dir3
   if !(<- path.pathExists) then

Tests/Ix.lean

@@ -119,7 +119,7 @@ def parseHex (x : String) : ByteArray :=
   let x :=
     if x.startsWith "0x" || x.startsWith "0X" then x.drop 2 else x
   -- remove underscores
-  let x := String.mk (x.toList.filter (· ≠ '_'))
+  let x := String.ofList (x.toList.filter (· ≠ '_'))
   -- must have an even number of hex digits
   if x.length % 2 = 1 then
     panic! "parseHex: odd number of hex digits"
@@ -128,8 +128,8 @@ def parseHex (x : String) : ByteArray :=
     let rec loop (i : Nat) (acc : ByteArray) : ByteArray :=
       if i < n then
         -- safe since ASCII: `String.get!` indexes by chars
-        let c1 := x.get! ⟨i⟩
-        let c2 := x.get! ⟨i+1⟩
+        let c1 := String.Pos.Raw.get! x ⟨i⟩ 
+        let c2 := String.Pos.Raw.get! x ⟨i+1⟩
         match hexVal? c1, hexVal? c2 with
         | some hi, some lo =>
           let b : UInt8 := (hi <<< 4) ||| lo
@@ -148,8 +148,8 @@ def printHex (ba : ByteArray) : String :=
       let b := ba.get! i
       let hi := (b.toNat / 16)
       let lo := (b.toNat % 16)
-      let acc := acc.push (hexdigits.get! ⟨hi⟩)
-      let acc := acc.push (hexdigits.get! ⟨lo⟩)
+      let acc := acc.push (String.Pos.Raw.get! hexdigits ⟨hi⟩)
+      let acc := acc.push (String.Pos.Raw.get! hexdigits ⟨lo⟩)
       go (i + 1) acc
     else acc
   "0x" ++ go 0 ""

deny.toml

@@ -75,7 +75,6 @@ ignore = [
     "RUSTSEC-2024-0370", # `proc-macro-error` crate is unmaintained
     "RUSTSEC-2023-0089", # `atomic-polyfill` crate is unmaintained
     "RUSTSEC-2025-0141", # `bincode` crate is unmaintained
-
     #{ id = "RUSTSEC-0000-0000", reason = "you can specify a reason the advisory is ignored" },
     #"a-crate-that-is-yanked@0.1.1", # you can also ignore yanked crate versions if you wish
     #{ crate = "a-crate-that-is-yanked@0.1.1", reason = "you can specify why you are ignoring the yanked crate" },
@@ -122,66 +121,12 @@ exceptions = [
 # Some crates don't have (easily) machine readable licensing information,
 # adding a clarification entry for it allows you to manually specify the
 # licensing information
-[[licenses.clarify]]
-crate = "binius_circuits"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_core"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_field"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_hal"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_hash"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_macros"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_math"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_maybe_rayon"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_ntt"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_utils"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
+# [[licenses.clarify]]
+# crate = "binius_circuits"
+# expression = "Apache-2.0"
+# license-files = [
+#   { path = "../../LICENSE.txt", hash = 0 }
+# ]
 # The package spec the clarification applies to
 #crate = "ring"
 # The SPDX expression for the license requirements of the crate