Skip to main content

🇿 Zk_rollup_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Zk_rollup_does_not_exist" "ZK Rollup does not exist"
      "Attempted to use a ZK rollup that has not been originated."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (x_value : Zk_rollup_repr.Address.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Rollup "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " does not exist"
                      CamlinternalFormatBasics.End_of_format)))
                "Rollup %a does not exist") Zk_rollup_repr.Address.pp x_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "rollup" Zk_rollup_repr.Address.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Zk_rollup_does_not_exist" then
            let x_value := cast Zk_rollup_repr.t payload in
            Some x_value
          else None
        end)
      (fun (x_value : Zk_rollup_repr.Address.t) ⇒
        Build_extensible "Zk_rollup_does_not_exist" Zk_rollup_repr.Address.t
          x_value) in
  Error_monad.register_error_kind Error_monad.Permanent
    "Zk_rollup_invalid_op code" "Invalid op code in append"
    "Invalid op code in append"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (oc : int) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Op code "
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  (CamlinternalFormatBasics.String_literal
                    " is not valid for this ZK Rollup"
                    CamlinternalFormatBasics.End_of_format)))
              "Op code %d is not valid for this ZK Rollup") oc))
    (Data_encoding.obj1
      (Data_encoding.req None None "op_code" Data_encoding.int31))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Zk_rollup_invalid_op_code" then
          let oc := cast int payload in
          Some oc
        else None
      end)
    (fun (oc : int) ⇒ Build_extensible "Zk_rollup_invalid_op_code" int oc).

Definition originate
  (ctxt : Raw_context.t) (static : Zk_rollup_account_repr.static)
  (init_state : Zk_rollup_state_repr.t)
  : M? (Raw_context.t × Zk_rollup_repr.Address.t × Z.t) :=
  let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
  let? address := Zk_rollup_repr.Address.from_nonce nonce_value in
  let origination_size := Constants_storage.zk_rollup_origination_size ctxt in
  let initial_account :=
    {| Zk_rollup_account_repr.t.static := static;
      Zk_rollup_account_repr.t.dynamic :=
        {| Zk_rollup_account_repr.dynamic.state := init_state;
          Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space :=
            Z.of_int origination_size;
          Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space :=
            Z.zero; |}; |} in
  let? '(ctxt, account_size) :=
    Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      ctxt address initial_account in
  let init_pl :=
    Zk_rollup_repr.Empty
      {| Zk_rollup_repr.pending_list.Empty.next_index := 0; |} in
  let? '(ctxt, pl_size) :=
    Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      ctxt address init_pl in
  let address_size := Zk_rollup_repr.Address.size_value in
  let size_value :=
    Z.of_int (((origination_size +i address_size) +i account_size) +i pl_size)
    in
  return? (ctxt, address, size_value).

Definition add_to_pending
  (ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
  (ops :
    list
      Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value))
  : M? (Raw_context.t × Z.t) :=
  let? '(ctxt, acc_value) :=
    Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      ctxt rollup in
  let? '_ :=
    List.iter_e
      (fun (function_parameter :
        Zk_rollup_operation_repr.t × option Ticket_hash_repr.t) ⇒
        let '(op, _ticket_hash_opt) := function_parameter in
        if
          (op.(Zk_rollup_operation_repr.t.op_code) i
          acc_value.(Zk_rollup_account_repr.t.static).(Zk_rollup_account_repr.static.nb_ops))
          || (op.(Zk_rollup_operation_repr.t.op_code) <i 0)
        then
          Error_monad.error_value
            (Build_extensible "Zk_rollup_invalid_op_code" int
              op.(Zk_rollup_operation_repr.t.op_code))
        else
          return? tt) ops in
  let? '(ctxt, pl) :=
    Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      ctxt rollup in
  let '(next_index, length) :=
    match pl with
    |
      Zk_rollup_repr.Empty {|
        Zk_rollup_repr.pending_list.Empty.next_index := next_index |} ⇒
      (next_index, 0)
    |
      Zk_rollup_repr.Pending {|
        Zk_rollup_repr.pending_list.Pending.next_index := next_index;
          Zk_rollup_repr.pending_list.Pending.length := length
          |} ⇒ (next_index, length)
    end in
  let? '(ctxt, next_index, length, storage_diff) :=
    List.fold_left_es
      (fun (function_parameter : Raw_context.t × int64 × int × int) ⇒
        let '(ctxt, next_index, length, storage_diff) := function_parameter in
        fun (op :
          Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.value))
          ⇒
          let? '(ctxt, new_storage_diff, _was_bound) :=
            Storage.Zk_rollup.Pending_operation.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
              (ctxt, rollup) next_index op in
          return?
            (ctxt, (Int64.succ next_index), (length +i 1),
              (new_storage_diff +i storage_diff))) (ctxt, next_index, length, 0)
      ops in
  let used_l2_operations_storage_space :=
    acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.used_l2_operations_storage_space)
    +Z (Z.of_int storage_diff) in
  let l2_operations_storage_space_to_pay :=
    Z.max Z.zero
      (used_l2_operations_storage_space -Z
      acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space))
    in
  let :=
    acc_value.(Zk_rollup_account_repr.t.dynamic).(Zk_rollup_account_repr.dynamic.paid_l2_operations_storage_space)
    +Z l2_operations_storage_space_to_pay in
  let acc_value :=
    Zk_rollup_account_repr.t.with_dynamic
      (Zk_rollup_account_repr.dynamic.with_used_l2_operations_storage_space
        used_l2_operations_storage_space
        (Zk_rollup_account_repr.dynamic.with_paid_l2_operations_storage_space
          paid_l2_operations_storage_space
          acc_value.(Zk_rollup_account_repr.t.dynamic))) acc_value in
  let pl :=
    if length =i 0 then
      Zk_rollup_repr.Empty
        {| Zk_rollup_repr.pending_list.Empty.next_index := next_index; |}
    else
      Zk_rollup_repr.Pending
        {| Zk_rollup_repr.pending_list.Pending.next_index := next_index;
          Zk_rollup_repr.pending_list.Pending.length := length; |} in
  let? '(ctxt, _diff_acc) :=
    Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      ctxt rollup acc_value in
  let? '(ctxt, _diff_pl) :=
    Storage.Zk_rollup.Pending_list.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      ctxt rollup pl in
  return? (ctxt, l2_operations_storage_space_to_pay).

Definition assert_exist
  (ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
  : M? Raw_context.t :=
  let? '(ctxt, _exists) :=
    Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
      ctxt rollup in
  let? '_ :=
    Error_monad.error_unless _exists
      (Build_extensible "Zk_rollup_does_not_exist" Zk_rollup_repr.Address.t
        rollup) in
  return? ctxt.

Definition _exists (ctxt : Raw_context.t) (rollup : Zk_rollup_repr.Address.t)
  : M? (Raw_context.t × bool) :=
  Storage.Zk_rollup.Account.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
    ctxt rollup.