🍬 Script_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_map.

Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_comparable_input_size.
(* Require TezosOfOCaml.Proto_alpha.Proofs.Script_comparable. *)
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_from] is valid

Lemma empty_from_is_valid
  (k v v': Ty.t) tyk
  (k_cmp : Script_typed_ir.ty.Comparable.t tyk)
  (k_tyk : Script_typed_ir.ty.Valid.proj_rel k tyk)
  (map : Script_typed_ir.map (Ty.to_Set k) (Ty.to_Set v))
  : Script_typed_ir.Valid.value (Ty.Map k v) map →
    Script_typed_ir.Valid.value
      (Ty.Map k v') (Script_map.empty_from (c := Ty.to_Set v') map).
Proof.
Admitted.

The function [empty] is valid

Lemma empty_is_valid
  (k v : Ty.t) tyk
  (k_cmp : Script_typed_ir.ty.Comparable.t tyk)
  (k_tyk : Script_typed_ir.ty.Valid.proj_rel k tyk)
  : Script_typed_ir.Valid.value
      (Ty.Map k v) (Script_map.empty (a := Ty.to_Set k) (b := Ty.to_Set v) tyk).
Proof.
Admitted.

The function [update] is valid

Lemma update_is_valid
  (k v : Ty.t) tyk
  (map : Script_typed_ir.map (Ty.to_Set k) (Ty.to_Set v))
  (k_cmp : Script_typed_ir.ty.Comparable.t tyk)
  (k_tyk : Script_typed_ir.ty.Valid.proj_rel k tyk)
  (key : Ty.to_Set k)
  (val : option (Ty.to_Set v)) :
  Script_typed_ir.Valid.value (Ty.Map k v) (Script_map.update key val map).
Proof.
Admitted.