Skip to content
Merged
4 changes: 4 additions & 0 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -92,9 +92,13 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
- **emitted crate partition** — derive the Rust crate layout from the module graph (builds on #6677 derived registration; dissolves the hand-drawn 2-crate split in `stage0_crates.dag`). Shared `CompilationUnit` home with the language-consolidation lane; Rust workflow realization here. → [emitted crate partition design](docs/plans/emitted-crate-partition-design.md)
- **duplicate work = the content-hash qualification of `Materialization`** — the operator's "kill compile→…→recompile" generalized codebase-wide, corrected off a §3 catch: it is NOT a new lens but the qualification step *inside* the spine's `materialize` — the generalization of `std.realization` `reconcile`/`has_collapsible_peer` from the effect-pairwise `create_double_init_collapsible` key to a `ComputationIdentity` lattice (`StructurallyIdentical | NormalizedIdentical | ExtensionallyIdentical{bound} | IdentityUnknown{cause}`, mirroring `DescentEvidence`). Two coupled halves (assembly line): **Half A** = materialization describes the result of *all* computation (spine lane, `materialize`/FLAG D — not just `RealizedStep` effects); **Half B** = the generalized qualifier + multiplicity-source axis (fork/placement/runtime/scope) that picks the fix (this lane). `.dag` boundedness demotes the "undecidable" residue: `IdentityUnknown` is never permanent — it is a *typed, located* `MissingConcept | MissingEnforcement | BoundUnmodeled` debt (the undecidability often *is* a §3 fork), so the lens's product is the located root, not the symptom (§6 moat). Placement-grain flagship (CI release build across 3 `needs:[]` jobs → 1 violation, rewire → clean) proven green-by-execution. No S2 dep; couples to the materialization model. → [duplicate-work design](docs/plans/duplicate-work-graph-lens-design.md)
- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). FLAGs D/E/F operator-SIGNED 2026-07-10 and the within-body FACT layer LANDED (#6443): one sugar rule table (`SugarKey` = surface-atom | production identity, type_alias_rhs migrated as proof), the 3-edge seam Loop (`^loop_carrier_edge`, at-most-one, excluded from the iteration fold in one motion; the lens carrier read is a named-edge lookup, the surface navigation deleted), the lexeme-stamped let binder, and the lens definition closure (`let grown = acc` a PROVEN suspect, transitively; pure-literal RHS decides clean; unbound RHS still refuses — the may_alias false-alarm class is dead; `^fold_accumulator_unread` narrowed to the named-step residue, a Stage-B callee-resolution fact). FLAG D condition: the binding-key re-grounding is REQUIRED cleanup before the feature closes. Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions); the fn_decl→Arrow producer rows + scaffold dissolution are gated on the namespace lane's containment `SymbolIndex`, staged behind a typed wrapper-retained frontier (lowered | wrapper-retained{cause}, counted, corpus stays green). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)
- **Rc-ownership wrap-decision — the emitter's §5 fail-open made a construction predicate.** Self-emit for the Rc-heavy core modules (`04_infer`, `06_translate`, `05_emit*` — 100+ `Rc<` sites each in the seed) is blocked by a latent fail-open that silently wraps every `shared_types` member in `Rc<T>`; the fix is ONE structural wrap-decision predicate (derived from ownership facts, never a string-scan of `Rc::new(`) so the bad wrap is unwritable. Gates the deep-emitter self-host lane (Weak → Strong Self Host). → [Rc-ownership wrap-decision design](docs/plans/rc-ownership-wrap-decision-design.md)
- **witness realization — the v2 execution path.** Emit witnesses to native code (Rust now; C a row-policy option, §7) and use realization/materialization to schedule the runs; the dependency-ordered work that discharges the v2 memory-control findings, none of it gated on self-hosting. → [witness realization plan](docs/plans/witness-realization-plan.md) (findings it discharges: [v2 memory-control audit](docs/plans/v2-memory-control-audit.md))
- **machine-shape orthogonal scheduling — one realization kernel over faithfully modeled machine facts, with locality (§2).** DRAFT for review; model-before-implement, each phase names its trigger. Its authority transfers to the std/extdeps carriers it names when Phase 1 lands, at which point this md dissolves into a registered `gunbc.plan.Plan` row (§6). → [machine-shape scheduling design](docs/plans/machine-shape-orthogonal-scheduling.md)
- **namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* ("own declarations ∪ direct import lists" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T{a}` → `a` *is* `T.a`; `T{a{a}}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = "the containment tree materialized" (`type-env-single-authority`, lively-raven lane), gated on loyal-heron's scaling receipt before any resolver surgery; `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md)
- **fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile<M,K>` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added/Modified → upsert, Removed → teardown-or-refuse, Unchanged → noop (absence of a hunk). A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 teardown-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberTeardownRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md)
- **effect grants over namespaces — dissolve `Hermetic | Wet` into (frame × verb × subtree).** The 2-valued `Hermetic | Wet` enum conflates four axes (input closure / replayability, output reach / interference, handler binding, selection eligibility) — a §3 state-space conflation with proto-envelopes already forked (the hand-rolled `workspace_root` containment gate, `std.resources.ResourceHandle`, `AuthScope`, `LiveTreeDisposition`). End shape (§3, cited not minted): an effect target is a position in a containment tree that already exists — filesystem paths, URIs, `/proc`, service-operation paths, and the unifying case **code names themselves** (the containment tree the namespace-resolution lane makes the single naming authority); permission is a grant of (verb × subtree) attached to a `Frame`; admissibility is the namespace prefix relation — the same `⊑` the resolver walks, content-addressing hashes, and termination reads, so effects become the **fourth consumer** of the one containment structure. Dispatch checks the envelope fail-closed (`EffectOutsideGrant`, a typed/located/counted refusal, never a silent widen — §5); *replayable* / *isolated* / `LiveTreeDisposition` become **derived** projections, and `Hermetic | Wet | Record` survive only as named envelope presets, deleted at the end. Frame-containment is graded on the §5 construction/validation axis (`LifecycleByConstruction` vs `LifecycleByConvention`). No code lands from the design doc; the FLAG-A interim is the only near-term consumer. → [effect-namespace-grants design](docs/plans/effect-namespace-grants.md)
- **shell → intent: the intent layer is language-blind (operator-aligned 2026-07-17).** §3/§4 restated for the shell case: the `.dag` intent may not name a target language — a workflow is an ordinary dependency graph over modeled operations (§4: a program is `Node`+`Edge`), and rendering it to bash is a separate, target-parametrized concern, so bash appears exactly where Rust does (its grammar spec `src/v2/extdeps/languages/bash.dag` + the emit rows) and NOWHERE in the intent (operator: *the intent IS the `.dag` graph*; `src/v2/std/orchestration.dag` `Pipeline` is optional sugar for linear-orchestration graphs, never the authority). Two distinct downstream layers, not to be conflated: **emit** (§4 — `emit(intent, Bash)`, one grammar read backward, target as a *parameter*) and **realization** (§2 — pure-spec → host-effect, N transports `LocalShell`/`SshShell`, `dag/gunbc/host_effect_realize.dag`) — emit renders surface, realization effects a host, and realization consumes emit's output. **Invariant (enforceable, not aspirational):** the intent imports no language-construction vocab (`bash_build`, `bash_command_fold_serialize`, the `ShellStmt`/`ShellWord`/`ShellProgram` coproduct, `serialize_bash`) — that vocab is emit-internal; `src/v2/lens/realization_vocabulary_containment.dag` **generalized** with the intent layer in scope, green = *conforms to §3/§4* (the natural `StandingIntent` home). **Residual (2026-07-17, operator-flagged):** two live classes — (1) raw `concat(...)` shell strings (`dag/gunbc/ci_spec.dag` `gunbc_ci_deploy_invoke` — UNTOUCHED by the `bash_build` migration, which only migrated the `ShellStmt`/`program.dag` consumers) and (2) structured-but-still-bash (`src/v2/workflow/floor_diff_observe.dag` `floor_git_diff_unified_stmts`/`floor_serialize_program`) — census counts ~110 raw-`concat` shell fns + ~9 structured sites across ~50 files (bulk in `dag/gunbc/**`; `dag/std`/`src/v2/lens`/`src/v2/compiler` clean), collapsing to ~10 operation families (gunbc-run · source-root flags · git · cargo/rustup/tar · deploy-preflight · live_deploy · install · systemd read-back · githooks · curl) — so it is ~10 operations to model, not 110 problems. **Phases:** 0 sidecar delete (in flight — PR-A/PR-B merged, PR-C/PR-D queued) → 1 complete the agnostic emit (`Pipeline` bounded-poll/`While`, general `Retry` — the gap that pushed workflows to `bash_build`) → 2 model the operations with transports (`git.diff`, the `gunbc run` invocation, unit upsert, readiness-poll — bash-CLI as one handler of N) → 3 migrate the intent off shell → wall green throughout. Flagship: `git.diff` via `floor_diff_observe`, end-to-end intent→emit→realization. Couples to `dag/gunbc/host_effect.dag` `ShellCommand{script}` — the same bash-shaped hole one layer down (the fleet-reconcile spine's realization), which should become *run this operation* with bash-rendering downstream, not a deepened `ShellCommand{script}`. → [shell → intent design](docs/plans/shell-intent-emit-realization-design.md)

## Building & checks

Expand Down
Loading
Loading