🐆 Tx_rollup_prefixes.v
Translated 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.
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.