Enhance word automation procedures WORD_ARITH and BITBLAST_RULE #110
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This makes the word decision procedures WORD_ARITH/WORD_ARITH_TAC
and BITBLAST_RULE more capable in several ways:
* Both BITBLAST_RULE and WORD_ARITH make more systematic reduction
of word ground expressions internally.
* BITBLAST_RULE now transforms "val(x) MOD n" and "val(x) DIV n"
where n is (or can be transformed into) a power of 2, into
bitwise equivalents so that the core procedure can handle it.
* WORD_ARITH also expands "val(word n)" into "n MOD ...." after
all the casewise "linear" expansions have been tried, giving
it some capacity to handle multiplication by constants.
* The underlying integer arithmetic procedure INT_ARITH has been
enhanced so that it is never worse to use it than the natural
number version, because it will infer nonnegativity of quotients
introduced by div/rem elimination where possible.
Here are some word examples that work now but didn't before:
WORD_ARITH
`!m n. m < 4096 /\ n <= 511
==> word_ule (word_add (word_mul (word n) (word 0x00001000)) (word m))
(word 0x0000000001FFFFFF:int64)`;;
BITBLAST_RULE
`word_and x (word 256):int64 = word 0 <=> val x MOD 512 < 256`;;
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This makes the word decision procedures WORD_ARITH/WORD_ARITH_TAC and BITBLAST_RULE more capable in several ways:
Both BITBLAST_RULE and WORD_ARITH make more systematic reduction of word ground expressions internally.
BITBLAST_RULE now transforms "val(x) MOD n" and "val(x) DIV n" where n is (or can be transformed into) a power of 2, into bitwise equivalents so that the core procedure can handle it.
WORD_ARITH also expands "val(word n)" into "n MOD ...." after all the casewise "linear" expansions have been tried, giving it some capacity to handle multiplication by constants.
The underlying integer arithmetic procedure INT_ARITH has been enhanced so that it is never worse to use it than the natural number version, because it will infer nonnegativity of quotients introduced by div/rem elimination where possible.
Here are some word examples that work now but didn't before:
WORD_ARITH
!m n. m < 4096 /\ n <= 511 ==> word_ule (word_add (word_mul (word n) (word 0x00001000)) (word m)) (word 0x0000000001FFFFFF:int64);;BITBLAST_RULE
word_and x (word 256):int64 = word 0 <=> val x MOD 512 < 256;;