#
66a2b80f |
|
24-Nov-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Make WORD_GROUND_ss visible in wordsLib.sig
|
#
14bfc6e9 |
|
08-May-2020 |
Anthony Fox <anthony.fox@cantab.net> |
Fixes for wordsLib pretty-printing
|
#
fc263107 |
|
19-May-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fix various breakages caused by 86935be3f42 Along the way adjust WORD_CANCEL_CONV to tidy up after itself so that when it sees x + y + z + u = a + y + b + u it doesn't turn it into x + y + z + u - y - u = a + y + b + u - y - u and wait for something else to clean it up, but rather goes straight to x + z = a + b
|
#
51a40c2e |
|
14-Mar-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add facility to print bit-vectors in binary or hex with leading zero padding.
|
#
758774c8 |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add theorem word_concat_assoc and an associated simpset fragment WORD_CONCAT_ASSOC_ss.
|
#
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.
|
#
1c5b031e |
|
14-Apr-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Provide facilities for extending compsets with support for words, strings and integers.
|
#
e63585cf |
|
14-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Further small improvements to PTREE_PEEK_CONV. Squeezes out a tiny bit more performance. The wordsLib conversion BIT_SET_CONV has been updated and is now exported.
|
#
5f7ad54b |
|
02-Oct-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add WORD_BIT_INDEX_CONV and tweak word_bit_CONV.
|
#
fee4467b |
|
20-Jul-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tidy-up formatting of wordsLib code. Also add configuration parameter to WORD_GROUND_CONV.
|
#
d4471915 |
|
30-May-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a new theorem about bit-vector overflow. Includes an improvement to the Cases_on_i2w tactic.
|
#
b5be4920 |
|
16-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Export LESS_CONV from wordsLib.
|
#
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
|
#
58efc826 |
|
06-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve HolSmt's coverage of bit-vector problems. This involves mapping some HOL bit-vector operations into suitable SMT-LIB operations. In particular, provide support for: 1. reduce_and, reduce_or, etc. This is done using wordsLib.EXPAND_REDUCE_CONV. 2. word_lsb, word_msb, word_bit, word_bits, word_slice and bit_field_insert. This is done through rewrites. 3. (w2w:'a word->'b word) and (sw2sw:'a word->'b word) where the word size decreases. Again done using rewrites. 4. ((h >< l) w) : 'a word, where 'a word is larger than h + 1 - l. This is done using wordsLib.EXTEND_EXTRACT_CONV.
|
#
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.
|
#
f6167147 |
|
03-Dec-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a few extra tools to wordsLib: * WORD_SUB_CONV / WORD_SUB_ss These can be used to simplify applications of unary/binary minus, introducing or eliminating subtractions where possible. These must *not* be used simulataneously with srw_ss, WORD_ARITH_ss or WORD_ss (as this will likely result in non-termination). However, can be used to good effect afterwards. For example: wordsLib.WORD_SUB_CONV ``a + -1w * b`` |- a + -1w * b = a - b wordsLib.WORD_SUB_CONV ``-(a - b)`` |- -(a - b) = b - a wordsLib.WORD_SUB_CONV ``a + b * 3w : word2`` |- a + b * 3w = a - b wordsLib.WORD_SUB_CONV ``192w * a + b : word8`` |- 192w * a + b = b - 64w * a * WORD_DIV_LSR_CONV Convert division by a power of two into a right shift. For example: wordsLib.WORD_DIV_LSR_CONV ``(a:word8) // 8w`` |- a // 8w = a >>> 3 * BITS_INTRO_CONV / BITS_INTRO_ss These convert DIV and MOD by powers of two into application of BITS. For example: wordsLib.BITS_INTRO_CONV ``(a DIV 4) MOD 8``; |- (a DIV 4) MOD 8 = BITS 4 2 a wordsLib.BITS_INTRO_CONV ``(a MOD 32) DIV 8``; |- a MOD 32 DIV 8 = BITS 4 3 a wordsLib.BITS_INTRO_CONV ``a MOD 2 ** 4``; |- a MOD 2 ** 4 = BITS 3 0 a wordsLib.BITS_INTRO_CONV ``a MOD dimword (:'a)``; |- a MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 a * n2w_INTRO_TAC <int> Attempts to convert goals of the form ``a = b``, ``a < b`` and ``a <= b`` into goals of the form ``n2w a = n2w b``, ``n2w a <+ n2w b`` and ``n2w a <=+ n2w b``. The integer argument denotes the required word size. This enables some bounded problems (over the naturals) to be proved using bit-vector tactics. For example, the goal: `((11 >< 8) (imm12:word16) : word12) <> 0w ==> ((31 + 2 * w2n ((11 >< 8) imm12 : word12)) MOD 32 = w2n (2w * (11 >< 8) imm12 + -1w : word32))` can be solved with STRIP_TAC THEN n2w_INTRO_TAC 32 THEN FULL_BBLAST_TAC
|
#
a70b492a |
|
31-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some changes to wordsLib.WORD_DP. It now takes a pre-processing conversion and is able to prove goals such as ``w2w (w:word4) : word8 <=+ 16w``.
|
#
3f71a7d7 |
|
18-Jun-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a (fairly crude) printer for showing the types of ><, w2w and @@. Invoked with wordsLib.add_word_cast_printer() and turned off with wordsLib.remove_word_cast_printer()
|
#
701f93ea |
|
24-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added wordsLib.dest_word_literal : term -> Arbnum.num Also ensure "/" is affected by deprecate_word and prefer_word.
|
#
8654de63 |
|
07-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Attempt to tidy up (fix) EmitML and finish off the transition that Scott started. EmitML has been moved to the end of the build sequence. "Hooks" have been eliminated and all EmitML related stuff has been removed from the various theory directories. All code for generating ML/Caml is now self-contained within src/emit. I've not tested the generated Caml code but the SML seems to build fine. The directories: src/theoryML src/theoryOcaml src/emitScript have been replaced by src/emit/theories/ML src/emit/theories/Caml src/emit/theories
|
#
3faf4042 |
|
13-Jan-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add trace variables for controlling the pretty-printing of words and for guessing word lengths. The function guess_word_lengths has been renamed inst_word_lengths and output_words_as_dec is now remove_word_printer. Trace "word printing" controls reference wordsLib.word_pp_mode. 0 - default: values >= 0x10000 print in Hexadecimal, otherwise in Decimal 1 - Binary 2 - Octal 3 - Decimal 4 - Hexadecimal For example: - with_flag (wordsLib.word_pp_mode, 1) term_to_string ``32w:word5``; > val it = "0b100000w" : string Trace "guess word lengths" controls flag wordsLib.guessing_word_lengths. For example: - with_flag (wordsLib.guessing_word_lengths, true) Term `(7 >< 0) w`; <<HOL message: inventing new type variable names: 'a, 'b>> <<HOL message: assigning word length(s): 'b <- 8>> > val it = ``(7 >< 0) w`` : term
|
#
d8a63927 |
|
15-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_EQ_CONV to the_compset and signature.
|
#
8eeeebdd |
|
13-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some extra functions under EmitML e.g. toWord32 and fromString32. Made fcpLib.index_to_num more robust. It can now cope with sum types. Added Cases_word_value and Cases_on_word_value. These do case splitting on the numeric value of a word.
|
#
d4b1b2cc |
|
25-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Made some changes to the pretty-printing support for words. The functions "pp_word", "pp_word_bin" etc. have been replaced by "output_word_as", "output_word_as_bin" etc. The function "output_word_as" is more flexible and a custom printer is turned on by default when wordsLib is loaded. (Word literals with a value >= 0x10000 are printed in hex, otherwise they are printed as decimal.) Added "dont_guess_lengths" function, which undoes "guess_lengths".
|
#
6e25f443 |
|
21-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added wordsTheory.WORD_INDUCT. This can be used with wordsLib.Induct_word. Added WORD_DECIDE_TAC and made some changes to WORD_DECIDE (to handle terms with quantifiers). Made changes to SIZES_CONV for faster evaluation of ``dimword(:N)`` etc. (Was slow for large N.) Dropped wordsLib.WORD_GROUND_ss -- this is contained within srw_ss() and WORD_ss.
|
#
8496cf9c |
|
16-Jan-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a number of tools for working with words. The main additions are: WORD_ss: Does some basic simplification, evaluation and AC rewriting (over *, +, && and !!). For example, ``a * 3w + a`` -> ``4w * a`` and ``a && 3w !! a && 2w`` -> ``3w && a``. BIT_ss: For example, ``BIT n 3`` -> ``n IN {0; 1}``. WORD_MUL_LSL_ss: Converts multiplications to left-shifts e.g. ``2w * a`` -> ``a << 1``. WORD_BIT_EQ_ss: Can be used to establish bit-wise (in)equality e.g. ``a && ~a = 0w`` -> ``T``. Does not work with *, + etc. WORD_ARITH_EQ_ss: Can be used to establish arithmetic (in)equality e.g. ``~(b + 1w = b + 4294967295w:word32)`` -> ``T``. WORD_EXTRACT_ss: Simplification for shifts and bit extraction. "Simplifies" --, w2w, sw2sw, #>>, @@ etc. and expresses operations using ><, << and !!. WORD_DECIDE: A decision procedure. Will solve Boolean (bitwise) problems and some problems over <, <+ etc.
|
#
995bd661 |
|
01-Nov-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added parsing preferences for words (prefer_word and deprecate_word).
|
#
b2db99ef |
|
07-May-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some new theorems - mostly to do with word extraction.
|
#
90b87cf3 |
|
20-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a top-level function for turning on word length guessing i.e. it is invoked with val _ = wordsLib.guess_lengths() This ensures that existing post_process_term functionality isn't bypassed.
|
#
b1a5f678 |
|
19-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Post processing for word parsing is supported with the function: wordsLib.guess_word_lengths : term -> term This was requested by Joe Hurd. When possible, word lengths are guessed for the extract and concatenate functions. That is, ``(a >< b) w`` is given type ``: (a + 1 - b) word`` and ``(a: a word) @@ (b: b word)`` is given type ``: (a + b) word``. For example: - val _ = Parse.post_process_term := wordsLib.guess_word_lengths; - ``(3 >< 0) a @@ (7 >< 4) a @@ (16 >< 8) a``; <<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd, 'e, 'f>> <<HOL message: assigning word length(s): 'a <- 4, 'b <- 13, 'c <- 17, 'e <- 4 and 'f <- 9>> > val it = ``(3 >< 0) a @@ (7 >< 4) a @@ (16 >< 8) a`` : term The assignment message is controlled by the trace variable "notify word length guesses".
|
#
95b7103d |
|
02-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a rule for use with EmitML i.e. when emitting a definition "th" (containing word operations), you need: EmitML.DEFN (wordsLib.WORDS_EMIT_RULE th)
|
#
db890776 |
|
23-Jan-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Thanks to Michael's last check-in, index types are now directly supported by the parser/printer, so there is no need to introduce the "iN" type abbreviations. The function fcpLib.mk_index_type has been removed. * Users of the theory must delete all occurrences of "i" * e.g. ``:i32`` must change to ``:32``. There is now support for evaluation with non-standard word sizes e.g. - load "wordsLib"; > val it = () : unit - EVAL ``123w + 321w:56 word``; > val it = |- 123w + 321w = 444w : thm Non-standard word sizes will evaluate more slowly when first used. However, size theorems are then added to the compset, so subsequent evaluations will be quicker. There is no change with standard word sizes e.g. can still use ``:word32`` and - wordsTheory.dimword_32; > val it = |- dimword (:32) = 4294967296 : thm
|
#
9d26d3e8 |
|
08-Sep-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Decided to replace the word case tactics with ranged versions.
|
#
bea43d5f |
|
07-Sep-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added theorem word_1_n2w, and tactics Cases_on_word_ranged and Cases_word_ranged.
|
#
ccbf3be3 |
|
01-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixed signature file.
|
#
c4e9aa47 |
|
01-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Allow pretty-printing of words in different number bases.
|
#
f4affa25 |
|
04-Jan-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Renamed wordsLib.mk_word_type to wordsLib.mk_word_size to avoid the name clash with wordsSyntax.mk_word_type
|
#
70a7f15a |
|
01-Oct-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
* Added a theorem w2w, which makes proofs about w2w a little easier. * bitLib and machine_wordsLib have been dropped and wordsLib extended. * wordsLib now has a function mk_word_type, which adds a type abbreviation for a new word size. * Fixed Cases_on_word so that it does type instantiation. * Increased the number of word sizes provided by machine_wordsTheory. * Added a couple of simpset fragments (SIZES_ss and FCP_ss).
|
#
6752f613 |
|
23-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have added the word "Case" tactics to wordsLib. Also added some theorems - in particular, a few for reasoning about w2w and word_bits.
|
#
1d0debf0 |
|
14-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A new theory of words - based on an idea from John Harrison. This is now a unified theory of words - so there's no more need for the Functor or mkword.exe. The old library (n_bit) will eventually be dropped, so current users are advised to adopt the new library as soon as possible. NB. bitTheory is nearly identical to the old bitsTheory. The new representing type is finite Cartesian products e.g. :bool ** 'a is the type for words whose length is the size of the indexing type 'a. The function fcpLib.mk_index_type can be used to create the required index type. Most theorems from the old theory should be present (if I've missed any out then let me know). NB. A few theorems have changed name and some have been dropped (e.g. there is no longer a word_suc function). Some symbols have changed. This avoids complaints from the parser and should hopefully aid readability. old new two's comp. : ~ $- bitwise not : NOT ~ bitwise or : | !! bitwise and : & && bitwise xor : # ?? unsigned < : <. <+ unsigned <= : <=. <=+ unsigned > : >. >+ unsigned >= : >=. >=+ The bits and slice functions no longer map to :num - they now map from :bool ** 'a to :bool ** 'a. bits : WORD_BITS h l w (h -- l) w slice : WORD_SLICE h l w (h <> l) w The function w2w converts between words of different sizes (unsigned) and sw2sw is a signed (2's complement) word-word conversion. The library machine_wordsLib provides the types word4, word8 word16, word32 and word64. Ground term evaluation with EVAL should work here. Some operations (+, *) can be evaluated with alpha types e.g. EVAL ``6w + 4w``; <<HOL message: inventing new type variable names: 'a>> > val it = |- 6w + 4w = 10w : thm Subtraction only works when the word size is known e.g. EVAL ``6w:word8 - 4w``; > val it = |- 6w - 4w = 258w : thm An attempt to do evaluation with alpha types around will likely result in gibberish.
|