🍬 Script_cache.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_cache.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [load_and_elaborate] is valid.

Definition load_and_elaborate_is_valid
  ctxt (addr : Contract_hash.t) :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Script_cache.load_and_elaborate ctxt addr in
    Raw_context.Valid.t ctxt.
Proof.
Admitted.

Module Client.

The function [value_of_identifier] is valid.

  Lemma value_of_identifier_is_valid ctxt identifier :
    Raw_context.Valid.t ctxt →
    letP? _ := Script_cache.Client.value_of_identifier ctxt identifier in
      Raw_context.Valid.t ctxt.
  Proof.
  Admitted.
End Client.

The function [find] is valid.

Lemma find_is_valid ctxt addr :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _, _) := Script_cache.find ctxt addr in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [update] is valid.

Lemma update_is_valid ctxt identifier updated_script approx_size :
  Raw_context.Valid.t ctxt →
  letP? ctxt :=
    Script_cache.update ctxt identifier updated_script approx_size in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [entries] is valid.

Lemma entries_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP? ctxt := Script_cache.entries ctxt in True.
Proof.
Admitted.

The function [insert] is valid.

Lemma insert_is_valid ctxt addr updated_script approx_size :
  Raw_context.Valid.t ctxt →
  letP? ctxt :=
    Script_cache.insert ctxt addr updated_script approx_size in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.