🦏 Sc_rollup_inbox_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_repr.
The function [update_num_and_size_of_messages] is valid.
Lemma update_num_and_size_of_messages_is_valid
num_messages total_messages_size message :
let '(num, size) :=
Sc_rollup_inbox_storage.update_num_and_size_of_messages
num_messages total_messages_size message in
Pervasives.Int.Valid.t num ∧
Pervasives.Int.Valid.t size.
Proof.
unfold Sc_rollup_inbox_storage.update_num_and_size_of_messages.
split; lia.
Qed.
num_messages total_messages_size message :
let '(num, size) :=
Sc_rollup_inbox_storage.update_num_and_size_of_messages
num_messages total_messages_size message in
Pervasives.Int.Valid.t num ∧
Pervasives.Int.Valid.t size.
Proof.
unfold Sc_rollup_inbox_storage.update_num_and_size_of_messages.
split; lia.
Qed.
The function [assert_inbox_nb_messages_in_commitment_period] is valid.
Lemma _assert_inbox_nb_messages_in_commitment_period_is_valid
ctxt inbox_value extra_messages
(H_ctxt : Raw_context.Valid.t ctxt)
(* (H_inbox_repr : Sc_rollup_inbox_repr.Valid.t inbox_value) *)
(H_extra_message : Pervasives.Int.Valid.t extra_messages) :
letP? _ :=
Sc_rollup_inbox_storage._assert_inbox_nb_messages_in_commitment_period
ctxt inbox_value extra_messages in
True.
Proof.
Admitted.
ctxt inbox_value extra_messages
(H_ctxt : Raw_context.Valid.t ctxt)
(* (H_inbox_repr : Sc_rollup_inbox_repr.Valid.t inbox_value) *)
(H_extra_message : Pervasives.Int.Valid.t extra_messages) :
letP? _ :=
Sc_rollup_inbox_storage._assert_inbox_nb_messages_in_commitment_period
ctxt inbox_value extra_messages in
True.
Proof.
Admitted.
The function [serialize_external_messages] is valid.
Lemma serialize_external_messages_is_valid ctxt external_messages
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, _) :=
Sc_rollup_inbox_storage.serialize_external_messages
ctxt external_messages in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, _) :=
Sc_rollup_inbox_storage.serialize_external_messages
ctxt external_messages in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [serialize_internal_message] is valid.
Lemma serialize_internal_message_is_valid ctxt internal_message
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_inbox_storage.serialize_internal_message
ctxt internal_message in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_inbox_storage.serialize_internal_message
ctxt internal_message in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [add_external_messages] is valid.
Lemma add_external_messages_is_valid ctxt external_messages
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(inbox, _, ctxt) :=
Sc_rollup_inbox_storage.add_external_messages
ctxt external_messages in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(inbox, _, ctxt) :=
Sc_rollup_inbox_storage.add_external_messages
ctxt external_messages in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [add_internal_message] is valid Validity pre- and post-conditions should be checked, in particular
regarding [z], which is specified as a size diff in the mli file.
It then must be positive since the function *adds* a message when
it succeeds. But it may even also be only equal only to 0 or 1,
depending on the notion of size diff here.