🍬 Script_map.v
Proofs
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.
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.
(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.
(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.
(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.