👥 Delegate_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.Delegate_storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Stake_storage.

Require TezosOfOCaml.Proto_alpha.Contract_storage.

Module participation_info.
  Module Valid.
    Import Proto_alpha.Delegate_storage.participation_info.

    Record t (x : Delegate_storage.participation_info) : Prop := {
      expected_cycle_activity :
        Pervasives.Int31.Valid.t x.(expected_cycle_activity);
      minimal_cycle_activity :
        Pervasives.Int31.Valid.t x.(minimal_cycle_activity);
      missed_slots :
        Pervasives.Int31.Valid.t x.(missed_slots);
      missed_levels :
        Pervasives.Int31.Valid.t x.(missed_levels);
      remaining_allowed_missed_slots :
        Pervasives.Int31.Valid.t x.(remaining_allowed_missed_slots);
      expected_endorsing_rewards :
        Tez_repr.Valid.t x.(expected_endorsing_rewards);
    }.
  End Valid.
End participation_info.

[set_frozen_deposits_limit] followed by [frozen_deposits_limit] is an identity

Lemma set_frozen_deposits_limit_frozen_deposits_limit_eq
  (absolute_key : Context.key)
  (ctxt : Raw_context.t)
  (delegate : _)
  (amount : Tez_repr.t) :
  Delegate_storage.frozen_deposits_limit
    (Delegate_storage.set_frozen_deposits_limit
       ctxt delegate (Some amount)) delegate =
    Pervasives.Ok (Some amount).
Proof.
  unfold Delegate_storage.set_frozen_deposits_limit.
  rewrite (Storage.Eq.Contracts.Frozen_deposits_limit.eq).(
    Storage_sigs.Indexed_data_storage.Eq.add_or_remove); simpl.
  unfold Delegate_storage.frozen_deposits_limit.
  rewrite (Storage.Eq.Contracts.Frozen_deposits_limit.eq).(
    Storage_sigs.Indexed_data_storage.Eq.find); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.find; simpl.
  unfold Storage.Eq.Contracts.Frozen_deposits_limit.parse.
  unfold Storage.Eq.Contracts.Frozen_deposits_limit.apply.
  rewrite Storage.parse_apply. simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.find_add_eq_some; [easy|].
  apply Storage.generic_Path_encoding_Valid.
Qed.

Lemma full_balance_is_valid (ctxt : Raw_context.t)
  (delegate : public_key_hash) :
    letP? frozen_deposits := Delegate_storage.frozen_deposits
        ctxt delegate in
    let ' Tez_repr.Tez_tag frozen_deposits := frozen_deposits.(
        Storage.deposits.current_amount) in
    let delegate_contract := Contract_repr.implicit_contract delegate in
    letP? 'Tez_repr.Tez_tag balance_and_frozen_bonds :=
      Contract_storage.get_balance_and_frozen_bonds ctxt delegate_contract in
    Tez_repr.Repr.Valid.t frozen_deposits →
    Tez_repr.Repr.Valid.t balance_and_frozen_bonds →
    Tez_repr.Repr.Valid.t (frozen_deposits +Z balance_and_frozen_bonds) →
    letP? full_balance := Delegate_storage.full_balance ctxt delegate in
    Tez_repr.Valid.t full_balance.
