(*
app load ["relationTheory", "pred_setSimps","pred_setTheory","whileTheory","finite_mapTheory","rich_listTheory", "listSyntax", 
          "ILTheory", "rulesTheory", "preARMSyntax", "annotatedIL", "funCall"];

quietdec := true;
open HolKernel Parse boolLib bossLib numLib pairLib relationTheory pairTheory arithmeticTheory listSyntax preARMTheory
     pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory finite_mapTheory annotatedIL ILTheory rulesTheory;
quietdec := false;
*)

app load ["relationTheory", "pred_setSimps","pred_setTheory","whileTheory","finite_mapTheory","rich_listTheory", "listSyntax",
          "ILTheory", "rulesTheory", "preARMSyntax", "annotatedIL", "funCall"];

quietdec := true;
open HolKernel Parse boolLib bossLib numLib pairLib relationTheory pairTheory arithmeticTheory listSyntax preARMTheory
     pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory finite_mapTheory annotatedIL ILTheory rulesTheory;
quietdec := false;

(*---------------------------------------------------------------------------------*)
(*      Simplifier on finite maps                                                  *) 
(*---------------------------------------------------------------------------------*)

val fupdate_normalizer =
 let val thm = SPEC_ALL ARMCompositionTheory.FUPDATE_LT_COMMUTES
     val pat = lhs(snd(dest_imp(concl thm)))
 in
   {name = "Finite map normalization",
    trace = 2,
    key = SOME([],pat),
    conv = let fun reducer tm =
                 let val (theta,ty_theta) = match_term pat tm
                     val thm' = INST theta (INST_TYPE ty_theta thm)
                     val constraint = fst(dest_imp(concl thm'))
                     val cthm = EQT_ELIM(reduceLib.REDUCE_CONV constraint)
                 in MP thm' cthm
                 end
           in
               K (K reducer)
           end}
 end;

val finmap_conv_frag =
 simpLib.SSFRAG
     {convs = [fupdate_normalizer],
      rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]};

val finmap_ss = std_ss ++ finmap_conv_frag ++  rewrites [FUPDATE_EQ, FAPPLY_FUPDATE_THM];

val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss;

(*---------------------------------------------------------------------------------*)
(*   Assistant Functions                                                           *) 
(*---------------------------------------------------------------------------------*)

(* make variable tuple, e.g. ((v0,v1),v2,...) *)

fun mk_vars exp =
  let
    val i = ref (~1);
    fun set_vars (annotatedIL.PAIR (e1,e2)) =
          mk_pair(set_vars e1, set_vars e2)
     |  set_vars exp =
          mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`)
  in
    set_vars exp 
  end

(* make mread tuple, e.g. ((st<v0>,st<v1>),st<v2>,...) *)

fun mk_mreads st (annotatedIL.PAIR (e1,e2)) =
        mk_pair(mk_mreads st e1, mk_mreads st e2)
 |  mk_mreads st exp =
        mk_comb ( mk_comb (Term`mread`, st), annotatedIL.convert_exp exp)
  handle e => (print "mk_mreads: invalid incoming expression"; Raise e);


(* make a list of rules [exp0 <- v0, exp1 <- v1, ...] *)

fun mk_subst_rules expL =
  let
    val i = ref (~1);
  in 
    List.map (fn exp => (i := !i + 1; {redex = exp, residue = mk_var ("v" ^ (Int.toString (!i)), Type `:DATA`)})) expL
  end


fun read_one_var s exp =
  let
     val v0 = list_mk_comb (Term`mread`, [s, convert_exp exp]);
     val v1 = rhs (concl ((WORD_RULE o SIMP_CONV finmap_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm]) v0))
  in
     v1
  end

(*---------------------------------------------------------------------------------*)
(*      Symbolic Simulation of Instructions                                        *) 
(*---------------------------------------------------------------------------------*)

val ACCESS_CONV = SIMP_CONV finmap_ss [mread_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def];
val ACCESS_RULE = SIMP_RULE finmap_ss [mread_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def];

(*  Basic RULE for instructions execpt for PUSH and POP                            *) 

val SIM_RULE = 
    fn thm =>
    (WORD_RULE o
     REWRITE_RULE [GSYM WORD_ADD_ASSOC] o
     CONV_RULE (DEPTH_CONV (
	REWRITE_CONV [Once mdecode_def] THENC 
	SIMP_CONV finmap_ss [write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def]))) thm;


(*      Symbolically simulate PUSH and POP instructions                            *) 

val [FOLDL_NIL, FOLDL_CONS] = CONJUNCTS FOLDL;

(*
val POP_TAC =
    CONV_TAC (DEPTH_CONV (REWRITE_CONV [Once mdecode_def, popL_def])) THEN
    REWRITE_TAC [MAP, LENGTH] THEN
    SIMP_TAC finmap_ss [read_thm] THEN
    CONV_TAC (DEPTH_CONV ((REWR_CONV FOLDL_CONS ORELSEC REWR_CONV FOLDL_NIL)
        THENC RATOR_CONV (RAND_CONV (DEPTH_CONV GEN_BETA_CONV
                THENC REWRITE_CONV [read_thm, write_thm, pair_case_def]
                THENC reduceLib.REDUCE_CONV)))) THEN
    SIMP_TAC finmap_ss [write_thm];
*)

val POP_RULE =
    fn th =>
     (WORD_RULE o
      REWRITE_RULE [GSYM WORD_ADD_ASSOC] o
      SIMP_RULE finmap_ss [write_thm] o
      CONV_RULE (DEPTH_CONV ((REWR_CONV FOLDL_CONS ORELSEC REWR_CONV FOLDL_NIL)
          THENC RATOR_CONV (RAND_CONV (DEPTH_CONV GEN_BETA_CONV
                THENC REWRITE_CONV [read_thm, write_thm, pair_case_def]
                THENC reduceLib.REDUCE_CONV)))) o
      SIMP_RULE finmap_ss [read_thm] o
      REWRITE_RULE [MAP, LENGTH] o
      CONV_RULE (DEPTH_CONV (REWRITE_CONV [Once mdecode_def, popL_def]))
     ) th;

(*
val PUSH_TAC =
    CONV_TAC (DEPTH_CONV (REWRITE_CONV [Once mdecode_def, pushL_def])) THEN
    REWRITE_TAC [GSYM MAP_REVERSE, REVERSE_DEF, APPEND, MAP, LENGTH] THEN
    SIMP_TAC finmap_ss [read_thm] THEN
    CONV_TAC (DEPTH_CONV ((REWR_CONV FOLDL_CONS ORELSEC REWR_CONV FOLDL_NIL)
        THENC RATOR_CONV (RAND_CONV (DEPTH_CONV GEN_BETA_CONV
                THENC REWRITE_CONV [read_thm, write_thm, pair_case_def]
                THENC reduceLib.REDUCE_CONV)))) THEN
    SIMP_TAC finmap_ss [write_thm] THEN
    WORD_TAC
*)

val PUSH_RULE =
    fn th =>
     (WORD_RULE o
      REWRITE_RULE [GSYM WORD_ADD_ASSOC] o
      SIMP_RULE finmap_ss [write_thm] o
      CONV_RULE (DEPTH_CONV ((REWR_CONV FOLDL_CONS ORELSEC REWR_CONV FOLDL_NIL)
          THENC RATOR_CONV (RAND_CONV (DEPTH_CONV GEN_BETA_CONV
                THENC REWRITE_CONV [read_thm, write_thm, pair_case_def]
                THENC reduceLib.REDUCE_CONV)))) o
      SIMP_RULE finmap_ss [read_thm] o
      REWRITE_RULE [GSYM MAP_REVERSE, REVERSE_DEF, APPEND, MAP, LENGTH] o
      CONV_RULE (DEPTH_CONV (REWRITE_CONV [Once mdecode_def, pushL_def]))
     ) th;


(* Find the first instruction to be simulated next   *)
 
fun locate_first_inst t = 
    if type_of t = Type `:DOPER` then true
    else false;

(* eliminate all "decode"s and get the new state *) 

fun elim_decode th = 
  let val t1 = concl th
      val st = if is_imp t1 then rhs (#2 (dest_imp t1)) else rhs t1
  in 
      if is_pair st then th
      else
          let val t1 = find_term locate_first_inst st;
              val operator = #1 (strip_comb t1);
              val _ = print ("Simulating a " ^ (#1 (dest_const operator)) ^ " instruction\n");
              val rule1 = if same_const operator (Term `MPUSH`) then PUSH_RULE
                          else if same_const operator (Term `MPOP`) then POP_RULE
                          else SIM_RULE 
              val th' =  rule1 th
          in  elim_decode th'
          end
  end
  handle e => (print "get_blk_spec: errors occur while symbolically simulating a block"; Raise e);

(* Given a list of IR statements, return a theorem indicating the state after symolic simulation *)
(* pre_spec specifies the pre-conditions before the simulation                                   *)

fun sim_stms stms pre_p = 
  let
     val blk = mk_comb (Term`BLK`, mk_list (List.map convert_stm stms, Type`:DOPER`));
     val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`));
     val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [blk, st]);
     val th0 =  REWRITE_CONV [IR_SEMANTICS_BLK] instance;
     val th1 = prove (mk_imp (mk_comb(pre_p,st), concl th0), SIMP_TAC std_ss [th0]);
     val th2 = SIMP_RULE std_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] th1;
     val th3 = elim_decode th2              (* symbolically simulate the block *)
  in
     th3
  end;

