Skip to main content

🦏 Sc_rollup_commitment_storage.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.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Module Store := Storage.Sc_rollup.

Module Commitment := Sc_rollup_commitment_repr.

Module Commitment_hash := Commitment.Hash.

Definition get_commitment_opt_unsafe
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (commitment : Sc_rollup_commitment_repr.Hash.t)
  : M? (option Sc_rollup_commitment_repr.V1.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) commitment in
  return? (res, ctxt).

Definition get_commitment_unsafe
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (commitment : Sc_rollup_commitment_repr.Hash.t)
  : M? (Sc_rollup_commitment_repr.V1.t × Raw_context.t) :=
  let? '(res, ctxt) := get_commitment_opt_unsafe ctxt rollup commitment in
  match res with
  | None
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Sc_rollup_unknown_commitment"
        Sc_rollup_commitment_repr.Hash.t commitment)
  | Some commitmentreturn? (commitment, ctxt)
  end.

Definition last_cemented_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? (Sc_rollup_commitment_repr.Hash.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Last_cemented_commitment.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt rollup in
  match res with
  | None
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some lccreturn? (lcc, ctxt)
  end.

Definition get_commitment
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (commitment : Sc_rollup_commitment_repr.Hash.t)
  : M? (Sc_rollup_commitment_repr.V1.t × Raw_context.t) :=
  let? '(_lcc, ctxt) := last_cemented_commitment ctxt rollup in
  get_commitment_unsafe ctxt rollup commitment.

Definition last_cemented_commitment_hash_with_level
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? (Sc_rollup_commitment_repr.Hash.t × Raw_level_repr.t × Raw_context.t) :=
  let? '(commitment_hash, ctxt) := last_cemented_commitment ctxt rollup in
  Error_monad.Lwt_result_syntax.op_letplus
    (get_commitment_unsafe ctxt rollup commitment_hash)
    (fun function_parameter
      let
        '({| Sc_rollup_commitment_repr.V1.t.inbox_level := inbox_level |}, ctxt) :=
        function_parameter in
      (commitment_hash, inbox_level, ctxt)).

Definition set_commitment_added
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_commitment_repr.Hash.t) (new_value : Raw_level_repr.t)
  : M? (int × Raw_level_repr.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) node_value in
  match res with
  | Some old_valuereturn? (0, old_value, ctxt)
  | None
    let? '(ctxt, size_diff, _was_bound) :=
      Store.Commitment_added.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
        (ctxt, rollup) node_value new_value in
    return? (size_diff, new_value, ctxt)
  end.

Definition get_predecessor_opt_unsafe
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_commitment_repr.Hash.t)
  : M? (option Commitment.Hash.t × Raw_context.t) :=
  let? '(commitment, ctxt) := get_commitment_opt_unsafe ctxt rollup node_value
    in
  return?
    ((Option.map
      (fun (c_value : Commitment.t) ⇒
        c_value.(Sc_rollup_commitment_repr.V1.t.predecessor)) commitment), ctxt).

Definition get_predecessor_unsafe
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (node_value : Sc_rollup_commitment_repr.Hash.t)
  : M? (Sc_rollup_commitment_repr.Hash.t × Raw_context.t) :=
  let? '(commitment, ctxt) := get_commitment_unsafe ctxt rollup node_value in
  return? (commitment.(Sc_rollup_commitment_repr.V1.t.predecessor), ctxt).

Definition hash_value
  (ctxt : Raw_context.t) (commitment : Sc_rollup_commitment_repr.t)
  : M? (Raw_context.t × Sc_rollup_commitment_repr.Hash.t) :=
  let? ctxt :=
    Raw_context.consume_gas ctxt
      Sc_rollup_costs.Constants.cost_serialize_commitment in
  let commitment_bytes_opt :=
    Data_encoding.Binary.to_bytes_opt None Sc_rollup_commitment_repr.encoding
      commitment in
  let? commitment_bytes :=
    Option.to_result
      (Error_monad.trace_of_error
        (Build_extensible "Sc_rollup_bad_commitment_serialization" unit tt))
      commitment_bytes_opt in
  let bytes_len := Bytes.length commitment_bytes in
  let? ctxt :=
    Raw_context.consume_gas ctxt (Sc_rollup_costs.cost_hash_bytes bytes_len) in
  return?
    (ctxt, (Sc_rollup_commitment_repr.Hash.hash_bytes None [ commitment_bytes ])).