1\DOC 2 3\TYPE {BBLAST_CONV : conv} 4 5\SYNOPSIS 6 7Bit-blasting conversion for words. 8 9\DESCRIBE 10 11This conversion expands bit-vector terms into Boolean propositions. It goes 12beyond the functionality of {wordsLib.WORD_BIT_EQ_CONV} by handling addition, 13subtraction and orderings. Consequently, this conversion can automatically 14handle small, but tricky, bit-vector goals that {wordsLib.WORD_DECIDE} cannot 15handle. Obviously bit-blasting is a brute force approach, so this conversion 16should be used with care. It will only work well for smallish word sizes and 17when there is only and handful of additions around. It is also "eager" -- 18additions are expanded out even when not strictly necessary. For example, in 19{ 20(a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32 21} 22the sum {a + b} is expanded. Users may be able to achieve speed-ups by first 23introducing abbreviations and then proving general forms, e.g. 24{ 25x <+ c /\ c <+ d ==> x <+ d:word32 26} 27The conversion handles most operators, however, the following are not covered / 28interpreted: 29 30 -- Type variables for word lengths, i.e. terms of type {:'a word}. 31 32 -- General multiplication, i.e. {w1 * w2}. Multiplication by a literal is 33 okay, although this may introduce many additions. 34 35 -- Bit-field selections with non-literal bounds, e.g. {(expr1 -- expr2) w}. 36 37 -- Shifting by non-literal amounts, e.g. {w << expr}. 38 39 -- {n2w expr} and {w2n w}. Also {w2s}, {s2w}, {w2l} and {l2w}. 40 41 -- {word_div}, {word_sdiv}, {word_mod} and {word_log2}. 42 43\EXAMPLE 44Word orderings are handled: 45{ 46- blastLib.BBLAST_CONV ``!a b. ~word_msb a /\ ~word_msb b ==> (a <+ b = a < b:word32)``; 47val it = 48 |- (!a b. ~word_msb a /\ ~word_msb b ==> (a <+ b <=> a < b)) <=> T 49 : thm 50} 51In some cases the result will be a proposition over bit values: 52{ 53- blastLib.BBLAST_CONV ``!a. (a + 1w:word8) ' 1``; 54val it = 55 |- (!a. (a + 1w) ' 1) <=> !a. a ' 1 <=> ~a ' 0 56 : thm 57} 58This conversion is especially useful where "logical" and "arithmetic" bit-vector operations are combined: 59{ 60- blastLib.BBLAST_CONV ``!a. ((((((a:word8) * 16w) + 0x10w)) && 0xF0w) >>> 4) = (3 -- 0) (a + 1w)``; 61val it = 62 |- (!a. (a * 16w + 16w && 240w) >>> 4 = (3 -- 0) (a + 1w)) <=> T 63 : thm 64} 65 66\SEEALSO 67 68wordsLib.WORD_ss, wordsLib.WORD_ARITH_CONV, wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_EVAL_CONV, wordsLib.WORD_CONV 69 70\ENDDOC 71