🇿 Zk_rollup_update_repr.v

Translated OCaml

Gitlab , 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)).