Skip to main content

🍃 Blake2B.v

Proofs

See code, Gitlab

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).

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.