From 906b6551cdd7b3363d762bfb1cf97595641d2bc5 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 5 Nov 2026 21:38:58 +0100 Subject: [PATCH 1/5] docs(plan): P6 holographic Bagop design --- .../gridcraft-bagop-falsifier-program-v1.md | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 docs/plans/gridcraft-bagop-falsifier-program-v1.md diff --git a/docs/plans/gridcraft-bagop-falsifier-program-v1.md b/docs/plans/gridcraft-bagop-falsifier-program-v1.md new file mode 100644 index 0000000000..69c8c23466 --- /dev/null +++ b/docs/plans/gridcraft-bagop-falsifier-program-v1.md @@ -0,0 +1,87 @@ +# GRIDCRAFT-BAGOP-FALSIFIER-1: Cross-repository proof and admission program + +**Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P5. + +**Research question:** Can the exact same witnessed holographic Bag answer Excel XVERWEIS, a PSCustomObject-shaped named property and direct Bagop folding without materializing one row/cell/object per logical identity, without fabricating a second authority, and while preserving Excel semantics and OGAR scopes? + +## Explicit non-goals + +No production code, dependency update, merge, full GridCraft rewrite, new SIMD engine, new Bagop interpreter, custom Gather, independent identity dictionary, or claim that file decoding/serialization costs zero bytes. Do not promote a lab to a production admission. + +## Fixture F0: independently specified + +Create a *future implementation* fixture with exactly DR256 × 256 tiles (65,536 local positions), deliberately permuted local order and at least two distinct OGAR-granted tenant populations whose external labels collide. Each population includes duplicate lookup keys, unique keys, one not-found key, multiple typed columns, reversed and sorted presentations, and invalid/foreign source identifiers. + +The independent oracle carries canonical source-qualified identities, Bag occurrence numbers, typed values and a separate **logical row order**. It does **not** share DR local positions, Bagop execution plans, a candidate index or the production codebook implementation. + +Required values: zero, negative number, exact decimal text 9007199254740993, null/absent, blank, empty text, explicit missing, formula anchor and spill cached child, error state, Unicode text, and a changed value between versions. Do not pretend all these states are equivalent or always native to one codec. + +## Paths under test + +A. Direct source-qualified Bagop fold via admitted Quack/RelAlg/mask-risc/ndarray. + +B. GridCraft XVERWEIS expression over mounted virtual BagSheet, using the same Bagop contract. Cover exact first and last; unadmitted wildcard/approximate/binary must give a typed refusal. + +C. PSCustomObject-shaped named property projection over the same Bag, with no nested object tree in execution. + +D. Independent scalar Excel-style oracle for exact matching and order, with distinct Bag multiplicity oracle. Optional real Excel/XLSX terminal roundtrip must be reported as external compatibility evidence, not as an internal oracle. + +## Acceptance and disable matrix + +| Gate | Positive oracle | Disable/falsifier | +|---|---|---| +| G0 semantic authority | Delete every derived index then rebuild: same IDs, multiplicities and results | Substitute workbook-minted ordinal: fail | +| G1 exact first/last | Excel-style independent source order matches | Remove order witness: red | +| G2 duplicates | Bag fold counts all occurrences, XVERWEIS chooses specified one | Implicit DISTINCT: red | +| G3 field binding | DT64 property name binds same meaning after input column reorder | Mutable basis without witness: red | +| G4 epistemic states | Blank, EmptyText, Absent, Missing, Formula/Spilled and error distinct as admitted | Conflate two states: red | +| G5 precision | Exact decimal string roundtrips or refuses lossless conversion | f64 conversion: red | +| G6 frame correctness | Permuted tile/frame refused or correctly rebound | Remove digest: red | +| G7 tenant isolation | Equal labels in two scopes do not alias | Bypass scope check: red | +| G8 value revision | Value-bearing cached method refuses stale revision; map COUNT valid | Remove value witness: red | +| G9 amortization | 256 repeated methods after one bind: zero additional global→local lookups | Re-route each method: counter red | +| G10 no row hydration | 65,536 Bag rows, zero persistent GridCraft Cell/PSCustomObject instances per Bag row | Force per-row Cell creation: allocation test red | +| G11 viewport | 30×12 window memory bounded by visible rows/cells and descriptors | Eager entire 65K×24 render: red | +| G12 dynamic arrays | Visible spill children have correct anchor, shape and order | Collapse spilled cached child: red | +| G13 admission law | Unadmitted Gather/composition/mask reuse refuses | Permit value-derived cross-table address: red | +| G14 backend parity | Scalar, AVX2, AVX512, NEON, WASM where runnable | Tail/stride corruption: red | +| G15 egress scope | Export only authorized values; no cross-scope cache | Reuse view after permission revocation: red | + +A negative control must be run in a disposable test mutation and restored. A red disable proves the test can catch the violation; it is not evidence of production readiness. + +## Performance experimental matrix + +Record CPU model, ISA, Rust version, build flags, source revision, fixture seed, warmup, repetitions, distribution and resident/peak bytes. Separate: + +1. XLSX parse/decompression and eTag/snapshot validation. +2. Canonical source bind and DR global→local preparation (map count). +3. One exact-match fold. +4. 256 warm repeated folds under the same prepared descriptor. +5. 30×12 viewport presentation and all-cell scrolling. +6. Cold text hydration and exact numeric conversion. +7. Terminal CSV/XLSX/PowerShell serialization and total bytes. +8. Cache invalidation/rebind after scope, frame or value change. + +Compare to GridCraft CellStore and report-rs #33 **only where work and witness obligations match**. The ~0.39ns warmed lookup is not an end-to-end XVERWEIS comparator. Record p50/p95 and allocation deltas; do not cherry-pick backend/shape. + +## PR/program gate order + +| Phase | Prerequisite | Pass requirement | +|---|---|---| +| R0 | P0 owner decision | One-authority law with no hidden contradictory DR interpretation | +| R1 | P1, P2 owners | Exact-match ordered fold admitted or explicit STOP | +| R2 | P3, P4 review | GridCraft virtual presentation and object façade bounds | +| R3 | P5 convergence | report-rs does not create a second source | +| R4 | DRISA M1/M2, OGAR | Frame, route and scope attestations | +| R5 | D4/S-INGRESS if writing requested | Canonical writer admission; otherwise read-only | +| R6 | This falsifier plan | Independent oracle and negative controls defined **before** code | + +**Decision log 2026-11-05:** proposed test program, not proof. **Next implementation PR:** one read-only lab vertical slice with fixture and independent scalar oracle, not production. Stop if the required Bagop operator or layout/scope witness is not admitted. + +## References / companion plans + +- [P0/P2 source repository](https://github.com/AdaWorldAPI/lance-graph), [DRISA lab #1955](https://github.com/AdaWorldAPI/lance-graph/pull/1955) +- [P1 ndarray FACET STRIDE](https://github.com/AdaWorldAPI/ndarray/blob/master/src/simd_stride.rs) +- [P3 GridCraft CellStore](https://github.com/AdaWorldAPI/gridcraft/blob/main/crates/model/src/store.rs) +- [P4 Java membrane](https://github.com/AdaWorldAPI/lance-graph-java/blob/main/java/README.md) +- [P5 report-rs PR #33](https://github.com/AdaWorldAPI/report-rs/pull/33) From b3a9e0b72708f2c2a4b8bf34a5fff76585612d02 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 5 Nov 2026 21:45:44 +0100 Subject: [PATCH 2/5] docs(plan): narrow LGJ to non-materializing fold precedent only --- docs/plans/gridcraft-bagop-falsifier-program-v1.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/plans/gridcraft-bagop-falsifier-program-v1.md b/docs/plans/gridcraft-bagop-falsifier-program-v1.md index 69c8c23466..1c7eae0316 100644 --- a/docs/plans/gridcraft-bagop-falsifier-program-v1.md +++ b/docs/plans/gridcraft-bagop-falsifier-program-v1.md @@ -1,6 +1,6 @@ # GRIDCRAFT-BAGOP-FALSIFIER-1: Cross-repository proof and admission program -**Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P5. +**Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P3 and P5. **P4 (lance-graph-java) is a non-blocking historical/empirical precedent solely for folding without per-row materialization, not an implementation, runtime or semantic dependency.** **Research question:** Can the exact same witnessed holographic Bag answer Excel XVERWEIS, a PSCustomObject-shaped named property and direct Bagop folding without materializing one row/cell/object per logical identity, without fabricating a second authority, and while preserving Excel semantics and OGAR scopes? @@ -70,7 +70,7 @@ Compare to GridCraft CellStore and report-rs #33 **only where work and witness o |---|---|---| | R0 | P0 owner decision | One-authority law with no hidden contradictory DR interpretation | | R1 | P1, P2 owners | Exact-match ordered fold admitted or explicit STOP | -| R2 | P3, P4 review | GridCraft virtual presentation and object façade bounds | +| R2 | P3 review | GridCraft virtual presentation and object-materialization bounds; P4 reference optional | | R3 | P5 convergence | report-rs does not create a second source | | R4 | DRISA M1/M2, OGAR | Frame, route and scope attestations | | R5 | D4/S-INGRESS if writing requested | Canonical writer admission; otherwise read-only | @@ -83,5 +83,5 @@ Compare to GridCraft CellStore and report-rs #33 **only where work and witness o - [P0/P2 source repository](https://github.com/AdaWorldAPI/lance-graph), [DRISA lab #1955](https://github.com/AdaWorldAPI/lance-graph/pull/1955) - [P1 ndarray FACET STRIDE](https://github.com/AdaWorldAPI/ndarray/blob/master/src/simd_stride.rs) - [P3 GridCraft CellStore](https://github.com/AdaWorldAPI/gridcraft/blob/main/crates/model/src/store.rs) -- [P4 Java membrane](https://github.com/AdaWorldAPI/lance-graph-java/blob/main/java/README.md) +- [P4 non-blocking evidence for non-materializing native folds](https://github.com/AdaWorldAPI/lance-graph-java/blob/main/java/README.md) - [P5 report-rs PR #33](https://github.com/AdaWorldAPI/report-rs/pull/33) From df45abb0719f80035e9e9e5ebf9ff8dd90f3be8d Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 5 Nov 2026 21:55:23 +0100 Subject: [PATCH 3/5] docs(plan): add F### formula polyfill and Codegraph non-dilution contract --- .../plans/gridcraft-bagop-falsifier-program-v1.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/docs/plans/gridcraft-bagop-falsifier-program-v1.md b/docs/plans/gridcraft-bagop-falsifier-program-v1.md index 1c7eae0316..22f401dcdd 100644 --- a/docs/plans/gridcraft-bagop-falsifier-program-v1.md +++ b/docs/plans/gridcraft-bagop-falsifier-program-v1.md @@ -1,6 +1,6 @@ # GRIDCRAFT-BAGOP-FALSIFIER-1: Cross-repository proof and admission program -**Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P3 and P5. **P4 (lance-graph-java) is a non-blocking historical/empirical precedent solely for folding without per-row materialization, not an implementation, runtime or semantic dependency.** +**Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P3, P5 and [P7 F### formula polyfills #3](https://github.com/AdaWorldAPI/gridcraft/pull/3). **P4 (lance-graph-java) is a non-blocking historical/empirical precedent solely for folding without per-row materialization, not an implementation, runtime or semantic dependency.** **Research question:** Can the exact same witnessed holographic Bag answer Excel XVERWEIS, a PSCustomObject-shaped named property and direct Bagop folding without materializing one row/cell/object per logical identity, without fabricating a second authority, and while preserving Excel semantics and OGAR scopes? @@ -85,3 +85,16 @@ Compare to GridCraft CellStore and report-rs #33 **only where work and witness o - [P3 GridCraft CellStore](https://github.com/AdaWorldAPI/gridcraft/blob/main/crates/model/src/store.rs) - [P4 non-blocking evidence for non-materializing native folds](https://github.com/AdaWorldAPI/lance-graph-java/blob/main/java/README.md) - [P5 report-rs PR #33](https://github.com/AdaWorldAPI/report-rs/pull/33) + +## G16–G19: F### formula method and Codegraph non-dilution gates (2026-11-05) + +These gates extend G0–G15 and depend on [P7 #3](https://github.com/AdaWorldAPI/gridcraft/pull/3). The F### numbering/MethodRef registry is **not verified** and must be discovered in its canonical owner before an implementation can claim parity. + +| Gate | Positive independent oracle | Negative control | +|---|---|---| +| G16 method identity | Identical parsed formula+scope+registry version resolves to the same canonical F###/MethodRef; change in source location affects provenance but not method semantics | Locally mint an ordinal or remove registry version check: red | +| G17 no materializing formula fallback | SUM/COUNT and admitted XVERWEIS over 65,536 identities perform no per-row `Vec` or `Cell` hydration in canonical execution | Route to `Host::range_values` collecting entire population: allocation test red | +| G18 Kythe/Codegraph boundary | Verified source/def-use/call provenance is derived, read-only and keyed to actual owner contract, not a second formula evaluator | Insert invented formula identity in Codegraph or mutate it as value authority: contract test red | +| G19 R2IL integrity | Existing R2IL machine opcode vocabulary/semantics remain unchanged while formula method calls are separately traced | Alias an Excel formula to R2IL IntAdd or mint a competing opcode: vocabulary parity red | + +Additional semantics: lazy IF/LET/LAMBDA, volatile/effectful formulas, exact decimals, formula sources/spans and spilled arrays must have separate independent oracles or remain NOT ADMITTED. **Do not assert every formula is a reduction.** Formulas require typed F### method contracts; some lower to elementwise, control, reference or effect semantics. A source-level formula→method→operator mapping is provenance, not a new storage substrate. From 48186509c45e3d7723af5cbbb9d749a5aaa2b94b Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 5 Nov 2026 22:13:06 +0100 Subject: [PATCH 4/5] docs(plan): prioritize SAP-shaped Guid128 tile POC over spreadsheet/lakehouse expansion --- docs/plans/gridcraft-bagop-falsifier-program-v1.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/docs/plans/gridcraft-bagop-falsifier-program-v1.md b/docs/plans/gridcraft-bagop-falsifier-program-v1.md index 22f401dcdd..66df23e449 100644 --- a/docs/plans/gridcraft-bagop-falsifier-program-v1.md +++ b/docs/plans/gridcraft-bagop-falsifier-program-v1.md @@ -1,5 +1,11 @@ # GRIDCRAFT-BAGOP-FALSIFIER-1: Cross-repository proof and admission program +## POC scope reset: integration corpus deferred (2026-11-05) + +This GridCraft/Excel falsifier remains a **downstream integration gate**, not a prerequisite for the core SAP-shaped Guid128 tile POC. The core independent proof belongs in lance-graph/OGAR: scoped, unambiguous 128-bit GUID correspondence over separate SoA populations; one SAP/CATS-shaped typed property fold using Quack/mask-risc; logical PSCustomObject field projection; and zero per-row object materialization in the hot path. Distinguish cold sorted index building from hot numeric fold. The existing correspondence implementation must not be relabeled as a completed pure `simd_stride` GUID join. + +P3 GridCraft, P5 workbook, P7 F###, and this Excel parity suite may follow **after** that POC. None is needed to admit or benchmark its first business tile fold. + **Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P3, P5 and [P7 F### formula polyfills #3](https://github.com/AdaWorldAPI/gridcraft/pull/3). **P4 (lance-graph-java) is a non-blocking historical/empirical precedent solely for folding without per-row materialization, not an implementation, runtime or semantic dependency.** **Research question:** Can the exact same witnessed holographic Bag answer Excel XVERWEIS, a PSCustomObject-shaped named property and direct Bagop folding without materializing one row/cell/object per logical identity, without fabricating a second authority, and while preserving Excel semantics and OGAR scopes? From 4a4cd1c9c4d14b2ddac4204578d1e37a5bd97892 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 5 Nov 2026 22:56:12 +0100 Subject: [PATCH 5/5] docs(plan): scope GridCraft falsifiers to downstream consumer parity --- .../gridcraft-bagop-falsifier-program-v1.md | 123 +++++------------- 1 file changed, 31 insertions(+), 92 deletions(-) diff --git a/docs/plans/gridcraft-bagop-falsifier-program-v1.md b/docs/plans/gridcraft-bagop-falsifier-program-v1.md index 66df23e449..1f7f2776eb 100644 --- a/docs/plans/gridcraft-bagop-falsifier-program-v1.md +++ b/docs/plans/gridcraft-bagop-falsifier-program-v1.md @@ -1,106 +1,45 @@ -# GRIDCRAFT-BAGOP-FALSIFIER-1: Cross-repository proof and admission program +# GRIDCRAFT-TILE-CONSUMER-FALSIFIER-1: Optional Excel parity after the core tile proof -## POC scope reset: integration corpus deferred (2026-11-05) +**Status:** DEFERRED, documentation only. **Date:** 2026-11-05. **Owner:** GridCraft owns Excel consumer parity, not the DR routing, DT behavior or source-GUID identity laws. -This GridCraft/Excel falsifier remains a **downstream integration gate**, not a prerequisite for the core SAP-shaped Guid128 tile POC. The core independent proof belongs in lance-graph/OGAR: scoped, unambiguous 128-bit GUID correspondence over separate SoA populations; one SAP/CATS-shaped typed property fold using Quack/mask-risc; logical PSCustomObject field projection; and zero per-row object materialization in the hot path. Distinguish cold sorted index building from hot numeric fold. The existing correspondence implementation must not be relabeled as a completed pure `simd_stride` GUID join. +## 1. Proof order -P3 GridCraft, P5 workbook, P7 F###, and this Excel parity suite may follow **after** that POC. None is needed to admit or benchmark its first business tile fold. +The first POC runs in lance-graph / OGAR / ndarray without GridCraft. It demonstrates a SAP- or PSCustomObject-shaped logical tile over normalized, ordinal-addressed SoA populations. DR resolves the coordinates, DT checks class and method parity, and an admitted Quack/mask-RISC fold performs the calculation. -**Status:** PROPOSED / planning-only. **Date:** 2026-11-05. **Owner:** GridCraft as integration harness; all semantic and kernel decisions remain with their owners. **Depends on:** P0–P3, P5 and [P7 F### formula polyfills #3](https://github.com/AdaWorldAPI/gridcraft/pull/3). **P4 (lance-graph-java) is a non-blocking historical/empirical precedent solely for folding without per-row materialization, not an implementation, runtime or semantic dependency.** +Only afterward may a GridCraft adapter present the same tile as worksheet cells. This optional consumer test must not become a prerequisite for the foundation. -**Research question:** Can the exact same witnessed holographic Bag answer Excel XVERWEIS, a PSCustomObject-shaped named property and direct Bagop folding without materializing one row/cell/object per logical identity, without fabricating a second authority, and while preserving Excel semantics and OGAR scopes? +## 2. Core proof criteria, owned outside GridCraft -## Explicit non-goals +| Gate | Test | +|---|---| +| C1 Identity | Preserve the complete 128-bit Guid128 and explicit tenant/domain scope; no display-label identity shortcut | +| C2 Hybrid correspondence | Compare normalized AD backsync GUID to Entra id and EXO ExternalDirectoryObjectId; sourceAnchor remains an independent witness | +| C3 Ambiguity | Detect conflicting or duplicate associations; never silently choose a match | +| C4 Coordinate lifetime | On a row reorder, route change or data revision, rebind a local ordinal reference or refuse it | +| C5 DT parity | Verify ClassView field basis, WideFieldMask presence, method signature, guards, ordered effects and derived-class routing | +| C6 Execution | Compare an admitted SAP-style typed fold against a separately implemented scalar oracle | +| C7 Hydration | No per-row PSCustomObject, Excel Cell or joined DTO allocation in canonical execution | +| C8 Admission | Report unavailable foreign-lane joins and derived-mask reuse; never bypass the existing restrictions | +| C9 Measurement | Separate cold identity binding/index cost, warmed read, fold, replay checks and terminal presentation | -No production code, dependency update, merge, full GridCraft rewrite, new SIMD engine, new Bagop interpreter, custom Gather, independent identity dictionary, or claim that file decoding/serialization costs zero bytes. Do not promote a lab to a production admission. +The foundation owns these tests. An existing cold sorted GUID index is a valid baseline. No claim that ndarray's byte-LUT helpers already implement the GUID join. -## Fixture F0: independently specified +## 3. Optional GridCraft proof -Create a *future implementation* fixture with exactly DR256 × 256 tiles (65,536 local positions), deliberately permuted local order and at least two distinct OGAR-granted tenant populations whose external labels collide. Each population includes duplicate lookup keys, unique keys, one not-found key, multiple typed columns, reversed and sorted presentations, and invalid/foreign source identifiers. +A future virtual sheet may present a 30 by 12 viewport over the witnessed tile without building a copy of the entire row population. If Excel XVERWEIS is supported, independently verify match order, duplicates, not-found results, blank and empty text, exact decimals and array spills. These are Excel result semantics, not the meaning of the DT operation pointer. -The independent oracle carries canonical source-qualified identities, Bag occurrence numbers, typed values and a separate **logical row order**. It does **not** share DR local positions, Bagop execution plans, a candidate index or the production codebook implementation. +The operation pointer identifies behavior; the execution can resolve a coordinate; a requested property read can return a value. Keep all three distinct. A coordinate reference must carry or be bound to scope, source snapshot and layout, rather than a naked snapshot-local ordinal. -Required values: zero, negative number, exact decimal text 9007199254740993, null/absent, blank, empty text, explicit missing, formula anchor and spill cached child, error state, Unicode text, and a changed value between versions. Do not pretend all these states are equivalent or always native to one codec. +The optional test also compares cold and warm costs, observed allocations, and output serialization. Unsupported formula modes must be explicitly reported, not silently executed through a row-materializing fallback. -## Paths under test +## 4. Dependencies and non-dependencies -A. Direct source-qualified Bagop fold via admitted Quack/RelAlg/mask-risc/ndarray. +- [P0 foundation](https://github.com/AdaWorldAPI/lance-graph/pull/1960): DR coordinate routing, DT parity, and hybrid GUID tile architecture. +- [P1 ndarray](https://github.com/AdaWorldAPI/ndarray/pull/408): position-oriented execution mechanics. +- [P2 method pointer](https://github.com/AdaWorldAPI/lance-graph/pull/1961): optional coordinate-returning operation contract. +- [P3 GridCraft](https://github.com/AdaWorldAPI/gridcraft/pull/1): optional virtual worksheet consumer. +- [P7 F###](https://github.com/AdaWorldAPI/gridcraft/pull/3): optional formula-to-DT behavior-lens adapter. +- [P5 report-rs](https://github.com/AdaWorldAPI/report-rs/pull/34): separate report consumer. +- [P4 Java precedent](https://github.com/AdaWorldAPI/lance-graph-java/pull/93): non-blocking evidence for folding without host-object construction. -B. GridCraft XVERWEIS expression over mounted virtual BagSheet, using the same Bagop contract. Cover exact first and last; unadmitted wildcard/approximate/binary must give a typed refusal. - -C. PSCustomObject-shaped named property projection over the same Bag, with no nested object tree in execution. - -D. Independent scalar Excel-style oracle for exact matching and order, with distinct Bag multiplicity oracle. Optional real Excel/XLSX terminal roundtrip must be reported as external compatibility evidence, not as an internal oracle. - -## Acceptance and disable matrix - -| Gate | Positive oracle | Disable/falsifier | -|---|---|---| -| G0 semantic authority | Delete every derived index then rebuild: same IDs, multiplicities and results | Substitute workbook-minted ordinal: fail | -| G1 exact first/last | Excel-style independent source order matches | Remove order witness: red | -| G2 duplicates | Bag fold counts all occurrences, XVERWEIS chooses specified one | Implicit DISTINCT: red | -| G3 field binding | DT64 property name binds same meaning after input column reorder | Mutable basis without witness: red | -| G4 epistemic states | Blank, EmptyText, Absent, Missing, Formula/Spilled and error distinct as admitted | Conflate two states: red | -| G5 precision | Exact decimal string roundtrips or refuses lossless conversion | f64 conversion: red | -| G6 frame correctness | Permuted tile/frame refused or correctly rebound | Remove digest: red | -| G7 tenant isolation | Equal labels in two scopes do not alias | Bypass scope check: red | -| G8 value revision | Value-bearing cached method refuses stale revision; map COUNT valid | Remove value witness: red | -| G9 amortization | 256 repeated methods after one bind: zero additional global→local lookups | Re-route each method: counter red | -| G10 no row hydration | 65,536 Bag rows, zero persistent GridCraft Cell/PSCustomObject instances per Bag row | Force per-row Cell creation: allocation test red | -| G11 viewport | 30×12 window memory bounded by visible rows/cells and descriptors | Eager entire 65K×24 render: red | -| G12 dynamic arrays | Visible spill children have correct anchor, shape and order | Collapse spilled cached child: red | -| G13 admission law | Unadmitted Gather/composition/mask reuse refuses | Permit value-derived cross-table address: red | -| G14 backend parity | Scalar, AVX2, AVX512, NEON, WASM where runnable | Tail/stride corruption: red | -| G15 egress scope | Export only authorized values; no cross-scope cache | Reuse view after permission revocation: red | - -A negative control must be run in a disposable test mutation and restored. A red disable proves the test can catch the violation; it is not evidence of production readiness. - -## Performance experimental matrix - -Record CPU model, ISA, Rust version, build flags, source revision, fixture seed, warmup, repetitions, distribution and resident/peak bytes. Separate: - -1. XLSX parse/decompression and eTag/snapshot validation. -2. Canonical source bind and DR global→local preparation (map count). -3. One exact-match fold. -4. 256 warm repeated folds under the same prepared descriptor. -5. 30×12 viewport presentation and all-cell scrolling. -6. Cold text hydration and exact numeric conversion. -7. Terminal CSV/XLSX/PowerShell serialization and total bytes. -8. Cache invalidation/rebind after scope, frame or value change. - -Compare to GridCraft CellStore and report-rs #33 **only where work and witness obligations match**. The ~0.39ns warmed lookup is not an end-to-end XVERWEIS comparator. Record p50/p95 and allocation deltas; do not cherry-pick backend/shape. - -## PR/program gate order - -| Phase | Prerequisite | Pass requirement | -|---|---|---| -| R0 | P0 owner decision | One-authority law with no hidden contradictory DR interpretation | -| R1 | P1, P2 owners | Exact-match ordered fold admitted or explicit STOP | -| R2 | P3 review | GridCraft virtual presentation and object-materialization bounds; P4 reference optional | -| R3 | P5 convergence | report-rs does not create a second source | -| R4 | DRISA M1/M2, OGAR | Frame, route and scope attestations | -| R5 | D4/S-INGRESS if writing requested | Canonical writer admission; otherwise read-only | -| R6 | This falsifier plan | Independent oracle and negative controls defined **before** code | - -**Decision log 2026-11-05:** proposed test program, not proof. **Next implementation PR:** one read-only lab vertical slice with fixture and independent scalar oracle, not production. Stop if the required Bagop operator or layout/scope witness is not admitted. - -## References / companion plans - -- [P0/P2 source repository](https://github.com/AdaWorldAPI/lance-graph), [DRISA lab #1955](https://github.com/AdaWorldAPI/lance-graph/pull/1955) -- [P1 ndarray FACET STRIDE](https://github.com/AdaWorldAPI/ndarray/blob/master/src/simd_stride.rs) -- [P3 GridCraft CellStore](https://github.com/AdaWorldAPI/gridcraft/blob/main/crates/model/src/store.rs) -- [P4 non-blocking evidence for non-materializing native folds](https://github.com/AdaWorldAPI/lance-graph-java/blob/main/java/README.md) -- [P5 report-rs PR #33](https://github.com/AdaWorldAPI/report-rs/pull/33) - -## G16–G19: F### formula method and Codegraph non-dilution gates (2026-11-05) - -These gates extend G0–G15 and depend on [P7 #3](https://github.com/AdaWorldAPI/gridcraft/pull/3). The F### numbering/MethodRef registry is **not verified** and must be discovered in its canonical owner before an implementation can claim parity. - -| Gate | Positive independent oracle | Negative control | -|---|---|---| -| G16 method identity | Identical parsed formula+scope+registry version resolves to the same canonical F###/MethodRef; change in source location affects provenance but not method semantics | Locally mint an ordinal or remove registry version check: red | -| G17 no materializing formula fallback | SUM/COUNT and admitted XVERWEIS over 65,536 identities perform no per-row `Vec` or `Cell` hydration in canonical execution | Route to `Host::range_values` collecting entire population: allocation test red | -| G18 Kythe/Codegraph boundary | Verified source/def-use/call provenance is derived, read-only and keyed to actual owner contract, not a second formula evaluator | Insert invented formula identity in Codegraph or mutate it as value authority: contract test red | -| G19 R2IL integrity | Existing R2IL machine opcode vocabulary/semantics remain unchanged while formula method calls are separately traced | Alias an Excel formula to R2IL IntAdd or mint a competing opcode: vocabulary parity red | - -Additional semantics: lazy IF/LET/LAMBDA, volatile/effectful formulas, exact decimals, formula sources/spans and spilled arrays must have separate independent oracles or remain NOT ADMITTED. **Do not assert every formula is a reduction.** Formulas require typed F### method contracts; some lower to elementwise, control, reference or effect semantics. A source-level formula→method→operator mapping is provenance, not a new storage substrate. +No GridCraft workbook import, Java runtime, DataFusion, or Codegraph adapter is required for the core POC. No runtime code, test implementation, merge or production admission is included in this PR.