Skip to main content

🍬 Script_typed_ir.v

Proofs

See code, See simulations, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require Import TezosOfOCaml.Proto_alpha.Script_typed_ir.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Chain_id.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Timelock.
Require TezosOfOCaml.Proto_alpha.Proofs.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int_repr.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_typed_ir.

Module Script_signature.
  Import Proto_alpha.Script_typed_ir.Script_signature.

  Lemma make_get (s : t) : make (get s) = s.
  Proof.
    now destruct s.
  Qed.

  Lemma get_make (s : Signature.t) : get (make s) = s.
  Proof.
    reflexivity.
  Qed.

  Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True) encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

  Definition canonize (s : t) : t :=
    make (Signature.canonize (get s)).

  Lemma compare_is_valid : Compare.Valid.t (fun _True) canonize compare.
  Proof.
    apply (Compare.equality (Compare.projection get Signature.compare));
      [sauto lq: on|].
    eapply Compare.implies.
    { eapply Compare.projection_is_valid.
      apply Signature.compare_is_valid.
    }
    all: unfold canonize, get; hauto l: on.
  Qed.
End Script_signature.

Module Script_chain_id.
  Import Proto_alpha.Script_typed_ir.Script_chain_id.

  Lemma compare_is_valid : Compare.Valid.t (fun _True) id compare.
  Proof.
    apply (Compare.equality (
      let proj '(Chain_id_tag x) := x in
      Compare.projection proj Chain_id.compare
    )); [sauto q: on|].
    eapply Compare.implies.
    { eapply Compare.projection_is_valid.
      apply Chain_id.compare_is_valid.
    }
    all: sauto q: on.
  Qed.

  Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True) encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Script_chain_id.

Module Script_timelock.
  Import Proto_alpha.Script_typed_ir.Script_timelock.

  Lemma chest_key_encoding_is_valid : Data_encoding.Valid.t (fun _True) chest_key_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve chest_key_encoding_is_valid : Data_encoding_db.

  Lemma chest_encoding_is_valid : Data_encoding.Valid.t (fun _True) chest_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve chest_encoding_is_valid : Data_encoding_db.

End Script_timelock.

Module Ticket.
  Module Valid.
    Import Script_typed_ir.ticket.

    Record t {a : Set} (x : Script_typed_ir.ticket a) : Prop := {
      amount : 0 let 'Alpha_context.Script_int.Num_tag x' := x.(amount) in x';
    }.
  End Valid.
End Ticket.

Module With_family.
If a type is comparable.
The validity of the various Michelson types.
  Module Valid.
The validity of [ty].
    Fixpoint ty {a : Ty.t} (t : With_family.ty a) : Prop :=
      match t with
      | With_family.Unit_tTrue
      | With_family.Int_tTrue
      | With_family.Nat_tTrue
      | With_family.Signature_tTrue
      | With_family.String_tTrue
      | With_family.Bytes_tTrue
      | With_family.Mutez_tTrue
      | With_family.Key_hash_tTrue
      | With_family.Key_tTrue
      | With_family.Timestamp_tTrue
      | With_family.Address_tTrue
      | With_family.Tx_rollup_l2_address_tTrue
      | With_family.Bool_tTrue
      | With_family.Pair_t t1 t2 _ _ty t1 ty t2
      | With_family.Union_t t1 t2 _ _ty t1 ty t2
      | With_family.Lambda_t arg ret _ty arg ty ret
      | With_family.Option_t t _ _ty t
      | With_family.List_t t _ty t
      | With_family.Set_t t _With_family.is_Comparable t ty t
      | With_family.Map_t key value _
        With_family.is_Comparable key ty key ty value
      | With_family.Big_map_t key value _
        With_family.is_Comparable key ty key ty value
      | With_family.Contract_t arg _ty arg
      | With_family.Sapling_transaction_t _True
      | With_family.Sapling_transaction_deprecated_t _True
      | With_family.Sapling_state_t _True
      | With_family.Operation_tTrue
      | With_family.Chain_id_tTrue
      | With_family.Never_tTrue
      | With_family.Bls12_381_g1_tTrue
      | With_family.Bls12_381_g2_tTrue
      | With_family.Bls12_381_fr_tTrue
      | With_family.Ticket_t t _With_family.is_Comparable t ty t
      | With_family.Chest_key_tTrue
      | With_family.Chest_tTrue
      end.

