🐆 Tx_rollup_l2_batch.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Definition tag_size : Variant.t := Variant.Build "Uint8" unit tt.
Inductive signer : Set :=
| Bls_pk : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → signer
| L2_addr : Tx_rollup_l2_address.t → signer.
Definition Signer_indexable :=
Indexable.Make
(let t : Set := signer in
let pp (fmt : Format.formatter) (function_parameter : signer) : unit :=
match function_parameter with
| Bls_pk _ ⇒ Format.pp_print_string fmt "<bls_signature>"
| L2_addr addr ⇒ Tx_rollup_l2_address.pp fmt addr
end in
let compare (x_value : signer) (y_value : signer) : int :=
match (x_value, y_value) with
| (Bls_pk pk1, Bls_pk pk2) ⇒
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare) pk1 pk2
| (L2_addr addr1, L2_addr addr2) ⇒
Tx_rollup_l2_address.compare addr1 addr2
| (L2_addr _, Bls_pk _) ⇒ (-1)
| (Bls_pk _, L2_addr _) ⇒ 1
end in
let encoding :=
Data_encoding.union None
[
Data_encoding.case_value "bls_pk" None (Data_encoding.Tag 0)
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
(fun (function_parameter : signer) ⇒
match function_parameter with
| Bls_pk pk ⇒ Some pk
| _ ⇒ None
end)
(fun (pk : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
Bls_pk pk);
Data_encoding.case_value "l2_addr" None (Data_encoding.Tag 1)
Tx_rollup_l2_address.encoding
(fun (function_parameter : signer) ⇒
match function_parameter with
| L2_addr addr ⇒ Some addr
| _ ⇒ None
end)
(fun (addr : Tx_rollup_l2_address.t) ⇒ L2_addr addr)
] in
{|
Indexable.VALUE.encoding := encoding;
Indexable.VALUE.compare := compare;
Indexable.VALUE.pp := pp
|}).
Module V1.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Definition tag_size : Variant.t := Variant.Build "Uint8" unit tt.
Inductive signer : Set :=
| Bls_pk : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → signer
| L2_addr : Tx_rollup_l2_address.t → signer.
Definition Signer_indexable :=
Indexable.Make
(let t : Set := signer in
let pp (fmt : Format.formatter) (function_parameter : signer) : unit :=
match function_parameter with
| Bls_pk _ ⇒ Format.pp_print_string fmt "<bls_signature>"
| L2_addr addr ⇒ Tx_rollup_l2_address.pp fmt addr
end in
let compare (x_value : signer) (y_value : signer) : int :=
match (x_value, y_value) with
| (Bls_pk pk1, Bls_pk pk2) ⇒
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare) pk1 pk2
| (L2_addr addr1, L2_addr addr2) ⇒
Tx_rollup_l2_address.compare addr1 addr2
| (L2_addr _, Bls_pk _) ⇒ (-1)
| (Bls_pk _, L2_addr _) ⇒ 1
end in
let encoding :=
Data_encoding.union None
[
Data_encoding.case_value "bls_pk" None (Data_encoding.Tag 0)
Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
(fun (function_parameter : signer) ⇒
match function_parameter with
| Bls_pk pk ⇒ Some pk
| _ ⇒ None
end)
(fun (pk : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
Bls_pk pk);
Data_encoding.case_value "l2_addr" None (Data_encoding.Tag 1)
Tx_rollup_l2_address.encoding
(fun (function_parameter : signer) ⇒
match function_parameter with
| L2_addr addr ⇒ Some addr
| _ ⇒ None
end)
(fun (addr : Tx_rollup_l2_address.t) ⇒ L2_addr addr)
] in
{|
Indexable.VALUE.encoding := encoding;
Indexable.VALUE.compare := compare;
Indexable.VALUE.pp := pp
|}).
Module V1.
Records for the constructor parameters
Module ConstructorRecords_operation_content.
Module operation_content.
Module Withdraw.
Record record {destination ticket_hash qty : Set} : Set := Build {
destination : destination;
ticket_hash : ticket_hash;
qty : qty;
}.
Arguments record : clear implicits.
Definition with_destination {t_destination t_ticket_hash t_qty}
destination (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty destination r.(ticket_hash)
r.(qty).
Definition with_ticket_hash {t_destination t_ticket_hash t_qty}
ticket_hash (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination) ticket_hash
r.(qty).
Definition with_qty {t_destination t_ticket_hash t_qty} qty
(r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination)
r.(ticket_hash) qty.
End Withdraw.
Definition Withdraw_skeleton := Withdraw.record.
Module Transfer.
Record record {destination ticket_hash qty : Set} : Set := Build {
destination : destination;
ticket_hash : ticket_hash;
qty : qty;
}.
Arguments record : clear implicits.
Definition with_destination {t_destination t_ticket_hash t_qty}
destination (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty destination r.(ticket_hash)
r.(qty).
Definition with_ticket_hash {t_destination t_ticket_hash t_qty}
ticket_hash (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination) ticket_hash
r.(qty).
Definition with_qty {t_destination t_ticket_hash t_qty} qty
(r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination)
r.(ticket_hash) qty.
End Transfer.
Definition Transfer_skeleton := Transfer.record.
End operation_content.
End ConstructorRecords_operation_content.
Import ConstructorRecords_operation_content.
Reserved Notation "'operation_content.Withdraw".
Reserved Notation "'operation_content.Transfer".
Inductive operation_content : Set :=
| Withdraw : 'operation_content.Withdraw → operation_content
| Transfer : 'operation_content.Transfer → operation_content
where "'operation_content.Withdraw" :=
(operation_content.Withdraw_skeleton Signature.public_key_hash
Alpha_context.Ticket_hash.t Tx_rollup_l2_qty.t)
and "'operation_content.Transfer" :=
(operation_content.Transfer_skeleton Tx_rollup_l2_address.Indexable.t
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.t)
Tx_rollup_l2_qty.t).
Module operation_content.
Include ConstructorRecords_operation_content.operation_content.
Definition Withdraw := 'operation_content.Withdraw.
Definition Transfer := 'operation_content.Transfer.
End operation_content.
Module operation.
Record record : Set := Build {
signer : Signer_indexable.(Indexable.INDEXABLE.t);
counter : int64;
contents : list operation_content;
}.
Definition with_signer signer (r : record) :=
Build signer r.(counter) r.(contents).
Definition with_counter counter (r : record) :=
Build r.(signer) counter r.(contents).
Definition with_contents contents (r : record) :=
Build r.(signer) r.(counter) contents.
End operation.
Definition operation := operation.record.
Definition transaction : Set := list operation.
Definition signature : Set := Bls.t.
Module t.
Record record : Set := Build {
contents : list transaction;
aggregated_signature : signature;
}.
Definition with_contents contents (r : record) :=
Build contents r.(aggregated_signature).
Definition with_aggregated_signature aggregated_signature (r : record) :=
Build r.(contents) aggregated_signature.
End t.
Definition t := t.record.
Definition compact_operation_content
: Data_encoding.Compact.t operation_content :=
Data_encoding.Compact.union None None
[
Data_encoding.Compact.case_value "withdraw" None
(Data_encoding.Compact.obj3
(Data_encoding.Compact.req "destination"
(Data_encoding.Compact.payload
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(Data_encoding.Compact.req "ticket_hash"
(Data_encoding.Compact.payload
Alpha_context.Ticket_hash.encoding))
(Data_encoding.Compact.req "qty"
Tx_rollup_l2_qty.compact_encoding))
(fun (function_parameter : operation_content) ⇒
match function_parameter with
|
Withdraw {|
operation_content.Withdraw.destination := destination;
operation_content.Withdraw.ticket_hash :=
ticket_hash;
operation_content.Withdraw.qty := qty
|} ⇒ Some (destination, ticket_hash, qty)
| _ ⇒ None
end)
(fun (function_parameter :
Signature.public_key_hash × Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_qty.t) ⇒
let '(destination, ticket_hash, qty) := function_parameter
in
Withdraw
{|
operation_content.Withdraw.destination :=
destination;
operation_content.Withdraw.ticket_hash :=
ticket_hash;
operation_content.Withdraw.qty := qty; |});
Data_encoding.Compact.case_value "transfer" None
(Data_encoding.Compact.obj3
(Data_encoding.Compact.req "destination"
(Indexable.compact Tx_rollup_l2_address.encoding))
(Data_encoding.Compact.req "ticket_hash"
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.compact))
(Data_encoding.Compact.req "qty"
Tx_rollup_l2_qty.compact_encoding))
(fun (function_parameter : operation_content) ⇒
match function_parameter with
|
Transfer {|
operation_content.Transfer.destination := destination;
operation_content.Transfer.ticket_hash :=
ticket_hash;
operation_content.Transfer.qty := qty
|} ⇒ Some (destination, ticket_hash, qty)
| _ ⇒ None
end)
(fun (function_parameter :
Indexable.t Tx_rollup_l2_address.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.either)
× Tx_rollup_l2_qty.t) ⇒
let '(destination, ticket_hash, qty) := function_parameter
in
Transfer
{|
operation_content.Transfer.destination :=
destination;
operation_content.Transfer.ticket_hash :=
ticket_hash;
operation_content.Transfer.qty := qty; |})
].
Definition operation_content_encoding
: Data_encoding.encoding operation_content :=
Data_encoding.Compact.make (Some tag_size) compact_operation_content.
Definition compact_operation_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.Compact.t operation :=
Data_encoding.Compact.conv None
(fun (function_parameter : operation) ⇒
let '{|
operation.signer := signer;
operation.counter := counter;
operation.contents := contents
|} := function_parameter in
(signer, counter, contents))
(fun (function_parameter :
Signer_indexable.(Indexable.INDEXABLE.t) × int64 ×
list operation_content) ⇒
let '(signer, counter, contents) := function_parameter in
{| operation.signer := signer; operation.counter := counter;
operation.contents := contents; |})
(Data_encoding.Compact.obj3
(Data_encoding.Compact.req "signer" encoding_signer)
(Data_encoding.Compact.req "counter" Data_encoding.Compact.int64_value)
(Data_encoding.Compact.req "contents"
(Data_encoding.Compact.list_value 4 operation_content_encoding))).
Definition operation_encoding_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.encoding operation :=
Data_encoding.Compact.make (Some tag_size)
(compact_operation_raw encoding_signer).
Definition compact_transaction_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.Compact.t (list operation) :=
Data_encoding.Compact.list_value 8 (operation_encoding_raw encoding_signer).
Definition transaction_encoding_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.t transaction :=
Data_encoding.Compact.make (Some tag_size)
(compact_transaction_raw encoding_signer).
Definition compact_signer_index
: Data_encoding.Compact.t (Indexable.index signer) :=
Data_encoding.Compact.conv None Indexable.to_int32 Indexable.index_exn
Data_encoding.Compact.int32_value.
Definition compact_signer_either
: Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.either) :=
Signer_indexable.(Indexable.INDEXABLE.compact).
Definition compact_operation : Data_encoding.Compact.t operation :=
compact_operation_raw compact_signer_either.
Definition compact_transaction_signer_index
: Data_encoding.Compact.t (list operation) :=
compact_transaction_raw compact_signer_index.
Definition compact_transaction : Data_encoding.Compact.t (list operation) :=
compact_transaction_raw compact_signer_either.
Definition transaction_encoding : Data_encoding.t transaction :=
transaction_encoding_raw compact_signer_either.
Definition compact (bits : int) : Data_encoding.Compact.t t :=
Data_encoding.Compact.conv None
(fun (function_parameter : t) ⇒
let '{|
t.contents := contents;
t.aggregated_signature := aggregated_signature
|} := function_parameter in
(aggregated_signature, contents))
(fun (function_parameter : signature × list transaction) ⇒
let '(aggregated_signature, contents) := function_parameter in
{| t.contents := contents;
t.aggregated_signature := aggregated_signature; |})
(Data_encoding.Compact.obj2
(Data_encoding.Compact.req "aggregated_signature"
(Data_encoding.Compact.payload Bls.encoding))
(Data_encoding.Compact.req "contents"
(Data_encoding.Compact.list_value bits transaction_encoding))).
End V1.
Inductive t (signer content : Set) : Set :=
| V1 : V1.t → t signer content.
Arguments V1 {_ _}.
Module operation_content.
Module Withdraw.
Record record {destination ticket_hash qty : Set} : Set := Build {
destination : destination;
ticket_hash : ticket_hash;
qty : qty;
}.
Arguments record : clear implicits.
Definition with_destination {t_destination t_ticket_hash t_qty}
destination (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty destination r.(ticket_hash)
r.(qty).
Definition with_ticket_hash {t_destination t_ticket_hash t_qty}
ticket_hash (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination) ticket_hash
r.(qty).
Definition with_qty {t_destination t_ticket_hash t_qty} qty
(r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination)
r.(ticket_hash) qty.
End Withdraw.
Definition Withdraw_skeleton := Withdraw.record.
Module Transfer.
Record record {destination ticket_hash qty : Set} : Set := Build {
destination : destination;
ticket_hash : ticket_hash;
qty : qty;
}.
Arguments record : clear implicits.
Definition with_destination {t_destination t_ticket_hash t_qty}
destination (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty destination r.(ticket_hash)
r.(qty).
Definition with_ticket_hash {t_destination t_ticket_hash t_qty}
ticket_hash (r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination) ticket_hash
r.(qty).
Definition with_qty {t_destination t_ticket_hash t_qty} qty
(r : record t_destination t_ticket_hash t_qty) :=
Build t_destination t_ticket_hash t_qty r.(destination)
r.(ticket_hash) qty.
End Transfer.
Definition Transfer_skeleton := Transfer.record.
End operation_content.
End ConstructorRecords_operation_content.
Import ConstructorRecords_operation_content.
Reserved Notation "'operation_content.Withdraw".
Reserved Notation "'operation_content.Transfer".
Inductive operation_content : Set :=
| Withdraw : 'operation_content.Withdraw → operation_content
| Transfer : 'operation_content.Transfer → operation_content
where "'operation_content.Withdraw" :=
(operation_content.Withdraw_skeleton Signature.public_key_hash
Alpha_context.Ticket_hash.t Tx_rollup_l2_qty.t)
and "'operation_content.Transfer" :=
(operation_content.Transfer_skeleton Tx_rollup_l2_address.Indexable.t
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.t)
Tx_rollup_l2_qty.t).
Module operation_content.
Include ConstructorRecords_operation_content.operation_content.
Definition Withdraw := 'operation_content.Withdraw.
Definition Transfer := 'operation_content.Transfer.
End operation_content.
Module operation.
Record record : Set := Build {
signer : Signer_indexable.(Indexable.INDEXABLE.t);
counter : int64;
contents : list operation_content;
}.
Definition with_signer signer (r : record) :=
Build signer r.(counter) r.(contents).
Definition with_counter counter (r : record) :=
Build r.(signer) counter r.(contents).
Definition with_contents contents (r : record) :=
Build r.(signer) r.(counter) contents.
End operation.
Definition operation := operation.record.
Definition transaction : Set := list operation.
Definition signature : Set := Bls.t.
Module t.
Record record : Set := Build {
contents : list transaction;
aggregated_signature : signature;
}.
Definition with_contents contents (r : record) :=
Build contents r.(aggregated_signature).
Definition with_aggregated_signature aggregated_signature (r : record) :=
Build r.(contents) aggregated_signature.
End t.
Definition t := t.record.
Definition compact_operation_content
: Data_encoding.Compact.t operation_content :=
Data_encoding.Compact.union None None
[
Data_encoding.Compact.case_value "withdraw" None
(Data_encoding.Compact.obj3
(Data_encoding.Compact.req "destination"
(Data_encoding.Compact.payload
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(Data_encoding.Compact.req "ticket_hash"
(Data_encoding.Compact.payload
Alpha_context.Ticket_hash.encoding))
(Data_encoding.Compact.req "qty"
Tx_rollup_l2_qty.compact_encoding))
(fun (function_parameter : operation_content) ⇒
match function_parameter with
|
Withdraw {|
operation_content.Withdraw.destination := destination;
operation_content.Withdraw.ticket_hash :=
ticket_hash;
operation_content.Withdraw.qty := qty
|} ⇒ Some (destination, ticket_hash, qty)
| _ ⇒ None
end)
(fun (function_parameter :
Signature.public_key_hash × Alpha_context.Ticket_hash.t ×
Tx_rollup_l2_qty.t) ⇒
let '(destination, ticket_hash, qty) := function_parameter
in
Withdraw
{|
operation_content.Withdraw.destination :=
destination;
operation_content.Withdraw.ticket_hash :=
ticket_hash;
operation_content.Withdraw.qty := qty; |});
Data_encoding.Compact.case_value "transfer" None
(Data_encoding.Compact.obj3
(Data_encoding.Compact.req "destination"
(Indexable.compact Tx_rollup_l2_address.encoding))
(Data_encoding.Compact.req "ticket_hash"
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.compact))
(Data_encoding.Compact.req "qty"
Tx_rollup_l2_qty.compact_encoding))
(fun (function_parameter : operation_content) ⇒
match function_parameter with
|
Transfer {|
operation_content.Transfer.destination := destination;
operation_content.Transfer.ticket_hash :=
ticket_hash;
operation_content.Transfer.qty := qty
|} ⇒ Some (destination, ticket_hash, qty)
| _ ⇒ None
end)
(fun (function_parameter :
Indexable.t Tx_rollup_l2_address.t ×
Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.either)
× Tx_rollup_l2_qty.t) ⇒
let '(destination, ticket_hash, qty) := function_parameter
in
Transfer
{|
operation_content.Transfer.destination :=
destination;
operation_content.Transfer.ticket_hash :=
ticket_hash;
operation_content.Transfer.qty := qty; |})
].
Definition operation_content_encoding
: Data_encoding.encoding operation_content :=
Data_encoding.Compact.make (Some tag_size) compact_operation_content.
Definition compact_operation_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.Compact.t operation :=
Data_encoding.Compact.conv None
(fun (function_parameter : operation) ⇒
let '{|
operation.signer := signer;
operation.counter := counter;
operation.contents := contents
|} := function_parameter in
(signer, counter, contents))
(fun (function_parameter :
Signer_indexable.(Indexable.INDEXABLE.t) × int64 ×
list operation_content) ⇒
let '(signer, counter, contents) := function_parameter in
{| operation.signer := signer; operation.counter := counter;
operation.contents := contents; |})
(Data_encoding.Compact.obj3
(Data_encoding.Compact.req "signer" encoding_signer)
(Data_encoding.Compact.req "counter" Data_encoding.Compact.int64_value)
(Data_encoding.Compact.req "contents"
(Data_encoding.Compact.list_value 4 operation_content_encoding))).
Definition operation_encoding_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.encoding operation :=
Data_encoding.Compact.make (Some tag_size)
(compact_operation_raw encoding_signer).
Definition compact_transaction_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.Compact.t (list operation) :=
Data_encoding.Compact.list_value 8 (operation_encoding_raw encoding_signer).
Definition transaction_encoding_raw
(encoding_signer :
Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
: Data_encoding.t transaction :=
Data_encoding.Compact.make (Some tag_size)
(compact_transaction_raw encoding_signer).
Definition compact_signer_index
: Data_encoding.Compact.t (Indexable.index signer) :=
Data_encoding.Compact.conv None Indexable.to_int32 Indexable.index_exn
Data_encoding.Compact.int32_value.
Definition compact_signer_either
: Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.either) :=
Signer_indexable.(Indexable.INDEXABLE.compact).
Definition compact_operation : Data_encoding.Compact.t operation :=
compact_operation_raw compact_signer_either.
Definition compact_transaction_signer_index
: Data_encoding.Compact.t (list operation) :=
compact_transaction_raw compact_signer_index.
Definition compact_transaction : Data_encoding.Compact.t (list operation) :=
compact_transaction_raw compact_signer_either.
Definition transaction_encoding : Data_encoding.t transaction :=
transaction_encoding_raw compact_signer_either.
Definition compact (bits : int) : Data_encoding.Compact.t t :=
Data_encoding.Compact.conv None
(fun (function_parameter : t) ⇒
let '{|
t.contents := contents;
t.aggregated_signature := aggregated_signature
|} := function_parameter in
(aggregated_signature, contents))
(fun (function_parameter : signature × list transaction) ⇒
let '(aggregated_signature, contents) := function_parameter in
{| t.contents := contents;
t.aggregated_signature := aggregated_signature; |})
(Data_encoding.Compact.obj2
(Data_encoding.Compact.req "aggregated_signature"
(Data_encoding.Compact.payload Bls.encoding))
(Data_encoding.Compact.req "contents"
(Data_encoding.Compact.list_value bits transaction_encoding))).
End V1.
Inductive t (signer content : Set) : Set :=
| V1 : V1.t → t signer content.
Arguments V1 {_ _}.
We use two bits for the versioning of the layer-2 batches, which
leaves six bits in the shared tag of compact encoding. We use
these six bits to efficiently encode small lists.
To ensure backward compatibility, the value of the label
[tag_bits] cannot be modified. To have more than 3 versions of the
encoding, one would have to use the fourth case to wrap a new
union.
{[
union
~tag_bits:2
~inner_bits:6
[
case "V1" ...;
case "V2" ...;
case "V3" ...;
case "V_next" ...
(union [ case "V4" ... ; ... ]);
]
]}
Definition compact
: Data_encoding.Compact.t (t Indexable.unknown Indexable.unknown) :=
Data_encoding.Compact.union (Some 2) (Some 6)
[
Data_encoding.Compact.case_value "V1" None (V1.compact 6)
(fun (function_parameter : t Indexable.unknown Indexable.unknown) ⇒
let 'V1 x_value := function_parameter in
Some x_value) (fun (x_value : V1.t) ⇒ V1 x_value)
].
: Data_encoding.Compact.t (t Indexable.unknown Indexable.unknown) :=
Data_encoding.Compact.union (Some 2) (Some 6)
[
Data_encoding.Compact.case_value "V1" None (V1.compact 6)
(fun (function_parameter : t Indexable.unknown Indexable.unknown) ⇒
let 'V1 x_value := function_parameter in
Some x_value) (fun (x_value : V1.t) ⇒ V1 x_value)
].
An encoding for [t] that uses a specialized, space-efficient encoding
for the list of transactions.
Definition encoding : Data_encoding.t (t Indexable.unknown Indexable.unknown) :=
Data_encoding.Compact.make (Some tag_size) compact.
Data_encoding.Compact.make (Some tag_size) compact.