🍬 Script_interpreter.v

Proofs

See code, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_interpreter.

Require TezosOfOCaml.Proto_alpha.Proofs.Script_interpreter_defs.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_map.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_set.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.
Require TezosOfOCaml.Proto_alpha.Simulations.Script_interpreter.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_typed_ir.

This [Opaque] seems to be necessary to terminate the evaluation.

Opaque Local_gas_counter.local_gas_counter_and_outdated_context.

This [Opaque] is mainly to clarify the output as the details of these functions are not really important.

Opaque Script_interpreter_defs.consume_instr
  Script_interpreter_defs.dep_consume_instr
  Script_interpreter_defs.consume_control.

Helper tactic.

Ltac dep_eq_case :=
  simpl;
  (
    try (
      match goal with
      | |- context[
          Script_interpreter_defs.dep_consume_instr _ _ (?accu, ?stack)
        ] ⇒
          rewrite (Script_interpreter_defs.dep_consume_instr_eq _ _ accu stack)
      end;
      simpl;
      destruct Script_interpreter_defs.consume_instr in |- ×
    );
    try destruct (Script_interpreter_defs.consume_control _ _)
  ); [|discriminate];
  cbn in *;
  try rewrite cast_eval;
  try rewrite_cast_exists.

Verify for our definition [dep_step] is equivalent to the original function [step]. For unknown reasons, disabling the guard checking is needed. Maybe because of local recursive functions in the [step] function.

