engine: complete the finite-set lattice, and seam off the representation

Q_PAGE_OFFSET is about to become a finite set on most architectures. Two
things had to be true first, and neither was.

estimate_meet handled only C_EQUALS on LK_FINSET. Both bounds and C_EXCLUDE
were accepted and discarded, so a measured bound would have narrowed nothing
and "the compile-time split is ruled out" -- which is an exclude -- would have
been dropped by the lattice that most invites it. Every op now runs through
one constraint_admits() predicate applied to each live candidate. Its switch
has no default: deliberately, so a newly added op fails -Wswitch rather than
being silently ignored the way C_EXCLUDE was. n_candidates is bounded by the
bitmask width at compile time; the shift past a word is undefined, not merely
wrong.

`struct estimate` means different things per lattice -- on a finite set `lo`
is a live-candidate bitmask and `hi` is unused -- so the 51 sites reading .lo
and .hi were correct only for the lattice they were written against, which is
not a property of the source once the same file compiles both ways. They now
go through quantity_pinned/window/admits/narrowed, and check-lattice-seam
holds the line. It discovers the pointer alias from its binding rather than
assuming the `po` convention, so renaming cannot slip a read past.

Two of those sites were already lattice-aware and would have failed silently:
four rules gate on `kind != LK_INTERVAL` and would have gone inert on arm64
and riscv64, and the orchestrator's default_excluded test compared window
edges, which still calls an excluded interior value possible. Asking the
estimate is both representation-free and more correct.

test_kasld and test_render exercise engine_sync_authoritative, which projects
resolved estimates, so those single-TU builds now carry the value model they
read -- after orchestrator.c, whose feature-test macros must come first.

Author: bcoles

Makefile

@@ -624,6 +624,7 @@ lint :
 	@$(TEST_DIR)/check-text-floor
 	@$(TEST_DIR)/check-text-region
 	@$(TEST_DIR)/check-confidence-floor
+	@$(TEST_DIR)/check-lattice-seam
 	@$(TEST_DIR)/check-image-size
 	@$(TEST_DIR)/check-fdt-unflatten
 	@$(TEST_DIR)/check-ksymoff

docs/testing.md

@@ -108,6 +108,7 @@ and `make` halts on the first.
 | `check-text-floor` | no component rolls its own text-base floor — they must use the `api.h` helper |
 | `check-shellcheck` | shellcheck over the `extra/` helper scripts |
 | `check-confidence-floor` | no engine rule pins the *guaranteed* window from a guess — a sub-floor signal may shape `likely` only, outside the reviewed allowlist |
+| `check-lattice-seam` | quantities whose lattice varies by architecture (`Q_PAGE_OFFSET`, `Q_VA_BITS`) are read through `quantity_pinned/window/admits/narrowed`, never through `.lo` / `.hi`. `struct estimate` means different things per lattice — on a finite set `lo` is a live-candidate bitmask and `hi` is unused — so a direct read is correct only for the lattice it was written against, which is not a property of the source when the same file compiles both ways. Nothing would fail loudly: a bitmask read as an address is a small integer, so the result is a plausible wrong answer rather than a crash. The pointer alias is discovered from its binding rather than assumed to be named `po`, so renaming it cannot slip a read past |
 | `check-text-region` | the `KERNEL_TEXT` vs `KERNEL_IMAGE` base contract holds — only reviewed emitters may publish a `_stext` base |
 | `check-image-size` | the kernel image size is read only through the evidence accessors, never re-derived in a component |
 | `check-hash-parity` | every hashed offset-table row's key recomputes to the stored value under the shipped `kasld_fnv1a64()`, so the runtime hash and the offline generator's cannot drift apart |

src/estimate.c

@@ -136,6 +136,40 @@ static int stride_intersects_interval(unsigned long lo, unsigned long hi,
   return first <= hi;
 }
 
