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