🦏 Sc_rollup_outbox_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [level_index] is valid.

Lemma level_index_is_valid ctxt level
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_level : Raw_level_repr.Valid.t level) :
  Int32.Valid.t (Sc_rollup_outbox_storage.level_index ctxt level).
Proof.
Admitted.

The function [record_applied_message] is valid.

Lemma record_applied_message_is_valid ctxt rollup level message_index
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_level : Raw_level_repr.Valid.t level)
  (H_message_index : Pervasives.Int.Valid.t message_index) :
  letP? '(_, ctxt) :=
    Sc_rollup_outbox_storage.record_applied_message
      ctxt rollup level message_index in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.