🦏 Sc_rollup_outbox_storage.v
Proofs
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.
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.
(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.
(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.