CaZzzer/fwl
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

doc: update grammar spec and AGENTS.md for v2 design decisions

Browse Source 
- policyDecl: replace verbose on{hook,table,priority} block with
  compact `hook <Hook> [priority <P>]` syntax; table is inferred
  from hook, priority defaults to canonical value for that hook
- Add portforwardDecl and masqueradeDecl top-level declarations
- Add implicit injection rules for stateful/loopback/ndp to
  compiler behaviour section (MVP; importable builtins deferred)
- Remove nat_prerouting / nat_postrouting from canonical policy
  example (replaced by portforward/masquerade declarations)
- Update reserved keywords: add portforward, masquerade, hook (was
  already reserved), priority (was already reserved); remove table
  as a reserved word since it no longer appears in policyDecl
- AGENTS.md: update architecture notes, reserved-words rule, and
  boundaries to reflect new declarations and compiler synthesis
This commit is contained in:
Yura
2026-05-04 02:15:58 -07:00
parent 9390647f7a
commit 55c1d347e6
2 changed files with 229 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files

105
AGENTS.md
View File

@@ -10,9 +10,9 @@ Stack: GHC 9.10.3, Cabal, Parsec 3.x, Aeson 2.x, Tasty/HUnit for tests.
```bash ```bash
cabal build # build everything cabal build # build everything
cabal test # run all test suites cabal test # run all test suites
cabal run fwlc -- check examples/router.fwl # parse + type-check a source file cabal run fwlc -- check examples/simple-router.fwl # parse + type-check a source file
cabal run fwlc -- compile examples/router.fwl # emit nftables JSON to stdout cabal run fwlc -- compile examples/simple-router.fwl # emit nftables JSON to stdout
cabal run fwlc -- pretty examples/router.fwl # pretty-print the parsed AST 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`. 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/ fwl/
├── AGENTS.md ├── AGENTS.md
├── doc/ ├── doc/
│ ├── proposal.md ← initial design document and exploration │ ├── proposal.md <- initial design document and exploration
│ ├── fwl_grammar.md ← authoritative grammar reference; keep in sync with Parser.hs │ ├── fwl_grammar.md <- authoritative grammar reference; keep in sync with Parser.hs
│ └── ref/ │ └── ref/
│ ├── ruleset.nft ← example nftables ruleset │ ├── ruleset.nft <- example nftables ruleset
│ └── ruleset.json ← the same example nftables ruleset in json format │ └── ruleset.json <- the same example nftables ruleset in json format
├── examples/ ├── 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/ ├── src/FWL/
│ ├── AST.hs ← all data types; source of truth for the AST │ ├── AST.hs <- all data types; source of truth for the AST
│ ├── Lexer.hs ← Parsec TokenParser, reservedNames, reservedOpNames │ ├── Lexer.hs <- Parsec TokenParser, reservedNames, reservedOpNames
│ ├── Parser.hs ← top-level parser, all sub-parsers │ ├── Parser.hs <- top-level parser, all sub-parsers
│ ├── Pretty.hs ← AST → FWL source (round-trip printer) │ ├── Pretty.hs <- AST -> FWL source (round-trip printer)
│ ├── TypeCheck.hs ← effect row checker, exhaustiveness, CIDR intervals │ ├── TypeCheck.hs <- effect row checker, exhaustiveness, CIDR intervals
│ ├── Interpret.hs ← evaluator + effect dispatch │ ├── Interpret.hs <- evaluator + effect dispatch
│ ├── Compile.hs ← AST → nftables JSON (Aeson Value) │ ├── Compile.hs <- AST -> nftables JSON (Aeson Value)
│ └── Util.hs ← shared helpers │ └── Util.hs <- shared helpers
└── test/ └── test/
├── Main.hs ├── Main.hs
├── ParserTests.hs ├── ParserTests.hs
@@ -48,7 +50,7 @@ fwl/
└── CompileTests.hs └── 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. 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 source text
→ Lexer (Text.Parsec.Token) -> Lexer (Text.Parsec.Token)
→ Parser → [Decl] (AST.hs) -> Parser -> [Decl] (AST.hs)
→ TypeCheck → TypedDecl -> TypeCheck -> TypedDecl
→ Compile → Aeson Value (nftables JSON) -> Compile -> Aeson Value (nftables JSON)
``` ```
The interpreter (`Interpret.hs`) runs the policy against a mock packet environment The interpreter (`Interpret.hs`) runs the policy against a mock packet environment
and is separate from the compiler. It uses the same typed AST. 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 ## 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` 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. 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 <Hook> [priority <P>]` 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 ## 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. not `literal` — the base `literal` parser does not handle `:N` syntax.
- `Frame` and `FlowPattern` are NOT in `reservedNames`; they appear as type - `Frame` and `FlowPattern` are NOT in `reservedNames`; they appear as type
names and must be accepted by `identifier`. 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. `LIPv4 (a,b,c,d)` tuple constructors.
- Priority assertions use `Priority n` directly, e.g. `Priority 0`, `Priority (-100)`. - Priority assertions use `Priority n` directly, e.g. `Priority 0`, `Priority (-100)`.
- All parse tests must compile and pass before any PR is merged. - 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 ### ✅ Safe to do without asking
- Read any file, list directories - Read any file, list directories
- Run `cabal build`, `cabal test`, `cabal run fwlc` - 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 - Add new test cases to existing test files
### ⚠️ Ask first ### ⚠️ Ask first
- Add or remove Cabal dependencies (`fwl.cabal`) - Add or remove Cabal dependencies (`fwl.cabal`)
- Rename or delete source modules - Rename or delete source modules
- Change the nftables JSON schema emitted by `Compile.hs` - 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 ### 🚫 Never
- Add semantic value names (`Allow`, `Drop`, `Log`, etc.) to `reservedNames` - 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 - Break the `cabal test` suite
- Emit nftables `"prio"` as a string — it must always be an integer - 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