The validity of [stack_ty].
    Fixpoint stack_ty {s} (stack : With_family.stack_ty s) : Prop :=
      match stack with
      | With_family.Item_t t restty t stack_ty rest
      | With_family.Bot_tTrue
      end.

The validity of [kinfo].
    Definition kinfo {s} (info : With_family.kinfo s) : Prop :=
      let 'With_family.Kinfo _ kstack_ty := info in
      stack_ty kstack_ty.

The validity of [view_signature].
    Definition view_signature {a b}
      (signature : With_family.view_signature a b) : Prop :=
      let 'With_family.View_signature _ i_ty o_ty := signature in
      ty i_ty ty o_ty.

The validity of [kinstr].
    #[bypass_check(guard)]
    Fixpoint kinstr {s f} (i : With_family.kinstr s f) {struct i} : Prop :=
      match i with
      (*
        Stack
        -----
      *)

      | With_family.IDrop info k
          kinfo info kinstr k
      | With_family.IDup info k
          kinfo info kinstr k
      | With_family.ISwap info k
          kinfo info kinstr k
      | With_family.IConst info v k
          kinfo info value v kinstr k
      (*
        Pairs
        -----
      *)

      | With_family.ICons_pair info k
          kinfo info kinstr k
      | With_family.ICar info k
          kinfo info kinstr k
      | With_family.ICdr info k
          kinfo info kinstr k
      | With_family.IUnpair info k
          kinfo info kinstr k
      (*
        Options
        -------
      *)

      | With_family.ICons_some info k
          kinfo info kinstr k
      | With_family.ICons_none info k
          kinfo info kinstr k
      | With_family.IIf_none info branch_if_none branch_if_some k
          kinfo info kinstr branch_if_none kinstr branch_if_some kinstr k
      | With_family.IOpt_map info body k
          kinfo info kinstr body kinstr k
      (*
        Unions
        ------
      *)

      | With_family.ICons_left info k
          kinfo info kinstr k
      | With_family.ICons_right info k
          kinfo info kinstr k
      | With_family.IIf_left info branch_if_left branch_if_right k
          kinfo info kinstr branch_if_left kinstr branch_if_right kinstr k
      (*
        Lists
        -----
      *)

      | With_family.ICons_list info k
          kinfo info kinstr k
      | With_family.INil info k
          kinfo info kinstr k
      | With_family.IIf_cons info branch_if_cons branch_if_nil k
          kinfo info kinstr branch_if_cons kinstr branch_if_nil kinstr k
      | With_family.IList_map info body k
          kinfo info kinstr body kinstr k
      | With_family.IList_iter info body k
          kinfo info kinstr body kinstr k
      | With_family.IList_size info k
          kinfo info kinstr k
      (*
      Sets
      ----
        *)

      | With_family.IEmpty_set info t instr
          kinfo info ty t kinstr instr
      | With_family.ISet_iter info instr1 instr2
          kinfo info kinstr instr1 kinstr instr2
      | With_family.ISet_mem info instr
          kinfo info kinstr instr
      | With_family.ISet_update info instr
          kinfo info kinstr instr
      | With_family.ISet_size info instr
          kinfo info kinstr instr
      (*
        Maps
        ----
        *)

      | With_family.IEmpty_map info key instr
          kinfo info ty key kinstr instr
      | With_family.IMap_map info instr1 instr2
          kinfo info kinstr instr1 kinstr instr2
      | With_family.IMap_iter info instr1 instr2
          kinfo info kinstr instr1 kinstr instr2
      | With_family.IMap_mem info instr
          kinfo info kinstr instr
      | With_family.IMap_get info instr
          kinfo info kinstr instr
      | With_family.IMap_update info instr
          kinfo info kinstr instr
      | With_family.IMap_get_and_update info instr
          kinfo info kinstr instr
      | With_family.IMap_size info instr
          kinfo info kinstr instr
      (*
        Big maps
        --------
        *)

      | With_family.IEmpty_big_map info key val instr
          kinfo info ty key ty val kinstr instr
      | With_family.IBig_map_mem info instr
          kinfo info kinstr instr
      | With_family.IBig_map_get info instr
          kinfo info kinstr instr
      | With_family.IBig_map_update info instr
          kinfo info kinstr instr
      | With_family.IBig_map_get_and_update info instr
          kinfo info kinstr instr
      (*
        Strings
        -------
        *)

      | With_family.IConcat_string info instr
          kinfo info kinstr instr
      | With_family.IConcat_string_pair info instr
          kinfo info kinstr instr
      | With_family.ISlice_string info instr
          kinfo info kinstr instr
      | With_family.IString_size info instr
          kinfo info kinstr instr
      (*
        Bytes
        -----
        *)

      | With_family.IConcat_bytes info instr
          kinfo info kinstr instr
      | With_family.IConcat_bytes_pair info instr
          kinfo info kinstr instr
      | With_family.ISlice_bytes info instr
          kinfo info kinstr instr
      | With_family.IBytes_size info instr
          kinfo info kinstr instr
      (*
        Timestamps
        ----------
        *)

      | With_family.IAdd_seconds_to_timestamp info instr
          kinfo info kinstr instr
      | With_family.IAdd_timestamp_to_seconds info instr
          kinfo info kinstr instr
      | With_family.ISub_timestamp_seconds info instr
          kinfo info kinstr instr
      | With_family.IDiff_timestamps info instr
          kinfo info kinstr instr
      (*
        Tez
        ---
        *)

      | With_family.IAdd_tez info instr
          kinfo info kinstr instr
      | With_family.ISub_tez info instr
          kinfo info kinstr instr
      | With_family.ISub_tez_legacy info instr
          kinfo info kinstr instr
      | With_family.IMul_teznat info instr
          kinfo info kinstr instr
      | With_family.IMul_nattez info instr
          kinfo info kinstr instr
      | With_family.IEdiv_teznat info instr
          kinfo info kinstr instr
      | With_family.IEdiv_tez info instr
          kinfo info kinstr instr
      (*
        Booleans
        --------
      *)

      | With_family.IOr info k
          kinfo info kinstr k
      | With_family.IAnd info k
          kinfo info kinstr k
      | With_family.IXor info k
          kinfo info kinstr k
      | With_family.INot info k
          kinfo info kinstr k
      (*
        Integers
        --------
        *)

      | With_family.IIs_nat info instr
          kinfo info kinstr instr
      | With_family.INeg info instr
          kinfo info kinstr instr
      | With_family.IAbs_int info instr
          kinfo info kinstr instr
      | With_family.IInt_nat info instr
          kinfo info kinstr instr
      | With_family.IAdd_int info instr
          kinfo info kinstr instr
      | With_family.IAdd_nat info instr
          kinfo info kinstr instr
      | With_family.ISub_int info instr
          kinfo info kinstr instr
      | With_family.IMul_int info instr
          kinfo info kinstr instr
      | With_family.IMul_nat info instr
          kinfo info kinstr instr
      | With_family.IEdiv_int info instr
          kinfo info kinstr instr
      | With_family.IEdiv_nat info instr
          kinfo info kinstr instr
      | With_family.ILsl_nat info instr
          kinfo info kinstr instr
      | With_family.ILsr_nat info instr
          kinfo info kinstr instr
      | With_family.IOr_nat info instr
          kinfo info kinstr instr
      | With_family.IAnd_nat info instr
          kinfo info kinstr instr
      | With_family.IAnd_int_nat info instr
          kinfo info kinstr instr
      | With_family.IXor_nat info instr
          kinfo info kinstr instr
      | With_family.INot_int info instr
          kinfo info kinstr instr
      (*
        Control
        -------
      *)

      | With_family.IIf info branch_if_true branch_if_false k
          kinfo info kinstr branch_if_true kinstr branch_if_false kinstr k
      | With_family.ILoop info body k
          kinfo info kinstr body kinstr k
      | With_family.ILoop_left info bl br
          kinfo info kinstr bl kinstr br
      | With_family.IDip info b k
          kinfo info kinstr b kinstr k
      | With_family.IExec info k
          kinfo info kinstr k
      | With_family.IApply info capture_ty k
          kinfo info ty capture_ty kinstr k
      | With_family.ILambda info lam k
          kinfo info lambda lam kinstr k
      | With_family.IFailwith info kloc tv
          kinfo info ty tv
      (*
        Comparison
        ----------
        *)

      | With_family.ICompare info t instr
          kinfo info ty t kinstr instr
      (*
        Comparators
        -----------
        *)

      | With_family.IEq info instr
          kinfo info kinstr instr
      | With_family.INeq info instr
          kinfo info kinstr instr
      | With_family.ILt info instr
          kinfo info kinstr instr
      | With_family.IGt info instr
          kinfo info kinstr instr
      | With_family.ILe info instr
          kinfo info kinstr instr
      | With_family.IGe info instr
          kinfo info kinstr instr
      (*
        Protocol
        --------
        *)

      | With_family.IAddress info instr
          kinfo info kinstr instr
      | With_family.IContract info t str instr
          kinfo info ty t kinstr instr
      | With_family.IView info sign instr
          kinfo info view_signature sign kinstr instr
      | With_family.ITransfer_tokens info instr
          kinfo info kinstr instr
      | With_family.IImplicit_account info instr
          kinfo info kinstr instr
      | With_family.ICreate_contract info storage_type code instr
          kinfo info ty storage_type kinstr instr
      | With_family.ISet_delegate info instr
          kinfo info kinstr instr
      | With_family.INow info instr
          kinfo info kinstr instr
      | With_family.IBalance info instr
          kinfo info kinstr instr
      | With_family.ILevel info instr
          kinfo info kinstr instr
      | With_family.ICheck_signature info instr
          kinfo info kinstr instr
      | With_family.IHash_key info instr
          kinfo info kinstr instr
      | With_family.IPack info t instr
          kinfo info ty t kinstr instr
      | With_family.IUnpack info t instr
          kinfo info ty t kinstr instr
      | With_family.IBlake2b info instr
          kinfo info kinstr instr
      | With_family.ISha256 info instr
          kinfo info kinstr instr
      | With_family.ISha512 info instr
          kinfo info kinstr instr
      | With_family.ISource info instr
          kinfo info kinstr instr
      | With_family.ISender info instr
          kinfo info kinstr instr
      | With_family.ISelf info t str instr
          kinfo info ty t kinstr instr
      | With_family.ISelf_address info instr
          kinfo info kinstr instr
      | With_family.IAmount info instr
          kinfo info kinstr instr
      | With_family.ISapling_empty_state info sz instr
          kinfo info Sapling_repr.Memo_size.Valid.t sz kinstr instr
      | With_family.ISapling_verify_update info instr
          kinfo info kinstr instr
      | With_family.IDig info v spref instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IDug info v spref instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IDipn info v spref instr1 instr2
          kinfo info Pervasives.Int.Valid.t v kinstr instr1 kinstr instr2
      | With_family.IDropn info v spref instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IChainId info instr
          kinfo info kinstr instr
      | With_family.INever info
          kinfo info
      | With_family.IVoting_power info instr
          kinfo info kinstr instr
      | With_family.ITotal_voting_power info instr
          kinfo info kinstr instr
      | With_family.IKeccak info instr
          kinfo info kinstr instr
      | With_family.ISha3 info instr
          kinfo info kinstr instr
      | With_family.IAdd_bls12_381_g1 info instr
          kinfo info kinstr instr
      | With_family.IAdd_bls12_381_g2 info instr
          kinfo info kinstr instr
      | With_family.IAdd_bls12_381_fr info instr
          kinfo info kinstr instr
      | With_family.IMul_bls12_381_g1 info instr
          kinfo info kinstr instr
      | With_family.IMul_bls12_381_g2 info instr
          kinfo info kinstr instr
      | With_family.IMul_bls12_381_fr info instr
          kinfo info kinstr instr
      | With_family.IMul_bls12_381_z_fr info instr
          kinfo info kinstr instr
      | With_family.IMul_bls12_381_fr_z info instr
          kinfo info kinstr instr
      | With_family.IInt_bls12_381_fr info instr
          kinfo info kinstr instr
      | With_family.INeg_bls12_381_g1 info instr
          kinfo info kinstr instr
      | With_family.INeg_bls12_381_g2 info instr
          kinfo info kinstr instr
      | With_family.INeg_bls12_381_fr info instr
          kinfo info kinstr instr
      | With_family.IPairing_check_bls12_381 info instr
          kinfo info kinstr instr
      | With_family.IComb info v comb instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IUncomb info v comb instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IComb_get info v comb instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IComb_set info v comb instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.IDup_n info v dup_n instr
          kinfo info Pervasives.Int.Valid.t v kinstr instr
      | With_family.ITicket info instr
          kinfo info kinstr instr
      | With_family.IRead_ticket info instr
          kinfo info kinstr instr
      | With_family.ISplit_ticket info instr
          kinfo info kinstr instr
      | With_family.IJoin_tickets info t instr
          kinfo info ty t kinstr instr
      | With_family.IOpen_chest info instr
          kinfo info kinstr instr
      (*
        Internal control instructions
        -----------------------------
      *)

      | With_family.IHalt info
          kinfo info
      end

    
