🐣 Bootstrap_storage.v

Proofs

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bootstrap_storage.

Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

The function [init_account] is valid.

Lemma init_account_is_valid ctxt updates account :
  Raw_context.Valid.t ctxt →
  Receipt_repr.balance_updates.Valid.t updates →
  Parameters_repr.bootstrap_account.Valid.t account →
  letP ? '(ctxt , updates ) :=
    Bootstrap_storage.init_account (ctxt, updates) account in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

[init_account] with no public key and zero amount is an identity

Lemma init_account_identity ctxt public_key_hash :
  let bootstrap_account := {|
    Parameters_repr.bootstrap_account.public_key_hash := public_key_hash;
    Parameters_repr.bootstrap_account.public_key := None;
    Parameters_repr.bootstrap_account.amount := Tez_repr.zero;
    Parameters_repr.bootstrap_account.delegate_to := None;
    Parameters_repr.bootstrap_account.consensus_key := None;
  |} in
  letP ? '(ctxt', l ) := Bootstrap_storage.init_account (ctxt, [])
                                             bootstrap_account in
    l = [] ∧ ctxt = ctxt'.
Proof.
  easy.
Qed.

The function [init_contract] is valid.

Lemma init_contract_is_valid typecheck ctxt updates contract :
  (∀ ctxt script,
    Raw_context.Valid.t ctxt →
    letP ? '(_, ctxt ) := typecheck ctxt script in
    Raw_context.Valid.t ctxt
  ) →
  Raw_context.Valid.t ctxt →
  Receipt_repr.balance_updates.Valid.t updates →
  Parameters_repr.bootstrap_contract.Valid.t contract →
  letP ? '(ctxt , updates ) :=
    Bootstrap_storage.init_contract typecheck (ctxt, updates) contract in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [init_value] is valid.

Lemma init_value_is_valid ctxt typecheck no_reward_cycles accounts contracts :
  Raw_context.Valid.t ctxt →
  (∀ ctxt script,
    Raw_context.Valid.t ctxt →
    letP ? '(_, ctxt ) := typecheck ctxt script in
    Raw_context.Valid.t ctxt
  ) →
  Option.Forall Pervasives.Int.Valid.t no_reward_cycles →
  List.Forall Parameters_repr.bootstrap_account.Valid.t accounts →
  List.Forall Parameters_repr.bootstrap_contract.Valid.t contracts →
  letP ? '(ctxt , updates ) :=
    Bootstrap_storage.init_value
      ctxt typecheck no_reward_cycles accounts contracts in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [cycle_end] is valid.

Lemma cycle_end_is_valid ctxt last_cycle :
  Raw_context.Valid.t ctxt →
  Cycle_repr.Valid.t last_cycle →
  letP ? ctxt := Bootstrap_storage.cycle_end ctxt last_cycle in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

[cycle_end] is an identity when there are no rewards in

the next cycle

Lemma cycle_end_id ctxt last_cycle :
  Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.find)
    ctxt (Cycle_repr.succ last_cycle) =
    Pervasives.Ok None →
  letP ? ctxt' := Bootstrap_storage.cycle_end ctxt last_cycle in
    ctxt' = ctxt.
Proof.
  intros. unfold Bootstrap_storage.cycle_end.
  now rewrite H.
Qed.

When cycle reaches [Int32.max_int] and assumming that there are no negative indexes on the [Storage.Ramp_up.Rewards], [cycle_end] becomes an identity.

Lemma cycle_max_int_id ctxt :
  (∀ (i : Int32.t),
      Int32.Valid.negative i →
      Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.find)
                                ctxt i = Pervasives.Ok None) →
  letP ? ctxt' := Bootstrap_storage.cycle_end ctxt Int32.max_int in
  ctxt' = ctxt.
Proof.
  intros.
  unfold Bootstrap_storage.cycle_end.
  assert (HCycle_repr_succ_overflows : Cycle_repr.succ Int32.max_int = Int32.min_int) by lia.
  rewrite HCycle_repr_succ_overflows. unfold Int32.min_int.
  now rewrite H.
Qed.

[cycle_end] succedes when [Storage.Ramp_up.Rewards.(_.find)] succedes

Lemma cycle_end_is_ok ctxt last_cycle :
  Pervasives.is_ok (Storage.Ramp_up.Rewards.(
           Storage_sigs.Indexed_data_storage.find)
      ctxt (Cycle_repr.succ last_cycle)) →
  Pervasives.is_ok (Bootstrap_storage.cycle_end ctxt last_cycle).
Proof.
  intros.
  unfold Bootstrap_storage.cycle_end.
  destruct (Storage.Ramp_up.Rewards.(
             Storage_sigs.Indexed_data_storage.find) _ _) eqn:?;
           [|easy].
  destruct o; simpl; try easy.
Admitted.