cubelinux/cubelinux-kernel
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

cubelinux: the key and the span move into the shared file, and the driver stops having its own

Browse Source 
`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.
This commit is contained in:
surface-camera-build
2026-09-21 18:19:36 -04:00
parent 087c6b0e60
commit 72a6bbe173
2 changed files with 138 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files
drivers/cube/cube_format.rs
+132
View File
@@ -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<u32> {
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]
}
drivers/cube/cubelinux_store.rs
+6 -14
View File
@@ -1064,20 +1064,12 @@ fn log_valid_len(log: &[u8]) -> Result<usize, &'static str> {
/// 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`.