🐆 Tx_rollup_message_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Module deposit.
Record record : Set := Build {
sender : Signature.public_key_hash;
destination : Tx_rollup_l2_address.Indexable.value;
ticket_hash : Ticket_hash_repr.t;
amount : Tx_rollup_l2_qty.t;
}.
Definition with_sender sender (r : record) :=
Build sender r.(destination) r.(ticket_hash) r.(amount).
Definition with_destination destination (r : record) :=
Build r.(sender) destination r.(ticket_hash) r.(amount).
Definition with_ticket_hash ticket_hash (r : record) :=
Build r.(sender) r.(destination) ticket_hash r.(amount).
Definition with_amount amount (r : record) :=
Build r.(sender) r.(destination) r.(ticket_hash) amount.
End deposit.
Definition deposit := deposit.record.
Definition deposit_encoding : Data_encoding.encoding deposit :=
Data_encoding.conv
(fun (function_parameter : deposit) ⇒
let '{|
deposit.sender := sender;
deposit.destination := destination;
deposit.ticket_hash := ticket_hash;
deposit.amount := amount
|} := function_parameter in
(sender, destination, ticket_hash, amount))
(fun (function_parameter :
Signature.public_key_hash × Tx_rollup_l2_address.Indexable.value ×
Ticket_hash_repr.t × Tx_rollup_l2_qty.t) ⇒
let '(sender, destination, ticket_hash, amount) := function_parameter in
{| deposit.sender := sender; deposit.destination := destination;
deposit.ticket_hash := ticket_hash; deposit.amount := amount; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "sender"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "destination"
Tx_rollup_l2_address.Indexable.value_encoding)
(Data_encoding.req None None "ticket_hash" Ticket_hash_repr.encoding)
(Data_encoding.req None None "amount" Tx_rollup_l2_qty.encoding)).
Inductive t : Set :=
| Batch : string → t
| Deposit : deposit → t.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Batch" None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "batch"
(Data_encoding.string' None Data_encoding.Hex)))
(fun (function_parameter : t) ⇒
match function_parameter with
| Batch batch ⇒ Some batch
| _ ⇒ None
end) (fun (batch : string) ⇒ Batch batch);
Data_encoding.case_value "Deposit" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "deposit" deposit_encoding))
(fun (function_parameter : t) ⇒
match function_parameter with
| Deposit deposit ⇒ Some deposit
| _ ⇒ None
end) (fun (deposit : deposit) ⇒ Deposit deposit)
].
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Batch str ⇒
let subsize := 10 in
let '(str, ellipsis) :=
if subsize <i (String.length str) then
let substring := String.sub str 0 subsize in
(substring, "...")
else
(str, "") in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "Batch:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))
"@[<hov 2>Batch:@ %s%s@]") (Hex.show (Hex.of_string None str)) ellipsis
|
Deposit {|
deposit.sender := sender;
deposit.destination := destination;
deposit.ticket_hash := ticket_hash;
deposit.amount := amount
|} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "Deposit:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "sender="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "destination="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal
"ticket_hash="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal
"," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal
"amount:"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))))))))))))))
"@[<hov 2>Deposit:@ sender=%a,@ destination=%a,@ ticket_hash=%a,@ amount:%a@]")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) sender
Tx_rollup_l2_address.Indexable.pp destination Ticket_hash_repr.pp
ticket_hash Tx_rollup_l2_qty.pp amount
end.
Definition size_value (function_parameter : t) : int :=
match function_parameter with
| Batch batch ⇒ String.length batch
|
Deposit {|
deposit.sender := _;
deposit.destination := d_value;
deposit.ticket_hash := _;
deposit.amount := _
|} ⇒
let sender_size :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
let destination_size := Tx_rollup_l2_address.Indexable.size_value d_value in
let key_hash_size := 32 in
let amount_size := 8 in
((sender_size +i destination_size) +i key_hash_size) +i amount_size
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Module deposit.
Record record : Set := Build {
sender : Signature.public_key_hash;
destination : Tx_rollup_l2_address.Indexable.value;
ticket_hash : Ticket_hash_repr.t;
amount : Tx_rollup_l2_qty.t;
}.
Definition with_sender sender (r : record) :=
Build sender r.(destination) r.(ticket_hash) r.(amount).
Definition with_destination destination (r : record) :=
Build r.(sender) destination r.(ticket_hash) r.(amount).
Definition with_ticket_hash ticket_hash (r : record) :=
Build r.(sender) r.(destination) ticket_hash r.(amount).
Definition with_amount amount (r : record) :=
Build r.(sender) r.(destination) r.(ticket_hash) amount.
End deposit.
Definition deposit := deposit.record.
Definition deposit_encoding : Data_encoding.encoding deposit :=
Data_encoding.conv
(fun (function_parameter : deposit) ⇒
let '{|
deposit.sender := sender;
deposit.destination := destination;
deposit.ticket_hash := ticket_hash;
deposit.amount := amount
|} := function_parameter in
(sender, destination, ticket_hash, amount))
(fun (function_parameter :
Signature.public_key_hash × Tx_rollup_l2_address.Indexable.value ×
Ticket_hash_repr.t × Tx_rollup_l2_qty.t) ⇒
let '(sender, destination, ticket_hash, amount) := function_parameter in
{| deposit.sender := sender; deposit.destination := destination;
deposit.ticket_hash := ticket_hash; deposit.amount := amount; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "sender"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "destination"
Tx_rollup_l2_address.Indexable.value_encoding)
(Data_encoding.req None None "ticket_hash" Ticket_hash_repr.encoding)
(Data_encoding.req None None "amount" Tx_rollup_l2_qty.encoding)).
Inductive t : Set :=
| Batch : string → t
| Deposit : deposit → t.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Batch" None (Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "batch"
(Data_encoding.string' None Data_encoding.Hex)))
(fun (function_parameter : t) ⇒
match function_parameter with
| Batch batch ⇒ Some batch
| _ ⇒ None
end) (fun (batch : string) ⇒ Batch batch);
Data_encoding.case_value "Deposit" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "deposit" deposit_encoding))
(fun (function_parameter : t) ⇒
match function_parameter with
| Deposit deposit ⇒ Some deposit
| _ ⇒ None
end) (fun (deposit : deposit) ⇒ Deposit deposit)
].
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Batch str ⇒
let subsize := 10 in
let '(str, ellipsis) :=
if subsize <i (String.length str) then
let substring := String.sub str 0 subsize in
(substring, "...")
else
(str, "") in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "Batch:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))
"@[<hov 2>Batch:@ %s%s@]") (Hex.show (Hex.of_string None str)) ellipsis
|
Deposit {|
deposit.sender := sender;
deposit.destination := destination;
deposit.ticket_hash := ticket_hash;
deposit.amount := amount
|} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "Deposit:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "sender="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal "destination="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal
"ticket_hash="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal
"," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String_literal
"amount:"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))))))))))))))
"@[<hov 2>Deposit:@ sender=%a,@ destination=%a,@ ticket_hash=%a,@ amount:%a@]")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) sender
Tx_rollup_l2_address.Indexable.pp destination Ticket_hash_repr.pp
ticket_hash Tx_rollup_l2_qty.pp amount
end.
Definition size_value (function_parameter : t) : int :=
match function_parameter with
| Batch batch ⇒ String.length batch
|
Deposit {|
deposit.sender := _;
deposit.destination := d_value;
deposit.ticket_hash := _;
deposit.amount := _
|} ⇒
let sender_size :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
let destination_size := Tx_rollup_l2_address.Indexable.size_value d_value in
let key_hash_size := 32 in
let amount_size := 8 in
((sender_size +i destination_size) +i key_hash_size) +i amount_size
end.