#
5504ac72 |
|
01-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Define entrypoint to change grammars to be tight/loose equality Existing entrypoints change the global grammar; new functions make it easy to adjust arbitrary grammar values.
|
#
1827d4c8 |
|
29-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get src/n-bit to pass its selftest given tight-equality
|
#
5a3e2622 |
|
13-Jun-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid some "inventing new type variable" messages.
|
#
6ff1f5f5 |
|
29-Jan-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove uses of global grammar from some library files Uses of Q.prove dodge redefinitions of the Parse structure, and end up using the surrounding global grammar. For this reason, it's best not to use Q in library implementations.
|
#
4888f523 |
|
15-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove eqtype declaration for term type
|
#
268ca9e2 |
|
06-Sep-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid "inventing new type variable" messages when loading some Lib files.
|
#
b280a5fc |
|
19-Apr-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve treatment of multiplication by constant in blastLib. For example, testing with BBLAST_PROVE ``x <+ 10w: word32 ==> x * n2w (2 ** 8 - 2 ** 4) <+ 2500w`` showed an improvement of 10.8s (before) to 0.53s (after).
|
#
ecb0e313 |
|
15-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add Conv.memoize. This can be used to build conversions that lookup previous result in a red-black tree. The n-bit libraries are updated to make use of Conv.memoize and new functions in computeLib.
|
#
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.
|
#
8691d59e |
|
28-Jun-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add blastLib.BBLAST_PROVE_TAC.
|
#
bbc169fb |
|
23-Aug-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tidy-up of blastLib.
|
#
a9c9addc |
|
21-Aug-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
wordsLib.SIZES_CONV was not behaving properly when applied to some unsuitable terms. Was causing problems in blastLib.
|
#
1a8337d0 |
|
16-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for blastLib.ADD_INDEX_CONV.
|
#
585da7bf |
|
22-Jan-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Ensure that FULL_BBLAST_TAC picks up assumptions containing ``word_bit`` terms.
|
#
994d4858 |
|
27-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Overhaul to rich_listTheory (it had become a bit of a disaster area). Some points: 1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN. 2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them. 3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g. val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC 4. Some incompatibilities are introduced: * FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT. * COUNT_LIST___ADD -> COUNT_LIST_ADD * COUNT_LIST___COUNT -> COUNT_LIST_COUNT * The compute theorems for COUNT_LIST and SPLITP have been renamed. * Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT 5. Some theorems in listTheory have gained quantifiers.
|
#
bf071804 |
|
27-Jun-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweaks to various conversions under src/n-bit.
|
#
b99f6206 |
|
26-Jun-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a theory of bit-strings, which defines word operations over ``:bool list``. The maps "v2w" and "w2v" provide a connection to fixed-width bit vectors.
|
#
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.
|
#
4cf9fe3d |
|
27-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_sign_extend to words emit + minor cosmetic changes.
|
#
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
|
#
4b685909 |
|
22-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added new definitions and theorems for various bit-vector "saturation" operations. These operations return maximal or minimal values instead of, e.g., overflowing (wrapping). For example: |- signed_saturate_add 100w 50w = 127w: thm Also added a new configuration option for printing word literals as 2's complement values. For example: > set_trace "word pp as 2's comp" 1; > ``253w:word8``; val it = ``-3w``: term Be warned that this term is actually ``n2w 253``, it's just being printed as ``word_2comp (n2w 3)``. This printing mode is useful when checking the veracity of machine arithmetic. For example: > EVAL ``signed_saturate_sub 226w 100w : word8``; val it = |- signed_saturate_sub -30w 100w = -128w: thm
|
#
952cfd54 |
|
06-May-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make BBLAST_CONV support division by power of two.
|
#
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.
|
#
f59b5956 |
|
11-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Assorted extra theorems and tools. Added a new constant word_abs, which gives the absolute value of a bit-vector.
|
#
79c3ccd3 |
|
08-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Ensure that FULL_BBLAST_TAC picks up more relevant assumptions.
|
#
e833b627 |
|
27-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Small refinement to reporting of counterexamples. This time indicate when a variables can be assigned any value. For example: > BBLAST_PROVE ``w <+ 0w : word4``; Found counterexample: w -> ARB (0w) Exception- SAT_cex |- 0w <₊ 0w ⇔ F raised
|
#
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).
|
#
6cf565a6 |
|
12-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add function boolSyntax.dest_strip_comb. boolSyntax.dest_strip_comb ``a + b``; val it = ("arithmetic$+", [``a``, ``b``])
|
#
cca2b5bd |
|
26-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweaks.
|
#
890baa4b |
|
27-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix performance bug.
|
#
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".
|
#
b8fb45cb |
|
18-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
More Unicode removal.
|
#
b7e8d478 |
|
18-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove Unicode (reported by Magnus).
|
#
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``
|
#
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.
|
#
f48c6820 |
|
16-Aug-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixes and tweaks following check-in 8434 (GENLIST moving to listTheory).
|
#
6d891ca0 |
|
03-Aug-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make use of rich_listTheory.COUNT_LIST.
|
#
16f473cd |
|
30-Jul-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tweak to expansion of literals.
|
#
ad74a98b |
|
30-Jul-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make WORD_MUL_LSL_CONV more robust with respect to oversized word literals. For example, we now have > WORD_MUL_LSL_CONV ``130w * w : word4``; val it = |- 130w * w = w ≪ 1 : thm whereas previously it would fail.
|
#
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.
|
#
7eaa3169 |
|
03-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Simplified code and added extra tracing information. (Work preformed by FCP_INDEX_CONV is now done by the pre-processing conversion BLAST_CONV.)
|
#
f081f775 |
|
27-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweak to speed up checking trivial propositions.
|
#
cb277121 |
|
27-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Speed things up by using DPLL on small propositions.
|
#
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.
|