Skip to main content

✒️ Contract_manager_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_manager_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.

[is_manager_key_revealed] after [reveal_manager_key] returns [Pervaives.Ok true]
Lemma reveal_implies_is_manager_key_revelead_to_be_true
  (absolute_key : Context.key) (ctxt : Raw_context.t)
  (pkh : public_key_hash) (pk : public_key) :
  letP? ctxt' := Contract_manager_storage.reveal_manager_key
    ctxt pkh pk in
  Contract_manager_storage.is_manager_key_revealed
      ctxt' pkh = Pervasives.Ok true.
Proof.
  intros.
  destruct Contract_manager_storage.reveal_manager_key eqn:?; [|easy].
  simpl; revert Heqt.
  unfold Contract_manager_storage.reveal_manager_key.
  rewrite Storage.Eq.Contracts.Manager.eq.(
    Storage_sigs.Indexed_data_storage.Eq.get); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  destruct (Map.Make _).(S.find) eqn:?;
  repeat
    match goal with
    | |- context [match ?e with __ end] ⇒ destruct e eqn:?; [simpl|easy]
    end; [|easy].
  unfold Contract_manager_storage.is_manager_key_revealed.
  simpl.
  rewrite Storage.Eq.Contracts.Manager.eq.(
    Storage_sigs.Indexed_data_storage.Eq.update); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  destruct (Map.Make _).(S.mem) eqn:?; [simpl|easy].
  intros. injection Heqt as Heqt. rewrite <- Heqt.
  rewrite Storage.Eq.Contracts.Manager.eq.(
    Storage_sigs.Indexed_data_storage.Eq.find); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  Storage.auto_parse_apply.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  rewrite Map.find_add_eq_some; simpl; auto.
  apply Storage.generic_Path_encoding_Valid.
Qed.

[get_manager_key] after [reveals] returns [Pevasives.Ok]
Lemma reveal_implies_get_manager_key_success
  (ctxt : Raw_context.t) (pkh : public_key_hash) (pk : public_key) :
  letP? ctxt' := Contract_manager_storage.reveal_manager_key
    ctxt pkh pk in
  Pervasives.is_ok (Contract_manager_storage.get_manager_key
    None ctxt' pkh).
Proof.
  intros.
  destruct Contract_manager_storage.reveal_manager_key eqn:?; [|easy].
  revert Heqt.
  unfold Contract_manager_storage.reveal_manager_key.
  destruct
    Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.get)
    eqn:?; [|easy]; simpl.
  repeat
    match goal with
    | |- context [match ?e with __ end] ⇒ destruct e eqn:?; [simpl|easy]
    end.
  revert Heqt0.
  rewrite Storage.Eq.Contracts.Manager.eq.(
      Storage_sigs.Indexed_data_storage.Eq.get),
    Storage.Eq.Contracts.Manager.eq.(
      Storage_sigs.Indexed_data_storage.Eq.update); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  destruct (Map.Make _).(S.find) eqn:?;
    [destruct o; [|easy]|easy]; simpl.
  destruct (Map.Make _).(S.mem) eqn:?; [|easy].
  simpl. intros. injection Heqt as Heqt; rewrite <- Heqt.
  unfold Contract_manager_storage.get_manager_key.
  rewrite Storage.Eq.Contracts.Manager.eq.(
      Storage_sigs.Indexed_data_storage.Eq.find); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  Storage.auto_parse_apply.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  rewrite Map.find_add_eq_some; try easy.
  apply Storage.generic_Path_encoding_Valid.
Qed.

[remove_existing] after [get_manager_key] success returns [Pervasives.Ok]
Lemma get_manager_key_implies_remove_exists_success
  (ctxt : Raw_context.t) (pkh : public_key_hash) :
  Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.find)
      ctxt (Contract_repr.implicit_contract pkh) Pervasives.Ok None
  let contract := Contract_repr.Implicit pkh in
  letP? pk := Contract_manager_storage.get_manager_key
    None ctxt pkh in
    Pervasives.is_ok (Contract_manager_storage.remove_existing
        ctxt contract).
Proof.
  intros.
  unfold Contract_manager_storage.get_manager_key.
  destruct Storage.Contract.Manager.(
    Storage_sigs.Indexed_data_storage.find) eqn:?; [simpl|easy].
  destruct o eqn:?; [|sfirstorder].
  revert Heqt.
  rewrite Storage.Eq.Contracts.Manager.eq.(
      Storage_sigs.Indexed_data_storage.Eq.find); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  destruct (Map.Make _).(S.find) eqn:?; [destruct o|]; try easy.
  destruct o0 eqn:?; [|easy].
  intros. injection Heqt as Heqt. rewrite Heqt in Heqo1.
  destruct t eqn:?; [easy|].
  simpl.
  unfold Contract_manager_storage.remove_existing.
  rewrite Storage.Eq.Contracts.Manager.eq.(
      Storage_sigs.Indexed_data_storage.Eq.remove_existing); simpl.
  Storage_sigs.Indexed_data_storage.Op.Unfold.all.
  apply Map.find_mem_eq in Heqo1.
  subst contract.
  unfold Contract_repr.implicit_contract in Heqo1.
  now rewrite Heqo1.
Qed.