Proof.
  intros.
  destruct Delegate_storage.frozen_deposits
    as [frozen_deposits'|] eqn:?; [|easy]; simpl.
  destruct Contract_storage.get_balance_and_frozen_bonds eqn:?;
    [|hauto l:on]; simpl.
  unfold Delegate_storage.full_balance.
  rewrite Heqt, Heqt0; simpl.
  destruct (frozen_deposits'.(Storage.deposits.current_amount)).
  destruct t.
  intros.
  unfold Tez_repr.op_plusquestion.
  unfold "+i64"; simpl.
  rewrite Int64.normalize_identity; [|lia].
  now replace (_ <? _) with false by lia.
Qed.

Lemma staking_balance_is_valid
  (ctxt : Raw_context.t) (delegate : public_key_hash)
  (balance : Tez_repr.t) :
  Delegate_storage.staking_balance ctxt delegate =
    Pervasives.Ok balance →
  Tez_repr.Valid.t balance.
Proof.
  unfold Delegate_storage.staking_balance.
  destruct Contract_delegate_storage.registered; [|easy]; simpl.
  destruct b; [now apply Stake_storage.get_staking_storage_is_valid|].
  intros Hinj; injection Hinj as Hinj. now rewrite <- Hinj.
Qed.

Lemma balance_is_valid
  (absolute_key : Context.key)
  (ctxt : Raw_context.t) (delegate : public_key_hash)
  (balance : Tez_repr.t) :
  Tez_repr.Valid.t balance →
  letP? ctxt' := Storage.Contract.Spendable_balance.(
    Storage_sigs.Indexed_data_storage.init_value)
    ctxt (Contract_repr.Implicit delegate) balance in
  letP? balance' := Delegate_storage.balance ctxt' delegate in
  Tez_repr.Valid.t balance'.
 Proof.
   unfold Delegate_storage.balance.
   now apply Contract_storage.spendable_balance_get_is_valid.
Qed.

Lemma frozen_deposits_is_valid :
 ∀ (absolute_key : Context.key) (ctxt ctxt' : Raw_context.t)
   (delegate : public_key_hash),
  let deposits := {|
    Storage.deposits.initial_amount := Tez_repr.zero;
    Storage.deposits.current_amount := Tez_repr.zero
  |} in
  Frozen_deposits_storage.init_value ctxt delegate = Pervasives.Ok ctxt' →
  Delegate_storage.frozen_deposits ctxt' delegate = Pervasives.Ok deposits →
  Tez_repr.Valid.t deposits.(Storage.deposits.current_amount).
Proof.
  do 5 intro.
  intro Hinit.
  unfold Delegate_storage.frozen_deposits.
  apply Frozen_deposits_storage.get_is_valid
        with (deposits := deposits)
    in Hinit; try easy.
  revert Hinit.
  unfold Frozen_deposits_storage.get,
    Frozen_deposits_storage.init_value.
  rewrite
    (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.init_value),
    (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.get); simpl.
  unfold
    Storage_sigs.Indexed_data_storage.Op.init_value,
    Storage_sigs.Indexed_data_storage.Op.get,
    Storage_sigs.Indexed_data_storage.Op.find,
    Storage_sigs.Indexed_data_storage.Op.mem,
    Storage_sigs.Indexed_data_storage.Op.add,
    Storage_sigs.Indexed_data_storage.State.Map.
  destruct (Map.Make _).(S.mem) eqn:?; [easy|simpl].
  intro Hinj. injection Hinj as Hinj. rewrite <- Hinj.
  unfold
    Storage.Eq.Contracts.Frozen_deposits.apply,
    Storage.Eq.Contracts.Frozen_deposits.parse.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.find_add_eq_some; [easy|].
  apply Storage.generic_Path_encoding_Valid.
Qed.

Lemma delegated_balance_is_valid
  (absolute_key : Context.key)
  (ctxt : Raw_context.t) (delegate : public_key_hash)
  (initial_balance : Tez_repr.t):
  Tez_repr.Valid.t initial_balance →
  letP? ctxt' := Storage.Contract.Spendable_balance.(
    Storage_sigs.Indexed_data_storage.init_value)
    ctxt (Contract_repr.Implicit delegate) initial_balance in
  letP? '{| Storage.deposits.current_amount :=
            Tez_repr.Tez_tag current_amount |} :=
    Delegate_storage.frozen_deposits ctxt' delegate in
  letP? 'Tez_repr.Tez_tag balance := Delegate_storage.balance
    ctxt' delegate in
  Int64.Valid.t (balance +Z current_amount) →
  letP? tez := Delegate_storage.delegated_balance ctxt' delegate in
  Tez_repr.Valid.t tez.
Proof.
  intros.
  destruct (_.(Storage_sigs.Indexed_data_storage.init_value) _ _ _)
    as [ctxt'|] eqn:Hinit; [simpl|easy].
  destruct Delegate_storage.frozen_deposits
           as [frozen_deposits|] eqn:?; [simpl|easy].
  destruct frozen_deposits as [frozen_deposits'] eqn:Hfrozen_deposits,
      current_amount as [current_amount'] eqn:Hcurrent_amount.
  destruct Delegate_storage.balance
           as [balance|] eqn:?; [simpl|easy].
  destruct balance as [balance'].
  intros.
  unfold Delegate_storage.delegated_balance.
  destruct Delegate_storage.staking_balance
    as [staking_balance|] eqn:?; [|easy]; simpl.
  rewrite Heqt0; simpl.
  rewrite Heqt; simpl.
  destruct (_ <? _) eqn:?; simpl; [sauto q:on|].
  unfold Tez_repr.op_minusquestion.
  destruct staking_balance as [staking_balance]; simpl.
  destruct (_ <=? _) eqn:?; [|easy]; simpl.
  unfold "-i64", "+i64" in ×.
  apply staking_balance_is_valid in Heqt1.
  assert (Hbalance_is_valid : Delegate_storage.balance ctxt' delegate =
    Pervasives.Ok (Tez_repr.Tez_tag balance') →
    Tez_repr.Valid.t (Tez_repr.Tez_tag balance')).
  { pose proof (balance_is_valid absolute_key ctxt delegate
      initial_balance).
    specialize (H1 H).
    rewrite Hinit in H1. simpl in H1. revert H1.
    destruct Delegate_storage.balance eqn:?; simpl; [|easy].
    intros. injection H2 as H2. rewrite H2 in H1. easy. }
  apply Hbalance_is_valid in Heqt0.
  rewrite Int64.normalize_identity in Heqb, Heqb0;
  repeat rewrite Int64.normalize_identity; lia.
Qed.