\DOC

\TYPE {BBLAST_CONV : conv}

\SYNOPSIS

Bit-blasting conversion for words.

\DESCRIBE

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

wordsLib.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

\ENDDOC