diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eeb9e57..6a7c041 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Blake3.lean b/Blake3.lean index 5e8d981..d0691b9 100644 --- a/Blake3.lean +++ b/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 diff --git a/blake3.nix b/blake3.nix index 4ba66ba..f27e152 100644 --- a/blake3.nix +++ b/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 diff --git a/flake.lock b/flake.lock index 18e555d..53038b9 100644 --- a/flake.lock +++ b/flake.lock @@ -3,16 +3,16 @@ "blake3": { "flake": false, "locked": { - "lastModified": 1740677543, - "narHash": "sha256-YJ3rRzpmF6oS8p377CEoRteARCD1lr/L7/fbN5poUXw=", + "lastModified": 1745192552, + "narHash": "sha256-IABVErXWYQFXZcwsFKfQhm3ox7UZUcW5uzVrGwsSp94=", "owner": "BLAKE3-team", "repo": "BLAKE3", - "rev": "0f9dc2706f931366632a378a95b348e3cb40ed01", + "rev": "df610ddc3b93841ffc59a87e3da659a15910eb46", "type": "github" }, "original": { "owner": "BLAKE3-team", - "ref": "refs/tags/1.6.1", + "ref": "refs/tags/1.8.2", "repo": "BLAKE3", "type": "github" } @@ -22,11 +22,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1743550720, - "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=", + "lastModified": 1754487366, + "narHash": "sha256-pHYj8gUBapuUzKV/kN/tR3Zvqc7o6gdFB9XKXIp1SQ8=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "c621e8422220273271f52058f618c94e405bb0f5", + "rev": "af66ad14b28a127c5c0f3bbb298218fc63528a18", "type": "github" }, "original": { @@ -40,11 +40,11 @@ "nixpkgs-lib": "nixpkgs-lib_2" }, "locked": { - "lastModified": 1743550720, - "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=", + "lastModified": 1727826117, + "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "c621e8422220273271f52058f618c94e405bb0f5", + "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1", "type": "github" }, "original": { @@ -56,31 +56,29 @@ "lean4-nix": { "inputs": { "flake-parts": "flake-parts_2", - "nixpkgs": [ - "nixpkgs" - ] + "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1744206621, - "narHash": "sha256-17kctQIIENhliHEQzzM06OlzrF4uyq6w7KOXSeNbZc4=", - "owner": "argumentcomputer", + "lastModified": 1755389677, + "narHash": "sha256-q79j0+9Vr+QlRmJJijoXmEiMy2hl2lOXsLbjkGeAGnU=", + "owner": "lenianiva", "repo": "lean4-nix", - "rev": "f798c4f818301c3dd3f5ffa1b667f824b72921a4", + "rev": "f6b97c79060dcbc7db0c2c9cde5061186c77f4af", "type": "github" }, "original": { - "owner": "argumentcomputer", + "owner": "lenianiva", "repo": "lean4-nix", "type": "github" } }, "nixpkgs": { "locked": { - "lastModified": 1744098102, - "narHash": "sha256-tzCdyIJj9AjysC3OuKA+tMD/kDEDAF9mICPDU7ix0JA=", + "lastModified": 1743095683, + "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=", "owner": "nixos", "repo": "nixpkgs", - "rev": "c8cd81426f45942bb2906d5ed2fe21d2f19d95b7", + "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6", "type": "github" }, "original": { @@ -92,11 +90,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1743296961, - "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=", + "lastModified": 1753579242, + "narHash": "sha256-zvaMGVn14/Zz8hnp4VWT9xVnhc8vuL3TStRqwk22biA=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa", + "rev": "0f36c44e01a6129be94e3ade315a5883f0228a6e", "type": "github" }, "original": { @@ -107,17 +105,14 @@ }, "nixpkgs-lib_2": { "locked": { - "lastModified": 1743296961, - "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=", - "owner": "nix-community", - "repo": "nixpkgs.lib", - "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa", - "type": "github" + "lastModified": 1727825735, + "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" }, "original": { - "owner": "nix-community", - "repo": "nixpkgs.lib", - "type": "github" + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" } }, "root": { @@ -125,7 +120,10 @@ "blake3": "blake3", "flake-parts": "flake-parts", "lean4-nix": "lean4-nix", - "nixpkgs": "nixpkgs" + "nixpkgs": [ + "lean4-nix", + "nixpkgs" + ] } } }, diff --git a/flake.nix b/flake.nix index c9fd2b5..0f1c217 100644 --- a/flake.nix +++ b/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; }; }; diff --git a/lakefile.lean b/lakefile.lean index dedd76e..0e529fa 100644 --- a/lakefile.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index b2153cd..980709b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0 +leanprover/lean4:v4.21.0