#
b4b8e85c |
|
18-Aug-2018 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Don't export ERR from HolKernel
|
#
e5fc0f36 |
|
11-Sep-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improving naming of bit-vector signed division constants. This renaming introduces incompatibilities: • words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor). • words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor). • integer_word$word_sdiv (this is a new constant defined directly in terms of int_div). • words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).
|
#
eb1399dc |
|
02-Nov-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Datatype parsing array[number] type Includes test-case
|
#
6c8715da |
|
17-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Tidy up some selftests, making output prettier
|
#
744f9a3b |
|
21-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix many selftests to have prettier output
|
#
df27aa58 |
|
15-Feb-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some function in bitstringSyntax are now based on Arbnum.num instead of Int.int. The old versions were vulnerable to Overflow exceptions.
|
#
58b7f2bd |
|
20-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Various tweaks to bit-vector development. NOTE: It is possible that some bit-vector proofs may break, due to subtle changes in bit-vector simplification. The selftest script now tests calls to WORD_GROUND_CONV. (This conversion's flag is also set to false for use outside of wordsLib.) Some unused tools have been removed from blastLib.
|
#
7a2254a5 |
|
14-May-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence. Includes some tidying-up work. This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib. This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.
|
#
a0a3537b |
|
26-Jan-2013 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Selftest demonstrating problem of #106.
|
#
772fc050 |
|
26-Jan-2013 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use testutils in n-bit/selftest.sml
|
#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
c0e456e5 |
|
28-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix WORD_MUL_LSL_CONV so that it works with ``:'a word`` terms, i.e. words of unspecified width.
|
#
f3bd4784 |
|
27-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add wordsLib.WORD_CANCEL_ss, which is a fancy version of WORD_ARITH_EQ_ss. WORD_CANCEL_ss is now used during the preliminary simplification stage of BBLAST_PROVE, which enables the procedure to better handle simple arithmetic properties (i.e. avoiding unnecessary bit-blasting). For example: we have > SIMP_CONV (srw_ss() ++ wordsLib.WORD_CANCEL_ss) [] ``2w * a - b * 2w + -7w = b + 1w + a`` <<HOL message: inventing new type variable names: 'a>> val it = |- (2w * a − b * 2w + -7w = b + 1w + a) ⇔ (3w * b + 8w = a): thm which is preferable to > SIMP_CONV (srw_ss() ++ wordsLib.WORD_ARITH_EQ_ss) [] <<HOL message: inventing new type variable names: 'a>> val it = |- (2w * a − b * 2w + -7w = b + 1w + a) ⇔ (a + -3w * b + -8w = 0w): thm
|
#
9c35830c |
|
14-Apr-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix glitch in WORD_AND_CANON_CONV.
|
#
08369277 |
|
04-Apr-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few extra theorems.
|
#
ed3dbdc9 |
|
29-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Cosmetic changes.
|
#
2e079a71 |
|
29-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added new operations for shifting by a bit-vector value, namely: LSL: <<~ LSR: >>>~ ASR: >>~ ROR: #>>~ ROL: #<<~ These are supported by the procedures in blastLib. For example, one can prove w <+ 10w /\ s <+ 3w ==> w <<~ (s + 1w) <+ 73w : word16 The time-complexity is a pretty shocking but "simple" 32-bit problems seem to be okay. NB. ROR and ROL only bit-blast with word sizes that are a power of two. Added a new conversion WORD_MOD_BITS_CONV for mapping applications of ``word_mod w (n2w n)`` into ``(h -- 0) w`` where n is a power of two. Also added support for bit-blasting arbitrary multiplication, but the word-size limit is set to 8 bits by default. Things seem to be just about feasible with that limit (and become horrendously slow after that). To improve performance, the conversion BBLAST_CONV does not have exactly the same coverage as before. For backward compatibility, a conversion EBLAST_CONV (which calls SAT at every bit position) is now available.
|
#
2a7fb9dc |
|
26-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improvement to handling of counterexamples under BBLAST_PROVE. (Word variables that do not appear in the SAT theorem are assigned to 0w).
|
#
1f607f6f |
|
24-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Small tidy-up.
|
#
9bc7e4f5 |
|
21-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changes to WORD_MUL_LSL_CONV in an attempt to make it more robust - it was failing on some corner cases. It should also be a bit quicker now too.
|
#
c16f1645 |
|
27-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor bug fix.
|
#
93b5c8c1 |
|
25-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tweak.
|
#
026388c1 |
|
25-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added Tactical.PRED_ASSUM. It's similar to PAT_ASSUM but uses a predicate to pick the assumption. Added blastLib.FULL_BBLAST_TAC, which attempts to use "blastable" assumptions. Make blastLib.BBLAST_PROVE smarter with respect to counterexamples (existential goals). For example, > blastLib.BBLAST_PROVE ``?x y. x + y = 12w : word8``; val it = |- ?x y. x + y = 12w: thm is now possible, and we also have: > blastLib.BBLAST_PROVE ``x < y = x <=+ y : word8``; Found counterexample: y -> 255w and x -> 0w Exception- SAT_cex |- (0w < 255w <=> 0w <=+ 255w) <=> F raised The printing of counterexamples is controlled by the trace "print blast counterexamples".
|
#
d9777034 |
|
25-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add fcpSyntax and tidy up related code.
|
#
2831eaec |
|
20-Oct-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean up type grammars to reflect reality of suffixes as tightest operators. Also, fix a minor pretty-printing bug that was affecting types like ('a + 'b) [32] and document this in src/n-bit/selftest.sml
|
#
1a77b251 |
|
20-Oct-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix bug concerning interaction of arrays and other suffixes. In the process, make it clear that suffixes really do have to be the tightest operators in the grammar. Also, add a type-parsing test for array types to src/n-bit/selftest.sml. Thanks to Anthony for the report.
|
#
d52cb810 |
|
13-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add BBLAST_PROVE.
|
#
c56266a6 |
|
06-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add FST and SND rewrites for BLAST_CONV. This help when proving things about word_rrx, e.g. ``SND (word_rrx (T,v:word32)) = v >>> 1 !! 0x80000000w``
|
#
6283401d |
|
30-Sep-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix glitch in WORD_OR_CANON_CONV where, for example. ``0x20000000w !! 0w`` would not be converted to ``0x20000000w``.
|
#
909ec7e6 |
|
20-Sep-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix problem with BBLAST_CONV raising an Empty exception on certain terms. This was due to dpll.DPLL_TAUT which, for example, raises Empty on ``if b then T else T`` This case has been avoided by adding this theorem as a rewrite. To avoid any similar problems, the call to dpll.DPLL_TAUT is now made under Lib.trye. Thanks to Tjark Weber for reporting this problem.
|
#
cf46facb |
|
25-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix handling of quantifiers in BBLAST_CONV. For example, was previously converting ``!a. P a`` to ``!a. P a = T`` instead of ``(!a. P a) = T``. Few other minor tweaks.
|
#
97bd855d |
|
09-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix a non-termination (stack overflow) bug. Example added to selftest.
|
#
e8d4e1da |
|
27-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Slightly tidy up output of selftest.
|
#
f5a93c8d |
|
27-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove left over junk.
|
#
406b1d45 |
|
27-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix n-bit selftest (had some junk(?) at end) and make it prettier.
|
#
4d386328 |
|
26-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a bit-blasting conversion: BBLAST_CONV. This goes beyond the capabilities of WORD_BIT_EQ_CONV by expanding out additions / subtractions. This allows the new conversion to automatically handle small but tricky bit vector goals. For example: ``(x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)`` and ``!a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w`` (These aren't provable with wordsLib.WORD_DECIDE.) Obviously bit-blasting is a brute force approach, so the new 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. ``(exp1 -- exp2) w``. -- Shifting by non-literal amounts, e.g. ``w << exp``. -- ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w. -- word_div, word_sdiv, word_mod and word_log2.
|