1(* 2loadPath := 3 (concat Globals.HOLDIR "/examples/dev/sw") :: 4 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 5 (concat Globals.HOLDIR "/examples/temporal_deep/src/tools") :: 6 (concat Globals.HOLDIR "/examples/sep") :: 7 !loadPath; 8 9app load ["pred_setLib","finite_mapTheory","rich_listTheory", "wordsLib", 10 "ILTheory", "rulesTheory", "preARMSyntax", "annotatedIR", 11 "funCall", "preARMTheory"]; 12 13quietdec := true; 14open numLib pairLib relationTheory pairTheory arithmeticTheory listSyntax 15 preARMTheory preARMSyntax Assem pred_setSimps pred_setTheory listTheory 16 rich_listTheory whileTheory finite_mapTheory declFuncs 17 annotatedIR ILTheory rulesTheory wordsLib wordsTheory IRSyntax; 18quietdec := false; 19*) 20 21structure mechReasoning = 22struct 23local open 24 HolKernel Parse boolLib bossLib numLib pairLib relationTheory 25 pairTheory arithmeticTheory listSyntax preARMTheory preARMSyntax 26 Assem pred_setSimps pred_setTheory listTheory rich_listTheory 27 whileTheory finite_mapTheory declFuncs annotatedIR ILTheory 28 rulesTheory wordsLib wordsTheory IRSyntax 29 infix ++ THENC THEN THENL |-> 30in 31 32val used_thm_num = ref 1; 33 34fun get_new_thm_name () = 35 let val n = !used_thm_num; 36 val _ = used_thm_num := (n+1); 37 in 38 "lemma_"^(Int.toString n) 39 end; 40 41(*---------------------------------------------------------------------------*) 42(* Simplifier on finite maps *) 43(*---------------------------------------------------------------------------*) 44 45fun mk_unchanged_set f_name = 46 let val {regs=regs,...} = declFuncs.getFunc f_name; 47 val univ_set = Binaryset.addList 48 (Binaryset.empty Int.compare, 49 [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]) 50 val neg_regs = Binaryset.difference(univ_set,regs) 51 in 52 neg_regs 53 end; 54 55fun mk_unchanged_term set = 56 let val int_list = Binaryset.listItems set; 57 fun mapper n = 58 let val n_term = term_of_int n 59 in rhs (concl (EVAL (mk_comb (Term `from_reg_index`, n_term)))) 60 end 61 val mreg_list = map mapper int_list 62 val changed_list = mk_list (mreg_list, Type`:MREG`); 63 in 64 changed_list 65 end; 66 67val fupdate_normalizer = 68 let val thm = SPEC_ALL FUPDATE_LT_COMMUTES 69 val pat = lhs(snd(dest_imp(concl thm))) 70 in 71 {name = "Finite map normalization", 72 trace = 2, 73 key = SOME([],pat), 74 conv = let fun reducer tm = 75 let val (theta,ty_theta) = match_term pat tm 76 val thm' = INST theta (INST_TYPE ty_theta thm) 77 val constraint = fst(dest_imp(concl thm')) 78 val cthm = EQT_ELIM(reduceLib.REDUCE_CONV constraint) 79 in MP thm' cthm 80 end 81 in 82 K (K reducer) 83 end} 84 end; 85 86val finmap_conv_frag = 87 simpLib.SSFRAG 88 {convs = [fupdate_normalizer], 89 rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]}; 90 91val finmap_ss = std_ss ++ finmap_conv_frag ++ 92 rewrites [FUPDATE_EQ, FAPPLY_FUPDATE_THM]; 93 94val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 95 96(*---------------------------------------------------------------------------------*) 97(* Assistant Functions *) 98(*---------------------------------------------------------------------------------*) 99 100 101 102(* make variable tuple, e.g. ((v0,v1),v2,...) *) 103 104fun mk_vars exp = 105 let 106 val i = ref (~1); 107 fun set_vars (IRSyntax.PAIR (e1,e2)) = 108 mk_pair(set_vars e1, set_vars e2) 109 | set_vars exp = 110 mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`) 111 in 112 set_vars exp 113 end 114 115(* make mread tuple, e.g. ((st<v0>,st<v1>),st<v2>,...) *) 116 117val mread_tm = prim_mk_const{Name = "mread", Thy="rules"}; 118val RR_tm = prim_mk_const{Name = "RR", Thy = "rules"}; 119val RM_tm = prim_mk_const{Name = "RM", Thy = "rules"}; 120 121fun mk_mreads st (IRSyntax.PAIR (e1,e2)) = 122 mk_pair(mk_mreads st e1, mk_mreads st e2) 123 | mk_mreads st (IRSyntax.REG e) = 124 list_mk_comb (mread_tm, 125 [st, mk_comb (RR_tm, IRSyntax.convert_reg (IRSyntax.REG e))]) 126 | mk_mreads st (IRSyntax.MEM m) = 127 list_mk_comb (mread_tm, 128 [st, mk_comb (RM_tm, IRSyntax.convert_mem (IRSyntax.MEM m))]) 129 | mk_mreads st _ = 130 (print "mk_mreads: invalid incoming expression"; 131 raise ERR "" ("mk_mreads: invalid incoming expression")); 132 133 134fun MEM_ADDR_CONV t = 135 let val (f, args) = dest_comb t; 136 val _ = if same_const (Term `MEM_ADDR`) f then () 137 else Raise (ERR "" "Syntax"); 138 val num_term = rand (rand args); 139 val num = dest_numeral num_term; 140 val (c, r) = Arbnum.divmod(num, Arbnum.fromInt 4); 141 val _ = if (r = Arbnum.zero) then () else Raise (ERR "" "Syntax"); 142 val mult_term = mk_mult(mk_numeral c, term_of_int 4); 143 val mult_thm = GSYM (EVAL mult_term); 144 val thm = RAND_CONV (RAND_CONV (REWRITE_CONV [mult_thm])) t 145 in 146 thm 147 end; 148 149val word_extract_thm = 150 GSYM ((SIMP_RULE std_ss [w2w_def, combinTheory.o_DEF, FUN_EQ_THM]) 151 word_extract_def); 152 153 154val SIM_REWRITE_CONV = REWRITE_CONV 155 [mdecode_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, 156 index_of_reg_def, WORD_ADD_0, FAPPLY_FUPDATE_THM, word4_distinct, 157 GSYM WORD_ADD_ASSOC, FUPDATE_EQ, fupdate_lt_commutes_word4, word_sub_def]; 158 159val SIM_CONV = 160 SIM_REWRITE_CONV THENC 161 WORDS_CONV THENC 162 REWRITE_CONV [word_extract_thm, WORD_ADD_0] 163 164val SIM_MEM_CONV = 165 SIM_REWRITE_CONV THENC 166 SIMP_CONV arith_ss [word4_distinct, MEM_ADDR_ADD_CONST_MOD, 167 GSYM WORD_ADD_ASSOC, WORD_EQ_ADD_LCANCEL] THENC 168 WORDS_CONV THENC 169 REWRITE_CONV [word_extract_thm, WORD_ADD_0] 170 171val SIM_PUSH_CONV = 172 REWRITE_CONV [mdecode_def, pushL_def, GSYM MAP_REVERSE, REVERSE_DEF, 173 APPEND, MAP, LENGTH, FOLDL] THENC 174 DEPTH_CONV GEN_BETA_CONV THENC 175 SIM_REWRITE_CONV THENC 176 SIMP_CONV arith_ss [MEM_ADDR_ADD_CONST_MOD] THENC 177 SIM_CONV; 178 179val SIM_POP_CONV = 180 REWRITE_CONV [mdecode_def, popL_def, GSYM MAP_REVERSE, 181 REVERSE_DEF, APPEND, MAP, LENGTH, FOLDL] THENC 182 DEPTH_CONV GEN_BETA_CONV THENC 183 SIM_REWRITE_CONV THENC 184 SIMP_CONV arith_ss [word4_distinct, MEM_ADDR_ADD_CONST_MOD, 185 GSYM WORD_ADD_ASSOC, WORD_EQ_ADD_LCANCEL] THENC 186 SIM_CONV; 187 188(* make a list of rules [exp0 <- v0, exp1 <- v1, ...] *) 189fun mk_subst_rules expL = 190 let 191 val i = ref (~1) 192 fun new_var() = (i := !i + 1; mk_var ("v"^Int.toString (!i), Type`:DATA`)) 193 in 194 List.map (fn exp => (exp |-> new_var())) expL 195 end 196 197fun read_one_var s exp = 198 let val v0 = IRSyntax.read_exp s exp; 199 fun conv (IRSyntax.MEM (b, off)) = SIM_MEM_CONV 200 | conv _ = SIM_CONV 201 val v1 = rhs (concl ((conv exp) v0)) 202 in 203 v1 204 end 205 206 207(*---------------------------------------------------------------------------------*) 208(* Symbolic Simulation of Instructions *) 209(*---------------------------------------------------------------------------------*) 210 211val ACCESS_CONV = SIMP_CONV finmap_ss 212 [mread_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def]; 213 214val ACCESS_RULE = CONV_RULE ACCESS_CONV; 215 216(*---------------------------------------------------------------------------*) 217(* Basic RULE for instructions execpt for PUSH and POP *) 218(*---------------------------------------------------------------------------*) 219 220(* Find the first instruction to be simulated next *) 221 222val doper_ty = mk_thy_type{Tyop="DOPER",Thy="IL",Args=[]};; 223val mdecode_tm = prim_mk_const{Name = "mdecode", Thy = "IL"}; 224 225fun locate_first_inst t = (type_of t = doper_ty); 226 227fun is_mdecode_exp t = same_const (#1 (strip_comb t)) mdecode_tm 228 229 230fun find_innermost_mdecode t = 231 let val state = rand (rator t) 232 in if is_mdecode_exp state 233 then find_innermost_mdecode state 234 else t 235 end 236 handle e as HOL_ERR _ => 237 (print "find_innermost_mdecode:syntax error"; Raise e); 238 239(*---------------------------------------------------------------------------*) 240(* eliminate all "decode"s and get the new state *) 241(*---------------------------------------------------------------------------*) 242 243val mpush_tm = prim_mk_const {Name="MPUSH", Thy="IL"}; 244val mpop_tm = prim_mk_const {Name="MPOP", Thy="IL"}; 245val mldr_tm = prim_mk_const {Name="MLDR", Thy="IL"}; 246val mstr_tm = prim_mk_const {Name="MSTR", Thy="IL"}; 247 248fun elim_decode th = 249 let val t1 = concl th 250 val st = if is_imp t1 then rhs (#2 (dest_imp t1)) else rhs t1 251 in 252 if is_pair st then th 253 else let val t1 = find_term locate_first_inst st 254 val operator = #1 (strip_comb t1); 255 val _ = print ("Simulating a " ^ 256 (#1 (dest_const operator)) ^ " instruction\n") 257 val t2 = find_innermost_mdecode st 258 val conv = if same_const operator mpush_tm then SIM_PUSH_CONV else 259 if same_const operator mpop_tm then SIM_POP_CONV else 260 if same_const operator mldr_tm then SIM_MEM_CONV else 261 if same_const operator mstr_tm then SIM_MEM_CONV 262 else SIM_CONV 263 val t2_thm = conv t2; 264 val th' = REWRITE_RULE [t2_thm] th 265 in elim_decode th' 266 end 267 end 268 handle e => 269 (print "get_blk_spec: errors occur while symbolically simulating a block! "; 270 Raise e); 271 272 273(*---------------------------------------------------------------------------*) 274(* Given a list of IR statements, return a theorem indicating the state *) 275(* after symbolic simulation. Note that pre_spec specifies the *) 276(* pre-conditions before the simulation *) 277(*---------------------------------------------------------------------------*) 278 279(* val stms = instL *) 280 281fun printProof [] = () | 282 printProof (e::l) = (print e;print "\n";printProof l) 283 284fun printProofToFile file_name p = 285 let val file_st = TextIO.openOut(file_name); 286 val _ = map (fn s => TextIO.output(file_st, s^"\n")) p; 287 val _ = TextIO.output(file_st, "\n\n"); 288 val _ = TextIO.flushOut file_st; 289 val _ = TextIO.closeOut file_st; 290 in 291 () 292 end; 293 294fun append_proofs [] = [] 295 | append_proofs [e] = e 296 | append_proofs (h::l) = h@[""]@(append_proofs l); 297 298val LET_ELIM_RULE = SIMP_RULE std_ss [LET_THM]; 299 300fun SPLIT_SPEC_RULE spec = 301 let val thmL = CONJUNCTS (LET_ELIM_RULE spec) 302 in (el 1 thmL, el 2 thmL, el 3 thmL) 303 end; 304 305fun make_proof_string term tac = 306 let val name = get_new_thm_name (); 307 val line1 = "val "^name^" = prove ("; 308 val line2 = "``"^(term_to_string term)^"``,"; 309 val tac' = map (fn s => (" "^s)) tac; 310 in 311 (name, (line1::line2::tac')@[");"]) 312 end; 313 314fun cheat_tac (asl,g) = ACCEPT_TAC(ASSUME g) (asl,g); 315 316fun make_assume_string term = 317 let val name = get_new_thm_name (); 318 val line1 = "val "^name^" = mk_oracle_thm \"ARM-Compiler\""; 319 val line2 = "([], ``"^(term_to_string term)^"``);"; 320 in 321 (name, [line1,line2]) 322 end; 323 324fun make_proof_split_spec thm_name = 325 let val name1 = get_new_thm_name (); 326 val name2 = get_new_thm_name (); 327 val name3 = get_new_thm_name (); 328 val line = "val ("^name1^","^name2^","^name3^") = SPLIT_SPEC_RULE " 329 ^thm_name^";" 330 in 331 ([name1, name2, name3], [line]) 332 end; 333 334fun sim_stms_CONV instance = 335 let val th0 = REWRITE_CONV [IR_SEMANTICS_BLK] instance; 336 val th1 = SIMP_RULE std_ss [mread_def, toMEM_def, toREG_def, 337 index_of_reg_def, read_thm] th0 338 val th2 = elim_decode th1 (* symbolically simulate the block *) 339 in 340 th2 341 end; 342 343fun sim_stms blk = 344 let val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), 345 mk_var ("mem", Type `:ADDR |-> DATA`)) 346 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [blk, st]); 347 348 val thm = sim_stms_CONV instance; 349 350 val (name, proof) = make_proof_string (concl thm) 351 ["CONV_TAC (LHS_CONV sim_stms_CONV) THEN", "REWRITE_TAC[]"] 352 353 in 354 (thm, name, proof) 355 end; 356 357 358(*---------------------------------------------------------------------------------*) 359(* PSPEC specification and Mechanized Reasoning *) 360(*---------------------------------------------------------------------------------*) 361 362(* Make a PSPEC specification *) 363 364val basic_outL = [IRSyntax.REG 11, IRSyntax.REG 13]; (* fp and sp *) 365 366val PSPEC_term = Term `PSPEC:('a, 'b, 'c) PSPEC_TYPE`; 367 368 369fun mk_PSPEC ir (pre_st,post_st) (ins,outs) = 370 let 371 372 fun calculate_outs st (IRSyntax.PAIR (a,b)) = 373 mk_pair (calculate_outs st a, calculate_outs st b) 374 | calculate_outs st exp = 375 read_one_var st exp 376 377 fun clean_pair (IRSyntax.PAIR (a,b)) = 378 IRSyntax.PAIR (clean_pair a, clean_pair b) 379 | clean_pair (IRSyntax.REG r) = IRSyntax.REG r 380 | clean_pair (IRSyntax.MEM (r, off)) = IRSyntax.MEM (r, off) 381 | clean_pair _ = IRSyntax.NA 382 383 val ins = trim_pair (clean_pair ins); 384 val outs = trim_pair (clean_pair outs); 385 386 (* the characteristic function *) 387 val rules = mk_subst_rules (List.map (read_one_var pre_st) (IRSyntax.pair2list ins)); 388 val (initV,out_vars) = (mk_vars ins, mk_vars outs); 389 val f_c = mk_pabs (initV, subst rules (calculate_outs post_st outs)); (* the charateristic function *) 390 391 (* the pre-condition and the post-condition *) 392 393 val st' = mk_var ("st", Type `:DSTATE`); 394 395 (* the stack function *) 396 val stk_f = mk_pabs (st', Term `T`); 397 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 398 399 (* the projective specification *) 400 val (in_f,out_f) = (mk_pabs (st', mk_mreads st' ins), mk_pabs (st', mk_mreads st' outs)); 401 val pspec = list_mk_comb (inst [{redex = alpha, residue = stk_tp}, 402 {redex = beta, residue = type_of initV}, 403 {redex = gamma, residue = type_of out_vars}] (PSPEC_term), 404 [ir, mk_pair(stk_f, stk_f), stk_f, list_mk_pair[in_f,f_c,out_f]]); 405 in 406 pspec 407 end; 408 409(*---------------------------------------------------------------------------*) 410(* Symbolic Simulation of Basic Blocks *) 411(* *) 412(* Given a basic block, the charateristic function on inputs and outputs is *) 413(* derived by symbolic simulation and the context about unchanged variables *) 414(* is maintained. Finally well_formed information is given. *) 415(*---------------------------------------------------------------------------*) 416(* 417fun extract (annotatedIR.BLK (instL,{ins = ins, outs = outs, context = context, ...})) = 418(instL, ins, outs, context); 419val (instL, ins, outs, context) = extract f_ir; 420val (unchanged_list, _) = unchanged_lists_weak 421val unchanged_list = emptyset 422mk_blk_spec pre_ir unchanged_lists_weak 423val stack_size = 1 424*) 425 426fun blk_UNCHANGED_TAC spec = 427 REWRITE_TAC[UNCHANGED_THM, spec, EVERY_DEF] THEN 428 BETA_TAC THEN 429 REWRITE_TAC[read_thm, toREG_def, index_of_reg_def, FAPPLY_FUPDATE_THM, word4_distinct]; 430 431fun blk_USED_STACK_TAC stack_size spec = 432 let 433 val stack_size_thm = 434 let 435 val nterm = mk_comb (Term `LIST_COUNT`, (term_of_int stack_size)); 436 in 437 (REDEPTH_CONV num_CONV) nterm handle UNCHANGED => REFL nterm 438 end 439 in 440 (REWRITE_TAC [USED_STACK_THM, spec, MAP, read_thm, Once stack_size_thm, LIST_COUNT_def] THEN 441 SIMP_TAC list_ss [] THEN 442 CONV_TAC WORDS_CONV THEN 443 ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]) 444 end; 445 446fun blk_SPEC_TAC unchanged_thm used_stack_thm spec = 447 ( 448 SIMP_TAC std_ss [LET_THM, PSPEC_def, HSPEC_def, FORALL_DSTATE, BLOCK_IS_WELL_FORMED, read_thm, unchanged_thm, UNCHANGED_STACK_def, used_stack_thm] THEN 449 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm, spec] THEN 450 CONV_TAC SIM_MEM_CONV THEN 451 SIMP_TAC std_ss [pair_induction] 452 ); 453 454 455fun mk_blk_spec (annotatedIR.BLK (instL,{ins = ins, outs = outs, context = context, ...})) unchanged_list = 456 let 457 val (blk, stack_size) = IRSyntax.convert_instL instL; 458 val (th, th_name, th_proof) = sim_stms blk; 459 val t1 = concl th; 460 val spec_terms = (#2 (strip_comb (lhs t1)), rhs t1); 461 val blk_ir = el 1 (#1 spec_terms); 462 val pre_st = el 2 (#1 spec_terms); 463 val post_st = #2 spec_terms; 464 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 465 466 val f_spec = mk_PSPEC blk_ir (pre_st,post_st) (ins,outs); 467 val f_spec' = subst [{redex = blk_ir, residue = ir_abbr}] f_spec; 468 469 val unchanged_term = list_mk_comb (Term`UNCHANGED`, [mk_unchanged_term unchanged_list, blk_ir]); 470 471 val unchanged_thm = prove (unchanged_term, (* set_goal ([],unchanged_term) *) 472 blk_UNCHANGED_TAC th); 473 val (unchanged_thm_name, unchanged_thm_proof) = make_proof_string unchanged_term 474 ["blk_UNCHANGED_TAC "^th_name] 475 476 val used_stack_term = list_mk_comb (Term`USED_STACK`, [ term_of_int stack_size, blk_ir]); 477 478 val used_stack_thm = prove (used_stack_term, (* set_goal ([],used_stack_term) *) 479 blk_USED_STACK_TAC stack_size th) 480 481 val (used_stack_thm_name, used_stack_thm_proof) = make_proof_string used_stack_term 482 ["blk_USED_STACK_TAC "^(Int.toString stack_size)^" "^th_name] 483 484 val unchanged_spec = list_mk_comb (Term`UNCHANGED_STACK`, [mk_unchanged_term unchanged_list, term_of_int stack_size, ir_abbr]); 485 486 487 (* well_formedness *) 488 val wf_spec = mk_comb (Term`WELL_FORMED`, ir_abbr); 489 490 (* specifiction of functional correctness *) 491 val fspec = mk_let (mk_abs (ir_abbr, list_mk_conj [f_spec', wf_spec, unchanged_spec]), blk_ir); 492 493 val spec = prove (fspec, (* set_goal ([],fspec) *) 494 blk_SPEC_TAC unchanged_thm used_stack_thm th) 495 496 val (spec_thm_name, spec_thm_proof) = make_proof_string fspec 497 ["blk_SPEC_TAC "^unchanged_thm_name^" "^used_stack_thm_name^" "^th_name] 498 499 val proofs = append_proofs [th_proof, unchanged_thm_proof, used_stack_thm_proof, spec_thm_proof] 500 in 501 (spec, spec_thm_name, th, th_name, proofs) 502 end 503 | mk_blk_spec _ _ = 504 raise Fail "mk_blk_spec: BLK is expected!"; 505 506 507 508(* Obtain the specification associated with pointers *) 509fun get_p_spec spec = 510 let 511 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 512 val (t0,t1) = strip_comb (concl th0) 513 in 514 List.nth (t1,1) 515 end 516 517 518 fun make_unchanged_stack_term u_spec1 u_spec2 ir = 519 let 520 val stack_size1 = rand (rator u_spec1) 521 val stack_size2 = rand (rator u_spec2) 522 val stack_size = list_mk_comb (Term `MAX`, [stack_size1, stack_size2]); 523 val body = rator (rator (u_spec1)) 524 in 525 list_mk_comb (body, [stack_size, ir]) 526 end 527 528(*---------------------------------------------------------------------------------*) 529(* Specification for Sequential Composition *) 530(*---------------------------------------------------------------------------------*) 531 532(* retrieve information from a PSPEC specification *) 533fun get_spec_info spec = 534 let val f_spec = hd (strip_conj spec); 535 val (_, [ir, ps, stk_f, fs]) = strip_comb f_spec; 536 val (ps1,ps2) = dest_pair ps; 537 val list0 = strip_pair fs; 538 val (in_f, f_c, out_f) = (#2 (dest_abs (hd list0)), List.nth(list0,1), #2 (dest_abs (List.nth(list0,2)))) 539 in 540 (ir, (ps1, ps2), stk_f, (in_f, f_c, out_f)) 541 end 542 handle e => (print "get_spec_info: the input is not valid PSPEC and UNCHANGED"; Raise e); 543 544(* 545val (ir1_spec, ir1_spec_name, ir1_wf, ir1_wf_name, ir2_spec, ir2_spec_name, ir2_wf, ir2_wf_name, proofs) = 546( 547(el 1 specL1), (el 1 specL1_name), (el 2 specL1), (el 2 specL1_name), (el 1 specL2), (el 1 specL2_name), (el 2 specL2), (el 2 specL2_name), []) 548*) 549 550fun sc_SPEC_TAC ir1_spec ir2_spec ir1_wf ir2_wf post_p1 out_f1 = 551 MATCH_MP_TAC PRJ_SC_RULE THEN 552 EXISTS_TAC post_p1 THEN EXISTS_TAC out_f1 THEN 553 SIMP_TAC std_ss [ir1_spec, ir2_spec, ir1_wf, ir2_wf] THEN 554 MP_TAC ir2_spec THEN 555 SIMP_TAC std_ss [PSPEC_def, HSPEC_def] 556 557fun sc_WELL_FORMED_TAC ir1_wf ir2_wf = 558 ONCE_REWRITE_TAC [GSYM IR_SC_IS_WELL_FORMED] THEN 559 SIMP_TAC std_ss [ir1_wf, ir2_wf]; 560 561 562fun mk_sc_spec___pre ir1_spec ir1_spec_name ir1_wf ir1_wf_name ir2_spec ir2_spec_name ir2_wf ir2_wf_name proofs = 563 let 564 val (ir1,(pre_p1,post_p1),stk_f,(ins1,f1,outs1)) = get_spec_info (concl ir1_spec); 565 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (concl ir2_spec); 566 567 (* SC (ir1, ir2) *) 568 val sc_ir = list_mk_comb (Term`IL$SC`, [ir1, ir2]); 569 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 570 val st = mk_var ("st", Type `:DSTATE`); 571 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [sc_ir, st]); 572 573 (* the characteristic function of SC *) 574 val sc_f = combinSyntax.mk_o (f2,f1); 575 val (in_f,out_f) = (mk_pabs (st,ins1), mk_abs (st,outs2)); 576 val out_f1 = mk_pabs (st, outs1); 577 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 578 579 (* the SC specification *) 580 val f_spec = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of ins1, gamma |-> type_of outs2] (PSPEC_term), 581 [sc_ir, mk_pair(pre_p1, post_p2), stk_f, list_mk_pair[in_f,sc_f,out_f]]); 582 583 val f_th = prove (f_spec, (* set_goal ([],f_spec) *) 584 sc_SPEC_TAC ir1_spec ir2_spec ir1_wf ir2_wf post_p1 out_f1 585 ) 586 587 val _ = show_types := true; 588 val post_p1_string = term_to_string post_p1; 589 val out_f1_string = term_to_string out_f1; 590 val _ = show_types := false; 591 val (f_th_name, f_th_proof) = make_proof_string f_spec 592 ["sc_SPEC_TAC "^ir1_spec_name^" "^ir2_spec_name^" " 593 ^ir1_wf_name^" "^ir2_wf_name^" (Term `"^post_p1_string^"`) (Term `"^out_f1_string^"`)"] 594 595 val sc_f_thm = (SIMP_CONV std_ss [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] sc_f); 596 val (sc_f_thm_name, sc_f_thm_proof) = make_proof_string (concl sc_f_thm) 597 ["CONV_TAC (LHS_CONV (SIMP_CONV std_ss [combinTheory.o_DEF, pairTheory.LAMBDA_PROD])) THEN", "REWRITE_TAC[]"] 598 599 val f_th = REWRITE_RULE [sc_f_thm] f_th 600 val (f_th_name', f_th_proof') = make_proof_string (concl f_th) 601 ["REWRITE_TAC [Once (GSYM "^sc_f_thm_name^"), "^f_th_name^"]"] 602 603 604 val well_formed_spec = mk_comb (Term`WELL_FORMED`, sc_ir); 605 val well_formed_th = prove (well_formed_spec, (* set_goal ([],well_formed_spec) *) 606 sc_WELL_FORMED_TAC ir1_wf ir2_wf 607 ); 608 val (well_formed_th_name, well_formed_th_proof) = make_proof_string well_formed_spec 609 ["sc_WELL_FORMED_TAC "^ir1_wf_name^" "^ir2_wf_name] 610 611 val proofs' = append_proofs [proofs, f_th_proof, sc_f_thm_proof, f_th_proof', well_formed_th_proof]; 612 613 in 614 (f_th, f_th_name', well_formed_th, well_formed_th_name, sc_ir, proofs') 615 end; 616 617(* 618val (ir1_spec, ir1_name, ir2_spec, ir2_name, proofs) = (spec1, spec1_name, spec2, spec2_name, []) 619 620 mk_sc_spec spec1 spec1_name spec2 spec2_name unchanged_list proofs2 621 622*) 623 624fun sc_UNCHANGED_TAC ir1_wf ir1_unchanged ir2_wf ir2_unchanged = 625 MATCH_MP_TAC IR_SC_UNCHANGED_STACK THEN 626 SIMP_TAC list_ss [ir1_unchanged, ir2_unchanged, ir1_wf, ir2_wf] 627 628 629fun mk_sc_spec ir1_spec ir1_name ir2_spec ir2_name proofs = 630 let 631 val specL1 = CONJUNCTS (LET_ELIM_RULE ir1_spec) 632 val (specL1_name, specL1_proof) = make_proof_split_spec ir1_name; 633 val specL2 = CONJUNCTS (LET_ELIM_RULE ir2_spec) 634 val (specL2_name, specL2_proof) = make_proof_split_spec ir2_name; 635 636 val proofs' = append_proofs [proofs, specL1_proof, specL2_proof]; 637 val (ir_spec, ir_spec_name, ir_wf, ir_wf_name, sc_ir, proofs'') = 638 mk_sc_spec___pre (el 1 specL1) (el 1 specL1_name) (el 2 specL1) (el 2 specL1_name) (el 1 specL2) (el 1 specL2_name) (el 2 specL2) (el 2 specL2_name) proofs'; 639 640 val unchanged_spec = make_unchanged_stack_term (concl (el 3 specL1)) (concl (el 3 specL2)) sc_ir 641 642 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) 643 sc_UNCHANGED_TAC (el 2 specL1) (el 3 specL1) (el 2 specL2) (el 3 specL2) 644 ); 645 val (unchanged_th_name, unchanged_th_proof) = make_proof_string unchanged_spec 646 ["sc_UNCHANGED_TAC "^(el 2 specL1_name)^" "^(el 3 specL1_name)^" "^(el 2 specL2_name)^" "^(el 3 specL2_name)] 647 648 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 649 val spec = subst [sc_ir |-> ir_abbr] (list_mk_conj [concl ir_spec, concl ir_wf, unchanged_spec]); 650 val spec' = mk_let (mk_abs (ir_abbr, spec), sc_ir); 651 652 val th = prove (spec', (* set_goal ([],spec') *) 653 SIMP_TAC std_ss [LET_THM, ir_spec, ir_wf, unchanged_th] 654 ) 655 656 val (th_name, th_proof) = make_proof_string spec' 657 ["SIMP_TAC std_ss [LET_THM,"^ir_spec_name^","^ 658 ir_wf_name^","^unchanged_th_name^"]"] 659 660 val proofs''' = append_proofs[proofs'', unchanged_th_proof, th_proof] 661(* 662 val sc_th_term = mk_comb(mk_comb (Term`run_ir`,sc_ir), Term `(r, m):DSTATE`); 663 val sc_th = 664 (SIMP_CONV std_ss [IR_SEMANTICS_SC, 665 ir1_spec, ir2_spec, ir1_th, ir2_th] THENC 666 SIM_MEM_CONV) sc_th_term;*) 667 668 669 in 670 (th, th_name, proofs''') 671 end; 672 673(*---------------------------------------------------------------------------------*) 674(* Specification for Function Calls *) 675(*---------------------------------------------------------------------------------*) 676 677fun compute_outL modifiedRegL = 678 let val i = ref 0 679 in 680 List.map (fn e => (i := !i - 1; IRSyntax.MEM (11, !i))) ([12, 11] @ (List.rev modifiedRegL)) (* neglect pc and lr *) 681 end 682 683 684 685fun fc_body_PSPEC body_pspec body_unchanged new_stack_size = 686 let 687 val new_stack_size_thm = 688 let 689 val nterm = mk_comb (Term `LIST_COUNT`, (term_of_int new_stack_size)); 690 in 691 (REDEPTH_CONV num_CONV) nterm handle UNCHANGED => REFL nterm 692 end 693 in 694 MP_TAC (body_pspec) THEN 695 SIMP_TAC std_ss [PSPEC_def, HSPEC_def, mread_def] THEN 696 DISCH_TAC THEN POP_ASSUM (fn t => ALL_TAC) THEN 697 REPEAT STRIP_TAC THEN ( 698 699 MP_TAC (body_unchanged) THEN 700 MATCH_MP_TAC UNCHANGED_STACK___READ_STACK_IMP THEN 701 SIMP_TAC list_ss [] 702 ) 703 end 704 705 706fun fc_UNCHANGED_TAC rewrites bodyUnchanged= 707 let 708 val common_rewrites = SIMP_RULE std_ss [UNCHANGED_STACK_def, 709 WELL_FORMED_thm] (LET_ELIM_RULE (LIST_CONJ rewrites)); 710 in 711 (REWRITE_TAC [UNCHANGED_STACK_def] THEN 712 CONJ_TAC THENL [ 713 SIMP_TAC std_ss [UNCHANGED_THM, common_rewrites, 714 Once IR_SEMANTICS_SC, Once IR_SEMANTICS_SC, 715 WELL_FORMED_thm, GSYM RIGHT_FORALL_IMP_THM, EVERY_MEM] THEN 716 REPEAT GEN_TAC THEN 717 (fn (a, g) => 718 let 719 val (_, t1) = dest_imp g; 720 val t2 = (lhs t1); 721 val t3 = rand (rand (rator t2)); 722 val t4 = Term `?r'' m''. ^t3 = (r'', m'')` 723 val thm = METIS_PROVE [pairTheory.PAIR] t4 724 in 725 ASSUME_TAC thm (a,g) 726 end) THEN 727 FULL_SIMP_TAC std_ss [common_rewrites] THEN 728 SPEC_TAC (Term `r:MREG`, Term `r:MREG`) THEN 729 SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM, toREG_def, index_of_reg_def, read_thm] THEN 730 CONV_TAC SIM_MEM_CONV THEN 731 732 (fn (a, g) => 733 let 734 val thm =CONJUNCT1 ( 735 REWRITE_RULE [UNCHANGED_STACK_def] bodyUnchanged); 736 val thm2 = SIMP_RULE std_ss [UNCHANGED_THM, 737 EVERY_MEM, GSYM RIGHT_FORALL_IMP_THM] thm 738 val (r,m) = dest_pair (rand (lhs (hd a))) 739 val thm3 = SPECL [Term `r:MREG`, r, m] thm2; 740 val thm4 = GEN (Term `r:MREG`) thm3; 741 in 742 MP_TAC thm4 (a,g) 743 end) THEN 744 ASM_REWRITE_TAC[] THEN 745 746 SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM, toREG_def, index_of_reg_def, read_thm] THEN 747 CONV_TAC SIM_MEM_CONV THEN 748 METIS_TAC[], 749 750 MATCH_MP_TAC IR_SC_USED_STACK___FC_CASE1 THEN 751 CONJ_TAC THENL [ 752 MATCH_MP_TAC IR_SC_USED_STACK___FC_CASE2 THEN 753 SIMP_TAC std_ss [common_rewrites, WELL_FORMED_thm, read_thm] THEN 754 CONV_TAC SIM_MEM_CONV THEN 755 ONCE_REWRITE_TAC[GSYM n2w_mod] THEN 756 SIMP_TAC std_ss [WORD_ADD_0, dimword_32, dimword_4], 757 758 759 SIMP_TAC std_ss [common_rewrites, WELL_FORMED_thm, read_thm, 760 Once IR_SEMANTICS_SC] THEN 761 762 ASSUME_TAC ( 763 CONJUNCT1 ( 764 REWRITE_RULE [UNCHANGED_STACK_def] bodyUnchanged)) (*body UNCHANGED*) THEN 765 FULL_SIMP_TAC list_ss [UNCHANGED_THM, EVERY_MEM, DISJ_IMP_THM, FORALL_AND_THM, toREG_def, index_of_reg_def] THEN 766 CONV_TAC SIM_MEM_CONV THEN 767 ONCE_REWRITE_TAC[GSYM n2w_mod] THEN 768 SIMP_TAC std_ss [WORD_ADD_0, dimword_32, dimword_4] 769 ] 770 ]) 771 end; 772 773 774fun mk_fc_spec (pre_spec, pre_spec_name, body_spec, body_spec_name, post_spec, post_spec_name, pre_th, pre_th_name, post_th, post_th_name, proofs, unchanged_list) = 775 let 776 val preL = CONJUNCTS (LET_ELIM_RULE pre_spec) 777 val (preL_name, preL_proof) = make_proof_split_spec pre_spec_name; 778 779 val bodyL = CONJUNCTS (LET_ELIM_RULE body_spec) 780 val (bodyL_name, bodyL_proof) = make_proof_split_spec body_spec_name; 781 782 val postL = CONJUNCTS (LET_ELIM_RULE post_spec) 783 val (postL_name, postL_proof) = make_proof_split_spec post_spec_name; 784 785 val proofs' = append_proofs [proofs, preL_proof, bodyL_proof, postL_proof]; 786 787 fun fix_body_spec pre_spec body_spec post_spec = 788 let 789 val (_,_,_,(_,_,outs_pre)) = get_spec_info (concl (LET_ELIM_RULE pre_spec)); 790 val (_,_,_,(ins_post,_,_)) = get_spec_info (concl (LET_ELIM_RULE post_spec)); 791 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (concl (LET_ELIM_RULE body_spec)); 792 793 fun extend_f f 0 = f | 794 extend_f f n = 795 let 796 val (vars, body) = dest_pabs f; 797 val newvar = variant ((free_vars vars)@(free_vars body)) (Term `v_gen:DATA`); 798 val body' = mk_pair (newvar,body); 799 val vars' = mk_pair (newvar,vars); 800 val f' = mk_pabs (vars', body') 801 in 802 extend_f f' (n-1) 803 end; 804 805 806 val ins_l = length (strip_pair ins) 807 val new_ins_l = length (strip_pair outs_pre) 808 val f' = extend_f f (new_ins_l - ins_l) 809 810 val st = mk_var ("st", Type `:DSTATE`); 811 val arg' = list_mk_pair [mk_abs(st, outs_pre), f', mk_abs(st, ins_post)] 812 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 813 814 val spec_term = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of outs_pre, gamma |-> type_of ins_post] (PSPEC_term), 815 [ir, mk_pair(pre_p, post_p), stk_f, 816 arg']); 817 in 818 (spec_term, ir) 819 end 820 821 val (body_spec_term, body_ir) = fix_body_spec pre_spec body_spec post_spec; 822 823 val new_stack = rand (rator (concl (el 3 preL))) 824 val body_stack = rand (rator (concl (el 3 bodyL))) 825 val new_stack_size_thm = 826 let 827 val nterm = mk_comb (Term `LIST_COUNT`, new_stack); 828 in 829 (REDEPTH_CONV num_CONV) nterm handle UNCHANGED => REFL nterm 830 end 831 832 val body_PSPEC = prove (body_spec_term, (*set_goal ([], body_spec_term)*) 833 834 fc_body_PSPEC (el 1 bodyL) (el 3 bodyL) (int_of_term new_stack)); 835 val (body_PSPEC_name, body_PSPEC_proof) = make_proof_string 836 body_spec_term 837 ["fc_body_PSPEC "^(el 1 bodyL_name)^" "^(el 3 bodyL_name)^" "^(term_to_string new_stack)] 838 839 840 val bodyL = body_PSPEC :: (tl bodyL); 841 val bodyL_name = body_PSPEC_name :: (tl bodyL_name); 842 val proofs'' = append_proofs [proofs', body_PSPEC_proof]; 843 844 val (ir_spec1, ir_spec1_name, ir_wf1, ir_wf1_name, _, proofs''') = 845 mk_sc_spec___pre (el 1 preL) (el 1 preL_name) (el 2 preL) (el 2 preL_name) (el 1 bodyL) (el 1 bodyL_name) (el 2 bodyL) (el 2 bodyL_name) proofs''; 846 847 val (ir_spec, ir_spec_name, ir_wf, ir_wf_name, sc_ir, proofs'''') = 848 mk_sc_spec___pre ir_spec1 ir_spec1_name ir_wf1 ir_wf1_name (el 1 postL) (el 1 postL_name) (el 2 postL) (el 2 postL_name) proofs'''; 849 850(* 851 val sc_th_term = mk_comb(mk_comb (Term`run_ir`,sc_ir), Term `(r, m):DSTATE`); 852 853 val sc_th = 854 (SIMP_CONV std_ss [IR_SEMANTICS_SC, 855 pre_th, post_th, body_th, 856 pre_spec, body_spec, post_spec, ir_wf1] THENC 857 SIM_MEM_CONV) sc_th_term;*) 858 859 val sum_stack = numSyntax.mk_plus (numSyntax.mk_plus (new_stack, body_stack), numSyntax.zero_tm) 860 val unchanged_spec = list_mk_comb (Term`UNCHANGED_STACK`, [mk_unchanged_term unchanged_list, sum_stack, sc_ir]); 861 862 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) fc_UNCHANGED_TAC [pre_spec, body_spec, post_spec, 863 pre_th, post_th] (el 3 bodyL) 864 ); 865 val (unchanged_th_name, unchanged_th_proof) = make_proof_string 866 unchanged_spec 867 ["fc_UNCHANGED_TAC ["^ 868 pre_spec_name^","^ 869 body_spec_name^","^ 870 post_spec_name^","^ 871 pre_th_name^","^ 872 post_th_name^"] "^ 873 (el 3 bodyL_name)]; 874 875 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 876 val spec = subst [sc_ir |-> ir_abbr] (list_mk_conj [concl ir_spec, concl ir_wf, unchanged_spec]); 877 val spec' = mk_let (mk_abs (ir_abbr, spec), sc_ir); 878 879 val th = prove (spec', (* set_goal ([],spec') *) 880 SIMP_TAC std_ss [LET_THM, unchanged_th, ir_spec, ir_wf] 881 ) 882 val (th_name, th_proof) = make_proof_string 883 spec' 884 ["SIMP_TAC std_ss [LET_THM,"^ 885 unchanged_th_name^","^ 886 ir_spec_name^","^ 887 ir_wf_name^"]"]; 888 val proofs''''' = append_proofs [proofs'''', unchanged_th_proof, th_proof]; 889 in 890 (th, th_name, proofs''''') 891 end; 892 893(*---------------------------------------------------------------------------------*) 894(* Specification for input/output matching *) 895(*---------------------------------------------------------------------------------*) 896 897(* 898PROJ_POST_RULE 899 |- !ir in_f out_f convert_f. 900 PSPEC ir (pre_p,post_p) (in_f,f,out_f) ==> 901 PSPEC ir (pre_p,post_p) (in_f,convert_f o f,convert_f o out_f) : thm 902 903 904fun mk_match_spec spec in_f2 = 905 let 906 907 val (_, (pre_p1, post_p1), (in_f1, f_c, out_f1), _) = get_spec_info spec; 908 909 910 in 911 th 912 end; 913*) 914 915 916 917(*---------------------------------------------------------------------------------*) 918(* Specification for Tail Recursion *) 919(*---------------------------------------------------------------------------------*) 920 921(* Given a TR, the charateristic function on inputs and outputs are derived by the TR_RULE *) 922(* and the context about unchanged variables is maintained *) 923 924fun convert_cond (exp1, rop, exp2) = 925 let 926 val cond_t0 = list_mk_pair [IRSyntax.convert_reg exp1, 927 IRSyntax.convert_rop rop, 928 IRSyntax.convert_exp exp2]; 929 in 930 cond_t0 931 end 932 handle e => (print "mk_cond: errors occur while converting the condition"; Raise e); 933 934fun strip_pair2 t = 935 if is_pair t then List.foldl (fn (t0,L0) => L0 @ (strip_pair2 t0)) [] (strip_pair t) 936 else [t]; 937 938 939fun mk_cj_cond cond_t ins = 940 let 941 val st = mk_var ("st", Type `:DSTATE`); 942 val instance = list_mk_comb (Term`eval_il_cond`, [cond_t, st]); 943 944 val read_const_th = prove (Term`!st v. read st (WCONST v) = v`, SIMP_TAC std_ss [FORALL_DSTATE, read_thm]); 945 946 val th0 = REWRITE_CONV [ARMCompositionTheory.eval_cond_def, 947 ILTheory.eval_il_cond_def, 948 ILTheory.translate_condition_def, 949 ILTheory.toREG_def, 950 ILTheory.toEXP_def, 951 ILTheory.index_of_reg_def] instance; 952 val th1 = REWRITE_RULE [read_const_th] th0; 953 val th1 = WORDS_RULE th1; 954 val instance1 = rhs (concl th1); 955 956 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)); 957 val cj_cond = subst rules instance1 (* the condition function *) 958 in 959 cj_cond 960 end 961 962fun mk_cond_f cond_t ins = (* the condition function *) 963 let 964 val rules = mk_subst_rules (strip_pair2 ins) 965 in 966 mk_pabs (subst rules ins, mk_cj_cond cond_t ins) 967 end 968 969fun guessR2 tp = 970 let val tp1 = List.nth(#2 (dest_type tp),1) 971 in 972 (Term`(measure (w2n o FST)):(word32#word32)->(word32#word32)->bool`) 973 end 974 975 976fun tr_WF_TAC body_spec initVType prj_f f cond_f_0 (asm, g) = 977 let 978 val my_WF_TR_LEM_2 = INST_TYPE [alpha |-> initVType] WF_TR_LEM_2 979 in 980 (MATCH_MP_TAC my_WF_TR_LEM_2 THEN 981 EXISTS_TAC prj_f THEN EXISTS_TAC f THEN EXISTS_TAC cond_f_0 THEN 982 SIMP_TAC std_ss [SIMP_RULE std_ss [PSPEC_def, HSPEC_def, LET_THM] body_spec] THEN 983 SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, 984 eval_il_cond_def, translate_condition_def, toEXP_def, 985 index_of_reg_def,toREG_def, toMEM_def, read_thm] THEN 986 WORDS_TAC THEN 987 SIMP_TAC std_ss [] THEN 988 MATCH_MP_TAC (INST_TYPE [alpha |-> initVType] WF_TR_LEM_3) THEN 989 (let val r = guessR2 (initVType) in 990 WF_REL_TAC `^r` THEN 991 WORDS_TAC THEN 992 RW_TAC std_ss [WORDS_RULE 993 (INST_TYPE [alpha |-> Type `:i32`] WORD_PRED_THM)] 994 end 995 handle e => (print "fail to prove totalness, add statement into assumption list"; cheat_tac) 996 )) (asm, g) 997 end 998 999fun tr_PSPEC_TAC wf_th body_spec = 1000 ASSUME_TAC wf_th THEN 1001 MATCH_MP_TAC PRJ_TR_RULE THEN 1002 SIMP_TAC std_ss [SIMP_RULE std_ss [LET_THM] body_spec] THEN 1003 STRIP_TAC THENL [ 1004 RW_TAC std_ss [], 1005 SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, eval_il_cond_def, translate_condition_def, 1006 index_of_reg_def, toREG_def, toEXP_def, toMEM_def, read_thm] THEN 1007 WORDS_TAC THEN 1008 SIMP_TAC std_ss [] 1009 ] 1010 1011fun tr_WELL_FORMED_TAC wf_th body_spec = 1012 ASSUME_TAC wf_th THEN 1013 MATCH_MP_TAC WELL_FORMED_TR_RULE THEN 1014 SIMP_TAC std_ss [SIMP_RULE std_ss [LET_THM] body_spec] THEN 1015 RW_TAC std_ss [] 1016 1017fun tr_UNCHANGED_TAC well_formed_th body_spec = 1018 MATCH_MP_TAC UNCHANGED_STACK_TR_RULE THEN 1019 SIMP_TAC list_ss [well_formed_th, SIMP_RULE std_ss [LET_THM] body_spec] 1020 1021 1022fun mk_tr_spec cond body_spec body_name proofs = 1023 let 1024 val specL = strip_conj (concl (LET_ELIM_RULE body_spec)); 1025 val (body_ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd specL); 1026 1027 val t_cond = convert_cond cond; 1028 val tr_ir = list_mk_comb (Term`TR`, [t_cond, body_ir]); 1029 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 1030 val st = mk_var ("st", Type `:DSTATE`); 1031 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [tr_ir, st]); 1032 1033 val initV = #1 (dest_pabs f); 1034 1035 val cond_f_0 = mk_cond_f t_cond ins; 1036 val cond_f = combinSyntax.mk_o (Term `$~:bool->bool`, cond_f_0); 1037 1038 val tr_f = list_mk_comb (inst [alpha |-> type_of initV] (Term`WHILE:('a -> bool) -> ('a -> 'a) -> 'a -> 'a`), [cond_f, f]); 1039 val prj_f = mk_pabs (st,ins); 1040 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 1041 1042 (* well_founded relation: WF (\st1 st0. ~eval_cond cond st0 /\ (st1 = run_ir ir st0)) *) 1043 1044 val (st0,st1) = (mk_var ("st0", Type `:DSTATE`), mk_var ("st1", Type `:DSTATE`)); 1045 val wf_t0 = mk_neg (list_mk_comb (Term`eval_il_cond`, [t_cond, st0])); 1046 val wf_t1 = mk_eq (st1, list_mk_comb (Term`run_ir`, [body_ir, st0])); 1047 val wf_t2 = list_mk_abs ([st1,st0],mk_conj(wf_t0,wf_t1)); 1048 val wf_t3 = mk_comb (Term`WF:(DSTATE->DSTATE->bool)->bool`, wf_t2); 1049 val wf_th = prove (wf_t3, (* set_goal ([],wf_t3) *) 1050 tr_WF_TAC body_spec (type_of initV) prj_f f cond_f_0 1051 ); 1052 1053 1054 val _ = show_types := true 1055 val (wf_th_name, wf_th_proof) = make_proof_string wf_t3 1056 ["tr_WF_TAC "^body_name^" (Type `"^ 1057 (type_to_string (type_of initV))^"`) (Term `"^ 1058 (term_to_string prj_f)^"`) (Term `"^ 1059 (term_to_string f)^"`) (Term `"^ 1060 (term_to_string cond_f_0)^"`)"] 1061 val _ = show_types := false; 1062 1063 1064 (* the characteristic function *) 1065 val f_spec = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of initV, gamma |-> type_of initV] (PSPEC_term), 1066 [tr_ir, mk_pair(pre_p, post_p), stk_f, list_mk_pair[prj_f,tr_f, prj_f]]); 1067 1068 val f_th = prove (f_spec, (* set_goal ([],f_spec) *) 1069 tr_PSPEC_TAC wf_th body_spec 1070 ) 1071 val (f_th_name, f_th_proof) = make_proof_string f_spec 1072 ["tr_PSPEC_TAC "^wf_th_name^" "^body_name] 1073 1074 (* Well-formedness *) 1075 1076 val well_formed_spec = mk_comb (Term`WELL_FORMED`, tr_ir); 1077 val well_formed_th = prove (well_formed_spec, (* set_goal ([],well_formed_spec) *) 1078 tr_WELL_FORMED_TAC wf_th body_spec 1079 ); 1080 val (well_formed_th_name, well_formed_th_proof) = make_proof_string well_formed_spec 1081 ["tr_WELL_FORMED_TAC "^wf_th_name^" "^body_name] 1082 1083 (* unchanged *) 1084 val unchanged_spec = mk_comb (rator (el 3 specL), tr_ir); 1085 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) 1086 tr_UNCHANGED_TAC well_formed_th body_spec 1087 1088 ); 1089 val (unchanged_th_name, unchanged_th_proof) = make_proof_string unchanged_spec 1090 ["tr_UNCHANGED_TAC "^well_formed_th_name^" "^body_name] 1091 1092 1093 val spec = subst [tr_ir |-> ir_abbr] (list_mk_conj [f_spec, well_formed_spec, unchanged_spec]); 1094 val spec' = mk_let (mk_abs (ir_abbr, spec), tr_ir); 1095 1096 val th = prove (spec', (* set_goal ([],spec') *) 1097 SIMP_TAC std_ss [f_th, well_formed_th, unchanged_th, LET_THM] 1098 ) 1099 1100 val (th_name, th_proof) = make_proof_string spec' 1101 ["SIMP_TAC std_ss [LET_THM,"^f_th_name^","^ 1102 well_formed_th_name^","^unchanged_th_name^"]"] 1103 1104 val proofs' = append_proofs[proofs, wf_th_proof, f_th_proof, well_formed_th_proof, unchanged_th_proof, th_proof] 1105 1106(* 1107 val tr_th_term = mk_comb(mk_comb (Term`run_ir`,tr_ir), Term `(r, m):DSTATE`); 1108 1109 val tr_th = 1110 (SIMP_CONV std_ss [IR_SEMANTICS_TR, GSYM WELL_FORMED_thm, 1111 well_formed_th] THENC 1112 SIM_MEM_CONV) tr_th_term;*) 1113 1114 in 1115 (th, th_name, proofs') 1116 end; 1117 1118 1119(*---------------------------------------------------------------------------------*) 1120(* Specification for Conditional Jumps *) 1121(*---------------------------------------------------------------------------------*) 1122 1123 1124fun cj_PSPEC_TAC thm1 thm2 (asm, g) = 1125 let 1126 val type_inst = type_of (body (#1 (dest_pair (rand g)))); 1127 val my_prj_cj_rule = (GEN_ALL (SIMP_RULE std_ss [LAMBDA_PROD] (INST_TYPE [beta |-> type_inst] 1128 (SPEC_ALL PRJ_CJ_RULE)))) 1129 in 1130 (MATCH_MP_TAC my_prj_cj_rule THEN 1131 SIMP_TAC std_ss [LET_ELIM_RULE thm1, LET_ELIM_RULE thm2] THEN 1132 SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, 1133 ILTheory.eval_il_cond_def, 1134 ILTheory.translate_condition_def, 1135 FORALL_DSTATE, mread_def, 1136 index_of_reg_def, toREG_def, 1137 toEXP_def, read_thm, GSYM PFORALL_THM] THEN 1138 WORDS_TAC THEN 1139 SIMP_TAC std_ss []) (asm, g) 1140 end 1141 1142fun cj_WELL_FORMED_TAC thm1 thm2 = ( 1143 REWRITE_TAC [GSYM IR_CJ_IS_WELL_FORMED] THEN 1144 SIMP_TAC std_ss [LET_ELIM_RULE thm1, LET_ELIM_RULE thm2]) 1145 1146 1147fun cj_UNCHANGED_TAC thm1 thm2 = ( 1148 MATCH_MP_TAC IR_CJ_UNCHANGED_STACK THEN 1149 SIMP_TAC std_ss [LET_ELIM_RULE thm1, LET_ELIM_RULE thm2]) 1150 1151(* 1152val (ir1_spec, ir1_name, ir2_spec, ir2_name, proofs) = (spec1, spec1_name, spec2, spec2_name, proofs2); 1153 1154*) 1155 1156fun mk_cj_spec cond ir1_spec ir1_name ir2_spec ir2_name unchanged_list proofs = 1157 let 1158 val (specL1,specL2) = (strip_conj (concl (LET_ELIM_RULE ir1_spec)),strip_conj (concl (LET_ELIM_RULE ir2_spec))); 1159 val (ir1,(pre_p1,post_p1),stk_f,(ins1,f1,outs1)) = get_spec_info (hd specL1); 1160 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (hd specL2); 1161(* val (spec1_thm, spec2_thm) = (SIMP_RULE std_ss [LET_THM] ir1_spec, SIMP_RULE std_ss [LET_THM] ir2_spec);*) 1162 1163 1164 val t_cond = convert_cond cond; 1165 val cj_ir = list_mk_comb (Term`CJ`, [t_cond, ir1, ir2]); 1166 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 1167 val st = mk_var ("st", Type `:DSTATE`); 1168 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [cj_ir, st]); 1169 1170 val initV = #1 (dest_pabs f1); 1171 val cj_cond = mk_cond_f t_cond ins1; 1172 val cj_f = mk_pabs(initV, list_mk_comb (inst [alpha |-> type_of outs1] (Term`COND:bool->'a->'a->'a`), 1173 [mk_comb(cj_cond,initV), mk_comb(f1,initV), mk_comb(f2,initV)])); 1174 1175 val (in_f,out_f) = (mk_pabs (st,ins1), mk_abs (st,outs2)); 1176 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 1177 1178 (* the characteristic function *) 1179 val f_spec = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of ins1, gamma |-> type_of outs2] (PSPEC_term), 1180 [cj_ir, mk_pair(pre_p1,post_p1), stk_f, list_mk_pair[in_f,cj_f,out_f]]); 1181 1182 1183 1184 val f_th = prove (f_spec, (* set_goal ([],f_spec) *) 1185 cj_PSPEC_TAC ir1_spec ir2_spec) 1186 val (f_th_name, f_th_proof) = make_proof_string f_spec 1187 ["cj_PSPEC_TAC "^ir1_name^" "^ir2_name] 1188 1189 (* well-formedness *) 1190 1191 val well_formed_spec = mk_comb (Term`WELL_FORMED`, cj_ir); 1192 val well_formed_th = prove (well_formed_spec, (* set_goal ([],well_formed_spec) *) 1193 cj_WELL_FORMED_TAC ir1_spec ir2_spec 1194 ); 1195 val (well_formed_th_name, well_formed_th_proof) = make_proof_string well_formed_spec 1196 ["cj_WELL_FORMED_TAC "^ir1_name^" "^ir2_name] 1197 1198 (* unchanged *) 1199 1200 val unchanged_spec = make_unchanged_stack_term (el 3 specL1) (el 3 specL2) cj_ir; 1201 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) 1202 cj_UNCHANGED_TAC ir1_spec ir2_spec 1203 ); 1204 val (unchanged_th_name, unchanged_th_proof) = make_proof_string unchanged_spec 1205 ["cj_UNCHANGED_TAC "^ir1_name^" "^ir2_name] 1206 1207 1208 val spec = list_mk_conj [f_spec, well_formed_spec, unchanged_spec]; 1209 1210 val th = prove (spec, (* set_goal ([],spec) *) 1211 SIMP_TAC std_ss [f_th, well_formed_th, unchanged_th, LET_THM] 1212 ) 1213 1214 val (th_name, th_proof) = make_proof_string spec 1215 ["SIMP_TAC std_ss ["^f_th_name^","^unchanged_th_name^","^well_formed_th_name^", LET_THM]"] 1216 1217 val proofs = append_proofs [proofs, f_th_proof, unchanged_th_proof, well_formed_th_proof, th_proof] 1218 1219(* 1220 val cj_th_term = mk_comb(mk_comb (Term`run_ir`,cj_ir), Term `(r, m):DSTATE`); 1221 val cj_th = 1222 (SIMP_CONV std_ss [IR_SEMANTICS_CJ, 1223 spec1_thm, spec2_thm, 1224 ir1_th, ir2_th] THENC 1225 SIM_MEM_CONV) cj_th_term;*) 1226 in 1227 (th, th_name, proofs) 1228 end; 1229 1230 1231(*---------------------------------------------------------------------------------*) 1232(* Application of the SHUFFLE rule *) 1233(*---------------------------------------------------------------------------------*) 1234 1235fun mk_shuffle_spec spec (in_f', g) = 1236 let 1237 val spec_thm = SIMP_RULE std_ss [LET_THM] spec; 1238 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd (strip_conj (concl spec_thm))); 1239 val st = mk_var ("st", Type `:DSTATE`); 1240 val (in_f,out_f) = (mk_pabs(st,ins), mk_pabs(st,outs)); 1241 1242 (* (g o in_f' = f o in_f) *) 1243 val (g_tp,f_tp) = (#2 (dest_type (type_of g)), #2 (dest_type (type_of f))); 1244 val g_com = list_mk_comb (inst [alpha |-> hd g_tp, beta |-> hd (tl g_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [g,in_f']); 1245 val f_com = list_mk_comb (inst [alpha |-> hd f_tp, beta |-> hd (tl f_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [f,in_f]); 1246 val shuffle_th = prove (mk_eq(g_com,f_com), (* set_goal ([],(mk_eq(g_com,f_com))) *) 1247 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_DSTATE, LET_THM, read_thm] THEN 1248 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN 1249 WORDS_TAC THEN 1250 SIMP_TAC std_ss [pair_induction] 1251 ); 1252 1253 val fspec = subst [f |-> g, in_f |-> in_f'] (concl spec_thm); 1254 1255 val spec = prove (fspec, (* set_goal ([],fspec) *) 1256 SIMP_TAC std_ss [spec_thm] THEN 1257 MATCH_MP_TAC PRJ_SHUFFLE_RULE2 THEN 1258 EXISTS_TAC in_f' THEN EXISTS_TAC g THEN 1259 RW_TAC std_ss [spec_thm, shuffle_th] 1260 ) 1261 in 1262 spec 1263 end; 1264 1265(*---------------------------------------------------------------------------------*) 1266(* Application of the PUSH rule *) 1267(*---------------------------------------------------------------------------------*) 1268 1269fun mk_push_spec spec = 1270 let 1271 val spec_thm = SIMP_RULE std_ss [LET_THM] spec; 1272 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd (strip_conj (concl spec_thm))); 1273 val st = mk_var ("st", Type `:DSTATE`); 1274 val (in_f,out_f) = (mk_pabs(st,ins), mk_pabs(st,outs)); 1275 val (g,in_f') = (f,in_f); 1276 1277 (* (g o in_f' = f o in_f) *) 1278 val (g_tp,f_tp) = (#2 (dest_type (type_of g)), #2 (dest_type (type_of f))); 1279 val g_com = list_mk_comb (inst [alpha |-> hd g_tp, beta |-> hd (tl g_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [g,in_f']); 1280 val f_com = list_mk_comb (inst [alpha |-> hd f_tp, beta |-> hd (tl f_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [f,in_f]); 1281 val push_th = prove (mk_eq(g_com,f_com), (* set_goal ([],(mk_eq(g_com,f_com))) *) 1282 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_DSTATE, LET_THM, read_thm] THEN 1283 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN 1284 WORDS_TAC THEN 1285 SIMP_TAC std_ss [pair_induction] 1286 ); 1287 1288 val fspec = subst [f |-> g, in_f |-> in_f'] (concl spec_thm); 1289 1290 val spec = prove (fspec, (* set_goal ([],fspec) *) 1291 SIMP_TAC std_ss [spec_thm] THEN 1292 MATCH_MP_TAC PRJ_PUSH_RULE THEN 1293 EXISTS_TAC in_f' THEN EXISTS_TAC g THEN 1294 RW_TAC std_ss [spec_thm, push_th] 1295 ) 1296 in 1297 spec 1298 end; 1299 1300(*---------------------------------------------------------------------------------*) 1301(* Application of the POP rule *) 1302(*---------------------------------------------------------------------------------*) 1303 1304fun mk_pop_spec spec = 1305 let 1306 val spec_thm = SIMP_RULE std_ss [LET_THM] spec; 1307 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd (strip_conj (concl spec_thm))); 1308 val st = mk_var ("st", Type `:DSTATE`); 1309 val (in_f,out_f) = (mk_pabs(st,ins), mk_pabs(st,outs)); 1310 val (g,in_f') = (f,in_f); 1311 1312 (* (g o in_f' = f o in_f) *) 1313 val (g_tp,f_tp) = (#2 (dest_type (type_of g)), #2 (dest_type (type_of f))); 1314 val g_com = list_mk_comb (inst [alpha |-> hd g_tp, beta |-> hd (tl g_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [g,in_f']); 1315 val f_com = list_mk_comb (inst [alpha |-> hd f_tp, beta |-> hd (tl f_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [f,in_f]); 1316 val pop_th = prove (mk_eq(g_com,f_com), (* set_goal ([],(mk_eq(g_com,f_com))) *) 1317 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_DSTATE, LET_THM, read_thm] THEN 1318 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN 1319 WORDS_TAC THEN 1320 SIMP_TAC std_ss [pair_induction] 1321 ); 1322 1323 val fspec = subst [f |-> g, in_f |-> in_f'] (concl spec_thm); 1324 1325 val spec = prove (fspec, (* set_goal ([],fspec) *) 1326 SIMP_TAC std_ss [spec_thm] THEN 1327 MATCH_MP_TAC PRJ_POP_RULE THEN 1328 EXISTS_TAC in_f' THEN EXISTS_TAC g THEN 1329 RW_TAC std_ss [spec_thm, pop_th] 1330 ) 1331 in 1332 spec 1333 end; 1334 1335 1336(*---------------------------------------------------------------------------------*) 1337(* Forward Reasoning *) 1338(*---------------------------------------------------------------------------------*) 1339 1340(* 1341fun extract (annotatedIR.SC (ir1, ir2, info)) = (ir1, ir2, info); 1342val (ir1, ir2, info) = extract f_ir; 1343val (ir1, ir2, info) = extract ir2; 1344 1345fun extract (annotatedIR.CALL (fname, pre_ir, body_ir, post_ir,info)) = (fname, pre_ir, body_ir, post_ir, info); 1346val (fname, pre_ir, body_ir, post_ir, info) = extract ir1 1347 1348fun extract (annotatedIR.SC (ir1, ir2, info)) = (ir1, ir2, info); 1349val (ir1, ir2, info) = extract ir1 1350 1351 1352fun extract (annotatedIR.TR (cond, body, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) = (cond, body) 1353val (cond, body) = extract ir1 1354 1355fun extract (annotatedIR.CJ (cond, ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) = (cond, ir1, ir2) 1356val (cond, ir1, ir2) = extract ir1 1357 1358fwd_reason f_ir unchanged_list [] 1359 1360val proof = #3 it 1361 1362printInstL proof 1363 val proofs = []; 1364used_thm_num := 1 1365*) 1366 1367 1368fun fwd_reason (annotatedIR.BLK blk_ir) unchanged_list proofs = 1369 let 1370 val (spec, spec_thm_name, th, th_name, proofs_blk) = 1371 (mk_blk_spec (annotatedIR.BLK blk_ir) unchanged_list) 1372 in 1373 (spec, spec_thm_name, append_proofs [proofs, proofs_blk]) 1374 end 1375 1376 | fwd_reason (annotatedIR.SC (ir1, ir2, info)) unchanged_list proofs = 1377 let 1378 val (spec1, spec1_name, proofs1) = fwd_reason ir1 unchanged_list proofs; 1379 val (spec2, spec2_name, proofs2) = fwd_reason ir2 unchanged_list proofs1; 1380 in 1381 mk_sc_spec spec1 spec1_name spec2 spec2_name proofs2 1382 end 1383 1384 | fwd_reason (annotatedIR.TR (cond, body, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) unchanged_list proofs = 1385 let val (body_spec, body_name, proofs') = fwd_reason body unchanged_list proofs 1386 in 1387 mk_tr_spec cond body_spec body_name proofs' 1388 end 1389 | fwd_reason (annotatedIR.CJ (cond, ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) unchanged_list proofs = 1390 let 1391 val (spec1, spec1_name, proofs1) = fwd_reason ir1 unchanged_list proofs; 1392 val (spec2, spec2_name, proofs2) = fwd_reason ir2 unchanged_list proofs1; 1393 in 1394 mk_cj_spec cond spec1 spec1_name spec2 spec2_name unchanged_list proofs2 1395 end 1396 | fwd_reason (annotatedIR.CALL (fname, pre_ir, body_ir, post_ir,info)) unchanged_list proofs = 1397 let 1398 val emptyset = Binaryset.empty Int.compare; 1399 val f_unchanged_list = mk_unchanged_set fname; 1400 val (body_spec, body_spec_name, proofs') = fwd_reason body_ir f_unchanged_list proofs; 1401 val (pre_spec, pre_spec_name, pre_th, pre_th_name, pre_proofs) = mk_blk_spec pre_ir emptyset; 1402 val (post_spec, post_spec_name, post_th, post_th_name, post_proofs) = mk_blk_spec post_ir emptyset; 1403 1404 val proofs'' = append_proofs [proofs', pre_proofs, post_proofs]; 1405 in 1406 mk_fc_spec (pre_spec, pre_spec_name, body_spec, body_spec_name, post_spec, post_spec_name, pre_th, pre_th_name, post_th, post_th_name, proofs'', unchanged_list) 1407 end 1408 | fwd_reason _ _ _ = 1409 raise Fail "fwd_reason: unsupported IR strcuture" 1410 ; 1411 1412(*---------------------------------------------------------------------------------*) 1413(* Equivalence between the original function and the spec function *) 1414(*---------------------------------------------------------------------------------*) 1415fun restore_f_TAC defs = 1416 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_PROD] THEN 1417 REPEAT GEN_TAC THEN 1418 1419 SIMP_TAC std_ss defs THEN 1420 REPEAT (CHANGED_TAC (FIRST [CHANGED_TAC (SIMP_TAC std_ss ([LET_THM, WORD_ADD_ASSOC] @ defs)), WORDS_TAC])) THEN 1421 REPEAT (CHANGED_TAC (FIRST [CHANGED_TAC (SIMP_TAC std_ss ([LET_THM, GSYM WORD_ADD_ASSOC] @ defs)), WORDS_TAC])) THEN 1422 METIS_TAC[WORD_ADD_COMM, WORD_AND_COMM, WORD_OR_COMM, WORD_XOR_COMM]; 1423 1424 1425 1426fun restore_f spec def prove_equiv = 1427 let 1428 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 1429 val [in_f,spec_f,out_f] = strip_pair (List.nth (#2 (strip_comb (concl th0)),3)); 1430 val sfl_f_const = #1 (strip_comb (lhs ((concl o SPEC_ALL) def))); 1431 val eq_stat = mk_eq (spec_f, sfl_f_const); 1432 val eq_th = if (prove_equiv) then 1433 (print "Proving equivalence with input function\n"; 1434 prove(eq_stat, restore_f_TAC [def]) handle _ => 1435 let 1436 val _ = print "! Equivalence proof between original function and\n"; 1437 val _ = print "! derived program semantics failed!\n\n"; 1438 in 1439 ASSUME eq_stat 1440 end) 1441 else ASSUME eq_stat; 1442 in 1443 eq_th 1444 end; 1445 1446fun restore_f_proof f_spec0 thm_name thm_proofs prove_equiv def def_option = 1447 let 1448 val f_th = restore_f f_spec0 def prove_equiv; 1449 val f_th_spec = concl f_th; 1450 val def_given = isSome def_option; 1451 val (f_th_name, proofs) = 1452 if (def_given andalso prove_equiv) then 1453 let 1454 val (def_name, def_proofs) = 1455 valOf def_option 1456 val (spec_name, p) = make_proof_string f_th_spec ["restore_f_TAC ["^def_name^"]"]; 1457 in 1458 (spec_name, append_proofs [thm_proofs, def_proofs,p]) 1459 end 1460 else 1461 let 1462 val (spec_name, p) = 1463 make_assume_string f_th_spec; 1464 in 1465 (spec_name, append_proofs [thm_proofs, p]) 1466 end 1467 val thm = SIMP_RULE std_ss [f_th] f_spec0 1468 val (thm_name, thm_proof) = make_proof_string 1469 (concl thm) ["ASSUME_TAC (SIMP_RULE std_ss ["^ f_th_name^"] "^thm_name^") THEN", "ASM_SIMP_TAC std_ss []"]; 1470 val proofs' = append_proofs [proofs, thm_proof]; 1471 in 1472 (thm, thm_name, proofs') 1473 end 1474 1475(*---------------------------------------------------------------------------------*) 1476(* Display the theorem at the level of ARM flat code *) 1477(*---------------------------------------------------------------------------------*) 1478 1479fun f_correct spec = 1480 let 1481 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 1482 val th1 = SIMP_RULE std_ss [PSPEC_def, HSPEC_def, run_ir_def] th0; 1483 val f = let val t0 = concl (SPEC_ALL th1) 1484 val (assm,f_spec) = 1485 let val (assm, t1) = dest_imp t0 1486 in (assm,#2 (dest_conj t1)) 1487 end handle e => (Term`T`,t0) 1488 in 1489 mk_imp (assm, f_spec) 1490 end 1491 val th2 = GEN_ALL (prove (f, SIMP_TAC std_ss [th1])); 1492 val th3 = SIMP_RULE std_ss [translate_def, translate_assignment_def, toEXP_def, toREG_def, toMEM_def, index_of_reg_def, translate_condition_def] th2; 1493 val th4 = SIMP_RULE list_ss [ARMCompositionTheory.mk_SC_def, ARMCompositionTheory.mk_CJ_def, ARMCompositionTheory.mk_TR_def] th3 1494 val th5 = SIMP_RULE std_ss [GSYM proper_def] th4 1495 val th6 = WORDS_RULE th5 1496 in 1497 th6 1498 end; 1499 1500 1501fun f_correct_ir spec = 1502 let 1503 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 1504 val th1 = SIMP_RULE std_ss [PSPEC_def, HSPEC_def] th0; 1505 val f = let val t0 = concl (SPEC_ALL th1) 1506 val (assm,f_spec) = 1507 let val (assm, t1) = dest_imp t0 1508 in (assm,#2 (dest_conj t1)) 1509 end handle e => (Term`T`,t0) 1510 in 1511 mk_imp (assm, f_spec) 1512 end 1513 val th2 = GEN_ALL (prove (f, SIMP_TAC std_ss [th1])); 1514 val th3 = SIMP_RULE std_ss [toEXP_def, toREG_def, toMEM_def, index_of_reg_def] th2; 1515 val th4 = SIMP_RULE list_ss [] th3 1516 val th5 = SIMP_RULE std_ss [GSYM proper_def] th4 1517 val th6 = WORDS_RULE th5 1518 in 1519 th6 1520 end; 1521 1522 1523(*---------------------------------------------------------------------------------*) 1524(* Print out *) 1525(*---------------------------------------------------------------------------------*) 1526 1527(* Extract the IR tree from the specification and print it out *) 1528 1529fun extract_ir spec = 1530 let 1531 val (f_name, _, (f_args,f_ir,f_outs), _, _, _) = spec; 1532 in 1533 (print (" Name : " ^ f_name ^ "\n"); 1534 print (" Arguments : " ^ (IRSyntax.format_exp f_args) ^ "\n"); 1535 print (" Returns : " ^ (IRSyntax.format_exp f_outs) ^ "\n"); 1536 print " Body: \n"; 1537 annotatedIR.printIR (annotatedIR.merge_ir f_ir) 1538 ) 1539 end 1540 1541(* Extract the ARM instruction list from the specification and print it out *) 1542 1543fun extract_arm spec = 1544 let 1545 val (f_name, _, (f_args,_,f_outs), _, stat0, _, _, _, _) = spec; 1546 val stat1 = let val t0 = concl (SPEC_ALL stat0) 1547 in if is_imp t0 then #2 (dest_imp t0) else t0 1548 end 1549 val stms = find_term (fn t => type_of t = Type `:INST list`) stat1; 1550 val stms1 = preARMSyntax.dest_arm stms 1551 in 1552 (print (" Name : " ^ f_name ^ "\n"); 1553 print (" Arguments : " ^ (IRSyntax.format_exp f_args) ^ "\n"); 1554 print (" Returns : " ^ (IRSyntax.format_exp f_outs) ^ "\n"); 1555 print " Body: \n"; 1556 Assem.printInsts stms1 1557 ) 1558 end 1559 1560(*---------------------------------------------------------------------------------*) 1561(* Interface *) 1562(*---------------------------------------------------------------------------------*) 1563 1564(* To make the initial value of fp or sp unspecified, assign it a negative integer *) 1565(* For example, init_fp = ~1 will lead to st<MR R11> = ARB *) 1566 1567(*val init_fp = ref (100);*) 1568val init_sp = ref (~1); 1569 1570fun mk_pre_p sp_v = 1571 if (!init_sp < 0) then mk_pabs (mk_var ("st", Type `:DSTATE`), Term`T`) 1572 else 1573 let val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`)); 1574 val (fp',sp') = (read_one_var st (IRSyntax.REG 11), read_one_var st (IRSyntax.REG 13)); 1575 fun convert_pt v = if v < 0 then inst [alpha |-> Type `:DATA`] (Term `ARB`) else mk_comb (Term `n2w:num->word32`, term_of_int v) 1576 in mk_pabs (st, mk_conj ( mk_eq(fp', convert_pt (!init_sp)), mk_eq(sp', convert_pt (!init_sp)))) (* Initially fp = sp *) 1577 end; 1578 1579(*---------------------------------------------------------------------------------*) 1580(*Preprocess definition to eliminate ugly constants *) 1581(*---------------------------------------------------------------------------------*) 1582 1583fun wordsplit t = 1584 let 1585 fun term2Arbnum t = 1586 let 1587 val t = mk_comb (Term `w2n:word32->num`, t) 1588 val t = rhs (concl (EVAL t)); 1589 val n = numLib.dest_numeral t; 1590 in 1591 n 1592 end; 1593 1594 fun arbnum2term n = 1595 let 1596 val t = numLib.mk_numeral n; 1597 val t = mk_comb (Term `n2w:num->word32`, t) 1598 val t = rhs (concl (EVAL t)); 1599 in 1600 t 1601 end; 1602 1603 1604 fun remove_zero n c = 1605 let 1606 val (n1, n2) = (Arbnum.divmod (n, Arbnum.fromInt 4)) 1607 in 1608 if (n2 = Arbnum.zero) then 1609 remove_zero n1 (Arbnum.plus1 c) 1610 else 1611 (n, c) 1612 end; 1613 1614 1615 fun wordsplit_internal (n:num) l = 1616 if (n = Arbnum.zero) then 1617 if (l = []) then [n] else l 1618 else 1619 let 1620 val (n_div, n_mod) = remove_zero n Arbnum.zero; 1621 val n' = Arbnum.mod (n_div, Arbnum.fromInt 256); 1622 val n' = Arbnum.* (n', Arbnum.pow (Arbnum.fromInt 4, n_mod)); 1623 val m = Arbnum.- (n, n'); 1624 in 1625 wordsplit_internal m (n'::l) 1626 end; 1627 1628 val l = wordsplit_internal (term2Arbnum t) []; 1629 val l = map arbnum2term l; 1630 in 1631 l 1632 end; 1633 1634fun needs_split t = not (length(wordsplit t) = 1) 1635 1636fun WORD_EVAL_CONV t = 1637 if ((wordsSyntax.is_word_type(type_of t)) andalso (free_vars t = [])) then 1638 (CHANGED_CONV EVAL t) else raise ERR "WORD_EVAL_CONV" "" 1639 1640 1641fun DATA_RESTRICT_CONV t = 1642 if (wordsSyntax.is_n2w t andalso needs_split t) then 1643 let 1644 val l = wordsplit t; 1645 val (h, l) = (hd l, tl l); 1646 val new_t = foldl (fn (x, y) => mk_comb (mk_comb (Term `($!!):word32->word32->word32`, x), y)) h l; 1647 in 1648 GSYM (WORDS_CONV new_t) 1649 end 1650 else raise ERR "DATA_RESTRICT_CONV" "" 1651 1652 1653 1654val extra_defs = ref [DECIDE (Term `T`)]; 1655 1656fun preprocess_def prog = 1657 CONV_RULE ((DEPTH_CONV WORD_EVAL_CONV) THENC (DEPTH_CONV DATA_RESTRICT_CONV)) prog 1658 1659fun preprocess_def_proof def prog_name = 1660 if (isSome prog_name) then 1661 SOME ( 1662 make_proof_string (concl def) 1663 ["PROVE_TAC[preprocess_def "^(valOf prog_name)^"]"]) 1664 else NONE 1665 1666 1667fun pp_prepare_compile prog = 1668 let 1669 val def = preprocess_def prog; 1670 val _ = funCall.link_ir def; 1671 in 1672 () 1673 end; 1674 1675(*val prog = fact_def; 1676 val prog = ex1_field_mult_aux_alt 1677 val prog = def1 1678 val def = 1679 val prog_name = SOME "def1" 1680 val prove_equiv = false 1681*) 1682fun pp_compile_proof_opt prog prog_name prove_equiv = 1683 let 1684 val def = preprocess_def prog; 1685 val (f_name, f_type, (f_args,f_ir,f_outs), defs) = funCall.link_ir def; 1686 val unchanged_list = mk_unchanged_set f_name; 1687 val (f_spec0, thm_name, thm_proof) = fwd_reason f_ir unchanged_list []; 1688 val def_option = preprocess_def_proof def prog_name; 1689 val (f_spec1, thm_name, thm_proof) = 1690 restore_f_proof f_spec0 thm_name thm_proof prove_equiv def def_option 1691 val thm_list = CONJ_LIST 3 (SIMP_RULE std_ss [LET_THM] f_spec1); 1692 val stat = f_correct f_spec1 1693 val stat_ir = f_correct_ir f_spec1 1694 in 1695 (f_name, f_type, (f_args,f_ir,f_outs), defs, stat, stat_ir, el 1 thm_list, el 2 thm_list, el 3 thm_list, thm_name, thm_proof) 1696 end 1697 1698fun pp_compile_proof prog prog_name prove_equiv = 1699 pp_compile_proof_opt prog (SOME prog_name) prove_equiv; 1700 1701fun pp_compile prog prove_equiv = 1702 pp_compile_proof_opt prog NONE prove_equiv; 1703 1704type spec_type = 1705 string * hol_type * (exp * anntIR * exp) * thm list * thm * thm * thm * thm * 1706 thm * string * string list; 1707 1708 1709fun get_spec_assums ((_, _, _, thmL, thm1, thm2, thm3, thm4, thm5, _, _):spec_type) = 1710 let 1711 val thmL' = thm2::thm3::thm4::thm5::thmL; 1712 val s1 = hypset thm1; 1713 val s = foldl (fn (thm, set) => HOLset.union (set, hypset thm)) s1 thmL'; 1714 val l = HOLset.listItems s 1715 val t = list_mk_conj l 1716 in 1717 (t, l) 1718 end 1719 1720fun set_goal___spec_assums spec = 1721 goalstackLib.set_goal ([], #1 (get_spec_assums spec)) 1722 1723fun prove___spec_assums (spec as (x1, x2, x3, thmL, thm1, thm2, thm3, thm4, thm5, thm_name, thm_proof)) tac = 1724let 1725 val (t, l) = (get_spec_assums spec); 1726 val thm = prove (t, tac); 1727 1728 fun prove_hyp hyp_thm = 1729 let 1730 val hyps = hyp hyp_thm; 1731 fun elim_hyp_list hyp_thm [] = hyp_thm | 1732 elim_hyp_list hyp_thm (t::l) = 1733 let 1734 val t_thm = prove (t, REWRITE_TAC [thm]) 1735 val hyp_thm' = PROVE_HYP t_thm hyp_thm 1736 in 1737 elim_hyp_list hyp_thm' l 1738 end 1739 in 1740 elim_hyp_list hyp_thm hyps 1741 end 1742 1743 val thmL' = map prove_hyp thmL; 1744 val thm1' = prove_hyp thm1; 1745 val thm2' = prove_hyp thm2; 1746 val thm3' = prove_hyp thm3; 1747 val thm4' = prove_hyp thm4; 1748 val thm5' = prove_hyp thm5; 1749in 1750 (x1, x2, x3, thmL', thm1', thm2', thm3', thm4', thm5', thm_name, thm_proof) 1751end 1752 1753end 1754end 1755