@@ 0,0 1,477 @@
+let Genode = env:DHALL_GENODE
+
+let Prelude = Genode.Prelude
+
+let XML = Prelude.XML
+
+let boolAttr =
+ λ(x : Optional Bool) →
+ merge
+ { Some = λ(x : Bool) → Some (if x then "yes" else "no")
+ , None = None Text
+ }
+ x
+
+let naturalAttr =
+ λ(x : Optional Natural) →
+ merge
+ { Some = λ(x : Natural) → Some (Natural/show x), None = None Text }
+ x
+
+let mergeAttributes =
+ λ(attrs : Prelude.Map.Type Text (Optional Text)) →
+ Prelude.List.fold
+ (Prelude.Map.Entry Text (Optional Text))
+ attrs
+ (Prelude.Map.Type Text Text)
+ ( λ(entry : Prelude.Map.Entry Text (Optional Text)) →
+ λ(map : Prelude.Map.Type Text Text) →
+ merge
+ { Some =
+ λ(mapValue : Text) →
+ map # [ { mapKey = entry.mapKey, mapValue } ]
+ , None = map
+ }
+ entry.mapValue
+ )
+ (Prelude.Map.empty Text Text)
+
+let Init = Genode.Init
+
+let Seconds = Natural
+
+let DomainName = Text
+
+let SessionLabel = Text
+
+let Ipv4AddressPrefix = Text
+
+let Ipv4Address = Text
+
+let Port = Natural
+
+let L2Rule =
+ let L2Rule/Type = { dst : Ipv4AddressPrefix, domain : DomainName }
+
+ in { Type = L2Rule/Type
+ , toXML =
+ λ(name : Text) →
+ λ(rule : L2Rule/Type) →
+ XML.leaf { name, attributes = toMap rule }
+ }
+
+let L3Rule =
+ let L3Rule/Permit = { port : Port, domain : DomainName }
+
+ let L3Rule/PermitAny = { domain : DomainName }
+
+ let L3Rule/Type =
+ { dst : Ipv4AddressPrefix
+ , permit : List L3Rule/Permit
+ , permitAny : List L3Rule/PermitAny
+ }
+
+ in { Type = L3Rule/Type
+ , default =
+ { permit = [] : List L3Rule/Permit
+ , permitAny = [] : List L3Rule/PermitAny
+ }
+ , toXML =
+ λ(name : Text) →
+ λ(rule : Optional L3Rule/Type) →
+ merge
+ { Some =
+ λ(rule : L3Rule/Type) →
+ [ XML.element
+ { name
+ , attributes = toMap { dst = rule.dst }
+ , content =
+ Prelude.List.map
+ L3Rule/Permit
+ XML.Type
+ ( λ(p : L3Rule/Permit) →
+ XML.leaf
+ { name = "permit"
+ , attributes = toMap
+ { port = Natural/show p.port
+ , domain = p.domain
+ }
+ }
+ )
+ rule.permit
+ # Prelude.List.map
+ L3Rule/PermitAny
+ XML.Type
+ ( λ(p : L3Rule/PermitAny) →
+ XML.leaf
+ { name = "permit-any"
+ , attributes = toMap
+ { domain = p.domain }
+ }
+ )
+ rule.permitAny
+ }
+ ]
+ , None = [] : List XML.Type
+ }
+ rule
+ }
+
+let L3ForwardRule =
+ let L3ForwardRule/Type =
+ { port : Port
+ , domain : DomainName
+ , to : Ipv4Address
+ , to_port : Port
+ }
+
+ in { Type = L3ForwardRule/Type
+ , toXML =
+ λ(name : Text) →
+ λ(rule : Optional L3ForwardRule/Type) →
+ merge
+ { Some =
+ λ(rule : L3ForwardRule/Type) →
+ [ XML.leaf
+ { name
+ , attributes = toMap
+ { port = Natural/show rule.port
+ , domain = rule.domain
+ , to = rule.to
+ , to_port = Natural/show rule.to_port
+ }
+ }
+ ]
+ , None = [] : List XML.Type
+ }
+ rule
+ }
+
+let Settings =
+ let Settings/Type =
+ { max_packets_per_signal : Optional Natural
+ , verbose : Optional Bool
+ , verbose_packets : Optional Bool
+ , verbose_packet_drop : Optional Bool
+ , verbose_domain_state : Optional Bool
+ , dhcp_discover_timeout_sec : Optional Seconds
+ , dhcp_request_timeout_sec : Optional Seconds
+ , dhcp_offer_timeout_sec : Optional Seconds
+ , udp_idle_timeout_sec : Optional Seconds
+ , tcp_idle_timeout_sec : Optional Seconds
+ , icmp_idle_timeout_sec : Optional Seconds
+ , tcp_max_segm_lifetime_sec : Optional Seconds
+ , icmp_echo_server : Optional Bool
+ }
+
+ in { Type = Settings/Type
+ , default =
+ { max_packets_per_signal = None Natural
+ , verbose = None Bool
+ , verbose_packets = None Bool
+ , verbose_packet_drop = None Bool
+ , verbose_domain_state = None Bool
+ , dhcp_discover_timeout_sec = None Seconds
+ , dhcp_request_timeout_sec = None Seconds
+ , dhcp_offer_timeout_sec = None Seconds
+ , udp_idle_timeout_sec = None Seconds
+ , tcp_idle_timeout_sec = None Seconds
+ , icmp_idle_timeout_sec = None Seconds
+ , tcp_max_segm_lifetime_sec = None Seconds
+ , icmp_echo_server = None Bool
+ }
+ , toAttributes =
+ λ(s : Settings/Type) →
+ mergeAttributes
+ ( toMap
+ { max_packets_per_signal =
+ naturalAttr s.max_packets_per_signal
+ , verbose = boolAttr s.verbose
+ , verbose_packets = boolAttr s.verbose_packets
+ , verbose_packet_drop = boolAttr s.verbose_packet_drop
+ , verbose_domain_state = boolAttr s.verbose_domain_state
+ , dhcp_discover_timeout_sec =
+ naturalAttr s.dhcp_discover_timeout_sec
+ , dhcp_request_timeout_sec =
+ naturalAttr s.dhcp_request_timeout_sec
+ , dhcp_offer_timeout_sec =
+ naturalAttr s.dhcp_offer_timeout_sec
+ , udp_idle_timeout_sec =
+ naturalAttr s.udp_idle_timeout_sec
+ , tcp_idle_timeout_sec =
+ naturalAttr s.tcp_idle_timeout_sec
+ , icmp_idle_timeout_sec =
+ naturalAttr s.icmp_idle_timeout_sec
+ , tcp_max_segm_lifetime_sec =
+ naturalAttr s.tcp_max_segm_lifetime_sec
+ , icmp_echo_server = boolAttr s.icmp_echo_server
+ }
+ )
+ }
+
+let Report =
+ let Report/Type =
+ { config : Optional Bool
+ , config_triggers : Optional Bool
+ , bytes : Optional Bool
+ , stats : Optional Bool
+ , link_state : Optional Bool
+ , link_state_triggers : Optional Bool
+ , quota : Optional Bool
+ , interval_sec : Optional Seconds
+ }
+
+ in { Type = Report/Type
+ , default =
+ { config = None Bool
+ , config_triggers = None Bool
+ , bytes = None Bool
+ , stats = None Bool
+ , link_state = None Bool
+ , link_state_triggers = None Bool
+ , quota = None Bool
+ , interval_sec = None Seconds
+ }
+ : Report/Type
+ , toXML =
+ λ(x : Report/Type) →
+ XML.leaf
+ { name = "report"
+ , attributes =
+ mergeAttributes
+ ( toMap
+ { config = boolAttr x.config
+ , config_triggers = boolAttr x.config_triggers
+ , bytes = boolAttr x.bytes
+ , stats = boolAttr x.stats
+ , link_state = boolAttr x.link_state
+ , link_state_triggers =
+ boolAttr x.link_state_triggers
+ , quota = boolAttr x.quota
+ , interval_sec = naturalAttr x.interval_sec
+ }
+ )
+ }
+ }
+
+let Uplink =
+ let Uplink/Type = { label : SessionLabel, domain : DomainName }
+
+ in { Type = Uplink/Type
+ , toXML =
+ λ(x : Uplink/Type) →
+ XML.leaf { name = "uplink", attributes = toMap x }
+ }
+
+let Nat =
+ let Nat/Type =
+ { domain : DomainName
+ , icmp-ids : Natural
+ , tcp-ports : Natural
+ , udp-ports : Natural
+ }
+
+ in { Type = Nat/Type
+ , default = { icmp-ids = 0, tcp-ports = 0, udp-ports = 0 }
+ , toXML =
+ λ(x : Nat/Type) →
+ XML.leaf
+ { name = "nat"
+ , attributes = toMap
+ { domain = x.domain
+ , icmp-ids = Natural/show x.icmp-ids
+ , tcp-ports = Natural/show x.tcp-ports
+ , udp-ports = Natural/show x.udp-ports
+ }
+ }
+ }
+
+let DhcpServer =
+ let DhcpServer/Type =
+ { ip_first : Optional Ipv4Address
+ , ip_last : Optional Ipv4Address
+ , ip_lease_time_sec : Optional Seconds
+ , dns_server : Optional Ipv4Address
+ , dns_server_from : Optional DomainName
+ }
+
+ in { Type = DhcpServer/Type
+ , default =
+ { ip_first = None Ipv4Address
+ , ip_last = None Ipv4Address
+ , ip_lease_time_sec = None Seconds
+ , dns_server = None Ipv4Address
+ , dns_server_from = None DomainName
+ }
+ , toXML =
+ λ(x : DhcpServer/Type) →
+ XML.leaf
+ { name = "dhcp-server"
+ , attributes =
+ mergeAttributes
+ ( toMap
+ ( x
+ with ip_lease_time_sec =
+ naturalAttr x.ip_lease_time_sec
+ )
+ )
+ }
+ }
+
+let Domain =
+ let Domain/Type =
+ { settings :
+ { name : DomainName
+ , interface : Optional Ipv4AddressPrefix
+ , gateway : Optional Ipv4Address
+ , verbose_packets : Optional Bool
+ , verbose_packet_drop : Optional Bool
+ , icmp_echo_server : Optional Bool
+ }
+ , ip : List L2Rule.Type
+ , icmp : List L2Rule.Type
+ , nat : List Nat.Type
+ , dhcpServer : List DhcpServer.Type
+ , tcp : Optional L3Rule.Type
+ , udp : Optional L3Rule.Type
+ , tcpForward : Optional L3ForwardRule.Type
+ , udpForward : Optional L3ForwardRule.Type
+ }
+
+ in { Type = Domain/Type
+ , default =
+ { settings =
+ { interface = None Ipv4AddressPrefix
+ , gateway = None Ipv4Address
+ , verbose_packets = None Bool
+ , verbose_packet_drop = None Bool
+ , icmp_echo_server = None Bool
+ }
+ , ip = [] : List L2Rule.Type
+ , icmp = [] : List L2Rule.Type
+ , nat = [] : List Nat.Type
+ , dhcpServer = [] : List DhcpServer.Type
+ , tcp = None L3Rule.Type
+ , udp = None L3Rule.Type
+ , tcpForward = None L3ForwardRule.Type
+ , udpForward = None L3ForwardRule.Type
+ }
+ , toXML =
+ λ(domain : Domain/Type) →
+ XML.element
+ { name = "domain"
+ , attributes =
+ mergeAttributes
+ ( toMap
+ { interface = domain.settings.interface
+ , gateway = domain.settings.gateway
+ , verbose_packets =
+ boolAttr domain.settings.verbose_packets
+ , verbose_packet_drop =
+ boolAttr domain.settings.verbose_packet_drop
+ , icmp_echo_server =
+ boolAttr domain.settings.icmp_echo_server
+ }
+ )
+ , content =
+ Prelude.List.map
+ L2Rule.Type
+ XML.Type
+ (L2Rule.toXML "ip")
+ domain.ip
+ # Prelude.List.map
+ L2Rule.Type
+ XML.Type
+ (L2Rule.toXML "icmp")
+ domain.icmp
+ # Prelude.List.map Nat.Type XML.Type Nat.toXML domain.nat
+ # Prelude.List.map
+ DhcpServer.Type
+ XML.Type
+ DhcpServer.toXML
+ domain.dhcpServer
+ # L3Rule.toXML "tcp" domain.tcp
+ # L3Rule.toXML "udp" domain.udp
+ # L3ForwardRule.toXML "tcp-forward" domain.tcpForward
+ # L3ForwardRule.toXML "udp-forward" domain.udpForward
+ }
+ }
+
+let Policy = { domain : DomainName, label : Init.LabelSelector.Type }
+
+let Config/Type =
+ { settings : Settings.Type
+ , report : Report.Type
+ , uplinks : List Uplink.Type
+ , domains : List Domain.Type
+ , policies : List Policy
+ , defaultPolicyDomain : Optional DomainName
+ }
+
+let Config/toConfig =
+ λ(config : Config/Type) →
+ Init.Config::{
+ , attributes = Settings.toAttributes config.settings
+ , content = [ Report.toXML config.report ]
+ , policies =
+ let Entry = Prelude.Map.Entry DomainName Init.LabelSelector.Type
+
+ in Prelude.List.map
+ Policy
+ Init.Config.Policy.Type
+ ( λ(x : Policy) →
+ Init.Config.Policy::{
+ , attributes = toMap { domain = x.domain }
+ , label = x.label
+ , service = "Nic"
+ }
+ )
+ config.policies
+ , defaultPolicy =
+ merge
+ { Some =
+ λ(domain : DomainName) →
+ Some
+ Init.Config.DefaultPolicy::{
+ , attributes = toMap { domain }
+ }
+ , None = None Init.Config.DefaultPolicy.Type
+ }
+ config.defaultPolicyDomain
+ }
+
+let Config/toChild =
+ λ(config : { binary : Text } ⩓ Config/Type) →
+ Init.Child.flat
+ Init.Child.Attributes::{
+ , binary = config.binary
+ , resources = Init.Resources::{
+ , caps = 300
+ , ram = Genode.units.MiB 10
+ }
+ , config = Config/toConfig config.(Config/Type)
+ }
+
+let Nic_router =
+ { Config =
+ { Settings
+ , Uplink
+ , Nat
+ , DhcpServer
+ , Domain
+ , Report
+ , Type = Config/Type
+ , default =
+ { settings = Settings.default
+ , report = Report.default
+ , uplinks = [] : List Uplink.Type
+ , domains = [] : List Domain.Type
+ , policies = [] : List Policy
+ , defaultPolicyDomain = None DomainName
+ }
+ , toConfig = Config/toConfig
+ , toChild = Config/toChild
+ }
+ }
+
+in Nic_router