🪅 Token.v

Proofs

The function [allocated] is valid.

Lemma allocated_is_valid ctxt stored :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , _) := Token.allocated ctxt stored in
    Raw_context.Valid.t ctxt.
Proof.
  intros; unfold Token.allocated; step; trivial.
  apply Contract_storage.bond_allocated_is_valid; trivial.
Qed.

The function [balance] is valid.

Lemma balance_is_valid ctxt stored :
  Raw_context.Valid.t ctxt →
  letP ? '(ctxt , amount ) := Token.balance ctxt stored in
    Raw_context.Valid.t ctxt ∧ Tez_repr.Valid.t amount.
Proof.
  intros; unfold Token.balance; step; trivial.
  { eapply Error.split_letP; trivial. {
      apply Contract_storage.get_balance_is_valid; trivial.
    }
    intros. easy. }
  { eapply Error.split_letP; trivial. {
      apply Commitment_storage.committed_amount_is_valid; trivial.
    }
    intros. easy. }
  {
    (* @TODO [Storage_sigs] blacklisted. *)
    admit.
  }
  { eapply Error.split_letP; trivial. {
      apply Frozen_deposits_storage.find_is_valid; trivial.
    }
    intros. simpl. split ; [assumption |].
    destruct x as [frozen_deposits |].
    { destruct H0. assumption. }
    { easy. }
  }
  { split ; [assumption |].
    (* currently no [get_collected_fees_is_valid] lemma *)
    admit. }
  { eapply Error.split_letP; trivial. {
      apply Contract_storage.find_bond_is_valid; trivial.
    }
    clear ctxt H.
    intros [ctxt amount] [H Hamount].
    split ; [assumption |].
    unfold Option.value_value. destruct amount ; simpl in Hamount ; easy.
  }
  (* hauto lq: on. *)
Admitted.

The function [credit] is valid.

Lemma credit_is_valid {A} ctxt dest amount origin :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t amount →
  letP ? '(ctxt , (_, balance_update , _)) := @Token.credit A ctxt dest amount origin in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_update.Valid.t balance_update.
