1structure blastLib :> blastLib = 2struct 3 4open HolKernel boolLib bossLib; 5open bitTheory wordsTheory bitstringTheory blastTheory; 6open listLib wordsLib bitSyntax bitstringSyntax; 7 8structure Parse = struct 9 open Parse 10 val (Type,Term) = 11 parse_from_grammars 12 (apsnd ParseExtras.grammar_loose_equality blast_grammars) 13end 14 15open Parse 16 17(* ------------------------------------------------------------------------ *) 18 19val ERR = Feedback.mk_HOL_ERR "blastLib" 20 21val blast_trace = ref 0 22val blast_counter = ref true 23val blast_multiply_limit = ref 8 24 25val _ = Feedback.register_trace ("bit blast", blast_trace, 3) 26val _ = Feedback.register_btrace ("print blast counterexamples", blast_counter) 27val _ = Feedback.register_trace 28 ("blast multiply limit", blast_multiply_limit, 32) 29 30val rhsc = boolSyntax.rhs o Thm.concl 31 32val dim_of_word = fcpLib.index_to_num o wordsSyntax.dim_of 33 34(* ------------------------------------------------------------------------ 35 mk_index_thms : Generate rewrites of the form ``($FCP f) ' i = f i``. 36 INDEX_CONV : Evaluation for terms of the form ``($FCP f) ' i``. 37 ------------------------------------------------------------------------ *) 38 39fun mk_leq_thm (i,j) = 40 numSyntax.mk_leq (i, j) 41 |> (DEPTH_CONV wordsLib.SIZES_CONV THENC numLib.REDUCE_CONV) 42 |> Drule.EQT_ELIM 43 44fun mk_less_thm (i,j) = 45 numSyntax.mk_less (i, j) 46 |> (Conv.RAND_CONV (TRY_CONV wordsLib.SIZES_CONV) THENC numLib.REDUCE_CONV) 47 |> Drule.EQT_ELIM 48 49fun mk_size_thm (i,ty) = mk_less_thm (i, wordsSyntax.mk_dimindex ty) 50 51local 52 val e_tys = ref (Redblackset.empty Type.compare) 53 val cmp = reduceLib.num_compset () 54 val () = computeLib.add_thms [combinTheory.o_THM, combinTheory.K_THM] cmp 55 val cnv = computeLib.CBV_CONV cmp 56 57 val fcp_beta_thm = fcpTheory.FCP_BETA 58 |> Thm.INST_TYPE [Type.alpha |-> Type.bool] 59 60 fun mk_index_thms ty = 61 case Lib.total fcpSyntax.dest_int_numeric_type ty of 62 SOME n => 63 let 64 val indx_thm = Thm.INST_TYPE [Type.beta |-> ty] fcp_beta_thm 65 in 66 List.tabulate 67 (n, fn i => 68 let 69 val j = numSyntax.term_of_int i 70 in 71 Thm.MP (Thm.SPEC j indx_thm) (mk_size_thm (j, ty)) 72 end) 73 end 74 | NONE => [] 75 76 fun is_new tm = 77 case Lib.total wordsSyntax.dim_of tm of 78 SOME ty => not (Redblackset.member (!e_tys, ty)) andalso 79 (e_tys := Redblackset.add (!e_tys, ty); true) 80 | NONE => false 81 82 val new_index_thms = 83 List.concat o List.map (mk_index_thms o wordsSyntax.dim_of) o 84 HolKernel.find_terms is_new 85 86 fun add_index_thms tm = computeLib.add_thms (new_index_thms tm) cmp 87in 88 fun ADD_INDEX_CONV tm = (add_index_thms tm; cnv tm) 89 90 fun INDEX_CONV tm = Conv.CHANGED_CONV cnv tm 91 handle HOL_ERR _ => raise Conv.UNCHANGED 92end 93 94(* -------------------------------------------------------------------- 95 mk_testbit_thms : find terms of the form ``FCP i. testbit i [..]`` and 96 ``testbit n [..]``, then generate rewrites for extracting 97 bits from the bitstring 98 -------------------------------------------------------------------- *) 99 100local 101 val nd = Drule.CONJUNCTS numeralTheory.numeral_distrib 102 val cmp = computeLib.new_compset 103 [Thm.CONJUNCT1 listTheory.EL, listTheory.EL_simp_restricted, 104 listTheory.HD, numeralTheory.numeral_pre, 105 arithmeticTheory.NORM_0, List.nth (nd, 15), List.nth (nd, 16)] 106 val EL_CONV = computeLib.CBV_CONV cmp 107 108 fun gen_testbit_thms (n, m) = 109 let 110 val vs = List.tabulate 111 (n, fn i => Term.mk_var ("v" ^ Int.toString i, Type.bool)) 112 val vs = listSyntax.mk_list (vs, Type.bool) 113 val lvs = listSyntax.mk_length vs 114 val l = listLib.LENGTH_CONV lvs 115 val el_thms = 116 List.tabulate (n, 117 fn i => EL_CONV (listSyntax.mk_el (numSyntax.term_of_int i, vs))) 118 in 119 List.tabulate (m, 120 fn i => 121 let 122 val ti = numSyntax.term_of_int i 123 in 124 if i < n then 125 let 126 val thm = numSyntax.mk_less (ti, lvs) 127 |> (Conv.RAND_CONV (Conv.REWR_CONV l) 128 THENC numLib.REDUCE_CONV) 129 |> Drule.EQT_ELIM 130 val thm = Drule.MATCH_MP bitstringTheory.testbit_el thm 131 in 132 Conv.RIGHT_CONV_RULE 133 (PURE_REWRITE_CONV [l] 134 THENC Conv.RATOR_CONV 135 (Conv.RAND_CONV numLib.REDUCE_CONV) 136 THENC PURE_REWRITE_CONV el_thms) thm 137 end 138 else 139 let 140 val thm = numSyntax.mk_leq (lvs, ti) 141 |> (Conv.LAND_CONV (Conv.REWR_CONV l) 142 THENC numLib.REDUCE_CONV) 143 |> Drule.EQT_ELIM 144 in 145 Drule.MATCH_MP bitstringTheory.testbit_geq_len thm 146 end 147 end) 148 end 149 150 fun testbit_dest tm = 151 let 152 val (i, v) = bitstringSyntax.dest_testbit tm 153 in 154 (List.length (fst (listSyntax.dest_list v)), 155 numSyntax.int_of_term i + 1) 156 end 157 handle HOL_ERR _ => 158 let 159 val (j, t) = 160 HolKernel.dest_binder fcpSyntax.fcp_tm (ERR "dest_FCP" "") tm 161 val (i, v) = bitstringSyntax.dest_testbit t 162 in 163 (List.length (fst (listSyntax.dest_list v)), 164 Arbnum.toInt (wordsSyntax.size_of tm)) 165 end 166in 167 fun mk_testbit_thms tm = 168 tm |> HolKernel.find_terms (Lib.can testbit_dest) 169 |> List.map testbit_dest 170 |> Listsort.sort (Lib.pair_compare (Int.compare, Int.compare)) 171 |> Lib.op_mk_set (fn a => fn b => fst a = fst b) 172 |> List.map gen_testbit_thms 173 |> List.concat 174end 175 176(* ------------------------------------------------------------------------ 177 EVAL_CONV : General purpose evaluation 178 ------------------------------------------------------------------------ *) 179 180val EVAL_CONV = 181 computeLib.compset_conv (reduceLib.num_compset()) 182 [computeLib.Defs 183 [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT, 184 REWRITE_RULE [GSYM arithmeticTheory.DIV2_def] BIT_SET_def, 185 listTheory.EVERY_DEF, listTheory.FOLDL, 186 numLib.SUC_RULE rich_listTheory.COUNT_LIST_AUX_def, 187 GSYM rich_listTheory.COUNT_LIST_GENLIST, 188 rich_listTheory.COUNT_LIST_compute, 189 numeral_bitTheory.numeral_log2, numeral_bitTheory.numeral_ilog2, 190 numeral_bitTheory.LOG_compute, GSYM DISJ_ASSOC], 191 computeLib.Convs 192 [(``fcp$dimindex:'a itself -> num``, 1, wordsLib.SIZES_CONV), 193 (``words$word_mod:'a word -> 'a word -> 'a word``, 2, 194 wordsLib.WORD_MOD_BITS_CONV)]] 195 196(* ------------------------------------------------------------------------ *) 197 198fun INST_b3 t thm = 199 Thm.GENL [``x:num->bool``, ``y:num->bool``, ``c:bool``, ``i:num``, 200 ``n:num``, ``b1:bool``, ``b2:bool``] o 201 PURE_REWRITE_RULE [thm] o Thm.INST [``b3:bool`` |-> t] o Drule.SPEC_ALL 202 203val BCARRY_mp = prove( 204 ���!x y c i n b1 b2 b3. 205 (i = SUC n) /\ (x n = b1) /\ (y n = b2) /\ (BCARRY n x y c = b3) ==> 206 (BCARRY i x y c = bcarry b1 b2 b3)���, 207 SRW_TAC [] [BCARRY_def]) 208 209val BCARRY_mp = REWRITE_RULE [bcarry_def] BCARRY_mp 210 211val BCARRY_mp_carry = 212 INST_b3 boolSyntax.T (DECIDE ``x /\ y \/ (x \/ y) /\ T = x \/ y``) BCARRY_mp 213 214val BCARRY_mp_not_carry = 215 INST_b3 boolSyntax.F (DECIDE ``x /\ y \/ (x \/ y) /\ F = x /\ y``) BCARRY_mp 216 217fun INST_b3 t thm = 218 Thm.GENL [``x:num->bool``,``y:num->bool``, ``c:bool``, ``i:num``, 219 ``b1:bool``, ``b2:bool``] o 220 PURE_REWRITE_RULE [thm] o Thm.INST [``b3:bool`` |-> t] o Drule.SPEC_ALL 221 222val BSUM_mp = prove( 223 ���!x y c i b1 b2 b3. 224 (x i = b1) /\ (y i = b2) /\ (BCARRY i x y c = b3) ==> 225 (BSUM i x y c = bsum b1 b2 b3)���, 226 SRW_TAC [] [BSUM_def]) 227 228val BSUM_mp = REWRITE_RULE [bsum_def] BSUM_mp 229 230val BSUM_mp_carry = 231 INST_b3 boolSyntax.T (DECIDE ``((x = ~y) = ~T) = (x:bool = y)``) BSUM_mp 232 233val BSUM_mp_not_carry = 234 INST_b3 boolSyntax.F (DECIDE ``((x = ~y) = ~F) = (x:bool = ~y)``) BSUM_mp 235 236val rhs_rewrite = 237 Conv.RIGHT_CONV_RULE 238 (Rewrite.REWRITE_CONV 239 [satTheory.AND_INV, Drule.EQF_INTRO boolTheory.NOT_AND, 240 DECIDE ``!b:bool. (b = ~b) = F``, 241 DECIDE ``!b:bool. (~b = b) = F``]) 242 243(* -------------------------------------------------------------------- 244 mk_summation : returns theorems of the form ``BSUM i x y c = exp`` 245 for all 0 < i < max, where "exp" is a propositional 246 expression. 247 -------------------------------------------------------------------- *) 248 249fun SP l (thm1, thm2) = (Drule.SPECL (tl l) thm1, Drule.SPECL l thm2) 250 251fun mk_summation rwts (max, x, y, c) = 252 let 253 val conv = INDEX_CONV THENC PURE_REWRITE_CONV rwts 254 val SPEC_SUM = Drule.SPECL [x, y, c] 255 val iBSUM_mp_carry = SPEC_SUM BSUM_mp_carry 256 val iBSUM_mp_not_carry = SPEC_SUM BSUM_mp_not_carry 257 val iBSUM_mp = SPEC_SUM BSUM_mp 258 val iBCARRY_mp_carry = SPEC_SUM BCARRY_mp_carry 259 val iBCARRY_mp_not_carry = SPEC_SUM BCARRY_mp_not_carry 260 val iBCARRY_mp = SPEC_SUM BCARRY_mp 261 fun mk_sums p (s, c_thm) = 262 if p = max 263 then s 264 else let 265 val pp = Arbnum.plus1 p 266 in 267 mk_sums pp 268 (let 269 val n = numLib.mk_numeral p 270 val i = numLib.mk_numeral pp 271 val () = 272 if !blast_trace > 2 273 then print ("Expanding bit... " ^ 274 Arbnum.toString pp ^ "\n") 275 else () 276 val i_thm = boolSyntax.mk_eq (i, numSyntax.mk_suc n) 277 |> numLib.REDUCE_CONV |> Drule.EQT_ELIM 278 val x_thm = Conv.QCONV conv (Term.mk_comb (x, n)) 279 val y_thm = Conv.QCONV conv (Term.mk_comb (y, n)) 280 val x_concl = rhsc x_thm 281 val y_concl = rhsc y_thm 282 val c_concl = rhsc c_thm 283 val (thm1,thm2) = 284 if Teq c_concl 285 then SP [i, n, x_concl, y_concl] 286 (iBSUM_mp_carry, iBCARRY_mp_carry) 287 else if Feq c_concl 288 then SP [i, n, x_concl, y_concl] 289 (iBSUM_mp_not_carry, iBCARRY_mp_not_carry) 290 else SP [i, n, x_concl, y_concl, c_concl] 291 (iBSUM_mp, iBCARRY_mp) 292 in 293 (rhs_rewrite 294 (Thm.MP thm1 295 (Drule.LIST_CONJ [x_thm, y_thm, c_thm])) :: s, 296 rhs_rewrite 297 (Thm.MP thm2 298 (Drule.LIST_CONJ [i_thm, x_thm, y_thm, c_thm]))) 299 end) 300 end 301 in 302 mk_sums Arbnum.zero 303 ([], BCARRY_def |> Thm.CONJUNCT1 |> Drule.SPECL [x,y,c]) 304 end 305 306(* -------------------------------------------------------------------- 307 mk_carry : returns theorem of the form ``BCARRY max x y c = exp``, 308 where "exp" is a propositional expression. 309 -------------------------------------------------------------------- *) 310 311fun mk_carry rwts (max, x, y, c) = 312 let 313 val conv = INDEX_CONV THENC PURE_REWRITE_CONV rwts 314 315 val SPEC_CARRY = Drule.SPECL [x, y, c] 316 317 val iBCARRY_mp_carry = SPEC_CARRY BCARRY_mp_carry 318 val iBCARRY_mp_not_carry = SPEC_CARRY BCARRY_mp_not_carry 319 val iBCARRY_mp = SPEC_CARRY BCARRY_mp 320 321 fun mk_c p c_thm = 322 if p = max 323 then c_thm 324 else let 325 val pp = Arbnum.plus1 p 326 in 327 mk_c pp 328 (let 329 val n = numLib.mk_numeral p 330 val i = numLib.mk_numeral pp 331 val () = 332 if !blast_trace > 2 333 then print ("Expanding bit... " ^ 334 Arbnum.toString pp ^ "\n") 335 else () 336 val i_thm = boolSyntax.mk_eq (i, numSyntax.mk_suc n) 337 |> numLib.REDUCE_CONV |> Drule.EQT_ELIM 338 val x_thm = Conv.QCONV conv (Term.mk_comb (x, n)) 339 val y_thm = Conv.QCONV conv (Term.mk_comb (y, n)) 340 val x_concl = rhsc x_thm 341 val y_concl = rhsc y_thm 342 val c_concl = rhsc c_thm 343 val thm = 344 if Teq c_concl 345 then Drule.SPECL [i, n, x_concl, y_concl] 346 iBCARRY_mp_carry 347 else if Feq c_concl 348 then Drule.SPECL [i, n, x_concl, y_concl] 349 iBCARRY_mp_not_carry 350 else Drule.SPECL [i, n, x_concl, y_concl, c_concl] 351 iBCARRY_mp 352 in 353 rhs_rewrite 354 (Thm.MP thm 355 (Drule.LIST_CONJ [i_thm, x_thm, y_thm, c_thm])) 356 end) 357 end 358 in 359 mk_c Arbnum.zero (BCARRY_def |> Thm.CONJUNCT1 |> Drule.SPECL [x,y,c]) 360 end 361 362(* -------------------------------------------------------------------- 363 mk_sums : find terms of the form ``FCP i. BSUM i x y c`` and 364 ``BCARRY n x y c``; it then uses mk_summation and mk_carry 365 to generate appropriate rewrites 366 -------------------------------------------------------------------- *) 367 368local 369 fun dest_sum tm = 370 case boolSyntax.dest_strip_comb tm of 371 ("fcp$FCP", [f]) => 372 (case f |> Term.dest_abs |> snd |> boolSyntax.dest_strip_comb of 373 ("blast$BSUM", [i, x, y, c]) => 374 (false, (dim_of_word tm, x, y, c)) 375 | _ => raise ERR "dest_sum" "") 376 | ("blast$BSUM", [n, x, y, c]) => 377 (false, (Arbnum.plus1 (numLib.dest_numeral n), x, y, c)) 378 | ("blast$BCARRY", [n, x, y, c]) => 379 (true, (numLib.dest_numeral n, x, y, c)) 380 | _ => raise ERR "dest_sum" "" 381 382 val is_sum = Lib.can dest_sum 383 384 fun pick_max [] m = m 385 | pick_max ((h as (_,(n,_,_,_)))::t) (m as (_,(n2,_,_,_))) = 386 pick_max t (if Arbnum.>(n, n2) then h else m) 387 388 fun remove_redundant [] = [] 389 | remove_redundant ((h as (_,(n,x,y,c)))::t) = 390 let 391 val (l,r) = List.partition 392 (fn (_, (n2, x2, y2, c2)) => 393 x ~~ x2 andalso y ~~ y2 andalso c ~~ c2) t 394 in 395 pick_max l h :: remove_redundant r 396 end 397in 398 fun mk_sums tm = 399 let 400 val rws = mk_testbit_thms tm 401 val tms = HolKernel.find_terms is_sum tm 402 val tms = tms |> Lib.op_mk_set aconv 403 |> Listsort.sort 404 (Int.compare o (Term.term_size ## Term.term_size)) 405 |> List.map dest_sum 406 |> remove_redundant 407 val () = if !blast_trace > 0 andalso not (List.null tms) 408 then print ("Found " ^ Int.toString (List.length tms) ^ 409 " summation term(s)\n") 410 else () 411 val (_, rwts, c_outs) = 412 List.foldl 413 (fn ((b,nxyc), (i, rwts, c_outs)) => 414 (if !blast_trace > 0 415 then print ("Expanding term... " ^ Int.toString i ^ "\n") 416 else () 417 ; if b then (i + 1, rwts, mk_carry rwts nxyc :: c_outs) 418 else (i + 1, mk_summation rwts nxyc @ rwts, c_outs))) 419 (1, rws, []) tms 420 in 421 rwts @ c_outs 422 end 423end 424 425(* ------------------------------------------------------------------------ 426 WORD_LIT_CONV : Rewrites occurances of ``BIT i v`` using theorems 427 ``BIT i v = (i = p1) \/ ... \/ (i = pn)``, where 428 v is the numeric value of the literal and p1..pn 429 are the bit positions for T bits. 430 ------------------------------------------------------------------------ *) 431 432local 433 val BIT_SET_CONV = Conv.REWR_CONV wordsTheory.BIT_SET THENC EVAL_CONV 434 435 fun is_bit_lit tm = 436 case Lib.total bitSyntax.dest_bit tm of 437 SOME (_, n) => numSyntax.is_numeral n 438 | NONE => false 439 440 fun mk_bit_sets tm = 441 let 442 val tms = Lib.op_mk_set aconv (HolKernel.find_terms is_bit_lit tm) 443 in 444 List.map BIT_SET_CONV tms 445 end 446in 447 fun WORD_LIT_CONV tm = PURE_REWRITE_CONV (mk_bit_sets tm) tm 448end 449 450(* ------------------------------------------------------------------------ 451 fcp_eq_thm : generates a bitwise equality theorem for a given word type. 452 For example, fcp_eq_thm ``:word2`` gives the theorem 453 |- !a b. (a = b) = (a ' 0 = b ' 0) /\ (a ' 1 = b ' 1). 454 ------------------------------------------------------------------------ *) 455 456local 457 val FCP_EQ_EVERY = prove( 458 ���!a b:'a word. 459 (a = b) = EVERY (\i. a ' i = b ' i) (GENLIST I (dimindex (:'a)))���, 460 SRW_TAC [fcpLib.FCP_ss] [listTheory.EVERY_GENLIST]) 461 462 val FCP_EQ_EVERY = 463 REWRITE_RULE [GSYM rich_listTheory.COUNT_LIST_GENLIST, 464 rich_listTheory.COUNT_LIST_compute] FCP_EQ_EVERY 465 466 val FCP_EQ_CONV = Conv.REWR_CONV FCP_EQ_EVERY THENC EVAL_CONV 467 468 val fcp_map = ref (Redblackmap.mkDict Arbnum.compare) 469 : (Arbnum.num, Thm.thm) Redblackmap.dict ref 470in 471 fun fcp_eq_thm ty = 472 case Lib.total (fcpLib.index_to_num o wordsSyntax.dest_word_type) ty of 473 SOME n => 474 (case Redblackmap.peek (!fcp_map, n) of 475 SOME thm => thm 476 | _ => 477 let 478 val a = Term.mk_var ("a", ty) 479 val b = Term.mk_var ("b", ty) 480 val thm = FCP_EQ_CONV (boolSyntax.mk_eq (a,b)) 481 val thm = Thm.GEN a (Thm.GEN b thm) 482 val () = fcp_map := Redblackmap.insert (!fcp_map, n, thm) 483 in 484 thm 485 end) 486 | NONE => raise ERR "fcp_eq_thm" "" 487end 488 489(* ------------------------------------------------------------------------ 490 SMART_MUL_LSL_CONV : converts ``n2w n * w`` into 491 ``w1 << p1 + ... + wn << pn`` where wi is either w or -w 492 ------------------------------------------------------------------------ *) 493 494local 495 val SYM_WORD_NEG_MUL = GSYM wordsTheory.WORD_NEG_MUL 496 fun boolify s = 497 Substring.full o String.implode o (fn l => List.take (l, s)) o 498 String.explode o StringCvt.padLeft #"0" s o Arbnum.toBinString 499 fun pos x = (true, x) 500 fun neg x = (false, x) 501 fun partials a i s = 502 if Substring.isEmpty s 503 then a 504 else let 505 val (zeros, r) = Substring.splitl (Lib.equal #"0") s 506 val (ones, r) = Substring.splitl (Lib.equal #"1") r 507 val j = i - Substring.size zeros 508 val l = Substring.size ones 509 in 510 if l = 0 511 then a 512 else if i = j orelse l < 3 513 then partials (a @ List.tabulate (l, fn x => pos (j - x))) (j - l) 514 r 515 else partials (a @ [pos (j + 1), neg (j + 1 - l)]) (j - l) r 516 end 517 val partials = partials [] 518 val WORD_LSL_CONV = 519 Conv.DEPTH_CONV 520 (Conv.REWR_CONV 521 (SPECL [���w: 'a word���, ���arithmetic$NUMERAL a���] WORD_MUL_LSL)) 522 THENC wordsLib.WORD_ARITH_CONV 523 fun partials_thm (n, sz) = 524 let 525 val s = Arbnum.toInt sz 526 val p = partials (s - 1) o boolify s 527 val l = p n 528 val nl = p (Arbnum.- (Arbnum.pow (Arbnum.two, sz), n)) 529 val pos = List.length l < 2 * List.length nl 530 val l = if pos then l else nl 531 fun mk_lsl x p = 532 if p = 0 then x else wordsSyntax.mk_word_lsl (x, numLib.term_of_int p) 533 val x = Term.mk_var ("x", wordsSyntax.mk_int_word_type s) 534 val nx = wordsSyntax.mk_word_2comp x 535 fun mk (sgn, p) = 536 mk_lsl (if pos = sgn then x else wordsSyntax.mk_word_2comp x) p 537 in 538 List.foldl 539 (fn (x, t) => wordsSyntax.mk_word_add (t, mk x)) (mk (hd l)) (tl l) 540 |> WORD_LSL_CONV 541 |> GSYM 542 end 543in 544 fun SMART_MUL_LSL_CONV tm = 545 let 546 val l = fst (wordsSyntax.dest_word_mul tm) 547 in 548 case Lib.total wordsSyntax.dest_word_2comp l of 549 SOME v => 550 if Lib.total wordsSyntax.dest_word_literal v = SOME Arbnum.one 551 then Conv.REWR_CONV SYM_WORD_NEG_MUL tm 552 else raise ERR "SMART_MUL_LSL_CONV" "not -1w * x" 553 | NONE => 554 let 555 val x as (n, sz) = 556 wordsSyntax.dest_mod_word_literal l 557 handle HOL_ERR _ => (Arbnum.zero, Arbnum.zero) 558 in 559 if sz = Arbnum.zero orelse Arbnum.< (n, Arbnum.fromInt 11) 560 then wordsLib.WORD_MUL_LSL_CONV tm 561 else Conv.REWR_CONV (partials_thm x) tm 562 end 563 end 564end 565 566(* ------------------------------------------------------------------------ *) 567 568local 569 val thm = 570 SPECL [���a: 'a words$word���, ���n2w (NUMERAL n) : 'a word���] 571 wordsTheory.WORD_SUM_ZERO 572 val WORD_SUM_ZERO_CONV = 573 Conv.REWR_CONV thm THENC Conv.RHS_CONV wordsLib.WORD_EVAL_CONV 574 575 val word_ss = std_ss++wordsLib.SIZES_ss++wordsLib.WORD_ARITH_ss++ 576 wordsLib.WORD_LOGIC_ss++wordsLib.WORD_SHIFT_ss++ 577 wordsLib.WORD_CANCEL_ss 578 579 val SYM_WORD_NOT_LOWER = GSYM WORD_NOT_LOWER 580 581 val bit_rwts = [word_lsb_def, word_msb_def, word_bit_def] 582 583 val order_rwts = 584 [WORD_HIGHER, 585 REWRITE_RULE [SYM_WORD_NOT_LOWER] WORD_HIGHER_EQ, 586 SYM_WORD_NOT_LOWER, 587 WORD_GREATER, 588 WORD_GREATER_EQ, 589 REWRITE_RULE [SYM_WORD_NOT_LOWER, word_L_def] WORD_LT_LO, 590 REWRITE_RULE [SYM_WORD_NOT_LOWER, word_L_def] WORD_LE_LS, 591 WORD_LOWER_REFL, WORD_LOWER_EQ_REFL, 592 WORD_LESS_REFL, WORD_LESS_EQ_REFL, 593 WORD_0_LS, WORD_LESS_0_word_T, 594 WORD_LS_word_0, WORD_LO_word_0] 595in 596 val WORD_SIMP_CONV = 597 SIMP_CONV word_ss bit_rwts 598 THENC Conv.TRY_CONV WORD_SUM_ZERO_CONV 599 THENC REWRITE_CONV order_rwts 600 THENC Conv.DEPTH_CONV wordsLib.SIZES_CONV 601 THENC Conv.DEPTH_CONV SMART_MUL_LSL_CONV 602 THENC Conv.DEPTH_CONV WORD_DIV_LSR_CONV 603end 604 605(* ------------------------------------------------------------------------ 606 LSL_BV_CONV, LSR_BV_CONV, ASR_BV_CONV, ROR_BV_CONV, ROL_BV_CONV : 607 Expand shifts by bit-vector 608 ------------------------------------------------------------------------ *) 609 610local 611 val word_bits_thm1 = prove( 612 ���!l h n w:'a word. 613 l + n < dimindex(:'a) /\ l + n <= h ==> 614 ((h -- l) w ' n = w ' (n + l))���, 615 SRW_TAC [fcpLib.FCP_ss, ARITH_ss] [word_bits_def]) 616 617 val word_bits_thm2 = prove( 618 ���!l h n w:'a word. 619 n < dimindex(:'a) /\ h < l + n ==> ((h -- l) w ' n = F)���, 620 SRW_TAC [fcpLib.FCP_ss, ARITH_ss] [word_bits_def]) 621 622 val word_bits_thm3 = word_bits_thm1 |> SPEC ���0n��� |> SIMP_RULE std_ss [] 623 val word_bits_thm4 = word_bits_thm1 |> SPECL [���l:num���,���dimindex(:'a) - 1���] 624 |> SIMP_RULE (arith_ss++boolSimps.CONJ_ss) [] 625 |> GEN_ALL 626 val word_bits_thm5 = word_bits_thm2 |> SPEC ���0n��� |> SIMP_RULE std_ss [] 627 val word_bits_thm6 = word_bits_thm2 |> SPECL [���l:num���,���dimindex(:'a) - 1���] 628 |> SIMP_RULE (arith_ss++boolSimps.CONJ_ss) 629 [DECIDE ``a < b + (c + 1) = a <= b + c : num``] 630 |> GEN_ALL 631 632 fun mk_word_eq_lit_thms ty = 633 let 634 val d = fcpSyntax.dest_int_numeric_type ty 635 val wty = wordsSyntax.mk_word_type ty 636 val v = Term.mk_var ("m", wty) 637 val eq_thm = fcp_eq_thm wty 638 in 639 List.tabulate (d, fn i => 640 let 641 val n = wordsSyntax.mk_n2w (numLib.term_of_int i, ty) 642 val tm = boolSyntax.mk_eq (v, n) 643 in 644 (Conv.RHS_CONV (Conv.REWR_CONV n2w_def THENC WORD_LIT_CONV) 645 THENC Conv.REWR_CONV eq_thm 646 THENC ADD_INDEX_CONV) tm 647 end) 648 end 649 650 fun mk_word_bits_indx_thms ty = 651 let 652 val d = fcpSyntax.dest_int_numeric_type ty 653 val h = Arbnum.toInt (Arbnum.log2 (Arbnum.fromInt (d - 1))) 654 val h_plus1 = h + 1 655 val h_tm = numLib.term_of_int h 656 val h_plus1_tm = numLib.term_of_int h_plus1 657 val wty = wordsSyntax.mk_word_type ty 658 val v = Term.mk_var ("m", wty) 659 val dim = fcpSyntax.mk_dimindex ty 660 in 661 List.tabulate (d, fn i => 662 let 663 val n = numLib.term_of_int i 664 val lt_thm = mk_less_thm (n, dim) 665 val sm = numSyntax.mk_plus (h_plus1_tm,n) 666 val rwt1 = 667 if i <= h 668 then let 669 val le_thm = mk_leq_thm (n, h_tm) 670 in 671 Thm.MP (Drule.ISPECL [h_tm, n, v] word_bits_thm3) 672 (Thm.CONJ lt_thm le_thm) 673 end 674 else let 675 val lt_thm2 = mk_less_thm (h_tm, n) 676 in 677 Thm.MP (Drule.ISPECL [h_tm, n, v] word_bits_thm5) 678 (Thm.CONJ lt_thm lt_thm2) 679 end 680 val rwt2 = 681 if i + h_plus1 < d 682 then let 683 val lt_thm2 = mk_less_thm (sm, dim) 684 in 685 wordsLib.WORD_EVAL_RULE 686 (Thm.MP (Drule.ISPECL [h_plus1_tm, n, v] 687 word_bits_thm4) lt_thm2) 688 end 689 else let 690 val le_thm = mk_leq_thm (dim, sm) 691 in 692 wordsLib.WORD_EVAL_RULE 693 (Thm.MP (Drule.ISPECL [h_plus1_tm, n, v] 694 word_bits_thm6) 695 (Thm.CONJ lt_thm le_thm)) 696 end 697 in 698 [rwt1,rwt2] 699 end) 700 end 701 702 val mk_word_bits_indx_thms = List.concat o mk_word_bits_indx_thms 703 704 fun mk_bv_thm thm ty = 705 let 706 val rwts = mk_word_eq_lit_thms ty @ mk_word_bits_indx_thms ty 707 in 708 thm 709 |> Thm.INST_TYPE [Type.alpha |-> ty] 710 |> Conv.CONV_RULE 711 (Conv.STRIP_QUANT_CONV (Conv.RHS_CONV 712 (EVAL_CONV THENC REWRITE_CONV rwts))) 713 end 714 715 fun BV_CONV last mk_bv tm = 716 Conv.REWR_CONV (!last) tm 717 handle HOL_ERR _ => 718 let 719 val thm = mk_bv (wordsSyntax.dim_of tm) 720 in 721 (last := thm; Conv.REWR_CONV thm tm) 722 end 723 724 val last_lsl_thm = ref combinTheory.I_THM 725 val last_lsr_thm = ref combinTheory.I_THM 726 val last_asr_thm = ref combinTheory.I_THM 727 val last_ror_thm = ref combinTheory.I_THM 728 val last_rol_thm = ref combinTheory.I_THM 729in 730 fun LSL_BV_CONV tm = BV_CONV last_lsl_thm 731 (mk_bv_thm blastTheory.word_lsl_bv_expand) tm 732 fun LSR_BV_CONV tm = BV_CONV last_lsr_thm 733 (mk_bv_thm blastTheory.word_lsr_bv_expand) tm 734 fun ASR_BV_CONV tm = BV_CONV last_asr_thm 735 (mk_bv_thm blastTheory.word_asr_bv_expand) tm 736 fun ROR_BV_CONV tm = BV_CONV last_rol_thm 737 (mk_bv_thm blastTheory.word_ror_bv_expand) tm 738 fun ROL_BV_CONV tm = BV_CONV last_rol_thm 739 (mk_bv_thm blastTheory.word_rol_bv_expand) tm 740end 741 742(* ------------------------------------------------------------------------ 743 BLAST_MUL_CONV : expands bit vector multiplication 744 ------------------------------------------------------------------------ *) 745 746local 747 fun mk_bitwise_mul i = 748 blastTheory.BITWISE_MUL 749 |> Thm.INST_TYPE [Type.alpha |-> fcpSyntax.mk_int_numeric_type i] 750 |> Conv.CONV_RULE 751 (Conv.STRIP_QUANT_CONV (Conv.RHS_CONV 752 (EVAL_CONV THENC PURE_REWRITE_CONV [wordsTheory.WORD_ADD_0]))) 753 754 val mul_rwts = ref ([]: thm list) 755in 756 fun BLAST_MUL_CONV tm = 757 let 758 val l = fst (wordsSyntax.dest_word_mul tm) 759 val sz = fcpSyntax.dest_int_numeric_type (wordsSyntax.dim_of l) 760 val _ = sz <= !blast_multiply_limit orelse 761 raise ERR "BLAST_MUL_CONV" "bigger than multiply limit" 762 in 763 PURE_REWRITE_CONV (!mul_rwts) tm 764 handle Conv.UNCHANGED => 765 (mul_rwts := mk_bitwise_mul sz :: !mul_rwts 766 ; PURE_REWRITE_CONV (!mul_rwts) tm) 767 end 768end 769 770(* ------------------------------------------------------------------------ 771 BLAST_CONV : expands a bit vector term using the definitions for 772 the standard operations. First does a normalization to 773 re-introduce subtraction 774 ------------------------------------------------------------------------ *) 775 776local 777 val word_join = SIMP_RULE (std_ss++boolSimps.LET_ss) [] word_join_def 778 val index_cond = 779 ``(if b then x:'a word else y) ' i = if b then x ' i else y ' i`` 780 |> simpLib.SIMP_PROVE std_ss [COND_RAND, COND_RATOR] |> GEN_ALL 781 val xor_thm = tautLib.TAUT_PROVE ``~(a = b) = (a = ~b:bool)`` 782 val word_xor = REWRITE_RULE [xor_thm] word_xor_def 783 val reduce_xor = REWRITE_RULE [xor_thm] reduce_xor_def 784 785 val word_L_thm = prove( 786 ���INT_MINw :'a word = FCP i. i = dimindex (:'a) - 1���, 787 SRW_TAC [fcpLib.FCP_ss] [word_L]) 788 789 val minus1_thm = prove( 790 ���-1w : 'a word = $FCP (K T)���, 791 SRW_TAC [fcpLib.FCP_ss] [REWRITE_RULE [SYM WORD_NEG_1] word_T]) 792 793 val w2w_thm = prove( 794 ���!w: 'a word. w2w w : 'b word = FCP i. i < dimindex (:'a) /\ w ' i���, 795 SRW_TAC [fcpLib.FCP_ss] [w2w]) 796 797 val sw2sw_thm = prove( 798 ���!w: 'a word. 799 sw2sw w :'b word = 800 FCP i. if i < dimindex (:'a) \/ dimindex (:'b) < dimindex (:'a) then 801 w ' i 802 else 803 w ' (dimindex (:'a) - 1)���, 804 SRW_TAC [fcpLib.FCP_ss] [sw2sw, word_msb_def]) 805 806 fun WORD_NEG_CONV tm = 807 let 808 val t = wordsSyntax.dest_word_2comp tm 809 in 810 case Lib.total wordsSyntax.dest_word_literal t of 811 SOME v => if v = Arbnum.one 812 then raise Conv.UNCHANGED 813 else wordsLib.WORD_EVAL_CONV tm 814 | NONE => ONCE_REWRITE_CONV [WORD_NEG] tm 815 end 816 817 val cnv = computeLib.compset_conv (reduceLib.num_compset()) 818 [computeLib.Defs 819 [n2w_def, v2w_def, word_xor, word_or_def, word_and_def, 820 word_1comp_def, word_nor_def, word_xnor_def, word_nand_def, 821 word_reduce_def, reduce_or_def, reduce_and_def, reduce_xor, 822 reduce_xnor_def, reduce_nand_def, word_compare_def, 823 word_replicate_def, word_join, word_concat_def, word_reverse_def, 824 word_modify_def, word_lsl_def, word_lsr_def, word_asr_def, 825 word_ror_def, word_rol_def, word_rrx_def, word_msb_def, word_lsb_def, 826 word_extract_def, word_bits_def, word_abs, word_slice_def, 827 word_bit_def, word_signed_bits_def, bit_field_insert_def, index_cond, 828 SYM WORD_NEG_1, word_L_thm, minus1_thm, w2w_thm, sw2sw_thm, 829 BITWISE_ADD, BITWISE_SUB, BITWISE_LO, fcpTheory.FCP_UPDATE_def, 830 listTheory.HD, listTheory.TL, listTheory.SNOC, listTheory.FOLDL, 831 listTheory.GENLIST_GENLIST_AUX, numLib.SUC_RULE 832 listTheory.GENLIST_AUX, combinTheory.o_THM, pairTheory.SND, 833 pairTheory.FST], 834 computeLib.Convs 835 [(``fcp$dimindex:'a itself -> num``, 1, wordsLib.SIZES_CONV), 836 (``words$dimword:'a itself -> num``, 1, wordsLib.SIZES_CONV), 837 (``words$INT_MIN:'a itself -> num``, 1, wordsLib.SIZES_CONV), 838 (``words$word_2comp:'a word -> 'a word``, 1, WORD_NEG_CONV), 839 (``words$word_mul:'a word -> 'a word -> 'a word``, 2, BLAST_MUL_CONV), 840 (``words$word_lsl_bv:'a word -> 'a word -> 'a word``, 2, LSL_BV_CONV), 841 (``words$word_lsr_bv:'a word -> 'a word -> 'a word``, 2, LSR_BV_CONV), 842 (``words$word_asr_bv:'a word -> 'a word -> 'a word``, 2, ASR_BV_CONV), 843 (``words$word_ror_bv:'a word -> 'a word -> 'a word``, 2, ROR_BV_CONV), 844 (``words$word_rol_bv:'a word -> 'a word -> 'a word``, 2, ROL_BV_CONV) 845 ]] 846in 847 val BLAST_CONV = 848 PURE_REWRITE_CONV [GSYM word_sub_def, WORD_SUB] 849 THENC cnv 850 THENC WORD_LIT_CONV 851end 852 853(* ------------------------------------------------------------------------ 854 BIT_TAUT_CONV : wrapper around HolSatLib.SAT_PROVE 855 ------------------------------------------------------------------------ *) 856 857fun non_prop_terms tm = 858 let 859 fun non_prop_args acc tmlist = 860 case tmlist of 861 [] => acc 862 | tm :: ts => 863 let 864 val (opp, args) = boolSyntax.dest_strip_comb tm 865 handle HOL_ERR _ => ("", []) 866 in 867 if Lib.mem opp ["bool$T", "bool$F", "bool$~", 868 "bool$/\\", "bool$\\/", "min$==>"] 869 then non_prop_args acc (args @ ts) 870 else if Lib.mem opp ["min$=", "bool$COND"] andalso 871 Lib.all (fn t => Term.type_of t = Type.bool) args 872 then non_prop_args acc (args @ ts) 873 else if Term.type_of tm = Type.bool 874 then non_prop_args (HOLset.add (acc, tm)) ts 875 else raise ERR "non_prop_terms" "Not a boolean term" 876 end 877 in 878 non_prop_args Term.empty_tmset [tm] 879 end 880 881local 882 val lem = numLib.DECIDE ``!b. if b then T else T`` 883in 884 fun PROP_PROVE conv tm = 885 let 886 val thm = Conv.QCONV (REWRITE_CONV [lem]) tm 887 val c = rhsc thm 888 in 889 if Teq c orelse Feq c 890 then thm 891 else Conv.RIGHT_CONV_RULE 892 (Conv.REWR_CONV (Drule.EQT_INTRO (conv c))) thm 893 handle HOL_ERR _ => 894 Drule.EQF_INTRO (conv (boolSyntax.mk_neg tm)) 895 handle HOL_ERR _ => 896 raise ERR "PROP_PROVE" "contingent proposition" 897 end 898end 899 900fun SAT_CONV tm = HolSatLib.SAT_PROVE tm (* HolSatLib.SAT_ORACLE *) 901 handle HolSatLib.SAT_cex _ => raise ERR "SAT_CONV" "" 902 903fun DPLL_CONV tm = Thm.CCONTR tm (Lib.trye dpll.DPLL_TAUT tm) 904 905fun BIT_TAUT_CONV tm = 906 let 907 val insts = HOLset.listItems (non_prop_terms tm) 908 val vars = Term.genvars Type.bool (List.length insts) 909 val theta = Lib.map2 (Lib.curry (op |->)) insts vars 910 val tm' = Term.subst theta tm 911 val sz = Term.term_size tm' 912 val f = if !blast_trace > 2 913 then (print ("Checking proposition of size: " ^ 914 Int.toString sz ^ "\n") 915 ; real_time) 916 else I 917 val thm = f (PROP_PROVE (if sz < 100 then DPLL_CONV else SAT_CONV)) tm' 918 val theta' = Lib.map2 (Lib.curry (op |->)) vars insts 919 in 920 Thm.INST theta' thm 921 end 922 923local 924 fun eq_fst_partition [] = [] 925 | eq_fst_partition ((x,y)::l) = 926 let 927 val (eqx,neqx) = List.partition (term_eq x o fst) l 928 in 929 ((x, y :: List.map snd eqx)) :: eq_fst_partition neqx 930 end 931 932 fun word_counter (x,l) = 933 let 934 val i = Term.mk_var ("i", numLib.num) 935 val ty' = wordsSyntax.dest_word_type (type_of x) 936 in 937 l |> List.filter fst 938 |> List.map (fn (_,n) => boolSyntax.mk_eq (i, n)) 939 |> (fn l => if List.null l 940 then boolSyntax.F 941 else boolSyntax.list_mk_disj l) 942 |> (fn f => fcpSyntax.mk_fcp (Term.mk_abs (i, f), ty')) 943 |> wordsLib.WORD_EVAL_CONV 944 |> concl 945 |> rhs 946 |> (fn t => {redex = x, residue = t}) 947 end 948 949 fun bool_counter tm = 950 case Lib.total boolSyntax.dest_neg tm of 951 SOME t => {redex = t, residue = boolSyntax.F} 952 | NONE => {redex = tm, residue = boolSyntax.T} 953 954 fun dest_fcp (b: bool) tm = 955 let 956 val (x, y) = fcpSyntax.dest_fcp_index tm 957 in 958 (x, (b, y)) 959 end 960 961 fun dest_bit tm = 962 case Lib.total boolSyntax.dest_neg tm of 963 SOME t => dest_fcp false t 964 | NONE => dest_fcp true tm 965in 966 fun counterexample tm = 967 let 968 val tm = snd (boolSyntax.strip_forall tm) 969 in 970 if Feq tm orelse Teq tm then [] 971 else let 972 val insts = HOLset.listItems (non_prop_terms tm) 973 val vars = Term.genvars Type.bool (List.length insts) 974 val theta = Lib.map2 (Lib.curry (op |->)) insts vars 975 val tm' = Term.subst theta tm 976 val thm = (HolSatLib.SAT_PROVE tm'; NONE) 977 handle HolSatLib.SAT_cex thm => SOME thm 978 in 979 case thm of 980 NONE => [] 981 | SOME t => 982 let 983 val theta' = Lib.map2 (Lib.curry (op |->)) vars insts 984 val c = fst (boolSyntax.dest_imp (concl t)) 985 val c = boolSyntax.strip_conj (Term.subst theta' c) 986 val (bits,rest) = List.partition (Lib.can dest_bit) c 987 val bits = eq_fst_partition (List.map dest_bit bits) 988 in 989 List.map word_counter bits @ List.map bool_counter rest 990 end 991 end 992 end 993end 994 995val arb_num_tm = boolSyntax.mk_arb numSyntax.num 996 997local 998 fun print_subst {redex,residue} = 999 let 1000 val s = case Lib.total wordsSyntax.dest_n2w residue of 1001 SOME (tm, _) => 1002 if Term.term_eq tm arb_num_tm 1003 then "ARB (0w)" 1004 else Hol_pp.term_to_string residue 1005 | NONE => Hol_pp.term_to_string residue 1006 in 1007 Hol_pp.term_to_string redex ^ " -> " ^ s ^ "\n\n" 1008 end 1009in 1010 fun print_counterexample l = 1011 if List.null l 1012 then print "No counterexample found!\n" 1013 else (print "Found counterexample:\n\n" 1014 ; List.app (fn c => print (print_subst c ^ "and\n\n")) 1015 (Lib.butlast l) 1016 ; print (print_subst (List.last l))) 1017end 1018 1019(* ------------------------------------------------------------------------ 1020 BIT_BLAST_CONV : convert a bit vector assertion ``a = b``, ``a ' n`` or 1021 ``a <+ b`` into bitwise propositions. Uses SAT to try 1022 to reduce sub-expressions to T or F. 1023 BBLAST_CONV : wrapper around BIT_BLAST_CONV. 1024 ------------------------------------------------------------------------ *) 1025 1026local 1027 fun is_word_index tm = 1028 case Lib.total wordsSyntax.dest_index tm of 1029 SOME (w, i) => numLib.is_numeral i andalso Lib.can dim_of_word w 1030 | NONE => false 1031in 1032 fun is_blastable tm = 1033 is_word_index tm orelse 1034 case Lib.total boolSyntax.dest_eq tm of 1035 SOME (w, v) => Lib.can dim_of_word w 1036 | NONE => (case Lib.total wordsSyntax.dest_word_lo tm of 1037 SOME (w, _) => Lib.can dim_of_word w 1038 | NONE => false) 1039 1040 fun full_is_blastable tm = 1041 is_blastable tm orelse 1042 case Lib.total boolSyntax.dest_strip_comb tm of 1043 SOME ("words$word_bit", [_, w]) => Lib.can dim_of_word w 1044 | SOME (s, [w, _]) => 1045 Lib.can dim_of_word w andalso 1046 Lib.mem s 1047 ["words$word_lt", "words$word_le", "words$word_gt", 1048 "words$word_ge", "words$word_hi", "words$word_hs", "words$word_ls"] 1049 | SOME (s, [w]) => 1050 Lib.can dim_of_word w andalso 1051 Lib.mem s ["words$word_msb", "words$word_lsb"] 1052 | _ => false 1053end 1054 1055local 1056 val FCP_NEQ = trace ("metis",0) prove( 1057 ���!i a b:'a word. 1058 i < dimindex (:'a) /\ ((a ' i = b ' i) = F) ==> ((a = b) = F)���, 1059 SRW_TAC [fcpLib.FCP_ss] [] 1060 THEN METIS_TAC []) 1061 1062 val dummy_thm = SPEC_ALL combinTheory.I_THM 1063 1064 val toString = Arbnum.toString 1065 1066 fun bit_theorems conv (n, l, r) = 1067 let 1068 fun BIT_TAUT_CONV tm = (INDEX_CONV THENC conv) tm 1069 handle Conv.UNCHANGED => dummy_thm 1070 val tr = !blast_trace > 1 1071 val () = if tr then print ("Checking " ^ toString n ^ " bit word\n") 1072 else () 1073 fun bit_theorem i a = 1074 if i = n 1075 then Lib.PASS a 1076 else let 1077 val () = 1078 if tr then print ("Checking bit... " ^ toString i ^ "\n") 1079 else () 1080 val ii = numLib.mk_numeral i 1081 val li = wordsSyntax.mk_index (l, ii) 1082 val ri = wordsSyntax.mk_index (r, ii) 1083 val idx_thm = BIT_TAUT_CONV (boolSyntax.mk_eq (li, ri)) 1084 in 1085 if Feq (rhsc idx_thm) then Lib.FAIL (ii, idx_thm) 1086 else bit_theorem (Arbnum.plus1 i) (idx_thm :: a) 1087 end 1088 in 1089 bit_theorem Arbnum.zero [] 1090 end 1091 1092 fun FORALL_EQ_RULE vars t = 1093 List.foldr (fn (v,t) => Drule.FORALL_EQ v t) t vars 1094 |> Conv.RIGHT_CONV_RULE (Rewrite.REWRITE_CONV []) 1095in 1096 fun BIT_BLAST_CONV tm = 1097 let 1098 val _ = is_blastable tm orelse 1099 raise ERR "BIT_BLAST_CONV" "term not suited to bit blasting" 1100 val thm = Conv.QCONV (BLAST_CONV THENC ADD_INDEX_CONV) tm 1101 val c = rhsc thm 1102 in 1103 if Term.term_eq c boolSyntax.T orelse Term.term_eq c boolSyntax.F 1104 then thm 1105 else let 1106 val RW_CONV = PURE_REWRITE_CONV (mk_sums c) 1107 in 1108 if wordsSyntax.is_index tm 1109 then Conv.RIGHT_CONV_RULE RW_CONV thm 1110 handle Conv.UNCHANGED => thm 1111 else if wordsSyntax.is_word_lo tm 1112 then Conv.RIGHT_CONV_RULE RW_CONV thm 1113 else let 1114 val (l,r) = boolSyntax.dest_eq c 1115 in 1116 case bit_theorems RW_CONV (dim_of_word l, l, r) of 1117 Lib.PASS thms => 1118 Conv.RIGHT_CONV_RULE 1119 (Conv.REWR_CONV (fcp_eq_thm (Term.type_of l)) 1120 THENC REWRITE_CONV thms) thm 1121 | Lib.FAIL (i, fail_thm) => 1122 let 1123 val ty = wordsSyntax.dim_of l 1124 val sz_thm = mk_size_thm (i, ty) 1125 val thm2 = Drule.MATCH_MP FCP_NEQ 1126 (Thm.CONJ sz_thm fail_thm) 1127 in 1128 Conv.RIGHT_CONV_RULE (Conv.REWR_CONV thm2) thm 1129 end 1130 end 1131 end 1132 end 1133 fun BBLAST_CONV tm = 1134 let 1135 val _ = Term.type_of tm = Type.bool orelse 1136 raise ERR "BBLAST_CONV" "not a bool term" 1137 val (vars,tm') = boolSyntax.strip_forall tm 1138 val thm = Conv.QCONV WORD_SIMP_CONV tm' 1139 val tms = 1140 Lib.op_mk_set aconv (HolKernel.find_terms is_blastable (rhsc thm)) 1141 val thms = Lib.mapfilter BIT_BLAST_CONV tms 1142 val res = FORALL_EQ_RULE vars 1143 (Conv.RIGHT_CONV_RULE 1144 (Rewrite.ONCE_REWRITE_CONV thms 1145 THENC Conv.TRY_CONV BIT_TAUT_CONV) thm) 1146 in 1147 if term_eq (rhsc res) tm then raise Conv.UNCHANGED else res 1148 end 1149end 1150 1151local 1152 fun is_quant tm = boolSyntax.is_forall tm orelse boolSyntax.is_exists tm 1153 1154 fun counter_terms _ [] = raise ERR "counter_terms" "empty" 1155 | counter_terms [] tms = tl tms 1156 | counter_terms ({redex,residue}::l) (t::tms) = 1157 counter_terms l 1158 (Term.subst [redex |-> residue] 1159 (snd (boolSyntax.dest_exists t)) :: t :: tms) 1160 1161 fun build_exists [] _ cthm = cthm 1162 | build_exists _ [] cthm = cthm 1163 | build_exists ({redex,residue}::l1) (t::l2) cthm = 1164 build_exists l1 l2 (Thm.EXISTS (t, residue) cthm) 1165 1166 fun order_ctr [] [] a = List.rev a 1167 | order_ctr [] _ _ = raise ERR "BBLAST_PROVE" "Couldn't prove goal." 1168 | order_ctr (v::vars) counter a = 1169 let 1170 val (c,rest) = Lib.pluck (fn {redex,residue} => (redex ~~ v)) counter 1171 in 1172 order_ctr vars rest (c :: a) 1173 end 1174 handle HOL_ERR _ => raise ERR "BBLAST_PROVE" "Couldn't prove goal." 1175 fun order_counter v c = order_ctr v c [] 1176 1177 val arb_tm = wordsSyntax.mk_n2w (arb_num_tm, Type.alpha) 1178 fun mk_zero_subst v = 1179 (v |-> Term.inst [Type.alpha |-> wordsSyntax.dim_of v] arb_tm) 1180 fun add_subst (s1: (term, term) Lib.subst, s2: (term, term) Lib.subst) = 1181 let 1182 val reds = 1183 List.map (#redex) s2 fun okay v = Lib.all (not o term_eq v) reds 1184 in 1185 s2 @ (List.filter (okay o #redex) s1) 1186 end 1187in 1188 fun BBLAST_PROVE tm = 1189 let 1190 val (vars,tm') = boolSyntax.strip_exists tm 1191 val thm = Conv.QCONV BBLAST_CONV tm' 1192 in 1193 if List.null vars 1194 then Drule.EQT_ELIM thm 1195 handle HOL_ERR _ => 1196 let 1197 val body = snd (boolSyntax.strip_forall tm) 1198 val fvars = Term.free_vars body 1199 val w_subst = Lib.mapfilter mk_zero_subst fvars 1200 val counter = 1201 add_subst (w_subst, counterexample (rhsc thm)) 1202 in 1203 if not (List.null counter) andalso 1204 Lib.can (order_counter fvars) counter 1205 then let 1206 val () = if !blast_counter 1207 then print_counterexample counter 1208 else () 1209 val ctm = 1210 Term.subst [arb_num_tm |-> numSyntax.zero_tm] 1211 (Term.subst counter body) 1212 in 1213 raise HolSatLib.SAT_cex 1214 (wordsLib.WORD_EVAL_CONV ctm) 1215 end 1216 else raise ERR "BBLAST_PROVE" "Couldn't prove goal." 1217 end 1218 else let 1219 val ctm = rhsc thm 1220 in 1221 if Teq ctm 1222 then Drule.EQT_ELIM 1223 ((PURE_ONCE_REWRITE_CONV [thm] 1224 THENC REPEATC Conv.EXISTS_SIMP_CONV) tm) 1225 else let 1226 val counter = counterexample (boolSyntax.mk_neg ctm) 1227 val counter = order_counter vars counter 1228 val ctms = counter_terms counter 1229 [boolSyntax.list_mk_exists (vars, ctm)] 1230 val cthm = 1231 Drule.EQT_ELIM 1232 (wordsLib.WORD_EVAL_CONV (Term.subst counter ctm)) 1233 val cthm' = build_exists (List.rev counter) ctms cthm 1234 in 1235 PURE_ONCE_REWRITE_RULE [GSYM thm] cthm' 1236 end 1237 end 1238 end 1239end 1240 1241val BBLAST_RULE = Conv.CONV_RULE BBLAST_CONV 1242val BBLAST_TAC = Tactic.CONV_TAC BBLAST_CONV 1243 1244val MP_BLASTABLE_TAC = 1245 REPEAT (Tactical.PRED_ASSUM 1246 (fn t => not (markerSyntax.is_abbrev t) andalso 1247 Lib.can (HolKernel.find_term full_is_blastable) t) MP_TAC) 1248 1249val FULL_BBLAST_TAC = MP_BLASTABLE_TAC THEN BBLAST_TAC 1250 1251fun BBLAST_PROVE_TAC (asl, w) = ACCEPT_TAC (BBLAST_PROVE w) (asl, w) 1252 1253(* ------------------------------------------------------------------------ *) 1254 1255end 1256