🍬 Script_big_map.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_big_map.

Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_comparable_input_size.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_comparable.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

The function [empty] is valid.

Lemma empty_is_valid {k b k_cmp b_t} :
  Script_typed_ir.ty.Valid.proj_rel k k_cmp →
  Script_typed_ir.ty.Valid.proj_rel b b_t →
  Script_typed_ir.Valid.value
    (Ty.Big_map k b)
    (Script_big_map.empty (a := Ty.to_Set k) (b := Ty.to_Set b) k_cmp b_t).
Proof.
  intros; now constructor.
Qed.

The function [update_by_hash] is valid.

Lemma update_by_hash_is_valid
  {k v : Ty.t}
  (key_hash : Script_expr_hash.t)
  (key_value : Ty.to_Set k)
  (value_value : option (Ty.to_Set v))
  (big_map : Script_typed_ir.big_map)
  : Script_typed_ir.Valid.value (Ty.Big_map k v) big_map →
    Script_typed_ir.Valid.value (Ty.Big_map k v)
      (Script_big_map.update_by_hash key_hash key_value value_value big_map).
Proof.
Admitted.

The function [update] is valid.

Lemma update_is_valid
  {k v : Ty.t}
  (ctxt : Alpha_context.context)
  (key_value : Ty.to_Set k)
  (value_value : option (Ty.to_Set v))
  (big_map : Script_typed_ir.big_map)
  : Raw_context.Valid.t ctxt →
    Script_typed_ir.Valid.value (Ty.Big_map k v) big_map →
    letP? '(map, ctxt) :=
      Script_big_map.update ctxt key_value value_value big_map in
    Script_typed_ir.Valid.value (Ty.Big_map k v) map ∧
      Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [get_and_update] is valid.

Lemma get_and_update_is_valid
  {k v : Ty.t}
  (ctxt : Alpha_context.context)
  (key_value : Ty.to_Set k)
  (value_value : option (Ty.to_Set v))
  (big_map : Script_typed_ir.big_map)
  : Raw_context.Valid.t ctxt →
    Script_typed_ir.Valid.value (Ty.Big_map k v) big_map →
    letP? '((_, map), ctxt) :=
      Script_big_map.get_and_update ctxt key_value value_value big_map in
    Script_typed_ir.Valid.value (Ty.Big_map k v) map ∧
      Raw_context.Valid.t ctxt.
Proof.
Admitted.