### 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

BSD License

### Topics

- Computer science/Data structures

### Session Word_Lib

- Enumeration
- Even_More_List
- Legacy_Aliases
- More_Arithmetic
- More_Divides
- More_Misc
- More_Sublist
- More_Bit_Ring
- More_Word
- Strict_part_mono
- Bit_Shifts_Infix_Syntax
- Most_significant_bit
- Least_significant_bit
- Generic_set_bit
- Bit_Comprehension
- Bits_Int
- Aligned
- Next_and_Prev
- Signed_Division_Word
- Many_More
- Singleton_Bit_Shifts
- Typedef_Morphisms
- Reversed_Bit_Lists
- Bitwise
- Bit_Comprehension_Int
- Signed_Words
- Bitwise_Signed
- Enumeration_Word
- Hex_Words
- Norm_Words
- Rsplit
- 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

- Schönhage-Strassen Multiplication
- A Formal CHERI-C Memory Model
- X86 instruction semantics and basic block symbolic execution
- Interval Arithmetic on 32-bit Words
- CakeML
- COMPLX: A Verification Framework for Concurrent Imperative Programs
- A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
- IP Addresses
- Native Word
- A Formal Model of IEEE Floating Point Arithmetic

## Cite

×

Word_Lib-AFP

    @article{Word_Lib-AFP,
      author  = {Joel Beeren and Matthew Fernandez and Xin Gao and Gerwin Klein and Rafal Kolanski and Japheth Lim and Corey Lewis and Daniel Matichuk and Thomas Sewell},
      title   = {Finite Machine Word Library},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Word_Lib.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Jun 9, 2016 : Isabelle2016