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
113 changes: 113 additions & 0 deletions docs/design-brand-phase2-cross-module.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
# Design: Cross-Module Identity at Scale — brand phase 2 (TODO A.2)

> **Status: DESIGN — completes the partially-designed phase 2.** Phase 1 (the `binding_id`
> side channel: ctrl#4579 + Amendment 4 #4587, impl gunbc#4581 — **out-of-clone**, cited per
> operator report) stamps declaration identity within a single resolved graph. Phase 2 is
> identity **across modules**: same-spelling declarations in different modules, imports,
> re-exports, and a multi-module compile of the compiler's own corpus (self-host breadth).
> Field/equality policy authority: `design-node-identity-channels.md` — this design lands

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: This makes design-node-identity-channels.md the field/equality authority, but git ls-tree origin/main -- docs/design-node-identity-channels.md returns no blob and the file is not in this PR, so the identity policy is not reviewable (INVARIANTS P2).

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Re-verified against origin/main: git ls-tree origin/main -- docs/design-node-identity-channels.md returns blob a1b08ea1558970a80bc11ee725725297ff95d495 — the file exists on main (landed in the #4605 squash, 1d68a2c). It is not in this PR because it is already merged; the authority reference resolves. Same mis-grounding pattern as the two refuted threads on #4605 (files claimed absent that ls-tree finds at the base) — the review tooling's checkout/ref looks stale. No doc change needed.


Generated by Claude Code

> through its table, rule 1 (#4581 defines the channel; phase 2 rides it).

## 1. Problem

Self-host means compiling `src/v4/**` as one multi-module corpus — hundreds of modules with
heavy same-spelling reuse (`Outcome`, `Node`, `Witness` declared once, imported everywhere;
plus genuine same-spelling *distinct* declarations across modules). Phase 1 makes identity a
stamped fact instead of a spelling within one graph. The phase-2 questions:

1. Do two same-spelled declarations in different modules get **distinct** identities by
construction?
2. Do imports and re-exports **reference** identity rather than re-minting or re-deriving it
from spelling at the module boundary (the boundary is where spelling-joins sneak back)?
3. Is identity **deterministic across the corpus** — independent of module admission order —
so DB-8 and the self-host fixed point don't inherit order-dependence through ids?

## 2. What already exists (M9 DFS)

| Piece | Where | Role |
|---|---|---|
| Cross-file admission machinery: `Import`, `ImportVisibility`, `ResolutionSubject`, `Admission`, `AdmittedSubject`, `AdmissionState`, module-root validation | `src/v4/compiler/03_name_resolve.dag` (T-28-B) | **the seam**: admission is where cross-module references resolve — identity must ride through it as a fact |
| Single-file use→def resolution (canonical-spelling substitution today) | `03_resolve.dag` (K-1) | phase-1's stamping site; phase 2 extends what admission *carries*, not how K-1 works |
| `QualifiedName = FreeMonoid<Symbol>` | `std/qualified_name.dag` | the declared identifier of a module/declaration — the minting key's first half |
| `binding_id` channel: allocator + stamping seam + equality participation (**YES**) | #4581 (out-of-clone impl) + `design-node-identity-channels.md` | the carrier; phase 2 adds no second identity vocabulary |
| Allocator-determinism obligation | `design-node-identity-channels.md` rule 5 | phase 2 is where this obligation **bites** (§4.3) |
| Consumers: A3/A4 call-arg checks (#4533/#4554), the T-9 BindsTo rider, the termination call graph, COMPREP callee refs | landed/queued | everything that reads identity gets cross-module correctness for free if §4 holds |

## 3. Principles (short, because phase 1 did the hard part)

- **Minting is per-declaration, at the declaring module, exactly once.** Identity =
minted at the declaration site keyed by (module `QualifiedName`, declaration). Two
same-spelled declarations in different modules get distinct ids *by construction* —
question 1 needs no checking pass, only the rule that **nothing else mints**.
- **Imports reference; re-exports preserve.** An import binds a local spelling to a foreign
`binding_id` through `Admission`/`AdmittedSubject` — the admitted subject carries the id,
so post-admission resolution never consults spelling across the boundary (the cross-module
twin of phase 1's intra-graph rule). A re-export forwards the same id (no re-mint); an
alias declared *as a new type* mints fresh — that distinction is exactly the brand rules,
unchanged, applied at module boundaries.
- **No spelling-joins at boundaries, enforced.** The phase-2 failure mode is a consumer
"temporarily" matching qualified-name text to connect modules. Same verdict as the
termination audit gave intra-graph: refused; the admission carrier is the only path.

## 4. Design

### 4.1 Carry identity through admission
`AdmittedSubject` (or its successor in the T-28-B shape) gains the foreign declaration's
`binding_id` as a typed fact populated at admission time. Downstream (`04_infer`
call-arg checks, T-9 BindsTo facts, COMPREP callee refs) read the id off the admitted
subject — one carrier, every cross-module consumer.

### 4.2 Same-spelling distinctness is then a theorem, with one claim guarding it
Mint-once + reference-through-admission ⇒ distinct declarations have distinct ids
regardless of spelling. The corpus-scale claim (§5) exists to catch *regressions of the
rule* (someone minting at an import site), not to verify arithmetic.

### 4.3 Determinism across the corpus (the load-bearing decision — escalated)
A sequential graph-global allocator makes ids a function of **module admission order**;
order-dependence then leaks into everything ids touch (equality, hashes, emitted
artifacts), violating the channel authority's rule 5 and threatening DB-8/fixed-point.
Two compliant options:

- **(a) Canonicalized allocation:** keep the phase-1 allocator, but allocate in a declared
canonical corpus order (sorted module `QualifiedName`, then declaration order). Cheap,
keeps #4581 unchanged; the canonical order becomes one more declared fact.
- **(b) Content-derived ids:** id = stable hash of (module `QualifiedName`, declaration
path) — order-independent by construction, no allocator state; but it changes #4581's
mechanism and id equality semantics (collision posture must be stated).

**Recommendation: (a)** for phase 2 — it honors fewer-variants, leaves the building #4581
intact, and the canonical order is checkable. (b) remains the dissolution target if the
canonical-order fact ever proves fragile. **Operator ruling requested** (it touches the
in-flight #4581).

### 4.4 What phase 2 explicitly does not do
No cross-*compile* identity stability (a fresh compile may re-mint; consumers are
per-compile — same scoping as PROV's occurrence ids, Q-P1). No global registry file, no
identity persistence. If incremental compilation later needs stable ids, that is a new
consumer arriving with its own design.

## 5. Consumers and minimal slice (E-10)

- **Consumers (exist):** the A3 call-arg suite (its cross-module case is currently the
PD-3-DOGFOOD gap — phase 2 is what makes un-skipping the compiler's own modules sound);
the T-9 BindsTo rider (cross-module edges need foreign ids); self-host stage B
(per-module artifact comparison needs deterministic ids in anything emitted).
- **Minimal slice:** two fixture modules each declaring same-spelled `type Token`, a third
importing both under aliases — claims: **green** — distinct ids; cross-module call-arg
check rejects passing one for the other (A3, across the boundary, by execution);
**green** — a re-export carries the original id (witnessed equal); **red
(discriminating)** — a deliberate spelling-join shim at admission accepts the brand-twin,
proving the claim catches the regression class; **red** — two corpus orders produce
identical ids under §4.3(a)'s canonical order (order-perturbation claim).

## 6. Open questions
- **Q-B2-1 — §4.3 ruling**: canonicalized allocator (rec) vs content-derived ids.
- **Q-B2-2 — visibility interaction**: does `ImportVisibility` affect id propagation
(private declarations' ids crossing via re-export chains)? Recommend ids propagate only
where admission admits — visibility stays the admission question it already is.
- **Q-B2-3 — phase-1 doc reconciliation**: ctrl#4579/#4587 predate this doc; their next
amendment should cite it (and the channel authority) as phase-2's home.

## 7. Non-goals
Persistent/incremental identity, cross-repo identity, any change to phase-1 stamping
semantics, any second identity field (the channel table governs).
84 changes: 84 additions & 0 deletions docs/design-compute-dispatch.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
# Design: Compute Dispatch — running the selected work (fabric brief D, gated)

> **Status: DESIGN — gated dependency statement + bridge contract.** Brief D of the
> compute-fabric set. A/B/C are pure model and prototypable now; D is where the fabric
> touches a runtime, so most of D is **deliberately deferred to the runtime-architecture
> design** (open decision #4) — this doc fixes the boundary, the bridge, and the bridge's
> dissolution trigger, and enumerates what the runtime design must answer for D. It does
> not design execution semantics.

## 1. The pipeline position

`ComputeRequest` (A) → `compute_select` (C) → `SelectionResult` → **dispatch**: bind the
work to the selected provider's transport facts (B) and run it, producing typed receipts.
Pieces already landed or in flight:

| Piece | Where | State |
|---|---|---|
| Runnable-frontier scheduler (`RunnableFrontier`, `SchedulerPlan`, readiness folds) | `src/v4/workflow/scheduler.dag` (#4566) | landed — decides *what is ready*, provider-agnostic |
| Executor batching | #4603 | in flight (rebasing) — decides *in what order/groups* |
| Host-run receipts (`ExecutionEvidence` host arm, `EmitHostRunReceipt`) | `src/v4/std/host_run.dag`; ROADMAP T-22 bridge row | landed receipt carriers — dispatch reuses these, not a new receipt family |
| **Dispatcher** — fire work on the chosen backend via its transport facts | nowhere | **the gap D names** |

## 2. The bridge (the operator-proposed shape, made contractual)

Wave 1 dispatch rides the existing execution substrate instead of waiting for the v4
runtime: **daglang emits the selected task graph; the `OaaS_v2` runner executes it.** This
is the unify direction (B §5) and it rides v2's working emission — it does **not** need
COMPREP. Per P5, a bridge is only legitimate with its receipts and trigger fixed up front:

- **Contract:** the bridge consumes `SelectionResult` + the provider's transport facts and
emits the runner's task-graph input (proto/JSON at the boundary — a boundary artifact,
not a parallel IR authority). Results return as `host_run`-family receipts attributed to
the request, so claims can assert on dispatch outcomes with the same typed-verdict
discipline as everything else.
- **Boundary discipline inherited verbatim** (INVARIANTS P2 host-process boundary (a)–(e)):
typed outcomes not string probes; setup failure ≠ logical exit; **no implicit
re-execution** — a failed or contract-divergent dispatch (B §4) surfaces fail-closed, and
re-selection (go ask C again, excluding the offender) is an **explicit, bounded, declared
policy step**, never a hidden retry.
- **Dissolution trigger:** the bridge deletes when the runtime-architecture design's native
dispatch path executes the same task graph with the same receipts — tracked the same way
as ROADMAP's T-22 eval-host bridge row (and it should land *as* a row in that table).
- **Out-of-clone honesty:** `OaaS_v2` is not reachable from this session; the task-graph
input format is operator-supplied grounding to be pinned (schema cited in the bridge PR)
when that repo is in scope.

## 3. What the runtime-architecture design must answer for D (its input spec)

D is the first concrete consumer of decision #4's design; these are the questions it needs
answered, so the runtime design can be checked against a real consumer rather than written
in the abstract (the seesaw discipline):

1. **Effects/IO model at the dispatch boundary** — how a dispatched workload's declared
effect shape (A's workload facts) becomes an enforced contract rather than a description:
what the runtime checks before/around execution, and what receipt proves it.
2. **Preemption semantics** — what `Preemptible` means operationally: checkpoint/resume
hooks, re-execution windows, and how the obligation discharged at selection time (C §3)
is *kept honest* at runtime.
3. **Receipt taxonomy** — whether `host_run.dag`'s evidence arms suffice for remote
dispatch (exit/setup/divergence/preemption) or need bounded extension — extension lands
in `std/host_run.dag`, single authority, not a dispatcher-private result enum.
4. **Cancellation and bounded waiting** — dispatch is the first place the system waits on
external completion; the runtime design owns how waiting stays bounded/fail-closed
(P4's premise does not get an exception because the loop is "just polling").
5. **Re-selection policy shape** — the explicit declared form of "provider diverged, pick
the next" (count-bounded, policy-cited, receipt-leaving), so it exists as data, not as a
retry loop someone writes under pressure.

## 4. Consumers and slice (E-10) — gated, with one honest interim

The real slice is: dispatch the A+B+C homelab selection — a trivial containerized workload
— through the bridge, receipts asserted by a `TestClaim` (green), plus the discriminating
red: a workload whose declared capability the homelab fixture *doesn't* offer never
dispatches (refused at C; the claim proves nothing leaks past a refusal into execution).
This slice is **gated on**: the runtime-architecture design (for §3's answers, even in
bridge form: items 3 and 5 are needed immediately), the `OaaS_v2` schema pin, and a session
scope that can see it. Until those, D correctly stays a dependency statement — building a
dispatcher ahead of them would be the spec-without-execution trap with a network attached.

## 5. Non-goals

Execution semantics (runtime design's), autoscaling/candidate generation (excluded by C's
closedness), secrets handling (transport facts name mechanisms only), multi-request
placement (Q-PS2), and any second receipt vocabulary.
Loading
Loading