174
doc/fwl_grammar.md
View File

@@ -14,6 +14,8 @@
- **Types are explicit** — top-level declarations carry full type annotations in the MVP. - **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. - **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. - **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 | patternDecl
| flowDecl | flowDecl
| ruleDecl | ruleDecl
| portforwardDecl
| masqueradeDecl
| policyDecl | policyDecl
``` ```
@@ -60,23 +64,104 @@ flowExpr ::= ident
| ident "." ident "within" duration | ident "." ident "within" duration
ruleDecl ::= "rule" ident ":" type "=" lambdaExpr ";" 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<IPv4>` 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 policyDecl ::= "policy" ident ":" type
"on" "{" "hook" hook ( "priority" priority )?
"hook" "=" hook ","
"table" "=" tableName ","
"priority" "=" priority
"}"
"=" armBlock ";" "=" 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 ```ebnf
hook ::= "Input" | "Forward" | "Output" | "Prerouting" | "Postrouting" hook ::= "Input" | "Forward" | "Output" | "Prerouting" | "Postrouting"
tableName ::= "Filter" | "NAT" | ident
-- Priority is always an integer in nftables JSON. -- Priority is always an integer in nftables JSON.
-- Named constants are resolved at parse time: -- Named constants are resolved at parse time:
-- Raw = -300, ConnTrack = -200, Mangle = -150, -- Raw = -300, ConnTrack = -200, Mangle = -150,
@@ -127,7 +212,7 @@ stmt ::= "let" ident "=" expr
infixExpr ::= prefixExpr { infixOp prefixExpr } infixExpr ::= prefixExpr { infixOp prefixExpr }
infixOp ::= "&&" | "||" | "==" | "!=" | "<" | "<=" | ">" | ">=" infixOp ::= "&&" | "||" | "==" | "!=" | "<" | "<=" | ">" | ">="
| "++" | ">>" | ">>=" | "∈" | "in" | "++" | ">>" | ">>=" | "\u2208" | "in"
prefixExpr ::= "!" prefixExpr | appExpr prefixExpr ::= "!" prefixExpr | appExpr
@@ -136,7 +221,7 @@ appExpr ::= atom { atom }
atom ::= performExpr atom ::= performExpr
| mapLit -- { expr -> expr, ... } tried before setLit | mapLit -- { expr -> expr, ... } tried before setLit
| setLit -- { expr, ... } | setLit -- { expr, ... }
| tupleLit -- ( expr, expr, ... ) requires ≥ 2 | tupleLit -- ( expr, expr, ... ) requires >= 2
| "(" expr ")" | "(" expr ")"
| literal | literal
| portLit -- :22 :8080 | portLit -- :22 :8080
@@ -161,7 +246,7 @@ qualName ::= ident { "." ident }
```ebnf ```ebnf
pat ::= wildcardPat -- _ pat ::= wildcardPat -- _
| framePat -- Frame(...) | framePat -- Frame(...)
| tuplePat -- (p, p, ...) requires ≥ 2 | tuplePat -- (p, p, ...) requires >= 2
| bytesPat -- [ byteElem* ] | bytesPat -- [ byteElem* ]
| recordPat -- Ctor { field = lit, ... } | recordPat -- Ctor { field = lit, ... }
| namedOrCtorPat -- Ctor(p,...) or bare identifier | namedOrCtorPat -- Ctor(p,...) or bare identifier
@@ -175,7 +260,7 @@ frameArgs ::= pathPat "," pat -- with explicit path
pathPat ::= endpointPat? ( "->" endpointPat? )? pathPat ::= endpointPat? ( "->" endpointPat? )?
endpointPat ::= "_" endpointPat ::= "_"
| ident "in" ident -- iif in lan_zone | ident "in" ident -- iif in lan_zone
| ident "∈" ident | ident "\u2208" ident
| ident | ident
tuplePat ::= "(" pat "," pat { "," pat } ")" tuplePat ::= "(" pat "," pat { "," pat } ")"
@@ -188,7 +273,7 @@ byteElem ::= hexByte -- 0xff
recordPat ::= ident "{" fieldPat { "," fieldPat } "}" recordPat ::= ident "{" fieldPat { "," fieldPat } "}"
fieldPat ::= ident "=" fieldLit -- exact match fieldPat ::= ident "=" fieldLit -- exact match
| ident "in" expr -- membership | ident "in" expr -- membership
| ident "∈" expr | ident "\u2208" expr
| ident "as" ident -- bind with alias | ident "as" ident -- bind with alias
| ident -- bind to same name | ident -- bind to same name
@@ -222,7 +307,7 @@ literal ::= ipOrCidrLit
portLit ::= ":" nat -- :22, :8080, :51944 portLit ::= ":" nat -- :22, :8080, :51944
ipOrCidrLit ::= ipLit ( "/" nat )? -- optional prefix → CIDR ipOrCidrLit ::= ipLit ( "/" nat )? -- optional prefix -> CIDR
ipLit ::= ipv6Lit | ipv4Lit 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): 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 let in pattern flow rule policy on
case of if then else do perform case of if then else do perform
within as dynamic cidr4 cidr6 within as dynamic cidr4 cidr6
hook priority hook priority
portforward masquerade
WAN LAN WireGuard WAN LAN WireGuard
Input Forward Output Prerouting Postrouting Input Forward Output Prerouting Postrouting
Filter NAT Mangle DstNat SrcNat Filter NAT Mangle DstNat SrcNat
@@ -283,6 +369,9 @@ Raw ConnTrack
true false 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 The following are **not** reserved and parse as plain identifiers in all positions
(type names, constructors, action values, effect labels): (type names, constructors, action values, effect labels):
@@ -291,7 +380,7 @@ Frame FlowPattern
Allow Drop Continue Masquerade DNAT DNATMap Allow Drop Continue Masquerade DNAT DNATMap
Log Info Warn Error Log Info Warn Error
Matched Unmatched Matched Unmatched
Action Packet IP Port Protocol Action Packet IP IPv4 IPv6 Port Protocol
CIDRSet Map Bytes CIDRSet Map Bytes
``` ```
@@ -320,7 +409,7 @@ From lowest to highest binding:
| Level | Operators | Associativity | | Level | Operators | Associativity |
|-------|------------------------|---------------| |-------|------------------------|---------------|
| 1 | `if … then … else` | — | | 1 | `if ... then ... else` | — |
| 2 | `\|\|` | left | | 2 | `\|\|` | left |
| 3 | `&&` | left | | 3 | `&&` | left |
| 4 | `==` `!=` | none | | 4 | `==` `!=` | none |
@@ -344,6 +433,23 @@ interface wg0 : WireGuard {};
zone lan_zone = { lan, wg0 }; zone lan_zone = { lan, wg0 };
``` ```
### Port-forward and masquerade declarations
```fwl
let rfc1918 : Set<IPv4> = { 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 ### Map literal
```fwl ```fwl
@@ -382,18 +488,28 @@ rule blockOutboundWG : Frame -> <FlowMatch, Log> Action =
}; };
``` ```
### Policy ### Policy (new compact hook syntax)
```fwl ```fwl
policy input : Frame -- stateful, loopback, and ndp are injected automatically by the compiler.
on { hook = Input, table = Filter, priority = Filter } = -- No need to write them in the arm list.
{ policy input : Frame hook Input = {
| _ if ct.state in { Established, Related } -> Allow; | Frame(_, IPv4(_, TCP(tcp, _)))
| Frame(lo, _) -> Allow; if tcp.dport in open_ports -> Allow;
| Frame(_, Ether(_, IPv4(_, TCP(tcp, _)))) | Frame(_, IPv4(_, UDP(udp, _)))
if tcp.dport == :22 -> Allow; if udp.dport == :51944 -> Allow;
| Frame(_, Ether(_, IPv4(_, UDP(udp, _)))) | _ -> Drop;
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.