🐆 Tx_rollup_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [fresh_tx_rollup_from_current_nonce] is valid.

Lemma fresh_tx_rollup_from_current_nonce_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) :=
    Tx_rollup_storage.fresh_tx_rollup_from_current_nonce ctxt in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [originate] is valid.

Lemma originate_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Tx_rollup_storage.originate ctxt in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.