section\<open>Example: Executing an Iptables ruleset in Isabelle\<close>
theory Executable_Iptables
  imports Alternative_Semantics "Primitive_Matchers/Common_Primitive_Matcher"
    (* arbitrarily: *) "Examples/SQRL_Shorewall/SQRL_2015_nospoof"
begin
text\<open>This is just a little example theory that demonstrates that one can directly
  execute a loaded ruleset on an inductively defined semantics.
  Unfortunately, doing so is only possible with the \textbf{values} command and we cannot
  extract or document its result automatically.
  This makes for an interesting toy example, but nothing more.\<close>

code_pred (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as compute_iptables_bigstep_r) iptables_bigstep_r .
    print_theorems

definition "some_p \<equiv> \<lparr>p_iiface = ''lmd'', p_oiface = ''lup'',
           p_src = ipv4addr_of_dotdecimal (10,13,42,130), p_dst= ipv4addr_of_dotdecimal (80,237,132,143),
           p_proto=TCP, p_sport=51065, p_dport=80, p_tcp_flags = {},
           p_payload = '''', p_tag_ctstate = CT_New\<rparr>"

(*values "{t. (\<lambda>_. None),(\<lambda>m p. the (ternary_to_bool (common_matcher m p))),some_p\<turnstile> \<langle>[],Undecided\<rangle> \<Rightarrow> t}"
  This won't work. I have no idea if one somehow can make it work\<dots> *)
term "map_of_string_ipv4 filter_fw1"
definition "entry_rs \<equiv> [Rule MatchAny (Call ''FORWARD''), Rule MatchAny filter_fw1_FORWARD_default_policy]"

value [code] "Predicate.the (compute_iptables_bigstep_r
  (map_of_string_ipv4 filter_fw1)
  (\<lambda>m p. the (ternary_to_bool (common_matcher m p)))
  some_p
  entry_rs)"



end