Theory L4_Protocol

theory L4_Protocol
imports "../Common/Lib_Enum_toString" "HOL-Library.Word"
begin

section‹Transport Layer Protocols›
type_synonym primitive_protocol = "8 word"

definition "ICMP ≡ 1 :: 8 word"
definition "TCP ≡ 6 :: 8 word"
definition "UDP ≡ 17 :: 8 word"
context begin (*let's not pollute the namespace too much*)
qualified definition "SCTP ≡ 132  :: 8 word"
qualified definition "IGMP ≡ 2 :: 8 word"
qualified definition "GRE ≡ 47 :: 8 word"
qualified definition "ESP ≡ 50 :: 8 word"
qualified definition "AH ≡ 51 :: 8 word"
qualified definition "IPv6ICMP ≡ 58 :: 8 word"
end
(* turn http://www.iana.org/assignments/protocol-numbers/protocol-numbers.xhtml into a separate file or so? *)

datatype protocol = ProtoAny | Proto "primitive_protocol"

fun match_proto :: "protocol ⇒ primitive_protocol ⇒ bool" where
  "match_proto ProtoAny _ ⟷ True" |
  "match_proto (Proto (p)) p_p ⟷ p_p = p"

  fun simple_proto_conjunct :: "protocol ⇒ protocol ⇒ protocol option" where
    "simple_proto_conjunct ProtoAny proto = Some proto" |
    "simple_proto_conjunct proto ProtoAny = Some proto" |
    "simple_proto_conjunct (Proto p1) (Proto p2) = (if p1 = p2 then Some (Proto p1) else None)"
  lemma simple_proto_conjunct_asimp[simp]: "simple_proto_conjunct proto ProtoAny = Some proto"
    by(cases proto) simp_all

  lemma simple_proto_conjunct_correct: "match_proto p1 pkt ∧ match_proto p2 pkt ⟷ 
    (case simple_proto_conjunct p1 p2 of None ⇒ False | Some proto ⇒ match_proto proto pkt)"
    apply(cases p1)
     apply(simp_all)
    apply(cases p2)
     apply(simp_all)
    done

  lemma simple_proto_conjunct_Some: "simple_proto_conjunct p1 p2 = Some proto ⟹ 
    match_proto proto pkt ⟷ match_proto p1 pkt ∧ match_proto p2 pkt"
    using simple_proto_conjunct_correct by simp
  lemma simple_proto_conjunct_None: "simple_proto_conjunct p1 p2 = None ⟹ 
    ¬ (match_proto p1 pkt ∧ match_proto p2 pkt)"
    using simple_proto_conjunct_correct by simp

  lemma conjunctProtoD:
    "simple_proto_conjunct a (Proto b) = Some x ⟹ x = Proto b ∧ (a = ProtoAny ∨ a = Proto b)"
  by(cases a) (simp_all split: if_splits)
  lemma conjunctProtoD2:
    "simple_proto_conjunct (Proto b) a = Some x ⟹ x = Proto b ∧ (a = ProtoAny ∨ a = Proto b)"
  by(cases a) (simp_all split: if_splits)

  text‹Originally, there was a @{typ nat} in the protocol definition, allowing infinitely many protocols 
        This was intended behavior. We want to prevent things such as @{term "¬TCP = UDP"}.
        So be careful with what you prove...›
  lemma primitive_protocol_Ex_neq: "p = Proto pi ⟹ ∃p'. p' ≠ pi" for pi
  proof
  	show "pi + 1 ≠ pi" by simp
  qed
  lemma protocol_Ex_neq: "∃p'. Proto p' ≠ p"
    by(cases p) (simp_all add: primitive_protocol_Ex_neq)

section‹TCP flags›
  datatype tcp_flag = TCP_SYN | TCP_ACK | TCP_FIN | TCP_RST | TCP_URG | TCP_PSH (*| TCP_ALL | TCP_NONE*)

  lemma UNIV_tcp_flag: "UNIV = {TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST, TCP_URG, TCP_PSH}" using tcp_flag.exhaust by auto 
  instance tcp_flag :: finite
  proof
    from UNIV_tcp_flag show "finite (UNIV:: tcp_flag set)" using finite.simps by auto 
  qed
  instantiation "tcp_flag" :: enum
  begin
    definition "enum_tcp_flag = [TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST, TCP_URG, TCP_PSH]"
  
    definition "enum_all_tcp_flag P ⟷ P TCP_SYN ∧ P TCP_ACK ∧ P TCP_FIN ∧ P TCP_RST ∧ P TCP_URG ∧ P TCP_PSH"
    
    definition "enum_ex_tcp_flag P ⟷ P TCP_SYN ∨ P TCP_ACK ∨ P TCP_FIN ∨ P TCP_RST ∨ P TCP_URG ∨ P TCP_PSH"
  instance proof
    show "UNIV = set (enum_class.enum :: tcp_flag list)"
      by(simp add: UNIV_tcp_flag enum_tcp_flag_def)
    next
    show "distinct (enum_class.enum :: tcp_flag list)"
      by(simp add: enum_tcp_flag_def)
    next
    show "⋀P. (enum_class.enum_all :: (tcp_flag ⇒ bool) ⇒ bool) P = Ball UNIV P"
      by(simp add: UNIV_tcp_flag enum_all_tcp_flag_def)
    next
    show "⋀P. (enum_class.enum_ex :: (tcp_flag ⇒ bool) ⇒ bool) P = Bex UNIV P"
      by(simp add: UNIV_tcp_flag enum_ex_tcp_flag_def)
  qed
  end

subsection‹TCP Flags to String›
  fun tcp_flag_toString :: "tcp_flag ⇒ string" where
    "tcp_flag_toString TCP_SYN = ''TCP_SYN''" |
    "tcp_flag_toString TCP_ACK = ''TCP_ACK''" |
    "tcp_flag_toString TCP_FIN = ''TCP_FIN''" |
    "tcp_flag_toString TCP_RST = ''TCP_RST''" |
    "tcp_flag_toString TCP_URG = ''TCP_URG''" |
    "tcp_flag_toString TCP_PSH = ''TCP_PSH''"


  definition ipt_tcp_flags_toString :: "tcp_flag set ⇒ char list" where
    "ipt_tcp_flags_toString flags ≡ list_toString tcp_flag_toString (enum_set_to_list flags)"

  lemma "ipt_tcp_flags_toString {TCP_SYN,TCP_SYN,TCP_ACK} = ''[TCP_SYN, TCP_ACK]''" by eval


end