Floor attribution — what one admitted transition spends its cycles on

Status: measurement note, opened 2026-09-19. Opens no new semantics, adds no feature to any image, changes no anchor. Its receipts are stamped, not gated. Instrument: tools/floor_attribution.py; it reuses tools/kernellet_abi.py (ptrace, build), tools/sflr_bench.py (measure, provenance) and tools/r4_shootout.py (MixSUT, the BENCHMIX mixes). Numbers: receipts/FLOOR-ATTRIBUTION-{SMOKE|OFFICIAL}-<stamp>.{md,json}.

No numeral in this document is a measurement.

0. The question, and why it was asked

The compiled WRL backend (TRVM/compiled/) folds a sealed world's epoch as one C step over a few hundred bits, four to six orders of magnitude under the interaction calculus reducing the same epoch. That made a proposal natural: if the world's laws were expressed once at a meta level, discharged at admission over the sealed finite state space, and the step, its residual checks, its battery and its certificate all generated from that one source — how much of the floor could go with them?

The proposal's premise is that the floor spends cycles checking world-local law. This note and its tool ask whether that premise is true of cd-kernellet as built, in two halves:

1. By reading (§2): what does step check, and is any of it a WRL law?

2. By measuring (§3): of one transition's cost, how much is the semantic

step at all, and how much is carrying a context in and out of it?

Only the first half can say "none". The second says what a change to either half would be worth.

1. What a transition is here

The subject is the promoted production floor (prod, no features; R4-P, receipts/R4-P-PROMOTED.md), whose image anchor the tool checks against the newest receipts/R7-BATTERY-*.json before it measures anything (F141). One transition is one step(lineage, op, …) -> (lineage, outcome): kernellet_main takes the slot's Option<Lineage> out of TABLE, calls step, and puts the returned lineage back. The lineage is the Locus Core Context — admission, finality warden, possession — and the authority row lives in a private sidecar, borrowed by AUTH and consumed-and-returned by GRANT/REVOKE (authority_store).

2. What step checks, by line

Every check reached from step (cd-kernellet/src/main.rs, the step function) at the promoted default, and what kind of fact it is about:

Every row is about a locus, a carrier, a generation, a fence epoch, a mark or a worker. Not one is about a WRL object: no spinner saturation, no door's COMMIT-then-REACT, no affine single-use, no width bound. Those are checked in the compiled step's admission battery and in the calculus, not here. The floor's safety is succession safety — the same carrier cannot be attached twice, a stale attachment cannot detach, a fence epoch cannot go backwards — and its authority is evidence authority. All of it is open-world: it is about who and which and when, none of it about what the world computes.

So the strong form of the proposal — "hoist the WRL laws and the floor shrinks" — is answered by reading: the floor would shrink by nothing, because it evaluates none of them. What remains is the second half.

3. How the measurement is made

Two instruments over the same command streams on the same image in the same run, reconciled per row before anything is subtracted:

• perf, R4's instrument: user-domain hardware counters

(sflr_bench.measure), marginal between K and 2K iterations of one in-image BENCHMIX command so BOOT, BEGIN, the pre-GRANTs and the I/O loop cancel; median of repeats; a multiplexed reading is dropped, never scaled.

• ptrace, R1's instrument: PTRACE_SINGLESTEP over the same streams at

small iteration counts, again as a K → 2K difference, every executed rip bucketed by symbol: inside step, inside memcpy, elsewhere in .text. memcpy entries are counted and their widths read from %rdx (R4 F66), so bytes moved per op is exact.

step is a symbol only in the benchraw images — prod inlines it into kernellet_main — so those are the images traced, in two families: benchraw (byte-loop intrinsics) and benchraw+fastmem (rep movsb/rep stosb intrinsics). Both carry the promoted default's semantics exactly; benchraw is bench with the rdtsc pair and histogram removed, so nothing that measures is in the loop. M4 holds: each traced image runs the full external witness battery (kernellet_census.battery) first, and a failure blocks its numbers.

The control. BENCHMIX mix 3 is STATE, STATE: the lineage is taken from the table, step is called on an op whose only work is to hand the values back, and the lineage is put back. It is the plumbing of a transition with no semantics in it. For a semantic mix m, semantic(m) = per_op(m) − per_op(3), in cycles and in instructions, and the tool refuses the subtraction unless both rows reconciled. The ptrace split gives the same answer a second way: instructions inside step against instructions outside it.

Reconciliation, and the instrument fact it turned up. A rep-prefixed string instruction retires once under perf but traps once per iteration under PTRACE_SINGLESTEP. The tool therefore counts distinct consecutive rips as retired-instruction equivalents (no instruction in these images jumps to itself) and prints the iterations in their own column. On fastmem those iterations are the bytes rep movsb moved. Inside step they are an inlined rep movsq aggregate copy (LLVM's lowering; seven sites inside step) on the FINALIZE and AUTH paths — present in both families, and invisible to R1's ptrace-vs-perf agreement check because that check was made on the byte-loop image, where a constant nine-step excess sits under a per-cent tolerance on a thousand-instruction transition. The first version of this tool compared raw steps and passed the byte-loop rows the same way; the fastmem rows, an order of magnitude smaller, exposed it. The reconciliation rule is now one rule for both families: retired-equivalent ptrace count against perf instructions, per op, within a stated tolerance, or the row DISAGREES and is withheld from the split.

Two loops over the same pair. bench (op 20, the loop R1 and R2 published) and mix 0 (op 24) both perform ATTACH then DETACH on each context. The receipt prints each loop's memcpy entries and bytes moved per op so the difference between them — the published figure carries more copies per pair than the mix — is read from the row, not assumed.

4. What the numbers do not say

• Nothing about a WRL law; §2 is the whole answer there, by reading.

• The semantic column is succession, provenance and authority. It is the

cost of the floor's own laws, which are also hand-transcribed into the C, Go, Erlang and cd-core comparators (sflr/, fcb/kc/) and cross-checked by the class-S suite — the generator question, if it is asked, is asked of those laws.

• The mix-3 control's in-step count is zero because the compiler

specialises step for a constant op and the STATE arm is a move; the control is take + put + the call shape, which is what it is meant to be.

• A smoke receipt is taken on a shared host and says so in its status line;

the spreads are printed. Only an --official run under docs/battery-host-profile.md is evidence.

• Nothing is compared across languages here, and nothing here enters the FCB

kernellet-cost campaign (docs/fcb-kernellet-cost-contract.md) or the reverse.

• Hardware counters are this CPU, this frequency, this day. Stamped, never

diffed.