Skip to main content

Storage-specs

Gitlab

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_end idendity on

commitment_storage.mli

  • Validty of committed_amount
  • increase and decrease are 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
  • _exist implies must_exists success.
  • aloocated implies must_be_allocated success.

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
  • pred is equivalent to Z.pred
  • succ is equivalent to Z.succ
  • sub is equivalent to Z.sub
  • add is equivalent to Z.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
  • reveal implies get success and identity on revelead and getted value

stake_storage.mli

  • add_stake is equivalent to Z.add on success
  • remove_stake is equivalent to Z.sub on success
  • Validity of get_selected_distribution
  • Validity of find_selected_distribution
  • Delegate_sampler_state.get after Delegate_sampler_state.init returns the same value.
  • Delegate_sampler_state.get success implies Delegate_sampler_state.remove_existing success.

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_stake and remove_contract_stake are inverse of one each other

contract_manager_storage.mli

  • reveal_manager_key implies is_manager_key_revealed to be true
  • reveal_manager_key implies get_manager_key success
  • get_manager_key implies remove_existing success

delegate_activation_storage.mli

  • set_inactive implies is_inactive to be true
  • set_active equals true implies is_inactive to be true
  • Validity of grace_period

frozen_deposits_storage.mli

  • init implies allocated to be true
  • init implies get success
  • init implies find success
  • credit_only_call_from_token equals to Z.add (closed on non-negatives)
  • spend_only_call_from_token equals to Z.sub (closed on non-negatives)

global_constants_storage.mli

  • Identity between register and get

sc_rollup_storage.mli

  • Validity of originate

ticket_storage.mli

  • Identity between adjust_balance and get