🇿 Zk_rollup_circuit_public_inputs_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_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_scalar.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.

Module pending_op_public_inputs.
  Record record : Set := Build {
    old_state : Zk_rollup_state_repr.t;
    new_state : Zk_rollup_state_repr.t;
    fee : Zk_rollup_scalar.t;
    exit_validity : bool;
    zk_rollup : Zk_rollup_repr.t;
    l2_op : Zk_rollup_operation_repr.t;
  }.
  Definition with_old_state old_state (r : record) :=
    Build old_state r.(new_state) r.(fee) r.(exit_validity) r.(zk_rollup)
      r.(l2_op).
  Definition with_new_state new_state (r : record) :=
    Build r.(old_state) new_state r.(fee) r.(exit_validity) r.(zk_rollup)
      r.(l2_op).
  Definition with_fee fee (r : record) :=
    Build r.(old_state) r.(new_state) fee r.(exit_validity) r.(zk_rollup)
      r.(l2_op).
  Definition with_exit_validity exit_validity (r : record) :=
    Build r.(old_state) r.(new_state) r.(fee) exit_validity r.(zk_rollup)
      r.(l2_op).
  Definition with_zk_rollup zk_rollup (r : record) :=
    Build r.(old_state) r.(new_state) r.(fee) r.(exit_validity) zk_rollup
      r.(l2_op).
  Definition with_l2_op l2_op (r : record) :=
    Build r.(old_state) r.(new_state) r.(fee) r.(exit_validity) r.(zk_rollup)
      l2_op.
End pending_op_public_inputs.
Definition pending_op_public_inputs := pending_op_public_inputs.record.

Module private_batch_public_inputs.
  Record record : Set := Build {
    old_state : Zk_rollup_state_repr.t;
    new_state : Zk_rollup_state_repr.t;
    fees : Zk_rollup_scalar.t;
    zk_rollup : Zk_rollup_repr.t;
  }.
  Definition with_old_state old_state (r : record) :=
    Build old_state r.(new_state) r.(fees) r.(zk_rollup).
  Definition with_new_state new_state (r : record) :=
    Build r.(old_state) new_state r.(fees) r.(zk_rollup).
  Definition with_fees fees (r : record) :=
    Build r.(old_state) r.(new_state) fees r.(zk_rollup).
  Definition with_zk_rollup zk_rollup (r : record) :=
    Build r.(old_state) r.(new_state) r.(fees) zk_rollup.
End private_batch_public_inputs.
Definition private_batch_public_inputs := private_batch_public_inputs.record.

Module fee_public_inputs.
  Record record : Set := Build {
    old_state : Zk_rollup_state_repr.t;
    new_state : Zk_rollup_state_repr.t;
    fees : Zk_rollup_scalar.t;
  }.
  Definition with_old_state old_state (r : record) :=
    Build old_state r.(new_state) r.(fees).
  Definition with_new_state new_state (r : record) :=
    Build r.(old_state) new_state r.(fees).
  Definition with_fees fees (r : record) :=
    Build r.(old_state) r.(new_state) fees.
End fee_public_inputs.
Definition fee_public_inputs := fee_public_inputs.record.

Inductive t : Set :=
| Pending_op : pending_op_public_inputs → t
| Private_batch : private_batch_public_inputs → t
| Fee : fee_public_inputs → t.

Definition bool_to_scalar (b_value : bool) : Zk_rollup_scalar.t :=
  if b_value then
    Zk_rollup_scalar.of_z Z.one
  else
    Zk_rollup_scalar.of_z Z.zero.

Definition to_scalar_array (function_parameter : t)
  : Array.t Zk_rollup_scalar.t :=
  match function_parameter with
  |
    Pending_op {|
      pending_op_public_inputs.old_state := old_state;
        pending_op_public_inputs.new_state := new_state;
        pending_op_public_inputs.fee := fee;
        pending_op_public_inputs.exit_validity := exit_validity;
        pending_op_public_inputs.zk_rollup := zk_rollup;
        pending_op_public_inputs.l2_op := l2_op
        |} ⇒
    Array.concat
      [
        old_state;
        new_state;
        (* ❌ Arrays not handled. *)
        [ fee; bool_to_scalar exit_validity; Zk_rollup_repr.to_scalar zk_rollup ];
        Zk_rollup_operation_repr.to_scalar_array l2_op
      ]
  |
    Private_batch {|
      private_batch_public_inputs.old_state := old_state;
        private_batch_public_inputs.new_state := new_state;
        private_batch_public_inputs.fees := fees;
        private_batch_public_inputs.zk_rollup := zk_rollup
        |} ⇒
    Array.concat
      [
        old_state;
        new_state;
        (* ❌ Arrays not handled. *)
        [ fees; Zk_rollup_repr.to_scalar zk_rollup ]
      ]
  |
    Fee {|
      fee_public_inputs.old_state := old_state;
        fee_public_inputs.new_state := new_state;
        fee_public_inputs.fees := fees
        |} ⇒
    Array.concat
      [
        old_state;
        new_state;
        (* ❌ Arrays not handled. *)
        [ fees ]
      ]
  end.