Skip to main content

🍃 Blake2B.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.S.

Module Name.
  Record signature : Set := {
    name : string;
    title : string;
    size_value : option int;
  }.
End Name.
Definition Name := @Name.signature.

Module PrefixedName.
  Record signature : Set := {
    name : string;
    title : string;
    size_value : option int;
    b58check_prefix : string;
  }.
End PrefixedName.
Definition PrefixedName := @PrefixedName.signature.

Parameter Make_minimal_t : (Name : Name), Set.

Parameter Make_minimal :
   (Name : Name), S.MINIMAL_HASH (t := Make_minimal_t Name).

Module Register.
  Record signature : Set := {
    register_encoding :
       {a : Set},
      string int (a string) (string option a)
      (a Base58.data) Base58.encoding a;
  }.
End Register.
Definition Register := @Register.signature.

Parameter Make_t : (Register : Register) (Name : PrefixedName), Set.

Parameter Make_Set_t :
   (Register : Register) (Name : PrefixedName), Set.

Parameter Make_Map_t :
   (Register : Register) (Name : PrefixedName), Set Set.

Parameter Make :
   (Register : Register),
   (Name : PrefixedName),
  S.HASH (t := Make_t Register Name) (Set_t := Make_Set_t Register Name)
    (Map_t := Make_Map_t Register Name).