From 0a3cac4c2f91745d70a16e5621e686c16ff95a7f Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Fri, 17 Jan 2025 17:23:12 +0100 Subject: [PATCH] fixed examples --- engine/backends/fstar/fstar_backend.ml | 79 ++-- examples/Cargo.lock | 11 +- .../extraction/Chacha20.Hacspec_helper.fst | 235 +++++----- .../proofs/fstar/extraction/Chacha20.fst | 296 ++++++------ .../proofs/fstar/extraction/Lob_backend.fst | 63 ++- examples/proverif-psk/src/lib.rs | 4 +- .../sha256/proofs/fstar/extraction/Sha256.fst | 433 +++++++++--------- .../Rust_primitives.Integers.fsti | 14 +- 8 files changed, 601 insertions(+), 534 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7ca56bcb6..757b8997f 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -152,53 +152,60 @@ struct let pnegative = function true -> "-" | false -> "" - let rec pliteral span (e : literal) = + (* Print a literal as an F* constant *) + let rec pliteral_as_const span (e : literal) = match e with | String s -> F.Const.Const_string (s, F.dummyRange) | Char c -> F.Const.Const_char (Char.to_int c) | Int { value; kind = { size; signedness }; negative } -> - let open F.Const in - let size = - match size with - | S8 -> Int8 - | S16 -> Int16 - | S32 -> Int32 - | S64 -> Int64 - | S128 -> - Error.unimplemented ~issue_id:464 - ~details: - "Matching on u128 or i128 literals is not yet supported." span - | SSize -> - Error.unimplemented ~issue_id:464 - ~details: - "Matching on usize or isize literals is not yet supported. \ - As a work-around, instead of `match expr { 0 => ... }`, \ - please cast for instance to `u64` before: `match expr as \ - u64 { 0 => ... }`." - span + Error.unimplemented + ~details:"Integers cannot be printed as constants, they can only be printed as expressions." span + | Float _ -> + Error.unimplemented + ~details:"Floats cannot be printed as constants, they can only be printed as expressions." span + | Bool b -> F.Const.Const_bool b + + (* Print a literal appearing in a pattern as an F* pattern *) + let rec pliteral_as_pat span (e : literal) = + match e with + | Int { value; kind = { size; signedness }; negative } -> + let pat_name = + F.pat @@ F.AST.PatName (F.lid [ "Rust_primitives"; "Integers"; "MkInt" ]) in - F.Const.Const_int - ( pnegative negative ^ value, - Some - ( (match signedness with Signed -> Signed | Unsigned -> Unsigned), - size ) ) + let mk_const c = F.AST.PatConst c |> F.pat in + let mk_int value negative = mk_const (F.Const.Const_int (pnegative negative ^ value, None)) + in + F.pat_app pat_name + @@ + [mk_int value negative] | Float _ -> Error.unimplemented ~issue_id:464 - ~details:"Matching on f32 or f64 literals is not yet supported." span - | Bool b -> F.Const.Const_bool b + ~details:"Pattern matching on floats is not yet supported." span + | _ -> F.pat @@ F.AST.PatConst (pliteral_as_const span e) let pliteral_as_expr span (e : literal) = let mk_const c = F.AST.Const c |> F.term in - let mk_nat value negative = + let mk_int value negative = mk_const (F.Const.Const_int (pnegative negative ^ value, None)) in - let wrap_app fn x n = F.mk_e_app (F.term_of_lid [ fn ]) [ mk_nat x n ] in match e with - | Int { value; kind = { size = SSize; signedness = sn }; negative = n } -> - wrap_app (match sn with Signed -> "isz" | Unsigned -> "sz") value n - | Int { value; kind = { size = S128; signedness = sn }; negative } -> - let prefix = match sn with Signed -> "i" | Unsigned -> "u" in - wrap_app ("pub_" ^ prefix ^ "128") value negative + | Int { value; kind = { size; signedness }; negative = n } -> + let f = + match (size, signedness) with + | S8, Signed -> F.lid ["mk_i8"] + | S16, Signed -> F.lid ["mk_i16"] + | S32, Signed -> F.lid ["mk_i32"] + | S64, Signed -> F.lid ["mk_i64"] + | S128, Signed -> F.lid ["mk_i128"] + | SSize, Signed -> F.lid ["mk_isize"] + | S8, Unsigned -> F.lid ["mk_u8"] + | S16, Unsigned -> F.lid ["mk_u16"] + | S32, Unsigned -> F.lid ["mk_u32"] + | S64, Unsigned -> F.lid ["mk_u64"] + | S128, Unsigned -> F.lid ["mk_u128"] + | SSize, Unsigned -> F.lid ["mk_usize"] + in + F.mk_e_app (F.term @@ F.AST.Name f) [ mk_int value n ] | Float { value; negative; _ } -> F.mk_e_app (F.term_of_lid [ "mk_float" ]) @@ -206,7 +213,7 @@ struct mk_const (F.Const.Const_string (pnegative negative ^ value, F.dummyRange)); ] - | _ -> mk_const @@ pliteral span e + | _ -> mk_const @@ pliteral_as_const span e let pconcrete_ident (id : concrete_ident) = let id = U.Concrete_ident_view.to_view id in @@ -458,7 +465,7 @@ struct @@ if is_record then [ pat_rec () ] else List.map ~f:(fun { field; pat } -> ppat pat) fields - | PConstant { lit } -> F.pat @@ F.AST.PatConst (pliteral p.span lit) + | PConstant { lit } -> pliteral_as_pat p.span lit | _ -> . and pfield_pat ({ field; pat } : field_pat) = diff --git a/examples/Cargo.lock b/examples/Cargo.lock index af90ddc48..d0f1ab5b7 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -248,7 +248,7 @@ checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156" [[package]] name = "hax-bounded-integers" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "duplicate", "hax-lib", @@ -257,7 +257,7 @@ dependencies = [ [[package]] name = "hax-lib" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "hax-lib-macros", "num-bigint", @@ -266,7 +266,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "hax-lib-macros-types", "paste", @@ -278,7 +278,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "proc-macro2", "quote", @@ -385,7 +385,6 @@ name = "kyber_compress" version = "0.1.0" dependencies = [ "hax-lib", - "hax-lib-macros", ] [[package]] @@ -733,7 +732,7 @@ dependencies = [ name = "sha256" version = "0.1.0" dependencies = [ - "hax-lib-macros", + "hax-lib", ] [[package]] diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst index d7e0ee997..21d11370e 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst @@ -1,231 +1,220 @@ module Chacha20.Hacspec_helper -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 40" open Core open FStar.Mul -let add_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.t_Range - usize) - ({ 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) +let add_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 16) + (fun state temp_1_ -> + let state:t_Array u32 (mk_usize 16) = state in + let _:usize = temp_1_ in + true) state (fun state i -> - let state:t_Array u32 (sz 16) = state in + let state:t_Array u32 (mk_usize 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)) + t_Array u32 (mk_usize 16)) in state -let update_array (array: t_Array u8 (sz 64)) (v_val: t_Slice u8) : t_Array u8 (sz 64) = +let update_array (array: t_Array u8 (mk_usize 64)) (v_val: t_Slice u8) : t_Array u8 (mk_usize 64) = let _:Prims.unit = - if ~.(sz 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool) - then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: 64 >= val.len()" - <: - Rust_primitives.Hax.t_Never) + Hax_lib.v_assert (mk_usize 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool) in - let array:t_Array u8 (sz 64) = - 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 #u8 v_val <: usize - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + let array:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (Core.Slice.impl__len #u8 v_val <: usize) + (fun array temp_1_ -> + let array:t_Array u8 (mk_usize 64) = array in + let _:usize = temp_1_ in + true) array (fun array i -> - let array:t_Array u8 (sz 64) = array in + let array:t_Array u8 (mk_usize 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)) + t_Array u8 (mk_usize 64)) in array -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.t_Range - usize) - ({ 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) +let xor_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 16) + (fun state temp_1_ -> + let state:t_Array u32 (mk_usize 16) = state in + let _:usize = temp_1_ in + true) state (fun state i -> - let state:t_Array u32 (sz 16) = state in + let state:t_Array u32 (mk_usize 16) = state in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state i ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32) <: - t_Array u32 (sz 16)) + t_Array u32 (mk_usize 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.t_Range - usize) - ({ 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) +let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) = + let out:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 16) in + let out:t_Array u32 (mk_usize 16) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 16) + (fun out temp_1_ -> + let out:t_Array u32 (mk_usize 16) = out in + let _:usize = temp_1_ in + true) out (fun out i -> - let out:t_Array u32 (sz 16) = out in + let out:t_Array u32 (mk_usize 16) = 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 #(t_Array u8 (sz 4)) + (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) - #(t_Array u8 (sz 4)) + #(t_Array u8 (mk_usize 4)) + #FStar.Tactics.Typeclasses.solve (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.f_start = mk_usize 4 *! i <: usize; + Core.Ops.Range.f_end + = + (mk_usize 4 *! i <: usize) +! mk_usize 4 <: usize } <: Core.Ops.Range.t_Range usize ] <: t_Slice u8) <: - Core.Result.t_Result (t_Array u8 (sz 4)) Core.Array.t_TryFromSliceError) + Core.Result.t_Result (t_Array u8 (mk_usize 4)) Core.Array.t_TryFromSliceError) <: - t_Array u8 (sz 4)) + t_Array u8 (mk_usize 4)) <: u32) <: - t_Array u32 (sz 16)) + t_Array u32 (mk_usize 16)) in out -let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (sz 3) = - let out:t_Array u32 (sz 3) = Rust_primitives.Hax.repeat 0ul (sz 3) in - let out:t_Array u32 (sz 3) = - 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 = sz 3 } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) +let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) = + let out:t_Array u32 (mk_usize 3) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 3) in + let out:t_Array u32 (mk_usize 3) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 3) + (fun out temp_1_ -> + let out:t_Array u32 (mk_usize 3) = out in + let _:usize = temp_1_ in + true) out (fun out i -> - let out:t_Array u32 (sz 3) = out in + let out:t_Array u32 (mk_usize 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 #(t_Array u8 (sz 4)) + (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) - #(t_Array u8 (sz 4)) + #(t_Array u8 (mk_usize 4)) + #FStar.Tactics.Typeclasses.solve (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.f_start = mk_usize 4 *! i <: usize; + Core.Ops.Range.f_end + = + (mk_usize 4 *! i <: usize) +! mk_usize 4 <: usize } <: Core.Ops.Range.t_Range usize ] <: t_Slice u8) <: - Core.Result.t_Result (t_Array u8 (sz 4)) Core.Array.t_TryFromSliceError) + Core.Result.t_Result (t_Array u8 (mk_usize 4)) Core.Array.t_TryFromSliceError) <: - t_Array u8 (sz 4)) + t_Array u8 (mk_usize 4)) <: u32) <: - t_Array u32 (sz 3)) + t_Array u32 (mk_usize 3)) in out -let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (sz 8) = - let out:t_Array u32 (sz 8) = Rust_primitives.Hax.repeat 0ul (sz 8) in - let out:t_Array u32 (sz 8) = - 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 = sz 8 } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) +let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) = + let out:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 8) in + let out:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 8) + (fun out temp_1_ -> + let out:t_Array u32 (mk_usize 8) = out in + let _:usize = temp_1_ in + true) out (fun out i -> - let out:t_Array u32 (sz 8) = out in + let out:t_Array u32 (mk_usize 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 #(t_Array u8 (sz 4)) + (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) - #(t_Array u8 (sz 4)) + #(t_Array u8 (mk_usize 4)) + #FStar.Tactics.Typeclasses.solve (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.f_start = mk_usize 4 *! i <: usize; + Core.Ops.Range.f_end + = + (mk_usize 4 *! i <: usize) +! mk_usize 4 <: usize } <: Core.Ops.Range.t_Range usize ] <: t_Slice u8) <: - Core.Result.t_Result (t_Array u8 (sz 4)) Core.Array.t_TryFromSliceError) + Core.Result.t_Result (t_Array u8 (mk_usize 4)) Core.Array.t_TryFromSliceError) <: - t_Array u8 (sz 4)) + t_Array u8 (mk_usize 4)) <: u32) <: - t_Array u32 (sz 8)) + t_Array u32 (mk_usize 8)) 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.t_Range - usize) - ({ - Core.Ops.Range.f_start = sz 0; - Core.Ops.Range.f_end - = - Core.Slice.impl__len #u32 (Rust_primitives.unsize state <: t_Slice u32) <: usize - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) +let u32s_to_le_bytes (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 64) = + let out:t_Array u8 (mk_usize 64) = Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 64) in + let out:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (Core.Slice.impl__len #u32 (state <: t_Slice u32) <: usize) + (fun out temp_1_ -> + let out:t_Array u8 (mk_usize 64) = out in + let _:usize = temp_1_ in + true) out (fun out i -> - let out:t_Array u8 (sz 64) = out in + let out:t_Array u8 (mk_usize 64) = out in let i:usize = i in - 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.t_Range - usize) - ({ 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) + let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl__u32__to_le_bytes (state.[ i ] <: u32) in + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 4) + (fun out temp_1_ -> + let out:t_Array u8 (mk_usize 64) = out in + let _:usize = temp_1_ in + true) out (fun out j -> - let out:t_Array u8 (sz 64) = out in + let out:t_Array u8 (mk_usize 64) = out in let j:usize = j in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out - ((i *! sz 4 <: usize) +! j <: usize) + ((i *! mk_usize 4 <: usize) +! j <: usize) (tmp.[ j ] <: u8) <: - t_Array u8 (sz 64))) + t_Array u8 (mk_usize 64))) in out diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst index d9a7bb02a..f21b19a52 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst @@ -1,38 +1,29 @@ module Chacha20 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 40" open Core open FStar.Mul -unfold -let t_Block = t_Array u8 (sz 64) - -unfold -let t_ChaChaIV = t_Array u8 (sz 12) - -unfold -let t_ChaChaKey = t_Array u8 (sz 32) - -unfold -let t_State = t_Array u32 (sz 16) - -unfold -let t_StateIdx = Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15) +let _ = + (* This module has implicit dependencies, here we make them explicit. *) + (* The implicit dependencies arise from typeclasses instances. *) + let open Hax_bounded_integers in + () let chacha20_line - (a b d: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + (a b d: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) (s: u32) - (m: t_Array u32 (sz 16)) - : t_Array u32 (sz 16) = - let state:t_Array u32 (sz 16) = m in - let state:t_Array u32 (sz 16) = + (m: t_Array u32 (mk_usize 16)) + : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = m in + let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.update_at state a (Core.Num.impl__u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32) in - let state:t_Array u32 (sz 16) = + let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.update_at state d ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32) in - let state:t_Array u32 (sz 16) = + let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.update_at state d (Core.Num.impl__u32__rotate_left (state.[ d ] <: u32) s <: u32) @@ -40,116 +31,137 @@ let chacha20_line state let chacha20_quarter_round - (a b c d: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (state: t_Array u32 (sz 16)) - : t_Array u32 (sz 16) = - let state:t_Array u32 (sz 16) = chacha20_line a b d 16ul state in - let state:t_Array u32 (sz 16) = chacha20_line c d b 12ul state in - let state:t_Array u32 (sz 16) = chacha20_line a b d 8ul state in - chacha20_line c d b 7ul state + (a b c d: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (state: t_Array u32 (mk_usize 16)) + : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = chacha20_line a b d (mk_u32 16) state in + let state:t_Array u32 (mk_usize 16) = chacha20_line c d b (mk_u32 12) state in + let state:t_Array u32 (mk_usize 16) = chacha20_line a b d (mk_u32 8) state in + chacha20_line c d b (mk_u32 7) state -let chacha20_double_round (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 0 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 4 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 8 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 12 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) +let chacha20_double_round (state: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 0 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 4 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 8 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 12 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 1 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 5 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 9 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 13 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 1 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 5 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 9 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 13 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 2 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 6 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 10 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 14 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 2 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 6 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 10 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 14 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 3 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 7 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 11 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 15 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 3 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 7 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 11 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 15 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 0 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 5 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 10 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 15 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 0 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 5 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 10 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 15 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 1 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 6 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 11 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 12 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 1 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 6 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 11 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 12 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 2 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 7 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 8 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 13 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + let state:t_Array u32 (mk_usize 16) = + chacha20_quarter_round (mk_usize 2 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 7 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 8 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 13 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state in - chacha20_quarter_round (sz 3 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 4 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 9 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 14 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) + chacha20_quarter_round (mk_usize 3 + <: + Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 4 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 9 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) + (mk_usize 14 <: Hax_bounded_integers.t_BoundedUsize (mk_usize 0) (mk_usize 15)) state -let chacha20_rounds (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = - let st:t_Array u32 (sz 16) = state in - let st:t_Array u32 (sz 16) = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range - i32) - ({ Core.Ops.Range.f_start = 0l; Core.Ops.Range.f_end = 10l } <: Core.Ops.Range.t_Range i32 - ) - <: - Core.Ops.Range.t_Range i32) +let chacha20_rounds (state: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let st:t_Array u32 (mk_usize 16) = state in + let st:t_Array u32 (mk_usize 16) = + Rust_primitives.Hax.Folds.fold_range (mk_i32 0) + (mk_i32 10) + (fun st temp_1_ -> + let st:t_Array u32 (mk_usize 16) = st in + let _:i32 = temp_1_ in + true) st (fun st v__i -> - let st:t_Array u32 (sz 16) = st in + let st:t_Array u32 (mk_usize 16) = st in let v__i:i32 = v__i in - chacha20_double_round st <: t_Array u32 (sz 16)) + chacha20_double_round st <: t_Array u32 (mk_usize 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) = +let chacha20_core (ctr: u32) (st0: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = st0 in + let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state - (sz 12) - (Core.Num.impl__u32__wrapping_add (state.[ sz 12 ] <: u32) ctr <: u32) + (mk_usize 12) + (Core.Num.impl__u32__wrapping_add (state.[ mk_usize 12 ] <: u32) ctr <: u32) in - let k:t_Array u32 (sz 16) = chacha20_rounds state in + let k:t_Array u32 (mk_usize 16) = chacha20_rounds state in Chacha20.Hacspec_helper.add_state state k -let chacha20_encrypt_block (st0: t_Array u32 (sz 16)) (ctr: u32) (plain: t_Array u8 (sz 64)) - : t_Array u8 (sz 64) = - let st:t_Array u32 (sz 16) = chacha20_core ctr st0 in - let (pl: t_Array u32 (sz 16)):t_Array u32 (sz 16) = - Chacha20.Hacspec_helper.to_le_u32s_16_ (Rust_primitives.unsize plain <: t_Slice u8) +let chacha20_encrypt_block + (st0: t_Array u32 (mk_usize 16)) + (ctr: u32) + (plain: t_Array u8 (mk_usize 64)) + : t_Array u8 (mk_usize 64) = + let st:t_Array u32 (mk_usize 16) = chacha20_core ctr st0 in + let (pl: t_Array u32 (mk_usize 16)):t_Array u32 (mk_usize 16) = + Chacha20.Hacspec_helper.to_le_u32s_16_ (plain <: t_Slice u8) in - let encrypted:t_Array u32 (sz 16) = Chacha20.Hacspec_helper.xor_state st pl in + let encrypted:t_Array u32 (mk_usize 16) = Chacha20.Hacspec_helper.xor_state st pl in Chacha20.Hacspec_helper.u32s_to_le_bytes encrypted -let chacha20_encrypt_last (st0: t_Array u32 (sz 16)) (ctr: u32) (plain: t_Slice u8) +let chacha20_encrypt_last (st0: t_Array u32 (mk_usize 16)) (ctr: u32) (plain: t_Slice u8) : Prims.Pure (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (requires (Core.Slice.impl__len #u8 plain <: usize) <=. sz 64) + (requires (Core.Slice.impl__len #u8 plain <: usize) <=. mk_usize 64) (fun _ -> Prims.l_True) = - let (b: t_Array u8 (sz 64)):t_Array u8 (sz 64) = Rust_primitives.Hax.repeat 0uy (sz 64) in - let b:t_Array u8 (sz 64) = Chacha20.Hacspec_helper.update_array b plain in - let b:t_Array u8 (sz 64) = chacha20_encrypt_block st0 ctr b in + let (b: t_Array u8 (mk_usize 64)):t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 64) + in + let b:t_Array u8 (mk_usize 64) = Chacha20.Hacspec_helper.update_array b plain in + let b:t_Array u8 (mk_usize 64) = chacha20_encrypt_block st0 ctr b in Alloc.Slice.impl__to_vec #u8 (b.[ { - Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_start = mk_usize 0; Core.Ops.Range.f_end = Core.Slice.impl__len #u8 plain <: usize } <: @@ -157,72 +169,76 @@ let chacha20_encrypt_last (st0: t_Array u32 (sz 16)) (ctr: u32) (plain: t_Slice <: t_Slice u8) -let chacha20_init (key: t_Array u8 (sz 32)) (iv: t_Array u8 (sz 12)) (ctr: u32) - : t_Array u32 (sz 16) = - let (key_u32: t_Array u32 (sz 8)):t_Array u32 (sz 8) = - Chacha20.Hacspec_helper.to_le_u32s_8_ (Rust_primitives.unsize key <: t_Slice u8) +let chacha20_init (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) (ctr: u32) + : t_Array u32 (mk_usize 16) = + let (key_u32: t_Array u32 (mk_usize 8)):t_Array u32 (mk_usize 8) = + Chacha20.Hacspec_helper.to_le_u32s_8_ (key <: t_Slice u8) in - let (iv_u32: t_Array u32 (sz 3)):t_Array u32 (sz 3) = - Chacha20.Hacspec_helper.to_le_u32s_3_ (Rust_primitives.unsize iv <: t_Slice u8) + let (iv_u32: t_Array u32 (mk_usize 3)):t_Array u32 (mk_usize 3) = + Chacha20.Hacspec_helper.to_le_u32s_3_ (iv <: t_Slice u8) in let list = [ - 1634760805ul; 857760878ul; 2036477234ul; 1797285236ul; key_u32.[ sz 0 ]; key_u32.[ sz 1 ]; - key_u32.[ sz 2 ]; key_u32.[ sz 3 ]; key_u32.[ sz 4 ]; key_u32.[ sz 5 ]; key_u32.[ sz 6 ]; - key_u32.[ sz 7 ]; ctr; iv_u32.[ sz 0 ]; iv_u32.[ sz 1 ]; iv_u32.[ sz 2 ] + mk_u32 1634760805; mk_u32 857760878; mk_u32 2036477234; mk_u32 1797285236; + key_u32.[ mk_usize 0 ]; key_u32.[ mk_usize 1 ]; key_u32.[ mk_usize 2 ]; key_u32.[ mk_usize 3 ]; + key_u32.[ mk_usize 4 ]; key_u32.[ mk_usize 5 ]; key_u32.[ mk_usize 6 ]; key_u32.[ mk_usize 7 ]; + ctr; iv_u32.[ mk_usize 0 ]; iv_u32.[ mk_usize 1 ]; iv_u32.[ mk_usize 2 ] ] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16); Rust_primitives.Hax.array_of_list 16 list -let chacha20_key_block (state: t_Array u32 (sz 16)) : t_Array u8 (sz 64) = - let state:t_Array u32 (sz 16) = chacha20_core 0ul state in +let chacha20_key_block (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 64) = + let state:t_Array u32 (mk_usize 16) = chacha20_core (mk_u32 0) state in Chacha20.Hacspec_helper.u32s_to_le_bytes state -let chacha20_key_block0 (key: t_Array u8 (sz 32)) (iv: t_Array u8 (sz 12)) : t_Array u8 (sz 64) = - let state:t_Array u32 (sz 16) = chacha20_init key iv 0ul in +let chacha20_key_block0 (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) + : t_Array u8 (mk_usize 64) = + let state:t_Array u32 (mk_usize 16) = chacha20_init key iv (mk_u32 0) in chacha20_key_block state -let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8) +let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in - let num_blocks:usize = (Core.Slice.impl__len #u8 m <: usize) /! sz 64 in - let remainder_len:usize = (Core.Slice.impl__len #u8 m <: usize) %! sz 64 in + let num_blocks:usize = (Core.Slice.impl__len #u8 m <: usize) /! mk_usize 64 in + let remainder_len:usize = (Core.Slice.impl__len #u8 m <: usize) %! mk_usize 64 in let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - 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 = num_blocks } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + num_blocks + (fun blocks_out temp_1_ -> + let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = blocks_out in + let _:usize = temp_1_ in + true) 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) = + let b:t_Array u8 (mk_usize 64) = chacha20_encrypt_block st0 (cast (i <: usize) <: u32) - (Core.Result.impl__unwrap #(t_Array u8 (sz 64)) + (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 64)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) - #(t_Array u8 (sz 64)) + #(t_Array u8 (mk_usize 64)) + #FStar.Tactics.Typeclasses.solve (m.[ { - Core.Ops.Range.f_start = sz 64 *! i <: usize; - Core.Ops.Range.f_end = (sz 64 *! i <: usize) +! sz 64 <: usize + Core.Ops.Range.f_start = mk_usize 64 *! i <: usize; + Core.Ops.Range.f_end + = + (mk_usize 64 *! i <: usize) +! mk_usize 64 <: usize } <: Core.Ops.Range.t_Range usize ] <: t_Slice u8) <: - Core.Result.t_Result (t_Array u8 (sz 64)) Core.Array.t_TryFromSliceError) + Core.Result.t_Result (t_Array u8 (mk_usize 64)) Core.Array.t_TryFromSliceError) <: - t_Array u8 (sz 64)) + t_Array u8 (mk_usize 64)) in let _:Prims.unit = Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =. - (i *! sz 64 <: usize) + (i *! mk_usize 64 <: usize) <: bool) in @@ -230,24 +246,24 @@ let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8) Alloc.Vec.impl_2__extend_from_slice #u8 #Alloc.Alloc.t_Global blocks_out - (Rust_primitives.unsize b <: t_Slice u8) + (b <: t_Slice u8) in blocks_out) in let _:Prims.unit = Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =. - (num_blocks *! sz 64 <: usize) + (num_blocks *! mk_usize 64 <: usize) <: bool) in let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - if remainder_len <>. sz 0 + if remainder_len <>. mk_usize 0 then let b:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = chacha20_encrypt_last st0 (cast (num_blocks <: usize) <: u32) (m.[ { - Core.Ops.Range.f_start = sz 64 *! num_blocks <: usize; + Core.Ops.Range.f_start = mk_usize 64 *! num_blocks <: usize; Core.Ops.Range.f_end = Core.Slice.impl__len #u8 m <: usize } <: @@ -259,14 +275,22 @@ let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8) Alloc.Vec.impl_2__extend_from_slice #u8 #Alloc.Alloc.t_Global blocks_out - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) b <: t_Slice u8) + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + b + <: + t_Slice u8) in blocks_out else blocks_out in blocks_out -let chacha20 (m: t_Slice u8) (key: t_Array u8 (sz 32)) (iv: t_Array u8 (sz 12)) (ctr: u32) +let chacha20 + (m: t_Slice u8) + (key: t_Array u8 (mk_usize 32)) + (iv: t_Array u8 (mk_usize 12)) + (ctr: u32) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let state:t_Array u32 (sz 16) = chacha20_init key iv ctr in + let state:t_Array u32 (mk_usize 16) = chacha20_init key iv ctr in chacha20_update state m diff --git a/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst b/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst index 110c7758b..40e6f5a59 100644 --- a/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst +++ b/examples/limited-order-book/proofs/fstar/extraction/Lob_backend.fst @@ -3,10 +3,6 @@ module Lob_backend open Core open FStar.Mul -type t_Side = - | Side_Buy : t_Side - | Side_Sell : t_Side - type t_Match = { f_bid_id:u64; f_ask_id:u64; @@ -14,6 +10,10 @@ type t_Match = { f_quantity:u64 } +type t_Side = + | Side_Buy : t_Side + | Side_Sell : t_Side + type t_Order = { f_id:u64; f_side:t_Side; @@ -21,8 +21,20 @@ type t_Order = { f_quantity:u64 } +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_7': Core.Cmp.t_PartialEq t_Side t_Side + +let impl_7 = impl_7' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_14': Core.Clone.t_Clone t_Order + +let impl_14 = impl_14' + let is_match (order other: t_Order) : bool = - order.f_quantity >. 0uL && other.f_quantity >. 0uL && order.f_side <>. other.f_side && + order.f_quantity >. mk_u64 0 && other.f_quantity >. mk_u64 0 && order.f_side <>. other.f_side && (order.f_side =. (Side_Buy <: t_Side) && order.f_price >=. other.f_price || order.f_side =. (Side_Sell <: t_Side) && order.f_price <=. other.f_price) @@ -58,20 +70,16 @@ let process_order let done, matches, order, other_side:(bool & Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & t_Order & Alloc.Collections.Binary_heap.t_BinaryHeap v_T Alloc.Alloc.t_Global) = - 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 1; - Core.Ops.Range.f_end - = - Alloc.Collections.Binary_heap.impl_11__len #v_T #Alloc.Alloc.t_Global other_side - <: - usize - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + Rust_primitives.Hax.Folds.fold_range (mk_usize 1) + (Alloc.Collections.Binary_heap.impl_11__len #v_T #Alloc.Alloc.t_Global other_side <: usize) + (fun temp_0_ temp_1_ -> + let done, matches, order, other_side:(bool & Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & + t_Order & + Alloc.Collections.Binary_heap.t_BinaryHeap v_T Alloc.Alloc.t_Global) = + temp_0_ + in + let _:usize = temp_1_ in + true) (done, matches, order, other_side <: (bool & Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & t_Order & @@ -95,7 +103,8 @@ let process_order let other:v_T = other in impl__Order__try_match (Core.Convert.f_into #v_T #t_Order - (Core.Clone.f_clone #v_T other <: v_T) + #FStar.Tactics.Typeclasses.solve + (Core.Clone.f_clone #v_T #FStar.Tactics.Typeclasses.solve other <: v_T) <: t_Order) order @@ -116,13 +125,16 @@ let process_order tmp0 in let (other: t_Order):t_Order = - Core.Convert.f_into #v_T #t_Order (Core.Option.impl__unwrap #v_T out <: v_T) + Core.Convert.f_into #v_T + #t_Order + #FStar.Tactics.Typeclasses.solve + (Core.Option.impl__unwrap #v_T out <: v_T) in let other:t_Order = { other with f_quantity = other.f_quantity -! m.f_quantity } <: t_Order in let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T Alloc.Alloc.t_Global = - if other.f_quantity >. 0uL + if other.f_quantity >. mk_u64 0 then let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T Alloc.Alloc.t_Global = @@ -131,7 +143,10 @@ let process_order other_side (Core.Convert.f_from #v_T #t_Order - (Core.Clone.f_clone #t_Order other <: t_Order) + #FStar.Tactics.Typeclasses.solve + (Core.Clone.f_clone #t_Order #FStar.Tactics.Typeclasses.solve other + <: + t_Order) <: v_T) in @@ -160,7 +175,7 @@ let process_order let hax_temp_output:(Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global & Core.Option.t_Option t_Order) = matches, - (if order.f_quantity >. 0uL + (if order.f_quantity >. mk_u64 0 then Core.Option.Option_Some order <: Core.Option.t_Option t_Order else Core.Option.Option_None <: Core.Option.t_Option t_Order) <: diff --git a/examples/proverif-psk/src/lib.rs b/examples/proverif-psk/src/lib.rs index 7ce191a69..27a18aa16 100644 --- a/examples/proverif-psk/src/lib.rs +++ b/examples/proverif-psk/src/lib.rs @@ -34,10 +34,10 @@ impl From for Error { } } -#[hax::opaque_type] +#[hax::opaque] pub struct Message(aead::Tag, Vec); -#[hax::opaque_type] +#[hax::opaque] pub struct KeyIv(libcrux::aead::Key, libcrux::aead::Iv); /* Wire formats */ diff --git a/examples/sha256/proofs/fstar/extraction/Sha256.fst b/examples/sha256/proofs/fstar/extraction/Sha256.fst index 4d2137688..835f8bf68 100644 --- a/examples/sha256/proofs/fstar/extraction/Sha256.fst +++ b/examples/sha256/proofs/fstar/extraction/Sha256.fst @@ -3,65 +3,58 @@ module Sha256 open Core open FStar.Mul -unfold -let t_Block = t_Array u8 (sz 64) +let v_BLOCK_SIZE: usize = mk_usize 64 -unfold -let t_Hash = t_Array u32 (sz 8) - -unfold -let t_OpTableType = t_Array u8 (sz 12) - -unfold -let t_RoundConstantsTable = t_Array u32 (sz 64) - -unfold -let t_Sha256Digest = t_Array u8 (sz 32) - -let v_BLOCK_SIZE: usize = sz 64 - -let v_HASH_INIT: t_Array u32 (sz 8) = +let v_HASH_INIT: t_Array u32 (mk_usize 8) = let list = [ - 1779033703ul; - 3144134277ul; - 1013904242ul; - 2773480762ul; - 1359893119ul; - 2600822924ul; - 528734635ul; - 1541459225ul + mk_u32 1779033703; + mk_u32 3144134277; + mk_u32 1013904242; + mk_u32 2773480762; + mk_u32 1359893119; + mk_u32 2600822924; + mk_u32 528734635; + mk_u32 1541459225 ] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8); Rust_primitives.Hax.array_of_list 8 list -let v_HASH_SIZE: usize = sz 256 /! sz 8 +let v_HASH_SIZE: usize = mk_usize 256 /! mk_usize 8 -let v_K_SIZE: usize = sz 64 +let v_K_SIZE: usize = mk_usize 64 -let v_K_TABLE: t_Array u32 (sz 64) = +let v_K_TABLE: t_Array u32 (mk_usize 64) = let list = [ - 1116352408ul; 1899447441ul; 3049323471ul; 3921009573ul; 961987163ul; 1508970993ul; - 2453635748ul; 2870763221ul; 3624381080ul; 310598401ul; 607225278ul; 1426881987ul; 1925078388ul; - 2162078206ul; 2614888103ul; 3248222580ul; 3835390401ul; 4022224774ul; 264347078ul; 604807628ul; - 770255983ul; 1249150122ul; 1555081692ul; 1996064986ul; 2554220882ul; 2821834349ul; - 2952996808ul; 3210313671ul; 3336571891ul; 3584528711ul; 113926993ul; 338241895ul; 666307205ul; - 773529912ul; 1294757372ul; 1396182291ul; 1695183700ul; 1986661051ul; 2177026350ul; - 2456956037ul; 2730485921ul; 2820302411ul; 3259730800ul; 3345764771ul; 3516065817ul; - 3600352804ul; 4094571909ul; 275423344ul; 430227734ul; 506948616ul; 659060556ul; 883997877ul; - 958139571ul; 1322822218ul; 1537002063ul; 1747873779ul; 1955562222ul; 2024104815ul; - 2227730452ul; 2361852424ul; 2428436474ul; 2756734187ul; 3204031479ul; 3329325298ul + mk_u32 1116352408; mk_u32 1899447441; mk_u32 3049323471; mk_u32 3921009573; mk_u32 961987163; + mk_u32 1508970993; mk_u32 2453635748; mk_u32 2870763221; mk_u32 3624381080; mk_u32 310598401; + mk_u32 607225278; mk_u32 1426881987; mk_u32 1925078388; mk_u32 2162078206; mk_u32 2614888103; + mk_u32 3248222580; mk_u32 3835390401; mk_u32 4022224774; mk_u32 264347078; mk_u32 604807628; + mk_u32 770255983; mk_u32 1249150122; mk_u32 1555081692; mk_u32 1996064986; mk_u32 2554220882; + mk_u32 2821834349; mk_u32 2952996808; mk_u32 3210313671; mk_u32 3336571891; mk_u32 3584528711; + mk_u32 113926993; mk_u32 338241895; mk_u32 666307205; mk_u32 773529912; mk_u32 1294757372; + mk_u32 1396182291; mk_u32 1695183700; mk_u32 1986661051; mk_u32 2177026350; mk_u32 2456956037; + mk_u32 2730485921; mk_u32 2820302411; mk_u32 3259730800; mk_u32 3345764771; mk_u32 3516065817; + mk_u32 3600352804; mk_u32 4094571909; mk_u32 275423344; mk_u32 430227734; mk_u32 506948616; + mk_u32 659060556; mk_u32 883997877; mk_u32 958139571; mk_u32 1322822218; mk_u32 1537002063; + mk_u32 1747873779; mk_u32 1955562222; mk_u32 2024104815; mk_u32 2227730452; mk_u32 2361852424; + mk_u32 2428436474; mk_u32 2756734187; mk_u32 3204031479; mk_u32 3329325298 ] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 64); Rust_primitives.Hax.array_of_list 64 list -let v_LEN_SIZE: usize = sz 8 +let v_LEN_SIZE: usize = mk_usize 8 -let v_OP_TABLE: t_Array u8 (sz 12) = - let list = [2uy; 13uy; 22uy; 6uy; 11uy; 25uy; 7uy; 18uy; 3uy; 17uy; 19uy; 10uy] in +let v_OP_TABLE: t_Array u8 (mk_usize 12) = + let list = + [ + mk_u8 2; mk_u8 13; mk_u8 22; mk_u8 6; mk_u8 11; mk_u8 25; mk_u8 7; mk_u8 18; mk_u8 3; mk_u8 17; + mk_u8 19; mk_u8 10 + ] + in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 12); Rust_primitives.Hax.array_of_list 12 list @@ -69,19 +62,32 @@ let ch (x y z: u32) : u32 = (x &. y <: u32) ^. ((~.x <: u32) &. z <: u32) let maj (x y z: u32) : u32 = (x &. y <: u32) ^. ((x &. z <: u32) ^. (y &. z <: u32) <: u32) -let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. sz 4) (fun _ -> Prims.l_True) = +let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. mk_usize 4) (fun _ -> Prims.l_True) = let (tmp: u32):u32 = Core.Num.impl__u32__rotate_right x - (Core.Convert.f_into #u8 #u32 (v_OP_TABLE.[ (sz 3 *! i <: usize) +! sz 2 <: usize ] <: u8) + (Core.Convert.f_into #u8 + #u32 + #FStar.Tactics.Typeclasses.solve + (v_OP_TABLE.[ (mk_usize 3 *! i <: usize) +! mk_usize 2 <: usize ] <: u8) <: u32) in let tmp:u32 = - if op =. sz 0 then x >>! (v_OP_TABLE.[ (sz 3 *! i <: usize) +! sz 2 <: usize ] <: u8) else tmp + if op =. mk_usize 0 + then x >>! (v_OP_TABLE.[ (mk_usize 3 *! i <: usize) +! mk_usize 2 <: usize ] <: u8) + else tmp + in + let rot_val_1_:u32 = + Core.Convert.f_into #u8 + #u32 + #FStar.Tactics.Typeclasses.solve + (v_OP_TABLE.[ mk_usize 3 *! i <: usize ] <: u8) in - let rot_val_1_:u32 = Core.Convert.f_into #u8 #u32 (v_OP_TABLE.[ sz 3 *! i <: usize ] <: u8) in let rot_val_2_:u32 = - Core.Convert.f_into #u8 #u32 (v_OP_TABLE.[ (sz 3 *! i <: usize) +! sz 1 <: usize ] <: u8) + Core.Convert.f_into #u8 + #u32 + #FStar.Tactics.Typeclasses.solve + (v_OP_TABLE.[ (mk_usize 3 *! i <: usize) +! mk_usize 1 <: usize ] <: u8) in ((Core.Num.impl__u32__rotate_right x rot_val_1_ <: u32) ^. (Core.Num.impl__u32__rotate_right x rot_val_2_ <: u32) @@ -89,31 +95,34 @@ let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. sz 4) (fun _ -> u32) ^. tmp -let shuffle (ws: t_Array u32 (sz 64)) (hashi: t_Array u32 (sz 8)) : t_Array u32 (sz 8) = - let h:t_Array u32 (sz 8) = hashi in - let h:t_Array u32 (sz 8) = - 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_SIZE } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) +let shuffle (ws: t_Array u32 (mk_usize 64)) (hashi: t_Array u32 (mk_usize 8)) + : t_Array u32 (mk_usize 8) = + let h:t_Array u32 (mk_usize 8) = hashi in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + v_K_SIZE + (fun h temp_1_ -> + let h:t_Array u32 (mk_usize 8) = h in + let _:usize = temp_1_ in + true) h (fun h i -> - let h:t_Array u32 (sz 8) = h in + let h:t_Array u32 (mk_usize 8) = h in let i:usize = i in - let a0:u32 = h.[ sz 0 ] in - let b0:u32 = h.[ sz 1 ] in - let c0:u32 = h.[ sz 2 ] in - let d0:u32 = h.[ sz 3 ] in - let e0:u32 = h.[ sz 4 ] in - let f0:u32 = h.[ sz 5 ] in - let g0:u32 = h.[ sz 6 ] in - let (h0: u32):u32 = h.[ sz 7 ] in + let a0:u32 = h.[ mk_usize 0 ] in + let b0:u32 = h.[ mk_usize 1 ] in + let c0:u32 = h.[ mk_usize 2 ] in + let d0:u32 = h.[ mk_usize 3 ] in + let e0:u32 = h.[ mk_usize 4 ] in + let f0:u32 = h.[ mk_usize 5 ] in + let g0:u32 = h.[ mk_usize 6 ] in + let (h0: u32):u32 = h.[ mk_usize 7 ] in let t1:u32 = Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add - (Core.Num.impl__u32__wrapping_add h0 (sigma e0 (sz 1) (sz 1) <: u32) <: u32) + (Core.Num.impl__u32__wrapping_add h0 + (sigma e0 (mk_usize 1) (mk_usize 1) <: u32) + <: + u32) (ch e0 f0 g0 <: u32) <: u32) @@ -123,48 +132,50 @@ let shuffle (ws: t_Array u32 (sz 64)) (hashi: t_Array u32 (sz 8)) : t_Array u32 (ws.[ i ] <: u32) in let t2:u32 = - Core.Num.impl__u32__wrapping_add (sigma a0 (sz 0) (sz 1) <: u32) (maj a0 b0 c0 <: u32) + Core.Num.impl__u32__wrapping_add (sigma a0 (mk_usize 0) (mk_usize 1) <: u32) + (maj a0 b0 c0 <: u32) in - let h:t_Array u32 (sz 8) = + let h:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h - (sz 0) + (mk_usize 0) (Core.Num.impl__u32__wrapping_add t1 t2 <: u32) in - let h:t_Array u32 (sz 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 1) a0 + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 1) a0 in - let h:t_Array u32 (sz 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 2) b0 + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 2) b0 in - let h:t_Array u32 (sz 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 3) c0 + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 3) c0 in - let h:t_Array u32 (sz 8) = + let h:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h - (sz 4) + (mk_usize 4) (Core.Num.impl__u32__wrapping_add d0 t1 <: u32) in - let h:t_Array u32 (sz 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 5) e0 + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 5) e0 in - let h:t_Array u32 (sz 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 6) f0 + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 6) f0 in - let h:t_Array u32 (sz 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (sz 7) g0 + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 7) g0 in h) in h -let to_be_u32s (block: t_Array u8 (sz 64)) : Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = +let to_be_u32s (block: t_Array u8 (mk_usize 64)) : Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = - Alloc.Vec.impl__with_capacity #u32 (v_BLOCK_SIZE /! sz 4 <: usize) + Alloc.Vec.impl__with_capacity #u32 (v_BLOCK_SIZE /! mk_usize 4 <: usize) in let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact u8) - (Core.Slice.impl__chunks_exact #u8 (Rust_primitives.unsize block <: t_Slice u8) (sz 4) + #FStar.Tactics.Typeclasses.solve + (Core.Slice.impl__chunks_exact #u8 (block <: t_Slice u8) (mk_usize 4) <: Core.Slice.Iter.t_ChunksExact u8) <: @@ -174,13 +185,16 @@ let to_be_u32s (block: t_Array u8 (sz 64)) : Alloc.Vec.t_Vec u32 Alloc.Alloc.t_G let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = out in let block_chunk:t_Slice u8 = block_chunk in let block_chunk_array:u32 = - Core.Num.impl__u32__from_be_bytes (Core.Result.impl__unwrap #(t_Array u8 (sz 4)) + Core.Num.impl__u32__from_be_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError - (Core.Convert.f_try_into #(t_Slice u8) #(t_Array u8 (sz 4)) block_chunk + (Core.Convert.f_try_into #(t_Slice u8) + #(t_Array u8 (mk_usize 4)) + #FStar.Tactics.Typeclasses.solve + block_chunk <: - Core.Result.t_Result (t_Array u8 (sz 4)) Core.Array.t_TryFromSliceError) + Core.Result.t_Result (t_Array u8 (mk_usize 4)) Core.Array.t_TryFromSliceError) <: - t_Array u8 (sz 4)) + t_Array u8 (mk_usize 4)) in let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push #u32 #Alloc.Alloc.t_Global out block_chunk_array @@ -189,35 +203,34 @@ let to_be_u32s (block: t_Array u8 (sz 64)) : Alloc.Vec.t_Vec u32 Alloc.Alloc.t_G in out -let schedule (block: t_Array u8 (sz 64)) : t_Array u32 (sz 64) = +let schedule (block: t_Array u8 (mk_usize 64)) : t_Array u32 (mk_usize 64) = let b:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = to_be_u32s block in - let s:t_Array u32 (sz 64) = Rust_primitives.Hax.repeat 0ul (sz 64) in - let s:t_Array u32 (sz 64) = - 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_SIZE } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + let s:t_Array u32 (mk_usize 64) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 64) in + let s:t_Array u32 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + v_K_SIZE + (fun s temp_1_ -> + let s:t_Array u32 (mk_usize 64) = s in + let _:usize = temp_1_ in + true) s (fun s i -> - let s:t_Array u32 (sz 64) = s in + let s:t_Array u32 (mk_usize 64) = s in let i:usize = i in - if i <. sz 16 <: bool + if i <. mk_usize 16 <: bool then - let s:t_Array u32 (sz 64) = + let s:t_Array u32 (mk_usize 64) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize s i (b.[ i ] <: u32) in s else - let t16:u32 = s.[ i -! sz 16 <: usize ] in - let t15:u32 = s.[ i -! sz 15 <: usize ] in - let t7:u32 = s.[ i -! sz 7 <: usize ] in - let t2:u32 = s.[ i -! sz 2 <: usize ] in - let s1:u32 = sigma t2 (sz 3) (sz 0) in - let s0:u32 = sigma t15 (sz 2) (sz 0) in - let s:t_Array u32 (sz 64) = + let t16:u32 = s.[ i -! mk_usize 16 <: usize ] in + let t15:u32 = s.[ i -! mk_usize 15 <: usize ] in + let t7:u32 = s.[ i -! mk_usize 7 <: usize ] in + let t2:u32 = s.[ i -! mk_usize 2 <: usize ] in + let s1:u32 = sigma t2 (mk_usize 3) (mk_usize 0) in + let s0:u32 = sigma t15 (mk_usize 2) (mk_usize 0) in + let s:t_Array u32 (mk_usize 64) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize s i (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add @@ -236,174 +249,182 @@ let schedule (block: t_Array u8 (sz 64)) : t_Array u32 (sz 64) = in s -let compress (block: t_Array u8 (sz 64)) (h_in: t_Array u32 (sz 8)) : t_Array u32 (sz 8) = - let s:t_Array u32 (sz 64) = schedule block in - let h:t_Array u32 (sz 8) = shuffle s h_in in - let h:t_Array u32 (sz 8) = - 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 = sz 8 } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) +let compress (block: t_Array u8 (mk_usize 64)) (h_in: t_Array u32 (mk_usize 8)) + : t_Array u32 (mk_usize 8) = + let s:t_Array u32 (mk_usize 64) = schedule block in + let h:t_Array u32 (mk_usize 8) = shuffle s h_in in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 8) + (fun h temp_1_ -> + let h:t_Array u32 (mk_usize 8) = h in + let _:usize = temp_1_ in + true) h (fun h i -> - let h:t_Array u32 (sz 8) = h in + let h:t_Array u32 (mk_usize 8) = h in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h i (Core.Num.impl__u32__wrapping_add (h.[ i ] <: u32) (h_in.[ i ] <: u32) <: u32) <: - t_Array u32 (sz 8)) + t_Array u32 (mk_usize 8)) in h -let u32s_to_be_bytes (state: t_Array u32 (sz 8)) : t_Array u8 (sz 32) = - let (out: t_Array u8 (sz 32)):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.Ops.Range.t_Range - usize) - ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN_SIZE } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) +let u32s_to_be_bytes (state: t_Array u32 (mk_usize 8)) : t_Array u8 (mk_usize 32) = + let (out: t_Array u8 (mk_usize 32)):t_Array u8 (mk_usize 32) = + Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) + in + let out:t_Array u8 (mk_usize 32) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + v_LEN_SIZE + (fun out temp_1_ -> + let out:t_Array u8 (mk_usize 32) = out in + let _:usize = temp_1_ in + true) out (fun out i -> - let out:t_Array u8 (sz 32) = out in + let out:t_Array u8 (mk_usize 32) = out in let i:usize = i in let tmp:u32 = state.[ i ] in - let tmp:t_Array u8 (sz 4) = Core.Num.impl__u32__to_be_bytes tmp in - 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 = sz 4 } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl__u32__to_be_bytes tmp in + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 4) + (fun out temp_1_ -> + let out:t_Array u8 (mk_usize 32) = out in + let _:usize = temp_1_ in + true) out (fun out j -> - let out:t_Array u8 (sz 32) = out in + let out:t_Array u8 (mk_usize 32) = out in let j:usize = j in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out - ((i *! sz 4 <: usize) +! j <: usize) + ((i *! mk_usize 4 <: usize) +! j <: usize) (tmp.[ j ] <: u8) <: - t_Array u8 (sz 32))) + t_Array u8 (mk_usize 32))) in out -let hash (msg: t_Slice u8) : t_Array u8 (sz 32) = - let h:t_Array u32 (sz 8) = v_HASH_INIT in - let (last_block: t_Array u8 (sz 64)):t_Array u8 (sz 64) = - Rust_primitives.Hax.repeat 0uy (sz 64) +let hash (msg: t_Slice u8) : t_Array u8 (mk_usize 32) = + let h:t_Array u32 (mk_usize 8) = v_HASH_INIT in + let (last_block: t_Array u8 (mk_usize 64)):t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 64) in - let last_block_len:usize = sz 0 in - let h, last_block, last_block_len:(t_Array u32 (sz 8) & t_Array u8 (sz 64) & usize) = + let last_block_len:usize = mk_usize 0 in + let h, last_block, last_block_len:(t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64) & usize) = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Chunks u8) + #FStar.Tactics.Typeclasses.solve (Core.Slice.impl__chunks #u8 msg v_BLOCK_SIZE <: Core.Slice.Iter.t_Chunks u8) <: Core.Slice.Iter.t_Chunks u8) - (h, last_block, last_block_len <: (t_Array u32 (sz 8) & t_Array u8 (sz 64) & usize)) + (h, last_block, last_block_len + <: + (t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64) & usize)) (fun temp_0_ block -> - let h, last_block, last_block_len:(t_Array u32 (sz 8) & t_Array u8 (sz 64) & usize) = + let h, last_block, last_block_len:(t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64) & + usize) = temp_0_ in let block:t_Slice u8 = block in if (Core.Slice.impl__len #u8 block <: usize) <. v_BLOCK_SIZE <: bool then - let last_block:t_Array u8 (sz 64) = - 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 #u8 block <: usize - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + let last_block:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (Core.Slice.impl__len #u8 block <: usize) + (fun last_block temp_1_ -> + let last_block:t_Array u8 (mk_usize 64) = last_block in + let _:usize = temp_1_ in + true) last_block (fun last_block i -> - let last_block:t_Array u8 (sz 64) = last_block in + let last_block:t_Array u8 (mk_usize 64) = last_block in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block i (block.[ i ] <: u8) <: - t_Array u8 (sz 64)) + t_Array u8 (mk_usize 64)) in let last_block_len:usize = Core.Slice.impl__len #u8 block in - h, last_block, last_block_len <: (t_Array u32 (sz 8) & t_Array u8 (sz 64) & usize) + h, last_block, last_block_len + <: + (t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64) & usize) else - let h:t_Array u32 (sz 8) = - compress (Core.Result.impl__unwrap #(t_Array u8 (sz 64)) + let h:t_Array u32 (mk_usize 8) = + compress (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 64)) #Core.Array.t_TryFromSliceError - (Core.Convert.f_try_into #(t_Slice u8) #(t_Array u8 (sz 64)) block + (Core.Convert.f_try_into #(t_Slice u8) + #(t_Array u8 (mk_usize 64)) + #FStar.Tactics.Typeclasses.solve + block <: - Core.Result.t_Result (t_Array u8 (sz 64)) Core.Array.t_TryFromSliceError) + Core.Result.t_Result (t_Array u8 (mk_usize 64)) Core.Array.t_TryFromSliceError + ) <: - t_Array u8 (sz 64)) + t_Array u8 (mk_usize 64)) h in - h, last_block, last_block_len <: (t_Array u32 (sz 8) & t_Array u8 (sz 64) & usize)) + h, last_block, last_block_len + <: + (t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64) & usize)) in - let last_block:t_Array u8 (sz 64) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block last_block_len 128uy + let last_block:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block + last_block_len + (mk_u8 128) in - let len_bist:u64 = cast ((Core.Slice.impl__len #u8 msg <: usize) *! sz 8 <: usize) <: u64 in - let len_bist_bytes:t_Array u8 (sz 8) = Core.Num.impl__u64__to_be_bytes len_bist in - let h, last_block:(t_Array u32 (sz 8) & t_Array u8 (sz 64)) = + let len_bist:u64 = cast ((Core.Slice.impl__len #u8 msg <: usize) *! mk_usize 8 <: usize) <: u64 in + let len_bist_bytes:t_Array u8 (mk_usize 8) = Core.Num.impl__u64__to_be_bytes len_bist in + let h, last_block:(t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64)) = if last_block_len <. (v_BLOCK_SIZE -! v_LEN_SIZE <: usize) then - let last_block:t_Array u8 (sz 64) = - 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_LEN_SIZE } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + let last_block:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + v_LEN_SIZE + (fun last_block temp_1_ -> + let last_block:t_Array u8 (mk_usize 64) = last_block in + let _:usize = temp_1_ in + true) last_block (fun last_block i -> - let last_block:t_Array u8 (sz 64) = last_block in + let last_block:t_Array u8 (mk_usize 64) = last_block in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize last_block ((v_BLOCK_SIZE -! v_LEN_SIZE <: usize) +! i <: usize) (len_bist_bytes.[ i ] <: u8) <: - t_Array u8 (sz 64)) + t_Array u8 (mk_usize 64)) in - let h:t_Array u32 (sz 8) = compress last_block h in - h, last_block <: (t_Array u32 (sz 8) & t_Array u8 (sz 64)) + let h:t_Array u32 (mk_usize 8) = compress last_block h in + h, last_block <: (t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64)) else - let (pad_block: t_Array u8 (sz 64)):t_Array u8 (sz 64) = - Rust_primitives.Hax.repeat 0uy (sz 64) + let (pad_block: t_Array u8 (mk_usize 64)):t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 64) in - let pad_block:t_Array u8 (sz 64) = - 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_LEN_SIZE } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Ops.Range.t_Range usize) + let pad_block:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + v_LEN_SIZE + (fun pad_block temp_1_ -> + let pad_block:t_Array u8 (mk_usize 64) = pad_block in + let _:usize = temp_1_ in + true) pad_block (fun pad_block i -> - let pad_block:t_Array u8 (sz 64) = pad_block in + let pad_block:t_Array u8 (mk_usize 64) = pad_block in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize pad_block ((v_BLOCK_SIZE -! v_LEN_SIZE <: usize) +! i <: usize) (len_bist_bytes.[ i ] <: u8) <: - t_Array u8 (sz 64)) + t_Array u8 (mk_usize 64)) in - let h:t_Array u32 (sz 8) = compress last_block h in - let h:t_Array u32 (sz 8) = compress pad_block h in - h, last_block <: (t_Array u32 (sz 8) & t_Array u8 (sz 64)) + let h:t_Array u32 (mk_usize 8) = compress last_block h in + let h:t_Array u32 (mk_usize 8) = compress pad_block h in + h, last_block <: (t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64)) in u32s_to_be_bytes h -let sha256 (msg: t_Slice u8) : t_Array u8 (sz 32) = hash msg +let sha256 (msg: t_Slice u8) : t_Array u8 (mk_usize 32) = hash msg diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti index 65ff3f90d..9805f84a9 100644 --- a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti +++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti @@ -293,9 +293,21 @@ unfold type rotval (t:inttype) (t':inttype) = val shift_right (#t:inttype) (#t':inttype) (a:int_t t) (b:shiftval t t') : int_t t +val shift_right_lemma (#t:inttype) (#t':inttype) + (a:int_t t) (b:shiftval t t'): + Lemma (v (shift_right #t #t' a b) == (v a / pow2 (v b))) + [SMTPat (shift_right #t #t' a b)] + val shift_left (#t:inttype) (#t':inttype) (a:int_t t) (b:shiftval t t') : int_t t - + +val shift_left_positive_lemma (#t:inttype) (#t':inttype) + (a:int_t t) (b:shiftval t t'): + Lemma (requires (unsigned t \/ v a >= 0)) + (ensures ((v (shift_left #t #t' a b) == (v a * pow2 (v b)) @%. t))) + [SMTPat (shift_left #t #t' a b)] + + val rotate_right: #t:inttype{unsigned t} -> #t':inttype -> a:int_t t -> rotval t t'