⏺ Stage B is built and green. #21

Merged
navicore merged 2 commits from fact-table-stage-B into main 2026-06-18 18:37:04 +00:00
Owner

What landed

First-argument index — bound-key fact queries now binary-search instead of
full-scanning:

  • Codegen (facts.rs): for arity ≥ 1, emit a second .rodata global
    @plg_facts___idx — row indices sorted by (column-0 word, row), so
    within a key they stay in program order. The entry passes the index pointer
    (null for arity-0) to the lookup. One extra word per row.
  • Runtime (facts.rs): plg_rt_fact_first derefs the first arg; when it's a
    bound atom/int (column 0's exact domain), equal_range binary-searches the
    index for [lower, upper) and the scan iterates only that range, mapping
    each position through the index. Unbound or non-immediate first args fall
    back to the full scan — identical to Stage A. The fast path is only taken
    where Word-equality coincides with what unify accepts, so the indexed set
    is exactly the rows Stage A would have matched, in the same order.

#3 single-unify cleanup — added Machine::push_cp_at(retry, env, trail_mark,
heap_mark) (a choice point with an explicit pre-binding restore-point).
fact_scan now binds a matching row once: it pushes the CP with the captured
clean marks instead of unify → rewind → re-unify. Failed rows still rewind
and continue.

Verification

  • Equivalence: differential byte-identical to the v1 oracle; the existing
    fact_table + family suites (bound-key queries like parent(tom,X),
    parent(bob,ann) now route through the index) all pass.
  • New tests: indexed_lookup_gathers_nonadjacent_rows_in_program_order (key
    tom at rows 0/3/4 → a,d,e, skipping interleaved rows; absent key fast-fails
    via empty range); golden test asserts the _idx global is emitted.
  • 100k bound-key query correct and no longer scans the table; no-match
    fast-fails. Full workspace green, clippy + fmt clean.
  • FACT_TABLE.md checkpoint 2 updated to record Stage B.
What landed First-argument index — bound-key fact queries now binary-search instead of full-scanning: - Codegen (facts.rs): for arity ≥ 1, emit a second .rodata global @plg_facts_<f>_<a>_idx — row indices sorted by (column-0 word, row), so within a key they stay in program order. The entry passes the index pointer (null for arity-0) to the lookup. One extra word per row. - Runtime (facts.rs): plg_rt_fact_first derefs the first arg; when it's a bound atom/int (column 0's exact domain), equal_range binary-searches the index for [lower, upper) and the scan iterates only that range, mapping each position through the index. Unbound or non-immediate first args fall back to the full scan — identical to Stage A. The fast path is only taken where Word-equality coincides with what unify accepts, so the indexed set is exactly the rows Stage A would have matched, in the same order. #3 single-unify cleanup — added Machine::push_cp_at(retry, env, trail_mark, heap_mark) (a choice point with an explicit pre-binding restore-point). fact_scan now binds a matching row once: it pushes the CP with the captured clean marks instead of unify → rewind → re-unify. Failed rows still rewind and continue. Verification - Equivalence: differential byte-identical to the v1 oracle; the existing fact_table + family suites (bound-key queries like parent(tom,X), parent(bob,ann) now route through the index) all pass. - New tests: indexed_lookup_gathers_nonadjacent_rows_in_program_order (key tom at rows 0/3/4 → a,d,e, skipping interleaved rows; absent key fast-fails via empty range); golden test asserts the _idx global is emitted. - 100k bound-key query correct and no longer scans the table; no-match fast-fails. Full workspace green, clippy + fmt clean. - FACT_TABLE.md checkpoint 2 updated to record Stage B.
⏺ Stage B is built and green.
All checks were successful
CI - Linux / CI - Linux x86_64 (pull_request) Successful in 1m33s
b84f9ac371
What landed

  First-argument index — bound-key fact queries now binary-search instead of
  full-scanning:
  - Codegen (facts.rs): for arity ≥ 1, emit a second .rodata global
  @plg_facts_<f>_<a>_idx — row indices sorted by (column-0 word, row), so
  within a key they stay in program order. The entry passes the index pointer
  (null for arity-0) to the lookup. One extra word per row.
  - Runtime (facts.rs): plg_rt_fact_first derefs the first arg; when it's a
  bound atom/int (column 0's exact domain), equal_range binary-searches the
  index for [lower, upper) and the scan iterates only that range, mapping
  each position through the index. Unbound or non-immediate first args fall
  back to the full scan — identical to Stage A. The fast path is only taken
  where Word-equality coincides with what unify accepts, so the indexed set
  is exactly the rows Stage A would have matched, in the same order.

  #3 single-unify cleanup — added Machine::push_cp_at(retry, env, trail_mark,
  heap_mark) (a choice point with an explicit pre-binding restore-point).
  fact_scan now binds a matching row once: it pushes the CP with the captured
  clean marks instead of unify → rewind → re-unify. Failed rows still rewind
  and continue.

  Verification

  - Equivalence: differential byte-identical to the v1 oracle; the existing
  fact_table + family suites (bound-key queries like parent(tom,X),
  parent(bob,ann) now route through the index) all pass.
  - New tests: indexed_lookup_gathers_nonadjacent_rows_in_program_order (key
  tom at rows 0/3/4 → a,d,e, skipping interleaved rows; absent key fast-fails
  via empty range); golden test asserts the _idx global is emitted.
  - 100k bound-key query correct and no longer scans the table; no-match
  fast-fails. Full workspace green, clippy + fmt clean.
  - FACT_TABLE.md checkpoint 2 updated to record Stage B.
