🐆 Tx_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.Tx_rollup_inbox_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_state_repr.

The function [find] is valid.

Lemma find_is_valid ctxt level tx_rollup :
  Raw_context.Valid.t ctxt →
  Tx_rollup_level_repr.Valid.t level →
  letP? '(ctxt, inbox) := Tx_rollup_inbox_storage.find ctxt level tx_rollup in
  Raw_context.Valid.t ctxt ∧
  Option.Forall Tx_rollup_inbox_repr.Valid.t inbox.
Proof.
Admitted.

The function [get] is valid.

Lemma get_is_valid ctxt level tx_rollup :
  Raw_context.Valid.t ctxt →
  Tx_rollup_level_repr.Valid.t level →
  letP? '(ctxt, inbox) := Tx_rollup_inbox_storage.get ctxt level tx_rollup in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_inbox_repr.Valid.t inbox.
Proof.
Admitted.

The function [prepare_inbox] is valid.

Lemma prepare_inbox_is_valid ctxt rollup state_value level :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Raw_level_repr.Valid.t level →
  letP? '(ctxt, state, level, inbox, _) :=
    Tx_rollup_inbox_storage.prepare_inbox ctxt rollup state_value level in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state ∧
  Raw_level_repr.Valid.t level ∧
  Tx_rollup_inbox_repr.Valid.t inbox.
Proof.
Admitted.

The function [update_inbox] is valid.

Lemma update_inbox_is_valid metadata msg_size merkle_root :
  Tx_rollup_inbox_repr.Valid.t metadata →
  Pervasives.Int.Valid.t msg_size →
  Tx_rollup_inbox_repr.Valid.t (
    Tx_rollup_inbox_storage.update_inbox metadata msg_size merkle_root
  ).
Proof.
Admitted.

The function [append_message] is valid.

Lemma append_message_is_valid ctxt rollup state_value message :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_message_repr.Valid.t message →
  letP? '(ctxt, state, _) :=
    Tx_rollup_inbox_storage.append_message ctxt rollup state_value message in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.

The function [remove] is valid.

Lemma remove_is_valid ctxt level rollup :
  Raw_context.Valid.t ctxt →
  Raw_level_repr.Valid.t level →
  letP? ctxt := Tx_rollup_inbox_storage.remove ctxt level rollup in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [check_message_hash] is valid.

Lemma check_message_hash_is_valid ctxt level tx_rollup position message path :
  Raw_context.Valid.t ctxt →
  Tx_rollup_level_repr.Valid.t level →
  Pervasives.Int.Valid.t position →
  Tx_rollup_message_repr.Valid.t message →
  letP? ctxt :=
    Tx_rollup_inbox_storage.check_message_hash ctxt level tx_rollup position message path in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.