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›
datatype ipt_l4_ports = L4Ports primitive_protocol raw_ports


end