🍬 Script_set.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_set.
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_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_set.
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_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
We axiomatize that if we [add] and element to
the set, which is alsready in the set, i.e. [mem elem set = true],
then set wouldn't change.
Axiom BOXED_set_OPS_add_existing : ∀
(a : Ty.t) (t : Set)
(OPS : Script_typed_ir.Boxed_set_OPS (t:=t) (elt:= Ty.to_Set a))
(boxed : t)
(v : Ty.to_Set a),
OPS.(Script_typed_ir.Boxed_set_OPS.mem) v boxed = true →
(OPS.(Script_typed_ir.Boxed_set_OPS.add) v boxed) = boxed.
(a : Ty.t) (t : Set)
(OPS : Script_typed_ir.Boxed_set_OPS (t:=t) (elt:= Ty.to_Set a))
(boxed : t)
(v : Ty.to_Set a),
OPS.(Script_typed_ir.Boxed_set_OPS.mem) v boxed = true →
(OPS.(Script_typed_ir.Boxed_set_OPS.add) v boxed) = boxed.
Updating a valid set returns a valid set.
Lemma update_is_valid {a : Ty.t} (v : Ty.to_Set a)
(b : bool) (x : Script_typed_ir.set (Ty.to_Set a)) :
Script_typed_ir.Valid.value a v →
Script_typed_ir.Valid.value (Ty.Set_ a) x →
Script_typed_ir.Valid.value (Ty.Set_ a) (Script_set.update v b x).
Proof.
intros Hv Hax.
unfold Script_set.update.
step. step.
destruct b0. simpl.
step.
{ step.
{ rewrite BOXED_set_OPS_add_existing; trivial. }
{ admit. } (* axiom that if we add new element, size increases. *)
}
{ step.
{ admit. } (* axiom that if we remove existing element size decreases *)
{ admit. } (* axiom that if we remove non-existing element,
size stays the same *)
}
Admitted.
(b : bool) (x : Script_typed_ir.set (Ty.to_Set a)) :
Script_typed_ir.Valid.value a v →
Script_typed_ir.Valid.value (Ty.Set_ a) x →
Script_typed_ir.Valid.value (Ty.Set_ a) (Script_set.update v b x).
Proof.
intros Hv Hax.
unfold Script_set.update.
step. step.
destruct b0. simpl.
step.
{ step.
{ rewrite BOXED_set_OPS_add_existing; trivial. }
{ admit. } (* axiom that if we add new element, size increases. *)
}
{ step.
{ admit. } (* axiom that if we remove existing element size decreases *)
{ admit. } (* axiom that if we remove non-existing element,
size stays the same *)
}
Admitted.