Merge pull request hacl-star#864 from hacl-star/afromher_blake

Add support for parameters beyond key/output length in Blake2

code/blake2/Hacl.Impl.Blake2.Core.fst

@@ -31,6 +31,30 @@ let row_v #a #m h r =
 
 let row_v_lemma #a #m h0 h1 r1 r2 = ()
 
+let create_default_params a salt personal =
+ match a with
+ | Spec.Blake2S -> {
+ digest_length = u8 32;
+ key_length = u8 0;
+ fanout = u8 1;
+ depth = u8 1;
+ leaf_length = u32 0;
+ node_offset = u32 0;
+ xof_length = u16 0;
+ node_depth = u8 0;
+ inner_length = u8 0;
+ salt; personal } <: blake2s_params
+ | Spec.Blake2B -> {
+ digest_length = u8 64;
+ key_length = u8 0;
+ fanout = u8 1;
+ depth = u8 1;
+ leaf_length = u32 0;
+ node_offset = u32 0;
+ xof_length = u32 0;
+ node_depth = u8 0;
+ inner_length = u8 0;
+ salt; personal }
 
 #push-options "--z3rlimit 50"
 let g_rowi_disjoint #a #m st idx1 idx2 =

code/blake2/Hacl.Impl.Blake2.Core.fsti

@@ -53,6 +53,179 @@ val row_v_lemma: #a:Spec.alg -> #m:m_spec -> h0:mem -> h1:mem -> r1:row_p a m ->
  row_v h0 r1 == row_v h1 r2))
  [SMTPat (row_v h0 r1); SMTPat (row_v h1 r2)]
 
