✒️ Contract_manager_storage.v

Proofs

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [init_value] is valid.

Lemma init_value_is_valid ctxt contract key :
  Raw_context.Valid.t ctxt →
  letP ? ctxt := Contract_manager_storage.init_value ctxt contract key in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [is_manager_key_revealed] is valid.

Lemma is_manager_key_revealed_is_valid ctxt manager :
  Raw_context.Valid.t ctxt →
  letP ? _ := Contract_manager_storage.is_manager_key_revealed ctxt manager in
  True.
Proof.
Admitted.

The function [check_public_key] is valid.

Lemma check_public_key_is_valid public_key expected_hash :
  letP ? _ :=
    Contract_manager_storage.check_public_key public_key expected_hash in
  True.
Proof.
Admitted.

The function [reveal_manager_key] is valid.

Lemma reveal_manager_key_is_valid check_consistency ctxt manager public_key :
  Raw_context.Valid.t ctxt →
  letP ? ctxt :=
    Contract_manager_storage.reveal_manager_key
      check_consistency ctxt manager public_key in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [get_manager_key] is valid.

Lemma get_manager_key_is_valid error_value ctxt pkh :
  match error_value with
  | Some error_value ⇒ Error.not_internal [error_value]
  | None ⇒ True
  end →
  Raw_context.Valid.t ctxt →
  letP ? _ := Contract_manager_storage.get_manager_key error_value ctxt pkh in
  True.
Proof.
Admitted.

The function [remove_existing] is valid.

Lemma remove_existing_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP ? ctxt := Contract_manager_storage.remove_existing ctxt contract in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

@TODO commented out [axiom Storage.Eq.Contracts.Manager.eq.] from [Storage.v] used in the proof. [is_manager_key_revealed] after [reveal_manager_key] returns [Pervasives.Ok true]

Lemma reveal_implies_is_manager_key_revelead_to_be_true
  (absolute_key : Context.key) ctxt
  (pkh : public_key_hash) (pk : public_key) :
  letP ? ctxt' := Contract_manager_storage.reveal_manager_key
    (Some false) ctxt pkh pk in
  Contract_manager_storage.is_manager_key_revealed
      ctxt' pkh = Pervasives.Ok true.
Proof.
  intros.
Admitted.

@TODO commented out [axiom Storage.Eq.Contracts.Manager.eq.] from [Storage.v] used in the proof. [get_manager_key] after [reveals] returns [Pervasives.Ok]

Lemma reveal_implies_get_manager_key_success
  ctxt (pkh : public_key_hash) (pk : public_key) :
  letP ? ctxt' := Contract_manager_storage.reveal_manager_key
    (Some false) ctxt pkh pk in
  Pervasives.is_ok (Contract_manager_storage.get_manager_key
    None ctxt' pkh).
Proof.
  intros.
Admitted.

@TODO commented out [axiom Storage.Eq.Contracts.Manager.eq.] from [Storage.v] used in the proof. [remove_existing] after [get_manager_key] success returns [Pervasives.Ok] Lemma get_manager_key_implies_remove_exists_success ctxt pkh : Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.find) ctxt (Contract_repr.Implicit 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. Admitted.