🍬 Script_set.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.