🍃 Blake2B.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.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.V8.
Require TezosOfOCaml.Environment.V8.Proofs.S.
Axiom Make_is_valid
: ∀ (R : Blake2B.Register) (N : Blake2B.PrefixedName),
S.HASH.Valid.t (fun _ ⇒ True) (Blake2B.Make R N).
The [equal] field of the output of [Blake2B.Make] is valid.
Lemma Make_equal_is_valid R N:
Compare.Equal.Valid.t (fun _ ⇒ True) (Blake2B.Make R N).(S.HASH.equal).
Proof.
apply @S.HASH.valid_implies_equal_valid with (fun _ ⇒ True).
apply Make_is_valid.
Qed.
Compare.Equal.Valid.t (fun _ ⇒ True) (Blake2B.Make R N).(S.HASH.equal).
Proof.
apply @S.HASH.valid_implies_equal_valid with (fun _ ⇒ True).
apply Make_is_valid.
Qed.