Skip to main content

⛄ Frozen_deposits_storage.v

Proofs

See code, Gitlab , OCaml

[allocated] after [init_value] returns [true]
[get] after [init_value] returns [Pervasives.Ok]
[find] after [init_value] returns [Pervasives.Ok]
[credit_only_call_from_token] after [init_value] returns [Pervasives.Ok]
Lemma credit_only_call_from_token_after_init_is_ok
  (ctxt : Raw_context.t)
  (pkh : public_key_hash) (amount : int) :
  Tez_repr.Repr.Valid.t amount
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt' := Frozen_deposits_storage.init_value ctxt pkh in
  Pervasives.is_ok (Frozen_deposits_storage.credit_only_call_from_token
    ctxt' pkh (Tez_repr.Tez_tag amount)).
Proof.
  intros.
  destruct Frozen_deposits_storage.init_value eqn:Hinit_value;
    [simpl|easy].
  revert Hinit_value.
  unfold Frozen_deposits_storage.init_value.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.init_value); simpl.
  set (deposits := {|
          Storage.deposits.initial_amount := Tez_repr.zero;
          Storage.deposits.current_amount := Tez_repr.zero
        |}).
  unfold Storage_sigs.Indexed_data_storage.Op.init_value.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  destruct (Map.Make _).(S.mem) eqn:?; [easy|simpl].
  unfold Storage_sigs.Indexed_data_storage.Op.add.
  intro. injection Hinit_value as Hinit_value. rewrite <- Hinit_value.
  unfold Frozen_deposits_storage.credit_only_call_from_token.
  unfold Frozen_deposits_storage.update_balance.
  unfold Frozen_deposits_storage.get.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.get).
  simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.get.
  unfold Storage_sigs.Indexed_data_storage.Op.find.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  unfold Storage.Eq.Contracts.Frozen_deposits.apply.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.find_add_eq_some. simpl.
  unfold "+i64".
  rewrite Int64.normalize_identity; [|lia].
  replace (_ <? 0) with false by lia; simpl.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.update); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.update.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.mem_add_eq; try easy.
  all: apply Storage.generic_Path_encoding_Valid.
Qed.

Lemma get_is_valid_helper
  (ctxt : Raw_context.t) (delegate : public_key_hash) :
  letP? ctxt := Frozen_deposits_storage.init_value ctxt delegate in
  letP? deposits := Frozen_deposits_storage.get ctxt
    (Contract_repr.implicit_contract delegate) in
  Tez_repr.Valid.t deposits.(Storage.deposits.current_amount).
Proof.
  intros.
  unfold Frozen_deposits_storage.init_value.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.init_value); simpl.
  set (deposits' := {|
          Storage.deposits.initial_amount := Tez_repr.zero;
          Storage.deposits.current_amount := Tez_repr.zero
        |}).
  unfold Storage_sigs.Indexed_data_storage.Op.init_value.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  destruct (Map.Make _).(S.mem) eqn:?; [easy|simpl].
  unfold Storage_sigs.Indexed_data_storage.Op.add.

  unfold Frozen_deposits_storage.get.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.get); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.get.
  unfold Storage_sigs.Indexed_data_storage.Op.find.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  unfold Storage.Eq.Contracts.Frozen_deposits.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.

(* @TODO, used on Delegate_storage *)
Lemma get_is_valid (ctxt ctxt' : Raw_context.t)
  (delegate : public_key_hash) (deposits : Storage.deposits) :
  Frozen_deposits_storage.init_value ctxt delegate = Pervasives.Ok ctxt'
  Frozen_deposits_storage.get ctxt' (Contract_repr.implicit_contract
    delegate) = Pervasives.Ok deposits
  Tez_repr.Valid.t deposits.(Storage.deposits.current_amount).
Proof.
  pose proof (get_is_valid_helper ctxt delegate).
  destruct Frozen_deposits_storage.init_value eqn:?; [simpl|easy].
  intros Hinj. injection Hinj as Hinj. rewrite Hinj in H.
  simpl in H. revert H.
  destruct Frozen_deposits_storage.get eqn:?; [|easy].
  scongruence.
Qed.

Lemma spend_only_call_from_token_eq
  (ctxt : Raw_context.t)
  (pkh : public_key_hash) (amount : Tez_repr.t) :
  Tez_repr.Valid.t amount
  let contract := Contract_repr.Implicit pkh in
  letP? ctxt := Frozen_deposits_storage.init_value ctxt pkh in
  letP? ctxt := Frozen_deposits_storage.credit_only_call_from_token
    ctxt pkh amount in
  Pervasives.is_ok (Frozen_deposits_storage.spend_only_call_from_token ctxt pkh amount).
Proof.
  intros.
  destruct Frozen_deposits_storage.init_value eqn:Hinit_value;
    [simpl|easy].
  revert Hinit_value.
  unfold Frozen_deposits_storage.init_value.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.init_value); simpl.
  set (deposits := {|
          Storage.deposits.initial_amount := Tez_repr.zero;
          Storage.deposits.current_amount := Tez_repr.zero
        |}).
  unfold Storage_sigs.Indexed_data_storage.Op.init_value.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  destruct (Map.Make _).(S.mem) eqn:?; [easy|simpl].
  unfold Storage_sigs.Indexed_data_storage.Op.add.
  intro. injection Hinit_value as Hinit_value. rewrite <- Hinit_value.
  unfold Frozen_deposits_storage.update_initial_amount.
  unfold Frozen_deposits_storage.get.
  unfold Frozen_deposits_storage.credit_only_call_from_token.
  unfold Frozen_deposits_storage.update_balance.
  unfold Frozen_deposits_storage.get.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.get); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.get.
  unfold Storage_sigs.Indexed_data_storage.Op.find.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  unfold Storage.Eq.Contracts.Frozen_deposits.apply.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.find_add_eq_some; simpl.
  destruct amount as [amount].
  unfold "+i64"; simpl.
  rewrite Int64.normalize_identity; [|lia].
  replace (amount <? 0) with false by lia; simpl.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.update); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.update.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.mem_add_eq; simpl.
  unfold Frozen_deposits_storage.spend_only_call_from_token.
  unfold Frozen_deposits_storage.update_balance.
  unfold Frozen_deposits_storage.get.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.get); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.get.
  unfold Storage_sigs.Indexed_data_storage.Op.find.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  unfold Storage.Eq.Contracts.Frozen_deposits.apply.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.find_add_eq_some; simpl.
  replace (amount <=? amount) with true by lia; simpl.
  rewrite (Storage.Eq.Contracts.Frozen_deposits.eq).(
    Storage_sigs.Indexed_data_storage.Eq.update); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.update.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  unfold Storage.Eq.Contracts.Frozen_deposits.parse.
  rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.mem_add_eq; try easy.
  all: apply Storage.generic_Path_encoding_Valid.
Qed.