Status: measurement instrument. Opens no round, rules nothing. Numbers: receipts/FLOOR-CENSUS.md (generated; guards.sh refuses drift). Instrument: cd-floor/src/main.rs + tools/floor_census.py.
There is deliberately no numeral in this document that is a measurement. The receipt carries them; this file says how they were produced and how far they may be read.
A planning conversation proposed three tiers — an 8, a 16 and a 32 KiB "ComputeDriven floor" — and a per-core "kernellet" built on the premise that the floor was already known to sit somewhere in the 32–64 KiB band. It was not. What the tree held was a 64 KiB RAM budget in cd-micro/link.ld and a codec probe whose linked .text is under two kilobytes and which links none of the lifecycle. Nobody had sized the semantic floor. Naming tiers ahead of the first number is the WORLD_SIZE.md §11 error again, so this instrument produces the number first; whether tiers are worth naming is a question for after the receipt.
Same profile as cd-micro. no_std, no_main, no allocator, no libc, own 8 KiB stack inside the 64 KiB map, the same linker script copied verbatim. The four crates cd-core / cd-wire / cd-node / cd-micro are frozen since R0.6 (verify_r08_freeze.sh check 4), so the census is a second image beside cd-micro, not an edit of it.
Five mechanisms behind Cargo features.
| feature | mechanism |
|---|---|
codec | cd-wire HELLO/ACK encode + decode |
lifecycle | attach / detach / finalize_loss, each consuming the admission |
custody | suspend (checkpoint) + recover_attachment (reconstitute); requires lifecycle |
replay | replay_lifecycle + audit_replay; requires lifecycle |
worker | reconstruct worker authority from grant / revocation evidence |
Code is attributed by difference, never by symbol. With lto = true and codegen-units = 1 the whole image folds into one unit, and a symbol table would attribute most of the lifecycle to floor_main. The census therefore builds every valid subset (a subset is valid when it contains what its members require) and reports each mechanism four ways:
standalone(M) = size(base + M) − size(base) what M costs on its own removal-closure(M) = size(all) − size(all − M − deps(M)) what deleting M takes with it conditional(M) = size(C + M) − size(C), every valid C min / mean / max Shapley(M) = mean marginal over precedence-consistent orderings
For custody and replay, "base" is lifecycle, which they require. The removal-closure column was first labelled "marginal" and the receipt said "shared code shows as the gap"; GPT's R1 review corrected that: for lifecycle most of the gap is dependency closure (custody and replay cannot exist without it), not sharing. The conditional and Shapley columns exist so the attribution is harder to argue with, and the pairwise interaction matrix says which pairs share code.
`.rodata` is reported net of the harness. The runner prints three keys per mechanism; those strings sit in .rodata and are harness, not mechanism. The script parses their lengths out of the source and subtracts them. The runner's three kv calls per mechanism do cost a few instructions in .text, and those are not subtracted; they bound the over-attribution at three call sites.
Every mechanism is exercised, and every input crosses `black_box`. Without the first, LTO deletes an unreferenced mechanism and "it costs zero bytes" is true and useless. Without the second, LLVM evaluates a transition over literal inputs at compile time and folds the witness to a constant, and the figure is a measurement of LLVM's evaluator, not of cd-core.
A witness is a named invariant, and it is a load-bearing witness, not yet a necessity witness. The witnesses are listed in the receipt (§5) and in the source header. Each must hold in every subset that enables its mechanism; the binary's exit code is the count of witnesses that failed. Deleting a mechanism deletes its witnesses, which shows the mechanism as written is load-bearing for those invariants. It does not show that a smaller mechanism could not enforce them: that stronger experiment keeps the property required externally, shrinks or replaces the implementation, and asks whether the property still holds. "Necessity witness" is reserved for that (GPT R1 correction). The brief's rule — optimise until going smaller causes a named invariant to fail — is applied here before any optimisation, to the code as it stands.
Per-instance state is `size_of`. Every lifecycle value's in-memory size on this toolchain, with repr(Rust) layout, plus derived sums: what one live locus needs, what one vacant locus needs, what a checkpoint is, what an orderly or post-loss carrier change produces as evidence.
Stack is a conservative bound below a paint point. Each phase is #[inline(never)]; the runner paints the reserve below its own rsp, calls the phase, then scans up from the bottom for the first byte that changed. A fixed margin under the paint point is left unpainted (red zone plus the painter's spills), so the figure is never below the margin and a phase that touches less than the margin reads as exactly the margin.
| class | measured? | where / why not |
|---|---|---|
| instruction bytes | yes | receipt §1, .text per mechanism, standalone and marginal |
| hot instruction working set | yes, R1 | receipts/KERNELLET-R1.md §4: exact executed-instruction sets by ptrace single-step, per workload, as bytes and 64 B lines; L1I misses per transition in the stamped dynamic receipt |
| constant tables | yes | receipt §1, .rodata per mechanism, net of harness strings |
| per-instance mutable bytes | yes | receipt §2, size_of and the per_live_locus / per_vacant_locus sums |
| stack requirement | bound | receipt §3, per phase, never below the margin |
| context-switch bytes | partial | the semantic context is per_live_locus; the register/stack context of a carrier is not in cd-core and is the host's |
| checkpoint bytes | in-memory only | CarrierCustody; no wire encoding exists — cd-wire carries HELLO/ACK and nothing else |
| migration bytes | in-memory only | the evidence pair a carrier change produces; same caveat, and a migration protocol does not exist in R0 |
| worker-authority reconstruction state | yes | Evidence, Authority; reconstruct holds one boolean over the slice. Only that: this image holds no TRVM verifier, and the row is narrowed to say so (GPT R1) |
The two "in-memory only" rows are the honest shape of the answer: the byte count of a checkpoint on the wire cannot be measured because nothing in R0 serialises one. That is a fact about the tree, not a gap in the instrument.
They are x86-64 bytes at `opt-level = "s"`. A Thumb-2 or RV32C image
would be a different size in both directions of the usual folklore; nothing is claimed for another ISA until one is built.
Size is not isolation. An immutable floor stays immutable only where
hardware protection stops a corrupted instance from writing over it. The R0 census recorded that isolation today comes from KVM, not from the semantic monitor. Nothing here moves that.
"Floor" is not "irreducible". The census shows each mechanism is
load-bearing for named invariants as written. It does not show the code is minimal; a smaller implementation enforcing the same witnesses is possible and would be measured the same way.
One image, many instances is what every OS does. Shared text pages plus
per-process data is fork. The interesting figure is per_live_locus, not the layout; whether Locus and Worker identity survive a carrier change across cores is R0.4's succession model, already ruled, and is not re-proved here.
Shadow promotion is not addressed. Promoting a standby when the primary
is INDETERMINATE is the split-brain question; LossBasis has no reachability variant on purpose (R0.4.2), and two cores on coherent memory do not make it go away. Any per-core study inherits that as a falsifier.
The first stack row was vacuous. Measured from the top of the reserve,
every phase reported the same bound, because the phases inlined into floor_main and their locals lived in a frame above the paint point that was never painted. The instrument was measuring the harness's frame. Fixed by measuring from the paint point down with non-inlined phases; the census now refuses a run in which every phase reports the same bound.
`bcmp`. LLVM lowers == on byte arrays to bcmp, which the freestanding
image did not provide; the link failed. Provided as memcmp.
The first receipt mislabelled dependency closure as "marginal" and its
bundle's checksum manifest hashed itself. Both found by GPT's review of the R0 bundle; both fixed in R1 (the column is renamed, the manifest excludes itself).
The receipt is generated, and the gate diffs it. A count in prose drifts
(tools/counts_gate.py exists because three did at once). Here no number is typed anywhere: guards.sh rebuilds every variant and refuses if the committed receipt differs by a byte. A toolchain change therefore fails the build, which is the intended behaviour — the receipt names its toolchain.
The receipt states, derived, whether the full image's .text + .rodata sits under 8, 16 and 32 KiB. Read that line and then read §3 above before quoting it: it is a statement about this image on this target, including the harness. The floor and semantic-floor rows are the ones that exclude the harness.