Skip to main content

🦏 Sc_rollup_inbox_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_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.
The function [assert_inbox_nb_messages_in_commitment_period] is valid.
The function [serialize_external_messages] is valid.
The function [serialize_internal_message] is valid.
The function [add_external_messages] is valid.
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.