🌍 Global_constants_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Global_constants_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [get] is valid.

Lemma get_is_valid ctxt hash :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Global_constants_storage.get ctxt hash in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

(* @TODO *)
Axiom register_get_eq : ∀ {ctxt} {value : Script_repr.expr},
  letP? '(ctxt, hash, size) := Global_constants_storage.register ctxt value in
  letP? '(ctxt, value'):= Global_constants_storage.get ctxt hash in
  value = value'.

The function [expr_to_address_in_context] is valid.

Lemma expr_to_address_in_context_is_valid ctxt expr :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) :=
    Global_constants_storage.expr_to_address_in_context ctxt expr in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [expand_node] is valid.

Lemma expand_node_is_valid ctxt node :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Global_constants_storage.expand_node ctxt node in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [expand] is valid.

Lemma expand_is_valid ctxt expr :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) := Global_constants_storage.expand ctxt expr in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [check_depth] is valid.

Lemma check_depth_is_valid {A B} (node : Micheline.node A B) :
  letP? depth := Global_constants_storage.check_depth node in
  Pervasives.Int.Valid.t depth.
Proof.
Admitted.

The function [register] is valid.

Lemma register_is_valid ctxt value :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _, _) := Global_constants_storage.register ctxt value in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.