docs: AUTODIFF_NEXTGEN_PLAN — one derivative functor, algebra as a parameter (W6.3 design) - #582
Merged
Merged
Conversation
…s parameter Scoped plan (plan_state: draft, not yet bound to INTEGRATED_COMPILER_PLAN) supplying the design content behind W6.3's "research estimate required": one DerivativeContract datum per primitive evaluated under an explicit DifferentialAlgebra codomain (Dual / TruncatedJet Weil / CliffordTangent / OperatorTangent / TaylorModel), correctness as six executable laws instead of pointwise gradcheck, and slices AD-LAW-1 -> AD-WEIL-1 -> AD-JET-STRUCT-1 -> AD-JET-IR-1 (+ AD-OPERATOR-1, AD-CERT-1 consumer-gated). Cross-checked against CORE_SUBSTRATE_VIEW (S5/S6/S8 findings incorporated, incl. the vmap-is-a-for-loop funding correction) and CUTE_IR_ASSESSMENT (jet coefficient axis as LAYOUT-ALG-1's sixth consumer). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 01816e29a1
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…ions
All four review findings accepted after independent verification:
- plan_state: draft -> open (AGENTS.md permits only open/landing/closed;
fixes test_plan_docs_declare_a_valid_plan_state). Proposal status moved
into the routing banner prose.
- Route AUTODIFF_NEXTGEN_PLAN.md from the compiler README index (fixes
test_compiler_index_routes_every_live_document).
- §3.1: the nested-vs-jet relationship is the diagonal EMBEDDING
ℝ[ε]/(ε^{k+1}) ↪ ⊗ᵢℝ[εᵢ]/(εᵢ²), ε ↦ Σεᵢ — the previously claimed
surjection εᵢ ↦ ε is not an algebra map (εᵢ²=0 would force ε²=0).
Correction recorded in place; the wrong map becomes a negative fixture
in the AD-LAW-1 math harness (#10a).
- §3.5/§4: Law 3 re-scoped as complete for the transpose relationship
only (a matched-wrong JVP/VJP pair passes); derivative correctness
stays with Laws 1/2/4 + existing FD oracles. E2E-REAL-6 note softened
to match.
- §3.6: "every primitive is semialgebraic" was false (exp; unrestricted
trig is not o-minimal-definable). Replaced definable:bool with a
per-primitive path-differentiability witness (smooth |
definable:<structure>); program-level guarantee composes via the
conservative-field chain rule.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This was referenced Aug 18, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Adds
docs/audit/compiler/AUTODIFF_NEXTGEN_PLAN.md— a scoped plan (plan_state: draft, not yet bound toINTEGRATED_COMPILER_PLAN.md) that supplies the design + acceptance detail behind W6.3's "research estimate required" row, plus a law-oracle evidence lane that can start immediately.Core thesis
Every AD mode is one functor evaluated in a different codomain algebra. Today the codomain ℝⁿ is hardwired into two hand-paired registries (
vjp.py+jvp.py, ~9.6k lines), and five in-tree structures have each independently paid for that: the dual registry itself, thegeometric/forked tape (_VJPS_GEO/_JVPS_GEO),linear.py's derived-JVP workaround,nonsmooth.py's policy registry, andimplicit.py's matvec pattern.The plan replaces this with one
DerivativeContractdatum per primitive (multilinearity declaration / holonomic ODE / linearize+transpose pair / kink policy / definability) evaluated under an explicitDifferentialAlgebraparameter —Dual()reproduces today's semantics;TruncatedJet(k)gives order-k derivatives at cost k+1 instead of 2^k;CliffordTangentabsorbs thegeometric/fork;OperatorTangentpromotesimplicit.py's pattern;TaylorModelis the consumer-gated certified mode. Correctness is enforced as six executable algebraic laws (adjoint ⟨Jv,u⟩=⟨v,Jᵀu⟩, homomorphism-exact-by-nilpotency, jet≡nested quotient proof, kink-policy probes, …) rendered to a generated dashboard, instead of tolerance-tuned pointwise gradcheck.Slices proposed (estimates, Decision #31 ordering: derive → prove differentially → only then retire)
Dual()+TruncatedJet(k)+ ODE table; settles the W6.4-note GA-substrate hypothesis withga/signature.pyas oracleflash_attn/norms; STDE-style estimators on Philox with unbiasedness contractsTaylorLiftPass(W); coefficient axis in the L5#tile.layoutcarrier; L0-shape C++ homeOperatorTangent+ adopts S8's previously-unowned strict-complementarity hardening (H3)Cross-checks already folded in
batching_rules are a dependency, and AD-JET is the second forcing function after G4); PDE's S6 row already demands "jet AD" (second Apple GPU MLA: native f16/bf16 for the absorbed decode kernel #29 consumer); AD-JET-IR-1 is the fourth mandate for the unowned S5numeric_policycarrier;TaylorModelnamed as the Decision Apple GPU MLA: same-length B>1 batching in decode_batch (throughput) #28 accuracy-budget certificatelogical_product/regroup/cosize/⊑/coalesce/crd2idx); AD-JET-IR-1 depends on L1+L5; the jet kernel's eventual C++ descent copies L0's one-home shapeDeliberately NOT in this PR (owner's call, listed as proposed bindings in the doc)
INTEGRATED_COMPILER_PLAN.mdwith these estimatesCUTE_IR_ASSESSMENT.md§3docs/audit/compiler/README.md's authority chainNo code, no status claims, no generated-doc changes — pure design/plan document.
🤖 Generated with Claude Code