From e7a35339a4646647dc486541ecb4fbd8c608d793 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Sun, 25 Oct 2026 01:04:36 +0200 Subject: [PATCH 1/4] docs(D-SAG-6): preregister Rust codegraph math/logic traceroute and agent handoff --- ...-6-rust-codegraph-math-logic-tracert-v1.md | 147 ++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 .claude/plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md diff --git a/.claude/plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md b/.claude/plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md new file mode 100644 index 000000000..ebba16ebe --- /dev/null +++ b/.claude/plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md @@ -0,0 +1,147 @@ +# D-SAG-6 — Rust Codegraph → Mathematics → Logic → Tracert + +**Date:** 2026-10-24. **Status:** PROPOSAL / documentation and falsifier preregistration only. **Implementation:** NOT STARTED. No Rust, Cargo, ABI, policy, storage, proof checker, source rewrite, CI or performance changes are authorized by this PR. +**Coordination:** [Linear EXO-50](https://linear.app/exo-red/issue/EXO-50/agent-message-bus-gpt-xgrok-ccsession-id). **Execution brief:** [D-SAG-6 prompt](../prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md). +**Parent contracts:** [SAG capstone alignment](sag-capstone-alignment-v1.md), [D-SAG-2 Ruff/ONA](software-awareness-graph-v2-ruff-ona-closed-loop.md), [DR mathematical compiler](dr-mathematical-compiler-v1.md), [Ascent/BYODS cold fold](ascent-byods-dr-fold-polyfill-v1.md), [D-NFR native representation](d-native-repr-contract-v1.md), [D-NFC native-first correction](d-native-first-dependency-correction-v1.md). + +## 0. Thesis and explicit authority boundaries + +The goal is **Codegraph → Mathematics → Logic → Tracert**, not a second Rust compiler, AST interpreter, query executor, method registry or rewrite authority. + +- **Codegraph** is a source/revision-aware, typed, directed relational *view* of Rust items and operations. Source symbols, MIR places, effects, dataflow edges and callsite identities are distinct. +- **Mathematics** expresses admitted equivalence laws or candidate rewrites in the existing ClassView/RelAlg/set_rules/R2IL vocabulary. A discovered pattern is not a verified law. +- **Logic** derives reachability, dependency, alias/capture eligibility, preconditions and closed-world findings only under declared coverage. Ascent/Datafrog/Prolog are comparative **cold analysis or oracle** arms; not additional production runtimes. Egglog performs guarded equality exploration, not source authority. +- **Tracert** is a typed provenance path linking source → semantic witness → logic rule → law admission → proof/extraction → native lowering → differential/target result. A rendered egglog proof or replay capsule is not an independent proof checker. +- **Extraction** may use eggcc-style effect-ordered candidate selection offline. It must not reorder Rust drops, mutations, panics, volatile/unsafe behavior or externally visible effects without proved legality. +- **Output** is a *proposed*, reviewable Rust source patch or existing native recipe, never an automatic hot write. MLIR is an optional export/lowering arm, not the semantic source of truth. + +**SAG ownership:** D-SAG-1 software-awareness code was removed/reset; D-SAG-2 is a research plan, not a shipped generic graph. The SAG capstone reserves one inert **ProposedMethod** shape and separate proposal/verification/approval/authorization/application/re-observation stages. Do not revive removed glove-parity code or create a second ProposedMethod type. + +**Ruff disambiguation:** the relevant [AdaWorldAPI/ruff](https://github.com/AdaWorldAPI/ruff) is the fork with polyglot SPO harvest/ModelGraph and codegen arms. It may independently corroborate supported **source structure**, not Rust MIR semantics, executable equivalence or machine-code performance. Its existing ModelGraph → addressed SoA plan is [lance-graph as ModelGraph](lance-graph-as-the-modelgraph-v1.md). Preserve the stated dependency direction: Ruff crates do **not** import lance-graph; an external projection/byte boundary connects them. Do not mistake this fork for a complete Rust compiler frontend merely because upstream Ruff is written in Rust. + +## 1. Orthogonal views, not a linear tower + +~~~text +Rust source/crate/feature/target revision + | | + v v +rust-analyzer HIR rustc MIR / Charon LLBC (candidate; pin and test) + \ / + \-- typed read-only source/semantic binding --/ + | + Codegraph (DR focus / ClassView / SoA) + {defines, calls, captures, trait_impl, + def_use, cfg, borrow, drop, effect, reads} + / | \ + / | \ + Ascent/Datafrog/Datalog RelAlg/egglog Trace receipts + rule queries guarded rewrites evidence lineage + \ | / + \----- cold admission -------/ + | + eggcc-style lawful extraction + | + inert ProposedMethod / candidate recipe + / \ + Rust AST edits optional MLIR dialect export + + rustc/tests + target-specific differential + | + independent replay +~~~ + +MIR is an **input semantic view**; MLIR may be an optional **downstream representation**. Datalog and egglog are parallel reasoning views over shared native facts. Tracert follows all of them; it is not a single later pass. None is a mandatory hot dependency. + +## 2. Minimal graph contract (conceptual, not new ABI) + +**Node identities:** RepoIdentity, CargoCrateInstance (revision, features, target triple, rustc build), SourceDefId, SourceCallsiteId, MIRBodyId, BasicBlockId, PlaceId, ValueVersionId, TraitImplId, Method/ClassId, RuleId, ProofId and RecipeId. An identical label or source line number across builds does not establish identity. + +**Edge families:** +- DEFINES / CALLS / DISPATCH_POSSIBILITY / IMPLEMENTS / CAPTURES / CONSTRAINS_TRAIT +- CFG_NEXT / DEF_USE / BORROWS / REBORROWS / MOVES / DROPS / ALIASES_POSSIBLY +- DEPENDS_ON / READS / WRITES / MAY_PANIC / HAS_EFFECT / LOWERS_TO +- DERIVED_BY / USES_LAW / PROOF_FOR / VALIDATED_BY / REFUSED_FOR / REPLAYED_AT + +**Evidence grades:** observed source, compiler-derived, logically derived, hypothesis, tested, independently verified; use SAG aligned Witnessed/Refuted/Undetermined/Conflicted plus separate stale/unsupported markers. These are not interchangeable. A call edge (possibly dynamic) does not imply an observed call. An unexamined region is UNKNOWN, not FALSE. + +**Physical interpretation:** DR64² / DR256² are bounded local relationship views; proposed DR64³ and any DRⁿ are typed, factorized logical axes, never compulsory dense allocations. The global identity and original source remain in their owners; DR ordinals are local witnessed coordinates. SoA holds canonical values. Do not create owned pairs/row lists for hot folds or resurrect withdrawn method tables. Keep masks, bag multiplicity, SQL K3 validity and epistemic evidence distinct. + +**Higher order:** closure/function values require signature, captures, trait-bound dispatch and monomorphization/dynamic resolution status. Trait method bodies, callsites, and possible callees must not collapse into one identity. MIR lifetimes and Rust borrow checking take precedence over labels or LLM-inferred aliasing. + +## 3. Rule engines, extraction and proof separation + +| Tool | Candidate responsibility | NOT claimed | +|---|---|---| +| rust-analyzer | source-anchored syntax/HIR, symbol/type/reference maps and source edits | target-accurate MIR execution proof | +| rustc MIR / Charon | CFG, places, borrows, drops, operations and semantic witness under pinned toolchain | lossless reproduction of all Rust source formatting, comprehensive unsafe semantics | +| AdaWorldAPI/ruff | independent supported SPO structure/codegen source crosswalk | Rust binary equivalence, mandatory Cargo dependency of lance-graph | +| Datalog / Ascent | cold declarative relations, SCC, reachability, guarded selection, rule metadata | automatic DR-native folds from stock BYODS or arbitrary negation | +| Datafrog | independent fixed-point differential/recursion oracle | production graph executor or semantic proof | +| Prolog | optional goal-directed exploration / diagnostics | independent oracle when derived from same evidence | +| egglog | typed congruence and equational candidate exploration | independent validation of underlying axioms | +| eggcc-style | choose candidate extraction with explicit effect constraints | proof that a transform preserves all Rust semantics | +| MLIR | optional vector/LLVM/GPU lowering experiment | replacement for MIR ownership/borrow truth | + +Direct native execution remains Quack-bound R2IL router → supported direct/composed ndarray SIMD or mask-risc; ClassId route chosen once, not per fold. Egglog and Datalog do not execute in the hot path. + +**Three independent warrants:** (1) sourced method/graph facts, (2) admissible mathematical law with independently checked proof where required, (3) current binding, authority and executable target parity. A proof of algebraic equality cannot authorize a source edit or an external effect. + +## 4. Concrete first fixture (read-only) + +Source shape: a Rust iterator count of values satisfying a pure unsigned scalar predicate, and a second fixture that counts a set of Boolean DR mask positions. + +Candidate (not asserted as a universally valid source rewrite): + +~~~text +count(filter(P, X)) popcount(mask(P, X)) +~~~ + +For the narrow pure/read-only, exactly-once and compatible-integer case, compare a Rust scalar oracle, an explicitly prepared ndarray mask+popcount path, and an independently evaluated relational query. Keep two source identities: original source and proposed rewrite; neither replaces the other during the proof. + +Capture and disposition: exact type/trait implementation, closure capture, predicate evaluation count, panic behavior, overflow/range, provenance of the mask, snapshot and target. The rule engine may find this candidate even when the legal response is REFUSE. Negative examples are essential. + +## 5. Falsification matrix, preregistered + +| Gate | Adversarial case | Required behavior | +|---|---|---| +| F01 | same-named symbol across crates/feature sets/revisions | distinct identities; no cross-build evidence merge | +| F02 | generic Fn closure captures mutable state | no pure-count fusion and no predicate-call elision | +| F03 | predicate can panic / integer overflow / eager evaluation differs | refuse unproven reordering, preserve observable evaluation | +| F04 | trait dispatch unresolved or changed impl | possible-call edge not treated as confirmed callee | +| F05 | borrow/move/drop/unsafe/volatile/atomic ordering | effects remain ordered; unsupported semantics typed refusal | +| F06 | a missing edge in incomplete MIR/Ruff coverage | UNKNOWN not FALSE; no closed-world claim | +| F07 | DR 64/256 same ordinal in different frames/scopes | stale/foreign coordinates refused | +| F08 | Boolean DISTINCT count vs SQL K3 NULL / BAG duplicates | distinct typed contracts; no false equivalence | +| F09 | egglog equality derived under wrong law assumptions, forged proof text, wrong ABI | refused; external independent checker required before certified status | +| F10 | cold optimized path compared against unfair baseline / identical source oracle | no performance win or correctness claim | +| F11 | changed source SHA while retaining old recipe/callsite ids | invalidation or independently established rebinding | +| F12 | MLIR lower is successful but changes signed zero, NaN, FMA or rounding | parity failure; no source rewrite | +| F13 | graph candidate is applied without operator/source approval | forbidden; ProposedMethod inert | +| F14 | arbitrary generic method invokes dynamic external side effect | no mathematical reduction and no OGAR bypass | +| F15 | fixture passes only with synthetic labels or fabricated AST semantics | evidence grade = unsupported/undetermined; no admission | + +For each implemented gate: preregister counterexample, independent oracle, disable-red-run, fixture/compiler revision and reproducible result. Zero discovered candidates is a permissible result; report it honestly. + +## 6. Staged handoff (this PR is S0 only) + +| D-id | Deliverable | Gate | Owner/status | +|---|---|---|---| +| **D-SAG-6-0** | this additive architecture + prompt + board reference | all scope/authority statuses explicit | docs PR only | +| **D-SAG-6-1** | pinned Rust HIR/MIR/Charon and Ruff capability audit | real source fixtures, unsupported inventory, no new runtime | future read-only audit | +| **D-SAG-6-2** | minimal read-only native Codegraph projection in lab | exact source identity; F01/F04/F06/F07/F11 | separate review/approval | +| **D-SAG-6-3** | logic candidate + independent Datafrog/Ascent oracle | F02/F03/F08/F10/F15 | separate review/approval | +| **D-SAG-6-4** | egglog law, effect-aware extraction, complete traceroute | F05/F09/F13/F14, external proof gap named | separate review/approval | +| **D-SAG-6-5** | opt-in Rust patch/codegen vs optional MLIR cross-check | F03/F05/F12/F13, compilation + target+oracle parity | separate review/approval | + +**Ownership conflict stop:** Check D-SAG capstone, D-RFT/Math Foundry and D-DRMC owners before introducing types, changing proof references or producing source patches. EXO-50 is the communication bus, not a merge/approval authority. No automatic code changes, authorization decisions or writes to source/SoA in S0. + +## 7. Reference ledger (entry points to inspect; status is not proof) + +- [lance-graph #1523](https://github.com/AdaWorldAPI/lance-graph/pull/1523): SAG capstone; D-SAG-1 original method graph reset/withdrawn. +- [AdaWorldAPI/ruff](https://github.com/AdaWorldAPI/ruff): polyglot graph extraction + Rust codegen arms, structural observer only. +- [lance-graph #1693](https://github.com/AdaWorldAPI/lance-graph/pull/1693), [#1694](https://github.com/AdaWorldAPI/lance-graph/pull/1694): replay capsule and guarded math catalogue; lab only, not independent theorem prover. +- [lance-graph #1740](https://github.com/AdaWorldAPI/lance-graph/pull/1740): frame-reused DR recipe lab, independent checker still missing. +- [lance-graph #1752](https://github.com/AdaWorldAPI/lance-graph/pull/1752), [#1753](https://github.com/AdaWorldAPI/lance-graph/pull/1753), [#1755](https://github.com/AdaWorldAPI/lance-graph/pull/1755): native router, binding status and borrowed SoA. +- [lance-graph #1759](https://github.com/AdaWorldAPI/lance-graph/pull/1759): parallel board catch-up; do not amend/reinterpret its status changes. +- External subjects for pinned capability audit: rust-analyzer HIR, rustc MIR, [Charon](https://github.com/AeneasVerif/charon), [Ascent](https://github.com/AdaWorldAPI/ascent), Datafrog, egglog, [eggcc paper](https://rtjoa.com/papers/oopsla26-eggcc.pdf), [MLIR](https://mlir.llvm.org/). + +**D-SAG-6-0 is a design/coordination artifact, NOT a functional codegraph, MIR/MLIR bridge, verified rewrite, executed benchmark, or authorization to merge.** From 1630464e5c01cf77345b8764ddd22e387e0b21f7 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Sun, 25 Oct 2026 01:04:39 +0200 Subject: [PATCH 2/4] docs(D-SAG-6): preregister Rust codegraph math/logic traceroute and agent handoff --- ...ust-codegraph-logic-tracert-claude-code.md | 62 +++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 .claude/prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md diff --git a/.claude/prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md b/.claude/prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md new file mode 100644 index 000000000..8641bbde9 --- /dev/null +++ b/.claude/prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md @@ -0,0 +1,62 @@ +# Claude Code handoff — D-SAG-6 Rust Codegraph → Mathematics → Logic → Tracert + +**Status:** research / implementation handoff only. S0 is DOCUMENTATION, no code authorized. **Canonical plan:** [D-SAG-6](../plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md). **Coordination:** [Linear EXO-50](https://linear.app/exo-red/issue/EXO-50/agent-message-bus-gpt-xgrok-ccsession-id). + +## Mission + +Audit whether **Rust source semantics** can be reflected into a *typed*, versioned, read-only Lance-graph Codegraph and fed to the **existing** RelAlg/Quack/R2IL/egglog Math Foundry for: +1. detecting source-level higher-order pattern candidates through Datalog/Ascent; +2. separately verifying a narrowly admitted mathematical rewrite; +3. emitting a reproducible **Mathe → Logik → Tracert** from compiler source facts to a candidate native recipe; +4. optionally comparing a source patch and an MLIR lowering ONLY after review and separate approval. + +Do not replace Rust MIR with MLIR, make Ruff a Rust semantics authority, or invent new CodeGraph/ProposedMethod/ProofRef systems. The model must preserve Rust evaluation/borrow/drop/effect semantics; syntax similarity is not equivalence. + +## Must read before work + +1. Root **CLAUDE.md** P0 architecture, nanosecond hot fold and cold-compiler reporting exception; check newest main SHA and active PR ownership. +2. SAG [capstone alignment](../plans/sag-capstone-alignment-v1.md); D-SAG-1 withdrawal in [software-awareness-v1](../plans/software-awareness-graph-v1.md); [D-SAG-2 Ruff closed loop](../plans/software-awareness-graph-v2-ruff-ona-closed-loop.md). +3. [Ruff ModelGraph plan](../plans/lance-graph-as-the-modelgraph-v1.md) and AdaWorldAPI/ruff crate graph: ruff_spo_triplet, ruff_r2il, ruff_cpp_codegen, ruff_spo_address. **Ruff has no Cargo edge into lance-graph.** +4. [DR Mathematical Compiler](../plans/dr-mathematical-compiler-v1.md), [Ascent/BYODS cold compiler](../plans/ascent-byods-dr-fold-polyfill-v1.md), [D-NFR](../plans/d-native-repr-contract-v1.md) and [D-NFC](../plans/d-native-first-dependency-correction-v1.md). +5. Source: lance-graph-contract ClassView/set_rules/set_algebra, Quack binder, R2IL router, RelAlg, mask-risc, ndarray SIMD; math foundry #1693/#1694, DR certification #1740, binding #1753/#1755; check current contents rather than relying on plans. +6. External actual-source audits, each pinned to a revision/toolchain before claims: rust-analyzer HIR/rowan, rustc MIR or Charon LLBC, Datafrog, Ascent, egglog, eggcc research, MLIR. Do not declare support from a landing page. + +## Do Phase 0 now if a coding agent picks this up; STOP after report + +**D-SAG-6-1 read-only capability mapping, no code or PR without operator go-ahead:** +- Record SHIPPED / LAB / PROPOSED / MISSING separately for parsing, rust-analyzer source identities, MIR/Charon export (toolchain compatibility), Rust effect/lifetime handling, Ruff crosswalk, DR binding, Datalog planning, egglog proof, independently checked certification, target codegen. +- Pin concrete example Rust sources with closures, trait dispatch and masks; extract only relationships actually witnessed. Name incomplete/unsupported operators. Distinguish callsite, possible dynamic callee and observed call. +- Identify smallest already-owned location for a read-only *projection adapter*; propose typed schema without adding a second store or method registry. Compare existing SAG/Quack/DR types before inventing an alternative. +- Determine which Ascent/Datafrog/Ruff input is **independent** of the candidate under test. No "oracle" based on the same helper. +- Inventory legal source edit path (rust-analyzer text edits or syn/quote only if justified) and optional MLIR path. No source mutation. +- Cross-check the plan's F01–F15 falsifiers. If the correct answer is to PARK (no new math, only aliases), say so. + +## After explicit approval: staged probes, one narrow PR per stage + +**D-SAG-6-2 graph projection:** read-only Rust source/HIR + MIR evidence into typed DR focused facts; coordinate/source seals, target/compiler revisions, captures, trait dispatch. F01/F04/F06/F07/F11 must fail red on injected defect and pass with correct schema. Do not materialize owned tuples in native hot folds. + +**D-SAG-6-3 logic:** one pure predicate-filter-count fixture and one impure captured-closure negative fixture. Datalog/Ascent rules propose candidates; Datafrog or a truly independent Rust oracle checks finite relation answers; include alternative direct SIMD/mask-risc route. F02/F03/F08/F10/F15. + +**D-SAG-6-4 math + Tracert:** canonical RelAlg law under exact domain; egglog candidate/replay where supported, effect-safe extraction only for admitted effects; a traceroute with source revision, HIR/MIR witness, rule, law, proof/checker status, lowering, target result and refusals. Reuse #1693/#1694/#1740 without claiming a full independent proof checker. F05/F09/F13/F14. + +**D-SAG-6-5 opt-in codegen:** if independently admitted, write one minimal Rust source patch on a dedicated branch with operator approval; run rustfmt, cargo check/test and differential tests. Optional MLIR export is a comparative test, not required runtime. Record bit-exact or declared tolerance behavior; F12. + +## Required negative controls + +Same symbol label but different crate features; mutated/moved drop; predicate with a mutable captured counter; possible panic; non-monomorphized trait call; incomplete MIR or unsupported unsafe; source SHA change; changed DR focus; fake proof text; K3 UNKNOWN treated as FALSE; SQL BAG mistaken for DISTINCT; wrapping arithmetic treated as checked; FMA signed-zero/NaN divergence; no-approval attempted source write. Correct response is REFUSE or UNKNOWN, never an invented proof. + +## Trace and report format + +For each derived candidate output: source path + commit + rustc target/features; original span & callsite identity; HIR/MIR body + coverage; typed relation and DR frame; rule ID and premises; admitted law and domain; proof/checker evidence versus replay-only artifact; extraction cost/ABI; native kernel/binding; independent reference answer; measured cold/bind/hot components; refusal cause. Use source links, actual commands and real observations, no speculative speedup. Counterexample tests must be recorded before implementation and disable-red evidence preserved. + +**IMPORTANT**: The operator ruled a cold out-of-fold compiler/oracle cost may be reported in microseconds as informational, not gates. Hot folds retain nanosecond/microsecond P0. A millisecond-scale in-fold result fails; never disguise it as useful runtime throughput. Avoid reintroducing tuple materialization, foreign gather or runtime Datalog interpreters. + +## Handoff/coordination + +- Github PR/board is canonical durable evidence; EXO-50 is **append-only coordination**. Post one new comment using its envelope for each meaningful result or blocking ownership decision. Do not edit earlier session comments or infer ACK from existence. +- D-SAG-6 belongs to the SAG continuation, Math Foundry and D-DRMC owners retain proof/compiler authorities, D-RMAP retains binding and scope, OGAR retains action authorization. No effectful DO method may execute as a learned candidate. +- Check parallel [#1759](https://github.com/AdaWorldAPI/lance-graph/pull/1759), which is only a board catch-up; avoid conflict with its STATUS_BOARD/INTEGRATION_PLANS corrections. +- Report no-code outcome after Phase 0; ask operator before implementing Phase 1+, editing existing source, changing Rust/compiler dependency pins, opening implementation PRs or merging. +- If creating an entry later, use **python3 .claude/tools/entries_index.py --write** then **--check**. Do not hand-edit generated README. Run plan_dids.py, append_only_gate.py, citation_decay.py and project-specific checks where applicable; mark NOT RUN if unavailable. + +**Deliverable at this stage:** a falsifiable gap inventory and a recommendation of the smallest independent read-only adapter, NOT a new compiler, codegraph store or automatic Rust rewrite. From a60992e392f212102b2732ce9b3a0a00919a95f6 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Sun, 25 Oct 2026 01:04:43 +0200 Subject: [PATCH 3/4] docs(board): index proposed D-SAG-6 Codegraph math logic traceroute --- .claude/board/STATUS_BOARD.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index e381fda96..1215fd70e 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,16 @@ +## D-SAG-6 — Rust Codegraph → Mathematics → Logic → Tracert (2026-10-24) + +**Status: S0 PROPOSAL / DOCS ONLY.** Plan: [d-sag-6-rust-codegraph-math-logic-tracert-v1.md](../plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md). Agent prompt: [d-sag-6-rust-codegraph-logic-tracert-claude-code.md](../prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md). Coordination: [EXO-50](https://linear.app/exo-red/issue/EXO-50/agent-message-bus-gpt-xgrok-ccsession-id). Continuation of D-SAG / D-DRMC / Ascent-BYODS, **not** a revived SoftwareGraph, separate registry, runtime or new proof authority. Parallel #1759 only reconciles existing board status. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-SAG-6-0** | authority/ownership map, Rust Codegraph math/logic traceroute contract, Claude Code prompt | DOCS / PROPOSAL (this PR) | no Rust/Cargo/ABI edits; source/proof/execution authority separated | +| **D-SAG-6-1** | pinned rust-analyzer HIR, rustc MIR/Charon, AdaWorldAPI/ruff fork capability audit | PROPOSED (read-only) | code-backed availability and unsupported inventory; F01–F15 preregistered | +| **D-SAG-6-2** | source-revision-bound typed Rust Codegraph projection to existing DR/SoA/Quack | PROPOSED; separate approval | identity, capture, trait dispatch, sealed-coordinate and stale-source refusals | +| **D-SAG-6-3** | Datalog/Ascent candidates versus Datafrog/independent Rust oracle | PROPOSED; separate approval | pure filter/count vs impure-closure/panic/Bag/K3 controls | +| **D-SAG-6-4** | egglog guarded law + effect-aware extraction + proof/replay traceroute | PROPOSED; separate approval | independent checker gap explicit; no effect reorder or forged proof promotion | +| **D-SAG-6-5** | optional approved Rust source edit and comparative MLIR lowering | PROPOSED; separate approval | rustc/tests/differential target parity; FMA/NaN/signed-zero and effect gates | + ## D-ONNX-NATIVE — ONNX vocabulary over existing native functions (2026-10-23) Plan: `.claude/plans/d-onnx-native-v1.md`. Crate: `crates/lance-graph-onnx` (ALIAS / INLINE only; no dispatch). From 1840579dfd3e2a03a86e3027e7af9d9b411b498c Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Sun, 25 Oct 2026 01:04:47 +0200 Subject: [PATCH 4/4] docs(board): index proposed D-SAG-6 Codegraph math logic traceroute --- .claude/board/INTEGRATION_PLANS.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 155a9bae2..543c913b3 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,9 @@ +## 2026-10-24 — D-SAG-6 Rust Codegraph → Mathematics → Logic → Tracert → `.claude/plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md` + +**Status:** S0 PROPOSAL / DOCUMENTATION ONLY, no code, benchmarks, new compiler, proof certification or source rewrite. **Prompt:** `.claude/prompts/d-sag-6-rust-codegraph-logic-tracert-claude-code.md`. **Handoff:** [Linear EXO-50](https://linear.app/exo-red/issue/EXO-50/agent-message-bus-gpt-xgrok-ccsession-id). + +Rust HIR/MIR (source/semantic input) and the [AdaWorldAPI/ruff](https://github.com/AdaWorldAPI/ruff) polyglot structural crosswalk feed a typed, read-only Codegraph on existing DR/Quack/SoA ownership. Datalog/Ascent/Datafrog analyze logic beside RelAlg/egglog's guarded mathematical transformations; a provenance traceroute links derivations, independent proof-check status, effect-safe extraction and native prepared R2IL/ndarray recipes. MLIR is optional downstream; it does not own Rust semantics. S1+ implementation is separately gated by D-SAG capstone, D-DRMC/Math Foundry and OGAR owners. Parallel #1759 is a distinct board catch-up; no overlap in claims. + ## 2026-10-24 — index catch-up: six ONNX-family plans merged without an index entry (#1745–#1749, #1751) - `d-onnx-relalg-cap-convergence-1745-v1` (#1745), `d-onnx-relalg-s1-s2-semantic-intake-v1` (#1746), `d-dr3-holo-onnx-s3a-s3c-v1` (#1747), `d-onnx-relalg-s3d-physical-shootout-v1` (#1748), `d-onnx-relalg-s4-s5-palette-export-v1` (#1749), `d-optimum-bgz-offline-frontend-v1` (#1751) → `.claude/plans/.md`.