diff --git a/ROADMAP.md b/ROADMAP.md index d2c22735f5a..f1ed029e708 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -543,6 +543,40 @@ Three illegal-state boundaries dissolved, in order: the old `Bool + String?` adm Cleared (prior PR #521): `DerivedOpEffect { method, path_template, shape }` collapsed into `OperationEffect { operation_name, shape }`. The `method` / `path_template` fields were never consumed downstream — both the modifier check and obligation generator project through `shape` alone, and the `ReadEffect` variant already encodes "method was GET/HEAD/OPTIONS." `derive_op_effect` now returns `OperationEffect?` directly, so Stage 2b's `compose_effects` consumes the same shape derivation produces. Future diagnostic rendering that wants the originating method/path should attach a separate evidence carrier to the diagnostic, not smuggle transport facts onto the effect record. +### Lane 2 Stage 2d — symbolic cost (✅ Shipped) + +**DB-7 symbolic-cost algebra and per-Behavior lens landed.** Authority: [`design-symbolic-cost-algebra.md`](docs/design-symbolic-cost-algebra.md). Three .dag files + a Rust mirror + acceptance tests: + +- `src/v3/std/algebra.dag` — `SymbolicCost` coproduct (7 variants: Constant / Linear / Polynomial / Product / Sum / Log / Unknown) with a stamped 4-pattern dissolution receipt, `SizeVariable { source_port }`, `sequential` / `iterate` / `max_path` composition, `normalize` (drop zero, single-term reduction, `Linear(v) * Linear(v) → Polynomial(v, 2)` collapse), `dominates` partial order. +- `src/v3/std/dimensions.dag` — minimal `Dimension` + `Witness` types for Stage 2f's future generic walker. Full DB-3 abstraction (`analyze`, `DimensionReport`, bootstrap discovery) lands in 2f per its design doc's own sequencing. +- `src/v3/lenses/cost.dag` — per-Behavior lowering: Value → Constant(0); Transform → sequential(1, Σ inputs); Branch → sequential(1, condition, max_path(arms)); Loop → iterate(LinearCost(source), body); Bind → passthrough. Forward-fold accumulator pattern mirrors `lenses/complexity.dag`; `MissingCost` short-circuits every composition wrapper so malformed references never silently substitute a zero leaf. +- Rust mirror in `src/v3/compiler/src/dag.rs`: `SymbolicCost` / `SizeVariable` carriers and `sequential` / `iterate` / `max_path` / `normalize` / `dominates` functions — needed because `emit_rust_module`'s `is_bootstrap_file` filter excludes `src/v3/std/` declarations from Rust emission; same pattern `Behavior` / `LoopBound` use. +- `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens_cost_symbolic` binary. Exposed as `v3_compiler::lens_cost_symbolic::{symbolic_cost_of, SymbolicCostEntry, SymbolicCostLookup}`. +- Acceptance fixture: `src/v3/compiler/tests/lane2_stage_2d_symbolic_cost_test.rs` (20 tests). Covers Value/Transform/Branch/Loop lowering; recursive-fn body-cost fact-flow (PR #537 briansrls/codex BLOCKING); zero-drop normalization; `Linear(v) * Linear(v) → Polynomial(v, 2)` nested-fold fingerprint; cross-variable product stays `Product`; composite-dominance child-walk (PR #537 codex P2); `max_path` three-way step preserving incomparable branches (PR #537 briansrls BLOCKING) with an order-independence pin; dominance partial order (Unknown / Linear / Log / Polynomial degree ordering); `max_path` dominant-selection; checked-in generated-module snapshot guard. + +**Loop cost for `LoopBound::Descent` clusters uses `LoopNode.source` as the size-variable carrier.** The cluster's `members: NonSingletonList` and `intra_cluster_calls` carry the descent witnesses needed for the termination proof (#519), but the loop's own `source` port is the runtime value being descended upon — which is the honest recursion-depth bound for both `Cardinality` and `Descent` bounds. Richer per-member analysis (distinguishing list-descent from bounded-integer descent so `Descent` clusters report `ConstantCost` for bounded-int descent instead of `LinearCost`) is a Stage 2d follow-up, flagged in DB-7 §"Recursion depth bounds". + +**Substrate gap flagged for 2f pre-work: `data symbolic_cost_dimension: Dimension = { ... }` is DEFERRED to Stage 2f.** v3's surface grammar rejects record literals inside `data X: T = { ... }` bodies (DOWNSTREAM_REQUIREMENTS.md class-5 gap #3) and record / match / lambda inside `fn X { body }` block-bodied definitions simultaneously, which both shapes the `Dimension` record's field-carrying receipt pattern requires. The lens ships its behavior-variant lowering as the authority in the interim; Stage 2f materializes the `Dimension` instance alongside the grammar extensions that unlock it. Rationale + authority: DB-7 §"Dimension wiring" documents the target shape; cost.dag's closing comment block records the grammar-gap waypoint. + +**Build-script change (documented load-order fix).** `src/v3/compiler/build.rs` now prioritizes `list.dag` and `substrate.dag` ahead of alphabetical order within `STAGED_FILES`. Structural-recursion termination analysis walks a recursing argument back to its declared `Disj` connective via `structural_binding_info_for_variant`; the walk only succeeds after the declaring file has been phase-2 lowered, so std files that recursively descend over `List` or `Behavior` variants (post-2d: `src/v3/std/algebra.dag` and `src/v3/lenses/cost.dag`) need their dependencies loaded first. Without the priority list, alphabetical order put `algebra.dag` and `dimensions.dag` ahead of `list.dag`/`substrate.dag`, and their recursive helpers failed termination against placeholder connectives. Same pattern the spec loader already uses to pin `v3_l1.dag` first. + +**Acceptance-test infra migration (documented side effect).** Pre-existing tests that queried `dag.nodes().iter().find_map(Behavior::as_transform)` etc. on the `compile_to_dag` output assumed the bootstrap Dag contributed no `Transform` / `Branch` / `Loop` / `Bind` nodes before the user's source lowered. Lane 2 Stage 2d invalidates that assumption — `src/v3/std/algebra.dag`'s lowered bodies contribute many nodes. Eleven tests across four files migrated to filter by `span.file` (or subtract a bootstrap baseline) so they pin the user-code count/shape rather than the global node list: m0_acceptance's `test_let_binding_produces_dag_shape` (1); m1_substrate_test's `m17_operator_lowers_to_structural_transform_target`, `m17_comparison_operator_lowers_to_structural_transform_target`, `m17_user_function_call_lowers_to_callable_target`, `m18_r15_match_on_aliased_sum_type_compiles`, `m18_r13_mutual_recursion_poisons_callers`, `mutual_recursion_planner_ignores_callable_parameter_shadowing` (6); m1_3_emit_rust_test's three reflected-harness fixtures `rustc_roundtrip_emitted_module_matches_reflected_behavior_payloads`, `rustc_roundtrip_emitted_module_compares_reflected_port_ids_in_list_contains`, `rustc_roundtrip_emitted_module_returns_user_record_list_from_reflected_binds` (3); emit_rust.rs lib test `render_field_project_constructs_owned_list_from_borrowed_nodes` (1). This is a general test-authoring hygiene rule for every future std-module consumer to consider — a dedicated walker in Lane 1e would emit typed span-filtered iterators and dissolve the hand-written `.filter(|t| t.span.file == ...)` idiom. + +**Follow-up — `ProductCost` / `SumCost` NSL lift (not blocking, post-normalize-≥2-invariant gates graduation).** `SymbolicCost::ProductCost(List)` and `SymbolicCost::SumCost(List)` admit `[]` and singleton inputs at construction time; `normalize` already reduces both back to scalar variants, so the post-normalize canonical shape has `len ≥ 2`. Lift the field type to `NonSingletonList` (Track 9 vocabulary) so the `≥ 2 elements` fact becomes structural instead of a convention enforced only by `reduce_sum` / `reduce_product`. **Dissolution trigger:** the first call site that needs to pattern-match two guaranteed children without a `len() >= 2` check (likely a richer `normalize` variant or a multi-variable dominance rule). **Yellow-flag threshold: when a second normalization helper is added** — two such helpers is the moment the invariant becomes worth encoding at the type level. + +**Follow-up — `PolynomialCost.degree` typed carrier (not blocking, degree-arithmetic surface gates graduation).** `PolynomialCost { var, degree: Int }` — post-normalize, `degree >= 2` (degree = 1 collapses to `Linear`, degree = 0 to `Constant`). The raw `Int` admits 0, 1, and negatives; the domain constraint is behavioral, not structural. Replace with a typed carrier (`NonNegativeInt` at minimum; `DegreeAtLeastTwo` ideally). **Dissolution trigger:** DB-7's degree-arithmetic surface lands (multi-variable polynomial composition like `Polynomial(n, 2) * Polynomial(m, 3) = Polynomial`), which needs numeric operations on `degree` and is the natural moment to introduce the typed carrier. **Yellow-flag threshold: 1 month** after the first degree-arithmetic fixture lands on the lens side. + +**Follow-up — `LinearCost(v)` vs `PolynomialCost(v, 1)` canonicalization (not blocking, normalization-step extension gates graduation).** The two variants encode the same asymptotic fact; `dominates` and `normalize` explicitly pattern-match on both (`payload.degree <= 1` in the Polynomial-vs-Linear arm). Representation duality (audit Q6). Pick one canonical form — either dissolve `LinearCost` into `PolynomialCost(_, 1)`, OR constrain `PolynomialCost.degree ≥ 2` so `Linear` is the sole degree-1 surface. **Dissolution trigger:** the same normalization extension that introduces the `DegreeAtLeastTwo` typed carrier above — both items collapse cleanly when normalization collapses Linear↔Polynomial(_, 1) as a structural invariant. **Yellow-flag threshold: graduates alongside the typed-degree follow-up** (coupled dissolution). + +**Follow-up — `dominates` composite branches .dag↔Rust divergence (not blocking, cross-type mutual-recursion gates graduation).** Rust `src/v3/compiler/src/dag.rs::dominates` correctly walks children for `ProductCost` / `SumCost` (codex-flagged patch on this PR). The `.dag` authority `src/v3/std/algebra.dag::dominates` returns `False` conservatively for composites because #519's mutual-recursion termination analyzer only accepts cluster members sharing a descent parameter type — the list-iterating helper would descend on `List` while `dominates` descends on `SymbolicCost`, so the cluster can't form. Rust composite-dominance is the authority; .dag is an over-approximation. **Dissolution trigger:** substrate extension letting a mutual-recursion cluster admit cross-type members with per-member structural-descent witnesses (list-head / list-tail descent alongside variant-payload descent). Likely a Lane 1e or later addition to the termination-proof surface. **Yellow-flag threshold: 2 months** or whenever a second .dag↔Rust divergence shows up — the divergence between authorities is only tolerable as long as it's isolated to this single call. + +**Follow-up — `build.rs` load-order priority list bootstrap scaffold (not blocking, type-readiness signal gates graduation).** `src/v3/compiler/build.rs` prioritizes `list.dag` and `substrate.dag` ahead of alphabetical order so `structural_binding_info_for_variant` sees populated `Disj` connectives when downstream std files (Lane 2 Stage 2d's `algebra.dag` and the lens) are lowered. This is a bootstrap scaffold: the phase-order prerequisite lives in a filename priority list instead of flowing structurally from the declarations/import graph. **Dissolution trigger:** termination analysis grows a type-readiness signal (phase-1 declaration with fully-populated variant-list, rather than requiring phase-2-lowered body) so `structural_binding_info_for_variant` can succeed regardless of file order. When that lands, the priority list collapses to the empty default. **Yellow-flag threshold: whenever a third std file joins the priority list** — two entries is scaffold, three signals the rule is load-bearing enough to need structural lift. + +**Follow-up — symbolic-cost lens fixed-point cycle coverage (not blocking, `compile_stage_snapshots` extension gates graduation).** `src/v3/compiler/src/lens_cost_symbolic_generated.rs` is currently out of the `l1_5_fixed_point_test.rs` / `compile_stage_snapshots` stage-replay loop — that loop iterates pipeline stages (`parse` → `lower` → `infer` → `compute_ownership` → `emit` → `lens_complexity`) but does not include `lens_cost_symbolic` as a stage. Staleness today is guarded only by `cost_generated_module_matches_checked_in_snapshot` in `tests/lane2_stage_2d_symbolic_cost_test.rs`, which re-emits the module and compares against the checked-in file. That's drift protection, but narrower than the fixed-point cycle Complexity / Provenance / Structural-Resolution / Unused-Parameters get. **Dissolution trigger:** first-class stage registration for symbolic cost in `pipeline.dag` (adds a `lens_cost_symbolic` stage + realization), mirroring the existing `lens_complexity` wiring. When that lands, the lens's generated file automatically participates in the fixed-point comparison. **Yellow-flag threshold: 1 month** or whenever a second Stage 2d lens wants regen coverage. + +**Follow-up — hand-maintained `SymbolicCost` Rust mirror drift ratchet (not blocking, authority unification gates graduation).** PR #537 ChatGPT review (`sha:0f8c215c0`) call-out: the `SymbolicCost` / `SizeVariable` carriers + the composition functions (`sequential`, `iterate`, `max_path`, `normalize`, `dominates`, `reduce_sum`, `reduce_product`, `combine_binary_product`, `drop_dominated_in_sum`) are hand-maintained in `src/v3/compiler/src/dag.rs` because `emit_rust_module`'s `is_bootstrap_file` filter excludes `src/v3/std/` declarations from Rust emission. The scope is bounded (9 fns + 2 carrier types) and the current surface matches `src/v3/std/algebra.dag` modulo the documented composite-dominance gap (Follow-up above). The risk is future consumers attaching to the Rust mirror and not noticing when it drifts from the .dag authority — "declaration is the implementation" gets quietly replaced by "declaration + stronger hand-maintained Rust version" as the operating pattern. **Dissolution trigger:** the same substrate extension that closes the composite-dominance gap — once termination analysis admits cross-type mutual-recursion clusters, the .dag side matches Rust's richness and the hand-maintained mirror becomes `emit_rust_module`-generated like every other substrate type. Until then, a lightweight ratchet (e.g., a test that greps `src/v3/compiler/src/dag.rs` for fn signatures starting with `SymbolicCost::*` / `pub fn sequential|iterate|...` and cross-checks the count against `src/v3/std/algebra.dag` top-level `fn` decls) would catch silent expansion of the Rust surface. **Yellow-flag threshold: when a tenth hand-maintained fn is added to the mirror** — nine current fns is the baseline; a tenth without matching .dag growth is the signal that the scaffold is growing faster than the authority and needs explicit ratchet wiring. + + ### Lane 1 Stage 1b **Deferral: 1b full implementation (M).** 1b's first attempt escalated (PR #495 shipped 1a; 1b code was reverted). Root cause: `.dag` linear-walk bodies for substrate accessors polluted every user DAG. DB-14 codifies the correct pattern (ExternalRealization mirroring pipeline.dag). Unblocked once DB-14 (PR #497) lands. Design: [design-substrate-external-primitives.md](docs/design-substrate-external-primitives.md) (DB-14). Acceptance in DB-14 §Acceptance. diff --git a/src/v3/compiler/build.rs b/src/v3/compiler/build.rs index f2194362c4f..6d499a278d7 100644 --- a/src/v3/compiler/build.rs +++ b/src/v3/compiler/build.rs @@ -131,7 +131,19 @@ fn main() { println!("cargo:rerun-if-changed={}", spec_dir.display()); println!("cargo:rerun-if-changed={}", compiler_dir.display()); - let staged_entries = collect_dag_entries(&std_dir, &[]); + // Structural-recursion termination analysis walks a recursing + // argument back to its declared Disj connective (see + // `structural_binding_info_for_variant` in `lower.rs`). The walk + // only succeeds after the declaring file has been phase-2 lowered, + // so `std/list.dag` (declares `List = Empty | Cons {...}`) + // and `std/substrate.dag` (declares `Behavior = Value | Transform + // | Branch | Loop | Bind`) must land before any sibling std file + // that recursively descends over those variants. Without this + // priority list, alphabetical order puts `algebra.dag` and + // `dimensions.dag` ahead of `list.dag`/`substrate.dag`, and their + // recursive helpers fail termination against placeholder + // connectives. + let staged_entries = collect_dag_entries(&std_dir, &["list.dag", "substrate.dag"]); let spec_entries = collect_dag_entries(&spec_dir, &["v3_l1.dag"]); let compiler_entries = collect_dag_entries(&compiler_dir, &["pipeline.dag"]); let staged_generated = diff --git a/src/v3/compiler/src/bin/regen_lens_cost_symbolic.rs b/src/v3/compiler/src/bin/regen_lens_cost_symbolic.rs new file mode 100644 index 00000000000..9c7852081d7 --- /dev/null +++ b/src/v3/compiler/src/bin/regen_lens_cost_symbolic.rs @@ -0,0 +1,50 @@ +// Regen driver for `src/v3/lenses/cost.dag` — Lane 2 Stage 2d +// symbolic-cost lens (DB-7). Mirrors the shape of +// `regen_lens_cost.rs` (the structural-cost lens) so the two stay +// reviewable side by side. +// +// Output: `src/v3/compiler/src/lens_cost_symbolic_generated.rs`. + +use std::io::Write; +use std::path::PathBuf; +use std::process::{Command, Stdio}; + +use v3_compiler::compile_to_dag; +use v3_compiler::emit_rust::emit_rust_module; + +fn main() { + let lens_path = PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("lenses") + .join("cost.dag"); + let source = std::fs::read_to_string(&lens_path).expect("read cost.dag"); + let dag = + compile_to_dag(&source, lens_path.to_string_lossy().as_ref()).expect("cost.dag compiles"); + let raw = emit_rust_module(&dag).expect("emit lens module"); + let header = "// AUTO-GENERATED from `src/v3/lenses/cost.dag` via\n\ + // `emit_rust_module`. Regenerate instead of hand-editing.\n\n"; + let combined = format!("{header}{raw}"); + + let mut child = Command::new("rustfmt") + .arg("--emit") + .arg("stdout") + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .spawn() + .expect("spawn rustfmt"); + child + .stdin + .as_mut() + .unwrap() + .write_all(combined.as_bytes()) + .unwrap(); + let output = child.wait_with_output().expect("rustfmt"); + assert!(output.status.success(), "rustfmt failed"); + let formatted = String::from_utf8(output.stdout).expect("utf8"); + + let out_path = PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("src") + .join("lens_cost_symbolic_generated.rs"); + std::fs::write(&out_path, &formatted).expect("write lens_cost_symbolic_generated.rs"); + println!("wrote {}", out_path.display()); +} diff --git a/src/v3/compiler/src/dag.rs b/src/v3/compiler/src/dag.rs index 4b28d2d3a72..34d91d1cd72 100644 --- a/src/v3/compiler/src/dag.rs +++ b/src/v3/compiler/src/dag.rs @@ -1012,6 +1012,219 @@ impl LoopBound { } } +/// 🟢 TERMINAL at Stage 2d scope. Rust mirror of the +/// `SymbolicCost` coproduct declared in `src/v3/std/algebra.dag`. +/// The .dag declaration is the authority — this mirror exists +/// because `emit_rust_module` filters declarations from +/// `src/v3/std/` as bootstrap-resident, so the generated +/// `lens_cost_symbolic_generated.rs` references `SymbolicCost` +/// by name without re-declaring it. Keeping the Rust shape +/// adjacent to the other substrate carriers (`Behavior`, +/// `LoopBound`, `Cluster`) matches the existing pattern used for +/// every other .dag type the generated lenses consume. +/// +/// The `SizeVariable` name field the DB-7 design doc sketches is +/// deliberately not mirrored at this stage: the MVP render path +/// pins structural equality on `source_port` alone (two +/// `LinearCost` terms collapse to `PolynomialCost(var, 2)` when +/// their ports match), and pulling a user-facing name through +/// would require an InternTable lookup the lens doesn't yet run. +/// Name-rendering lands when a concrete display consumer pins +/// the missing piece — tracked in DB-7 Open Question §1's +/// size-variable normalization. +/// +/// Fields mirror the .dag variants exactly (anonymous tuple +/// payloads render as `{ _0: ... }`, record payloads render as +/// `{ field: ... }`); kept in sync by hand for now and tracked as +/// Lane 1e scheduled-deletion work when substrate emission grows +/// a cross-file type-mirror pass. +/// +/// See `docs/design-symbolic-cost-algebra.md` (DB-7) for the +/// dissolution receipt and variant rationale. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum SymbolicCost { + ConstantCost { _0: i64 }, + LinearCost { _0: SizeVariable }, + PolynomialCost { var: SizeVariable, degree: i64 }, + ProductCost { _0: Vec }, + SumCost { _0: Vec }, + LogCost { _0: SizeVariable }, + UnknownCost { _0: String }, +} + +/// 🟢 TERMINAL at Stage 2d scope. Rust mirror of `SizeVariable` +/// from `src/v3/std/algebra.dag`. Structural equality on +/// `source_port` is how two `LinearCost` terms collapse into +/// `PolynomialCost(var, 2)` through +/// `std.algebra::combine_binary_product` — the nested-fold +/// fingerprint DB-7's `all_pairs` acceptance fixture exercises. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SizeVariable { + pub source_port: PortId, +} + +// Composition functions mirroring `src/v3/std/algebra.dag`. +// `emit_rust_module` filters declarations under `src/v3/std/` as +// bootstrap-resident, so the functions there never emit their own +// Rust projection; `lens_cost_symbolic_generated.rs` references +// `sequential`, `iterate`, `max_path` by name and resolves them +// through `use crate::dag::*`. Kept in sync with the .dag source +// by hand for now, same cadence as the `SymbolicCost` variant +// mirror above. +// +// Algorithmic equivalence receipts: +// - `sequential` / `iterate` follow DB-7 §"Composition +// operations": sequential is a normalized sum, iterate is a +// normalized product. +// - `normalize` implements the Sum/Product reductions DB-7 +// §"Dominance / normalization" specifies: drop `ConstantCost(0)` +// out of sums, collapse singleton wrappers, fold two identical +// `LinearCost` terms into `PolynomialCost(var, 2)`. +// - `dominates` implements the dominance partial order: +// Unknown dominates everything (safest over-approximation), +// Constant dominated by every other variant, Polynomial degrees +// strictly-order, Linear≡Polynomial(v, 1), Sum/Product use +// dominant-child summary. + +pub fn sequential(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost { + normalize(SymbolicCost::SumCost { _0: vec![a, b] }) +} + +pub fn iterate(bound: SymbolicCost, body: SymbolicCost) -> SymbolicCost { + normalize(SymbolicCost::ProductCost { + _0: vec![bound, body], + }) +} + +pub fn max_path(paths: &[SymbolicCost]) -> SymbolicCost { + // Three-way step: candidate-wins / acc-wins / keep-both. Fixes + // PR #537 review (Facts Flow Forward violation): pairing paths + // via a two-way `if dominates(c, acc) then c else acc` silently + // dropped whichever path was ordered later when the two were + // incomparable (e.g. `Linear(n)` vs `Linear(m)` with distinct + // size variables). When neither dominates, preserve both via + // `sequential`, which normalizes through `drop_dominated`; + // `Big-O(f + g) = Big-O(max(f, g))` makes the sum asymptotically + // identical to the max. + paths + .iter() + .fold(SymbolicCost::ConstantCost { _0: 0 }, |acc, candidate| { + if dominates(candidate, &acc) { + candidate.clone() + } else if dominates(&acc, candidate) { + acc + } else { + sequential(acc, candidate.clone()) + } + }) +} + +pub fn normalize(cost: SymbolicCost) -> SymbolicCost { + match cost { + SymbolicCost::SumCost { _0: terms } => reduce_sum(drop_zero_terms(terms)), + SymbolicCost::ProductCost { _0: terms } => reduce_product(drop_zero_terms(terms)), + other => other, + } +} + +fn drop_zero_terms(terms: Vec) -> Vec { + terms + .into_iter() + .filter(|t| !matches!(t, SymbolicCost::ConstantCost { _0: 0 })) + .collect() +} + +fn reduce_sum(mut terms: Vec) -> SymbolicCost { + terms = drop_dominated_in_sum(terms); + match terms.len() { + 0 => SymbolicCost::ConstantCost { _0: 0 }, + 1 => terms.into_iter().next().unwrap(), + _ => SymbolicCost::SumCost { _0: terms }, + } +} + +fn reduce_product(terms: Vec) -> SymbolicCost { + match terms.len() { + 0 => SymbolicCost::ConstantCost { _0: 0 }, + 1 => terms.into_iter().next().unwrap(), + 2 => { + let mut iter = terms.into_iter(); + let a = iter.next().unwrap(); + let b = iter.next().unwrap(); + combine_binary_product(a, b) + } + _ => SymbolicCost::ProductCost { _0: terms }, + } +} + +fn combine_binary_product(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost { + if let (SymbolicCost::LinearCost { _0: va }, SymbolicCost::LinearCost { _0: vb }) = (&a, &b) { + if va == vb { + return SymbolicCost::PolynomialCost { + var: va.clone(), + degree: 2, + }; + } + } + SymbolicCost::ProductCost { _0: vec![a, b] } +} + +fn drop_dominated_in_sum(terms: Vec) -> Vec { + let mut keep: Vec = Vec::with_capacity(terms.len()); + for term in terms { + let term_dominated = keep.iter().any(|k| dominates(k, &term)); + if term_dominated { + continue; + } + keep.retain(|k| !dominates(&term, k)); + keep.push(term); + } + keep +} + +pub fn dominates(a: &SymbolicCost, b: &SymbolicCost) -> bool { + match a { + SymbolicCost::UnknownCost { .. } => true, + SymbolicCost::ConstantCost { .. } => matches!(b, SymbolicCost::ConstantCost { .. }), + SymbolicCost::LinearCost { _0: va } => match b { + SymbolicCost::ConstantCost { .. } | SymbolicCost::LogCost { .. } => true, + SymbolicCost::LinearCost { _0: vb } => va == vb, + SymbolicCost::PolynomialCost { var, degree } => va == var && *degree <= 1, + _ => false, + }, + SymbolicCost::PolynomialCost { + var: va, + degree: ka, + } => match b { + SymbolicCost::ConstantCost { .. } | SymbolicCost::LogCost { .. } => true, + SymbolicCost::LinearCost { _0: vb } => va == vb && *ka >= 1, + SymbolicCost::PolynomialCost { + var: vb, + degree: kb, + } => va == vb && *ka >= *kb, + _ => false, + }, + SymbolicCost::LogCost { _0: va } => match b { + SymbolicCost::ConstantCost { .. } => true, + SymbolicCost::LogCost { _0: vb } => va == vb, + _ => false, + }, + // Composite dominance via "dominant child summary" (DB-7 + // §Dominance). Both `Sum([A, B])` and `Product([A, B])` bound + // each child from below — sum and product of non-negative + // terms are ≥ any single term — so the composite dominates + // `b` iff *any* child does. Short-circuit evaluation keeps + // this O(n) worst-case over the (post-normalize) ≤ few-term + // lists. Fixes PR #537 review (codex): prior code hardcoded + // `LinearCost(_) => True` / `LogCost(_) => True` without + // inspecting terms, so e.g. `Product([Log(n)])` incorrectly + // dominated `Linear(n)`. + SymbolicCost::ProductCost { _0: terms } | SymbolicCost::SumCost { _0: terms } => { + terms.iter().any(|child| dominates(child, b)) + } + } +} + #[derive(Debug, Clone)] pub struct LoopNode { pub id: NodeId, diff --git a/src/v3/compiler/src/emit_rust.rs b/src/v3/compiler/src/emit_rust.rs index 3fcf3a245ba..286084747a8 100644 --- a/src/v3/compiler/src/emit_rust.rs +++ b/src/v3/compiler/src/emit_rust.rs @@ -5079,6 +5079,7 @@ mod tests { }; dag.set_port_type(parent_port, crate::types::TypeShape::new(dag_type)); + let mut test_node_ids = Vec::new(); for _ in 0..2 { let node_id = dag.alloc_node_id(); let output = dag.alloc_port(Some(node_id)); @@ -5093,13 +5094,17 @@ mod tests { span: SourceSpan::new("", 0, 0), })); dag.set_port_type(output, crate::types::TypeShape::new(dag_nodes_type)); + test_node_ids.push(node_id); } - let first_transform = dag - .nodes() - .iter() - .find_map(Behavior::as_transform) - .expect("first field project exists"); + // Query by the specific node we just pushed — earlier Transform + // nodes in `dag.nodes()` belong to bootstrap-loaded std modules + // and have no `parent` binding in `bound_names`, which renders + // as the empty-list fallback rather than the expected projection. + let first_transform = match dag.node(test_node_ids[0]) { + Behavior::Transform(t) => t, + other => panic!("pushed transform went missing, got {other:?}"), + }; let indexes = RealizationIndexes::build(&dag).expect("indexes build"); let input_use_facts = InputUseFacts::build(&dag, &indexes); let mut bound_names = HashMap::new(); diff --git a/src/v3/compiler/src/lens_cost_symbolic_generated.rs b/src/v3/compiler/src/lens_cost_symbolic_generated.rs new file mode 100644 index 00000000000..c8da711365f --- /dev/null +++ b/src/v3/compiler/src/lens_cost_symbolic_generated.rs @@ -0,0 +1,222 @@ +// AUTO-GENERATED from `src/v3/lenses/cost.dag` via +// `emit_rust_module`. Regenerate instead of hand-editing. + +#[derive(Clone, Debug)] +pub struct SymbolicCostEntry { + pub port: PortId, + pub cost: SymbolicCostLookup, +} +#[derive(Clone, Debug)] +pub enum SymbolicCostLookup { + MissingCost, + FoundCost { _0: SymbolicCost }, +} +pub fn symbolic_cost_of(p0: &Dag, p1: &PortId) -> SymbolicCostLookup { + lookup_cost(&(compute_symbolic_costs(p0)), p1) +} +pub fn compute_symbolic_costs(p0: &Dag) -> Vec { + ((p0).nodes()) + .iter() + .fold(seed_bind_params((p0).nodes()), |__fold_acc, __fold_item| { + let mut __list = (__fold_acc).clone(); + __list.insert(0, entry_for(p0, &__fold_acc, __fold_item)); + __list + }) +} +pub fn seed_bind_params(p0: &[Behavior]) -> Vec { + match p0 { + [] => Vec::new(), + [__list_head, __list_tail @ ..] => { + concat_entries(&(params_of(__list_head)), seed_bind_params(__list_tail)) + } + } +} +pub fn params_of(p0: &Behavior) -> Vec { + match p0 { + Behavior::Value(_) => Vec::new(), + Behavior::Transform(_) => Vec::new(), + Behavior::Branch(_) => Vec::new(), + Behavior::Loop(_) => Vec::new(), + Behavior::Bind(bind) => param_entries(&((bind).params)), + } +} +pub fn param_entries(p0: &[PortId]) -> Vec { + match p0 { + [] => Vec::new(), + [__list_head, __list_tail @ ..] => { + let mut __list = param_entries(__list_tail); + __list.insert( + 0, + SymbolicCostEntry { + port: (*(__list_head)), + cost: SymbolicCostLookup::FoundCost { + _0: SymbolicCost::ConstantCost { _0: 0 }, + }, + }, + ); + __list + } + } +} +pub fn concat_entries( + p0: &[SymbolicCostEntry], + p1: Vec, +) -> Vec { + match p0 { + [] => p1, + [__list_head, __list_tail @ ..] => { + let mut __list = concat_entries(__list_tail, (p1).clone()); + __list.insert(0, (__list_head).clone()); + __list + } + } +} +pub fn entry_for(p0: &Dag, p1: &[SymbolicCostEntry], p2: &Behavior) -> SymbolicCostEntry { + match p2 { + Behavior::Value(v) => SymbolicCostEntry { + port: (v).result_port(), + cost: SymbolicCostLookup::FoundCost { + _0: SymbolicCost::ConstantCost { _0: 0 }, + }, + }, + Behavior::Transform(t) => SymbolicCostEntry { + port: (t).result_port(), + cost: transform_cost(p1, &((t).inputs)), + }, + Behavior::Branch(b) => SymbolicCostEntry { + port: (b).result_port(), + cost: branch_cost(p1, &((b).input), &((b).paths)), + }, + Behavior::Loop(l) => SymbolicCostEntry { + port: (l).result_port(), + cost: loop_cost(p0, p1, l), + }, + Behavior::Bind(bind) => SymbolicCostEntry { + port: (bind).result_port(), + cost: lookup_cost(p1, &((bind).result_port())), + }, + } +} +pub fn loop_cost(p0: &Dag, p1: &[SymbolicCostEntry], p2: &LoopNode) -> SymbolicCostLookup { + combine_iterate( + &(linear_at((p2).source)), + &(body_cost(p0, p1, &((p2).body))), + ) +} +pub fn body_cost(p0: &Dag, p1: &[SymbolicCostEntry], p2: &NodeId) -> SymbolicCostLookup { + match &((p0).node_opt(p2).cloned()) { + None => SymbolicCostLookup::MissingCost, + Some(body_behavior) => lookup_cost(p1, &(behavior_result_port(body_behavior))), + } +} +pub fn behavior_result_port(p0: &Behavior) -> PortId { + match p0 { + Behavior::Value(v) => (v).result_port(), + Behavior::Transform(t) => (t).result_port(), + Behavior::Branch(br) => (br).result_port(), + Behavior::Loop(lp) => (lp).result_port(), + Behavior::Bind(bind) => (bind).result_port(), + } +} +pub fn linear_at(p0: PortId) -> SymbolicCostLookup { + SymbolicCostLookup::FoundCost { + _0: SymbolicCost::LinearCost { + _0: SizeVariable { source_port: p0 }, + }, + } +} +pub fn combine_iterate(p0: &SymbolicCostLookup, p1: &SymbolicCostLookup) -> SymbolicCostLookup { + match p0 { + SymbolicCostLookup::MissingCost => SymbolicCostLookup::MissingCost, + SymbolicCostLookup::FoundCost { _0: b } => match p1 { + SymbolicCostLookup::MissingCost => SymbolicCostLookup::MissingCost, + SymbolicCostLookup::FoundCost { _0: y } => SymbolicCostLookup::FoundCost { + _0: iterate((b).clone(), (y).clone()), + }, + }, + } +} +pub fn branch_cost(p0: &[SymbolicCostEntry], p1: &PortId, p2: &[Path]) -> SymbolicCostLookup { + combine_sequential( + &(SymbolicCostLookup::FoundCost { + _0: SymbolicCost::ConstantCost { _0: 1 }, + }), + &(combine_sequential(&(lookup_cost(p0, p1)), &(max_of_paths(p0, p2)))), + ) +} +pub fn max_of_paths(p0: &[SymbolicCostEntry], p1: &[Path]) -> SymbolicCostLookup { + (p1).iter().fold( + SymbolicCostLookup::FoundCost { + _0: SymbolicCost::ConstantCost { _0: 0 }, + }, + |__fold_acc, __fold_item| { + combine_max( + &__fold_acc, + &(lookup_cost(p0, &((__fold_item).result_port()))), + ) + }, + ) +} +pub fn combine_max(p0: &SymbolicCostLookup, p1: &SymbolicCostLookup) -> SymbolicCostLookup { + match p0 { + SymbolicCostLookup::MissingCost => SymbolicCostLookup::MissingCost, + SymbolicCostLookup::FoundCost { _0: ax } => match p1 { + SymbolicCostLookup::MissingCost => SymbolicCostLookup::MissingCost, + SymbolicCostLookup::FoundCost { _0: bx } => SymbolicCostLookup::FoundCost { + _0: dominant((ax).clone(), (bx).clone()), + }, + }, + } +} +pub fn dominant(p0: SymbolicCost, p1: SymbolicCost) -> SymbolicCost { + max_path( + &({ + let mut __list = { + let mut __list = Vec::new(); + __list.insert(0, (p1).clone()); + __list + }; + __list.insert(0, (p0).clone()); + __list + }), + ) +} +pub fn transform_cost(p0: &[SymbolicCostEntry], p1: &[PortId]) -> SymbolicCostLookup { + combine_sequential( + &(SymbolicCostLookup::FoundCost { + _0: SymbolicCost::ConstantCost { _0: 1 }, + }), + &(sum_costs(p0, p1)), + ) +} +pub fn sum_costs(p0: &[SymbolicCostEntry], p1: &[PortId]) -> SymbolicCostLookup { + (p1).iter().fold( + SymbolicCostLookup::FoundCost { + _0: SymbolicCost::ConstantCost { _0: 0 }, + }, + |__fold_acc, __fold_item| combine_sequential(&__fold_acc, &(lookup_cost(p0, __fold_item))), + ) +} +pub fn combine_sequential(p0: &SymbolicCostLookup, p1: &SymbolicCostLookup) -> SymbolicCostLookup { + match p0 { + SymbolicCostLookup::MissingCost => SymbolicCostLookup::MissingCost, + SymbolicCostLookup::FoundCost { _0: ax } => match p1 { + SymbolicCostLookup::MissingCost => SymbolicCostLookup::MissingCost, + SymbolicCostLookup::FoundCost { _0: bx } => SymbolicCostLookup::FoundCost { + _0: sequential((ax).clone(), (bx).clone()), + }, + }, + } +} +pub fn lookup_cost(p0: &[SymbolicCostEntry], p1: &PortId) -> SymbolicCostLookup { + match p0 { + [] => SymbolicCostLookup::MissingCost, + [__list_head, __list_tail @ ..] => { + if ((__list_head).port == (*(p1))) { + ((__list_head).cost).clone() + } else { + lookup_cost(__list_tail, p1) + } + } + } +} diff --git a/src/v3/compiler/src/lib.rs b/src/v3/compiler/src/lib.rs index 7a3caa5094a..b5a7645bc5b 100644 --- a/src/v3/compiler/src/lib.rs +++ b/src/v3/compiler/src/lib.rs @@ -57,6 +57,37 @@ pub mod lens_cost { pub use generated::{cost_of, CostLookup}; } +/// Symbolic-cost lens (Lane 2 Stage 2d / DB-7). Authority lives in +/// `src/v3/lenses/cost.dag`; the Rust projection is auto-emitted +/// into `src/v3/compiler/src/lens_cost_symbolic_generated.rs` and +/// re-exported so callers use `v3_compiler::lens_cost_symbolic::*`. +/// +/// The `SymbolicCost` + `SizeVariable` carriers live in +/// `src/v3/compiler/src/dag.rs` rather than the generated module +/// because they're declared in `src/v3/std/algebra.dag`, which +/// `emit_rust_module`'s `is_bootstrap_file` filter excludes from +/// type emission. The hand-maintained Rust mirror adjacent to +/// `Behavior` / `LoopBound` follows the same substrate-ownership +/// pattern the other bootstrap-resident types use. +pub mod lens_cost_symbolic { + #[allow( + dead_code, + unused_imports, + unused_parens, + unused_variables, + clippy::clone_on_copy, + clippy::collapsible_else_if + )] + mod generated { + use crate::dag::*; + use crate::diagnostics::*; + + include!("lens_cost_symbolic_generated.rs"); + } + + pub use generated::{symbolic_cost_of, SymbolicCostEntry, SymbolicCostLookup}; +} + /// Provenance lens. The authority lives in /// `src/v3/lenses/provenance.dag`; the Rust projection is auto-emitted /// into `src/v3/compiler/src/lens_provenance_generated.rs` and wrapped diff --git a/src/v3/compiler/tests/lane2_stage_2d_symbolic_cost_test.rs b/src/v3/compiler/tests/lane2_stage_2d_symbolic_cost_test.rs new file mode 100644 index 00000000000..0b0c07de8fe --- /dev/null +++ b/src/v3/compiler/tests/lane2_stage_2d_symbolic_cost_test.rs @@ -0,0 +1,493 @@ +// Lane 2 Stage 2d / DB-7 — symbolic-cost lens acceptance tests. +// +// Authority: `src/v3/lenses/cost.dag` (projection: +// `src/v3/compiler/src/lens_cost_symbolic_generated.rs`). +// +// These tests pin the per-Behavior lowering contract DB-7 specifies +// — every Behavior variant produces an honest asymptotic bound, and +// the composition algebra in `src/v3/std/algebra.dag` (+ its Rust +// mirror in `dag.rs`) normalizes correctly. + +use std::io::Write; +use std::path::PathBuf; +use std::process::{Command, Stdio}; + +use v3_compiler::compile_to_dag; +use v3_compiler::dag::{ + dominates, iterate, max_path, normalize, sequential, Behavior, Dag, PortId, SizeVariable, + SymbolicCost, +}; +use v3_compiler::emit_rust::emit_rust_module; +use v3_compiler::lens_cost_symbolic::{symbolic_cost_of, SymbolicCostLookup}; + +fn find_bind_value(dag: &Dag, name: &str) -> PortId { + dag.nodes() + .iter() + .filter_map(Behavior::as_bind) + .find(|b| b.name == name) + .unwrap_or_else(|| panic!("bind `{name}` not found")) + .value +} + +fn expect_cost(dag: &Dag, port: PortId) -> SymbolicCost { + match symbolic_cost_of(dag, &port) { + SymbolicCostLookup::FoundCost { _0: cost } => cost, + SymbolicCostLookup::MissingCost => { + panic!("symbolic_cost_of returned MissingCost for {port:?}") + } + } +} + +fn bind_cost(source: &str, file: &str, name: &str) -> SymbolicCost { + let dag = compile_to_dag(source, file).expect("fixture compiles"); + expect_cost(&dag, find_bind_value(&dag, name)) +} + +fn is_constant(cost: &SymbolicCost) -> bool { + matches!(cost, SymbolicCost::ConstantCost { .. }) +} + +fn mentions_linear(cost: &SymbolicCost) -> bool { + match cost { + SymbolicCost::LinearCost { .. } => true, + SymbolicCost::SumCost { _0: terms } | SymbolicCost::ProductCost { _0: terms } => { + terms.iter().any(mentions_linear) + } + _ => false, + } +} + +// Two real PortIds from the bootstrap Dag — just need distinct +// handles for the structural-equality checks the composition tests +// exercise. `Dag::new()` ports are stable across runs. +fn two_distinct_ports() -> (PortId, PortId) { + let dag = Dag::new(); + let ports: Vec = dag.ports().iter().map(|p| p.id()).collect(); + assert!( + ports.len() >= 2, + "bootstrap Dag should allocate at least two ports" + ); + (ports[0], ports[1]) +} + +fn size_var(source_port: PortId) -> SizeVariable { + SizeVariable { source_port } +} + +fn linear(port: PortId) -> SymbolicCost { + SymbolicCost::LinearCost { _0: size_var(port) } +} + +fn polynomial(port: PortId, degree: i64) -> SymbolicCost { + SymbolicCost::PolynomialCost { + var: size_var(port), + degree, + } +} + +fn log_cost(port: PortId) -> SymbolicCost { + SymbolicCost::LogCost { _0: size_var(port) } +} + +fn constant(n: i64) -> SymbolicCost { + SymbolicCost::ConstantCost { _0: n } +} + +// ── Per-Behavior lowering ──────────────────────────────────────── + +#[test] +fn value_reports_constant() { + // `let x = 1` → ConstantCost(0) (leaf literal, no work). + let dag = compile_to_dag("let x = 1", "test.v3").expect("compiles"); + let cost = expect_cost(&dag, find_bind_value(&dag, "x")); + assert!( + is_constant(&cost), + "literal value should report Constant, got {cost:?}" + ); +} + +#[test] +fn transform_single_op_reports_constant() { + // `let x = 1 + 2` → sequential(Constant(1), sum(Constant(0), Constant(0))) + // → Constant wrapper. Asymptotically O(1). + let cost = bind_cost("let x = 1 + 2", "test.v3", "x"); + assert!( + is_constant(&cost), + "single scalar op should report Constant, got {cost:?}" + ); +} + +#[test] +fn branch_reports_constant_when_both_arms_constant() { + // `if 1 > 0 then 10 else 20` — both arms are leaf literals, so + // max_path over two Constants stays Constant. + let cost = bind_cost("let r = if 1 > 0 then 10 else 20", "test.v3", "r"); + assert!( + is_constant(&cost), + "branch over constant arms should report Constant, got {cost:?}" + ); +} + +#[test] +fn recursive_fn_body_contributes_to_loop_cost() { + // PR #537 reviewer call-out (briansrls, BLOCKING): the prior + // `loop_cost(acc, l.source)` shape fed the loop its source + // port as the body cost — the SAME port as the bound — so + // body work contributed `ConstantCost(0)` (the pre-seeded + // param-port cost) and `normalize` dropped it from the + // iteration. A recursive fn `fn f(n) = if ... else f(n - 1)` + // then flattened to a bare `LinearCost` instead of a + // `ProductCost([LinearCost, body-cost])`. + // + // Post-fix: `l.body: NodeId` is resolved through + // `node(d, body_id)` → result_port, and THAT port's cost + // enters the iterate composition. The recursive fn's Branch + // body has a `ConstantCost(1)` (the comparison op), which is + // non-zero and does NOT drop in `drop_zero`. The resulting + // shape is `ProductCost([LinearCost, ConstantCost])` — the + // iterate composition is preserved structurally. + // + // Pin the structural signal: the cost must be a `ProductCost` + // that carries BOTH a LinearCost term (from `l.source`) and a + // non-zero leaf (from the body). A regression that drops the + // body fact collapses this back to bare LinearCost, which + // this assertion catches. + let dag = compile_to_dag( + "fn countdown(n: Int) -> Int =\n if n == 0 then 0 else countdown(n - 1)", + "loop_body_countdown.v3", + ) + .expect("compiles"); + let cost = expect_cost(&dag, find_bind_value(&dag, "countdown")); + match &cost { + SymbolicCost::ProductCost { _0: terms } => { + let has_linear = terms + .iter() + .any(|t| matches!(t, SymbolicCost::LinearCost { .. })); + let has_nonzero_body = terms + .iter() + .any(|t| matches!(t, SymbolicCost::ConstantCost { _0: n } if *n != 0)); + assert!( + has_linear, + "Loop cost must carry a LinearCost term from the bound port, got {cost:?}" + ); + assert!( + has_nonzero_body, + "Loop cost must carry a non-zero body-cost term (regression of briansrls BLOCKING \ + on PR #537 — body fact silently dropped), got {cost:?}" + ); + } + other => panic!( + "recursive fn should produce a ProductCost wrapping `iterate(Linear, body-cost)`; \ + a bare LinearCost means body is being dropped. Got {other:?}" + ), + } +} + +#[test] +fn recursive_fn_reports_linear_via_loop_lowering() { + // `fn countdown(n) = if n == 0 then 0 else countdown(n - 1)` + // lowers to a Loop whose source is the `n` param port. The + // lens's `loop_cost` fires LinearCost(size_var_of(source)), + // so the bound carries a LinearCost term. + let dag = compile_to_dag( + "fn countdown(n: Int) -> Int =\n if n == 0 then 0 else countdown(n - 1)", + "countdown.v3", + ) + .expect("compiles"); + let cost = expect_cost(&dag, find_bind_value(&dag, "countdown")); + assert!( + mentions_linear(&cost), + "recursive fn should surface a LinearCost term, got {cost:?}" + ); +} + +// ── Composition algebra (std.algebra Rust mirror) ──────────────── + +#[test] +fn sum_of_linear_and_constant_zero_normalizes_to_linear() { + // DB-7 acceptance gate: `SumCost([LinearCost, ConstantCost(0)])` + // normalizes to `LinearCost` (zero drops out). + let (port, _) = two_distinct_ports(); + let l = linear(port); + let result = sequential(l.clone(), constant(0)); + assert_eq!( + result, l, + "Linear + Constant(0) should normalize to Linear, got {result:?}" + ); +} + +#[test] +fn sum_of_constant_and_linear_normalizes_to_linear() { + // Dominance is order-independent: Constant + Linear also + // normalizes to Linear (Constant is dominated). + let (port, _) = two_distinct_ports(); + let l = linear(port); + let result = sequential(constant(5), l); + assert!( + matches!(result, SymbolicCost::LinearCost { .. }), + "Constant + Linear should normalize to Linear, got {result:?}" + ); +} + +#[test] +fn product_of_two_linears_over_same_var_folds_to_polynomial_squared() { + // DB-7 §"Nested fold detection (O(n²) diagnostic)": + // `iterate(Linear(n), Linear(n))` folds to `Polynomial(n, 2)`. + let (port, _) = two_distinct_ports(); + let l = linear(port); + let result = iterate(l.clone(), l); + match result { + SymbolicCost::PolynomialCost { var, degree } => { + assert_eq!(var, size_var(port)); + assert_eq!(degree, 2); + } + other => panic!("expected PolynomialCost(n, 2), got {other:?}"), + } +} + +#[test] +fn product_of_linears_over_different_vars_stays_product() { + // Two folds over DISTINCT lists stay as ProductCost — the + // two size variables aren't the same, so the polynomial + // collapse doesn't fire. + let (port_a, port_b) = two_distinct_ports(); + let result = iterate(linear(port_a), linear(port_b)); + assert!( + matches!(result, SymbolicCost::ProductCost { .. }), + "Linear(a) * Linear(b) over different ports should stay Product, got {result:?}" + ); +} + +#[test] +fn dominance_unknown_dominates_everything() { + // DB-7 §"Dominance" — Unknown is the safest over-approximation. + let (port, _) = two_distinct_ports(); + let unknown = SymbolicCost::UnknownCost { + _0: "reflection".to_string(), + }; + assert!(dominates(&unknown, &linear(port))); + assert!(dominates(&unknown, &constant(0))); +} + +#[test] +fn dominance_linear_dominates_log_and_constant() { + let (port, _) = two_distinct_ports(); + assert!(dominates(&linear(port), &log_cost(port))); + assert!(dominates(&linear(port), &constant(3))); + assert!(!dominates(&constant(3), &linear(port))); +} + +#[test] +fn dominance_polynomial_degree_ordering() { + let (port, _) = two_distinct_ports(); + assert!(dominates(&polynomial(port, 3), &polynomial(port, 2))); + assert!(!dominates(&polynomial(port, 2), &polynomial(port, 3))); +} + +#[test] +fn composite_dominance_reads_children_not_outer_variant() { + // PR #537 review (codex P2): Product / Sum dominance must + // derive from children, not hardcode "any Product dominates + // Linear". A product whose strongest child is `Log(n)` + // should NOT dominate `Linear(n)`. + let (port, _) = two_distinct_ports(); + let product_of_logs = SymbolicCost::ProductCost { + _0: vec![log_cost(port), log_cost(port)], + }; + let linear_cost = linear(port); + assert!( + !dominates(&product_of_logs, &linear_cost), + "Product([Log, Log]) must NOT dominate Linear — children don't reach Linear, \ + got dominates=true (regression of codex P2 on PR #537)" + ); + + // Symmetric positive case: a product WITH a Linear child DOES + // dominate Log, because the dominant-child summary walks the + // children. + let product_with_linear = SymbolicCost::ProductCost { + _0: vec![log_cost(port), linear(port)], + }; + assert!( + dominates(&product_with_linear, &log_cost(port)), + "Product([Log, Linear]) must dominate Log via its Linear child" + ); +} + +#[test] +fn sum_dominance_reads_children_not_outer_variant() { + // Same fix as ProductCost: Sum's dominance is a dominant-child + // summary, not a hardcoded "any Sum dominates scalars". + let (port, _) = two_distinct_ports(); + let sum_of_logs = SymbolicCost::SumCost { + _0: vec![log_cost(port), log_cost(port)], + }; + assert!( + !dominates(&sum_of_logs, &linear(port)), + "Sum([Log, Log]) must NOT dominate Linear — no child reaches Linear" + ); + + let sum_with_polynomial = SymbolicCost::SumCost { + _0: vec![constant(0), polynomial(port, 2)], + }; + assert!( + dominates(&sum_with_polynomial, &linear(port)), + "Sum containing Polynomial(n, 2) must dominate Linear(n) via the poly child" + ); +} + +#[test] +fn max_path_returns_dominant_term() { + // `max_path([Constant(0), Linear(n), Polynomial(n, 2)])` → Polynomial(n, 2). + let (port, _) = two_distinct_ports(); + let paths = vec![constant(0), linear(port), polynomial(port, 2)]; + let result = max_path(&paths); + match result { + SymbolicCost::PolynomialCost { degree, .. } => assert_eq!(degree, 2), + other => panic!("expected PolynomialCost, got {other:?}"), + } +} + +#[test] +fn max_path_preserves_both_incomparable_branches() { + // PR #537 review (briansrls, BLOCKING): two incomparable + // branches — `Linear(n)` over port_a vs `Linear(m)` over + // port_b — must NOT drop one silently. `Big-O(f + g) = + // Big-O(max(f, g))` for non-negative asymptotic terms, so the + // preserved-as-sum shape is the honest worst case. + let (port_a, port_b) = two_distinct_ports(); + let paths = vec![linear(port_a), linear(port_b)]; + let result = max_path(&paths); + match &result { + SymbolicCost::SumCost { _0: terms } => { + assert_eq!( + terms.len(), + 2, + "incomparable Linear(n) + Linear(m) must preserve both as a two-element Sum, \ + got {result:?}" + ); + assert!( + terms.contains(&linear(port_a)) && terms.contains(&linear(port_b)), + "both branch costs must remain in the Sum, got {result:?}" + ); + } + other => panic!("expected SumCost preserving both branches, got {other:?}"), + } +} + +#[test] +fn max_path_order_independence_on_incomparable_branches() { + // Reversing the input order must yield the same asymptotic + // shape — the previous two-way dominance fold depended on + // fold order and dropped whichever branch landed later when + // both were incomparable. + let (port_a, port_b) = two_distinct_ports(); + let forward = max_path(&[linear(port_a), linear(port_b)]); + let reversed = max_path(&[linear(port_b), linear(port_a)]); + let (forward_terms, reversed_terms) = match (&forward, &reversed) { + (SymbolicCost::SumCost { _0: fwd }, SymbolicCost::SumCost { _0: rev }) => { + (fwd.clone(), rev.clone()) + } + _ => panic!( + "both orderings should produce a SumCost, got forward={forward:?} reversed={reversed:?}" + ), + }; + assert_eq!( + forward_terms.len(), + reversed_terms.len(), + "element count must not depend on fold order" + ); + assert!( + forward_terms.iter().all(|t| reversed_terms.contains(t)) + && reversed_terms.iter().all(|t| forward_terms.contains(t)), + "the preserved set of terms must be the same regardless of input order; \ + got forward={forward_terms:?} reversed={reversed_terms:?}" + ); +} + +#[test] +fn normalize_keeps_singleton_costs_unchanged() { + // `normalize` is structural — non-Sum/Product variants pass + // through unmodified. + let (port, _) = two_distinct_ports(); + for cost in [ + constant(7), + linear(port), + log_cost(port), + SymbolicCost::UnknownCost { + _0: "opaque".to_string(), + }, + ] { + let normalized = normalize(cost.clone()); + assert_eq!(normalized, cost, "normalize should pass through leaf costs"); + } +} + +// ── Generated-module staleness guard ───────────────────────────── + +const GENERATED_LENS_HEADER: &str = "// AUTO-GENERATED from `src/v3/lenses/cost.dag` via\n\ + // `emit_rust_module`. Regenerate instead of hand-editing.\n\n"; + +fn lens_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("lenses") + .join("cost.dag") +} + +fn emit_lens_module() -> String { + let source = std::fs::read_to_string(lens_path()).expect("read cost.dag"); + let dag = compile_to_dag(&source, lens_path().to_string_lossy().as_ref()) + .expect("cost.dag should compile cleanly"); + assert!( + dag.diagnostics().is_empty(), + "cost.dag should compile without diagnostics, got {:?}", + dag.diagnostics() + ); + let raw = emit_rust_module(&dag).expect("emit compiled lens module"); + format_rust_source(&format!("{GENERATED_LENS_HEADER}{raw}")) +} + +fn format_rust_source(source: &str) -> String { + let mut child = Command::new("rustfmt") + .arg("--emit") + .arg("stdout") + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .spawn() + .expect("spawn rustfmt"); + child + .stdin + .as_mut() + .expect("rustfmt stdin") + .write_all(source.as_bytes()) + .expect("write source to rustfmt"); + let output = child.wait_with_output().expect("wait for rustfmt"); + assert!( + output.status.success(), + "rustfmt failed on emitted lens module" + ); + String::from_utf8(output.stdout).expect("rustfmt output should be utf-8") +} + +#[test] +fn cost_dag_compiles_cleanly() { + let source = std::fs::read_to_string(lens_path()).expect("read cost.dag"); + let dag = compile_to_dag(&source, lens_path().to_string_lossy().as_ref()) + .expect("cost.dag should compile cleanly"); + assert!( + dag.diagnostics().is_empty(), + "cost.dag should compile without diagnostics, got {:?}", + dag.diagnostics() + ); +} + +#[test] +fn cost_generated_module_matches_checked_in_snapshot() { + let fresh = emit_lens_module(); + let checked_in = include_str!("../src/lens_cost_symbolic_generated.rs"); + assert_eq!( + fresh.trim(), + checked_in.trim(), + "checked-in `lens_cost_symbolic_generated.rs` is stale; run `cargo run --bin regen_lens_cost_symbolic`" + ); +} diff --git a/src/v3/compiler/tests/m0_acceptance.rs b/src/v3/compiler/tests/m0_acceptance.rs index 10780606d78..fec96e7a6eb 100644 --- a/src/v3/compiler/tests/m0_acceptance.rs +++ b/src/v3/compiler/tests/m0_acceptance.rs @@ -72,9 +72,18 @@ fn compile_any(src: &str, file: &str) -> Dag { fn test_let_binding_produces_dag_shape() { let dag = compile_to_dag("let x = 1 + 2", "test.v3").expect("compiles"); + // Count only user-code nodes. The bootstrap Dag carries std + // module bodies (effects, list, algebra, ...) whose nodes live + // in `dag.nodes()` alongside user output; filtering by source + // span isolates the four structural nodes this fixture actually + // asserts. + let user_node_count = dag + .nodes() + .iter() + .filter(|behavior| behavior.span().file == "test.v3") + .count(); assert_eq!( - dag.nodes().len(), - 4, + user_node_count, 4, "Value(1) + Value(2) + Transform(Add) + Bind(x)" ); diff --git a/src/v3/compiler/tests/m1_3_emit_rust_test.rs b/src/v3/compiler/tests/m1_3_emit_rust_test.rs index bb3950a9b1b..a3e3e3b3607 100644 --- a/src/v3/compiler/tests/m1_3_emit_rust_test.rs +++ b/src/v3/compiler/tests/m1_3_emit_rust_test.rs @@ -189,7 +189,11 @@ const REFLECTED_FIXTURES: &[ReflectedFixture] = &[ ReflectedFixture { name: "bind_count", module_source: "fn bind_count(d: Dag) -> Int = fold(d.nodes, 0, |n, behavior| match behavior { Value(v) => n, Transform(t) => n, Branch(b) => n, Loop(l) => n, Bind(bind) => n + 1 })", - wrapper_body: "let dag = v3_compiler::compile_to_dag(\"let x: Int = 1\\nlet y: Int = x + 2\", \"runtime_reflection.v3\").expect(\"compiles\"); bind_count(&dag)", + // Subtract the bootstrap baseline so the test still pins the + // user-program bind count after Lane 2 Stage 2d added + // `src/v3/std/algebra.dag` + `dimensions.dag`, whose lowered + // bodies contribute their own Bind nodes to `d.nodes`. + wrapper_body: "let dag = v3_compiler::compile_to_dag(\"let x: Int = 1\\nlet y: Int = x + 2\", \"runtime_reflection.v3\").expect(\"compiles\"); let baseline = v3_compiler::dag::Dag::new(); bind_count(&dag) - bind_count(&baseline)", }, ReflectedFixture { name: "singleton_span", @@ -199,7 +203,11 @@ const REFLECTED_FIXTURES: &[ReflectedFixture] = &[ ReflectedFixture { name: "result_port_is_param", module_source: "fn result_port_is_param(bind: BindNode) -> Bool = contains(bind.params, bind.result_port)", - wrapper_body: "let dag = v3_compiler::compile_to_dag(\"fn id(x: Int) -> Int = x\", \"runtime_reflection.v3\").expect(\"compiles\"); let bind = dag.nodes().iter().find_map(|node| match node { v3_compiler::dag::Behavior::Bind(bind) if !bind.params.is_empty() => Some(bind.clone()), _ => None }).expect(\"function bind\"); if result_port_is_param(&bind) { 1 } else { 0 }", + // Filter by source file so the bind picked is the user's `id` + // — after Lane 2 Stage 2d landed std-module binds with + // non-empty params, the raw `params.is_empty()` filter was + // no longer specific enough to isolate user code. + wrapper_body: "let dag = v3_compiler::compile_to_dag(\"fn id(x: Int) -> Int = x\", \"runtime_reflection.v3\").expect(\"compiles\"); let bind = dag.nodes().iter().find_map(|node| match node { v3_compiler::dag::Behavior::Bind(bind) if !bind.params.is_empty() && bind.span.file == \"runtime_reflection.v3\" => Some(bind.clone()), _ => None }).expect(\"function bind\"); if result_port_is_param(&bind) { 1 } else { 0 }", }, ReflectedFixture { name: "bind_names", @@ -213,7 +221,11 @@ const REFLECTED_FIXTURES: &[ReflectedFixture] = &[ Loop(l) => acc, \ Bind(bind) => cons({ name: bind.name }, acc) \ })", - wrapper_body: "let dag = v3_compiler::compile_to_dag(\"let x: Int = 1\\nlet y: Int = x + 2\", \"runtime_reflection.v3\").expect(\"compiles\"); bind_names(&dag).len() as i64", + // Same bootstrap-baseline subtraction as `bind_count` — the + // test pins the two user-program binds (`x`, `y`) even + // though `bind_names` also materializes a record per std- + // module bind in `d.nodes`. + wrapper_body: "let dag = v3_compiler::compile_to_dag(\"let x: Int = 1\\nlet y: Int = x + 2\", \"runtime_reflection.v3\").expect(\"compiles\"); let baseline = v3_compiler::dag::Dag::new(); (bind_names(&dag).len() as i64) - (bind_names(&baseline).len() as i64)", }, ]; diff --git a/src/v3/compiler/tests/m1_substrate_test.rs b/src/v3/compiler/tests/m1_substrate_test.rs index 3e681bf7fd2..0ac6f0f109b 100644 --- a/src/v3/compiler/tests/m1_substrate_test.rs +++ b/src/v3/compiler/tests/m1_substrate_test.rs @@ -522,10 +522,15 @@ fn m17_operator_lowers_to_structural_transform_target() { // anonymous stub declaration is allocated for the operator // symbol; the dispatch fact lives on the Transform's variant. let dag = compile_to_dag("let x = 1 + 2", "test.v3").expect("compiles"); + // Scope to user-source transforms — std modules loaded by + // bootstrap (e.g. `src/v3/std/algebra.dag`) also push Transform + // nodes, so the first entry in `dag.nodes()` is no longer + // guaranteed to be the user's. let add_node = dag .nodes() .iter() - .find_map(Behavior::as_transform) + .filter_map(Behavior::as_transform) + .find(|t| t.span.file == "test.v3") .expect("Transform node exists"); match &add_node.target { TransformTarget::Operator(OperatorKind::Arithmetic(ArithmeticOp::Add)) => {} @@ -543,7 +548,8 @@ fn m17_comparison_operator_lowers_to_structural_transform_target() { let cmp_node = dag .nodes() .iter() - .find_map(Behavior::as_transform) + .filter_map(Behavior::as_transform) + .find(|t| t.span.file == "test.v3") .expect("Transform node exists"); match &cmp_node.target { TransformTarget::Operator(OperatorKind::Comparison(ComparisonOp::Lt)) => {} @@ -566,7 +572,7 @@ fn m17_user_function_call_lowers_to_callable_target() { .nodes() .iter() .filter_map(Behavior::as_transform) - .find(|t| matches!(&t.target, TransformTarget::Callable(_))) + .find(|t| t.span.file == "test.v3" && matches!(&t.target, TransformTarget::Callable(_))) .expect("Callable Transform exists"); let target_id = match &f_call.target { TransformTarget::Callable(id) => *id, @@ -1308,10 +1314,14 @@ fn classify(h: Hue) -> Int = match h { Red => 0, Green => 1, Blue => 2 } // The Branch exists and its pattern resolution ran through // the alias walk — each path should carry a ResolvedVariant. + // Scope to the user-source branch: bootstrap modules (notably + // `src/v3/std/algebra.dag`) now push Branch nodes for their own + // if/else lowering, so first-match is no longer reliable. let branch = dag .nodes() .iter() - .find_map(Behavior::as_branch) + .filter_map(Behavior::as_branch) + .find(|b| b.span.file == "aliased_sum.v3") .expect("Branch exists"); assert_eq!(branch.paths.len(), 3); for path in &branch.paths { @@ -1409,12 +1419,17 @@ let c = a(1) 0, "failed mutual recursion must not materialize a cluster witness" ); + // Scope the Loop check to this fixture — bootstrap std modules + // (e.g. `src/v3/std/algebra.dag`) correctly materialize Loop + // nodes for their own structural recursion, so a global + // `filter_map(as_loop).next().is_none()` no longer reflects the + // test's intent ("user's non-terminating SCC didn't fabricate a + // Loop"). assert!( dag.nodes() .iter() .filter_map(Behavior::as_loop) - .next() - .is_none(), + .all(|l| l.span.file != "mutual_recursion_cascade.v3"), "failed mutual recursion must not fabricate Loop materialization" ); } @@ -2809,12 +2824,14 @@ fn odd(n: Int, even: fn(Int) -> Bool) -> Bool = even(n) 0, "shadowed callable parameters are not top-level mutual recursion" ); + // Scope the Loop check to this fixture's source — bootstrap + // std modules legitimately contribute Loop nodes for their own + // structural recursion (e.g. `src/v3/std/algebra.dag::drop_zero`). assert!( dag.nodes() .iter() .filter_map(Behavior::as_loop) - .next() - .is_none(), + .all(|l| l.span.file != "mutual_shadowing_false_positive.v3"), "shadowed callable parameters must not introduce synthetic recursion loops" ); } diff --git a/src/v3/lenses/cost.dag b/src/v3/lenses/cost.dag new file mode 100644 index 00000000000..6001084bdf7 --- /dev/null +++ b/src/v3/lenses/cost.dag @@ -0,0 +1,250 @@ +module lenses.cost + +import std.list { List, empty, fold, cons } +import std.substrate { Dag, Behavior, BranchPath, LoopNode, NodeId, PortId, node } +import std.algebra { SymbolicCost, SizeVariable, sequential, iterate, max_path } + +type SymbolicCostEntry { + port: PortId + cost: SymbolicCostLookup +} + +type SymbolicCostLookup + = MissingCost + | FoundCost(SymbolicCost) + +fn symbolic_cost_of(d: Dag, port_id: PortId) -> SymbolicCostLookup = + lookup_cost(compute_symbolic_costs(d), port_id) + +fn compute_symbolic_costs(d: Dag) -> List = + fold(d.nodes, seed_bind_params(d.nodes), |acc, behavior| + cons(entry_for(d, acc, behavior), acc) + ) + +fn seed_bind_params(nodes: List) -> List = + match nodes { + Empty => empty() + Cons(payload) => + concat_entries(params_of(payload.head), seed_bind_params(payload.tail)) + } + +fn params_of(behavior: Behavior) -> List = + match behavior { + Value(v) => empty() + Transform(t) => empty() + Branch(b) => empty() + Loop(l) => empty() + Bind(bind) => param_entries(bind.params) + } + +fn param_entries(params: List) -> List = + match params { + Empty => empty() + Cons(payload) => + cons( + { port: payload.head, cost: FoundCost(ConstantCost(0)) }, + param_entries(payload.tail) + ) + } + +fn concat_entries( + a: List, + b: List +) -> List = + match a { + Empty => b + Cons(payload) => cons(payload.head, concat_entries(payload.tail, b)) + } + +fn entry_for( + d: Dag, + acc: List, + behavior: Behavior +) -> SymbolicCostEntry = + match behavior { + Value(v) => + { port: v.result_port, cost: FoundCost(ConstantCost(0)) } + Transform(t) => + { port: t.result_port, cost: transform_cost(acc, t.inputs) } + Branch(b) => + { port: b.result_port, cost: branch_cost(acc, b.input, b.paths) } + Loop(l) => + { port: l.result_port, cost: loop_cost(d, acc, l) } + Bind(bind) => + { port: bind.result_port, cost: lookup_cost(acc, bind.result_port) } + } + +// `loop_cost` composes iteration: bound × body. +// +// - Bound: `LinearCost(size_var_of(l.source))` — the runtime value +// the Loop descends upon (same carrier for `Cardinality { count }` +// and `Descent { cluster }` via `LoopNode.source`). +// - Body: the already-lowered cost of `l.body`'s result port. The +// forward-fold contract guarantees the body's `entry_for` ran +// earlier in the walk (producers precede consumers in +// `d.nodes`), so its cost is already in `acc`. +// +// PR #537 reviewer call-out (briansrls, BLOCKING): the earlier +// shape `loop_cost(acc, l.source)` passed only the source port +// and then looked that same port up as "body cost" — so +// recursive-body work silently contributed zero, violating Facts +// Flow Forward. Now `l.body: NodeId` is resolved through the +// `node(d, NodeId) -> Behavior?` substrate accessor to recover +// the body's result port, and THAT port's cost is the honest +// body cost. +fn loop_cost( + d: Dag, + acc: List, + l: LoopNode +) -> SymbolicCostLookup = + combine_iterate( + linear_at(l.source), + body_cost(d, acc, l.body) + ) + +fn body_cost( + d: Dag, + acc: List, + body_id: NodeId +) -> SymbolicCostLookup = + match node(d, body_id) { + None => MissingCost + Some(body_behavior) => lookup_cost(acc, behavior_result_port(body_behavior)) + } + +fn behavior_result_port(b: Behavior) -> PortId = + match b { + Value(v) => v.result_port + Transform(t) => t.result_port + Branch(br) => br.result_port + Loop(lp) => lp.result_port + Bind(bind) => bind.result_port + } + +fn linear_at(port_id: PortId) -> SymbolicCostLookup = + FoundCost(LinearCost({ source_port: port_id })) + +fn combine_iterate( + bound: SymbolicCostLookup, + body: SymbolicCostLookup +) -> SymbolicCostLookup = + match bound { + MissingCost => MissingCost + FoundCost(b) => + match body { + MissingCost => MissingCost + FoundCost(y) => FoundCost(iterate(b, y)) + } + } + +fn branch_cost( + acc: List, + input: PortId, + paths: List +) -> SymbolicCostLookup = + combine_sequential( + FoundCost(ConstantCost(1)), + combine_sequential( + lookup_cost(acc, input), + max_of_paths(acc, paths) + ) + ) + +fn max_of_paths( + acc: List, + paths: List +) -> SymbolicCostLookup = + fold(paths, FoundCost(ConstantCost(0)), |running, path| + combine_max(running, lookup_cost(acc, path.result_port)) + ) + +fn combine_max( + a: SymbolicCostLookup, + b: SymbolicCostLookup +) -> SymbolicCostLookup = + match a { + MissingCost => MissingCost + FoundCost(ax) => + match b { + MissingCost => MissingCost + FoundCost(bx) => FoundCost(dominant(ax, bx)) + } + } + +fn dominant(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + max_path(cons(a, cons(b, empty()))) + +fn transform_cost( + acc: List, + inputs: List +) -> SymbolicCostLookup = + combine_sequential( + FoundCost(ConstantCost(1)), + sum_costs(acc, inputs) + ) + +fn sum_costs( + acc: List, + ports: List +) -> SymbolicCostLookup = + fold(ports, FoundCost(ConstantCost(0)), |running, port_id| + combine_sequential(running, lookup_cost(acc, port_id)) + ) + +fn combine_sequential( + a: SymbolicCostLookup, + b: SymbolicCostLookup +) -> SymbolicCostLookup = + match a { + MissingCost => MissingCost + FoundCost(ax) => + match b { + MissingCost => MissingCost + FoundCost(bx) => FoundCost(sequential(ax, bx)) + } + } + +fn lookup_cost(acc: List, port_id: PortId) -> SymbolicCostLookup = + match acc { + Empty => MissingCost + Cons(payload) => + if payload.head.port == port_id then + payload.head.cost + else + lookup_cost(payload.tail, port_id) + } + +// ── Dimension wiring — DEFERRED to Stage 2f ─────── +// +// DB-7 §"Dimension wiring" specifies a +// `data symbolic_cost_dimension: Dimension = {..}` +// declaration with `witness_of`, `compose`, `identity` fields +// carrying function references. +// +// Stage 2d does NOT ship this data declaration because v3's +// current parser/lowerer rejects two v3 surface-grammar gaps that +// the declaration's shape requires simultaneously: +// +// 1. Record literals inside `data X: T = { ... }` bodies. At +// M1(2.8) the lowerer reports "data has an opaque body — +// user code cannot yet use record / list / map literals +// inside data bodies" (DOWNSTREAM_REQUIREMENTS.md class-5 +// gap #3). +// 2. Record literals / match / lambdas inside `fn X { body }` +// block-bodied definitions. Constructing `Witness::Violates +// { reason, at }` — the MissingCost-to-violation shim the +// Dimension contract requires — hits the same block-body +// restriction. +// +// The lens ships its Behavior-variant lowering (`entry_for` + +// helpers) as the authority. When Stage 2f's generic `analyze` +// walker lands, it will materialize the `Dimension` +// instance alongside the surface-grammar extensions that unlock +// the receipt form. Dispatching the instance from here today +// would either require a parallel Rust-side declaration (bypassing +// `.dag`-as-authority) or wait on the grammar extension — the +// second path is the one the ROADMAP already sequences (Stage 2f +// extracts the abstraction once multiple instances exist). +// +// See `docs/design-symbolic-cost-algebra.md` §"Dimension +// wiring" for the target shape. diff --git a/src/v3/std/algebra.dag b/src/v3/std/algebra.dag new file mode 100644 index 00000000000..89c96749b64 --- /dev/null +++ b/src/v3/std/algebra.dag @@ -0,0 +1,430 @@ +// std.algebra — structural algebra shared across lenses. +// +// 🟡 SCAFFOLD at Stage 2d scope. This file ships the carrier types + +// composition algebra for `SymbolicCost`, the asymptotic-bound +// coproduct consumed by `lenses/cost.dag` (DB-7). The broader +// algebra hierarchy (Monoid, Lattice, Ring, ...) authored at +// `dsl/std/algebra.dag` for v2 is NOT ported yet — Stage 2d needs +// `SymbolicCost` alone; later lanes pull algebra structures in as +// concrete consumers demand them, same policy as +// `src/v3/std/effects.dag` Stage 2a. +// +// **SymbolicCost coproduct (seven variants per DB-7 +// `docs/design-symbolic-cost-algebra.md`):** +// - `ConstantCost(Int)` — O(1) bounds +// - `LinearCost(SizeVariable)` — O(n) over a named size +// - `PolynomialCost { var, degree }` — O(n^k) +// - `ProductCost(List)` — O(n·m) product +// - `SumCost(List)` — O(n + m) sum, dominated terms drop +// - `LogCost(SizeVariable)` — O(log n) +// - `UnknownCost(String)` — top of the dominance lattice +// +// **`UnknownCost` role — algebra element, not failure channel.** +// Reviewer call-out on PR #537: the earlier "fail-open" framing +// straddled two stories. Locked here: `UnknownCost` is a +// legitimate member of the cost algebra representing the most +// conservative asymptotic upper bound. `dominates(Unknown, X) = +// True` for every `X`; nothing but itself dominates Unknown. +// The `String` payload carries a user-facing reason (exotic +// bound the thesis doesn't yet model — O(n!), O(2^n) — or "the +// analyzer could not prove a tighter bound"). Treating Unknown +// as top keeps the composition algebra total and keeps +// downstream consumers from having to special-case "bound not +// known yet." +// +// Failure — "this behavior cannot inhabit the cost dimension at +// all" (malformed DAG reference, missing producer) — lives +// OUTSIDE `SymbolicCost`: +// - `SymbolicCostLookup::MissingCost` is the lens-boundary +// failure carrier (see `src/v3/lenses/cost.dag`); every +// composition wrapper propagates it. +// - `Witness::Violates` from +// `src/v3/std/dimensions.dag` is the Dimension-boundary +// failure carrier. Stage 2f's generic `analyze` will route +// MissingCost-at-the-lens into Violates-at-the-dimension. +// Keeping the two failure channels outside the algebra carrier +// lets `SymbolicCost` stay a trustworthy algebra element without +// a "maybe" mode consumers have to unwrap. +// +// Four-pattern dissolution receipt (Q4 per DB-7): +// +// - Pattern 1 (fact placement): fails. Every consumer dispatches +// on cost variant first — dominance on Polynomial/Linear pairs, +// list flattening on Sum/Product, name extraction on +// Linear/Log/Polynomial. No neutral placement above the variant +// tag. +// - Pattern 2 (variant-is-data): fails. ConstantCost carries a +// literal Int; LinearCost/LogCost carry a SizeVariable; +// PolynomialCost carries `{var, degree}`; Product/Sum carry +// lists of costs; UnknownCost carries a reason String. Each +// payload is structurally distinct. +// - Pattern 3 (algebraic-form): confirms terminality. The seven +// variants are the asymptotic bounds the thesis reasons about; +// exotic bounds (O(n!), O(2^n)) collapse to `UnknownCost` with +// a reason until a concrete consumer forces variant growth. +// - Pattern 4 (dimensional): fails. No common coordinate space +// generates all seven — LinearCost's payload is a SizeVariable, +// ProductCost's is a list, ConstantCost's is an Int. +// +// STOP SIGNAL: wanting an eighth variant. Pause and escalate rather +// than extending; the thesis claim is that seven covers the +// asymptotic surface, and any new variant should carry its own +// dissolution receipt. + +module v3.std.algebra + +import std.list { List, empty, fold, cons } +import std.substrate { PortId } + +// 🟢 TERMINAL. `SizeVariable` names the runtime size of a DAG +// port's value. Two cost expressions correlate structurally via +// `source_port` equality — different folds over the same port +// describe the SAME size; two folds over different ports do NOT, +// even if both lists have the same declared type. +// +// No `name: String` field: MVP rendering pins on port equality +// alone, and the user-facing label the DB-7 design doc sketches +// needs an InternTable lookup the lens doesn't yet run. When a +// render consumer pins the missing piece, `SizeVariable` grows a +// `name` field alongside the Rust mirror in `src/v3/compiler/src/dag.rs`. +type SizeVariable { + source_port: PortId +} + +// 🟢 TERMINAL at Stage 2d scope. The asymptotic-bound coproduct +// DB-7 locks. See the module-level receipt for dissolution-pattern +// evidence. +type SymbolicCost + = ConstantCost(Int) + | LinearCost(SizeVariable) + | PolynomialCost { var: SizeVariable, degree: Int } + | ProductCost(List) + | SumCost(List) + | LogCost(SizeVariable) + | UnknownCost(String) + +// ── Composition (sequential / iterate / max_path) ─────────────── + +// `sequential(a, b)` composes two costs in series. The resulting +// sum normalizes dominated terms away — `O(n) + O(1) = O(n)`. +fn sequential(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + normalize(SumCost(cons(a, cons(b, empty())))) + +// `iterate(bound, body)` composes an iteration: `body` runs +// `bound`-many times. `O(n) * O(1) = O(n)`; `O(n) * O(n) = O(n²)` +// when the two LinearCost terms share a SizeVariable. +fn iterate(bound: SymbolicCost, body: SymbolicCost) -> SymbolicCost = + normalize(ProductCost(cons(bound, cons(body, empty())))) + +// Lambda-free helper so `max_path`'s fold below resolves its +// function-type parameter without relying on bidirectional +// inference through a closure. +// +// Three-way semantics (fixes PR #537 review: Facts Flow Forward +// violation — pairing paths via `if dominates(c, acc) then c else +// acc` silently dropped whichever path was ordered later when the +// two were incomparable, e.g. `Linear(n)` vs `Linear(m)` with +// distinct size variables): +// +// - candidate dominates acc → return candidate (acc drops, Big-O +// dominance is stable). +// - acc dominates candidate → return acc (candidate drops). +// - neither dominates → preserve both via `sequential`, relying +// on `Big-O(f + g) = Big-O(max(f, g))` for non-negative +// asymptotic terms; `normalize` inside `sequential` still drops +// anything the other term dominates. +fn max_path_step(acc: SymbolicCost, candidate: SymbolicCost) -> SymbolicCost = + if dominates(candidate, acc) then + candidate + else + keep_or_sum(acc, candidate) + +fn keep_or_sum(acc: SymbolicCost, candidate: SymbolicCost) -> SymbolicCost = + if dominates(acc, candidate) then + acc + else + sequential(acc, candidate) + +// `max_path(paths)` takes the dominant cost across alternative +// control-flow paths (Branch arms). Worst-case asymptotic +// semantics: a branch between `O(n)` and `O(n²)` costs `O(n²)` +// overall; a branch between `O(n)` and `O(m)` (incomparable) +// costs `O(n + m)` — both facts flow forward. +fn max_path(paths: List) -> SymbolicCost = + fold(paths, ConstantCost(0), max_path_step) + +// ── Dominance ─────────────────────────────────────────────────── +// +// Asymptotic dominance: `a` dominates `b` iff `a` grows at least as +// fast as `b`. Dropped terms in `normalize` and path selection in +// `max_path` both read this. +// +// Rules implemented here (DB-7 §"Dominance / normalization"): +// - Unknown dominates everything (safest over-approximation). +// - Constant is dominated by everything else. +// - Polynomial(v, k1) dominates Polynomial(v, k2) iff k1 >= k2. +// - Linear(v) = Polynomial(v, 1) for dominance purposes. +// - Product/Sum use the dominant child as a summary (MVP — full +// term-by-term comparison lands with the multi-variable +// fixtures in Stage 2d+ follow-up). +fn dominates(a: SymbolicCost, b: SymbolicCost) -> Bool = + match a { + UnknownCost(_) => True + ConstantCost(_) => + match b { + ConstantCost(_) => True + UnknownCost(_) => False + LinearCost(_) => False + PolynomialCost(_) => False + ProductCost(_) => False + SumCost(_) => False + LogCost(_) => False + } + LinearCost(va) => + match b { + ConstantCost(_) => True + LogCost(_) => True + LinearCost(vb) => same_size_variable(va, vb) + PolynomialCost(payload) => + if same_size_variable(va, payload.var) then + payload.degree <= 1 + else + False + UnknownCost(_) => False + ProductCost(_) => False + SumCost(_) => False + } + PolynomialCost(pa) => + match b { + ConstantCost(_) => True + LogCost(_) => True + LinearCost(vb) => + if same_size_variable(pa.var, vb) then + pa.degree >= 1 + else + False + PolynomialCost(pb) => + if same_size_variable(pa.var, pb.var) then + pa.degree >= pb.degree + else + False + UnknownCost(_) => False + ProductCost(_) => False + SumCost(_) => False + } + LogCost(va) => + match b { + ConstantCost(_) => True + LogCost(vb) => same_size_variable(va, vb) + LinearCost(_) => False + PolynomialCost(_) => False + ProductCost(_) => False + SumCost(_) => False + UnknownCost(_) => False + } + // Conservative fallback: the correct "dominant child summary" + // rule walks the composite's children and returns True iff any + // child dominates `b`. Expressing that walk in .dag requires + // mutual recursion between `dominates` (descending on + // `SymbolicCost`) and a list-iterating helper (descending on + // `List`), which v3's termination analyzer + // cannot prove yet — cluster descent witnesses in #519 share + // a single type, and cross-type mutual recursion lands as a + // substrate extension (flagged as a Lane 1 / Stage 2d+ + // follow-up in the ROADMAP). The Rust mirror in + // `src/v3/compiler/src/dag.rs::dominates` carries the + // recursive form; this .dag branch returns `False` as a + // conservative over-approximation — callers that ask "does a + // composite dominate `b`" get `False` (safe: composite stays + // in `drop_dominated`'s keep list, `max_path` preferring + // scalars), never a false True that could drop legitimate + // terms. The generated Rust projection of this lens is not + // affected because it reads through the Rust `dominates` + // function directly. + ProductCost(_) => False + SumCost(_) => False + } + +fn same_size_variable(a: SizeVariable, b: SizeVariable) -> Bool = + a.source_port == b.source_port + +// ── Normalization ─────────────────────────────────────────────── +// +// `normalize(c)` simplifies a SymbolicCost expression by: +// - dropping `ConstantCost(0)` from Sum/Product lists, +// - collapsing Sums/Products whose term lists reduce to a single +// element, +// - folding a Product of two identical LinearCosts into +// `PolynomialCost(var, 2)` — the nested-fold fingerprint the +// `all_pairs` fixture leans on, +// - otherwise returning the input unchanged. +// +// Full recursive flattening of nested Sums/Products is deferred — +// the composition ops construct trees two deep at most, so the +// MVP handles that surface directly. +fn normalize(c: SymbolicCost) -> SymbolicCost = + match c { + ConstantCost => c + LinearCost => c + PolynomialCost => c + LogCost => c + UnknownCost => c + SumCost(terms) => reduce_sum(drop_zero(terms)) + ProductCost(terms) => reduce_product(drop_zero(terms)) + } + +// Drops `ConstantCost(0)` terms from a list of costs. Used by +// normalize so `SumCost([Linear, Constant(0)])` collapses to the +// single Linear term (DB-7 acceptance test). +fn drop_zero(terms: List) -> List = + match terms { + Empty => empty() + Cons(payload) => + if is_zero_constant(payload.head) then + drop_zero(payload.tail) + else + cons(payload.head, drop_zero(payload.tail)) + } + +fn is_zero_constant(c: SymbolicCost) -> Bool = + match c { + ConstantCost(n) => n == 0 + LinearCost(_) => False + PolynomialCost(_) => False + ProductCost(_) => False + SumCost(_) => False + LogCost(_) => False + UnknownCost(_) => False + } + +// If a SumCost reduces to a single term, return that term; else +// keep the SumCost wrapper with dominated terms dropped. +// +// PR #537 reviewer (ChatGPT) call-out: the Cons-branch previously +// wrapped the result of `drop_dominated` in `SumCost(...)` +// unconditionally, so an input like `SumCost([Linear(n), +// Constant(5)])` — where `drop_dominated` correctly strips the +// dominated `Constant(5)` and leaves a singleton — landed as the +// invalid `SumCost([Linear(n)])`. Now a post-drop singleton +// unwraps via `wrap_sum` so the post-normalize carrier stays +// canonical (≥ 2 terms in any surviving `SumCost`). Rust mirror +// in `dag.rs::reduce_sum` already handles this via its +// `match terms.len()` arms; this keeps the .dag authority in +// sync. +fn reduce_sum(terms: List) -> SymbolicCost = + match terms { + Empty => ConstantCost(0) + Cons(payload) => + match payload.tail { + Empty => payload.head + Cons(_) => wrap_sum(drop_dominated(cons(payload.head, payload.tail))) + } + } + +fn wrap_sum(terms: List) -> SymbolicCost = + match terms { + Empty => ConstantCost(0) + Cons(payload) => + match payload.tail { + Empty => payload.head + Cons(_) => SumCost(cons(payload.head, payload.tail)) + } + } + +// If a ProductCost reduces to a single term, return it; if the +// product is two LinearCosts over the same variable, fold to +// `PolynomialCost(var, 2)`; otherwise keep the wrapper. +fn reduce_product(terms: List) -> SymbolicCost = + match terms { + Empty => ConstantCost(0) + Cons(payload) => + match payload.tail { + Empty => payload.head + Cons(second) => + match second.tail { + Empty => combine_binary_product(payload.head, second.head) + Cons(_) => ProductCost(cons(payload.head, payload.tail)) + } + } + } + +// Binary product special-case: two LinearCosts over the same port +// collapse to PolynomialCost with degree 2. Other shapes stay as +// a two-element ProductCost. +fn combine_binary_product(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + match a { + LinearCost(va) => combine_linear_with(va, a, b) + ConstantCost(_) => product_pair(a, b) + PolynomialCost(_) => product_pair(a, b) + LogCost(_) => product_pair(a, b) + SumCost(_) => product_pair(a, b) + ProductCost(_) => product_pair(a, b) + UnknownCost(_) => product_pair(a, b) + } + +fn combine_linear_with(va: SizeVariable, a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + match b { + LinearCost(vb) => collapse_linear_square(va, vb, a, b) + ConstantCost(_) => product_pair(a, b) + PolynomialCost(_) => product_pair(a, b) + LogCost(_) => product_pair(a, b) + SumCost(_) => product_pair(a, b) + ProductCost(_) => product_pair(a, b) + UnknownCost(_) => product_pair(a, b) + } + +fn collapse_linear_square( + va: SizeVariable, + vb: SizeVariable, + a: SymbolicCost, + b: SymbolicCost +) -> SymbolicCost = + if same_size_variable(va, vb) then + polynomial_square(va) + else + product_pair(a, b) + +fn polynomial_square(v: SizeVariable) -> SymbolicCost { + PolynomialCost { var: v, degree: 2 } +} + +fn product_pair(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost = + ProductCost(cons(a, cons(b, empty()))) + +fn any_dominates(candidates: List, term: SymbolicCost) -> Bool = + match candidates { + Empty => False + Cons(payload) => + if dominates(payload.head, term) then + True + else + any_dominates(payload.tail, term) + } + +fn filter_not_dominated_by( + candidates: List, + winner: SymbolicCost +) -> List = + match candidates { + Empty => empty() + Cons(payload) => + if dominates(winner, payload.head) then + filter_not_dominated_by(payload.tail, winner) + else + cons(payload.head, filter_not_dominated_by(payload.tail, winner)) + } + +fn drop_dominated_step( + acc: List, + term: SymbolicCost +) -> List = + if any_dominates(acc, term) then + acc + else + cons(term, filter_not_dominated_by(acc, term)) + +// Drops terms from a SumCost list that are dominated by another +// term in the list. MVP: O(n²) pairwise walk; acceptable because +// the sum lists in practice are short (≤ 3 terms). +fn drop_dominated(terms: List) -> List = + fold(terms, empty(), drop_dominated_step) diff --git a/src/v3/std/dimensions.dag b/src/v3/std/dimensions.dag new file mode 100644 index 00000000000..e1027e0b75e --- /dev/null +++ b/src/v3/std/dimensions.dag @@ -0,0 +1,59 @@ +// std.dimensions — the structural shape every compile-time proof +// lens shares. +// +// 🟡 SCAFFOLD at Stage 2d scope. This file declares the minimum +// `Dimension` + `Witness` types required for 2d's +// `symbolic_cost_dimension: Dimension` data +// declaration. Per DB-3 (`docs/design-dimension-abstraction.md`), +// Stage 2f owns the full abstraction — the generic `analyze` walker, +// `DimensionReport`, workflow detection, bootstrap discovery. +// 2d ships the carrier shape so that (a) 2f's later refactor keeps +// the same field names, and (b) 2b/2d/2e instances can already +// declare against a single-authority type. +// +// **What does not come over yet:** `fn analyze`, +// `DimensionReport`, monoid-law declarations. Those land +// in Stage 2f when the abstraction is pulled back over three +// concrete dimensions. +// +// See DB-3 §"Core type" for the full locked shape. + +module v3.std.dimensions + +import std.substrate { Dag, Behavior } + +// 🟢 TERMINAL at the structural-witness scope. `Witness` +// partitions per-operation evidence into two disjoint cases: +// +// - `Inhabits(c)` — this behavior is an ok member of the +// dimension's algebra; compose absorbs `c`. +// - `Violates {..}` — this behavior breaks the dimension; a +// diagnostic fires and composition stalls. +// +// The coproduct is authored at the witness level, not above it in +// an `Option` shape, so "no evidence" and "evidence of +// violation" cannot masquerade as each other (DB-3 §Rationale). +type Witness + = Inhabits(Carrier) + | Violates { reason: String, at: Behavior } + +// 🟢 TERMINAL at the dimension-surface scope. The four fields are +// the irreducible contract a compile-time property has to publish: +// - `name` — human-facing identifier +// - `witness_of`— per-op evidence extraction +// - `compose` — how two pieces of evidence combine along a +// workflow (must form a monoid with `identity`; +// law is documented not mechanically enforced — +// Stage 2f open question §2) +// - `identity` — fold unit / empty workflow value +// +// Stage 2d consumers MAY additionally declare a +// `break_diagnostic: fn(Behavior, Carrier) -> Diagnostic?` as a +// free-standing function on the lens side; the field form lands +// with the full abstraction in Stage 2f. +type Dimension { + name: String + witness_of: fn(Dag, Behavior) -> Witness + compose: fn(Carrier, Carrier) -> Carrier + identity: Carrier +}