Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -837,10 +837,11 @@ Classified as invariant violations:
(`Dynamic` matches anything, plus same-name/same-connective/same-child-count
fallback) that hide missing earlier normalization. This violates "No
fallbacks that fabricate" / "Explicit boundary contracts."
- Reconcile downgrades semantic gaps to `Warning`
(`access_error` / `inference_error`), and `compile_sources` gates only
on `Error`, so emit still runs on known inference/access gaps. This is
a warning-permissive boundary rather than a fail-closed one.
- ~~Reconcile downgrades semantic gaps to `Warning`~~
**FIXED (2026-04-01).** `OwnershipWarning` renamed to `OwnershipViolation`,
`VariantCollisionWarning` renamed to `VariantCollision`, both promoted to
errors. `is_error_diagnostic` now always returns `true`. No warning
severity remains in the compiler.

Not invariant violations by themselves:

Expand Down Expand Up @@ -964,13 +965,12 @@ error state is encoded as:
- `LitNull` with `return_type: none` (37 sites across parser/reconcile/emit)
- `Dynamic` type name (universal compat in `node_type_equals`)
- `<error:*>` strings detected by `string_contains` (2 check sites, 4 production sites)
- `Warning` severity for semantic errors (`access_error`, `inference_error`)
- ~~`Warning` severity for semantic errors (`access_error`, `inference_error`)~~ **FIXED (2026-04-01).** All diagnostics are now errors; `is_error_diagnostic` always returns `true`.

The fix: make error a structural variant — either an `ExprError` in ExprData
or a flag on Node — so downstream phases can test `is_error(node)` without
string parsing. Emit skips error nodes (or emits `compile_error!()`) instead
of translating fabricated values. Reconcile promotes `access_error` /
`inference_error` to Error severity so `compile_sources` gates correctly.
of translating fabricated values.

Parser LitNull recovery (23 sites in `02_parse.dag`) is a separate concern —
parser error recovery that produces dummy nodes with attached error
Expand All @@ -986,7 +986,7 @@ recognize these as error nodes and try to process them normally.
| C-5 | `<error:*>` detection via string_contains | 2 check | `04_reconcile.dag:900`, `05_emit_rust.dag:1473` |
| C-6 | `<error:unknown_*>` sentinels in emit | 2 | `05_emit_rust.dag:1766,2117` |
| C-7 | Dynamic as universal compatibility | multiple | `node_type_equals` in `04_reconcile.dag:901+`; `extend_scope_for_lambda` in `05_emit_rust.dag:1959` |
| C-8 | Warning severity for semantic errors | 2 helpers | `access_error` / `inference_error` at `04_reconcile.dag:1236,1245`; `compile_sources` gates on Error only |
| C-8 | ~~Warning severity for semantic errors~~ | **FIXED** | `OwnershipWarning` → `OwnershipViolation`, `VariantCollisionWarning` → `VariantCollision`; `is_error_diagnostic` always returns `true` (2026-04-01) |
| C-9 | Empty node / empty string fabrication | 2 | `05_emit_rust.dag:819` (empty Node for missing field), `05_emit_rust.dag:3368` (LitNull → "") |
| C-10 | `Rc::try_unwrap` clone fallback (v1) | 1 | `fn_codegen.rs:3783` — blocked on Track D ownership proof |

Expand Down
20 changes: 10 additions & 10 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -179,8 +179,8 @@ diagnostics. Generic fn syntax already supported by stage0 parser.
`lookup_in_scope` is a pure lookup with no synthesis.
- [x] `try_unwrap` clone fallback: ownership analysis
(`ownership.dag`) already proves fallbacks unnecessary.
Diagnostics wired into pipeline. Hard-error gate deferred
until ownership violations are promoted from warnings.
Diagnostics wired into pipeline. Ownership violations promoted
to errors (`OwnershipViolation`); no warning severity remains.

*Codegen correctness (pre-existing, not new in this PR):*
- Primitive type lowering, algebraic types, callable type, async fn
Expand Down Expand Up @@ -438,21 +438,21 @@ instead of hardcoding them. Includes FF-9 as prerequisite.
types and all 6 template data tables to `dsl/std/algebra.dag`
- [x] `00_core.dag` re-imports from `std.types` for backward compat
- [x] `04_types.dag` imports from `std.algebra`
- [ ] Convert per-profile field builders to `.dag` functions
- [x] Convert per-profile field builders to `.dag` functions
(`algebra_templates_for_profile` moved to `std/algebra.dag`)

