Skip to content

Add cloud resource + secret modeling with DAG upsert patterns - #5

Closed
briansrls wants to merge 1 commit into
mainfrom
claude/cloud-resource-upserts-7DDP1
Closed

briansrls wants to merge 1 commit into
mainfrom
claude/cloud-resource-upserts-7DDP1

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Introduces typed cloud resource modeling (GCP, AWS) and secret reference system for idempotent resource provisioning via DAG upserts.

Transport layer (core/ir):

  • cloud/mod.rs: CloudProvider, CloudResource, CloudResourceState
  • cloud/gcp.rs: GcpProject, GcpResource (bucket, SA, secret, pubsub, artifact registry), GcpWifConfig for Workload Identity Federation
  • cloud/aws.rs: AwsAccount, AwsResource (S3, IAM role, secrets manager, ECR), AwsOidcConfig for GitHub Actions OIDC federation
  • secret.rs: SecretRef, SecretSource, SecretFederation, SecretRequirements with federation-first design (no static keys in DAG)

GitHub Actions integration:

  • AWS OIDC integration (aws-actions/configure-aws-credentials@v4)
  • GitHubSecret type for declaring required repository secrets
  • Standard secret catalog (GCP WIF, AWS OIDC role ARN)
  • WorkflowConfig.required_secrets for secret dependency tracking

Resource model:

  • ResourceId::cloud() and ResourceId::secret() constructors
  • ResourceId::from_cloud_resource() for typed conversion

gunbc-dag workspace:

  • CloudOp enum in WorkspaceOp for cloud upsert phases
  • cloud_upsert SubDag using UpsertBuilder (Check → Create → Resolve)
  • Integrated into workspace DAG composition

https://claude.ai/code/session_01BueK16sY3G3hQKvgfNWXPW

Introduces typed cloud resource modeling (GCP, AWS) and secret
reference system for idempotent resource provisioning via DAG upserts.

Transport layer (core/ir):
- cloud/mod.rs: CloudProvider, CloudResource, CloudResourceState
- cloud/gcp.rs: GcpProject, GcpResource (bucket, SA, secret, pubsub,
  artifact registry), GcpWifConfig for Workload Identity Federation
- cloud/aws.rs: AwsAccount, AwsResource (S3, IAM role, secrets manager,
  ECR), AwsOidcConfig for GitHub Actions OIDC federation
- secret.rs: SecretRef, SecretSource, SecretFederation, SecretRequirements
  with federation-first design (no static keys in DAG)

GitHub Actions integration:
- AWS OIDC integration (aws-actions/configure-aws-credentials@v4)
- GitHubSecret type for declaring required repository secrets
- Standard secret catalog (GCP WIF, AWS OIDC role ARN)
- WorkflowConfig.required_secrets for secret dependency tracking

Resource model:
- ResourceId::cloud() and ResourceId::secret() constructors
- ResourceId::from_cloud_resource() for typed conversion

gunbc-dag workspace:
- CloudOp enum in WorkspaceOp for cloud upsert phases
- cloud_upsert SubDag using UpsertBuilder (Check → Create → Resolve)
- Integrated into workspace DAG composition

https://claude.ai/code/session_01BueK16sY3G3hQKvgfNWXPW

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1a2f2f48d8

ℹ️ 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".