+/* Does one concrete value satisfy this constraint?
+ *
+ * The finite-set lattice narrows by testing each live candidate, so it needs a
+ * predicate that is TOTAL over the op enum. The switch carries no `default:`
+ * deliberately: a newly added constraint op then fails -Wswitch until someone
+ * states how a finite set answers it. That is the guard the old code lacked —
+ * it handled C_EQUALS and let every other op through untouched, so C_EXCLUDE
+ * and both bounds were silently discarded on a finite set.
+ *
+ * Interval semantics are not expressed here. An interval cannot represent an
+ * interior hole, so LK_INTERVAL keeps its own op-by-op narrowing, including
+ * the end-trim approximation for C_EXCLUDE. */
+static int constraint_admits(const struct constraint *c, unsigned long v) {
+  switch (c->op) {
+  case C_LOWER_BOUND:
+    return v >= c->value;
+  case C_UPPER_BOUND:
+    return v <= c->value;
+  case C_EQUALS:
+    return v == c->value;
+  case C_AT_LEAST_ALIGN:
+    /* A zero alignment constrains nothing; say so rather than divide by it. */
+    return c->value == 0 || (v % c->value) == 0;
+  case C_EXCLUDE:
+    /* Inclusive [value, value2]. A reversed pair is an empty range, which
+     * excludes nothing — this test admits everything for it, as it should. */
+    return v < c->value || v > c->value2;
+  case C_STRIDE:
+    /* q = value (mod value2). A zero modulus is not a residue class. */
+    return c->value2 == 0 || (v % c->value2) == (c->value % c->value2);
+  }
+  return 1; /* not reached; an unhandled op is a -Wswitch build failure */
+}
+
 /* ------------------------------------------------------------------------
  * Meet — narrow an estimate by one constraint.
  * ------------------------------------------------------------------------ */
@@ -236,22 +270,28 @@ void estimate_meet(struct estimate *e, const struct quantity_def *qd,
     }
     break;
 
-  case LK_FINSET:
-    if (c->op == C_EQUALS) {
-      /* Pin to the candidate whose value == c->value; if no candidate
-       * matches, the intersection is empty (bottom). */
-      unsigned long mask = 0;
-      for (int i = 0; i < qd->n_candidates; i++)
-        if (qd->candidates[i] == c->value)
-          mask = 1ul << i;
-      unsigned long narrowed = e->lo & mask;
-      if (narrowed != e->lo) {
-        e->lo = narrowed;
-        e->lo_binding = c->id;
-      }
+  case LK_FINSET: {
+    /* Keep every live candidate the constraint admits and drop the rest. One
+     * uniform narrowing for all ops, so none can be ignored by omission: a
+     * C_EQUALS naming no candidate empties the set (bottom), a bound trims the
+     * ends, and a C_EXCLUDE removes an interior candidate exactly — the finite
+     * set represents holes that the interval lattice has to approximate.
+     *
+     * `stride` stays 0 here: a C_STRIDE narrows the live set directly, leaving
+     * no residue annotation to carry (see struct estimate). The shift is safe
+     * unguarded because n_candidates is bounded at compile time by
+     * KASLD_FINSET_MAX_CANDIDATES. */
+    unsigned long mask = 0;
+    for (int i = 0; i < qd->n_candidates; i++)
+      if ((e->lo & (1ul << i)) && constraint_admits(c, qd->candidates[i]))
+        mask |= 1ul << i;
+    if (mask != e->lo) {
+      e->lo = mask;
+      e->lo_binding = c->id;
     }
     break;
   }
+  }
 
   /* Propagate the binding constraint's confidence to whichever edge it just set
    * (ids are monotonic from 1, so this only matches an edge this call bound;
@@ -388,6 +428,105 @@ void estimate_resolve(enum kasld_quantity q, enum kasld_confidence floor,
 /* ------------------------------------------------------------------------
  * quantity_ranges — interval-set value-access for consumers.
  * ------------------------------------------------------------------------ */
