Email Gateway (Aug 18 2022 at 11:26): Email Gateway (Aug 18 2022 at 11:26):From: Sascha Boehme <boehmes@in.tum.de>
Hello,
while studying the current (most recent) Word library, I didn't find a function which extracts a part from a word. I started to implement a function on my own, but I'm sure there must be a better version (especially wrt. to doing proofs on it).
Here is my solution:
definition word_extract :: "'a::len0 word => int => int => 'b::len word"
where "word_extract w from to = (of_bl o rev o drop (nat from) o take (nat to) o rev o to_bl) w"
I'm grateful for any hints how to improve this.
Regards,
Sascha
Email Gateway (Aug 18 2022 at 11:27):From: John Matthews <matthews@galois.com>
Hi Sascha,
Here is the bit-segment extraction operator I've been using:
text {* Bit segment extraction operator: Given lb, mb :: int, where
lb = the least significant bit to extract, and mb = the most significant
bit to extract, then
@{term "(sliceLH lb mb w)"} extracts
bit segment [mb:lb] from bitvector w (assuming the result bitwidth
type @{typ 'b} is large enough to hold it). *}
definition
sliceLH :: "nat \<Rightarrow> nat \<Rightarrow> 'a::len word
\<Rightarrow> 'b::len word" where
"sliceLH lb mb w \<equiv> ucast ((w AND mask (mb + 1)) >> lb)"
Hope this helps,
-john
Email Gateway (Aug 18 2022 at 11:27):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Sascha Boehme wrote:
If that is your current definition, John's version is probably what you want
(reasoning about mask and shift is easier than type conversions).
There is also the built-in "slice :: nat => 'a word => 'b word". The nat
says from where to slice, the target type length says how much to slice.
Cheers,
Gerwin
Last updated: May 03 2024 at 04:19 UTC