🐆 Tx_rollup_prefixes.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.

Module t.
  Record record : Set := Build {
    b58check_prefix : string;
    prefix : string;
    hash_size : int;
    b58check_size : int;
  }.
  Definition with_b58check_prefix b58check_prefix (r : record) :=
    Build b58check_prefix r.(prefix) r.(hash_size) r.(b58check_size).
  Definition with_prefix prefix (r : record) :=
    Build r.(b58check_prefix) prefix r.(hash_size) r.(b58check_size).
  Definition with_hash_size hash_size (r : record) :=
    Build r.(b58check_prefix) r.(prefix) hash_size r.(b58check_size).
  Definition with_b58check_size b58check_size (r : record) :=
    Build r.(b58check_prefix) r.(prefix) r.(hash_size) b58check_size.
End t.
Definition t := t.record.

Definition rollup_address : t :=
  {|
    t.b58check_prefix :=
      String.String "001" (String.String "128" ("x" ++ String.String "031" ""));
    t.prefix := "txr1"; t.hash_size := 20; t.b58check_size := 37; |}.

Definition inbox_hash : t :=
  {| t.b58check_prefix := "O" ++ String.String "148" (String.String "196" "");
    t.prefix := "txi"; t.hash_size := 32; t.b58check_size := 53; |}.

Definition inbox_list_hash : t := inbox_hash.

Definition message_hash : t :=
  {| t.b58check_prefix := "O" ++ String.String "149" (String.String "030" "");
    t.prefix := "txm"; t.hash_size := 32; t.b58check_size := 53; |}.

Definition commitment_hash : t :=
  {| t.b58check_prefix := "O" ++ String.String "148" (String.String "017" "");
    t.prefix := "txc"; t.hash_size := 32; t.b58check_size := 53; |}.

Definition message_result_hash : t :=
  {|
    t.b58check_prefix :=
      String.String "018" (String.String "007" (String.String "206" "W"));
    t.prefix := "txmr"; t.hash_size := 32; t.b58check_size := 54; |}.

Definition message_result_list_hash : t :=
  {| t.b58check_prefix := "O" ++ String.String "146" "R"; t.prefix := "txM";
    t.hash_size := 32; t.b58check_size := 53; |}.

Definition withdraw_list_hash : t :=
  {| t.b58check_prefix := "O" ++ String.String "150" "H"; t.prefix := "txw";
    t.hash_size := 32; t.b58check_size := 53; |}.

Definition check_encoding {A : Set} (function_parameter : t)
  : Base58.encoding A → unit :=
  let '{| t.prefix := prefix; t.b58check_size := b58check_size |} :=
    function_parameter in
  fun (encoding : Base58.encoding A) ⇒
    Base58.check_encoded_prefix encoding prefix b58check_size.