🌍 Global_constants_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Global_constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Script_repr.

(* @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'.