🇿 Zk_rollup_account_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.Zk_rollup_state_repr.
Definition SMap :=
Map.Make
{|
Compare.COMPARABLE.compare := String.compare
|}.
Inductive circuit_info : Set :=
| Public : circuit_info
| Private : circuit_info
| Fee : circuit_info.
Module static.
Record record : Set := Build {
public_parameters : Plonk.public_parameters;
state_length : int;
circuits_info : SMap.(Map.S.t) circuit_info;
nb_ops : int;
}.
Definition with_public_parameters public_parameters (r : record) :=
Build public_parameters r.(state_length) r.(circuits_info) r.(nb_ops).
Definition with_state_length state_length (r : record) :=
Build r.(public_parameters) state_length r.(circuits_info) r.(nb_ops).
Definition with_circuits_info circuits_info (r : record) :=
Build r.(public_parameters) r.(state_length) circuits_info r.(nb_ops).
Definition with_nb_ops nb_ops (r : record) :=
Build r.(public_parameters) r.(state_length) r.(circuits_info) nb_ops.
End static.
Definition static := static.record.
Module dynamic.
Record record : Set := Build {
state : Zk_rollup_state_repr.t;
paid_l2_operations_storage_space : Z.t;
used_l2_operations_storage_space : Z.t;
}.
Definition with_state state (r : record) :=
Build state r.(paid_l2_operations_storage_space)
r.(used_l2_operations_storage_space).
Definition with_paid_l2_operations_storage_space
paid_l2_operations_storage_space (r : record) :=
Build r.(state) paid_l2_operations_storage_space
r.(used_l2_operations_storage_space).
Definition with_used_l2_operations_storage_space
used_l2_operations_storage_space (r : record) :=
Build r.(state) r.(paid_l2_operations_storage_space)
used_l2_operations_storage_space.
End dynamic.
Definition dynamic := dynamic.record.
Module t.
Record record : Set := Build {
static : static;
dynamic : dynamic;
}.
Definition with_static static (r : record) :=
Build static r.(dynamic).
Definition with_dynamic dynamic (r : record) :=
Build r.(static) dynamic.
End t.
Definition t := t.record.
Definition circuits_info_encoding
: Data_encoding.t (SMap.(Map.S.t) circuit_info) :=
let variant_encoding :=
let '(public_tag, public_encoding) :=
(0,
(Data_encoding.obj1
(Data_encoding.req None None "public" Data_encoding.unit_value))) in
let '(private_tag, private_encoding) :=
(1,
(Data_encoding.obj1
(Data_encoding.req None None "private" Data_encoding.unit_value))) in
let '(fee_tag, fee_encoding) :=
(2,
(Data_encoding.obj1
(Data_encoding.req None None "fee" Data_encoding.unit_value))) in
Data_encoding.matching None
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Public ⇒ Data_encoding.matched None public_tag public_encoding tt
| Private ⇒ Data_encoding.matched None private_tag private_encoding tt
| Fee ⇒ Data_encoding.matched None fee_tag fee_encoding tt
end)
[
Data_encoding.case_value "Public" None (Data_encoding.Tag public_tag)
public_encoding
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Public ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Public);
Data_encoding.case_value "Private" None (Data_encoding.Tag private_tag)
private_encoding
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Private ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Private);
Data_encoding.case_value "Fee" None (Data_encoding.Tag fee_tag)
fee_encoding
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Fee ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Fee)
] in
Data_encoding.conv_with_guard
(fun (m_value : SMap.(Map.S.t) circuit_info) ⇒
List.of_seq (SMap.(Map.S.to_seq) m_value))
(fun (l_value : list (String.t × circuit_info)) ⇒
let m_value := SMap.(Map.S.of_seq) (List.to_seq l_value) in
if
Compare.List_length_with.op_ltgt l_value (SMap.(Map.S.cardinal) m_value)
then
Pervasives.Error
"Zk_rollup_origination: circuits_info has duplicated keys"
else
Pervasives.Ok m_value) None
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.string_value variant_encoding)).
Definition encoding : Data_encoding.encoding t :=
let static_encoding :=
Data_encoding.conv
(fun (function_parameter : static) ⇒
let '{|
static.public_parameters := public_parameters;
static.state_length := state_length;
static.circuits_info := circuits_info;
static.nb_ops := nb_ops
|} := function_parameter in
(public_parameters, state_length, circuits_info, nb_ops))
(fun (function_parameter :
Plonk.public_parameters × int × SMap.(Map.S.t) circuit_info × int) ⇒
let '(public_parameters, state_length, circuits_info, nb_ops) :=
function_parameter in
{| static.public_parameters := public_parameters;
static.state_length := state_length;
static.circuits_info := circuits_info; static.nb_ops := nb_ops; |})
None
(Data_encoding.obj4
(Data_encoding.req None None "public_parameters"
Plonk.public_parameters_encoding)
(Data_encoding.req None None "state_length" Data_encoding.int31)
(Data_encoding.req None None "circuits_info" circuits_info_encoding)
(Data_encoding.req None None "nb_ops" Data_encoding.int31)) in
let dynamic_encoding :=
Data_encoding.conv
(fun (function_parameter : dynamic) ⇒
let '{|
dynamic.state := state_value;
dynamic.paid_l2_operations_storage_space :=
paid_l2_operations_storage_space;
dynamic.used_l2_operations_storage_space :=
used_l2_operations_storage_space
|} := function_parameter in
(state_value, paid_l2_operations_storage_space,
used_l2_operations_storage_space))
(fun (function_parameter : Zk_rollup_state_repr.t × Z.t × Z.t) ⇒
let
'(state_value, paid_l2_operations_storage_space,
used_l2_operations_storage_space) := function_parameter in
{| dynamic.state := state_value;
dynamic.paid_l2_operations_storage_space :=
paid_l2_operations_storage_space;
dynamic.used_l2_operations_storage_space :=
used_l2_operations_storage_space; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "state" Zk_rollup_state_repr.encoding)
(Data_encoding.req None None "paid_l2_operations_storage_space"
Data_encoding.n_value)
(Data_encoding.req None None "used_l2_operations_storage_space"
Data_encoding.n_value)) in
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.static := static; t.dynamic := dynamic |} := function_parameter
in
(static, dynamic))
(fun (function_parameter : static × dynamic) ⇒
let '(static, dynamic) := function_parameter in
{| t.static := static; t.dynamic := dynamic; |}) None
(Data_encoding.obj2 (Data_encoding.req None None "static" static_encoding)
(Data_encoding.req None None "dynamic" dynamic_encoding)).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Definition SMap :=
Map.Make
{|
Compare.COMPARABLE.compare := String.compare
|}.
Inductive circuit_info : Set :=
| Public : circuit_info
| Private : circuit_info
| Fee : circuit_info.
Module static.
Record record : Set := Build {
public_parameters : Plonk.public_parameters;
state_length : int;
circuits_info : SMap.(Map.S.t) circuit_info;
nb_ops : int;
}.
Definition with_public_parameters public_parameters (r : record) :=
Build public_parameters r.(state_length) r.(circuits_info) r.(nb_ops).
Definition with_state_length state_length (r : record) :=
Build r.(public_parameters) state_length r.(circuits_info) r.(nb_ops).
Definition with_circuits_info circuits_info (r : record) :=
Build r.(public_parameters) r.(state_length) circuits_info r.(nb_ops).
Definition with_nb_ops nb_ops (r : record) :=
Build r.(public_parameters) r.(state_length) r.(circuits_info) nb_ops.
End static.
Definition static := static.record.
Module dynamic.
Record record : Set := Build {
state : Zk_rollup_state_repr.t;
paid_l2_operations_storage_space : Z.t;
used_l2_operations_storage_space : Z.t;
}.
Definition with_state state (r : record) :=
Build state r.(paid_l2_operations_storage_space)
r.(used_l2_operations_storage_space).
Definition with_paid_l2_operations_storage_space
paid_l2_operations_storage_space (r : record) :=
Build r.(state) paid_l2_operations_storage_space
r.(used_l2_operations_storage_space).
Definition with_used_l2_operations_storage_space
used_l2_operations_storage_space (r : record) :=
Build r.(state) r.(paid_l2_operations_storage_space)
used_l2_operations_storage_space.
End dynamic.
Definition dynamic := dynamic.record.
Module t.
Record record : Set := Build {
static : static;
dynamic : dynamic;
}.
Definition with_static static (r : record) :=
Build static r.(dynamic).
Definition with_dynamic dynamic (r : record) :=
Build r.(static) dynamic.
End t.
Definition t := t.record.
Definition circuits_info_encoding
: Data_encoding.t (SMap.(Map.S.t) circuit_info) :=
let variant_encoding :=
let '(public_tag, public_encoding) :=
(0,
(Data_encoding.obj1
(Data_encoding.req None None "public" Data_encoding.unit_value))) in
let '(private_tag, private_encoding) :=
(1,
(Data_encoding.obj1
(Data_encoding.req None None "private" Data_encoding.unit_value))) in
let '(fee_tag, fee_encoding) :=
(2,
(Data_encoding.obj1
(Data_encoding.req None None "fee" Data_encoding.unit_value))) in
Data_encoding.matching None
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Public ⇒ Data_encoding.matched None public_tag public_encoding tt
| Private ⇒ Data_encoding.matched None private_tag private_encoding tt
| Fee ⇒ Data_encoding.matched None fee_tag fee_encoding tt
end)
[
Data_encoding.case_value "Public" None (Data_encoding.Tag public_tag)
public_encoding
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Public ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Public);
Data_encoding.case_value "Private" None (Data_encoding.Tag private_tag)
private_encoding
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Private ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Private);
Data_encoding.case_value "Fee" None (Data_encoding.Tag fee_tag)
fee_encoding
(fun (function_parameter : circuit_info) ⇒
match function_parameter with
| Fee ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Fee)
] in
Data_encoding.conv_with_guard
(fun (m_value : SMap.(Map.S.t) circuit_info) ⇒
List.of_seq (SMap.(Map.S.to_seq) m_value))
(fun (l_value : list (String.t × circuit_info)) ⇒
let m_value := SMap.(Map.S.of_seq) (List.to_seq l_value) in
if
Compare.List_length_with.op_ltgt l_value (SMap.(Map.S.cardinal) m_value)
then
Pervasives.Error
"Zk_rollup_origination: circuits_info has duplicated keys"
else
Pervasives.Ok m_value) None
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.string_value variant_encoding)).
Definition encoding : Data_encoding.encoding t :=
let static_encoding :=
Data_encoding.conv
(fun (function_parameter : static) ⇒
let '{|
static.public_parameters := public_parameters;
static.state_length := state_length;
static.circuits_info := circuits_info;
static.nb_ops := nb_ops
|} := function_parameter in
(public_parameters, state_length, circuits_info, nb_ops))
(fun (function_parameter :
Plonk.public_parameters × int × SMap.(Map.S.t) circuit_info × int) ⇒
let '(public_parameters, state_length, circuits_info, nb_ops) :=
function_parameter in
{| static.public_parameters := public_parameters;
static.state_length := state_length;
static.circuits_info := circuits_info; static.nb_ops := nb_ops; |})
None
(Data_encoding.obj4
(Data_encoding.req None None "public_parameters"
Plonk.public_parameters_encoding)
(Data_encoding.req None None "state_length" Data_encoding.int31)
(Data_encoding.req None None "circuits_info" circuits_info_encoding)
(Data_encoding.req None None "nb_ops" Data_encoding.int31)) in
let dynamic_encoding :=
Data_encoding.conv
(fun (function_parameter : dynamic) ⇒
let '{|
dynamic.state := state_value;
dynamic.paid_l2_operations_storage_space :=
paid_l2_operations_storage_space;
dynamic.used_l2_operations_storage_space :=
used_l2_operations_storage_space
|} := function_parameter in
(state_value, paid_l2_operations_storage_space,
used_l2_operations_storage_space))
(fun (function_parameter : Zk_rollup_state_repr.t × Z.t × Z.t) ⇒
let
'(state_value, paid_l2_operations_storage_space,
used_l2_operations_storage_space) := function_parameter in
{| dynamic.state := state_value;
dynamic.paid_l2_operations_storage_space :=
paid_l2_operations_storage_space;
dynamic.used_l2_operations_storage_space :=
used_l2_operations_storage_space; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "state" Zk_rollup_state_repr.encoding)
(Data_encoding.req None None "paid_l2_operations_storage_space"
Data_encoding.n_value)
(Data_encoding.req None None "used_l2_operations_storage_space"
Data_encoding.n_value)) in
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.static := static; t.dynamic := dynamic |} := function_parameter
in
(static, dynamic))
(fun (function_parameter : static × dynamic) ⇒
let '(static, dynamic) := function_parameter in
{| t.static := static; t.dynamic := dynamic; |}) None
(Data_encoding.obj2 (Data_encoding.req None None "static" static_encoding)
(Data_encoding.req None None "dynamic" dynamic_encoding)).