Skip to main content

✒️ Contract_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.Contract_storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.

Module Legacy_big_map_diff.
  Lemma item_encoding_is_valid
    : Data_encoding.Valid.t (fun _True) Contract_storage.Legacy_big_map_diff.item_encoding.
    Data_encoding.Valid.data_encoding_auto.
    intros []; simpl; try tauto.
    destruct u, diff_value; tauto.
  Qed.
  #[global] Hint Resolve item_encoding_is_valid : Data_encoding_db.

  Lemma encoding_is_valid
    : Data_encoding.Valid.t (fun _True) Contract_storage.Legacy_big_map_diff.encoding.
    Data_encoding.Valid.data_encoding_auto.
    now intros; apply List.Forall_True.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Legacy_big_map_diff.

[must_exists] after [_exists] returns [Pervasives.Ok unit]
[must_be_allocated] after [allocated] returns [Pervasives.Ok unit]
[Storage.Contract.Spendable_balance.get] is valid when the same storage was initialized with a valid balance
Lemma spendable_balance_get_is_valid
  (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' := Storage.Contract.Spendable_balance.(
    Storage_sigs.Indexed_data_storage.get)
    ctxt' (Contract_repr.Implicit delegate) in
  Tez_repr.Valid.t balance'.
Proof.
  rewrite (Storage.Eq.Contracts.Balance.eq).(
    Storage_sigs.Indexed_data_storage.Eq.init_value); simpl.
  destruct (Storage_sigs.Indexed_data_storage.Op.init_value _ _ _) eqn:?; [|easy].
  simpl. revert Heqt.
  rewrite (Storage.Eq.Contracts.Balance.eq).(
    Storage_sigs.Indexed_data_storage.Eq.get); simpl.
  unfold Storage_sigs.Indexed_data_storage.Op.init_value.
  unfold Storage_sigs.Indexed_data_storage.Op.get.
  unfold Storage_sigs.Indexed_data_storage.Op.mem.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  destruct ((Map.Make _).(S.mem) _ _) eqn:?; [easy|].
  unfold Storage_sigs.Indexed_data_storage.Op.add.
  intros Hinj; injection Hinj as Hinj. rewrite <- Hinj.
  unfold Storage_sigs.Indexed_data_storage.Op.find.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  unfold Storage.Eq.Contracts.Balance.parse,
    Storage.Eq.Contracts.Balance.apply;
    rewrite Storage.parse_apply; simpl.
  unfold Storage_sigs.Indexed_data_storage.State.Map.
  rewrite Map.find_add_eq_some; auto.
  apply Storage.generic_Path_encoding_Valid.
Qed.