fun load_path_add x = loadPath := !loadPath @ [concat Globals.HOLDIR x];
load_path_add "/examples/mc-logic";
load_path_add "/examples/ARM/v4";
load_path_add "/tools/mlyacc/mlyacclib";

use "prelim";
hide "C";

app load ["pred_setTheory", "rich_listTheory", "wordsLib", "arm_progLib",
          "multiwordTheory"];

quietdec := true;
open HolKernel boolLib bossLib Parse;
open pred_setTheory res_quanTheory arithmeticTheory 
     wordsLib wordsTheory bitTheory;
open pairTheory listTheory rich_listTheory relationTheory pairTheory;
open set_sepTheory set_sepLib progTheory arm_progTheory 
     arm_instTheory arm_progLib;
open multiwordTheory;

quietdec := false;

infix \\ << >>

val op \\ = op THEN;
val op << = op THENL;
val op >> = op THEN1;

val RW = REWRITE_RULE;
val RW1 = ONCE_REWRITE_RULE;

fun MATCH_MP th1 th2 = 
 let fun SIMPLE_MATCH_MP impth =
      let val (hy,c) = dest_thm impth
          val (vs,imp) = strip_forall c
          val pat = fst(dest_imp imp) handle HOL_ERR _ 
                    => raise ERR "SIMPLE_MATCH_MP" "not an implication"
          val fvs = set_diff (free_vars pat) (free_varsl hy)
          val gth = GSPEC (GENL fvs (SPECL vs impth))
          val matchfn = match_term (fst(dest_imp(concl gth)))
      in
      fn th => MP (INST_TY_TERM (matchfn (concl th)) gth) th
               handle e => raise wrap_exn "SIMPLE_MATCH_MP" "does not match" e
      end
 in
  Drule.MATCH_MP th1 th2 handle HOL_ERR _ 
  => (HOL_MESG "Drule.MATCH_MP fails, trying simpler version";
      SIMPLE_MATCH_MP th1 th2)
 end;


(* lemmas *)

val n2w_x_eq_0w = prove(
  ``1073741824w = 0w:word30``,
  ONCE_REWRITE_TAC [GSYM n2w_mod] \\ SIMP_TAC (std_ss++SIZES_ss) []);

val ARM_PROG_COMPOSE_WEAKEN = prove(
  ``ARM_PROG P code C Q {} ==> 
    ARM_PROG P1 code C Q1 ((P * Q2,I) INSERT Z) ==>
    SEP_IMP (Q * Q2) Q1 ==>
    ARM_PROG P1 code C Q1 Z``,
  REWRITE_TAC [ARM_PROG_THM] \\ REPEAT STRIP_TAC 
  \\ Q.PAT_ASSUM `ARM_GPROG {(P,I)} ((code,I) INSERT C) {(Q,pcINC code)}` 
    (ASSUME_TAC o RW [setSTAR_CLAUSES] o Q.SPEC `Q2` o MATCH_MP ARM_GPROG_FRAME)
  \\ IMP_RES_TAC ARM_GPROG_WEAKEN_POST
  \\ (MATCH_MP_TAC o RW [INSERT_UNION_EQ,UNION_EMPTY,UNION_IDEMPOT,INSERT_INSERT] o 
      RW1 [UNION_COMM] o Q.SPECL [`Y`,`{}`,`{(P * Q2,I)}`,`C`,`C`,
      `(Q1,pcINC code) INSERT Z`,`{(Q1,pcINC code)}`]) ARM_GPROG_COMPOSE
  \\ ONCE_REWRITE_TAC [INSERT_COMM] \\ ASM_REWRITE_TAC []);

(* helpers *)

fun extract_spec th substs uni_list abs_list = let
  val p = parse_in_context (free_varsl (concl th :: hyp th))
  val ss = map (fn (x,y) => (p x |-> p y)) substs
  val tm = (fst o dest_comb o concl) th
  val tm = mk_comb(tm,(snd o dest_comb o snd o dest_comb o concl) th)
  val tm = subst ss tm
  val tm = foldr mk_forall tm (map p uni_list)
  val tm = foldr mk_abs tm (map p abs_list)
  in tm end;

fun extract_assum th = let
  val tm = (repeat (snd o dest_forall) o fst o dest_imp o concl) th
  val th = (SPEC_ALL o ASSUME o fst o dest_imp) tm
  in th end;

fun tidy_up th1 th = let
  val tm = (fst o dest_imp o concl) th1
  val (tm,vs1) = repeat 
                  (fn (tm,xs) => 
                      let val (v,x) = dest_forall tm 
                      in (x,xs@[v]) end) 
                  (tm,[])
  val tm = (snd o dest_imp) tm
  val (tm,vs2) = repeat 
                  (fn (tm,xs) => 
                      let val (v,x) = dest_forall tm 
                      in (x,xs@[v]) end) 
                  (tm,[])
  in (GENL vs1 o DISCH_ALL o GENL vs2) th end;


(* definition *)

val f32_def = Define 
   `f32(x:word32,a:word32) =
          if x=0w then a else f32(x-1w,a*x)`;

val f32_ind = fetch "-" "f32_ind";


val def = compile3 [f32_def];

val f32_compiled_def = 
 Define 
   `f32_compiled (v1:word32,v2:word32) =
      let v3 = (if v1 = 0w then v2
                else let v4 = v1 - 1w in
                     let v5 = v2 * v1 in
                     let v6 = f32 (v4,v5) 
                     in v6)
      in
        v3`;

