🐣 Bootstrap_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Bootstrap_storage.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Token.

Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int32.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Pervasives.

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

Lemma init_account_identity (ctxt : Raw_context.t)
      (public_key_hash : Signature.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 |} in
  letP? '(ctxt', l) := Bootstrap_storage.init_account (ctxt, [])
                                             bootstrap_account in
    l = [] ∧ ctxt = ctxt'.
Proof.
  easy.
Qed.

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

the next cycle

Lemma cycle_end_id (ctxt : Raw_context.t)
      (last_cycle : Cycle_repr.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 : Raw_context.t) :
  (∀ (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 ctxt' : Raw_context.t)
      (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.
  rewrite (Storage.Eq.Ramp_up.Rewards.eq).(
    Storage_sigs.Indexed_data_storage.Eq.remove_existing); simpl.
  simpl in ×.
  unfold Indexed_data_storage.Op.remove_existing.
  unfold Indexed_data_storage.Op.mem.
  unfold Indexed_data_storage.State.Map.
  revert Heqt.
  rewrite (Storage.Eq.Ramp_up.Rewards.eq).(
    Storage_sigs.Indexed_data_storage.Eq.find); simpl.
  unfold Indexed_data_storage.Op.find.
  unfold Indexed_data_storage.State.Map.
  intros Heqt.
  assert ((Map.Make
    (Indexed_data_storage.State.Ord Storage.generic_Path_encoding)).(
       S.find)
       (Cycle_repr.succ last_cycle)
       (Storage.Eq.Ramp_up.Rewards.parse ctxt) = Some (Some t)).
  { set (Ord := (Indexed_data_storage.State.Ord _)).
    destruct ((Map.Make _).(S.find) _ _).
    destruct o; [|easy].
    inversion Heqt. reflexivity. easy. }
  rewrite (Map.find_mem_eq _ (Some t)); [|assumption].
  easy.
Qed.