Typed layer with ci

.github/workflows/build.yml

@@ -0,0 +1,41 @@
+# based on the CI file from MetaRocq
+name: Certified Nftables CI
+
+on:
+  push:
+  pull_request:
+    types: [opened, reopened, ready_for_review]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+
+      - name: Checkout code
+        uses: actions/checkout@v6
+        with:
+          fetch-depth: 1
+
+      - name: Docker-Coq-Action
+        uses: coq-community/docker-coq-action@v1
+        with:
+          coq_version: 9.1
+          ocaml_version: 4.14-flambda
+          opam_file: .github/workflows/nft.opam
+          before_install: |
+            startGroup "Print opam config"
+              opam config list; opam repo list; opam list
+            endGroup
+            startGroup "Workaround permission issue"
+              sudo chown -R 1000:1000 .
+            endGroup
+          script: |
+            startGroup "Build project"
+              cd proof
+              make proofs
+            endGroup
+      - name: Revert permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .  # <--

.github/workflows/nft.opam

@@ -0,0 +1,45 @@
+opam-version: "2.0"
+compiler: [
+  "base-bigarray.base"
+  "base-threads.base"
+  "base-unix.base"
+  "ocaml.4.14.2"
+  "ocaml-base-compiler.4.14.2"
+  "ocaml-config.2"
+  "ocaml-options-vanilla.1"
+]
+roots: [
+  "conf-gcc.1.0"
+  "coq.9.1.1"
+  "dune.3.23.1"
+  "menhir.20260209"
+  "ocaml-base-compiler.4.14.2"
+]
+installed: [
+  "base-bigarray.base"
+  "base-threads.base"
+  "base-unix.base"
+  "conf-gcc.1.0"
+  "conf-gmp.5"
+  "conf-linux-libc-dev.0"
+  "conf-pkg-config.4"
+  "coq.9.1.1"
+  "coq-core.9.1.1"
+  "coq-stdlib.9.0.0"
+  "coqide-server.9.1.1"
+  "dune.3.23.1"
+  "menhir.20260209"
+  "menhirCST.20260209"
+  "menhirGLR.20260209"
+  "menhirLib.20260209"
+  "menhirSdk.20260209"
+  "ocaml.4.14.2"
+  "ocaml-base-compiler.4.14.2"
+  "ocaml-config.2"
+  "ocaml-options-vanilla.1"
+  "ocamlfind.1.9.8"
+  "rocq-core.9.1.1"
+  "rocq-runtime.9.1.1"
+  "rocq-stdlib.9.0.0"
+  "zarith.1.14"
+]

NOTES.md

@@ -17,17 +17,17 @@ see [`adversarial.md`](adversarial.md).
   each machine-checked & composed into `optimize_table` — see `Optimize_Table.v`
   for the exact order). The families now folded (each verdict-preserving,
   kernel-datapath-checked):
-  - **value → SET**: network addresses (`setsN`); transport ports & `ether saddr`
+  - **value → SET**: network addresses (`valueset`); transport ports & `ether saddr`
     L2 (`setg`); fixed-width meta scalars — `mark`/`skuid`/`skgid`/`l4proto`/
     `nfproto`/`pkttype`/`cpu`/`protocol` — plus `iifname`/`oifname` strings and
-    scalar `ct mark` (`Optimize_Merge`).
+    scalar `ct mark` (`Optimize_ValueSet`).
   - **value+verdict → VMAP**: network address + transport + `ether saddr` L2
