feat(ilp): Tensorized Differentiable ILP engine by levi770 · Pull Request #1 · BrainyBlaze/xlog

levi770 · 2026-02-25T15:46:53Z

Summary

Adds full-stack Tensorized Differentiable ILP (Inductive Logic Programming) to XLOG, enabling gradient-based logical rule learning via a continuous N×N×N tensor mask over a predicate super-graph
Frontend: New learnable(W) :: head(X,Y) :- body1(X,Z), body2(Z,Y). grammar production, AST type, parser, stratifier integration, optimizer pass-through, and RIR lowering to TensorMaskedJoin node
Runtime: IlpRegistry for mask lifecycle + DLPack zero-copy bridge, execute_tensor_masked_join with GPU kernel extraction → hash-join dispatch → head projection → per-target union/diff
CUDA: New ilp.cu kernel (extract_nonzero_indices) for GPU-side active rule extraction with soft-mask priority sorting and budget cap
Python: CompiledIlpProgram PyO3 class with set_rule_mask, evaluate, get_tagged_results, fact_exists, tagged_entries_containing_fact, commit_induced_rule — full ST-Gumbel-Softmax training loop support

Validation

Gate	Result
Rust workspace tests	All pass (0 failures)
CUDA certification suite	206/206 pass
Python tests (full suite)	154 passed, 11 skipped
ILP Python tests	7/7 pass
ILP Rust integration tests	5/5 pass
ILP CUDA kernel tests	5/5 pass

Key design decisions (from RFC v4.4, 37 RDs)

Product T-norm for non-vanishing gradient flow (RD-5)
DLPack zero-copy tensor bridge — Python flattens 3D→1D, .detach() before export (RD-6)
Budget cap via max_active_rules (default 32) with soft-mask priority sorting (RD-9)
Head projection to map join result columns to head schema (discovered during integration testing)
Arity guard in executor — skip relations where join key indices exceed arity (RD-37 robustness)

Test plan

Grammar parses learnable(W) :: head :- body. syntax
AST round-trips through parser
Stratifier adds learnable rule edges to dependency graph
Lowerer produces TensorMaskedJoin with correct rel_index and head_projection
CUDA kernel extracts correct indices, respects budget cap, handles empty mask
Executor no-ops when no mask registered, joins correctly with identity mask, tags metadata
Python: compile → set_mask → evaluate → get_tagged_results → gradient flow
Python: temperature annealing increases discreteness, missed-positive penalty fires
Python: predecessor benchmark smoke runs 5 optimizer steps without crash

Wire parser dispatch for learnable_rule grammar production: when the parser encounters Rule::learnable_rule, it calls build_learnable_rule which uses existing build_head and build_body helpers to construct a LearnableRule AST node and pushes it into program.learnable_rules. Also adds mask_name grammar rule that accepts both lowercase and uppercase-starting identifiers for tensor mask parameters (e.g. W_mask). Includes test fixture (learnable.xlog) and two integration tests verifying correct parsing and separation from normal rules.

Add lower_learnable_rule and extract_template_join_keys to the Lowerer, wired into lower_program before the final build(). Validates body shape (RD-34), sorts rel_index by RelId (RD-36), and lazily allocates head RelIds (RD-30). Also adds TensorMaskedJoin stub arms to executor match sites so the workspace compiles cleanly.

Add ILP tensor mask registry module with: - IlpRegistry for managing hard/soft mask pairs per learnable rule - IlpMask, IlpTaggedResult, IlpTagEntry types - read_device_row_count helper using public APIs (RD-22) - Executor fields: ilp_registry and ilp_last_result - Accessor methods: ilp_registry_mut() and ilp_last_result()

…ding Add three integration tests for TensorMaskedJoin execution: - T3.1: Identity mask activating (b1, b2) -> reach produces correct join - T3.2: Empty mask (all zeros) produces no derivations - T3.3: No mask registered results in graceful no-op Also fixes two bugs discovered during testing: - Add head_projection field to TensorMaskedJoin IR node so the executor can project join results (left++right columns) down to head arity - Infer schemas for learnable rule head predicates during lowering (previously only facts/rules were handled by infer_schemas)

Three tests covering the tensorized ILP Python API: - test_ilp_compile_and_schema: verifies IlpProgramFactory.compile() and schema introspection - test_ilp_set_mask_and_evaluate: validates mask injection and zero-mask produces no results - test_ilp_gradient_flow: confirms ST-Gumbel-Softmax gradients flow through per-fact surrogate credit assignment (RFC T4.1, RD-21, RD-24)

M1: Parse failure on malformed learnable rules, referenced_relations completeness, optimizer TMJ handling. M2: ILP module load verification, multi-element extraction with priority sorting. M3: Tag metadata correctness, diff-based deduplication across repeated executions. M4/M5: Missed-positive penalty gradient flow, temperature annealing discreteness, predecessor benchmark smoke test, rule commit with post-commit evaluation.

- Add arity bounds check before hash_join_v2: skip relations where join key column indices exceed the relation's arity (prevents crash when mask maps a body slot to a relation with fewer columns) - Fix predecessor smoke test to use uniform 2-arity predicates - Fix pre-existing useless_vec clippy lint in xlog-ir/plan.rs - Suppress dead_code warning for _learnable_source in pyxlog - Update Cargo.lock for pyxlog dependency additions

- RFC v4.4 with 37 resolved design decisions - 15-task implementation plan (all tasks completed)

Copilot

Pull request overview

This pull request adds a comprehensive Tensorized Differentiable ILP (Inductive Logic Programming) system to XLOG, enabling gradient-based logical rule learning through continuous tensor masks over predicate super-graphs.

Changes:

Frontend: New learnable(W) :: head(X,Y) :- body1(X,Z), body2(Z,Y) syntax with full AST, parser, stratification, optimizer, and lowering support
Runtime: ILP registry for mask lifecycle, GPU kernel for active rule extraction, hash-join dispatch with head projection, and per-rule metadata tagging
CUDA: New extract_nonzero_indices kernel with priority sorting and budget capping
Python: CompiledIlpProgram PyO3 class with mask injection, evaluation, gradient flow support via tagged results, and rule commitment

Reviewed changes

Copilot reviewed 27 out of 28 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
`crates/xlog-logic/src/grammar.pest`	Adds learnable_rule production to grammar
`crates/xlog-logic/src/ast.rs`	Defines LearnableRule struct
`crates/xlog-logic/src/parser.rs`	Implements learnable rule parsing
`crates/xlog-logic/src/stratify.rs`	Adds learnable edges to dependency graph
`crates/xlog-logic/src/optimizer.rs`	Pass-through arms for TensorMaskedJoin
`crates/xlog-logic/src/lower.rs`	Lowers learnable rules to TensorMaskedJoin with head projection
`crates/xlog-ir/src/rir.rs`	Defines TensorMaskedJoin IR node variant
`kernels/ilp.cu`	CUDA kernel for extracting active mask indices
`crates/xlog-cuda/src/provider.rs`	Provider wrapper for ILP kernel with priority sorting
`crates/xlog-runtime/src/ilp_registry.rs`	Registry for tensor mask management
`crates/xlog-runtime/src/executor.rs`	TensorMaskedJoin execution with join dispatch and head projection
`crates/pyxlog/src/lib.rs`	IlpProgramFactory and CompiledIlpProgram Python bindings
`python/tests/test_ilp.py`	Python integration tests for gradient flow

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

- Guard torch.nn.functional import with pytest.importorskip - Clarify mask_name vs ident difference in grammar comment - Document semantic correctness as optimizer responsibility (RD-37) - Add comment explaining commit_induced_rule uses concrete predicates

The reviewer flagged cudarc init failures — this was an env issue (missing LD_LIBRARY_PATH), not a test gate issue. Keep the standard torch.cuda.is_available() check consistent with all other test files.

1. tagged_entries_containing_fact now applies head_projection when checking join results against head facts. Previously checked raw 4-col join output against 2-col head values (always false negative). 2. Learnable rule lowering now fails compilation when head contains variables not present in body atoms or constants. Previously silently defaulted unbound variables to column 0. 3. set_rule_mask validates that Python-provided schema_size matches the compile-time value from the TensorMaskedJoin RIR node.

…check - test_learnable_head_unbound_variable_fails: rejects head var not in body - test_learnable_head_constant_fails: rejects constant in learnable head - test_ilp_schema_size_mismatch_rejected: validates set_rule_mask N check - test_ilp_projected_credit_path: verifies per-fact credit uses projection

Design fixes: - #6: candidate_set_hash → candidate_map_hash in persistence section - #7: valid_candidates() accepts allow_recursive param (maps to TrainConfig) Impl plan rewrite fixes: - #1: learnable syntax corrected to learnable(W_name) :: head :- body - #2: IlpProgramFactory.compile() uses static method with correct args - #3: valid_candidates() uses compiled_schema_size + rel_index, not registry - #4: Return type is list[dict] (PyO3 HashMap), consistent with Rust impl - #5: Alpha uses dense N³ mask; factorized scoring deferred to RC - #8: Robustness tests include behavioral all-distractors scenario - #9: All GPU tests use importorskip + cuda.is_available() skip pattern - #10: Template pruning test uses actual relation names, not prefix heuristic Also: mask names match showcase (W_reach, W_gp, W_col, W_p2), Stage 2 positives match actual showcase data, explicit alpha/deferred scope section.

