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