Repository navigation
Conversation
…, not MQuota; sweep-text 31→26 Two documentation-only corrections: - Named-quota model-boundary bullet claimed anonymous inline 'quota N bytes' keeps MQuota drop semantics. False: parser.mly has no inline-quota statement production (only QUOTA IDENT STRING objref, QUOTA IDENT LBRACE obj_body RBRACE declaration, and the objref-map clause), so an inline quota in a rule is a loud parse error — as the T3 corpus ok/fail residual list already said. The bullet now states that, and that only the named objref form lowers (verdict-neutrally). - T2A verdict paragraph now carries the honest corpus-text accounting, correcting commit e0b1c5e's 'all 31 leave the divergent set': 26 of the 31 fixed blocks become byte-identical; 5 remain textually divergent but wire-correct/packet-equal (host-endian display residual, not bugs). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The extracted verified surface typechecker (Surface/Typecheck.v, typecheck_ruleset) used to run only in the parse-test / sweep GATES, so the shipped CLI path (nft_parse.parse_file -> nft_inject.lower, i.e. nftc compile/optimize/send) silently lowered a config whose rule referenced an undeclared or wrong-kind named object: `counter name "nosuch"` with no declaration (or with `quota "nosuch"` declared) compiled to `[ objref type 1 name nosuch ]`, exit 0 — contradicting "zero silent drops". Nft_inject.lower now calls the extracted Typecheck.typecheck_ruleset on the injected surface tree before the verified lowering, so EVERY frontend consumer (nftc CLI, parse_test CLI mode, semtest, e2e) gets the same verified check; the OCaml side only re-runs the extracted per-table/per-chain checkers to NAME the failing table/chain in the Lower_error message, never deciding acceptance. Both bad configs now exit 1 with "ill-typed ruleset rejected by the verified surface typecheck (table ip filter, chain input)"; a config with the proper declaration still compiles byte-identically. The FULL typecheck runs (not an objref-only subset): the only gate friction was the source-sweep's own synthetic wrap, which compiles each corpus .t.payload block's bare rule without the !set/%object declarations its recording context had — those wraps (undeclared @setn and the six objects.t objref blocks) are genuinely ill-typed, so the sweep now re-injects the sibling .t file's `;ok` declarations (parse_test.ml Harness.decls_for_payload, first-decl-wins, individually validated like OSweep's decl_ok); the OSweep helpers were deduplicated into the shared Harness module. Source-sweep pass/parsefail/ mismatch counts and block sets are byte-for-byte identical to before (1187/504/51, floor 1187). make gates: ALL GATES GREEN (proofs, axioms all closed, corpus 2532/2532, byteorder 21/21, source-sweep 1187 >= 1187, objects-sweep 14/14, corpus-okfail 1003/1391 fa=47<=47, validate 28/28, parse-test incl. TYPECHECK-RULESETS 4/4 + ILLTYPED-REJECT 13/13, gen-check, boundary). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…-to-end
The parenthesized OR-group flag idiom was a hard parser gap: the lexer had
no (/) tokens at all. Representation: the group is parsed STRUCTURALLY into
a new surface constructor (Nft_ast.Vor -> Ast.SVOr, a list of surface
values) and carried UNRESOLVED across the OCaml/Coq seam — symbol values
(syn=0x02, ...) and the OR-fold live only in verified Coq, per the
typed-source decision. A new constructor (not SVSet reuse) because SVOr has
exactly one meaning: constant OR-fold, never set membership.
- lexer.mll/parser.mly: LPAREN/RPAREN tokens; the CBitmatch mask position
takes `( v | v | ... )` (maskval/orvals) and any elem value position takes
a bare `v | v` group (rhs compare values, set elements). Zero new menhir
conflicts (38 states / 48 s-r before and after).
- Typecheck.v: resolve_value split into resolve_atom + an SVOr wrapper;
nftval_or joins two resolved values of the same integer constructor/width
with N.lor; or_fold/resolve_or fold a group member-by-member through the
symbol tables (so address/name types refuse OR, like `iifname & 0xff`).
resolve_value_wf re-proved via resolve_atom_wf + lor_lt_pow2/nftval_or_wf/
or_fold_wf (OR cannot exceed either operand's width); expand_var and
svalue_size get SVOr cases ($defines expand inside groups); tc_bitmatch
additionally refuses SOpBang.
- Lower.v: lower_bitmatch inherits SVOr through atom/resolve_value — the
EXISTING CBitmatch -> TXBitwise pipeline, byte-for-byte untouched on old
inputs — and mirrors the SOpBang refusal (`& mask ! v` is an nft syntax
error, inet/tcp.t:90 `;fail`, still rejected); resolve_sv gets SVOr.
Pinned Examples: (fin|syn|rst|ack) mask folds to 0x17, (syn|ack) value to
0x12 -> TXBitwise BOand, matching golden inet/tcp.t.payload:441-447
`bitwise reg1 = (reg1 & 0x17) ^ 0x00; cmp eq reg1 0x12` — reproduced
byte-identical compiling from source.
Floors ratcheted: corpus-okfail pass 1003 -> 1008 (the 5 compound-mask `;ok`
lines inet/tcp.t:81-85 flip; false_accept stays 47, false_reject 341 -> 336),
source-sweep 1187 -> 1196 (9 paren/OR golden payload blocks now byte-identical
from source). The two remaining tcp-flags misses are SET-shaped
(`{ syn, syn|ack }` membership, `& (...) == { ... }` masked lookup) — a
different refusal class, ledgered in DEVELOPMENT.md. All headline theorems
stay axiom-free; full `make gates` green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…nearization parity
nft performs the class-I adjacent-payload merge (payload_can_merge) and the
class-L bitwise-xor constant fold (binop_transfer) UNCONDITIONALLY at netlink
linearization — no `nft -o` involved. Since T2B both existed as verified
UNCONDITIONAL passes but were reachable only via opt-in `-O`, so plain
`nftc compile` still diverged from plain `nft`. This commit makes them
default-on.
Wiring point (new theories/Optimizer/Optimize_Linearize.v):
linearize_chain := xorfold_chain ∘ paymerge_chain
compile_chain_default := compile_chain ∘ linearize_chain
Linearization sits at the COMPILE boundary — mirroring nft, where it happens
at emission, after any -o consolidation — NOT inside optimize_table_uncond.
`nftc compile`, `nftc optimize`, and `nftc send` all bottom out in
compile_chain_default (nftc_cli.ml); glue.ml's render demo and the Nftc
library facade (new `compile_default`, bare `compile` kept and labelled)
follow.
Theorem composition, all axiom-free and added to AXIOM_GATE_THEOREMS:
- linearize_chain_eval: the composed stage preserves eval_chain
(paymerge_chain_eval + xorfold_chain_eval), forall c e p.
- compile_chain_default_correct (HEADLINE, default-pipeline axis):
run_chain (compile_chain_default c) (c_policy c) e p = eval_chain c e p —
compile_chain_correct carried through both always-on stages.
- optimize_table_uncond_compile_correct (optimizer HEADLINE) RESTATED over
compile_chain_default via the new compile_chain_default_sets_correct, so
it is about the term the CLI actually emits. Main.v axis 3 restated
accordingly; new axis 3b main_compile_chain_default_correct; the
pre-split ratchet corollary keeps its historical plain-compile_chain
statement, re-derived from optimize_table_uncond_correct +
compile_chain_sets_correct.
Non-vacuity, Compute-pinned in Optimize_Linearize.v:
default_pipeline_merges_payload_loads — `tcp sport 1 tcp dport 2`
default-compiles to ONE 4-byte transport load + cmp 0x00010002 (plain
compile_chain emits two 2-byte loads: plain_compile_emits_two_loads);
default_pipeline_folds_xor — the mark-xor match compiles with xor slot 0
and compare value V^C.
Gate-convention handling (no floor lowered, no check deleted):
- make corpus (2532/2532) is a bytecode->render round-trip
(corpus_test.ml compile_rule) — untouched by the default-pipeline change;
still 2532/2532.
- source-sweep now compiles through the SHIPPED compile_chain_default
instead of the harness-side ad-hoc paymerge_chain application (parse_test
source_sweep); pass count HELD at 1196 (floor unchanged): the class-I
blocks were already closed by T2B's pass application, and the class-L
blocks stay open on the ledgered host-endian display residual plus nft's
identity-binop elision (unsound to replicate over unbounded-byte
registers — Optimize_XorFold scope note). A MISMATCH debug print was
added under SWEEP_DEBUG.
- byteorder-gate also compiles through compile_chain_default; on its
accepted shape (meta/ct/fib load + cmp/range only, no payload loads, no
bitwise) neither stage can fire — still 21/21.
- -O paymerge / -O xorfold registry passes remain (explicit use before the
default compile is an idempotent second application).
Docs: DEVELOPMENT.md new section "Classes I + L are DEFAULT-ON"; THEOREMS.md
headline table + derivation rows; README claim line; Extract.v extracts
linearize_chain/compile_chain_default.
Gates: ALL GREEN — proofs axioms (90/90 Closed under the global context,
incl. the two new entries) corpus 2532/2532, byteorder-gate 21/21,
source-sweep 1196>=1196 at this commit, objects-sweep 14/14, corpus-okfail
1008/1391 fa 47<=47, validate 28/28, parse-test, gen-check, boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ng fix (floor 1196 -> 1198)
The mandated post-wiring audit of every remaining compile-from-source
mismatch, written to reports/default-linearization-audit.md (the class ledger
A-O lives in owner-private notes, so the audit gets its own committed file).
Classification of the 49 residual blocks:
27 host-endian display residual (ledgered T2A endian-unportable class:
meta length/mark-and/mark-or/skuid/skgid/cpu/cgroup, ct mark/zone/
expiration/event/label/id, mark-set immediates)
4 class-L residual: the xor FOLD is now default-on and byte-visible
(xor operand 0, folded compare value), but the blocks stay text-open on
nft's identity-binop elision (unsound over unbounded-byte registers —
Optimize_XorFold scope note) stacked on host-endian display
12 further baked-in nft default rewrites, catalogued as NEW classes with
the precise blocking reason, none implementable as a small
unconditional verdict-preserving chain->chain pass:
P family-implied `meta protocol` elision (2) — needs the hook/family
fact a per-chain semantics does not carry
P' transport-dependency dedup after `ip6 nexthdr` (2) — meta l4proto
and the nexthdr byte are independent oracles in the model
Q dep-guard hoisting for `reject with tcp reset` (3) — a lowering
emission-order decision; reorder only sound for stateless bodies
R reject family concretization (5) — ICMPX vs family ICMP are
DIFFERENT Reject verdict values; needs an encoding quotient or
frontend concretization
S inet link-layer dependency choice (1, stacked on R) — payload
ethertype guard (merges) vs our meta nfproto guard (blocks merge)
6 render/attribute-materialization text divergences: log option
canonicalization (4; ILog's opts string is near-verbatim source text),
fib presence-check shape (2; result column + eq-1 vs neq-0 polarity)
Implemented audit finding (this commit): the fib concat-selector spelling.
parser.mly joined concat fib keys with "." ("saddr.iif") while nft's netlink
debug prints " . " ("saddr . iif") — which was ALREADY the canonical spelling
elsewhere in the development: corpus_test validate_pairs confirms
FFib ("daddr . iif", ...) against live nft, and Fib_Local.fibkey_wf keys
"daddr . iif"/"saddr . iif" — i.e. the parser produced a selector string the
fib theorems never talk about. One-token join fix in parser.mly (single-key
selectors unaffected; the sel stays an opaque string through
Selector/Lower/compile); comment in Selector.v updated.
inet/fib.t.payload:6/:11 move from divergent to byte-identical:
source-sweep 1196 -> 1198, floor raised accordingly (never lowered).
Gates: ALL GREEN at this tree — proofs axioms (90/90 Closed under the global
context) corpus 2532/2532, byteorder-gate 21/21, source-sweep 1198>=1198,
objects-sweep 14/14, corpus-okfail 1008/1391 fa 47<=47, validate 28/28,
parse-test, gen-check, boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… read width-normalized BY CONSTRUCTION The packet/env oracles (pkt_meta, e_ct, e_rt, pkt_sock, pkt_osf, pkt_numgen, pkt_symhash) stay width-free; every READ of them is now fit-normalized at the semantics boundary (Syntax.do_load AND the VM's mirror instructions) to the exact byte width the kernel eval writes into the destination register. Bytes.fit w d = firstn w (d ++ zeros) — the nft_reg_store8/16/64 + struct nft_regs register-store discipline. Width tables are TOTAL and cite linux-6.18.33 eval source per entry (Syntax.meta_width / ct_width / rt_width / socket_width / osf_width / numgen_width / symhash_width); cross-checked against the frontend dtype table by the computed Selector.selector_widths_agree (now non-vacuous on every meta/ct/rt/socket row). No packet_wf/env_wf anywhere; width facts are definitional. Notable table resolution: meta cgroup is the u32 net_cls classid (nft_meta.c:173, len sizeof(u32) :501-503; nftables meta.c:669 4*BITS_PER_BYTE agrees) — the u64 is socket cgroupv2 (nft_socket.c:54), both pinned. Opaque abstractions (pkt_flow, pkt_fibkey beyond fibkey_wf, pkt_ctdir tuple columns, pkt_xfrm, pkt_tunnel, pkt_inner, connlimit keys) untouched per TODO.md. Previously-raw reads now normalized: do_load LRt/LSocket/LOsf/LSymhash/ LNumgen-random; VM IMetaLoad/IRtLoad/ISocketLoad/IOsf/ISymhash; lim_cost/quota_cost (meta len), l4_csum_slot's l4proto read, nat_addrfamily's nfproto read — all via read_meta & co. Theorem-statement changes (every one): - NEW (all in make axioms): Bytes.fit_length, Bytes.fit_exact, Bytes.fit_idempotent; Syntax.read_meta_length, meta_load_length, ct_load_length, read_rt_length, read_socket_length, read_osf_length, read_numgen_length, read_symhash_length (AXIOM_GATE 77 -> 88). - RETIRED (strata note in THEOREMS.md §7): Syntax.meta_load_len / ct_load_len — conditional on the old PARTIAL meta_fixed_len / ct_fixed_len option tables, which are retired with them; successors are the UNCONDITIONAL meta_load_length / ct_load_length / read_meta_length (strictly stronger: old = new at the pinned keys). - RESTATED Regression/Limit_Over.v: mtu_packet_overspends_small_quota and bytemode_length_is_live hypotheses pin the FULL 4-byte u32 meta len register ([0;0;5;220] for 1500; [0;0;0;1]/[0;0;0;3]) — skb->len is a u32, sub-4-byte oracle values were model artifacts; quota_consumes_packet_len's conclusion reads read_meta p MKlen. - RETIRED Example Semantics/TypedEval.v tev_stuck_undecodable (its premise — an undecodable ct zone register — is no longer a representable state; every conntrack entry has a zone, default id 0); successor tev_ctzone_always_decodes pins the read evaluating. - All pre-existing headline theorems (AXIOM_GATE list) verbatim; all 88 Closed under the global context. Optimizer fidelity fix forced by the total width tables: Optimize_Concat.concat_merge_pair (and the K>=3 recogniser via no_guard_fields) now excludes the frontend's implicit-guard meta keys (concat_guard_field: l4proto, nfproto, iiftype, oiftype, protocol) from concat tuples — with every meta key fixed-width the recognisers would otherwise absorb a hoistable guard into the tuple, diverging from nft -o's hoisted shape (pinned by Optimize_SetGuarded_LinkLayer_Witness). Compiler/Compile.v's private slot table is now DERIVED from the kernel table (meta_slot_width = max 4 (meta_width k)); Optimize_XorFold's scope note updated: the identity-mask drop is now blocked ONLY by the byte RANGE (nat bytes), no longer by width. Gates (all green, floors/ceilings unchanged): corpus 2532/2532, byteorder 21/21, source-sweep pass=1198 >= floor 1198, objects-sweep 14/14, corpus-okfail pass=1008/1391 floor=1008 false_accept=47 ceil=47, validate 28/28, typecheck-rulesets 4/4, illtyped-reject 13/13, gen-check 4/4, boundary ok, axioms 88/88 closed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…harged for every frontend program
The kernel admits a rule only after nft_validate_register_load/store checks
every register operand (linux-6.18.33 nf_tables_api.c: nft_parse_register's
netlink-number -> 32-bit-word-index map, the NFT_REG32_NUM=20-word/80-byte
struct nft_regs file with data words 4..19, nonzero lengths, and the 16-byte
struct nft_data value cap). This commit states that validator over the
bytecode and proves EVERY compiled frontend output passes it — BY
CONSTRUCTION (a fail-loud lowering admission), never a hypothesis.
New file theories/Compiler/RegsValid.v:
- nft_reg_index / reg_load_ok / reg_store_ok / imm_value_ok / data_reg_ok:
the kernel bounds, each constant cited to its kernel source line.
- instr_regs_ok: ONE ARM PER Bytecode.instr CONSTRUCTOR (51/51, no
catch-all), each register operand checked at the length the kernel's
expression init validates it with (per-arm citations: nft_meta/ct/rt/
socket/osf/numgen/hash/exthdr/payload/cmp/range/bitwise/byteorder/lookup/
dynset/objref/immediate/nat/masq/redir/tproxy/fwd/queue/fib/xfrm/tunnel/
dup .c). The W1 width tables (meta_width & co.) are reused unchanged —
one width table per oracle. Set-keyed operands (klen/dlen live in the
set object, not the expression) are checked at word granularity; lossless
because the loads that fill the span are store-checked at full width.
- regs_valid / regs_valid_prog + regs_valid_app.
Lowering admission (theories/Surface/Lower.v):
- lower_rule now admits a rule only if RegsValid.regs_valid
(Compile.compile_rule r) — the frontend twin of nft's own evaluate-time
register-allocation bound; new fail-loud error LEregalloc (lerr grew one
constructor; lerr_message extended). No accepted corpus/sweep rule is
affected (all floors identical), so the check is pure insurance + proof
leverage.
New file theories/Compiler/RegsValid_Proofs.v — theorem additions:
- HEADLINE lower_ruleset_default_regs_valid: for every ruleset lower_ruleset
accepts, every chain's DEFAULT-pipeline bytecode
(compile_chain_default = compile o xorfold o paymerge) satisfies
regs_valid_prog. Quantified over ALL lowerings, no hypothesis, axiom-free.
- lower_ruleset_compile_regs_valid: the plain-compile mirror.
- lower_ruleset_regs_ok / lower_rule_regs + the chain/table plumbing
(numgen_free walk pattern).
- Pass preservation from the passes' own guards alone: paymerge_rule_regs
(seg_can_merge's 16-byte NFT_REG_SIZE cap => the fused load/cmp
re-validates; try_merge_regs, merge_body_fuel_regs, payload_seg_imm),
xorfold_rule_regs (xorfold_mc's guard pins |mask|=|xor|=|v|;
xorfold_mc_regs), composed as linearize_rule_regs.
- Non-vacuity Compute pins: regs_valid_rejects_out_of_file (16-byte name at
NFT_REG32_15 overflows the file), regs_valid_rejects_wide_immediate
(17-byte nft_data), regs_valid_accepts_compiled_match.
Pre-existing theorem statements: ALL survive verbatim.
Lower_Proofs.lower_ruleset_numgen_free statement unchanged (proof walks the
new admission). No theorem weakened, no hypothesis added anywhere; grep
confirms no packet_wf/env_wf exists.
Gates:
- AXIOM_GATE_THEOREMS 88 -> 90 (both new theorems added; all 90 "Closed
under the global context").
- Runtime twin wired into make corpus: extracted/corpus_test.ml asserts
RegsValid.regs_valid on every compiled corpus rule and FAILS the run on
any violation — 2532/2532 blocks pass ("OK: ... (all regs-valid)");
red-tested by inverting the assertion (run goes FAIL/exit 1), reverted.
- make gates fully green, floors identical: corpus 2532/2532, byteorder
21/21, source-sweep 1198 >= 1198, objects-sweep 14/14, corpus-okfail
1008/1008 floor + false-accept 47 <= 47, validate 28/28, typecheck 4/4,
illtyped 13/13, gen-check 4/4, boundary ok.
Docs: THEOREMS.md headline-table row + new section 8 (register-file
discipline); DEVELOPMENT.md file table rows for RegsValid(.v/_Proofs.v).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…fault elide pass; class-L closed byte-identically
The trivial binop nft deletes after its xor constant transfer
(src/evaluate.c binop_transfer_handle_lhs, OP_XOR: the spent
`(reg & 0xff..ff) ^ 0x00` binop is replaced by its left operand) is now a
proved, default-on pass — sound BY CONSTRUCTION, never by hypothesis.
Register bytes are octets by construction (the W1 discipline extended to
byte RANGE): every fixed-width oracle read (meta/ct/rt/socket/osf/numgen/
symhash) is now `fit w (octets d)` — each byte clamped to its low 8 bits
(`Bytes.octet := b mod 256`; a register cell is a u8 lane of the
`u32 data[NFT_REG32_NUM]` word array, include/net/netfilter/nf_tables.h;
every eval-side store writes u8/u16/u32/u64 components, nf_tables_core.h
nft_reg_store8/16/64). `octet` is spelled `mod 256` rather than
`Nat.land b 255` (extensionally equal, `Nat.land_ones`) because this
Stdlib's `cbn` diverges reducing `Nat.land` on literals.
Theorem-statement changes (everything else survives verbatim):
NEW (all axiom-free; AXIOM_GATE 90 -> 93):
- Optimize_Elide.elide_chain_eval : forall c e p,
eval_chain (elide_chain c) e p = eval_chain c e p — UNCONDITIONAL;
the pass rewrites MMasked f op (all-ones@w) (zeros@w) v -> MCmp f op v
only where w = load_octet_width (field_load f) and |v| = w (the exact
residue Optimize_XorFold leaves). Gated. Non-vacuity Compute-pinned
(elide_witness / elide_nonvacuous / elide_leaves_real_mask /
elide_leaves_live_xor / elide_leaves_payload).
- Bytes.data_bitops_fit_octets_id (gated): the all-ones/zero bitwise at a
normalised read's own width is the identity on `fit w (octets d)` —
no hypothesis. Supporting: octet, octets, octets_length, octet_and_255,
data_bitops_id, Forall_firstn, fit_octets_clamped.
- Syntax.load_octet_width (the register-normalised loads) and
Syntax.do_load_bitops_id (gated): the octet identity at the do_load
boundary, definitional.
CHANGED DEFINITIONS (statements of all pre-existing gated theorems kept
verbatim):
- Syntax.meta_load / ct_load / rt_load / socket_load / read_osf /
read_numgen / read_symhash: `fit w d` -> `fit w (octets d)`.
- Optimize_Linearize.linearize_chain := elide_chain ∘ xorfold_chain ∘
paymerge_chain (was xorfold ∘ paymerge); linearize_chain_eval and
compile_chain_default_correct STATEMENTS unchanged, proofs carried
through the new stage.
- Optimize_Registry: new pass_elide; registry = [normalize; base;
paymerge; xorfold; elide]; `-O elide` and --list-passes pick it up via
extraction (no glue change).
RESTATED (non-headline, noted in THEOREMS.md):
- Optiplex_Mark.mark_after_set: was `length v = 4 -> read-after-set = v`;
successor is the STRONGER hypothesis-free
`field_value FMetaMark e (set_meta p MKmark v) = fit 4 (octets v)`
(the old statement is false for an out-of-range byte the clamp now
normalises; every concrete use computes identically).
- RegsValid_Proofs internals: linearize_rule_regs / compile_chain_default_rules
now include elide_rule; NEW elide_mc_regs / elide_bi_regs /
elide_body_regs / elide_rule_regs (the elision only deletes the spent
IBitwise from a validated sequence). Headlines
lower_ruleset_default_regs_valid / lower_ruleset_compile_regs_valid
verbatim.
- Optimize_Linearize examples: default_pipeline_folds_xor now pins the
elided form (load+cmp, NO bitwise); NEW xorfold_alone_keeps_trivial_binop
and default_pipeline_elides_trivial_binop (`meta mark xor 0x3 == 0x1`
default-compiles to [IMetaLoad MKmark 1; ICmp CEq 1 [2;0;0;0]], matching
live nft --debug=netlink byte-for-byte: `meta load mark => reg 1;
cmp eq reg 1 0x00000002`, no bitwise).
Scope-note debt paid: Optimize_XorFold.v's "dropping the mask would be
UNSOUND over the byte model" argument is discharged and rewritten (the
byte-range normalisation it called for is exactly what octets adds);
DEVELOPMENT.md and THEOREMS.md updated to match.
Measured results (all gates green):
- source-sweep pass 1198 -> 1202, mismatch 49 -> 45; floor RAISED to 1202.
The 4 class-L blocks (any/meta.t.payload:174/179, any/ct.t.payload:151/156)
close BYTE-IDENTICALLY: the endian-unportable part was the deleted
bitwise's mask/xor immediates; the residual plain host-order cmp renders
in the goldens' recorded byte order.
- byteorder-gate 21 -> 25 blocks in scope (the same 4 enter the plain-cmp
class), 25 passed / 0 failed.
- corpus 2532/2532 (all regs-valid); objects-sweep 14/14;
corpus-okfail 1008/1391 floor 1008, false-accept 47 ceil 47;
validate 28/28; typecheck 4/4; illtyped-reject 13/13; gen-check 4/4;
boundary ok; axioms: 93/93 closed under the global context.
- reports/default-linearization-audit.md class-L ledger updated (closed;
coverage math 45).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…16/64 Bytes.v cited include/net/netfilter/nf_tables_core.h for the register store helpers in two places (the W1 fit header and the W3 octets header). In linux-6.18.33 nft_reg_store8/16/store_be16/64 and the load twins are static inlines in include/net/netfilter/nf_tables.h (lines 144-181), the same header as struct nft_regs; nf_tables_core.h has no reg_store/load helpers. (fb5697f's commit message repeats the miscitation; the sources are now correct.) Comment-only; full gates re-run green after the rebuild (93 AXIOM_GATE closed, corpus 2532/2532, byteorder 25/25, sweep 1202/1202). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…en class re-ledgered with a true post-W1 blocker
Re-audit of everything the linearization audit had ledgered as blocked, with
the W1-W3 by-construction width discipline landed. Two classes were never
width-blocked but were small, unambiguous emission-fidelity fixes in the
verified reject lowering -- implemented; the survivors are re-adjudicated in
writing with blockers that are NOT width facts.
Class Q (reject guard placement, 3 blocks) CLOSED:
- Lower.rl_push_head / push_guard_via / ensure_dep_via / ensure_dep_head:
the reject dependency guard (meta l4proto tcp for `reject with tcp
reset`, the family guard for `with icmp/icmpv6` on inet) lands at the
RULE HEAD, mirroring nft's evaluate-time list_add
(src/evaluate.c stmt_reject_gen_dependency: "Otherwise we'd log things
that won't be rejected"). Match-synthesised deps keep their in-place
ensure_dep position; dedup is placement-independent.
- CORRECTION of the audit's (and DEVELOPMENT.md class E's) claim that the
two placements were "packet-equal / pure placement": WRONG for stateful
bodies -- a counter/log/mark-write between the positions runs under
guard-last and not under guard-first. Both docs corrected.
- ip/reject.t.payload:37, ip6/reject.t.payload.ip6:33,
inet/reject.t.payload.inet:67 byte-identical from source; live nft 1.1.6
netns check byte-identical (guard before mark cmp and counter).
Class R (bare-reject family concretization, 4 of 5 blocks) CLOSED:
- Lower.deps_pinned_nfproto (over the per-rule guard/dedup set: meta
nfproto, or an IPv4/IPv6 ethertype under any layer_class spelling --
meta protocol / ether type / payload @ link+12/+16; the 0x8100 vlan tag
does not pin) + Lower.reject_type_code now taking the pinned family:
a BARE reject on inet/bridge/netdev concretizes from icmpx (2,1) to
icmp (0,3) / icmpv6 (0,4) exactly when nft's
stmt_evaluate_reject_default does; explicit `with icmpx` never does
(the ICMPX break in stmt_evaluate_reject_inet_family).
- inet/reject.t.payload.inet:79/:85, bridge/reject.t.payload:81/:87
byte-identical; inet:135 keeps the concretized reject, open on class S
only. Live nft netns check byte-identical (pinned and unpinned).
Theorem-statement delta: NO pre-existing theorem statement changed (all
survive verbatim; push_guard/ensure_dep keep their exact types as instances
of the _via generalisation; reject_type_code is a Definition and gained the
pinned-family argument). ADDED, all axiom-free and in AXIOM_GATE_THEOREMS
(93 -> 98, every verdict "Closed under the global context"):
- Reject_GuardFirst.udp_guard_breaks_before_mark_write: DSL dsl_rule_step
on the lowered `mark set 1 reject with tcp reset` and a non-TCP packet
yields no verdict AND an untouched mark (guard breaks before the body
effect).
- Reject_GuardFirst.tcp_mark_written_and_rejected: the TCP packet takes
the write and Reject 1 0.
- Reject_GuardFirst.vm_udp_guard_breaks_before_mark_write /
vm_tcp_mark_written_and_rejected: the same two facts over the COMPILED
rule (vm_rule_step (compile_rule ...)).
- Reject_GuardFirst.guard_last_leaks_the_write: the counterfactual -- the
pre-fix guard-last body writes the mark on the same non-TCP packet, so
the placements are observably different (the regression trip wire).
Non-gated pins added: Reject_GuardFirst.counter_guard_first /
mark_guard_first (lowered body order: guard BEFORE SCounter/SMetaSet;
SCounter is verdict-neutral and stateless in the model, so the counter
placement is pinned structurally and the observable-effect twin uses the
mark write; the limiter cannot witness ordering -- Known_Infidelities
gate_limit_drained); Lower.v Examples reject_bare_inet_unpinned /
_pinned_v4 / _pinned_v6, reject_icmpx_explicit_stays_abstract,
deps_pin_spellings.
Re-adjudications written into reports/default-linearization-audit.md (each
open class now names a post-W1 blocker that is not width):
- P (family-implied meta protocol elision, 2): chains carry no family; the
fact lives in hook dispatch. Out of scope for an unconditional pass.
- P' (transport-dep dedup, 2): ORACLE INDEPENDENCE, not width -- the
missing fact is the value implication nexthdr=58 -> l4proto=58; a
blanket definitional equation would be kernel-unfaithful on
extension-header packets (meta l4proto is pkt->tprot, resolved past
exthdrs; ip6 nexthdr is the raw byte 6), so the faithful close is a
tprot-deriving packet-record restructure (Fib_Local-style de-oracle of
the transport protocol), not a W4-sized fix.
- S (inet+ether guard choice, 1): emission-fidelity item in the class-G
guard machinery; its R-half closed here.
- log canonicalization (4): attribute text, no register involved.
- fib presence (2): the e_routes result column is an env-oracle VALUE;
{0,1}-ness is a value-range fact a width clamp cannot supply (kernel
DERIVES presence: nft_fib_store_result stores !!index) -- re-ledgered as
oracle-typed fib result column.
- (b) 27 host-endian display blocks: golden-text byte order, model-
independent, unchanged.
- Optimizer scope-note sweep: no note remains that refuses a rewrite on
unbounded-width/byte-range grounds (XorFold/Syntax rewritten in W3;
Concat = nft-shape fact; DataMap = write-aliasing; Vmap/Uncond =
quantification scope; Fib_Local's unbounded-nat note is about payload
bytes, correctly outside the W1/W3 oracle clamp).
Gates (all green, floors ratcheted): source-sweep pass 1202 -> 1209 (floor
raised, mismatch 45 -> 38, every survivor ledgered), corpus 2532/2532,
byteorder-gate 25/25, objects-sweep 14/14, corpus-okfail 1008 floor /
47 ceil, validate 28/28, typecheck 4/4, illtyped 13/13, gen-check 4/4,
boundary ok, axioms 98/98 closed. No Axiom/Admitted/Parameter anywhere;
no packet_wf/env_wf-style hypothesis introduced.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ntics per side; pure/flat strands demoted to proven projections THE category error this run eradicates — an effectful rule modeled by a pure evaluator — is closed at the architecture level: the semantics of a ruleset is now ONE unified fuel-bounded fold per side that BOTH threads every state effect (meta/ct writes, dynset env writes, notrack, limiter depletion, via dsl_rule_step/vm_rule_step) AND follows control flow (jump/goto/return, user chains, multi-table + hook dispatch), with cross-packet env carry. A jumped-to chain sees the caller's accumulated writes; the callee's writes survive the return. "Mutation x jump/goto is not jointly verified" no longer appears anywhere: it IS jointly verified, and every earlier evaluator is a theorem-licensed projection of the unified fold. New evaluators (Semantics.v, section "The unified semantics"): - DSL: eval_rules_u / eval_table_u / eval_ruleset_u / eval_hook_u / eval_hook_env_u; VM: run_rules_u / run_table_u / run_ruleset_u / run_ruleset_env_u. New theorems (all axiom-free, all in AXIOM_GATE_THEOREMS): - Correct.compile_table_u_correct / compile_ruleset_u_correct / compile_hook_u_correct / compile_seq_hook_u_correct (stratum 8 HEADLINE): compiled VM unified fold = DSL unified fold — verdict AND left state — for every fuel/chain-env/base-list/hook/packet-sequence. Only hypothesis: rule_numgen_free (VM-only numgen sweep), discharged for every frontend-emitted program by Lower_Proofs.lower_ruleset_numgen_free. No hypothesis excludes any effect or any control-flow shape. - Semantics.eval_rules_u_writefree / eval_table_u_writefree / eval_ruleset_u_writefree / eval_hook_u_writefree (projection license 1): on write-free rules (rule_writefree / chains_writefree / bases_writefree: no meta/ct set, dynset, notrack, limiter/quota/connlimit) the pure jump strand is the verdict projection of the unified fold with state untouched: eval_rules_u fuel cs rs e p = (eval_rules_j fuel cs rs e p, (e, p)). - Semantics.eval_rules_u_mut_proj / eval_table_u_mut_proj (projection license 2): on transfer-free rules (rule_plain — a STEP-THREADED faithful-domain predicate: rule writes provably cannot touch verdict maps, dsl_rule_step_vmap et al.) the flat mutation strand is the unified fold's projection: fst = eval_rules_mut, env = snd of eval_rules_mut_env. This is the "threaded redefinition" Correct.v's old rationale block said could not even be stated; that block is rewritten accordingly. - Correct.run_table_writefree_compiled (VM-side license), Correct.eval_chain_writefree_jumpfree_proj (flat pure strand license, packaged), Nft_Tactics.nft_yields_unified (+ accepts/drops forms: the config surface upgraded to unified-semantics statements under the one-reflexivity nft_writefree check). - Supporting: dsl_rule_step_writefree, rule_step_plain, rule_plain_vmap_ext, body_step_vmap / after_step_vmap / rule_step_vmap / dsl_rule_step_vmap / limit_sweep_body_vmap (e_vmap invariance under the fold), after_step_verdict_drop, chains_writefree_lookup, chains_numgen_free(_lookup), base_numgen_free, run_rules_u_compile. Witness pins (new Regression/Setread_UnderJump.v, Compute-verified, DSL+VM, gate-listed): intra-rule set-then-read ACCEPTS inside a jumped-to chain (setread_under_jump_accepted / vm_...); caller write visible in callee; callee write survives the return; dynset learned across a jump (+ env-left pin, + non-vacuity drops); the retired-as-independent pure eval_table computes the wrong verdict class there and its rule_writefree license check is false (pure_strand_misses_the_write / setread_rule_not_writefree). License-boundary pins (Correct.v): rg_jump_not_plain, unified_strand_jump_drops beside the re-framed mut_strand_jump_pin. Pre-existing headline theorems: ALL survive verbatim (compile_chain_correct, compile_chain_mut(_env)_correct, compile_seq_mut_correct, compile_table/ruleset/hook/seq_correct, optimizer family, fuel-discipline family) — none weakened, none re-quantified; their status changes from parallel semantics to licensed projections (strata-retirement note in THEOREMS.md section 3: no evaluator deleted, successor for out-of-domain inputs is the _u family). Docs: Semantics.v header matrix rewritten (unified semantics + license table; DISJOINT-strands admission deleted); eval_rules_j/eval_ruleset/eval_hook headers rewritten as projection evaluators; Correct.v strata list + rationale block rewritten; Main.v gains Axis 0 (main_compile_hook_u_correct / main_compile_seq_hook_u_correct restatements + Print Assumptions); THEOREMS.md sections 1-3 overhauled (stratum 8 rows, projection-license matrix, example-config license coverage incl. the honest router residual); DEVELOPMENT.md matrix + ledger entry 3 + file map updated; CONFIG_PROOFS.md gains "The projection license (U1)" section. Per-config licenses (Compute): Tutorial_Proofs.tutorial_license, Ruleset_Verified.firewall_inbound_license, Optiplex_Antispoof.vmfilter_output_license. Honest residual (documented in THEOREMS.md section 3): the router global table carries one limiter rule, so Router_* example statements are not yet licensed as unified-semantics statements — designated follow-up: restate over eval_table_u or prove a limiter-tolerant license. Gates: make gates fully green (proofs; axioms — every AXIOM_GATE theorem "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>
…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>
…le fold at every hook; trace strand retired; dnat/snat/masquerade/redirect compiled-certified The NAT packet rewrite + flow-keyed e_nat establish/reuse + no-usable-address NF_DROP are now effects OF the single per-rule fold, evaluated AT the NAT terminal the walk actually reached — a vmap HIT structurally never runs them (outcome provenance) — on BOTH sides (DSL terminal_step / VM INat case), threaded through the unified jump-aware evaluators, at every netfilter hook (Section AtHook: rule_step/run_rule_step and every effect-threading evaluator now take the hook h; redirect/masquerade are hook-dependent). The side evaluator eval_rules_trace/eval_chain_trace/trace_nat_drops (Known Infidelity 2: NAT dispatched out-of-band on r_nat at any terminal verdict) is DELETED; chain_out/chain_out_env re-based on eval_chain_u (the unified fold's chain form). DSL and VM share the effect core verbatim (apply_nat_c/nat_drops_c; the VM feeds INat's register operands); the DSL port model is extended kernel-faithfully (masq/redir primary operand IS its port: nat_portonly/ nat_port_val), making the bridge unconditional beyond numgen-freedom. Theorem-statement deltas: - NEW headline (AXIOM_GATE): Correct.compile_nat_effect_correct — the per-rule bridge run_rule_step h empty_rf (compile_rule r) e p = rule_step h r e p under its NAT-effect name; the _u traversal family now certifies the NAT data plane under jumps/multi-chain/hook dispatch. - Hook threading (h prepended; statements otherwise verbatim): rule_step/terminal_step/end_step/dsl_step, run_rule_step, eval_rules_mut(_env), eval_chain_mut(_env), run_program_mut(_env), run_chain_mut(_env), eval_rules_u/eval_table_u/run_rules_u/run_table_u/eval_ruleset_u/ run_ruleset_u/eval_hook_u(env)/run_ruleset_env_u, all their compile theorems (compile_chain_mut*, compile_seq_mut, compile_table_u/ruleset_u/hook_u/ seq_hook_u), the projection licenses (writefree/limiter-tolerant/mut_proj), Nft_Tactics.nft_yields_unified, Main.v restatements. - rule_mutfree/rule_writefree now require rule_natfree (a NAT terminal IS a write); rule_step_mutfree/terminal_step_mutfree/end_step_mutfree/ dsl_step_after_free gain that hypothesis; Correct.writes_instr counts INat. - RESTATED (post-M3 the old blanket claims are genuinely false — a cs containing the masquerade chain is outside every pure-strand license): Router licenses now over the NAT-free restriction global_tol_chains/ global_tol_hooks (Router_Input.inbound_licensed/router_rules_licensed, Router_Forward.forward_licensed, Router_Private.private_rules_licensed, Router_Hooks.input/forward_hook_licensed, Router_Realistic.*_licensed_real); Nft_Demo_Concrete.demo_*_unified now forall h over the FULL chain env. - RETIRED: postrouting_hook_licensed (masquerade as a pure projection) — successors Router_Hooks.postrouting_hook_unified + Router_NatHook.postrouting_hook_verdict_trichotomy (both unified); eval_rules_trace_verdict family retires with the strand; Nat_NoAddr_Drop.trace_diverges_from_mut_via_nat_drop / mut_unaffected_still_accepts -> successors mut_agrees_nat_drop / vm_nat_drop_agrees (the NAT NF_DROP is the verdict of THE semantics, DSL + compiled VM); Router_Reach masq_dsl_step_id/bug_dsl_step_id (a NAT rule's step IS its effect) -> masq_rule_step/masq_chain_u. - Pins flipped POSITIVE (AXIOM_GATE): vmaphit_daddr_rewritten = [1;2;3;4] (unrewritten), vmaphit_stores_nat_mapping = None, + miss-side non-vacuity (vmapmiss_*) and VM twins (vm_vmaphit_*/vm_vmapmiss_*); known-infidelity ledger now EMPTY (DEVELOPMENT.md), zero KNOWN INFIDELITY markers in sources. - Optimizer NAT certificates re-proved over the new wrappers (apply_nat_dnat_eq/apply_nat_snat_eq unchanged statements). Gates: ALL GREEN (proofs, axioms 144/144 closed, corpus 2532/2532, validate, parse-test — one runtime expectation updated: eval_chain_mut now DROPS the no-address redirect, agreeing with the kernel — gen-check, boundary). Audit-C repairs (challenger R1-R4, doc/naming-level only, no proof changes): - R1 Semantics.v NAT-drop comment: the NF_DROP lives in nat_drops_c, consumed by terminal_step (DSL) and the INat case (VM), compiler-certified by compile_nat_effect_correct (stale "no compiler analogue / lives only in the trace evaluator" wording deleted). - R2 Semantics.v step-function header: "mutation/trace evaluator" -> "mutation evaluator" (trace strand is retired). - R3 parse_test.ml: alias ev_chain_trace renamed ev_chain_u (all call sites) and the section-(E) comment names eval_chain_u. - R4 DEVELOPMENT.md NAT paragraph: explicit unmodeled-feature entry for the NXmap_port/NXmap_full concat-map value-slot PORT skip (identical on both sides, compile theorem exact; pointer from THEOREMS.md now resolves). - Optional: Router_NatHook.eval_trace_bases renamed eval_u_bases. No theorem statements changed; make gates fully green (144/144 axiom-gate theorems closed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…set's own env-out; external-step stratum retired The between-packet environment of the sequence semantics is now DEFINITIONALLY the ruleset's own env-out from the unified (U1) effect-threading hook evaluator (seq_eval_env over eval_hook_env_u / run_ruleset_env_u) — there is no external step function left anywhere for a caller to model (or mis-model) the ruleset's cross-packet learning with. Theorem-statement deltas: - RENAMED (statement verbatim): compile_seq_hook_u_correct -> compile_seq_hook_correct (Main.v: main_compile_seq_hook_u_correct -> main_compile_seq_hook_correct). With the external-step stratum gone it is the unique sequence theorem, so the _u disambiguator is retired with the thing it disambiguated against. - RETIRED (deleted; THEOREMS.md strata-retirement note "M4 cross-packet carry" names the successor): Semantics.seq_eval (the sequence combinator over an EXTERNAL caller-supplied step : verdict -> env -> env), Correct.seq_eval_ext, Correct.compile_seq_correct, Main.main_compile_seq_correct, Main.pre_split_compile_seq_correct. Successor: seq_eval_env instantiated with eval_hook_env_u (VM: run_ruleset_env_u), compile theorem compile_seq_hook_correct. - NEW positive pins (Regression/Seq_Hook_Carry.v, all in AXIOM_GATE and "Closed under the global context", quantified over every netfilter hook): seq_hook_limit_depletes / vm_seq_hook_limit_depletes — a limiter inside a jumped-to chain gives identical back-to-back packets [Accept; Drop] (the bucket packet 1 depletes is the bucket packet 2 reads); seq_hook_dynset_learns / vm_seq_hook_dynset_learns — dynset learning crosses a jump, a base-chain (priority) boundary and a packet boundary; plus non-vacuity Examples (limit_bucket_left_empty, no_learning_no_drop). - AXIOM_GATE_THEOREMS: compile_seq_hook_u_correct -> compile_seq_hook_correct, compile_seq_correct removed, 4 Seq_Hook_Carry pins added. - semtest (4c) moved off the external step onto the unified env-out; its limiter spec fixed to a faithful bucket (rate 1/second burst 2: per-packet cost 1, cap 2 — the old rate-2 spec cost-rounded to 0 under the M2 model) and the expected [accept; accept; drop] sequence is now asserted, not just DSL=VM. - Docs: Semantics.v matrix row + § Stateful accumulation rewritten as the retirement note; Correct.v strata list; THEOREMS.md §1 axis row, §2 classification rows, §3 evaluator table + new strata-retirement note; DEVELOPMENT.md limiter entry, gap-closing status, evaluator architecture. All gates green: proofs axioms corpus byteorder-gate source-sweep-gate objects-sweep-gate corpus-okfail-gate validate parse-test gen-check boundary. No new Axiom/Admitted/Parameter; no new hypotheses (base_numgen_free is pre-existing and discharged by Lower_Proofs.lower_ruleset_numgen_free). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e stops being verdict-only
The 18-stage optimize_table_uncond is now certified, hypothesis-free, against
the EFFECT-OBSERVING chain semantics eval_chain_mut_env h (the single
rule_step fold: meta/ct writes, dynset env writes, notrack, limiter/quota/
connlimit consumption, NAT data plane): a stage can no longer preserve every
eval_chain verdict while altering a write a later hook observes.
Theorem-statement deltas (all pre-existing headline statements survive verbatim):
ADDED (new file theories/Optimizer/Optimize_MutEnv.v, ~5000 lines):
- HEADLINE optimize_table_uncond_mut_env_correct (AXIOM_GATE, prints Closed
under the global context): optimize_table_uncond c = (n',d',c') ->
eval_chain_mut_env h c' (env_with_sets base d') p
= eval_chain_mut_env h c (env_with_sets base d') p, for every hook h,
base env, packet -- verdict AND resulting environment, no hypothesis on c.
- SUPPORTING optimize_table_mut_env_correct_uncond_gen (the (n,d)-threaded
whole-pipeline form) + 15 per-stage optimize_rules_*_mut_env lemmas +
absorb/ctmask/base-pass/normalize effect lemmas, composed exactly like the
verdict harness but under ONE deployed environment.
- Fold-level effect certificates for the three effect-rewriting merges:
eval_rules_mut_env_map_merge (datamap), eval_rules_mut_env_dnat_merge,
eval_rules_mut_env_snat_merge (on M3's apply_nat_{dnat,snat}_eq and
dsl_step_map_merge), plus rule_step characterisations of the NAT shells.
- Generic machinery: rule_step_sm_stable (a rule step preserves e_set/e_map
outside its dynset write targets; e_vmap everywhere), the write-free-block
projection eval_rules_mut_env_mutfree_prefix (a rule_mutfree block evaluates
as pure eval_rules with state unchanged), and per-stage dynset-freshness
preservation.
OPTIMIZER DEFINITION changes (verdict theorems re-proved over them, unchanged
statements; corpus/validate/difftest/witness gates all green):
- EFFECT-SAFETY GUARD rule_mutfree r1 added to the 15 pure-merge pair
recognisers (value_merge_pair, concat_merge[K/g]_pair, value_mergeGs_pair,
range_merge[Gr]_pair, ivsett/dscp/mix pairs, vmap_run_pair[G], dscpv_run_pair,
absorb_pair, ctmask_pair): a merge that would re-run an effect-bearing shared
tail is refused, making every pure merge live on the write-free fold
projection (companion *_pair_mutfree lemmas extract the guard).
- map_merge_pair (datamap) additionally requires is_payload_load on the key
field -- exactly the hypothesis of its effect certificate (a meta key could
be rewritten by the first rule's own meta set).
- Optimize.dedup_rule fires only on rule_mutfree rules (its match reordering /
nodup is verdict-preserving but not effect-preserving on write-bearing or
limiter-bearing bodies).
- Optimize_Uncond.chain_seed now also collects the dynset WRITE-target names
(rule_dynset_names), so seed_start mints past every name a rule can write:
no dynset can clobber a minted declaration (seed_start_dynset_fresh) -- the
headline stays hypothesis-free by construction.
RETIRED admissions: the "VERDICTS ONLY" scope note on
optimize_table_uncond_compile_correct (the formal gap "a stage could preserve
every eval_chain verdict while altering a mark write that flips a later hook's
decision" is now closed by theorem) and the "NOT composed through
optimize_table" caveat on the datamap/dnat/snat effect certificates
(Optimize_Table.v fidelity note). THEOREMS.md and DEVELOPMENT.md updated:
optimizer axis now lists both observation levels.
Gates: ALL GREEN (proofs, axioms incl. the new AXIOM_GATE theorem, corpus
2532/2532, corpus-okfail, validate 28/28, parse-test, gen-check, boundary).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…erdict, env, packet)
R1: new full-state flat fold export Semantics.eval_rules_mut_st/eval_chain_mut_st
(option verdict * (env * packet)); bridges eval_rules_mut_env_st /
eval_chain_mut_env_st (mut_env = (fst, fst.snd) of mut_st), eval_rules_mut_st_fst;
unified-semantics license eval_rules_u_mut_st_proj / eval_table_u_mut_st_proj
(whole-triple equality on rule_plain). The whole Optimize_MutEnv development is
restated at the full-state evaluator and the NEW HEADLINE is
Optimize_MutEnv.optimize_table_uncond_mut_st_correct (hypothesis-free:
eval_chain_mut_st h c' (env_with_sets base d') p = eval_chain_mut_st h c ... p) —
verdict, env-out AND packet-out; added to AXIOM_GATE_THEOREMS.
Precision pin (Part H): [meta mark set 0x1] vs [] identified by eval_chain_mut_env
(mutst_pin_mut_env_blind) but distinguished by eval_chain_mut_st
(mutst_pin_mark_observed: exported pkt_meta MKmark = [0;0;0;1] vs [];
mutst_pin_distinguishes, also gate-listed).
Theorem-statement deltas: all M5-added *_mut_env stage/merge/base lemmas are
STRENGTHENED to *_mut_st (same shapes, full-state evaluator; none pre-dated M5);
the reported M5 headline optimize_table_uncond_mut_env_correct survives VERBATIM
as a projection corollary of the mut_st headline (still gate-listed). No pre-M5
statement changed. eval_rules_mut_st_{map,dnat,snat}_merge now genuinely carry
(env, packet) out (R3).
R2: prose in Optimize_Uncond.v scope note 2, THEOREMS.md headline rows/projection
table, DEVELOPMENT.md optimizer entry now describe the full-state observable
truthfully. R4: honest jump-scope note (flat fold skips callees; jump-bearing
chains certified against the flat projection only) in Optimize_MutEnv header,
THEOREMS.md and DEVELOPMENT.md — no 'can no longer' claim covering jumps.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…eorem; gate the whole-triple licenses The top-level HEADLINE summary row 'optimizer pipeline, EFFECT level' was stale first-attempt text: it named optimize_table_uncond_mut_env_correct (demoted to SUPPORTING corollary by the taxonomy table below) and attributed mark writes to the env observable, which mutst_pin_mut_env_blind proves blind to them. The row now crowns Optimize_MutEnv.optimize_table_uncond_mut_st_correct under eval_chain_mut_st h with the full (verdict, env, packet) observable, attributes mark/ct-set to the packet half, keeps mut_env_correct as the surviving projection corollary, and points at the flat-fold jump-scope caveat. AXIOM_GATE_THEOREMS additionally gates the whole-triple licenses Semantics.eval_rules_u_mut_st_proj and Semantics.eval_table_u_mut_st_proj (component forms were already gated); axioms gate 152/152 closed, full suite ALL GATES GREEN. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… per side; jx twin, entry-state predicates, and the clean stratum retired Theorem-statement deltas (everything else survives verbatim): Evaluator consolidation (statements/values UNCHANGED, definitions demoted): - Exactly ONE recursive rule-list/jump traversal per side remains: the Fixpoints eval_rules_u (DSL) and run_rules_u (VM). Converted to NON-RECURSIVE Definitions with unfolding equations restating the historical recursion verbatim (_nil/_cons, _0/_S): eval_rules, run_program (fold_right of the pure per-rule read); eval_rules_j, run_rules_j (nat_rect on the fuel); eval_ruleset, run_ruleset, eval_ruleset_u, run_ruleset_u (fold_left with a settled accumulator); eval_rules_mut_st (fold_left of rule_step with an absorbing stopped accumulator; NEW VM twin run_program_mut_st). eval_rules_mut / eval_rules_mut_env / run_program_mut / run_program_mut_env are now projections BY DEFINITION of the full-state folds; the in-strand bridges (eval_rules_mut_env_fst/_st, eval_rules_mut_st_fst, run_program_mut_env_fst) survive verbatim with reflexivity-level proofs. Fuel discipline (jx stratum RETIRED; THEOREMS.md strata note): - DELETED: eval_rules_jx (exhaustion-observable twin traversal), eval_rules_jx_agree/_S/_monotone/_stable, eval_rules_jx_adequate(_aux), and the jx-witnessed eval_rules_j_fuel_stable. - SURVIVE VERBATIM with new direct rank-descent proofs (eval_rules_j_fuel_indep_aux): eval_rules_j_fuel_indep, eval_table_fuel_indep. - RESTATED (same name/role): eval_table_policy_is_fallthrough - a None at adequate fuel persists at every adequate fuel (no jx witness in the type). - NEW at the unified semantics: eval_rules_u_vmap, rule_step_targets_below, chain_ranked_u, eval_rules_u_fuel_indep(_aux), eval_table_u_fuel_indep, chains_plain, chains_plain_ranked_u - effectful configs are inside the adequacy story, not carved out of it. Pure-walk projection (notrack admitted): - NEW: body_item_purewalk, body_purewalk, rule_purewalk_ok - rule_applies_walk is the break/no-break projection of body_step on loadable effect-free-but-notrack bodies; the walk's set_untracked threading is licensed as body_step's own SNotrack transform. (The acceptance test's deletion route is semantically impossible: the threading is pinned kernel behaviour, Regression/Notrack_CrossRule.v, and removing it or fold-projecting the walk would falsify compile_chain_correct on limiter bodies without a cascading run_rule rewrite; milestone step 2's rule_purewalk_ok disjunct taken instead - documented for the challenger, T9 grep = 1, the definition line.) Entry-state predicate replacement: - NEW: rule_jumpfree_syn, rules_jumpfree_syn, chain_jumpfree_syn + rule/rules/chain_jumpfree_syn_sound (syntactic -> forall e p semantic); NEW gated packaging Correct.eval_chain_writefree_jumpfree_syn_proj. Clean-predicate stratum RETIRED (grep 'rule_clean' over theories = 0): - DELETED: Optimize_ValueSet mc_clean/bi_clean/rule_clean/rules_clean, eval_matchcond_clean_env, rule_applies_clean_env, body_synproxy_stops_clean, body_has_notrack_clean, rule_clean_env, eval_rules_clean_env; Optimize_Table rule_clean_body_stmts_nil, rule_clean_body_matches_clean, forallb_bi_clean_map_BMatch, forallb_mc_clean_nodup, dedup_rule_clean, simplify_rule_clean, rules_clean_map_simplify_dedup, rules_clean_prune_noops, rules_clean_dce, optimize_preserves_rules_clean; Optimize_Table_Inv rule_lookup_vmapN_ok, rs_vmapN_ok. Dead since the unconditional pipeline; successor is the read-freshness generation (Optimize_Uncond.rule_set_fresh family). (field_value_env_with_sets / do_load_env_with_sets kept - still used.) AXIOM_GATE: removed eval_rules_jx_monotone, eval_rules_jx_adequate, eval_rules_j_fuel_stable; added eval_rules_j_fuel_indep, eval_rules_u_fuel_indep, eval_table_u_fuel_indep, rule_purewalk_ok, eval_chain_writefree_jumpfree_syn_proj (152 -> 154, all Closed). Docs: THEOREMS.md (fuel section restated, M6 consolidation + retirement notes, matrix rows for the syntactic license and the notrack walk projection), DEVELOPMENT.md, Semantics.v header matrix. Gates: ALL GREEN - proofs, axioms 154/154 Closed, corpus 2532/2532, byteorder 25/25, source-sweep 1209 (floor 1209), objects-sweep 14/14, corpus-okfail 1008/floor 1008 false-accept 47/ceil 47, validate 28/28, parse-test, gen-check, boundary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…-note ledger; gate the per-rule bridge Comment/doc history-narration cleanup only — no definition, statement, or proof logic changed. Every comment now describes what the code IS; archaeology of evaluators that no longer exist in the tree is removed. All gates stay green and axiom-free. Removed obituary comments referencing already-deleted evaluators/predicates: - Semantics.v: seq_eval, dsl_rule_step/vm_rule_step, eval_rules_trace/ eval_chain_trace, the exhaustion-observable "jx" twin strand, dsl_step_limit_free - Correct.v: compile_seq_correct stratum notes; vm_rule_step_compile_rule note; stratum-7 RETIRED list item - Main.v: compile_seq_correct / pre_split_compile_seq_correct notes - Regression/Nat_NoAddr_Drop.v, Known_Infidelities.v: eval_rules_trace / trace-strand notes - Regression/Setread_UnderJump.v, Setread_IntraRule.v: two-fold-split / "retired pure strand" notes - Examples/Router_Hooks.v, Router_Reach.v: postrouting_hook_licensed / masq_dsl_step_id notes - Optimizer/Optimize_Table.v, Optimize_Table_Inv.v, Optimize_ValueSet.v: retired clean-predicate notes - Surface/Lower_Proofs.v: retired Elab.elab_matchcond_correct notes Living docs (THEOREMS.md, DEVELOPMENT.md): deleted the standalone strata-retirement ledgers (M2/M3/M4/T1/U1/M6 narratives), the RETIRED/deleted-theorem table rows (compile_seq_correct, optimize_preserves_rules_clean, seq_eval), the U1 status-change note, and the "### Strata retirement: IR/Elab.v" section; fixed every now-dangling "§ strata retirements" cross-reference; rewrote affected passages to present tense. Surviving present-tense status markers (SUPERSEDED-vacuous with _real successors, KNOWN-UNFAITHFUL non-shipped passes) are kept — they describe current theorem roles, not deletion history. Gate strengthening: added Correct.run_rule_step_compile_rule (the load-bearing per-rule bridge: run_rule_step (compile_rule r) = rule_step r on numgen-free rules) to AXIOM_GATE_THEOREMS; verified Closed under the global context. Gates: proofs, axioms, corpus 2532/2532 0 mismatches, byteorder 25/25, source-sweep 1209, objects 14/14, corpus-okfail 1008/47, validate 28/28, gen-check 4/4, boundary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… no deletions) Add eval_rules_mut_st_run_merge_abs (Optimize_MutEnv, Section WithHook): the direct first-match N-way merge/absorption certificate over the state-threading fold eval_rules_mut_st, mirroring the pure Optimize_ValueSet.eval_rules_run_merge_abs which is stated over the write-free verdict eval_rules. The new lemma's conclusion is the FULL observable of the fold (verdict AND resulting (env, packet)), proving the same shared-body/shared-r1 run collapses to the merged shell whose head realises the existsb disjunction. The rule_mutfree hypotheses on every shell (merged + run) are load-bearing, not incidental: on the state fold a non-firing shell can still advance the env (a limiter head consumes at its position) and a firing non-terminal shell re-runs its body on the next shell, so an unconstrained merge is NOT state-preserving. rule_step_mutfree pins each shell's step to leave the state at (e,p); the threaded state is then constant across the run and the first-match/break argument is exactly the pure induction lifted into the fold's (verdict, state) pair. No mention of the pure eval_rules in statement or proof. Additive only: no Definition/Theorem/Lemma deleted or restated. Gated in proof/Makefile AXIOM_GATE_THEOREMS; prints "Closed under the global context". Intended follow-up mapping: the merge-tower sites in Optimize_MutEnv (~675/832/970/ 1115) currently do eval_rules_run_merge_abs (pure) + two eval_rules_mut_st_mutfree_prefix + rewrite Hpure; each can be re-pointed onto eval_rules_mut_st_run_merge_abs (same mutfree/match_loadable/existsb hypotheses already established locally), with the existing eval_rules_mut_st_cons_cong + IH bridging the recursively-optimized tail, after which the pure eval_rules strand and eval_rules_run_merge_abs can be dropped. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…erge/xorfold/elide) + compile_chain_default over the state fold Additive state-threading (eval_chain_mut_st) analogue of the DEFAULT-compile pipeline correctness, matching M5 full-observable fidelity (verdict AND the resulting (env, packet)). No deletions/restatements; the pure theorems stay. New file theories/Optimizer/Optimize_Linearize_MutSt.v: - body_step_tail_cong: body_step is congruent in its tail. - try_merge_body_step / merge_body_fuel_step / merge_body_step: payload-merge preserves the full-state body fold (fused/operand matches are consume-free). - xorfold_body_step / elide_body_step: xor-fold and trivial-binop elision preserve the full-state body fold (rewrite only consume-free BMatch conds). - end_step_outcome_after_cong / rule_step_body_cong: a body-only rewrite that keeps r_outcome/r_after preserves rule_step. - paymerge_rule_step / xorfold_rule_step / elide_rule_step and their chain lifts paymerge_chain_mut_st / xorfold_chain_mut_st / elide_chain_mut_st. - linearize_chain_mut_st: the composed always-on linearization preserves the full state fold, unconditionally. - run_program_mut_st_compile_chain + run_chain_mut_st + compile_chain_mut_st_correct: the plain-compile full-state bridge (_st analogue of Correct.run_program_mut_env_compile_chain), rule_numgen_free only. - linearize_chain_numgen_free (per-pass ngfree preservation) carries the hypothesis to the SOURCE chain. - compile_chain_default_mut_st_correct: HEADLINE — the DEFAULT pipeline's bytecode, run on the state VM, reproduces the source chain's DSL state fold (verdict AND (env, packet)) for every chain/env/packet, under only rule_numgen_free. Each linearization pass is state-preserving with no soundness surprise: the rewrites touch BMatch conditions only, never a statement/write, and every matchcond touched or emitted is limiter-consume-free. Gated in proof/Makefile (AXIOM_GATE_THEOREMS): paymerge/xorfold/elide _chain_mut_st, linearize_chain_mut_st, compile_chain_mut_st_correct, compile_chain_default_mut_st_correct — all "Closed under the global context". make gates fully green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…le over the state fold)
Add optimize_table_uncond_compile_mut_st_correct, the full-state
(verdict AND resulting (env, packet)) analogue of the pure
optimize_table_uncond_compile_correct, over the effect-observing
eval_chain_mut_st fold.
It composes the two existing pieces:
- compile_chain_default_mut_st_correct (the default-compiled optimized
chain's state-VM run reproduces its own DSL state fold, under the
single rule_numgen_free hypothesis every frontend chain discharges),
- Optimize_MutEnv.optimize_table_uncond_mut_st_correct (the 18-stage
consolidation preserves the source chain's state fold at every hook).
Unlike the pure headline (which reads the source at empty_decls because
eval_chain discards the env), both sides run under env_with_sets base d':
the state fold RETURNS the threaded env, so the synthesized declarations
d' the compiled side needs to resolve its set/map lookups are part of the
observable and must appear on both sides for the returned (env, packet)
pairs to match.
Lives in Optimize_Linearize_MutSt (next to compile_chain_default_mut_st_correct),
re-exported as Main.main_optimize_table_uncond_compile_mut_st_correct, and
added to AXIOM_GATE_THEOREMS. Closed under the global context; all gates green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…fold; delete the redundant pure optimizer verdict stack The state-threading fold is now the sole canonical semantics for the optimizer and default-compile axes: a cold reader sees ONE "compiler is correct" headline family, over eval_chain_mut_st / run_chain_mut_st, not a pure eval_chain twin. Main.v retargets: - main_optimize_table_uncond_compile_mut_st_correct is now the single optimizer headline (the pure main_optimize_table_uncond_compile_correct is deleted, not kept alongside it). - main_compile_chain_default_correct retargeted from the pure compile_chain_default_correct onto compile_chain_default_mut_st_correct (state). - pre_split_optimize_table_uncond_correct and pre_split_optimize_table_uncond_compile_correct deleted (they only transported the pure optimizer headlines). State proofs made independent of the pure merge strand: the 4 valueset/dscp/ intervalsethostorder/intervalset merge sites in Optimize_MutEnv.v no longer detour through the pure eval_rules_run_merge_abs; they route through the new Optimize_MutEnv.eval_rules_st_merge_pure, which reads the state-fold certificate eval_rules_mut_st_run_merge_abs back as an eval_rules equality for the mut-free run (via the new eval_rules_mutfree_fst projection). Deleted (pure optimizer verdict stack, now superseded by the state fold): - Optimize_Uncond.v: optimize_table_uncond_correct, optimize_table_uncond_compile_correct, optimize_table_correct_uncond_gen; the 13 optimize_rules_*_correct_uncond and 14 optimize_chain_*_correct_uncond pass-correctness theorems; the pure dnat/snat eval theorems optimize_rules_dnat_eval, optimize_chain_dnat_eval, optimize_rules_snat_eval, optimize_chain_snat_eval. (Definitions, freshness/output lemmas, and optimize_table_uncond itself are kept — the state stack consumes them.) - Optimize_ValueSet.v: eval_rules_run_merge_abs (the pure first-match merge). - Optimize_Linearize.v: compile_chain_default_correct and compile_chain_default_sets_correct. - Main.v: main_optimize_table_uncond_compile_correct (pure) and the two pre_split optimizer corollaries above. Makefile AXIOM_GATE_THEOREMS drops the deleted optimize_table_uncond_correct, optimize_table_uncond_compile_correct, and Optimize_Linearize.compile_chain_default_correct (the state names were already gated). Remaining pure consumers left for later units: the -O registry (Optimize_Registry.run_passes_correct over paymerge/xorfold/elide/normalize/base _eval passes), eval_rules_run_collapse (still fed by Optimize_ConcatMulti's pure proof), and the jump-aware write-free strand (compile_hook_correct family). make gates green: corpus 2532/2532, validate 28/28, source-sweep pass=1209 (floor 1209), objects-sweep 14/14, corpus-okfail pass=1008 (floor 1008, false_accept 47/47), typecheck 4/4, illtyped-reject 13/13; every AXIOM_GATE theorem Closed under the global context. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Restate the -O pass registry over the state-threading fold. The opt_pass
record's certificate field becomes an eval_chain_mut_st-preservation
obligation; run_passes_correct and resolve_run_correct re-prove over the
state fold, quantified over every hook. Each registered pass now carries
its existing state analogue:
normalize -> Optimize_MutEnv.normalize_chain_mut_st
base -> Optimize_MutEnv.optimize_chain_mut_st
paymerge -> Optimize_Linearize_MutSt.paymerge_chain_mut_st
xorfold -> Optimize_Linearize_MutSt.xorfold_chain_mut_st
elide -> Optimize_Linearize_MutSt.elide_chain_mut_st
The nftc -O CLI is unchanged: registry lists the same five passes by the
same names in the same order; run_passes/resolve_passes/registry_names have
identical computational content.
Delete the now-orphaned pure pass-eval theorems and their dead
verdict-strand machinery (the state analogues subsume them):
Optimize_PayMerge.paymerge_chain_eval (+ paymerge_eval_rules,
paymerge_rule_loadable/applies, paymerge_outcome, merge_body_loadable/applies)
Optimize_XorFold.xorfold_chain_eval (+ xorfold_eval_rules,
xorfold_rule_loadable/applies, xorfold_outcome)
Optimize_Elide.elide_chain_eval (+ elide_eval_rules,
elide_rule_loadable/applies, elide_outcome)
Optimize_Normalize.normalize_chain_eval (+ normalize_eval_rules,
normalize_rule_loadable/applies, normalize_outcome[_core],
normalize_end_loadable, and the now-dead body-walk helpers)
Optimize_Linearize.linearize_chain_eval
The four intra-rule pass files (PayMerge, XorFold, Elide, Normalize) are now
pure-verdict-strand-free. Structural projections still consumed by the state
proofs (paymerge_rule_body/xorfold_r_body/elide_r_body/normalize_r_body and
the normalize_mc_* extensional lemmas) are retained.
Makefile AXIOM_GATE_THEOREMS drops the four deleted gated pure theorems
(paymerge_chain_eval, xorfold_chain_eval, elide_chain_eval,
linearize_chain_eval); the state analogues (*_chain_mut_st) remain gated and
run_passes_correct stays gated.
make gates green: proofs, axioms (all Closed under the global context),
corpus 2532/2532, byteorder 25/25, sweeps at floor, validate 28/28,
parse-test, gen-check, boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Add Optimize_MutEnv.eval_rules_mut_st_run_collapse (the family-agnostic N-way collapse certificate over the state-threading fold, via rule_step_mutfree), re-point the ValueSet/ConcatMulti/Concat/ConcatGuarded/SetGuarded/Vmap merge sites onto it, and delete the pure Optimize_ValueSet.eval_rules_run_collapse. Gates green, axiom-free. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…pure match strand
Re-express the write-free per-pass effect-correctness proofs in
Optimize_MutEnv so the merge- and collapse-shaped stages apply the gated
state-native certificates (eval_rules_mut_st_run_merge_abs /
eval_rules_mut_st_run_collapse) DIRECTLY over eval_rules_mut_st, instead of
projecting to a pure eval_rules verdict via eval_rules_st_merge_pure /
eval_rules_st_collapse_pure and lifting back with the mut-free prefix bridge.
New reusable state-fold primitives (WithHook):
- rule_step_mutfree_state: a mut-free rule's step pins the state to (e,p),
read off rule_step_mutfree with no pure-verdict naming;
- eval_rules_mut_st_mutfree_cons: the fold's cons equation on a write-free
head, keyed on fst (rule_step h r e p);
- eval_rules_mut_st_mutfree_cons_cong: cons congruence on a write-free head,
where the tail equality need only hold at the pinned (e,p).
Re-pointed passes (each: run-certificate on the merged head + rest', with
mutfree_cons_cong bridging the recursively-optimised tail): valueset, dscp,
intervalset, intervalsethostorder, intervalsetguarded,
mixedpointrangeguarded, concat, concatguarded, setguarded. The collapse
re-points use refine + eq_refl so the shared LL/O evars resolve from the
merged rule without naming the pure outcome/rule_applies. dedup now steps
both sides through eval_rules_mut_st_mutfree_cons, aligning the write-free
verdicts without a pure-branch destruct.
The now-dead pure projection eval_rules_st_merge_pure is deleted.
Headlines unchanged and axiom-free (optimize_table_uncond_mut_st_correct,
run_passes_correct, optimize_table_uncond_compile_mut_st_correct); the gated
certificates eval_rules_mut_st_run_merge_abs / _run_collapse keep their
statements. make gates fully green: corpus 2532/2532, validate 28/28, all
sweeps at floor.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e combinator Purge the pure match strand from eval_rules_mut_st_run_merge_abs's PROOF (target 4). Factor the first-match/break argument into a new abstract combinator shell_run_merge, parametrised over the shared loadability [Lc], body applicability [Ac] and fired verdict [Oc] as OPAQUE values plus a shell builder [mk] and the per-shell step-verdict hypothesis; it reasons only over rule_step / eval_rules_mut_st (grep-clean). run_merge_abs then supplies the shell verdicts by unifying Lc/Ac/Oc against each shell's own rule_step under rule_step_mutfree + the mk_head head/tail/end equations, so no body_loadable_walk / rule_applies_walk / outcome_core / bare outcome / rule_applies name survives in the proof. Statement, gate membership and full observable are unchanged; both lemmas Closed (axiom-free). MutEnv acceptance grep 67 -> 55; the run_merge_abs region (380-520) is now pure-match-strand-free. Remaining hits are one tightly-coupled cluster (the eval_rules-side prefix/block/mutfree_fst bridge; run_collapse's outcome/rule_applies PREMISES and its 5 call sites; the concat/ concatguarded existsb rule_applies_walk factoring; the pure concat-K / vmap merge feeders and their concatmulti/vmap/vmapguarded/dscpvmap re-points; absorb/ctmask's block bridge) that cannot be moved off the pure strand without either reworking run_collapse's applies premise pure-free across all 5 sites or relocating the collapse bridge into Semantics.v — deferred rather than risk a red build. make gates fully green: corpus 2532/2532, validate 28/28, byteorder 25/25, objects-sweep 14/14 (floor), corpus-okfail 1008 (floor), typecheck 4/4, illtyped-reject 13/13, axioms clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…trand-free Eliminate the entire interlocked pure-match cluster from Optimize_MutEnv.v in one coordinated pass (grep over eval_rules/eval_chain/rule_applies/rule_applies_walk/ outcome/outcome_core/terminal_outcome/body_loadable_walk/body_synproxy_stops = 0). - eval_rules_mut_st_run_collapse: reformulated abstractly over rule_step — premises are per-shell fst(rule_step h (mk x) e p) = if LL && mc x then O else None and the merged shell's existsb disjunction. No pure-strand names. The 5 guarded call sites (concat/concatguarded/setguarded/intervalsetguarded/ mixedpointrangeguarded) discharge them uniformly via rule_step_mutfree + the passes' orig/merged structural certificates + andb reassociation helpers (andb_swap_mid/andb_pull3/andb_reassoc_g2). - eval_rules_mut_st_mutfree_prefix/_block restated over fst(eval_rules_mut_st); eval_rules_mutfree_fst and eval_rules_st_collapse_pure deleted. - eval_rules_concat_mergeK is now a state-fold equality proved by the abstract collapse; concatmulti re-pointed onto it. - vmap/vmapguarded/dscpvmap: state-native merges. New name-safe per-rule step lemmas (fst_step_vmap_merged/_orig, fst_step_dscpv_merged/_orig) read the merged and shell steps off body_step/end_step (first_match / first_match_m), replacing the pure-strand decomposition; eval_rules_mut_st_vmap_mergeN/_mergeNg/ _dscpv_mergeN driven by a shared body_step case split. vmapguarded reduces to the plain merge via eval_rules_mut_st_map_cong + orig_ruleGv_eq_swap. - absorb: eval_rules_mut_st_absorb_pair (state subsumption) + _absorb_mk; ctmask: state run-collapse over the mask-union disjunction. Both drop the pure block bridge. match_if_push (name-safe) restates the fold's match-on-if in the pure-guarded shape the merge inductions read. No new Axiom/Admitted/Parameter; every gated optimizer headline unchanged in statement, gated, axiom-free. make gates fully green: proofs, axioms (Closed under the global context), corpus 2532/2532, validate 28/28, source-sweep 1209 (floor 1209), objects-sweep 14/14, corpus-okfail pass=1008 (floor 1008) false_accept=47 (ceil 47), byteorder/parse-test/gen-check/boundary all green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…-match-strand-free
Delete the orphaned pure per-pass semantic lemmas over the pure match strand
(eval_rules / eval_chain / rule_applies(_walk) / outcome(_core) /
terminal_outcome / body_loadable_walk / body_synproxy_stops). 81 pure lemmas
removed across 17 pass files; all gates green, axiom-free.
Deleted (pure fold / headline / chain / agree lemmas):
Optimize.v eval_rules_dce, eval_rules_map_dedup,
eval_rules_map_simplify, eval_rules_prune_noops,
rule_applies_simplify, rule_loadable_simplify,
optimize_chain_correct
Optimize_Absorb.v eval_rules_absorb_pair/_mk/_correct, eval_rules_cons_cong,
optimize_rules_absorb_eval, absorb_chain_eval
Optimize_Concat.v eval_rules_concat_merge2, orig_rule2_loadable/outcome_indep
Optimize_ConcatGuarded.v orig_rule2g_loadable/outcome_indep
Optimize_CtMask.v eval_rules_ctmask_correct, optimize_rules_ctmask_eval,
ctmask_chain_eval
Optimize_DataMap.v eval_rules_continue, eval_rules_map_merge,
optimize_rules_datamap_eval, outcome_orig/mk_map_none
Optimize_Dnat.v outcome/applies/loadable_orig/mk_dnat, eval_rules_dnat_merge
Optimize_DscpVmap.v eval_rules_dscpv_mergeN, orig_rule_m_applies/outcome_clean,
outcome_core_dscpvN
Optimize_Elide.v elide_body_synproxy_stops/loadable_walk, elide_rule_applies_walk
Optimize_PayMerge.v merge_body_synproxy_stops/fuel_applies/fuel_loadable
Optimize_SetGuarded.v orig_ruleGs_loadable/outcome_indep
Optimize_Snat.v outcome/applies/loadable_orig/mk_snat, eval_rules_snat_merge
Optimize_Uncond.v eval_rules/outcome/outcome_core/rule_applies/
rule_applies_walk/rule_loadable_agree_gen, eval_rules_cons_cong
Optimize_ValueSet.v eval_rules_merge2/value_merge/range_value_merge/drop_dup/
dedup_adj/app_cong/cons_cong, optimize_chain2_correct
Optimize_Vmap.v eval_rules_vmap_merge2/mergeN, vmap_two_points,
orig_rule_applies/loadable/outcome/outcome_clean,
outcome_core_vmapN, terminal_outcome_vmap_base
Optimize_VmapGuarded.v eval_rules_map_cong, eval_rules_vmap_mergeNg
Optimize_XorFold.v xorfold_body_synproxy_stops/loadable_walk, xorfold_rule_applies_walk
Cleaned comment-only strand mentions (survivors + pass file headers):
Optimize_Table.v, Optimize_Table_Inv.v, Optimize_Linearize_MutSt.v,
Optimize.v, Optimize_DataMap.v, Optimize_Dnat.v, Optimize_Snat.v,
Optimize_ValueSet.v, Optimize_Concat.v, Optimize_Vmap.v, Optimize_ConcatMulti.v,
Optimize_DscpVmap.v, Optimize_Uncond.v. eval_chain/eval_rules mentions -> 0.
DECOUPLE GAP (reported, not papered over): 127 acceptance-grep hits remain, all
the 39 "shell" characterisation certs (rule_applies_mk_head, outcome_mk_head,
rule_loadable_mk_head, merged/orig_ruleGs/ruleK/rule2(g)_applies/loadable/outcome,
orig_ruleGv_eq_swap, the dedup_* shells, kmatches_*) in ConcatMulti/ValueSet/
SetGuarded/Concat/ConcatGuarded/IntervalSetGuarded/MixedPointRangeGuarded/
VmapGuarded/Optimize + the Syntax.outcome eq-decider. These are NOT dead: the
gated state proofs in Optimize_MutEnv.v (eval_rules_mut_st_run_merge_abs,
optimize_table_uncond_mut_st/_env_correct, the per-pass mut_st certs) reduce a
mutfree rule's state step to the pure triple via Semantics.rule_step_mutfree
(rule_step r e p = (if rule_loadable && rule_applies then outcome else None,(e,p)))
and consume these shells to characterise it. Removing them without first making
those state proofs fold-native (C4c-completion) or dropping the rule_step_mutfree
bridge (Semantics.v, out of scope) would break gated state theorems.
No gated theorem deleted; Makefile AXIOM_GATE_THEOREMS unchanged. make gates
green: proofs, axioms (all closed), corpus 2532/2532, validate 28/28,
source-sweep 1209>=1209, objects 14/14, okfail 1008/1391, byteorder,
gen-check, boundary.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…al_Fw Additive step toward retiring the pure jump strand from Examples/Regression. Adds one-step unfolding lemmas [eru_nil]/[eru_cons]/[eru_empty] for the canonical unified interpreter [eval_rules_u] and the shared symbolic engine [eval_fw_core_u] over it (mirroring the pure [erj_*]/[eval_fw_core]). The pure steppers stay in place so unmigrated consumers keep compiling; they are removed once every consumer runs on [eval_rules_u]. [eval_rules_u] is deliberately left transparent (the mixed already-canonical proofs step it with [cbn [eval_rules_u]]; the engine keeps it folded with a [cbn -[eval_rules_u ...]] blacklist). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…_Antispoof(_Gaps) off the pure jump strand onto the canonical evaluators Restates every config-correctness theorem in these four files over the canonical unified evaluator eval_table_u (as [forall h, fst (eval_table_u h ...) = v], recording that these write-free configs' verdicts are hook-independent), and reproves them by stepping eval_rules_u: - Ruleset_Verified / Example_Ruleset: eval_fw now unfolds eval_table_u and runs the shared eval_fw_core_u engine; forward_drops_all steps eru_nil; Example_Ruleset's bytecode transport goes through run_table_u / compile_table_u_correct. - Optiplex_Antispoof: the antispoof DROP headline runs through eval_fw_core_u; the accept/skip witnesses use local canonical steppers eru_fires_drop / eru_skip with an rstep_reduce tactic that reduces a rule's rule_step (case-splitting a match whose field the theorem leaves symbolic, since body_step is sequential-break). - Optiplex_Antispoof_Gaps reuses those steppers. - Eval_Fw's eval_fw_core_u also rewrites concat_set_mem hypotheses. All theorems axiom-free; acceptance grep is 0 in all four files. make gates green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…sumers off the pure jump strand onto the canonical evaluators Makes the readable config surface stand on the canonical unified evaluator: - Nft_Tactics: nft_yields fuel cs c e p v is now [forall h, fst (eval_table_u h fuel cs c e p) = v] (verdict on the canonical semantics, at every hook -- hook-independent for the write-free / limiter- tolerant configs the surface is used on). The _spec anchors, fuel-independence (now over chain_ranked_u / eval_table_u_fuel_indep) and the payload-prefix exactness lemmas (nft_prefix_chain_verdict + the two iff lemmas) are reproved over eval_rules_u; nft_eval runs eval_fw_core_u and normalises typed encode literals in field hypotheses. The pure rule_fires_*/rule_skips steppers and the now-trivial nft_*_unified lemmas are dropped; nft_writefree stays with a hook-independence-focused note (nft_yields_writefree_at). - Tutorial_Proofs / Nft_Demo_Concrete / Nft_Demo_Symbolic: restated over eval_table_u; tutorial fuel-independence uses chains_plain_ranked_u; false-claim refutations specialise the hook. - Makefile AXIOM_GATE_THEOREMS: nft_yields_unified -> nft_yields_writefree_at. All gated theorems axiom-free; acceptance grep 0 in all four files. make gates green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ump strand onto the canonical evaluators Each per-config regression theorem now stands on the canonical stateful evaluator: - Exthdr_Absent_Break / LinkLayer_MacGuard: keep only the eval_chain_mut witnesses (the pure eval_chain twins are dropped). - Payload_Break / Synproxy: eval_chain -> eval_chain_mut (over every hook) and the bytecode witnesses go through run_chain_mut / compile_chain_mut_correct. - Notrack_IntraRule: the intra-rule notrack witnesses are re-expressed on rule_step (fires -> Some verdict / skipped -> None) and eval_chain_mut. - Dnat_Rewrite: drop the unused pure outcome helper. - Setread_UnderJump: the divergence is now witnessed by the canonical eval_table_u result plus the false rule_writefree license check; the redundant effect-dropping-projection value witness is removed. - Known_Infidelities: prose "outcome" -> "verdict". All axiom-free; acceptance grep 0 in all eight files. make gates green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ure jump strand - Router_Reach: drop the pure masq_rule_applies_eq helper; its consumers (nat_masquerade_does_not_fire, nat_no_leak) reason directly on the bool firing condition (saddr_private && oif_ppp0) and the already-canonical masq_chain_u. - Router_NatHook: replace the pure NAT-blind eval_chain divergence witness (mutated_postrouting_verdict) with the canonical statement that the honest eval_chain_u verdict is Drop (not the Accept a NAT-blind projection would leak); comment references updated to eval_hook_u / eval_ruleset_u. Both axiom-free; acceptance grep 0. make gates green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ig-proof files onto the canonical evaluators Completes the pure-jump-strand purge for Examples/Regression: the acceptance grep (eval_table|eval_hook|eval_ruleset|eval_rules_j|run_table|run_ruleset| run_rules_j|eval_chain|eval_rules|rule_applies|outcome) is now 0 across every Examples/*.v and Regression/*.v. - Eval_Fw: add the generic per-rule rule_step reductions the config proofs share (field_value_set_limit, vmap_single_step, vmap_concat_step), then DELETE the transitional pure block (erj_nil/erj_cons/erj_empty + Ltac eval_fw_core + Global Opaque eval_rules_j) now that no consumer steps eval_rules_j. - Router_Input/Forward/Private: the *_eval_unfold chain characterisations are re-derived over eval_table_u/eval_rules_u with eru_cons + per-rule rule_step lemmas (r_ct_step/r_iif_step/r1_world_step/r2_fwd_step/r_svc_step/r_icmp_step) replacing the rule_applies/outcome/rule_loadable triples; each _of_vmap CORE is parametrised by the vmap contents, with the gen_env forms as corollaries. The ONE limiter rule (r_icmp) is stepped through its own consuming rule_step, the consumption shown invisible to the downstream vmap lookup. Config theorems are restated as forall h, fst (eval_table_u h ...) = v (hook-independent verdict). - Router_Hooks: eval_ruleset_u_singleton + singleton_hook_drop over eval_ruleset_u/eval_table_u; the hook bridges and dispatch theorems over eval_hook_u; select_* and the swap mutation-kill unchanged. - Router_Realistic: the _real unfolds are now the thin _of_vmap cores; the _real security theorems and hook lifts ride them, all forall h / fst (eval_table_u). - Optiplex_Mark: the mark-gating lemmas (masquerade_gated_on_mark / unmarked_not_masqueraded) re-expressed over body_step (BRdone/BRbreak); the gated streaming theorems' "rule applies" conjunct restated as body_step (r_body post1) = BRdone; dead rule_applies/outcome helpers removed. - The per-file UNIFIED-SEMANTICS LICENSE sections (the pure<->_u bridges, now vestigial) are deleted; Makefile AXIOM_GATE_THEOREMS swaps the removed license names for the migrated headline security theorems. make gates green: proofs axiom-free (all gated theorems "Closed under the global context"); corpus 2532/2532; validate 28/28; parse-test TYPECHECK 4/4 ILLTYPED 13/13; source-sweep 1209/floor 1209, objects-sweep 14/14, corpus-okfail 1008/floor 1008; gen-check 4/4. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…aluators; delete the pure base-compile headlines
Correct.v: delete the four pure base-compile headlines compile_chain_correct,
compile_table_correct, compile_ruleset_correct, compile_hook_correct together
with the pure helper/bridge/license theorems only they reached
(run_program_compile_chain, compile_chain_sets_correct, run_eval_rules_j,
run_table_fuel_indep_compiled, the eval_chain-faithfulness bridge
eval_rules_jumpfree_eq_j / eval_chain_eq_table_jumpfree /
compile_chain_faithful_jumpfree, the pure regression pins, and the
run_table_writefree_compiled / eval_chain_writefree_jumpfree_proj{,_syn}
projection licenses). The canonical stateful successors
(compile_chain_mut{,_env}_correct, compile_table_u_correct,
compile_ruleset_u_correct, compile_hook_u_correct, compile_seq_hook_correct)
stay; the shared prog_lookup_compile_env / compile_base scaffolding and the
canonical jump pins (mut_strand_jump_pin, rg_jump_not_plain,
unified_strand_jump_drops) are retained.
Main.v: drop the redundant pure Axis-1 wrapper main_compile_hook_correct and
the four pure pre_split_* corollaries (chain/table/ruleset/hook); the unified
axis 0 and the mut pre_split_* corollaries remain the exported guarantees.
Renumber the axes.
Extract.v: drop the pure eval_chain/run_chain/eval_table/run_table/
eval_ruleset/run_ruleset roots; add rule_applies so the per-rule glue keeps
its projection. semtest.ml + parse_test.ml differentials repoint onto
eval_chain_mut/run_chain_mut/eval_table_u/run_table_u/eval_ruleset_u/
run_ruleset_u; both build and pass.
Makefile: remove the deleted theorems from AXIOM_GATE_THEOREMS.
make gates fully green: corpus 2532/2532, validate 28/28, parse-test
TYPECHECK 4/4 + ILLTYPED 13/13, source-sweep 1209, objects 14/14,
corpus-okfail 1008/ceil 47, gen-check 4/4, boundary; axiom-free.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ure list/jump evaluators + orphaned licenses
Reprove the last consumer of the pure-bridge licenses directly over the
canonical stateful evaluators, then delete the pure list/jump semantics and
its now-orphaned coincidence licenses from Semantics.v.
Step 1 (reproves, off the pure bridge):
- Nft_Tactics.nft_yields_writefree_at now derives its [forall h] from a new
hook-independence lemma over eval_rules_u/eval_table_u
(eval_rules_u_hookindep_writefree / eval_table_u_hookindep_writefree, built
from the kept rule_step_writefree + chains_writefree_lookup), dropping
eval_table_u_writefree.
- Optiplex_Antispoof, Tutorial_Proofs, Ruleset_Verified, Setread_UnderJump:
prose retargeted off the deleted licenses (their proofs already computed
over eval_table_u directly).
Step 2 (deletions from Semantics.v):
- pure list/jump evaluators: eval_rules, eval_chain, eval_rules_j, eval_table,
run_program, run_chain, run_rules_j, run_table, eval_ruleset, run_ruleset,
eval_hook (+ their nil/cons/settled step lemmas).
- pure fuel/adequacy/jumpfree theory that mentioned them: eval_rules_j_fuel_indep,
eval_table_fuel_indep, eval_table_policy_is_fallthrough, chain_ranked,
rule_targets_below, outcome_jumpfree/rules_jumpfree/chain_jumpfree +
*_jumpfree_syn(_sound), verdict_no_transfer/rule_no_transfer/chains_no_transfer(_ranked),
fuel_probe_* + eval_table_under_fueled/adequately_fueled/eval_rules_j_not_naively_monotone.
- orphaned coincidence licenses: eval_{rules,table,ruleset,hook}_u_writefree,
bases_writefree, and the whole limiter-tolerant projection
(eval_{rules,table}_u_limiter_tolerant, eval_hook_u_limiter_tolerant_1 and
their limiter_inv/env_upd_limits/rule_one_limiter/rule_limiter_tol apparatus).
Kept shared primitives (chain_lookup_in, assoc_verdict_in, sufficient_fuel,
chain_len_max, base_continues, select_hook, rule_step_writefree, the _u
evaluators, the mut/mut_st strands, the per-rule pure reads). Removed deleted
names from Makefile AXIOM_GATE_THEOREMS.
make gates green; all theorems axiom-free.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The legacy pure per-rule compile lemmas prove the compiled bytecode's verdict against the write-free pure functions (rule_applies/outcome/ rule_loadable via run_compile_body/run_terminal/run_compile_end). Their only consumers, run_rule_compile_rule and run_rule_compile_rule_break, have no references: the canonical run_rule_step_compile_rule goes through the state-threading run_step_compile_body + step_compile_end instead. Delete the whole dead block (stmts_after_outcome_nonsyn, run_stmts_after, run_verdict_tail_after, body_thread_cons_notrack, body_thread_cons_other, synproxy_stops_untracked_or, run_compile_body, compile_match_break, run_compile_body_break, run_terminal, run_terminal_break, run_compile_end, run_compile_end_break, run_rule_compile_rule, run_rule_compile_rule_break), removing every bare pure-per-rule-fn use from Correct.v. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…te the per-rule pure merge certs Re-express every optimizer merge/collapse site over the fold's own step: add rule_step_fst_cons_bmatch (Semantics.v) — a leading consume-free BMatch peels off rule_step's verdict, guarded by the head match, over the shared end fields — and the mk_head-level corollaries (rule_step_fst_mk_head, rule_step_fst_swap_head, rule_step_fst_matches_prefix, if_and_nest, eval_matchcond_loadable_absorb) in Optimize_ValueSet.v, plus rule_step_fst_kmatches in Optimize_ConcatMulti.v. Re-point eval_rules_mut_st_run_merge_abs and all run_collapse sites (valueset/dscp/intervalset/intervalsethostorder via run_merge_abs; concat, setguarded, intervalsetguarded, mixedpointrange, concatguarded, concatmulti, ctmask, absorb, vmapguarded-swap) onto the native peel — no rule_applies/outcome/rule_loadable/body_loadable_walk/rule_applies_walk/ body_synproxy_stops/outcome_core/terminal_outcome named. Delete the now-orphaned per-rule pure certs: the mk_head shell certs (rule_loadable_mk_head, outcome_mk_head, rule_applies_mk_head, outcome_core_mk_head, end_loadable_mk_head, synproxy_stops_mk_head) and every per-pass merge cert (orig_*_applies / merged_*_loadable_eq_orig / merged_*_outcome_eq_orig / merged_*_applies / orig_ruleGv_eq_swap / orig_ruleK_loadable/outcome/applies / kmatches_loadable_walk / kmatches_applies_walk / synproxy_stops_bmatch / orig_rule_m_loadable_eq). Optimizer pass files (Concat, ConcatGuarded, SetGuarded, IntervalSetGuarded, MixedPointRangeGuarded, VmapGuarded, DscpVmap, ConcatMulti, ValueSet) reach grep=0 for the per-rule pure fns. make gates green, axiom-free. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e/outcome_core/terminal_outcome); keep the structural load predicates The pure verdict evaluators computed a rule's verdict IGNORING its writes (the category error). Delete them and read every verdict off the ONE fold [rule_step]: - Semantics.v: delete rule_applies/rule_applies_walk, outcome, outcome_core, terminal_outcome, and the dead rule_prod ratchet (run_rule_outcome_eq + outcome_prod/outcome_core_prod/terminal_outcome_prod, rule_prod/rule_of_prod/ outcome_of_prod/prod_wf in Syntax.v — used solely by the deleted ratchet). The mut-free coincidence bridges are re-expressed as state-invariance (rule_step_state_mutfree / body_step_state_mutfree / terminal_ / end_) plus the synproxy-free two-way body classification body_step_mutfree_synfree. tail_loadable inlines the terminal fall-through test (no terminal_outcome). - Optimizer/Optimize.v: rule_applies_dedup / outcome_dedup replaced by the fold-native body-completion classification body_step_done_class; the dedup verdict certificate is fst_rule_step_dedup (Optimize_MutEnv.v). - Nft_Tactics.v: hook-independence re-derived directly on rule_step for nat-free rules (rule_step_natfree_hookindep), replacing the deleted rule_step_writefree. - Extract.v / parse_test.ml: the rule_applies extraction root is retired; rule_applies_on reads body_step (BRbreak <=> the rule does not apply). - Makefile: the two gated theorems that only characterised deleted evaluators (run_rule_outcome_eq, rule_purewalk_ok) leave the axiom gate; rule_step_mutfree becomes rule_step_state_mutfree. Kept: the structural load-liveness predicates rule_loadable, body_loadable_walk, body_synproxy_stops (write-independent, not body_step projections). make gates fully green (clean from-source rebuild), axiom-free: proofs, axioms all Closed, corpus 2532/2532, validate 28/28, parse-test (TYPECHECK 4/4, ILLTYPED 13/13), source-sweep 1209, objects 14/14, corpus-okfail 1008/47, gen-check 4/4, boundary. No gated compiler/property headline weakened. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ames
The jump-following operational semantics (eval/run_{rules,table,chain,ruleset,
hook,hook_env}) shed its _u qualifier now that the pure evaluators are gone:
eval_rules_u -> eval_rules, run_ruleset_u -> run_ruleset, compile_*_u_correct
-> compile_*_correct, and every derived lemma carrying the _u tag renamed to
match. The fixed-width write-freeness / mut-guard predicates are untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… _flat The optimizer/compile-tool's flat single-chain state fold sheds its _mut_st tag for the _flat family: eval_rules_mut_st -> eval_rules_flat (full-state fold), eval_rules_mut -> eval_rules_flat_verdict (verdict projection), eval_rules_mut_env -> eval_rules_flat_env (env projection), and likewise for eval_chain/run_program/run_chain plus every derived lemma (compile_chain_*, optimize_table_uncond_*, the *_proj coincidence lemmas, run_merge_abs, ...). The write-freeness / mut-guard predicates (rule_mutfree, is_mut_stmt, rule_step_state_mutfree, match_consumefree, ...) keep their mut naming. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ent architecture Replace pure-strand / refactor-history narration in code comments and the living docs (THEOREMS.md, DEVELOPMENT.md) with present-tense descriptions of the one stateful jump-following semantics (eval_table/eval_chain/eval_rules), the flat single-chain fold (eval_chain_flat) as the optimizer's tool, and the kept structural load predicates. Comment/doc only; no definition, theorem, or proof changed. Gates green, axiom-free. 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.
The agent for some reason decided to keep around the broken pure semantics that make the assumption that the environment is unmodified when evaluating an nftables rule. This PR completely removes the broken semantics and ensures that the correctness theorems all refer to the accurate effectful semantics.