BBLAST_CONV : conv
STRUCTURE
SYNOPSIS
Bit-blasting conversion for words.
DESCRIPTION
This conversion expands bit-vector terms into Boolean propositions. It goes beyond the functionality of wordsLib.WORD_BIT_EQ_CONV by handling addition, subtraction and orderings. Consequently, this conversion can automatically handle small, but tricky, bit-vector goals that wordsLib.WORD_DECIDE cannot handle. Obviously bit-blasting is a brute force approach, so this conversion should be used with care. It will only work well for smallish word sizes and when there is only and handful of additions around. It is also "eager" -- additions are expanded out even when not strictly necessary. For example, in
(a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32
the sum a + b is expanded. Users may be able to achieve speed-ups by first introducing abbreviations and then proving general forms, e.g.
x <+ c /\ c <+ d ==> x <+ d:word32
The conversion handles most operators, however, the following are not covered / interpreted:

-- Type variables for word lengths, i.e. terms of type :'a word.

-- General multiplication, i.e. w1 * w2. Multiplication by a literal is okay, although this may introduce many additions.

-- Bit-field selections with non-literal bounds, e.g. (expr1 -- expr2) w.

-- Shifting by non-literal amounts, e.g. w << expr.

-- n2w expr and w2n w. Also w2s, s2w, w2l and l2w.

-- word_div, word_sdiv, word_mod and word_log2.

EXAMPLE
Word orderings are handled:
- blastLib.BBLAST_CONV ``!a b. ~word_msb a /\ ~word_msb b ==> (a <+ b = a < b:word32)``;
val it =
   |- (!a b. ~word_msb a /\ ~word_msb b ==> (a <+ b <=> a < b)) <=> T
   : thm
In some cases the result will be a proposition over bit values:
- blastLib.BBLAST_CONV ``!a. (a + 1w:word8) ' 1``;
val it =
   |- (!a. (a + 1w) ' 1) <=> !a. a ' 1 <=> ~a ' 0
   : thm
This conversion is especially useful where "logical" and "arithmetic" bit-vector operations are combined:
- blastLib.BBLAST_CONV ``!a. ((((((a:word8) * 16w) + 0x10w)) && 0xF0w) >>> 4) = (3 -- 0) (a + 1w)``;
val it =
   |- (!a. (a * 16w + 16w && 240w) >>> 4 = (3 -- 0) (a + 1w)) <=> T
   : thm
SEEALSO
HOL  Trindemossen-1