✒️ 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]

Lemma exists_implies_must_exists_success (ctxt : Raw_context.t)
  (hash : Contract_hash.t) :
  let contract := Contract_repr.Originated hash in
  Contract_storage._exists ctxt contract = Pervasives.Ok true →
  Contract_storage.must_exist ctxt contract = Pervasives.Ok tt.
Proof.
  unfold Contract_storage.must_exist; simpl.
  intros.
  now rewrite H.
Qed.

[must_be_allocated] after [allocated] returns [Pervasives.Ok unit]

Lemma allocated_implies_must_be_allocated_success
  (ctxt : Raw_context.t) (contract : Contract_repr.t) :
  Contract_storage.allocated ctxt contract = return? true →
  Contract_storage.must_be_allocated ctxt contract = return? tt.
Proof.
  intros.
  unfold Contract_storage.must_be_allocated.
  now rewrite H.
Qed.

[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.