Skip to main content

🦏 Sc_rollup_stake_storage.v

Proofs

See code, Gitlab , OCaml

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.

The function [find_staker_unsafe] is valid.
The function [find_staker] is valid.
The function [modify_staker_count] is valid.
The function [get_contract_and_stake] is valid.
The function [deposit_stake] is valid.
The function [withdraw_stake] is valid.
The function [assert_commitment_not_too_far_ahead] is valid.
The function [assert_commitment_period] is valid.
The function [assert_refine_conditions_met] is valid.
The function [get_commitment_stake_count] is valid.
The function [modify_commitment_stake_count] is valid.
The function [deallocate_commitment] is valid.
The function [deallocate_commitment_metadata] is valid.
The function [deallocate] is valid.
The function [find_commitment_to_deallocate] is valid.
The function [decrease_commitment_stake_count] is valid.
The function [increase_commitment_stake_count] is valid.
The function [refine_stake] is valid.
The function [publish_commitment] is valid.
The function [cement_commitment] is valid.
The function [remove_staker] is valid.