Author
Owner

Review — Fact-table Stage B (first-argument index)

Tight, focused PR that closes out two open items from prior reviews — the O(log n) bound-key lookup, and PR #20 review #3's double-unify-and-rewind cleanup via the new push_cp_at primitive. The correctness reasoning is the load-bearing piece, and it's right: the index is sorted by raw u64 (Word) comparison, the binary search uses the same comparator, and the fast path is gated on TAG_ATOM | TAG_INT — the exact column-0 domain where Word equality coincides with what unify accepts. So the indexed set equals what Stage A would have matched, in the same order. The comment near equal_range makes this explicit, which is the right place for it.

Other strong calls:

  • push_cp_at is the right abstraction, not a fact-table-private helper. Any future nondeterministic builtin that wants to bind-then-record-restore-point can reuse it. The single-unify cleanup is the immediate beneficiary; that's a reusable primitive earned by doing it.
  • Ties on col 0 preserve program order. sort_by_key(|&r| (col0, r)) — solution order = program order is preserved through the index, which is the whole point. indexed_lookup_gathers_nonadjacent_rows_in_program_order pins it.
  • Mixed-type col 0 works correctly. Atoms and ints have distinct tag bits, so the u64-sorted index naturally clusters by type. The binary search lands in the right cluster. Elegant — no special-case for "this column is atoms" vs "this column is ints."
  • Empty equal_range fast-fails the absent-key case. A bound key not in the table returns (lower, lower), the loop sees pos >= end immediately, returns 0. Tested via rel(zzz, X).
  • Fallback to full-scan for unbound or non-immediate first args keeps Stage A semantics. Stage B is strictly additive.

Issues below, ordered by impact — none are blockers.

Real concerns

1. push_cp_at's contract is debug-only. debug_assert!(trail_mark <= self.trail.len() && heap_mark <= self.heap.len()) only fires in debug builds. In release, an out-of-range mark passed by a future caller would silently no-op the truncate at backtrack time (Vec::truncate(N) where N > len() is a no-op), which would manifest as state-leak bugs — bindings from an "undone" alternative surviving into the next. The single in-tree caller (fact_scan) is correct, but the primitive is now publicly visible (pub fn) and the next caller has to know this. Two options:

  • Clamp in release: let trail_mark = trail_mark.min(self.trail.len()); — small overhead, defensive.
  • Document the invariant explicitly on the function doc: "CALLER MUST GUARANTEE marks are ≤ current lengths; out-of-range marks silently no-op in release."

Leaning toward the doc note since the clamp would hide bugs rather than expose them. But pick one — a pub API with a debug-only contract is the failure mode that bites later.

2. Stage B's perf claim is structural, not measured. FACT_TABLE.md now reads "Stage B (2026-06-18): a first-arg index ... gives bound-key queries an O(log n) binary search to the matching row range." Structurally true by construction. But Stage A's note in the same doc cited an actual measurement ("100k 2-column facts ... compile in ~1.0s total ... 4.5M binary ... a worst-case bound-key query over 100k rows ~90ms"). The natural close-the-loop for Stage B is "and the same 100k query now takes <Xms," which would be a one-line criterion bench or even just a tests/perf/ one-off the dev runs. It's the same measurement gap PR #20 review #1 flagged — closer to closed now, since the structural path is in place, but still not measured. Worth either landing the number or being explicit that the Stage B perf claim is structural-not-measured.

Small observations