The validity of a [lambda].
    with lambda {arg ret} (lam : With_family.lambda arg ret) {struct lam} : Prop :=
        let '(descr, _) := lam in kdescr descr

    
The validity of a [kdescr].
    with kdescr {s f} (descr : With_family.kdescr s f) {struct descr} : Prop :=
        stack_ty descr.(With_family.kdescr.kbef)
        stack_ty descr.(With_family.kdescr.kaft)
        kinstr descr.(With_family.kdescr.kinstr)

    
The validity of a Michelson value.
    with value {t : Ty.t} {struct t} :
      With_family.ty_to_dep_Set t Prop :=
      match t return With_family.ty_to_dep_Set t Prop with
      | Ty.Unitfun xTrue
      | Ty.Num Ty.Num.Intfun _True
      | Ty.Num Ty.Num.NatScript_int_repr.N.Valid.t
      | Ty.Signaturefun xTrue
      | Ty.Stringfun xTrue
      | Ty.Bytesfun xTrue
      | Ty.Mutezfun xTez_repr.Valid.t x
      | Ty.Key_hashfun xTrue
      | Ty.Keyfun xTrue
      | Ty.Timestampfun xTrue
      | Ty.Addressfun xTrue
      | Ty.Tx_rollup_l2_addressfun xTrue
      | Ty.Boolfun xTrue
      | Ty.Pair ty1 ty2fun '(x1, x2) ⇒ @value ty1 x1 @value ty2 x2
      | Ty.Union ty1 ty2fun x
        match x with
        | Script_typed_ir.L x ⇒ @value ty1 x
        | Script_typed_ir.R x ⇒ @value ty2 x
        end
      | Ty.Lambda ty_arg ty_reslambda
      | Ty.Option tyfun x
        match x with
        | NoneTrue
        | Some x ⇒ @value ty x
        end
      | Ty.List ty
          fun xsForall (fun x ⇒ @value ty x) xs.(boxed_list.elements)
      | Ty.Set_ kfun xScript_family.Ty.is_Comparable k
      | Ty.Map k vfun xScript_family.Ty.is_Comparable k
      | Ty.Big_map _ _fun x
        List.Forall
          (fun '(_, (k, v))
             value k Option.Forall value v)
          (Big_map_overlay.(Map.S.bindings)
            x.(With_family.big_map.diff).(big_map_overlay.map))
        With_family.is_Comparable x.(With_family.big_map.key_type)
        ty x.(With_family.big_map.key_type)
        ty x.(With_family.big_map.value_type)
      | Ty.Contract _fun '(With_family.Typed_contract ty _) ⇒ Valid.ty ty
      | Ty.Sapling_transactionfun xTrue
      | Ty.Sapling_transaction_deprecatedfun xTrue
      | Ty.Sapling_statefun xTrue
      | Ty.Operationfun xTrue
      | Ty.Chain_idfun xTrue
      | Ty.Neverfun xFalse
      | Ty.Bls12_381_g1fun xTrue
      | Ty.Bls12_381_g2fun xTrue
      | Ty.Bls12_381_frfun xTrue
      | Ty.Ticket tyfun xTicket.Valid.t x
      | Ty.Chest_keyfun xTrue
      | Ty.Chestfun xTrue
      end.