*Tier 2 — factor `enrich_kernel_type` (modest compiler change):*
- [ ] `enrich_kernel_type` calls `.dag` function in `std/algebra.dag`
- [x] `enrich_kernel_type` calls `.dag` function in `std/algebra.dag`
(`algebra_templates_for_profile` moved to `std/algebra.dag`)
- [ ] Delete `intrinsic_method_index()` /
`runtime_bridge_method_index()`
- [ ] ~60 string branches → structural algebra queries

*Tier 2.5 — algebra bridge fidelity (no new infra, modeling only):*
- [ ] Fix `Set`/`NonEmptySet` profile: `FreeMonoidCollectionProfile`
→ `BooleanAlgebraCollectionProfile` (or split). The `std/algebra.dag`
denotation says sets inhabit `BooleanAlgebra<A>`, but the bridge maps
them to `FreeMonoidCollectionProfile` which gives them list operations
(append, sort_by, fold) instead of set operations (union, intersect,
diff, member). New profile + template list needed.
- [x] Fix `Set`/`NonEmptySet` profile: `FreeMonoidCollectionProfile`
→ `BooleanAlgebraCollectionProfile`. Added `BooleanAlgebraCollectionProfile`
variant, `boolean_algebra_collection_templates()`, and updated
`KERNEL_ALGEBRA_PROFILE` for `Set`/`NonEmptySet` in both `.dag` and stage0 Rust.
- [ ] Fix carrier-changing type loss in `free_monoid_collection_templates`:
`map`/`flat_map`/`fold` param_types and return_types are `ReceiverSelf`
but should express the higher-order function parameter structure (e.g.,
Expand Down
8 changes: 8 additions & 0 deletions docs/bootstrap-b-and-lane-work-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,10 @@ or FreeMonoid generic threading areas until the parallel work merges.

## 1. L1 Tier 1 Remaining: Per-Profile Field Builders → `.dag` Functions

> **Status: DONE (2026-04-01).** Per-profile builders are `.dag` functions
> in `std/algebra.dag`. `algebra_templates_for_profile` dispatcher also moved
> to `std/algebra.dag`. `04_types.dag` imports the dispatcher.

### What

Convert the six per-profile `data` template lists in `dsl/std/algebra.dag`
Expand Down Expand Up @@ -145,6 +149,10 @@ Can land on `main` independently.

## 2. L1 Tier 2.5: Fix Set/NonEmptySet Algebra Profile

> **Status: DONE (2026-04-01).** `BooleanAlgebraCollectionProfile` added
> with `boolean_algebra_collection_templates()`. `Set`/`NonEmptySet` updated
> in both `.dag` and stage0 Rust `KERNEL_ALGEBRA_PROFILE`.

### What

`kernel_algebra_profile` maps `"Set"` and `"NonEmptySet"` to
Expand Down
12 changes: 12 additions & 0 deletions dsl/std/algebra.dag
Original file line number Diff line number Diff line change
Expand Up @@ -493,3 +493,15 @@ fn partial_function_templates() -> List<AlgebraFieldTemplate> {
{ name: "length", param_types: [ReceiverSelf], return_type: NamedTemplate { name: "Int" } }
]
}