+noextract inline_for_extraction
+let salt_len (a:Spec.alg) : size_t =
+ match a with
+ | Spec.Blake2S -> 8ul
+ | Spec.Blake2B -> 16ul
+
+noextract inline_for_extraction
+let personal_len (a:Spec.alg) : size_t =
+ match a with
+ | Spec.Blake2S -> 8ul
+ | Spec.Blake2B -> 16ul
+
+noeq
+type blake2s_params = {
+ digest_length: uint8;
+ key_length: uint8;
+ fanout: uint8;
+ depth: uint8;
+ leaf_length: uint32;
+ node_offset: uint32;
+ xof_length: uint16;
+ node_depth: uint8;
+ inner_length: uint8;
+ salt: lbuffer uint8 8ul;
+ personal: lbuffer uint8 8ul;
+}
+
+inline_for_extraction noextract
+let get_blake2s_salt (p: blake2s_params) = p.salt
+
+inline_for_extraction noextract
+let get_blake2s_personal (p: blake2s_params) = p.personal
+
+inline_for_extraction noextract
+let set_blake2s_digest_length
+ (p: blake2s_params)
+ (nn: size_t{1 <= v nn /\ v nn <= Spec.max_output Spec.Blake2S})
+ : blake2s_params =
+ {p with digest_length = to_u8 nn}
+
+inline_for_extraction noextract
+let set_blake2s_key_length
+ (p: blake2s_params)
+ (kk: size_t{v kk <= Spec.max_key Spec.Blake2S})
+ : blake2s_params =
+ {p with key_length = to_u8 kk}
+
+let blake2s_params_inv (h: mem) (p: blake2s_params): GTot prop =
+ live h p.salt /\ live h p.personal
+
+let blake2s_params_loc (p: blake2s_params) =
+ loc p.salt `union` loc p.personal
+
+let blake2s_params_v (h: mem) (p: blake2s_params): GTot Spec.blake2s_params =
+ Spec.Mkblake2s_params
+ p.digest_length
+ p.key_length
+ p.fanout
+ p.depth
+ p.leaf_length
+ p.node_offset
+ p.xof_length
+ p.node_depth
+ p.inner_length
+ (as_seq h p.salt)
+ (as_seq h p.personal)
+
+noeq
+type blake2b_params = {
+ digest_length: uint8;
+ key_length: uint8;
+ fanout: uint8;
+ depth: uint8;
+ leaf_length: uint32;
+ node_offset: uint32;
+ xof_length: uint32;
+ node_depth: uint8;
+ inner_length: uint8;
+ // Blake2b also contains 14 reserved bytes here, but they seem
+ // unused and to only contain zeros, hence we do not expose them
+ salt: lbuffer uint8 16ul;
+ personal: lbuffer uint8 16ul;
+}
+
+let blake2b_params_inv (h: mem) (p: blake2b_params): GTot prop =
+ live h p.salt /\ live h p.personal
+
+let blake2b_params_loc (p: blake2b_params) =
+ loc p.salt `union` loc p.personal
+
+let blake2b_params_v (h: mem) (p: blake2b_params): GTot Spec.blake2b_params =
+ Spec.Mkblake2b_params
+ p.digest_length
+ p.key_length
+ p.fanout
+ p.depth
+ p.leaf_length
+ p.node_offset
+ p.xof_length
+ p.node_depth
+ p.inner_length
+ (as_seq h p.salt)
+ (as_seq h p.personal)
+
+noextract inline_for_extraction
+let blake2_params (a:Spec.alg) =
+ match a with
+ | Spec.Blake2S -> blake2s_params
+ | Spec.Blake2B -> blake2b_params
+
+inline_for_extraction noextract
+let set_digest_length (#a: Spec.alg)
+ (p: blake2_params a)
+ (nn: size_t{1 <= v nn /\ v nn <= Spec.max_output a})
+ : blake2_params a =
+ match a with
+ | Spec.Blake2S -> set_blake2s_digest_length p nn
+ | Spec.Blake2B -> {p with digest_length = to_u8 nn}
+
+inline_for_extraction noextract
+let set_key_length (#a: Spec.alg)
+ (p: blake2_params a)
+ (kk: size_t{v kk <= Spec.max_key a})
+ : blake2_params a =
+ match a with
+ | Spec.Blake2S -> set_blake2s_key_length p kk
+ | Spec.Blake2B -> {p with key_length = to_u8 kk}
+
+inline_for_extraction noextract
+let get_salt (#a: Spec.alg) (p: blake2_params a) : lbuffer uint8 (salt_len a) =
+ match a with
+ | Spec.Blake2S -> get_blake2s_salt p
+ | Spec.Blake2B -> p.salt
+
+inline_for_extraction noextract
+let get_personal (#a: Spec.alg) (p: blake2_params a) : lbuffer uint8 (personal_len a) =
+ match a with
+ | Spec.Blake2S -> get_blake2s_personal p
+ | Spec.Blake2B -> p.personal
+
+noextract inline_for_extraction
+let blake2_params_inv (#a:Spec.alg) (h: mem) (p: blake2_params a) =
+ match a with
+ | Spec.Blake2S -> blake2s_params_inv h p
+ | Spec.Blake2B -> blake2b_params_inv h p
+
+noextract inline_for_extraction
+let blake2_params_loc (#a:Spec.alg) (p: blake2_params a) =
+ match a with
+ | Spec.Blake2S -> blake2s_params_loc p
+ | Spec.Blake2B -> blake2b_params_loc p
+
+noextract inline_for_extraction
+let blake2_params_v (#a:Spec.alg) (h: mem) (p: blake2_params a) : GTot (Spec.blake2_params a) =
+ match a with
+ | Spec.Blake2S -> blake2s_params_v h p
+ | Spec.Blake2B -> blake2b_params_v h p
+
+noextract inline_for_extraction
+val create_default_params: a:Spec.alg ->
+ salt: lbuffer uint8 (salt_len a) ->
+ personal: lbuffer uint8 (personal_len a) ->
+ Stack (blake2_params a)
+ (requires fun h -> live h salt /\ live h personal /\
+ as_seq h salt == Seq.create (Spec.salt_length a) (u8 0) /\
+ as_seq h personal == Seq.create (Spec.personal_length a) (u8 0)
+ )
+ (ensures (fun h0 p h1 ->
+ h0 == h1 /\
+ blake2_params_loc p == loc salt `union` loc personal /\
+ blake2_params_inv h1 p /\
+ blake2_params_v h1 p == Spec.blake2_default_params a))
+
 noextract inline_for_extraction
 unfold let state_p (a:Spec.alg) (m:m_spec) =
  lbuffer (element_t a m) (4ul *. row_len a m)