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

Require Export eval_rt.
Require Export rt_gen.
Require Export rt_gen_util.
Require Export CpdtTactics.

Lemma overflow_check_OK_exist_int: forall v v',
  overflowCheck v (OK v') ->
    v' = Int v.
Proof.
  intros.
  remember (OK v') as x.
  inversion H; smack.
Qed.

Ltac apply_overflow_check_OK_exist_int :=
  match goal with
  | [H: overflowCheck ?v (OK ?v') |- _] =>
    specialize (overflow_check_OK_exist_int _ _ H);
    let HZ := fresh "HZ" in intros HZ
  end.

Lemma binop_overflow_check_soundness: forall op v1 v2 v3,
  op = Plus \/ op = Minus \/ op = Multiply ->
    do_run_time_check_on_binop op v1 v2 v3 ->
      evalBinOpRTS (OverflowCheck :: nil) op v1 v2 v3.
Proof.
  intros;
  match goal with
  | [H: do_run_time_check_on_binop _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: overflowCheck ?v ?v' |- _] => destruct v'
  end;
  match goal with
  | [H: overflowCheck ?v ?v' |- _] => inversion H; smack
  end;
  repeat progress match goal with
    | [|- evalBinOpRTS _ _ _ _ _ ] => econstructor; smack
    | [|- evalBinOpRT _ _ _ _ _ ] => econstructor; smack
  end.
Qed.

Ltac apply_binop_overflow_check_soundness :=
  match goal with
  | [H1: ?op = Plus \/ ?op = Minus \/ ?op = Multiply,
     H2: do_run_time_check_on_binop ?op ?v1 ?v2 ?v3 |- _ ] =>
      specialize (binop_overflow_check_soundness _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_flagged_overflow_check_soundness: forall op v1 v2 v3,
  op = Plus \/ op = Minus \/ op = Multiply ->
    evalBinOpRTS (OverflowCheck :: nil) op v1 v2 v3 ->
      do_run_time_check_on_binop op v1 v2 v3.
Proof.
  intros.
  repeat progress match goal with
    | [H: evalBinOpRTS _ _ _ _ _ |- _] => inversion H; clear H; smack
    | [H: evalBinOpRT _ _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: overflowCheck ?v1 (RTE _) |- do_run_time_check_on_binop _ _ _ (RTE _)] =>
      apply DoCheckOnBinops with (v:=v1); auto
  | [H: overflowCheck ?v1 (OK _) |- do_run_time_check_on_binop _ _ _ (OK _)] =>
      apply DoCheckOnBinops with (v:=v1); smack;
      apply_overflow_check_OK_exist_int; smack
  end.
Qed.

Ltac apply_binop_flagged_overflow_check_soundness :=
  match goal with
  | [H1: ?op = Plus \/ ?op = Minus \/ ?op = Multiply,
     H2: evalBinOpRTS (OverflowCheck :: nil) ?op ?v1 ?v2 ?v3 |- _ ] =>
      specialize (binop_flagged_overflow_check_soundness _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_overflow_division_check_soundness: forall v1 v2 v3,
    do_run_time_check_on_binop Divide v1 v2 v3 ->
      evalBinOpRTS (DivCheck :: OverflowCheck :: nil) Divide v1 v2 v3.
Proof.
  intros;
  match goal with
  | [H: do_run_time_check_on_binop _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H1: divCheck _ _ _ (OK ?v1), H2: overflowCheck _ ?v2 |- _] =>
      destruct v2; apply ChecksBinOp with (v:= v1)
  | _ => idtac
  end;
  repeat progress match goal with
    | [|- evalBinOpRTS _ _ _ _ _ ] => econstructor; smack
    | [|- evalBinOpRT _ _ _ _ _ ] => econstructor; smack
  end;
  match goal with
  | [H1: divCheck _ _ _ _, H2: overflowCheck _ _ |- _] =>
      inversion H1; smack; inversion H2; smack
  end.
Qed.

Ltac apply_binop_overflow_division_check_soundness :=
  match goal with
  | [H: do_run_time_check_on_binop Divide ?v1 ?v2 ?v3 |- _] =>
      specialize (binop_overflow_division_check_soundness _ _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_flagged_overflow_division_check_soundness: forall v1 v2 v3,
    evalBinOpRTS (DivCheck :: OverflowCheck :: nil) Divide v1 v2 v3 ->
      do_run_time_check_on_binop Divide v1 v2 v3.
Proof.
  intros;
  repeat progress match goal with
    | [H: evalBinOpRTS _ _ _ _ _ |- _] => inversion H; clear H; smack
    | [H: evalBinOpRT _ _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
    | [H: divCheck _ _ _ _ |- _] => inversion H; smack
  end.
  constructor; auto.
  apply DoCheckOnDivide with (v:=(Z.quot v0 v3)); auto.
  apply DoCheckOnDivide with (v:=(Z.quot v0 v3)); auto;
  match goal with
    | [H: overflowCheck _ _ |- _] => inversion H; smack
  end.
Qed.

Ltac apply_binop_flagged_overflow_division_check_soundness :=
  match goal with
  | [H: evalBinOpRTS (DivCheck :: OverflowCheck :: nil) Divide ?v1 ?v2 ?v3 |- _] =>
      specialize (binop_flagged_overflow_division_check_soundness _ _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_division_check_soundness: forall v1 v2 v3,
    do_run_time_check_on_binop Modulus v1 v2 v3 ->
      evalBinOpRTS (DivCheck :: nil) Modulus v1 v2 v3.
Proof.
  intros;
  match goal with
  | [H: do_run_time_check_on_binop _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: divCheck _ ?v1 ?v2 ?v3 |- _] => destruct v3
  end;
  match goal with
  | [H: divCheck _ _ _ _ |- _] => inversion H; smack
  end;
  repeat progress match goal with
    | [|- evalBinOpRTS _ _ _ _ _ ] => econstructor; smack
    | [|- evalBinOpRT _ _ _ _ _ ] => econstructor; smack
  end.
Qed.

Ltac apply_binop_division_check_soundness :=
  match goal with
  | [H: do_run_time_check_on_binop Modulus ?v1 ?v2 ?v3 |- _] =>
      specialize (binop_division_check_soundness _ _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_flagged_division_check_soundness: forall v1 v2 v3,
    evalBinOpRTS (DivCheck :: nil) Modulus v1 v2 v3 ->
      do_run_time_check_on_binop Modulus v1 v2 v3.
Proof.
  intros;
  repeat progress match goal with
    | [H: evalBinOpRTS _ _ _ _ _ |- _] => inversion H; clear H; smack
    | [H: evalBinOpRT _ _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
    | [H: divCheck _ _ _ _ |- _] => inversion H; smack
  end;
  apply DoCheckOnModulus; auto.
Qed.

Ltac apply_binop_flagged_division_check_soundness :=
  match goal with
  | [H: evalBinOpRTS (DivCheck :: nil) Modulus ?v1 ?v2 ?v3 |- _] =>
      specialize (binop_flagged_division_check_soundness _ _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_no_check_soundness: forall op v1 v2 v3,
  op <> Plus /\ op <> Minus /\ op <> Multiply /\ op <> Divide /\ op <> Modulus ->
    do_run_time_check_on_binop op v1 v2 v3 ->
      evalBinOpRTS nil op v1 v2 v3.
Proof.
  intros;
  match goal with
    | [H: do_run_time_check_on_binop _ _ _ _ |- _] =>
        inversion H; clear H; smack
  end;
  constructor; auto.
Qed.

Ltac apply_binop_no_check_soundness :=
  match goal with
  | [H1: ?op <> Plus /\ ?op <> Minus /\ ?op <> Multiply /\ ?op <> Divide /\ ?op <> Modulus,
     H2: do_run_time_check_on_binop ?op ?v1 ?v2 ?v3 |- _] =>
      specialize (binop_no_check_soundness _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma binop_no_check_flagged_soundness: forall op v1 v2 v3,
  op <> Plus /\ op <> Minus /\ op <> Multiply /\ op <> Divide /\ op <> Modulus ->
    evalBinOpRTS nil op v1 v2 v3 ->
      do_run_time_check_on_binop op v1 v2 v3.
Proof.
  intros;
  inversion H0; subst;
  constructor; smack.
Qed.

Ltac apply_binop_no_check_flagged_soundness :=
  match goal with
  | [H1: ?op <> Plus /\ ?op <> Minus /\ ?op <> Multiply /\ ?op <> Divide /\ ?op <> Modulus,
     H2: evalBinOpRTS nil ?op ?v1 ?v2 ?v3 |- _] =>
      specialize (binop_no_check_flagged_soundness _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma unop_overflow_check_soundness: forall v v',
    do_run_time_check_on_unop Unary_Minus v v' ->
      evalUnOpRTS (OverflowCheck :: nil) Unary_Minus v v'.
Proof.
  intros;
  destruct v';
  repeat progress match goal with
    | [H: do_run_time_check_on_unop _ _ _ |- _] => inversion H; clear H; smack
    | [|- evalUnOpRTS _ _ _ _] => econstructor; smack
    | [|- evalUnOpRT _ _ _ _] => econstructor; smack
    end;
  match goal with
  | [H: overflowCheck _ _ |- _] => inversion H; smack
  end.
Qed.

Ltac apply_unop_overflow_check_soundness :=
  match goal with
  | [H: do_run_time_check_on_unop Unary_Minus ?v ?v' |- _] =>
      specialize (unop_overflow_check_soundness _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma unop_flagged_overflow_check_soundness: forall v v',
    evalUnOpRTS (OverflowCheck :: nil) Unary_Minus v v' ->
      do_run_time_check_on_unop Unary_Minus v v'.
Proof.
  intros;
  inversion H;
  repeat progress match goal with
    | [H: evalUnOpRTS _ _ _ _ |- _] => inversion H; clear H; subst
    | [H: evalUnOpRT _ _ _ _ |- _] => inversion H; clear H; subst
    end.
  apply DoCheckOnUnary_Minus with (v':=v'); smack.
  apply DoCheckOnUnary_Minus with (v':=v'3); smack;
  apply_overflow_check_OK_exist_int; smack.
Qed.

Ltac apply_unop_flagged_overflow_check_soundness :=
  match goal with
  | [H: evalUnOpRTS (OverflowCheck :: nil) Unary_Minus ?v ?v' |- _] =>
      specialize (unop_flagged_overflow_check_soundness _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma unop_no_check_soundness: forall op v v',
  op <> Unary_Minus ->
    do_run_time_check_on_unop op v v' ->
      evalUnOpRTS nil op v v'.
Proof.
  intros;
  repeat progress match goal with
  | [H: do_run_time_check_on_unop _ _ _ |- _] => inversion H; clear H; smack
  | [|- evalUnOpRTS _ _ _ _] => constructor; smack
  end.
Qed.

Ltac apply_unop_no_check_soundness :=
  match goal with
  | [H1: ?op <> Unary_Minus,
     H2: do_run_time_check_on_unop ?op ?v ?v' |- _] =>
      specialize (unop_no_check_soundness _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma unop_no_check_flagged_soundness: forall op v v',
  op <> Unary_Minus ->
    evalUnOpRTS nil op v v' ->
      do_run_time_check_on_unop op v v'.
Proof.
  intros;
  inversion H0; subst;
  constructor; auto.
Qed.

Ltac apply_unop_no_check_flagged_soundness :=
  match goal with
  | [H1: ?op <> Unary_Minus,
     H2: evalUnOpRTS nil ?op ?v ?v' |- _] =>
      specialize (unop_no_check_flagged_soundness _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  end.


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

Lemma toExpRT_soundness: forall e e' st st' s v,
  evalExpRT st' s e' v ->
    toExpRT st e e' ->
      toSymTabRT st st' ->
        evalExp st s e v.
Proof.
  apply (expression_ind
    (fun e: exp => forall (e' : expRT) (st: symTab) (st': symTabRT) (s : STACK.state) (v: Ret value),
      evalExpRT st' s e' v ->
      toExpRT st e e' ->
      toSymTabRT st st' ->
      evalExp st s e v)
    (fun n: name => forall (n': nameRT) (st: symTab) (st': symTabRT) (s : STACK.state) (v: Ret value),
      evalNameRT st' s n' v ->
      toNameRT st n n' ->
      toSymTabRT st st' ->
      evalName st s n v)
    ); smack.
  -
  match goal with
  | [H: toExpRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalExpRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  constructor; auto;
  repeat progress match goal with
    | [H: evalLiteralRT _ _ _ |- _] => inversion H; clear H; smack
    | [H: overflowChecks _ _ _ |- _] => inversion H; clear H; smack
    | [H: overflowCheck _ _ |- _] => inversion H; clear H; smack
    end;
  repeat progress match goal with
    | [|- evalLiteral _ _] => constructor
    | [|- overflowCheck _ _] => constructor; smack
    end;
  repeat progress match goal with
  | [H: in_bound _ _ _ |- _] => inversion H; clear H; smack
  end.
  -
  match goal with
  | [H: toExpRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalExpRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  constructor; auto;
  apply H with (n':=nRT) (st':=st'); auto.
  -
  match goal with
  | [H: toExpRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalExpRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  repeat progress match goal with
  | [H1: forall (e' : expRT) (st : symTab)
        (st' : symTabRT) (s : STACK.state) (v : Ret value),
      evalExpRT st' s e' v ->
      toExpRT st ?e e' ->
      toSymTabRT st st' -> evalExp st s ?e v,
     H2: evalExpRT _ _ ?e' _,
     H3: toExpRT _ _ ?e',
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4); smack
  end;
  match goal with
  | [H1: evalExpRT _ _ ?e (OK _),
     H2: evalExpRT _ _ ?e0 (RTE _) |- _] =>
      apply EvalBinOpE2_RTE with (v1 := v1); auto
  | [H1: evalExpRT _ _ ?e (OK _),
     H2: evalExpRT _ _ ?e0 (OK _) |- _] =>
      apply EvalBinOp with (v1 := v1) (v2 := v2); auto
  | [H: evalExpRT _ _ ?e (RTE _) |- _] =>
      constructor; auto
  | _ => idtac
  end;
  match goal with
  | [ |- do_run_time_check_on_binop Divide _ _ _ ] =>
      apply binop_flagged_overflow_division_check_soundness; smack
  | [ |- do_run_time_check_on_binop Modulus _ _ _ ] =>
      apply binop_flagged_division_check_soundness; smack
  | [H: ?op = Plus -> False |- _] => apply binop_no_check_flagged_soundness; smack
  | _ => apply binop_flagged_overflow_check_soundness; smack
  end.
  -
  match goal with
  | [H: toExpRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalExpRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H1: forall (e' : expRT) (st : symTab)
        (st' : symTabRT) (s : STACK.state) (v : Ret value),
      evalExpRT st' s e' v ->
      toExpRT st ?e e' ->
      toSymTabRT st st' -> evalExp st s ?e v,
     H2: evalExpRT _ _ ?e' _,
     H3: toExpRT _ _ ?e',
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4); smack
  end;
  match goal with
  | [H: evalExpRT _ _ ?e (RTE _) |- _] =>
      constructor; auto
  | [H1: evalExpRT _ _ ?e (OK ?v1) |- _] =>
      apply EvalUnOp with (v := v1); auto
  end;
  [ apply unop_flagged_overflow_check_soundness; auto |
    apply unop_no_check_flagged_soundness; auto
  ].
  -
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalNameRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  constructor; auto.
  -
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalNameRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H1: forall (n' : nameRT) (st : symTab) (st' : symTabRT)
        (s : STACK.state) (v : Ret value),
      evalNameRT st' s n' v ->
      toNameRT st ?n n' ->
      toSymTabRT st st' -> evalName st s ?n v,
     H2: evalNameRT _ _ ?n1 _,
     H3: toNameRT _ _ ?n1,
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4); smack
  end;
  try
  match goal with
  | [H1: forall (e' : expRT) (st : symTab)
        (st' : symTabRT) (s : STACK.state) (v : Ret value),
      evalExpRT st' s e' v ->
      toExpRT st ?e e' ->
      toSymTabRT st st' -> evalExp st s ?e v,
     H2: evalExpRT _ _ ?e' _,
     H3: toExpRT _ _ ?e',
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4); smack
  end.
  + apply EvalIndexedComponentX_RTE; auto.
  + apply EvalIndexedComponentE_RTE with (a:=a0); auto.
    apply H0 with (e':=eRT) (st':=st'); auto.
    eapply eval_exp_ex_cks_stripped; smack.
  + apply EvalIndexedComponent_Range_RTE with (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u); smack.
    apply H0 with (e':=eRT) (st':=st'); auto.
    eapply eval_exp_ex_cks_stripped; smack.
    rewrite (name_ast_num_eq _ _ _ H10);
    specialize (symbol_table_exp_type_eq _ _ (name_astnum_rt xRT) H3); smack.
    apply index_range_rel_backward with (st' := st'); auto.
    rewrite exp_updated_exterior_checks in H16; constructor; auto.
    repeat progress match goal with
    | [H: rangeChecks _ _ _ _ _ |- _] => inversion H; clear H; subst
    | [H: rangeCheck _ _ _ _ |- _] => inversion H; clear H; subst
    end; auto.
  + apply EvalIndexedComponent with (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u); smack.
    apply H0 with (e':=eRT) (st':=st'); auto.
    eapply eval_exp_ex_cks_stripped; smack.
    rewrite (name_ast_num_eq _ _ _ H10);
    specialize (symbol_table_exp_type_eq _ _ (name_astnum_rt xRT) H3); smack.
    apply index_range_rel_backward with (st' := st'); auto.
    rewrite exp_updated_exterior_checks in H16; constructor; auto.
    repeat progress match goal with
    | [H: rangeChecks _ _ _ _ _ |- _] => inversion H; clear H; subst
    | [H: rangeCheck _ _ _ _ |- _] => inversion H; clear H; subst
    end; auto.
  -
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalNameRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H1: forall (n' : nameRT) (st : symTab) (st' : symTabRT)
        (s : STACK.state) (v : Ret value),
      evalNameRT st' s n' v ->
      toNameRT st ?n n' ->
      toSymTabRT st st' -> evalName st s ?n v,
     H2: evalNameRT _ _ ?n1 _,
     H3: toNameRT _ _ ?n1,
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4); smack
  end;
  [ apply EvalSelectedComponentX_RTE; auto |
    apply EvalSelectedComponent with (r := r); auto
  ].
Qed.

Ltac apply_toExpRT_soundness :=
  match goal with
  | [H1: evalExpRT ?st' ?s ?e' ?v,
     H2: toExpRT ?st ?e ?e',
     H3: toSymTabRT ?st ?st' |- _] =>
      specialize (toExpRT_soundness _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma toNameRT_soundness: forall n n' st st' s v,
  evalNameRT st' s n' v ->
    toNameRT st n n' ->
      toSymTabRT st st' ->
        evalName st s n v.
Proof.
  induction n; smack.
  -
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalNameRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  constructor; auto.
  -
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalNameRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H1: forall (n' : nameRT) (st : symTab)
        (st' : symTabRT) (s : STACK.state) (v : Ret value),
      evalNameRT _ _ ?n _ ->
      toNameRT _ _ ?n ->
      toSymTabRT _ _ -> evalName _ _ _ _,
     H2: evalNameRT _ _ ?n1 _,
     H3: toNameRT _ _ ?n1,
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4)
  end;
  match goal with
  | [H1: evalExpRT _ _ (update_exterior_checks_exp _ _) _ |- _] =>
      specialize (eval_exp_ex_cks_stripped _ _ _ _ _ H1); intro HZ;
       apply_toExpRT_soundness
  | _ => idtac
  end.
  apply EvalIndexedComponentX_RTE; auto.
  apply EvalIndexedComponentE_RTE with (a:=a0); auto.
  apply EvalIndexedComponent_Range_RTE with (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u); smack.
    rewrite (name_ast_num_eq _ _ _ H8).
      specialize (symbol_table_exp_type_eq _ _ (name_astnum_rt xRT) H1); smack.
    apply index_range_rel_backward with (st' := st'); auto.
    rewrite exp_updated_exterior_checks in H14; constructor; auto.
    repeat progress match goal with
    | [H: rangeChecks _ _ _ _ _ |- _] => inversion H; clear H; subst
    | [H: rangeCheck _ _ _ _ |- _] => inversion H; clear H; subst
    end; auto.
  apply EvalIndexedComponent with (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u); smack.
    rewrite (name_ast_num_eq _ _ _ H8);
      specialize (symbol_table_exp_type_eq _ _ (name_astnum_rt xRT) H1); smack.
    apply index_range_rel_backward with (st' := st'); auto.
    rewrite exp_updated_exterior_checks in H14; constructor; auto.
    repeat progress match goal with
    | [H: rangeChecks _ _ _ _ _ |- _] => inversion H; clear H; subst
    | [H: rangeCheck _ _ _ _ |- _] => inversion H; clear H; subst
    end; auto.
  -
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: evalNameRT _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H1: forall (n' : nameRT) (st : symTab)
        (st' : symTabRT) (s : STACK.state) (v : Ret value),
      evalNameRT _ _ ?n _ ->
      toNameRT _ _ ?n ->
      toSymTabRT _ _ -> evalName _ _ _ _,
     H2: evalNameRT _ _ ?n1 _,
     H3: toNameRT _ _ ?n1,
     H4: toSymTabRT _ _ |- _] =>
      specialize (H1 _ _ _ _ _ H2 H3 H4)
  end;
  [ apply EvalSelectedComponentX_RTE; auto |
    apply EvalSelectedComponent with (r := r); auto
  ].
Qed.

Ltac apply_toNameRT_soundness :=
  match goal with
  | [H1: evalNameRT ?st' ?s ?n' ?v,
     H2: toNameRT ?st ?n ?n',
     H3: toSymTabRT ?st ?st' |- _ ] =>
      specialize (toNameRT_soundness _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma toDeclRT_soundness: forall st s f d f' d' st',
  evalDeclRT st' s f d' f' ->
    toDeclRT st d d' ->
      toSymTabRT st st' ->
        evalDecl st s f d f'.
Proof.
  intros st s f d f' d' st' H; revert d st;
  induction H; intros;
  match goal with
  | [H: toDeclRT _ _ _ |- _] => inversion H; clear H; smack
  end;
  match goal with
  | [H: toObjDeclRT _ _ _ |- _] => inversion H; clear H; smack
  | _ => idtac
  end;
  match goal with
  | [H1: is_range_constrainted_type ?t = false,
     H2: extract_subtype_range_rt _ ?t (RangeRT _ _) |- _] =>
      destruct t; inversion H2; smack
  | _ => idtac
  end;
  match goal with
  | [ H: context[exp_exterior_checks (update_exterior_checks_exp _ _)] |- _] =>
      rewrite exp_updated_exterior_checks in H; inversion H; subst
  | _ => idtac
  end;
  try (apply_eval_exp_ex_cks_stripped);
  try (apply_eval_name_ex_cks_stripped);
  try (apply_toExpRT_soundness);
  [ apply EvalDecl_Null |
    apply EvalDecl_Var_None; auto |
    apply EvalDecl_Var_RTE with (e:=e0); smack |
    apply EvalDecl_Var_RTE with (e:=e0); smack |
    apply EvalDecl_Var with (e:=e0); auto |
    apply EvalDecl_Var_Range_RTE with (e:=e0) (v:=v) (l:=l) (u:=u); smack;
      apply subtype_range_rel_backward with (st':=st); auto |
    apply EvalDecl_Var_Range with (e:=e0) (l:=l) (u:=u); smack;
      apply subtype_range_rel_backward with (st':=st); auto |
    apply EvalDecl_Type |
    apply EvalDecl_Proc |
    apply EvalDecl_Seq_RTE; auto |
    apply EvalDecl_Seq with (f':=f'); auto
  ].
Qed.

Ltac apply_toDeclRT_soundness :=
  match goal with
  | [H1: evalDeclRT ?st' ?s ?f ?d' ?f',
     H2: toDeclRT ?st ?d ?d',
     H3: toSymTabRT ?st ?st' |- _] =>
      specialize (toDeclRT_soundness _ _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma storeUpdateRT_soundness: forall st s x v s' x' st',
  storeUpdateRT st' s x' v s' ->
    toNameRT st x x' ->
      toSymTabRT st st' ->
        storeUpdate st s x v s'.
Proof.
  intros st s x;
  induction x; smack;
  match goal with
  | [H: toNameRT _ _ _ |- _] => inversion H; subst
  end.
- match goal with
  | [H: storeUpdateRT _ _ _ _ _ |- _] => inversion H; clear H; subst
  end; constructor; auto.
- match goal with
  | [H: storeUpdateRT _ _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  try (apply_eval_exp_ex_cks_stripped);
  try (apply_toNameRT_soundness; smack);
  try (apply_toExpRT_soundness; smack);
  match goal with
  | [H1: storeUpdateRT _ _ ?x _ _ ,
     H2: toNameRT _ _ ?x ,
     H3: toSymTabRT _ _ |- _ ] => specialize (IHx _ _ _ _ H1 H2 H3)
  | _ => idtac
  end;
  match goal with
  | [ H: context[exp_exterior_checks (update_exterior_checks_exp _ _)] |- _] =>
      rewrite exp_updated_exterior_checks in H; inversion H; subst
  | _ => idtac
  end;
  [ apply SU_Indexed_Component_xRTE; auto |
    apply SU_Indexed_Component_eRTE with (a:=a0); auto |
    apply SU_Indexed_Component_eRTE with (a:=a0); auto |
    apply SU_Indexed_Component_Range_RTE with (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u); auto |
    apply SU_Indexed_Component_Range_RTE with (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u); auto |
    apply SU_Indexed_Component with (arrObj:=ArrayV a0) (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u) (a1:=(updateIndexedComp a0 i v)); auto |
    apply SU_Indexed_Component with (arrObj:=Undefined) (a:=a0) (i:=i) (t:=t) (l:=l) (u:=u) (a1:=((i, v) :: nil)); auto
  ];
  solve [
    match goal with
    | [H1: toSymTabRT _ _,
       H2: toNameRT ?st0 ?x ?x' |- context[fetch_exp_type (name_astnum ?x) _]] =>
        rewrite (name_ast_num_eq _ _ _ H2);
        specialize (symbol_table_exp_type_eq _ _ (name_astnum_rt x') H1); smack
    end |
    apply index_range_rel_backward with (st':=st'); auto
  ].
- match goal with
  | [H: storeUpdateRT _ _ _ _ _ |- _] => inversion H; clear H; smack
  end;
  try (apply_toNameRT_soundness; smack);
  match goal with
  | [H1: storeUpdateRT _ _ ?x _ _ ,
     H2: toNameRT _ _ ?x ,
     H3: toSymTabRT _ _ |- _ ] => specialize (IHx _ _ _ _ H1 H2 H3)
  | _ => idtac
  end;
  [ apply SU_Selected_Component_xRTE; auto |
    apply SU_Selected_Component with (recObj:=(RecordV r)) (r:=r) (r1:=(updateSelectedComp r i v)); auto |
    apply SU_Selected_Component with (recObj:=Undefined) (r:=r) (r1:=((i, v) :: nil)); auto
  ].
Qed.

Ltac apply_storeUpdateRT_soundness :=
  match goal with
  | [H1: storeUpdateRT ?st' ?s ?x' ?v ?s',
     H2: toNameRT ?st ?x ?x',
     H3: toSymTabRT ?st ?st' |- _ ] =>
      specialize (storeUpdateRT_soundness _ _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma copyInRT_soundness: forall params st s f args f' params' args' st',
  copyInRT st' s f params' args' f' ->
    toParamSpecsRT params params' ->
      toArgsRT st params args args' ->
        toSymTabRT st st' ->
          copyIn st s f params args f'.
Proof.
  induction params; smack.
- inversion H0; inversion H1; subst;
  inversion H; subst; constructor.
- destruct args, args', params';
  match goal with
  | [H: copyInRT _ _ _ (?a :: ?al) nil _ |- _] => inversion H
  | [H: copyInRT _ _ _ nil (?a :: ?al) _ |- _] => inversion H
  | [H: toArgsRT _ (?a :: ?al) nil _ |- _] => inversion H
  | [H: toParamSpecsRT (?param :: ?params) nil |- _] => inversion H
  | _ => idtac
  end.
  inversion H0; clear H0; subst.
  assert(HZ1: p.(parameter_nameRT) = a.(parameter_name)).
    inversion H6; smack.
  assert(HZ2: p.(parameter_mode_rt) = a.(parameter_mode)).
    inversion H6; smack.
  assert (HZ3: p.(parameter_subtype_mark_rt) = a.(parameter_subtype_mark)).
    inversion H6; smack.
  inversion H1; clear H1; subst;
  inversion H; clear H; subst; smack;
  try (rewrite HZ1 in *); try (rewrite HZ3 in *);
  match goal with
  | [H1: is_range_constrainted_type ?t = false,
     H2: extract_subtype_range_rt _ ?t (RangeRT _ _) |- _] =>
      destruct t; inversion H2; smack
  | _ => idtac
  end;
  try (apply_toExpRT_soundness; smack);
  try (apply_toNameRT_soundness; smack);
  match goal with
  | [H1: copyInRT _ _ _ ?params' ?args' ?f',
     H2: toParamSpecsRT ?params ?params',
     H3: toArgsRT ?st ?params ?args ?args',
     H4: toSymTabRT _ _ |- _] =>
      specialize (IHparams _ _ _ _ _ _ _ _ H1 H2 H3 H4)
  | _ => idtac
  end;
  match goal with
  | [ H: context[exp_exterior_checks (update_exterior_checks_exp _ _)] |- _] =>
      rewrite exp_updated_exterior_checks in H; smack
  | [ H: context[name_exterior_checks (update_exterior_checks_name _ _)] |- _] =>
      rewrite name_updated_exterior_checks in H; smack
  | _ => idtac
  end;
  match goal with
  | [H1: evalExpRT _ _ (update_exterior_checks_exp _ _) _ |- _] =>
      specialize (eval_exp_ex_cks_stripped _ _ _ _ _ H1); let HZ := fresh "HZ" in intro HZ;
       apply_toExpRT_soundness
  | [H1: evalNameRT _ _ (update_exterior_checks_name _ _) _ |- _] =>
      specialize (eval_name_ex_cks_stripped _ _ _ _ _ H1); let HZ := fresh "HZ" in intro HZ;
       apply_toNameRT_soundness
  | _ => idtac
  end;
  match goal with
  | [H1: toSymTabRT ?st ?st',
     H2: extract_subtype_range_rt ?st' ?t (RangeRT ?l ?u) |- _] =>
      specialize (subtype_range_rel_backward _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ
  | _ => idtac
  end;
  [ apply CopyIn_Mode_In_eRTE; smack |
    apply CopyIn_Mode_In_NoRange with (v:=v) (f':=(STACK.push f (parameter_name a) v)); smack |
    apply CopyIn_Mode_In_eRTE; smack |
    apply CopyIn_Mode_In_Range_RTE with (v:=v) (l:=l) (u:=u); smack |
    apply CopyIn_Mode_In_Range with (v:=v) (l:=l) (u:=u) (f':=(STACK.push f (parameter_name a) (Int v))); smack |
    apply CopyIn_Mode_Out with (f':=(STACK.push f (parameter_name a) Undefined)); smack |
    apply CopyIn_Mode_Out with (f':=(STACK.push f (parameter_name a) Undefined)); smack |
    apply CopyIn_Mode_InOut_eRTE; smack |
    apply CopyIn_Mode_InOut_NoRange with (v:=v) (f':=(STACK.push f (parameter_name a) v)); smack |
    apply CopyIn_Mode_InOut_eRTE; smack |
    apply CopyIn_Mode_InOut_Range_RTE with (v:=v) (l:=l) (u:=u); smack |
    apply CopyIn_Mode_InOut_Range with (v:=v) (l:=l) (u:=u) (f':=(STACK.push f (parameter_name a) (Int v))); smack |
    apply CopyIn_Mode_InOut_eRTE; smack |
    apply CopyIn_Mode_InOut_NoRange with (v:=v) (f':=(STACK.push f (parameter_name a) v)); smack |
    apply CopyIn_Mode_InOut_eRTE; smack |
    apply CopyIn_Mode_InOut_Range_RTE with (v:=v) (l:=l) (u:=u); smack |
    apply CopyIn_Mode_InOut_Range with (v:=v) (l:=l) (u:=u) (f':=(STACK.push f (parameter_name a) (Int v))); smack
  ].
Qed.

Ltac apply_copyInRT_soundness :=
  match goal with
  | [H1: copyInRT ?st' ?s ?f ?params' ?args' ?f',
     H2: toParamSpecsRT ?params ?params',
     H3: toArgsRT ?st ?params ?args ?args',
     H4: toSymTabRT ?st ?st' |- _] =>
      specialize (copyInRT_soundness _ _ _ _ _ _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma copyOutRT_soundness: forall params st s f args f' params' args' st',
  copyOutRT st' s f params' args' f' ->
    toParamSpecsRT params params' ->
      toArgsRT st params args args' ->
        toSymTabRT st st' ->
          copyOut st s f params args f'.
Proof.
  induction params; smack.
- inversion H0; inversion H1; subst; inversion H;
  constructor.
- destruct args, args', params';
  match goal with
  | [H: copyOutRT _ _ _ (?a :: ?al) nil _ |- _] => inversion H
  | [H: copyOutRT _ _ _ nil (?a :: ?al) _ |- _] => inversion H
  | [H: toArgsRT _ (?a :: ?al) nil _ |- _] => inversion H
  | [H: toParamSpecsRT (?param :: ?params) nil |- _] => inversion H
  | _ => idtac
  end.
  inversion H0; clear H0; subst.
  assert(HZ1: p.(parameter_nameRT) = a.(parameter_name)).
    inversion H6; smack.
  assert(HZ2: p.(parameter_mode_rt) = a.(parameter_mode)).
    inversion H6; smack.
  assert (HZ3: p.(parameter_subtype_mark_rt) = a.(parameter_subtype_mark)).
    inversion H6; smack.

  inversion H1; clear H1; subst;
  inversion H; clear H; subst; smack;
  try (rewrite HZ1 in *); try (rewrite HZ3 in *);
  match goal with
  | [H: parameter_mode ?x = In |- _] => apply CopyOut_Mode_In; smack
  | _ => idtac
  end;
  match goal with
  | [H1: fetch_exp_type ?x ?st = Some ?t, H2: fetch_exp_type_rt ?x ?st' = Some ?t0,
     H3: toSymTabRT ?st ?st' |- _] =>
      rewrite (symbol_table_exp_type_eq _ _ x H3) in H1;
      rewrite H1 in H2; inversion H2; subst
  | _ => idtac
  end;
  match goal with
  | [H1: is_range_constrainted_type ?t = false,
     H2: extract_subtype_range_rt _ ?t (RangeRT _ _) |- _] =>
      destruct t; inversion H2; smack
  | _ => idtac
  end;
  match goal with
  | [H1: copyOutRT ?st' ?s ?f ?params' ?args' ?f',
     H2: toParamSpecsRT ?params ?params',
     H3: toArgsRT st params ?args ?args',
     H4: toSymTabRT _ _ |- _] =>
      specialize (IHparams _ _ _ _ _ _ _ _ H1 H2 H3 H4)
  | _ => idtac
  end;
  match goal with
  | [ H: context[exp_exterior_checks (update_exterior_checks_exp _ _)] |- _] =>
      rewrite exp_updated_exterior_checks in H; smack
  | [ H: context[name_exterior_checks (update_exterior_checks_name _ _)] |- _] =>
      rewrite name_updated_exterior_checks in H; smack
  | _ => idtac
  end;
  match goal with
  | [H1: toSymTabRT _ _ |- context[fetch_exp_type ?ast_num _]] =>
      specialize (symbol_table_exp_type_eq _ _ ast_num H1); let HZ := fresh "HZ" in intro HZ
  | _ => idtac
  end;
  try (apply_store_update_ex_cks_stripped);
  try (apply_storeUpdateRT_soundness);
  [ apply CopyOut_Mode_Out_nRTE with (v:=v) (t:=t); smack |
    apply CopyOut_Mode_Out_NoRange with (v:=v) (s':=s') (t:=t); smack |
    apply CopyOut_Mode_Out_Range_RTE with (v:=v) (t:=t0) (l:=l) (u:=u); smack |
    apply CopyOut_Mode_Out_Range_nRTE with (v:=v) (t:=t0) (l:=l) (u:=u); smack |
    apply CopyOut_Mode_Out_Range with (v:=v) (t:=t0) (l:=l) (u:=u) (s':=s'); smack |
    apply CopyOut_Mode_Out_nRTE with (v:=v) (t:=t); smack |
    apply CopyOut_Mode_Out_NoRange with (v:=v) (s':=s') (t:=t); smack |
    apply CopyOut_Mode_Out_nRTE with (v:=v) (t:=t); smack |
    apply CopyOut_Mode_Out_NoRange with (v:=v) (s':=s') (t:=t); smack |
    apply CopyOut_Mode_Out_Range_RTE with (v:=v) (t:=t0) (l:=l) (u:=u); smack |
    apply CopyOut_Mode_Out_Range_nRTE with (v:=v) (t:=t0) (l:=l) (u:=u); smack |
    apply CopyOut_Mode_Out_Range with (v:=v) (t:=t0) (l:=l) (u:=u) (s':=s'); smack |
    apply CopyOut_Mode_Out_Range_RTE with (v:=v) (t:=t0) (l:=l) (u:=u); smack |
    apply CopyOut_Mode_Out_Range_nRTE with (v:=v) (t:=t0) (l:=l) (u:=u); smack |
    apply CopyOut_Mode_Out_Range with (v:=v) (t:=t0) (l:=l) (u:=u) (s':=s'); smack
  ];
  match goal with
  | [H1: toSymTabRT _ _ |- context[fetch_exp_type ?ast_num _]] =>
      rewrite (symbol_table_exp_type_eq _ _ ast_num H1); smack
  | [H1: toSymTabRT ?st ?st',
     H2: extract_subtype_range_rt ?st' ?t (RangeRT ?l ?u) |- _] =>
      specialize (subtype_range_rel_backward _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; auto
  | _ => idtac
  end.
Qed.

Ltac apply_copyOutRT_soundness :=
  match goal with
  | [H1: copyOutRT ?st' ?s ?f ?params' ?args' ?f',
     H2: toParamSpecsRT ?params ?params',
     H3: toArgsRT ?st ?params ?args ?args',
     H4: toSymTabRT ?st ?st' |- _ ] =>
      specialize (copyOutRT_soundness _ _ _ _ _ _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma toAssignStmtRT_soundness: forall st s n x e s' stmt' st',
  evalStmtRT st' s stmt' s' ->
    toStmtRT st (Assign n x e) stmt' ->
      toSymTabRT st st' ->
        evalStmt st s (Assign n x e) s'.
Proof.
  intros.
  inversion H0; inversion H; subst; clear H0 H;
  match goal with
  | [H: _ = AssignRT _ _ _ |- _] => inversion H; subst
  | _ => idtac
  end;
  match goal with
  | [H: toNameRT ?st ?x ?x' |- _] =>
      specialize (name_ast_num_eq _ _ _ H); let HZ := fresh "HZ" in intro HZ;
      try (rewrite HZ in *)
  end;
  match goal with
  | [H1: toSymTabRT ?st ?st',
     H2: fetch_exp_type ?x ?st = Some ?t |- _] =>
      specialize (symbol_table_exp_type_eq _ _ x H1);
      let HZ := fresh "HZ" in intro HZ
  end;
  match goal with
  | [H1: fetch_exp_type ?x ?st = fetch_exp_type_rt ?x' ?st',
     H2: fetch_exp_type ?x ?st = Some ?t,
     H3: fetch_exp_type_rt ?x ?st' = Some ?t' |- _] =>
      rewrite H2 in H1; rewrite H3 in H1; inversion H1; subst
  | _ => idtac
  end;

  match goal with
  | [H1: is_range_constrainted_type ?t = false,
     H2: extract_subtype_range_rt _ ?t (RangeRT _ _) |- _] =>
      destruct t; inversion H2; smack
  | _ => idtac
  end;
  match goal with
  | [ H: context[exp_exterior_checks (update_exterior_checks_exp _ _)] |- _] =>
      rewrite exp_updated_exterior_checks in H; smack
  | [ H: context[name_exterior_checks (update_exterior_checks_name _ _)] |- _] =>
      rewrite name_updated_exterior_checks in H; smack
  | _ => idtac
  end;
  match goal with
  | [H1: evalExpRT _ _ (update_exterior_checks_exp _ _) _ |- _] =>
      specialize (eval_exp_ex_cks_stripped _ _ _ _ _ H1); let HZ := fresh "HZ" in intro HZ;
       apply_toExpRT_soundness
  | [H1: evalNameRT _ _ (update_exterior_checks_name _ _) _ |- _] =>
      specialize (eval_name_ex_cks_stripped _ _ _ _ _ H1); let HZ := fresh "HZ" in intro HZ;
       apply_toNameRT_soundness
  | _ => idtac
  end;
  try (apply_toExpRT_soundness; smack);
  try (apply_storeUpdateRT_soundness; smack);
  [ apply EvalAssign_RTE; auto |
    apply EvalAssign with (v:=v) (t:=t); auto |
    apply EvalAssign_RTE; auto |
    apply EvalAssign_Range_RTE with (v:=v) (t:=t0) (l:=l) (u:=u); auto |
    apply EvalAssign_Range with (v:=v) (t:=t0) (l:=l) (u:=u); auto
  ];
  match goal with
  | [H1: toSymTabRT _ _ |- context[fetch_exp_type ?n _]] =>
      rewrite (symbol_table_exp_type_eq _ _ n H1); smack
  | [H1: toSymTabRT ?st ?st',
     H2: extract_subtype_range_rt ?st' ?t (RangeRT ?l ?u) |- _] =>
      specialize (subtype_range_rel_backward _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intro HZ; auto
  | _ => idtac
  end.
Qed.

Ltac apply_toAssignStmtRT_soundness :=
  match goal with
  | [H1: evalStmtRT ?st' ?s ?stmt' ?s',
     H2: toStmtRT ?st (Assign ?n ?x ?e) ?stmt',
     H3: toSymTabRT ?st ?st' |- _ ] =>
      specialize (toAssignStmtRT_soundness _ _ _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma toStmtRT_soundness: forall st s stmt s' stmt' st',
  evalStmtRT st' s stmt' s' ->
    toStmtRT st stmt stmt' ->
      toSymTabRT st st' ->
        evalStmt st s stmt s'.
Proof.
  intros st s stmt s' stmt' st' H; revert stmt st;
  induction H; intros.
-
  inversion H; subst;
  constructor.
-
  match goal with
  | [H: toStmtRT ?st0 ?stmt (AssignRT _ _ _) |- _] => inversion H; subst
  end;
  match goal with
  | [H1: evalExpRT _ _ (update_exterior_checks_exp _ _) _ |- _] =>
      specialize (eval_exp_ex_cks_stripped _ _ _ _ _ H1); intro HZ
  | _ => idtac
  end;
  [ apply toAssignStmtRT_soundness with (st':=st) (stmt' := (AssignRT n x e)); smack |
    apply toAssignStmtRT_soundness with (st':=st) (stmt' := ((AssignRT n x
            (update_exterior_checks_exp eRT (RangeCheck :: nil))))); smack
  ];
  apply EvalAssignRT_RTE; auto.
-
  match goal with
  | [H: toStmtRT ?st0 ?stmt (AssignRT _ _ _) |- _] => inversion H; subst
  end;
  match goal with
  | [ H: context[exp_exterior_checks (update_exterior_checks_exp _ _)] |- _] =>
      rewrite exp_updated_exterior_checks in H; inversion H; subst
  | _ => idtac
  end.
  apply toAssignStmtRT_soundness with (st':=st) (stmt' := (AssignRT n x e)); smack.
  apply EvalAssignRT with (v:=v); auto.
-
  match goal with
  | [H: toStmtRT ?st0 ?stmt (AssignRT _ _ _) |- _] => inversion H; subst
  end.
  match goal with
  | [H: toNameRT ?st ?x ?x' |- _] =>
      specialize (name_ast_num_eq _ _ _ H); let HZ := fresh "HZ" in intro HZ;
      try (rewrite HZ in *)
  end;
  match goal with
  | [H1: toSymTabRT ?st ?st',
     H2: fetch_exp_type ?x ?st = Some ?t |- _] =>
      specialize (symbol_table_exp_type_eq _ _ x H1);
      let HZ := fresh "HZ" in intro HZ
  end;
  match goal with
  | [H1: fetch_exp_type ?x ?st = fetch_exp_type_rt ?x' ?st',
     H2: fetch_exp_type ?x ?st = Some ?t,
     H3: fetch_exp_type_rt ?x ?st' = Some ?t' |- _] =>
      rewrite H2 in H1; rewrite H3 in H1; inversion H1; subst
  end;
  match goal with
  | [H1: is_range_constrainted_type ?t = false,
     H2: extract_subtype_range_rt _ ?t (RangeRT _ _) |- _] =>
      destruct t; inversion H2; smack
  | _ => idtac
  end.
  apply toAssignStmtRT_soundness with (st':=st) (stmt' := (AssignRT n x
            (update_exterior_checks_exp eRT (RangeCheck :: nil)))); smack.
  apply EvalAssignRT_Range_RTE with (v:=v) (t:=t) (l:=l) (u:=u); auto.
-
  match goal with
  | [H: toStmtRT ?st0 ?stmt (AssignRT _ _ _) |- _] => inversion H; subst
  end.
  match goal with
  | [H: toNameRT ?st ?x ?x' |- _] =>
      specialize (name_ast_num_eq _ _ _ H); let HZ := fresh "HZ" in intro HZ;
      try (rewrite HZ in *)
  end;
  match goal with
  | [H1: toSymTabRT ?st ?st',
     H2: fetch_exp_type ?x ?st = Some ?t |- _] =>
      specialize (symbol_table_exp_type_eq _ _ x H1);
      let HZ := fresh "HZ" in intro HZ
  end;
  match goal with
  | [H1: fetch_exp_type ?x ?st = fetch_exp_type_rt ?x' ?st',
     H2: fetch_exp_type ?x ?st = Some ?t,
     H3: fetch_exp_type_rt ?x ?st' = Some ?t' |- _] =>
      rewrite H2 in H1; rewrite H3 in H1; inversion H1; subst
  end;
  match goal with
  | [H1: is_range_constrainted_type ?t = false,
     H2: extract_subtype_range_rt _ ?t (RangeRT _ _) |- _] =>
      destruct t; inversion H2; smack
  | _ => idtac
  end.
  apply toAssignStmtRT_soundness with (st':=st) (stmt' := (AssignRT n x
            (update_exterior_checks_exp eRT (RangeCheck :: nil)))); smack.
  apply EvalAssignRT_Range with (v:=v) (t:=t) (l:=l) (u:=u); auto.
-
  inversion H0; clear H0; subst.
  apply EvalIf_RTE;
  apply_toExpRT_soundness; auto.
-
  inversion H1; clear H1; subst;
  apply EvalIf_True;
  apply_toExpRT_soundness; auto.
-
  inversion H1; clear H1; subst;
  apply EvalIf_False;
  apply_toExpRT_soundness; auto.
-
  inversion H0; clear H0; subst;
  apply EvalWhile_RTE;
  apply_toExpRT_soundness; auto.
-
  inversion H1; clear H1; subst;
  apply EvalWhile_True_RTE;
  apply_toExpRT_soundness; auto.
-
  inversion H2; clear H2; subst;
  apply EvalWhile_True with (s1:=s1);
  apply_toExpRT_soundness; auto.
  specialize (IHevalStmtRT1 _ _ H10 H3).
  apply IHevalStmtRT2; smack.
  constructor; auto.
-
  inversion H0; clear H0; subst;
  apply EvalWhile_False;
  apply_toExpRT_soundness; auto.
-
  inversion H1; subst.
  specialize (symbol_table_procedure_rel_backward _ _ _ _ _ H2 H); smack.
  match goal with
  | [H1: fetch_proc ?p ?st0 = Some _, H2: fetch_proc ?p ?st0 = Some _ |- _] =>
      rewrite H2 in H1; inversion H1; subst
  end.
  specialize (procedure_components_rel _ _ _ H5); smack.
  apply_copyInRT_soundness.
  apply EvalCall_Args_RTE with (n0:=n1) (pb:=pb0); smack.
-
  inversion H3; subst.
  specialize (symbol_table_procedure_rel_backward _ _ _ _ _ H4 H); smack.
  match goal with
  | [H1: fetch_proc ?p ?st0 = Some _, H2: fetch_proc ?p ?st0 = Some _ |- _] =>
      rewrite H2 in H1; inversion H1; subst
  end.
  specialize (procedure_components_rel _ _ _ H7); smack.
  apply_copyInRT_soundness.
  apply_toDeclRT_soundness.
  apply EvalCall_Decl_RTE with (n0:=n1) (pb:=pb0) (f:=f) (intact_s:=intact_s) (s1:=s1); smack.
-
  inversion H4; subst.
  specialize (symbol_table_procedure_rel_backward _ _ _ _ _ H5 H); smack.
  match goal with
  | [H1: fetch_proc ?p ?st0 = Some _, H2: fetch_proc ?p ?st0 = Some _ |- _] =>
      rewrite H2 in H1; inversion H1; subst
  end.
  specialize (procedure_components_rel _ _ _ H8); smack.
  apply_copyInRT_soundness.
  apply_toDeclRT_soundness.
  apply EvalCall_Body_RTE with (n0:=n1) (pb:=pb0) (f:=f) (intact_s:=intact_s) (s1:=s1) (f1:=f1); smack.
-
  inversion H7; subst.
  specialize (symbol_table_procedure_rel_backward _ _ _ _ _ H8 H); smack.
  match goal with
  | [H1: fetch_proc ?p ?st0 = Some _, H2: fetch_proc ?p ?st0 = Some _ |- _] =>
      rewrite H2 in H1; inversion H1; subst
  end.
  specialize (procedure_components_rel _ _ _ H10); smack.
  apply_copyInRT_soundness.
  apply_copyOutRT_soundness.
  apply_toDeclRT_soundness.
  specialize (IHevalStmtRT _ _ H13 H8); smack;
  apply EvalCall with (n0:=n1) (pb:=pb0) (f:=f) (intact_s:=intact_s) (s1:=s1) (f1:=f1)
                      (s2:=((n, locals_section ++ params_section) :: s3))
                      (locals_section:=locals_section) (params_section:=params_section)
                      (s3:=s3); smack.
-
  inversion H0; smack;
  apply EvalSeq_RTE;
  apply IHevalStmtRT; smack.
-
  inversion H1; smack;
  apply EvalSeq with (s1:=s1); smack.
Qed.

Ltac apply_toStmtRT_soundness :=
  match goal with
  | [H1: evalStmtRT ?st' ?s ?stmt' ?s',
     H2: toStmtRT ?st ?stmt ?stmt',
     H3: toSymTabRT ?st ?st' |- _ ] =>
      specialize (toStmtRT_soundness _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.