-    (`vmapNg`), network (`vmapN`), `ip dscp` (`dscpv`).
-  - **interval RANGE → set**: network (`ivset`), host-order `ct mark` (`ivsett`),
-    guarded transport/inet (`ivsetg`), mixed point+range (`ivmixg`).
-  - **concat**: K-field (`concatK`), 2-field (`concatN`), transport-guarded
-    (`concatM`, e.g. `ip saddr . tcp dport`).
-  - **maps**: `dnat`/`snat` bare-map, meta-mark map (`mapn`, sound superset).
+    (`vmapguarded`), network (`vmap`), `ip dscp` (`dscpvmap`).
+  - **interval RANGE → set**: network (`intervalset`), host-order `ct mark` (`intervalsethostorder`),
+    guarded transport/inet (`intervalsetguarded`), mixed point+range (`mixedpointrangeguarded`).
+  - **concat**: K-field (`concatmulti`), 2-field (`concat`), transport-guarded
+    (`concatguarded`, e.g. `ip saddr . tcp dport`).
+  - **maps**: `dnat`/`snat` bare-map, meta-mark map (`datamap`, sound superset).
   - **`ct state` bitmask-UNION** (`ctmask` — the *sound* `state & 0x0a != 0`,
     NOT nft's exact-set; see the nft bitmask defect below), **`ip dscp` masked
     set** (`dscp`), same-verdict **prefix absorption** `/24 ⊂ /16 → /16` (`absorb`).
@@ -53,7 +53,7 @@ see [`adversarial.md`](adversarial.md).
      set (dropping the bitwise). A packet with extra bits set (e.g. `tcp flags`
      `0x12` = SYN+ACK) matches the bit-test but misses the exact set → the fold
      silently changes the verdict. We instead fold the *sound* same-verdict
-     mask-union (`state & (a|b) != 0`, one masked compare; `Optimize_Ctmask`).
+     mask-union (`state & (a|b) != 0`, one masked compare; `Optimize_CtMask`).
 
 ## Remaining work
 
@@ -66,13 +66,13 @@ What remains open:
 
 - **G1 — differing-verdict multi-field concat → concat VMAP** (soundly closeable,
   no new semantics; the honest deferral from the 2026-07-02 G1–G4 round). The
-  *same-verdict* concat→SET case already folds (`concatK/N/M`); the open case is
+  *same-verdict* concat→SET case already folds (`concatmulti/N/M`); the open case is
   `ip saddr X tcp dport Y accept; … Z drop` → `saddr . tcp dport vmap { X.Y :
   accept, … : drop }`. No stage today produces a *concat-keyed vmap* (every vmap
   stage has a single-field key; every concat stage yields a single-verdict set).
-  Spec: a new `Optimize_ConcatVmap.v` = `Optimize_ConcatM` (multi-field concat-key
+  Spec: a new `Optimize_ConcatVmap.v` = `Optimize_ConcatGuarded` (multi-field concat-key
   recogniser) × `Optimize_Vmap` (`assoc_verdict` first-match order), composed
-  between `concatM` and `setg`. A substantial new proof, not a template tweak.
+  between `concatguarded` and `setg`. A substantial new proof, not a template tweak.
 
 - **Shapes 14/15 — strictly-interior overlapping-verdict concat → vmap** (needs a
   semantics extension). `nft -o`'s fold *is* verdict-correct here: a concatenated
@@ -101,6 +101,21 @@ the per-shape classification and kernel-source citations.
   has). Still to adjudicate against a real kernel: `ct state`'s own representation and
   the remaining host-order `ct`/`meta`/`rt` keys the display fix covers by class but
   that were not individually packet-tested.
+  **Source-side corpus coverage (measured 2026-07; the widen-the-gate TODO).** Driving
+  the WHOLE corpus source-side (parse each block's `# <src>` header, compile with the
+  verified compiler, diff all rendered lines): of **1742** attemptable headered blocks,
+  **1142 (65.6 %)** are already byte-identical, **517** fail loudly on frontend syntax
+  gaps, and **83** are genuine text mismatches — host-order byte-order divergences on
+  keys *outside* byteorder-gate's set (`meta length/cpu/skuid/skgid`, `ct expiration`,
+  bitwise mask/xor operands), nft constant-folds/merges we don't replicate (`xor`
+  fold, adjacent-payload merge), and render/lowering text differences with no
+  adjudicated wire divergence (dependency guards, reject/log defaults).
+  A full source gate would be red today (83), and most of that red is *unadjudicated
+  display-vs-wire divergence*, so the gate stays scoped to the adjudicated host-order
+  plain-cmp/range class (13 blocks). TODO: adjudicate the mismatch classes against a
+  real kernel (netns packet counters, as for meta/ct mark), then widen the gate
+  class-by-class. Details: `proof/DEVELOPMENT.md` § "What the round-trip does and does
+  NOT validate".
 - **Field-unit faithfulness**: `FPayload` off/len are in bytes vs nft's bits;
   `SMangle`/`SExthdrWrite` carry raw byte geometry rather than a `field`.
 - **Network-state model**: single-address-per-interface assumption; the long-term

