Repository navigation
Typed layer with ci - #1
Merged
Merged
Conversation
… changes)
An external reviewer can now answer "what exactly is proved, by which theorem,
under which evaluator, and is it axiom-free?" from checked-in artifacts:
- proof/THEOREMS.md (new): one HEADLINE theorem per verified axis
(compile_hook_correct + compile_seq_correct; compile_seq_mut_correct;
optimize_table_uncond_compile_correct), HEADLINE/STAGE/SUPPORTING/
SUPERSEDED/DEMO classification of every Theorem/Corollary in Correct.v and
Optimize*.v with derivation edges, and the 9-evaluator feature matrix with
a bridging theorem (or "no bridging theorem") for every no-cell, plus the
explicit "mutation x jump/goto is not jointly verified" scope line.
- theories/Main.v (new, in _CoqProject): the four entry-point theorems
restated verbatim (exact-aliases, no new proof terms) with timeless scope
paragraphs, each followed by Print Assumptions.
- Correct.v: header/section comments rewritten as bottom-up strata (the old
"Main result/Main theorem" headers designated the weakest stratum); an
axiom-freedom audit block (8x Print Assumptions) appended;
compile_seq_correct's docstring demoted to what it is (a per-packet
congruence under an arbitrary caller-supplied step, not ruleset-generated
state accumulation).
- Makefile: new `make axioms` gate — Print Assumptions over the THEOREMS.md
HEADLINE set + Correct.v strata (10 theorems), fails on anything but
"Closed under the global context".
- Semantics.v: evaluator matrix in the header ("threads writes" columns);
mutation-free-domain notes on eval_rules_j/eval_ruleset/eval_hook mirroring
the existing jump-free note on eval_rules; seq_eval scope note.
- SUPERSEDED markers: Optimize.optimize_chain_correct (successor
optimize_table_uncond_correct; survives as the pipeline's base stage),
Optimize_Merge.optimize_chain2_correct (not in the shipped pipeline), and
eval_rules_range_value_merge (known-unfaithful RANGE-vs-SET note moved from
the file header onto the theorem itself). The 15 per-pass Optimize_Uncond
theorems tagged STAGE; the optimizer headline tagged with its per-chain
scope.
- DEVELOPMENT.md: optimizer section rewritten as two layers (rule-local base
pass; the shipped 18-stage optimize_table pipeline enumerated in
composition order) — no more "5 passes"; compile_seq_correct row fixed
("arbitrary step"); stale fib-oracle "Known abstractions" text replaced
with the lpm_fib/e_routes description; duplicate/contradictory
conntrack, hook-dispatch and concat-padding bullets reconciled.
- README.md: optimizer claim scoped per-chain (was "for any input ruleset";
multi-chain/hook preservation is the separate compile_ruleset/hook family,
not composed with the optimizer); broken Optiplex_Antispoof.v link fixed.
Declaration keyword changes (proof terms identical, statements verbatim):
compile_chain_sets_correct and compile_chain_faithful_jumpfree
Theorem->Corollary; faithful_table_jump_drops, compiled_table_jump_drops,
rg_base_not_jumpfree Theorem->Example under a "Regression pins (DEMO)"
header. Deleted the unused trivial Lemma optimize_chain_eval_any_env
(Optimize_Table.v; a vacuous `-> True` placeholder referenced nowhere).
No theorem statement changed; every pre-existing headline survives verbatim.
Gates: make proofs OK; make corpus 2532/2532, 0 mismatches; make validate
28/28; make parse-test OK; make axioms 10/10 "Closed under the global
context".
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…mment-only) Every load-bearing comment now states the invariant that holds today (with its kernel citation) instead of the history of how it came to hold. Zero definition or proof changes: a comment-stripped diff of all 41 touched .v files is empty, verified mechanically; every theorem statement survives verbatim. - Red_*.v (11 files): headers keep the kernel-truth paragraph and the model mechanism, drop the RED-probe/BLUE-fix war stories, and gain one 'Regression gate:' line naming the theorems that lock the invariant in and the model regression that would make them unprovable. - All 16 'Round N' cross-references (Router_Hooks/Forward/Realistic/NatHook, Red_NatReplyDir/NatPerPacket, Semantics, Dnat_Rewrite, Ip6_Nat, Optiplex_Mark) now cite the concrete theorem/module names they always meant (e.g. Router_Input.world_ingress_locked_down); Round refs in the hand-written extracted/ glue comments removed likewise. - 'the old X / formerly-provable / previously / no longer' contrasts rewritten as positive present-tense invariants; negative regression lemmas stay but are documented as 'the naive flat/unpadded/ASCII/exact-equality alternative is refuted', with the concrete wrong term inlined (Bytes.v byteorder, Concat_Iv, Ifname_Exact, Iif_Index, Ct_State, Tcpflag, Payload_Break, Limit_Over, Synproxy, Ip6_Nat, Dnat_Rewrite). Phantom identifiers ([Limit_Inert_RED.rate_is_inert], [ctmark_matches_untracked_BUG]) removed. - 'gap G2/G3/G4' labels retired (two audit branches assigned the same numbers to different shapes); passes now carry the self-describing battery-shape names, and DEVELOPMENT.md gains an 11-row nft -o fold-shape ledger (shape / example fold / pass module / fidelity status). - Packet.v: e_ifaddr/ifaddrs_of are denotational specs (inet_select_addr at RT_SCOPE_UNIVERSE / the one-primary-address list); the stale [e_ifaddr_ifaddrs_of] reference now names [inet_select_ifaddrs_of]; the e_nat tuple doc lists all four components. - Essay sites compressed to <= 15-line invariant-first comments: Optimize_Mapn D1 (points at eval_rules_mut_map_merge + e2e.sh §B6), the Packet.v e_numgen field (detail moved beside env_numgen_upd in Semantics.v, 4-line pointer left), Nftval.v header (drops CRUCIAL, cites encode_VPort_80/meq_encode_agrees as the enc_atom-agreement evidence). - Syntax.v header now states what the file is: a lowered, byte-level rule IR whose typed-surface->IR elaboration is UNVERIFIED OCaml (extracted/nft_lower.ml: kind, enc_atom), with Nftval.v as the verified typed view. Theorem statements changed: none. Gates: make proofs green; corpus 2532/2532, 0 mismatches; validate 28/28; parse-test all passed; make axioms all 'Closed under the global context'. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… per side, derived _mut stratum, source-side mut_wf
Type signatures no longer lie about state. The five findings this closes:
A. The dead per-packet conntrack oracle pkt_ct is GONE from Record packet
(no evaluator read it: do_load's LCt case reads the flow-keyed e_ct), with
every packet literal, with_pkt_* setter, and glue site updated, and the
ct_writable / pkt_numgen comments rewritten in present tense to the
e_ct/e_numgen dataflow.
B. ONE step function per rule per side: Semantics.dsl_rule_step (DSL) and
vm_rule_step (VM) each package (guarded verdict, (env, packet) left:
writes + numgen advance + limiter consumption); every mutation/trace
evaluator (eval_rules_mut/_mut_env, run_program_mut/_mut_env,
eval_rules_trace, trace_nat_drops) pattern-matches on them, so the
verdict/effect composition is written once. The DSL/VM agreement is the
single equation Correct.vm_rule_step_compile_rule.
C. The _mut stratum is DERIVED, not re-proved: eval_rules_mut_env_fst /
run_program_mut_env_fst (+ chain-level forms) prove the _mut evaluators
are fst-projections of the _env ones; run_program_mut_compile_chain /
compile_chain_mut_correct now rewrite with the fst lemmas instead of
duplicating the induction.
D. mut_wf is stated on the SOURCE AST: its numgen conjunct is the syntactic
Semantics.rule_numgen_free; Correct.numgen_free_compile_rule proves it
EQUAL to the bytecode-side numgen_free_prog (compile_rule r), and
Correct.mut_wf_prog_eq restates the old body verbatim. No Definition used
as a compile_*_correct hypothesis mentions compile_rule.
E. THE STATE SPLIT: Record packet no longer carries the mutable cross-packet
world. pkt_env is gone; every evaluator takes the env as an EXPLICIT
argument and the mutation evaluators RETURN the env they leave:
eval_rules : list rule -> env -> packet -> option verdict
eval_rules_mut_env : list rule -> env -> packet -> option verdict * env
eval_rules_trace : ... -> env -> packet -> option verdict * (env * packet)
do_load/field_value/eval_matchcond/outcome thread the env; loadability
predicates (match_loadable, body_loadable_walk, synproxy_stops, ...) take
only the packet, so env-stability of loadability is now a TYPING fact.
All three set_env* definitions (set_env, set_env_dynset,
set_env_dynset_map) and with_pkt_env are deleted; the dynset writes are the
env-level env_set_upd/env_map_upd. Demo/witness/optimizer files and the
hand-written OCaml glue (parse_test.ml, semtest.ml: test packets are now
explicit (env, packet) pairs) are migrated.
STATEMENT CHANGES (the complete list; everything else is verbatim):
1. State-split re-quantification (Step E): every theorem over packets now
quantifies forall (e : env) (p : packet) instead of one bundled packet.
For each pre-split HEADLINE the old claim is restated as an explicit
corollary over the bundled pair Packet.pstate (ps_env/ps_wire) in Main.v,
proved by exact/apply of its successor (axiom-free, Print Assumptions
guarded):
pre_split_compile_chain_correct
pre_split_compile_chain_mut_correct
pre_split_compile_chain_mut_env_correct
pre_split_compile_seq_mut_correct
pre_split_compile_table_correct
pre_split_compile_ruleset_correct
pre_split_compile_hook_correct
pre_split_compile_seq_correct
pre_split_optimize_table_uncond_correct
pre_split_optimize_table_uncond_compile_correct
2. Definition mut_wf — third conjunct is the source-side rule_numgen_free
(pointwise EQUAL to the old numgen_free_prog (compile_rule r) by
numgen_free_compile_rule; old body restated verbatim by mut_wf_prog_eq).
3. Internal lemma vm_step_dsl_step deleted — subsumed by the strictly more
informative vm_rule_step_compile_rule (its snd component).
4. Red_CtMark_Crosspkt.flow_mark_overrides_packet2_oracle — the vacuous,
unused hypothesis `pkt_ct p2 CKmark = [9]` is dropped; conclusion
unchanged (statement strictly stronger).
5. The mutation/trace evaluator Fixpoints are restructured over the
transparent step functions (definitionally the same evaluators).
6. Optimize_Uncond's env-stability lemmas for loadability
(set_untracked_set_env, body_item_loadable_env, body_loadable_walk_env,
body_synproxy_stops_env) are deleted: their statements are now typing
facts (loadability no longer takes an env).
Gates: make proofs green; corpus 2532/2532, 0 mismatches; validate 28/28;
parse-test ALL PASSED; make axioms 10/10 Closed under the global context;
semtest battery PASS. THEOREMS.md/DEVELOPMENT.md updated to the new
signatures and the pre_split_* ratchet corollaries.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e IR
A reviewer can now read any *_Gen.v term without the OCaml kind table: the
generated sources carry TYPED immediates and structured shapes, elaborated
onto the byte-level IR by a VERIFIED, evaluation-exact function.
1. Typed source layer (Elab.v, new; Nftval.v extended)
- Elab.tmatch: TMEq/TMNeq over Nftval.nftval, MPrefix (CIDR with prefix
length), MWildcard (trailing-* ifname / ct-tuple prefix — the one surface
construct whose meaning IS a short compare).
- elab_m : tmatch -> matchcond total; THEOREM elab_matchcond_correct
(eval_matchcond (elab_m m) = eval_tmatch m, axiom-free, in `make axioms`).
- The CIDR byte-alignment split (truncated-load direct cmp vs full-width
mask) moved from nft_lower.ml into the verified Elab.prefix_expand, with
vm_compute witnesses (prefix_aligned_24 / prefix_unaligned_20).
- Nftval gains VHostInt (host-endian LE integer: mark/ifindex/ct-zone/...);
all round-trip proofs extended.
- The frontend obtains EVERY match immediate through the verified encode:
nft_lower's enc_atom is now literally Nftval.encode ∘ typed_atom, and
every typed-representable match is constructed via the extracted elab_m.
- MEq/MNeq eval clauses now visibly ARE the kernel cmp (eval_cmp CEq/CNe,
definitionally equal to the previous firstn form — zero proof churn):
one predicate, named; the surface distinctions live in the typed layer.
2. One outcome per rule (Syntax.rule restructured)
- Inductive outcome := OVerdict | ONone | OVmap | OVmapNat | ONat | OTproxy
| OFwd | OQueue; rule = { r_body; r_outcome; r_after }. The historical
product (one filler verdict + five optional slots) survives as
Syntax.rule_prod with translation rule_of_prod; RATCHET theorem
Semantics.run_rule_outcome_eq: for every prod_wf product the outcome
evaluation is unchanged (axiom-free, in `make axioms`).
- OVmapNat keeps the genuine vmap-miss->NAT combination expressible
(semtest exercises it; no coverage regression).
- r_verdict/r_vmap/r_nat/r_tproxy/r_fwd/r_queue survive as projection
Definitions over the sum, so evaluator/compiler texts are unchanged;
recognisers in Optimize_{Dnat,Snat,Mapn} now pin r_outcome directly.
3. MMasked polarity honest (bool -> cmpop)
- MMasked carries the comparison operator; the eval clause is eval_cmp op.
- MFlagsSet f bits names the positive implicit-bitmask idiom
((field & bits) <> 0, CNe) that previously read as `neg := true`.
4. Enums instead of strings (Bytecode.v)
- nat_op (NKsnat/NKdnat/NKmasq/NKredir), nat_af (NFip4/NFip6/NFinet),
dynset_op (SOadd/SOupdate/SOdelete) replace the "snat"/"ip"/"add"
strings in nat_spec, SDynset(Imm), INat, IDynset and the whole NAT
data plane (set_saddr/set_daddr/... now take nat_af). Rendering
strings exist only at the codec/netlink boundary (codec.ml, nl_send.ml);
`make corpus` (2532/2532) pins the rendered bytes unchanged.
5. Synthesized dependency tags + set hygiene (frontend/emitter)
- BDep (definitional alias of BMatch) marks frontend-synthesized
protocol-dependency guards in generated sources.
- Anonymous inline sets are deduplicated by encoded contents
(one __setN binding per distinct element list; Optiplex: 19 -> 8).
- Set-declaration elements print as SEl v / SRange lo hi (definitional
views of the stored interval pair, Elab.v), not degenerate ([x],[x]).
- nft2coq emits typed terms: BMatch (elab_m (TMEq FThDport (VPort 22))),
(ifname "home"), (ip4 192 168 51 20), MPrefix ... 24; all four *_Gen.v
regenerated.
Theorem-statement changes (ratchet listing):
- Every pre-existing HEADLINE statement survives verbatim (they quantify
over rule/matchcond, whose types were restructured representation-
compatibly; texts unchanged). Print rule/matchcond/nat_spec show the
new representations.
- orig_dnat_data_shape / orig_snat_data_shape now conclude
r_outcome r = ONat (…imm_spec T) (previously r_nat r = Some (...) —
equivalent via the r_nat projection).
- is_orig_{dnat,snat,map} recognisers pin the outcome constructor instead
of the five-slot filler pattern (same accepted set on frontend shapes).
- rule_end_eqb compares (r_outcome, r_after) instead of 7 projections
(rule_end_eqb_mk_head restated 1:1).
- New: Elab.elab_matchcond_correct, Semantics.run_rule_outcome_eq —
both in the make axioms gate.
Proof-engineering note: Tutorial_Proofs.v's two prefix-goal reductions use
vm_compute, not cbn — the regenerated typed Gen terms put
[encode (ip4 a b c d)] with VARIABLE bytes next to a closed elaborated
prefix, a mix cbn diverges on and vm_compute reduces instantly. Concrete-
packet demo layers should prefer vm_compute over cbn on elab_m residuals.
Gates: make proofs green; make corpus 2532/2532, 0 mismatches;
make validate 28/28; make parse-test ALL PASSED; semtest PASS;
make axioms: 12/12 Closed under the global context
(gate names qualified where needed: Semantics.run_rule_outcome_eq).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…s, one optimizer convention
The 88-file flat theories/ namespace is now organised by trust role, so the
directory listing answers "what must I read to trust the theorem":
Core/ Bytes, Verdict, Packet, Bytecode
IR/ Syntax, Nftval, Elab
Semantics/ Semantics, Fib_Local, Netstate_MultiAddr
Compiler/ Compile, Correct, Main, Extract
Optimizer/ the nft -o passes + Table/Table_Inv/Uncond composition
Optimizer/Witness/ fires-witnesses, all Optimize_<Shape>[_<Arm>]_Witness.v
Regression/ kernel-behaviour gates, named after the invariant they pin
Examples/ worked per-configuration proofs + their shared engine
Generated/ nft2coq output (*_Gen.v; make gen now writes here)
Pure moves and alpha-renames; zero statement changes. The single
`-Q theories Nft` mapping is kept; `From Nft Require Import <name>` resolves
by suffix (as with Stdlib), so imports were untouched by moves and only
renamed modules were rewritten.
Audit-log file names replaced by invariant/shape names:
Red_NumgenProbe > Numgen_RoundRobin Red_CtMark_Crosspkt > CtMark_CrossPacket
Red_LimitProbe > Limit_SharedBucket Red_Ct_Untracked > Ct_Untracked_Break
Red_Exthdr_Probe> Exthdr_Absent_Break Red_LinkLayer > LinkLayer_MacGuard
Red_NatNoAddrDrop > Nat_NoAddr_Drop Red_NatPerPacket > Nat_FlowStateful
Red_NatReplyDir > Nat_ReplyDirection Red_Notrack > Notrack_CrossRule
Red_NotrackIntra> Notrack_IntraRule Concat_Iv > Concat_Interval
One optimizer naming convention (pass file Optimize_<Shape>.v, entrypoint
optimize_chain_<shape> lowercase; every stem in Optimize_Table.v maps 1:1
case-insensitively onto its pass file):
setsN>valueset (Optimize_Merge>Optimize_ValueSet) mapn>datamap (Mapn>DataMap;
"BareMap" would mislabel it - the bare-map passes are Dnat/Snat)
vmapN>vmap, concatN>concat (the superseded 2-adjacent-rule stratum frees the
stems as optimize_{rules,chain}_{vmap2,concat2}, matching optimize_chain2)
vmapNg>vmapguarded (Vmapg>VmapGuarded) setg>setguarded (Setg>SetGuarded)
concatK>concatmulti (ConcatK>ConcatMulti) concatM>concatguarded (>ConcatGuarded)
ivset>intervalset (Ivset>IntervalSet) ivsetg>intervalsetguarded
ivsett>intervalsethostorder (Ivsett>IntervalSetHostOrder)
ivmixg>mixedpointrangeguarded (Ivmixg>MixedPointRangeGuarded)
dscpv>dscpvmap (Dscpv>DscpVmap) Ctmask>CtMask
The three witness conventions fold into one: Snat_Witness, Concatm_Witness,
Ivset(g)_Witness, Setl2_Witness, Metaset_Witness, Vmapgn_Witness are now
Optimize_<Shape>[_<Arm>]_Witness.v under Optimizer/Witness/.
Alpha-renames of non-pass identifiers (statements verbatim): the seam lemma
optimize_chain_clean is optimize_preserves_rules_clean (it is not a pass, so
it no longer wears the optimize_chain_<stem> shape); the refuted-alternative
pins drop their audit-log names (fix_changes_behaviour >
refuted_alternative_diverges in 4 files; old_flat_wrongly_accepts >
flat_lex_wrongly_accepts; old_meq_wrongly_rejects{,_synack} >
refuted_meq_rejects{,_synack}; m_estab_old/m_syn_old > *_refuted;
old_unpadded_wrongly_accepts_prefix > refuted_unpadded_accepts_prefix).
Every pre-existing HEADLINE statement survives verbatim (compile_hook_correct,
compile_seq_correct, compile_seq_mut_correct, compile_chain_correct strata,
optimize_table_uncond_correct, optimize_table_uncond_compile_correct,
elab_matchcond_correct, run_rule_outcome_eq, the pre_split_* ratchets).
Infra: _CoqProject lists the new paths; make gen emits into Generated/ (nft2coq
usage comment updated); make clean and proof/.gitignore are recursive over the
role subdirectories; stale extracted modules for renamed files removed
(regenerated under the new names); THEOREMS.md/DEVELOPMENT.md gained the role
directory map; CONFIG_PROOFS.md, battery_cases/README.md, README.md, NOTES.md
references updated.
Gates: make proofs green; make corpus 2532/2532, 0 mismatches; make validate
28/28; make parse-test ALL PASSED; make semtest PASS; make axioms 12/12
"Closed under the global context"; make gen regenerates byte-identically.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…EADME, gen-check, make gates, mut_wf + nat-overflow discharged at the tool boundary Every README-advertised guarantee is now behind a build-FAILING mechanical check, and the two advertised-but-unchecked tool-boundary properties are actually checked: - make axioms now gates all 41 claimed theorems (was 12): + antispoof_general and its 3 concrete corollaries, Example_Ruleset.established_accepted, both Netstate_MultiAddr masquerade theorems, all 17 Fib_Local heads, all 5 Ct_State theorems. In-file Print Assumptions lines relabelled "informational" (they cannot fail a build); missing prints added (Ct_State had zero, Optiplex_Antispoof printed 1 of 4, Netstate_MultiAddr missed masq_drop_iff_no_eligible_addr). THEOREMS.md §4 states the rule: the gate follows the claim, in the same commit. - make gen-check: byte-diff every checked-in theories/Generated/*_Gen.v against fresh nft2coq output, ALL FOUR rulesets — router.nft added to make gen (it was regenerated by no target). A stale Gen file is no longer a valid proof about a ruleset that is not the deployed one. - make gates: proofs axioms corpus validate parse-test gen-check, in sequence; DEVELOPMENT.md "Enforcement model" answers the enforcement-point question honestly (no CI; per-commit history unknowable; workflow revert-on-red binds only agent runs; NOTES.md byte-order near-miss cited). - mut_wf discharged at the tool boundary: is_mut_stmt/mut_wf moved to the Semantics stratum (Correct.v keeps them as Notation abbreviations — every theorem statement and proof verbatim, mut_wf_prog_eq intact), mut_wf extracted, parse-test asserts forallb mut_wf over every chain of all four rulesets + a hand-broken detector pin, nftc warns on violating chains. - ExtrOcamlNatInt seam: the frontend REJECTS scaled limit rate/burst > 2^40 (limit_value in parser.mly, re-checked in nft_lower.limit_spec), keeping every extracted product under 604800 * 2^41 < 2^62; oversized literals are a clean lexer error (was an uncaught int_of_string crash; limit rate 9000000000000 mbytes/second silently wrapped into wrong bytecode). Classification comment beside the Extract.v import; TCB paragraph in DEVELOPMENT.md; parse-test pins the rejection. Gates: proofs green; axioms 41/41 Closed under the global context; corpus 2532/2532, 0 mismatches; validate 28/28; parse-test ALL PASSED (incl. new mut_wf + natint sections); gen-check 4/4; make gates exit 0. Negative probes verified and reverted: Admitted in Ct_State fails make axioms; byte-edited Optiplex_Gen.v fails gen-check. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three confirmed model-vs-kernel divergences (shared by DSL and VM, so no
gate or compile theorem ever moved) become a single discoverable ledger
instead of implicit lore, with checked ratchets:
- DEVELOPMENT.md gains "Known model infidelities (open, confirmed)": (1)
the whole-body limiter sweep drains limit/quota/connlimit past a failing
earlier match (kernel NFT_BREAKs first); (2) an OVmapNat vmap HIT still
runs nat_drops/apply_nat in eval_rules_trace, rewriting the packet and
spuriously storing a flow-keyed e_nat mapping (kernel: a hit ends the
rule); (3) intra-rule set-then-read (`meta mark set 0x1 meta mark 0x1
accept` as ONE rule) drops in the model, accepts in the kernel. Each
entry: kernel citation, code location, repro, why open (semantics change
= adversarial-audit track). Cross-linked from THEOREMS.md scope notes,
adversarial.md's Outcome ("red satisfied" now scoped), and the README.
- New Regression/Known_Infidelities.v: vm_compute pins that LOCK IN the
divergent model behaviour (gate_limit_drained / vmaphit_daddr_rewritten
+ vmaphit_stores_nat_mapping / setread_dropped, with VM twins) — a
fidelity fix must consciously flip a pin and update the ledger.
- Comment corrections where text asserted kernel exactness the code lacks:
the limiter-sweep/set_limit/env_limit_upd headers, run_rule's
IMetaSet/ICtSet clause (incl. the stale "covered by the corpus, not
Rocq"), eval_rules_trace's NAT dispatch, Syntax.v's OVmapNat doc,
mut_wf's "one residual mutation case" (both files), and
Notrack_IntraRule.v's over-general intra-rule-threading header.
- Optimizer scope: the pipeline headline is verdict-only over the
write-blind eval_chain; the per-stage effect certificates (datamap mut
merge, dnat/snat apply_nat_eq) are per-merge-shape lemmas NOT composed
through optimize_table — stated on the headline (Optimize_Uncond.v
scope note 2), in THEOREMS.md, and Optimize_Table.v's fidelity contract,
with the not-lifted rationale.
- numgen asymmetry: rationale at dsl_step (why no DSL-side numgen sweep;
its cost: Numgen_RoundRobin's behaviour is VM-only, never
compiler-preserved); the M3 "ONE step function per side" header no
longer claims a DSL-side numgen advance; DEVELOPMENT.md + THEOREMS.md
carry the caveat.
- mutation x jump: why the mut strata carry mut_wf but no chain_jumpfree
hypothesis (rationale block in Correct.v, parallel to the fidelity
bridge), plus the executable pin mut_strand_jump_pin (a mut_wf,
jump-bearing chain inside the theorems but outside the faithful domain).
No semantics change; every pre-existing theorem statement verbatim (diff
is comments + new Example/pins only). Gates: proofs ok, axioms 41/41
Closed, corpus 2532/2532 (0 mismatches), validate 28/28, parse-test ALL
PASSED, gen-check ok.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… evidence ledger, elab boundary, pkt_flow rationale, fuzz-gate rationale, byteorder/jhash Doc/comment-only (zero proof-term changes; all touched .v files compile, gates re-run): - Corpus oracle: README + DEVELOPMENT state the 2532/2532 gate's direction (payload-reconstruction round-trip FIXED POINT, not a source diff), name the independent cross-checks, and record the measured source-side numbers (1742 headered blocks: 1142 = 65.6% compile-from-source byte-identical, 517 loud frontend gaps, 83 mismatches in unadjudicated display-vs-wire classes) plus why the full source gate is deliberately NOT wired in (it would be red on open questions); NOTES.md carries the widen-the-gate TODO; byteorder-gate.sh states its scope rationale. - Evidence ledger: every adversarial.md fix bullet now carries an (a)/(b)/(c) evidence-class tag (kernel-executed / C-source+golden-bytes / Coq repro); Outcome gains a scoping note: 'kernel fidelity' = fidelity-to-source-as-read except where an (a) tag exists; NOTES.md still-to-adjudicate cross-linked. - Elab boundary: Syntax.v/Elab.v headers, THEOREMS.md and DEVELOPMENT scoped from 'every match immediate' to the four tmatch shapes, naming the raw-bytes residue (set/map elements incl. OCaml CIDR expansion, range endpoints, vmap keys, NAT/tproxy targets, mangle/vsrc immediates, bitwise masks); CONFIG_PROOFS.md gains the 'what the Gen bytes rest on' trust paragraph. - pkt_flow: Packet.v states why the ct/NAT key is an opaque parametric oracle, the injective-canonicalisation assumption transfer rests on, and flow_wf (a Fib_Local-style additive layer) as the designated de-oracling step; honest-gaps bullet + THEOREMS.md scope note added; stale ct_wf pointer replaced with the real Ct_Flow.v flow_is_new entry-state invariant; pkt_fibkey comment now names its four pinned selectors. - Fuzz gate: DEVELOPMENT's false 'not extracted' claim corrected (semtest runs the extracted packet semantics — but against repo-authored expectations, no external oracle); a written answer to 'why no at-scale data-plane differential' (generator effort / limiter observability / privileges, with the existing ingredients named). - Bytes.v: data_byteorder docstring now matches the code (ignores hton — kernel-faithful — and len, with the producer invariant that makes the dead len safe); data_jhash carries the fails-by-design caveat and joins the eyeball-trusted list; DEVELOPMENT's 'len-byte element' corrected to size-byte; STILL-OPEN entry cross-links both. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…cuized
Fuel strand (Semantics.v § "Fuel discipline for the jump strand"):
- eval_rules_jx makes fuel exhaustion observable (None = exhausted,
Some o = clean run with eval_rules_j result o); erjx agree/monotone/
stable lemmas give the CORRECT monotonicity (eval_rules_j_fuel_stable).
- Naive monotonicity (eval_rules_j fuel = Some v -> S fuel = Some v) is
FALSE: machine-refuted in-file (eval_rules_j_not_naively_monotone,
Some Accept at fuel 2 vs Some Drop at fuel 3 on a two-chain probe).
- Adequacy: computable sufficient_fuel + chain_ranked (the semantic
shadow of nft's load-time jump-loop rejection; kernel bound
NFT_JUMP_STACK_SIZE=16 cited) => every run clean, verdict fuel-
independent (eval_rules_jx_adequate / eval_table_fuel_indep), policy
fallback provably genuine fall-through; chains_no_transfer discharges
chain_ranked by reflexivity for jump-free environments.
- VM mirror via the compile bridge: Correct.run_table_fuel_indep_compiled.
- User surface: Nft_Tactics.nft_{yields,accepts,drops}_fuel_indep;
Tutorial_Proofs.tutorial_blocks_exactly_any_fuel (headline verbatim at
every fuel >= 4); CONFIG_PROOFS.md "Choosing the fuel budget";
semtest.ml fuel constant documented against the bound.
gen_env de-vacuization:
- Optiplex_Mark: e = gen_env + fib-local hypotheses proved jointly
unsatisfiable (genenv_fib_local_contradiction); all pinned lemmas/
theorems restated _real over the three e_set contents the chain reads
(Router_Realistic pattern); originals kept VERBATIM as SUPERSEDED-
vacuous corollaries of the contradiction; concrete witness
env_stream/pkt_stream (real local route + wf fibkey) discharges every
_real hypothesis jointly; headline slot -> streaming_flow_whole_ruleset_real.
- Optiplex_Antispoof: the pin was INERT — antispoof_general_any_env drops
it (same proof minus the ?Henv rewrite); pinned original survives as a
corollary; rationale comments on both and on the (satisfiable) concrete
corollaries.
- Router_Input:379 false "NOT vacuous" claim corrected with the
ctstate_under_genenv_never_new cross-reference; Router_Forward/Private/
Hooks headers now point at the Router_Realistic *_real successors.
- Same ct-pin vacuity in Example_Ruleset/Ruleset_Verified/Nft_Demo_Symbolic
marked in-file and ledgered OPEN (THEOREMS.md §5, README scope note) —
not silently rewritten.
Docs/gates: CONFIG_PROOFS.md new recipes ("Pin only what the lookups
read", "Choosing the fuel budget") + stale pkt_env notation fixed;
THEOREMS.md §3 fuel-adequacy entry, §5 config-proof claim table, gate
count 41->55; DEVELOPMENT.md workflow soundness rules; Makefile
AXIOM_GATE_THEOREMS extended (all 55 Closed under the global context).
Gates: proofs green; axioms 55/55 Closed; corpus 2532/2532, 0 mismatches;
validate 28/28; parse-test ALL PASSED; gen-check 4/4; semtest PASS.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…pechecker gate
Purely additive: the untyped surface tree, nft's datatype lattice, ALL
symbolic-constant tables, the selector->dtype map, and a coercion-aware
typechecker are now Coq definitions, extracted and wired into parse-test
as a gate. The OCaml lowering is untouched (byte parity is asserted, not
migrated — that is M2+).
New (theories/Surface/):
- Ast.v: constructor-for-constructor mirror of extracted/nft_ast.ml. int
crosses the ExtrOcamlNatInt seam guarded (negative / >= 2^40 rejected at
injection); negative chain priorities cross in sign-magnitude form.
- Datatype.v: dtype enum covering nft_lower.ml's 24-kind table + the 8
declared-set type atoms + the chain-interior bitmask/string types;
dt_width (bits, bit-precise: dscp is 6), dt_bytes, dt_byteorder (host
set = {mark, ifindex, fib_addrtype} + host integers), basetype_of
implementing datatype.c's chains (ct_state -> bitmask -> integer;
inet_service -> integer+BE; mark -> integer+host; ifname -> STRING),
coercible/dt_compat/int_basetype/lit_fits. Cited against
/tmp/nftables-src/src/{datatype,ct,meta,proto,fib}.c.
- Symbols.v: all 17 sym_* tables + tcpopt/syslog/reject/nat-flag/ct-dir
tables as dt_syms_* data with NUMERIC values (bytes only ever come from
Nftval.encode); lookup_symbol walks the basetype chain with the
evaluate.c integer-literal fallback; tables_fit_their_dtype pins every
table value inside its dtype's declared width.
- Selector.v: key_field's ~100 selectors as a table + the parametric
fib/ctdir/tcpopt families -> (Syntax.field, dtype, dep specs); bitfield
table as sub-byte NUMBERS (bit width + shift, not byte masks);
selector_widths_agree/bitfield_widths_agree re-check every row's dtype
width against the IR load width by vm_compute.
- Typecheck.v: resolve_value normalises spelling (symbol and numeric forms
hit the IDENTICAL nftval through the shared resolve_num); ifname_bytes
(exact/wildcard/escaped-star) in Coq; define expansion (fueled: cyclic
defines fail loudly, the OCaml resolve_var would diverge);
typecheck_clause/rule/ruleset covering matches, concat matches, vmaps,
set declarations/references (declared-type compatibility via the
coercion lattice), bitwise (integer-basetype only), bare comma lists
(bitmask-basetype only, evaluate.c:1871), statements.
Theorems (axiom-free): resolve_num_wf, resolve_num_width,
resolve_num_byteorder (the kind table's width/byteorder decisions as
theorems, not just tables), symbol_numeric_same_term (the same-typed-
term guarantee in general form), resolve_value_wf (wf modulo the
deliberate short ifname wildcard). Pinned Examples incl.
ct_state_symbol_numeric_same_term, reject_iifname_and_0xff,
kind_table_widths_and_byteorders.
Boundary groundwork (M-C):
- extracted/nft_inject.ml (new): the ONLY OCaml->Coq translation site,
pure structural constructor mapping with the 2^40/negative nat-seam
guards.
- extracted/parse_test.ml: gates (a) TYPECHECK-RULESETS 4/4, (b)
ILLTYPED-REJECT 7/7 over new proof/tests/illtyped/ (cross-type bitwise,
unknown symbol, width overflow, set-type mismatch, comma list on ports,
undefined define, ct-state-vs-service), (c) KIND-PARITY 24/24: per kind,
unverified enc_atom bytes == verified encode(resolve_value) on
byteorder-revealing values, + the 8 set-type atoms (temporary
scaffolding; dies with the OCaml kind table).
- theories/Compiler/Extract.v: extract the surface layer; realise
String.length natively (Stdlib.String.length == Coq String.length under
the native-string+nat-int seams) so re-extraction no longer emits a
String.ml that shadows Stdlib.String inside the nftc library;
extracted/dune additionally excludes any stray String module (fresh
re-extraction previously broke dune - latent since the seed_start
change, exposed by this milestone's re-extraction).
No theorem statements changed; no existing theory file modified except
Extract.v (extraction wiring only). All gates green: proofs, axioms
(all 44 'Closed under the global context'), corpus 2532/2532 with 0
mismatches, validate 28/28, parse-test (incl. the three new gate lines),
gen-check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…s constructing byte-level scalar matchconds
Every scalar match shape now lowers through extracted Coq:
- theories/Surface/Typed.v: the typed match-term language beyond Elab.v's
four shapes — TXRange (datatype byteorder decides plain-BE range vs the
mandatory `byteorder hton` path with BE re-encoded bounds), TXBitmask
(ct state/status, tcp flags: implicit/bang/==/!= over an OR-fold, comma
lists), TXBitfield (dscp/flowlabel/doff/vlan/frag: mask+shift COMPUTED in
Coq from Selector.v's numeric bit specs), TXBitwise (and/or/xor mask
matches), TXFlag (fib/exthdr/tcpopt presence) — with the total verified
elaboration elab_tx onto the byte IR, byte-pinned by vm_compute Examples.
- theories/Surface/Lower.v: lower_match/lower_bitmatch — symbol resolution
and coercion via Typecheck.resolve_value (`ct state 2` = `ct state
established` at the typed-term level, `iifname & 0xff` refused), CIDR/
bitfield range admission, dep_guard (family-aware guard VALUES encoded in
Coq) and discharge; every refusal an explicit lerr, never a silent OCaml
byte fallback.
- theories/Semantics/TypedEval.v: INDEPENDENT partial semantics — decodes
register bytes at the shape's datatype and compares numerically in N;
whole-word-free of encode/data_eqb/firstn/eval_matchcond/elab_m (gated);
stuckness (None) is reachable and demonstrated (unadjudicated host-endian
range class, width mismatch, undecodable stored value, byteorder-
incoherent operand), unloadable fields are Some false (NFT_BREAK).
- theories/Surface/Lower_Proofs.v: NON-definitional erasure theorems with
real obligations — range_erasure_be (byte-lex = numeric, same-width BE),
range_erasure_host (the hton re-encoding: the historical core-byteorder
bug class, proved not tested), bitmask_erasure (encode of OR-fold vs
N.land), bitfield_erasure (mask/shift bytes vs numeric shift/mask),
bitwise_erasure, flag_erasure, composed txmatch_erasure; plus typed-vs-
compiled agreement of the verified lowering outputs.
- Makefile: AXIOM_GATE_THEOREMS += Lower_Proofs.{range_erasure_be,
range_erasure_host,bitmask_erasure,bitfield_erasure} (all print "Closed
under the global context").
- extracted/nft_lower.ml: now a DRIVER — scalar CMatch/CBitmatch paths and
dep-guard/discharge values route through extracted Lower; the old atom/
range/hton-range/bitmask/bitfield/presence/wildcard byte branches, the
4-operator dispatches, bitfield_sel/mask_shift, and every construction or
pattern of the byte-level eq/neq/masked/range matchcond constructors are
DELETED (grep-gated at 0, comments included). Only the untyped set/map
paths (M3) and statement immediates (M4) still encode bytes here.
- theories/Compiler/Extract.v, _CoqProject: wire the new modules into the
build and extraction (additive only).
Theorem-statement changes: NONE. Every pre-existing headline theorem
survives verbatim; Elab.v (tmatch/eval_tmatch/elab_matchcond_correct) is
untouched. All gates green: proofs, axioms (incl. the 4 new erasure
theorems), corpus 2532/2532 with 0 mismatches, validate 28/28, parse-test,
gen-check; byteorder-gate.sh and difftest.sh pass.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ments, CIDR intervals, concat slot padding, interning
All set/map/vmap byte composition moves into the VERIFIED Rocq lowering; the
OCaml frontend no longer composes a single set byte and no longer constructs
MSetT/MConcatSet. New verified Lower.v functions (Surface/Lower.v):
- value_interval / cidr_interval / data_or: point / range / CIDR (net +
broadcast) element intervals, built from the SAME Elab.prefix_mask/data_and
arithmetic as Elab.prefix_expand (one CIDR expansion, no OCaml duplicate);
- the host-endian interval MSetT[TByteorder] path with big-endian bounds
(Typed.encode_be), taken exactly when the field is host-endian AND the set
has an interval element; set_has_interval decided in Coq;
- concat_intervals + pad_slot + concat_padded: concatenated set tuples with
4-byte register-slot padding; concat_flat: the FLAT unpadded vmap-key form;
- typeatom_dtype + decl_elem_interval: the 8 declared set type atoms;
- lstate + intern_set/fresh_map/add_*: content-dedup __setN/__mapN interning
as a state-passing fold (nat_dec extracts to string_of_int, an injective/
decimal naming seam re-checked end-to-end by corpus + gen-check);
- lower_anon_set / lower_set_ref / lower_concat_set / vmap_entries_* /
decl_set_elems / decl_vmap_ents: the entry points the frontend calls.
Independent numeric membership in Semantics/TypedEval.v (iv_mem_N / set_mem_N /
field_mem_N), decode-and-compare in N, no encode.
Three NON-definitional erasure theorems (Surface/Lower_Proofs.v), all axiom-free
and gated in `make axioms`:
- set_interval_erasure: byte-level set_mem over ENCODED interval bounds equals
numeric membership over DECODED values (byte-lex = numeric, same-width BE;
reuses M2 data_le_num);
- concat_key_erasure: the slot-padded concatenation is faithfully invertible —
split-and-truncate recovers each field's own bound (split_by_recover
injectivity), so a concatenated key's membership is the per-field cross
product (the historical padding bug, now proved);
- cidr_interval_agrees_prefix_expand: for every prefix length, membership in
the CIDR net..broadcast interval equals Elab.prefix_expand's masked-prefix
compare (prefix_mask_val closed form + the land-with-prefix-mask =
shiftr/shiftl fact) — the two-implementations tension is gone.
Non-vacuity Examples for all three (vm_compute, member true / non-member false).
OCaml (extracted/nft_lower.ml): the set/vmap/decl paths call the extracted Coq
lowering and thread Lower.lstate; DELETED interval_of_value, interval_of_value_be,
interval_of_decl_elem, bytes_of_typeatom, pad_to_slot, reg_slot, prefix_mask,
band, bor, set_has_interval, intern_elems, intern_anon_set, intern_anon_set_be,
intern_anon_concat — and the now-orphaned key_field, enc_atom_be, width_of_kind.
parse-test's set-type-atom parity check now exercises Lower.decl_set_elems.
No pre-existing theorem statement changed; Elab.v and Typed.v untouched. Makefile
axiom gate += set_interval_erasure, concat_key_erasure,
cidr_interval_agrees_prefix_expand. All gates green: proofs, axioms, corpus
2532/2532 with 0 mismatches (set/map element lines 651/642/9 unchanged), validate
28/28, parse-test, gen-check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…o structural injection (M-C grep-zero)
The last value->byte OCaml dies. Every remaining encoding decision moves into
the VERIFIED Coq lowering, and the whole driver becomes a Rocq function; the
OCaml frontend is now pure structural injection + the ifindex oracle + a call.
Coq (theories/Surface/Lower.v):
- statement immediates: `meta <k> set` / `ct <k> set` register widths from the
datatype lattice (mark/priority 4B, pkttype 1B; zone 2B, label 16B,
mark/event 4B), the immediate encoded via Nftval.encode (round-trip-proved)
— replaces meta_set_kind/ct_set_kind/enc_atom/typed_atom and the 17 symbol
tables (all now dead in OCaml and deleted);
- NAT/tproxy terminals: masq/addr/portonly/redir specs, IPv4-literal targets,
2-byte BE ports, nat flag bits + PROTO_SPECIFIED, l3-family; non-literal NAT
degrades to bare Accept EXACTLY as before, undefined $var is a loud lerr;
- reject family-default + explicit icmp/icmpv6/icmpx/tcp-reset type/code tables;
- syslog level canonicalisation; limit unit + MLimit (the 2^40 seam guard stays
ONLY at the OCaml injection boundary);
- lower_ruleset : (string -> option nat) -> sruleset -> lres lowered_ruleset:
define ($var) expansion, the clause fold with family-aware dependency-guard
dedup + discharge, outcome assembly (every refusal an lerr constructor),
chains/tables, declaration-then-chain interning order — mirrors the retired
OCaml driver byte-for-byte (corpus/gen-check/validate re-check end to end).
Witnesses (theories/Surface/Lower_Examples.v): lower_dnat_addr_port_example,
lower_ct_mark_set_example, lower_tproxy_port_example (pinned bytes), a
kind_encode_coverage Example pinning the lattice's width/byteorder across BE and
host-endian registers (the coverage the deleted OCaml KIND-PARITY test held), and
three fail-loud lerr witnesses.
OCaml: extracted/nft_lower.ml DELETED (1028 lines). extracted/nft_inject.ml is
the sole untrusted site: structural Nft_ast -> Ast.sruleset injection (+ the 2^40
nat seam), the single ifindex oracle ("lo"->1), a call to Lower.lower_ruleset,
and structural read-back into the [parsed] record + typed_of/is_dep for the
emitter. Consumers rebound Nft_lower.* -> Nft_inject.*; the temporary KIND-PARITY
scaffolding (which read the OCaml kind table) is removed; the illtyped harness now
also counts a Coq-lowering lerr as a rejection, and four statement-level reject
files (unknown reject code / nat flag, non-literal tproxy, vmap+static verdict)
grow the suite to ILLTYPED-REJECT 11/11.
No pre-existing theorem statement changed; only additions. make gates green:
proofs, axioms ("Closed under the global context" throughout), corpus 2532/2532
0 mismatches, validate 28/28, parse-test, gen-check (4 Gen files byte-identical).
The full M-C banned-name grep over the frontend is 0 and nametoindex appears once.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…y gate, TCB ledger
The proof-side frontend goes fully typed. nft_emit now prints the SURFACE
ruleset (Definition <name>_surface : sruleset — IP literals via the sip4 smart
ctor, i.e. decimal octets, never a byte list), and each Gen file defines its
tables / chains / decls / hooks as the VERIFIED Lower.lower_ruleset applied to
it (lower_or_empty ifindex_pins <name>_surface, reduced once by Eval vm_compute,
carved by the lr_* projections), guarded by a fail-loud
Example <name>_lowers_ok : lower_ok ifindex_pins <name>_surface = true.
No raw byte is written by hand in any *_Gen.v (grep '\[[0-9]' over the four = 0);
a refused construct breaks make proofs, never a silent OCaml byte.
New Coq (all additive; no pre-existing statement changed):
- Surface/Lower.v: lower_ok / lower_or_empty / empty_lowered / empty_chain /
lr_chains_of / lr_chain_of / lr_hookinfo_of projections; and a fail-loud
LEhook + is_known_hook validation in lower_chain, so a base chain bound to an
unknown netfilter hook is an explicit lower_ok=false (previously an untrusted
OCaml raise inside nft_emit's hook_id).
- Generated/Gen_Support.v (new, NOT extracted): the Semantics-level projections
lr_set_decls / lr_hooks_of / hook_id_of_string, compiled after Semantics and
before the four *_Gen.v.
- Surface/Ast.v: the sip4 smart ctor (grouping only — no byteorder decision).
nft_emit.ml is rewritten: it prints only the untyped surface constructors and
the lr_* projection spellings; it composes NO byte and makes NO datatype /
byteorder decision. nft_parse.ml gains parse_file_surface; nft2coq emits the
surface tree. Downstream identifiers (filter_chains, filter_input, decls,
gen_env, *_hooks, …) keep their exact names and byte-identical values (the
projections Eval-vm_compute to the same literals the lowering produced before),
so every Optiplex_* / Fib_Local / Ct_State / Example_Ruleset / Router_* /
Tutorial_Proofs statement is re-checked verbatim.
make boundary (new gate; appended to make gates and the ALL GATES GREEN line):
(1) the OCaml frontend (nft_ast/nft_inject/nft_parse/nft_emit/nft2coq) has no
value->byte identifier and no symbol table;
(2) extracted/nft_lower.ml stays deleted;
(3) TypedEval.v stays independent of the encode path
(grep -cwE 'encode|data_eqb|firstn|eval_matchcond|elab_m' = 0 — removed the
dead field_mem_N whose firstn was the only hit).
Docs. THEOREMS.md reclassifies elab_matchcond_correct as a consistency check
(reflexivity over an encode-defined eval_tmatch) and maps typed_erasure onto the
Lower_Proofs.*_erasure family; typed_progress / typed_source_vm are recorded as
the owner-descoped whole-language results (deliberately not built this run).
DEVELOPMENT.md documents the now-permanent M-C boundary gate and the three
allowed residues (a) ifindex oracle, (b) structural injection, (c) the
ExtrOcamlNatInt seam. Elab.v's SCOPE comment is corrected (comment-only): its
"unverified frontend bytes / nft_lower.ml composes immediates" paragraph has
been false since M4.
Gates: proofs, axioms (all Closed under the global context), corpus 2532/2532
with 0 mismatches, validate 28/28, parse-test, gen-check (all four), boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…verified Coq
Adversarial-sweep MAJOR: the unverified lexer (extracted/lexer.mll) was
decoding IPv6 literals to their 16 network-order bytes — a big-endian
16-bit-group split `(n lsr 8) land 0xff; n land 0xff` plus `::` zero-run
reconstruction. That is a byteorder/value->byte decision on a live path
(nftc CLI + parse_test), exactly what M-C forbids in the OCaml frontend, and
`make boundary` structurally could not see it (lexer.mll is not in FRONTEND_ML
and the grepped identifiers never matched raw bit-arithmetic). The TCB ledger's
residue-(b) entry falsely claimed the frontend "Decodes nothing".
Fix: full migration. The lexer now carries the literal UN-expanded — its colon
groups (16-bit hex numerals via int_of_string, or an embedded IPv4 tail's dotted
octets) split at the single `::` — and a verified Coq function does the byte
work:
theories/Surface/Ast.v
- new ip6grp (G16 / G4) + ip6grps_bytes: the big-endian 16-bit split lives
HERE (Nat.div/Nat.modulo), in Coq.
- new sip6_bytes: `::` zero-fill to exactly 16 bytes, failing loud (None) on
any literal that cannot be 16 bytes (the old lexer silently pad/truncated).
- SVIp6 now carries (list ip6grp) (option (list ip6grp)) instead of a
pre-decoded data.
- lemmas ip6_fill_len, sip6_bytes_len: expansion is always exactly 16 bytes.
Threaded through: Typecheck.resolve_value (SVIp6 -> sip6_bytes, wf case
re-proved), prefix_ok/Lower guards (constructor arity), and the OCaml frontend
(nft_ast ip6grp/ip6lit, lexer ipv6_groups with NO bit-arithmetic, parser IPV6
token type, nft_inject structural ip6grp injection, nft_emit arity). Verified
end-to-end: `ip6 daddr ::1` -> 0x..01, `ip6 saddr fc00::/18` -> 0xfc000000 with
an 18-bit mask.
Gate: boundary check (5) forbids `lsl|lsr|land|lor|asr` in lexer.mll (the old
byteorder split matches it), and `boundary` is now wired into `make gates` so
the residue is enforced, not a code review. DEVELOPMENT.md ledger corrected:
IPv4/MAC are one-byte-per-group grouping; IPv6 group split + `::` fill are the
verified Surface.Ast.sip6_bytes.
No headline theorem STATEMENT changed (resolve_value_wf et al. verbatim); new
lemmas only. All gates green: proofs, axioms (all "Closed under the global
context"), corpus 2532/2532 0 mismatches, validate 28/28, parse-test, gen-check,
boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ructors
The legacy 4-shape typed-match module — embedded in the typed layer through
the TXElab wrapper constructor — is retired whole, per TODO.md's
strata-retirement policy: theories/Surface/ is the real typed source
language, and the wrapper stratum no longer earns its keep.
Moved (old -> new):
- Elab.TMEq / TMNeq / MPrefix / MWildcard
-> Typed.TXEq / TXNeq / TXPrefix / TXWildcard (first-class txmatch
constructors; the TXElab wrapper and the tx_view projection are gone)
- Elab.prefix_expand + payload_prefix_field / mask_byte / prefix_mask /
data_and -> Surface/Typed.v (bodies and doc comments verbatim)
- Elab.prefix_aligned_24 / prefix_unaligned_20 / elab_port_22 /
elab_wildcard -> Surface/Typed.v (restated over elab_tx, same names)
- Elab.SEl / SRange (+ SEl_iv / SRange_iv) -> Surface/Lower.v (statements
unchanged)
- Elab.eval_tmatch's semantics -> Semantics/TypedEval.v, as INDEPENDENT
numeric clauses (read_val_N / read_lead_N / prefix_full_N), inside the
make-boundary encode-independence grep gate
Theorem-statement delta:
- RETIRED Elab.elab_matchcond_correct — a definitional consistency check
(reflexivity, because the legacy typed semantics was itself defined
through the byte encoding). SUPERSEDED BY the non-definitional per-shape
erasure theorems Lower_Proofs.eq_erasure / neq_erasure / prefix_erasure /
wildcard_erasure (composed into txmatch_erasure): the four shapes now
carry genuine decode / byteorder / mask-arithmetic obligations, the same
treatment every other typed shape gets. Documented in THEOREMS.md
("Strata retirement").
- RETIRED Lower_Proofs.txelab_erasure (the Some-form restatement over the
TXElab wrapper); subsumed by the same four theorems.
- ADDED Lower_Proofs.{eq,neq,prefix,wildcard}_erasure + supporting lemmas
(read_val_cmp_num, prefix_full_erasure, prefix_short_erasure,
read_lead_N_inv, data_to_N_app(_shiftr), bytes_wfb_app/firstn) and four
non-vacuity Examples; the make-axioms gate swaps elab_matchcond_correct
for the new family + txmatch_erasure.
- Every other pre-existing theorem statement survives verbatim (the
prefix-mask arithmetic lemmas moved earlier in Lower_Proofs.v unchanged).
Plumbing: Lower's dep guards and the fs_typed/lr_typed side channel carry
txmatch; nft_emit.ml stops printing the Elab import (all four Gen files
regenerated through nft2coq; gen-check green); Extract.v extracts elab_tx
only (elab_m / tx_view gone); nft_inject.ml's typed-view table is
Typed.txmatch; the axioms preamble drops Elab; _CoqProject drops the file;
THEOREMS.md / DEVELOPMENT.md / CONFIG_PROOFS.md updated.
Gates: proofs, axioms (all Closed under the global context), corpus
2532/2532 with 0 mismatches, validate 28/28, parse-test (TYPECHECK-RULESETS
4/4, ILLTYPED-REJECT 11/11), gen-check 4/4, boundary — ALL GATES GREEN.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ut_wf eliminated The two-fold verdict/write split dies: per rule there is now ONE left-to-right fold (Semantics.rule_step / run_rule_step), exactly nft_rule_dp_for_each_expr — every expression (match, statement operand, vmap key, limiter check) sees the packet-local (meta/ct set) AND env (dynset) writes of earlier expressions in the SAME rule; a failing match / breaking load stops the walk keeping earlier writes; statements after a terminal verdict never run; r_after statements (writes included) run only on a Continue fall-through. Theorem-statement changes: New (all axiom-free; gate additions marked *): - Semantics.body_step / after_step / terminal_step / end_step / rule_step / run_rule_step: the DSL and bytecode single folds. - * Semantics.rule_step_mutfree: on mut-free rules the fold IS the historical loadability-guarded verdict at unchanged state — rule_applies/outcome/ rule_loadable and run_rule survive only as the pure strand's write-free projection of the fold (Correct.run_rule_step_no_writes is the VM twin). - Semantics.after_step_mutfree / end_step_mutfree / terminal_step_mutfree, rule_step_state_after_free: coincidence layer for the retired pieces. - Correct.run_rule_step_compile_rule: UNCONDITIONAL per-rule bridge run_rule_step empty_rf (compile_rule r) e p = rule_step r e p (degenerate zero-field jhash/map/or operands included — Compile.compile_vsrc now pins their source register with IImmediateData _ [], removing the simple_writes hypothesis instead of assuming it). - Correct.step_compile_after / step_compile_terminal / step_compile_end, run_rule_step_no_writes, run_imms_step, step_extra_inat, after_step_nonset: the end/after machinery of the bridge. - * Lower_Proofs.lower_ruleset_numgen_free (+ lower_rule/chain/table lemmas): every chain of every successful lowering is numgen-free — the DISCHARGE of the strand's only hypothesis over ALL frontend-emitted programs. Lower.lower_rule now refuses incremental numgen fail-loud (new Lower.LEnumgen). - * Regression/Setread_IntraRule.v: positive pins — setread_accepted / vm_setread_accepted (the one-rule `meta mark set 0x1 meta mark 0x1 accept` ACCEPTS on both sides), dynset_feedback_accepted / vm_dynset_feedback_accepted (intra-rule `add @s {key}` then `@s` lookup in ONE rule), non-vacuity controls, and break-keeps-earlier-writes pins. Changed statements (successors; strata-retirement note in THEOREMS.md §3): - Semantics.dsl_rule_step / vm_rule_step: redefined as projections of the fold (+ limiter sweep; numgen sweep VM-side) — the intra-rule set-then-read infidelity is thereby REPAIRED, not re-ledgered. - Correct.vm_rule_step_compile_rule, run_program_mut(_env)_compile_chain, compile_chain_mut_correct, compile_chain_mut_env_correct, compile_seq_mut_correct, Main.main_compile_seq_mut_correct and the three pre_split mut corollaries: hypothesis `forallb mut_wf` becomes `forallb rule_numgen_free` (strictly larger domain), conclusion now the single-fold semantics (strictly stronger: intra-rule feedback, r_after mutation, degenerate operands all covered). - Semantics.dsl_rule_step_fst: now `= fst (rule_step r e p)` (old reading recovered via rule_step_mutfree); dsl_step_limit_free gains the r_after-mut-free hypothesis (its old statement is false for rules whose r_after writes — a shape the old strata excluded by hypothesis). - Semantics.body_writes: the fixpoint becomes the state projection of body_step (same values everywhere, one evaluator family). - Correct.mut_strand_jump_pin: mut_wf conjunct becomes rule_numgen_free. - Correct.eval_rules_trace_verdict (statement unchanged; proof over the fold). - Optimize_DataMap.eval_rules_mut_continue: hypothesis `outcome r e p = None` becomes `fst (rule_step r e p) = None` (+ step_orig_map_none / step_mk_map_none). Retired/deleted (successors named above): - Semantics.mut_wf, simple_vsrc, simple_body, simple_writes; Correct.mut_wf_prog_eq; Correct.run_rule_writes_compile_rule. - Semantics.run_rule_writes / body_writes fixpoints -> run_rule_step / body_step (the Correct.v writes toolkit is renamed *_writes -> *_step and re-proved over the fold, unconditional on operands). - Known_Infidelities entry 3 (setread_dropped / vm_setread_dropped / setread_write_happens / setread_mut_wf): FLIPPED to the positive pins in Setread_IntraRule.v; DEVELOPMENT.md ledger now has two entries; the two-fold header comments are deleted. - parse_test/nftc_cli mut_wf tool-boundary checks: replaced by a rule_numgen_free sanity pin (the discharge is now the theorem, not a gate). Gates: ALL GREEN — corpus 2532/2532 round-tripped, 0 mismatches; validate 28/28; TYPECHECK-RULESETS 4/4; ILLTYPED-REJECT 11/11; gen-check 4/4; boundary ok; make axioms: every AXIOM_GATE theorem "Closed under the global context" (list extended with the discharge, the coincidence theorem and the new pins). Challenger repairs (comment/doc-only; no proof, definition, or theorem statement touched): - Semantics.v INumgen and IR/Syntax.v LNumgen comments: retired two-pass vocabulary removed; the counter advance is correctly attributed to numgen_sweep_prog at the vm_rule_step boundary (VM-only; no DSL twin — the lowering rejects incremental numgen, Lower.LEnumgen). - Regression/Notrack_CrossRule.v, Regression/Ct_Untracked_Break.v, extracted/parse_test.ml: dangling [run_rule_writes]/[body_writes] pointers rebased onto the fold ([body_step]/[run_rule_step]). - DEVELOPMENT.md: mutation-machinery file map, oracle-relocation and new-mutation recipes, known-infidelity 1 "why open", and TODO 2/3 plans rebased onto the post-T1 names (simple_body route replaced by the prove-unconditional / Lower-fail-loud alternatives). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…m ct-id Fix the real wire-level frontend bugs from reports/corpus-divergence-bugs.md, all relocated into the verified Coq lowering by the typed-layer migration. Verified packet-identical to live nft in netns (B/C/E/F), byte-verified against the corpus (D/N), gates all green. Fixes (6 of the 7 bug classes; G deferred — see below): - B (host-endian ordered ranges, 10 blocks): Surface/Typed.range_hton is now `dt_byteorder = BoHost`, so EVERY host-endian ordered range (meta length/ skuid/skgid/cpu/cgroup/iifgroup/oifgroup, ct id/zone, mark/iif/oif/fib-type) takes nft's mandatory `byteorder hton` + big-endian-bounds path. netns: `meta length 33-45` counters now equal nft's (no longer over-matches len 300). - C (ct expiration unit+byteorder, 3 blocks): new DTtime datatype scales the SECONDS literal to the kernel's MILLISECONDS host-endian register (resolve_num DTtime n = VHostInt 4 (n*1000)) and rides the class-B hton path. netns: `ct expiration 25-35` lists 25s-35s / counts 4 (was 0s-0s / 0). - D (exthdr/tcpopt != exists|missing polarity, 2 blocks + 1 corpus-invisible twin): Lower.lower_presence threads the surface `!=` (cmp neq, not cmp eq). - E (reject with tcp reset, 3 blocks): reject_dep adds DepL4 6 so the RST cannot fire on non-TCP. netns: ICMP ping SUCCEEDS through our rule (was dropped), matching nft. - F (ether type/vlan link guard, 4 blocks): Selector attaches the iiftype guard to ether type and the vlan bitfields; Lower.guard_host encodes the iiftype immediate HOST-endian ([1;0], nft meta.c arphrd_type = BYTEORDER_HOST_ENDIAN) so it matches real ethernet (a BE [0;1] read as 256 and wrongly broke). netns: nft renders our rule identically to its own `ether type ip`, counter 0 on loopback. - N (ct label set K, 1 block): Lower.ct_label_imm emits 2^K as a 16-byte big-endian bitmap; N_to_data is N arithmetic so 2^127 does not wrap. Tooling / gates (all wired into `make gates`): - byteorder-gate now covers the ORDERED-RANGE class (triggers on the hton byteorder transform): 19/19 compile-from-source == corpus .payload (was 13). - new source-sweep-gate: a TRACKED-COUNT RATCHET (pass floor 1166 pinned in the Makefile; a frontend regression that drops a block below the floor is red). - codec.ml renders meta iiftype/oiftype host-endian (kernel truth); corpus round-trip stays 2532/2532 (reconstruction is symmetric via field_host_endian). - nl_send.ml gains a real ILog encoder emitting distinct NFTA_LOG_GROUP/SNAPLEN/ QTHRESHOLD/LEVEL/FLAGS/PREFIX attrs (was: whole string in PREFIX). netns: `log group 2` round-trips through the kernel and nft lists `log group 2`. Class O (upstream nftables bug): reports/upstream-ct-id.md drafts the `ct id` byteorder mismatch (nft declares NFT_CT_ID BIG_ENDIAN, kernel writes a native u32) with both citations; we are kernel-faithful (Selector: ct id = DThostint 4). Class G (L2 in-frame ethertype guard, 8 blocks) DEFERRED: it changes the L2-family network-guard SHAPE (meta protocol -> payload load @ link+12/+16), which is consumed by the axiom-gated Optiplex_Antispoof/Optiplex_Mark headline theorems and the Optiplex_Gen bytecode; a faithful fix needs nft's stateful vlan-offset protocol context + regenerating Optiplex_Gen + updating those headline proofs in lock-step — a dedicated milestone, ledgered in DEVELOPMENT.md. Theorem-statement changes: NONE. range_erasure_be/range_erasure_host and the resolve_num_* theorems keep their statements verbatim; range_hton's definition broadened, so range_erasure_host now covers the DThostint/DTtime dtypes with an unchanged statement (strengthened coverage, not weakened). No new Axiom/Admitted/Parameter; no new headline theorem (only vm_compute regression Examples: lower_metalen_range, lower_ctexpiration_range/_neq, lower_exthdr_ neq_exists, lower_tcpopt_neq_exists, reject_dep_tcp_reset, lower_ct_label_set_*, tev_hostint_range_hton_hit/_miss). make gates fully green: proofs, axioms, corpus 2532/2532, byteorder-gate 19/19, source-sweep 1166, validate 28/28, parse-test 4/4+11/11, gen-check 4/4, boundary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…gate + ratchet raise
Completes the T2A milestone: the 8 class-G bridge/netdev L2 network-guard blocks
now compile byte-identical to live nft v1.1.6 (source-sweep pass 1168 -> 1176),
so all 31 real wire-level bugs from reports/corpus-divergence-bugs.md leave the
divergent set.
Class G (L2 in-frame ethertype network guard). The bridge/netdev network-layer
ethertype guard is NOT always `meta protocol` (src/proto.c proto_eth vs
proto_netdev vs proto_vlan protocol_key; src/payload.c payload_gen_dependency /
payload_gen_special_dependency):
- a direct network selector (ip saddr / ip protocol) keeps proto_netdev's
`meta protocol` (unchanged);
- a transport-implied network dep (icmp/icmpv6/igmp type) uses proto_eth in
bridge -> `payload load 2b @ link+12`, but stays `meta protocol` in netdev
(golden bridge/icmpX.t.payload vs any/icmpX.t.netdev.payload);
- past a matched vlan tag (0x8100) the context is proto_vlan -> every in-frame
read moves to `payload load 2b @ link+16`, in both L2 families.
Implemented via new Selector.depspec DepNetLL (icmp/icmpv6/igmp reroute), a
vlan-context flag threaded through Lower.dep_guard, and a once-per-network-layer
dedup (Lower.layer_class) unifying the three interchangeable guard spellings.
No IR field added (reuses parametric FPayload PLink off 2). Optiplex_Gen.v is
byte-identical (its bridge ip daddr rules are direct, non-vlan) so the axiom-gated
Optiplex_Antispoof / Optiplex_Mark headline proofs are untouched. Verified against
live nft v1.1.6 under netns for both the icmp (+12) and vlan (+16) shapes.
Theorem-statement changes: NONE. No headline theorem added/removed/weakened;
AXIOM_GATE_THEOREMS unchanged. Selector gains the DepNetLL constructor and
dep_guard gains a `vlan` parameter; the affected regression Examples are re-pinned
and five new class-G Example pins added (all vm_compute reflexivity):
- Selector.selector_icmp_two_deps: [DepNfproto 2; DepL4 1] -> [DepNetLL 2; DepL4 1]
- Lower.dep_guard_{icmp_inet,ip_family_noop,bridge_ethertype,vlan_netdev_refused}:
thread the `vlan` arg (results unchanged)
- Lower.dep_guard_{bridge_netll_icmp,netdev_netll_icmp,bridge_vlan_ip,
netdev_vlan_ip}: new class-G shape pins
Also in this commit:
- parse_test.ml: check_big_literal_no_overflow pins `meta mark 0x80000000` (2^31)
compiling without stack overflow, so a revert of the Extract Constant N.of_nat
(Compiler/Extract.v) reddens the parse-test gate; ledgered as TCB residue (d)
in DEVELOPMENT.md.
- source-sweep-gate.sh: floor raised 1166 -> 1176 (never lowered).
- Makefile: drop the duplicate `$(MAKE) boundary` in the gates target.
- DEVELOPMENT.md: class G moved from DEFERRED to FIXED with the proto-context
rationale; N.of_nat Extract Constant added to the TCB residue list.
make gates: green (proofs, axioms, corpus 2532/2532 0 mismatches, byteorder-gate
21/21, source-sweep 1176>=1176, validate, parse-test, gen-check, boundary).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…sable -O CLI
Two new self-guarding intra-rule optimizer passes, proved UNCONDITIONALLY
(forall c e p, no hypotheses), plus a named/composable pass registry with ONE
generic composition theorem, and a `nftc -O`/`--list-passes` CLI.
New headline theorems (all axiom-free, added to AXIOM_GATE_THEOREMS):
- Optimize_PayMerge.paymerge_chain_eval : forall c e p,
eval_chain (paymerge_chain c) e p = eval_chain c e p.
Adjacent-payload-load merge (corpus class I): two byte-contiguous full-width
payload equalities in the same header fuse into one wider load+compare,
exactly where nft's payload_can_merge (src/payload.c) does. Unconditional:
a payload read and its loadability split at any interior offset for EVERY
packet (read_payload_split / read_payload_ok_split) — no byte/length wf
hypothesis. Closes the 5 class-I sweep blocks; floor 1176 -> 1181.
- Optimize_XorFold.xorfold_chain_eval : forall c e p,
eval_chain (xorfold_chain c) e p = eval_chain c e p.
Bitwise-xor constant fold (corpus class L): nft's binop_transfer step —
transfer the pure-xor register operand onto the compare value
((reg & 0xff..) ^ C <op> V -> ^ 0 <op> V^C). Unconditional by involutivity of
bytewise xor. Does NOT move the sweep floor: class-L blocks are host-endian
(endian-unportable in the text corpus) and nft further drops the residual
identity binop, which needs a register-byte-width fact the unbounded-byte
packet model cannot carry soundly (documented in the file header).
- Optimize_Registry.run_passes_correct : forall ps c e p,
eval_chain (run_passes ps c) e p = eval_chain c e p.
ONE generic composition theorem: folding any list of registered opt_passes
(each bundling its own eval-preservation proof) preserves eval_chain, proved
once quantified over the list.
No existing theorem statement changed, weakened, or retired — all additive.
CLI: nftc grows `-O p1,p2,...` (parses names into a pass list via the extracted
resolve_passes/run_passes; `default` = optimize_table_uncond, byte-identical to
`nftc optimize`) and `--list-passes`. The two intra-rule passes act on disjoint
matchcond shapes so they commute at the bytecode level; the CLI applies them in
the given order and run_passes_correct holds for every order.
Non-vacuity: in-repo vm_compute witnesses of real rewrites (paymerge_witness,
paymerge_link_witness, paymerge_no_gap, xorfold_witness, xorfold_leaves_and) and
the corpus class-I closure in the source-sweep ratchet.
Gates: proofs, axioms (3 new theorems Closed under the global context), corpus
2532/2532 0 mismatches, byteorder-gate 21/21, source-sweep 1181>=1181,
validate 28/28, parse-test, gen-check, boundary — all green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Named stateful objects end-to-end, config-management ops, and the parser's
token-soup catch-all deleted. The verified core already carried the object IR
(SObjref/SObjrefMap/MQuota/SCounter); this wires the surface layer to it.
Named objects:
- Surface/Ast.v: sobjkind + objkind_otype (NFT_OBJECT_*, nf_tables.h); StCounter
now carries (pkts,bytes); StObjref/CObjrefMap; TObj retains its kind.
- Surface/Typecheck.v: obj_ctx + objkind_declared + tc_objrefmap; a rule's
`counter name`/`quota name`/`ct helper set`/objref-map reference is checked
for declared-existence + kind agreement (undeclared / wrong-kind rejected).
- Surface/Lower.v: StCounter -> SCounter pkts bytes (initial values no longer
discarded); StObjref -> SObjref (objkind_otype k); CObjrefMap -> SObjrefMap.
- parser.mly/lexer.mll/nft_ast.ml/nft_inject.ml/nft_emit.ml: real per-kind
object grammar, the `counter/quota/limit/ct-helper/ct-timeout/ct-expectation/
synproxy name` reference forms + objref verdict-maps. Verified byte-identical
to live nft (ip/objects.t.payload: type 1/2/3/4/7/9, `[ objref sreg 1 set ]`).
Config ops (unverified preprocessing, extracted/nft_config.ml): delete/destroy/
flush of table/chain/ruleset parse to structured TopOps applied in file order
before the injection; delete errors on a missing entity, destroy is
delete-if-exists, flush empties. Zero TopNop productions remain.
Parser: the `IDENT IDENT LBRACE junk RBRACE` catch-all is deleted; an unknown
table item (`frobtable x {}`) is a parse error; a flowtable is parsed
structurally then loudly refused.
Gates: objects-sweep-gate ratchet (ip/objects.t rule lines, BIDIRECTIONAL,
14/14, floor 14) added to `make gates`; source-sweep floor 1181 -> 1187 (objref
blocks now byte-identical); ILLTYPED-REJECT 11 -> 13 (objref_undeclared,
objref_wrong_kind). corpus 2532/2532, validate 28/28, TYPECHECK 4/4, gen-check
4/4, boundary all green; axiom-freedom unchanged.
THEOREM STATEMENTS: none changed, none retired, none weakened. No new domain
hypotheses (numgen-freedom of the new lowering is auto-discharged by the
existing lower_rule guard + Lower_Proofs.lower_ruleset_numgen_free; the new IR
uses are covered by the existing total compile/semantics theorems). New pinned
`vm_compute` Examples only (objref_{declared_accepts,undeclared_rejects,
wrong_kind_rejects}, objrefmap_{declared_accepts,undeclared_rejects}).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Challenger REJECT on Acceptance Test 3 (broad ok/fail ratchet). Repairs:
1. Broaden the ok/fail sweep from ip/objects.t to all supported families
(ip, inet, any) and pin it as a Makefile-gated bidirectional ratchet
(corpus-okfail-gate.sh, `make gates`): pass >= 671 (a supported `;ok` line
newly rejected, or a `;fail` line newly accepted, drops pass -> red) and
false_accept <= 42 (a NEW invalid `;fail` line slipping through -> red).
2. Reject the three in-scope invalid `;fail` forms that were silently accepted:
- `queue num 65536` — queue num is a u16 (kernel nf_queue __u16):
new Typecheck.sverdict_valid, checked on CVerdict and CVmap entries.
- `tcp option 256 exists` — a raw tcp option kind is a byte (nft tcpopt.c):
Symbols.dt_tcpopt_num rejects a numeric name > 255.
- `tcp option eol left` / `tcp option eol left 1` — eol/nop carry only `kind`:
new Symbols.tcpopt_field_valid gates dt_tcpopt_field to the option's
template fields.
3. OSweep harness: strip the corpus `- ` list-output continuation prefix and
skip `define`/variable lines so the residual list is trustworthy; count all
four directions (pass/false_accept/false_reject).
4. DEVELOPMENT.md § T3: retract the false "covered by source-sweep-gate and the
semantic gates" claim for the `;fail` direction; add a per-case ledger of the
42 residual model-boundary false-accepts (NAT/tproxy hook-context 22,
family/nfproto-scoped selectors+reject 10, log option mutual-exclusion 8, fib
key-set 1, icmp field inter-dependency 1), each with a named follow-up.
5. Minor: remove the dead Surface TopNop constructor (Ast.v), its nft_emit.ml
render branch, and the stale Ast.v comment — config ops are OCaml-layer
TopOps applied by nft_config.ml, so no config-op node reaches the surface AST.
No theorem added, retired, changed, or weakened; AXIOM_GATE_THEOREMS unchanged.
sverdict_valid/tcpopt_field_valid/dt_tcpopt_num are definitions referenced by no
theorem statement; the numgen-freedom discharge (lower_ruleset_numgen_free) is
byte-untouched and recompiles over the unchanged lowering. All gates green;
axiom-free (every AXIOM_GATE theorem "Closed under the global context").
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The corpus-okfail-gate harness undercounted false-accepts because it wrapped
every rule in the file's last-wins chain hook (netdev `hook egress device lo`
for ~30 ip/inet/any files), so lowering failed for a hook reason on every rule
there and the false_accept ceiling was blind to those files.
R1: wrap each rule in a fixed ip/filter/`hook input` base chain (valid for the
hardcoded family; nf_tables.h NF_INET_LOCAL_IN), ignoring the rule's own
family-specific chain hook. Also translate the corpus `!name type ...`
set/map declaration directives (inject the ones that individually
typecheck+lower, mirroring the existing `%` object-decl handling) so `@name`
rules resolve, and skip `?name elem` set-element directives — both were
miscounted as rule false-rejects.
R2: re-derived and re-pinned FLOOR 671->1003, CEIL 42->47 (the true post-fix
counts). Three of the challenger's masked false-accepts are now REJECTED in
the parser (nft grammar, not model typing): `limit rate 1 gbytes/second`
(byte units are only bytes/kbytes/mbytes, src/statement.c data_unit[]);
`limit rate 1023/second burst 10 bytes` and `limit rate 512 kbytes/second
burst 5 packets` (a packet-rate pairs only with a packet-burst and a
byte-rate only with a byte-burst, src/parser_bison.y limit_args).
R3: the true residual (47 false-accepts, 341 false-rejects) is walked and
ledgered per-category in DEVELOPMENT.md; the false-rejects are named
unsupported-construct model boundaries, not gaps in supported constructs.
R4: retracted the false "residual list is trustworthy" claim in DEVELOPMENT.md
and corpus-okfail-gate.sh; replaced with the harness-correctness rationale.
No Coq `.v` file touched: no theorem added/retired/changed/weakened,
AXIOM_GATE_THEOREMS byte-identical, no new Axiom/Admitted/Parameter. All changes
are in the untrusted OCaml frontend (parser.mly), the harness (parse_test.ml),
the gate script, and docs. `make gates` green: corpus 2532/2532 0 mismatches,
source-sweep pass=1187, objects-sweep 14/14, corpus-okfail pass=1003/1391
floor=1003 false_accept=47 ceil=47, validate 28/28, parse-test ILLTYPED 13/13,
gen-check 4/4, boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
yiyunliu
added a commit
that referenced
this pull request
Jul 22, 2026
…mgen advance inside the break-aware fold; boundary sweeps and step wrappers retired Eliminates Known Infidelity #1: `limit`/`quota`/`connlimit` consumption (DSL body_step via the new match_consume, VM run_rule_step's ILimit/IQuota/ IConnlimit cases) and the VM `numgen inc` counter advance (INumgen case) are now evaluated AT their body/instruction position INSIDE the break-aware per-rule fold — kernel NFT_BREAK order: a limiter after a failing match is never evaluated and never consumes; a reached limiter writes its bucket on both the pass and the exhausted branch; a limiter before a break consumes and the write survives. The unconditional whole-body sweeps and the dsl_rule_step/vm_rule_step boundary wrappers that carried them are RETIRED (with the consumption in-fold they equalled the folds). Theorem-statement deltas (full ledger: THEOREMS.md § strata retirement (M2)): - CHANGED Correct.run_rule_step_compile_rule: was unconditional, now takes rule_numgen_free r (the VM fold's in-fold numgen advance has no DSL twin); discharged over ALL frontend-emitted programs by the pre-existing Lower_Proofs.lower_ruleset_numgen_free (AXIOM_GATE). It now IS the one per-rule DSL/VM bridging equation (same strength as the retired composite vm_rule_step_compile_rule). - VERBATIM but domain-narrowed underneath (honest write-free domains): Semantics.rule_step_mutfree (rule_mutfree/body_item_mutfree now count a limiter match as a write via match_consumefree), Correct.run_rule_step_no_writes (writes_instr now counts ILimit/IQuota/ IConnlimit and incremental INumgen as writes), eval_rules_u_writefree / eval_table_u_writefree / eval_ruleset_u_writefree / eval_hook_u_writefree / run_table_writefree_compiled / eval_chain_writefree_jumpfree_proj (rule_writefree := rule_mutfree, the limit_free_body conjunct absorbed). All other AXIOM_GATE statements verbatim; all still Closed under the global context. - RETIRED (successors in parentheses): dsl_rule_step, vm_rule_step (rule_step / run_rule_step empty_rf), dsl_rule_step_fst/_snd (trivial), dsl_rule_step_vmap (rule_step_vmap), dsl_rule_step_writefree (rule_step_writefree), dsl_step_limit_free (dsl_step_after_free — the limit-freedom hypothesis existed only to cancel the boundary sweep), limit_sweep_body/limit_sweep_prog/numgen_sweep_prog + identity lemmas, limit_free_body/limit_free_prog, Correct.vm_rule_step_compile_rule (run_rule_step_compile_rule), the sweep-agreement family (lf_*, limit_sweep_prog_compile_rule, straight_imp_lf) and the dead no_writes fragment family (nw_load_fields..nw_compile_end, straight_imp_nw) whose statements are false under the honest writes_instr. - NEW: Semantics.match_consume/match_consumefree/match_consume_free_id, rule_step_writefree, dsl_step_after_free; Correct.forallb_alloc_regs_ng; ngfree hypotheses threaded through the run_rule_step scaffolding (compile_load_step, run_load_fields(_t)_step(_break), run_or_chain_step, run_vsrc_step(_break), step_match_one — now consuming/env-parameterised — run_stmt_step_neutral/break, run_dynset_*_step, run_step_compile_body, step_compile_after/terminal/end, run_rule_step_straight). - PINS flipped + added (all in AXIOM_GATE): Known_Infidelities.gate_limit_undrained / vm_gate_limit_undrained (e_limit stays 1 after a failing match; flipped from gate_limit_drained's "= 0"), Limit_SharedBucket.limit_before_failing_match_consumed / vm_limit_before_failing_match_consumed (position-exactness: a limiter before the failing match consumes to 0 and the write survives the break). The intra-rule left-to-right token state is now real on both sides: a second limiter in the same rule reads the first one's consumption, and the mutation, trace and unified (U1) evaluators inherit the corrected fold unchanged — every later effect milestone builds on it. Docs: DEVELOPMENT.md ledger entry 1 moved to (repaired) with the flipped pins; THEOREMS.md evaluator matrix + strata-retirement note; stale sweep references purged from Core/Packet.v, IR/Syntax.v, Reject_GuardFirst.v, Limit_SharedBucket.v headers and the Semantics.v header matrix. Gates: make gates fully green (proofs, axioms incl. 4 new pins, corpus 2532/2532, corpus-okfail, byteorder/source-sweep/objects-sweep, validate, parse-test, gen-check, boundary); 0 Admitted/Axiom/Parameter added. R1+R2 repair (challenger round 2) — the Router pure-strand statements are now LICENSED unified-semantics statements; no effectful rule is evaluated through an unlicensed pure evaluator anywhere: - NEW general license (Semantics.v § Projection 1b, all AXIOM_GATE, Closed): * Semantics.eval_rules_u_limiter_tolerant: forallb rule_limiter_tol rs -> chains_limiter_tol cs -> fst (eval_rules_u fuel cs rs e p) = eval_rules_j fuel cs rs e p — the pure jump strand is the VERDICT projection of the unified fold on limiter-tolerant configs (every rule write-free OR a rule_one_limiter rule: match-only body whose single non-consume-free match is a non-inverted limit/quota or any connlimit, in last position, under a static terminal verdict), for EVERY fuel/env/packet — jumps, gotos and adversarial-env chain re-entries included. Proof: a traversal invariant (limiter_inv) relating the threaded env to the entry env (equal outside the consumable components; every touched bucket exhausted at both — non-inverted fail-branch re-caps, quota only shrinks, connlimit insert is idempotent), plus env congruence of every consume-free read. * Semantics.eval_table_u_limiter_tolerant (table form), Semantics.eval_hook_u_limiter_tolerant_1 (single-base hook form; the multi-base restriction is honest — a fired limiter's depletion crosses base chains where the pure strand cannot follow). - Router config instances (each Compute-discharged, each AXIOM_GATE, each cited in its file): Router_Input.inbound_licensed / router_rules_licensed / bug_chains_licensed; Router_Forward.forward_licensed / bug_forward_licensed; Router_Private.private_rules_licensed / bug_priv_chains_licensed; Router_Hooks.input_hook_licensed / forward_hook_licensed / postrouting_hook_licensed / input_hook_bug_licensed (+ select_input_bug); Router_Realistic.{inbound,forward,private_rules,input_hook,forward_hook} _licensed_real; Nft_Demo_Concrete.demo_dns_accepted_unified / demo_smtp_denied_unified (concrete cruxes restated over eval_table_u). - THEOREMS.md: "Residual (designated follow-up)" paragraph REPLACED by the limiter-tolerant license row + per-file citation list. - DEVELOPMENT.md: "(3) In-traversal mutation" now claims ONE confirmed divergence (OVmapNat vmap-hit trace NAT); the limiter entry is described as repaired (M2 in-fold consumption, positive pins). - New supporting lemmas (Semantics.v): env_upd_limits normal form + congruence family (do_load/field_value/eval_matchcond/rule_applies_walk/ rule_loadable/outcome/... _upd_limits), spec eqb_eq/refl (limit/quota/connlimit), lim/quota/connlimit_under_ext, limiter_inv + set_limit/set_quota/set_connlimit/match_consume preservation, body/rule_step_one_limiter, pure_step_inv, eval_rules_u_limiter_tol_aux. No pre-existing statement changed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
yiyunliu
added a commit
that referenced
this pull request
Jul 22, 2026
…mgen advance inside the break-aware fold; boundary sweeps and step wrappers retired Eliminates Known Infidelity #1: `limit`/`quota`/`connlimit` consumption (DSL body_step via the new match_consume, VM run_rule_step's ILimit/IQuota/ IConnlimit cases) and the VM `numgen inc` counter advance (INumgen case) are now evaluated AT their body/instruction position INSIDE the break-aware per-rule fold — kernel NFT_BREAK order: a limiter after a failing match is never evaluated and never consumes; a reached limiter writes its bucket on both the pass and the exhausted branch; a limiter before a break consumes and the write survives. The unconditional whole-body sweeps and the dsl_rule_step/vm_rule_step boundary wrappers that carried them are RETIRED (with the consumption in-fold they equalled the folds). Theorem-statement deltas (full ledger: THEOREMS.md § strata retirement (M2)): - CHANGED Correct.run_rule_step_compile_rule: was unconditional, now takes rule_numgen_free r (the VM fold's in-fold numgen advance has no DSL twin); discharged over ALL frontend-emitted programs by the pre-existing Lower_Proofs.lower_ruleset_numgen_free (AXIOM_GATE). It now IS the one per-rule DSL/VM bridging equation (same strength as the retired composite vm_rule_step_compile_rule). - VERBATIM but domain-narrowed underneath (honest write-free domains): Semantics.rule_step_mutfree (rule_mutfree/body_item_mutfree now count a limiter match as a write via match_consumefree), Correct.run_rule_step_no_writes (writes_instr now counts ILimit/IQuota/ IConnlimit and incremental INumgen as writes), eval_rules_u_writefree / eval_table_u_writefree / eval_ruleset_u_writefree / eval_hook_u_writefree / run_table_writefree_compiled / eval_chain_writefree_jumpfree_proj (rule_writefree := rule_mutfree, the limit_free_body conjunct absorbed). All other AXIOM_GATE statements verbatim; all still Closed under the global context. - RETIRED (successors in parentheses): dsl_rule_step, vm_rule_step (rule_step / run_rule_step empty_rf), dsl_rule_step_fst/_snd (trivial), dsl_rule_step_vmap (rule_step_vmap), dsl_rule_step_writefree (rule_step_writefree), dsl_step_limit_free (dsl_step_after_free — the limit-freedom hypothesis existed only to cancel the boundary sweep), limit_sweep_body/limit_sweep_prog/numgen_sweep_prog + identity lemmas, limit_free_body/limit_free_prog, Correct.vm_rule_step_compile_rule (run_rule_step_compile_rule), the sweep-agreement family (lf_*, limit_sweep_prog_compile_rule, straight_imp_lf) and the dead no_writes fragment family (nw_load_fields..nw_compile_end, straight_imp_nw) whose statements are false under the honest writes_instr. - NEW: Semantics.match_consume/match_consumefree/match_consume_free_id, rule_step_writefree, dsl_step_after_free; Correct.forallb_alloc_regs_ng; ngfree hypotheses threaded through the run_rule_step scaffolding (compile_load_step, run_load_fields(_t)_step(_break), run_or_chain_step, run_vsrc_step(_break), step_match_one — now consuming/env-parameterised — run_stmt_step_neutral/break, run_dynset_*_step, run_step_compile_body, step_compile_after/terminal/end, run_rule_step_straight). - PINS flipped + added (all in AXIOM_GATE): Known_Infidelities.gate_limit_undrained / vm_gate_limit_undrained (e_limit stays 1 after a failing match; flipped from gate_limit_drained's "= 0"), Limit_SharedBucket.limit_before_failing_match_consumed / vm_limit_before_failing_match_consumed (position-exactness: a limiter before the failing match consumes to 0 and the write survives the break). The intra-rule left-to-right token state is now real on both sides: a second limiter in the same rule reads the first one's consumption, and the mutation, trace and unified (U1) evaluators inherit the corrected fold unchanged — every later effect milestone builds on it. Docs: DEVELOPMENT.md ledger entry 1 moved to (repaired) with the flipped pins; THEOREMS.md evaluator matrix + strata-retirement note; stale sweep references purged from Core/Packet.v, IR/Syntax.v, Reject_GuardFirst.v, Limit_SharedBucket.v headers and the Semantics.v header matrix. Gates: make gates fully green (proofs, axioms incl. 4 new pins, corpus 2532/2532, corpus-okfail, byteorder/source-sweep/objects-sweep, validate, parse-test, gen-check, boundary); 0 Admitted/Axiom/Parameter added. R1+R2 repair (challenger round 2) — the Router pure-strand statements are now LICENSED unified-semantics statements; no effectful rule is evaluated through an unlicensed pure evaluator anywhere: - NEW general license (Semantics.v § Projection 1b, all AXIOM_GATE, Closed): * Semantics.eval_rules_u_limiter_tolerant: forallb rule_limiter_tol rs -> chains_limiter_tol cs -> fst (eval_rules_u fuel cs rs e p) = eval_rules_j fuel cs rs e p — the pure jump strand is the VERDICT projection of the unified fold on limiter-tolerant configs (every rule write-free OR a rule_one_limiter rule: match-only body whose single non-consume-free match is a non-inverted limit/quota or any connlimit, in last position, under a static terminal verdict), for EVERY fuel/env/packet — jumps, gotos and adversarial-env chain re-entries included. Proof: a traversal invariant (limiter_inv) relating the threaded env to the entry env (equal outside the consumable components; every touched bucket exhausted at both — non-inverted fail-branch re-caps, quota only shrinks, connlimit insert is idempotent), plus env congruence of every consume-free read. * Semantics.eval_table_u_limiter_tolerant (table form), Semantics.eval_hook_u_limiter_tolerant_1 (single-base hook form; the multi-base restriction is honest — a fired limiter's depletion crosses base chains where the pure strand cannot follow). - Router config instances (each Compute-discharged, each AXIOM_GATE, each cited in its file): Router_Input.inbound_licensed / router_rules_licensed / bug_chains_licensed; Router_Forward.forward_licensed / bug_forward_licensed; Router_Private.private_rules_licensed / bug_priv_chains_licensed; Router_Hooks.input_hook_licensed / forward_hook_licensed / postrouting_hook_licensed / input_hook_bug_licensed (+ select_input_bug); Router_Realistic.{inbound,forward,private_rules,input_hook,forward_hook} _licensed_real; Nft_Demo_Concrete.demo_dns_accepted_unified / demo_smtp_denied_unified (concrete cruxes restated over eval_table_u). - THEOREMS.md: "Residual (designated follow-up)" paragraph REPLACED by the limiter-tolerant license row + per-file citation list. - DEVELOPMENT.md: "(3) In-traversal mutation" now claims ONE confirmed divergence (OVmapNat vmap-hit trace NAT); the limiter entry is described as repaired (M2 in-fold consumption, positive pins). - New supporting lemmas (Semantics.v): env_upd_limits normal form + congruence family (do_load/field_value/eval_matchcond/rule_applies_walk/ rule_loadable/outcome/... _upd_limits), spec eqb_eq/refl (limit/quota/connlimit), lim/quota/connlimit_under_ext, limiter_inv + set_limit/set_quota/set_connlimit/match_consume preservation, body/rule_step_one_limiter, pure_step_inv, eval_rules_u_limiter_tol_aux. No pre-existing statement changed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.