3. Float column lookups will be a future Stage C concern. Today Stage A's fact_columns rejects float first args (column 0 is atom/int only), so the indexed path is correct for what's in the table. If Stage C adds float columns to fact tables, the binary search will need to be revisited: NaN doesn't have a total order, and float equality has its own gotchas (-0.0 == 0.0 but their bit patterns differ; quiet NaN vs signaling NaN). A note in FACT_TABLE.md's Stage C section saying "float columns will need a non-u64 comparator or a normalized bit representation in the index" would head off a "let's just use the same equal_range" reflex.

4. The "IDX=0 means no index" sentinel. Works because no real .rodata global lives at address 0 (page zero is unmapped). Standard C-FFI convention. Worth a one-line comment at the IDX constant declaration confirming the sentinel choice — a reader who isn't FFI-fluent might wonder why an array pointer ever equals zero.

5. The frame-layout comments could cross-reference the cursor→row mapping. The IDX constant says "first-arg index pointer, or 0 for a full scan"; CURSOR says "next position to try — mutated in place, untrailed"; END says "exclusive upper bound of the cursor's range." The actual semantics — that cursor is a position in [cursor_0, end) that maps to a row through idx[cursor] when set, else IS the row — only appears in fact_scan's body. A one-line "(see fact_scan for the cursor→row mapping)" at IDX/CURSOR would save the reader a hop.

6. equal_range is two explicit binary searches. Could be replaced by slice::partition_point for slightly more idiomatic Rust:

let lower = (0..idx.len()).collect::<Vec<_>>().partition_point(|&k| col0(k) < key);

But the explicit form is more transparent and matches the comment ("lower bound: first k with col0(k) >= key"). Keep it.

7. The new fact_scan loop bumps CURSOR unconditionally after the unify try. Old Stage A bumped CURSOR only on the matched branch; on failure, the bump happened implicitly via the next iteration's i += 1. New shape: one write, both branches. Cleaner; doesn't change semantics. Just noting that the write-survives-backtrack invariant (CURSOR is untrailed, frame cells survive heap truncation) is the same as before — worth confirming with a one-line "the CURSOR write is intentionally untrailed; it advances monotonically across the CP's resume" at the bump site if a reader has to verify it.

What's good

  • Word equality coincides with unify semantics for atom/int. The single load-bearing claim of the indexed fast path, explicitly documented, and correct. Tag bits distinguish atom from int so mixed columns work without special-casing.
  • push_cp_at is reusable, not fact-table-private. The single-unify cleanup is the first beneficiary; future nondeterministic builtins (Stage C compound-column unify, or a future indexed between/3-style) can reuse the primitive without reinventing it.
  • Frame layout extends cleanly. IDX/END are named constants slotted into the prefix; ARGS moves accordingly. No clever encoding.
  • The fallback path is the Stage A path, byte-identical. Unbound or non-immediate first args take exactly the previous code path. Stage B can't regress anything Stage A handled.
  • Two new integration tests pin the non-trivial cases: non-adjacent rows visited in program order (key tom at rows 0/3/4 → solutions a, d, e in that order), and absent-key fast-fail (binary search empty range). Plus the golden test asserts the _idx global is emitted.
  • The differential corpus (existing bound-key queries like parent(tom, X)) now exercises the indexed path automatically without any test churn — the equivalence pin from Stage A still byte-matches the oracle through the new code.
  • The PR description names the load-bearing invariant ("the fast path is only taken where Word-equality coincides with what unify accepts"), so a future contributor reading the commit log understands the design discipline before reading the code.

Suggested order

#1 (push_cp_at contract — pick docs or clamp) and #2 (measure the Stage B perf claim, or downgrade the FACT_TABLE.md wording from "gives O(log n)" to "structurally O(log n)") are worth doing before merge. #3 (float Stage C note in FACT_TABLE.md) is one line and saves future-you a reflex. #4+ are observations.

