Zhi Zhang
Department of Computer and Information Sciences
Kansas State University
zhangzhi@ksu.edu

Require Export rt_opt_consistent_util.

Scheme expression_ind := Induction for exp Sort Prop
                         with name_ind := Induction for name Sort Prop.

Scheme expression_x_ind := Induction for expRT Sort Prop
                         with name_x_ind := Induction for nameRT Sort Prop.

Ltac apply_copy_out_opt_H :=
  match goal with
  | [H1: forall (st : symTab) (st' : symTabRT)
                (s : STACK.state) (f : STACK.scope_level * STACK.store)
                (s' : Ret STACK.state)
                (params : list paramSpec)
                (args : list exp) (args' args'' : list expRT),
              toArgsRT st params args args' ->
              toSymTabRT st st' ->
              toParamSpecsRT params ?params' ->
              well_typed_symbol_table st' ->
              well_typed_value_in_stack st' s ->
              well_typed_value_in_store st' (snd f) ->
              well_typed_exps_x st' args' ->
              well_typed_params_x st' ?params' ->
              well_typed_args_x st' args' ?params' ->
              optArgs st' ?params' args' args'' ->
              copyOutRT st' s f ?params' args' s' ->
              copyOutRT st' s f ?params' args'' s',
     H2: toArgsRT ?st ?params ?args ?args',
     H3: toSymTabRT ?st ?st',
     H4: toParamSpecsRT ?params ?params',
     H5: well_typed_symbol_table ?st',
     H6: well_typed_value_in_stack ?st' ?s,
     H7: well_typed_value_in_store ?st' (snd ?f),
     H8: well_typed_exps_x ?st' ?args',
     H9: well_typed_params_x ?st' ?params',
     H10: well_typed_args_x ?st' ?args' ?params',
     H11: optArgs ?st' ?params' ?args' ?args'',
     H12: copyOutRT ?st' ?s ?f ?params' ?args' ?s' |- _ ] =>
      specialize (H1 _ _ _ _ _ _ _ _ _ H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12)
  end.

Lemma optArgs_copyout_soundness: forall st params args args' params' st' s f s' args'',
  toArgsRT st params args args' ->
  toSymTabRT st st' ->
  toParamSpecsRT params params' ->
  well_typed_symbol_table st' ->
  well_typed_value_in_stack st' s ->
  well_typed_value_in_store st' (snd f) ->
  well_typed_exps_x st' args' ->
  well_typed_params_x st' params' ->
  well_typed_args_x st' args' params' ->
  optArgs st' params' args' args'' ->
  copyOutRT st' s f params' args'' s' ->
  copyOutRT st' s f params' args' s'.
Proof.
 intros st params args args' params' st' s f s' args'' H.
 revert params' st' s f s' args''.
 induction H; intros.
-
 inversion H7; subst; auto.
-
 inversion H4; subst;
 inversion H8; subst;
 inversion H9; subst;
 inversion H10; subst.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H11; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end.
 inversion H12; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end.
 apply CopyOut_Mode_In_X; auto;
 apply IHtoArgsRT with (args'' := args'); auto.
-
 inversion H4; subst;
 inversion H8; subst;
 inversion H9; subst;
 inversion H10; subst.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H11; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end.
 inversion H12; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end.
 apply CopyOut_Mode_In_X; auto;
 apply IHtoArgsRT with (args'' := args'); auto.
-
 inversion H5; subst;
 inversion H9; subst;
 inversion H10; subst;
 inversion H11; subst.
 match goal with
 | [H: well_typed_value_in_stack _ _ |- _] =>
     specialize (well_typed_stack_infer _ _ H); let HB := fresh "HB" in intro HB
 end;
 match goal with
 | [H: well_typed_value_in_store _ _ |- _] =>
     specialize (well_typed_store_infer _ _ H); let HB := fresh "HB" in intro HB
 end.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H12; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 inversion H13; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: toSymTabRT ?st ?st',
    H2: fetch_exp_type _ ?st = _ |- _ ] =>
     specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 repeat progress match goal with
 | [H1: fetch_exp_type_rt ?x ?st = _,
    H2: fetch_exp_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = false,
    H2: is_range_constrainted_type ?x = true |- _] =>
     rewrite H1 in H2; inversion H2
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 match goal with
 | [H1: ?x = true,
    H2: ?y = true,
    H3: ?x = false \/ ?y = false |- _] => rewrite H1 in H3; rewrite H2 in H3; clear - H3; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (_ :: ?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H1: extract_subtype_range_rt _ ?t _,
    H2: extract_subtype_range_rt _ ?t _ |- _] =>
     specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
 | _ => idtac
 end;
 match goal with
 | [H: optName _ _ _ |- _] =>
     specialize (optimize_name_ex_cks_eq _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_exp_x _ (NameRT _ _) |- _] => inversion H; subst
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_name_x ?st (update_exterior_checks_name ?n ?cks) |- _] =>
     specialize (well_typed_name_preserve _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;

 match goal with
 | [H: storeUpdateRT _ _ (update_exterior_checks_name _ _) _ _ |- _] =>
     specialize (store_update_ex_cks_stripped _ _ _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: optName _ (update_exterior_checks_name _ _) _ |- _] =>
     specialize (optimize_name_ex_cks_stripped _ _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H: parameter_mode_rt _ = In |- _] => apply CopyOut_Mode_In_X; auto
 | _ => idtac
 end; simpl in *.
 apply CopyOut_Mode_Out_nRTE_X with (v:=v); auto.
 rewrite <- HZ0; auto.
 apply_storeUpdateRT_opt_soundness'; auto.
 apply CopyOut_Mode_Out_NoRange_X with (v:=v) (s':=s'0); auto.
 rewrite <- HZ0; auto.
 apply_storeUpdateRT_opt_soundness'; auto.
 apply IHtoArgsRT with (args'' := args'); auto.
   repeat progress match goal with
   | [H1: fetch_exp_type_rt ?x ?y = _, H2: fetch_exp_type_rt ?x ?y = _ |- _] => rewrite H1 in H2; inversion H2; subst
   end.
   apply_well_typed_value_in_store_fetch.
   apply_value_well_typed_with_matched_type.
   match goal with
   | [H: Some ?t = fetch_exp_type_rt (name_astnum_rt ?n_flagged) ?st |- _] => symmetry in H
   end.
   apply_storeUpdateRT_opt_soundness; auto.
   apply_storeUpdate_with_typed_value_preserve_typed_stack; auto.
-
 inversion H5; subst;
 inversion H9; subst;
 inversion H10; subst;
 inversion H11; subst.
 match goal with
 | [H: well_typed_value_in_stack _ _ |- _] =>
     specialize (well_typed_stack_infer _ _ H); let HB := fresh "HB" in intro HB
 end;
 match goal with
 | [H: well_typed_value_in_store _ _ |- _] =>
     specialize (well_typed_store_infer _ _ H); let HB := fresh "HB" in intro HB
 end.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H12; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 inversion H13; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: toSymTabRT ?st ?st',
    H2: fetch_exp_type _ ?st = _ |- _ ] =>
     specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 repeat progress match goal with
 | [H1: fetch_exp_type_rt ?x ?st = _,
    H2: fetch_exp_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = false,
    H2: is_range_constrainted_type ?x = true |- _] =>
     rewrite H1 in H2; inversion H2
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 match goal with
 | [H1: ?x = true,
    H2: ?y = true,
    H3: ?x = false \/ ?y = false |- _] => rewrite H1 in H3; rewrite H2 in H3; clear - H3; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (_ :: ?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H1: extract_subtype_range_rt _ ?t _,
    H2: extract_subtype_range_rt _ ?t _ |- _] =>
     specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
 | _ => idtac
 end;
 match goal with
 | [H: optName _ _ _ |- _] =>
     specialize (optimize_name_ex_cks_eq _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_exp_x _ (NameRT _ _) |- _] => inversion H; subst
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_name_x ?st (update_exterior_checks_name ?n ?cks) |- _] =>
     specialize (well_typed_name_preserve _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;

 match goal with
 | [H: storeUpdateRT _ _ (update_exterior_checks_name _ _) _ _ |- _] =>
     specialize (store_update_ex_cks_stripped _ _ _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: optName _ (update_exterior_checks_name _ _) _ |- _] =>
     specialize (optimize_name_ex_cks_stripped _ _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H: parameter_mode_rt _ = In |- _] => apply CopyOut_Mode_In_X; auto
 | _ => idtac
 end; simpl in *.
 apply_well_typed_bounded_var_exists_int_value.
 assert (HA1: sub_bound (Interval u v) (Interval u' v') true).
   match goal with
   | [H: optimize_range_check_on_copy_out _ _ _ _ |- _] => inversion H; subst; auto
   end.
   match goal with
   | [H1: ~ List.In RangeCheckOnReturn (name_exterior_checks ?n0),
      H2: name_exterior_checks ?n0 = name_exterior_checks _ |- _] =>
       rewrite name_updated_exterior_checks in H2; rewrite H2 in H1; clear - H1; smack
   end.
 assert (HA2: in_bound x (Interval u' v') true).
    apply_well_typed_var_in_bound.
    apply_In_Bound_SubBound_Trans; auto.

 apply CopyOut_Mode_Out_Range_nRTE_X with (v:=x) (l:=u') (u:=v') (t:=t); auto.
 rewrite name_updated_exterior_checks; smack.
 constructor; auto.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 apply_well_typed_bounded_var_exists_int_value.
 assert (HA1: sub_bound (Interval u v) (Interval u' v') true).
   match goal with
   | [H: optimize_range_check_on_copy_out _ _ _ _ |- _] => inversion H; subst; auto
   end.
   match goal with
   | [H1: ~ List.In RangeCheckOnReturn (name_exterior_checks ?n0),
      H2: name_exterior_checks ?n0 = name_exterior_checks _ |- _] =>
       rewrite name_updated_exterior_checks in H2; rewrite H2 in H1; clear - H1; smack
   end.
 assert (HA2: in_bound x (Interval u' v') true).
    apply_well_typed_var_in_bound.
    apply_In_Bound_SubBound_Trans; auto.
 apply CopyOut_Mode_Out_Range_X with (v:=x) (t:=t) (l:=u') (u:=v') (s':=s'0); auto.
 rewrite name_updated_exterior_checks; smack.
 constructor; auto.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 apply IHtoArgsRT with (args'' := args'); auto.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 assert(HA3: storeUpdateRT st' s (update_exterior_checks_name n' (name_exterior_checks nRT)) (Int x) (OK s'0)).
   apply_store_update_ex_cks_added; auto.
 apply_storeUpdateRT_opt_soundness.
 apply storeUpdate_with_typed_value_preserve_typed_stack with (st0:=st) (x0:=nm) (x:=nRT) (s:=s) (t:=t) (v:=Int x); auto.
   match goal with
   | [H: context[fetch_exp_type_rt (name_astnum_rt ?nRT) ?st] |- _] =>
       rewrite update_exterior_checks_name_astnum_eq in H; smack
   end.
   apply_well_typed_value_of_var.
   apply_well_typed_value_subtype_trans; auto.
 apply CopyOut_Mode_Out_Range_RTE_X with (v:=v0) (l:=u') (u:=v') (t:=t); auto.
 rewrite name_updated_exterior_checks; smack.
 assert(HA: n = n0).
   clear -H35; inversion H35; subst; smack.
 subst. rewrite H40 in H31; inversion H31; subst;
 match goal with
  | [H1: extract_subtype_range_rt _ ?t _,
     H2: extract_subtype_range_rt _ ?t _ |- _] =>
      specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst; auto
 end.
 apply CopyOut_Mode_Out_Range_nRTE_X with (v:=v0) (t:=t) (l:=u') (u:=v'); auto.
 rewrite name_updated_exterior_checks; smack.
 assert(HA: n = n0).
   clear -H35; inversion H35; subst; smack.
 subst. rewrite H40 in H31; inversion H31; subst;
 match goal with
  | [H1: extract_subtype_range_rt _ ?t _,
     H2: extract_subtype_range_rt _ ?t _ |- _] =>
      specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst; auto
 end.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 assert(HA: n = n0).
   clear -H35; inversion H35; subst; smack.
 apply CopyOut_Mode_Out_Range_X with (v:=v0) (t:=t) (l:=u') (u:=v') (s':=s'0); subst; auto.
 rewrite name_updated_exterior_checks; smack.
 rewrite H37 in H31; inversion H31; subst;
 match goal with
  | [H1: extract_subtype_range_rt _ ?t _,
     H2: extract_subtype_range_rt _ ?t _ |- _] =>
      specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst; auto
 end.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.

 apply IHtoArgsRT with (args'' := args'); auto.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 assert(HA3: storeUpdateRT st' s (update_exterior_checks_name n' (name_exterior_checks nRT)) (Int v0) (OK s'0)).
   apply_store_update_ex_cks_added; auto.
 apply_storeUpdateRT_opt_soundness.
 apply storeUpdate_with_typed_value_preserve_typed_stack with (st0:=st) (x0:=nm) (x:=nRT) (s:=s) (t:=t) (v:=Int v0); auto.
   match goal with
   | [H: context[fetch_exp_type_rt (name_astnum_rt ?nRT) ?st] |- _] =>
       rewrite update_exterior_checks_name_astnum_eq in H; smack
   end.
  match goal with
  | [H1: toSymTabRT ?st ?st',
     H2: fetch_exp_type _ ?st = _ |- _ ] =>
      specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.
   rewrite H37 in HZ7; inversion HZ7; subst.
   apply_value_in_range_is_well_typed; auto. smack.
-
 inversion H6; subst;
 inversion H10; subst;
 inversion H11; subst;
 inversion H12; subst.
 match goal with
 | [H: well_typed_value_in_stack _ _ |- _] =>
     specialize (well_typed_stack_infer _ _ H); let HB := fresh "HB" in intro HB
 end;
 match goal with
 | [H: well_typed_value_in_store _ _ |- _] =>
     specialize (well_typed_store_infer _ _ H); let HB := fresh "HB" in intro HB
 end.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H13; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 inversion H14; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: toSymTabRT ?st ?st',
    H2: fetch_exp_type _ ?st = _ |- _ ] =>
     specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 repeat progress match goal with
 | [H1: fetch_exp_type_rt ?x ?st = _,
    H2: fetch_exp_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = false,
    H2: is_range_constrainted_type ?x = true |- _] =>
     rewrite H1 in H2; inversion H2
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 match goal with
 | [H1: ?x = true,
    H2: ?y = true,
    H3: ?x = false \/ ?y = false |- _] => rewrite H1 in H3; rewrite H2 in H3; clear - H3; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (_ :: ?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H1: extract_subtype_range_rt _ ?t _,
    H2: extract_subtype_range_rt _ ?t _ |- _] =>
     specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
 | _ => idtac
 end;
 match goal with
 | [H: optName _ _ _ |- _] =>
     specialize (optimize_name_ex_cks_eq _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_exp_x _ (NameRT _ _) |- _] => inversion H; subst
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_name_x ?st (update_exterior_checks_name ?n ?cks) |- _] =>
     specialize (well_typed_name_preserve _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;

 match goal with
 | [H: storeUpdateRT _ _ (update_exterior_checks_name _ _) _ _ |- _] =>
     specialize (store_update_ex_cks_stripped _ _ _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: optName _ (update_exterior_checks_name _ _) _ |- _] =>
     specialize (optimize_name_ex_cks_stripped _ _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end; simpl in *.
 apply CopyOut_Mode_Out_nRTE_X with (v:=v); auto.
 rewrite <- HZ0; auto.
 apply_storeUpdateRT_opt_soundness'; auto.
 apply CopyOut_Mode_Out_NoRange_X with (v:=v) (s':=s'0); auto.
 rewrite <- HZ0; auto.
 apply_storeUpdateRT_opt_soundness'; auto.
 apply IHtoArgsRT with (args'' := args'); auto.
   repeat progress match goal with
   | [H1: fetch_exp_type_rt ?x ?y = _, H2: fetch_exp_type_rt ?x ?y = _ |- _] => rewrite H1 in H2; inversion H2; subst
   end.
   apply_well_typed_value_in_store_fetch.
   apply_value_well_typed_with_matched_type.
   match goal with
   | [H: Some ?t = fetch_exp_type_rt (name_astnum_rt ?nRT) ?st |- _] => symmetry in H
   end.
   apply_storeUpdateRT_opt_soundness; auto.
   apply_storeUpdate_with_typed_value_preserve_typed_stack; auto.
-
 inversion H6; subst;
 inversion H10; subst;
 inversion H11; subst;
 inversion H12; subst.
 match goal with
 | [H: well_typed_value_in_stack _ _ |- _] =>
     specialize (well_typed_stack_infer _ _ H); let HB := fresh "HB" in intro HB
 end;
 match goal with
 | [H: well_typed_value_in_store _ _ |- _] =>
     specialize (well_typed_store_infer _ _ H); let HB := fresh "HB" in intro HB
 end.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H13; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 inversion H14; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: toSymTabRT ?st ?st',
    H2: fetch_exp_type _ ?st = _ |- _ ] =>
     specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 repeat progress match goal with
 | [H1: fetch_exp_type_rt ?x ?st = _,
    H2: fetch_exp_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = false,
    H2: is_range_constrainted_type ?x = true |- _] =>
     rewrite H1 in H2; inversion H2
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 match goal with
 | [H1: ?x = true,
    H2: ?y = true,
    H3: ?x = false \/ ?y = false |- _] => rewrite H1 in H3; rewrite H2 in H3; clear - H3; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (_ :: ?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H1: extract_subtype_range_rt _ ?t _,
    H2: extract_subtype_range_rt _ ?t _ |- _] =>
     specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
 | _ => idtac
 end;
 match goal with
 | [H: optName _ _ _ |- _] =>
     specialize (optimize_name_ex_cks_eq _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_exp_x _ (NameRT _ _) |- _] => inversion H; subst
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_name_x ?st (update_exterior_checks_name ?n ?cks) |- _] =>
     specialize (well_typed_name_preserve _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;

 match goal with
 | [H: storeUpdateRT _ _ (update_exterior_checks_name _ _) _ _ |- _] =>
     specialize (store_update_ex_cks_stripped _ _ _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: optName _ (update_exterior_checks_name _ _) _ |- _] =>
     specialize (optimize_name_ex_cks_stripped _ _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end; simpl in *.
 apply CopyOut_Mode_Out_nRTE_X with (v:=v); auto.
 rewrite <- HZ0; auto.
 apply_store_update_ex_cks_added.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 apply CopyOut_Mode_Out_NoRange_X with (v:=v) (s':=s'0); auto.
 rewrite <- HZ0; auto.
 apply_store_update_ex_cks_added.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 apply IHtoArgsRT with (args'' := args'); auto.
   repeat progress match goal with
   | [H1: fetch_exp_type_rt ?x ?y = _, H2: fetch_exp_type_rt ?x ?y = _ |- _] => rewrite H1 in H2; inversion H2; subst
   end.
   apply_well_typed_value_in_store_fetch.
   apply_value_well_typed_with_matched_type.
   apply_well_typed_name_preserve.
   assert(HA1: storeUpdateRT st' s (update_exterior_checks_name n' (name_exterior_checks nRT)) (v) (OK s'0)).
   apply_store_update_ex_cks_added; auto.
   apply_storeUpdateRT_opt_soundness.
   apply storeUpdate_with_typed_value_preserve_typed_stack with (st0:=st) (x0:=nm) (x:=nRT) (s:=s) (t:=t) (v:=v); auto.
   match goal with
   | [H: context[fetch_exp_type_rt (name_astnum_rt ?nRT) ?st] |- _] =>
       rewrite update_exterior_checks_name_astnum_eq in H; smack
   end.
-
 inversion H6; subst;
 inversion H10; subst;
 inversion H11; subst;
 inversion H12; subst.
 match goal with
 | [H: well_typed_value_in_stack _ _ |- _] =>
     specialize (well_typed_stack_infer _ _ H); let HB := fresh "HB" in intro HB
 end;
 match goal with
 | [H: well_typed_value_in_store _ _ |- _] =>
     specialize (well_typed_store_infer _ _ H); let HB := fresh "HB" in intro HB
 end.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H13; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 inversion H14; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end;
 match goal with
 | [H: extract_subtype_range_rt _ (parameter_subtype_mark_rt _) (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: toSymTabRT ?st ?st',
    H2: fetch_exp_type _ ?st = _ |- _ ] =>
     specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 repeat progress match goal with
 | [H1: fetch_exp_type_rt ?x ?st = _,
    H2: fetch_exp_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = false,
    H2: is_range_constrainted_type ?x = true |- _] =>
     rewrite H1 in H2; inversion H2
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 match goal with
 | [H1: ?x = true,
    H2: ?y = true,
    H3: ?x = false \/ ?y = false |- _] => rewrite H1 in H3; rewrite H2 in H3; clear - H3; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (_ :: ?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H1: extract_subtype_range_rt _ ?t _,
    H2: extract_subtype_range_rt _ ?t _ |- _] =>
     specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
 | _ => idtac
 end;
 match goal with
 | [H: optName _ _ _ |- _] =>
     specialize (optimize_name_ex_cks_eq _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_exp_x _ (NameRT _ _) |- _] => inversion H; subst
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_name_x ?st (update_exterior_checks_name ?n ?cks) |- _] =>
     specialize (well_typed_name_preserve _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;

 match goal with
 | [H: storeUpdateRT _ _ (update_exterior_checks_name _ _) _ _ |- _] =>
     specialize (store_update_ex_cks_stripped _ _ _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: optName _ (update_exterior_checks_name _ _) _ |- _] =>
     specialize (optimize_name_ex_cks_stripped _ _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H: parameter_mode_rt _ = In |- _] => apply CopyOut_Mode_In_X; auto
 | _ => idtac
 end; simpl in *.
 match goal with
 | [H1: ~ List.In RangeCheckOnReturn (name_exterior_checks ?n'),
    H2: name_exterior_checks ?n' = name_exterior_checks (update_exterior_checks_name _ _) |- _] =>
     rewrite H2 in H1; rewrite name_updated_exterior_checks in H1; clear - H1; smack
 end.
 match goal with
 | [H1: ~ List.In RangeCheckOnReturn (name_exterior_checks ?n'),
    H2: name_exterior_checks ?n' = name_exterior_checks (update_exterior_checks_name _ _) |- _] =>
     rewrite H2 in H1; rewrite name_updated_exterior_checks in H1; clear - H1; smack
 end.
 apply CopyOut_Mode_Out_Range_RTE_X with (v:=v) (l:=l) (u:=u) (t:=t); auto.
 rewrite name_updated_exterior_checks; smack.
 apply CopyOut_Mode_Out_Range_nRTE_X with (v:=v) (t:=t) (l:=l) (u:=u); auto.
 rewrite name_updated_exterior_checks; smack.
 apply_store_update_ex_cks_added.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 apply CopyOut_Mode_Out_Range_X with (v:=v) (t:=t) (l:=l) (u:=u) (s':=s'0); subst; auto.
 rewrite name_updated_exterior_checks; smack.
 apply_store_update_ex_cks_added.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=nBound); auto.
 apply_store_update_ex_cks_added; auto.
 apply IHtoArgsRT with (args'' := args'); auto.
   apply_well_typed_value_in_store_fetch.
   assert(HA1: storeUpdateRT st' s (update_exterior_checks_name n' (name_exterior_checks nRT)) (Int v) (OK s'0)).
     apply_store_update_ex_cks_added; auto.
   apply_storeUpdateRT_opt_soundness; auto.
 apply storeUpdate_with_typed_value_preserve_typed_stack with (st0:=st) (x0:=nm) (x:=nRT) (s:=s) (t:=t) (v:=Int v); auto.
   match goal with
   | [H: context[fetch_exp_type_rt (name_astnum_rt ?nRT) ?st] |- _] =>
       rewrite update_exterior_checks_name_astnum_eq in H; smack
   end.
  apply_value_in_range_is_well_typed; auto.
  smack.
-
 inversion H6; subst;
 inversion H10; subst;
 inversion H11; subst;
 inversion H12; subst.
 match goal with
 | [H: well_typed_value_in_stack _ _ |- _] =>
     specialize (well_typed_stack_infer _ _ H); let HB := fresh "HB" in intro HB
 end;
 match goal with
 | [H: well_typed_value_in_store _ _ |- _] =>
     specialize (well_typed_store_infer _ _ H); let HB := fresh "HB" in intro HB
 end.
 assert(HZ1: param.(parameter_mode) = paramRT.(parameter_mode_rt) /\
            (parameter_subtype_mark param) = (parameter_subtype_mark_rt paramRT)).
 match goal with
 | [H: toParamSpecRT ?param ?paramRT |- _] => clear - H; inversion H; smack
 end. destruct HZ1 as [HZ1a HZ1b].
 inversion H13; subst;
 match goal with
 | [H1: parameter_mode ?p = parameter_mode_rt ?a,
    H2: parameter_mode ?p = _ ,
    H3: parameter_mode_rt ?a = _ |- _] =>
     rewrite H2 in H1; rewrite H3 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 end;
 match goal with
 | [H: extract_subtype_range_rt _ _ (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 rewrite HZ1b in *;
 inversion H14; subst;
 match goal with
 | [H1: parameter_mode_rt ?a = _ ,
    H2: parameter_mode_rt ?a = _ |- _] => rewrite H2 in H1; inversion H1
 | [H1: parameter_mode_rt ?a = In ,
    H2: parameter_mode_rt ?a = Out \/ parameter_mode_rt ?a = In_Out |- _] =>
     rewrite H1 in H2; clear - H2; smack
 | _ => idtac
 end;
 match goal with
 | [H: extract_subtype_range_rt _ (parameter_subtype_mark_rt _) (RangeRT _ _) |- _] =>
     specialize (range_constrainted_type_true _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 match goal with
 | [H1: toSymTabRT ?st ?st',
    H2: fetch_exp_type _ ?st = _ |- _ ] =>
     specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 repeat progress match goal with
 | [H1: fetch_exp_type_rt ?x ?st = _,
    H2: fetch_exp_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
 | _ => idtac
 end;
 match goal with
 | [H1: is_range_constrainted_type ?x = _,
    H2: is_range_constrainted_type ?y = _,
    H3: ?x = ?y |- _] =>
     rewrite H3 in H1; rewrite H1 in H2; inversion H2
 | _ => idtac
 end;
 match goal with
 | [H1: ?x = true,
    H2: ?y = true,
    H3: ?x = false \/ ?y = false |- _] => rewrite H1 in H3; rewrite H2 in H3; clear - H3; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H: ~ List.In ?x (name_exterior_checks (update_exterior_checks_name _ (_ :: ?x :: _))) |- _] =>
     rewrite name_updated_exterior_checks in H; clear - H; smack
 | [H1: extract_subtype_range_rt _ ?t _,
    H2: extract_subtype_range_rt _ ?t _ |- _] =>
     specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
     let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
 | _ => idtac
 end;
 match goal with
 | [H: optExp ?st (NameRT _ _) _ |- _] => inversion H; subst
 end;
 match goal with
 | [H: optName _ _ _ |- _] =>
     specialize (optimize_name_ex_cks_eq _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_exp_x _ (NameRT _ _) |- _] => inversion H; subst
 | _ => idtac
 end;
 match goal with
 | [H: well_typed_name_x ?st (update_exterior_checks_name ?n ?cks) |- _] =>
     specialize (well_typed_name_preserve _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;

 match goal with
 | [H: storeUpdateRT _ _ (update_exterior_checks_name _ _) _ _ |- _] =>
     specialize (store_update_ex_cks_stripped _ _ _ _ _ _ H);
     let HZ := fresh "HZ" in intro HZ
 | _ => idtac
 end;
 match goal with
 | [H: optName _ (update_exterior_checks_name _ _) _ |- _] =>
     specialize (optimize_name_ex_cks_stripped _ _ _ _ _ H);
     let HZ := fresh "HZ" in intros HZ
 | _ => idtac
 end;
 simpl in *.
 assert(HA0: bound_of_type st' (parameter_subtype_mark_rt paramRT) (Interval u v)). constructor; auto.
 apply_well_typed_bounded_var_exists_int_value.
 assert (HA1: sub_bound (Interval u v) (Interval u' v') true).
   match goal with
   | [H: optimize_range_check_on_copy_out _ _ _ _ |- _] => inversion H; subst; auto
   end.
   rewrite name_updated_exterior_checks in HZ2.
   apply_range_check_on_copyout_preserve; smack.
 assert (HA2: in_bound x (Interval u' v') true).
   apply_well_typed_var_in_bound.
   apply_In_Bound_SubBound_Trans; auto.
 assert(HA3: exists n'', arg = NameRT n n'').
   clear - H36; inversion H36; smack.
 destruct HA3; subst.

 apply CopyOut_Mode_Out_Range_nRTE_X with (v:=x) (l:=u') (u:=v') (t:=t); auto.
 rewrite name_updated_exterior_checks; smack.
 constructor; auto.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply_optimize_range_check_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=Interval v1 v2); auto.
 apply_store_update_ex_cks_added; auto.
 assert(HA0: bound_of_type st' (parameter_subtype_mark_rt paramRT) (Interval u v)). constructor; auto.
 apply_well_typed_bounded_var_exists_int_value.
 assert (HA1: sub_bound (Interval u v) (Interval u' v') true).
   match goal with
   | [H: optimize_range_check_on_copy_out _ _ _ _ |- _] => inversion H; subst; auto
   end.
   rewrite name_updated_exterior_checks in HZ2.
   apply_range_check_on_copyout_preserve; smack.
 assert (HA2: in_bound x (Interval u' v') true).
   apply_well_typed_var_in_bound.
   apply_In_Bound_SubBound_Trans; auto.
 assert(HA3: exists n'', arg = NameRT n n'').
   clear - H36; inversion H36; smack.
 destruct HA3; subst.

 apply CopyOut_Mode_Out_Range_X with (v:=x) (t:=t) (l:=u') (u:=v') (s':=s'0); auto.
 rewrite name_updated_exterior_checks; smack.
 constructor; auto.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply_optimize_range_check_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=Interval v1 v2); auto.
 apply_store_update_ex_cks_added; auto.
 apply IHtoArgsRT with (args'' := args'); auto.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply_optimize_range_check_reserve_storeUpdate_backward.
 assert(HA3: storeUpdateRT st' s (update_exterior_checks_name n' (name_exterior_checks nRT)) (Int x) (OK s'0)).
   apply_store_update_ex_cks_added; auto.
 apply_storeUpdateRT_opt_soundness.
 apply storeUpdate_with_typed_value_preserve_typed_stack with (st0:=st) (x0:=nm) (x:=nRT) (s:=s) (t:=t) (v:=Int x); auto.
   match goal with
   | [H: context[fetch_exp_type_rt (name_astnum_rt ?nRT) ?st] |- _] =>
       rewrite update_exterior_checks_name_astnum_eq in H; smack
   end.
   apply_well_typed_value_of_var.
   apply_well_typed_value_subtype_trans; auto.
 assert(HA1: exists n'', arg = NameRT n n'').
   clear - H36; inversion H36; smack.
 destruct HA1; subst.
 apply CopyOut_Mode_Out_Range_RTE_X with (v:=v0) (l:=u') (u:=v') (t:=t); auto.
 rewrite name_updated_exterior_checks; smack.

 assert(HA1: n = n0).
   clear -H37; inversion H37; subst; smack.
 subst. rewrite H42 in H31; inversion H31; subst;
 match goal with
  | [H1: extract_subtype_range_rt _ ?t _,
     H2: extract_subtype_range_rt _ ?t _ |- _] =>
      specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst; auto
 end.
 assert(HA1: exists n'', arg = NameRT n n'').
   clear - H36; inversion H36; smack.
 destruct HA1; subst.
 apply CopyOut_Mode_Out_Range_nRTE_X with (v:=v0) (t:=t) (l:=u') (u:=v'); auto.
 rewrite name_updated_exterior_checks; smack.
 assert(HA: n = n0).
   clear -H37; inversion H37; subst; smack.
 subst. rewrite H42 in H31; inversion H31; subst;
 match goal with
  | [H1: extract_subtype_range_rt _ ?t _,
     H2: extract_subtype_range_rt _ ?t _ |- _] =>
      specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst; auto
 end.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply_optimize_range_check_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=Interval v1 v2); auto.
 apply_store_update_ex_cks_added; auto.
 assert(HA1: exists n'', arg = NameRT n n'').
   clear - H36; inversion H36; smack.
 destruct HA1; subst.
 assert(HA2: n = n0).
   clear -H37; inversion H37; subst; smack.
 apply CopyOut_Mode_Out_Range_X with (v:=v0) (t:=t) (l:=u') (u:=v') (s':=s'0); subst; auto.
 rewrite name_updated_exterior_checks; smack.
 rewrite H39 in H31; inversion H31; subst;
 match goal with
  | [H1: extract_subtype_range_rt _ ?t _,
     H2: extract_subtype_range_rt _ ?t _ |- _] =>
      specialize (extract_subtype_range_unique _ _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst; auto
 end.
 apply_store_update_ex_cks_added.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply_optimize_range_check_reserve_storeUpdate_backward.
 apply storeUpdateRT_opt_soundness
   with (n:=nm) (st:=st) (n'':=update_exterior_checks_name n' (name_exterior_checks nRT)) (nBound:=Interval v1 v2); auto.
 apply_store_update_ex_cks_added; auto.

 apply IHtoArgsRT with (args'' := args'); auto.
 apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward.
 apply_optimize_range_check_reserve_storeUpdate_backward.
 assert(HA3: storeUpdateRT st' s (update_exterior_checks_name n' (name_exterior_checks nRT)) (Int v0) (OK s'0)).
   apply_store_update_ex_cks_added; auto.
 apply_storeUpdateRT_opt_soundness.
 apply storeUpdate_with_typed_value_preserve_typed_stack with (st0:=st) (x0:=nm) (x:=nRT) (s:=s) (t:=t) (v:=Int v0); auto.
   match goal with
   | [H: context[fetch_exp_type_rt (name_astnum_rt ?nRT) ?st] |- _] =>
       rewrite update_exterior_checks_name_astnum_eq in H; smack
   end.
  match goal with
  | [H1: toSymTabRT ?st ?st',
     H2: fetch_exp_type _ ?st = _ |- _ ] =>
      specialize (symbol_table_exp_type_rel _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.
   rewrite H39 in HZ8; inversion HZ8; subst.
   apply_value_in_range_is_well_typed; auto. smack.
Qed.

Ltac apply_optArgs_copyout_soundness :=
  match goal with
  | [H1: toArgsRT ?st ?params ?args ?args',
     H2: toSymTabRT ?st ?st',
     H3: toParamSpecsRT ?params ?params',
     H4: well_typed_symbol_table ?st',
     H5: well_typed_value_in_stack ?st' ?s,
     H6: well_typed_value_in_store ?st' (snd ?f),
     H7: well_typed_exps_x ?st' ?args',
     H8: well_typed_params_x ?st' ?params',
     H9: well_typed_args_x ?st' ?args' ?params',
     H10: optArgs ?st' ?params' ?args' ?args'',
     H11: copyOutRT ?st' ?s ?f ?params' ?args'' ?s' |- _ ] =>
      specialize (optArgs_copyout_soundness _ _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11);
      let HZ := fresh "HZ" in intro HZ
  end.