diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst index d7917df15..d54a96e87 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst @@ -1,5 +1,5 @@ module Chacha20.Hacspec_helper -#set-options "--fuel 0 --ifuel 1 --z3rlimit 30" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -15,7 +15,9 @@ let add_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = Core.Ops.Range.t_Range usize) state (fun state i -> - Rust_primitives.Hax.update_at state + let state:t_Array u32 (sz 16) = state in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state i (Core.Num.impl__u32__wrapping_add (state.[ i ] <: u32) (other.[ i ] <: u32) <: u32) <: @@ -23,95 +25,6 @@ let add_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = in state -let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (sz 16) = - let out:t_Array u32 (sz 16) = Rust_primitives.Hax.repeat 0ul (sz 16) in - let out:t_Array u32 (sz 16) = - 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 = sz 16 - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) - out - (fun out i -> - Rust_primitives.Hax.update_at out - i - (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[ - { - Core.Ops.Range.f_start = sz 4 *! i <: usize; - Core.Ops.Range.f_end = (sz 4 *! i <: usize) +! sz 4 <: usize - } - <: - Core.Ops.Range.t_Range usize ] - <: - t_Slice u8) - <: - Core.Result.t_Result (t_Array u8 (sz 4)) Core.Array.t_TryFromSliceError) - <: - t_Array u8 (sz 4)) - <: - u32) - <: - t_Array u32 (sz 16)) - in - out - -let u32s_to_le_bytes (state: t_Array u32 (sz 16)) : t_Array u8 (sz 64) = - let out:t_Array u8 (sz 64) = Rust_primitives.Hax.repeat 0uy (sz 64) in - let out:t_Array u8 (sz 64) = - 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 - = - Core.Slice.impl__len (Rust_primitives.unsize state <: t_Slice u32) <: usize - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) - out - (fun out i -> - let tmp:t_Array u8 (sz 4) = Core.Num.impl__u32__to_le_bytes (state.[ i ] <: u32) 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 = sz 4 - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) - out - (fun out j -> - Rust_primitives.Hax.update_at out - ((i *! sz 4 <: usize) +! j <: usize) - (tmp.[ j ] <: u8) - <: - t_Array u8 (sz 64))) - in - out - -let xor_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = - let state:t_Array u32 (sz 16) = - 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 = sz 16 - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) - state - (fun state i -> - Rust_primitives.Hax.update_at state - i - ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32) - <: - t_Array u32 (sz 16)) - in - state - let update_array (array: t_Array u8 (sz 64)) (v_val: t_Slice u8) : t_Array u8 (sz 64) = let _:Prims.unit = if ~.(sz 64 >=. (Core.Slice.impl__len v_val <: usize) <: bool) @@ -131,7 +44,11 @@ let update_array (array: t_Array u8 (sz 64)) (v_val: t_Slice u8) : t_Array u8 (s Core.Ops.Range.t_Range usize) array (fun array i -> - Rust_primitives.Hax.update_at array i (v_val.[ i ] <: u8) <: t_Array u8 (sz 64)) + let array:t_Array u8 (sz 64) = array in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array i (v_val.[ i ] <: u8) + <: + t_Array u8 (sz 64)) in array @@ -149,7 +66,7 @@ let xor_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = (fun state i -> let state:t_Array u32 (sz 16) = state in let i:usize = i in - Rust_primitives.Hax.update_at state + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state i ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32) <: @@ -172,7 +89,7 @@ let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (sz 16) = (fun out i -> let out:t_Array u32 (sz 16) = out in let i:usize = i in - Rust_primitives.Hax.update_at out + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[ { @@ -207,7 +124,9 @@ let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (sz 3) = Core.Ops.Range.t_Range usize) out (fun out i -> - Rust_primitives.Hax.update_at out + let out:t_Array u32 (sz 3) = out in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[ { @@ -242,7 +161,9 @@ let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (sz 8) = Core.Ops.Range.t_Range usize) out (fun out i -> - Rust_primitives.Hax.update_at out + let out:t_Array u32 (sz 8) = out in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[ { @@ -294,7 +215,7 @@ let u32s_to_le_bytes (state: t_Array u32 (sz 16)) : t_Array u8 (sz 64) = (fun out j -> let out:t_Array u8 (sz 64) = out in let j:usize = j in - Rust_primitives.Hax.update_at out + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out ((i *! sz 4 <: usize) +! j <: usize) (tmp.[ j ] <: u8) <: diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst index e061195e1..311945991 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst @@ -1,5 +1,5 @@ module Chacha20 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 30" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -21,15 +21,17 @@ let chacha20_line (a b d: usize) (s: u32) (m: t_Array u32 (sz 16)) (fun _ -> Prims.l_True) = let state:t_Array u32 (sz 16) = m in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state a (Core.Num.impl__u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32) in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state d ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32) + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state + d + ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32) in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state d (Core.Num.impl__u32__rotate_left (state.[ d ] <: u32) s <: u32) in @@ -66,14 +68,17 @@ let chacha20_rounds (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = <: Core.Ops.Range.t_Range i32) st - (fun st v__i -> chacha20_double_round st <: t_Array u32 (sz 16)) + (fun st v__i -> + let st:t_Array u32 (sz 16) = st in + let v__i:i32 = v__i in + chacha20_double_round st <: t_Array u32 (sz 16)) in st let chacha20_core (ctr: u32) (st0: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = let state:t_Array u32 (sz 16) = st0 in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state (sz 12) (Core.Num.impl__u32__wrapping_add (state.[ sz 12 ] <: u32) ctr <: u32) in @@ -147,6 +152,8 @@ let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8) Core.Ops.Range.t_Range usize) blocks_out (fun blocks_out i -> + let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = blocks_out in + let i:usize = i in let b:t_Array u8 (sz 64) = chacha20_encrypt_block st0 (cast (i <: usize) <: u32)