Add saturating word conversions and word duplication #118
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
Added both unsigned and signed *saturating* conversions from N and Z to
machine words, which rather than wrapping modulo 2^wordsize as the main
"word" and "iword" do, saturate at the extremal values of that size:
word_saturate =
|- word_saturate n =
if n > val word_UINT_MAX then word_UINT_MAX else word n
iword_saturate =
|- iword_saturate x =
if x < ival word_INT_MIN then word_INT_MIN
else if x > ival word_INT_MAX then word_INT_MAX
else iword x
Also added a natural "word_duplicate" operation, a kind of iterated
word_join inferring relative sizes and hence number of duplicates from
the types.
word_duplicate =
|- (word_duplicate:M word->N word) x =
word_of_bits {i | bit (i MOD dimindex (:M)) x
There are also a few elementary lemmas about it:
BIT_WORD_DUPLICATE =
|- !x i.
bit i (word_duplicate x) <=>
i < dimindex(:N) /\ bit (i MOD dimindex(:M)) x
VAL_WORD_DUPLICATE =
|- !x k.
dimindex(:N) <= k * dimindex(:M)
==> val (word_duplicate x) =
((2 EXP (k * dimindex(:M)) - 1) DIV (2 EXP dimindex(:M) - 1) *
val x) MOD
2 EXP dimindex(:N)
WORD_DUPLICATE =
|- !m k.
dimindex(:N) <= k * dimindex(:M)
==> word_duplicate (word m) =
word
((2 EXP (k * dimindex(:M)) - 1) DIV (2 EXP dimindex(:M) - 1) *
m MOD 2 EXP dimindex(:M))
WORD_DUPLICATE_DOUBLE =
|- !x. word_duplicate (word_join x x) = word_duplicate x
WORD_DUPLICATE_REFL =
|- !x. word_duplicate x = x
WORD_SUBWORD_DUPLICATE =
|- !x pos len.
pos MOD dimindex(:M) + len <= dimindex(:M) /\
pos + len <= dimindex(:N)
==> word_subword (word_duplicate x) (pos,len) =
word_subword x (pos MOD dimindex(:M),len)
The relevant conversions like BIT_WORD_CONV, SIMPLE_WORD_SUBWORD_CONV
and WORD_RED_CONV have all been updated to take these three new operations
into account.
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.
No description provided.