## Review — Fact-table Stage B (first-argument index) Tight, focused PR that closes out two open items from prior reviews — the O(log n) bound-key lookup, and PR #20 review #3's double-unify-and-rewind cleanup via the new `push_cp_at` primitive. The correctness reasoning is the load-bearing piece, and it's right: the index is sorted by raw `u64` (Word) comparison, the binary search uses the same comparator, and the fast path is gated on `TAG_ATOM | TAG_INT` — the exact column-0 domain where Word equality coincides with what `unify` accepts. So the indexed set equals what Stage A would have matched, in the same order. The comment near `equal_range` makes this explicit, which is the right place for it. Other strong calls: - **`push_cp_at` is the right abstraction**, not a fact-table-private helper. Any future nondeterministic builtin that wants to bind-then-record-restore-point can reuse it. The single-unify cleanup is the immediate beneficiary; that's a reusable primitive earned by doing it. - **Ties on col 0 preserve program order.** `sort_by_key(|&r| (col0, r))` — solution order = program order is preserved through the index, which is the whole point. `indexed_lookup_gathers_nonadjacent_rows_in_program_order` pins it. - **Mixed-type col 0 works correctly.** Atoms and ints have distinct tag bits, so the u64-sorted index naturally clusters by type. The binary search lands in the right cluster. Elegant — no special-case for "this column is atoms" vs "this column is ints." - **Empty equal_range fast-fails the absent-key case.** A bound key not in the table returns `(lower, lower)`, the loop sees `pos >= end` immediately, returns 0. Tested via `rel(zzz, X)`. - **Fallback to full-scan for unbound or non-immediate first args** keeps Stage A semantics. Stage B is strictly additive. Issues below, ordered by impact — none are blockers. ### Real concerns **1. `push_cp_at`'s contract is debug-only.** `debug_assert!(trail_mark <= self.trail.len() && heap_mark <= self.heap.len())` only fires in debug builds. In release, an out-of-range mark passed by a future caller would silently no-op the truncate at backtrack time (`Vec::truncate(N)` where `N > len()` is a no-op), which would manifest as state-leak bugs — bindings from an "undone" alternative surviving into the next. The single in-tree caller (`fact_scan`) is correct, but the primitive is now publicly visible (`pub fn`) and the next caller has to know this. Two options: - Clamp in release: `let trail_mark = trail_mark.min(self.trail.len());` — small overhead, defensive. - Document the invariant explicitly on the function doc: "**CALLER MUST GUARANTEE** marks are ≤ current lengths; out-of-range marks silently no-op in release." Leaning toward the doc note since the clamp would hide bugs rather than expose them. But pick one — a `pub` API with a debug-only contract is the failure mode that bites later. **2. Stage B's perf claim is structural, not measured.** FACT_TABLE.md now reads "*Stage B (2026-06-18):* a first-arg index ... gives bound-key queries an O(log n) binary search to the matching row range." Structurally true by construction. But Stage A's note in the same doc cited an actual measurement ("100k 2-column facts ... compile in ~1.0s total ... 4.5M binary ... a worst-case bound-key query over 100k rows ~90ms"). The natural close-the-loop for Stage B is "and the same 100k query now takes <Xms," which would be a one-line `criterion` bench or even just a `tests/perf/` one-off the dev runs. It's the same measurement gap PR #20 review #1 flagged — closer to closed now, since the structural path is in place, but still not measured. Worth either landing the number or being explicit that the Stage B perf claim is structural-not-measured. ### Small observations **3. Float column lookups will be a future Stage C concern.** Today Stage A's `fact_columns` rejects float first args (column 0 is atom/int only), so the indexed path is correct for what's in the table. If Stage C adds float columns to fact tables, the binary search will need to be revisited: NaN doesn't have a total order, and float equality has its own gotchas (`-0.0 == 0.0` but their bit patterns differ; quiet NaN vs signaling NaN). A note in FACT_TABLE.md's Stage C section saying "float columns will need a non-`u64` comparator or a normalized bit representation in the index" would head off a "let's just use the same equal_range" reflex. **4. The "IDX=0 means no index" sentinel.** Works because no real `.rodata` global lives at address 0 (page zero is unmapped). Standard C-FFI convention. Worth a one-line comment at the IDX constant declaration confirming the sentinel choice — a reader who isn't FFI-fluent might wonder why an array pointer ever equals zero. **5. The frame-layout comments could cross-reference the cursor→row mapping.** The IDX constant says "first-arg index pointer, or 0 for a full scan"; CURSOR says "next position to try — mutated in place, untrailed"; END says "exclusive upper bound of the cursor's range." The actual semantics — that `cursor` is a position in `[cursor_0, end)` that maps to a row through `idx[cursor]` when set, else IS the row — only appears in `fact_scan`'s body. A one-line "(see fact_scan for the cursor→row mapping)" at IDX/CURSOR would save the reader a hop. **6. `equal_range` is two explicit binary searches.** Could be replaced by `slice::partition_point` for slightly more idiomatic Rust: ```rust let lower = (0..idx.len()).collect::<Vec<_>>().partition_point(|&k| col0(k) < key); ``` But the explicit form is more transparent and matches the comment ("lower bound: first k with col0(k) >= key"). Keep it. **7. The new fact_scan loop bumps CURSOR unconditionally after the unify try.** Old Stage A bumped CURSOR only on the matched branch; on failure, the bump happened implicitly via the next iteration's `i += 1`. New shape: one write, both branches. Cleaner; doesn't change semantics. Just noting that the write-survives-backtrack invariant (CURSOR is untrailed, frame cells survive heap truncation) is the same as before — worth confirming with a one-line "the CURSOR write is intentionally untrailed; it advances monotonically across the CP's resume" at the bump site if a reader has to verify it. ### What's good - **Word equality coincides with unify semantics for atom/int.** The single load-bearing claim of the indexed fast path, explicitly documented, and correct. Tag bits distinguish atom from int so mixed columns work without special-casing. - **`push_cp_at` is reusable**, not fact-table-private. The single-unify cleanup is the first beneficiary; future nondeterministic builtins (Stage C compound-column unify, or a future indexed `between/3`-style) can reuse the primitive without reinventing it. - **Frame layout extends cleanly.** IDX/END are named constants slotted into the prefix; ARGS moves accordingly. No clever encoding. - **The fallback path is the Stage A path, byte-identical.** Unbound or non-immediate first args take exactly the previous code path. Stage B can't regress anything Stage A handled. - **Two new integration tests** pin the non-trivial cases: non-adjacent rows visited in program order (key `tom` at rows 0/3/4 → solutions `a, d, e` in that order), and absent-key fast-fail (binary search empty range). Plus the golden test asserts the `_idx` global is emitted. - **The differential corpus** (existing bound-key queries like `parent(tom, X)`) now exercises the indexed path automatically without any test churn — the equivalence pin from Stage A still byte-matches the oracle through the new code. - **The PR description names the load-bearing invariant** ("the fast path is only taken where Word-equality coincides with what unify accepts"), so a future contributor reading the commit log understands the design discipline before reading the code. ### Suggested order #1 (`push_cp_at` contract — pick docs or clamp) and #2 (measure the Stage B perf claim, or downgrade the FACT_TABLE.md wording from "gives O(log n)" to "structurally O(log n)") are worth doing before merge. #3 (float Stage C note in FACT_TABLE.md) is one line and saves future-you a reflex. #4+ are observations.
⏺ Done — all gates green, clippy + fmt clean, changes behavior-preserving
All checks were successful
CI - Linux / CI - Linux x86_64 (pull_request) Successful in 58s
fdfcbb4729
(only comments + doc + the push_cp_at doc text changed; no logic).

  Review disposition (PR #21)

  Before-merge items:
  - #1 (push_cp_at debug-only contract) — added an explicit "CALLER MUST
  GUARANTEE … out-of-range marks silently no-op in release" warning to the
  doc. Chose docs over a release clamp, per the reviewer's reasoning that a
  clamp would mask bugs the debug assertion is there to expose.
  - #2 (perf claim unmeasured) — measured it at 500k rows: the indexed
  bound-first-arg query is flat ~0.36s regardless of key position (= the
  binary-load/startup floor, matched by the absent-key case), vs ~0.47s for a
  comparable full scan over the rows. Recorded in FACT_TABLE.md, stating
  plainly that the index removes the linear scan but its absolute win is
  asymptotic — at single-query CLI scale the per-row compare is cheap
  relative to process startup, so the payoff grows with N and query volume.
  - #3 (float-column indexing) — added a Stage C caveat under Constraints:
  the u64 equal_range can't be reused for floats (no total order on bits,
  -0.0 == 0.0 bit-differ, NaN), so float keys need a normalized
  representation or stay unindexed.

  Readability comments added: #4 (IDX=0 sentinel — no .rodata at address 0),
  #5 (cursor→row mapping cross-ref at IDX/CURSOR), #7 (the cursor bump is
  intentionally untrailed and advances monotonically across a CP resume).

  No change: #6 — reviewer said keep the explicit two-binary-search form over
  partition_point.

  Everything else was praise / correctly-deferred. Stage C —
  compound/float/big-int columns via a codegen serializer + copyterm restore
  — is next, with the float-indexing constraint now on record. Ready on your
  word.
navicore deleted branch fact-table-stage-B 2026-06-18 18:37:04 +00:00
Sign in to join this conversation.
No reviewers
No labels
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
navicore/patch-prolog!21
No description provided.