🐆 Tx_rollup_commitment_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_commitment_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_state_repr.

The function [check_message_result] is valid.

Lemma check_message_result_is_valid ctxt param result_value path index_value :
  Raw_context.Valid.t ctxt →
  Pervasives.Int.Valid.t index_value →
  letP? ctxt :=
    Tx_rollup_commitment_storage.check_message_result ctxt param result_value path index_value in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [adjust_commitments_count] is valid.

Lemma adjust_commitments_count_is_valid ctxt tx_rollup pkh dir :
  Raw_context.Valid.t ctxt →
  letP? ctxt :=
    Tx_rollup_commitment_storage.adjust_commitments_count ctxt tx_rollup pkh dir in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [remove_bond] is valid.

Lemma remove_bond_is_valid ctxt tx_rollup contract :
  Raw_context.Valid.t ctxt →
  letP? ctxt :=
    Tx_rollup_commitment_storage.remove_bond ctxt tx_rollup contract in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [slash_bond] is valid.

Lemma slash_bond_is_valid ctxt tx_rollup contract :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) :=
    Tx_rollup_commitment_storage.slash_bond ctxt tx_rollup contract in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [find] is valid.

Lemma find_is_valid ctxt tx_rollup state_value level :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_level_repr.Valid.t level →
  letP? '(ctxt, _) :=
    Tx_rollup_commitment_storage.find ctxt tx_rollup state_value level in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [get] is valid.

Lemma get_is_valid ctxt tx_rollup state_value level :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_level_repr.Valid.t level →
  letP? '(ctxt, _) :=
    Tx_rollup_commitment_storage.get ctxt tx_rollup state_value level in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [get_finalized] is valid.

Lemma get_finalized_is_valid ctxt tx_rollup state_value level :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_level_repr.Valid.t level →
  letP? '(ctxt, _) :=
    Tx_rollup_commitment_storage.get_finalized ctxt tx_rollup state_value level in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [check_commitment_level] is valid.

Lemma check_commitment_level_is_valid {A} current_level state_value commitment :
  Raw_level_repr.Valid.t current_level →
  Tx_rollup_state_repr.Valid.t state_value →
  letP? _ :=
    Tx_rollup_commitment_storage.check_commitment_level (A := A)
      current_level state_value commitment in
  True.
Proof.
Admitted.

The function [check_commitment_predecessor] is valid.

Lemma check_commitment_predecessor_is_valid {B} ctxt state_value commitment :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  letP? ctxt :=
    Tx_rollup_commitment_storage.check_commitment_predecessor (B := B)
      ctxt state_value commitment in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [check_commitment_batches_and_merkle_root] is valid.

Lemma check_commitment_batches_and_merkle_root_is_valid {C}
  ctxt state_value inbox_value commitment :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_inbox_repr.Valid.t inbox_value →
  letP? '(ctxt, state) :=
    Tx_rollup_commitment_storage.check_commitment_batches_and_merkle_root
      (C := C)
      ctxt state_value inbox_value commitment in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.

The function [add_commitment] is valid.

Lemma add_commitment_is_valid ctxt tx_rollup state_value pkh commitment :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  letP? '(ctxt, state, _) :=
    Tx_rollup_commitment_storage.add_commitment
      ctxt tx_rollup state_value pkh commitment in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.

The function [pending_bonded_commitments] is valid.

Lemma pending_bonded_commitments_is_valid ctxt tx_rollup pkh :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, pending) :=
    Tx_rollup_commitment_storage.pending_bonded_commitments
      ctxt tx_rollup pkh in
  Raw_context.Valid.t ctxt ∧
  Pervasives.Int.Valid.t pending.
Proof.
Admitted.

The function [has_bond] is valid.

Lemma has_bond_is_valid ctxt tx_rollup pkh :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) :=
    Tx_rollup_commitment_storage.has_bond ctxt tx_rollup pkh in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [finalize_commitment] is valid.

Lemma finalize_commitment_is_valid ctxt rollup state_value :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  letP? '(ctxt, state, level) :=
    Tx_rollup_commitment_storage.finalize_commitment ctxt rollup state_value in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state ∧
  Tx_rollup_level_repr.Valid.t level.
Proof.
Admitted.

The function [remove_commitment] is valid.

Lemma remove_commitment_is_valid ctxt rollup state_value :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  letP? '(ctxt, state, level) :=
    Tx_rollup_commitment_storage.remove_commitment ctxt rollup state_value in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state ∧
  Tx_rollup_level_repr.Valid.t level.
Proof.
Admitted.

The function [check_agreed_and_disputed_results] is valid.

Lemma check_agreed_and_disputed_results_is_valid
  ctxt tx_rollup state_value submitted_commitment agreed_result
  agreed_result_path disputed_result disputed_position disputed_result_path :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Pervasives.Int.Valid.t disputed_position →
  letP? ctxt :=
    Tx_rollup_commitment_storage.check_agreed_and_disputed_results
      ctxt tx_rollup state_value submitted_commitment agreed_result
      agreed_result_path disputed_result disputed_position
      disputed_result_path in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [reject_commitment] is valid.

Lemma reject_commitment_is_valid ctxt rollup state_value level :
  Raw_context.Valid.t ctxt →
  Tx_rollup_state_repr.Valid.t state_value →
  Tx_rollup_level_repr.Valid.t level →
  letP? '(ctxt, state) :=
    Tx_rollup_commitment_storage.reject_commitment
      ctxt rollup state_value level in
  Raw_context.Valid.t ctxt ∧
  Tx_rollup_state_repr.Valid.t state.
Proof.
Admitted.