🇿 Zk_rollup_update_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_scalar.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Module op_pi.
Record record : Set := Build {
new_state : Zk_rollup_state_repr.t;
fee : Zk_rollup_scalar.t;
exit_validity : bool;
}.
Definition with_new_state new_state (r : record) :=
Build new_state r.(fee) r.(exit_validity).
Definition with_fee fee (r : record) :=
Build r.(new_state) fee r.(exit_validity).
Definition with_exit_validity exit_validity (r : record) :=
Build r.(new_state) r.(fee) exit_validity.
End op_pi.
Definition op_pi := op_pi.record.
Module private_inner_pi.
Record record : Set := Build {
new_state : Zk_rollup_state_repr.t;
fees : Zk_rollup_scalar.t;
}.
Definition with_new_state new_state (r : record) :=
Build new_state r.(fees).
Definition with_fees fees (r : record) :=
Build r.(new_state) fees.
End private_inner_pi.
Definition private_inner_pi := private_inner_pi.record.
Module fee_pi.
Record record : Set := Build {
new_state : Zk_rollup_state_repr.t;
}.
Definition with_new_state new_state (r : record) :=
Build new_state.
End fee_pi.
Definition fee_pi := fee_pi.record.
Module t.
Record record : Set := Build {
pending_pis : list (string × op_pi);
private_pis : list (string × private_inner_pi);
fee_pi : fee_pi;
proof : Plonk.proof;
}.
Definition with_pending_pis pending_pis (r : record) :=
Build pending_pis r.(private_pis) r.(fee_pi) r.(proof).
Definition with_private_pis private_pis (r : record) :=
Build r.(pending_pis) private_pis r.(fee_pi) r.(proof).
Definition with_fee_pi fee_pi (r : record) :=
Build r.(pending_pis) r.(private_pis) fee_pi r.(proof).
Definition with_proof proof (r : record) :=
Build r.(pending_pis) r.(private_pis) r.(fee_pi) proof.
End t.
Definition t := t.record.
Definition op_pi_encoding : Data_encoding.t op_pi :=
Data_encoding.conv
(fun (function_parameter : op_pi) ⇒
let '{|
op_pi.new_state := new_state;
op_pi.fee := fee;
op_pi.exit_validity := exit_validity
|} := function_parameter in
(new_state, fee, exit_validity))
(fun (function_parameter :
Zk_rollup_state_repr.t × Zk_rollup_scalar.t × bool) ⇒
let '(new_state, fee, exit_validity) := function_parameter in
{| op_pi.new_state := new_state; op_pi.fee := fee;
op_pi.exit_validity := exit_validity; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "new_state" Zk_rollup_state_repr.encoding)
(Data_encoding.req None None "fee" Plonk.scalar_encoding)
(Data_encoding.req None None "exit_validity" Data_encoding.bool_value)).
Definition private_inner_pi_encoding : Data_encoding.t private_inner_pi :=
Data_encoding.conv
(fun (function_parameter : private_inner_pi) ⇒
let '{|
private_inner_pi.new_state := new_state;
private_inner_pi.fees := fees
|} := function_parameter in
(new_state, fees))
(fun (function_parameter : Zk_rollup_state_repr.t × Zk_rollup_scalar.t) ⇒
let '(new_state, fees) := function_parameter in
{| private_inner_pi.new_state := new_state; private_inner_pi.fees := fees;
|}) None
(Data_encoding.obj2
(Data_encoding.req None None "new_state" Zk_rollup_state_repr.encoding)
(Data_encoding.req None None "fee" Plonk.scalar_encoding)).
Definition fee_pi_encoding : Data_encoding.t fee_pi :=
Data_encoding.conv
(fun (function_parameter : fee_pi) ⇒
let '{| fee_pi.new_state := new_state |} := function_parameter in
new_state)
(fun (new_state : Zk_rollup_state_repr.t) ⇒
{| fee_pi.new_state := new_state; |}) None
(Data_encoding.obj1
(Data_encoding.req None None "new_state" Zk_rollup_state_repr.encoding)).
Definition encoding : Data_encoding.t t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.pending_pis := pending_pis;
t.private_pis := private_pis;
t.fee_pi := fee_pi;
t.proof := proof_value
|} := function_parameter in
(pending_pis, private_pis, fee_pi, proof_value))
(fun (function_parameter :
list (string × op_pi) × list (string × private_inner_pi) × fee_pi ×
Plonk.proof) ⇒
let '(pending_pis, private_pis, fee_pi, proof_value) := function_parameter
in
{| t.pending_pis := pending_pis; t.private_pis := private_pis;
t.fee_pi := fee_pi; t.proof := proof_value; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "pending_pis"
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.string_value op_pi_encoding)))
(Data_encoding.req None None "private_pis"
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.string_value
private_inner_pi_encoding)))
(Data_encoding.req None None "fee_pi" fee_pi_encoding)
(Data_encoding.req None None "proof" Plonk.proof_encoding)).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_scalar.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Module op_pi.
Record record : Set := Build {
new_state : Zk_rollup_state_repr.t;
fee : Zk_rollup_scalar.t;
exit_validity : bool;
}.
Definition with_new_state new_state (r : record) :=
Build new_state r.(fee) r.(exit_validity).
Definition with_fee fee (r : record) :=
Build r.(new_state) fee r.(exit_validity).
Definition with_exit_validity exit_validity (r : record) :=
Build r.(new_state) r.(fee) exit_validity.
End op_pi.
Definition op_pi := op_pi.record.
Module private_inner_pi.
Record record : Set := Build {
new_state : Zk_rollup_state_repr.t;
fees : Zk_rollup_scalar.t;
}.
Definition with_new_state new_state (r : record) :=
Build new_state r.(fees).
Definition with_fees fees (r : record) :=
Build r.(new_state) fees.
End private_inner_pi.
Definition private_inner_pi := private_inner_pi.record.
Module fee_pi.
Record record : Set := Build {
new_state : Zk_rollup_state_repr.t;
}.
Definition with_new_state new_state (r : record) :=
Build new_state.
End fee_pi.
Definition fee_pi := fee_pi.record.
Module t.
Record record : Set := Build {
pending_pis : list (string × op_pi);
private_pis : list (string × private_inner_pi);
fee_pi : fee_pi;
proof : Plonk.proof;
}.
Definition with_pending_pis pending_pis (r : record) :=
Build pending_pis r.(private_pis) r.(fee_pi) r.(proof).
Definition with_private_pis private_pis (r : record) :=
Build r.(pending_pis) private_pis r.(fee_pi) r.(proof).
Definition with_fee_pi fee_pi (r : record) :=
Build r.(pending_pis) r.(private_pis) fee_pi r.(proof).
Definition with_proof proof (r : record) :=
Build r.(pending_pis) r.(private_pis) r.(fee_pi) proof.
End t.
Definition t := t.record.
Definition op_pi_encoding : Data_encoding.t op_pi :=
Data_encoding.conv
(fun (function_parameter : op_pi) ⇒
let '{|
op_pi.new_state := new_state;
op_pi.fee := fee;
op_pi.exit_validity := exit_validity
|} := function_parameter in
(new_state, fee, exit_validity))
(fun (function_parameter :
Zk_rollup_state_repr.t × Zk_rollup_scalar.t × bool) ⇒
let '(new_state, fee, exit_validity) := function_parameter in
{| op_pi.new_state := new_state; op_pi.fee := fee;
op_pi.exit_validity := exit_validity; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "new_state" Zk_rollup_state_repr.encoding)
(Data_encoding.req None None "fee" Plonk.scalar_encoding)
(Data_encoding.req None None "exit_validity" Data_encoding.bool_value)).
Definition private_inner_pi_encoding : Data_encoding.t private_inner_pi :=
Data_encoding.conv
(fun (function_parameter : private_inner_pi) ⇒
let '{|
private_inner_pi.new_state := new_state;
private_inner_pi.fees := fees
|} := function_parameter in
(new_state, fees))
(fun (function_parameter : Zk_rollup_state_repr.t × Zk_rollup_scalar.t) ⇒
let '(new_state, fees) := function_parameter in
{| private_inner_pi.new_state := new_state; private_inner_pi.fees := fees;
|}) None
(Data_encoding.obj2
(Data_encoding.req None None "new_state" Zk_rollup_state_repr.encoding)
(Data_encoding.req None None "fee" Plonk.scalar_encoding)).
Definition fee_pi_encoding : Data_encoding.t fee_pi :=
Data_encoding.conv
(fun (function_parameter : fee_pi) ⇒
let '{| fee_pi.new_state := new_state |} := function_parameter in
new_state)
(fun (new_state : Zk_rollup_state_repr.t) ⇒
{| fee_pi.new_state := new_state; |}) None
(Data_encoding.obj1
(Data_encoding.req None None "new_state" Zk_rollup_state_repr.encoding)).
Definition encoding : Data_encoding.t t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.pending_pis := pending_pis;
t.private_pis := private_pis;
t.fee_pi := fee_pi;
t.proof := proof_value
|} := function_parameter in
(pending_pis, private_pis, fee_pi, proof_value))
(fun (function_parameter :
list (string × op_pi) × list (string × private_inner_pi) × fee_pi ×
Plonk.proof) ⇒
let '(pending_pis, private_pis, fee_pi, proof_value) := function_parameter
in
{| t.pending_pis := pending_pis; t.private_pis := private_pis;
t.fee_pi := fee_pi; t.proof := proof_value; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "pending_pis"
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.string_value op_pi_encoding)))
(Data_encoding.req None None "private_pis"
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.string_value
private_inner_pi_encoding)))
(Data_encoding.req None None "fee_pi" fee_pi_encoding)
(Data_encoding.req None None "proof" Plonk.proof_encoding)).