🐆 Tx_rollup_commitment_storage.v
Proofs
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.