README.md

@@ -12,14 +12,14 @@ interprets the bytecode, is trusted and unverified.
 
 Other than building and running the `nftc_cli.exe` command line tool,
 you can also use Rocq to formally prove properties about your ruleset (see
-[proof/theories/Optiplex_Antispoof.v](Optiplex\_Antispoof.v), which
-reasons about the ruleset [optiplex.nft](rulesets/optiplex.nft).
+[proof/theories/Examples/Optiplex_Antispoof.v](proof/theories/Examples/Optiplex_Antispoof.v), which
+reasons about the ruleset [optiplex.nft](rulesets/optiplex.nft)).
 A step-by-step tutorial for this analysis workflow — write a `.nft` file,
 parse it into Coq terms with `make gen`, then prove it blocks *exactly* one
 IP range (an iff, for all packets) — is in
 [proof/CONFIG_PROOFS.md](proof/CONFIG_PROOFS.md), with the worked example
 [rulesets/tutorial.nft](rulesets/tutorial.nft) /
-[proof/theories/Tutorial_Proofs.v](proof/theories/Tutorial_Proofs.v).
+[proof/theories/Examples/Tutorial_Proofs.v](proof/theories/Examples/Tutorial_Proofs.v).
 
 The core compiler is tested against the stock `nft` utility, but the
 untrusted OCaml code isn't fully exercised. Therefore, you should
@@ -56,17 +56,46 @@ The remaining text in the README file is generated by LLM.
 - **Semantics-preserving compilation + a verified DSL optimizer**, machine-checked in Rocq.
   `compile_chain_correct` says the bytecode VM agrees with the DSL semantics, and
   `optimize_table_uncond_compile_correct` says the compiled bytecode of the *optimized*
-  ruleset preserves every packet's verdict — for **any** input ruleset, with no
-  `rules_clean` or freshness precondition.
+  chain preserves every packet's verdict. The optimizer theorem is **per-chain**:
+  it quantifies over a single chain and *all* environments and packets, with no
+  `rules_clean` or freshness precondition; multi-chain/hook preservation is the
+  separate `compile_ruleset_correct`/`compile_hook_correct` family (not composed
+  with the optimizer). The full theorem map is
+  [proof/THEOREMS.md](proof/THEOREMS.md).
 - **Differential-tested against the upstream nftables test corpus.** Extracted to OCaml, it
   reproduces the real tool's bytecode on **2532/2532 (100%)** of the corpus's rule-blocks
-  with zero mismatches (`cd proof && make corpus`), and validates field offsets / meta-ct
-  names against a live `nft` (`make validate`, 28/28).
+  with zero mismatches (`cd proof && make corpus`). Read that number for what its oracle
+  direction supports: `make corpus` *reconstructs* the DSL rule **from** each corpus
+  netlink block and checks `render(compile(reconstruct(b))) = b` — a payload-level
+  round-trip **fixed point**, not a compile-from-`.nft`-source diff, so a systematic
+  misunderstanding of nft's source→bytecode mapping that the reconstructor and compiler
+  *share* would round-trip cleanly. The independent cross-checks are `make validate`
+  (field offsets / meta-ct names vs a **live `nft`**, 28/28), `make byteorder-gate`
+  (host-endian corpus blocks compiled **from their `# <src>` headers**), and the
+  `difftest`/`e2e`/`parse-test` source-side diffs vs live `nft`. The measured
+  source-side coverage of the corpus itself, and why the full source-driven gate is
+  not wired in yet, are in [proof/DEVELOPMENT.md](proof/DEVELOPMENT.md)
+  § "What the round-trip does and does NOT validate".
 - **Data-plane semantics hardened by an adversarial red/blue fidelity audit** against the