+/* ------------------------------------------------------------------------
+ * Lattice-agnostic value access — see the contract in estimate.h.
+ * ------------------------------------------------------------------------ */
+int quantity_pinned(enum kasld_quantity q, const struct estimate *e,
+                    unsigned long *out) {
+  const struct quantity_def *qd = &quantities[q];
+  unsigned long v = 0;
+  switch (qd->lattice) {
+  case LK_INTERVAL:
+    if (e->lo != e->hi)
+      return 0;
+    v = e->lo;
+    break;
+  case LK_FINSET:
+    if (!estimate_finset_value(qd, e, &v))
+      return 0;
+    break;
+  case LK_MAXALIGN:
+    return 0; /* an alignment is not a value */
+  }
+  if (out)
+    *out = v;
+  return 1;
+}
+
+int quantity_window(enum kasld_quantity q, const struct estimate *e,
+                    unsigned long *lo, unsigned long *hi) {
+  const struct quantity_def *qd = &quantities[q];
+  unsigned long a = 0, b = 0;
+  switch (qd->lattice) {
+  case LK_INTERVAL:
+    if (e->lo > e->hi)
+      return 0; /* bottom */
+    a = e->lo;
+    b = e->hi;
+    break;
+  case LK_FINSET: {
+    /* Candidate tables are not required to be sorted, so scan for both edges
+     * rather than reading the first and last live bits. */
+    int seen = 0;
+    for (int i = 0; i < qd->n_candidates; i++) {
+      if (!(e->lo & (1ul << i)))
+        continue;
+      unsigned long v = qd->candidates[i];
+      if (!seen || v < a)
+        a = v;
+      if (!seen || v > b)
+        b = v;
+      seen = 1;
+    }
+    if (!seen)
+      return 0; /* empty set — bottom */
+    break;
+  }
+  case LK_MAXALIGN:
+    return 0;
+  }
+  if (lo)
+    *lo = a;
+  if (hi)
+    *hi = b;
+  return 1;
+}
+
+int quantity_admits(enum kasld_quantity q, const struct estimate *e,
+                    unsigned long v) {
+  const struct quantity_def *qd = &quantities[q];
+  switch (qd->lattice) {
+  case LK_INTERVAL:
+    if (e->lo > e->hi || v < e->lo || v > e->hi)
+      return 0;
+    if (e->stride && (v % e->stride) != e->stride_offset)
+      return 0;
+    return 1;
+  case LK_FINSET:
+    for (int i = 0; i < qd->n_candidates; i++)
+      if ((e->lo & (1ul << i)) && qd->candidates[i] == v)
+        return 1;
+    return 0;
+  case LK_MAXALIGN:
+    return 0;
+  }
+  return 0;
+}
+
+int quantity_narrowed(enum kasld_quantity q, const struct estimate *e) {
+  const struct quantity_def *qd = &quantities[q];
+  struct estimate top;
+  qd->init_top(&top);
+  switch (qd->lattice) {
+  case LK_INTERVAL:
+    return e->lo > top.lo || e->hi < top.hi || e->stride != top.stride;
+  case LK_FINSET:
+  case LK_MAXALIGN:
+    return e->lo != top.lo;
+  }
+  return 0;
+}
+
 int quantity_ranges(enum kasld_quantity q, const struct estimate *e,
                     enum kasld_confidence floor, const struct constraint *cs,
                     int n_cs, struct range *out, int out_max) {
@@ -397,6 +536,12 @@ int quantity_ranges(enum kasld_quantity q, const struct estimate *e,
     return 0; /* an alignment is not an address set */
 
   if (qd->lattice == LK_FINSET) {
+    /* One degenerate range per live candidate, with no read-time carving. The
+     * interval path below carves C_EXCLUDE holes here because a single
+     * interval cannot hold them; a bitmask can, so estimate_meet has already
+     * applied every exclude at or above the floor `e` was resolved at. Carving
+     * again would be a no-op at best and, if handed a different floor than `e`
+     * was resolved at, inconsistent with the mask. */
     int n = 0;
     for (int i = 0; i < qd->n_candidates && n < out_max; i++)
       if (e->lo & (1ul << i)) {

src/include/kasld/estimate.h

@@ -48,7 +48,9 @@ struct estimate {
    * value satisfies (q % stride) == stride_offset in addition to lying in
    * [lo, hi]. Multiple C_STRIDE constraints fold via CRT in estimate_meet;
    * unsolvable systems push the estimate to bottom. Always 0 on
-   * LK_MAXALIGN / LK_FINSET (the stride concept doesn't apply there). */
+   * LK_MAXALIGN / LK_FINSET. On a finite set a C_STRIDE still narrows — it
+   * drops every candidate outside the residue class — but it does so directly,
+   * leaving no annotation to carry afterwards. */
   unsigned long stride;
   unsigned long stride_offset;
 };
@@ -98,6 +100,47 @@ int estimate_is_bottom(const struct estimate *e, const struct quantity_def *qd);
 int estimate_finset_value(const struct quantity_def *qd,
                           const struct estimate *e, unsigned long *out);
 
+/* ------------------------------------------------------------------------
+ * Lattice-agnostic value access.
+ *
+ * `struct estimate` means different things per lattice — on LK_FINSET `lo` is
+ * a live-candidate BITMASK and `hi` is unused — so reading `.lo` / `.hi`
+ * directly only works if the caller already knows the quantity's lattice. That
+ * coupling is what these exist to remove: a quantity may change lattice (or an
+ * arch may compile it differently) without every consumer changing with it.
+ *
+ * `.lo_binding` and `.lo_conf` stay directly readable. They carry the same
+ * meaning on every lattice — the constraint that last narrowed the estimate,
+ * and its confidence — and no consumer reads the `hi_` pair, which LK_FINSET
+ * never sets.
+ * ------------------------------------------------------------------------ */
+
+/* Narrowed to exactly one value? Writes it to *out (may be NULL) and returns 1.
+ * An alignment (LK_MAXALIGN) is never a value, so it never pins. */
+int quantity_pinned(enum kasld_quantity q, const struct estimate *e,
+                    unsigned long *out);
+
+/* The smallest window CONTAINING every value still admitted — for LK_FINSET
+ * the lowest and highest live candidates, which is wider than the live set
+ * itself. Use quantity_admits() to ask about one value; use this only for
+ * arithmetic that genuinely wants edges. Returns 0 (leaving *lo / *hi
+ * untouched) when nothing is admitted, which also covers the bottom estimate.
+ * Either output may be NULL. */
+int quantity_window(enum kasld_quantity q, const struct estimate *e,
+                    unsigned long *lo, unsigned long *hi);
+
+/* Is `v` still possible? Exact on LK_FINSET. On LK_INTERVAL it honours the
+ * stride annotation but not interior C_EXCLUDE holes, which the lattice does
+ * not carry — so it can answer "yes" for a value a hole has removed. That
+ * direction is the sound one (it over-admits, never under-admits) and matches
+ * what edge comparisons already did. */
+int quantity_admits(enum kasld_quantity q, const struct estimate *e,
+                    unsigned long v);
+
+/* Has anything been proven about this quantity, or is it still at its honest
+ * top? Replaces open-coded comparisons against a freshly built top. */
+int quantity_narrowed(enum kasld_quantity q, const struct estimate *e);
+
 /* Resolve quantity q over the constraints in cs[0..n_cs), considering only
  * those with conf >= floor. Greedy strongest-first (conf DESC, lineage_count
  * DESC, id ASC); a constraint that would force bottom is skipped and

src/include/kasld/quantity.h

@@ -64,6 +64,14 @@ struct quantity_def {
   int n_candidates;
 };
 
+/* Upper bound on n_candidates. An LK_FINSET estimate stores its live set as a
+ * bitmask in a single unsigned long, so a longer list would have candidates
+ * with no bit to live in — and `1ul << i` past the word width is undefined
+ * rather than merely wrong. Every candidate table is checked against this at
+ * compile time in quantities.c, so the meet loop can shift without a runtime
+ * guard. */
+#define KASLD_FINSET_MAX_CANDIDATES ((int)(sizeof(unsigned long) * 8))
+
 extern const struct quantity_def quantities[Q__COUNT];
 
 #endif /* KASLD_QUANTITY_H */

src/orchestrator.c

@@ -3821,8 +3821,12 @@ static void engine_sync_authoritative(const struct engine *e) {
     layout.phys_kaslr_align = e->est[Q_VIRT_KASLR_ALIGN].lo;
 #endif
 
-  layout.virt_page_offset_min = e->est[Q_PAGE_OFFSET].lo;
-  layout.virt_page_offset_max = e->est[Q_PAGE_OFFSET].hi;
+  /* The rendered min/max are the window CONTAINING every admitted value, which
+   * is what the map draws as the direct-map band's uncertainty. On a lattice
+   * that can hold gaps this is wider than the live set — the right direction
+   * for a band, which must not appear narrower than the evidence supports. */
+  quantity_window(Q_PAGE_OFFSET, &e->est[Q_PAGE_OFFSET],
+                  &layout.virt_page_offset_min, &layout.virt_page_offset_max);
 
   /* Project the resolved direct-map base onto the rendered singular field
    * whenever the engine has pinned it. On coupled arches PAGE_OFFSET equals
@@ -3831,9 +3835,12 @@ static void engine_sync_authoritative(const struct engine *e) {
    * it to a different boundary, and the render must follow the engine rather
    * than show the compile-time seed. (The decoupled, possibly-unpinned
    * RANDOMIZE_MEMORY case is handled by the block below.) */
-  if (e->est[Q_PAGE_OFFSET].lo == e->est[Q_PAGE_OFFSET].hi &&
-      e->est[Q_PAGE_OFFSET].lo != 0)
-    layout.virt_page_offset = e->est[Q_PAGE_OFFSET].lo;
+  {
+    unsigned long po_pin;
+    if (quantity_pinned(Q_PAGE_OFFSET, &e->est[Q_PAGE_OFFSET], &po_pin) &&
+        po_pin != 0)
+      layout.virt_page_offset = po_pin;
+  }
 
 #if !TEXT_TRACKS_DIRECTMAP
   /* On decoupled arches the direct-map base (PAGE_OFFSET) is randomized away
@@ -3850,8 +3857,10 @@ static void engine_sync_authoritative(const struct engine *e) {
    * begins at the directmap base. */
   {
     const struct estimate *po = &e->est[Q_PAGE_OFFSET];
-    if (po->lo > (unsigned long)PAGE_OFFSET)
-      layout.virt_page_offset = po->lo;
+    unsigned long po_lo;
+    if (quantity_window(Q_PAGE_OFFSET, po, &po_lo, NULL) &&
+        po_lo > (unsigned long)PAGE_OFFSET)
+      layout.virt_page_offset = po_lo;
   }
 
   const struct estimate *pt = &e->est[Q_PHYS_IMAGE_BASE];
@@ -3954,20 +3963,27 @@ static void engine_sync_authoritative(const struct engine *e) {
    * reject a real module leak -- the failure mode the union contract guards. */
   {
     const struct estimate *po = &e->est[Q_PAGE_OFFSET];
-    int pinned = (po->lo == po->hi && po->lo != 0);
-    int default_excluded = po->lo > (unsigned long)PAGE_OFFSET ||
-                           po->hi < (unsigned long)PAGE_OFFSET;
-    if (po->lo && po->lo <= po->hi && (pinned || default_excluded)) {
-      unsigned long lo = MODULES_START_FOR(po->lo);
-      unsigned long hi = MODULES_END_FOR(po->hi);
+    unsigned long po_lo = 0, po_hi = 0, po_pin = 0;
+    int have = quantity_window(Q_PAGE_OFFSET, po, &po_lo, &po_hi);
+    int pinned = quantity_pinned(Q_PAGE_OFFSET, po, &po_pin) && po_pin != 0;
+    /* Ask the estimate whether the compile-time split is still admitted rather
+     * than comparing it against the window edges: on a lattice that can hold
+     * gaps, an edge comparison still calls an excluded interior value
+     * possible, and this test is what decides whether the band may move off
+     * that split at all. */
+    int default_excluded =
+        !quantity_admits(Q_PAGE_OFFSET, po, (unsigned long)PAGE_OFFSET);
+    if (have && po_lo && (pinned || default_excluded)) {
+      unsigned long lo = MODULES_START_FOR(po_lo);
+      unsigned long hi = MODULES_END_FOR(po_hi);
       /* Reject a wrapped floor; do NOT clamp it to KERNEL_VIRT_VAS_START. On
        * every arch that carves the module band out of vmalloc the band
        * legitimately sits BELOW PAGE_OFFSET, and on those KERNEL_VIRT_VAS_START
        * *is* PAGE_OFFSET -- clamping there would discard the whole band and
        * reject every genuine module leak, the exact failure the union contract
        * above exists to prevent. Same wrap test that
        * rules/module_base_bounds.c applies to these edges. */
-      if (kasld_module_band_floor_sane(po->lo, lo) && hi > lo) {
+      if (kasld_module_band_floor_sane(po_lo, lo) && hi > lo) {
         mod_union_lo = lo;
         mod_union_hi = hi;
         layout.modules_start = lo;

src/quantities.c

@@ -30,6 +30,12 @@ static const unsigned long va_bits_candidates[] = {48ul};
 #endif
 #define N_VA_BITS                                                              \
   ((int)(sizeof(va_bits_candidates) / sizeof(va_bits_candidates[0])))
+/* The live set is a bitmask in one unsigned long; see the bound's definition
+ * in quantity.h. Checked here so estimate_meet's `1ul << i` needs no runtime
+ * guard, on the 32-bit builds too. */
+__extension__ _Static_assert(N_VA_BITS <= KASLD_FINSET_MAX_CANDIDATES,
+                             "VA_BITS_CANDIDATES longer than the finite-set "
+                             "bitmask can represent");
 
 /* ---- honest tops ------------------------------------------------------ */