Theory Ports
theory Ports
imports
"HOL-Library.Word"
"../Common/WordInterval_Lists"
L4_Protocol_Flags
begin
section‹Ports (layer 4)›
text‹E.g. source and destination ports for TCP/UDP›
text‹list of (start, end) port ranges›
type_synonym raw_ports = "(16 word × 16 word) list"
fun ports_to_set :: "raw_ports ⇒ (16 word) set" where
"ports_to_set [] = {}" |
"ports_to_set ((s,e)#ps) = {s..e} ∪ ports_to_set ps"
lemma ports_to_set: "ports_to_set pts = ⋃ {{s..e} | s e . (s,e) ∈ set pts}"
proof(induction pts)
case Nil thus ?case by simp
next
case (Cons p pts) thus ?case by(cases p, simp, blast)
qed
text‹We can reuse the wordinterval theory to reason about ports›
lemma ports_to_set_wordinterval: "ports_to_set ps = wordinterval_to_set (l2wi ps)"
by(induction ps rule: l2wi.induct) (auto)
text‹inverting a raw listing of ports›
definition "raw_ports_invert" :: "raw_ports ⇒ raw_ports" where
"raw_ports_invert ps = wi2l (wordinterval_invert (l2wi ps))"
lemma raw_ports_invert: "ports_to_set (raw_ports_invert ps) = - ports_to_set ps"
by(auto simp add: raw_ports_invert_def l2wi_wi2l ports_to_set_wordinterval)
text‹A port always belongs to a protocol! We must not lose this information.
You should never use @{typ raw_ports} directly›