From 72a6bbe17369b0c748f64daa717153dde55e15a3 Mon Sep 17 00:00:00 2001 From: surface-camera-build Date: Mon, 21 Sep 2026 18:19:36 -0400 Subject: [PATCH] cubelinux: the key and the span move into the shared file, and the driver stops having its own MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `morton_encode` existed twice — once in the driver, once (as the curve) in cube-core — and the two had to agree byte for byte, because one side computes a key to look a record up and the other computes it to lay an image out. Nothing structural held that agreement: only the gates, which would notice afterwards. That is the same shape as the cube_format.rs finding recorded in DESIGN-coordinate-surface.md §7.4 — a shared *file* whose shared half has no callers — so this starts paying it off where it is cheap and exact. The interleave now lives in cube_format.rs, which both builds compile, and the driver's copy is a call to it. It is written as plain `while` loops rather than iterator chains because the kernel build of this file has no `std` and no `alloc`, which is the constraint the whole arrangement exists under. Alongside it, two things the range work needs and neither side had: key_cmp compare two keys as the 192-bit numbers they are. The key is big-endian, so this is the comparison a sorted index performs, and it is stated once rather than assumed at each site. key_span the key span a box covers, (key(lo), key(hi)) inclusive. This is the bound a seek needs, and — the point — it needs no decomposition at all: the interleave is monotone in every axis, so every point in the box has a key between its corners' keys. A sorted index can be binary-searched for the foot and scanned forward to the head. The span is a BOUND and not the set: records outside the box can have keys inside it, which is the classic Z-order amplification and is why a caller tests membership per candidate. Confusing the bound for the set is close to the mistake that put "an aligned box is one run" into two doc comments. aligned_box_is_one_run the condition, proved in crates/cube-format's tests and pinned there and in cube-store: a power-of-two-aligned box is exactly one contiguous run of the key iff max(k) - min(k) <= 1 AND the axes at the top level form a prefix of (x, y, z). A size that is not a power of two is answered `false` rather than rounded, because a caller passing one has a bug and "no" is the useful answer. Verified on build #53: verify-enum (the kernel's walk against userspace's, which is the check that would catch any change in the key), verify-boot-record, verify-syscall all pass. --- drivers/cube/cube_format.rs | 132 ++++++++++++++++++++++++++++++++ drivers/cube/cubelinux_store.rs | 20 ++--- 2 files changed, 138 insertions(+), 14 deletions(-) diff --git a/drivers/cube/cube_format.rs b/drivers/cube/cube_format.rs index 08ab23ca9..3146f5ebb 100644 --- a/drivers/cube/cube_format.rs +++ b/drivers/cube/cube_format.rs @@ -427,3 +427,135 @@ impl Digest { } } } + +// ── Where a coordinate's key sits, and what span a box covers ────────────────────────── +// +// The key is a three-axis bit interleave: axis `x` owns bit `3i`, `y` owns `3i+1`, `z` owns +// `3i+2`, and the 24-byte key is that 192-bit number written big-endian — so comparing two keys +// byte-wise from the front is comparing the interleaved integers, and `key_cmp` is the comparison +// a sorted index performs. +// +// This lives in the shared file rather than in the driver because it is the one piece of the +// addressing that the two sides must agree on byte for byte: the driver computes a key to look a +// record up, and userspace computes the same key to lay an image out. It was written twice before +// (`morton_encode` in `cubelinux_store.rs` and the curve in `cube-core`) with the agreement held +// by the gates rather than by the compiler; now the kernel's copy is this one. + +/// The key a coordinate has. +/// +/// `x` at bit `3i`, `y` at `3i+1`, `z` at `3i+2`, for `i` in `0..64`, big-endian into 24 bytes. +/// The correspondence is monotone in every axis — if `a <= a'` on all three then `key(a) <= key(a')` +/// — which is what makes [`key_span`] a sound bound rather than a guess. +pub fn morton_key(x: u64, y: u64, z: u64) -> [u8; RAW_KEY_LEN] { + let mut k = [0u8; RAW_KEY_LEN]; + let mut i = 0; + while i < 64 { + let mut axis = 0; + while axis < 3 { + let value = match axis { + 0 => x, + 1 => y, + _ => z, + }; + if (value >> i) & 1 != 0 { + let n = 3 * i + axis; + k[RAW_KEY_LEN - 1 - (n / 8)] |= 1 << (n % 8); + } + axis += 1; + } + i += 1; + } + k +} + +/// Compare two keys as the 192-bit numbers they are. `a < b` means `a` sorts first. +pub fn key_cmp(a: &[u8; RAW_KEY_LEN], b: &[u8; RAW_KEY_LEN]) -> core::cmp::Ordering { + let mut i = 0; + while i < RAW_KEY_LEN { + if a[i] != b[i] { + return if a[i] < b[i] { + core::cmp::Ordering::Less + } else { + core::cmp::Ordering::Greater + }; + } + i += 1; + } + core::cmp::Ordering::Equal +} + +/// The key span a box covers: `(key(lo), key(hi))`, inclusive. +/// +/// **This is the bound a seek needs, and it needs no decomposition.** Because the interleave is +/// monotone, every point in the box has a key between these two — so a sorted index can be +/// binary-searched for the lower one, scanned forward while the key stays under the upper one, and +/// each candidate tested for membership. Records may be found in that span that are *not* in the +/// box (that is the classic Z-order amplification, and how much depends on the box), but no record +/// in the box is outside the span. What is *not* true — and was believed here until it was checked +/// — is that the box is one contiguous run: see [`aligned_box_is_one_run`]. The span being sound +/// does not make it tight, and confusing the two is how an aligned box of three runs gets +/// documented as one. +pub fn key_span(lo: [u64; 3], hi: [u64; 3]) -> ([u8; RAW_KEY_LEN], [u8; RAW_KEY_LEN]) { + ( + morton_key(lo[0], lo[1], lo[2]), + morton_key(hi[0], hi[1], hi[2]), + ) +} + +/// Whether a power-of-two-aligned box with these per-axis sizes is exactly **one** contiguous run +/// of the key. +/// +/// The condition, derived and then checked against the keys themselves on every properly-aligned +/// box with sizes in `{1,2,4,8,16}` per axis and origins swept to 16 — 4,805 boxes, no +/// disagreement (pinned in `crates/cube-format`'s tests and in `cube-store`'s): +/// +/// > `max(k) - min(k) <= 1` **and** the axes at the top level form a prefix of `(x, y, z)` in that +/// > order, where `2^k` is the size on an axis. +/// +/// The free bit positions of such a box are `{3i + a : i < k_a}`, and that set is a prefix of +/// `{0,1,2,…}` only when the levels are complete except possibly the last — so a cube qualifies, a +/// cube doubled along `x` qualifies, a cube doubled along `x` and `y` qualifies, and **doubling `z` +/// alone, or `x` and `z` together, does not**, because `z` cannot be free at a level where `y` is +/// not. The asymmetry belongs to the interleave; it is why the property looked plausible. +/// +/// Sizes are taken as given: a size that is not a power of two is not an aligned box's size, and is +/// answered `false` rather than rounded, because a caller that passes one has a bug and the useful +/// answer is "no", not a guess. +pub fn aligned_box_is_one_run(sx: u64, sy: u64, sz: u64) -> bool { + fn k_of(s: u64) -> Option { + if s == 0 || !s.is_power_of_two() { + return None; + } + Some(s.trailing_zeros()) + } + let (kx, ky, kz) = match (k_of(sx), k_of(sy), k_of(sz)) { + (Some(a), Some(b), Some(c)) => (a, b, c), + _ => return false, + }; + let (lo, hi) = ( + kx.min(ky).min(kz), + kx.max(ky).max(kz), + ); + if hi - lo > 1 { + return false; + } + // The axes at the top level, in the order the interleave gives them: x, then y, then z. + let mut top = [false; 3]; + if kx == hi { + top[0] = true; + } + if ky == hi { + top[1] = true; + } + if kz == hi { + top[2] = true; + } + // A prefix: x before y before z, with no gaps. + if top[2] && !top[1] { + return false; + } + if top[1] && !top[0] { + return false; + } + top[0] +} diff --git a/drivers/cube/cubelinux_store.rs b/drivers/cube/cubelinux_store.rs index f3f550ad5..62cabe149 100644 --- a/drivers/cube/cubelinux_store.rs +++ b/drivers/cube/cubelinux_store.rs @@ -1064,20 +1064,12 @@ fn log_valid_len(log: &[u8]) -> Result { /// userspace reader decodes. Bit `i` of each axis lands at bit `3i` of the 192-bit key, /// counting from the least significant bit, which lives in the *last* byte. fn morton_encode(x: u64, y: u64, z: u64) -> [u8; 24] { - let mut k = [0u8; 24]; - let put = |n: usize, v: bool, k: &mut [u8; 24]| { - if !v { - return; - } - let byte = 23 - (n / 8); - k[byte] |= 1 << (n % 8); - }; - for i in 0..64 { - put(3 * i, (x >> i) & 1 != 0, &mut k); - put(3 * i + 1, (y >> i) & 1 != 0, &mut k); - put(3 * i + 2, (z >> i) & 1 != 0, &mut k); - } - k + // The interleave itself lives in the shared file, and this is now one of its callers rather + // than a second copy of it. That matters more than it looks: the driver and userspace have to + // agree on this key byte for byte, and they were two implementations of one rule whose + // agreement was held only by the gates. `crates/cube-format`'s tests pin the axis-to-bit + // correspondence by hand so that neither side can drift without a test failing. + cube_format::morton_key(x, y, z) } /// A mutation to append: the byte-plane write the store contract calls `put`.