chore: Update Lean to 4.21.0

.github/workflows/ci.yml

@@ -30,9 +30,5 @@ jobs:
         with:
           nix_path: nixpkgs=channel:nixos-unstable
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
-      - uses: cachix/cachix-action@v16
-        with:
-          name: argumentcomputer
-          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-      - run: nix build
-      - run: nix run
+      - run: nix build --accept-flake-config
+      - run: nix run --accept-flake-config

Blake3.lean

@@ -2,7 +2,7 @@
 
 theorem ByteArray.size_of_extract {hash : ByteArray} (hbe : b ≤ e) (h : e ≤ hash.data.size) :
     (hash.extract b e).size = e - b := by
-  simp [ByteArray.size, ByteArray.extract, ByteArray.copySlice, ByteArray.empty, ByteArray.mkEmpty]
+  simp [ByteArray.size, ByteArray.extract, ByteArray.copySlice, ByteArray.empty, ByteArray.emptyWithCapacity]
   rw [Nat.add_comm, Nat.sub_add_cancel hbe, Nat.min_eq_left h]
 
 namespace Blake3
@@ -61,7 +61,7 @@ opaque update (hasher : Hasher) (input : @& ByteArray) : Hasher
 instance {length : USize} : Inhabited { r : ByteArray // r.size = length.toNat } where
   default := ⟨
     ⟨⟨List.replicate length.toNat 0⟩⟩,
-    by simp only [ByteArray.size, List.toArray_replicate, Array.size_mkArray]
+    by simp only [ByteArray.size, List.toArray_replicate, Array.size_replicate]
   ⟩
 
 /-- Finalize the hasher and write the output to an array of a given length. -/
@@ -70,7 +70,7 @@ opaque finalize : (hasher : Hasher) → (length : USize) →
   {r : ByteArray // r.size = length.toNat}
 
 def finalizeWithLength (hasher : Hasher) (length : Nat)
-    (h : length % 2 ^ System.Platform.numBits = length := by native_decide) :
+    (h : length < 2 ^ System.Platform.numBits := by native_decide) :
     { r : ByteArray // r.size = length } :=
   let ⟨hash, h'⟩ := hasher.finalize length.toUSize
   have hash_size_eq_len : hash.size = length := by

blake3.nix

@@ -18,7 +18,7 @@
   buildSteps =
     builtins.map (file: "gcc -O3 -Wall -c ${blake3}/c/${file}.c -o ${file}.o ${blake3Flags}") blake3Files
     ++ [
-      "gcc -O3 -Wall -c ffi.c -o ffi.o -I ${pkgs.lean4}/include -I ${blake3}/c"
+      "gcc -O3 -Wall -c ffi.c -o ffi.o -I ${pkgs.lean}/include -I ${blake3}/c"
       "ar rcs libblake3.a ${(builtins.concatStringsSep " " (builtins.map (str: "${str}.o") blake3Files))} ffi.o"
     ];
   # The `libblake3.a` static library is exposed as the `staticLib` package, as it must be explicitly linked against

flake.nix

@@ -1,15 +1,21 @@
 {
   description = "Blake3 Nix Flake";
 
+  nixConfig = {
+    extra-substituters = [
+      "https://cache.garnix.io"
+    ];
+    extra-trusted-public-keys = [
+      "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g="
+    ];
+  };
+
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    nixpkgs.follows = "lean4-nix/nixpkgs";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix = {
-      url = "github:argumentcomputer/lean4-nix";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
+    lean4-nix.url = "github:lenianiva/lean4-nix";
     blake3 = {
-      url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.6.1";
+      url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.2";
       flake = false;
     };
   };

lakefile.lean

@@ -12,7 +12,7 @@ lean_lib Blake3 where
 lean_exe Blake3Test
 
 abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3"
-abbrev blake3RepoTag := "1.6.1"
+abbrev blake3RepoTag := "1.8.2"
 
 target cloneBlake3 pkg : GitRepo := do
   let repoDir : GitRepo := pkg.dir / "blake3"
@@ -67,4 +67,4 @@ extern_lib ffi pkg := do
   let oFileJobs := #[blake3O, blake3DispatchO, blake3PortableO, ffiO]
 
   let name := nameToStaticLib "ffi"
-  buildStaticLib (pkg.nativeLibDir / name) oFileJobs
+  buildStaticLib (pkg.staticLibDir / name) oFileJobs

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.21.0