Specs for the internal blake3_impl.h API
- blake3_hash_many for batches of independent 64-byte pair/merge blocks;
- blake3_compress_in_place to derive the MIP-8 leaf IV from the domain string in get_leaf_iv.
From Stdlib Require Import List NArith ZArith.
Import ListNotations.
Require Import skylabs.auto.cpp.proof.
Require Import skylabs.lang.cpp.cpp.
Require Import skylabs.prelude.fin.
Require Import monad.asts.storage_page_cpp.
Require Import monad.proofs.exec_specs.
Require Import monad.proofs.libspecs.blake3.model.
Import cQp_compat.
Local Open Scope Z_scope.
Definition all_blake3_flags : list blake3_flag :=
[FlagChunkStart; FlagChunkEnd; FlagParent; FlagRoot;
FlagKeyedHash; FlagDeriveKeyContext; FlagDeriveKeyMaterial].
Definition blake3_flag_is_set (flags : Z) (flag : blake3_flag) : bool :=
negb (Z.eqb (Z.land flags (blake3_flag_value flag)) 0).
Definition blake3_flags_of_Z (flags : Z) : list blake3_flag :=
filter (blake3_flag_is_set flags) all_blake3_flags.
Definition blake3_hash_many_call_params
(key : blake3_cv) (counter : N) (increment_counter : bool)
(flags flags_start flags_end : Z) : blake3_hash_many_params :=
{|
blake3_hash_many_key := key;
blake3_hash_many_counter := counter;
blake3_hash_many_increment_counter := increment_counter;
blake3_hash_many_flags := blake3_flags_of_Z flags;
blake3_hash_many_flags_start := blake3_flags_of_Z flags_start;
blake3_hash_many_flags_end := blake3_flags_of_Z flags_end;
|}.
Definition blake3_hash_many_outputs_from_params
(params : blake3_hash_many_params) (inputs : list bytes64) : list N :=
map (fun input ⇒ bytes32_to_N (blake3_hash_one_model params input))
inputs.
Definition blake3_compress_flags (flags : Z)
: option (list blake3_flag) :=
if flags =? blake3_flag_value FlagDeriveKeyMaterial
then Some [FlagDeriveKeyMaterial]
else
if flags =?
(blake3_flag_value FlagChunkStart +
blake3_flag_value FlagChunkEnd +
blake3_flag_value FlagRoot)
then Some [FlagChunkStart; FlagChunkEnd; FlagRoot]
else None.
Section with_Sigma.
Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.
Definition bytes32_ty : type := "evmc::bytes32"%cpp_type.
The original BLAKE3 API reads an array of uint8_t const × inputs. The
page commitment has two concrete call-site shapes:
The pointee bytes are read-only in both cases. The distinction below is
only the C++ type of each pointer object stored in the input-pointer
array.
- leaf hashing stores pointers to immutable page bytes;
- merge hashing stores pointers to mutable local blocks rows, then passes those pointers through the usual C++ qualification conversion.
Inductive blake3_input_pointer_kind : Type :=
| Blake3ConstInputPointers
| Blake3MutableInputPointers.
Definition blake3_input_ptr_ty_for
(kind : blake3_input_pointer_kind) : type :=
match kind with
| Blake3ConstInputPointers ⇒ Tptr (Qconst Tuchar)
| Blake3MutableInputPointers ⇒ Tptr Tuchar
end.
Definition blake3_input_ptr_ty : type :=
blake3_input_ptr_ty_for Blake3ConstInputPointers.
Definition blake3_input_ptr_store_ty_for
(kind : blake3_input_pointer_kind) : type :=
erase_qualifiers (blake3_input_ptr_ty_for kind).
Definition blake3_input_ptr_store_ty : type :=
blake3_input_ptr_store_ty_for Blake3ConstInputPointers.
Definition byte_value (byte : byte) : val :=
Vint (Z.of_N (fin.to_N byte)).
Definition byte_values (bytes : list byte) : list val :=
map byte_value bytes.
Definition bytes32_byte_values (word : bytes32) : list val :=
bytes32_be_values (bytes32_to_N word).
Definition bytes64_byte_values (block : bytes64) : list val :=
bytes32_byte_values (fst block) ++
bytes32_byte_values (snd block).
Definition blake3_cv_byte_values (cv : blake3_cv) : list val :=
byte_values (blake3_cv_bytes cv).
Definition RawDigestBytesR (q : Qp) (digest : digest) : Rep :=
arrayR Tuchar
(primR Tuchar (cQp.mut q))
(bytes32_byte_values digest).
Definition Blake3BlockR (q : Qp) (block : bytes64) : Rep :=
arrayR Tuchar
(primR Tuchar (cQp.mut q))
(bytes64_byte_values block).
Definition output_word_byte_values (word : N) : list val :=
bytes32_be_values word.
Definition output_words_byte_values (outputs : list N) : list val :=
concat (map output_word_byte_values outputs).
Fixpoint Blake3BlocksAtR
(q : Qp) (ptrs : list ptr) (blocks : list bytes64) : mpred :=
match ptrs, blocks with
| [], [] ⇒ emp
| blockp :: ptrs_rest, block :: blocks_rest ⇒
blockp |-> Blake3BlockR q block **
Blake3BlocksAtR q ptrs_rest blocks_rest
| _, _ ⇒ [| False |]
end.
Definition Blake3InputBlocksRFor
(kind : blake3_input_pointer_kind)
(q : Qp) (inputs : list bytes64) : Rep :=
as_Rep
(fun base ⇒
Exists input_ptrs : list ptr,
base |-> arrayLR (blake3_input_ptr_store_ty_for kind)
0 (Z.of_nat (length inputs))
(fun inputp ⇒
primR
(blake3_input_ptr_store_ty_for kind)
(cQp.mut q) (Vptr inputp))
input_ptrs
** [| length input_ptrs = length inputs |]).
Definition Blake3InputBlocksR (q : Qp) (inputs : list bytes64) : Rep :=
Blake3InputBlocksRFor Blake3ConstInputPointers q inputs.
Definition Blake3InputBlocksExactRFor
(kind : blake3_input_pointer_kind)
(q : Qp) (input_ptrs : list ptr) (inputs : list bytes64) : Rep :=
as_Rep
(fun base ⇒
base |-> arrayLR (blake3_input_ptr_store_ty_for kind)
0 (Z.of_nat (length inputs))
(fun inputp ⇒
primR
(blake3_input_ptr_store_ty_for kind)
(cQp.mut q) (Vptr inputp))
input_ptrs
** [| length input_ptrs = length inputs |]).
Definition Blake3OutputWordsR (q : Qp) (outputs : list N) : Rep :=
arrayR bytes32_ty (bytes32R q) outputs.
| Blake3ConstInputPointers
| Blake3MutableInputPointers.
Definition blake3_input_ptr_ty_for
(kind : blake3_input_pointer_kind) : type :=
match kind with
| Blake3ConstInputPointers ⇒ Tptr (Qconst Tuchar)
| Blake3MutableInputPointers ⇒ Tptr Tuchar
end.
Definition blake3_input_ptr_ty : type :=
blake3_input_ptr_ty_for Blake3ConstInputPointers.
Definition blake3_input_ptr_store_ty_for
(kind : blake3_input_pointer_kind) : type :=
erase_qualifiers (blake3_input_ptr_ty_for kind).
Definition blake3_input_ptr_store_ty : type :=
blake3_input_ptr_store_ty_for Blake3ConstInputPointers.
Definition byte_value (byte : byte) : val :=
Vint (Z.of_N (fin.to_N byte)).
Definition byte_values (bytes : list byte) : list val :=
map byte_value bytes.
Definition bytes32_byte_values (word : bytes32) : list val :=
bytes32_be_values (bytes32_to_N word).
Definition bytes64_byte_values (block : bytes64) : list val :=
bytes32_byte_values (fst block) ++
bytes32_byte_values (snd block).
Definition blake3_cv_byte_values (cv : blake3_cv) : list val :=
byte_values (blake3_cv_bytes cv).
Definition RawDigestBytesR (q : Qp) (digest : digest) : Rep :=
arrayR Tuchar
(primR Tuchar (cQp.mut q))
(bytes32_byte_values digest).
Definition Blake3BlockR (q : Qp) (block : bytes64) : Rep :=
arrayR Tuchar
(primR Tuchar (cQp.mut q))
(bytes64_byte_values block).
Definition output_word_byte_values (word : N) : list val :=
bytes32_be_values word.
Definition output_words_byte_values (outputs : list N) : list val :=
concat (map output_word_byte_values outputs).
Fixpoint Blake3BlocksAtR
(q : Qp) (ptrs : list ptr) (blocks : list bytes64) : mpred :=
match ptrs, blocks with
| [], [] ⇒ emp
| blockp :: ptrs_rest, block :: blocks_rest ⇒
blockp |-> Blake3BlockR q block **
Blake3BlocksAtR q ptrs_rest blocks_rest
| _, _ ⇒ [| False |]
end.
Definition Blake3InputBlocksRFor
(kind : blake3_input_pointer_kind)
(q : Qp) (inputs : list bytes64) : Rep :=
as_Rep
(fun base ⇒
Exists input_ptrs : list ptr,
base |-> arrayLR (blake3_input_ptr_store_ty_for kind)
0 (Z.of_nat (length inputs))
(fun inputp ⇒
primR
(blake3_input_ptr_store_ty_for kind)
(cQp.mut q) (Vptr inputp))
input_ptrs
** [| length input_ptrs = length inputs |]).
Definition Blake3InputBlocksR (q : Qp) (inputs : list bytes64) : Rep :=
Blake3InputBlocksRFor Blake3ConstInputPointers q inputs.
Definition Blake3InputBlocksExactRFor
(kind : blake3_input_pointer_kind)
(q : Qp) (input_ptrs : list ptr) (inputs : list bytes64) : Rep :=
as_Rep
(fun base ⇒
base |-> arrayLR (blake3_input_ptr_store_ty_for kind)
0 (Z.of_nat (length inputs))
(fun inputp ⇒
primR
(blake3_input_ptr_store_ty_for kind)
(cQp.mut q) (Vptr inputp))
input_ptrs
** [| length input_ptrs = length inputs |]).
Definition Blake3OutputWordsR (q : Qp) (outputs : list N) : Rep :=
arrayR bytes32_ty (bytes32R q) outputs.
blake3_hash_many has C signature uint8_t ×out. This predicate is
the call-boundary view of its output buffer: a flat byte array containing
the big-endian bytes of each 32-byte output word. Callers that allocate a
bytes32_t[] and pass it via reinterpret_cast<uint8_t *> must bridge
between this byte view and Blake3OutputWordsR at the call site.
Definition Blake3OutputBytesR (q : Qp) (outputs : list N) : Rep :=
arrayR Tuchar
(primR Tuchar (cQp.mut q))
(output_words_byte_values outputs).
Lemma blake3_hash_many_outputs_from_params_range params inputs :
List.Forall (fun x ⇒ (x < 2 ^ 256)%N)
(blake3_hash_many_outputs_from_params params inputs).
Definition Blake3KeyWordsR (q : Qp) (words : list N) : Rep :=
arrayR Tuint
(fun word ⇒ uintR (cQp.mut q) (Z.of_N word))
words
** [| length words = 8%nat |].
Definition Blake3ConstKeyWordsR (q : Qp) (words : list N) : Rep :=
arrayR Tuint
(fun word ⇒ uintR (cQp.const q) (Z.of_N word))
words.
Lemma Blake3ConstKeyWordsR_pack (p : ptr) q words :
length words = 8%nat →
p |-> arrayR Tuint
(fun word ⇒ uintR (cQp.const q) (Z.of_N word))
words |--
p |-> Blake3ConstKeyWordsR q words.
Definition Blake3ConstKeyWordsR_pack_F p q words Hlength :=
[FWD] (Blake3ConstKeyWordsR_pack p q words Hlength).
Lemma Blake3ConstKeyWordsR_unpack (p : ptr) q words :
p |-> Blake3ConstKeyWordsR q words |--
p |-> arrayR Tuint
(fun word ⇒ uintR (cQp.const q) (Z.of_N word))
words.
Definition Blake3ConstKeyWordsR_unpack_F p q words :=
[FWD] (Blake3ConstKeyWordsR_unpack p q words).
End with_Sigma.
arrayR Tuchar
(primR Tuchar (cQp.mut q))
(output_words_byte_values outputs).
Lemma blake3_hash_many_outputs_from_params_range params inputs :
List.Forall (fun x ⇒ (x < 2 ^ 256)%N)
(blake3_hash_many_outputs_from_params params inputs).
Definition Blake3KeyWordsR (q : Qp) (words : list N) : Rep :=
arrayR Tuint
(fun word ⇒ uintR (cQp.mut q) (Z.of_N word))
words
** [| length words = 8%nat |].
Definition Blake3ConstKeyWordsR (q : Qp) (words : list N) : Rep :=
arrayR Tuint
(fun word ⇒ uintR (cQp.const q) (Z.of_N word))
words.
Lemma Blake3ConstKeyWordsR_pack (p : ptr) q words :
length words = 8%nat →
p |-> arrayR Tuint
(fun word ⇒ uintR (cQp.const q) (Z.of_N word))
words |--
p |-> Blake3ConstKeyWordsR q words.
Definition Blake3ConstKeyWordsR_pack_F p q words Hlength :=
[FWD] (Blake3ConstKeyWordsR_pack p q words Hlength).
Lemma Blake3ConstKeyWordsR_unpack (p : ptr) q words :
p |-> Blake3ConstKeyWordsR q words |--
p |-> arrayR Tuint
(fun word ⇒ uintR (cQp.const q) (Z.of_N word))
words.
Definition Blake3ConstKeyWordsR_unpack_F p q words :=
[FWD] (Blake3ConstKeyWordsR_unpack p q words).
End with_Sigma.
This page has been generated by coqdoc