Abstract
This entry contains an extension to the Isabelle library for
fixed-width machine words. In particular, the entry adds quickcheck setup
for words, printing as hexadecimals, additional operations, reasoning
about alignment, signed words, enumerations of words, normalisation of
word numerals, and an extensive library of properties about generic
fixed-width words, as well as an instantiation of many of these to the
commonly used 32 and 64-bit bases.
License
Contributions
Multiple contributions and maintainance by Florian Haftmann since 2016
Sep 2024
Some proofs tidied by Lawrence C. Paulson
Topics
Session Word_Lib
- Enumeration
- Even_More_List
- Legacy_Aliases
- More_Arithmetic
- More_Divides
- More_Misc
- More_Sublist
- Strict_part_mono
- Bit_Comprehension
- More_Int
- More_Bit_Ring
- More_Word
- Bit_Shifts_Infix_Syntax
- Aligned
- Next_and_Prev
- Signed_Division_Word
- Many_More
- Singleton_Bit_Shifts
- Typedef_Morphisms
- Most_significant_bit
- Generic_set_bit
- Least_significant_bit
- Rsplit
- Reversed_Bit_Lists
- Bin_sign
- Bitwise
- Bit_Comprehension_Int
- Signed_Words
- Bitwise_Signed
- Enumeration_Word
- Hex_Words
- Norm_Words
- Syntax_Bundles
- Sgn_Abs
- Type_Syntax
- Word_EqI
- Boolean_Inequalities
- Word_Lemmas
- Word_8
- Word_16
- Word_Syntax
- Word_Names
- More_Word_Operations
- Word_32
- Word_Lib_Sumo
- Machine_Word_32_Basics
- Machine_Word_32
- Word_64
- Machine_Word_64_Basics
- Machine_Word_64
- Guide
- Examples
Used by
- A Formal Model of IEEE Floating Point Arithmetic
- Native Word
- IP Addresses
- A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
- COMPLX: A Verification Framework for Concurrent Imperative Programs
- CakeML
- Interval Arithmetic on 32-bit Words
- X86 instruction semantics and basic block symbolic execution
- A Formal CHERI-C Memory Model
- AutoCorres2
- Schönhage-Strassen Multiplication