Add a new CUDA kernel that fills COO arrays from a device-side mask + prefix-sum, reading its write offset from a device offset array. This eliminates the mask D2H transfer (Transfer #1) by keeping COO assembly fully on the GPU. - kernels/ilp.cu: add ilp_coo_fill_from_mask kernel - provider.rs: register kernel constant, add ilp_coo_fill_from_mask_launch() - xlog-cuda-tests: add 3 tests (basic, empty, all-zeros mask)

Closes v0.6.0 release blocker #1: the recorded launch discipline now has a public certification gate (`xlog-cuda-tests/tests/ certification_suite`) runnable against the production runtime stack. # Changes xlog-cuda-tests harness (`src/harness/provider.rs`): * `TestRuntimeBackend` enum (Legacy / DeviceRuntime) selectable via `XLOG_USE_DEVICE_RUNTIME` env var (cached per-process via `OnceLock`). Default stays Legacy so existing 206/206 cert evidence is unperturbed. * `TestContext::with_budget` builds the production decorator stack (`AsyncCudaResource → LoggingResource → GlobalDeviceBudget → XlogDeviceRuntime`) when DeviceRuntime is selected, and uses `GpuMemoryManager::with_runtime` + `CudaKernelProvider::with_runtime` so the env-gated dispatchers in `provider::sort` / `filter_by_mask` / `hash_join_v2` / etc. route operator calls through the recorded path when `XLOG_USE_RECORDED_*` is also set. * `TestContext::uses_device_runtime()` for diagnostics; held `Arc<XlogDeviceRuntime>` so the stream pool outlives the context. * `TestContext::reap_pending()` — drains pending async frees on the runtime allocator so the cert suite can release `GlobalDeviceBudget` reservations between categories. No-op on Legacy. xlog-cuda-tests cert suite (`tests/certification_suite.rs`): * Header now prints "Allocator backend" line plus the active `XLOG_USE_RECORDED_*` env flags, so the report makes the runtime / dispatch surface unambiguous. * Calls `ctx.reap_pending()` between every category so a long sequence of small allocate-then-drop tests does not pile up pending frees against the budget. xlog-cuda budget (`src/device_runtime/budget.rs`): * `GlobalDeviceBudget::allocate` now retries-after-reap on transient over-budget conditions: if the first reservation attempt fails AND the request fits the configured limit, drain pending frees once and retry. Fixes tight allocate-then-drop loops (the cert hardware sustained tests; recursive Datalog inner loops without explicit reap) that exhausted the reservation pool even when the GPU had plenty of free memory. * Genuinely oversized requests (`bytes > self.limit`) short-circuit with `OutOfBudget` before touching the inner stack — preserves the cheap-rejection path and keeps the `budget_rejects_over_limit_without_calling_inner` test green. # Validation Cert legacy: $ cargo test -p xlog-cuda-tests --test certification_suite --release → 206/206 PASS, 21s. Cert runtime + recorded-ops: $ XLOG_USE_DEVICE_RUNTIME=1 XLOG_USE_RECORDED_OPS=1 \ cargo test -p xlog-cuda-tests --test certification_suite --release → 206/206 PASS, 16s. The header confirms: Allocator backend: device-runtime (AsyncCudaResource → LoggingResource → GlobalDeviceBudget) Recorded-op dispatch: all Stream-safety regressions still clean: * cargo test -p xlog-cuda --release --test test_mt_sort_hj_alloc_ordering -- --test-threads=1 → 1024/1024 + 1024/1024 ✓ * XLOG_USE_RECORDED_OPS=1 XLOG_USE_DEVICE_RUNTIME=1 cargo test -p xlog-integration --test real_world_tests --release -- --test-threads=8 ×50 → 50/50 ✓ * cargo test --workspace --tests --exclude pyxlog --release -- --test-threads=1 → 141 result lines, 0 failures ✓

Closes v0.6.0 release blocker #3. # New files * docs/architecture/device-runtime.md — runtime stack (AsyncCudaResource → LoggingResource → GlobalDeviceBudget → XlogDeviceRuntime + StreamPool), the access-aware prepare/finish API, alloc-ready event semantics, GlobalDeviceBudget reservation + retry-after-reap, singleton (try_get) vs composed (with_resource) construction modes, env-gated dispatch matrix (XLOG_USE_RECORDED_FILTERS / SORT / DEDUP / GROUPBY / HASH_JOIN / OPS, plus XLOG_USE_DEVICE_RUNTIME on the integration / cert fixtures), and the supported certification modes (legacy 206/206 + runtime+recorded 206/206). Closes with a pointer to the documented A3 pre-existing concurrency residual. * docs/architecture/recorded-launch-migration.md — operator-author checklist for LaunchRecorder. API one-pager, the Access matrix (Read/Write/ReadWrite × what preflight waits on / what finish records to), helper- internal-scratch pattern via prepare_first_use / finish_first_use, host scalar reads + cu_stream.synchronize fence, external DLPack/Arrow handling (strict reject /permissive skip), and an explicit anti-pattern section covering: write_post_preflight_fresh removal, recording after preflight, using the singleton in production, long-term DeviceBlock retention, allocating helper scratch on launch_stream. Ends with the four-gate validation command sequence for migrating an operator. # ARCHITECTURE.md update Added a "v0.6 Device Runtime + Recorded Launch Discipline" subsection inside Memory Management, linking both new docs. No broader rewrite — surgical scope as directed. # ROADMAP.md update Marked the two v0.6.0 Documentation boxes complete, with links to the new docs. Updated the v0.6.0 Release Blockers Remaining summary: blocker #3 closed; remaining blocker #4 is the host-mask compact / ILP / ILP-exact recorded-migration scoping decision. # v0.6.0 status snapshot after this commit * Blocker #1 (formal cert harness) — DONE (3361785). * Blocker #2 (A3/A4 stress) — DONE (27ec3bd + a55fb11 re-scope: A4 fork-isolated PASS; A3 thread-of-N drift confirmed pre-existing against legacy default → v0.7.0). * Blocker #3 (docs) — DONE (this commit). * Blocker #4 (host-mask + ILP scoping) — pending. No code changes.

Closes W1.1 deliverable from the v0.6.5 closure board. ROADMAP.md changes: * Items 1, 4, 5, 8 marked [x] DONE with slice provenance (slices 1, 2, 4). * New "v0.6.5 Status" subsection: 4/22 DONE, 18/22 OPEN, 3 internal commitments OPEN. v0.6.5 is NOT releasable until the closure board reaches zero OPEN. * Pointer to docs/v065-closure-board.md as the authoritative tracker. docs/v065-closure-board.md (new): * 21 items enumerated (18 ROADMAP + 3 internal). * Process rules locked. Key rules: - Process rule #1: items only move to DONE with explicit user approval in the thread; the agent does NOT self-mark DONE. - Process rule #5: no `v0.6.6` references in any new file/comment/plan/evidence/commit until the board hits 0 OPEN. - Process rule #6: push/tag gated on board emptiness + explicit user say-so. - Process rule #7: BLOCKED is a real state with explicit blocker IDs. * Wave structure (1–7) follows the user-enforced order: process → foundation → kernel → runtime → cert → docs → release. * W2.5 (default flip skew → cardinality): BLOCKED until foundation + kernel + runtime + cert evidence (W2.1, W2.2, W2.3, W2.4, W3.2, W4.1, W5.1, W5.2). Default cannot flip without W5.2 bench evidence. * W2.6 (selectivity+heat into variable ordering): BLOCKED on W2.1 + W2.4. Scheduled last within Wave 2. * W2.2 (selectivity_pass) acceptance strengthened: requires same rule + two stats snapshots → two different chosen orders + identical row sets. Deterministic canonicalization that ignores stats does NOT pass. * W3.2 (general-arity template) acceptance strengthened: requires k=5 AND k=6 from one template; k=6 cert MUST pass without adding new `.cu` source for k=6. * W3.3 (heavy-row scheduling) acceptance gets numeric threshold: ≥ 2.0× speedup on superhub fixture; row-for-row deterministic; no regression on uniform fixture. * W3.4–W3.6 also have numeric thresholds (≥1.3×, ≥1.5×, ≥1.3× respectively) plus regression-floor requirements. No code change. No push. No tag.

…tch (W2.4) Closes board item W2.4 only. Successful triangle and 4-cycle WCOJ dispatches now wire observed selectivity back into `xlog_stats::StatsManager` via `record_join_result`. The slice 5 `CardinalityAwareCostModel` already consumes stats via `estimate_join_cardinality`; W2.4 closes the loop by writing them back so future dispatch decisions consult observed selectivity, not just default. Mechanism: * Two new `pub(super)` helpers on `Executor`: - `wcoj_output_rows(buf) -> Option<u64>` widens `CudaBuffer::cached_row_count()` (`Option<u32>`) and never invents `Some(0)` from `None`. Unknown row count stays unknown. - `record_wcoj_feedback(slot_rels, output_rows)` records on the inner pair `(slot_rels[0], slot_rels[1])` with keys `vec![1]/vec![0]` — the same pair the cardinality model reads via `estimate_join_cardinality` for `binary_est`. Early-returns on: - `output_rows == None` (unknown row count must not become a 0 selectivity record), - any of `slot_rels[0..2]` has missing or zero cardinality (`populated_cards` analog from slice 5), - `slot_rels.len() < 2` (defensive). * Triangle and 4-cycle success arms wire `record_wcoj_feedback` BEFORE the counter increment. Single line per call site; helper handles the math. * `record_join_result` takes owned `Vec<usize>` for the key columns (signature predates this slice); helper passes `vec![1] / vec![0]`. Recording semantics: * Triangle / 4-cycle output is a strict subset of the inner-join intermediate. Recorded selectivity is therefore an UPPER BOUND on the true binary selectivity — the correct conservative direction for the cost model. * Observed-empty output (`Some(0)`) is recorded; EMA tightens future estimates toward zero, making WCOJ less likely on the same inputs (the kernel produced nothing). * Unknown output (`None` from cache) is NOT recorded. Cert: `crates/xlog-integration/tests/test_wcoj_record_join_result_feedback.rs` * `triangle_dispatch_records_join_result_into_stats_manager` — pre `get_join_selectivity == None` → post `Some(_)`; `binary_est_run1 != binary_est_run2`; row-set parity. * `cycle4_dispatch_records_join_result_into_stats_manager` — same three properties for 4-cycle. * `wcoj_dispatch_does_not_record_when_input_cards_missing` — force-mode dispatch (counter advances) but selectivity stays None because input cards weren't seeded. Verification: * 3/3 W2.4 cert tests pass. * 135/135 xlog-runtime, 507/507 xlog-cuda, 128/128 xlog-integration, CUDA cert suite pass — slice 1–5 bit- identical preserved. * cargo fmt --check clean. Closure board proposal: * Per process rule #1, this commit does NOT self-mark W2.4 DONE. User reviews this commit and explicitly approves "mark W2.4 DONE"; a separate follow-up commit applies the board OPEN → DONE transition (DONE: 0 → 1, OPEN: 18 → 17).

User explicitly approved "mark W2.4 DONE" in the thread after reviewing implementation commit f586ce3. Per process rule #1 (no item moves to DONE without explicit user approval), this follow-up commit applies the closure-board transition: * W2.4 status: OPEN → DONE * Status tally: DONE 0 → 1; OPEN 18 → 17 (BLOCKED 2, IN-PROGRESS 1 unchanged); total still 21 * "Completed" section: W2.4 entry with impl commit hash f586ce3 and acceptance-gate summary W2.4 acceptance evidence (verified by user): * record_wcoj_feedback skips unknown output counts: crates/xlog-runtime/src/executor/wcoj_dispatch.rs:513 * Skips missing/zero input cards, calls record_join_result with owned vec![1]/vec![0]: crates/xlog-runtime/src/executor/wcoj_dispatch.rs:552 * Triangle records before counter increment: crates/xlog-runtime/src/executor/wcoj_dispatch.rs:760 * 4-cycle records before counter increment: crates/xlog-runtime/src/executor/wcoj_dispatch.rs:1091 Verification on this commit: * cargo test -p xlog-integration --release --test test_wcoj_record_join_result_feedback: 3/3 * cargo test -p xlog-integration --release --test test_wcoj_cardinality_cost_model: 7/7 * cargo test -p xlog-runtime --lib --release wcoj_cost_model: 23/23 * cargo fmt --all -- --check: clean No code change. No push, no tag.

W2.2 step 5 — workspace gate evidence + closure proposal. All gates green: * cargo fmt --check: clean * xlog-runtime: 135/135 * xlog-cuda: 507/507 * xlog-logic: 512/512 (+9 from W2.2 alt-shape promoter tests + selectivity_pass reordering tests) * xlog-integration: 131/131 (+3 from W2.2 Part B + Part C) * xlog-cuda-tests cert suite: full pass Acceptance: * Part A — 8 compile-time selectivity_pass tests (3 triangle inner-pair choices verified by direct plan synthesis, + 2-snapshots-differ, + fallback-edge-case tolerant, + 3 pre-existing no-op preserves). * Part A' — 26 promoter-extension tests in promote.rs (3 new alt-shape: triangle X-shared, triangle Z-shared, 4-cycle alt grouping; emit canonical-order MultiWayJoin.inputs and shape-fixed slot_vars). * Part B — 1 integration test: same source compiled with two distinct stats snapshots produces identical row sets. * Part C — 2 integration tests (triangle + 4-cycle): canonical-case dispatch + row-set match. Reframed as regression-style cert because right-deep optimizer output is OUT of W2.2 scope; reordering itself is exercised end-to-end by Part A + Part A'. Limitations documented: * Right-deep optimizer output: deferred per plan. * 10% default-fallback in estimate_join_cardinality: pinned by tolerant unit test. * No-op detection uses Debug-string comparison (RirNode doesn't impl PartialEq). Closure board proposal: * Per process rule #1, this commit does NOT self-mark W2.2 DONE. User reviews this commit and explicitly approves "mark W2.2 DONE"; a separate follow-up commit applies the board OPEN → DONE transition (DONE: 1 → 2, OPEN: 17 → 16).

User explicitly approved "Approved to mark W2.2 DONE" in the thread after reviewing the restored gates + review patches. Per process rule #1, this follow-up commit applies the closure-board transition: * W2.2 status: OPEN → DONE * Status tally: DONE 1 → 2 (W2.4, W2.2); OPEN 17 → 16 (BLOCKED 2 + IN-PROGRESS 1 unchanged); total still 21. * "Completed" section: W2.2 entry with all 9 commits (plan + 5 implementation steps + amendment + review patches) and an acceptance summary. W2.2 acceptance evidence (verified by user): * cargo test -p xlog-logic --lib selectivity_pass_tests: 12/12, no warnings. * cargo test -p xlog-runtime --lib wcoj_dispatch: 30/30. * cargo test -p xlog-integration --test test_selectivity_pass_reordering: 6/6. * cargo fmt --all -- --check: clean. * git diff --check HEAD~1..HEAD: clean. Restored gates close the original plan's acceptance: * Triangle + 4-cycle compile-time reordering (Part A). * Triangle + 4-cycle Part B row-set parity. * Triangle + 4-cycle Part C force-WCOJ on non-default synthesized bodies (counter ≥ 1, row-set equality vs binary reference). No code change. No push, no tag.

… (W2.1 step 9) Closes-board-item: W2.1 (proposing OPEN → DONE; awaiting user approval per process rule #1) Per the W2.1 plan §step 9, this evidence README documents the acceptance gate, code-level changes, decisions/limitations, and process-rule compliance for W2.1. * 32 acceptance tests (Part A 10 + B 7 + C 7 + D 2 + E 2 + resolver 4) all pass. * Workspace gate: 1914/0 (vs 1886/0 pre-W2.1 = +28 W2.1 tests on top of resolver 4 + cost-model 12 + helper 11 already counted at the unit-test level). * CUDA cert suite: 1/1 PASS (full certification). * Slice 1-5 + W2.4 + W2.2 regression preserved bit-identically under the `CompilerConfig::default()` (Disabled) path. Closure proposal: with user review and explicit approval, a follow-up commit applies W2.1 OPEN → DONE on the closure board + a "Completed" section entry. W2.1 closure also unblocks W2.6 (`Blocked by` set drops to {W2.4} which is already DONE). This commit does NOT self-mark W2.1 DONE per process rule #1. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Closes-board-item: W2.1 (DONE) Per process rule #1, this commit applies the OPEN → DONE transition for W2.1 after the user explicitly approved DONE in thread. Scoped strictly to docs/v065-closure-board.md; the W2.1 implementation + evidence is in commits 0c176e6..f82f999 (13 commits enumerated in the closure-board "Completed" entry). Changes: * Status tally: DONE 2 → 3 (added W2.1); BLOCKED 2 → 1 (W2.6 unblocked). * W2.1 row: OPEN → DONE with the 13 implementation commits + this board-update commit listed in the cert column. * W2.5 row: `Blocked by` set narrows from W2.1, W2.2, W2.3, W2.4, W3.2, W4.1, W5.1, W5.2 to W2.3, W3.2, W4.1, W5.1, W5.2 (W2.1, W2.2, W2.4 are now DONE). * W2.6 row: BLOCKED → OPEN (both blockers W2.1 + W2.4 are DONE); `Blocked by` set cleared. * Completed section: W2.1 entry added, mirroring the evidence README's commit list verbatim. User-approved DONE in thread; this is the only commit in this scope (no implementation, no test, no evidence — board state only). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…nce (W2.3 step 9) Closes-board-item: W2.3 (proposing OPEN → DONE; awaiting user approval per process rule #1) Per the W2.3 plan §step 9, this evidence README documents the acceptance gate, code-level changes, decisions/limitations, and process-rule compliance for W2.3. Highlights: * 10 acceptance tests (Part A 3 + Part B 2 + Part C 4 + Part D 1) pass on real CUDA under `--features xlog-runtime/recursive-stats-trace`. * Workspace gate: 1914/0 (pre-W2.3) → 1914/0 (default features — W2.3 tests skipped per `required-features` semantics, production zero overhead) → 1924/0 (with feature on, +10 W2.3 tests). * CUDA cert suite: 1/1 PASS. * Slice-4 recursive WCOJ certs: 6/6 PASS unchanged. * fmt: clean. Closure proposal: with user review + explicit approval, a follow-up commit applies W2.3 OPEN → DONE on the closure board + W2.5's `Blocked by` narrows to `{W3.2, W4.1, W5.1, W5.2}`. Per process rule #1, this commit does NOT self-mark W2.3 DONE. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Closes-board-item: W2.3 (DONE) Per process rule #1, this commit applies the OPEN → DONE transition for W2.3 after the user explicitly approved DONE in thread. Scoped strictly to docs/v065-closure-board.md; the W2.3 implementation + evidence is in commits d10bb72..72988c6 (7 commits enumerated in the closure-board "Completed" entry). Changes: * Status tally: DONE 3 → 4 (added W2.3); OPEN 16 → 15. * W2.3 row: OPEN → DONE with the 7 implementation commits + this board-update commit listed in the cert column. * W2.5 row: `Blocked by` set narrows from {W2.3, W3.2, W4.1, W5.1, W5.2} to {W3.2, W4.1, W5.1, W5.2} (W2.3 is now DONE, joining W2.1, W2.2, W2.4 in the no-longer-blocking set). * Completed section: W2.3 entry added, mirroring the evidence README's commit list and acceptance-gate summary. User-approved DONE in thread after fresh CUDA verification on this host (NVIDIA RTX PRO 3000 Blackwell, driver 591.59): * cargo fmt --all -- --check: clean. * cargo test -p xlog-runtime --release --features recursive-stats-trace --test test_w23_recursive_stats -- --nocapture: 10/10 PASS, no skip output (real GPU path). * cargo test --workspace --release --tests --exclude pyxlog --features xlog-runtime/recursive-stats-trace: exit 0. * cargo test --workspace --release --tests --exclude pyxlog: exit 0. This is the only commit in this scope (no implementation, no test, no evidence — board state only). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Closes W3.1 only. New generic wcoj_layout_sort_*_recorded surface (4-byte and 8-byte width-class entry points) on top of existing sort_recorded + dedup_full_row_recorded primitives. Plan iterates six times to lock: D1 — New entry points; existing arity-2 helpers stay bit-identical. D2 — Full-row keys, internally derive 0..arity. D3 — Uniform width-class per call (4-byte = U32 + Symbol mixable; 8-byte = U64). Reject mixed 4-byte + 8-byte. D4 — No fast-path for arity ≥ 3. Out of scope for W3.1 with no closure credit; no future-item invention. D5 — Cert at arities {2, 3, 4, 5, 6, 7}; arity-7 sentinel proves no silent W3.2-shaped cap. D6 — Branch off main at 475774e; plan as branch commit #1. 9-step plan: audit → add U32 entry → add U64 entry → manifest re-export check → width-class validation certs (10 tests) → round-trip grid certs (3 shapes × 4 width-class fixtures × 6 arities = 72 tests with real SymbolTable IDs) → workspace gate (+82 symbolic delta) → evidence README → closure proposal (user-gated). Acceptance total: 82 tests. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…teration 4) Closes W3.2 only. C++/CUDA template kernel covering k=5 and k=6 from a single template implementation; k=6 wrappers are template calls only with no hand-written algorithm body. Locked direction (iteration 4): D1 — C++/CUDA template `<int K>`. k=6 = ABI wrapper + explicit instantiation; no hand-written body. D2 — Test-only `cpu_clique_reference<T, const K>` brute-force oracle. Stable-Rust signature with runtime length-assert. D3 — u32 + u64 + Symbol (Symbol gets its own cert at both k). D4 — Runtime integration required. Default-dispatch on shape match; silent fallback on dispatcher decline / kernel error. No force/kill/adaptive knobs. D5 — Tree-flatten + complete-K_k validation. Robust to left-deep / right-deep / bushy. Rejects filter wrappers, reversed atoms, recursive clique bodies. D6 — Lex `(i, j)` for `i < j` canonical edge order. D7 — 33 tests (6 provider + 4 runtime + 15 promoter + 8 two-tier source-audit). D8 — Plan as branch commit #1 of feat/w32-general-arity-wcoj-template. 14-step plan: audit → CUDA template + 8 ABI wrappers → manifest register → provider u32 → provider u64 → promoter → runtime dispatcher → provider cert × width-class (6) → runtime dispatch + fallback cert (4) → promoter shape cert (15 incl. negatives + k=7 sentinel) → k=6 source-audit two-tier (Tier 1 wrapper-body template-call-only × 4 + Tier 2 file-wide no-specialization / no-K-branch / no-helper-body / no-K-literal × 4) → workspace gate (compile/link budget hard stop) → evidence README → closure proposal (user-gated). Acceptance total: 33 tests, +33 workspace delta.

…extension Two blocking findings from user iteration-4 review of the W3.2 implementation: **Finding #1 — Tier-1 wrapper contract violated.** The plan locked at iteration 4 §345 requires each k=6 ABI wrapper body to contain **exactly one statement** that calls the shared template, with NO conditionals (no `if`/`switch`/ternary), NO loops. The implementation had 3-statement count wrappers and 5-statement materialize wrappers (thread-idx + bound check + template call); the audit cert had been weakened from 1-stmt to 3/5-stmt to match. Restructured `wcoj.cu` to introduce two NEW grid-level templates: template <int K_VAL, typename T> __device__ __forceinline__ void wcoj_clique_template_count_grid_t(...); template <int K_VAL, typename T> __device__ __forceinline__ void wcoj_clique_template_materialize_grid_t(...); Both absorb the thread-idx + bounds checks. Each ABI wrapper body is now EXACTLY ONE statement: a single template call into the grid-level template. No `if`, no `for`, no `?:` anywhere in the wrappers. Tier-1 cert updated: shared `assert_wrapper_is_single_template_call` helper enforces stmts == 1, contains `<grid_template>`<K, ...`>, and rejects every conditional + loop token. All 4 Tier-1 cells pass on the new tightened contract. Tier-2's `no_six_literal_in_template_body` audit list extends to cover the new grid-level templates. **Finding #2 — Recursive WCOJ helper extension reverted.** The plan iteration 4 §177 explicitly says the recursive WCOJ helper is NOT extended for clique-keyed dispatch in W3.2. The earlier implementation added `try_dispatch_wcoj_clique5_on_body` / `_clique6_on_body` calls into `execute_wcoj_or_fallback_node` in `recursive.rs:46-52`. Removed those entries. Recursive clique bodies are still correctly rejected by the promoter's `recursive_scan_count == 0` gate in `promote_multiway`, so they fall through to binary-join. The non-recursive SCC dispatch chain (in `execute_stratum_impl`) retains the clique dispatch entries — that's the only path W3.2 wires up. Verification: * cargo fmt --check --all: clean. * cargo build -p xlog-cuda --release: clean (compile-budget gate still passing with the grid-level templates). * W3.2 acceptance: 33/33 still PASS (8 source-audit + 6 provider + 15 promoter + 4 dispatch). * Workspace tests: 1990 PASS / 0 FAIL / 17 ignored. * CUDA cert suite: 1/1. Evidence README updated to reflect the corrected wrapper structure + non-recursive-only dispatcher integration.

…ngs) Iteration 5 was not approved as-is. User-blocking findings: F1: Line 106 said "The 12-step sequence below" while canonical plan has 16 steps (line 103). Direct contradiction within 4 lines. F2: Lines 6, 9, 423, 600 still presented the plan as iteration 4 in live header + plan-approval gate text. Since iteration 5 (commit 8b170a9) already shipped, the live text was stale. User offered two acceptable resolutions: bump live iteration label everywhere, or explicitly state that the current iteration is wording-only and canonical content remains iteration 4. Iteration 6 chooses the explicit-clarification path: Header (line 9): "Plan iteration: 4 (paper-grounded, post- audit)..." → "Plan iteration: 6 — wording-only cleanups over iterations 4 and 5; canonical D-table + Step plan + Acceptance Grid content remains iteration 4 (no design changes since iteration 4)." Header line 6: "iteration 4 is approved" → "iteration 6 is approved" Step plan intro (line 106): "12-step sequence" → "16-step sequence" Live Plan-Approval Gate (was line 423): renamed from "(iteration-4 canonical)" to "(current iteration)"; gate body bumped to "iteration 6 draft" with explicit "canonical content remains iteration 4" clarification. Iteration-4 Plan-Approval Gate inside the iteration-4 amendment log (was line 600): renamed to "(Iteration 4 — historical, superseded)" with explicit historical-context wording. Process rule #1 (line 42 → 54 after header edit): "no DONE marking under any iteration-4 outcome" → "no DONE marking under any plan iteration's outcome" (iteration-agnostic to avoid bump churn on every wording-cleanup commit). No content changes (no design, no D-table revisions, no Step structure, no Acceptance Grid content). Wording-only. Banned-token sweep clean. No "iteration 4 draft", no "12 steps", no "iteration-4 outcome", no "iteration-1 outcome" remain in live text. Plan-approval gate (iteration 6) active: agent does NOT advance to Step 5 (promoter gate removal) until user explicit approval.

User finding on iteration-5 commit 2db729a: the live plan still carried soft `>= 1` counter criteria for Cert A/B/E/F and the "either path" / "no kernel-launch crash; empty output via either path" loophole text for Cert G across multiple canonical sites (D7 row, Acceptance Grid, Step 6 + Step 7 + Step 10 prose). The executed certs landed via the Step 6 patch (c665bd0 — Cert A `>= 1` → `== 1`) and Step 10 patch (6f25377 — Cert G adds D7 route assertions per fresh-executor subcase) with stricter exact-equality discipline. Plan was stale relative to certs. Logged as **F-W43-13 (Major)** inside iteration 5. This is the same class as F-W43-7/8/9/10 (file-wide-concern drift) but applied to a contract tightening rather than a label bump. Patches (in-place, all live sites): D7 row (line 35): * #1 (Cert A): `>= 1` → `== 1`, adds `nested_loop_dispatch_count == 0`. * #2 (Cert B): `>= 1 or hash` → `nested_loop_dispatch_count == 1` (W4.2 fallback fired exactly once). * #5 (Cert D'): adds explicit `nested_loop_dispatch_count == 0` (the certs already assert this; just makes it canonical). * #6 (Cert E): `>= 1 + parity` → `== 1` + `nested_loop == 0` + parity. * #7 (Cert F): `>= 1` → `== 1` + `nested_loop == 0` + output count == 4000 + all 4000 tuples distinct. * #7' (Cert G): replaces "reflects the chosen short-circuit (either dispatched OR not-dispatched)" with explicit per- fresh-executor `sort_merge == 1 AND nested_loop == 0` proving the F-W43-4 contract end-to-end (sortedness probe short-circuits n<2 → Ok(true), dispatch admits, kernel empty fast path emits empty output). * Row label provenance: now `per F-W43-3 + F-W43-4 + F-W43-12 + F-W43-13`. Acceptance Grid (lines 225-232): * Cert A: `>= 1` → `== 1`. * Cert B: `>= 1` → `== 1`. * Cert E: `>= 1 + parity` → `== 1 + nested_loop == 0 + parity`. * Cert F: `>= 1 + output count == 4000` → `== 1 + nested_loop == 0 + output count == 4000 + all 4000 tuples distinct + parity`. * Cert G: "no kernel-launch crash; empty output via either path; row-set parity" → "both subcases (empty L + empty R) per fresh executor: sort_merge == 1 + nested_loop == 0 + empty output + parity vs hash + no kernel-launch crash". Row label updated to `per F-W43-4 + F-W43-13`. Step prose (lines 146, 159, 181-183): * Step 6 (Cert A): `>= 1` → `== 1` (with "per F-W43-13 exact- equality discipline" rationale). * Step 7 (Cert B): `>= 1` → `== 1` (with same rationale). * Step 10 (Certs E + F + G): all three certs' counter assertions rewritten to match the executed exact-equality contract; Cert G prose specifically expanded to describe the F-W43-13 D7 route assertion that closes the parity-only loophole. Iteration-5 Amendment Log extended with F-W43-13 row (line 328) + updated process observation (line 332) noting that all three findings (F-W43-11, F-W43-12, F-W43-13) are execution-discovered. F-W43-13 specifically extends the F-W43-7/8/9/10 file-wide- concern lesson: when a contract is tightened (not just labeled), the same grep-everywhere discipline applies — D7 grid + Acceptance Grid + prose Steps must all be inspected before the iteration is declared closed. Line 3 (Plan iteration metadata) and Plan-Approval Gate paragraph (line 259) updated to reference all three findings (was: two; now: three). No code changes. No D-table design changes. No Step plan structural changes. The +8 Acceptance Grid pass-count delta is unchanged (Certs A, B, C, D, D', E, F, G still 8 cells). Verification: - Live plan grep for `>= 1` / `>=1` / "either path" returns hits ONLY inside the Iteration-5 Amendment Log (legitimate historical references describing the drift being patched). - All cert-contract claims in the live plan now match the committed test bodies at `crates/xlog-integration/tests/test_w43_sort_merge_dispatch.rs` (Cert A line 348, Cert B line 482, Cert E line 911, Cert F line 1063, Cert G G1 line 1277, Cert G G2 line 1344). Refs: docs/plans/2026-05-10-w43-sort-merge-join-plan.md (live iteration 5, F-W43-13); commits c665bd0 (Step 6 patch — Cert A exact-equality), 6f25377 (Step 10 patch — Cert G route assertions).

…itted' claim The README pinned verifier revision 0fbf449 as 'the exact revision that produced the committed MARITIME_VERIFY.json real-data report', but the report was never committed in any revision — it existed only on the runner's machine while carrying the sole backing for the 1.0 alignment fractions and the episode-boundary proof (deep-review finding #1, HIGH). Ship the report byte-exact at docs/experiments/maritime/results/verification/MARITIME_VERIFY.json (md5 of the committed bytes: c17b82672bc5144a61eeddf66b9ca21c, equal to the runner original), add a .gitattributes -text rule for docs/experiments/maritime/results/** so shipped artifacts are never EOL-normalized (the class behind finding #3), and add an explicit provenance-correction note to the Results section instead of silently rewording the claim.

…bytes The README pinned md5 1d3b7fcc... as 'byte-exact', but the committed artifact hashes ac650dc5... — the pin was computed on the Windows runner's CRLF original before git normalized line endings to LF at commit; content is identical modulo EOL (deep-review finding #3, MEDIUM, diagnosed by reconstruction). Make the committed-bytes hash the pin, keep the old value in a one-sentence provenance note, and rely on the .gitattributes -text rule (added with finding #1) to kill the failure class for future artifacts.

levi770 added 17 commits February 25, 2026 14:45

feat(ilp): add learnable_rule grammar production

6df0165

feat(ilp): add LearnableRule AST type and Program field

3e6f8e1

feat(ilp): add learnable rule edges to dependency graph

877ea64

feat(ilp): add TensorMaskedJoin RirNode variant

f1ec5bc

feat(ilp): add TensorMaskedJoin arms in optimizer

e274365

feat(ilp): add extract_nonzero_indices CUDA kernel and provider wrapper

69ada5b

feat(ilp): implement execute_tensor_masked_join with hash-join dispatch

15b9b2a

test(ilp): add CUDA kernel extraction tests

0da335d

feat(ilp): add CompiledIlpProgram PyO3 bindings for ILP

da58694

docs(ilp): add tensorized ILP RFC and implementation plan

d8f950a

- RFC v4.4 with 37 resolved design decisions - 15-task implementation plan (all tasks completed)

Copilot AI review requested due to automatic review settings February 25, 2026 15:46

Copilot started reviewing on behalf of levi770 February 25, 2026 15:47 View session

Copilot AI reviewed Feb 25, 2026

View reviewed changes

Comment thread python/tests/test_ilp.py

Comment thread crates/xlog-runtime/src/executor.rs

Comment thread python/tests/test_ilp.py Outdated

Comment thread crates/xlog-logic/src/grammar.pest

Comment thread crates/xlog-runtime/src/executor.rs

levi770 added 2 commits February 25, 2026 16:58

fix(ilp): keep simple torch.cuda skip gate for ILP tests

7da2d6c

The reviewer flagged cudarc init failures — this was an env issue (missing LD_LIBRARY_PATH), not a test gate issue. Keep the standard torch.cuda.is_available() check consistent with all other test files.

levi770 force-pushed the feat/tensorized-ilp branch from 2aa483f to 7da2d6c Compare February 25, 2026 16:29

levi770 added 2 commits February 25, 2026 17:55

levi770 merged commit 9d8d4f6 into main Feb 25, 2026
1 of 6 checks passed

levi770 deleted the feat/tensorized-ilp branch March 5, 2026 17:49

This was referenced Jul 16, 2026

Engine-mode follow-ups: witness-level mask schema, registration-seam delta (arity/sorts/artifact hashes), frozen entry point #155

Closed

feat(ilp): witness-level mask/abstain channel per the #155 field contract #157

Merged

This was referenced Aug 17, 2026

Constraint violation under epistemic reduction names the wrong authored constraint #242

Closed

Empty-database corpus queries cost ~0.5 ms per compiled statement: per-rule seeding scans and per-predicate multiway unions dominate at zero output rows #243

Closed

Navigation Menu

Uh oh!

feat(ilp): Tensorized Differentiable ILP engine - #1

feat(ilp): Tensorized Differentiable ILP engine#1
levi770 merged 21 commits into
mainfrom
feat/tensorized-ilp

levi770 commented Feb 25, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

levi770 commented Feb 25, 2026

Summary

Validation

Key design decisions (from RFC v4.4, 37 RDs)

Test plan

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants