Skip to main content

🍬 Script_big_map.v

Proofs

See code, Gitlab , OCaml

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.
The function [update] is valid.
The function [get_and_update] is valid.