Proof.
  intros.
  unfold Token.credit; do 2 step; trivial.
  all : apply Error.split_letP with (P:=(fun ' (x', _) ⇒ Raw_context.Valid.t x')).
  all :
    try apply Error.split_letP with (P:=(fun x' ⇒ Raw_context.Valid.t x'));
    try (apply Contract_storage.credit_only_call_from_token_is_valid);
    try (apply
     Commitment_storage.increase_commitment_only_call_from_token_is_valid);
    try (apply Contract_storage.increase_balance_only_call_from_token_is_valid);
    try (apply Raw_context.credit_collected_fees_only_call_from_token_is_valid);
    try (apply
     Contract_storage.credit_bond_only_call_from_token_is_valid); trivial;
    try step;
    try (apply Frozen_deposits_storage.init_value_is_valid); trivial;
    try scongruence; try hauto lq: on.
  intros; eapply Error.split_letP.
  apply Frozen_deposits_storage.credit_only_call_from_token_is_valid; trivial.
  scongruence.
Qed.

The function [spend] is valid. @TODO perhaps the [Tez_repr.Valid.positive] can be loosened into [Tez_repr.Valid.t] if there is a way to prove that [amount <> 0] in case of success.

Lemma spend_is_valid {A} ctxt src amount origin :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.positive amount →
  letP ? '(ctxt , p ) := @Token.spend A ctxt src amount origin in
    Raw_context.Valid.t ctxt ∧
    let ' (_, balance_update, _) := p in
    Receipt_repr.balance_update.Valid.t balance_update.
Proof.
  intros.
  unfold Token.spend.
  do 2 step ; try split ; try easy ;
  destruct amount eqn:eq_amount; unfold Tez_repr.Valid.positive in H0;
  unfold Tez_repr.Repr.Valid.positive in H0;
  ( apply Error.split_letP
    with (fun '(ctxt , _) ⇒ Raw_context.Valid.t ctxt) ; [|
      intros; try destruct x eqn:eq_x; simpl; split ; assumption ]).

The six cases below are boilerplate

  { eapply Error.split_letP. {
        apply Contract_storage.spend_only_call_from_token_is_valid.
        assumption. unfold Tez_repr.Repr.Valid.t. lia.
      }
      intros. assumption.
  }
  { eapply Error.split_letP. {
      apply
      Commitment_storage.decrease_commitment_only_call_from_token_is_valid ;
      [assumption|].
      unfold Tez_repr.Repr.Valid.t. lia. }
    intros ; assumption.
  }
  { eapply Error.split_letP. {
      apply Contract_storage.decrease_balance_only_call_from_token_is_valid ;
      [assumption|].
      unfold Tez_repr.Repr.Valid.t. lia. }
    intros ; assumption.
  }
  { eapply Error.split_letP with (Raw_context.Valid.t). {
      apply Frozen_deposits_storage.spend_only_call_from_token_is_valid;
      [assumption|].
      unfold Tez_repr.Repr.Valid.t. lia. }
    intros ; assumption.
  }
  { eapply Error.split_letP with (Raw_context.Valid.t). {
      apply Raw_context.spend_collected_fees_only_call_from_token_is_valid;
        [assumption|].
      unfold Tez_repr.Valid.t.
      unfold Tez_repr.Repr.Valid.t.
      lia.
      }
    intros ; assumption.
  }
  { eapply Error.split_letP with (Raw_context.Valid.t). {
      apply Contract_storage.spend_bond_only_call_from_token_is_valid;
      [assumption|].
      unfold Tez_repr.Repr.Valid.t. lia. }
    intros ; assumption.
  }
Qed.

Auxiliary lemma for transfer_n_is_valid

Lemma follow_letP_and {a : Set}
    (x : M ? a) (P : a → Prop) (Q : a → Prop) :
    (∀ x, (letP ? x := x in Q x) ∧ (letP ? x := x in P x)) →
    letP ? x := x in P x ∧ Q x.
Proof.
  intros. fcrush.
Qed.

If we have a list of pairs containing valid tezos which a not equal to zero, then these tezos are positive. @review: note if this lemma should be here, or if we shouldn't have a more generic version factorizing this proof.

Lemma tez_pair_non_negative_non_zero_implies_positive {A : Set}
  (l : list (A × Tez_repr.t)) l0 :
    List.Forall (fun '(_, t ) ⇒ Tez_repr.Valid.t t) l →
    List.filter (fun '(_, am ) ⇒ Tez_repr.op_ltgt am Tez_repr.zero) l =
    l0 → Forall (fun '(_, t ) ⇒ Tez_repr.Valid.positive t) l0.
Proof.
  intros Hval.
  generalize dependent l0.
  induction l as [ |p1 l1 IH]; intros l0 Hneqzero.
  { cbv in Hneqzero. rewrite <- Hneqzero. constructor. }
  {

Inductive case: we go back and forth from CoqOfOCaml [filter] to standard [filter], to simplify the hypothsis on filter. The only non-trivial case is when the new element has a positive tez value (grep true).

    rewrite List.filter_CoqOfOCaml_filter_eq in Hneqzero.
    destruct p1 as [a tz].
    destruct (Tez_repr.op_ltgt tz Tez_repr.zero) eqn:b ; simpl in Hneqzero;
    rewrite b in Hneqzero.
    { grep true.
      destruct l0 as [ |[a0 tz0] l00] ; [inversion Hneqzero |
       inversion Hneqzero as [[H0 H1 Hl1]] ]. subst a0 tz0.
      inversion Hval as [ |p l1' Htzval Hl1' [H1 H2]].
      subst l1' p.
      inversion Hneqzero as [Hneqzero'].
      rewrite <- List.filter_CoqOfOCaml_filter_eq in Hneqzero'.
      specialize (IH Hl1' l00 Hneqzero') as IH0.
      rewrite List.filter_CoqOfOCaml_filter_eq in Hneqzero'.
      rewrite Hneqzero'.
      constructor ; [|assumption].
      destruct tz as [r]. unfold Tez_repr.Valid.positive.
      unfold Tez_repr.Repr.Valid.positive.
      unfold Tez_repr.op_ltgt in b.
      simpl in b.
      lia.
    }
    { grep false.
      inversion Hval as [ | p l1' Htz H1val Hp]. subst l1' p.
      inversion Hval.
      rewrite <- List.filter_CoqOfOCaml_filter_eq in Hneqzero.
      apply IH ;
      assumption.
    }
  }
Qed.

The function [transfer_n] is valid. The positivity hypothesis on [lst] is perhaps to strong, or unusefull: we perhaps just need lst containt only valid elements (i.e. whose Tez value is non-negative, and retrieve the positivity with [filter])

Lemma transfer_n_is_valid op_staropstar ctxt lst sink :
  Raw_context.Valid.t ctxt →
  Forall (fun '(_, t ) ⇒ Tez_repr.Valid.t t) lst →
  letP ? '(ctxt , burn ) := Token.transfer_n op_staropstar
    ctxt lst sink in Raw_context.Valid.t ctxt
     ∧ Receipt_repr.balance_updates.Valid.t burn.
Proof.
  intros H Hlst. unfold Token.transfer_n.
  step; [split ; [assumption| constructor] |].
  apply Error.split_letP with (P:= (fun ' (x', am , debit_logs ) ⇒ Raw_context.Valid.t x'
    ∧ Tez_repr.Valid.t am ∧ Receipt_repr.balance_updates.Valid.t debit_logs )).
  { apply Error.follow_letP with (P:= fun '(a , t , debit_logs ) ⇒
      Raw_context.Valid.t a ∧ Tez_repr.Valid.t t ∧
      Receipt_repr.balance_updates.Valid.t debit_logs
      ). {
      intros x H1. step. step. destruct H1 as [? [? ?]].
      repeat split ; assumption.
    }
    unfold fold_left_es.
    apply List.fold_left_e_is_valid with
      (P_a:=(fun '(a , t , debit_logs ) ⇒ Raw_context.Valid.t a ∧ Tez_repr.Valid.t t ∧
      Receipt_repr.balance_updates.Valid.t debit_logs))
      (P_b:=(fun '(s , t ) ⇒ Tez_repr.Valid.positive t
      )).
    { intros [[ctxt0 total] debit_logs] [source amount] Hacc Hitem.
      eapply Error.split_letP. {
        apply Token.spend_is_valid; intuition. }
      intros [ctxt2 [[balance balance_update] update_origin]] [H2 Hp2].
      destruct Hacc as [Hacc1 [Hacc2 Hacc3]].
      apply Error.split_letP with (P := fun ' x ⇒ Tez_repr.Valid.positive x). {
        apply Tez_repr.op_plusquestion_is_valid_positive. assumption.
      }
      intros x x_pos.
      repeat split ; try assumption. {
        destruct x as [x_repr].
        simpl in x_pos. unfold Tez_repr.Repr.Valid.positive in x_pos.
        lia.
      }
      { constructor ; [ assumption |].
        unfold Receipt_repr.balance_updates.Valid.t in Hacc3. assumption.
        }
    }
    { repeat split ; [ assumption | easy | easy |].
      unfold Receipt_repr.balance_updates.Valid.t.
      constructor.
    }
    { assert (Heql' := Heql). constructor.
      { specialize (tez_pair_non_negative_non_zero_implies_positive lst (p :: l) Hlst
        Heql') as H0. inversion H0. assumption.
      }
      { apply List.filter_inv_tail in Heql.
        specialize (tez_pair_non_negative_non_zero_implies_positive lst (p :: l) Hlst
        Heql') as H0. inversion H0.
        assumption.
      }
    }
  }
  { intros [[ctxt0 amount] balance_updates] [H0 [Hamount Hb_updates]].
    eapply Error.split_letP with
      (fun '(ctxt ,(_,balance_update ,_)) ⇒
        Raw_context.Valid.t ctxt ∧
        Receipt_repr.balance_update.Valid.t balance_update
      ).
      { destruct op_staropstar as [ op_staropstar|] ;
        apply credit_is_valid; assumption .
      }
    intros [[ctxt1 balance] [[balance1 balance_update1] update_origin]]
[H1 Hval1].
    destruct H1 as [H11 [H12 [H13 H14]]] eqn:eq_H1.
    eapply Error.split_letP. {
      unfold fold_left_es.
      apply List.fold_left_e_is_valid with (P_a := Raw_context.Valid.t)
      (P_b := fun '(s , t ) ⇒ Tez_repr.Valid.positive t ). (* maybe Valid.t only*)
      { intros. destruct item as [? ?] eqn:eq_item.
        destruct s ; [ assumption |].
        destruct c ; try assumption; try
        (apply Contract_storage.ensure_deallocated_if_empty_is_valid;
          assumption).
      }
      { assumption.
      }
      { apply (tez_pair_non_negative_non_zero_implies_positive lst) ;
          assumption.
      }
    }
    intros. simpl. split ; [assumption |].
    (* use Hval1 , Hb_updates + lemma about innocuity rev*)
    unfold Receipt_repr.balance_updates.Valid.t.
    apply List.Forall_P_rev.
    constructor ; [ assumption |].
    unfold Receipt_repr.balance_updates.Valid.t. assumption.
  }
Qed.

The function [transfer] is valid.

Lemma transfer_is_valid origin ctxt src dest amount :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t amount →
  letP ? '(ctxt , burn ) := Token.transfer origin ctxt src dest amount in
  Raw_context.Valid.t ctxt ∧ Receipt_repr.balance_updates.Valid.t burn.
Proof.
  intros.
  unfold Token.transfer.
  apply transfer_n_is_valid; trivial.
  constructor ; [ assumption | constructor].
Qed.

The function [transfer] is valid, weaker version. At least, temporarily useful.

Lemma weak_transfer_is_valid origin ctxt src dest amount :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t amount →
  letP ? '(ctxt , burn ) := Token.transfer origin ctxt src dest amount in
  Raw_context.Valid.t ctxt.
Proof.
  intros H Hamount.
  apply Error.follow_letP with (P :=
  fun '(ctxt , burn ) ⇒
  Raw_context.Valid.t ctxt ∧ Receipt_repr.balance_updates.Valid.t burn
  ).
  { intros [ctxt0 burn0] [H0 _]. assumption. }
  apply transfer_is_valid ; assumption.
Qed.