1fun load_path_add x = loadPath := !loadPath @ [concat Globals.HOLDIR x]; 2load_path_add "/examples/mc-logic"; 3load_path_add "/examples/ARM/v4"; 4load_path_add "/tools/mlyacc/mlyacclib"; 5 6use "prelim"; 7hide "C"; 8 9app load ["pred_setTheory", "rich_listTheory", "wordsLib", "arm_progLib", 10 "multiwordTheory"]; 11 12quietdec := true; 13open HolKernel boolLib bossLib Parse; 14open pred_setTheory res_quanTheory arithmeticTheory 15 wordsLib wordsTheory bitTheory; 16open pairTheory listTheory rich_listTheory relationTheory pairTheory; 17open set_sepTheory set_sepLib progTheory arm_progTheory 18 arm_instTheory arm_progLib; 19open multiwordTheory; 20 21quietdec := false; 22 23infix \\ << >> 24 25val op \\ = op THEN; 26val op << = op THENL; 27val op >> = op THEN1; 28 29val RW = REWRITE_RULE; 30val RW1 = ONCE_REWRITE_RULE; 31 32fun MATCH_MP th1 th2 = 33 let fun SIMPLE_MATCH_MP impth = 34 let val (hy,c) = dest_thm impth 35 val (vs,imp) = strip_forall c 36 val pat = fst(dest_imp imp) handle HOL_ERR _ 37 => raise ERR "SIMPLE_MATCH_MP" "not an implication" 38 val fvs = set_diff (free_vars pat) (free_varsl hy) 39 val gth = GSPEC (GENL fvs (SPECL vs impth)) 40 val matchfn = match_term (fst(dest_imp(concl gth))) 41 in 42 fn th => MP (INST_TY_TERM (matchfn (concl th)) gth) th 43 handle e => raise wrap_exn "SIMPLE_MATCH_MP" "does not match" e 44 end 45 in 46 Drule.MATCH_MP th1 th2 handle HOL_ERR _ 47 => (HOL_MESG "Drule.MATCH_MP fails, trying simpler version"; 48 SIMPLE_MATCH_MP th1 th2) 49 end; 50 51 52(* lemmas *) 53 54val n2w_x_eq_0w = prove( 55 ``1073741824w = 0w:word30``, 56 ONCE_REWRITE_TAC [GSYM n2w_mod] \\ SIMP_TAC (std_ss++SIZES_ss) []); 57 58val ARM_PROG_COMPOSE_WEAKEN = prove( 59 ``ARM_PROG P code C Q {} ==> 60 ARM_PROG P1 code C Q1 ((P * Q2,I) INSERT Z) ==> 61 SEP_IMP (Q * Q2) Q1 ==> 62 ARM_PROG P1 code C Q1 Z``, 63 REWRITE_TAC [ARM_PROG_THM] \\ REPEAT STRIP_TAC 64 \\ Q.PAT_ASSUM `ARM_GPROG {(P,I)} ((code,I) INSERT C) {(Q,pcINC code)}` 65 (ASSUME_TAC o RW [setSTAR_CLAUSES] o Q.SPEC `Q2` o MATCH_MP ARM_GPROG_FRAME) 66 \\ IMP_RES_TAC ARM_GPROG_WEAKEN_POST 67 \\ (MATCH_MP_TAC o RW [INSERT_UNION_EQ,UNION_EMPTY,UNION_IDEMPOT,INSERT_INSERT] o 68 RW1 [UNION_COMM] o Q.SPECL [`Y`,`{}`,`{(P * Q2,I)}`,`C`,`C`, 69 `(Q1,pcINC code) INSERT Z`,`{(Q1,pcINC code)}`]) ARM_GPROG_COMPOSE 70 \\ ONCE_REWRITE_TAC [INSERT_COMM] \\ ASM_REWRITE_TAC []); 71 72(* helpers *) 73 74fun extract_spec th substs uni_list abs_list = let 75 val p = parse_in_context (free_varsl (concl th :: hyp th)) 76 val ss = map (fn (x,y) => (p x |-> p y)) substs 77 val tm = (fst o dest_comb o concl) th 78 val tm = mk_comb(tm,(snd o dest_comb o snd o dest_comb o concl) th) 79 val tm = subst ss tm 80 val tm = foldr mk_forall tm (map p uni_list) 81 val tm = foldr mk_abs tm (map p abs_list) 82 in tm end; 83 84fun extract_assum th = let 85 val tm = (repeat (snd o dest_forall) o fst o dest_imp o concl) th 86 val th = (SPEC_ALL o ASSUME o fst o dest_imp) tm 87 in th end; 88 89fun tidy_up th1 th = let 90 val tm = (fst o dest_imp o concl) th1 91 val (tm,vs1) = repeat 92 (fn (tm,xs) => 93 let val (v,x) = dest_forall tm 94 in (x,xs@[v]) end) 95 (tm,[]) 96 val tm = (snd o dest_imp) tm 97 val (tm,vs2) = repeat 98 (fn (tm,xs) => 99 let val (v,x) = dest_forall tm 100 in (x,xs@[v]) end) 101 (tm,[]) 102 in (GENL vs1 o DISCH_ALL o GENL vs2) th end; 103 104 105(* definition *) 106 107val f32_def = Define 108 `f32(x:word32,a:word32) = 109 if x=0w then a else f32(x-1w,a*x)`; 110 111val f32_ind = fetch "-" "f32_ind"; 112 113 114val def = compile3 [f32_def]; 115 116val f32_compiled_def = 117 Define 118 `f32_compiled (v1:word32,v2:word32) = 119 let v3 = (if v1 = 0w then v2 120 else let v4 = v1 - 1w in 121 let v5 = v2 * v1 in 122 let v6 = f32 (v4,v5) 123 in v6) 124 in 125 v3`; 126 127(* proof step 1: make a basic spec for a run through the code *) 128(* 129 make_spec' [ 130("teq r0,#0",true), 131("beq 16",true)] 132*) 133 134 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)) 135 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)` 136 val th = AUTO_HIDE_STATUS th 137 val th = SIMP_RULE (arith_ss++sep_ss++pcINC_ss) [wLENGTH_def,LENGTH,word_add_n2w] th 138 val th = APP_FRAME `cond (x1 = 0w:word32)` th 139 val th1 = th 140 141(* 142 make_spec' [ 143("teq r0,#0",true), 144("beq 16",false), 145("mul r1,r0,r1",true), 146("sub r0,r0,#1",true), 147("b -16",true)] 148*) 149 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)) 150 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)` 151 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)` 152 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)` 153 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)` 154 val th = AUTO_HIDE_STATUS th 155 val th = APP_FRAME `cond ~(x1 = 0w:word32)` th 156 val th = SIMP_RULE (arith_ss++sep_ss++pcINC_ss) [wLENGTH_def,LENGTH,word_add_n2w] th 157 val th1 = APP_FRAME `R 1w y3` th1 158 val th1 = MOVE_PRE `S` th1 159 val th = SIMP_RULE (bool_ss++sep2_ss) [] th 160 val th1 = SIMP_RULE (bool_ss++sep2_ss) [] th1 161 val th = SIMP_RULE (bool_ss++sep_ss) [] (APP_MERGE th th1) 162 val th = RW [n2w_x_eq_0w,pcADD_0,INSERT_UNION_EQ,UNION_EMPTY] th 163 val th = RW1 [INSERT_COMM] th 164 val th = ABSORB_POST th 165 166 (* step 2: clean up pre- and postconditions *) 167 val th = AUTO_HIDE_POST1 [`R 0w`] th 168 val th = APP_WEAKEN1 th 169 `~R 0w * R 1w (f32(x1,y3)) * ~S` 170 (SIMP_TAC (bool_ss++sep2_ss) [SEP_IMP_MOVE_COND] 171 \\ ONCE_REWRITE_TAC [f32_def] \\ REWRITE_TAC [] 172 \\ SIMP_TAC (bool_ss++star_ss) [SEP_IMP_REFL]) 173 174 (* step 3: instantiate induction and extract ind hyp *) 175 val tm = extract_spec th [] [] [`x1`,`y3`] 176 val ind = Q.GEN `P` (SIMP_RULE bool_ss [FST,SND] (Q.SPEC `\x. P (FST x) (SND x)` f32_ind)) 177 val th1 = SIMP_RULE std_ss [] (ISPEC tm ind) 178 val asm = extract_assum th1 179 val asm = RW [GSYM ARM_PROG_MOVE_COND] asm 180 181 (* step 4: match step and prove postcondition *) 182 val asm = MATCH_MP ARM_PROG_COMPOSE_WEAKEN asm 183 val th = RW1 [GSYM (REWRITE_CONV [SEP_cond_CLAUSES] ``cond b * cond b``)] th 184 val th = RW [STAR_ASSOC] th 185(* val th = Q.INST [`x1`|->`x`,`y3`|->`a`] th *) 186 val th = RW1 [WORD_MULT_COMM] th 187 val th = MATCH_MP asm th (* MATCH_MP now works w.o. above Q.INST *) 188 val lemma = prove((fst o dest_imp o concl) th, 189 SIMP_TAC (bool_ss++sep2_ss) [SEP_IMP_MOVE_COND] \\ REPEAT STRIP_TAC 190 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [f32_def])) 191 \\ ASM_REWRITE_TAC [SEP_IMP_REFL]) 192 val th = MP th lemma 193 194 (* step 5: clean up *) 195(* val th = MATCH_MP th1 (tidy_up th1 th) *) 196 val th2 = Q.GEN `x1` (Q.GEN `y3` (DISCH_ALL th));; 197 val th = MATCH_MP th1 th2 198 val th = SPEC_ALL (Q.SPECL [`x`,`a`] th) 199 200 201