Comment on lines +118 to +122
// Cloud ops are pure data transformations
WorkspaceOp::Cloud(_op) => {
// CloudOp nodes build/parse shell commands for cloud CLIs.
// Execution is delegated to TransportOps::Execute nodes.
Ok(inputs)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P1 Badge Emit required outputs from CloudOp nodes

The CloudOp branch currently just returns the input map unchanged, but the upsert SubDag expects the check phase to emit an exists output for the create guard and the resolve phase to emit a handle output. With no exists output, the executor skips the create node (missing guarded input causes a skip), and resolve never produces the handle, so cloud_upsert will never create resources and won’t return a handle when the workspace DAG is executed. The CloudOp implementations need to populate the expected ports (or add transport nodes that do) for the upsert pattern to work.

Useful? React with 👍 / 👎.

Comment on lines +342 to +345
pub fn required_resources(&self) -> Vec<AwsResource> {
vec![AwsResource::IamRole {
name: self.role_name.clone(),
assume_role_policy: self.trust_policy(),

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Include the IAM OIDC provider in AWS required_resources

The required_resources helper is documented as the set of resources that must exist for OIDC auth to work, but it only returns the IAM role. In a fresh AWS account, the GitHub OIDC provider (token.actions.githubusercontent.com) is also required for STS to accept the token; if the caller upserts only this list, OIDC auth will still fail unless the provider was created elsewhere. This should either model and include the OIDC provider resource or make the omission explicit.

Useful? React with 👍 / 👎.

Comment on lines +366 to +370
pub fn required_resources(&self) -> Vec<GcpResource> {
vec![
GcpResource::ServiceAccount {
id: self.service_account_id.clone(),
display_name: format!("WIF SA for {}", self.pool_id),

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Add WIF pool/provider to GCP required_resources

The WIF required_resources currently lists only the service account, but Workload Identity Federation also depends on the workload identity pool and provider referenced by provider_full_name(). If a caller uses this list to bootstrap a new GCP project, authentication will still fail because the pool/provider are missing. These resources should be included (once modeled) or the helper should not claim to be sufficient for WIF.

Useful? React with 👍 / 👎.

@briansrls briansrls closed this Jan 31, 2026
briansrls pushed a commit that referenced this pull request Feb 3, 2026
…fragility

TODO_hacks.md:
- Hack #5: cardinality Empty tests use concrete empty values (false/0/"")
  not actual absence. BoundaryMocks has no way to represent "absent."
  Blocks meaningful B.3 boundary testing for scalar types.
- Hack #4 amendment: Value::List filter_map silently drops non-string
  elements (separate from catch-all issue).
- Hack #3 note: runtime check() already handles lists correctly;
  codegen to_check_code() just needs to mirror it.
- Notes: typed matchers as finite logic language; Hack #5 priority.

consolidation.md:
- §5: type_id == "List" dual encoding across 4+ locations. Canonical
  model is element type + cardinality. Migration strategy documented.
- §6: Codebase fragility — builder functions as strings (rename-unsafe),
  buck-out/gen in 16 locations (no single constant), CODEGEN_SOURCES
  hardcoded directory list (staleness gap).
- Tasks updated for all new items.

https://claude.ai/code/session_01FcPT2VEZdE1W7QdL7SjJgC
briansrls pushed a commit that referenced this pull request Feb 13, 2026
Addresses feedback from 2026-02-12 PR review across 6 key areas:

1. Fix probe→observer recursion (#1): Intermediate observers are now
   promoted to probes unconditionally (not gated on Exact matchers).
   Tests are seeded from baseline DryRun, so concrete values aren't
   needed. This enables compositional segment testing A→B + B→C.

2. Fix extract_observers() seen/merge bug (#2): NodeExamples with only
   input-dependent matchers (Exact/Contains) no longer suppress valid
   chain-safe matchers from live_expected_outputs for the same node.
   Switched to merge-by-node approach using BTreeMap union.

3. Make gaps fail CI (#3): Coverage gaps now generate a failing
   test_observability_invariant_no_gaps test instead of just a header
   comment. Aligns behavior with the stated invariant.

4. Make lowering failures loud (#4): DAG lowering errors now generate a
   failing test_probe_observer_lowering_failed test instead of silently
   returning None and skipping all chain tests.

5. Seed policy fail-closed (#5/#8): Inverted seed_policy_for_type to
   whitelist known-safe primitive types (String, Bool, Int, etc.) and
   default unknown types to ExplicitSeedRequired. New types and aliases
   no longer silently fall into placeholder generation.

6. Additional hardening:
   - Add input_mocks as a probe source (#6) for DAGs seeded via entry
     input ports
   - Track weak observers (Any/IsRequest/IsResponse) in coverage
     reports (#5) so teams can identify low-value assertions
   - Promoted probes now appear in analysis results
   - ParamType::from(&str) panics on unknown types instead of silently
     defaulting to Str (#9)
   - Int parsing returns ParseError::InvalidInt instead of unwrap_or(0)

https://claude.ai/code/session_014cTfu4arnDzFZCELaR26P4
briansrls pushed a commit that referenced this pull request Mar 1, 2026
…ord, service move, clippy

- Fix #4: Add Value::Json field access support in eval.rs
- Fix #5: Scope validate_no_operation_overlap to freshness-vs-tool intersection only
- Fix #6: Nuanced passthrough enforcement — fail-closed when at least one
  passthrough was wired (partial lowerer gap), fall back to Skipped when zero
  passthroughs were wired (C10 gap)
- Fix #7: Physically move resolve_service.rs from gunbc-dag to
  core/resolve/src/service_ops/service_ops_impl.rs (removes #[path] hack)
- Fix #8: Change RateLimitConfig from sustained_per_minute to
  (requests, window_seconds) for lossless precision
- Hermetic keyword: downgrade from fatal parse error to silently accepted no-op
- Clippy: fix needless borrow and redundant closure in daglang-lower
- Fix shell.dag codegen invocation (--mode=ensure → codegen)
- Update pragma lint allowlists for moved service_ops file

https://claude.ai/code/session_014KdJPWApYizp7SDWHGEsmo
briansrls added a commit that referenced this pull request Mar 23, 2026
…map feedback (#193)

* Remove aspirational tests that describe target state not yet implemented

Delete 4 failing tests and their 5 now-dead helper functions:
- phase6_fold_lambda_uses_reconciled_accumulator_type (R3: fold type refinement)
- phase6_anonymous_record_literal_fails_closed_without_named_type (R2)
- phase6_anonymous_record_literal_does_not_rank_shape_candidates (R2)
- phase6_go_runtime_bridge_methods_keep_method_style_receivers (P1.10)

These tests were written to describe Phase 1 target behavior. They will
be re-added when the corresponding roadmap items (R2, R3, P1.10) land.

Co-authored-by: briansrls <briansrls@gmail.com>

* Fix lingering v2.compiler.pipeline references to v2.compiler.compile

M1 naming cleanup renamed 06_pipeline.dag to compile.dag (module
v2.compiler.compile), but emit_main_rs, emit_main_mod_uses, and
emit_compile_match_arm still referenced the old module name.

Co-authored-by: briansrls <briansrls@gmail.com>

* Align L1 ratchet script categories with ROADMAP.md

Break the connective count into '.connective direct access' and
'Conj/Disj references' (previously double-counted). Add
classify_type_structure as a separate tracked category. Fix
set -euo pipefail + grep exit code interaction via || true.

Script and roadmap table now measure the same 7 categories.
Ratchet set to 374 (current actual total).

Co-authored-by: briansrls <briansrls@gmail.com>

* Clarify milestone status labels: tree-green vs prior-branch vs structural

Feedback #2: readers could not tell which milestones are verified on the
current tree versus achieved on an earlier green branch. Added a status
column and a note explaining that prior-branch milestones re-verify once
stage0 self-compile is green. Updated P3.1 and M1 accordingly.

Co-authored-by: briansrls <briansrls@gmail.com>

* Add InferredNode migration boundary subsection (P1.9)

Feedback #3: the representation change was conceptually clear but the
mechanical migration plan was implicit. Added a table listing every
type, API, and layer that changes when P1.9 lands, plus the ordering
constraint that it must be an atomic commit.

Co-authored-by: briansrls <briansrls@gmail.com>

* Split normalization scope: Phase 1 (hardcoded arity) vs Phase 3 (declarations)

Feedback #4: the roadmap described normalization as populating structural
properties from .dag declarations, but P1.14 defers declaration-driven
population to Phase 3. Made the two scopes explicit so readers see that
Phase 1 normalization uses the hardcoded arity bridge, and Phase 3
normalization replaces it with generic slot substitution.

Co-authored-by: briansrls <briansrls@gmail.com>

* Narrow Phase 1 fabrication gate to Rust bootstrap-critical path

Feedback #5: 'no emit fabrication sites' in the Phase 1 checklist was
overstated — the document defers Go interface{}, Python _unimplemented(),
and Go unhandled-expr to Phase 4. Narrowed the Phase 1 state and exit
criteria to specify 'no silent/fail-open fabrication on the bootstrap-
critical Rust emit path' and explicitly list the Phase 4 deferrals.

Co-authored-by: briansrls <briansrls@gmail.com>

* Sharpen v1 retirement gate and scrambled-name test definition

Feedback #6:
- Phase 3 gate now includes a concrete feature-off proof (build + test
  without v1-bootstrap) rather than just saying 'can be removed.'
- Scrambled-name test explicitly defined as comparing inferred structure
  (typed graph shapes), not emitted artifacts. Emit is excluded because
  it legitimately reads names for target-language identifiers.

Co-authored-by: briansrls <briansrls@gmail.com>

* Add LanguageSpec checklist, DAG artifact schema, and TypeVar name-opacity note

Feedback #7: Phase 4 contracts were named but not specified. Added:
- P4.1 Contract: compact checklist of what belongs in LanguageSpec,
  grouped by purpose, with completeness test and existing values.
- P4.4 Contract: DAG artifact schema (version + modules + diagnostics),
  versioning mechanism, and note that it reuses the existing Value
  serialization format.
- TypeVar name-opacity explanation in generics design: slot names are
  structural placeholders consumed by normalization pre-inference, not
  type identities that inference branches on.

Co-authored-by: briansrls <briansrls@gmail.com>

* R2: Anonymous record tuple index emits compile_error!() for index >= 4

Stopgap: the hardcoded 0-3 index mapping now emits compile_error!()
instead of silently falling back to "0" for higher indices and for
field-not-found. The real fix (proper field access for any arity)
remains a backlog item.

Co-authored-by: briansrls <briansrls@gmail.com>

* R4: map_insert reads key type from actual argument instead of hardcoding String

The ExprCall bridge path for map_insert on a bare Map receiver now
reads the key type from the first argument (remaining |> first) rather
than fabricating leaf_node(name: "String"). The leaf_node fallback
remains only for the unreachable None branch (count >= 2 guard).

Co-authored-by: briansrls <briansrls@gmail.com>

* R3: Extract shared refine_collection_result_type for map/flat_map/fold

Both ExprCall (bridge path) and ExprMethodCall computed map/flat_map/fold
result types through independent inline blocks (~20 lines each). Extracted
into a single refine_collection_result_type helper that both paths call.

The ExprCall path still owns map_insert/map_merge refinement (those are
Call-bridge-specific, not duplicated in MethodCall).

Co-authored-by: briansrls <briansrls@gmail.com>

* P1.10: Delete dead runtime_bridge_method_name from core

The function had zero callers — each emitter owns its own
per-target bridge method name rendering (rust_bridge_fn_name,
go_bridge_method_name, py_bridge_method_name). These per-target
maps are legitimate rendering decisions (Go=PascalCase,
Python=with_update for BridgeWith) and remain as-is.

The 4-parallel-map problem is now 3 per-target maps with no
dead shared intermediary.

Co-authored-by: briansrls <briansrls@gmail.com>

* P1.19: Delete duplicate mock extraction; import has_mock_prefix from shared emit

Deleted starts_with_prefix (duplicated has_mock_prefix from 05_emit.dag).
extract_mock_props now uses the imported has_mock_prefix. The Rust-only
copy of mock prefix detection is eliminated.

Co-authored-by: briansrls <briansrls@gmail.com>

* P1.20: Replace testgen fabrication sites with compile_error!()

- emit_simple_expr wildcard: todo!() -> compile_error!()
- emit_data_value_json wildcard: "null" -> {"__error__": ...}
- Default::default() dry-run fallbacks -> compile_error!()

All three silent fabrication sites now fail loudly instead of
producing valid-looking but wrong test/mock code.

Co-authored-by: briansrls <briansrls@gmail.com>

* P1.21: Add testgen verification gate + fix emit_typed_data_value_json fabrication

New test v2_testgen_emits_valid_rust verifies:
- emit_simple_expr uses compile_error!() not todo!()
- dry-run fallbacks use compile_error!() not Default::default()
- mock extraction uses shared has_mock_prefix, not Rust-only duplicate
- shared emit defines TestProjection and extract_test_projections
- emit_data_value_json does not silently fabricate "null"

Also fixes emit_typed_data_value_json wildcard (second copy of the
same fabrication pattern, line 438 in 05_emit.dag).

Co-authored-by: briansrls <briansrls@gmail.com>

* R1: Delete 30-line RC3 emit safety net for Optional field access

field_summary_for_type in inference already correctly produces
OptionalUnwrap for .value on Optional bases. The emit-side
compensation (checking return_type and base_summary for Optional)
was dead code — no test exercises a path where StoredField is
produced for .value on an Optional base. All 116 tests pass.

Co-authored-by: briansrls <briansrls@gmail.com>

* Tighten L1 ratchet 374 -> 372 after R1 emit safety net deletion

Co-authored-by: briansrls <briansrls@gmail.com>

---------

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request Mar 26, 2026
Review feedback from PR #212:

1. Added Bridge Invariant Policy to ROADMAP: any new bridge must
   declare canonical authority, trust boundary, regression test, and
   deletion point. Ratchet increases must justify the safer landing zone.

2. Reframed CollectionKind trust boundary: before resolve_node_bounded,
   collection_kind may be absent; after normalization, if derivable,
   must equal collection_kind_for_name(name). Treat as normalized
   cache, not independent structural truth.

3. Added L3 Token Coherence Invariant: text and shape must stay aligned,
   tokenizer is the single producer, parse_parses_strict is the
   regression gate. This is end-state, not bridge debt.

4. Fixed roadmap variant list: described CollectionKind by category
   rather than stale subset (was missing NonEmptyListKind/NonEmptySetKind).

5. Added assembler fixup #5: duplicate collection_kind in Node literals
   (5 sites in parse.rs).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 1, 2026
…zy_static

Addresses review violation #4 (per-call rebuild overhead):
- Replace registry_for_target() value return with &'static references
  to lazy_static singletons (RUST_REGISTRY, PYTHON_REGISTRY, etc.)
- Registries built once at first access, O(1) thereafter

Also addresses violation #5 (tautological test):
- Delete coercion_parity_with_legacy_type_maps test — target_primitive_type
  now delegates to coerce_primitive_type, making it a self-comparison

Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
briansrls added a commit that referenced this pull request Apr 9, 2026
…MAP (review feedback)

#2 ExprLet scope: annotate_descent gave the value initializer access to
its own binding (inner_ctx applied to all children). Fixed: value sees
outer ctx, only body sees inner_ctx. Ratchet 528→485 (43 false descent
evidence entries eliminated). Regression test added.

#3 ROADMAP sync: KF-8 marked DEFERRED, heap-space marked TODO, binary
search stack corrected to O(1) via TCO (not O(log n)).

#4 Rename: time_bound → recurrence_bound. This is a structural
recurrence bound (work_exponent=0), not full runtime. Full time =
recurrence * per_step_cost.

#5 TCO guarantee: documented that stack O(1) for tail-recursive
functions assumes the target language guarantees tail-call elimination.

365 tests pass, clippy clean, stage0 fixed point verified (485 diagnostics).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
…rate shortcuts

Five-item pass from the latest ChatGPT review. The headline is #5 —
replacing `TypeShape::Primitive(Prim)` with a newtype around
`DeclarationId`. That was an M0-inheritance bug that propagated
through every subsequent substrate refactor unnoticed because Port
machinery was never in scope for the type substrate rework. After
this commit the declaration table is the SINGLE source of type
identity across the v3 compiler; no name-keyed bridge remains.

#1 — Delete `lower_fn_item_pending`; unoverload `ArrowBody::Pending`:
- Block-bodied `fn` items in std/ files no longer create Arrow
  declarations at all. They're skipped in `collect_symbols` (matched
  on `body: None`), so the declaration table never allocates a slot
  for them. `ArrowBody::Pending` reverts to its thesis meaning
  (primitive realization lag only) — no overloaded "user body not
  lowered yet" interpretation.
- Call sites that target block-bodied fns fail-closed at inference
  because no declaration exists with their name.

#2 — Remove `resolve_pending_identifiers` tolerance:
- Split the sweep into a tolerant bootstrap variant and a strict
  user-code variant. Bootstrap tolerates dangling stubs (the
  canonical `dsl/std/*.dag` files reference types like `Tuple` that
  live in std/ modules outside the M1(2.6) load set). User-code
  `lower()` captures a `user_start` snapshot and runs the strict
  variant over stubs allocated during user lowering — every
  Identifier stub at `id >= user_start` must resolve or it's a
  fail-closed `ResolveError`.
- `Atom(Identifier { resolved: None })` now means exactly one thing
  at the user-code boundary: "not yet resolved, pre-sweep".

#3 — Move `allocate_type_params` into `collect_symbols`:
- Pass 1 of lowering (`collect_symbols_phase`) now allocates top-level
  declarations AND their TypeParam children in one pass, populating
  `Declaration.type_params` before any body-lowering runs. Pass 2
  (`lower_bodies_phase`) reads `local_scope_from_parent` instead of
  re-allocating type params.
- Bootstrap is restructured into two phases: all files Phase-1 first
  (so every cross-file template has its type_params slot populated),
  then all files Phase-2 with a shared symbols map rebuilt from the
  post-Phase-1 declaration table. `build_template_arguments` no
  longer hits forward-reference gaps that would have required
  half-valid placeholder parameters for real declarations.
- `fixup_instantiation_template_params` is deleted. The half-valid
  state it repaired no longer exists for real declarations. Stub
  templates (bootstrap dangling refs) still use self-reference
  placeholders, but the stub itself is caught by the sweep and the
  Instantiation stays dead in bootstrap bodies — no repair pass.

#4 — Move `inject_realization_stub` into `#[cfg(test)]`:
- Production `bootstrap()` no longer injects realization declarations.
  The §6.5 smoke test moves into a `#[cfg(test)]` module inside
  `bootstrap.rs` where it builds its own synthetic realization chain
  (TestRealization meta-type, anonymous instance, anonymous
  realization Arrow) without polluting `Dag::new()`.
- `Dag::realization_smoke_arrow` / `set_realization_smoke_arrow`
  deleted — production Dag has no such slot.
- `assert_realization_shape` also moved to test-only.

#5 — Replace `TypeShape::Primitive(Prim)` with newtype over `DeclarationId`:
- `types.rs`: `TypeShape` is now `{ declaration: DeclarationId }`,
  `Copy + Eq + Hash`. `Prim` enum deleted.
- `infer.rs`: `primitive_shape(dag, name)` helper replaces all
  `TypeShape::Primitive(Prim::X)` constructions. Literal node
  dispatch looks up Int/Bool/String by name. `declaration_to_type_shape`
  + `type_shape_to_declaration` deleted — bridging is now a trivial
  `TypeShape::new(decl_id)`. `walk_to_type_shape` stops at the first
  named top-level declaration and returns it as the TypeShape; no
  name-keyed primitive matching.
- `lower.rs`: `lower_type_for_port(ty, dag)` looks up primitive
  names via `declaration_by_name`. `sentinel_type_shape` helper for
  the mark-unresolved fallback.
- `m0_acceptance.rs`: ~25 assertions updated via `primitive_shape(&dag, "X")`.

Test status: 1 unit test (bootstrap realization smoke) + 41 M0 + 3
M1 substrate + 4 real-stdlib parse smoke = **49/49 green**. Clippy
clean.

Name-bridge audit: `grep -rn` in `src/v3/compiler/src/` turns up:
- `OPERATOR_FIELD_MAP` (10 entries, documented dissolution trigger
  to M2 when surface grammar exposes algebra field access directly)
— one localized constant, not a pervasive pattern. No other
name-keyed bridges remain.

Review items now closed:
- FAIL-CLOSED: declaration-graph failures go through phantom ports
  (tolerant in bootstrap, strict in user code)
- ILLEGAL STATES: Pending unoverloaded, ExternalRealization typed
  edge checked at both construction and dispatch, TemplateArgument
  half-valid state eliminated for real templates
- FACTS FLOW FORWARD: declaration identity flows end-to-end from
  bootstrap source through inference to port types; no name-keyed
  collapse at the port boundary
- COPROD DISSOLUTION: ArrowBody back to terminal-2 + scaffold-1
  (Pending only for realization lag); AtomPayload Identifier phase
  coproduct tracked in ROADMAP as M2 substrate refactor
- SINGLE AUTHORITY: `inject_primitive_operators` and
  `inject_realization_stub` both out of production bootstrap; the
  declaration table is the only source of type identity
- API-LEVEL ENFORCEMENT: `lower()` runs the strict sweep before
  returning, so no caller discipline is required

Still deferred (tracked in ROADMAP):
- AtomPayload `Identifier { resolved: Option }` → split variants
  (M2 substrate refactor)
- Flat namespace via `declaration_by_name` (M2 module system)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
Codex review on 5d0fc6d was ✅ blocking:0 overall but flagged two
previously-flagged roadmap items still unresolved: Bool/collection
operator grounding (already tracked as class-5 gaps #1 and #2)
and skip_where_clause refinement fact loss (not yet tracked).

Added class-5 gap #5 describing what's missing (refinement
predicates on type aliases like CommitSha = String where sha1(.)),
why it's hard (requires a new Declaration field, new
RefinementSpec shape, new inference enforcement at value
boundaries), what the options are, and current status (the
skip_where_clause bridge at parse.rs:801 loses the fact
entirely).

Doc-only — no code changes. The PR is green and mergeable; this
just brings DOWNSTREAM_REQUIREMENTS in sync with what codex has
been asking us to track.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
Codex blockers on 636947f: FnExternalBody and Data items compile
cleanly in ordinary user code, leaving ArrowBody::Unparsed and
ValueBody::Unparsed scaffolds in user-range declarations with no
later rejection. `fn foo(x: Int) -> Int { junk }` and
`data foo: Int = { junk }` both round-tripped through compile_to_dag
without a diagnostic, violating THESIS.md static grounding and
modeling-discipline.md principle 1 FAIL-CLOSED.

Context: these scaffolds exist so the std/bootstrap files with
match/record/pipe/lambda bodies can parse cleanly (their bodies
stay as preserved source spans, dissolved when the parser grows
to cover the remaining grammar — DOWNSTREAM_REQUIREMENTS.md
class-5 gaps #3 and #5). Bootstrap-range declarations still need
them. Ordinary user code never should.

Fix: add `reject_user_unparsed_scaffolds(dag, strict_from)` sweep
in lower.rs that walks declarations at id `>= strict_from` (the
user-lowered range after bootstrap) and emits fail-closed
diagnostics for:
- `TypeConnective::Arrow { body: ArrowBody::Unparsed(span), .. }`
- `Declaration.value_body == Some(ValueBody::Unparsed(span))`

Called from `lower()` alongside `resolve_pending_identifiers_strict`.
Bootstrap-range declarations (id < strict_from) are still
tolerated — those scaffolds exist by design until the parser
catches up.

Regression tests:
- `m18_r14_user_block_bodied_fn_is_rejected`: user-code
  `fn foo(x: Int) -> Int { junk }` returns Err from compile_to_dag.
- `m18_r14_user_data_with_opaque_body_is_rejected`: user-code
  `data foo: Int = { junk }` returns Err.

Coverage: 41 M0 + 29 M1 substrate (27 existing + 2 new R14) +
7 real-stdlib smoke + 1 realization smoke = 78 green. Clippy
clean (collapsible-match warning fixed in the same pass).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
…rate shortcuts

Five-item pass from the latest ChatGPT review. The headline is #5 —
replacing `TypeShape::Primitive(Prim)` with a newtype around
`DeclarationId`. That was an M0-inheritance bug that propagated
through every subsequent substrate refactor unnoticed because Port
machinery was never in scope for the type substrate rework. After
this commit the declaration table is the SINGLE source of type
identity across the v3 compiler; no name-keyed bridge remains.

#1 — Delete `lower_fn_item_pending`; unoverload `ArrowBody::Pending`:
- Block-bodied `fn` items in std/ files no longer create Arrow
  declarations at all. They're skipped in `collect_symbols` (matched
  on `body: None`), so the declaration table never allocates a slot
  for them. `ArrowBody::Pending` reverts to its thesis meaning
  (primitive realization lag only) — no overloaded "user body not
  lowered yet" interpretation.
- Call sites that target block-bodied fns fail-closed at inference
  because no declaration exists with their name.

#2 — Remove `resolve_pending_identifiers` tolerance:
- Split the sweep into a tolerant bootstrap variant and a strict
  user-code variant. Bootstrap tolerates dangling stubs (the
  canonical `dsl/std/*.dag` files reference types like `Tuple` that
  live in std/ modules outside the M1(2.6) load set). User-code
  `lower()` captures a `user_start` snapshot and runs the strict
  variant over stubs allocated during user lowering — every
  Identifier stub at `id >= user_start` must resolve or it's a
  fail-closed `ResolveError`.
- `Atom(Identifier { resolved: None })` now means exactly one thing
  at the user-code boundary: "not yet resolved, pre-sweep".

#3 — Move `allocate_type_params` into `collect_symbols`:
- Pass 1 of lowering (`collect_symbols_phase`) now allocates top-level
  declarations AND their TypeParam children in one pass, populating
  `Declaration.type_params` before any body-lowering runs. Pass 2
  (`lower_bodies_phase`) reads `local_scope_from_parent` instead of
  re-allocating type params.
- Bootstrap is restructured into two phases: all files Phase-1 first
  (so every cross-file template has its type_params slot populated),
  then all files Phase-2 with a shared symbols map rebuilt from the
  post-Phase-1 declaration table. `build_template_arguments` no
  longer hits forward-reference gaps that would have required
  half-valid placeholder parameters for real declarations.
- `fixup_instantiation_template_params` is deleted. The half-valid
  state it repaired no longer exists for real declarations. Stub
  templates (bootstrap dangling refs) still use self-reference
  placeholders, but the stub itself is caught by the sweep and the
  Instantiation stays dead in bootstrap bodies — no repair pass.

#4 — Move `inject_realization_stub` into `#[cfg(test)]`:
- Production `bootstrap()` no longer injects realization declarations.
  The §6.5 smoke test moves into a `#[cfg(test)]` module inside
  `bootstrap.rs` where it builds its own synthetic realization chain
  (TestRealization meta-type, anonymous instance, anonymous
  realization Arrow) without polluting `Dag::new()`.
- `Dag::realization_smoke_arrow` / `set_realization_smoke_arrow`
  deleted — production Dag has no such slot.
- `assert_realization_shape` also moved to test-only.

#5 — Replace `TypeShape::Primitive(Prim)` with newtype over `DeclarationId`:
- `types.rs`: `TypeShape` is now `{ declaration: DeclarationId }`,
  `Copy + Eq + Hash`. `Prim` enum deleted.
- `infer.rs`: `primitive_shape(dag, name)` helper replaces all
  `TypeShape::Primitive(Prim::X)` constructions. Literal node
  dispatch looks up Int/Bool/String by name. `declaration_to_type_shape`
  + `type_shape_to_declaration` deleted — bridging is now a trivial
  `TypeShape::new(decl_id)`. `walk_to_type_shape` stops at the first
  named top-level declaration and returns it as the TypeShape; no
  name-keyed primitive matching.
- `lower.rs`: `lower_type_for_port(ty, dag)` looks up primitive
  names via `declaration_by_name`. `sentinel_type_shape` helper for
  the mark-unresolved fallback.
- `m0_acceptance.rs`: ~25 assertions updated via `primitive_shape(&dag, "X")`.

Test status: 1 unit test (bootstrap realization smoke) + 41 M0 + 3
M1 substrate + 4 real-stdlib parse smoke = **49/49 green**. Clippy
clean.

Name-bridge audit: `grep -rn` in `src/v3/compiler/src/` turns up:
- `OPERATOR_FIELD_MAP` (10 entries, documented dissolution trigger
  to M2 when surface grammar exposes algebra field access directly)
— one localized constant, not a pervasive pattern. No other
name-keyed bridges remain.

Review items now closed:
- FAIL-CLOSED: declaration-graph failures go through phantom ports
  (tolerant in bootstrap, strict in user code)
- ILLEGAL STATES: Pending unoverloaded, ExternalRealization typed
  edge checked at both construction and dispatch, TemplateArgument
  half-valid state eliminated for real templates
- FACTS FLOW FORWARD: declaration identity flows end-to-end from
  bootstrap source through inference to port types; no name-keyed
  collapse at the port boundary
- COPROD DISSOLUTION: ArrowBody back to terminal-2 + scaffold-1
  (Pending only for realization lag); AtomPayload Identifier phase
  coproduct tracked in ROADMAP as M2 substrate refactor
- SINGLE AUTHORITY: `inject_primitive_operators` and
  `inject_realization_stub` both out of production bootstrap; the
  declaration table is the only source of type identity
- API-LEVEL ENFORCEMENT: `lower()` runs the strict sweep before
  returning, so no caller discipline is required

Still deferred (tracked in ROADMAP):
- AtomPayload `Identifier { resolved: Option }` → split variants
  (M2 substrate refactor)
- Flat namespace via `declaration_by_name` (M2 module system)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
Codex review on 5d0fc6d was ✅ blocking:0 overall but flagged two
previously-flagged roadmap items still unresolved: Bool/collection
operator grounding (already tracked as class-5 gaps #1 and #2)
and skip_where_clause refinement fact loss (not yet tracked).

Added class-5 gap #5 describing what's missing (refinement
predicates on type aliases like CommitSha = String where sha1(.)),
why it's hard (requires a new Declaration field, new
RefinementSpec shape, new inference enforcement at value
boundaries), what the options are, and current status (the
skip_where_clause bridge at parse.rs:801 loses the fact
entirely).

Doc-only — no code changes. The PR is green and mergeable; this
just brings DOWNSTREAM_REQUIREMENTS in sync with what codex has
been asking us to track.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
Codex blockers on 636947f: FnExternalBody and Data items compile
cleanly in ordinary user code, leaving ArrowBody::Unparsed and
ValueBody::Unparsed scaffolds in user-range declarations with no
later rejection. `fn foo(x: Int) -> Int { junk }` and
`data foo: Int = { junk }` both round-tripped through compile_to_dag
without a diagnostic, violating THESIS.md static grounding and
modeling-discipline.md principle 1 FAIL-CLOSED.

Context: these scaffolds exist so the std/bootstrap files with
match/record/pipe/lambda bodies can parse cleanly (their bodies
stay as preserved source spans, dissolved when the parser grows
to cover the remaining grammar — DOWNSTREAM_REQUIREMENTS.md
class-5 gaps #3 and #5). Bootstrap-range declarations still need
them. Ordinary user code never should.

Fix: add `reject_user_unparsed_scaffolds(dag, strict_from)` sweep
in lower.rs that walks declarations at id `>= strict_from` (the
user-lowered range after bootstrap) and emits fail-closed
diagnostics for:
- `TypeConnective::Arrow { body: ArrowBody::Unparsed(span), .. }`
- `Declaration.value_body == Some(ValueBody::Unparsed(span))`

Called from `lower()` alongside `resolve_pending_identifiers_strict`.
Bootstrap-range declarations (id < strict_from) are still
tolerated — those scaffolds exist by design until the parser
catches up.

Regression tests:
- `m18_r14_user_block_bodied_fn_is_rejected`: user-code
  `fn foo(x: Int) -> Int { junk }` returns Err from compile_to_dag.
- `m18_r14_user_data_with_opaque_body_is_rejected`: user-code
  `data foo: Int = { junk }` returns Err.

Coverage: 41 M0 + 29 M1 substrate (27 existing + 2 new R14) +
7 real-stdlib smoke + 1 realization smoke = 78 green. Clippy
clean (collapsible-match warning fixed in the same pass).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
…rate shortcuts

Five-item pass from the latest ChatGPT review. The headline is #5 —
replacing `TypeShape::Primitive(Prim)` with a newtype around
`DeclarationId`. That was an M0-inheritance bug that propagated
through every subsequent substrate refactor unnoticed because Port
machinery was never in scope for the type substrate rework. After
this commit the declaration table is the SINGLE source of type
identity across the v3 compiler; no name-keyed bridge remains.

#1 — Delete `lower_fn_item_pending`; unoverload `ArrowBody::Pending`:
- Block-bodied `fn` items in std/ files no longer create Arrow
  declarations at all. They're skipped in `collect_symbols` (matched
  on `body: None`), so the declaration table never allocates a slot
  for them. `ArrowBody::Pending` reverts to its thesis meaning
  (primitive realization lag only) — no overloaded "user body not
  lowered yet" interpretation.
- Call sites that target block-bodied fns fail-closed at inference
  because no declaration exists with their name.

#2 — Remove `resolve_pending_identifiers` tolerance:
- Split the sweep into a tolerant bootstrap variant and a strict
  user-code variant. Bootstrap tolerates dangling stubs (the
  canonical `dsl/std/*.dag` files reference types like `Tuple` that
  live in std/ modules outside the M1(2.6) load set). User-code
  `lower()` captures a `user_start` snapshot and runs the strict
  variant over stubs allocated during user lowering — every
  Identifier stub at `id >= user_start` must resolve or it's a
  fail-closed `ResolveError`.
- `Atom(Identifier { resolved: None })` now means exactly one thing
  at the user-code boundary: "not yet resolved, pre-sweep".

#3 — Move `allocate_type_params` into `collect_symbols`:
- Pass 1 of lowering (`collect_symbols_phase`) now allocates top-level
  declarations AND their TypeParam children in one pass, populating
  `Declaration.type_params` before any body-lowering runs. Pass 2
  (`lower_bodies_phase`) reads `local_scope_from_parent` instead of
  re-allocating type params.
- Bootstrap is restructured into two phases: all files Phase-1 first
  (so every cross-file template has its type_params slot populated),
  then all files Phase-2 with a shared symbols map rebuilt from the
  post-Phase-1 declaration table. `build_template_arguments` no
  longer hits forward-reference gaps that would have required
  half-valid placeholder parameters for real declarations.
- `fixup_instantiation_template_params` is deleted. The half-valid
  state it repaired no longer exists for real declarations. Stub
  templates (bootstrap dangling refs) still use self-reference
  placeholders, but the stub itself is caught by the sweep and the
  Instantiation stays dead in bootstrap bodies — no repair pass.

#4 — Move `inject_realization_stub` into `#[cfg(test)]`:
- Production `bootstrap()` no longer injects realization declarations.
  The §6.5 smoke test moves into a `#[cfg(test)]` module inside
  `bootstrap.rs` where it builds its own synthetic realization chain
  (TestRealization meta-type, anonymous instance, anonymous
  realization Arrow) without polluting `Dag::new()`.
- `Dag::realization_smoke_arrow` / `set_realization_smoke_arrow`
  deleted — production Dag has no such slot.
- `assert_realization_shape` also moved to test-only.

#5 — Replace `TypeShape::Primitive(Prim)` with newtype over `DeclarationId`:
- `types.rs`: `TypeShape` is now `{ declaration: DeclarationId }`,
  `Copy + Eq + Hash`. `Prim` enum deleted.
- `infer.rs`: `primitive_shape(dag, name)` helper replaces all
  `TypeShape::Primitive(Prim::X)` constructions. Literal node
  dispatch looks up Int/Bool/String by name. `declaration_to_type_shape`
  + `type_shape_to_declaration` deleted — bridging is now a trivial
  `TypeShape::new(decl_id)`. `walk_to_type_shape` stops at the first
  named top-level declaration and returns it as the TypeShape; no
  name-keyed primitive matching.
- `lower.rs`: `lower_type_for_port(ty, dag)` looks up primitive
  names via `declaration_by_name`. `sentinel_type_shape` helper for
  the mark-unresolved fallback.
- `m0_acceptance.rs`: ~25 assertions updated via `primitive_shape(&dag, "X")`.

Test status: 1 unit test (bootstrap realization smoke) + 41 M0 + 3
M1 substrate + 4 real-stdlib parse smoke = **49/49 green**. Clippy
clean.

Name-bridge audit: `grep -rn` in `src/v3/compiler/src/` turns up:
- `OPERATOR_FIELD_MAP` (10 entries, documented dissolution trigger
  to M2 when surface grammar exposes algebra field access directly)
— one localized constant, not a pervasive pattern. No other
name-keyed bridges remain.

Review items now closed:
- FAIL-CLOSED: declaration-graph failures go through phantom ports
  (tolerant in bootstrap, strict in user code)
- ILLEGAL STATES: Pending unoverloaded, ExternalRealization typed
  edge checked at both construction and dispatch, TemplateArgument
  half-valid state eliminated for real templates
- FACTS FLOW FORWARD: declaration identity flows end-to-end from
  bootstrap source through inference to port types; no name-keyed
  collapse at the port boundary
- COPROD DISSOLUTION: ArrowBody back to terminal-2 + scaffold-1
  (Pending only for realization lag); AtomPayload Identifier phase
  coproduct tracked in ROADMAP as M2 substrate refactor
- SINGLE AUTHORITY: `inject_primitive_operators` and
  `inject_realization_stub` both out of production bootstrap; the
  declaration table is the only source of type identity
- API-LEVEL ENFORCEMENT: `lower()` runs the strict sweep before
  returning, so no caller discipline is required

Still deferred (tracked in ROADMAP):
- AtomPayload `Identifier { resolved: Option }` → split variants
  (M2 substrate refactor)
- Flat namespace via `declaration_by_name` (M2 module system)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
Codex review on 5d0fc6d was ✅ blocking:0 overall but flagged two
previously-flagged roadmap items still unresolved: Bool/collection
operator grounding (already tracked as class-5 gaps #1 and #2)
and skip_where_clause refinement fact loss (not yet tracked).

Added class-5 gap #5 describing what's missing (refinement
predicates on type aliases like CommitSha = String where sha1(.)),
why it's hard (requires a new Declaration field, new
RefinementSpec shape, new inference enforcement at value
boundaries), what the options are, and current status (the
skip_where_clause bridge at parse.rs:801 loses the fact
entirely).

Doc-only — no code changes. The PR is green and mergeable; this
just brings DOWNSTREAM_REQUIREMENTS in sync with what codex has
been asking us to track.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
Codex blockers on 636947f: FnExternalBody and Data items compile
cleanly in ordinary user code, leaving ArrowBody::Unparsed and
ValueBody::Unparsed scaffolds in user-range declarations with no
later rejection. `fn foo(x: Int) -> Int { junk }` and
`data foo: Int = { junk }` both round-tripped through compile_to_dag
without a diagnostic, violating THESIS.md static grounding and
modeling-discipline.md principle 1 FAIL-CLOSED.

Context: these scaffolds exist so the std/bootstrap files with
match/record/pipe/lambda bodies can parse cleanly (their bodies
stay as preserved source spans, dissolved when the parser grows
to cover the remaining grammar — DOWNSTREAM_REQUIREMENTS.md
class-5 gaps #3 and #5). Bootstrap-range declarations still need
them. Ordinary user code never should.

Fix: add `reject_user_unparsed_scaffolds(dag, strict_from)` sweep
in lower.rs that walks declarations at id `>= strict_from` (the
user-lowered range after bootstrap) and emits fail-closed
diagnostics for:
- `TypeConnective::Arrow { body: ArrowBody::Unparsed(span), .. }`
- `Declaration.value_body == Some(ValueBody::Unparsed(span))`

Called from `lower()` alongside `resolve_pending_identifiers_strict`.
Bootstrap-range declarations (id < strict_from) are still
tolerated — those scaffolds exist by design until the parser
catches up.

Regression tests:
- `m18_r14_user_block_bodied_fn_is_rejected`: user-code
  `fn foo(x: Int) -> Int { junk }` returns Err from compile_to_dag.
- `m18_r14_user_data_with_opaque_body_is_rejected`: user-code
  `data foo: Int = { junk }` returns Err.

Coverage: 41 M0 + 29 M1 substrate (27 existing + 2 new R14) +
7 real-stdlib smoke + 1 realization smoke = 78 green. Clippy
clean (collapsible-match warning fixed in the same pass).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 15, 2026
* M1(2.5): implementer task list

Small ordered checklist for the implementer taking on M1(2.5)
after PR #443 merges. Pairs with src/v3/M1_DESIGN.md as the spec
— M1_TASKS.md is the work breakdown, M1_DESIGN.md is the oracle.

Seven phases, dependency-ordered:

1. Substrate data model (~1.5h) — dag.rs type replacement
2. Tokenizer + parser (~4.5h) — parser extensions for
   type-params, sum types with payloads, Arrow-in-type-position,
   infix operators, T? syntax
3. Lower (~2h) — two-pass name resolution, substitution scopes
4. Inference (~3h) — SubstStack, lazy substitution, ArrowBody
   variant handling, infix operator resolution via inhabitance
5. Bootstrap std/ (~1h) — verify/create logic.dag, bit.dag,
   algebra.dag, types.dag; delete per-primitive fn declarations
6. Tests (~2h) — update M0 helpers, add two substrate tests
7. Close out (~30m) — clippy, variant audits, grep-based
   verification that no DeclKind/name-based-dispatch remains

Total: 14-16h, single PR.

Each phase has explicit "done when" acceptance gates. Phase 7
includes six grep-based audits that catch regressions against
the thesis commitments (no seventh connective, no sixth behavior,
no DeclKind, no name-based dispatch).

"If you hit a wall" section gives concrete guidance for five
common stuck-points. "Non-goals" section restates what is
explicitly out of scope so the implementer doesn't get tempted
into scope creep.

Not a replacement for M1_DESIGN.md — the design note answers
"what and why"; this list answers "in what order and how do I
know I'm done."

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.5) substrate rework — TypeConnective + Declaration table

Replaces M0.1's parallel-representation substrate (LiteralValue, FunctionRef
string dispatch, primitive_signature lookup table, Dag.signatures) with the
six-variant TypeConnective (Atom, Conj, Disj, Arrow, Cardinality, Instantiation)
carried by Declarations in Dag.declarations, plus ArrowBody (UserDefined |
ExternalRealization | Pending). Transform.target is now a DeclarationId;
operator dispatch goes through the declaration table via a bootstrap-registered
"+"/"-"/... arrow, pending full §8.9 inhabitance walks in M1(2.6).

Pipeline changes across the v3 crate:
- dag.rs: new substrate types per M1_DESIGN §3; Declaration carries meta_tag
  and inhabits as separate edges per PR #444's §Q0 split.
- tokenize.rs: new tokens (KwType, Pipe, Question, LBrace, RBrace, Semicolon)
  plus // line comments.
- parse.rs: SurfaceType grows to 4 variants (Named, Parameterized, Optional,
  Arrow); SurfaceItem adds TypeAtom/TypeRecord/TypeSum/TypeAlias; §8.9 Option A
  has operators emit raw identifiers ("+"), not pre-resolved paths.
- lower.rs: two-pass lowering with symbol table seeded from the bootstrap
  declarations; type_to_declaration_id bridges SurfaceType → DeclarationId;
  is_strictly_smaller updated to match target "-" (the post-§8.9 shape).
- infer.rs: TypeConnective dispatch via resolve_arrow, which walks Identifier
  atoms and Arrow connectives; declaration_to_type_shape bridges named
  primitive declarations back to TypeShape for M0 port compatibility.
- bootstrap.rs (NEW): embeds four fixture strings (logic/bit/algebra/types
  subsets) and layers them onto Dag::new() via lower_into. Injects primitive
  operator arrows so user-code dispatch works. Also installs §6.5's
  realization stub chain (Realization meta-type, Int64_add_rust instance,
  Int64_add Arrow with body=ExternalRealization) per PR #444.
- M0 test helpers: rewritten to walk Transform.target through the declaration
  table via assert_target_name, and to pattern on LiteralBits (renamed from
  LiteralValue). 40/40 M0 tests remain green.
- m1_substrate_test.rs (NEW): three tests — §5 walk of Int.add via
  Instantiation → OrderedRing → add field → substituted [Word64, Word64] →
  Word64, §6 synthetic nested-domain five-level Conj check, and the §6.5
  smoke_int_add_external_realization.

PR #444 pickup (design doc still open):
- Declaration.inhabits split into meta_tag + inhabits (two fields).
- §6.5 realization smoke test, adapted: the Realization + Int64_add_rust
  chain is constructed in Rust inside bootstrap rather than parsed from a
  rust.dag fixture (the parser does not yet handle record literals or the
  'realization' item keyword; deferred to M1(2.6) — see M1_FOLLOWUPS.md).

CI:
- Adds `cargo test -p v3-compiler` and `cargo clippy -p v3-compiler
  --all-targets -- -D warnings` steps to .github/workflows/ci.yml. Before
  this PR v3 was only checked locally; the stage0 CI pipeline ignores it.

Test status: 43/43 green (40 M0 acceptance + 3 M1 substrate). clippy clean.
Zero matches for FunctionRef, LiteralValue, primitive_signature,
register_signature, lookup_function, or "std::int::" in src/v3/compiler/src.
Zero DeclKind references.

See src/v3/M1_TASKS.md for the implementer task list, src/v3/M1_DESIGN.md
for the design oracle, and src/v3/M1_FOLLOWUPS.md for deferred work.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.5) review pickups — codex + ChatGPT

Addresses all four codex blockers and the mechanical ChatGPT items
from the PR #445 review cycle. Bigger ChatGPT concerns (FACTS FLOW
FORWARD, SINGLE AUTHORITY, AtomPayload phase coproduct) are deferred
to M1(2.6) with explicit tracking in src/v3/M1_FOLLOWUPS.md because
they require parser extensions and SubstStack / §8.9 inhabitance
walks that are out of scope for this PR's substrate rework.

Codex blockers (all fixed):
- lower_type_sum: variant declaration is now allocated AFTER its
  payload children so the dense-sequential invariant on
  Dag.declarations holds for non-empty sum types.
- Unresolved Identifier stubs: alloc_identifier_stub no longer
  emits diagnostics inline; instead, resolve_pending_identifiers
  is a post-lowering sweep that either fills each stub's `resolved`
  slot from the completed declaration table or emits a fail-closed
  ResolveError via a phantom port. Called at the end of
  bootstrap::bootstrap (for cross-fixture forward refs like
  algebra.dag → Bool from types.dag) and at the end of lower::lower
  (for user-code forward refs).
- Canonical Declaration.type_params slot: added as a first-class
  field. All three generic-carrying lowering paths (record, sum,
  alias) populate it via the shared allocate_type_params helper,
  which also keeps TypeParam atoms off the Conj.children /
  Disj.variants axis. template_param_id reads from this slot.
- Dissolution ledger receipts: TypeConnective, AtomPayload,
  ArrowBody, CardinalityBound, LiteralBits all carry 4-pattern
  ledger comments in dag.rs. M1_DESIGN.md §Q7 entries are mirrored
  in the Rust source.

ChatGPT review (partial pickup):
- FAIL-CLOSED for declarations: resolved via the sweep above; the
  port-based biconditional (port.state == Unresolved iff
  diagnostics.contains(port_id)) extends to declaration-level
  failures via phantom ports.
- ILLEGAL STATES / template_param_id(...).unwrap_or(value): replaced
  with build_template_arguments, which emits an ArityMismatch
  diagnostic on param-count mismatch AND a ResolveError on per-
  index miss. The compile fails at the boundary regardless of the
  fallback substitution.
- Dissolution ledger comments address the "enum ledger and trigger
  receipts were written" blocker from codex's #4.

CI:
- Moves v3 tests + clippy into a separate `v3` job that runs in
  parallel with the v2 `ci` job. Before this, v3 ran serially
  after v2 inside the same job, so v2 failures masked v3 signals.
  Responds to the reviewer's "CI not wired" concern.

Test status: 40 M0 + 3 M1 substrate = 43/43 green. Clippy clean
with -D warnings across --all-targets.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.6) — parse real dsl/std/*.dag + delete bootstrap injection

Closes the FACTS FLOW FORWARD and SINGLE AUTHORITY concerns from the
ChatGPT review of PR #445 (Option C). The four bootstrap fixture
strings are deleted; `Dag::new()` now consumes the real
`dsl/std/{logic,bit,algebra,integer,float,types,string_type}.dag`
files via `include_str!`. `bootstrap::inject_primitive_operators` is
deleted — operators no longer exist as parallel Arrow declarations.

Parser extensions (additive — M0 tests still green):
- Tokenizer: `module`, `import`, `match`, `data`, `where` keywords;
  `=>`, `.`, `[`, `]` punctuation.
- SurfaceItem grows: `Module`/`Import` (no-op parsed items),
  `DataDecl` (body opaque), `Fn.body: Option<SurfaceExpr>` (block
  body `fn f(x) -> T { body }` consumed via brace-balanced skip when
  `None`).
- `parse_dotted_path` for `std.foo.bar`-style paths.
- `skip_brace_balanced` / `skip_where_clause` helpers.
- `SurfaceVariant.payload: VariantPayload::{Unit, Positional, Record}`
  — sum variants can now carry `Ident { field: Type }` record-shape
  payloads alongside the original `Ident(Type, Type)` positional form.
- `rhs_is_sum` aware of the new item keywords and `where`.
- Production std files parse cleanly through this grammar; see
  `tests/real_stdlib_parse_smoke.rs` for the four acceptance cases.

Bootstrap migration:
- Seven .dag files loaded in dep order: logic → bit → algebra →
  integer → float → types → string_type. Cross-file forward refs
  (algebra → Bool, integer → OrderedRing, etc.) resolve through the
  existing `resolve_pending_identifiers` sweep after all files load.
- `fixup_instantiation_template_params` — new post-sweep pass that
  rewrites `TemplateArgument.parameter` slots on Instantiation
  declarations whose templates were unresolved stubs at lower time.
  Fires an ArityMismatch if the real template param count differs
  from the arg count; silent success otherwise.
- `build_template_arguments` no longer fires arity mismatch eagerly
  on stub templates — deferred to the fixup pass.
- `resolve_pending_identifiers` skips operator identifiers (they
  stay unresolved through lowering and are dispatched at inference
  time via §8.9 walks).

SubstStack + §8.9 operator dispatch in infer.rs:
- New `SubstStack` type with push/pop/lookup.
- `resolve_arrow_walk` descends `Instantiation` chains with subst
  stack maintenance; handles `Arrow`, `Atom(Identifier { resolved })`,
  `Atom(TypeParam)`, and `Instantiation`.
- `walk_to_type_shape` bridges DeclarationIds back to port-level
  `TypeShape`, short-circuiting at the first named primitive-rootable
  declaration (Int, Int64, Word*, Classical, Bit, etc.).
- `resolve_operator_arrow` handles the operator dispatch path. At
  M1(2.6), operators take a **fast path** rather than a true
  algebra-field walk: arithmetic `(T, T) -> T`, comparison
  `(T, T) -> Bool`. The real `dsl/std/algebra.dag` expresses
  derived ops (`sub`, `div`, `lt`, `gt`) through primitive
  operations + compare — walking that chain at compile time would
  require surface-grammar expression evaluation, which is M2+ work.
- `OPERATOR_FIELD_MAP` in the new `src/v3/compiler/src/operators.rs`
  module is the single localized bridge — 10 entries mapping
  operator symbols to algebra field names. Documented as the one
  remaining name-based bridge; dissolves in M2+ once the surface
  grammar exposes algebra field access directly.

ROADMAP consolidation:
- `src/v3/ROADMAP.md` rewritten as the single source of truth for v3
  status, active work, and deferred items. Folds in M1(2.5) and
  M1(2.6) progress plus the deferred M1(3)+/M2/M3/M4 work that was
  previously scattered across `M1_FOLLOWUPS.md` and the M0-era
  ROADMAP.
- `src/v3/M1_FOLLOWUPS.md` reduced to a stub redirect pointing at the
  ROADMAP for each category of deferred work.

M0 test helper updates:
- `assert_target_name` now reads the `Atom(Identifier { name })`
  payload first, falling back to `decl.name` — operator targets are
  anonymous stubs (name on payload, None on declaration).
- `parse_std_algebra_and_walk_int_add` updated to walk the full
  `Int → Int64 → OrderedRing<Word64>` Instantiation chain; the
  real `dsl/std/integer.dag` declares `Int = Int64` and
  `Int64 = OrderedRing<Word64>`, so Int reaches the OrderedRing
  algebra through two Instantiation hops.

Dissolution status:
- **FACTS FLOW FORWARD**: resolved. The declaration table is
  populated from `dsl/std/*.dag` via `include_str!`. Changing a
  primitive means editing the source; bootstrap code has no
  parallel representation.
- **SINGLE AUTHORITY**: resolved. `inject_primitive_operators` is
  deleted. Operators are unresolved Identifier stubs at lowering and
  resolve via `resolve_operator_arrow`'s §8.9 fast path at dispatch
  time. The `OPERATOR_FIELD_MAP` constant is the one localized
  name-based bridge (vs. parallel declarations).
- **AtomPayload Identifier phase coproduct**: still tracked in the
  ROADMAP as a deferred substrate refactor for M2.

Test status: 40 M0 + 3 M1 substrate + 4 real-stdlib-parse smoke =
47/47 green. Clippy clean. Zero matches for FunctionRef,
LiteralValue, primitive_signature, register_signature,
lookup_function, `"std::int::"`, or `inject_primitive_operators` in
`src/v3/compiler/src/` outside dissolution-receipt documentation.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.6) — anonymize child declarations + duplicate-name fail-closed

Addresses the blocking ChatGPT review on commit 5d6030a8c
(SINGLE AUTHORITY + FAIL-CLOSED + FACTS FLOW FORWARD + ILLEGAL
STATES + ARROW typed edge). Net effect: `Dag::declaration_by_name`'s
flat scan no longer leaks TypeParam binders, sum variants, or
realization scaffolds into cross-module name resolution.

Silent mis-resolution fix (core structural concern):
- `allocate_type_params` → TypeParam declarations are `name: None`.
  The binder name lives in `Atom(TypeParam(name))`; references
  inside the parent's body resolve by DeclarationId via the
  `local` scope map, not via `declaration_by_name`.
- `lower_type_sum` → sum-variant declarations are `name: None`.
  The variant name lives in the parent `Disj.variants` Field label.
  Variant constructors (`True`, `Less`, `Ok`, ...) are no longer
  referenceable outside their parent's Disj.
- `inject_realization_stub` → realization instance and realized
  Arrow are `name: None`. The `Realization` meta-type stays
  top-level (user code CAN refer to it as a type) but the
  instance + Arrow are scaffolds hidden from `declaration_by_name`.
- `Dag::declaration_by_name` doc comment now explicitly states
  top-level-only semantics and first-match policy (consistent
  with `collect_symbols`'s first-wins behavior).
- New test `child_declarations_are_anonymous`: asserts `T`,
  `True`, `False`, `Less`, `Equal`, `Greater`, `Int64_add_rust`,
  `Int64_add` all fail `declaration_by_name` while `Int`,
  `OrderedRing`, `Classical`, `Realization` still resolve.

Duplicate-declaration fail-closed (SINGLE AUTHORITY):
- `collect_symbols` seeds the symbols map with first-match
  semantics (`HashMap::entry().or_insert`) to match
  `declaration_by_name`. No more last-wins `insert` overwrite.
- On duplicate top-level item, `collect_symbols` emits a
  `ResolveError` via a phantom-port diagnostic and returns a
  side `is_first: Vec<bool>` that `lower_into` uses to skip
  the duplicate item at lowering time. The original's filled
  connective is not overwritten.
- New test `test_duplicate_type_declaration_is_rejected`:
  `type Foo\ntype Foo` produces `Err(CompileError::Semantic)`
  with the duplicate diagnostic in the Dag's diagnostic table.

ExternalRealization typed-edge check (ILLEGAL STATES /
COPROD DISSOLUTION):
- `inject_realization_stub` now calls `assert_realization_shape`
  before encoding the `ExternalRealization(instance_id)` body.
  The check verifies the instance is a `Conj` with a `meta_tag`
  pointing at the `Realization` meta-type. Bootstrap owns both
  sides so the assertion always holds — but it documents the
  invariant and catches future drift that tries to store a
  non-realization declaration in the body.
- `Dag::realization_smoke_arrow()` getter + setter — the §6.5
  smoke test Arrow's id is stashed on `Dag` because the Arrow
  itself is now anonymous and can't be looked up by name.

Supporting API:
- `DiagnosticTable::iter` — iterate (port, diagnostic) pairs.
  Needed by the duplicate-declaration test to scan for a
  specific error kind.

Test status: 41 M0 + 4 M1 substrate + 4 real-stdlib smoke = 49/49
green. Clippy clean.

Review items addressed in this commit:
- SINGLE AUTHORITY: duplicate names compile → ResolveError
- FAIL-CLOSED: silent overwrite → diagnostic
- SINGLE AUTHORITY: child declarations leak into flat scan →
  all child declarations anonymous
- FACTS FLOW FORWARD: child/parent fact dropped →
  parent→child lookup via `type_params` slot / `Disj.variants`
  Field label, no name recovery
- ILLEGAL STATES / COPROD DISSOLUTION: ExternalRealization
  opaque → typed-edge check at construction via
  `assert_realization_shape`

Still deferred (tracked in ROADMAP, not blocking):
- `decide_transform` does not walk the `ExternalRealization`
  target (M1(3)+ cost/emission lens work will consume it)
- `Dag::new()` still panics on bootstrap drift instead of
  routing through the diagnostic channel (requires Dag::new
  → Result refactor)
- AtomPayload Identifier pre/post resolution phase coproduct
  (M2 substrate refactor)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.6) — route bootstrap drift through diagnostics, validate ExternalRealization in decide_transform

Closes the last two items from the prior ChatGPT review that were
still deferred on the branch: bootstrap's panic-based failure channel
and `decide_transform`'s UserDefined-only body validation.

Bootstrap drift as diagnostic (FAIL-CLOSED structural):
- `parse_and_lower_fixture` no longer panics on tokenize/parse
  errors. It attaches the failure as a diagnostic via the new
  `Dag::attach_diagnostic` method and returns without lowering.
- `inject_realization_stub` gracefully skips the scaffold if `Int`
  is missing from the declaration table (earlier std/ fixture
  failed to load); the underlying cause is already in
  `dag.diagnostics()` from `parse_and_lower_fixture`.
- `bootstrap()` removes the post-sweep `panic!` that fired on
  non-empty diagnostics. Bootstrap completes cleanly even under
  drift; `compile_to_dag` surfaces the failure through the same
  `Err(CompileError::Semantic(dag))` channel user errors use.
- New `Dag::attach_diagnostic(diag)` — allocates a phantom port
  and routes the diagnostic through `mark_unresolved`. Used by
  bootstrap, `lower::report_declaration_error`, and any future
  crate code that needs a diagnostic carrier without a natural
  PortId.

decide_transform ExternalRealization walk (ILLEGAL STATES /
FACTS FLOW FORWARD):
- `decide_transform` now pattern-matches all three `ArrowBody`
  variants explicitly:
    - `UserDefined(bind_id)`: existing Bind.value port-state check.
    - `ExternalRealization(realization_id)`: new validation —
      calls `is_realization_shape` to verify the target declaration
      is still a `Conj` with `meta_tag = Realization`. Catches any
      drift that bypasses `bootstrap::assert_realization_shape`'s
      construction-time invariant.
    - `Pending`: documented as valid at M1(2.6) (§8.11 ratchet
      dissolves it by M3); no action.
- `is_realization_shape` helper in infer.rs mirrors
  `bootstrap::assert_realization_shape` as a runtime safety net.

Test status: 41 M0 + 4 M1 substrate + 4 real-stdlib smoke = 49/49
green. Clippy clean.

Review items now closed:
- FAIL-CLOSED: bootstrap panic → diagnostic channel (ALL three
  panic sites: tokenize/parse, Int missing, post-sweep non-empty)
- FACTS FLOW FORWARD / ILLEGAL STATES: decide_transform validates
  ExternalRealization, not just UserDefined

Still deferred (M2 substrate refactor, not blocking):
- AtomPayload `Identifier { resolved: Option }` pre/post
  resolution phase coproduct — M2 when the surface grammar
  stabilizes

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* docs: clarify M1(2.5) retrospective is historical; sync ROADMAP test count

Addresses a doc coherence nit from the latest PR #445 review: the
M0_RETROSPECTIVE addendum and the ROADMAP both claimed present-tense
truths about bootstrap that contradicted each other, and the test
counts had drifted apart as M1(2.6) work landed.

M0_RETROSPECTIVE.md:
- Reframe the M1(2.5) addendum as a historical snapshot. The
  bootstrap details (four embedded fixture modules,
  inject_primitive_operators, 42-green test count) describe the
  M1(2.5) handoff state, not the current state. Point readers to
  ROADMAP.md for current v3 status.
- Explicitly note that both transitional mechanisms were removed
  in M1(2.6): bootstrap now consumes real `dsl/std/*.dag` files
  via include_str!, operator dispatch goes through
  `infer::resolve_operator_arrow`.

ROADMAP.md:
- M1(2.5) status row changed from "In review / 43 green" to
  "Landed on PR #445" with a pointer at the 42-green historical
  snapshot in the retrospective.
- M1(2.6) status row updated to "In review on PR #445" with the
  actual current delta: parser extensions, real-std bootstrap,
  SubstStack + §8.9, deleted primitive-operator injection,
  anonymized child declarations, duplicate-name fail-closed,
  ExternalRealization typed-edge check, bootstrap drift routed
  through Dag::attach_diagnostic. **Current: 41 M0 + 4 M1
  substrate + 4 real-stdlib smoke = 49 green.**

`M1_DESIGN.md` and `M1_TASKS.md` still mention 42-green as the
design-time target; those stay as frozen historical reference docs.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.6) review round 5 — eliminate all name bridges + clean substrate shortcuts

Five-item pass from the latest ChatGPT review. The headline is #5 —
replacing `TypeShape::Primitive(Prim)` with a newtype around
`DeclarationId`. That was an M0-inheritance bug that propagated
through every subsequent substrate refactor unnoticed because Port
machinery was never in scope for the type substrate rework. After
this commit the declaration table is the SINGLE source of type
identity across the v3 compiler; no name-keyed bridge remains.

#1 — Delete `lower_fn_item_pending`; unoverload `ArrowBody::Pending`:
- Block-bodied `fn` items in std/ files no longer create Arrow
  declarations at all. They're skipped in `collect_symbols` (matched
  on `body: None`), so the declaration table never allocates a slot
  for them. `ArrowBody::Pending` reverts to its thesis meaning
  (primitive realization lag only) — no overloaded "user body not
  lowered yet" interpretation.
- Call sites that target block-bodied fns fail-closed at inference
  because no declaration exists with their name.

#2 — Remove `resolve_pending_identifiers` tolerance:
- Split the sweep into a tolerant bootstrap variant and a strict
  user-code variant. Bootstrap tolerates dangling stubs (the
  canonical `dsl/std/*.dag` files reference types like `Tuple` that
  live in std/ modules outside the M1(2.6) load set). User-code
  `lower()` captures a `user_start` snapshot and runs the strict
  variant over stubs allocated during user lowering — every
  Identifier stub at `id >= user_start` must resolve or it's a
  fail-closed `ResolveError`.
- `Atom(Identifier { resolved: None })` now means exactly one thing
  at the user-code boundary: "not yet resolved, pre-sweep".

#3 — Move `allocate_type_params` into `collect_symbols`:
- Pass 1 of lowering (`collect_symbols_phase`) now allocates top-level
  declarations AND their TypeParam children in one pass, populating
  `Declaration.type_params` before any body-lowering runs. Pass 2
  (`lower_bodies_phase`) reads `local_scope_from_parent` instead of
  re-allocating type params.
- Bootstrap is restructured into two phases: all files Phase-1 first
  (so every cross-file template has its type_params slot populated),
  then all files Phase-2 with a shared symbols map rebuilt from the
  post-Phase-1 declaration table. `build_template_arguments` no
  longer hits forward-reference gaps that would have required
  half-valid placeholder parameters for real declarations.
- `fixup_instantiation_template_params` is deleted. The half-valid
  state it repaired no longer exists for real declarations. Stub
  templates (bootstrap dangling refs) still use self-reference
  placeholders, but the stub itself is caught by the sweep and the
  Instantiation stays dead in bootstrap bodies — no repair pass.

#4 — Move `inject_realization_stub` into `#[cfg(test)]`:
- Production `bootstrap()` no longer injects realization declarations.
  The §6.5 smoke test moves into a `#[cfg(test)]` module inside
  `bootstrap.rs` where it builds its own synthetic realization chain
  (TestRealization meta-type, anonymous instance, anonymous
  realization Arrow) without polluting `Dag::new()`.
- `Dag::realization_smoke_arrow` / `set_realization_smoke_arrow`
  deleted — production Dag has no such slot.
- `assert_realization_shape` also moved to test-only.

#5 — Replace `TypeShape::Primitive(Prim)` with newtype over `DeclarationId`:
- `types.rs`: `TypeShape` is now `{ declaration: DeclarationId }`,
  `Copy + Eq + Hash`. `Prim` enum deleted.
- `infer.rs`: `primitive_shape(dag, name)` helper replaces all
  `TypeShape::Primitive(Prim::X)` constructions. Literal node
  dispatch looks up Int/Bool/String by name. `declaration_to_type_shape`
  + `type_shape_to_declaration` deleted — bridging is now a trivial
  `TypeShape::new(decl_id)`. `walk_to_type_shape` stops at the first
  named top-level declaration and returns it as the TypeShape; no
  name-keyed primitive matching.
- `lower.rs`: `lower_type_for_port(ty, dag)` looks up primitive
  names via `declaration_by_name`. `sentinel_type_shape` helper for
  the mark-unresolved fallback.
- `m0_acceptance.rs`: ~25 assertions updated via `primitive_shape(&dag, "X")`.

Test status: 1 unit test (bootstrap realization smoke) + 41 M0 + 3
M1 substrate + 4 real-stdlib parse smoke = **49/49 green**. Clippy
clean.

Name-bridge audit: `grep -rn` in `src/v3/compiler/src/` turns up:
- `OPERATOR_FIELD_MAP` (10 entries, documented dissolution trigger
  to M2 when surface grammar exposes algebra field access directly)
— one localized constant, not a pervasive pattern. No other
name-keyed bridges remain.

Review items now closed:
- FAIL-CLOSED: declaration-graph failures go through phantom ports
  (tolerant in bootstrap, strict in user code)
- ILLEGAL STATES: Pending unoverloaded, ExternalRealization typed
  edge checked at both construction and dispatch, TemplateArgument
  half-valid state eliminated for real templates
- FACTS FLOW FORWARD: declaration identity flows end-to-end from
  bootstrap source through inference to port types; no name-keyed
  collapse at the port boundary
- COPROD DISSOLUTION: ArrowBody back to terminal-2 + scaffold-1
  (Pending only for realization lag); AtomPayload Identifier phase
  coproduct tracked in ROADMAP as M2 substrate refactor
- SINGLE AUTHORITY: `inject_primitive_operators` and
  `inject_realization_stub` both out of production bootstrap; the
  declaration table is the only source of type identity
- API-LEVEL ENFORCEMENT: `lower()` runs the strict sweep before
  returning, so no caller discipline is required

Still deferred (tracked in ROADMAP):
- AtomPayload `Identifier { resolved: Option }` → split variants
  (M2 substrate refactor)
- Flat namespace via `declaration_by_name` (M2 module system)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.6) review round 6 — surface-AST dissolution ledgers + real_stdlib smoke expansion

Addresses the codex review on commit 41b3c54e (pre-round-5). The
first codex blocker — realization stub assertion-based validation —
is already closed by the round-5 commit (fbd4d6158), which moved
`inject_realization_stub` entirely into `#[cfg(test)]`; the
production compile path has no realization scaffold to assert on.
This commit addresses the remaining review items.

Surface-AST dissolution audit (blocking #2):
- `SurfaceItem` (9 variants): 🟡 mixed-lifecycle. Six terminal
  (Let, Fn, Type*), three scaffolds (Module, Import, DataDecl)
  with named dissolution triggers tied to M2 module system and
  M2 value-construction semantics. STOP signal documented for
  adding a 10th variant without revisiting the Type* collapse.
- `SurfaceType` (4 variants): 🟢 terminal. Each variant mirrors
  a distinct `TypeConnective` arm — collapsing would be a
  category error. STOP signal documented for variants that
  don't correspond to a substrate connective.
- `SurfaceExpr` (6 variants): 🟡. Three literal variants are a
  surface-side duplication of `LiteralBits`; dissolution trigger
  documented (fold into a single `Literal(LiteralBits)` when
  `LiteralBits` grows a fourth variant).
- `VariantPayload` (3 variants): 🟡. `Unit` is absorbable into
  `Positional(vec![])`; dissolution trigger documented.

All four ledgers follow the same 4-pattern template used by the
`dag.rs` receipts added in the M1(2.5) push.

Real-stdlib smoke expansion (non-blocking):
- `real_stdlib_parse_smoke.rs` now covers 7 bootstrap files
  instead of 4: logic, bit, algebra, types, plus integer, float,
  string_type. The smoke test ratchets parser regressions in
  isolation from `Dag::new` wiring, which is the whole point of
  the smoke lane.

Test status: 1 unit test + 41 M0 + 3 M1 substrate + 7 real-stdlib
smoke = 52/52 green. Clippy clean.

Review items now closed:
- Bootstrap panic elimination (closed in round 5 by moving
  `inject_realization_stub` to `#[cfg(test)]`)
- Surface coproduct audit (closed in this commit)
- Parser-only smoke gate coverage (closed in this commit)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.6) review round 7 — dissolve all remaining 🟡 coproducts

Four structural dissolutions from the round 6 ledger audit, plus the
corresponding ledger rewrites. After this commit the only 🟡 or
🔴 items left are those that are structurally deferred to later
milestones (M2 module system, M3 Pending ratchet).

#1 — VariantPayload::Unit dissolved
- Unit variant collapsed into `Positional(vec![])`. Unit and
  zero-arity positional were structurally indistinguishable at
  the substrate level; the dedicated Unit arm was cosmetic.
- VariantPayload is now a 2-variant enum (Positional, Record),
  reclassified 🟢 terminal.
- `parse_variant` emits `Positional(Vec::new())` for bare
  variants; `lower_type_sum` drops the Unit match arm.

#2 — SurfaceItem::Module/Import/DataDecl dissolved
- Parser absorbs module / import / data declarations at parse
  time instead of emitting them as SurfaceItem variants. Their
  M1(2.6) semantic effect was "no-op at lowering," so carrying
  them through as SurfaceItem scaffolds was pure scaffolding
  debt.
- New parser helpers `absorb_module_item` / `absorb_import_item`
  / `absorb_data_item` consume the token stream without
  emitting a SurfaceItem.
- `parse_item` returns `Result<Option<SurfaceItem>, Diagnostic>`:
  None means "absorbed, no item to emit."
- SurfaceItem drops from 9 variants to 6 (Let, Fn, TypeAtom,
  TypeRecord, TypeSum, TypeAlias), reclassified 🟢 terminal
  modulo the M2 Type* collapse question.
- `lower_item` / `collect_symbols_phase` / `item_span` all drop
  the Module/Import/DataDecl arms.

#3 — SurfaceExpr literal trio dissolved
- The three surface-expression literal variants
  (IntLit/BoolLit/StringLit) collapse into a single
  `Literal { value: SurfaceLiteral, span }` variant. The new
  `SurfaceLiteral` enum is parse-local (Int/Bool/String),
  preserving the G3 guardrail that parse.rs doesn't mention Dag
  types — `SurfaceLiteral` mirrors `LiteralBits` but lives in
  the parse layer.
- SurfaceExpr drops from 6 variants to 4 (Literal, Var, Call,
  If), reclassified 🟢 terminal.
- `lower_expr` collapses its three literal arms into one match
  with an inner `match value { SurfaceLiteral::* }`.
- `is_recursive`, `descent_provable`, `collect_calls`,
  `expr_span`, `is_strictly_smaller` all updated.

#4 — AtomPayload::Identifier phase coproduct split
- `Atom(Identifier { name: String, resolved: Option<DeclarationId> })`
  replaced by two structural variants:
    - `Atom(UnresolvedIdentifier(String))` — pre-sweep, name
      reference pending resolution.
    - `Atom(ResolvedIdentifier(DeclarationId))` — post-sweep,
      typed edge to referent declaration.
- The pre/post-sweep phase is now a coproduct variant, not a
  field value. Pattern matches for the two cases live on
  different arms instead of on `Some`/`None`.
- `resolve_pending_identifiers` rewrites the connective on
  resolution instead of mutating an `Option` in place. The
  sweep is a structural phase transition, not a field update.
- All pattern-match sites updated: `placeholder_connective`,
  `alloc_identifier_stub`, `build_template_arguments`'s stub
  check, `run_identifier_sweep`, `unresolved_operator_name`,
  `resolve_arrow_walk`, `walk_to_type_shape`,
  `target_display_name`, `assert_target_name` in tests.
- AtomPayload is now 4 variants (Literal, UnresolvedIdentifier,
  ResolvedIdentifier, TypeParam), reclassified 🟢 terminal. The
  former compression debt the ledger flagged (`Option<_>` hiding
  a phase coproduct) is eliminated.

Test status: 1 unit test (bootstrap realization smoke) + 41 M0 +
3 M1 substrate + 7 real-stdlib parse smoke = 52/52 green. Clippy
clean. Net -71 lines (parse.rs net -94, lower.rs net -58 via
simpler match arms, dag.rs +28 for the split AtomPayload).

Ledger audit after this commit:
- 🟢 terminal at M1(2.6): TypeConnective, AtomPayload,
  CardinalityBound, LiteralBits, ArrowBody (terminal-2 modulo
  the Pending scaffold), SurfaceItem, SurfaceType, SurfaceExpr,
  SurfaceLiteral, VariantPayload.
- 🟡 scaffold with thesis-defined dissolution trigger:
  ArrowBody::Pending (§8.11 ratchet to zero by M3).
- 🔴 deferred to M2+: flat namespace via declaration_by_name
  (needs module-scoped declaration table). Tracked in ROADMAP.

No remaining compression debt in the parse or declaration layers.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.7) — enumeration-driven substrate fix for all 14 gaps

Walked every substrate consumer end-to-end (infer.rs, lens_depth.rs,
lens_provenance.rs, plus the parse→lower write pipeline) and cataloged
every structural question each asks about a Node/Declaration/Port.
DOWNSTREAM_REQUIREMENTS.md captured 14 gaps across four fact-placement
classes. This commit resolves all 14 structurally in one coherent
pass rather than reactive per-reviewer fixes.

Class 1 (primitive type identity) — Dag::int_shape/bool_shape/
string_shape/realization_meta_id cached at bootstrap. lower_type_for_port
dissolved into type_to_declaration_id with a fresh-stub fail-closed
guard; the Int|Bool|String whitelist parallel authority is gone.

Class 2 (operator dispatch) — TransformTarget{Callable(DeclarationId),
Operator(OperatorKind)} replaces the raw target field. OperatorKind
splits Arithmetic(ArithmeticOp) and Comparison(ComparisonOp) so the
output-type rule lives on the variant. SurfaceExpr::Operator is a
first-class parser variant; operators never allocate stub declarations.
OPERATOR_FIELD_MAP / is_operator_name / is_comparison_operator /
unresolved_operator_name deleted. is_strictly_smaller checks
ArithmeticOp::Sub structurally instead of target == "-".

Class 3 (scaffold honesty) — ArrowBody::Unparsed(SourceSpan) fourth
variant for block-body scaffolds with its own dissolution trigger.
SurfaceItem::Fn now requires an expression body; FnExternalBody is a
sibling variant that lowers to Unparsed. SurfaceItem::Data/Module/Import
emit real facts instead of parser-absorbing. TemplateArgument stub
self-reference branch deleted — stub templates yield Vec::new() arguments.

Class 4 (parallel authorities) — is_realization_shape compares cached
DeclarationId instead of name; port-type authority dissolved in Class 1.

Coverage: 41 M0 + 11 M1 substrate (3 pre-existing + 8 new m17_*
regression tests) + 7 stdlib smoke + 1 realization smoke = 60 green.
Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.7) — document descent string comparisons, expand infer wildcards

Two follow-up clarifications to a8489aa20:

1. descent_provable / is_recursive / is_strictly_smaller still compare
   parser-stage identifier strings (target/self_name, name/first_param).
   Added a doc comment explaining these are not name-based dispatch:
   both sides come from a single parse tree reaching
   lower_fn_item_expr_body on the same call stack, with no symbol
   table lookup. The typed alternative (NodeId/PortId comparisons) is
   unavailable at this point in lowering because the BindNode that
   would own the fn's typed ports hasn't been pushed yet — that is
   what lower_fn_item_expr_body is currently creating. A future
   post-lowering DescentEvidence lens is the right home for the
   typed-id version. Not a bridge; documented so it is not re-flagged.

2. resolve_arrow_walk and walk_to_type_shape both ended in _ => None
   wildcards over TypeConnective. Expanded both to explicit per-variant
   arms so a future substrate extension (a 7th TypeConnective variant or
   a 5th AtomPayload) forces both sites to reconsider instead of
   silently falling through. Behavior unchanged; each non-matching
   case still returns None.

60/60 green, clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.7) R9 — algebra-walked operator dispatch + data value_body scaffold

ChatGPT review R9 on PR #445 flagged two structural gaps the initial
M1(2.7) commit did not close:

1. Operators still bypass declaration-backed arrows. OperatorKind +
   resolve_operator_arrow fabricated (T, T) -> T / (T, T) -> Bool in
   Rust instead of reading from std/algebra.dag.
2. Data items drop their body. lower_data_item set connective = the
   type annotation, making `data foo: Int = {...}` structurally
   identical to `type foo = Int`.

R9-A — operator dispatch grounded in algebra declarations:

- Extended std/algebra.dag: OrderedRing<T> gained direct fields for
  sub, div, eq, ne, lt, le, gt, ge so every arithmetic/comparison
  operator maps to a named algebra field with a declared Arrow
  signature. Existing record-field syntax — no grammar change. Runtime
  semantics (sub = add + negate, lt = compare == Less) stay in the
  realization layer; the declaration is the compiler's signature
  authority.
- Rewrote resolve_operator_arrow as a structural §8.9 walk. It walks
  the LHS type's chain through Instantiation / ResolvedIdentifier
  edges to an algebra Conj, looks up the operator's field via
  OperatorKind::algebra_field_name(), reads the field's Arrow from
  the declaration graph, and substitutes the receiver type parameter
  to the source declaration (not the template argument). For
  `1 + 2`: walk Int → Int64 → OrderedRing<Word64> → add → substitute
  T → Int → signature (Int, Int) -> Int. Matches user ports.
- Added read_algebra_field + substitute_receiver helpers. Bool and
  collection-level algebra receivers (FreeMonoid / Set / Map) are
  tracked as class-5 gaps in DOWNSTREAM_REQUIREMENTS.md with named
  triggers; they fall back to a documented Rust scaffold.

R9-B — data items structurally distinct from type aliases:

- Added Declaration.value_body: Option<ValueBody> with
  ValueBody::Unparsed(SourceSpan) as the scaffold form.
- lower_data_item now sets connective = the type AND value_body =
  Some(Unparsed(body_span)). Consumers discriminate "data value" from
  "type alias" by reading value_body directly. Body span preserved
  for M2+ parser extension to consume.
- Dissolution trigger: when the parser adopts record/map/list literal
  SurfaceExprs, Unparsed dissolves to Structural(NodeId).

Dissolution ledgers updated: OperatorKind and TransformTarget::Operator
are 🟡 scaffolds (not 🟢 terminal) with explicit M2+ triggers.
ValueBody gets a full 4-pattern check.

5 new m17_r9_* regression tests verify the algebra walk produces
source-typed signatures for arithmetic + comparison, OrderedRing
carries every required direct operator field, data items have
value_body = Some(Unparsed), and type aliases have value_body = None.

Coverage: 41 M0 + 16 M1 substrate + 7 real-stdlib smoke + 1 realization
smoke = 65 green. Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.7) R9 — collapse double-lower of fn param/return types

Codex review on d29a2eaa flagged a real bug in lower_fn_item_expr_body:
function param and return type annotations were lowered TWICE — once
via type_to_declaration_id for the Arrow connective input/output, and
again inside lower_type_for_port for the port TypeShape. For compound
types like `List<Int>` or user-declared records, each call allocates
a fresh anonymous declaration, so the Arrow signature and the port
TypeShape wound up carrying different DeclarationIds for the same
syntactic annotation. Infer later compared them by DeclarationId and
saw a split identity.

Fix: compute the DeclarationId once, reuse. `lower_type_for_port`
was renamed `declaration_to_port_shape` and now takes a pre-computed
DeclarationId (no internal call to type_to_declaration_id). Callers
in lower_item (Let), lower_fn_item_expr_body (param loop, return),
and lower_fn_item_unparsed all compute the id once and pass it
through.

New regression test m17_r9_fn_param_uses_single_declaration_id_for_arrow_and_port
compiles `fn identity(p: Point) -> Point = p` with a user-declared
Point record and asserts the Arrow's input DeclarationId equals the
Bind's param port TypeShape.declaration. Before the fix this split;
after the fix they share identity.

Coverage: 41 M0 + 17 M1 substrate + 7 real-stdlib smoke + 1 realization
smoke = 66 green. Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) — match expression parser + Branch generalization

Parser catch-up (not substrate redesign) to close the gap between
v3's minimal grammar and v2's richer surface. Match lowers to
Branch; no new L1 behavior variants.

Substrate:
- Add `BranchPattern { UnresolvedVariant { name, span },
  ResolvedVariant(DeclarationId) }` — phase coproduct mirroring
  `AtomPayload::Unresolved/ResolvedIdentifier`. Populated at lower
  time, resolved by a new infer-time pass.
- Add `Path.pattern: BranchPattern` — per-arm structural
  discriminator replacing the old positional convention
  (`paths[0] = then`, `paths[1] = else`). Emitters, exhaustiveness
  checkers, and lenses read this field instead of reconstructing
  from context.
- Add `Dag::nodes_mut()` crate-private accessor scoped to the
  pattern resolution pass.

Parser:
- `SurfaceExpr::Match { scrutinee, arms, span }` and
  `SurfaceMatchArm { pattern, body, span }`.
- `SurfacePattern::BareVariant { name, span }` — at M1(2.8)
  bare-variant patterns only (no wildcards, destructure, or
  nesting).
- `parse_primary` dispatches `match` to `parse_match`; arms are
  brace-delimited with optional comma separators.

Lowering:
- `SurfaceExpr::Match` lowers to a `Branch` with the scrutinee
  as input and one `Path` per arm. Each path carries
  `UnresolvedVariant { name, span }` built from the surface
  pattern. Arm bodies lower first, then `alloc_node_id` runs —
  preserves the dense-sequential node id invariant.
- `SurfaceExpr::If` lowering rewired to emit explicit
  `UnresolvedVariant { "True" }` / `{ "False" }` patterns on its
  two paths. Positional convention dissolves — the
  discriminator lives structurally.
- Walk helpers (`is_recursive`, `descent_provable`,
  `collect_calls`) extended with Match arms.

Inference:
- Branch input check relaxed from "must be Bool" to "must be a
  declaration whose connective is `Disj`." Bool, Classical, and
  user-defined sum types all pass; String, Int, etc. still fail.
  This is a widening, not a compromise: `Bool = True | False` was
  already a Disj, so M0's Bool-specific rule was the degenerate
  case.
- New `resolve_branch_patterns` post-infer pass. For each Branch
  whose input is Resolved, walks the scrutinee's Disj children,
  matches each path's pattern name scoped against them, and
  rewrites `UnresolvedVariant` to `ResolvedVariant(DeclarationId)`.
  Fail-closed on unknown variant names. Runs before the
  Uninferred → Unresolved sweep so patterns settle with ports.

Tests (5 new, 41 M0 + 22 M1 substrate + 7 stdlib smoke + 1
realization smoke = 71 green):
- `m18_match_on_user_sum_type_compiles` — match on `Sign = Plus |
  Minus` with literal RHS bodies type-checks and populates
  `ResolvedVariant` per path.
- `m18_match_on_non_disj_scrutinee_is_rejected` — match on String
  fails fail-closed.
- `m18_match_with_unknown_variant_is_rejected` — unknown variant
  pattern name fails fail-closed.
- `m18_if_then_else_populates_branch_pattern` — `if`/`else` paths
  are `ResolvedVariant` after infer (Bool.True and Bool.False).
- `m18_bool_is_structurally_a_disj` — substrate invariant pin:
  Bool must be a Disj with True/False variants; breaking this
  breaks `if`/`else`.

New class-5 gap #4: variant RHS expressions. logic.dag's
`classical_not`/`_and`/`_or` still load as `FnExternalBody`
because their match arm RHS uses bare `True` / `False` as
expressions — the R7 variant anonymization makes these
unresolvable. Documented in DOWNSTREAM_REQUIREMENTS.md with
three resolution options (surface syntax, targeted rollback, or
infer-time re-resolution).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R10 — ArithmeticOp/ComparisonOp receipts + relaxed is_realization_shape

Two blockers from codex review on 8061258e:

1. ArithmeticOp and ComparisonOp are N≥2 Rust enums but only the
   outer OperatorKind wrapper carried a dissolution receipt. Fix:
   add explicit 🟡 receipts to both sub-enums. They inherit
   OperatorKind's dissolution trigger (M2+ surface desugaring) and
   the 4-pattern check is run per-enum. No dissolution debt left
   unclassified at the operator scaffold.

2. is_realization_shape compared meta_tag against
   dag.realization_meta_id(), but the production bootstrap doesn't
   load any Realization declaration (realization facts live in
   dsl/extdeps/languages/* per the thesis, not in the M1(2.7)
   std/ set). The cache was always None and the check always
   failed. Fix: relax is_realization_shape to check structural
   shape only — "Conj with a non-None meta_tag" IS the
   realization marker, no further name/id comparison needed. The
   structural shape is what bootstrap::assert_realization_shape
   and the #[cfg(test)] realization smoke test already validate
   at construction. Deleted the now-unused realization_meta cache
   field + accessor + populate step; PrimitiveCache goes from 4
   roles to 3 (Int, Bool, String).

Coverage: 41 M0 + 22 M1 substrate + 7 stdlib smoke + 1
realization smoke = 71 green. Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v2: regenerate stage0 std_algebra.rs for OrderedRing operator fields

M1(2.8) R9 extended dsl/std/algebra.dag's OrderedRing<T> with direct
operator fields (sub, div, eq, ne, lt, le, gt, ge) so v3's §8.9
operator walk can read signatures from algebra declarations instead
of fabricating them. The extension also cascades into v2's stage0
bootstrap because v2 parses the same std/*.dag files and generates
Rust structs mirroring their record types.

ci_freshness was failing on PR #445 because the checked-in stage0
std_algebra.rs didn't include the 8 new fields. Regenerated via
./scripts/regenerate-stage0.sh. Fixed point verified (pass1 == pass2),
diagnostic ratchet unchanged (354 errors), and ci_freshness now passes
locally.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R11 — match exhaustiveness + uniqueness check

Codex review on 249f3f20 flagged coproduct-elimination soundness:
the pattern resolution pass rewrote `UnresolvedVariant` to
`ResolvedVariant` but never checked that the resolved arms
covered each scrutinee Disj variant exactly once. Without that,
`match a { True => x }` on `Classical = True | False` compiled
despite missing `False`, violating THESIS.md's exhaustiveness
guarantee.

Fix: after the main `resolve_branch_patterns` rewrite loop, run a
coverage pass. For each Branch whose output port is not already
Unresolved:
- **Uniqueness**: collect each Path's resolved DeclarationId and
  fail-closed with "duplicate match arm for variant `X`" if any
  id repeats.
- **Exhaustiveness**: diff the resolved set against the
  scrutinee's `Disj.variants` and fail-closed with "non-exhaustive
  match: missing arm(s) for variant(s) `X, Y`" if any expected
  variant is absent.

Both checks anchor to the Branch's output port span so the
diagnostic surfaces at the match expression itself. The pass is
skipped when the Branch already has a diagnostic from pattern
resolution — partial resolution makes coverage meaningless.

Three new regression tests:
- `m18_r11_non_exhaustive_match_is_rejected`: `match s { Plus => 0 }`
  on `Sign = Plus | Minus` fails (missing Minus arm).
- `m18_r11_duplicate_match_arm_is_rejected`: `Plus => 0, Plus => 1`
  fails on duplicate Plus.
- `m18_r11_three_variant_exhaustive_match_compiles`: a match
  covering all three variants of `Ternary = Low | Mid | High`
  compiles cleanly.

Non-blocking: refreshed `SurfaceExpr` dissolution receipt. The
ledger still claimed five variants and described match as future
work after M1(2.8) added the sixth variant. Updated to 🟡 scaffold
(down from the too-confident 🟢 terminal) with the M2+ dissolution
trigger naming the remaining grammar surface (pipe, lambda,
record/map/list literals, field access) and the Operator →
Call dissolution.

Coverage: 41 M0 + 25 M1 substrate (22 existing + 3 new R11) + 7
real-stdlib smoke + 1 realization smoke = 74 green. Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R12 — fold resolve_branch_patterns into infer fixpoint

Codex blocker on bb8223aa: pattern resolution ran after the main
infer fixpoint, so a Branch that the coverage pass flipped to
Unresolved (non-exhaustive match, duplicate arm) couldn't cascade
to downstream consumers whose ports were already Resolved. The
stale Resolved types leaked through the compile boundary and
violated FAIL-CLOSED.

Fix: fold `resolve_branch_patterns` into the fixpoint loop. The
helper now returns `bool` indicating whether any state changed
(Path.pattern rewrite OR Branch output port transition). When it
reports a change, the loop continues, and the next decide pass
sees Branch outputs as Unresolved and cascades Decision::Fail
through Transform / Branch / Loop / Bind consumers via the
existing upstream-failure guard in decide_transform. Eventually
the fixpoint settles with every invalid-match-descendant port
Unresolved, matching what FAIL-CLOSED requires.

Changed signatures + call sites:
- `resolve_branch_patterns(&mut Dag) -> bool` (was `-> ()`)
- infer's main loop calls it each iteration; `changed |= ...`
- rewrite branch sets `changed = true` when Path.pattern is
  mutated or when a pattern resolution error marks the port
- coverage branch sets `changed = true` on duplicate / missing
  arm diagnostics

Regression test `m18_r12_invalid_match_cascades_to_downstream_callers`:
compiles a fn with a non-exhaustive match body and asserts the
Bind's value port cascaded to Unresolved after infer. Before R12,
the Bind.value port was Resolved(Int) because the fixpoint had
converged before pattern resolution fired.

Non-blocking: refreshed parse.rs file header comment. M1(2.5)-era
text said "Operators compile to identifier-shaped Calls" which
was accurate then but replaced at M1(2.7) by `SurfaceExpr::Operator`
committing to `OperatorKind` at parse time. Updated to reflect the
current lowering path through `TransformTarget::Operator` and the
§8.9 algebra walk in `infer::resolve_operator_arrow`.

Coverage: 41 M0 + 26 M1 substrate (25 existing + 1 new R12
cascade test) + 7 real-stdlib smoke + 1 realization smoke = 75
green. Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R13 — mutual-recursion rejection poisons callers

Codex blocker on ca62e174: the mutually-recursive fn rejection
path stored `ArrowBody::Pending`, which `decide_transform` accepts
as a realization-lag scaffold (signature type-checks, body walking
skipped). Downstream callers of a mutually-recursive fn got
Resolved types from the declared signature even though the
callee's Bind value port was already Unresolved — a FAIL-CLOSED
leak, producer-invalidity facts severed at the call boundary.

Fix: change the mutual-recursion path to set
`body: ArrowBody::UserDefined(bind_id)` instead of `Pending`. The
UserDefined arm of `decide_transform` already reads the Bind's
value port state: Uninferred → Retry, Unresolved → fail the call
with "function `<name>` has an invalid body", Resolved → accept.
Routing mutual-recursion rejection through this arm cascades the
failure to callers via the existing upstream-failure mechanism.

The non-mutually-recursive rejection paths in the same function
(zero-param recursion, non-descent-provable recursion) already
use this shape — they fall through to the common
bottom-of-function code that emits UserDefined(bind_id). Only
the mutual-recursion branch was using Pending.

Regression test `m18_r13_mutual_recursion_poisons_callers`:
compiles `fn a(n: Int) -> Int = b(n); fn b(n: Int) -> Int = a(n);
let c = a(1)` and asserts the Bind(c).value port is Unresolved
after compile. Before R13, c was Resolved(Int) because the
Pending body bypassed the Bind check at the call site.

Coverage: 41 M0 + 27 M1 substrate (26 existing + 1 new R13
cascade test) + 7 real-stdlib smoke + 1 realization smoke = 76
green. Clippy clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: docs — track where-clause refinement loss as class-5 gap #5

Codex review on 5d0fc6dd was ✅ blocking:0 overall but flagged two
previously-flagged roadmap items still unresolved: Bool/collection
operator grounding (already tracked as class-5 gaps #1 and #2)
and skip_where_clause refinement fact loss (not yet tracked).

Added class-5 gap #5 describing what's missing (refinement
predicates on type aliases like CommitSha = String where sha1(.)),
why it's hard (requires a new Declaration field, new
RefinementSpec shape, new inference enforcement at value
boundaries), what the options are, and current status (the
skip_where_clause bridge at parse.rs:801 loses the fact
entirely).

Doc-only — no code changes. The PR is green and mergeable; this
just brings DOWNSTREAM_REQUIREMENTS in sync with what codex has
been asking us to track.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R14 — reject Unparsed scaffolds in user-range declarations

Codex blockers on 636947fb: FnExternalBody and Data items compile
cleanly in ordinary user code, leaving ArrowBody::Unparsed and
ValueBody::Unparsed scaffolds in user-range declarations with no
later rejection. `fn foo(x: Int) -> Int { junk }` and
`data foo: Int = { junk }` both round-tripped through compile_to_dag
without a diagnostic, violating THESIS.md static grounding and
modeling-discipline.md principle 1 FAIL-CLOSED.

Context: these scaffolds exist so the std/bootstrap files with
match/record/pipe/lambda bodies can parse cleanly (their bodies
stay as preserved source spans, dissolved when the parser grows
to cover the remaining grammar — DOWNSTREAM_REQUIREMENTS.md
class-5 gaps #3 and #5). Bootstrap-range declarations still need
them. Ordinary user code never should.

Fix: add `reject_user_unparsed_scaffolds(dag, strict_from)` sweep
in lower.rs that walks declarations at id `>= strict_from` (the
user-lowered range after bootstrap) and emits fail-closed
diagnostics for:
- `TypeConnective::Arrow { body: ArrowBody::Unparsed(span), .. }`
- `Declaration.value_body == Some(ValueBody::Unparsed(span))`

Called from `lower()` alongside `resolve_pending_identifiers_strict`.
Bootstrap-range declarations (id < strict_from) are still
tolerated — those scaffolds exist by design until the parser
catches up.

Regression tests:
- `m18_r14_user_block_bodied_fn_is_rejected`: user-code
  `fn foo(x: Int) -> Int { junk }` returns Err from compile_to_dag.
- `m18_r14_user_data_with_opaque_body_is_rejected`: user-code
  `data foo: Int = { junk }` returns Err.

Coverage: 41 M0 + 29 M1 substrate (27 existing + 2 new R14) +
7 real-stdlib smoke + 1 realization smoke = 78 green. Clippy
clean (collapsible-match warning fixed in the same pass).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R15 — walk aliases/instantiation to the underlying Disj

Codex blocker on 0359e248: the new Branch gate in decide() and the
pattern-resolution pass both read scrutinee_decl.connective
directly, rejecting aliased or instantiated sum types even though
the underlying Disj fact survives in the declaration graph. A
match on `type Hue = Color` where `Color = Red | Green | Blue`
would fail the gate because Hue's immediate connective is
Instantiation { template: Color }, not Disj. Violates Facts Flow
Forward.

Fix: add `walk_to_disj_decl(dag, start) -> Option<DeclarationId>`
that walks through `Instantiation` / `ResolvedIdentifier` /
`Atom(ResolvedIdentifier)` edges until it reaches a declaration
whose connective is `Disj`. Shared between decide_transform's
Branch gate and resolve_branch_patterns — both sites now
normalize aliased / instantiated sum scrutinees to the same
underlying Disj before variant resolution and coverage checks.

Regression tests:
- m18_r15_match_on_aliased_sum_type_compiles: compile
  `type Color = Red | Green | Blue; type Hue = Color; fn
  classify(h: Hue) -> Int = match h { Red => 0, Green => 1,
  Blue => 2 }`. The Branch gate accepts Hue (walks to Color's
  Disj), and each Path.pattern resolves to a Color variant.
- m18_r15_non_exhaustive_match_on_aliased_sum_type_is_rejected:
  same alias setup but only covers 2 of 3 variants; the
  exhaustiveness check still fires via the walked Disj.

Coverage: 41 M0 + 31 M1 substrate (29 existing + 2 new R15) +
7 real-stdlib smoke + 1 realization smoke = 80 green. Clippy
clean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(2.8) R16 — Scaffold Boundaries invariant + substrate audit

Response to the root-cause analysis of the review cycle: each round
fixed a symptom, and the fix often introduced a new scaffold variant
that the next round audited. The pattern breaks when the invariants
file enforces the boundary rule up front.

Three deliverables:

1. **New sustainability invariant in INVARIANTS.md — Scaffold
   Boundaries.** Every substrate scaffold variant must have an
   explicit unreachability gate that rejects it for user-range
   declarations before compile_to_dag returns Ok. The invariant
   names R14 as the motivating example, spells out the principle /
   diagnostic / test / fix / structural prevention format matching
   the surrounding sustainability invariants, and adds a ratchet
   for future substrate PRs: any new variant must ship with either
   a terminal 4-pattern receipt or a bounded-scaffold receipt
   (unreachability gate + regression test + dissolution trigger).

2. **Audit of every existing scaffold variant** in
   DOWNSTREAM_REQUIREMENTS.md. Walked:
   - ArrowBody::Unparsed — ✅ bounded by R14's reject_user_unparsed_scaffolds
   - ValueBody::Unparsed — ✅ bounded by same sweep
   - AtomPayload::UnresolvedIdentifier — ✅ bounded by resolve_pending_identifiers_strict
   - BranchPattern::UnresolvedVariant — ✅ bounded by resolve_branch_patterns in the fixpoint (with a latent edge case documented for emit-stage consumers)
   - ArrowBody::Pending — implicit boundary via grammar; first-class
     fn values aren't callable at M1(2.8), and the three production
     roles (algebra field signatures, user Arrow type annotations,
     operator fallback bridge) are either structurally unreachable
     via user dispatch or legitimately body-less by design.

3. **ArrowBody::Pending dissolution ledger honesty update.** The
   earlier ledger described Pending as "bootstrap realization lag"
   that would dissolve via a §8.11 monotonic-decrease ratchet when
   every Pending arrow binds to ExternalRealization. But production
   bootstrap has zero realization-lag arrows and hundreds of
   Pending arrows in three legitimate "no concrete body needed"
   roles. Updated the dag.rs receipt to honestly describe all
   three uses; no code change — the semantics are unchanged, only
   the receipt.

Context: R14 added the rejection sweep for the two Unparsed
variants, but the wider question "does every scaffold have a
boundary?" wasn't posed. The audit in this commit confirms the
other three scaffold variants all have boundaries. The invariant
in INVARIANTS.md turns this into a ratchet for future PRs — the
cycle breaks when the boundary check is a precondition for
landing a new variant, not a post-hoc audit after a reviewer
finds a leak.

Coverage: 80 green, clippy clean. Doc + receipt changes only;
no runtime or test changes.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* v3: M1(3) PR-B phases 1-5 — substrate grounding for Rust emission

Ship the substrate + lens foundation needed for PR-B's Rust emitter.
The 100% structural scope from the plan: data items with record-
literal bodies lower to a new ValueBody::Structural variant carrying
the field labels + literal bits; `dsl/extdeps/languages/rust.dag`
loads as a bootstrap fixture declaring Realization and 18 Rust-side
realization facts; a cost lens lands as the third observational lens
in the lens_depth/lens_provenance template.

Phase 1 — Parser (SurfaceExpr::Record + data body integration):
  - New SurfaceExpr::Record { fields, span } variant.
  - parse_data_item uses a 3-token lookahead (`{` → Ident → `:`) to
    distinguish record-literal bodies from unparseable bodies.
    Fallback path (brace-skip) preserved for non-record bodies.
  - New parse_record_literal helper.
  - Walk helpers (is_recursive/descent_provable/collect_calls) gain
    Record arms.

Phase 2 — Substrate (ValueBody::Structural variant):
  - ValueBody grows Structural { fields: Vec<(String, LiteralBits)> }.
    Dissolution ledger updated with 4-pattern receipt; the new variant
    is terminal at PR-B scope (class-5 gap #3 tracks the upgrade to
    nested records / port-carried field values).
  - reject_user_unparsed_scaffolds narrowed to match only Unparsed;
    Structural passes through unchecked as the structurally-grounded
    form, not a scaffold.

Phase 3 — Lowering (data body inhabitance checking):
  - walk_to_conj_decl helper mirrors walk_to_disj_decl from R15;
    walks Instantiation/ResolvedIdentifier edges to a Conj.
  - lower_record_to_structural enforces: type walks to Conj, no extra
    fields, no missing fields, scalar-literal field values only, and
    each literal's type matches the declared field type. Fails
    fail-closed with diagnostics anchored to the offending span.
  - Type check uses declaration_by_name("Int"/"Bool"/"String")
    directly — the primitive cache isn't populated until the end of
    bootstrap, AFTER lower_bodies_phase runs for rust.dag.
  - lower_data_item populates meta_tag from the type annotation even
    on the Unparsed fallback path; structural bodies take precedence.
  - SurfaceExpr::Record in user-code expression position emits a
    fail-closed diagnostic naming class-5 gap #3 as the follow-up;
    M1(3) only supports record literals in data-body position.

Phase 4 — rust.dag + bootstrap fixture:
  - New dsl/extdeps/languages/rust.dag with the Realization meta-type
    (target_name/op_name/carrier/cost — all scalar fields matching
    ValueBody::Structural's literal-only constraint) and 18 data
    items: 3 primitive mappings, 10 operator realizations, 3
    structural templates (Bind/Branch/Main).
  - bootstrap.rs appends rust.dag after string_type.dag so String is
    resolved by the time Realization.target_name lowers.
  - rust_main_wrap's carrier uses `%Q` as a literal-double-quote
    placeholder — the v3 tokenizer has no escape sequences, so `\"`
    inside a string is impossible.

Phase 5 — lens_cost.rs (third observational lens):
  - Pure-reader CostLens following the lens_depth/lens_provenance
    template. Transform costs 1 + sum(inputs); Branch costs 1 + cond
    + max(paths) (runtime fires exactly one path); Loop costs 1 +
    source + init; Value / parameters are leaves; Bind passes through.
  - 6 acceptance tests: literals, single transform, chained transform,
    branch max-of-paths, branch asymmetric paths, Bind pass-through.

Tests — m1_substrate_test.rs:
  - m1_3_prb_data_item_record_body_lowers_structurally uses local
    names (LocalMeta/test_local_item) to avoid colliding with
    rust.dag'…
briansrls added a commit that referenced this pull request Apr 18, 2026
Three additions per reviews on 12fbaff / 3a897f4:

**Identity-across-sites as a checked invariant (chatgpt design question).**
`test_3a4_refined_generic_identity_across_instantiation_sites` now
asserts a structural invariant rather than just verifying compilation
success. After compile, count anonymous refined-Int declarations
whose connective is `Atom(ResolvedIdentifier(Int))`. Expected: 2
(one per caller's own `where` clause). Dedup failure would produce
3+ as materialize-allocated carriers accumulate. Directly checks the
substrate-hygiene claim from D7 — if dedup regresses, the test fires
before duplicate carriers pollute the DAG.

**Test #7 (narrowing × substitution composition, claude-review).**
`test_3a4_refined_generic_narrowing_composite_discharges` locks the
cross-product of DB-11 arm-local narrowing and DB-16 substitution.
Caller narrows concrete `pred_a(n)` via `if pred_b(n, n) then ...`;
DB-11 produces composite `pred_a(n) && pred_b(n, n)` on the caller's
refined port; DB-16 materializes the callee's substituted-refined
carrier with the same composite; flatten-and-subset discharge (DB-11)
runs unchanged over the shared substrate.

Note on narrowing shape: DB-11's `narrowable_var_name` (`lower.rs:845`)
requires a 2-argument cond with exactly one scope-bound free
variable, so `pred_b` takes two args of T with both call sites
passing `n` for both. First attempt used a 1-arg `pred_b(n)` cond
— rejected by narrowing eligibility; predicate never narrowed;
discharge failed. Fixed by mirroring DB-11's 2-arg narrowing
convention.

**Test #5 (retry-on-unbound) deferred to ROADMAP follow-up.**
`test_3a4_refined_generic_retry_on_unbound_type_param` would
exercise the `is_retryable_generic_decl` retry path when a
TypeParam is unbound at iteration N and bound at N+1, locking the
retry-then-succeed outcome. Currently implicit-covered by the
multi-site and callable-in-predicate bonus tests (both depend on
fixpoint convergence through retry iterations); explicit construction
of the scenario requires synthesized fixpoint-iteration timing.
Tracked as Lane 3 Stage 3a.3 follow-up with a 1-month yellow-flag
threshold after merge. Audit anchor: Q5 construction-authority
invariant preserved under retry.

36/36 test_3a_* tests pass (16 DB-11 + 13 DB-16 + 7 other). Full
v3-compiler test suite green; clippy + fmt gates clean.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 18, 2026
Addresses codex review on cec4cb0 (non-blocking, fix-in-PR-if-easy):
the design doc's Acceptance section listed
`test_3a4_refined_generic_retry_on_unbound_type_param` as shipped
baseline even though R3.2 deferred it to a ROADMAP follow-up
(`Landing: DB-16` → `Follow-up — fixpoint-retry explicit test`).

Test #5 now annotated as "Deferred to ROADMAP follow-up" with the
rationale: implicit-covered by multi-site + callable-in-predicate
bonus tests; explicit construction requires synthesized fixpoint-
iteration timing; 1-month yellow-flag threshold.

Design record no longer overstates 3a.3 closure coverage.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 18, 2026
…e) (#522)

* WIP: D

* docs: DB-16 R2 — Transform-target substitution in cloned predicate body

Addresses codex blocking review on Part 1 (SHA f879d5f): D2 as
originally written specified predicate-body cloning with only the
parameter slot re-pointed, so generic `Callable(Instantiation{...})`
targets inside predicate bodies would retain template-rooted
`TypeParam` arguments post-clone. At discharge, the callee's cloned
body would carry `Instantiation{args: [T -> S_outer]}` while the
caller's body carries `Instantiation{args: [T -> Int]}`, and
`declaration_shapes_equivalent` (infer.rs:3579-3618) bottoms out on
atom-to-atom for the argument comparison — discharge silently fails.

Extension (D2 step 4 + D4 + D6 + Impl pointer + Open Q2):
- `clone_predicate_body` gets a new `subst: &SubstStack` parameter.
  Transform-target walk routes `Callable(id)` and `FieldProject.field_child`
  through `concretize_decl_with_subst`. `Operator(_)` untouched.
- DB-11's callers pass an empty `SubstStack` (no behavior change;
  16 `test_3a3_*` tests guard the regression).
- Acceptance gains two tests: `test_3a4_refined_generic_callable_in_predicate_discharges`
  (positive: load-bearing against the codex-named regression class)
  and `test_3a4_refined_generic_callable_in_predicate_distinct_template_rejects`
  (negative: confirms D6 no-entailment preserved under substitution).
- D6 commitment unchanged: substitution is categorical (`T := Int`
  writes `Int` everywhere), not inference/implication/ordering.

ChatGPT review still in flight; any orthogonal signal lands as a
follow-up commit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: DB-16 R2.1 — fail-closed diagnostics + single-authority cache

Addresses ChatGPT review (APPROVE_WITH_COMMENTS, non-blocking) on
SHA f879d5f. Two Part-2 clarifications folded into the design:

1. Fail-closed diagnostics (D2 steps 1, 2, 4). Once D1 establishes
   that substitution is required, subsequent failures (substituted
   base doesn't resolve, malformed predicate shape, out-of-fragment
   body reaching the materialize phase) register a Diagnostic per
   C-8 rather than silently returning None. Only unbound-TypeParam
   at D1 (legitimate retry absence) keeps the silent fallthrough.

2. Single-authority cache (D3, D7). Phase-based materialization
   locked: runs in materialize_callable_signature_instantiations
   (infer.rs:2236, already &mut Dag), extends
   concretize_decl_with_subst with a refinement branch. Dedup is a
   structural scan over dag.declarations() via
   find_equivalent_substituted_refined_decl — mirrors
   find_equivalent_anonymous_instantiation. The "cache" IS the Dag;
   no parallel semantic side table. signature_type_shape stays
   &Dag — no walker widening.

Open Q1 (`&Dag` vs `&mut Dag`) marked resolved: phase-based approach
chosen, rationale recorded in D3.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: DB-16 R2.2 — FieldProject acceptance lock (chatgpt R2 review)

Addresses ChatGPT review on R2 (SHA 04bd642, APPROVE_WITH_COMMENTS).
Non-blocking concern: D2 step 4 now makes two Transform-target
substitution arms load-bearing (Callable(id) and
FieldProject.field_child), but the Acceptance suite only locked the
Callable path.

Locks the FieldProject arm with test #11
(test_3a4_refined_generic_field_project_in_predicate_discharges):

    type Box<T> { inner: T, tag: Int }
    fn f<T>(x: Box<T> where x.tag != 0) -> Box<T> = x
    fn caller(b: Box<Int> where b.tag != 0) -> Box<Int> = f(b)

Tag-field-over-Int keeps the operator arm concrete so the test
isolates the FieldProject substitution path; pairs symmetrically
with #9 (Callable arm). Verifies D2's claim that FieldProject is
genuinely in the admitted Transform-target substitution class, not
a doc-only promise.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: DB-16 R3 — collapse to single construction authority

Addresses ChatGPT R2.1 review (SHA a13e383, REQUEST_CHANGES).
Blocking concern: R2.1's revised D3 moved construction to the
materialize phase (concretize_decl_with_subst branch), but D1, RA-4,
and Implementation Pointer still described signature_type_shape /
reattach_refinement_to_substituted_base as the constructor. Two
stories for one production site — avoidable "produce here, maybe
rediscover there" ambiguity Part 2 would inherit.

R3 collapses to one explicit authority:

- **Producer (D2):** concretize_decl_with_subst's new refinement
  branch, fired inside materialize_callable_signature_instantiations
  (&mut Dag). Sole construction site for substituted refined carriers.

- **Consumer (D1):** signature_type_shape gains a read-only pre-
  terminator branch. When refinement_base_requires_substitution
  fires, calls find_equivalent_substituted_refined_decl (&Dag, pure
  scan) to find the pre-materialized carrier. Lookup miss falls
  through to DB-11 identity-terminator + retry machinery.

Removed helper reattach_refinement_to_substituted_base — it was the
dual-authority artifact. D2's 7-step walk now explicitly runs inside
the concretize branch; no separate helper.

Touched sections: design preamble (new single-authority paragraph),
D1 (code sketch + narrative rewritten for lookup), D2 (opening
reframed), RA-4 (construction site = phase, not walker),
Implementation Pointer (split into Producer/Consumer sides),
Associations (construction site + lookup site distinguished).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* DB-16 Part 2: refined-generic substitution impl + tests (3a.3 closure)

Implements the design from docs/design-db16-refined-generic-substitution.md
(R3: unified construction authority).

**Producer (D2).** `concretize_decl_with_subst` (infer.rs:2706) gains
a refinement branch that fires before the connective match when
`decl.refinement.is_some()` AND `refinement_base_requires_substitution`
returns true. The branch calls `materialize_substituted_refined_decl`,
which performs the D2 7-step walk: resolve substituted base → extract
predicate slots → allocate fresh composite param port → clone
predicate body with Transform-target substitution → wrap in fresh
Bind → build fresh predicate-Arrow Declaration → allocate the fresh
substituted-refined carrier. Each failure mode registers an explicit
`Diagnostic::ResolveError` per C-8.

**Consumer (D1).** `signature_type_shape` stays `&Dag` read-only.
New pre-terminator branch: when the refinement base requires
substitution, call `find_equivalent_substituted_refined_decl` and
return the pre-materialized carrier if found. Lookup miss falls
through to the DB-11 identity-terminator + retry machinery.

**Transform-target substitution.** `clone_predicate_body` extended
with a `subst: &SubstStack` parameter. Transform-target walk routes
`Callable(id)` and `FieldProject.field_child` through
`concretize_decl_with_subst`. `Operator(_)` untouched. DB-11's
callers in `lower.rs` pass an empty `SubstStack` — regression-
guarded by all 16 `test_3a3_*` tests remaining green.

**Structural equivalence under substitution.**
`callable_decls_equal_under_subst` + `normalized_instantiation_args`
handle the template-side Instantiations that carry extra bindings
for outer TypeParams (e.g., gate's Instantiation{always_true,
[T'→T_gate, T_gate→T_gate]} vs caller's {always_true, [T'→Int]}):
normalize both to their template-own-type-param args only, then
resolve through subst and compare.

**Cross-module access.** `SubstStack` and `concretize_decl_with_subst`
promoted to `pub(crate)` in `infer.rs`. `clone_predicate_body` and
`outer_predicate_slots` promoted to `pub(crate)` in `lower.rs`.

**Acceptance.** `test_3a4_*` suite (9 new + 3 pre-existing) passes.
New DB-16 tests: discharges_across_substitution,
distinct_refinement_rejects, identity_across_instantiation_sites,
literal_arg_rejects, composite_discharges,
callable_in_predicate_discharges (Callable arm),
callable_in_predicate_distinct_template_rejects (no-entailment under
substitution), field_project_in_predicate_discharges (FieldProject
arm), substrate_integrity_behavior_still_five_variants. Tests use
`always_true<T>(x: T) -> Bool` generic-helper pattern so predicate
bodies type-check for abstract T.

**ROADMAP.** 3a.3 row flipped 🟡 Partial → ✅ Shipped. Closed-block
`Remaining (blocking for ✅ Shipped)` removed. New `Closed (DB-16,
PR #522)` entry. Added `Landing: DB-16 refined-generic substitution
(S, PR #522)` section.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* DB-16 R3.1: self-binding-only filter + harden materialize invariants

Addresses two reviews on 12fbaff:

**Codex BLOCKING (infer.rs:3244):** `normalized_instantiation_args`
previously filtered substituted callable-target instantiations down
to `template.type_params`, dropping all non-template-param bindings.
That silently collapsed two instantiations that differed only by
retained callable-argument identity — a Facts-Flow-Forward violation.

Fix: strip **only** self-bindings (`arg.parameter == arg.value`),
which are the reattachment artifacts from `resolve_callable_target`'s
unification under outer generic scopes (where outer TypeParams bind
to themselves pending inference). Non-self bindings carry semantic
identity from `retained_template_arguments_for_target` and are now
preserved across the equivalence walk. Two instantiations that differ
only by a non-self retained binding correctly compare unequal.

Why this still closes the original 1105-vs-1101 divergence: 1105 had
[T'→T_gate, T_gate→T_gate] — the second is self-binding, stripped.
Filtered form [T'→T_gate] matches 1101's [T'→Int] after subst.

**ChatGPT NON-BLOCKING (infer.rs:2873-2884, 2949-2952):** three
"defensive fallthrough" branches in `materialize_substituted_refined_decl`
silently returned `template_refined` on caller-contract violations
(missing refinement edge, non-ResolvedIdentifier connective, predicate
connective mutated post-slot-extraction). Per chatgpt's note: each
is probably unreachable today but could mask bugs if the construction
authority drifts.

Hardened to `unreachable!()` with explicit message naming the
violated caller contract. Truly-unreachable invariant violations now
panic with backtrace rather than degrading silently. Genuine
substrate-integrity failures (step-1 base resolution, step-2
predicate shape, step-4 out-of-fragment body) continue to attach
`Diagnostic::ResolveError` and return `template_refined` per C-8.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* DB-16 R3.2: close claude-review + chatgpt-review items

Three additions per reviews on 12fbaff / 3a897f4:

**Identity-across-sites as a checked invariant (chatgpt design question).**
`test_3a4_refined_generic_identity_across_instantiation_sites` now
asserts a structural invariant rather than just verifying compilation
success. After compile, count anonymous refined-Int declarations
whose connective is `Atom(ResolvedIdentifier(Int))`. Expected: 2
(one per caller's own `where` clause). Dedup failure would produce
3+ as materialize-allocated carriers accumulate. Directly checks the
substrate-hygiene claim from D7 — if dedup regresses, the test fires
before duplicate carriers pollute the DAG.

**Test #7 (narrowing × substitution composition, claude-review).**
`test_3a4_refined_generic_narrowing_composite_discharges` locks the
cross-product of DB-11 arm-local narrowing and DB-16 substitution.
Caller narrows concrete `pred_a(n)` via `if pred_b(n, n) then ...`;
DB-11 produces composite `pred_a(n) && pred_b(n, n)` on the caller's
refined port; DB-16 materializes the callee's substituted-refined
carrier with the same composite; flatten-and-subset discharge (DB-11)
runs unchanged over the shared substrate.

Note on narrowing shape: DB-11's `narrowable_var_name` (`lower.rs:845`)
requires a 2-argument cond with exactly one scope-bound free
variable, so `pred_b` takes two args of T with both call sites
passing `n` for both. First attempt used a 1-arg `pred_b(n)` cond
— rejected by narrowing eligibility; predicate never narrowed;
discharge failed. Fixed by mirroring DB-11's 2-arg narrowing
convention.

**Test #5 (retry-on-unbound) deferred to ROADMAP follow-up.**
`test_3a4_refined_generic_retry_on_unbound_type_param` would
exercise the `is_retryable_generic_decl` retry path when a
TypeParam is unbound at iteration N and bound at N+1, locking the
retry-then-succeed outcome. Currently implicit-covered by the
multi-site and callable-in-predicate bonus tests (both depend on
fixpoint convergence through retry iterations); explicit construction
of the scenario requires synthesized fixpoint-iteration timing.
Tracked as Lane 3 Stage 3a.3 follow-up with a 1-month yellow-flag
threshold after merge. Audit anchor: Q5 construction-authority
invariant preserved under retry.

36/36 test_3a_* tests pass (16 DB-11 + 13 DB-16 + 7 other). Full
v3-compiler test suite green; clippy + fmt gates clean.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: DB-16 R3.3 — align D3 wording with implementation helpers

Addresses ChatGPT review on 0d072a2 (lingering prose: D3 named
both `refinement_ports_equal` and `predicate_discharges` as the
dedup equivalence relation; the latter is composite-subset matching,
which would over-match in dedup). Also brings the doc in line with
the helpers R3.1 actually shipped.

Three prose tightenings:

1. **Strict structural equivalence, not discharge.** D3 now names
   `predicate_bodies_equal_under_subst` as the dedup relation — a
   strict lockstep walker modeled on DB-11's `refinement_ports_equal`.
   Removes `predicate_discharges` from the equivalence-relation
   wording (that helper is for conjunct-subset discharge, not
   dedup).

2. **Name the actual implementation helpers.** `callable_decls_equal_under_subst`
   and `normalized_instantiation_args` now appear in the doc with
   their actual semantics, matching `infer.rs`.

3. **Self-binding-only filter (R3.1).** D3 explicitly documents
   that `normalized_instantiation_args` strips **only** self-bindings
   (`arg.parameter == arg.value`) — the reattachment artifacts from
   `resolve_callable_target` unification under outer generic scopes.
   Non-self retained callable arguments are preserved so the
   Facts-Flow-Forward guarantee the codex R3.1 review locked in is
   documented, not just implemented.

4. **Dedup inclusive of user-authored carriers.** New paragraph
   explicit about the stronger guarantee the implementation provides:
   when a caller's `where` clause produces a structurally-equivalent
   carrier, the dedup scan returns the caller's carrier rather than
   allocating a fresh one. That is what
   `test_3a4_refined_generic_identity_across_instantiation_sites`
   checks (2 anon refined-Int carriers total, not 4).

Per the meta-review's KEEP_ITERATING prescription on Part 2: this
aligns the contract the remaining reviews will read against the
actual implementation object, rather than leaving them to reconcile
stale prose.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: D

* DB-16 R3.4 (revert WIP 484ca50) + authority-consolidation follow-up

Addresses ChatGPT R3.1 review (REQUEST_CHANGES): DB-16 maintains a
parallel equality authority (`predicate_bodies_equal_under_subst` +
`transform_targets_equal_under_subst` + `callable_decls_equal_under_subst` +
`normalized_instantiation_args`) shadowing DB-11's
`refinement_ports_equal` / `refinement_targets_equal` /
`declaration_shapes_equivalent`. Reviewer asked to either collapse
the dual authority or revert the ROADMAP ✅ Shipped flip.

**Attempt:** `484ca5034` (WIP: D auto-commit) tried the collapse —
extended `refinement_ports_equal` with `subst`, folded self-binding
normalization into `declaration_shapes_equivalent`'s Instantiation
arm, deleted the parallel stack.

**Regression:** the collapsed `refinement_targets_equal` resolved
the template side's Callable id through `resolve_decl_with_subst`
and then called `declaration_shapes_equivalent`. But
`declaration_shapes_equivalent` compares Instantiation argument
VALUES strictly, without threading subst. The pre-collapse
`callable_decls_equal_under_subst` had handled this via a
substitution-aware arg-value comparison. Without it, dedup scans
miss existing carriers; materialize reallocates per fixpoint
iteration; fixpoint never converges; tests hang.

**Correct consolidation path** requires threading `&SubstStack`
through `declaration_shapes_equivalent` itself, which has a
~20-call-site surface. Too wide for this PR round.

**Revert:** `src/v3/compiler/src/infer.rs` checked out from
`3dc043d7e` (R3.3 working state). 36/36 `test_3a_*` tests pass
(16 DB-11 + 13 DB-16 + 7 others). Clippy + fmt clean.

**Consolidation tracked as ROADMAP follow-up** under Landing: DB-16.
Yellow-flag threshold: 1 month after Part 2 merge. Design anchor:
`feedback_substrate_principle_audit` (single-authority invariant).

Honest posture: the parallel stack is correctness-preserving (dedup
emits strictly stronger matches than DB-11's discharge would, never
producing false dedups), but represents maintenance surface that
future drift would re-expose. The retained-argument bug Codex
caught in R3.1 was ONE class instance; the follow-up closes the
class structurally rather than locally.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: DB-16 R3.5 — mark test #5 deferred in Acceptance section

Addresses codex review on cec4cb0 (non-blocking, fix-in-PR-if-easy):
the design doc's Acceptance section listed
`test_3a4_refined_generic_retry_on_unbound_type_param` as shipped
baseline even though R3.2 deferred it to a ROADMAP follow-up
(`Landing: DB-16` → `Follow-up — fixpoint-retry explicit test`).

Test #5 now annotated as "Deferred to ROADMAP follow-up" with the
rationale: implicit-covered by multi-site + callable-in-predicate
bonus tests; explicit construction requires synthesized fixpoint-
iteration timing; 1-month yellow-flag threshold.

Design record no longer overstates 3a.3 closure coverage.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: DB-16 R3.6 — align D2 failure-path prose with shipped diagnostics

Addresses codex review on c016161 (non-blocking, fix-in-PR-if-easy):
D2's failure-path prose named `Diagnostic::Internal` (a variant that
doesn't exist in v3's Diagnostic enum) and "return None" semantics,
but the landed implementation uses `Diagnostic::ResolveError` and
returns `template_refined` (the template carrier, allowing
downstream retry machinery to take over via signature_type_shape's
lookup-miss path).

The `Diagnostic::Internal` name was a drafting artifact from R2.1's
fail-closed hardening pass — I discovered at implementation time
that the v3 Diagnostic enum has ResolveError / TypeMismatch /
ArityMismatch / ParseError / TokenizerError (no Internal variant),
used `attach_diagnostic(Diagnostic::ResolveError {...})` + return
template_refined via the `unreachable!()`-in-invariant-contract-
violation vs diagnostic-in-detectable-violation split that R3.1
hardened. The doc never caught up.

Three D2 steps (1, 2, 4) updated to reflect shipped semantics.
Substantive invariant unchanged: detectable substrate-integrity
violations attach a diagnostic (C-8 fail-closed); truly-unreachable
caller-contract violations panic via `unreachable!()` (R3.1).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants