Theory SimpleFw_toString
section‹Simple Firewall toString Functions›
theory SimpleFw_toString
imports "Primitives/Primitives_toString"
SimpleFw_Syntax
begin
fun simple_action_toString :: "simple_action ⇒ string" where
"simple_action_toString Accept = ''ACCEPT''" |
"simple_action_toString Drop = ''DROP''"
fun simple_rule_ipv4_toString :: "32 simple_rule ⇒ string" where
"simple_rule_ipv4_toString (SimpleRule ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p, sports=sps, dports=dps ⦈ a) =
simple_action_toString a @ '' '' @
protocol_toString p @ '' -- '' @
ipv4_cidr_toString sip @ '' '' @
ipv4_cidr_toString dip @ '' '' @
iface_toString ''in: '' iif @ '' '' @
iface_toString ''out: '' oif @ '' '' @
ports_toString ''sports: '' sps @ '' '' @
ports_toString ''dports: '' dps"
fun simple_rule_ipv6_toString :: "128 simple_rule ⇒ string" where
"simple_rule_ipv6_toString
(SimpleRule ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p, sports=sps, dports=dps ⦈ a) =
simple_action_toString a @ '' '' @
protocol_toString p @ '' -- '' @
ipv6_cidr_toString sip @ '' '' @
ipv6_cidr_toString dip @ '' '' @
iface_toString ''in: '' iif @ '' '' @
iface_toString ''out: '' oif @ '' '' @
ports_toString ''sports: '' sps @ '' '' @
ports_toString ''dports: '' dps"
fun simple_rule_iptables_save_toString :: "string ⇒ 32 simple_rule ⇒ string" where
"simple_rule_iptables_save_toString chain (SimpleRule ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p, sports=sps, dports=dps ⦈ a) =
''-A ''@chain@iface_toString '' -i '' iif @
iface_toString '' -o '' oif @
ipv4_cidr_opt_toString '' -s '' sip @
ipv4_cidr_opt_toString '' -d '' dip @
protocol_opt_toString '' -p '' p @
ports_toString '' --sport '' sps @
ports_toString '' --dport '' dps @
'' -j '' @ simple_action_toString a"
end