🌍 Global_constants_storage.v
Proofs
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Global_constants_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
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'.
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.
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.
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.
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.
letP? depth := Global_constants_storage.check_depth node in
Pervasives.Int.Valid.t depth.
Proof.
Admitted.
The function [register] is valid.