diff --git a/AGENTS.md b/AGENTS.md index 531c7a8..32fbbb0 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -10,9 +10,9 @@ Stack: GHC 9.10.3, Cabal, Parsec 3.x, Aeson 2.x, Tasty/HUnit for tests. ```bash cabal build # build everything cabal test # run all test suites -cabal run fwlc -- check examples/router.fwl # parse + type-check a source file -cabal run fwlc -- compile examples/router.fwl # emit nftables JSON to stdout -cabal run fwlc -- pretty examples/router.fwl # pretty-print the parsed AST +cabal run fwlc -- check examples/simple-router.fwl # parse + type-check a source file +cabal run fwlc -- compile examples/simple-router.fwl # emit nftables JSON to stdout +cabal run fwlc -- pretty examples/simple-router.fwl # pretty-print the parsed AST ``` Run tests before marking any task complete. The test suite is `cabal test`. @@ -25,22 +25,24 @@ Run tests before marking any task complete. The test suite is `cabal test`. fwl/ ├── AGENTS.md ├── doc/ -│ ├── proposal.md ← initial design document and exploration -│ ├── fwl_grammar.md ← authoritative grammar reference; keep in sync with Parser.hs +│ ├── proposal.md <- initial design document and exploration +│ ├── fwl_grammar.md <- authoritative grammar reference; keep in sync with Parser.hs │ └── ref/ -│ ├── ruleset.nft ← example nftables ruleset -│ └── ruleset.json ← the same example nftables ruleset in json format +│ ├── ruleset.nft <- example nftables ruleset +│ └── ruleset.json <- the same example nftables ruleset in json format ├── examples/ -│ └── router.fwl ← canonical example; must parse and compile cleanly +│ ├── simple-router.fwl <- canonical simple example; must parse and compile cleanly +│ ├── simple-router.nft <- compiled nftables text output of simple-router.fwl +│ └── router.fwl <- full router example with WireGuard detection ├── src/FWL/ -│ ├── AST.hs ← all data types; source of truth for the AST -│ ├── Lexer.hs ← Parsec TokenParser, reservedNames, reservedOpNames -│ ├── Parser.hs ← top-level parser, all sub-parsers -│ ├── Pretty.hs ← AST → FWL source (round-trip printer) -│ ├── TypeCheck.hs ← effect row checker, exhaustiveness, CIDR intervals -│ ├── Interpret.hs ← evaluator + effect dispatch -│ ├── Compile.hs ← AST → nftables JSON (Aeson Value) -│ └── Util.hs ← shared helpers +│ ├── AST.hs <- all data types; source of truth for the AST +│ ├── Lexer.hs <- Parsec TokenParser, reservedNames, reservedOpNames +│ ├── Parser.hs <- top-level parser, all sub-parsers +│ ├── Pretty.hs <- AST -> FWL source (round-trip printer) +│ ├── TypeCheck.hs <- effect row checker, exhaustiveness, CIDR intervals +│ ├── Interpret.hs <- evaluator + effect dispatch +│ ├── Compile.hs <- AST -> nftables JSON (Aeson Value) +│ └── Util.hs <- shared helpers └── test/ ├── Main.hs ├── ParserTests.hs @@ -48,7 +50,7 @@ fwl/ └── CompileTests.hs ``` -The grammar document at `docs/grammar.md` must stay in sync with `Parser.hs` and `Lexer.hs`. +The grammar document at `doc/fwl_grammar.md` must stay in sync with `Parser.hs` and `Lexer.hs`. When changing the parser, update the grammar doc in the same commit. --- @@ -59,15 +61,29 @@ The pipeline is strictly linear with no back-edges: ``` source text - → Lexer (Text.Parsec.Token) - → Parser → [Decl] (AST.hs) - → TypeCheck → TypedDecl - → Compile → Aeson Value (nftables JSON) + -> Lexer (Text.Parsec.Token) + -> Parser -> [Decl] (AST.hs) + -> TypeCheck -> TypedDecl + -> Compile -> Aeson Value (nftables JSON) ``` The interpreter (`Interpret.hs`) runs the policy against a mock packet environment and is separate from the compiler. It uses the same typed AST. +### Compiler Synthesis + +These constructs are synthesised by `Compile.hs` and do not appear directly in the +nftables output as user-written rules: + +| FWL construct | Synthesised nftables output | +|----------------------|-----------------------------| +| `portforward` decl | A named `map`, a `nat hook prerouting priority dstnat` chain with `fib daddr type local` guard and `dnat ip to ... map` rewrite, and a `ct status dnat accept` rule injected into every `Forward` chain in the file. | +| `masquerade` decl | A `nat hook postrouting priority srcnat` chain with `ip saddr @set masquerade` rule. | +| Filter hook policy | `ct state { established, related } accept` (stateful), `iifname "lo" accept` (loopback), and `meta nfproto ipv6 ip6 nexthdr ipv6-icmp ip6 saddr fe80::/10 accept` (NDP) are prepended automatically to every `Input`, `Forward`, and `Output` chain before user-written rules. | + +These injections are intentional and documented in `doc/fwl_grammar.md`. Do not remove +them without updating the grammar document and all affected tests. + --- ## Reserved Words Rule @@ -84,6 +100,42 @@ and expression positions without causing parse errors. If you add a new keyword: add it to both `reservedNames` in `Lexer.hs` AND use `reserved "word"` in `Parser.hs`. Never add a word to only one place. +**Current reserved keywords:** +``` +config interface zone import from +let in pattern flow rule policy on +case of if then else do perform +within as dynamic cidr4 cidr6 +hook priority +portforward masquerade +WAN LAN WireGuard +Input Forward Output Prerouting Postrouting +Filter NAT Mangle DstNat SrcNat +Raw ConnTrack +true false +``` + +> `table` is **not** a reserved keyword — it was removed when `policyDecl` switched +> from the verbose `on { hook = ..., table = ..., priority = ... }` syntax to the +> compact `hook [priority

]` form. + +--- + +## Policy Hook Syntax + +The `on { hook = ..., table = ..., priority = ... }` block is gone. +Policies now use: + +```fwl +policy name : Frame hook Input = { ... }; +-- or with a non-default priority: +policy name : Frame hook Prerouting priority Mangle = { ... }; +``` + +The table is inferred from the hook; the priority defaults to the canonical +value for that hook. See `doc/fwl_grammar.md` → *Policy Declaration* for the +full hook-to-table-to-priority mapping. + --- ## IP Address Representation @@ -132,6 +184,8 @@ never a string. Do not use the old `priorityStr` function (deleted). not `literal` — the base `literal` parser does not handle `:N` syntax. - `Frame` and `FlowPattern` are NOT in `reservedNames`; they appear as type names and must be accepted by `identifier`. +- `portforward` and `masquerade` are in `reservedNames`; their parsers + (`portforwardDeclP`, `masqueradeDeclP`) must use `reserved` for these words. --- @@ -143,6 +197,8 @@ never a string. Do not use the old `priorityStr` function (deleted). `LIPv4 (a,b,c,d)` tuple constructors. - Priority assertions use `Priority n` directly, e.g. `Priority 0`, `Priority (-100)`. - All parse tests must compile and pass before any PR is merged. +- `CompileTests.hs` must include tests for `portforward` and `masquerade` synthesis + (synthesised chain names, injected `ct status dnat accept`, injected stateful/loopback/ndp rules). --- @@ -151,16 +207,19 @@ never a string. Do not use the old `priorityStr` function (deleted). ### ✅ Safe to do without asking - Read any file, list directories - Run `cabal build`, `cabal test`, `cabal run fwlc` -- Edit `src/`, `test/`, `examples/`, `docs/` +- Edit `src/`, `test/`, `examples/`, `doc/` - Add new test cases to existing test files ### ⚠️ Ask first - Add or remove Cabal dependencies (`fwl.cabal`) - Rename or delete source modules - Change the nftables JSON schema emitted by `Compile.hs` -- Modify `examples/router.fwl` in ways that change its semantics +- Modify `examples/simple-router.fwl` or `examples/router.fwl` in ways that change their semantics +- Add new compiler-injected rules (stateful, loopback, ndp, or new ones) ### 🚫 Never - Add semantic value names (`Allow`, `Drop`, `Log`, etc.) to `reservedNames` +- Add `table` to `reservedNames` — it is not a keyword in the current grammar - Break the `cabal test` suite - Emit nftables `"prio"` as a string — it must always be an integer +- Remove the implicit stateful/loopback/ndp injections from filter-hook chain compilation without updating the grammar doc and all tests diff --git a/doc/fwl_grammar.md b/doc/fwl_grammar.md index cbb95e1..2992f81 100644 --- a/doc/fwl_grammar.md +++ b/doc/fwl_grammar.md @@ -1,7 +1,7 @@ # FWL Grammar Specification -> **Version:** MVP -> **Last updated:** May 2026 +> **Version:** MVP +> **Last updated:** May 2026 > This document is the authoritative grammar reference for the Firewall Language (FWL). > It supersedes the syntax examples in `proposal.md` and reflects the current parser implementation. @@ -14,6 +14,8 @@ - **Types are explicit** — top-level declarations carry full type annotations in the MVP. - **Patterns vs. guards are strictly separated** — structural decomposition happens in patterns; boolean predicates over bound names happen in guards. - **IP addresses are integers** — IPv4 is a 32-bit value; IPv6 is a 128-bit value. Named priority constants (`Filter`, `SrcNat`, etc.) lower to their canonical integer values at parse time. +- **High-level NAT declarations hide nftables mechanics** — `portforward` and `masquerade` compile to their respective prerouting/postrouting chains automatically. Users never write NAT hook policies directly for these common patterns. +- **Common filter boilerplate is compiler-injected** — stateful (established/related accept), loopback accept, and link-local NDP accept are automatically prepended to all filter-hook policies by the compiler. Future work: make these importable builtins that can be overridden. --- @@ -29,6 +31,8 @@ decl ::= interfaceDecl | patternDecl | flowDecl | ruleDecl + | portforwardDecl + | masqueradeDecl | policyDecl ``` @@ -60,23 +64,104 @@ flowExpr ::= ident | ident "." ident "within" duration ruleDecl ::= "rule" ident ":" type "=" lambdaExpr ";" +``` +### Port-Forward Declaration + +`portforward` declares an IPv4 DNAT rule. The compiler synthesises: +1. A named map set from the inline `Map<...>` literal. +2. A `nat hook prerouting priority dstnat` chain with `fib daddr type local` guard and `dnat ip to` rewrite. +3. A `ct status dnat accept` rule injected into every `Forward` policy in the same file. + +```ebnf +portforwardDecl ::= "portforward" ident + "on" ident + "via" type "=" mapLit ";" +``` + +**Example:** + +```fwl +portforward wan_forwards + on wan + via Map<(Protocol, Port), (IPv4, Port)> = { + (tcp, :8080) -> (10.0.0.10, :80) + }; +``` + +### Masquerade Declaration + +`masquerade` declares source NAT (masquerade) for outbound traffic. The compiler synthesises a `nat hook postrouting priority srcnat` chain. + +```ebnf +masqueradeDecl ::= "masquerade" ident + "on" ident + "src" ident ";" +``` + +**Example:** + +```fwl +masquerade wan_snat + on wan + src rfc1918; +``` + +The `src` field must name a `Set` bound with `let`. + +### Policy Declaration + +The `on` block is replaced by a compact `hook` clause. The table is inferred from the hook; the priority defaults to the canonical value for that hook and may be overridden. + +```ebnf policyDecl ::= "policy" ident ":" type - "on" "{" - "hook" "=" hook "," - "table" "=" tableName "," - "priority" "=" priority - "}" + "hook" hook ( "priority" priority )? "=" armBlock ";" ``` -### Policy Metadata +| Hook | Inferred table | Default priority | +|---------------|---------------|------------------| +| `Input` | `filter` | `Filter` (0) | +| `Forward` | `filter` | `Filter` (0) | +| `Output` | `filter` | `Filter` (0) | +| `Prerouting` | `nat` | `DstNat` (-100) | +| `Postrouting` | `nat` | `SrcNat` (100) | + +**Implicit compiler injections for filter-hook policies:** + +The compiler automatically prepends the following rules to every `Input`, `Forward`, and `Output` policy, before the user-written arms. These do not appear in the FWL source. + +| Rule | nftables equivalent | Suppressed by | +|--------------|-------------------------------------------------------------|---------------| +| `stateful` | `ct state { established, related } accept` | *(future: `no-stateful` annotation)* | +| `loopback` | `iifname "lo" accept` | *(future: `no-loopback` annotation)* | +| `ndp` | `meta nfproto ipv6 ip6 nexthdr ipv6-icmp ip6 saddr fe80::/10 accept` | *(future: `no-ndp` annotation)* | + +The intended full design is for these to be importable builtins (see `proposal.md`); compiler injection is an MVP simplification. + +The `ct status dnat accept` rule is also injected into every `Forward` policy when at least one `portforward` declaration exists in the file. + +**Note:** Because `portforward` and `masquerade` synthesise the NAT chains, explicit `Prerouting` and `Postrouting` policies are not needed for these common patterns. A user-written `Prerouting` or `Postrouting` policy is still valid for advanced NAT cases not covered by the declarative forms. + +**Example:** + +```fwl +-- No priority override needed; defaults to Filter (0) +policy input : Frame hook Input = { + | Frame(_, IPv4(_, TCP(tcp, _))) + if tcp.dport in open_ports -> Allow; + | _ -> Drop; +}; + +-- Non-default priority example +policy mangle_pre : Frame hook Prerouting priority Mangle = { + | _ -> Continue; +}; +``` ```ebnf hook ::= "Input" | "Forward" | "Output" | "Prerouting" | "Postrouting" -tableName ::= "Filter" | "NAT" | ident - -- Priority is always an integer in nftables JSON. -- Named constants are resolved at parse time: -- Raw = -300, ConnTrack = -200, Mangle = -150, @@ -127,7 +212,7 @@ stmt ::= "let" ident "=" expr infixExpr ::= prefixExpr { infixOp prefixExpr } infixOp ::= "&&" | "||" | "==" | "!=" | "<" | "<=" | ">" | ">=" - | "++" | ">>" | ">>=" | "∈" | "in" + | "++" | ">>" | ">>=" | "\u2208" | "in" prefixExpr ::= "!" prefixExpr | appExpr @@ -136,7 +221,7 @@ appExpr ::= atom { atom } atom ::= performExpr | mapLit -- { expr -> expr, ... } tried before setLit | setLit -- { expr, ... } - | tupleLit -- ( expr, expr, ... ) requires ≥ 2 + | tupleLit -- ( expr, expr, ... ) requires >= 2 | "(" expr ")" | literal | portLit -- :22 :8080 @@ -161,7 +246,7 @@ qualName ::= ident { "." ident } ```ebnf pat ::= wildcardPat -- _ | framePat -- Frame(...) - | tuplePat -- (p, p, ...) requires ≥ 2 + | tuplePat -- (p, p, ...) requires >= 2 | bytesPat -- [ byteElem* ] | recordPat -- Ctor { field = lit, ... } | namedOrCtorPat -- Ctor(p,...) or bare identifier @@ -175,7 +260,7 @@ frameArgs ::= pathPat "," pat -- with explicit path pathPat ::= endpointPat? ( "->" endpointPat? )? endpointPat ::= "_" | ident "in" ident -- iif in lan_zone - | ident "∈" ident + | ident "\u2208" ident | ident tuplePat ::= "(" pat "," pat { "," pat } ")" @@ -188,7 +273,7 @@ byteElem ::= hexByte -- 0xff recordPat ::= ident "{" fieldPat { "," fieldPat } "}" fieldPat ::= ident "=" fieldLit -- exact match | ident "in" expr -- membership - | ident "∈" expr + | ident "\u2208" expr | ident "as" ident -- bind with alias | ident -- bind to same name @@ -222,7 +307,7 @@ literal ::= ipOrCidrLit portLit ::= ":" nat -- :22, :8080, :51944 -ipOrCidrLit ::= ipLit ( "/" nat )? -- optional prefix → CIDR +ipOrCidrLit ::= ipLit ( "/" nat )? -- optional prefix -> CIDR ipLit ::= ipv6Lit | ipv4Lit @@ -271,11 +356,12 @@ CIDR host-bit validation: `(addr .&. hostMask) == 0` where `hostMask = (1 << (bi Only these words are reserved (i.e. `identifier` will reject them): ``` -config table interface zone import from +config interface zone import from let in pattern flow rule policy on case of if then else do perform within as dynamic cidr4 cidr6 hook priority +portforward masquerade WAN LAN WireGuard Input Forward Output Prerouting Postrouting Filter NAT Mangle DstNat SrcNat @@ -283,6 +369,9 @@ Raw ConnTrack true false ``` +> **Note:** `table` is no longer a reserved keyword — it was only used inside the old +> `on { hook = ..., table = ..., priority = ... }` block, which is removed. + The following are **not** reserved and parse as plain identifiers in all positions (type names, constructors, action values, effect labels): @@ -291,7 +380,7 @@ Frame FlowPattern Allow Drop Continue Masquerade DNAT DNATMap Log Info Warn Error Matched Unmatched -Action Packet IP Port Protocol +Action Packet IP IPv4 IPv6 Port Protocol CIDRSet Map Bytes ``` @@ -320,7 +409,7 @@ From lowest to highest binding: | Level | Operators | Associativity | |-------|------------------------|---------------| -| 1 | `if … then … else` | — | +| 1 | `if ... then ... else` | — | | 2 | `\|\|` | left | | 3 | `&&` | left | | 4 | `==` `!=` | none | @@ -344,6 +433,23 @@ interface wg0 : WireGuard {}; zone lan_zone = { lan, wg0 }; ``` +### Port-forward and masquerade declarations + +```fwl +let rfc1918 : Set = { 10.0.0.0/8, 172.16.0.0/12, 192.168.0.0/16 }; + +portforward wan_forwards + on wan + via Map<(Protocol, Port), (IPv4, Port)> = { + (tcp, :8080) -> (10.0.0.10, :80), + (tcp, :2222) -> (10.0.0.11, :22) + }; + +masquerade wan_snat + on wan + src rfc1918; +``` + ### Map literal ```fwl @@ -382,18 +488,28 @@ rule blockOutboundWG : Frame -> Action = }; ``` -### Policy +### Policy (new compact hook syntax) ```fwl -policy input : Frame - on { hook = Input, table = Filter, priority = Filter } = - { - | _ if ct.state in { Established, Related } -> Allow; - | Frame(lo, _) -> Allow; - | Frame(_, Ether(_, IPv4(_, TCP(tcp, _)))) - if tcp.dport == :22 -> Allow; - | Frame(_, Ether(_, IPv4(_, UDP(udp, _)))) - if udp.dport == :51944 -> Allow; - | _ -> Drop; - }; +-- stateful, loopback, and ndp are injected automatically by the compiler. +-- No need to write them in the arm list. +policy input : Frame hook Input = { + | Frame(_, IPv4(_, TCP(tcp, _))) + if tcp.dport in open_ports -> Allow; + | Frame(_, IPv4(_, UDP(udp, _))) + if udp.dport == :51944 -> Allow; + | _ -> Drop; +}; + +policy forward : Frame hook Forward = { + -- ct status dnat accept is injected automatically when portforward decls exist. + | Frame(iif in lan_zone -> wan, _) -> Allow; + | Frame(wan -> iif in lan_zone, IPv6(ip6, TCP(th, _) | UDP(th, _))) + if (ip6.protocol, ip6.dst, th.dport) in forwards_v6 -> Allow; + | _ -> Drop; +}; ``` + +### Simple router (full example) + +See `examples/simple-router.fwl` for the complete canonical simple router example.