(*---------------------------------------------------------------------------------*)
(*      PSPEC specification and Mechanized Reasoning                               *) 
(*---------------------------------------------------------------------------------*)

(* Make a PSPEC specification                                                                    *) 

(* val pre_p = ``\st.(mread st (MR R11) = 5w) /\ (mread st (MM (11,POS 1)) = 6w)``                  *)

val basic_outL = [IR.REG 11, IR.REG 13];               (* fp and sp *)

fun mk_fspec ir (pre_st,post_st) (ins,outs) pre_p = 
  let 

      fun calculate_outs st (IR.PAIR (a,b)) =
              mk_pair (calculate_outs st a, calculate_outs st b)
       |  calculate_outs st exp =
              read_one_var st exp

      fun simplify_pre_p q0 = 
        let
            val q1 = (rhs o concl o ACCESS_CONV) q0 handle e => q0;
            val eqs = strip_conj q1;
            val (qt_eqs, other_eqs) = (List.take(eqs,2), tl (tl eqs));
            val qt_rules = List.map (fn t => {redex = lhs t, residue = rhs t}) qt_eqs;
            val other_eq' = List.map (rhs o concl o WORD_CONV o (subst qt_rules)) other_eqs
        in
            list_mk_conj (qt_eqs @ other_eq')
        end

      (* the pt function *)
      val rules' = List.map (fn t => {redex = lhs t, residue = rhs t}) (strip_conj (simplify_pre_p (#2 (dest_pabs pre_p))));
      val sim1 = rhs o concl o WORD_CONV o (subst rules');

      (* the characteristic function *)
      val rules = mk_subst_rules (List.map (sim1 o (read_one_var pre_st)) (pair2list ins));
      val (initV,out_vars) = (mk_vars ins, mk_vars outs);
      val f_c = mk_pabs (initV, subst rules (sim1 (calculate_outs post_st outs)));  (* the charateristic function *)

      val post_p0 = list_mk_conj (List.map 
             (fn exp => mk_eq(read_one_var pre_st exp, ((subst rules') o rhs o concl o WORD_CONV) 
                             (subst rules' (read_one_var post_st exp)))) basic_outL);  
      val post_p1 = mk_pabs (pre_st, simplify_pre_p post_p0);

      (* the characteristic function *)
      val st' = mk_var ("st", Type `:DSTATE`);
      val (in_f,out_f) = (mk_pabs (st', mk_mreads st' ins), mk_pabs (st', mk_mreads st' outs));
      val f_spec = list_mk_comb (inst [{redex = alpha, residue = type_of initV}, {redex = beta, residue = type_of out_vars}] ``PSPEC``,
                                [ir, mk_pair(pre_p, post_p1), list_mk_pair[in_f,f_c,out_f]])
  in
     f_spec
  end

(*---------------------------------------------------------------------------------*)
(*      Symbolic Simulation of Basic Blocks                                        *) 
(*---------------------------------------------------------------------------------*)
      
(* Given an basic block, the charateristic function on inputs and outputs are derived by symbolic simulation *)
(* and the context about unchanged variables is maintained                                                   *) 
(* Finally well_formed information is given                                                                  *)

fun mk_blk_spec (IR.BLK (instL,{ins = ins, outs = outs, context = context, ...})) pre_p = 
  let 
      val th = sim_stms instL pre_p;
      val (assm,t1) = let val t0 = concl th in if is_imp t0 then dest_imp t0 else (Term`T`, t0) end;
      val ([blk_ir,pre_st], post_st) = (#2 (strip_comb (lhs t1)), rhs t1);
      val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);

      (* the characteristic function *)
      val f_spec = mk_fspec blk_ir (pre_st,post_st) (ins,outs) pre_p;
      val f_spec' = subst [{redex = blk_ir, residue = ir_abbr}] f_spec;

      (* context function *)
      val context_spec = list_mk_comb (Term`UNCHANGED`, [ir_abbr, mk_list (List.map convert_exp context, Type `:MEXP`)]);
      
      (* well_formedness *)
      val wf_spec = mk_comb (Term`WELL_FORMED`, ir_abbr);

      (* specifiction of functional correctness *)
      val fspec = mk_let (mk_abs (ir_abbr, list_mk_conj [f_spec', context_spec, wf_spec]), blk_ir); 

      val spec = prove (fspec,   (* set_goal ([],fspec) *)
             SIMP_TAC std_ss [LET_THM, PSPEC_def, HSPEC_def, UNCHANGED_def, FORALL_DSTATE, BLOCK_IS_WELL_FORMED, read_thm] THEN
                 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN
                 SIMP_TAC std_ss [th] THEN
                 SIMP_TAC finmap_ss [read_thm] THEN
                 WORD_TAC THEN
                 SIMP_TAC std_ss [pair_induction]
            )
   in
     spec
   end

 | mk_blk_spec _ _ = 
     raise Fail "mk_blk_spec: BLK is expected!";

(* Obtain the specification associated with pointers                               *)
fun get_p_spec spec =
  let
      val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec);
      val (t0,t1) = strip_comb (concl th0)
  in
      List.nth (t1,1) 
  end

(*---------------------------------------------------------------------------------*)
(*      Specification for Sequential Composition                                   *) 
(*---------------------------------------------------------------------------------*)

(* retrieve information from a PSPEC specification *)
fun get_spec_info spec = 
    let val specL = strip_conj (concl (SIMP_RULE std_ss [LET_THM] spec));
        val (f_spec, context_spec) = (hd specL, hd (tl specL));
        val (_, [ir, ps, fs]) = strip_comb f_spec;
        val (ps1,ps2) = dest_pair ps;
        val list0 = strip_pair fs;
        val (in_f, f_c, out_f) = (#2 (dest_abs (hd list0)), List.nth(list0,1), #2 (dest_abs (List.nth(list0,2))));
        val contextL = List.nth(#2 (strip_comb context_spec),1)
    in
       (ir, (ps1, ps2), (in_f, f_c, out_f),contextL)
    end
     handle e => (print "get_spec_info: the input is not valid PSPEC and UNCHANGED"; Raise e);


fun mk_sc_spec ir1_spec ir2_spec = 
  let 
      val (ir1,(pre_p1,post_p1),(ins1,f1,outs1),contextL1) = get_spec_info ir1_spec;
      val (ir2,(pre_p2,post_p2),(ins2,f2,outs2),contextL2) = get_spec_info ir2_spec;

      (* SC (ir1, ir2) *)
      val sc_ir = list_mk_comb (Term`SC`, [ir1, ir2]);
      val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
      val st = mk_var ("st", Type `:DSTATE`);
      val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [sc_ir, st]);
      
      (* the characteristic function of SC *)
      val sc_f = list_mk_comb (inst [alpha |-> type_of ins2, beta |-> type_of outs2, gamma |-> type_of ins1] (Term`$o`), [f2,f1]);
      val (in_f,out_f) = (mk_pabs (st,ins1), mk_abs (st,outs2));
      val out_f1 = mk_pabs (st, outs1);       

      val (spec1_thm, spec2_thm) = (SIMP_RULE std_ss [LET_THM] ir1_spec, SIMP_RULE std_ss [LET_THM] ir2_spec);

      (* the SC specification *)
      val f_spec = list_mk_comb (inst [alpha |-> type_of ins1, beta |-> type_of outs2] (Term`PSPEC`), 
                                [sc_ir, mk_pair(pre_p1, post_p2), list_mk_pair[in_f,sc_f,out_f]]);

      val f_th =  prove (f_spec,   (* set_goal ([],f_spec) *)
                        MATCH_MP_TAC PROJ_SC_RULE THEN
                        EXISTS_TAC post_p1 THEN EXISTS_TAC out_f1 THEN
                        SIMP_TAC std_ss [spec1_thm, spec2_thm]
		        )

      (* context function *)
      val context_spec = list_mk_comb (Term`UNCHANGED`, [sc_ir, contextL2]);
      val context_th = prove (context_spec,   (* set_goal ([],context_spec) *)
                      MATCH_MP_TAC CONTEXT_SC_RULE THEN
                      SIMP_TAC std_ss [spec1_thm, spec2_thm]
	        )

      val well_formed_spec = mk_comb (Term`WELL_FORMED`, sc_ir);
      val well_formed_th = prove (well_formed_spec,   (* set_goal ([],well_formed_spec) *)
                      MATCH_MP_TAC IR_SC_IS_WELL_FORMED THEN
                      SIMP_TAC std_ss [spec1_thm, spec2_thm]
	        );

      val spec = subst [sc_ir |-> ir_abbr] (list_mk_conj [f_spec, context_spec, well_formed_spec]);
      val spec' = mk_let (mk_abs (ir_abbr, spec), sc_ir);

      val th =  prove (spec',   (* set_goal ([],spec') *)
			SIMP_TAC std_ss [LET_THM, f_th, context_th, well_formed_th]
		      )
   in
        th
   end;

(*---------------------------------------------------------------------------------*)
(*      Specification for Function Calls                                           *) 
(*---------------------------------------------------------------------------------*)

fun compute_outL modifiedRegL =
    let val i = ref 0   
    in
        List.map (fn e => (i := !i - 1; IR.MEM (11, !i))) ([12, 11] @ (List.rev modifiedRegL))  (* neglect pc and lr *)
    end

fun mk_fc_spec (pre_spec, body_spec, post_spec) = 
    mk_sc_spec (mk_sc_spec pre_spec body_spec) post_spec;


(*---------------------------------------------------------------------------------*)
(*      Specification for input/output matching                                    *) 
(*---------------------------------------------------------------------------------*)

(*
PROJ_POST_RULE
 |- !ir in_f out_f convert_f.
         PSPEC ir (pre_p,post_p) (in_f,f,out_f) ==>
         PSPEC ir (pre_p,post_p) (in_f,convert_f o f,convert_f o out_f) : thm


fun mk_match_spec spec in_f2 = 
  let 
      
      val (_, (pre_p1, post_p1), (in_f1, f_c, out_f1), _) = get_spec_info spec;
      

   in
        th
   end;
*)


(***********************************************************************************

(*---------------------------------------------------------------------------------*)
(*      Specification for Tail Recursion                                           *) 
(*---------------------------------------------------------------------------------*)

(* Given a TR, the charateristic function on inputs and outputs are derived by the TR_RULE *)
(* and the context about unchanged variables is maintained                                 *) 

fun convert_cond (exp1, rop, exp2) =
  let
    val cond_t0 = list_mk_pair [mk_comb (Term`toEXP`, convert_exp exp1), 
				convert_rop rop, 
				mk_comb (Term`toEXP`, convert_exp exp2)];
    val cond_t1 = rhs (concl (SIMP_CONV std_ss [toEXP_def, toMEM_def, toREG_def, index_of_reg_def] cond_t0))
  in
    cond_t1
  end
  handle e => (print "mk_cond: errors occur while converting the condition"; Raise e);

fun strip_pair2 t =
  if is_pair t then List.foldl (fn (t0,L0) => L0 @ (strip_pair2 t0)) [] (strip_pair t)
  else [t];

fun mk_cj_cond cond_t ins =
  let 
    val st = mk_var ("st", Type `:DSTATE`);
    val instance = list_mk_comb (Term`eval_cond`, [cond_t, st]);

    val read_const_th = prove (Term`!st v. read st (WCONST v) = v`, SIMP_TAC std_ss [FORALL_DSTATE, read_thm]); 

    val th0 = REWRITE_CONV [ARMCompositionTheory.eval_cond_def] instance;
    val th1 = REWRITE_RULE [read_const_th] th0;
    val instance1 = rhs (concl th1);

    val rules = mk_subst_rules (List.map (fn t0 => rhs (concl (REWRITE_CONV [mread_def, toMEM_def, toREG_def, index_of_reg_def] t0))) (strip_pair2 ins));
    val cj_cond = subst rules instance1  (* the condition function *)
  in
     cj_cond
  end

fun mk_cond_f cond_t ins =                  (* the condition function *)
    let 
        val rules = mk_subst_rules (strip_pair2 ins)
    in 
        mk_pabs (subst rules ins, mk_cj_cond cond_t ins)
    end

fun guessR2 tp = 
    let val tp1 = List.nth(#2 (dest_type tp),1)
    in
        inst [alpha |-> tp1] ``measure (w2n o FST )``
    end

fun cheat_tac (asl,g) = ACCEPT_TAC(ASSUME g) (asl,g);


fun mk_tr_spec cond body_spec = 
  let 
      val specL = strip_conj (concl body_spec);
      val (body_ir,(ins,f,outs),contextL) = get_spec_info (hd specL, hd (tl specL));

      val t_cond = convert_cond cond;
      val tr_ir = list_mk_comb (Term`TR`, [t_cond, body_ir]);
      val st = mk_var ("st", Type `:DSTATE`);
      val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [tr_ir, st]);
      
      val initV = #1 (dest_pabs f);

      val cond_f_0 = mk_cond_f t_cond ins;
      val cond_f = list_mk_comb (inst [alpha |-> bool, beta |-> bool, gamma |-> type_of initV] (Term`$o`), [Term`$~:bool->bool`,cond_f_0]);

      val tr_f = list_mk_comb (inst [alpha |-> type_of initV] (Term`WHILE`), [cond_f, f]);
      val prj_f = mk_pabs (st,ins);
       
      (* well_founded relation: WF (\st1 st0. ~eval_cond cond st0 /\ (st1 = run_ir ir st0)) *)
      
      val (st0,st1) = (mk_var ("st0", Type `:DSTATE`), mk_var ("st1", Type `:DSTATE`));
      val wf_t0 = mk_neg (list_mk_comb (Term`eval_cond`, [t_cond, st0]));
      val wf_t1 = mk_eq (st1, list_mk_comb (Term`run_ir`, [body_ir, st0]));
      val wf_t2 = list_mk_abs ([st1,st0],mk_conj(wf_t0,wf_t1));
      val wf_t3 = mk_comb (inst [alpha |-> Type `:DSTATE`] (Term`WF`), wf_t2);
      val wf_th = prove (wf_t3, (* set_goal ([],wf_t3) *)
                         MATCH_MP_TAC (INST_TYPE [alpha |-> type_of initV] WF_TR_LEM_2) THEN
                         EXISTS_TAC prj_f THEN
                         EXISTS_TAC f THEN
                         EXISTS_TAC cond_f_0 THEN
                         SIMP_TAC std_ss [SIMP_RULE std_ss [PSPEC_def, HSPEC_def] body_spec] THEN
                         SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, 
                                         index_of_reg_def,toREG_def, toMEM_def, read_thm] THEN
                         MATCH_MP_TAC (INST_TYPE [alpha |-> type_of initV] WF_TR_LEM_3) THEN
                         (let val r = guessR2 (type_of initV) in 
                              WF_REL_TAC `^r`
                          end
                          handle e => (print "fail to prove totalness, add statement into assumption list"; cheat_tac)
                         )
                         );

      (* the characteristic function *)
      val f_spec = list_mk_comb (inst [alpha |-> type_of initV, beta |-> type_of initV] (Term`PSPEC`), 
                                [tr_ir, list_mk_pair[prj_f,tr_f,prj_f]]);

      val f_th =  prove (f_spec,   (* set_goal ([],f_spec) *)
                        ASSUME_TAC wf_th THEN
                        MATCH_MP_TAC PROJ_TR_RULE THEN
                        SIMP_TAC std_ss [body_spec] THEN
                        STRIP_TAC THENL [
                            RW_TAC std_ss [],
                            SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, 
                                         index_of_reg_def, toREG_def, toMEM_def, read_thm]
                            ]
		        )

      (* context function *)
      val context_spec = list_mk_comb (Term`UNCHANGED`, [tr_ir, contextL]);
      val context_th = prove (context_spec,   (* set_goal ([],context_spec) *)
                      ASSUME_TAC wf_th THEN
                      MATCH_MP_TAC CONTEXT_TR_RULE THEN
                      SIMP_TAC std_ss [body_spec] THEN
                      RW_TAC std_ss []
	        )

      val well_formed_spec = mk_comb (Term`WELL_FORMED`, tr_ir);
      val well_formed_th = prove (well_formed_spec,   (* set_goal ([],well_formed_spec) *)
                      ASSUME_TAC wf_th THEN
                      MATCH_MP_TAC WELL_FORMED_TR_RULE THEN
                      SIMP_TAC std_ss [body_spec] THEN
                      RW_TAC std_ss []
	        );

      val spec = list_mk_conj [f_spec, context_spec, well_formed_spec];

      val th =  prove (spec,   (* set_goal ([],spec) *)
			SIMP_TAC std_ss [f_th, context_th, well_formed_th]
		      )
   in
        th
   end;


(*---------------------------------------------------------------------------------*)
(*      Specification for Conditional Jumps                                        *) 
(*---------------------------------------------------------------------------------*)
 
fun mk_cj_spec cond ir1_spec ir2_spec = 
  let 
      val (specL1,specL2) = (strip_conj (concl ir1_spec), strip_conj (concl ir2_spec));
      val (ir1,(ins1,f1,outs1),contextL1) = get_spec_info (hd specL1, hd (tl specL1));
      val (ir2,(ins2,f2,outs2),contextL2) = get_spec_info (hd specL2, hd (tl specL2));

      val t_cond = convert_cond cond;
      val cj_ir = list_mk_comb (Term`CJ`, [t_cond, ir1, ir2]);
      val st = mk_var ("st", Type `:DSTATE`);
      val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [cj_ir, st]);
      
      val initV = #1 (dest_pabs f1);
      val cj_cond = mk_pabs(initV, mk_cj_cond t_cond ins1);
      val cj_f = mk_pabs(initV, list_mk_comb (inst [alpha |-> type_of outs1] (Term`COND`), 
                       [mk_comb(cj_cond,initV), mk_comb(f1,initV), mk_comb(f2,initV)]));

      val (in_f,out_f) = (mk_pabs (st,ins1), mk_abs (st,outs2));

      (* the characteristic function *)
      val f_spec = list_mk_comb (inst [alpha |-> type_of ins1, beta |-> type_of outs2] (Term`PSPEC`), 
                                [cj_ir, list_mk_pair[in_f,cj_f,out_f]]);

      val f_th =  prove (f_spec,   (* set_goal ([],f_spec) *)
                        MATCH_MP_TAC (SIMP_RULE std_ss [LAMBDA_PROD] (INST_TYPE [alpha |-> type_of initV] PROJ_CJ_RULE)) THEN
                        SIMP_TAC std_ss [ir1_spec, ir2_spec] THEN
                        SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, 
                                         index_of_reg_def, toREG_def, toMEM_def, read_thm, GSYM PFORALL_THM]
		        )

      (* context function *)
      val context_spec = list_mk_comb (Term`UNCHANGED`, [cj_ir, contextL2]);
      val context_th = prove (context_spec,   (* set_goal ([],context_spec) *)
                      MATCH_MP_TAC CONTEXT_CJ_RULE THEN
                      SIMP_TAC std_ss [ir1_spec, ir2_spec]
	        )

      val well_formed_spec = mk_comb (Term`WELL_FORMED`, cj_ir);
      val well_formed_th = prove (well_formed_spec,   (* set_goal ([],well_formed_spec) *)
                      MATCH_MP_TAC IR_CJ_IS_WELL_FORMED THEN
                      SIMP_TAC std_ss [ir1_spec, ir2_spec]
	        );

      val spec = list_mk_conj [f_spec, context_spec, well_formed_spec];

      val th =  prove (spec,   (* set_goal ([],spec) *)
			SIMP_TAC std_ss [f_th, context_th, well_formed_th]
		      )
   in
        th
   end;


************************************************************************************)


(*---------------------------------------------------------------------------------*)
(*      Forward Reasoning                                                          *) 
(*---------------------------------------------------------------------------------*)

(*
fun fwd_reason (IR.TR (cond, body, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) = 
      let val body_spec = fwd_reason body;
      in
          mk_tr_spec cond body_spec
      end

 |  fwd_reason (IR.SC (ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) =
      mk_sc_spec (fwd_reason ir1) (fwd_reason ir2)

 |  fwd_reason (IR.CJ (cond, ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) =
      mk_cj_spec cond (fwd_reason ir1) (fwd_reason ir2)

 |  fwd_reason (IR.BLK blk_ir) =
      mk_blk_spec (IR.BLK blk_ir)

 |  fwd_reason (IR.CALL (fname, pre_ir, body_ir, post_ir, info)) =
      mk_fc_spec (pre_ir, fwd_reason body_ir, post_ir, info)

 |  fwd_reason _ = 
      raise Fail "fwd_reason: unsupported IR strcuture"
 ;
*)

fun fwd_reason (IR.BLK blk_ir) pre_p =
      mk_blk_spec (IR.BLK blk_ir) pre_p

 |  fwd_reason (IR.CALL (fname, pre_ir, body_ir, post_ir, info)) pre_p =
      let 
          val pre_spec = mk_blk_spec pre_ir pre_p;
          val pre_p' = #2 (dest_pair (get_p_spec pre_spec));
          val body_spec = mk_blk_spec body_ir pre_p';
          val pre_p'' = #2 (dest_pair (get_p_spec body_spec));
          val post_spec = mk_blk_spec post_ir pre_p''
      in
          mk_fc_spec (pre_spec, body_spec, post_spec)
      end

 |  fwd_reason (IR.SC (ir1, ir2, info)) pre_p =
      let val spec1 = fwd_reason ir1 pre_p;
          val pre_p' = #2 (dest_pair (get_p_spec spec1))
          val spec2 = fwd_reason ir2 pre_p'
      in
          mk_sc_spec spec1 spec2
      end

 |  fwd_reason _ _ = 
      raise Fail "fwd_reason: unsupported IR strcuture"
 ;

(*---------------------------------------------------------------------------------*)
(*      Equivalence between the original function and the spec function            *) 
(*---------------------------------------------------------------------------------*)

fun restore_f spec defs =
  let
      val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec);
      val [in_f,spec_f,out_f] = strip_pair (List.nth (#2 (strip_comb (concl th0)),2));
      val sfl_f_const = #1 (strip_comb (lhs ((concl o SPEC_ALL) (hd defs))));
      val eq_stat = mk_eq (spec_f, sfl_f_const);
      val eq_th =  prove (eq_stat,   (* set_goal ([],eq_stat) *)
                        SIMP_TAC std_ss [FUN_EQ_THM, FORALL_PROD] THEN
                        REPEAT GEN_TAC THEN
                        REPEAT (FIRST [CHANGED_TAC (SIMP_TAC std_ss ([LET_THM, WORD_ADD_ASSOC] @ defs)), WORD_TAC])
		        )
  in
      eq_th
  end;


(*---------------------------------------------------------------------------------*)
(*      Display the theorem at the level of ARM flat code                          *) 
(*---------------------------------------------------------------------------------*)

fun f_correct spec =
  let
      val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec);
      val th1 = SIMP_RULE std_ss [PSPEC_def, HSPEC_def, run_ir_def] th0;
      val f = let val t0 = concl (SPEC_ALL th1)
                    val (assm, t1) = dest_imp t0
                    val f_spec = #1 (dest_conj t1)
              in
                    mk_imp (assm, f_spec)
              end
      val th2 = GEN_ALL (prove (f, SIMP_TAC std_ss [th1]));
      val th3 = SIMP_RULE std_ss [translate_def, translate_assignment_def, toEXP_def, toREG_def, toMEM_def, index_of_reg_def] th2;
      val th4 = SIMP_RULE list_ss [ARMCompositionTheory.mk_SC_def, ARMCompositionTheory.mk_CJ_def, ARMCompositionTheory.mk_TR_def] th3
  in
      th4
  end;
     
(*---------------------------------------------------------------------------------*)
(*      Print out                                                                  *) 
(*---------------------------------------------------------------------------------*)

(* Extract the IR tree from the specification and print it out *)

fun extract_ir spec =
    let
       val (f_name, _, (f_args,f_ir,f_outs), _, _) = spec;
    in
      (print ("  Name              : " ^ f_name ^ "\n");
       print ("  Arguments         : " ^ (IR.format_exp f_args) ^ "\n");
       print ("  Returns           : " ^ (IR.format_exp f_outs) ^ "\n");
       print  "  Body: \n";
       IR.printIR f_ir
      )
    end

(* Extract the ARM instruction list from the specification and print it out *)

fun extract_arm spec =
    let 
       val (f_name, _, (f_args,_,f_outs), _, stat0) = spec;
       val stat1 = #2 (dest_imp (concl (SPEC_ALL stat0)));
       val stms = find_term (fn t => type_of t = Type `:INST list`) stat1;
       val stms1 = preARMSyntax.dest_arm stms
    in          
      (print ("  Name              : " ^ f_name ^ "\n");
       print ("  Arguments         : " ^ (IR.format_exp f_args) ^ "\n");
       print ("  Returns           : " ^ (IR.format_exp f_outs) ^ "\n");
       print  "  Body: \n";
       Assem.printInsts stms1
      )
    end

(*---------------------------------------------------------------------------------*)
(*      Interface                                                                  *) 
(*---------------------------------------------------------------------------------*)

(* To make the initial value of fp or sp unspecified, assign it a negative integer *)
(* For example, init_fp = ~1 will lead to st<MR R11> = ARB                         *)

(*val init_fp = ref (100);*)
val init_sp = ref 100;

(*
fun get_spec prog = 
  let
    val (f_name, f_type, (f_args,f_ir,f_outs), defs) = sfl2ir prog;
    val pre_p = let val st = mk_var ("st", Type `:DSTATE`);
                      val (fp',sp') = (mk_mreads st (IR.REG 11), mk_mreads st (IR.REG 13));
                      fun convert_pt v = if v < 0 then inst [alpha |-> Type `:DATA`] (Term `ARB`) else mk_comb (Term `n2w`, term_of_int v)
                in  mk_abs (st, mk_conj ( mk_eq(fp', convert_pt (!init_sp)), mk_eq(sp', convert_pt (!init_sp)))) (* Initially fp = sp *)
                end
    val f_spec0 = #fspec (get_annt (fwd_reason f_ir pre_p));
  in
    f_spec0
  end
*)

fun pp_compile prog = 
  let  
      val (f_name, f_type, (f_args,f_ir,f_outs), defs) = funCall.link_ir prog;
      val pre_p = let val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`));
                      val (fp',sp') = (read_one_var st (IR.REG 11), read_one_var st (IR.REG 13));
                      fun convert_pt v = if v < 0 then inst [alpha |-> Type `:DATA`] (Term `ARB`) else mk_comb (Term `n2w`, term_of_int v)
                  in  mk_pabs (st, mk_conj ( mk_eq(fp', convert_pt (!init_sp)), mk_eq(sp', convert_pt (!init_sp)))) (* Initially fp = sp *)
                  end
      val f_spec0 = fwd_reason f_ir pre_p;
      val f_spec1 = SIMP_RULE std_ss [restore_f f_spec0 defs] f_spec0;
      val stat = f_correct f_spec1
  in
      (f_name, f_type, (f_args,f_ir,f_outs), defs, stat)
  end
