Skip to content

Commit

Permalink
Merge pull request #281 from cryspen/hax-679
Browse files Browse the repository at this point in the history
Regenerate patches following PR hacspec/hax#679
  • Loading branch information
franziskuskiefer authored May 17, 2024
2 parents e70711c + a6f7c49 commit 901dec8
Show file tree
Hide file tree
Showing 15 changed files with 1,324 additions and 730 deletions.
1,274 changes: 861 additions & 413 deletions proofs/fstar/extraction-edited.patch

Large diffs are not rendered by default.

128 changes: 64 additions & 64 deletions proofs/fstar/extraction-secret-independent.patch

Large diffs are not rendered by default.

8 changes: 5 additions & 3 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ let get_n_least_significant_bits (n: u8) (value: u32) =
let barrett_reduce (value: i32) =
let _:Prims.unit = () <: Prims.unit in
let t:i64 =
((Core.Convert.f_from value <: i64) *! v_BARRETT_MULTIPLIER <: i64) +!
((Core.Convert.f_from #i64 #i32 value <: i64) *! v_BARRETT_MULTIPLIER <: i64) +!
(v_BARRETT_R >>! 1l <: i64)
in
let quotient:i32 = cast (t >>! v_BARRETT_SHIFT <: i64) <: i32 in
Expand Down Expand Up @@ -48,11 +48,13 @@ let add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement) =
let _:Prims.unit = () <: Prims.unit in
let _:Prims.unit = () <: Prims.unit in
let lhs:t_PolynomialRingElement =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end
=
Core.Slice.impl__len (Rust_primitives.unsize lhs.f_coefficients <: t_Slice i32)
Core.Slice.impl__len #i32 (Rust_primitives.unsize lhs.f_coefficients <: t_Slice i32)
<:
usize
}
Expand Down
17 changes: 9 additions & 8 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fsti
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ val get_n_least_significant_bits (n: u8) (value: u32)
(ensures
fun result ->
let result:u32 = result in
result <. (Core.Num.impl__u32__pow 2ul (Core.Convert.f_into n <: u32) <: u32))
result <. (Core.Num.impl__u32__pow 2ul (Core.Convert.f_into #u8 #u32 n <: u32) <: u32))

/// Signed Barrett Reduction
/// Given an input `value`, `barrett_reduce` outputs a representative `result`
Expand All @@ -54,8 +54,8 @@ val get_n_least_significant_bits (n: u8) (value: u32)
val barrett_reduce (value: i32)
: Prims.Pure i32
(requires
(Core.Convert.f_from value <: i64) >. (Core.Ops.Arith.Neg.neg v_BARRETT_R <: i64) &&
(Core.Convert.f_from value <: i64) <. v_BARRETT_R)
(Core.Convert.f_from #i64 #i32 value <: i64) >. (Core.Ops.Arith.Neg.neg v_BARRETT_R <: i64) &&
(Core.Convert.f_from #i64 #i32 value <: i64) <. v_BARRETT_R)
(ensures
fun result ->
let result:i32 = result in
Expand Down Expand Up @@ -132,7 +132,8 @@ let impl__PolynomialRingElement__ZERO: t_PolynomialRingElement =
val add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement)
: Prims.Pure t_PolynomialRingElement
(requires
Hax_lib.v_forall (fun i ->
Hax_lib.v_forall #usize
(fun i ->
let i:usize = i in
Hax_lib.implies (i <. Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT
<:
Expand All @@ -155,12 +156,12 @@ val add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement)
(ensures
fun result ->
let result:t_PolynomialRingElement = result in
Hax_lib.v_forall (fun i ->
Hax_lib.v_forall #usize
(fun i ->
let i:usize = i in
Hax_lib.implies (i <.
(Core.Slice.impl__len (Rust_primitives.unsize result.f_coefficients
<:
t_Slice i32)
(Core.Slice.impl__len #i32
(Rust_primitives.unsize result.f_coefficients <: t_Slice i32)
<:
usize)
<:
Expand Down
11 changes: 6 additions & 5 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,9 @@ let compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_
let _:Prims.unit = () <: Prims.unit in
let (r: u8):u8 = 0uy in
let r:u8 =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_CIPHERTEXT_SIZE
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_CIPHERTEXT_SIZE }
<:
Core.Ops.Range.t_Range usize)
<:
Expand All @@ -38,7 +37,9 @@ let select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8) =
let mask:u8 = Core.Num.impl__u8__wrapping_sub (is_non_zero selector <: u8) 1uy in
let out:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in
let out:t_Array u8 (sz 32) =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE
}
Expand Down
21 changes: 9 additions & 12 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Hash_functions.fst
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,9 @@ let absorb (v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K) =
v_K
in
let data:t_Array (t_Slice u8) v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down Expand Up @@ -73,10 +72,9 @@ let squeeze_block (v_K: usize) (xof_state: Libcrux.Digest.Incremental_x4.t_Shake
Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy (sz 168) <: t_Array u8 (sz 168)) v_K
in
let out:t_Array (t_Array u8 (sz 168)) v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down Expand Up @@ -107,10 +105,9 @@ let squeeze_three_blocks (v_K: usize) (xof_state: Libcrux.Digest.Incremental_x4.
Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy (sz 504) <: t_Array u8 (sz 504)) v_K
in
let out:t_Array (t_Array u8 (sz 504)) v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down
106 changes: 62 additions & 44 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ let into_padded_array (v_LEN: usize) (slice: t_Slice u8) =
if true
then
let _:Prims.unit =
if ~.((Core.Slice.impl__len slice <: usize) <=. v_LEN <: bool)
if ~.((Core.Slice.impl__len #u8 slice <: usize) <=. v_LEN <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: slice.len() <= LEN"

Expand All @@ -20,12 +20,16 @@ let into_padded_array (v_LEN: usize) (slice: t_Slice u8) =
let out:t_Array u8 v_LEN = Rust_primitives.Hax.repeat 0uy v_LEN in
let out:t_Array u8 v_LEN =
Rust_primitives.Hax.Monomorphized_update_at.update_at_range out
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = Core.Slice.impl__len slice <: usize }
({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = Core.Slice.impl__len #u8 slice <: usize
}
<:
Core.Ops.Range.t_Range usize)
(Core.Slice.impl__copy_from_slice (out.[ {
(Core.Slice.impl__copy_from_slice #u8
(out.[ {
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = Core.Slice.impl__len slice <: usize
Core.Ops.Range.f_end = Core.Slice.impl__len #u8 slice <: usize
}
<:
Core.Ops.Range.t_Range usize ]
Expand All @@ -48,10 +52,9 @@ let sample_ring_element_cbd
let domain_separator, error_1_, prf_input:(u8 &
t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K &
t_Array u8 (sz 33)) =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down Expand Up @@ -105,10 +108,9 @@ let sample_vector_cbd_then_ntt
in
let domain_separator, prf_input, re_as_ntt:(u8 & t_Array u8 (sz 33) &
t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down Expand Up @@ -159,8 +161,13 @@ let compress_then_serialize_u
=
let out:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.repeat 0uy v_OUT_LEN in
let out:t_Array u8 v_OUT_LEN =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
(Core.Iter.Traits.Collect.f_into_iter input
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
(Core.Array.Iter.t_IntoIter Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K))
(Core.Iter.Traits.Iterator.f_enumerate #(Core.Array.Iter.t_IntoIter
Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
(Core.Iter.Traits.Collect.f_into_iter #(t_Array
Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
input
<:
Core.Array.Iter.t_IntoIter Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
<:
Expand All @@ -180,7 +187,8 @@ let compress_then_serialize_u
}
<:
Core.Ops.Range.t_Range usize)
(Core.Slice.impl__copy_from_slice (out.[ {
(Core.Slice.impl__copy_from_slice #u8
(out.[ {
Core.Ops.Range.f_start = i *! (v_OUT_LEN /! v_K <: usize) <: usize;
Core.Ops.Range.f_end
=
Expand Down Expand Up @@ -263,12 +271,11 @@ let encrypt_unpacked
let ciphertext:t_Array u8 v_CIPHERTEXT_SIZE =
Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from ciphertext
({ Core.Ops.Range.f_start = v_C1_LEN } <: Core.Ops.Range.t_RangeFrom usize)
(Core.Slice.impl__copy_from_slice (ciphertext.[ { Core.Ops.Range.f_start = v_C1_LEN }
<:
Core.Ops.Range.t_RangeFrom usize ]
(Core.Slice.impl__copy_from_slice #u8
(ciphertext.[ { Core.Ops.Range.f_start = v_C1_LEN } <: Core.Ops.Range.t_RangeFrom usize ]
<:
t_Slice u8)
(Core.Array.impl_23__as_slice v_C2_LEN c2 <: t_Slice u8)
(Core.Array.impl_23__as_slice #u8 v_C2_LEN c2 <: t_Slice u8)
<:
t_Slice u8)
in
Expand All @@ -282,8 +289,11 @@ let deserialize_then_decompress_u
Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
in
let u_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
(Core.Slice.impl__chunks_exact (Rust_primitives.unsize ciphertext <: t_Slice u8)
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
(Core.Slice.Iter.t_ChunksExact u8))
(Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_ChunksExact u8)
(Core.Slice.impl__chunks_exact #u8
(Rust_primitives.unsize ciphertext <: t_Slice u8)
((Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *!
v_U_COMPRESSION_FACTOR
<:
Expand Down Expand Up @@ -375,8 +385,11 @@ let deserialize_secret_key (v_K: usize) (secret_key: t_Slice u8) =
Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
in
let secret_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
(Core.Slice.impl__chunks_exact secret_key
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
(Core.Slice.Iter.t_ChunksExact u8))
(Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_ChunksExact u8)
(Core.Slice.impl__chunks_exact #u8
secret_key
Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT
<:
Core.Slice.Iter.t_ChunksExact u8)
Expand Down Expand Up @@ -423,8 +436,13 @@ let serialize_secret_key
=
let out:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.repeat 0uy v_OUT_LEN in
let out:t_Array u8 v_OUT_LEN =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
(Core.Iter.Traits.Collect.f_into_iter key
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
(Core.Array.Iter.t_IntoIter Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K))
(Core.Iter.Traits.Iterator.f_enumerate #(Core.Array.Iter.t_IntoIter
Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
(Core.Iter.Traits.Collect.f_into_iter #(t_Array
Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
key
<:
Core.Array.Iter.t_IntoIter Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
<:
Expand All @@ -450,7 +468,8 @@ let serialize_secret_key
}
<:
Core.Ops.Range.t_Range usize)
(Core.Slice.impl__copy_from_slice (out.[ {
(Core.Slice.impl__copy_from_slice #u8
(out.[ {
Core.Ops.Range.f_start
=
i *! Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT <: usize;
Expand Down Expand Up @@ -490,7 +509,8 @@ let serialize_public_key
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_RANKED_BYTES_PER_RING_ELEMENT }
<:
Core.Ops.Range.t_Range usize)
(Core.Slice.impl__copy_from_slice (public_key_serialized.[ {
(Core.Slice.impl__copy_from_slice #u8
(public_key_serialized.[ {
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_RANKED_BYTES_PER_RING_ELEMENT
}
Expand All @@ -513,9 +533,8 @@ let serialize_public_key
({ Core.Ops.Range.f_start = v_RANKED_BYTES_PER_RING_ELEMENT }
<:
Core.Ops.Range.t_RangeFrom usize)
(Core.Slice.impl__copy_from_slice (public_key_serialized.[ {
Core.Ops.Range.f_start = v_RANKED_BYTES_PER_RING_ELEMENT
}
(Core.Slice.impl__copy_from_slice #u8
(public_key_serialized.[ { Core.Ops.Range.f_start = v_RANKED_BYTES_PER_RING_ELEMENT }
<:
Core.Ops.Range.t_RangeFrom usize ]
<:
Expand All @@ -532,7 +551,7 @@ let generate_keypair_unpacked
=
let hashed:t_Array u8 (sz 64) = Libcrux.Kem.Kyber.Hash_functions.v_G key_generation_seed in
let seed_for_A, seed_for_secret_and_error:(t_Slice u8 & t_Slice u8) =
Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: t_Slice u8) (sz 32)
Core.Slice.impl__split_at #u8 (Rust_primitives.unsize hashed <: t_Slice u8) (sz 32)
in
let a_transpose:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
Libcrux.Kem.Kyber.Matrix.sample_matrix_A v_K
Expand All @@ -558,10 +577,9 @@ let generate_keypair_unpacked
in
let secret_as_ntt, tt_as_ntt:(t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K &
t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand All @@ -577,7 +595,9 @@ let generate_keypair_unpacked
temp_0_
in
let i:usize = i in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end
=
Expand Down Expand Up @@ -670,10 +690,9 @@ let generate_keypair_unpacked
a_transpose
in
let a_matrix:t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand All @@ -685,10 +704,9 @@ let generate_keypair_unpacked
a_matrix
in
let i:usize = i in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_K }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down
Loading

0 comments on commit 901dec8

Please sign in to comment.