Theory Example_Semantics

theory Example_Semantics
imports Call_Return_Unfolding "Primitive_Matchers/Common_Primitive_Matcher"
begin


section‹Examples Big Step Semantics›
text‹We use a primitive matcher which always applies. We don't care about matching in this example.›
  fun applies_Yes :: "('a, 'p) matcher" where
  "applies_Yes m p = True" 
  lemma[simp]: "Semantics.matches applies_Yes MatchAny p" by simp
  lemma[simp]: "Semantics.matches applies_Yes (Match e) p" by simp

  definition "m=Match (Src (IpAddr (0::ipv4addr)))"
  lemma[simp]: "Semantics.matches applies_Yes m p" by (simp add: m_def)

  lemma "[''FORWARD'' ↦ [(Rule m Log), (Rule m Accept), (Rule m Drop)]],applies_Yes,p⊢
      ⟨[Rule MatchAny (Call ''FORWARD'')], Undecided⟩ ⇒ (Decision FinalAllow)"
  apply(rule call_result)
    apply(auto)
  apply(rule seq_cons)
   apply(auto intro:Semantics.log)
  apply(rule seq_cons)
   apply(auto intro: Semantics.accept)
  apply(rule Semantics.decision)
  done
  
  lemma "[''FORWARD'' ↦ [(Rule m Log), (Rule m (Call ''foo'')), (Rule m Accept)],
          ''foo'' ↦ [(Rule m Log), (Rule m Return)]],applies_Yes,p⊢
      ⟨[Rule MatchAny (Call ''FORWARD'')], Undecided⟩ ⇒ (Decision FinalAllow)"
  apply(rule call_result)
    apply(auto)
  apply(rule seq_cons)
   apply(auto intro: Semantics.log)
  apply(rule seq_cons)
   apply(rule Semantics.call_return[where rs⇩1="[Rule m Log]" and rs⇩2="[]"])
      apply(simp)+
   apply(auto intro: Semantics.log)
  apply(auto intro: Semantics.accept)
  done
  
  lemma "[''FORWARD'' ↦ [Rule m (Call ''foo''), Rule m Drop], ''foo'' ↦ []],applies_Yes,p⊢
            ⟨[Rule MatchAny (Call ''FORWARD'')], Undecided⟩ ⇒ (Decision FinalDeny)"
  apply(rule call_result)
    apply(auto)
  apply(rule Semantics.seq_cons)
   apply(rule Semantics.call_result)
     apply(auto)
   apply(rule Semantics.skip)
  apply(auto intro: deny)
  done

  lemma "((λrs. process_call [''FORWARD'' ↦ [Rule m (Call ''foo''), Rule m Drop], ''foo'' ↦ []] rs)^^2)
                    [Rule MatchAny (Call ''FORWARD'')]
         = [Rule (MatchAnd MatchAny m) Drop]" by eval

  hide_const m
  
  definition "pkt=⦇p_iiface=''+'', p_oiface=''+'', p_src=0, p_dst=0,
                   p_proto=TCP, p_sport=0, p_dport=0, p_tcp_flags = {TCP_SYN},
                   p_payload='''',p_tag_ctstate= CT_New⦈"

  text‹We tune the primitive matcher to support everything we need in the example. Note that the undefined cases cannot be handled with these exact semantics!›
  fun applies_exampleMatchExact :: "(32 common_primitive, 32 tagged_packet) matcher" where
  "applies_exampleMatchExact (Src (IpAddr addr)) p ⟷ p_src p = addr" |
  "applies_exampleMatchExact (Dst (IpAddr addr)) p ⟷ p_dst p = addr" |
  "applies_exampleMatchExact (Prot ProtoAny) p ⟷ True" |
  "applies_exampleMatchExact (Prot (Proto pr)) p ⟷ p_proto p = pr"
  (* not exhaustive, only an example!!*)

  lemma "[''FORWARD'' ↦ [ Rule (MatchAnd (Match (Src (IpAddr 0))) (Match (Dst (IpAddr 0)))) Reject, 
                          Rule (Match (Dst (IpAddr 0))) Log, 
                          Rule (Match (Prot (Proto TCP))) Accept,
                          Rule (Match (Prot (Proto TCP))) Drop]
         ],applies_exampleMatchExact, pkt⦇p_src:=(ipv4addr_of_dotdecimal (1,2,3,4)), p_dst:=(ipv4addr_of_dotdecimal (0,0,0,0))⦈⊢
            ⟨[Rule MatchAny (Call ''FORWARD'')], Undecided⟩ ⇒ (Decision FinalAllow)"
  apply(rule call_result)
    apply(auto)
  apply(rule Semantics.seq_cons)
   apply(auto intro: Semantics.nomatch simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)
  apply(rule Semantics.seq_cons)
   apply(auto intro: Semantics.log simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)
  apply(rule Semantics.seq_cons)
   apply(auto simp add: pkt_def intro: Semantics.accept)
  apply(auto intro: Semantics.decision)
  done

end