Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions docs/audit/backend/apple/todo.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,18 @@ last_updated: 2026-08-24

# Apple compiler, exact-device, and performance plan

Cross-backend sync `NUMPOL-CARRIER-1-2026-08-24` — **shared Schedule→Tile
`numeric_policy` carrier contract (integrated-plan queue row 3b); Apple
outcome: follow-up required.** Newly owned row, nothing implemented yet.
Apple consumes the contract through the MSL emitters and the value-preserving
Target-IR lane; its `simdgroup_matrix` coopmat path is the natural first
carrier site (the accumulator choice there is exactly what the policy must
survive to reach). Note the standing seam: the Python MSL synthesizer and the
C++ MLIR pipeline are two disconnected compilers, so the carrier must be
designed not to require a third policy representation. M1 Max evidence
required before any numerical claim.


Cross-backend sync `LAYOUT-ALG-APPLE-PHYSICAL-2026-08-24` — **reachable Metal
physical-consumer tail closed.** The versioned native layout ABI now exports
the existing `Rank2Index.h` coordinate plan to source emitters without a Python
Expand Down
11 changes: 11 additions & 0 deletions docs/audit/backend/nvidia/todo.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,17 @@ last_updated: 2026-08-24

# NVIDIA compiler test-suite evaluation and rearchitecture

