🦏 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.

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.

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.

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.

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.

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.

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.

Lemma add_internal_message_is_valid ctxt internal_message
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP ? ' (inbox_repr , z , ctxt ) :=
    Sc_rollup_inbox_storage.add_internal_message
      ctxt internal_message in
  Int64.Valid.non_negative z ∧
  Raw_context.Valid.t ctxt.
Proof.
Admitted.