Skip to main content

🇿 Zk_rollup_account_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.

Definition SMap :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := String.compare
    |}.

Module static.
  Record record : Set := Build {
    public_parameters : Plonk.public_parameters;
    state_length : int;
    circuits_info : SMap.(Map.S.t) bool;
    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
     (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) bool) :=
  Data_encoding.conv_with_guard
    (fun (m_value : SMap.(Map.S.t) bool) ⇒
      List.of_seq (SMap.(Map.S.to_seq) m_value))
    (fun (l_value : list (String.t × bool)) ⇒
      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 Data_encoding.bool_value)).

Definition encoding : Data_encoding.encoding t :=
  let static_encoding :=
    let circuits_info_encoding :=
      Data_encoding.conv SMap.(Map.S.bindings)
        (fun (l_value : list (String.t × bool)) ⇒
          SMap.(Map.S.of_seq) (List.to_seq l_value)) None
        (Data_encoding.list_value None
          (Data_encoding.tup2 Data_encoding.string_value
            Data_encoding.bool_value)) in
    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) bool × 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)).