fn algebra_templates_for_profile(profile: AlgebraProfile) -> List<AlgebraFieldTemplate> {
match profile {
OrderedRingProfile => ordered_ring_templates()
ApproximateFieldProfile => approximate_field_templates()
BooleanAlgebraProfile => boolean_algebra_templates()
BooleanAlgebraCollectionProfile => boolean_algebra_collection_templates()
FreeMonoidScalarProfile => free_monoid_scalar_templates()
FreeMonoidCollectionProfile => free_monoid_collection_templates()
PartialFunctionProfile => partial_function_templates()
}
}
16 changes: 8 additions & 8 deletions dsl/std/symbols.dag
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,10 @@ type SymbolId
| Spinner8
| Spinner9
// Status indicators (general purpose)
| Success
| Failure
| Warning
| Info
| StatusSuccess
| StatusFailure
| StatusWarning
| StatusInfo
// Data type indicators
| DataList
| DataMap
Expand Down Expand Up @@ -138,10 +138,10 @@ data standard_symbols: List<SymbolEntry> = [
{ id: Spinner9, emoji: "/", unicode: "/", ascii: "/", color: Active },

// Status indicators
{ id: Success, emoji: "OK", unicode: "v", ascii: "OK", color: Success },
{ id: Failure, emoji: "FAIL", unicode: "x", ascii: "FAIL", color: Error },
{ id: Warning, emoji: "WARN", unicode: "!", ascii: "WARN", color: Warning },
{ id: Info, emoji: "INFO", unicode: "i", ascii: "INFO", color: Info },
{ id: StatusSuccess, emoji: "OK", unicode: "v", ascii: "OK", color: Success },
{ id: StatusFailure, emoji: "FAIL", unicode: "x", ascii: "FAIL", color: Error },
{ id: StatusWarning, emoji: "WARN", unicode: "!", ascii: "WARN", color: Warning },
{ id: StatusInfo, emoji: "INFO", unicode: "i", ascii: "INFO", color: Info },

// Data type indicators
{ id: DataList, emoji: "[L]", unicode: "=", ascii: "[L]", color: Default },
Expand Down
14 changes: 7 additions & 7 deletions src/v2/00_core.dag
Original file line number Diff line number Diff line change
Expand Up @@ -307,7 +307,8 @@ type CompilerDiagnostic
| MissingAnnotation { fn_name: String, what: String, span: SourceSpan }
| ParseError { message: String, span: SourceSpan }
| InternalError { message: String, span: SourceSpan }
| OwnershipWarning { binding: String, fn_name: String, consumers: Int, span: SourceSpan }
| OwnershipViolation { binding: String, fn_name: String, consumers: Int, span: SourceSpan }
| VariantCollision { variant: String, enum1: String, enum2: String, span: SourceSpan }

type ErrorNode {
diagnostic: CompilerDiagnostic
Expand All @@ -333,7 +334,8 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
MissingAnnotation { fn_name: _, what: _, span: s } => s
ParseError { message: _, span: s } => s
InternalError { message: _, span: s } => s
OwnershipWarning { binding: _, fn_name: _, consumers: _, span: s } => s
OwnershipViolation { binding: _, fn_name: _, consumers: _, span: s } => s
VariantCollision { variant: _, enum1: _, enum2: _, span: s } => s
}
}

Expand All @@ -352,15 +354,13 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
MissingAnnotation { fn_name: f, what: w, span: _ } => concat("function '", f, "' requires ", w, " annotation")
ParseError { message: m, span: _ } => m
InternalError { message: m, span: _ } => m
OwnershipWarning { binding: b, fn_name: f, consumers: c, span: _ } => concat("ownership: binding '", b, "' in '", f, "' has ", to_string(value: c), " consumers")
OwnershipViolation { binding: b, fn_name: f, consumers: c, span: _ } => concat("ownership: binding '", b, "' in '", f, "' has ", to_string(value: c), " consumers")
VariantCollision { variant: v, enum1: e1, enum2: e2, span: _ } => concat("variant '", v, "' appears in both '", e1, "' and '", e2, "'")
}
}

fn is_error_diagnostic(d: CompilerDiagnostic) -> Bool {
match d {
OwnershipWarning { binding: _, fn_name: _, consumers: _, span: _ } => false
_ => true
}
true
}

