### Abstract

This entry contains a definition of IP addresses and a library to work with them. Generic IP addresses are modeled as machine words of arbitrary length. Derived from this generic definition, IPv4 addresses are 32bit machine words, IPv6 addresses are 128bit words. Additionally, IPv4 addresses can be represented in dot-decimal notation and IPv6 addresses in (compressed) colon-separated notation. We support toString functions and parsers for both notations. Sets of IP addresses can be represented with a netmask (e.g. 192.168.0.0/255.255.0.0) or in CIDR notation (e.g. 192.168.0.0/16). To provide executable code for set operations on IP address ranges, the library includes a datatype to work on arbitrary intervals of machine words.

### License

BSD License

### Topics

- Computer science/Networks

### Session IP_Addresses

- NumberWang_IPv4
- NumberWang_IPv6
- WordInterval
- Hs_Compat
- IP_Address
- IPv4
- IPv6
- Prefix_Match
- CIDR_Split
- WordInterval_Sorted
- IP_Address_Parser
- Lib_Numbers_toString
- Lib_Word_toString
- Lib_List_toString
- IP_Address_toString
- Prefix_Match_toString

### Depends on

- Automatic Data Refinement
- Finite Machine Word Library

### Used by

- Simple Firewall

### Auto-related entries

- Tree Automata

## Cite

×

IP_Addresses-AFP

    @article{IP_Addresses-AFP,
      author  = {Cornelius Diekmann and Julius Michaelis and Lars Hupel},
      title   = {IP Addresses},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/IP_Addresses.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 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Jun 28, 2016 : Isabelle2016