The validity of a [big_map].
    Definition big_map {k v} (x : With_family.big_map k v) : Prop :=
      @value (Ty.Big_map _ _) x.
  End Valid.

[of_value] is an inverse of [to_value].
  Fixpoint of_value_to_value {ty : Ty.t} (x : With_family.ty_to_dep_Set ty)
    {struct ty} :
    Script_family.Ty.is_Comparable ty
    With_family.of_value (With_family.to_value x) = Some x.
  Proof.
    destruct ty; simpl; intros; try easy;
      unfold Option.map; step; trivial;
      repeat (rewrite of_value_to_value; try easy; simpl).
  Qed.

[to_value] is an inverse of [of_value].
  Fixpoint to_value_of_value {ty : Ty.t} (x : Ty.to_Set ty) {struct ty} :
    Script_family.Ty.is_Comparable ty
    match With_family.of_value x with
    | Some x'With_family.to_value x' = x
    | NoneFalse
    end.
  Proof.
    destruct ty; simpl; intros; try easy;
      step;
      repeat match goal with
      | |- context[With_family.of_value ?x] ⇒
        pose proof (to_value_of_value _ x);
        destruct (With_family.of_value x);
        simpl
      end;
      try easy;
      hauto lq: on.
  Qed.
End With_family.

Module Type_size.
The simulation [dep_check_eq] is valid.
  Lemma dep_check_eq_eq {error_trace}
    (error_details : Script_tc_errors.dep_error_details error_trace)
    (x_value : int) (y_value : int) :
    Type_size.dep_check_eq error_details x_value y_value =
      Type_size.check_eq (Script_tc_errors.to_error_details error_details)
        x_value y_value.
  Proof.
    unfold Type_size.dep_check_eq, Type_size.check_eq.
    step; [reflexivity|].
    now destruct error_details; simpl; rewrite cast_eval.
  Qed.
End Type_size.

The simulation [dep_kinfo_of_kinstr] is valid.
The simulation [dep_is_comparable] is valid.
The simulation [dep_pair_t] is valid.
We prove that dependent version of [pair_key] gives the same result as original [pair_key] function from the [Proto_alpha]
We prove that dependent version of [pair_3_key] gives the same result as original [pair_3_key] function from the [Proto_alpha]
Lemma dep_pair_3_key_eq
  loc {tl tm tr}
  (tyl : With_family.ty tl)
  (tym : With_family.ty tm)
  (tyr : With_family.ty tr) :
  (let? ty := dep_pair_3_key loc tyl tym tyr in
  return? (With_family.to_ty ty)) =
  Script_typed_ir.pair_3_key loc
    (With_family.to_ty tyl)
    (With_family.to_ty tym)
    (With_family.to_ty tyr).
Proof.
  unfold dep_pair_3_key, Script_typed_ir.pair_3_key.
  rewrite <- dep_pair_key_eq.
  destruct dep_pair_key; simpl; [|reflexivity].
  apply dep_pair_key_eq.
Qed.

The simulation [dep_option_t] is valid.
The simulation [dep_operation_t] is valid.
The simulation [dep_list_operation_t] is valid.