Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: IP Addresses


view this post on Zulip Email Gateway (Aug 22 2022 at 13:29):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
IP Addresses
by Cornelius Diekmann, Julius Michaelis and Lars Hupel

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.

[https://www.isa-afp.org/entries/IP_Addresses.shtml]

Enjoy!
Gerwin


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


Last updated: Mar 28 2024 at 08:18 UTC