Theory Tagged_Packet

theory Tagged_Packet
imports Simple_Firewall.Simple_Packet Conntrack_State
begin

section‹Tagged Simple Packet›
  text‹Packet constants are prefixed with ‹p››

  text‹A packet tagged with the following phantom fields:
             conntrack connection state›

  text‹The idea to tag the connection state into the packet is sound.
       See @{file ‹../Semantics_Stateful.thy›}›

  record (overloaded) 'i tagged_packet = "'i::len simple_packet" +
                         p_tag_ctstate :: ctstate


  value "⦇ 
          p_iiface = ''eth1'', p_oiface = '''', 
          p_src = 0, p_dst = 0, 
          p_proto = TCP, p_sport = 0, p_dport = 0, 
          p_tcp_flags = {TCP_SYN},
          p_payload = ''arbitrary payload'',
          p_tag_ctstate = CT_New
         ⦈:: 32 tagged_packet"

  definition simple_packet_tag
    :: "ctstate ⇒ ('i::len, 'a) simple_packet_scheme ⇒ ('i::len, 'a) tagged_packet_scheme" where
    "simple_packet_tag ct_state p ≡
      ⦇p_iiface = p_iiface p, p_oiface = p_oiface p, p_src = p_src p, p_dst = p_dst p, p_proto = p_proto p, 
       p_sport = p_sport p, p_dport = p_dport p, p_tcp_flags = p_tcp_flags p, 
       p_payload = p_payload p,
       p_tag_ctstate = ct_state,
       … = simple_packet.more p⦈"

  definition tagged_packet_untag
    :: "('i::len, 'a) tagged_packet_scheme ⇒ ('i::len, 'a) simple_packet_scheme" where
    "tagged_packet_untag p ≡
      ⦇p_iiface = p_iiface p, p_oiface = p_oiface p, p_src = p_src p, p_dst = p_dst p, p_proto = p_proto p, 
       p_sport = p_sport p, p_dport = p_dport p, p_tcp_flags = p_tcp_flags p, 
       p_payload = p_payload p,
       … = tagged_packet.more p⦈"

  lemma "tagged_packet_untag (simple_packet_tag ct_state p) = p"
        "simple_packet_tag ct_state (tagged_packet_untag p) = p⦇p_tag_ctstate := ct_state⦈"
    apply(case_tac [!] p)
     by(simp add: tagged_packet_untag_def simple_packet_tag_def)+
    

end