-
- 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 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]"
-
- values "{t.
- (map_of_string_ipv4 filter_fw1),(\<lambda>m p. the (ternary_to_bool (common_matcher m p))),some_p \<turnstile>
- entry_rs \<Rightarrow>\<^sub>r t}"
-
-
-
- end
-