🇿 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.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)).