(* proof step 1: make a basic spec for a run through the code *)
(*
  make_spec' [
("teq r0,#0",true),
("beq 16",true)]
*)

  val th = (*  teq r0,#0  *) FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(w2w (0w :word8) :word32)``] (Q.INST [`c_flag`|->`AL`,`a`|->`0w`,`a_mode`|->`Imm 0w`,`x`|->`x1` ] arm_TEQ1))
  val th = (*  beq 16     *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(sw2sw (2w :word24) :word30)``] (Q.INST [`c_flag`|->`EQ`,`offset`|->`2w` ] arm_B2))) `x1*x2` `(x2)*(x1)` `x1*x2` `(x1)*(x2)`
  val th = AUTO_HIDE_STATUS th
  val th = SIMP_RULE (arith_ss++sep_ss++pcINC_ss) [wLENGTH_def,LENGTH,word_add_n2w] th
  val th = APP_FRAME `cond (x1 = 0w:word32)` th
  val th1 = th

(*
  make_spec' [
("teq r0,#0",true),
("beq 16",false),
("mul r1,r0,r1",true),
("sub r0,r0,#1",true),
("b -16",true)]
*)
  val th = (*  teq r0,#0     *) FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(w2w (0w :word8) :word32)``] (Q.INST [`c_flag`|->`AL`,`a`|->`0w`,`a_mode`|->`Imm 0w`,`x`|->`x1` ] arm_TEQ1))
  val th = (*  beq 16        *) MOVE_COMPOSE th (SND_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(sw2sw (2w :word24) :word30)``] (Q.INST [`c_flag`|->`EQ`,`offset`|->`2w` ] arm_B2))) `x1*x2` `(x2)*(x1)` `x1*x2` `(x1)*(x2)`
  val th = (*  mul r1,r0,r1  *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [] (Q.INST [`c_flag`|->`AL`,`s_flag`|->`F`,`b`|->`1w`,`a`|->`0w`,`x`|->`x3`,`y`|->`y3` ] arm_MUL2))) `x1*x2` `(x1*x2)*(emp)` `x1*x2*x3` `(x3*x1)*(x2)`
  val th = (*  sub r0,r0,#1  *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(w2w (1w :word8) :word32)``] (Q.INST [`c_flag`|->`AL`,`s_flag`|->`F`,`a`|->`0w`,`a_mode`|->`Imm 1w`,`x`|->`x4` ] arm_SUB1))) `x1*x2*x3` `(x1*x3)*(x2)` `x1*x2` `(x1*x2)*(emp)`
  val th = (*  b -16         *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(sw2sw (16777210w :word24) :word30)``] (Q.INST [`c_flag`|->`AL`,`offset`|->`16777210w` ] arm_B2))) `x1*x2*x3` `(x2)*(x1*x3)` `x1` `(x1)*(emp)`
  val th = AUTO_HIDE_STATUS th
  val th = APP_FRAME `cond ~(x1 = 0w:word32)` th
  val th = SIMP_RULE (arith_ss++sep_ss++pcINC_ss) [wLENGTH_def,LENGTH,word_add_n2w] th
  val th1 = APP_FRAME `R 1w y3` th1 
  val th1 = MOVE_PRE `S` th1
  val th = SIMP_RULE (bool_ss++sep2_ss) [] th
  val th1 = SIMP_RULE (bool_ss++sep2_ss) [] th1
  val th = SIMP_RULE (bool_ss++sep_ss) [] (APP_MERGE th th1)
  val th = RW [n2w_x_eq_0w,pcADD_0,INSERT_UNION_EQ,UNION_EMPTY] th
  val th = RW1 [INSERT_COMM] th
  val th = ABSORB_POST th

  (* step 2: clean up pre- and postconditions *)
  val th = AUTO_HIDE_POST1 [`R 0w`] th
  val th = APP_WEAKEN1 th 
    `~R 0w * R 1w (f32(x1,y3)) * ~S`
   (SIMP_TAC (bool_ss++sep2_ss) [SEP_IMP_MOVE_COND]
    \\ ONCE_REWRITE_TAC [f32_def] \\ REWRITE_TAC []
    \\ SIMP_TAC (bool_ss++star_ss) [SEP_IMP_REFL])

  (* step 3: instantiate induction and extract ind hyp *)
  val tm = extract_spec th [] [] [`x1`,`y3`]
  val ind = Q.GEN `P` (SIMP_RULE bool_ss [FST,SND] (Q.SPEC `\x. P (FST x) (SND x)` f32_ind))
  val th1 = SIMP_RULE std_ss [] (ISPEC tm ind)
  val asm = extract_assum th1
  val asm = RW [GSYM ARM_PROG_MOVE_COND] asm

  (* step 4: match step and prove postcondition *)
  val asm = MATCH_MP ARM_PROG_COMPOSE_WEAKEN asm
  val th = RW1 [GSYM (REWRITE_CONV [SEP_cond_CLAUSES] ``cond b * cond b``)] th
  val th = RW [STAR_ASSOC] th
(*  val th = Q.INST [`x1`|->`x`,`y3`|->`a`] th *)
  val th = RW1 [WORD_MULT_COMM] th
  val th = MATCH_MP asm th  (* MATCH_MP now works w.o. above Q.INST *)
  val lemma = prove((fst o dest_imp o concl) th,
    SIMP_TAC (bool_ss++sep2_ss) [SEP_IMP_MOVE_COND] \\ REPEAT STRIP_TAC
    \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [f32_def]))
    \\ ASM_REWRITE_TAC [SEP_IMP_REFL])
  val th = MP th lemma
  
  (* step 5: clean up *)
(*   val th = MATCH_MP th1 (tidy_up th1 th) *)
  val th2 = Q.GEN `x1` (Q.GEN `y3` (DISCH_ALL th));;
  val th = MATCH_MP th1 th2
  val th = SPEC_ALL (Q.SPECL [`x`,`a`] th)