-  linux kernel source — see **[adversarial.md](adversarial.md)**.
+  linux kernel source — see **[adversarial.md](adversarial.md)**. Two residual,
+  confirmed model-vs-kernel divergences remain open by design and are ledgered (with
+  `vm_compute` lock-in pins) in [proof/DEVELOPMENT.md](proof/DEVELOPMENT.md)
+  § "Known model infidelities" (the historical third — intra-rule set-then-read —
+  is repaired by the single-fold rule semantics; positive pins in
+  `proof/theories/Regression/Setread_IntraRule.v`).
 - **Headline guarantees are axiom-free** ("Closed under the global context"): the
-  anti-spoofing, established-accept, NAT-masquerade, multi-address primary-selection, fib
-  host-local, and ct-state results.
+  anti-spoofing (env-universal `antispoof_general_any_env`), established-accept
+  (axiom-free but **vacuous as stated** — its whole-env pin contradicts its own
+  ct hypothesis; ledgered OPEN in [proof/THEOREMS.md](proof/THEOREMS.md) §5),
+  NAT-masquerade, multi-address primary-selection, fib host-local, ct-state,
+  fuel-adequacy (the jump strand's fuel budget is a *discharged* side condition:
+  verdicts are provably fuel-independent above a computable bound —
+  [proof/THEOREMS.md](proof/THEOREMS.md) §3 "Fuel adequacy"), and the de-vacuized
+  optiplex firewall-mark results (`Optiplex_Mark.*_real`,
+  [proof/THEOREMS.md](proof/THEOREMS.md) §5). This is a *gated* claim, not an eyeballed one:
+  every theorem in this list is in `AXIOM_GATE_THEOREMS` (`proof/Makefile`), and
+  `cd proof && make axioms` fails the build if any of them acquires an axiom or an
+  `Admitted` (see [proof/THEOREMS.md](proof/THEOREMS.md) §4 for the exact set).
 
 Start at **[proof/DEVELOPMENT.md](proof/DEVELOPMENT.md)** for the design notes and the
 honest scope of the "2532/2532" claim.
@@ -127,7 +156,10 @@ kernel state and requires `--commit`, otherwise it dry-runs). Flags: `--table T`
 | `make nl-send` | push verified-compiled rules to the kernel in a fresh net namespace, read back with `nft list ruleset` |
 | `make difftest` | byte-identical forward check of a hand-written ruleset vs the local `nft` |
 | `make lib` / `make example` | build the reusable `nftc` library / build+run its standalone consumer demo |
-| `make gen` | regenerate the parser-output Coq terms (`theories/*_Gen.v`) from the `.nft` sources |
+| `make gen` | regenerate the parser-output Coq terms (`theories/Generated/*_Gen.v`) from the `.nft` sources (all four rulesets, `router.nft` included) |
+| `make gen-check` | drift gate: fail unless every checked-in `theories/Generated/*_Gen.v` is byte-identical to a fresh `nft2coq` run over its `.nft` source |
+| `make axioms` | axiom-freedom gate: every claimed theorem must be "Closed under the global context" (fails the build otherwise) |
+| `make gates` | the aggregate enforcement point: `proofs` + `axioms` + `corpus` + `validate` + `parse-test` + `gen-check` in sequence |
 
 Sample rulesets to try the CLI on live in `rulesets/`: `rulesets/ruleset.nft`,
 `rulesets/router.nft`, `rulesets/optiplex.nft`, `rulesets/tutorial.nft`.