🍬 Script_ir_translator.v

Proofs

See code, See simulations, Gitlab , OCaml

destructs [Alpha_context.Gas.consume ctxt] expression in the goal

Ltac consume_gas :=
destruct Alpha_context.Gas.consume eqn:?H_gc in |- *; simpl; trivial.

destructs [Gas_monad.run ctxt m] expression in the goal

Ltac run_gas_monad := destruct Gas_monad.run eqn:?H_gmr in |- ×.

Since [dep_cinstr] contains a function, we cannot convert it back to [cinstr]. Instead, we define a custom equality predicate between [dep_cinstr] and [cinstr].

Module Eq_cinstr.
  Definition t {s u} (dep_x : dep_cinstr s u) (x : cinstr) : Prop :=
    ∀ {f} (kinfo : With_family.kinfo s) (kinstr : With_family.kinstr u f),
    With_family.to_kinstr (dep_x.(dep_cinstr.apply) kinfo kinstr) =
    x.(cinstr.apply)
      (With_family.to_kinfo kinfo) (With_family.to_kinstr kinstr).
End Eq_cinstr.

Equality between [dep_descr] and [descr].

Module Eq_descr.
  Record t {s u} (dep_x : dep_descr s u) (x : descr) : Prop := {
    loc : dep_x.(dep_descr.loc) = x.(descr.loc);
    bef : With_family.to_stack_ty dep_x.(dep_descr.bef) = x.(descr.bef);
    aft : With_family.to_stack_ty dep_x.(dep_descr.aft) = x.(descr.aft);
    aft_v : Script_typed_ir.With_family.Valid.stack_ty dep_x.(dep_descr.aft);
    instr : Eq_cinstr.t dep_x.(dep_descr.instr) x.(descr.instr);
  }.
End Eq_descr.

The simulation [dep_close_descr] is valid.

Lemma dep_close_descr_eq {s u} (dep_x : dep_descr s u) (x : descr) :
  Eq_descr.t dep_x x →
  With_family.to_kdescr (dep_close_descr dep_x) = close_descr x.
Proof.
  intros [].
  unfold dep_close_descr, close_descr; simpl.
  f_equal; trivial.
  rewrite instr; simpl.
  now repeat f_equal.
Qed.

The simulation [dep_kinfo_of_descr] is valid.

Lemma dep_kinfo_of_descr_eq {s u} (dep_x : dep_descr s u) (x : descr) :
  Eq_descr.t dep_x x →
  With_family.to_kinfo (dep_kinfo_of_descr dep_x) = kinfo_of_descr x.
Proof.
  intros [].
  unfold dep_kinfo_of_descr, kinfo_of_descr; simpl.
  now f_equal.
Qed.

The simulation [dep_compose_descr] is valid.

Lemma dep_compose_descr_eq {s u v} loc_value
  (dep_d1 : dep_descr s u) (dep_d2 : dep_descr u v) (d1 d2 : descr) :
  Eq_descr.t dep_d1 d1 →
  Eq_descr.t dep_d2 d2 →
  Eq_descr.t
    (dep_compose_descr loc_value dep_d1 dep_d2)
    (compose_descr loc_value d1 d2).
Proof.
  intros [] [].
  unfold dep_compose_descr, compose_descr.
  constructor; simpl; trivial.
  unfold Eq_cinstr.t; intros.
  simpl.
  repeat match goal with
  | H : Eq_cinstr.t _ _ |- _ ⇒ rewrite H
  end.
  repeat f_equal; now apply dep_kinfo_of_descr_eq.
Qed.

The simulation [dep_ty_of_comparable_ty] is valid.

Fixpoint dep_ty_of_comparable_ty_eq {t} (ty : With_family.ty t) :
  Script_typed_ir.With_family.is_Comparable ty →
  With_family.to_ty (dep_ty_of_comparable_ty ty) =
    ty_of_comparable_ty (With_family.to_ty ty).
Proof.
  intro Hvalid; destruct ty eqn:?Ety; try reflexivity;
    simpl; try step; simpl in *; try destruct Hvalid;
    repeat rewrite <- dep_ty_of_comparable_ty_eq; trivial.
Qed.

The simulation [dep_unparse_comparable_ty_uncarbonated] is valid.

Fixpoint dep_unparse_comparable_ty_uncarbonated_eq
  {loc : Set} {t} (loc_value : loc) (ty : With_family.ty t) :
    Script_typed_ir.With_family.is_Comparable ty →
    dep_unparse_comparable_ty_uncarbonated loc_value ty =
    unparse_comparable_ty_uncarbonated loc_value (With_family.to_ty ty).
Proof.
  intro is_cmp; destruct ty; try reflexivity; simpl in *;
    try step; try destruct is_cmp;
  repeat rewrite dep_unparse_comparable_ty_uncarbonated_eq; trivial.
Qed.

The simulation [dep_unparse_ty_entrypoints_uncarbonated] is valid.

Fixpoint dep_unparse_ty_entrypoints_uncarbonated_eq {loc : Set} {t}
  (loc_value : loc) (ty : With_family.ty t) (epoints : Script_typed_ir.entrypoints_node) :
  Script_typed_ir.With_family.Valid.ty ty →
  dep_unparse_ty_entrypoints_uncarbonated loc_value ty epoints =
  unparse_ty_entrypoints_uncarbonated loc_value (With_family.to_ty ty) epoints.
Proof.
  intro;
    destruct ty eqn:?Ety; try reflexivity;
    simpl in *; step;
    repeat rewrite dep_unparse_ty_entrypoints_uncarbonated_eq; try reflexivity;
    repeat rewrite dep_unparse_comparable_ty_uncarbonated_eq; try reflexivity;
    Tactics.destruct_pairs; trivial.
Qed.

The simulation [dep_unparse_ty_uncarbonated] is valid.

Lemma dep_unparse_ty_uncarbonated_eq {loc : Set} {t}
  (loc_value : loc) (ty : With_family.ty t) :
  Script_typed_ir.With_family.Valid.ty ty →
  dep_unparse_ty_uncarbonated loc_value ty =
  unparse_ty_uncarbonated loc_value (With_family.to_ty ty).
Proof.
  intros; unfold dep_unparse_ty_uncarbonated, unparse_ty_uncarbonated;
  rewrite dep_unparse_ty_entrypoints_uncarbonated_eq; trivial.
Qed.

The simulation [dep_unparse_ty] is valid.

Lemma dep_unparse_ty_eq
  {A : Set} {t} (loc_value : A)
  (ctxt : Alpha_context.context)
  (ty : With_family.ty t) :
  Script_typed_ir.With_family.Valid.ty ty →
  dep_unparse_ty loc_value ctxt ty =
  unparse_ty loc_value ctxt (With_family.to_ty ty).
Proof.
  intro; unfold dep_unparse_ty, unparse_ty;
  destruct (Alpha_context.Gas.consume ctxt); simpl;
  try rewrite dep_unparse_ty_uncarbonated_eq; trivial.
Qed.

The simulation [dep_unparse_comparable_ty] is valid.

Lemma dep_unparse_comparable_ty_eq {A : Set} {t}
  (loc_value : A) (ctxt : Alpha_context.context)
  (ty : With_family.ty t) :
  Script_typed_ir.With_family.is_Comparable ty →
  dep_unparse_comparable_ty loc_value ctxt ty =
    unparse_comparable_ty loc_value ctxt (With_family.to_ty ty).
Proof.
  intros; unfold dep_unparse_comparable_ty, unparse_comparable_ty;
  rewrite dep_unparse_comparable_ty_uncarbonated_eq; trivial.
Qed.

The simulation [dep_unparse_parameter_ty] is valid.

Lemma dep_unparse_parameter_ty_eq {A : Set} {t}
  (loc_value : A) (ctxt : Alpha_context.context) (ty : With_family.ty t)
  (entrypoints : Script_typed_ir.entrypoints) :
  Script_typed_ir.With_family.Valid.ty ty →
  dep_unparse_parameter_ty loc_value ctxt ty entrypoints =
    unparse_parameter_ty loc_value ctxt (With_family.to_ty ty) entrypoints.
Proof.
  intro; unfold dep_unparse_parameter_ty, unparse_parameter_ty;
    rewrite dep_unparse_ty_entrypoints_uncarbonated_eq; trivial.
Qed.

The simulation [dep_serialize_ty_for_error] is valid.

Lemma dep_serialize_ty_for_error_eq {t} (ty : With_family.ty t) :
  Script_typed_ir.With_family.Valid.ty ty →
  dep_serialize_ty_for_error ty = serialize_ty_for_error (With_family.to_ty ty).
Proof.
  intro;
    unfold dep_serialize_ty_for_error;
    rewrite dep_unparse_ty_uncarbonated_eq; trivial.
Qed.

The simulation [dep_comparable_ty_of_ty] is valid.

Fixpoint dep_comparable_ty_of_ty_eq
  {t}
  (ctxt : Alpha_context.context)
  (loc : Alpha_context.Script.location)
  (ty: With_family.ty t) :
  Script_typed_ir.With_family.Valid.ty ty →
  (let ? '(comp_ty , ctxt ) := dep_comparable_ty_of_ty ctxt loc ty in
    return ? (With_family.to_ty comp_ty, ctxt)) =
      comparable_ty_of_ty ctxt loc (With_family.to_ty ty).
Proof.
  intros; destruct ty eqn:D_TY; simpl;
  destruct Alpha_context.Gas.consume eqn:A;
  simpl in *; try rewrite → dep_serialize_ty_for_error_eq; simpl; try easy;
  repeat (
    rewrite <- dep_comparable_ty_of_ty_eq by easy;
    destruct dep_comparable_ty_of_ty; simpl; [|reflexivity];
    Tactics.destruct_pairs; simpl; trivial
  ).
Qed.

The simulation [dep_unparse_stack_uncarbonated] is valid.

Fixpoint dep_unparse_stack_uncarbonated_eq {t}
  (st : With_family.stack_ty t) :
  Script_typed_ir.With_family.Valid.stack_ty st →
  dep_unparse_stack_uncarbonated st =
  unparse_stack_uncarbonated (With_family.to_stack_ty st).
Proof.
  intro; destruct st; simpl in *;
    try rewrite dep_unparse_stack_uncarbonated_eq,
    dep_unparse_ty_uncarbonated_eq;
    Tactics.destruct_pairs; trivial.
Qed.

The simulation [dep_serialize_stack_for_error] is valid.

Fixpoint dep_serialize_stack_for_error_eq {t}
  (ctxt : Alpha_context.context) (st : With_family.stack_ty t) :
  Script_typed_ir.With_family.Valid.stack_ty st →
  dep_serialize_stack_for_error ctxt st =
    serialize_stack_for_error ctxt (With_family.to_stack_ty st).
Proof.
  intro; destruct st; simpl in *;
  unfold dep_serialize_stack_for_error, serialize_stack_for_error;
  destruct (Alpha_context.Gas.level ctxt);
  try rewrite dep_unparse_stack_uncarbonated_eq; trivial.
Qed.

The simulation [dep_unparse_contract] is valid.

Lemma dep_unparse_contract_eq {A B a} loc_value ctxt mode
  (contract : With_family.typed_contract a) :
  dep_unparse_contract (A := A) (B := B) loc_value ctxt mode contract =
  unparse_contract loc_value ctxt mode (With_family.to_typed_contract contract).
Proof.
  unfold dep_unparse_contract, unparse_contract.
  now destruct contract.
Qed.

The simulation [dep_comparable_comb_witness2] is valid.

Lemma dep_comparable_comb_witness2_eq {t} (ty : With_family.ty t) :
  dep_comparable_comb_witness2 ty =
  comparable_comb_witness2 (With_family.to_ty ty).
Proof.
  destruct ty eqn:Ety; Tactics.destruct_pairs; simpl; try reflexivity.
  destruct t0_2; reflexivity.
Qed.

The simulation [dep_unparse_comparable_data] is valid.

Fixpoint dep_unparse_comparable_data_eq {a} {loc : Set}
  (l_value : loc) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (ty : With_family.ty a) (value : With_family.ty_to_dep_Set a) {struct ty} :
  Script_typed_ir.With_family.is_Comparable ty →
  dep_unparse_comparable_data l_value ctxt mode ty value =
    unparse_comparable_data l_value ctxt mode
      (With_family.to_ty ty) (With_family.to_value value).
Proof.
  intros; destruct ty; simpl;
  consume_gas; try rewrite cast_eval; try easy;
  step; try easy.
  { grep @With_family.Pair_t.
    rewrite (cast_exists_eval_2
      (T:= (fun pat : [Set ** Set] ⇒
        [pat.(Primitive.fst) × pat.(Primitive.snd) **
          Script_typed_ir.ty** Script_typed_ir.ty]))
      (E1:=Ty.to_Set t1)
      (E2:=Ty.to_Set t2)).
    unfold unparse_pair.
    destruct value.
    destruct H.
    do 2 (
      rewrite dep_unparse_comparable_data_eq by easy;
      destruct unparse_comparable_data; simpl; [|reflexivity];
      Tactics.destruct_pairs).
    now destruct mode;
      try (
        rewrite dep_comparable_comb_witness2_eq;
        destruct comparable_comb_witness2).
  }
  { grep @With_family.Union_t.
    rewrite (cast_exists_eval_2
      (T:= (fun pat : [Set ** Set] ⇒
        [Script_typed_ir.union pat.(Primitive.fst) pat.(Primitive.snd) **
        Script_typed_ir.ty** Script_typed_ir.ty]))
      (E1:=Ty.to_Set t1)
      (E2:=Ty.to_Set t2)).
      unfold unparse_union.
      destruct value, H;
      rewrite dep_unparse_comparable_data_eq by easy;
      reflexivity.
  }
  { grep @With_family.Option_t.
    rewrite (cast_exists_eval_1
      (T:= (fun __4 : Set ⇒ [M × __4 ** Script_typed_ir.ty]))
      (E1:=Ty.to_Set t)).
    unfold unparse_option.
    destruct value;
    try rewrite dep_unparse_comparable_data_eq by easy;
    reflexivity.
  }
Qed.

The simulation of [dep_pack_comparable_data] is valid.

Fixpoint dep_pack_comparable_data_eq {t}
  (ctxt : Alpha_context.context) (ty : With_family.ty t)
  (data : With_family.ty_to_dep_Set t)
  (mode : unparsing_mode) :
  Script_typed_ir.With_family.is_Comparable ty →
  dep_pack_comparable_data ctxt ty data mode =
    pack_comparable_data ctxt
      (With_family.to_ty ty) (With_family.to_value data) mode.
Proof.
  intros.
  unfold dep_pack_comparable_data, pack_comparable_data.
  now rewrite dep_unparse_comparable_data_eq.
Qed.

The simulation of [dep_hash_comparable_data] is valid.

Lemma dep_hash_comparable_data_eq {t}
  (ctxt : Alpha_context.context) (ty : With_family.ty t)
  (data : With_family.ty_to_dep_Set t) :
  Script_typed_ir.With_family.is_Comparable ty →
  dep_hash_comparable_data ctxt ty data =
    hash_comparable_data ctxt
      (With_family.to_ty ty) (With_family.to_value data).
Proof.
  intros;
  destruct ty eqn:TY;
  unfold dep_hash_comparable_data;
  unfold hash_comparable_data;
  rewrite dep_pack_comparable_data_eq; try easy.
Qed.

The simulation [dep_check_dupable_comparable_ty] is valid.

Fixpoint dep_check_dupable_comparable_ty_eq {t}
  (ty : With_family.ty t) :
  Script_typed_ir.With_family.is_Comparable ty →
  dep_check_dupable_comparable_ty ty =
    check_dupable_comparable_ty (With_family.to_ty ty).
Proof.
  induction ty eqn:D_TY; try reflexivity;
  try (intro H; simpl in H; destruct H).
Qed.

The simulation [dep_check_dupable_ty] is valid.

Lemma dep_check_dupable_ty_eq {t}
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (ty : With_family.ty t) :
  dep_check_dupable_ty ctxt loc_value ty =
    check_dupable_ty ctxt loc_value (With_family.to_ty ty).
Proof.
  unfold dep_check_dupable_ty, check_dupable_ty.
  repeat f_equal.
  induction ty; try reflexivity; simpl;
    f_equal;
    apply FunctionalExtensionality.functional_extensionality; intro;
    hauto lq: on.
Qed.

The simulation of [dep_type_metadata_eq] is valid.

Lemma dep_type_metadata_eq_eq {error_trace}
  (error_details : Script_tc_errors.dep_error_details error_trace)
  (meta1 meta2 : Script_typed_ir.ty_metadata) :
  dep_type_metadata_eq error_details meta1 meta2 =
    type_metadata_eq (Script_tc_errors.to_error_details error_details)
      meta1 meta2.
Proof.
  destruct meta1, meta2.
  unfold dep_type_metadata_eq, type_metadata_eq.
  apply Script_typed_ir.Type_size.dep_check_eq_eq.
Qed.

The simulation [dep_default_ty_eq_error] is valid.

Lemma dep_default_ty_eq_error_eq {t1 t2}
  (ty1 : With_family.ty t1) (ty2 : With_family.ty t2) :
  dep_default_ty_eq_error ty1 ty2 =
    default_ty_eq_error (With_family.to_ty ty1) (With_family.to_ty ty2).
Proof.
  reflexivity.
Qed.

Conversion back to [eq] of OCaml.

Definition to_eq {Family : Set} {a b : Family} (_ : a = b) : eq := Eq.

The simulation [dep_comparable_ty_eq] is valid.

Fixpoint dep_comparable_ty_eq_eq {error_trace} {a b}
  (error_details : Script_tc_errors.dep_error_details error_trace)
  (ta : With_family.ty a) (tb : With_family.ty b) :
  Script_typed_ir.With_family.is_Comparable ta →
  Script_typed_ir.With_family.is_Comparable tb →
  Gas_monad.map to_eq (dep_comparable_ty_eq error_details ta tb) =
    comparable_ty_eq (Script_tc_errors.to_error_details error_details)
      (With_family.to_ty ta) (With_family.to_ty tb).
Proof.
  Opaque
    dep_ty_of_comparable_ty
    ty_of_comparable_ty
    Script_tc_errors.Error_trace_family.to_Set
    Script_tc_errors.to_error_details.
  intros H_ta H_tb.
  apply FunctionalExtensionality.functional_extensionality; intro gas.
  destruct ta, tb; simpl; simpl in H_ta, H_tb;
    try contradiction;
    unfold Gas_monad.map, Gas_monad.Syntax.op_letstar, Gas_monad.bind;
    (destruct Gas_monad.consume_gas; simpl; [|reflexivity]);
    Tactics.destruct_pairs;
    destruct_all
      (result unit (Script_tc_errors.Error_trace_family.to_Set error_trace));
    simpl;
    try reflexivity;
    repeat f_equal;
    destruct error_details;
    simpl;
    try (rewrite cast_eval; try reflexivity; repeat f_equal);
    try rewrite dep_default_ty_eq_error_eq;
    repeat rewrite dep_ty_of_comparable_ty_eq by assumption;
    try reflexivity;
    destruct_all Dependent_bool.dbool;
    destruct_all Dependent_bool.dand;
    simpl;
    try reflexivity.
  all:
    rewrite dep_type_metadata_eq_eq; simpl;
    destruct type_metadata_eq; simpl; [|reflexivity].
  all: repeat (
    rewrite <- dep_comparable_ty_eq_eq by easy;
    unfold Gas_monad.Syntax.op_letplus, Gas_monad.map;
    destruct dep_comparable_ty_eq; simpl; [|reflexivity];
    Tactics.destruct_pairs;
    destruct r; simpl; [|reflexivity]
  ).
  all: hauto lq: on.
  Transparent
    dep_ty_of_comparable_ty
    ty_of_comparable_ty
    Script_tc_errors.Error_trace_family.to_Set
    Script_tc_errors.to_error_details.
Qed.

Solve the simplest cases (without recursivity) for [dep_ty_eq_eq].

Ltac simple_dep_ty_eq_eq_case error_details :=
  unfold dep_ty_eq, ty_eq;
    simpl;
    rewrite dep_default_ty_eq_error_eq; simpl;
    unfold Gas_monad.map;
    apply FunctionalExtensionality.functional_extensionality_dep; intro gas;
    unfold Gas_monad.record_trace_eval;
    destruct error_details; simpl;
    rewrite !cast_eval;
    unfold Gas_monad.Syntax.op_letstar, Gas_monad.bind;
    (destruct Gas_monad.consume_gas; simpl; [|reflexivity]);
    Tactics.destruct_pairs;
    match goal with
    | r : result unit _ |- _ ⇒ destruct r; reflexivity
    end.

The simulation [dep_ty_eq] is valid.

Lemma dep_ty_eq_eq {error_trace a b}
  (error_details : Script_tc_errors.dep_error_details error_trace)
  (loc_value : Alpha_context.Script.location)
  (ty1 : With_family.ty a) (ty2 : With_family.ty b) :
  Gas_monad.map to_eq (dep_ty_eq error_details loc_value ty1 ty2) =
  ty_eq
    (Script_tc_errors.to_error_details error_details) loc_value
    (With_family.to_ty ty1) (With_family.to_ty ty2).
Proof.
  Opaque
    default_ty_eq_error
    dep_default_ty_eq_error
    Script_tc_errors.Error_trace_family.to_Set.
  destruct ty1, ty2.
  { simple_dep_ty_eq_eq_case error_details. }
  (* When applying the [simple_dep_ty_eq_eq_case] to all the goals, it gets
     really slow on recursive ones, in addition to the fact that there are more
     than a thousand of cases. We need to find another way, for example by
     moving the definitions inside [ty_eq] at top-level. *)
  Transparent
    default_ty_eq_error
    dep_default_ty_eq_error
    Script_tc_errors.Error_trace_family.to_Set.
Admitted.

Function `stack_eq` checks two variables, typed `Script_typed_ir.stack_ty` for equality. We created simulation function `dep_stack_eq`, and we prove it's backward compatibility with original `stack_eq` function.

Fixpoint dep_stack_eq_eq {t k}
  (loc_value : Alpha_context.Script.location) (ctxt : Alpha_context.context)
  (lvl : int) (stack1 : With_family.stack_ty t)
  (stack2 : With_family.stack_ty k) :
  (let ? '(e , ctxt ) := dep_stack_eq loc_value ctxt lvl stack1 stack2 in
   return ? (to_eq e, ctxt)) =
    stack_eq loc_value ctxt lvl (With_family.to_stack_ty stack1)
      (With_family.to_stack_ty stack2).
Proof.
  destruct stack1; simpl; destruct stack2; simpl; [|reflexivity..].
  Opaque stack_eq.
  change Script_tc_errors.Informative
    with (Script_tc_errors.to_error_details Script_tc_errors.Dep_informative).
  change (trace _error)
    with (Script_tc_errors.Error_trace_family.to_Set
            Script_tc_errors.Error_trace_family.Error_trace).
  rewrite <- dep_ty_eq_eq.
  rewrite Gas_monad.run_map.
  destruct Gas_monad.run; simpl; [|reflexivity].
  Tactics.destruct_pairs; simpl.
  repeat (step; [|reflexivity]; Tactics.destruct_pairs; simpl).
  rewrite <- dep_stack_eq_eq.
  repeat (step; simpl; try reflexivity).
  Transparent stack_eq.
Qed.

Equality between [dep_judgement] and [judgement].

Module Eq_judgement.
  Definition t {s} (dep_x : dep_judgement s) (x : judgement) : Prop :=
    match dep_x, x with
    | Dep_typed dep_x, Typed x ⇒ Eq_descr.t dep_x x
    | Dep_failed dep_f, Failed {| judgement.Failed.descr := f |} ⇒
        ∀ {u} (s : With_family.stack_ty u),
        Eq_descr.t (dep_f _ s) (f (With_family.to_stack_ty s))
    | _, _ ⇒ False
    end.
End Eq_judgement.

Equality between [dep_branch] and [branch].

Module Eq_branch.
  Definition t {s u v} (dep_x : dep_branch s u v) (x : branch) : Prop :=
    ∀ {f}
      (dep_x1 : dep_descr s f) (x1 : descr)
      (dep_x2 : dep_descr u f) (x2 : descr),
    Eq_descr.t dep_x1 x1 →
    Eq_descr.t dep_x2 x2 →
    Eq_descr.t
      (dep_x.(dep_branch.branch) dep_x1 dep_x2) (x.(branch.branch) x1 x2).
End Eq_branch.

The simulation [dep_merge_branches] is valid.

Lemma dep_merge_branches_eq {s u v : Stack_ty.t}
  (ctxt : Alpha_context.context)
  (loc : Alpha_context.Script.location)
  (dep_btr : dep_judgement s) (btr : judgement)
  (dep_bfr : dep_judgement u) (bfr : judgement)
  (dep_branch : dep_branch s u v) (branch : branch) :
  Eq_judgement.t dep_btr btr →
  Eq_judgement.t dep_bfr bfr →
  Eq_branch.t dep_branch branch →
  match
    dep_merge_branches ctxt loc dep_btr dep_bfr dep_branch,
    merge_branches ctxt loc btr bfr branch
  with
  | Pervasives.Ok (dep_result, dep_ctxt), Pervasives.Ok (result, ctxt) ⇒
    Eq_judgement.t dep_result result ∧ dep_ctxt = ctxt
  | Pervasives.Error dep_error, Pervasives.Error error ⇒ dep_error = error
  | _, _ ⇒ False
  end.
Proof.
  intros EJt EJf EDB.
  unfold dep_merge_branches, merge_branches.
  destruct dep_btr, btr; simpl in EJt; try contradiction;
  destruct dep_bfr, bfr; simpl in EJf; try contradiction;
  Tactics.destruct_all descr;
  repeat match goal with
  | H : dep_descr _ _ |- _ ⇒ destruct H
  | H : Eq_descr.t _ _ |- _ ⇒ destruct H
  end; destruct dep_branch, branch; simpl in *;
  [
    rewrite <- aft4, <- aft3, <- dep_stack_eq_eq;
    destruct dep_stack_eq;
      [|rewrite <- !dep_serialize_stack_for_error_eq; scongruence];
    Tactics.destruct_pairs; destruct e
  |..].
  all : split; intros; [apply EDB |]; hauto l: on.
Qed.

Lemma kind_equal_eq : ∀ (a b : Script_tc_errors.kind),
    kind_equal a b = true → a = b.
Proof. now intros [] []. Qed.

Lemma kind_equal_refl : ∀ x, kind_equal x x = true.
Proof. now intros []. Qed.

ty and comparable_ty are the same type. We express and prove properties of the type

Lemma ty_of_comparable_ty_eq {t} (ty : With_family.ty t) :
  Script_typed_ir.With_family.is_Comparable ty →
  ty_of_comparable_ty (With_family.to_ty ty) = With_family.to_ty ty.
Proof.
  intros.
  induction ty eqn:D_TY; simpl; try reflexivity;
    try destruct d eqn:DD; simpl in H; try destruct H.
  (* Pairs *)
  apply IHt0_1 with (ty:=t0_1) in H.
  apply IHt0_2 with (ty:=t0_2) in H0.
  rewrite H. rewrite H0. all : (repeat reflexivity).
  (* Union *)
  apply IHt0_1 with (ty:=t0_1) in H.
  apply IHt0_2 with (ty:=t0_2) in H0.
  rewrite H. rewrite H0. all : (repeat reflexivity).
  (* Option *)
  apply IHt0 with (ty:=t0) in H. rewrite H. all : (repeat reflexivity).
Qed.

Show that the two functions comparable_ty_of_ty and ty_of_comparable_ty are compatible. We create 2 reciprocal Fixpoints and prove them.

Fixpoint ty_of_comparable_ty_comparable_ty_of_ty {t}
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (ty : With_family.ty t) {struct ty}:
  Script_typed_ir.With_family.is_Comparable ty →
  match (comparable_ty_of_ty ctxt loc_value (With_family.to_ty ty)) with
  | Pervasives.Ok (comp_ty, alpha) ⇒
      ty_of_comparable_ty comp_ty = With_family.to_ty ty
  | Pervasives.Error _ ⇒ True
  end.
Proof.
  intro V; destruct ty eqn:T; simpl;
    destruct
      (Alpha_context.Gas.consume ctxt
        Typecheck_costs.comparable_ty_of_ty_cycle) eqn:G;
    simpl; try (reflexivity); try apply I; simpl in V; try destruct d eqn:DD;
    try destruct V.
  (* Pairs *)
  pose proof (ty_of_comparable_ty_comparable_ty_of_ty _ t0 loc_value t0_1 H).
  destruct comparable_ty_of_ty eqn:D1; simpl. destruct p.
  pose proof (ty_of_comparable_ty_comparable_ty_of_ty _ c0 loc_value t0_2 H0).
  destruct (comparable_ty_of_ty c0 loc_value) eqn:D2; simpl. destruct p. simpl.
  rewrite H1. rewrite H2. all : repeat trivial.
  (* Union *)
  pose proof (ty_of_comparable_ty_comparable_ty_of_ty _ t0 loc_value t0_1 H).
  destruct comparable_ty_of_ty eqn:D1; simpl. destruct p.
  pose proof (ty_of_comparable_ty_comparable_ty_of_ty _ c0 loc_value t0_2 H0).
  destruct (comparable_ty_of_ty c0 loc_value) eqn:D2; simpl. destruct p. simpl.
  rewrite H1. rewrite H2. all : repeat trivial.
  (* Option *)
  pose proof (ty_of_comparable_ty_comparable_ty_of_ty _ t2 loc_value t0 V).
  destruct comparable_ty_of_ty eqn:D1; simpl. destruct p.
  simpl. rewrite H. reflexivity. trivial.
Qed.

Fixpoint comparable_ty_of_ty_ty_of_comparable_ty {t}
         (ctxt ctxt1: Alpha_context.context)
         (loc_value : Alpha_context.Script.location)
         (comp_ty: With_family.ty t) (comp_ty1 : Script_typed_ir.ty):
  Script_typed_ir.With_family.is_Comparable comp_ty → comparable_ty_of_ty ctxt
   loc_value (ty_of_comparable_ty (With_family.to_ty comp_ty)) =
   Pervasives.Ok (comp_ty1, ctxt1) →
  (With_family.to_ty comp_ty) = comp_ty1.
Proof.
  intros Y H.
  destruct comp_ty eqn:G; simpl in H;
    destruct (Alpha_context.Gas.consume ctxt
              Typecheck_costs.comparable_ty_of_ty_cycle) eqn:G';
    simpl in H; (try injection H as H); trivial; simpl in H; try discriminate H.
  (* Pairs *)
  all : repeat (
            simpl in Y; try inversion Y; destruct d; try destruct Y;
            simpl in H; rewrite G' in H; simpl in H; try discriminate H).
  destruct (comparable_ty_of_ty t0 loc_value
           (ty_of_comparable_ty (With_family.to_ty t0_1))) eqn:P; simpl in *;
    try inversion H.
  simpl in H. destruct p.
  destruct (comparable_ty_of_ty c0 loc_value
           (ty_of_comparable_ty (With_family.to_ty t0_2))) eqn:P1; simpl in *;
    try inversion H.
  simpl in H. destruct p. simpl.
  apply (comparable_ty_of_ty_ty_of_comparable_ty _
           t0 c0 loc_value t0_1 c H0) in P.
  apply (comparable_ty_of_ty_ty_of_comparable_ty _
           c0 c2 loc_value t0_2 c1 H1) in P1.
  rewrite P. rewrite P1. injection H as H. trivial.
  (* Union_t *)
  destruct (comparable_ty_of_ty t0 loc_value
           (ty_of_comparable_ty (With_family.to_ty t0_1))) eqn:P; simpl in *;
    try inversion H.
  simpl in H. destruct p.
  destruct (comparable_ty_of_ty c0 loc_value
           (ty_of_comparable_ty (With_family.to_ty t0_2))) eqn:P1; simpl in *;
    try inversion H.
  simpl in H. destruct p. simpl.
  apply (comparable_ty_of_ty_ty_of_comparable_ty _
          t0 c0 loc_value t0_1 c H0) in P.
  apply (comparable_ty_of_ty_ty_of_comparable_ty _
           c0 c2 loc_value t0_2 c1 H1) in P1.
  rewrite P. rewrite P1. injection H as H. trivial.
  (* Option *)
  destruct (comparable_ty_of_ty t2 loc_value
           (ty_of_comparable_ty (With_family.to_ty t0))) eqn:P; simpl in H;
    try inversion H.
  destruct p. injection H as H.
  apply comparable_ty_of_ty_ty_of_comparable_ty in P; try trivial.
  subst; reflexivity.
Qed.

Validity predicate. This predicate states that given [comparable_ty] has correct metadata.

(*
Module Valid.
  Fixpoint t (cty : Script_typed_ir.comparable_ty) : Prop :=
    match cty with
    | Script_typed_ir.Unit_key
    | Script_typed_ir.Never_key
    | Script_typed_ir.Int_key
    | Script_typed_ir.Nat_key
    | Script_typed_ir.Signature_key
    | Script_typed_ir.String_key
    | Script_typed_ir.Bytes_key
    | Script_typed_ir.Mutez_key
    | Script_typed_ir.Bool_key
    | Script_typed_ir.Key_hash_key
    | Script_typed_ir.Key_key
    | Script_typed_ir.Timestamp_key
    | Script_typed_ir.Chain_id_key
    | Script_typed_ir.Address_key
    | Script_typed_ir.Tx_rollup_l2_address_key => True
      (* x = {| Script_typed_ir.ty_metadata.size := *)
      (*          Script_typed_ir.Type_size.(Script_typed_ir.TYPE_SIZE.one) |} *)
    | Script_typed_ir.Pair_key cty1 cty2 x
    | Script_typed_ir.Union_key cty1 cty2 x =>
      let sz := (1 +i Script_typed_ir.comparable_ty_size cty1 +i
                          Script_typed_ir.comparable_ty_size cty2) in
      x = {| Script_typed_ir.ty_metadata.size := sz |} /\
      sz <= Alpha_context.Constants.michelson_maximum_type_size /\
      t cty1 /\ t cty2
    | Script_typed_ir.Option_key cty1 x =>
      let sz := (1 +i Script_typed_ir.comparable_ty_size cty1) in
      x = {| Script_typed_ir.ty_metadata.size := sz |} /\
      sz <= Alpha_context.Constants.michelson_maximum_type_size /\
      t cty1
    end.
End Valid.

Lemma extract_annot_eq node : forall node1 x,
  Script_ir_annot.extract_field_annot node = Pervasives.Ok (node1, x) ->
  node = node1.
Proof.
  (** It is possible that this Lemma is not correct
     but this is issue with annotation (annotations
     should be changed soon), so just admitting.
  *)
Admitted.
*)

We prove that [parse (unparse comparable_ty) = comparable_ty] (skipping annotations). Here we prove this statement for auxillary functions. We require metadata of given comparable_ty to be correct in sense described above ([Valid.t] predicate). The most part of proof is by case analysis. So, we unfold definitions, check every possible case for comparable_ty, and show needed equaliy. Recursive cases are proved by recursive calls. We do not check error cases, go through success case only.

Fixpoint parse_comparable_ty_aux_unparse_comparable_ty_uncarbonated loc ty ctxt stack_depth : Valid.t ty -> let node := unparse_comparable_ty_uncarbonated loc ty in match parse_comparable_ty_aux stack_depth ctxt node with | Pervasives.Ok (Ex_comparable_ty ty', _) => ty = ty' | Pervasives.Error _ => True end. Proof. intro H; destruct ty eqn:Ety; try match goal with | |- context[Script_typed_ir.Pair_key] => (* We admit the [Pair_key] case for now as there should be changes to the
         annotations. *)
apply axiom end; simpl; destruct Alpha_context.Gas.consume; simpl; trivial; destruct (_ >i _); simpl; trivial; destruct Script_ir_annot.check_type_annot; simpl; trivial; try (rewrite H; reflexivity); simpl in *; [destruct H as [?H1 [?H2 [?H3 ?H4]]] | destruct H as [?H1 [?H2 ?H3]]]. { (* let node2 := fresh "node2" in *)
(* let node1 := fresh "node1" in *)
(* let En1 := fresh "En1" in *)
(* let En2 := fresh "En2" in *)
(* let Hc1 := fresh "Hc1" in *)
(* let Hc2 := fresh "Hc2" in *)
(* let Hvc1 := fresh "Hvc1" in *)
(* let Hvc2 := fresh "Hvc2" in *)
(* let fc1 := fresh "c1" in *)
(* let fc2 := fresh "c2" in *)
(* let floc := fresh "loc" in *)
(* let Epcaux2 := fresh "Epcaux2" in *)
(* let Epcaux1 := fresh "Epcaux1" in *)
(* let fEloc := fresh "Eloc" in *)
(* match goal with *)
(* | H : Alpha_context.Script.location |- _ => *)
(*   remember H as floc; *)
(*   subst H *)
(* end; *)
(* match goal with *)
(* | H : Valid.t ?c |- context [ Script_typed_ir.Union_key ?c _ _ = _ ] => *)
(*   remember (unparse_comparable_ty_uncarbonated _ c) as node1; *)
(*   remember H as Hvc1; *)
(*   remember c as fc1; *)
(*   subst c; *)
(*   subst H *)
(* end; *)
(* match goal with *)
(* | H : Valid.t ?c |- context [ Script_typed_ir.Union_key _ ?c _ = _ ] => *)
(*   remember (unparse_comparable_ty_uncarbonated _ c) as node2; *)
(*   remember H as Hvc2; *)
(*   remember c as fc2; *)
(*   subst c; *)
(*   subst H *)
(* end; *)
(* destruct (Script_ir_annot.extract_field_annot node1) eqn:En1; *)
(*   [|simpl;trivial]; *)
(* destruct (Script_ir_annot.extract_field_annot node2) eqn:En2; *)
(*   [|destruct p;simpl;trivial]; *)
(* Tactics.destruct_pairs; *)
(* apply extract_annot_eq in En1, En2; simpl; rewrite <- En1, <- En2; *)
(* clear En1 En2; *)
(* match goal with *)
(* | |- context [ parse_comparable_ty_aux ?sd ?ctx node2 ] => *)
(*   specialize ( *)
(*     parse_comparable_ty_aux_unparse_comparable_ty_uncarbonated *)
(*       floc _ ctx sd Hvc2) as Hc2 *)
(* end; *)
(* match goal with *)
(* | H : node2 = unparse_comparable_ty_uncarbonated _ _ |- _ => rewrite <- H in Hc2 *)
(* end; *)
(* destruct (parse_comparable_ty_aux _ _ node2) eqn:Epcaux2; *)
(* simpl; [|trivial]; Tactics.destruct_pairs; *)
(* match goal with *)
(* | H : match ?e with _ => _ end |- _ => destruct e *)
(* end; *)
(* match goal with *)
(* | |- context [ parse_comparable_ty_aux ?sd ?ctx node1 ] => *)
(*   specialize ( *)
(*     parse_comparable_ty_aux_unparse_comparable_ty_uncarbonated *)
(*       floc _ ctx sd Hvc1) as Hc1 *)
(* end; *)
(* match goal with *)
(* | H : node1 = unparse_comparable_ty_uncarbonated _ _ |- _ => rewrite <- H in Hc1 *)
(* end; *)
(* destruct (parse_comparable_ty_aux _ _ node1) eqn:Epcaux1; *)
(*   [|simpl;trivial]; Tactics.destruct_pairs; *)
(* match goal with *)
(* | H : match ?e with _ => _ end |- _ => destruct e *)
(* end; *)
(* subst; *)
(* repeat (unfold Script_typed_ir.union_key, *)
(*           Script_typed_ir.Type_size.compound2; simpl); *)
(* destruct(Script_typed_ir.Type_size.of_int floc _) eqn:fEloc; *)
(* simpl; [|trivial]; *)
(* unfold Script_typed_ir.Type_size.of_int in fEloc; simpl in *; *)
(*   sauto. *)
apply axiom. (* destruct (_ <=? _) eqn:E; [|lia]; *)
(*   injection fEloc as fEloc; rewrite <- fEloc. *) } { match goal with | H : Valid.t ?ty |- context [ parse_comparable_ty_aux ?stack_depth ?ctxt (unparse_comparable_ty_uncarbonated ?loc ?ty) ] => let H_eq := fresh "H_eq" in pose proof ( parse_comparable_ty_aux_unparse_comparable_ty_uncarbonated loc ty ctxt stack_depth H ) as H_eq; destruct parse_comparable_ty_aux; simpl; trivial; Tactics.destruct_pairs; destruct_all ex_comparable_ty; rewrite <- H_eq; clear H_eq end. repeat (unfold Script_typed_ir.option_key, Script_typed_ir.Type_size.compound1; simpl); destruct Script_typed_ir.Type_size.of_int eqn:?; simpl; trivial; unfold Script_typed_ir.Type_size.of_int in *; simpl in *; destruct (_ <=i _) eqn:E; simpl in *. now repeat match goal with | H : return? _ = _ |- _ => injection H as H; rewrite <- H | H : ?t = _ |- context [ Script_typed_ir.Option_key _ ?t ] => rewrite H end. sauto. } Qed.

(** We prove that [parse (unparse comparable_ty) = comparable_ty]
    (skipping annotations).
    We require metadata of given [comparable_ty] to be correct in sense
    described above ([Valid.t] predicate).
    For proof here we unfold definitions and perform case analysis for some
    simple cases until we are able to use lemma for auxillary functions
    which is proved above.
    We do not check error cases, go through success case only.
    Since we do both directions ([parse (unparse t)] and
    [unparse (parse t)]), we can be sure either both functions work right
    or they both have errors on the same cases with same results
    (kind of symmetric saying a bit more accurate..), so, these are
    most likely specification errors and we will likely just repeat them
    while building the error checking from function implementations.
*)

Lemma parse_unparse_comparable_ty : forall cty loc ctxt, Valid.t cty -> match unparse_comparable_ty loc ctxt cty with | Pervasives.Ok (node', ctxt') => match parse_comparable_ty ctxt' node' with | Pervasives.Ok (Ex_comparable_ty cty'', ctxt'') => cty = cty'' | Pervasives.Error _ => True end | Pervasives.Error _ => True end. Proof. intros cty loc ctxt H; unfold parse_comparable_ty, unparse_comparable_ty. destruct Alpha_context.Gas.consume eqn:Egc; simpl; [|trivial]. apply parse_comparable_ty_aux_unparse_comparable_ty_uncarbonated; trivial. Qed.

Module Node. Module Valid. Fixpoint t (node : Alpha_context.Script.node) (loc : Alpha_context.Script.location) : Prop := match node with | Prim l Michelson_v1_primitives.T_option [n] annot => l = loc /\ t n loc | Prim l Michelson_v1_primitives.T_or [n;n0] annot => l = loc /\ t n loc /\ t n0 loc | Prim l Michelson_v1_primitives.T_pair [n;n0] annot => l = loc /\ t n loc /\ t n0 loc | Prim l _ _ _ => l = loc | _ => True end. End Valid. End Node.

Fixpoint unparse_comparable_ty_uncarbonated_parse_comparable_ty_aux node ctxt stack_depth loc {struct node} : Node.Valid.t node loc -> match parse_comparable_ty_aux stack_depth ctxt node with | Pervasives.Ok (Ex_comparable_ty comp_ty, _) => let node' := unparse_comparable_ty_uncarbonated loc comp_ty in Alpha_context.Script.strip_annotations node' = Alpha_context.Script.strip_annotations node | Pervasives.Error _ => True end. Proof. destruct node eqn:E; intro H; simpl in *; destruct Alpha_context.Gas.consume; simpl; destruct (stack_depth >i 10000); simpl; trivial. destruct p eqn:P; simpl; trivial; repeat match goal with | |- match (match ?l0 with _ => _ end) with _ => _ end => destruct l0 eqn:?El0; simpl; trivial | |- match (let? ' _ := ?sc_ir_ann in _) with _ => _ end => destruct sc_ir_ann eqn:E'; simpl; subst; trivial end. (* Options *)
{ pose proof (unparse_comparable_ty_uncarbonated_parse_comparable_ty_aux n t (stack_depth +i 1) loc) as IH. destruct H as [H' H'']; apply IH in H''; clear IH. destruct (parse_comparable_ty_aux (stack_depth +i 1) t n) eqn:D. Tactics.destruct_pairs. destruct e; simpl; unfold Script_typed_ir.option_key; simpl; unfold Script_typed_ir.Type_size.compound1; destruct Script_typed_ir.Type_size.of_int eqn:?; simpl; [| trivial]. subst. rewrite H''. reflexivity. simpl. trivial. } (* Unions - admit due to annotations *)
{ admit. } (* Pairs - problem with annotations *)
{ admit. } Admitted.

(** Opposite lemma. We prove that [unparse (parse comparable_ty) = comparable_ty].
Unions and pairs cases in auxillary fixpoint admitted due to annotations
*)
Lemma unparse_parse_comparable_ty : forall node loc ctxt, Node.Valid.t node loc -> match parse_comparable_ty ctxt node with | Pervasives.Ok (Ex_comparable_ty comp_ty, ctxt') => match unparse_comparable_ty loc ctxt' comp_ty with | Pervasives.Ok (node', ctxt'') => Alpha_context.Script.strip_annotations node' = Alpha_context.Script.strip_annotations node | Pervasives.Error _ => True end | Pervasives.Error _ => True end. Proof. intros node loc ctxt. unfold parse_comparable_ty. unfold unparse_comparable_ty. specialize (unparse_comparable_ty_uncarbonated_parse_comparable_ty_aux node ctxt 0 loc) as Epu. destruct (parse_comparable_ty_aux 0 ctxt node) eqn:G; [| trivial]. Tactics.destruct_pairs; destruct e eqn:E. destruct (Alpha_context.Gas.consume c (Unparse_costs.unparse_comparable_type c0)) eqn:C; simpl; [|simpl; trivial]. intro H; apply Epu in H; trivial. Qed.

We prove that parse_comparable_ty_aux and dep_parse_comparable_ty_aux_eq are equivalent

Definition z_number_10000 : Z.t := 10000.
Opaque z_number_10000.

Global Hint Unfold z_number_10001 : tezos_z.

Ltac tr_lia :=
with_strategy transparent [z_number_10001] lia.

The auxiliary simulation [dep_parse_comparable_ty_aux_fuel] is valid.

Fixpoint dep_parse_comparable_ty_aux_fuel_eq
  (fuel : nat) (ctxt : Alpha_context.context)
  (node_value : Alpha_context.Script.node) {struct fuel} :
  Z.of_nat fuel ≤ z_number_10001 →
  (let ? '(res , ctxt ) := dep_parse_comparable_ty_aux_fuel fuel ctxt node_value in
  return ? (to_ex_comparable_ty res, ctxt)) =
  parse_comparable_ty_aux (fuel_to_stack_depth fuel) ctxt node_value.
Proof.
  intros H_fuel_valid; unfold fuel_to_stack_depth.
  destruct fuel as [|fuel]; simpl.
  { replace (z_number_10001 - 0) with z_number_10001 by lia.
    destruct node_value; simpl.
    all: now destruct Alpha_context.Gas.consume.
  }
  { destruct node_value; simpl; try reflexivity.
    (* We set this function as opaque to prevent future reductions. *)
    Opaque parse_comparable_ty_aux.
    all: destruct Alpha_context.Gas.consume; simpl; [|reflexivity].
    all:
      replace (Z.pos (Pos.of_succ_nat fuel)) with (Z.of_nat (Datatypes.S fuel))
        by lia.
    all: rewrite Z.gtb_ltb.
    all: set (z_fuel := Z.of_nat (Datatypes.S fuel)) in ×.
    all: replace (_ <? _) with false by tr_lia; try reflexivity.
    destruct_all Michelson_v1_primitives.prim; simpl; try reflexivity.
    all:
      repeat match goal with
      | |- context[match ?l with _ ⇒ _ end] ⇒
        destruct l; simpl; try reflexivity
      end.
    all:
      destruct (Script_ir_annot.check_type_annot _ _); simpl; try reflexivity.
    all: repeat (
      destruct (Script_ir_annot.remove_field_annot _); simpl; [|reflexivity]
    ).
    all: repeat (
      replace (z_number_10001 - z_fuel +i 1)
        with (z_number_10001 - Z.of_nat fuel) by tr_lia;
      rewrite <- (dep_parse_comparable_ty_aux_fuel_eq fuel) by lia;
      step; simpl; [|reflexivity];
      Tactics.destruct_pairs; destruct_all dep_ex_comparable_ty; simpl
    ).
    all:
      unfold Script_typed_ir.option_key,
        Script_typed_ir.union_key,
          Script_typed_ir.pair_key; simpl;
      step; reflexivity.
    (* We set this function back to transparent. *)
    Transparent parse_comparable_ty_aux.
  }
Qed.

[stack_depth_to_fuel] and [fuel_to_stack_depth] are inverses.

Lemma stack_depth_to_fuel_to_stack_depth stack_depth :
  0 ≤ stack_depth ≤ z_number_10001 →
  fuel_to_stack_depth (stack_depth_to_fuel stack_depth) =
  stack_depth.
Proof.
  unfold fuel_to_stack_depth, stack_depth_to_fuel.
  lia.
Qed.

[fuel_to_stack_depth] and [stack_depth_to_fuel] are inverses.

Lemma fuel_to_stack_depth_to_fuel fuel :
  0 ≤ Z.of_nat fuel ≤ z_number_10001 →
  stack_depth_to_fuel (fuel_to_stack_depth fuel) =
  fuel.
Proof.
  unfold fuel_to_stack_depth, stack_depth_to_fuel.
  lia.
Qed.

The simulation [dep_parse_comparable_ty_aux] is valid.

Lemma dep_parse_comparable_ty_aux_eq
  (stack_depth : int) (ctxt : Alpha_context.context)
  (node_value : Alpha_context.Script.node) :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(res , ctxt ) :=
    dep_parse_comparable_ty_aux stack_depth ctxt node_value in
  return ? (to_ex_comparable_ty res, ctxt)) =
  parse_comparable_ty_aux stack_depth ctxt node_value.
Proof.
  intros.
  unfold dep_parse_comparable_ty_aux, stack_depth_to_fuel.
  rewrite dep_parse_comparable_ty_aux_fuel_eq; f_equal;
    unfold fuel_to_stack_depth; lia.
Qed.

The auxiliary simulation [dep_parse_ty_aux_fuel] is valid.

Fixpoint dep_parse_ty_aux_fuel_eq
  (ctxt : Alpha_context.context) (fuel : nat) (legacy : bool)
  (allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
  (allow_ticket : bool) (ret_value : Parse_ty_ret_family.t)
  (node_value : Alpha_context.Script.node) {struct fuel} :
  Z.of_nat fuel ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_ty_aux_fuel
      ctxt fuel legacy
      allow_lazy_storage allow_operation allow_contract
      allow_ticket ret_value node_value in
  return ? (Parse_ty_ret_family.to_ret ret_value result, ctxt)) =
  parse_ty_aux
    ctxt (fuel_to_stack_depth fuel) legacy
    allow_lazy_storage
    allow_operation allow_contract allow_ticket
    (Parse_ty_ret_family.to_parse_ty_ret ret_value) node_value

with dep_parse_big_map_ty_fuel_eq ctxt fuel legacy big_map_loc args map_annot
  {struct fuel} :
  Z.of_nat fuel ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_big_map_ty_fuel ctxt fuel legacy big_map_loc args map_annot in
  return ? (to_ex_ty result, ctxt)) =
  parse_big_map_ty ctxt (fuel_to_stack_depth fuel)
    legacy big_map_loc args map_annot.
Proof.
{
  intros H_fuel_valid.
  destruct fuel; simpl; unfold fuel_to_stack_depth.
  { replace (z_number_10001 - 0) with z_number_10001 by lia.
    destruct node_value; simpl.
    all: destruct Alpha_context.Gas.consume; simpl; [|reflexivity].
    all: replace (z_number_10001 >i 10000) with true by lia; reflexivity.
  }
  { destruct node_value eqn:H_node_value_eq; simpl.
    (* We set this function as opaque to prevent future reductions. *)
    Opaque parse_ty_aux.
    all: destruct Alpha_context.Gas.consume; simpl; [|reflexivity].
    all:
      replace (z_number_10001 - Z.pos (Pos.of_succ_nat fuel) >i 10000)
        with false
        by (
          rewrite Z.gtb_ltb;
          symmetry; rewrite Z.ltb_ge;
          tr_lia
        );
        try reflexivity.
    (* For now we handle only one case of the [ret_value]. *)
    (* TODO: handle the other case. *)
    all: destruct ret_value; simpl; [|apply axiom].
    all: destruct_all Michelson_v1_primitives.prim; try reflexivity.
    all:
      repeat match goal with
      | |- context[match ?l with _ ⇒ _ end] ⇒
        destruct l; simpl; try reflexivity
      end.
    all: try (
      destruct (Script_ir_annot.check_type_annot _ _); simpl;
      try rewrite cast_eval; try reflexivity
    ).
    all : try (
      destruct (parse_memo_size _); simpl; [rewrite cast_eval|]; reflexivity
    ).
    all:
      replace (z_number_10001 - Z.pos (Pos.of_succ_nat fuel) +i 1)
        with (fuel_to_stack_depth fuel) by tr_lia.
    all:
      replace Don't_parse_entrypoints
        with (Parse_ty_ret_family.to_parse_ty_ret
          Parse_ty_ret_family.Don't_parse_entrypoints) by reflexivity.
    all: repeat (
      rewrite <- dep_parse_comparable_ty_aux_fuel_eq by lia;
      destruct (dep_parse_comparable_ty_aux_fuel _); simpl; [|reflexivity];
      Tactics.destruct_pairs; step; simpl; try reflexivity
    ).
    all: repeat (
      rewrite <- dep_parse_ty_aux_fuel_eq
        with (ret_value := Parse_ty_ret_family.Don't_parse_entrypoints)
        by lia;
      destruct (dep_parse_ty_aux_fuel _); simpl; [|reflexivity];
      Tactics.destruct_pairs; step; simpl; try reflexivity
    ).
    all: unfold
      Script_typed_ir.contract_t,
      Script_typed_ir.lambda_t,
      Script_typed_ir.list_t,
      Script_typed_ir.map_t,
      Script_typed_ir.option_t,
      Script_typed_ir.pair_t,
      Script_typed_ir.union_t,
      Script_typed_ir.set_t,
      Script_typed_ir.ticket_t.
    all: try (
      step; simpl; [|reflexivity];
      now rewrite cast_eval
    ).
    all: repeat (
      destruct (Script_ir_annot.remove_field_annot _); simpl; try reflexivity
    ).
    all: try (
      destruct (Script_ir_annot.check_composed_type_annot _); simpl;
        [|reflexivity]
    ).
    all: try (
      rewrite <- dep_parse_big_map_ty_fuel_eq by lia;
      destruct dep_parse_big_map_ty_fuel; simpl; [|reflexivity];
      Tactics.destruct_pairs; simpl; step; simpl; now rewrite cast_eval
    ).
    all: repeat (
      rewrite <- dep_parse_ty_aux_fuel_eq
        with (ret_value := Parse_ty_ret_family.Don't_parse_entrypoints)
        by lia;
      destruct (dep_parse_ty_aux_fuel _); simpl; try reflexivity;
      Tactics.destruct_pairs; simpl; try reflexivity
    ).
    all:
      repeat (try rewrite cast_eval; step; simpl);
      try rewrite cast_eval; reflexivity.
    (* We set this function back to transparent. *)
    Transparent parse_ty_aux.
  }
}
{ intros H_fuel_valid.
  destruct fuel; simpl; unfold fuel_to_stack_depth.
  { replace (z_number_10001 - 0) with z_number_10001 by lia.
    destruct args; simpl.
    all: destruct Alpha_context.Gas.consume; simpl; try reflexivity.
    destruct args; simpl; [reflexivity|].
    destruct args; simpl; [|reflexivity].
    destruct n; simpl;
      replace (z_number_10001 +i 1 >i 10000) with true by lia.
    all: destruct Alpha_context.Gas.consume; reflexivity.
  }
  { destruct args; simpl.
    all: destruct Alpha_context.Gas.consume; simpl; try reflexivity.
    destruct args; simpl; [reflexivity|].
    destruct args; simpl; [|reflexivity].
    replace (z_number_10001 - Z.pos (Pos.of_succ_nat fuel) +i 1)
        with (fuel_to_stack_depth fuel) by tr_lia.
    rewrite <- dep_parse_comparable_ty_aux_fuel_eq by lia.
    match goal with
    | |- context[dep_parse_comparable_ty_aux_fuel ?fuel ?ctxt ?node_value] ⇒
      assert (H_consume_parse_eq :
        (let ? ' _ :=
          Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle in
        dep_parse_comparable_ty_aux_fuel fuel ctxt node_value) =
        dep_parse_comparable_ty_aux_fuel fuel ctxt node_value
      )
    end. {
      destruct fuel; simpl;
        destruct Alpha_context.Gas.consume; simpl;
        reflexivity.
    }
    destruct Alpha_context.Gas.consume; simpl in *;
      [|now rewrite <- H_consume_parse_eq].
    destruct dep_parse_comparable_ty_aux_fuel; simpl; [|reflexivity].
    Tactics.destruct_pairs; step; simpl.
    rewrite <- dep_parse_ty_aux_fuel_eq
      with (ret_value := Parse_ty_ret_family.Don't_parse_entrypoints)
      by lia.
    destruct dep_parse_ty_aux_fuel; simpl; [|reflexivity].
    Tactics.destruct_pairs; step; simpl.
    destruct Script_ir_annot.check_type_annot; simpl; [|reflexivity].
    unfold Script_typed_ir.big_map_t; simpl.
    step; reflexivity.
  }
}
Qed.

The simulation [dep_parse_ty_aux] is valid.

Lemma dep_parse_ty_aux_eq
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
  (allow_ticket : bool) (ret_value : Parse_ty_ret_family.t)
  (node_value : Alpha_context.Script.node) :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_ty_aux
      ctxt stack_depth legacy
      allow_lazy_storage allow_operation allow_contract
      allow_ticket ret_value node_value in
  return ? (Parse_ty_ret_family.to_ret ret_value result, ctxt)) =
  parse_ty_aux
    ctxt stack_depth legacy
    allow_lazy_storage
    allow_operation allow_contract allow_ticket
    (Parse_ty_ret_family.to_parse_ty_ret ret_value) node_value.
Proof.
  intros.
  unfold dep_parse_ty_aux, stack_depth_to_fuel.
  rewrite dep_parse_ty_aux_fuel_eq; f_equal; lia.
Qed.

The simulation [dep_parse_big_map_ty] is valid.

Lemma dep_parse_big_map_ty_eq ctxt stack_depth legacy loc_value args annot :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_big_map_ty ctxt stack_depth legacy loc_value args annot in
  return ? (to_ex_ty result, ctxt)) =
  parse_big_map_ty ctxt stack_depth legacy loc_value args annot.
Proof.
  intros.
  unfold dep_parse_big_map_ty, stack_depth_to_fuel.
  rewrite dep_parse_big_map_ty_fuel_eq; f_equal; lia.
Qed.

The simulation [dep_parse_passable_ty_aux_with_ret] is valid.

Lemma dep_parse_passable_ty_aux_with_ret_eq ctxt stack_depth legacy ret_value
  node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_passable_ty_aux_with_ret ctxt stack_depth legacy ret_value
      node_value in
  return ? (Parse_ty_ret_family.to_ret ret_value result, ctxt)) =
  parse_passable_ty_aux_with_ret ctxt stack_depth legacy
    (Parse_ty_ret_family.to_parse_ty_ret ret_value) node_value.
Proof.
  intros.
  unfold dep_parse_passable_ty_aux_with_ret, stack_depth_to_fuel,
    parse_passable_ty_aux_with_ret.
  rewrite dep_parse_ty_aux_fuel_eq; f_equal; lia.
Qed.

The simulation [dep_parse_any_ty_aux] is valid.

Lemma dep_parse_any_ty_aux_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_any_ty_aux ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_any_ty_aux ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_ty_aux_fuel_eq
      ctxt (stack_depth_to_fuel stack_depth) legacy true true true true
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq.
  unfold dep_parse_any_ty_aux, stack_depth_to_fuel, parse_any_ty_aux in ×.
  destruct dep_parse_ty_aux_fuel; simpl in *; Tactics.destruct_pairs;
    rewrite H_eq; f_equal; lia.
Qed.

The simulation [dep_parse_big_map_value_ty_aux] is valid.

Lemma dep_parse_big_map_value_ty_aux_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_big_map_value_ty_aux ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_big_map_value_ty_aux ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_ty_aux_fuel_eq
      ctxt (stack_depth_to_fuel stack_depth) legacy false false legacy true
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq.
  unfold dep_parse_big_map_value_ty_aux, stack_depth_to_fuel,
    parse_big_map_value_ty_aux in ×.
  destruct dep_parse_ty_aux_fuel; simpl in *; Tactics.destruct_pairs;
    rewrite H_eq; f_equal; lia.
Qed.

The simulation [dep_parse_packable_ty_aux] is valid.

Lemma dep_parse_packable_ty_aux_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_packable_ty_aux ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_packable_ty_aux ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_ty_aux_eq
      ctxt stack_depth legacy false false legacy false
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq; simpl in H_eq.
  now apply H_eq.
Qed.

The simulation [dep_parse_view_input_ty] is valid.

Lemma dep_parse_view_input_ty_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_view_input_ty ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_view_input_ty ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_ty_aux_eq
      ctxt stack_depth legacy false false true false
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq; simpl in H_eq.
  now apply H_eq.
Qed.

The simulation [dep_parse_view_output_ty] is valid.

Lemma dep_parse_view_output_ty_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_view_output_ty ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_view_output_ty ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_ty_aux_eq
      ctxt stack_depth legacy false false true false
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq; simpl in H_eq.
  now apply H_eq.
Qed.

The simulation [dep_parse_normal_storage_ty] is valid.

Lemma dep_parse_normal_storage_ty_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_normal_storage_ty ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_normal_storage_ty ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_ty_aux_eq
      ctxt stack_depth legacy true false legacy true
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq; simpl in H_eq.
  now apply H_eq.
Qed.

The simulation [dep_parse_storage_ty] is valid.

Lemma dep_parse_storage_ty_eq
  (ctxt : Alpha_context.context)
  (stack_depth : int)
  (legacy : bool)
  (node_value : Alpha_context.Script.node):
  0 ≤ stack_depth ≤ z_number_10001 →
  0 ≤ stack_depth +i 1 ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_storage_ty ctxt stack_depth legacy node_value in
    return ? (to_ex_ty result, ctxt)) =
      parse_storage_ty ctxt stack_depth legacy node_value.
Proof.
  intros.
  destruct node_value eqn:G; simpl;
  unfold dep_parse_storage_ty;
  unfold parse_storage_ty;
  try rewrite dep_parse_normal_storage_ty_eq; try easy;
  consume_gas;
  destruct_all Michelson_v1_primitives.prim;
  try rewrite <- dep_parse_normal_storage_ty_eq; try easy.
  { do 8 (step; try apply dep_parse_normal_storage_ty_eq; try easy);
    destruct ((String.length s >i 0)
      && (Char.compare (String.get s 0) "%"%char =? 0));
    try easy.
    Import Coq.Program.Equality.
    all:
      unfold op_gtgtquestion;
      unfold Error_monad.ok;
      rewrite <- dep_parse_big_map_ty_eq; try easy;
      destruct dep_parse_big_map_ty; try easy;
      destruct p0;
      destruct d; simpl;
      rewrite <- dep_parse_normal_storage_ty_eq; try easy;
      destruct dep_parse_normal_storage_ty; try easy;
      destruct p0;
      destruct d;
      destruct
        (Script_ir_annot.check_composed_type_annot); try easy; simpl;
      rewrite <- Script_typed_ir.dep_pair_t_eq;
      destruct dep_pair_t; try easy;
      destruct d;
      destruct Dependent_bool.dand_value; simpl;
      dependent destruction t4; simpl.
    all:
      (* TODO: remove axiom *)
      replace (t4_1) with t1 by apply axiom;
      replace (t4_2) with t3 by apply axiom;
      replace (d) with d0 by apply axiom;
      try reflexivity.
  }
  { repeat (step; try apply dep_parse_normal_storage_ty_eq; try easy). }
Qed.

The simulation [dep_check_packable] is valid.

Lemma dep_check_packable_eq {t}
  (legacy : bool) (loc_value : Alpha_context.Script.location)
  (root_value : With_family.ty t) :
    dep_check_packable legacy loc_value root_value =
      check_packable legacy loc_value (With_family.to_ty root_value).
Proof.
  induction root_value; hauto q: on.
Qed.

The simulation [dep_make_dug_proof_argument] is valid.

Fixpoint dep_make_dug_proof_argument_eq {x s} loc_value n_value
  (x_value : With_family.ty x) (stk : With_family.stack_ty s) :
  (let × result :=
    dep_make_dug_proof_argument loc_value n_value x_value stk in
  Some (to_dug_proof_argument result)) =
  make_dug_proof_argument loc_value n_value
    (With_family.to_ty x_value) (With_family.to_stack_ty stk).
Proof.
  destruct stk; simpl.
  all: destruct n_value; simpl; try reflexivity.
  all: rewrite <- dep_make_dug_proof_argument_eq.
  all: destruct dep_make_dug_proof_argument; simpl; f_equal.
  all: now step.
Qed.

The simulation [dep_make_comb_get_proof_argument] is valid.

Fixpoint dep_make_comb_get_proof_argument_eq {b} n_value
  (ty : With_family.ty b) :
  (let × result := dep_make_comb_get_proof_argument n_value ty in
  Some (to_comb_get_proof_argument result)) =
  make_comb_get_proof_argument n_value (With_family.to_ty ty).
Proof.
  destruct ty, n_value as [|[]|]; simpl; try reflexivity.
  all: rewrite <- dep_make_comb_get_proof_argument_eq.
  all: destruct dep_make_comb_get_proof_argument; simpl; try reflexivity.
  all: now step.
Qed.

The simulation [dep_make_comb_set_proof_argument] is valid.

Fixpoint dep_make_comb_set_proof_argument_eq {s value before}
  ctxt (st : With_family.stack_ty s) loc_value n_value
  (value_ty : With_family.ty value) (ty : With_family.ty before) :
  Script_typed_ir.With_family.Valid.stack_ty st →
  (let ? result :=
    dep_make_comb_set_proof_argument
      ctxt st loc_value n_value value_ty ty in
  return ? (to_comb_set_proof_argument result )) =
  make_comb_set_proof_argument ctxt (With_family.to_stack_ty st)
    loc_value n_value (With_family.to_ty value_ty) (With_family.to_ty ty).
Proof.
  intros H.
  destruct ty, n_value as [|[]|]; try easy; simpl.
  all: try rewrite <- dep_serialize_stack_for_error_eq;
    try reflexivity; try apply H.
  all: try rewrite <- dep_make_comb_set_proof_argument_eq;
    try destruct dep_make_comb_set_proof_argument as [|d0]; try apply H; try easy.
  all: try destruct d0; try reflexivity; simpl.
  all: rewrite <- Script_typed_ir.dep_pair_t_eq; simpl.
  all: unfold op_gtgtquestion; unfold Error_monad.ok.
  all: repeat (step; try reflexivity).
Qed.

Equality between [dep_ex_ty_cstr] and [ex_ty_cstr].

Module Eq_ex_ty_cstr.
  Inductive t {a : Ty.t} :
    dep_ex_ty_cstr a → ex_ty_cstr (Ty.to_Set a) → Prop :=
  | Intro {b : Ty.t}
    (ty : With_family.ty b)
    (dep_construct : With_family.ty_to_dep_Set b → With_family.ty_to_dep_Set a)
    (construct : Ty.to_Set b → Ty.to_Set a)
    (original_type_expr : Alpha_context.Script.node) :
    (∀ v,
      With_family.to_value (dep_construct v) =
      construct (With_family.to_value v)) →
    t
      (Dep_ex_ty_cstr ty dep_construct original_type_expr)
      (Ex_ty_cstr {|
        ex_ty_cstr.Ex_ty_cstr.ty := With_family.to_ty ty;
        ex_ty_cstr.Ex_ty_cstr.construct := construct;
        ex_ty_cstr.Ex_ty_cstr.original_type_expr := original_type_expr;
      |}).
End Eq_ex_ty_cstr.

The simulation [dep_find_entrypoint] is valid.

Lemma dep_find_entrypoint_eq {error_trace} {full : Ty.t}
  (error_details : Script_tc_errors.dep_error_details error_trace)
  (full_value : With_family.ty full)
  (entrypoints : Script_typed_ir.entrypoints)
  (entrypoint : Alpha_context.Entrypoint.t) :
  Gas_monad.Eq.t (trace := Script_tc_errors.Error_trace_family.to_Set error_trace) Eq_ex_ty_cstr.t
    (dep_find_entrypoint error_details full_value entrypoints entrypoint)
    (find_entrypoint
      (Script_tc_errors.to_error_details error_details)
      (With_family.to_ty full_value)
      entrypoints
      entrypoint).
Admitted.

The simulation [dep_find_entrypoint_for_type] is valid.

Lemma dep_find_entrypoint_for_type_eq {full exp : Ty.t} {error_trace}
  (error_details : Script_tc_errors.dep_error_details error_trace)
  (full_value : With_family.ty full) (expected : With_family.ty exp)
  (entrypoints : Script_typed_ir.entrypoints)
  (entrypoint : Alpha_context.Entrypoint.t)
  (loc_value : Alpha_context.Script.location) ctxt :
  (let ? '(res , error_trace ) := Gas_monad.run ctxt
    (dep_find_entrypoint_for_type error_details full_value expected entrypoints
      entrypoint loc_value) in
  return ? (let ? '(ctxt , res ) := res in return ? (ctxt, With_family.to_ty res), error_trace))
  =
    Gas_monad.run ctxt
      (find_entrypoint_for_type
        (error_trace := Script_tc_errors.Error_trace_family.to_Set error_trace)
        (full := Ty.to_Set full)
        (Script_tc_errors.to_error_details error_details)
        (With_family.to_ty full_value) (With_family.to_ty expected)
        entrypoints entrypoint loc_value).
Proof.
  (* TODO: Remove axiom from definition *)
Admitted.

The simulation [dep_well_formed_entrypoints] is valid.

Lemma dep_well_formed_entrypoints_eq {full} (full_value : With_family.ty full)
  (entrypoints : Script_typed_ir.entrypoints_node) :
  dep_well_formed_entrypoints full_value entrypoints =
  well_formed_entrypoints (With_family.to_ty full_value) entrypoints.
Proof.
Admitted.

The simulation [dep_parse_parameter_ty_and_entrypoints_aux] is valid.

Lemma dep_parse_parameter_ty_and_entrypoints_aux_eq ctxt stack_depth legacy
  node_value :
  0 ≤ stack_depth + 1 ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_parameter_ty_and_entrypoints_aux ctxt stack_depth legacy node_value in
  return ? (to_ex_parameter_ty_and_entrypoints result, ctxt)) =
  parse_parameter_ty_and_entrypoints_aux ctxt stack_depth legacy node_value.
Proof.
  intros.
  unfold dep_parse_parameter_ty_and_entrypoints_aux,
    parse_parameter_ty_and_entrypoints_aux.
  pose proof (
    dep_parse_passable_ty_aux_with_ret_eq
      ctxt (stack_depth +i 1) legacy
      Parse_ty_ret_family.Parse_entrypoints node_value
  ) as H_eq; simpl in H_eq.
  destruct dep_parse_passable_ty_aux_with_ret;
    simpl in *; Tactics.destruct_pairs;
    rewrite <- H_eq by tr_lia; simpl; [|reflexivity].
  repeat (
    try rewrite dep_well_formed_entrypoints_eq;
    step; simpl; try reflexivity
  ).
Qed.

The simulation [dep_parse_passable_ty_aux] is valid.

Lemma dep_parse_passable_ty_aux_eq ctxt stack_depth legacy node_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  (let ? '(result , ctxt ) :=
    dep_parse_passable_ty_aux ctxt stack_depth legacy node_value in
  return ? (to_ex_ty result, ctxt)) =
  parse_passable_ty_aux ctxt stack_depth legacy node_value.
Proof.
  intros.
  pose proof (
    dep_parse_passable_ty_aux_with_ret_eq
      ctxt stack_depth legacy
      Parse_ty_ret_family.Don't_parse_entrypoints node_value
  ) as H_eq; simpl in H_eq.
  now apply H_eq.
Qed.

The simulation [dep_opened_ticket_type] is valid.

Lemma dep_opened_ticket_type_eq {a} loc (ty : With_family.ty a) :
  (let ? ty := dep_opened_ticket_type loc ty in
  return ? (With_family.to_ty ty )) =
  opened_ticket_type loc (With_family.to_ty ty).
Proof.
  unfold dep_opened_ticket_type, opened_ticket_type.
  apply Script_typed_ir.dep_pair_3_key_eq.
Qed.

The simulation [dep_comparable_comb_witness1] is valid.

Lemma dep_comparable_comb_witness1_eq {t} (ty : With_family.ty t) :
dep_comparable_comb_witness1 ty =
comparable_comb_witness1 (With_family.to_ty ty).
Proof. destruct ty; reflexivity. Qed.

The proof that [dep_parse_comparable_data] works in the same way as [parse_comparable_data].

The proof goes by induction on [ty].

Fixpoint dep_parse_comparable_data_eq a logger ctxt (ty : With_family.ty a) n :
  Script_typed_ir.With_family.is_Comparable ty →
  Script_typed_ir.With_family.Valid.ty ty →
  dep_parse_comparable_data logger ctxt ty n =
    parse_comparable_data logger ctxt (With_family.to_ty ty) n.
Proof.
  intros Hcmp Hv; destruct ty eqn:?Ety; try destruct Hcmp; simpl;
    consume_gas; repeat rewrite cast_eval; try reflexivity; try step;
    try destruct Hcmp.
  all:
    match goal with
    | t1 : Ty.t |- context[cast_exists ?T _] ⇒
      rewrite (cast_exists_eval_1 (T := T)
        (E1 := With_family.ty_to_dep_Set t1)
      );
      rewrite cast_eval
    | t1 : Ty.t, t2 : Ty.t |- context[cast_exists ?T _] ⇒
      rewrite (cast_exists_eval_2 (T := T)
        (E1 := With_family.ty_to_dep_Set t1)
        (E2 := With_family.ty_to_dep_Set t2)
      );
      rewrite cast_eval
    end.
  all: f_equal; [|f_equal].
  all: repeat (apply FunctionalExtensionality.functional_extensionality; intro).
  all: try now rewrite dep_parse_comparable_data_eq.
  all: repeat f_equal.
  4: apply dep_comparable_comb_witness1_eq.
  all: try rewrite dep_serialize_ty_for_error_eq; f_equal.
  all: unfold dep_ty_of_comparable_ty; simpl.
  all: repeat rewrite <- dep_ty_of_comparable_ty_eq by assumption.
  all: try split; try apply Hv.
  all: rewrite dep_parse_comparable_data_eq; trivial; apply Hv.
Qed.

Easy lemma about [dep_comb_witness1] equality. The proof is by trivial case analysis on [ty].

Lemma dep_comb_witness1_eq {a} (ty : With_family.ty a) :
dep_comb_witness1 ty = comb_witness1 (With_family.to_ty ty).
Proof.
destruct ty; reflexivity.
Qed.

The simulation [dep_parse_data_aux] is valid.

Lemma dep_parse_data_aux_eq {a}
  (type_logger_value : option type_logger) (stack_depth : int)
  (ctxt : Alpha_context.context) (legacy : bool) (allow_forged : bool)
  (ty : With_family.ty a) (expr : Alpha_context.Script.node) :
  (let ? '(result , ctxt ) :=
    dep_parse_data_aux
      type_logger_value stack_depth ctxt legacy allow_forged ty expr in
  return ? (With_family.to_value result, ctxt)) =
  parse_data_aux
    type_logger_value stack_depth ctxt legacy allow_forged
    (With_family.to_ty ty) expr.
Proof.
Admitted.

The simulation [dep_parse_view_returning] is valid.

Lemma dep_parse_view_returning_eq {storage}
  type_logger_value ctxt legacy (storage_type : With_family.ty storage) view :
  (let ? '(result , ctxt ) :=
    dep_parse_view_returning type_logger_value ctxt legacy storage_type view in
  return ? (to_ex_view result, ctxt)) =
  parse_view_returning type_logger_value ctxt legacy
    (With_family.to_ty storage_type) view.
Proof.
Admitted.

The simulation [dep_typecheck_views] is valid.

Lemma dep_typecheck_views_eq {storage}
  (type_logger_value : option type_logger) (ctxt : Alpha_context.context)
  (legacy : bool) (storage_type : With_family.ty storage)
  (views : With_family.view_map) :
  dep_typecheck_views type_logger_value ctxt legacy storage_type views =
  typecheck_views type_logger_value ctxt legacy
    (With_family.to_ty storage_type) (With_family.to_view_map views).
Proof.
  Opaque Script_map.fold_es.
  destruct type_logger_value eqn:?;
  unfold dep_typecheck_views, With_family.to_view_map; simpl.
  {
    rewrite → (Script_map.dep_fold_es_eq'
      ((fun (_ : With_family.ty_to_dep_Set Ty.String)
        (cur_view : Script_typed_ir.view) (ctxt0 : Alpha_context.context) ⇒
          let ? ' (_, ctxt1 )
          := dep_parse_view_returning (Some t) ctxt0 legacy storage_type cur_view
          in return ? ctxt1))
      (fun (_ : Alpha_context.Script_string.t) (cur_view : Script_typed_ir.view)
        (ctxt0 : Alpha_context.context) ⇒
          let ? ' (_, ctxt1 )
          := parse_view_returning (Some t) ctxt0 legacy
            (With_family.to_ty storage_type) cur_view in return ? ctxt1)
      views
      ctxt
    );
    try easy; intros; rewrite <- dep_parse_view_returning_eq;
    do 2 (step; simpl; try reflexivity).
  }
  {
    rewrite → (Script_map.dep_fold_es_eq'
      ((fun (_ : With_family.ty_to_dep_Set Ty.String)
        (cur_view : Script_typed_ir.view) (ctxt0 : Alpha_context.context) ⇒
          let ? ' (_, ctxt1 )
          := dep_parse_view_returning None ctxt0 legacy storage_type cur_view
          in return ? ctxt1))
      (fun (_ : Alpha_context.Script_string.t) (cur_view : Script_typed_ir.view)
        (ctxt0 : Alpha_context.context) ⇒
          let ? ' (_, ctxt1 )
          := parse_view_returning None ctxt0 legacy
            (With_family.to_ty storage_type) cur_view in return ? ctxt1)
      views
      ctxt
    );
    try easy; intros; rewrite <- dep_parse_view_returning_eq;
    do 2 (step; simpl; try reflexivity).
  }
  Transparent Script_map.fold_es.
Qed.

The simulation [dep_parse_instr_aux] is valid.

Lemma dep_parse_instr_aux_eq {s}
  (type_logger_value : option type_logger) (stack_depth : int)
  (tc_context_value : dep_tc_context) (ctxt : Alpha_context.context)
  (legacy : bool)
  (script_instr : Alpha_context.Script.node)
  (stack_ty : With_family.stack_ty s) :
  Error_monad.Eq.t
    (fun '(dep_result , dep_ctxt ) '(result , ctxt ) ⇒
      Eq_judgement.t dep_result result ∧
      dep_ctxt = ctxt
    )
    (dep_parse_instr_aux type_logger_value stack_depth tc_context_value ctxt
      legacy script_instr stack_ty)
    (parse_instr_aux type_logger_value stack_depth (to_tc_context tc_context_value) ctxt legacy
      script_instr (With_family.to_stack_ty stack_ty)).
Admitted.

The simulation [dep_parse_view_name] is valid

Lemma dep_parse_view_name_eq
  (ctxt : Alpha_context.context)
  (n : Micheline.node Alpha_context.Script.location Alpha_context.Script.prim)
  : dep_parse_view_name ctxt n = parse_view_name ctxt n.
Proof. Admitted.

The simulation [dep_find_fields] is valid

Fixpoint dep_find_fields_eq
  (ctxt : Alpha_context.context)
  (p_value :
    option
      (Micheline.node Alpha_context.Script.location
        Alpha_context.Script.prim × Alpha_context.Script.location ×
        Micheline.annot))
  (s_value :
    option
      (Micheline.node Alpha_context.Script.location
        Alpha_context.Script.prim × Alpha_context.Script.location ×
        Micheline.annot))
  (c_value :
    option
      (Micheline.node Alpha_context.Script.location
        Alpha_context.Script.prim × Alpha_context.Script.location ×
        Micheline.annot))
  (views : With_family.view_map)
  (fields :
    list
      (Micheline.node Alpha_context.Script.location
        Alpha_context.Script.prim))
  {struct fields}
  : (let ? '(ctxt , result ) := dep_find_fields
        ctxt p_value s_value c_value views fields in
    let '(a, b, c, d) := result in
    return ? (ctxt, (a, b, c, With_family.to_view_map d)))
    =
    find_fields
      ctxt p_value s_value c_value (With_family.to_view_map views) fields.
Proof.
  Opaque
    Script_map.mem
    Script_map.dep_mem
    Script_map.update
    Script_map.dep_update
    With_family.to_map_aux.
  destruct fields; simpl; [reflexivity|].
  do 7 (step; simpl; try reflexivity; try apply dep_find_fields_eq).
  rewrite dep_parse_view_name_eq.
  step; Tactics.destruct_pairs; [|reflexivity]; simpl.
  consume_gas; simpl.
  rewrite → Script_map.dep_mem_eq'.
  destruct Script_map.mem; simpl; [reflexivity|].
  rewrite → dep_find_fields_eq; simpl.
  unfold With_family.to_view_map.
  rewrite → Script_map.dep_update_eq'; reflexivity.
  Transparent
    Script_map.mem
    Script_map.dep_mem
    Script_map.update
    Script_map.dep_update
    With_family.to_map_aux.
Qed.

The simulation [dep_parse_toplevel_aux] is valid.

Lemma dep_parse_toplevel_aux_eq
  (ctxt : Alpha_context.context) (legacy : bool)
  (toplevel_value : Alpha_context.Script.expr) :
  (let ? '(result , ctxt ) :=
    dep_parse_toplevel_aux ctxt legacy toplevel_value in
  return ? (to_toplevel result, ctxt)) =
  parse_toplevel_aux ctxt legacy toplevel_value.
Proof.
  unfold dep_parse_toplevel_aux.
  destruct toplevel_value; simpl; try reflexivity.
  assert (Script_map.empty Script_typed_ir.string_key =
    With_family.to_view_map
      (Script_map.dep_empty dep_string_key)) as H.
  {
    unfold With_family.to_view_map.
    rewrite → Script_map.dep_empty_eq'; easy.
  }
  rewrite H.
  replace (_ ctxt None None None
    (Script_map.dep_empty dep_string_key) l)
  with (dep_find_fields ctxt None None None
    (Script_map.dep_empty dep_string_key) l) by reflexivity.
  rewrite <- dep_find_fields_eq; simpl.
  do 14 (step; simpl; try reflexivity; try apply dep_find_fields_eq).
  destruct (Script_ir_annot.has_field_annot n);
    simpl; try reflexivity.
  destruct b; simpl;
  repeat (step; simpl; try reflexivity).
Qed.

The simulation [dep_parse_returning] is valid.

Lemma dep_parse_returning_eq {a r : Ty.t}
  (type_logger_value : option type_logger) (stack_depth : int)
  (tc_context_value : dep_tc_context) (ctxt : Alpha_context.context)
  (legacy : bool) (arg : With_family.ty a) (ret_value : With_family.ty r)
  (script_instr : Alpha_context.Script.node) :
  (let ? '(result , ctxt ) :=
    dep_parse_returning type_logger_value stack_depth tc_context_value ctxt
      legacy arg ret_value script_instr in
  return ? (With_family.to_lambda result, ctxt)) =
  parse_returning type_logger_value stack_depth (to_tc_context tc_context_value)
    ctxt legacy (With_family.to_ty arg) (With_family.to_ty ret_value)
    script_instr.
Admitted.

The simulation [dep_parse_contract_aux] is valid.

Lemma dep_parse_contract_aux_eq {a}
  (fuel : nat) (ctxt : Alpha_context.context)
  (loc_value : Alpha_context.Script.location) (arg : With_family.ty a)
  (destination : Alpha_context.Destination.t)
  (entrypoint : Alpha_context.Entrypoint.t) :
  0 ≤ fuel_to_stack_depth fuel ≤ z_number_10001 - 2 →
  Script_typed_ir.With_family.Valid.ty arg →
  Script_typed_ir.With_family.is_Comparable arg →
  (let ? '(ctxt , result ) :=
     dep_parse_contract_aux
       (fuel_to_stack_depth fuel) ctxt loc_value arg destination entrypoint in
  return ? (ctxt, With_family.to_typed_contract result)) =
    parse_contract_aux
      (fuel_to_stack_depth fuel) ctxt loc_value
      (With_family.to_ty arg) destination entrypoint.
Proof.
  intros H **.
  unfold dep_parse_contract_aux, parse_contract_aux.
  rewrite fuel_to_stack_depth_to_fuel; [|lia].
  unfold fuel_to_stack_depth in H.
  destruct fuel; [simpl in H; lia|]; simpl.
  step; simpl.
  { destruct Alpha_context.Contract.is_implicit; simpl.
    {
      step; simpl; [|reflexivity].
      change Script_tc_errors.Informative with
        (Script_tc_errors.to_error_details Script_tc_errors.Dep_informative).
      change Script_typed_ir.unit_t with
        (With_family.to_ty Script_typed_ir.dep_unit_t).
      pose proof (
        dep_ty_eq_eq
          Script_tc_errors.Dep_informative
          loc_value
          arg
          dep_unit_t
      ) as H_ty_eq.
      simpl in ×.
      rewrite <- H_ty_eq.
      rewrite Gas_monad.run_map.
      destruct Gas_monad.run; simpl; [|reflexivity].
      repeat (step; simpl; try reflexivity).
    }
    {
      do 5 (step; simpl; try reflexivity).
      rewrite <- dep_parse_toplevel_aux_eq.
      destruct dep_parse_toplevel_aux; simpl; [|reflexivity].
      step; simpl.
      unfold "+i"; rewrite Pervasives.normalize_identity; [|tr_lia].
      rewrite <- dep_parse_parameter_ty_and_entrypoints_aux_eq; [|tr_lia].
      do 3 (step; simpl; try reflexivity).
      match goal with
      |_ : With_family.ty ?xa |- context[cast_exists ?T _] ⇒
         rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set xa))
      end.
      change Script_tc_errors.Informative
        with (Script_tc_errors.to_error_details
                Script_tc_errors.Dep_informative).
      rewrite <- (dep_find_entrypoint_for_type_eq Script_tc_errors.Dep_informative).
      run_gas_monad; simpl; [|reflexivity].
      do 3 (step; simpl; try reflexivity).
    }
  }
  {
    destruct Alpha_context.Tx_rollup_state.assert_exist;
      simpl; [|reflexivity].
    do 2 (step; simpl; try reflexivity).
    repeat (step; simpl).
    all : try rewrite → dep_serialize_ty_for_error_eq; try easy.
  }
Qed.

The simulation [dep_parse_contract_for_script] is valid.

Lemma dep_parse_contract_for_script_eq {a}
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (arg : With_family.ty a) (contract : Alpha_context.Destination.t)
  (entrypoint : Alpha_context.Entrypoint.t) :
  Script_typed_ir.With_family.is_Comparable arg →
  (let ? '(ctxt , result ) :=
    dep_parse_contract_for_script ctxt loc_value arg contract entrypoint in
  return ? (ctxt, Option.map With_family.to_typed_contract result)) =
  parse_contract_for_script ctxt loc_value (With_family.to_ty arg) contract
    entrypoint.
Proof.
  intros H1.
  unfold dep_parse_contract_for_script, parse_contract_for_script.
  step; simpl.
  {
    step; simpl.
    {
      step; simpl; [|now destruct Alpha_context.Gas.consume].
      change Script_tc_errors.Fast with
        (Script_tc_errors.to_error_details Script_tc_errors.Dep_fast).
      change Script_typed_ir.unit_t with
        (With_family.to_ty Script_typed_ir.dep_unit_t).
      pose proof (
        dep_ty_eq_eq
          Script_tc_errors.Dep_fast
          loc_value
          arg
          dep_unit_t
      ) as H_ty_eq.
      simpl in ×.
      rewrite <- H_ty_eq.
      rewrite Gas_monad.run_map.
      destruct Gas_monad.run; simpl; [|reflexivity].
      repeat (step; simpl; try reflexivity).
    }
    {
      do 7 (step; simpl; try reflexivity).
      rewrite <- dep_parse_parameter_ty_and_entrypoints_aux_eq; try easy.
      do 3 (step; simpl; try reflexivity).
      match goal with
      | _ : ?t |- context[cast_exists ?T _] ⇒
        rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set a0))
      end.
      change Script_tc_errors.Fast
        with (Script_tc_errors.to_error_details
                Script_tc_errors.Dep_fast).
      rewrite <- (dep_find_entrypoint_for_type_eq Script_tc_errors.Dep_fast).
      run_gas_monad; [|reflexivity]; simpl.
      do 3 (step; simpl; try reflexivity).
    }
  }
  {
    repeat (step; simpl; try reflexivity).
  }
Qed.

The simulation of [dep_code_size] is valid

Definition dep_code_size_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (code : With_family.lambda a b)
  (views : With_family.view_map)
  : dep_code_size ctxt code views =
    code_size ctxt (With_family.to_lambda code) (With_family.to_view_map views).
  unfold dep_code_size, code_size.
  do 2 match goal with
  | |- context [
       Script_typed_ir_size.op_plusplus ?arg1 ?arg2
      ] ⇒
      let fold := fresh "fold" in
      let arg := fresh "arg" in
      set (fold := arg1); set (arg := arg2); symmetry
  end.
  replace fold0 with fold; [reflexivity|].
  subst fold fold0.
  match goal with
  | |- _ ?f1' _ ?acc' = _ ?f2' _ ?acc' ⇒
      set (dep_f := f1'); set (f := f2');
      set (acc := acc')
  end.
  now rewrite (Script_map.dep_fold_eq' dep_f f views acc).
Qed.

The simulation [dep_parse_code] is valid.

Lemma dep_parse_code_eq
  (type_logger_value : option type_logger) (ctxt : Alpha_context.context)
  (legacy : bool) (code : Alpha_context.Script.lazy_expr) :
  (let ? '(result , ctxt ) := dep_parse_code type_logger_value ctxt legacy code in
  return ? (to_ex_code result, ctxt)) =
  parse_code type_logger_value ctxt legacy code.
Proof.
  unfold dep_parse_code, parse_code.
  destruct (Alpha_context.Script.force_decode_in_context
    Alpha_context.Script.When_needed ctxt code); [|reflexivity].
  { destruct p; simpl;
    step; simpl; [|reflexivity].
    destruct p; simpl.
    rewrite <- dep_parse_toplevel_aux_eq; simpl.
    destruct dep_parse_toplevel_aux; simpl; [|reflexivity].
    destruct p; simpl.
    assert (∀ c,
      (let ? ' (d , ctxt )
        := record_trace
          (Build_extensible "Ill_formed_type"
             (M × string × Alpha_context.Script.expr × Alpha_context.Script.location)
             (Some "parameter", c, location d.(dep_toplevel.arg_type)))
          (dep_parse_parameter_ty_and_entrypoints_aux c0 0 legacy d.(dep_toplevel.arg_type)) in
      return ? (to_ex_parameter_ty_and_entrypoints d, ctxt)) =
      record_trace
          (Build_extensible "Ill_formed_type"
            (M × string × Alpha_context.Script.expr × Alpha_context.Script.location)
            (Some "parameter", c, location (to_toplevel d).(toplevel.arg_type)))
          (parse_parameter_ty_and_entrypoints_aux c0 0 legacy (to_toplevel d).(toplevel.arg_type))
    ) as Heq1 by admit.
    rewrite <- Heq1; simpl.
    destruct record_trace; simpl; [|reflexivity].
    destruct p; simpl.
    destruct d0; simpl.
    assert (∀ c,
      (let ? ' (d , ctxt )
        := record_trace
          (Build_extensible "Ill_formed_type"
            (M × string × Alpha_context.Script.expr × Alpha_context.Script.location)
            (Some "storage", c, location d.(dep_toplevel.storage_type)))
          (dep_parse_storage_ty c1 0 legacy d.(dep_toplevel.storage_type)) in
      return ? (to_ex_ty d, ctxt)) =
        record_trace
          (Build_extensible "Ill_formed_type"
            (M × string × Alpha_context.Script.expr × Alpha_context.Script.location)
            (Some "storage", c, location (to_toplevel d).(toplevel.storage_type)))
          (parse_storage_ty c1 0 legacy (to_toplevel d).(toplevel.storage_type))
    ) as Heq2 by admit.
    rewrite <- Heq2; simpl.
    destruct record_trace; simpl; [|reflexivity].
    destruct p; simpl.
    destruct d0; simpl.
    rewrite <- Script_typed_ir.dep_pair_t_eq.
    destruct dep_pair_t; simpl; [|reflexivity].
    destruct d0; simpl.
    rewrite <- Script_typed_ir.dep_list_operation_t_eq.
    rewrite <- Script_typed_ir.dep_pair_t_eq.
    destruct dep_pair_t; simpl; [|reflexivity].
    destruct d0; simpl.
    assert (∀ c,
      (let ? ' (code , ctxt )
        := trace_value
          (Build_extensible "Ill_typed_contract"
            (Alpha_context.Script.expr × Script_tc_errors.type_map)
            (c, nil))
          (dep_parse_returning type_logger_value 0
            (Script_tc_context.dep_toplevel_value t3 t1 e0) c2 legacy t4
            t5 d.(dep_toplevel.code_field)) in
      return ? (With_family.to_lambda code, ctxt)) =
        trace_value
          (Build_extensible "Ill_typed_contract"
            (Alpha_context.Script.expr × Script_tc_errors.type_map)
            (c, nil))
          (parse_returning type_logger_value 0
            (Tc_context.toplevel_value (With_family.to_ty t3)
                (With_family.to_ty t1) e0) c2 legacy (With_family.to_ty t4)
            (With_family.to_ty t5) d.(dep_toplevel.code_field))
    ) as Heq3 by admit.
    rewrite <- Heq3.
    destruct trace_value; simpl; [|reflexivity].
    destruct p; simpl.
    rewrite <- dep_code_size_eq.
    destruct dep_code_size; simpl; [|reflexivity].
    destruct p; reflexivity.
  }
Admitted.

The simulation [dep_parse_storage] is valid.

Lemma dep_parse_storage_eq {storage}
  (type_logger_value : option type_logger) (ctxt : Alpha_context.context)
  (legacy : bool) (allow_forged : bool) (storage_type : With_family.ty storage)
  (storage_value : Alpha_context.Script.lazy_expr) :
  (let ? '(result , ctxt ) :=
    dep_parse_storage type_logger_value ctxt legacy allow_forged storage_type
      storage_value in
  return ? (With_family.to_value result, ctxt)) =
  parse_storage type_logger_value ctxt legacy allow_forged
    (With_family.to_ty storage_type) storage_value.
Proof.
  unfold parse_storage, dep_parse_storage.
  do 2 (step; simpl; try reflexivity).
  assert (
    (let ? ' (result , ctxt0 )
      := trace_eval
        (fun _ : unit ⇒
          Build_extensible "Ill_typed_data"
            (M × string × Alpha_context.Script.expr ×
            canonical Alpha_context.Script.prim)
            (None, e, dep_serialize_ty_for_error storage_type))
        (dep_parse_data_aux type_logger_value 0 t legacy allow_forged
            storage_type (root_value e))
    in return ? (With_family.to_value result, ctxt0)) =
      trace_eval
        (fun _ : unit ⇒
          Build_extensible "Ill_typed_data"
            (M × string × Alpha_context.Script.expr ×
            canonical Alpha_context.Script.prim)
            (None, e, serialize_ty_for_error (With_family.to_ty storage_type)))
        (parse_data_aux type_logger_value 0 t legacy allow_forged
            (With_family.to_ty storage_type) (root_value e))) as Heq1 by admit.
    rewrite <- Heq1.
    destruct trace_eval; reflexivity.
Admitted.

The simulation [dep_parse_script] is valid.

Lemma dep_parse_script_eq
  (type_logger_value : option type_logger) (ctxt : Alpha_context.context)
  (legacy : bool) (allow_forged_in_storage : bool)
  (script : Alpha_context.Script.t) :
  (let ? '(result , ctxt ) :=
    dep_parse_script type_logger_value ctxt legacy allow_forged_in_storage
      script in
  return ? (to_ex_script result, ctxt)) =
  parse_script type_logger_value ctxt legacy allow_forged_in_storage script.
Proof.
  unfold dep_parse_script, parse_script;
  rewrite <- dep_parse_code_eq;
  destruct dep_parse_code;
    Tactics.destruct_pairs;
    simpl; [|reflexivity].
  destruct_all dep_ex_code; simpl;
  match goal with
  | x : dep_code _ _ |- _ ⇒ destruct x
  end; simpl.
  match goal with
  | _ : With_family.lambda (Ty.Pair _ ?s) _ |- context [cast_exists ?T _] ⇒
    rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set s))
  end.
  rewrite <- dep_parse_storage_eq;
  destruct dep_parse_storage; Tactics.destruct_pairs; reflexivity.
Qed.

The simulation [dep_typecheck_code_inner] is valid.

Lemma dep_typecheck_code_inner_eq legacy show_types ctxt code :
  (let ? '(result , ctxt ) :=
     dep_typecheck_code_inner legacy show_types ctxt code in
  return ? (to_typechecked_code_internal result, ctxt)) =
  typecheck_code_inner legacy show_types ctxt code.
Proof.
  unfold dep_typecheck_code_inner, typecheck_code_inner.
  (* it looks like no one of them slows it down too much *)
  (* but after this, proof works noticeable faster *)
  Opaque
    parse_toplevel_aux parse_parameter_ty_and_entrypoints_aux
    parse_storage_ty parse_returning typecheck_views op_coloneq
    Tc_context.toplevel_value op_exclamation location dep_pair_t
    dep_parse_toplevel_aux dep_parse_parameter_ty_and_entrypoints_aux
    dep_parse_storage_ty.
  destruct Alpha_context.Global_constants_storage.expand; [|reflexivity];
  Tactics.destruct_pairs; simpl.
  rewrite <- dep_parse_toplevel_aux_eq;
    destruct dep_parse_toplevel_aux; [|reflexivity];
    Tactics.destruct_pairs; simpl.
  rewrite <- dep_parse_parameter_ty_and_entrypoints_aux_eq by tr_lia;
    destruct dep_parse_parameter_ty_and_entrypoints_aux; [|reflexivity];
    Tactics.destruct_pairs; simpl.
  rewrite <- dep_parse_storage_ty_eq by tr_lia;
    destruct dep_parse_storage_ty;
    destruct_all dep_ex_parameter_ty_and_entrypoints; [|reflexivity];
    Tactics.destruct_pairs; destruct_all dep_ex_ty; simpl.
  rewrite <- Script_typed_ir.dep_pair_t_eq;
    destruct dep_pair_t; [|reflexivity];
    match goal with
    | x : dep_ty_ex_c _ |- _ ⇒ destruct x
    end; simpl.
  rewrite
    <- Script_typed_ir.dep_list_operation_t_eq,
    <- Script_typed_ir.dep_pair_t_eq;
    destruct dep_pair_t; [|reflexivity];
    match goal with
    | x : dep_ty_ex_c _ |- _ ⇒ destruct x
    end; simpl.
  rewrite
    <- Script_tc_context.dep_toplevel_value_eq,
    <- dep_parse_returning_eq;
    destruct show_types, dep_parse_returning;
    try reflexivity.
  all:
    Tactics.destruct_pairs; simpl;
    destruct With_family.to_lambda;
    rewrite <- dep_typecheck_views_eq; try easy;
    destruct dep_typecheck_views; try reflexivity.
  Transparent
    parse_toplevel_aux parse_parameter_ty_and_entrypoints_aux
    parse_storage_ty parse_returning typecheck_views op_coloneq
    Tc_context.toplevel_value op_exclamation location dep_pair_t
    dep_parse_toplevel_aux dep_parse_parameter_ty_and_entrypoints_aux
    dep_parse_storage_ty.
Qed.

The simulation [dep_list_entrypoints_uncarbonated] is valid.

Lemma dep_list_entrypoints_uncarbonated_eq {full}
  (ty : With_family.ty full) entrypoints :
  (let '(prims, map) := dep_list_entrypoints_uncarbonated ty entrypoints in
  (
    prims,
    Entrypoint_repr.Map.(S.map) (fun '(ty , node ) ⇒ (to_ex_ty ty, node)) map
  )) =
  list_entrypoints_uncarbonated (With_family.to_ty ty) entrypoints.
Admitted.

The simulation [dep_comb_witness2] is valid.

Lemma dep_comb_witness2_eq {a} (ty : With_family.ty a) :
  dep_comb_witness2 ty = comb_witness2 (With_family.to_ty ty).
Proof.
  destruct ty; simpl; try reflexivity.
  hauto lq: on.
Qed.

The auxiliary simulation [dep_unparse_data_aux_fuel] is valid.

Fixpoint dep_unparse_data_aux_fuel_eq {t}
  fuel ctxt mode (ty : With_family.ty t) a_value {struct fuel} :
  dep_unparse_data_aux_fuel fuel ctxt mode ty a_value =
  unparse_data_aux ctxt (fuel_to_stack_depth fuel) mode
    (With_family.to_ty ty) (With_family.to_value a_value)

with dep_unparse_code_aux_fuel_eq ctxt fuel mode code {struct fuel} :
  dep_unparse_code_aux_fuel ctxt fuel mode code =
  unparse_code_aux ctxt (fuel_to_stack_depth fuel) mode code

with dep_unparse_items_fuel_eq {k v}
  ctxt fuel mode (kt : With_family.ty k) (vt : With_family.ty v) items
  {struct fuel} :
  dep_unparse_items_fuel ctxt fuel mode kt vt items =
  unparse_items ctxt (fuel_to_stack_depth fuel) mode
    (With_family.to_ty kt) (With_family.to_ty vt) items.
Proof.
Admitted.

The simulation [dep_unparse_data_aux] is valid.

Lemma dep_unparse_data_aux_eq {t}
  ctxt stack_depth mode (ty : With_family.ty t) a_value :
  0 ≤ stack_depth ≤ z_number_10001 →
  dep_unparse_data_aux ctxt stack_depth mode ty a_value =
  unparse_data_aux ctxt stack_depth mode
    (With_family.to_ty ty) (With_family.to_value a_value).
Proof.
  intros.
  unfold dep_unparse_data_aux.
  rewrite dep_unparse_data_aux_fuel_eq.
  now rewrite stack_depth_to_fuel_to_stack_depth.
Qed.

The simulation [dep_unparse_code_aux] is valid.

Lemma dep_unparse_code_aux_eq ctxt stack_depth mode code :
  0 ≤ stack_depth ≤ z_number_10001 →
  dep_unparse_code_aux ctxt stack_depth mode code =
  unparse_code_aux ctxt stack_depth mode code.
Proof.
  intros.
  unfold dep_unparse_code_aux.
  rewrite dep_unparse_code_aux_fuel_eq.
  now rewrite stack_depth_to_fuel_to_stack_depth.
Qed.

The simulation [dep_unparse_items] is valid.

Lemma dep_unparse_items_eq {k v} ctxt stack_depth mode
  (kt : With_family.ty k) (vt : With_family.ty v) items :
  0 ≤ stack_depth ≤ z_number_10001 →
  dep_unparse_items ctxt stack_depth mode kt vt items =
  unparse_items ctxt stack_depth mode
    (With_family.to_ty kt) (With_family.to_ty vt) items.
Proof.
  intros.
  unfold dep_unparse_items.
  rewrite dep_unparse_items_fuel_eq.
  now rewrite stack_depth_to_fuel_to_stack_depth.
Qed.

(* We do not verify the simulation [dep_parse_and_unparse_script_unaccounted]
   and make the lemma [dep_parse_and_unparse_script_unaccounted_eq] for now as
   it is not used in the interpreter. *)

The simulation [dep_pack_data_with_mode] is valid.

Lemma dep_pack_data_with_mode_eq {a} ctxt (ty : With_family.ty a) data mode :
  dep_pack_data_with_mode ctxt ty data mode =
  pack_data_with_mode ctxt
    (With_family.to_ty ty) (With_family.to_value data) mode.
Proof.
  unfold dep_pack_data_with_mode, pack_data_with_mode.
  now rewrite dep_unparse_data_aux_eq by tr_lia.
Qed.

The simulation [dep_hash_data] is valid.

Lemma dep_hash_data_eq {a} ctxt (ty : With_family.ty a) data :
  dep_hash_data ctxt ty data =
  hash_data ctxt (With_family.to_ty ty) (With_family.to_value data).
Proof.
  unfold dep_hash_data, hash_data.
  now rewrite dep_pack_data_with_mode_eq.
Qed.

The simulation [dep_pack_data] is valid.

Lemma dep_pack_data_eq {a}
  (ctxt : Alpha_context.context) (ty : With_family.ty a)
  (data : With_family.ty_to_dep_Set a) :
  dep_pack_data ctxt ty data =
  pack_data ctxt (With_family.to_ty ty) (With_family.to_value data).
Proof.
  apply dep_pack_data_with_mode_eq.
Qed.

The simulation [dep_empty_big_map] is valid.

Lemma dep_empty_big_map_eq {a b : Ty.t}
  (key_type : With_family.ty a) (value_type : With_family.ty b) :
  With_family.to_big_map (dep_empty_big_map key_type value_type) =
  empty_big_map
    (a := Ty.to_Set a) (b := Ty.to_Set b)
    (With_family.to_ty key_type) (With_family.to_ty value_type).
Proof.
  reflexivity.
Qed.

The simulation [dep_big_map_mem] is valid.

Lemma dep_big_map_mem_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (key_value : With_family.ty_to_dep_Set a)
  (big_map : With_family.big_map a b) :
  Script_typed_ir.With_family.Valid.big_map big_map →
  dep_big_map_mem ctxt key_value big_map =
  big_map_mem ctxt (With_family.to_value key_value)
    (With_family.to_big_map big_map).
Proof.
  intros [].
  unfold dep_big_map_mem, big_map_mem.
  rewrite dep_hash_comparable_data_eq by easy.
  simpl.
  destruct hash_comparable_data; simpl; [|reflexivity].
  Tactics.destruct_pairs.
  unfold Script_typed_ir.Big_map_overlay.
  rewrite <- Map.find_map.
  destruct (_.(Map.S.find)); simpl; [|reflexivity].
  Tactics.destruct_pairs.
  now step.
Qed.

The simulation [dep_big_map_get_by_hash] is valid.

Lemma dep_big_map_get_by_hash_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (key_value : Script_expr_hash.t)
  (big_map : With_family.big_map a b) :
  (let ? '(result , ctxt ) := dep_big_map_get_by_hash ctxt key_value big_map in
  return ? (Option.map With_family.to_value result, ctxt)) =
  big_map_get_by_hash (B := Ty.to_Set a) ctxt key_value
    (With_family.to_big_map big_map).
Proof.
  unfold dep_big_map_get_by_hash, big_map_get_by_hash.
  simpl.
  rewrite cast_eval.
  simpl.
  unfold Script_typed_ir.Big_map_overlay.
  rewrite <- Map.find_map.
  destruct (_.(Map.S.find)); simpl.
  { Tactics.destruct_pairs; reflexivity. }
  { destruct big_map; simpl.
    destruct id; simpl; [|reflexivity].
    destruct Alpha_context.Big_map.get_opt; simpl; [|reflexivity].
    Tactics.destruct_pairs.
    step; simpl; [|reflexivity].
    rewrite <- dep_parse_data_aux_eq.
    destruct dep_parse_data_aux; simpl; [|reflexivity].
    hauto lq:on.
  }
Qed.

The simulation [dep_big_map_get] is valid.

Lemma dep_big_map_get_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (key_value : With_family.ty_to_dep_Set a)
  (big_map : With_family.big_map a b) :
  Script_typed_ir.With_family.Valid.big_map big_map →
  (let ? '(result , ctxt ) := dep_big_map_get ctxt key_value big_map in
    return ? (Option.map With_family.to_value result, ctxt)) =
  big_map_get ctxt (With_family.to_value key_value)
    (With_family.to_big_map big_map).
Proof.
  Opaque big_map_get_by_hash.
  intros [].
  unfold dep_big_map_get, big_map_get; simpl.
  rewrite dep_hash_comparable_data_eq by easy.
  destruct hash_comparable_data; simpl; [|reflexivity].
  Tactics.destruct_pairs.
  now rewrite dep_big_map_get_by_hash_eq.
  Transparent big_map_get_by_hash.
Qed.

The simulation [dep_big_map_update_by_hash] is valid.

Lemma dep_big_map_update_by_hash_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (key_hash : Script_expr_hash.t)
  (key_value : With_family.ty_to_dep_Set a)
  (value_value : option (With_family.ty_to_dep_Set b))
  (big_map : With_family.big_map a b) :
  (let ? '(result , ctxt ) :=
    dep_big_map_update_by_hash ctxt key_hash key_value value_value big_map in
  return ? (With_family.to_big_map result, ctxt)) =
  big_map_update_by_hash ctxt key_hash (With_family.to_value key_value)
    (Option.map With_family.to_value value_value)
    (With_family.to_big_map big_map).
Proof.
  unfold dep_big_map_update_by_hash, big_map_update_by_hash.
  simpl.
  rewrite cast_eval.
  unfold With_family.big_map.with_diff,
    With_family.to_big_map, With_family.to_big_map_aux,
    Script_typed_ir.big_map.Big_map.with_diff.
  simpl.
  repeat f_equal; unfold Script_typed_ir.Big_map_overlay.
  { now rewrite <- Map.add_map. }
  { repeat rewrite Map.mem_from_find.
    rewrite <- Map.find_map.
    now destruct (_.(Map.S.find)).
  }
Qed.

The simulation [dep_big_map_update] is valid.

Lemma dep_big_map_update_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (key_value : With_family.ty_to_dep_Set a)
  (value_value : option (With_family.ty_to_dep_Set b))
  (big_map : With_family.big_map a b) :
  Script_typed_ir.With_family.Valid.big_map big_map →
  (let ? '(result , ctxt ) :=
    dep_big_map_update ctxt key_value value_value big_map in
  return ? (With_family.to_big_map result, ctxt)) =
  big_map_update ctxt (With_family.to_value key_value)
    (Option.map With_family.to_value value_value)
    (With_family.to_big_map big_map).
Proof.
  Opaque big_map_update_by_hash dep_big_map_update_by_hash.
  intros [].
  unfold dep_big_map_update, big_map_update.
  simpl.
  rewrite dep_hash_comparable_data_eq by easy.
  destruct hash_comparable_data; simpl; [|reflexivity].
  Tactics.destruct_pairs.
  now rewrite dep_big_map_update_by_hash_eq.
  Transparent big_map_update_by_hash dep_big_map_update_by_hash.
Qed.

The simulation [dep_big_map_get_and_update] is valid.

Lemma dep_big_map_get_and_update_eq {a b : Ty.t}
  (ctxt : Alpha_context.context) (key_value : With_family.ty_to_dep_Set a)
  (value_value : option (With_family.ty_to_dep_Set b))
  (big_map : With_family.big_map a b) :
  Script_typed_ir.With_family.Valid.big_map big_map →
  (let ? '(value , big_map , ctxt ) :=
    dep_big_map_get_and_update ctxt key_value value_value big_map in
  return ? (
    (Option.map With_family.to_value value, With_family.to_big_map big_map),
    ctxt
  )) =
  big_map_get_and_update ctxt (With_family.to_value key_value)
    (Option.map With_family.to_value value_value)
    (With_family.to_big_map big_map).
Proof.
  Opaque big_map_update_by_hash dep_big_map_update_by_hash
    big_map_get_by_hash dep_big_map_get_by_hash.
  intros [].
  unfold dep_big_map_get_and_update, big_map_get_and_update; simpl.
  rewrite dep_hash_comparable_data_eq by easy.
  destruct hash_comparable_data; simpl; [|reflexivity].
  Tactics.destruct_pairs.
  rewrite <- dep_big_map_update_by_hash_eq.
  destruct dep_big_map_update_by_hash; simpl; [|reflexivity].
  Tactics.destruct_pairs.
  simpl.
  rewrite <- dep_big_map_get_by_hash_eq.
  destruct dep_big_map_get_by_hash; simpl; [|reflexivity].
  Tactics.destruct_pairs.
  reflexivity.
  Transparent big_map_update_by_hash dep_big_map_update_by_hash
    big_map_get_by_hash dep_big_map_get_by_hash.
Qed.

The simulation [dep_diff_of_big_map] is valid.

Lemma dep_diff_of_big_map_eq {a b}
  (ctxt : Alpha_context.context) (mode : unparsing_mode) (temporary : bool)
  (ids_to_copy : Alpha_context.Lazy_storage.IdSet.t)
  (big_map : With_family.big_map a b) :
  dep_diff_of_big_map ctxt mode temporary ids_to_copy big_map =
  diff_of_big_map ctxt mode temporary ids_to_copy
    (With_family.to_big_map big_map).
Admitted.

We have a dependent definition `dep_has_lazy_storage` of `has_lazy_storage` and the function for conversion: `to_has_lazy_storage`. We prove backward compatibility with `Simulations` version.

Fixpoint dep_has_lazy_storage_value_eq {t} (ty : With_family.ty t) :
  to_has_lazy_storage (dep_has_lazy_storage_value ty) =
    has_lazy_storage_value (With_family.to_ty ty).
Proof.
  destruct ty eqn:DTY; simpl; try reflexivity;
    try (pose proof (dep_has_lazy_storage_value_eq _ t0_1);
      pose proof (dep_has_lazy_storage_value_eq _ t0_2);
          hauto q: on drew: off);
    pose proof (dep_has_lazy_storage_value_eq _ t0); hauto lq: on.
Qed.

Validity of [has_lazy_storage_Valid.t hls ty] is a relation between [has_lazy_storage] and [With_family.ty _] constructors. [Big_map_f] and [With_family.Big_map_t], [Pair_f] and [With_family.Pair_t], so on and so forth.

Module Has_lazy_storage.
  Module Valid.
    Fixpoint t {a : Ty.t} (has_lazy_storage_value : has_lazy_storage)
      (ty : With_family.ty a) : Prop :=
    match has_lazy_storage_value, ty with
    | Big_map_f, With_family.Big_map_t _ _ _ ⇒ True
    | Sapling_state_f, With_family.Sapling_state_t _ ⇒ True
    | Pair_f hls1 hls2, With_family.Pair_t wty1 wty2 _ _ ⇒
        (t hls1 wty1) ∧ (t hls2 wty2)
    | Union_f hls1 hls2, With_family.Union_t wty1 wty2 _ _⇒
        t hls1 wty1 ∧ t hls2 wty2
    | Option_f hls, With_family.Option_t wty _ _ ⇒
        t hls wty
    | List_f hls, With_family.List_t wty _ ⇒
        t hls wty
    | Map_f hls, With_family.Map_t wty1 wty2 _ ⇒
      t hls wty2
    | False_f, _ ⇒ True
    | _, _ ⇒ False
    end.
  End Valid.
End Has_lazy_storage.

The simulation [dep_fold_lazy_storage] is valid.

Fixpoint dep_fold_lazy_storage_eq
  {a} {acc : Set}
  (f_value :
    Alpha_context.Lazy_storage.IdSet.fold_f (Fold_lazy_storage.result acc))
  (init_value : acc) (ctxt : Alpha_context.context) (ty : With_family.ty a)
  (x_value : With_family.ty_to_dep_Set a) (has_lazy_storage_value : has_lazy_storage) :
  Script_family.Ty.Valid.t a →
  Has_lazy_storage.Valid.t has_lazy_storage_value ty →
  dep_fold_lazy_storage f_value init_value ctxt ty x_value
    has_lazy_storage_value =
  fold_lazy_storage f_value init_value ctxt (With_family.to_ty ty) (With_family.to_value x_value)
    has_lazy_storage_value.
Proof.
  intros H_ty H_has_lazy_storage.
  destruct has_lazy_storage_value, ty; try (inversion H || simpl; easy).
  { grep Big_map_f. simpl. now rewrite cast_eval. }
  { grep Sapling_state_f. simpl. now rewrite cast_eval. }
  { grep Pair_f.
    cbn. rewrite_cast_exists. step_let?.
    destruct x_value. rewrite dep_fold_lazy_storage_eq; [|apply H_ty|hauto lq:on].
    step; try easy. do 2 step; [|reflexivity].
    rewrite dep_fold_lazy_storage_eq; [reflexivity|apply H_ty|hauto lq:on]. }
  { grep Union_f.
    cbn. rewrite_cast_exists. step_let?.
    destruct x_value; rewrite dep_fold_lazy_storage_eq; try (easy||hauto lq:on). }
  { grep Option_f.
    cbn. rewrite_cast_exists. step_let?.
    destruct x_value; [|easy].
    now rewrite dep_fold_lazy_storage_eq. }
  { grep List_f.
    cbn. rewrite_cast_exists. step_let?.
    simpl. destruct x_value; simpl.
    match goal with
    | |- List.fold_left_e ?f1' _ _ = List.fold_left_e ?f2' _ _ ⇒
        set (f1 := f1'); set (f2 := f2')
    end.
    assert (H_fns_eq : ∀ acc value, f1 acc value = f2 acc (With_family.to_value value)).
    { intros. subst f1. subst f2. simpl.
      destruct acc0, r; [|easy]. rewrite dep_fold_lazy_storage_eq; try easy.
    }
    destruct elements; [reflexivity|].
    assert (Hfold_cons :
      List.fold_left_e
        f2
        (Fold_lazy_storage.Ok init_value, t1)
        (List.map With_family.to_value (t2 :: elements)) =
      List.fold_left_e
        (fun p x_value ⇒ f2 p (With_family.to_value x_value) )
        (Fold_lazy_storage.Ok init_value, t1)
        (t2 :: elements)) by now rewrite List.fold_left_e_map_eq.
    rewrite Hfold_cons.
    match goal with
    | |- List.fold_left_e _ _ _ = List.fold_left_e ?f3' _ _ ⇒
        set (f3 := f3')
    end.
    assert (Hf1f3_eq : f1 = f3).
    {
      do 2
        (apply FunctionalExtensionality.functional_extensionality; intro).
      rewrite H_fns_eq.
      subst f3. subst f2.
      now destruct x. }
    now rewrite Hf1f3_eq.
  }
  { grep Map_f.
    cbn. rewrite_cast_exists.
    step_let?.
    match goal with
    | |- ?fold' ?f1' _ ?acc1' = ?fold'' ?f2' ?map ?acc1' ⇒
        set (f1 := f1'); set (f2 := f2');
        set (acc' := acc1'); set (map' := map)
    end.
    simpl in H_ty.
    rewrite (Script_map.dep_fold_eq f1 f2 x_value); [reflexivity| |hauto lq: on].
    now destruct H_ty as [H_ty _]. }
Qed.

The simulation [dep_extract_lazy_storage_updates] is valid.

Fixpoint dep_extract_lazy_storage_updates_aux_eq {a}
  (ctxt : Alpha_context.context) (mode : unparsing_mode) (temporary : bool)
  (ids_to_copy : Alpha_context.Lazy_storage.IdSet.t)
  (acc_value : Alpha_context.Lazy_storage.diffs) (ty : With_family.ty a)
  (x_value : With_family.ty_to_dep_Set a)
  (has_lazy_storage_value : has_lazy_storage)
  {struct has_lazy_storage_value} :
  Has_lazy_storage.Valid.t has_lazy_storage_value ty →
  (let ? '(ctxt , value , ids , diff ) :=
     dep_extract_lazy_storage_updates_aux ctxt mode temporary ids_to_copy acc_value
       ty x_value has_lazy_storage_value in
   return ? (ctxt, With_family.to_value value, ids, diff)) =
  extract_lazy_storage_updates_aux ctxt mode temporary ids_to_copy acc_value
    (With_family.to_ty ty) (With_family.to_value x_value) has_lazy_storage_value.
Proof.
  simpl; intros H_hls_valid.
  destruct has_lazy_storage_value;
  try (grep False_f; simpl; consume_gas;
       now rewrite cast_eval);
  try solve [simpl; consume_gas; destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end)];
    remaining_goals 7.
  { grep Big_map_f.
    destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end).
    unfold dep_extract_lazy_storage_updates_aux,
      extract_lazy_storage_updates_aux.
    consume_gas.
    do 2 rewrite cast_eval.
    set (big_map := With_family.to_big_map_aux _ _ _).
    change big_map with (With_family.to_big_map x_value).
    rewrite <- dep_diff_of_big_map_eq.
    set (dep_diff_of_big_map' := dep_diff_of_big_map _ _ _ _ _).
    ez destruct dep_diff_of_big_map'; simpl.
    hauto l: on drew: off. }
  { grep Sapling_state_f.
    destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end).
    unfold dep_extract_lazy_storage_updates_aux,
      extract_lazy_storage_updates_aux.
    consume_gas.
    do 2 rewrite cast_eval.
    destruct (diff_of_sapling_state _ _ _ _); trivial; simpl.
    sauto lq: on rew: off. }
  { grep Pair_f.
    destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end).
    destruct x_value; simpl.
    consume_gas.
    cbn in *; rewrite_cast_exists; rewrite cast_eval.
    ez rewrite <- dep_extract_lazy_storage_updates_aux_eq.
    destruct H_hls_valid as [H_hls_valid1 H_hls_valid2].
    ez destruct (dep_extract_lazy_storage_updates_aux
      _ _ _ _ _ _ _ has_lazy_storage_value1).
    do 3 step; simpl.
    ez rewrite <- dep_extract_lazy_storage_updates_aux_eq.
    ez destruct (dep_extract_lazy_storage_updates_aux
      _ _ _ _ _ _ _ _).
    hauto l: on. }
  { grep Union_f. destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end). simpl.
    consume_gas.
    destruct H_hls_valid as [H_hls_valid1 H_hls_valid2].
    cbn; rewrite_cast_exists; rewrite cast_eval.
    destruct x_value; simpl;
      rewrite <- dep_extract_lazy_storage_updates_aux_eq; try assumption;
      destruct (dep_extract_lazy_storage_updates_aux _ _ _ _ _ _);
      simpl; try reflexivity; ecrush. }
  { grep Option_f. destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end). simpl.
    consume_gas.
    cbn in ×. rewrite_cast_exists. rewrite cast_eval.
    ez destruct x_value.
    ez rewrite <- dep_extract_lazy_storage_updates_aux_eq.
    ez destruct (dep_extract_lazy_storage_updates_aux _ _ _ _ _ _ _ _).
    now do 3 step. }
  { grep List_f. destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end). simpl.
    consume_gas.
    cbn; rewrite_cast_exists; rewrite cast_eval.
    do 2 match goal with
    | |- context [fold_left_es ?a' ?b' ?c'] ⇒
        let f := fresh "f" in
        let init := fresh "init" in
        let elements := fresh "elements" in
        set (f := a');
        set (init := b');
        set (elements := c');
        symmetry
    end.
    match goal with
    | |- ?nested_let = _ ⇒
        assert (H_nested_let_eq : nested_let =
          let ? '(ctxt , value , ids , acc )
            := fold_left_es f init elements in
          return ? (ctxt, {|
             Script_typed_ir.boxed_list.elements :=
               rev (List.map With_family.to_value
                 value.(Script_typed_ir.boxed_list.elements));
             Script_typed_ir.boxed_list.length :=
               value.(Script_typed_ir.boxed_list.length); |},
             ids, acc)) by admit
    end.
    rewrite H_nested_let_eq; clear H_nested_let_eq; simpl.
    simpl in × |- .
    move elements0 before elements.
    move init0 before init.
    subst elements0.
    rewrite List.fold_left_es_map_eq.
    match goal with
    | |- context [fold_left_es ?f' init0] ⇒
        let f := fresh "f" in
        set (f := f')
    end.
    (* @TODO : I didn't try to prove this axiom so I will not
               move it to the List module yet to prevent someone
               of using it. *)
    assert (fold_left_es_eq :
       ∀ {A B C D T : Set}
       (f1 : A → B → result A T)
       (f2 : C → D → result C T)
       (a : A) (c : C)
       (bl : list B) (dl : list D)
       (c_to_a : C → A),
       (∀ (a : A) (b : B) (c : C) (d : D),
         f1 a b = let ? c := f2 c d in return ? c_to_a c) →
       fold_left_es f1 a bl =
       let ? c' := fold_left_es f2 c dl in
       return ? c_to_a c') by admit.
    admit.
  }
  { grep Map_f.
    destruct ty eqn:?;
    simpl in H_hls_valid; try (match goal with
    | H : False |- _ ⇒ solve [destruct H]
    end). simpl.
    consume_gas.
    cbn; rewrite_cast_exists. rewrite cast_eval; simpl.
    do 2 match goal with
    | |- context [fold_left_es ?a' ?b' ?c'] ⇒
        let f := fresh "f" in
        let init := fresh "init" in
        let elements := fresh "elements" in
        set (f := a');
        set (init := b');
        set (elements := c');
        symmetry
    end.
    match goal with
    | |- ?nested_let = _ ⇒
        assert (H_let_eq : nested_let =
          let ? '(ctxt , dep_map , ids , diffs ) :=
            fold_left_es f init elements in
          return ? (ctxt, With_family.to_map_aux With_family.to_value dep_map,
          ids, diffs)) by admit
    end.
    rewrite H_let_eq.
    admit. }
Admitted.

The simulation [dep_extract_lazy_storage_updates] is valid.

Lemma dep_extract_lazy_storage_updates_eq {a}
  (ctxt : Alpha_context.context) (mode : unparsing_mode) (temporary : bool)
  (ids_to_copy : Alpha_context.Lazy_storage.IdSet.t)
  (acc_value : Alpha_context.Lazy_storage.diffs) (ty : With_family.ty a)
  (x_value : With_family.ty_to_dep_Set a) :
  let hls := has_lazy_storage_value (With_family.to_ty ty) in
  Has_lazy_storage.Valid.t hls ty →
  (let ? '(ctxt , value , ids , diff ) :=
     dep_extract_lazy_storage_updates ctxt mode temporary ids_to_copy acc_value
       ty x_value in
   return ? (ctxt, With_family.to_value value, ids, diff)) =
  extract_lazy_storage_updates ctxt mode temporary ids_to_copy acc_value
    (With_family.to_ty ty) (With_family.to_value x_value).
Proof.
  simpl; intros H_hls_valid.
  unfold dep_extract_lazy_storage_updates,
    extract_lazy_storage_updates.
  rewrite <- dep_extract_lazy_storage_updates_aux_eq; [|easy].
  now rewrite dep_has_lazy_storage_value_eq.
Qed.

Module Fold_lazy_storage.
  Module Valid.

The result of [fold_lazy_storage] is *invalid* if has the shape [Pervasives.OK (Fold_lazy_storage.Error, _)], otherwise is valid. We need this to eliminate [unrechable_gadt_branch] inside [fold_lazy_storage]

    Definition t {A B : Set} (fls : M ? (Fold_lazy_storage.result A × B )) :=
      match fls with
      | Pervasives.Ok (Fold_lazy_storage.Error, _) ⇒ False
      | _ ⇒ True
      end.

The result of [Alpha_context.Lazy_storage.IdSet.fold_f] is OK when has the shape [Fold_lazy_storage.Ok _]. We need this to eliminate [unreachable_gadt_branch] inside [fold_f] function

    Definition is_ok {A : Set} (fls : (Fold_lazy_storage.result A)) :=
      match fls with
      | Fold_lazy_storage.Ok _ ⇒ True
      | Fold_lazy_storage.Error ⇒ False
      end.
  End Valid.
End Fold_lazy_storage.

[fold_lazy_storage] never returns invalid results

Fixpoint dep_fold_lazy_storage_is_valid
  {a} {acc : Set}
  (f_value :
    Alpha_context.Lazy_storage.IdSet.fold_f (Fold_lazy_storage.result acc))
  (init_value : acc) (ctxt : Alpha_context.context) (ty : With_family.ty a)
  (x_value : With_family.ty_to_dep_Set a)
  (has_lazy_storage_value : has_lazy_storage) :
  Has_lazy_storage.Valid.t has_lazy_storage_value ty →
  (* [f_value] returns [Fold_lazy_storage.Ok] *)
  (∀ {B : Set} (a : Alpha_context.Lazy_storage.Kind.t)
    (b : B)
    (acc' : acc),
    Fold_lazy_storage.Valid.is_ok
      (f_value.(Alpha_context.Lazy_storage.IdSet.fold_f.f)
         a b (Fold_lazy_storage.Ok acc'))) →
  Fold_lazy_storage.Valid.t
    (dep_fold_lazy_storage f_value init_value ctxt ty x_value
       has_lazy_storage_value).
Proof.
  intros H_hls_valid H_f_is_ok.
  destruct has_lazy_storage_value, ty; simpl in *;
    try (match goal with
    | H : False |- _ ⇒ destruct H
    | |- Fold_lazy_storage.Valid.t
        (let ? ' _ := Alpha_context.Gas.consume _ _ in
         return ? (Fold_lazy_storage.Ok _, _)) ⇒ step; trivial
    end);
    remaining_goals 7.
  all :
    try (
    do 4 step; simpl; trivial; step; simpl; trivial;
    match goal with
    | |- match ?f ?a ?b ?c with _ ⇒ _ end ⇒
        let t := type of b in
        specialize (H_f_is_ok t a b); apply H_f_is_ok
    end).
  { step_let?. destruct x_value. step; try easy;
    destruct p eqn:?, r eqn:?; try easy.
    { apply dep_fold_lazy_storage_is_valid; easy. }
    { match goal with
      | H : dep_fold_lazy_storage ?f_value ?init_value ?t0
        ?ty1 ?t3 ?has_lazy_storage_value1 =
        Pervasives.Ok (Fold_lazy_storage.Error, _) |- _ ⇒
        specialize (dep_fold_lazy_storage_is_valid _ _
          f_value init_value t0 ty1 t3 has_lazy_storage_value1)
      end;
      rewrite Heqt5 in dep_fold_lazy_storage_is_valid;
      destruct H_hls_valid as [H_hls_valid _];
      now apply (dep_fold_lazy_storage_is_valid H_hls_valid). } }
  all : try (apply dep_fold_lazy_storage_is_valid; easy).
  all : try (do 2 step; simpl; trivial; apply dep_fold_lazy_storage_is_valid; easy).
  (* @TODOs *)
  { step_let?.
    match goal with
    | |- context [fold_left_e ?f' ?acc' _] ⇒
        set (f := f'); set (acc_arg := acc')
    end.
    destruct x_value; simpl.
    assert (TODO_fold_left_e :
      Fold_lazy_storage.Valid.t (
        fold_left_e f acc_arg elements)) by admit.
    apply TODO_fold_left_e. }
  { destruct x_value.
    { step_let?.
      match goal with
      | |- context [Script_map.dep_fold ?f' ?x' ?acc'] ⇒
          assert (TODO_Script_map_dep_fold :
            x' = [] →
           Script_map.dep_fold f' x' acc' = acc') by admit
      end.
      now rewrite TODO_Script_map_dep_fold. }
    { step_let?.
      match goal with
      | |- context [Script_map.dep_fold ?f ?x ?acc] ⇒
          assert (TODO_Script_dep_fold :
            Fold_lazy_storage.Valid.t (Script_map.dep_fold f x acc)) by admit
      end.
      apply TODO_Script_dep_fold. } }
  all : remaining_goals 0.
Admitted.

(* @TODO *)

[fold_lazy_storage f1 a b c d] is equal to [fold_lazy_storage f2 a b c d] if [f1] is pointwise equal to [f2] assumming that [Fold_lazy_storage.ok d] holds.

Lemma dep_fold_lazy_storage_ext_eq {a} {acc_t : Set}
  (r1 r2 : Alpha_context.Lazy_storage.IdSet.fold_f (Fold_lazy_storage.result acc_t))
  (acc : acc_t) (ctxt : Alpha_context.context) (script_ty : _) (x : With_family.ty_to_dep_Set a)
  (hls : has_lazy_storage) :
  let f1 := r1.(@Alpha_context.Lazy_storage.IdSet.fold_f.f (Fold_lazy_storage.result acc_t)) in
  let f2 := r2.(@Alpha_context.Lazy_storage.IdSet.fold_f.f (Fold_lazy_storage.result acc_t)) in
  (∀ a b c d,
    Fold_lazy_storage.Valid.is_ok d →
    f1 a b c d = f2 a b c d) →
  dep_fold_lazy_storage r1 acc ctxt script_ty x hls = dep_fold_lazy_storage r2 acc ctxt script_ty x hls.
Proof.
Admitted.

Simulation of [collect_lazy_storage] is valid

Definition dep_collect_lazy_storage_eq
  {a} (ctxt : Alpha_context.context) (ty : With_family.ty a)
  (x_value : With_family.ty_to_dep_Set a) :
  Script_family.Ty.Valid.t a →
  Has_lazy_storage.Valid.t (has_lazy_storage_value (With_family.to_ty ty)) ty →
  dep_collect_lazy_storage ctxt ty x_value =
  collect_lazy_storage ctxt (With_family.to_ty ty) (With_family.to_value x_value).
Proof.
  intros H_ty H_hls.
  unfold dep_collect_lazy_storage, collect_lazy_storage;
  rewrite <- dep_fold_lazy_storage_eq;
  destruct ty; simpl;
    try (destruct (Alpha_context.Gas.consume _ _); simpl);
    try easy.
  all : try (step_let?; destruct p, r; [easy|sauto q:on]).
  all : do 2 match goal with
    | |- context [dep_fold_lazy_storage ?a ?b ?c ?d ?e ?f] ⇒
      let arg := fresh "arg" in set (arg := a);
      let arg := fresh "arg" in set (arg := b);
      let arg := fresh "arg" in set (arg := c);
      let arg := fresh "arg" in set (arg := d);
      let arg := fresh "arg" in set (arg := e);
      let arg := fresh "arg" in set (arg := f);
      symmetry
    end.
  all : rewrite dep_fold_lazy_storage_ext_eq with (r2 := arg5); [|
    intros ? ? ? ? H_fls_ok; subst arg arg5; simpl; do 2 f_equal;
    step; [reflexivity|destruct H_fls_ok]].
  all : destruct (dep_fold_lazy_storage _ _ _ _ _ _) eqn:?; simpl; try easy;
    do 2 step; [reflexivity|];
    match goal with
    | H' : dep_fold_lazy_storage ?a ?b ?c ?d ?e ?f = _ _ |- _ ⇒
      let H := fresh "H" in
      pose proof (dep_fold_lazy_storage_is_valid a b c d e f) as H;
      try (rewrite H' in H; destruct H; easy)
    end.
Qed.

The simulation [dep_extract_lazy_storage_diff] is valid.

Lemma dep_extract_lazy_storage_diff_eq {a}
  (ctxt : Alpha_context.context) (mode : unparsing_mode) (temporary : bool)
  (to_duplicate : Alpha_context.Lazy_storage.IdSet.t)
  (to_update : Alpha_context.Lazy_storage.IdSet.t) (ty : With_family.ty a)
  (v_value : With_family.ty_to_dep_Set a) :
  Has_lazy_storage.Valid.t (has_lazy_storage_value (With_family.to_ty ty)) ty →
  (let ? '(value , diff , ctxt ) :=
    dep_extract_lazy_storage_diff ctxt mode temporary to_duplicate to_update ty
      v_value in
  return ? (With_family.to_value value, diff, ctxt)) =
  extract_lazy_storage_diff ctxt mode temporary to_duplicate to_update
    (With_family.to_ty ty) (With_family.to_value v_value).
Proof.
  intros H_hls_valid.
  unfold dep_extract_lazy_storage_diff, extract_lazy_storage_diff.
  ez rewrite <- dep_extract_lazy_storage_updates_eq.
  set (extract := dep_extract_lazy_storage_updates _ _ _ _ _ _ _).
  ez destruct extract eqn:?H_extract.
  hauto drew: off.
Qed.

The simulation [dep_parse_data] is valid.

Lemma dep_parse_data_eq {a}
  type_logger_value ctxt legacy allow_forged (ty : With_family.ty a) expr :
  (let ? '(result , ctxt ) :=
    dep_parse_data type_logger_value ctxt legacy allow_forged ty expr in
  return ? (With_family.to_value result, ctxt)) =
  parse_data type_logger_value ctxt legacy allow_forged (With_family.to_ty ty)
    expr.
Proof.
  unfold dep_parse_data, parse_data.
  now rewrite dep_parse_data_aux_eq.
Qed.

The simulation [dep_parse_instr] is valid.

Lemma dep_parse_instr_eq {s}
  (type_logger_value : option type_logger) (tc_context_value : dep_tc_context)
  (ctxt : Alpha_context.context) (legacy : bool)
  (script_instr : Alpha_context.Script.node)
  (stack_ty : With_family.stack_ty s) :
  Error_monad.Eq.t
    (fun '(dep_result , dep_ctxt ) '(result , ctxt ) ⇒
      Eq_judgement.t dep_result result ∧ dep_ctxt = ctxt
    )
    (dep_parse_instr
      type_logger_value tc_context_value ctxt legacy script_instr stack_ty)
    (parse_instr
      type_logger_value (to_tc_context tc_context_value) ctxt legacy script_instr
      (With_family.to_stack_ty stack_ty)).
Proof.
  unfold dep_parse_instr, parse_instr.
  apply dep_parse_instr_aux_eq.
Qed.

The simulation [dep_unparse_data] is valid.

Lemma dep_unparse_data_eq {t}
  ctxt mode (ty : With_family.ty t) a_value :
  dep_unparse_data ctxt mode ty a_value =
  unparse_data ctxt mode
    (With_family.to_ty ty) (With_family.to_value a_value).
Proof.
  unfold dep_unparse_data.
  apply dep_unparse_data_aux_eq.
  hecrush.
Qed.

The simulation [dep_unparse_code] is valid.

Lemma dep_unparse_code_eq {A : Set} ctxt mode code :
  dep_unparse_code ctxt mode code =
  @unparse_code A ctxt mode code.
Proof.
  unfold dep_unparse_code.
  unfold unparse_code.
  f_equal.
  apply FunctionalExtensionality.functional_extensionality_dep; intro.
  destruct x.
  apply dep_unparse_code_aux_eq.
  hecrush.
Qed.

The simulation [dep_parse_contract] is valid.

Lemma dep_parse_contract_eq {a}
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (arg_ty : With_family.ty a) (contract : Alpha_context.Destination.t)
  (entrypoint : Alpha_context.Entrypoint.t) :
  0 ≤ 0 +i 1 + 1 ≤ z_number_10001 →
  Script_typed_ir.With_family.Valid.ty arg_ty →
  Script_typed_ir.With_family.is_Comparable arg_ty →
  (let ? '(ctxt , result ) :=
    dep_parse_contract ctxt loc_value arg_ty contract entrypoint in
  return ? (ctxt, With_family.to_typed_contract result)) =
  parse_contract ctxt loc_value (With_family.to_ty arg_ty) contract entrypoint.
Proof.
  intros H1 H2 H3.
  simpl.
  unfold dep_parse_contract, parse_contract.
  change 0 with (fuel_to_stack_depth (Z.to_nat z_number_10001)).
  rewrite dep_parse_contract_aux_eq; [reflexivity|tr_lia|trivial..].
Qed.

The simulation [dep_parse_toplevel] is valid.

Lemma dep_parse_toplevel_eq
  (ctxt : Alpha_context.t) (legacy : bool)
  (toplevel_value : Alpha_context.Script.expr) :
  (let ? '(result , ctxt ) :=
    dep_parse_toplevel ctxt legacy toplevel_value in
  return ? (to_toplevel result, ctxt)) =
  parse_toplevel ctxt legacy (toplevel_value).
Proof.
  unfold dep_parse_toplevel, parse_toplevel.
  destruct (Alpha_context.Global_constants_storage.expand _ _); [|easy].
  simpl. destruct p.
  now rewrite dep_parse_toplevel_aux_eq.
Qed.

The simulation [dep_parse_comparable_ty] is valid.

Lemma dep_parse_comparable_ty_eq ctxt node_value :
  (let ? '(result , ctxt ) := dep_parse_comparable_ty ctxt node_value in
  return ? (to_ex_comparable_ty result, ctxt)) =
  parse_comparable_ty ctxt node_value.
Proof.
  unfold dep_parse_comparable_ty.
  now rewrite dep_parse_comparable_ty_aux_eq by tr_lia.
Qed.

The simulation [dep_parse_big_map_value_ty] is valid.

Lemma dep_parse_big_map_value_ty_eq ctxt