Skip to main content

🐆 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.Proto_alpha.Environment.

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 := "\001\128x\031"; t.prefix := "txr1";
    t.hash_size := 20; t.b58check_size := 37; |}.

Definition l2_address : t :=
  {| t.b58check_prefix := "\006\161\166"; t.prefix := "tz4"; t.hash_size := 20;
    t.b58check_size := 36; |}.

Definition inbox_hash : t :=
  {| t.b58check_prefix := "O\148\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\149\030"; t.prefix := "txm"; t.hash_size := 32;
    t.b58check_size := 53; |}.

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

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

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

Definition withdraw_list_hash : t :=
  {| t.b58check_prefix := "O\150H"; 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.