[AdaWorldAPI]

Docs, two lab examples in the workspace-excluded drf-focus-probe crate, and test-only falsifiers (soa-view-probe, cognitive-shader-driver/tests, lance-graph-planner/tests).

• No runtime, ABI, planner, writer, WAL or ownership change. No production source file is touched.
• No new opcode, selection vector, store, cache, generation or engine.
• The scatter survival condition (ir.rs:329-337) stays in force.
• P2 is complete; P3–P5 remain unauthorized.

Plan: .claude/plans/dr256-where-capstone-v1.md.

Sections

• P0 census, P1 lab: WHERE, COUNT and ANY already exist in Quack / mask-risc. Occupancy is the one missing statistic.
• Amendment A: DR64³ gap inventory, kept as a working model. DR Claude/review lance graph architecture i6 t kf #3's physical contract is still an open admission question (NFR-OP-2).
• Amendment B, P2 (examples/p2_quack_where.rs): the real Quack path, every arm oracle-checked.
  • Bind and lower ≈ 200 ns; building R ≈ 20 µs.
  • Reusing a kept R costs 0.05–0.60 of recomputing it per property.
  • Existing execution skips dead words only in gated predicates. A block schedule pays at sparse selections (0.02–0.39) and not near full occupancy.
  • Stale codebook, scope, selection and predicate-dependent property changes all run silently stale through Quack.
• Future compiler compatibility: cites D-DRMC-0 and the native-first plans instead of restating them.
• § D, evidence reconciliation: binding store planned/unbuilt; Quack numeric binding and RelAlg let reuse implemented; witnessed DR populations, typed DR method binding and compiled recipes implemented in lab; source-attested production integration missing. Spine linked with source (U2 (D-RU-2): let-bound planes over the contract set algebra #1649 … dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8) #1740). The predicate-dependent falsifier: a reused R2 keeps 1,032 rows against 31 fresh, silently.
• Part E, D-NFR-1 ownership correction and amendment:
  • Guarantees kept apart: structural (borrow, compile time), nominal (mailbox_owner, cast(on_behalf); not authorization), persisted, now split into horizon (QueryReference::at: row admission only, no dataset or owner field) and physical snapshot (checkout_version on one dataset: a separate, unrecorded step).
  • Borrow-scoped execution needs no frame, lease or guard; the next possible lab step is a thin zero-copy adapter over real owner lanes.
  • Escaped reuse must recompute or refuse until a contract establishes source/owner identity, a complete mutation witness, focus and coordinates, scope and authorization, codebook interpretation, and multi-source snapshot consistency. One owner generation may become a component of that, after every mutation path is closed; it is not the contract.
  • Mutation inventory: every MailboxSoA column and both stamps are pub fields; direct writes, the 12 setters, same-cycle write_row, reset_row, apply_edges, consume_firing, style and phase methods move no stamp. A method-local generation would miss direct writes; the fix options (encapsulation, owner-scoped capability, snapshot publication) are listed, not chosen.
  • Falsifiers (each disable-verified, red only in its own test; one non-binding disable recorded): raw setter; same-cycle write_row; later-cycle twin; direct public-field write; reset_row + same-cycle write restoring both stamps over new data; two owners with equal stamps and different answers; one pinned QueryReference admitting different rows from two sources; an exhaustive destructure proving the reference has no source field; the packet cycle as caller stamp.
  • Status: PROVEN borrow exclusion; PROVEN stamps cannot validate escaped masks; PROVEN no Quack ↔ MailboxSoA integration. NOT YET PROVEN that one generation suffices. OPEN mutation-path ownership, physical snapshot attestation, and NFR-OP-1 (the escaped-reuse authority contract).
• Ready if separately approved: the in-borrow D-NFR-1 lab adapter; a Quack Agg route to the existing power-sum terminals; a P3 gate-aware fold measurement.
• Blocked: the escaped-reuse authority contract; the production binding store; cross-frame named intermediates; lab(D-DR256-OD): on-demand global mask, u16 scatter, bounded reuse, L1 interference #1791 scattered-mask reuse; S-INGRESS; the proof reference (CC1); a proof checker; the DR³ physical contract; witness unification.

🤖 Generated with Claude Code

https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: a4592e55-ef6e-4e98-9058-cb12c03f4755

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Warning

Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-26T17:50:05.250711Z	62f6137	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.