#[bypass_check(guard)]
Fixpoint dep_step_eq {s t f}
  (fuel : nat)
  (g_value :
    Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  (gas : Local_gas_counter.local_gas_counter)
  (i_value : With_family.kinstr s t)
  (ks : With_family.continuation t f)
  (accu : With_family.stack_ty_to_dep_Set_head s)
  (stack : With_family.stack_ty_to_dep_Set_tail s)
  (dep_output_accu_stack : With_family.stack_ty_to_dep_Set f)
  (output_accu : Stack_ty.to_Set_head f)
  (output_stack : Stack_ty.to_Set_tail f)
  (dep_output_ctxt output_ctxt : Local_gas_counter.outdated_context)
  (dep_output_gas output_gas : Local_gas_counter.local_gas_counter)
  {struct fuel} :
  Script_interpreter.dep_step
    fuel g_value gas i_value ks (accu, stack) =
    Pervasives.Ok (
      dep_output_accu_stack,
      dep_output_ctxt,
      dep_output_gas
    ) →
  Script_interpreter.step
    g_value gas
      (With_family.to_kinstr i_value)
      (With_family.to_continuation ks)
      (With_family.to_stack_value_head accu)
      (With_family.to_stack_value_tail stack) =
    Pervasives.Ok (
      output_accu,
      output_stack,
      output_ctxt,
      output_gas
    ) →
  With_family.to_stack_value dep_output_accu_stack =
  (output_accu, output_stack)

with dep_next_eq {s f}
  (fuel : nat)
  (g_value :
    Local_gas_counter.outdated_context × Script_typed_ir.step_constants)
  (gas : Local_gas_counter.local_gas_counter)
  (ks : With_family.continuation s f)
  (accu : With_family.stack_ty_to_dep_Set_head s)
  (stack : With_family.stack_ty_to_dep_Set_tail s)
  (dep_output_accu_stack : With_family.stack_ty_to_dep_Set f)
  (output_accu : Stack_ty.to_Set_head f)
  (output_stack : Stack_ty.to_Set_tail f)
  (dep_output_ctxt output_ctxt : Local_gas_counter.outdated_context)
  (dep_output_gas output_gas : Local_gas_counter.local_gas_counter)
  {struct fuel} :
  Script_interpreter.dep_next
    fuel g_value gas ks (accu, stack) =
    Pervasives.Ok (
      dep_output_accu_stack,
      dep_output_ctxt,
      dep_output_gas
    ) →
  Script_interpreter.next
    g_value gas
    (With_family.to_continuation ks)
    (With_family.to_stack_value_head accu)
    (With_family.to_stack_value_tail stack) =
    Pervasives.Ok (
      output_accu,
      output_stack,
      output_ctxt,
      output_gas
    ) →
    With_family.to_stack_value dep_output_accu_stack =
    (output_accu, output_stack).
Proof.
{ destruct fuel, g_value, gas; [discriminate|]; dep_destruct i_value.
  { grep @With_family.IDrop.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IDup.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.ISwap.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IConst.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.ICons_pair.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ICar.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ICdr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IUnpair.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ICons_some.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.ICons_none.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set b))
    end.
    apply dep_step_eq.
  }
  { grep @With_family.IIf_none.
    dep_eq_case.
    step;
      simpl in *; Tactics.destruct_pairs;
      apply dep_step_eq.
  }
  { grep @With_family.IOpt_map.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_2 (T := T)
        (E1 := Ty.to_Set a) (E2 := Ty.to_Set b))
    end.
    step; apply dep_step_eq.
  }
  { grep @With_family.ICons_left.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set b))
    end.
    apply dep_step_eq.
  }
  { grep @With_family.ICons_right.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set a))
    end.
    apply dep_step_eq.
  }
  { grep @With_family.IIf_left.
    dep_eq_case.
    step; apply dep_step_eq.
  }
  { grep @With_family.ICons_list.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INil.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set b))
    end.
    apply dep_step_eq.
  }
  { grep @With_family.IIf_cons.
    dep_eq_case.
    step;
      simpl in *; Tactics.destruct_pairs;
      apply dep_step_eq.
  }
  { grep @With_family.IList_map.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_4 (T := T)
        (E1 := Stack_ty.to_Set_head s)
        (E2 := Stack_ty.to_Set_tail s)
        (E3 := Ty.to_Set a)
        (E4 := Ty.to_Set b)
      )
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_next_eq.
  }
  { grep @With_family.IList_iter.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_next_eq.
  }
  { grep @With_family.IList_size.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.IEmpty_set.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set b))
    end.
    rewrite <- Script_set.dep_empty_eq by admit. (* is comparable *)
    apply dep_step_eq.
  }
  { grep @With_family.ISet_iter.
    dep_eq_case.
    admit.
  }
  { grep @With_family.ISet_mem.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISet_update.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    admit.
  }
  { grep @With_family.ISet_size.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IEmpty_map.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_2 (T := T)
        (E1 := Ty.to_Set b) (E2 := Ty.to_Set c))
    end.
    rewrite <- Script_map.dep_empty_eq by admit. (* is comparable *)
    apply dep_step_eq.
  }
  { grep @With_family.IMap_map.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_5 (T := T) (E5 := Ty.to_Set c))
    end.
    erewrite Script_map.dep_fold_eq by admit.
    epose proof Script_map.dep_empty_from_eq as H_empty_from.
    unfold With_family.to_map in H_empty_from.
    rewrite <- H_empty_from.
    admit.
  }
  { grep @With_family.IMap_iter.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IMap_mem.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    rewrite Script_map.dep_mem_eq.
    apply dep_step_eq.
  }
  { grep @With_family.IMap_get.
    dep_eq_case.
    epose proof Script_map.dep_get_eq as H_mem.
    unfold With_family.to_map in H_mem.
    rewrite <- H_mem.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMap_update.
    dep_eq_case.
    epose proof Script_map.dep_update_eq as H_update.
    unfold With_family.to_map, Option.map in H_update.
    rewrite <- H_update.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMap_get_and_update.
    dep_eq_case.
    epose proof Script_map.dep_update_eq as H_update.
    unfold With_family.to_map, Option.map in H_update.
    rewrite <- H_update.
    epose proof Script_map.dep_get_eq as H_get.
    unfold With_family.to_map in H_get.
    rewrite <- H_get.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMap_size.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IEmpty_big_map.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_2 (T := T)
        (E1 := Ty.to_Set b) (E2 := Ty.to_Set c))
    end.
    admit.
  }
  { grep @With_family.IBig_map_mem.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    admit.
  }
  { grep @With_family.IBig_map_get.
    dep_eq_case.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IBig_map_update.
    dep_eq_case.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IBig_map_get_and_update.
    dep_eq_case.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IConcat_string.
    dep_eq_case.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IConcat_string_pair.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISlice_string.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    repeat step; simpl in ×.
    all: try apply dep_step_eq.
    all: admit.
  }
  { grep @With_family.IString_size.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IConcat_bytes.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IConcat_bytes_pair.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISlice_bytes.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    step; admit.
  }
  { grep @With_family.IBytes_size.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_seconds_to_timestamp.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_timestamp_to_seconds.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISub_timestamp_seconds.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IDiff_timestamps.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_tez.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    simpl; step; simpl; [|discriminate].
    apply dep_step_eq.
  }
  { grep @With_family.ISub_tez.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    unfold Alpha_context.Tez.sub_opt.
    destruct_all Tez_repr.t; simpl.
    destruct (_ <=? _); apply dep_step_eq.
  }
  { grep @With_family.ISub_tez_legacy.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    simpl; step; simpl; [|discriminate].
    apply dep_step_eq.
  }
  { grep @With_family.IMul_teznat.
    dep_eq_case.
    (* match goal with
    | |- context[cast_exists ?T ?e] =>
      erewrite (cast_exists_eval_1 (T := T)
        (E1 := Stack_ty.to_Set s)
        (x := e)
      )
    end. *)
    admit.
  }
  { grep @With_family.IMul_nattez.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IEdiv_teznat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct_all Script_int_repr.num; simpl.
    destruct ediv_rem, Script_int_repr.to_int64.
    all: admit.
  }
  { grep @With_family.IEdiv_tez.
    dep_eq_case.
    repeat step; simpl in *;
    Tactics.destruct_pairs;
    try apply dep_step_eq.
    (* TODO: fails for 2/4 cases *)
    all: admit.
  }
  { grep @With_family.IOr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAnd.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IXor.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct_all bool; simpl; apply dep_step_eq.
  }
  { grep @With_family.INot.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.IIs_nat.
    dep_eq_case.
    destruct Script_int_repr.is_nat; apply dep_step_eq.
  }
  { grep @With_family.INeg.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.IAbs_int.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.IInt_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct_all Script_int_repr.num; simpl.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_int.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISub_int.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_int.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IEdiv_int.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct Script_int_repr.ediv;
      simpl in *; Tactics.destruct_pairs;
      apply dep_step_eq.
  }
  { grep @With_family.IEdiv_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct Script_int_repr.ediv_n;
      simpl in *; Tactics.destruct_pairs;
      apply dep_step_eq.
  }
  { grep @With_family.ILsl_nat.
    dep_eq_case.
    admit.
  }
  { grep @With_family.ILsr_nat.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IOr_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAnd_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAnd_int_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IXor_nat.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INot_int.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IIf.
    dep_eq_case.
    repeat step;
      simpl in *; Tactics.destruct_pairs;
      apply dep_step_eq.
  }
  { grep @With_family.ILoop.
    dep_eq_case.
    apply dep_next_eq.
  }
  { grep @With_family.ILoop_left.
    dep_eq_case.
    apply dep_next_eq.
  }
  { grep @With_family.IDip.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IExec.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    match goal with
    | code : With_family.kdescr.skeleton _ _ _ _ |- _ ⇒
      destruct code; simpl
    end.
    apply dep_step_eq.
  }
  { grep @With_family.IApply.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    rewrite <- Script_interpreter_defs.dep_apply_eq.
    destruct Script_interpreter_defs.dep_apply; [|discriminate].
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ILambda.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.IFailwith.
    dep_eq_case.
    destruct trace_value; simpl; Tactics.destruct_pairs; discriminate.
  }
  { grep @With_family.ICompare.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    rewrite <- Script_comparable.dep_compare_comparable_eq by admit.
    apply dep_step_eq.
  }
  { grep @With_family.IEq.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INeq.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ILt.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IGt.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ILe.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IGe.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAddress.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct_all Script_typed_ir.typed_contract.
    step; simpl.
    apply dep_step_eq.
  }
  { grep @With_family.IContract.
    dep_eq_case.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IView.
    dep_eq_case.
    admit.
  }
  { grep @With_family.ITransfer_tokens.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IImplicit_account.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ICreate_contract.
    dep_eq_case.
    admit.
  }
  { grep @With_family.ISet_delegate.
    dep_eq_case.
    destruct Alpha_context.fresh_internal_nonce; simpl; [|discriminate].
    simpl in *; Tactics.destruct_pairs.
    destruct Local_gas_counter.local_gas_counter_and_outdated_context.
    destruct accu; simpl; apply dep_step_eq.
  }
  { grep @With_family.INow.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IBalance.
    dep_eq_case.
    destruct Local_gas_counter.local_gas_counter_and_outdated_context.
    apply dep_step_eq.
  }
  { grep @With_family.ILevel.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ICheck_signature.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IHash_key.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IPack.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    admit.
  }
  { grep @With_family.IUnpack.
    dep_eq_case.
    (* TODO: remove axiom *)
    admit.
  }
  { grep @With_family.IBlake2b.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISha256.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISha512.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISource.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISender.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISelf.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISelf_address.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAmount.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISapling_empty_state.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISapling_verify_update.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct Alpha_context.Sapling.verify_update; simpl; [|discriminate].
    Tactics.destruct_pairs.
    destruct Local_gas_counter.local_gas_counter_and_outdated_context.
    step; Tactics.destruct_pairs; apply dep_step_eq.
  }
  { grep @With_family.IDig.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      erewrite (cast_exists_eval_5 (T := T))
    end.
    admit.
  }
  { grep @With_family.IDug.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IDipn.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IDropn.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IChainId.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INever.
    dep_eq_case.
    step.
  }
  { grep @With_family.IVoting_power.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct Alpha_context.Vote.get_voting_power; simpl; [|discriminate].
    Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ITotal_voting_power.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    destruct Alpha_context.Vote.get_total_voting_power; simpl; [|discriminate].
    Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IKeccak.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.ISha3.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_bls12_381_g1.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_bls12_381_g2.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IAdd_bls12_381_fr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_bls12_381_g1.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_bls12_381_g2.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_bls12_381_fr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_bls12_381_z_fr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IMul_bls12_381_fr_z.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IInt_bls12_381_fr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INeg_bls12_381_g1.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INeg_bls12_381_g2.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.INeg_bls12_381_fr.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IPairing_check_bls12_381.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    set (elements := accu.(Script_typed_ir.boxed_list.elements)).
    replace (List.map _ _) with elements by (induction elements; hauto q: on).
    apply dep_step_eq.
  }
  { grep @With_family.IComb.
    dep_eq_case.
    (* repeat step.
    simpl in *; Tactics.destruct_pairs. *)
    admit.
  }
  { grep @With_family.IUncomb.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IComb_get.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IComb_set.
    dep_eq_case.
    admit.
  }
  { grep @With_family.IDup_n.
    dep_eq_case.
    admit.
  }
  { grep @With_family.ITicket.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_step_eq.
  }
  { grep @With_family.IRead_ticket.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.ISplit_ticket.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    simpl.
    destruct (_ =? _); apply dep_step_eq.
  }
  { grep @With_family.IJoin_tickets.
    dep_eq_case.
    match goal with
    | |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Ty.to_Set a))
    end.
    simpl in *; Tactics.destruct_pairs.
    simpl.
    rewrite <- Script_comparable.dep_compare_comparable_eq; [|admit].
    repeat (step; simpl); apply dep_step_eq.
  }
  { grep @With_family.IOpen_chest.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    simpl.
    repeat step; apply dep_step_eq.
  }
  { grep @With_family.IHalt.
    dep_eq_case.
    apply dep_next_eq.
  }
}
{ destruct fuel, g_value, gas; [discriminate|];
    dep_destruct ks.
  { grep @With_family.KNil.
    dep_eq_case.
    destruct dep_output_accu_stack; simpl.
    congruence.
  }
  { grep @With_family.KCons.
    dep_eq_case.
    apply dep_step_eq.
  }
  { grep @With_family.KReturn.
    dep_eq_case.
    apply dep_next_eq.
  }
  { grep @With_family.KMap_head.
    dep_eq_case.
    apply dep_next_eq.
  }
  { grep @With_family.KUndip.
    dep_eq_case.
    apply dep_next_eq.
  }
  { grep @With_family.KLoop_in.
    dep_eq_case.
    destruct_all bool;
      simpl in *; Tactics.destruct_pairs;
      [apply dep_step_eq | apply dep_next_eq].
  }
  { grep @With_family.KLoop_in_left.
    dep_eq_case.
    step; [apply dep_step_eq | apply dep_next_eq].
  }
  { grep @With_family.KIter.
    dep_eq_case.
    step; simpl; [apply dep_next_eq | apply dep_step_eq].
  }
  { grep @With_family.KList_enter_body.
    dep_eq_case.
    destruct l; simpl.
    { assert (H_rev_map : ∀ {a b : Set} (f : a → b) l,
        List.rev (List.map f l) = List.map f (List.rev l)
      ) by admit.
      rewrite H_rev_map.
      apply dep_next_eq. }
    { apply dep_step_eq. }
  }
  { grep @With_family.KList_exit_body.
    dep_eq_case.
    simpl in *; Tactics.destruct_pairs.
    apply dep_next_eq.
  }
  { grep @With_family.KMap_enter_body.
    dep_eq_case.
    step; simpl; Tactics.destruct_pairs.
    apply dep_next_eq.
    admit.
  }
  { grep @With_family.KMap_exit_body.
    dep_eq_case.
    match goal with
    | |- context[
        Script_map.update
          (With_family.to_value ?k)
          (Some (With_family.to_value ?v))
          (With_family.to_map ?m)
      ] ⇒
      pose proof (Script_map.dep_update_eq k (Some v) m) as H_update
    end.
    with_strategy opaque [Script_map.update] simpl in H_update.
    rewrite <- H_update.
    simpl in *; Tactics.destruct_pairs.
    apply dep_next_eq.
  }
  { grep @With_family.KView_exit.
    dep_eq_case.
    apply dep_next_eq.
  }
}
Admitted.