Skip to content

Commit

Permalink
fix(examples/chacha20): regenerate, eliminate duplicated function
Browse files Browse the repository at this point in the history
  • Loading branch information
@W95Psp
W95Psp committed Dec 7, 2023
1 parent fea5dbc commit 1353926
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 103 deletions.
115 changes: 18 additions & 97 deletions examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst
View file
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -15,103 +15,16 @@ 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)
<:
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)
Expand All @@ -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

Expand All @@ -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)
<:
Expand All @@ -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.[
{
Expand Down Expand Up @@ -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.[
{
Expand Down Expand Up @@ -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.[
{
Expand Down Expand Up @@ -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)
<:
Expand Down
19 changes: 13 additions & 6 deletions examples/chacha20/proofs/fstar/extraction/Chacha20.fst
View file
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 1353926

Please sign in to comment.