🐆 Tx_rollup_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.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.

Definition fresh_tx_rollup_from_current_nonce (ctxt : Raw_context.t)
  : M? (Raw_context.t × Tx_rollup_repr.t) :=
  let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
  return? (ctxt, (Tx_rollup_repr.originated_tx_rollup nonce_value)).

Definition originate (ctxt : Raw_context.t)
  : M? (Raw_context.t × Tx_rollup_repr.t) :=
  let? '(ctxt, tx_rollup) := fresh_tx_rollup_from_current_nonce ctxt in
  let? ctxt := Tx_rollup_state_storage.init_value ctxt tx_rollup in
  return? (ctxt, tx_rollup).