Cross-backend sync `NUMPOL-CARRIER-1-2026-08-24` — **shared Schedule→Tile
`numeric_policy` carrier contract (integrated-plan queue row 3b); NVIDIA
outcome: follow-up required, sequenced behind W1.1.** Newly owned row,
nothing implemented yet. NVIDIA will consume the same carrier, but its typed
fragment producers are still open under W1.1 — the carrier work here should
follow that, not race it, or the two will collide at the same seam. CAKE
(#32's original derivation) is an NVIDIA-facing consumer, so the barrier and
TCGen05 fragment paths are the ones to check first. sm_120 exact-device
evidence required before any numerical claim; no ROCm/x86 result transfers.


Cross-backend sync `LAYOUT-ALG-APPLE-PHYSICAL-2026-08-24` — **shared ABI
assessed; no CUDA physical change.** Apple now exports the existing C++ rank-2
plan through the native layout ABI for its MSL emitters and owns fresh M1 Max
Expand Down
13 changes: 13 additions & 0 deletions docs/audit/backend/rocm/todo.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,19 @@ scope: ROCm backend implementation and exact-device proof

# ROCm backend TODO

Cross-backend sync `NUMPOL-CARRIER-1-2026-08-24` — **shared Schedule→Tile
`numeric_policy` carrier contract (integrated-plan queue row 3b); ROCm
outcome: follow-up required — ROCm owns the worked reference.** The row is
newly owned and nothing is implemented yet; this entry records the
architecture-specific obligation, not parity. ROCm is the one backend with a
partial carrier today: the W1.1 typed route carries the accumulator inside
`!tile.fragment<…, acc, …>`. The generalization must RE-EXPRESS that path as
an instance of the general carrier (#31 — one implementation per boundary,
not a second), with bit-identical gfx1151 outputs as the acceptance bar, and
extend it to the pointwise/reduction/butterfly chains that carry no policy
today. Exact-device gfx1151 evidence required before any numerical claim.


Cross-backend sync `LAYOUT-ALG-APPLE-PHYSICAL-2026-08-24` — **shared ABI
assessed; no AMD physical change.** Apple now exports the existing C++ rank-2
plan through the native layout ABI for its MSL emitters and owns fresh M1 Max
Expand Down
11 changes: 11 additions & 0 deletions docs/audit/backend/x86/todo.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,17 @@ scope: x86 AVX-512 implementation/proof and AMX access planning

# x86 backend TODO

Cross-backend sync `NUMPOL-CARRIER-1-2026-08-24` — **shared Schedule→Tile
`numeric_policy` carrier contract (integrated-plan queue row 3b); x86
outcome: follow-up required.** Newly owned row, nothing implemented yet.
x86 has no fragment type, so it has NO carrier today — the accumulator
contract stated at Graph IR does not exist by the time the AVX-512 emitters
pick an instruction (Decision #32's original defect, on this backend in its
purest form). The row's acceptance names bit-identical existing x86 outputs,
so this backend is both a consumer of the contract and a regression gate for
it. Clean Zen 5 evidence required for any realizability verdict (FORGE §1.3).


Cross-backend sync `LAYOUT-ALG-APPLE-PHYSICAL-2026-08-24` — **shared ABI
assessed; no x86 physical change.** Apple now exports the existing C++ rank-2
plan through the native layout ABI for its MSL emitters and owns fresh M1 Max
Expand Down
4 changes: 2 additions & 2 deletions docs/audit/compiler/AUTODIFF_NEXTGEN_PLAN.md
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ defaulted silently:
| `kink_policy` | `nonsmooth.py`'s named policies | Already shipped; enters the *forward* of higher-order kernels (§3.4) |
| `pd_witness` | `smooth` \| `definable:<structure>` | Per-primitive witness for the §3.6 convergence guarantee — a bare boolean cannot carry the hypothesis (see §3.6's correction) |
| `control_at_order` | `0` (only legal value in v1) | Data-dependent control flow (branch predicates, `while` trip counts, `max` selections) evaluates on the **primal coefficient only**; coefficients follow the primal's trace. Matches W4-PRODUCT's predicate-replay identity, stated for jets |
| cotangent/coefficient `numeric_policy` | per Decision #15a | Higher coefficients shrink like 1/k!; accumulator and storage dtype per coefficient is a declared contract, not an accident. (Today the tape seeds backward at float64 regardless of model dtype per the spec's mechanism section — an implicitly chosen accumulation dtype this key makes explicit.) **Carrying this key below Graph IR depends on the S5 generalized `numeric_policy` carrier (`CORE_SUBSTRATE_VIEW.md` S5 — fragment-only today, no owning row); AD-JET-IR-1 is its fourth mandating consumer, §5a** |
| cotangent/coefficient `numeric_policy` | per Decision #15a | Higher coefficients shrink like 1/k!; accumulator and storage dtype per coefficient is a declared contract, not an accident. (Today the tape seeds backward at float64 regardless of model dtype per the spec's mechanism section — an implicitly chosen accumulation dtype this key makes explicit.) **Carrying this key below Graph IR depends on the S5 generalized `numeric_policy` carrier — owned since 2026-08-24 as integrated-plan queue row 3b, `NUMPOL-CARRIER-1` (`CORE_SUBSTRATE_VIEW.md` S5; fragment-only in implementation until that row lands); AD-JET-IR-1 is its fourth mandating consumer, §5a** |

Interleaved-vs-planar coefficient storage (§6) is deliberately **not** in this
table: both layouts compute the same jet, so it is a performance key —
Expand Down Expand Up @@ -481,7 +481,7 @@ above:
|---|---|
| **S8 transform substrate** | Three touch points. (1) **Real `batching_rule`s are a dependency, not an asset** — the funding-table correction above; AD-JET-* joins game theory G4 as a forcing function. (2) **Implicit-diff strict-complementarity hardening (H3)** — "one fix, three consumers, no row" — is adopted into AD-OPERATOR-1's scope (§7), since that slice already refactors `implicit.py`. (3) **Schedule-level autodiff** (CAKE capability #1: transpose the S2 schedule object) is the *same adjunction as §3.5 applied at the schedule level* — related, deliberately **not** claimed by this plan; it stays gated on S1+S2 per the substrate view. The two must eventually agree on transpose vocabulary, which is an argument for landing §3.5's value-level `OperatorTangent` first |
| **S6 structural-op tranche** | The PDE demand row **already names "jet AD"** as a demanded capability — a second in-tree consumer for AD-WEIL-1 beyond the law harness, materially strengthening its #29 position. The PDE Chebyshev/DST lane is likewise the named candidate consumer that would un-gate `ChebJet` (§2.2) |
| **S5 `numeric_policy` carrier** | The coefficient/cotangent `numeric_policy` key (§2.3) requires the generalized below-Graph-IR carrier, which S5 records as fragment-only with **no owning row**. AD-JET-IR-1 is the **fourth mandating consumer** (after CAKE, game theory §6, PDE §III.4) — added weight behind the substrate view's flagged input to the integrated plan |
| **S5 `numeric_policy` carrier** | The coefficient/cotangent `numeric_policy` key (§2.3) requires the generalized below-Graph-IR carrier, fragment-only in implementation today. **Owned since 2026-08-24 as integrated-plan queue row 3b, `NUMPOL-CARRIER-1`** — AD-JET-IR-1 is its fourth mandating consumer (after CAKE, game theory §6, PDE §III.4), and this gate now tracks that row rather than an unowned flagged input |
| **S4 keys + certificates** | Full alignment: §2.3's semantic keys are S4 instances; `LinearSolveInfo`, the Law dashboard, the measured conditioning envelope (§3.8), and `TaylorModel` enclosures follow the certificates-not-booleans discipline |
| **S3 calibration + arbiter** | `TaylorModel` enclosures are the strongest available form of the **accuracy certificate** the Decision #28 accuracy-budgeted arbiter needs (CAKE capability #4: accuracy budget as a search axis). Named as AD-CERT-1's candidate consumer (§7) |
| **S2 schedule object** | Jet kernel packages ride the Schedule Object digest (`SCHEDULE_OBJECT_DESIGN.md`) like every other content-addressed carrier; no new mechanism |
Expand Down
23 changes: 13 additions & 10 deletions docs/audit/compiler/CORE_SUBSTRATE_VIEW.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
last_updated: 2026-08-15
last_updated: 2026-08-24
audit_role: reference
verification: every previously prose-only mathematical claim this view inherits
is machine-checked — 13/13 in research/core_substrate/verify_substrate_math.py
Expand Down Expand Up @@ -206,7 +206,8 @@ learn from `numeric_policy`, not from a special case), and the PDE plan §III.4

**Stands:** partially landed where W1.1 reached — `!tile.fragment<…, acc, …>`
carries the accumulator on the typed ROCm route. Generalizing beyond MMA
fragments (pointwise/reduction/butterfly chains) has **no owning row**.
fragments (pointwise/reduction/butterfly chains) is owned by
**NUMPOL-CARRIER-1 (integrated-plan queue row 3b, 2026-08-24)**.
Comment thread
gstoner marked this conversation as resolved.
**FORGE §1.3 supplies the measured target** this carrier was missing: whether
the fused-epilogue fp32-accumulator win is realizable flips 913× → 1.1× → 1.0×
purely as a function of `accum` × state dtype — a fact only a compiler carrying
Expand Down Expand Up @@ -311,19 +312,21 @@ and it is deliberately host-free).
| S2 schedule object | **W5.2** (c/e/g landed/landing) | IR-surviving schedule datum; stated entry point (CAKE Ph 3); roles vocabulary (CAKE Ph 2) |
| S3 calibration + arbiter | W5.2b/c landed; TileSight §4 items | **Calibration sweeps** (fleet-box task, small); rasterization-knob consumers; certificate-driven candidate rejection (PDE §III.2) |
| S4 keys + certificates | Governance (#21a/#29/#30, drift-gated) | Per-lane, carried inside each plan |
| S5 numeric_policy carrier | W1.1 (fragments only) | **Generalized carrier + boundary verifier** — no row |
| S5 numeric_policy carrier | W1.1 (fragments only) | **Owned 2026-08-24: INTEGRATED_COMPILER_PLAN queue row 3b (NUMPOL-CARRIER-1)** |
Comment thread
gstoner marked this conversation as resolved.
| S6 structural-op tranche | — | **Entire tranche — no row** (G1b, scan, segment_sum, tridiagonal, attention modes, index ops) |
| S7 memory tiers + prefetch | W2.4a (sync floor); E4 chunk machinery | **Prefetch edge + feasibility check + KV-cache invariants** — no row beyond SparDA's own table |
| S8 transform substrate | AD-* rows (partial) | **Real batching; implicit-diff hardening** — no rows; schedule-AD deliberately deferred |
| S9 locality + residency (FORGE) | — (precedents: `TrainingStepFusionPass`, `LOWER-COUNT-1`, `numeric_policy` on `MatmulOp`) | **Entire pair — no rows** (FORGE W1–W4 in its own order); host-free |

Four flagged inputs for the integrated plan (recommendation only; ordering is
its call): a row for the **structural-op tranche** (S6 — serves three plans),
a row for the **generalized numeric_policy carrier** (S5 — three plans mandate
it via #32), and the **calibration sweeps** as an explicit small task rather
than a perpetual "still open" footnote (S3 — it silently gates four other
items). Fourth: **rows for FORGE W1→W2→W3→W4** (S9 — host-free, and W2's
residency proof is the cheapest honest answer to every future memory claim).
Flagged inputs for the integrated plan (recommendation only; ordering is its
call). **One of the original four is now closed:** the **generalized
numeric_policy carrier** (S5) was adopted as integrated-plan queue row 3b,
`NUMPOL-CARRIER-1`, on 2026-08-24 — do not re-propose it. The three that
remain open: a row for the **structural-op tranche** (S6 — serves three
plans); the **calibration sweeps** as an explicit small task rather than a
perpetual "still open" footnote (S3 — it silently gates four other items);
and **rows for FORGE W1→W2→W3→W4** (S9 — host-free, and W2's residency proof
is the cheapest honest answer to every future memory claim).

## 4. The updated build sequence (proposal — ordering authority stays with the integrated plan)

Expand Down
1 change: 1 addition & 0 deletions docs/audit/compiler/INTEGRATED_COMPILER_PLAN.md
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ This section owns what to do with those counts.
| 1 | **E2E-REAL-6F — remaining optimizer VJP authority complete; family migration continues** | SGD and Momentum/Nesterov on x86/gfx1151 plus Adam/AdamW on gfx1151 use explicit non-reexecuting plugins and one typed `schedule.optimizer_vjp` → `tile.training_kernel` artifact. The package binds tracer proof, state/cotangent lineage, numeric identity, target ownership, and exact Tile digest. Unsupported target pairs fail before construction. The three former `JitFn` compatibility helpers are deleted. | One-execution/plugin tests for the three ABI shapes; Schedule/Tile verifier negatives; existing AVX-512 and gfx1151 physical regressions; runtime receives no source Graph or operation dictionary. | E2E-REAL-6E state-lineage package. |
| 2 | **W4-PRODUCT-1 — executable multi-block regions** | The bounded arbitrary-CFG compiler boundary, per-slot dynamic saved-value envelopes, companion logical-shape tapes, mixed-state SAVE/HYBRID tapes, and nested canonical bodies are landed. Exact polynomial specialization guards remain outside Presburger proofs and require complete witnesses. Compiler-generated replay-safe assertions are admitted; mutation, unkeyed RNG, I/O, alias-sensitive work, and ordered collectives remain fail closed pending operation-owned recorded-product ABIs. The gfx1151 irreducible-state-machine row landed 2026-08-21: `--generate-rocm-state-machine-kernel` lowers a paired `bounded_state_machine_v1` function (forward AND generated backward) to one per-thread device kernel — per-element program counter, structured-CFG digest stamped on the gpu.func, `cf.assert` bound check host-enforced through a STATUS buffer — with both entry paths of a two-entry SCC executing on gfx1151 against the analytic oracle (`test_rocm_state_machine_exec.py`). The sibling x86 row landed 2026-08-21 as well: the same paired functions compile through `tessera_jit` (tessera-to-linalg → elementwise-to-linalg → one-shot-bufferize → loops → LLVM → ORC JIT) and execute natively on the AVX-512 host — both entry paths, forward + backward, digest/residual-policy bound, native `cf.assert` bound trap, proof-of-execution counter (`test_x86_state_machine_exec.py`). Next: one physical packet family with admissible effects. | Existing region verifier/paired VJP fixtures stay green; padded tape bounds must never replace logical extents; native x86/gfx1151 numerical rows must bind the exact CFG and residual digests before physical execution is claimed. | W2.1 dataflow, W2.2 effects, current bounded W4 carrier. |
| 3 | **SO-3 + W5.2e-PRODUCER-1 — one schedule authority** | Stamp the Schedule Object digest through lowering, delete scalar pipeline reconstruction, and make two representative physical producers—spectral and collective/MoE—consume inferred dependence edges. | Generated DAG covers hand-authored oracle edges; unknown facts conservatively serialize; emitted artifact preserves digest/roles/resources; numerical output is unchanged on x86 and gfx1151. | SO-1/SO-2 and W5.2e inference. |
| 3b | **NUMPOL-CARRIER-1 — the S5 generalized `numeric_policy` carrier (owned 2026-08-24)** | One carrier design for storage/accumulator/math-mode that survives Schedule and Tile IR beyond MMA fragments (pointwise, reduction, and butterfly chains), plus the Decision #32 boundary verifier that FAILS on silent loss instead of recording it. Builds on the landed W1.1 `!tile.fragment<…, acc, …>` accumulator carrier (typed ROCm route) as the worked reference. Four mandating consumers: CAKE (#32's original derivation), game-theory §6 (fusion is a correctness feature — the zeta intermediate must not round through fp32), PDE §III.4 (interim `tessera.info_loss` records retire), and AD-JET-IR-1 (coefficient/cotangent policy, W6.3 §2.3). FORGE §1.3 supplies the measured acceptance target: the fused-epilogue fp32-accumulator realizability verdict (913× → 1.1× → 1.0× purely as a function of accum × state dtype) must be decided by the carried policy, not a special case. | Carrier attribute round-trips Schedule→Tile with a lit-verified boundary check per crossing; a lowering that drops the policy fails closed with a named diagnostic (#21a/#32); the W1.1 fragment path re-expressed as an instance of the general carrier without behavior change (bit-identical existing gfx1151/x86 outputs); the PDE `tessera.info_loss` interim records replaced by carrier facts; dashboard row tracks per-boundary coverage. May proceed in parallel with Orders 3 and 5 (orthogonal IR-carrier work; the schedule authority does not consume the policy). | W1.1 fragments (landed); Decision #32; #21a semantic-key discipline. |
Comment thread
gstoner marked this conversation as resolved.
| 4 | **LAYOUT-ALG-1 L4 — physical layout decisions closed 2026-08-24** | L3 factorization/residency and SO-4 proof attachment are implemented. Mixed-radix/static tuple products, SM120 dynamic strided typed+macro routes, gfx1151 bounded-dynamic execution, the four x86 core GEMM index families, and every reachable Apple MSL rank-2 template consume shared authority. Dynamic non-separable tuple codomains remain fail closed. | Existing raster/index outputs remain bit-identical; unresolved layouts fail closed; materialization proof covers alias, capacity, and lifetime; Apple7 canonical and fused-cooperative cohorts pass exact-device; no architecture's schedule is promoted by another architecture's evidence. | Current L1/L3/L5 authority and architecture-owned device proofs. |
| 5 | **W5.4-RESHARD-1 — executable placement** | Consume the remaining domain/axis-changing sharding contracts, derive typed local-shard shapes, insert explicit reshard SSA through nested regions, and execute on a deterministic mock mesh. | Fixed-point convergence and join tests; exact local result types; subgroup/region negatives; all four collective forms and `collective_permute` execute without hidden host composition. | Orders 2–4. Native transports are a later evidence gate. |
| 6 | **DIST-NATIVE-1 — real multi-rank execution** | Bind explicit reshard/collective SSA to NCCL/RCCL and MPI/OFI/SHMEM launchers, including subgroup communicators and process-rank ownership. Keep ROCm LSA, GIN/RMA, Copy Engine, and gfx1250 DDA as independent advanced gates. | Two-rank then multi-rank numerical packets; deterministic ordering; communicator/topology digest match; fail-closed missing transport; no mock result may satisfy the native gate. | Order 5. |
Expand Down
2 changes: 1 addition & 1 deletion docs/audit/generated/docs_freshness.md
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ These docs need either YAML frontmatter (`last_updated: YYYY-MM-DD`) or a body-f
| `compiler/COMPILER_AUDIT.md` | - | 2026-08-10 | 14 | ✓ |
| `compiler/COMPILER_REFACTOR_PLAN.md` | - | 2026-08-08 | 16 | ✓ |
| `compiler/COMPILER_THEORY_OF_OPERATION.md` | - | 2026-07-28 | 27 | ✓ |
| `compiler/CORE_SUBSTRATE_VIEW.md` | - | 2026-08-15 | 9 | ✓ |
| `compiler/CORE_SUBSTRATE_VIEW.md` | - | 2026-08-24 | 0 | ✓ |
| `compiler/CUTE_IR_ASSESSMENT.md` | - | 2026-08-24 | 0 | ✓ |
| `compiler/DIFFERENTIABLE_PROGRAMMING_REVIEW.md` | - | 2026-08-08 | 16 | ✓ |
| `compiler/EGGROLL_SUPPORT_PLAN.md` | - | 2026-08-09 | 15 | ✓ |
Expand Down