Storage-specs
Storage specs
Here we go through each _storage.mli file and list what should be verified.
The techniques of such verifcation can be
found on the milestone
bootstrap_storage.mli​
cycle_endidendity on
commitment_storage.mli​
- Validty of
committed_amount increaseanddecreaseare inverse of each other
constants_storage.mli​
- Validity of
hard_gas_limit_per_operation - Validity of
hard_gas_limit_per_block - Validity of
cost_per_byte - Validity of
tokens_per_roll_is_valid - Validity of
seed_nonce_revelation_tip - Validity of
baking_reward_fixed_portion - Validity of
baking_reward_bonus_per_slot - Validity of
endorsing_reward_per_slot - Validity of
liquidity_baking_subsidy - Validity of
parametric_value - Validity of
minimal_participation_ratio - Validity of
double_baking_punishment - Validity of
ratio_of_frozen_deposits_slashed_per_double_endorsement - Validity of
minimal_block_delay - Validity of
delay_increment_per_round
contract_storage.mli​
- Validity of
Legacy_big_map_diff.item_encoding - Validity of
Legacy_big_map_diff.encoding _existimpliesmust_existssuccess.aloocatedimpliesmust_be_allocatedsuccess.
delegate_storage.mli​
- Validity of
frozen_deposits_limit - Validity of
balance - Validity of
record_baking_activity_and_pay_rewards_and_fees - Validity of
full_balance - Validity of
staking_balance - Validity of
delegated_balance - Validity of
freeze_deposits_do_not_call_except_for_migration
fees_storage.mli​
- Validity of
record_global_constant_storage_space - Validity of
record_paid_storage_space - Validity of
check_storage_limit - Validity of
burn_storage_fees
level_storage.mli​
- Validity of
current - Validity of
previous - Validity of
root - Validity of
from_raw - Validity of
from_raw_with_offset predis equivalent toZ.predsuccis equivalent toZ.succsubis equivalent toZ.subaddis equivalent toZ.add- Validity of
pred - Validity of
succ - Validity of
add - Validity of
sub - Validity of
first_level_in_cycle - Validity of
last_level_in_cycle - Validity of
levels_in_cycle - Validity of
levels_in_current_cycle - Validity of
levels_with_commitments_in_cycle - Validity of
last_allowed_fork_level - Validity of
dawn_of_a_new_cycle
nonce_storage.mli​
- Validity of
encoding - Validity of
get revealimpliesgetsuccess and identity on revelead and getted value
stake_storage.mli​
add_stakeis equivalent toZ.addon successremove_stakeis equivalent toZ.subon success- Validity of
get_selected_distribution - Validity of
find_selected_distribution Delegate_sampler_state.getafterDelegate_sampler_state.initreturns the same value.Delegate_sampler_state.getsuccess impliesDelegate_sampler_state.remove_existingsuccess.
seed_storage.mli​
- Validity of
for_cycle
vote_storage.mli​
- Validity of
ballots_encoding - Validity of
listings_encoding
voting_period_storage.mli​
- Validity of
get_current
contract_delegate_storage.mli​
add_contract_stakeandremove_contract_stakeare inverse of one each other
contract_manager_storage.mli​
reveal_manager_keyimpliesis_manager_key_revealedto be truereveal_manager_keyimpliesget_manager_keysuccessget_manager_keyimpliesremove_existingsuccess
delegate_activation_storage.mli​
set_inactiveimpliesis_inactiveto be trueset_activeequalstrueimpliesis_inactiveto be true- Validity of
grace_period
frozen_deposits_storage.mli​
initimpliesallocatedto be trueinitimpliesgetsuccessinitimpliesfindsuccesscredit_only_call_from_tokenequals to Z.add (closed on non-negatives)spend_only_call_from_tokenequals to Z.sub (closed on non-negatives)
global_constants_storage.mli​
- Identity between
registerandget
sc_rollup_storage.mli​
- Validity of
originate
ticket_storage.mli​
- Identity between
adjust_balanceandget