fn make_error_node(diagnostic: CompilerDiagnostic, module_name: String) -> ErrorNode {
Expand Down
53 changes: 34 additions & 19 deletions src/v2/04_infer.dag
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ import v2.std.core {
NodeType, Typed, InferError, InferVariable, Untyped,
Cardinality, Required, CardOptional,
ErrorNode, make_error_node, is_error_diagnostic,
InternalError,
InternalError, VariantCollision,
resource_use_name, resource_use_resource,
kernel_type_set, is_kernel_type,
expr_has_self_call, expr_has_non_tail_self_call,
Expand Down Expand Up @@ -166,6 +166,11 @@ type ModuleContext {
diagnostics: List<ErrorNode>
}

type VariantFoldState {
locals: Map<String, TypeBinding>
collision_errors: List<ErrorNode>
}

type InferScope {
type_env: TypeEnv
func_env: ResolvedFuncEnv
Expand Down Expand Up @@ -2498,32 +2503,42 @@ fn build_module_context(contributions: List<ItemContribution>,
// Disambiguation: when a variant name appears in multiple enums (e.g. Rust
// in both RenderTarget and CodegenBackend), prefer the enum explicitly named
// in this module's imports over ambient std.types injection.
let imported_variant_locals = fold(env.bindings |> map_values, init: empty_map(), f: (acc, binding) =>
// Pre-compute import membership as an indexed set (FF — facts flow forward).
let imported_enum_names = fold(resolved_imports, init: empty_map(), f: (acc, imp) =>
fold(imp.specific_names, init: acc, f: (inner, n) => map_insert(inner, n, true))
)
let variant_fold = fold(env.bindings |> map_values, init: VariantFoldState { locals: empty_map(), collision_errors: [] }, f: (acc, binding) =>
let is_coproduct = binding.resolved.connective == Disj
if is_coproduct {
let curr_is_imported = map_get(imported_enum_names, binding.resolved.name) != none
fold(binding.resolved.children, init: acc, f: (vacc, child) =>
match map_get(vacc, child.name) {
Some { value: _ } =>
// Ambiguous: only replace if current enum is explicitly imported.
// Avoids accessing prev.resolved.name (inference gap on bare Map value type).
let curr_is_imported = resolved_imports |> any(imp =>
imp.specific_names |> any(n => n == binding.resolved.name)
)
if curr_is_imported {
map_insert(vacc, child.name, TypeBinding {
name: child.name,
resolved: binding.resolved
})
match map_get(vacc.locals, child.name) {
Some { value: prev } =>
let prev_is_imported = map_get(imported_enum_names, prev.resolved.name) != none
if curr_is_imported && prev_is_imported {
// Both enums explicitly imported — ambiguous. Remove the
// binding so later phases cannot consume a fabricated choice.
VariantFoldState {
locals: vacc.locals,
collision_errors: list_push(vacc.collision_errors, make_error_node(diagnostic: VariantCollision { variant: child.name, enum1: prev.resolved.name, enum2: binding.resolved.name, span: no_span() }, module_name: module_name))
}
} else if curr_is_imported {
VariantFoldState {
locals: map_insert(vacc.locals, child.name, TypeBinding { name: child.name, resolved: binding.resolved }),

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Invariant violation: When two explicitly imported enums share a variant name, this code still overwrites locals with one enum after only emitting VariantCollisionWarning, fabricating a winner for an ambiguous reference and violating No fallbacks that fabricate / Explicit boundary contracts.

collision_errors: vacc.collision_errors
}
} else { vacc }
None =>
map_insert(vacc, child.name, TypeBinding {
name: child.name,
resolved: binding.resolved
})
VariantFoldState {
locals: map_insert(vacc.locals, child.name, TypeBinding { name: child.name, resolved: binding.resolved }),
collision_errors: vacc.collision_errors
}
}
)
} else { acc }
)
let imported_variant_locals = variant_fold.locals
let variant_collision_errors = variant_fold.collision_errors
let env_variant_locals = variant_locals_from_items(items: local.resolved_items, init: imported_variant_locals)
let merged_scope = merge_scope_from_imports(
remaining: resolved_imports,
Expand Down Expand Up @@ -2552,7 +2567,7 @@ fn build_module_context(contributions: List<ItemContribution>,
svc_registry: merged_scope.svc_registry,
locals: all_locals,
item_registry: local.item_registry,
diagnostics: concat(flat_map(local.diag_chunks, c => c), resolve_result.diagnostics)
diagnostics: concat(concat(flat_map(local.diag_chunks, c => c), resolve_result.diagnostics), variant_collision_errors)
}
}

Expand Down
17 changes: 1 addition & 16 deletions src/v2/04_types.dag
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,7 @@ import std.algebra {
NamedTemplate, ReceiverCollectionOf, ListOf, OptionalOf, TupleOf,
AlgebraFieldTemplate,
kernel_algebra_profile,
ordered_ring_templates, approximate_field_templates, boolean_algebra_templates,
boolean_algebra_collection_templates,
free_monoid_scalar_templates, free_monoid_collection_templates,
partial_function_templates
algebra_templates_for_profile
}
import v2.std.core {
Node, make_param_node, param_node_type_expr,
Expand Down Expand Up @@ -198,18 +195,6 @@ fn instantiate_algebra_field(template: AlgebraFieldTemplate, base: Node) -> Node
}
}

fn algebra_templates_for_profile(profile: AlgebraProfile) -> List<AlgebraFieldTemplate> {
match profile {
OrderedRingProfile => ordered_ring_templates()
ApproximateFieldProfile => approximate_field_templates()
BooleanAlgebraProfile => boolean_algebra_templates()
BooleanAlgebraCollectionProfile => boolean_algebra_collection_templates()
FreeMonoidScalarProfile => free_monoid_scalar_templates()
FreeMonoidCollectionProfile => free_monoid_collection_templates()
PartialFunctionProfile => partial_function_templates()
}
}

// Enrich a kernel type with algebraic structure fields.
// Looks up the algebra profile from kernel_algebra_profile data table,
// instantiates field templates against the receiver shape, and wraps the result
Expand Down
19 changes: 16 additions & 3 deletions src/v2/compile.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ module v2.compiler.compile

import v2.std.core {
CompileResult, TextFile, SourceSpan,
ErrorNode, CompilerDiagnostic, is_error_diagnostic, diagnostic_to_message, diagnostic_to_span, make_error_node, InternalError, OwnershipWarning, no_span,
ErrorNode, CompilerDiagnostic, is_error_diagnostic, diagnostic_to_message, diagnostic_to_span, make_error_node, InternalError, OwnershipViolation, no_span,
Connective, NoConnective, Cardinality,
resource_use_name, resource_use_resource,
param_node_name, param_node_type_expr, param_node_default_value, param_node_span,
Expand Down Expand Up @@ -119,7 +119,7 @@ fn ownership_diagnostics(proofs: List<OwnershipProof>) -> List<ErrorNode> {
proof.decisions |> flat_map(decision =>
match decision {
SharedError { binding: binding, consumer_count: count, sites: sites } =>
[make_error_node(diagnostic: OwnershipWarning { binding: binding, fn_name: proof.func_name, consumers: count, span: no_span() }, module_name: proof.func_name)]
[make_error_node(diagnostic: OwnershipViolation { binding: binding, fn_name: proof.func_name, consumers: count, span: no_span() }, module_name: proof.func_name)]

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Invariant violation: Stage 6 now emits OwnershipViolation diagnostics here, but the pipeline still proceeds through artifact planning and emit without gating on ownership_diags, so a known error crosses the ownership→emit boundary in violation of the Early Detection invariant.

_ => []
}
)
Expand Down Expand Up @@ -653,7 +653,7 @@ fn serialize_typed_module(module: TypedModule) -> String {
}

fn serialize_diagnostic(diagnostic: ErrorNode) -> String {
let severity = if is_error_diagnostic(d: diagnostic.diagnostic) { "error" } else { "warning" }
let severity = "error"
concat(
"{\"severity\": ", json_quote(s: severity),
", \"message\": ", json_quote(s: diagnostic_to_message(d: diagnostic.diagnostic)),
Expand Down Expand Up @@ -842,6 +842,19 @@ fn compile_sources(sources: List<SourceFile>, target: RenderTarget) -> PipelineR
let ownership = extract_ownership_proofs(typed: typed)
let ownership_diags = ownership_diagnostics(proofs: ownership)

// Gate: ownership errors block emission (Early Detection invariant).
let ownership_errors = ownership_diags |> filter(d => is_error_diagnostic(d: d.diagnostic))
if ownership_errors |> count > 0 {
return PipelineResult {
files: [],
diagnostics: concat(frontend.diagnostics, norm_diags, all_infer_diags, ownership_diags),
complexity: complexity,
ownership: ownership,
artifact_plan: empty_artifact_plan(),
newline_indices: newline_indices
}
}

// Stage 7: Default artifact planning for the current single-artifact flow.
let artifact_plan = default_artifact_plan(
root_modules: typed.modules |> map(m => m.module.name),
Expand Down
4 changes: 2 additions & 2 deletions src/v2/stage0/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use v2_compiler::v2_compiler_compile;
use v2_compiler::v2_compiler_compile::PipelineResult;
use v2_compiler::v2_compiler_artifact;
use v2_compiler::v2_std_core::{
is_error_diagnostic, diagnostic_to_message, diagnostic_to_span,
diagnostic_to_message, diagnostic_to_span,
byte_to_line_col, source_line_at, NewlineIndex,
};

Expand Down Expand Up @@ -297,7 +297,7 @@ fn render_one_diagnostic(
index_map: &HashMap<String, Rc<NewlineIndex>>,
indent: &str,
) {
let severity = if is_error_diagnostic(d.diagnostic.clone()) { "error" } else { "warning" };
let severity = "error";
let message = diagnostic_to_message(d.diagnostic.clone());
let span = diagnostic_to_span(d.diagnostic.clone());

Expand Down
Loading
Loading