🍃 Blake2B.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.S.
Axiom Make_is_valid
: ∀ (R : Blake2B.Register) (N : Blake2B.PrefixedName),
S.HASH.Valid.t (fun _ ⇒ True) (Blake2B.Make R N).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.S.
Axiom Make_is_valid
: ∀ (R : Blake2B.Register) (N : Blake2B.PrefixedName),
S.HASH.Valid.t (fun _ ⇒ True) (Blake2B.Make R N).