🦏 Sc_rollup_stake_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
The function [find_staker_unsafe] is valid.
Lemma find_staker_unsafe_is_valid ctxt rollup staker
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_stake_storage.find_staker_unsafe ctxt rollup staker in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_stake_storage.find_staker_unsafe ctxt rollup staker in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [find_staker] is valid.
Lemma find_staker_is_valid ctxt rollup staker
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_stake_storage.find_staker ctxt rollup staker in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_stake_storage.find_staker ctxt rollup staker in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [modify_staker_count] is valid.
Lemma modify_staker_count_is_valid ctxt rollup f
(H_ctxt : Raw_context.Valid.t ctxt)
(H_f : ∀ i,
Int32.Valid.t i →
Int32.Valid.t (f i)
) :
letP? ctxt :=
Sc_rollup_stake_storage.modify_staker_count ctxt rollup f in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_f : ∀ i,
Int32.Valid.t i →
Int32.Valid.t (f i)
) :
letP? ctxt :=
Sc_rollup_stake_storage.modify_staker_count ctxt rollup f in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_contract_and_stake] is valid.
Lemma get_contract_and_stake_is_valid ctxt staker
(H_ctxt : Raw_context.Valid.t ctxt) :
let '(_, stake) :=
Sc_rollup_stake_storage.get_contract_and_stake ctxt staker in
Tez_repr.Valid.t stake.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
let '(_, stake) :=
Sc_rollup_stake_storage.get_contract_and_stake ctxt staker in
Tez_repr.Valid.t stake.
Proof.
Admitted.
The function [deposit_stake] is valid.
Lemma deposit_stake_is_valid ctxt rollup staker
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, updates, _) :=
Sc_rollup_stake_storage.deposit_stake ctxt rollup staker in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, updates, _) :=
Sc_rollup_stake_storage.deposit_stake ctxt rollup staker in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.
The function [withdraw_stake] is valid.
Lemma withdraw_stake_is_valid ctxt rollup staker
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, updates) :=
Sc_rollup_stake_storage.withdraw_stake ctxt rollup staker in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, updates) :=
Sc_rollup_stake_storage.withdraw_stake ctxt rollup staker in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.
The function [assert_commitment_not_too_far_ahead] is valid.
Lemma assert_commitment_not_too_far_ahead_is_valid ctxt rollup lcc commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.assert_commitment_not_too_far_ahead
ctxt rollup lcc commitment in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.assert_commitment_not_too_far_ahead
ctxt rollup lcc commitment in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [assert_commitment_period] is valid.
Lemma assert_commitment_period_is_valid ctxt rollup commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.assert_commitment_period ctxt rollup commitment in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.assert_commitment_period ctxt rollup commitment in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [assert_refine_conditions_met] is valid.
Lemma assert_refine_conditions_met_is_valid ctxt rollup lcc commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.assert_refine_conditions_met
ctxt rollup lcc commitment in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.assert_refine_conditions_met
ctxt rollup lcc commitment in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_commitment_stake_count] is valid.
Lemma get_commitment_stake_count_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(stake_count, ctxt) :=
Sc_rollup_stake_storage.get_commitment_stake_count ctxt rollup node_value in
Int32.Valid.t stake_count ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(stake_count, ctxt) :=
Sc_rollup_stake_storage.get_commitment_stake_count ctxt rollup node_value in
Int32.Valid.t stake_count ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [modify_commitment_stake_count] is valid.
Lemma modify_commitment_stake_count_is_valid ctxt rollup node_value f
(H_ctxt : Raw_context.Valid.t ctxt)
(H_f : ∀ i,
Int32.Valid.t i →
Int32.Valid.t (f i)
) :
letP? '(new_count, diff, ctxt) :=
Sc_rollup_stake_storage.modify_commitment_stake_count
ctxt rollup node_value f in
Int32.Valid.t new_count ∧
Pervasives.Int.Valid.t diff ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_f : ∀ i,
Int32.Valid.t i →
Int32.Valid.t (f i)
) :
letP? '(new_count, diff, ctxt) :=
Sc_rollup_stake_storage.modify_commitment_stake_count
ctxt rollup node_value f in
Int32.Valid.t new_count ∧
Pervasives.Int.Valid.t diff ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [deallocate_commitment] is valid.
Lemma deallocate_commitment_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.deallocate_commitment ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.deallocate_commitment ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [deallocate_commitment_metadata] is valid.
Lemma deallocate_commitment_metadata_is_valid ctxt rollup metadata
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.deallocate_commitment_metadata
ctxt rollup metadata in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.deallocate_commitment_metadata
ctxt rollup metadata in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [deallocate] is valid.
Lemma deallocate_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.deallocate ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.deallocate ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [find_commitment_to_deallocate] is valid.
Lemma find_commitment_to_deallocate_is_valid
ctxt rollup commitment_hash num_commitments_to_keep
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_stake_storage.find_commitment_to_deallocate
ctxt rollup commitment_hash num_commitments_to_keep in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
ctxt rollup commitment_hash num_commitments_to_keep
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_stake_storage.find_commitment_to_deallocate
ctxt rollup commitment_hash num_commitments_to_keep in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [decrease_commitment_stake_count] is valid.
Lemma decrease_commitment_stake_count_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.decrease_commitment_stake_count
ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? ctxt :=
Sc_rollup_stake_storage.decrease_commitment_stake_count
ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [increase_commitment_stake_count] is valid.
Lemma increase_commitment_stake_count_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(diff, ctxt) :=
Sc_rollup_stake_storage.increase_commitment_stake_count
ctxt rollup node_value in
Pervasives.Int.Valid.t diff ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(diff, ctxt) :=
Sc_rollup_stake_storage.increase_commitment_stake_count
ctxt rollup node_value in
Pervasives.Int.Valid.t diff ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [refine_stake] is valid.
Lemma refine_stake_is_valid ctxt rollup staker staked_on commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, level, ctxt) :=
Sc_rollup_stake_storage.refine_stake
ctxt rollup staker staked_on commitment in
Raw_level_repr.Valid.t level ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, level, ctxt) :=
Sc_rollup_stake_storage.refine_stake
ctxt rollup staker staked_on commitment in
Raw_level_repr.Valid.t level ∧
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [publish_commitment] is valid.
Lemma publish_commitment_is_valid ctxt rollup staker commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, level, ctxt, updates) :=
Sc_rollup_stake_storage.publish_commitment ctxt rollup staker commitment in
Raw_level_repr.Valid.t level ∧
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, level, ctxt, updates) :=
Sc_rollup_stake_storage.publish_commitment ctxt rollup staker commitment in
Raw_level_repr.Valid.t level ∧
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.
The function [cement_commitment] is valid.
Lemma cement_commitment_is_valid ctxt rollup new_lcss
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, _) :=
Sc_rollup_stake_storage.cement_commitment ctxt rollup new_lcss in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, _) :=
Sc_rollup_stake_storage.cement_commitment ctxt rollup new_lcss in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [remove_staker] is valid.