🐆 Tx_rollup_reveal_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
The function [record] is valid.
Lemma record_is_valid ctxt tx_rollup level message_position :
Raw_context.Valid.t ctxt →
Tx_rollup_level_repr.Valid.t level →
Pervasives.Int.Valid.t message_position →
letP? ctxt :=
Tx_rollup_reveal_storage.record ctxt tx_rollup level message_position in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tx_rollup_level_repr.Valid.t level →
Pervasives.Int.Valid.t message_position →
letP? ctxt :=
Tx_rollup_reveal_storage.record ctxt tx_rollup level message_position in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [mem] is valid.
Lemma mem_is_valid ctxt tx_rollup level message_position :
Raw_context.Valid.t ctxt →
Tx_rollup_level_repr.Valid.t level →
Pervasives.Int.Valid.t message_position →
letP? '(ctxt, _) :=
Tx_rollup_reveal_storage.mem ctxt tx_rollup level message_position in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tx_rollup_level_repr.Valid.t level →
Pervasives.Int.Valid.t message_position →
letP? '(ctxt, _) :=
Tx_rollup_reveal_storage.mem ctxt tx_rollup level message_position in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [remove] is valid.
Lemma remove_is_valid ctxt tx_rollup level :
Raw_context.Valid.t ctxt →
Tx_rollup_level_repr.Valid.t level →
letP? ctxt := Tx_rollup_reveal_storage.remove ctxt tx_rollup level in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tx_rollup_level_repr.Valid.t level →
letP? ctxt := Tx_rollup_reveal_storage.remove ctxt tx_rollup level in
Raw_context.Valid.t ctxt.
Proof.
Admitted.