✒️ Contract_delegate_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [find] is valid.

Lemma find_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP? _ := Contract_delegate_storage.find ctxt contract in
  True.
Proof.
Admitted.

The function [init_value] is valid.

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

The function [unlink] is valid.

Lemma unlink_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Contract_delegate_storage.unlink ctxt contract in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [delete] is valid.

Lemma delete_is_valid ctxt contract :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Contract_delegate_storage.delete ctxt contract in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [set] is valid.

Lemma set_is_valid ctxt contract delegate :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Contract_delegate_storage.set ctxt contract delegate in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [delegated_contracts] is valid.

Lemma delegated_contracts_is_valid ctxt delegate :
  Raw_context.Valid.t ctxt →
  letP? _ := Contract_delegate_storage.delegated_contracts ctxt delegate in
  True.
Proof.
Admitted.