Correctness Proofs for SHA-3 (Part 2): Proofs for Portable Keccak-f1600

CHANGELOG.md

@@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added
+
+- [#1399](https://github.com/cryspen/libcrux/pull/1399): Add a Rust spec for SHA-3
+
 ### Removed
 
 - [#1391](https://github.com/cryspen/libcrux/pull/1391): Remove support for HMAC-SHA1

Cargo.toml

@@ -87,7 +87,7 @@ readme = "Readme.md"
 allow-branch = ["main"]
 
 [workspace.dependencies]
-hax-lib = { version = "=0.3.6" }
+hax-lib = { git = "https://github.com/cryspen/hax", branch = "integer-lemmas" }
 libcrux-aead = { version = "=0.0.7", path = "crates/primitives/aead" }
 libcrux-aesgcm = { version = "=0.0.7", path = "crates/algorithms/aesgcm" }
 libcrux-blake2 = { version = "=0.0.6", path = "crates/algorithms/blake2" }
@@ -234,6 +234,9 @@ rand_chacha = { version = "0.10.0" }
 getrandom = { version = "0.4" }
 wasm-bindgen-test = "0.3"
 
+[patch.crates-io]
+hax-lib = { git = "https://github.com/cryspen/hax", branch = "integer-lemmas" }
+
 [profile.release]
 lto = "fat"
 codegen-units = 1

crates/algorithms/sha3/Cargo.toml

@@ -34,6 +34,7 @@ rand = "0.10"
 cavp = { path = "../../../cavp" }
 pretty_env_logger = "0.5.0"
 clap = { version = "4.5.39", features = ["derive"] }
+hacspec_sha3 = { path = "../../../specs/sha3" }
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)', 'cfg(eurydice)'] }

crates/algorithms/sha3/hax.sh

@@ -1,6 +1,15 @@
 #!/usr/bin/env bash
 set -ex
 
+# GNU sed: system `sed` on Linux is already GNU sed; on macOS the system
+# `sed` is BSD and rejects the GNU `-i` form, so we need `gsed` (Homebrew
+# `gnu-sed` package) there. Detect at script start and route through $SED.
+if [ "$(uname)" = "Darwin" ]; then
+    SED="gsed"
+else
+    SED="sed"
+fi
+
 function extract_all() {
     extract crates/sys/platform \
         into -i "+:** -**::x86::init::cpuid -**::x86::init::cpuid_count" \
@@ -79,14 +88,14 @@ function rename_core_models_files() {
         new_filename="Libcrux_core_models${filename#Core_models}"
         mv "$file" "$dir_path/$new_filename"
     done
-    find "$target_dir" -type f \( -name "*.fst" -o -name "*.fsti" \) -exec sed -i'' \
+    find "$target_dir" -type f \( -name "*.fst" -o -name "*.fsti" \) -exec "$SED" -i \
         -e 's/module Core_models/module Libcrux_core_models/g' \
         {} +
 }
 
 function rename_core_models_uses() {
     local target_dir="proofs/fstar/extraction"
-    find "$target_dir" -type f \( -name "*.fst" -o -name "*.fsti" \) -exec sed -i'' \
+    find "$target_dir" -type f \( -name "*.fst" -o -name "*.fsti" \) -exec "$SED" -i \
         -e 's/Core_models\.Abstractions/Libcrux_core_models.Abstractions/g' \
         -e 's/Core_models\.Core_arch/Libcrux_core_models.Core_arch/g' \
         {} +

crates/algorithms/sha3/proofs/fstar/equivalence/.hints/EquivImplSpec.Keccakf.SpecRounds.fst.hints

@@ -0,0 +1,249 @@
+[
+  "afc9855a38c759d630ff8d17d99a7c4c",
+  [
+    [
+      "EquivImplSpec.Keccakf.SpecRounds.spec_state",
+      1,
+      0,
+      1,
+      [
+        "@MaxFuel_assumption", "@MaxIFuel_assumption",
+        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
+        "constructor_distinct_Rust_primitives.Integers.USIZE",
+        "equality_tok_Rust_primitives.Integers.USIZE@tok",
+        "equation_Prims.nat", "equation_Rust_primitives.Integers.bits",
+        "equation_Rust_primitives.Integers.maxint",
+        "equation_Rust_primitives.Integers.minint",
+        "equation_Rust_primitives.Integers.range",
+        "equation_Rust_primitives.Integers.unsigned",
+        "lemma_Rust_primitives.Integers.pow2_values",
+        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
+        "primitive_Prims.op_Subtraction",
+        "projection_inverse_BoxBool_proj_0",
+        "projection_inverse_BoxInt_proj_0",
+        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
+        "refinement_interpretation_Tm_refine_b045b04f0bb15cd7c94a2ec78d3283ce",
+        "typing_Rust_primitives.Integers.bits",
+        "typing_Rust_primitives.Integers.size_bits",
+        "typing_tok_Rust_primitives.Integers.USIZE@tok"
+      ],
+      0,
+      "ce4923e4039227e2a37c9774b71f6bbf"
+    ],
+    [
+      "EquivImplSpec.Keccakf.SpecRounds.spec_one_round",
+      1,
+      0,
+      1,
+      [
+        "@MaxFuel_assumption", "@MaxIFuel_assumption",
+        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
+        "constructor_distinct_Rust_primitives.Integers.USIZE",
+        "equality_tok_Rust_primitives.Integers.USIZE@tok",
+        "equation_EquivImplSpec.Keccakf.SpecRounds.spec_state",
+        "equation_Prims.nat", "equation_Rust_primitives.Integers.bits",
+        "equation_Rust_primitives.Integers.maxint",
+        "equation_Rust_primitives.Integers.minint",
+        "equation_Rust_primitives.Integers.range",
+        "equation_Rust_primitives.Integers.unsigned",
+        "lemma_Rust_primitives.Integers.pow2_values",
+        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
+        "primitive_Prims.op_Subtraction",
+        "projection_inverse_BoxBool_proj_0",
+        "projection_inverse_BoxInt_proj_0",
+        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
+        "refinement_interpretation_Tm_refine_b045b04f0bb15cd7c94a2ec78d3283ce",
+        "typing_Rust_primitives.Integers.bits",
+        "typing_Rust_primitives.Integers.size_bits",
+        "typing_tok_Rust_primitives.Integers.USIZE@tok"
+      ],
+      0,
+      "a57f7bfa4f2d05b475bada4f0e7a6959"
+    ],
+    [
+      "EquivImplSpec.Keccakf.SpecRounds.spec_rounds",
+      1,
+      0,
+      1,
+      [
+        "@MaxFuel_assumption", "@MaxIFuel_assumption",
+        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
+        "Prims_pretyping_ae567c2fb75be05905677af440075565",
+        "assumption_Rust_primitives.Integers.int_t__uu___haseq",
+        "binder_x_3a77ceb7bb6324c0d5c09dbbede3a3d5_1",
+        "binder_x_6173fc66c0db2954367d8319920acab1_0",
+        "constructor_distinct_Rust_primitives.Integers.USIZE",
+        "data_elim_Rust_primitives.Integers.MkInt",
+        "equality_tok_Rust_primitives.Integers.USIZE@tok",
+        "equation_Prims.nat", "equation_Rust_primitives.Integers.add",
+        "equation_Rust_primitives.Integers.bits",
+        "equation_Rust_primitives.Integers.lt",
+        "equation_Rust_primitives.Integers.lte",
+        "equation_Rust_primitives.Integers.maxint",
+        "equation_Rust_primitives.Integers.minint",
+        "equation_Rust_primitives.Integers.mk_int",
+        "equation_Rust_primitives.Integers.mk_usize",
+        "equation_Rust_primitives.Integers.range",
+        "equation_Rust_primitives.Integers.range_t",
+        "equation_Rust_primitives.Integers.unsigned",
+        "equation_Rust_primitives.Integers.usize",
+        "equation_Rust_primitives.Integers.v",
+        "fuel_guarded_inversion_Rust_primitives.Integers.int_t",
+        "function_token_typing_Prims.__cache_version_number__",
+        "int_inversion", "int_typing",
+        "lemma_Rust_primitives.Integers.pow2_values",
+        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
+        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
+        "primitive_Prims.op_LessThanOrEqual",
+        "primitive_Prims.op_Subtraction",
+        "proj_equation_Rust_primitives.Integers.MkInt_@_0",
+        "projection_inverse_BoxBool_proj_0",
+        "projection_inverse_BoxInt_proj_0",
+        "projection_inverse_Rust_primitives.Integers.MkInt_@_0",
+        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
+        "refinement_interpretation_Tm_refine_a6d4eccfb2603ce5e66d6162c32df2b0",
+        "refinement_interpretation_Tm_refine_b045b04f0bb15cd7c94a2ec78d3283ce",
+        "typing_Rust_primitives.Integers.bits",
+        "typing_Rust_primitives.Integers.size_bits",
+        "typing_tok_Rust_primitives.Integers.USIZE@tok",
+        "well-founded-ordering-on-nat"
+      ],
+      0,
+      "39eac20f15176d5f09eebdb7e2164dc9"
+    ],
+    [
+      "EquivImplSpec.Keccakf.SpecRounds.spec_rounds",
+      2,
+      0,
+      1,
+      [
+        "@MaxFuel_assumption", "@MaxIFuel_assumption",
+        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
+        "constructor_distinct_Rust_primitives.Integers.USIZE",
+        "equality_tok_Rust_primitives.Integers.USIZE@tok",
+        "equation_Prims.nat", "equation_Rust_primitives.Integers.bits",
+        "equation_Rust_primitives.Integers.maxint",
+        "equation_Rust_primitives.Integers.minint",
+        "equation_Rust_primitives.Integers.range",
+        "equation_Rust_primitives.Integers.unsigned",
+        "lemma_Rust_primitives.Integers.pow2_values",
+        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
+        "primitive_Prims.op_Subtraction",
+        "projection_inverse_BoxBool_proj_0",
+        "projection_inverse_BoxInt_proj_0",
+        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
+        "refinement_interpretation_Tm_refine_b045b04f0bb15cd7c94a2ec78d3283ce",
+        "typing_Rust_primitives.Integers.bits",
+        "typing_Rust_primitives.Integers.size_bits",
+        "typing_tok_Rust_primitives.Integers.USIZE@tok"
+      ],
+      0,
+      "d203dc7fe693e0e6798b9ff52b01fce4"
+    ],
+    [
+      "EquivImplSpec.Keccakf.SpecRounds.lemma_keccak_f_is_rounds",
+      1,
+      30,
+      2,
+      [
+        "@MaxFuel_assumption", "@MaxIFuel_assumption",
+        "@fuel_correspondence_EquivImplSpec.Keccakf.SpecRounds.spec_rounds.fuel_instrumented",
+        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
+        "@fuel_correspondence_Rust_primitives.Hax.Folds.fold_range.fuel_instrumented",
+        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
+        "Hacspec_sha3.Keccak_f_interpretation_Tm_arrow_6810ffd7fedc9f5daa2182e9ac575b71",
+        "Hacspec_sha3.Keccak_f_interpretation_Tm_arrow_7a864fbdb6dd4bcf55036cd2914f3e4c",
+        "Hacspec_sha3.Keccak_f_interpretation_Tm_arrow_d98c07d1b05717a33aa6ea3355704a07",
+        "Hacspec_sha3_interpretation_Tm_arrow_bf71e124d232d47c997d72c21e536b9a",
+        "Rust_primitives.Arrays_interpretation_Tm_arrow_0d263c675f2f6a422e85e8ffa504d5e2",
+        "Rust_primitives.Hax.Folds_interpretation_Tm_arrow_8a1b3c71b8eb003c7bfb24d380080447",
+        "Rust_primitives.Hax.Folds_interpretation_Tm_arrow_c8b6fefc6a1ff03b84fa2dbb43486b72",
+        "bool_inversion", "bool_typing",
+        "constructor_distinct_Rust_primitives.Integers.USIZE",
+        "equality_tok_Rust_primitives.Integers.USIZE@tok",
+        "equation_EquivImplSpec.Keccakf.SpecRounds.spec_one_round",
+        "equation_EquivImplSpec.Keccakf.SpecRounds.spec_state",
+        "equation_Hacspec_sha3.Keccak_f.chi",
+        "equation_Hacspec_sha3.Keccak_f.iota",
+        "equation_Hacspec_sha3.Keccak_f.keccak_f",
+        "equation_Hacspec_sha3.Keccak_f.pi",
+        "equation_Hacspec_sha3.Keccak_f.rho",
+        "equation_Hacspec_sha3.Keccak_f.theta",
+        "equation_Hacspec_sha3.createi", "equation_Prims.logical",
+        "equation_Prims.nat", "equation_Rust_primitives.Arrays.t_Array",
+        "equation_Rust_primitives.Integers.add",
+        "equation_Rust_primitives.Integers.bits",
+        "equation_Rust_primitives.Integers.lt",
+        "equation_Rust_primitives.Integers.lte",
+        "equation_Rust_primitives.Integers.max_usize",
+        "equation_Rust_primitives.Integers.maxint",
+        "equation_Rust_primitives.Integers.minint",
+        "equation_Rust_primitives.Integers.mk_int",
+        "equation_Rust_primitives.Integers.mk_usize",
+        "equation_Rust_primitives.Integers.range",
+        "equation_Rust_primitives.Integers.range_t",
+        "equation_Rust_primitives.Integers.u64",
+        "equation_Rust_primitives.Integers.unsigned",
+        "equation_Rust_primitives.Integers.usize",
+        "equation_Rust_primitives.Integers.v",
+        "equation_with_fuel_EquivImplSpec.Keccakf.SpecRounds.spec_rounds.fuel_instrumented",
+        "equation_with_fuel_Rust_primitives.Hax.Folds.fold_range.fuel_instrumented",
+        "fuel_guarded_inversion_Rust_primitives.Integers.int_t",
+        "function_token_typing_EquivImplSpec.Keccakf.SpecRounds.spec_state",
+        "function_token_typing_Prims.l_True",
+        "function_token_typing_Rust_primitives.Integers.u64",
+        "int_inversion", "int_typing",
+        "interpretation_Tm_abs_c7a42c9e2d08fd782bf7613c32495cc6",
+        "interpretation_Tm_abs_fec714da2f5de09f2f4136a904db729a",
+        "kinding_Tm_arrow_d28fde83d99b9fd411f0baa86bc882a5",
+        "lemma_Rust_primitives.Integers.pow2_values",
+        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
+        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
+        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
+        "primitive_Prims.op_Subtraction",
+        "proj_equation_Rust_primitives.Integers.MkInt_@_0",
+        "projection_inverse_BoxBool_proj_0",
+        "projection_inverse_BoxInt_proj_0",
+        "projection_inverse_Rust_primitives.Integers.MkInt_@_0",
+        "refinement_interpretation_Tm_refine_066b9eb21a98c28e978234780f41cd65",
+        "refinement_interpretation_Tm_refine_21e0277b21b9413896fa7f0b23f8625e",
+        "refinement_interpretation_Tm_refine_221edc532b512849362f091b0318b99d",
+        "refinement_interpretation_Tm_refine_414b3103e63acaca337a620ee42bb932",
+        "refinement_interpretation_Tm_refine_51996c5c6192f6c4d97f417a4cc27ac1",
+        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
+        "refinement_interpretation_Tm_refine_6af5dd912a49c5aa2d10fa9f5a5534c2",
+        "refinement_interpretation_Tm_refine_6c47c697fcc84e50a76cc2c5fae4d1cf",
+        "refinement_interpretation_Tm_refine_a6d4eccfb2603ce5e66d6162c32df2b0",
+        "refinement_interpretation_Tm_refine_b045b04f0bb15cd7c94a2ec78d3283ce",
+        "refinement_interpretation_Tm_refine_d68a8e9a56d7d58a15fd1befad9cf1e1",
+        "refinement_interpretation_Tm_refine_de8fb64794f3d3be9a0d175b28ad5581",
+        "refinement_interpretation_Tm_refine_e39af703595e7eb2b64454d7798b53d7",
+        "refinement_interpretation_Tm_refine_eea4a7aaf0d9fd792b6bd561042bfd5e",
+        "refinement_interpretation_Tm_refine_f21ae58475c7fc74d7e8a7c2eff3f408",
+        "true_interp",
+        "typing_EquivImplSpec.Keccakf.SpecRounds.spec_one_round",
+        "typing_FStar.Seq.Base.length", "typing_Hacspec_sha3.Keccak_f.chi",
+        "typing_Hacspec_sha3.Keccak_f.iota",
+        "typing_Hacspec_sha3.Keccak_f.keccak_f",
+        "typing_Hacspec_sha3.Keccak_f.pi",
+        "typing_Hacspec_sha3.Keccak_f.rho",
+        "typing_Hacspec_sha3.Keccak_f.theta", "typing_Hacspec_sha3.createi",
+        "typing_Rust_primitives.Arrays.createi",
+        "typing_Rust_primitives.Integers.add",
+        "typing_Rust_primitives.Integers.bits",
+        "typing_Rust_primitives.Integers.minint",
+        "typing_Rust_primitives.Integers.mk_int",
+        "typing_Rust_primitives.Integers.mk_usize",
+        "typing_Rust_primitives.Integers.range",
+        "typing_Rust_primitives.Integers.size_bits",
+        "typing_Tm_abs_6e12770ddd2256a6e162b3b613591f54",
+        "typing_Tm_abs_6ec269a97cc9e7124e00f9ceda15e72d",
+        "typing_Tm_abs_c7a42c9e2d08fd782bf7613c32495cc6",
+        "typing_Tm_abs_fec714da2f5de09f2f4136a904db729a",
+        "typing_tok_Rust_primitives.Integers.USIZE@tok"
+      ],
+      0,
+      "f80a8d850b6b37d5a508bb2607f78e6d"
+    ]
+  ]
+]