Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
e5c2e7a
feat(v3): gate #92 T-LAS complexity enforcement compile error
cursoragent May 9, 2026
1403cb9
fix(v3): truthful LensEnforcement in complexity.dag + consume via len…
cursoragent May 9, 2026
470c508
fix: order ClassPolynomial budgets by PositiveDescentAmount in asympt…
cursoragent May 9, 2026
aeb247d
docs(v3): note poly–poly degree comparison in complexity_lattice
cursoragent May 9, 2026
9eb9be8
fix(ci): regen bootstrap — algebra asymptotic_dominates stays poly-ti…
cursoragent May 9, 2026
a3388aa
ci: exempt gate #92 T-LAS demo from 2s ratchet; bump exemption floor
cursoragent May 9, 2026
ddf99d8
fix(v3): emit complexity lens to complexity_lens_generated for L-8
cursoragent May 9, 2026
b540655
fix(v3): honest complexity_lens + Witness Inhabits emit for regen
cursoragent May 9, 2026
e426705
chore: apply cargo fmt to m2 lens cost migration test
cursoragent May 9, 2026
9f080c0
test(v3): ratchet complexity monoid op — no monoid_op_stub, sequentia…
cursoragent May 9, 2026
45b8164
test(v3): ratchet honest complexity_lens branch/iterate; doc compose …
cursoragent May 9, 2026
f543c78
ci: SG-0 append for PR #2340 (+4 census paths, issue #1952 pairing)
cursoragent May 9, 2026
2ca2ec3
fix(complexity): correct work-class predicate; track poly lattice bridge
cursoragent May 9, 2026
1a3cbf9
ci: classify ComplexityEnforcedApplication in compiler-std ratchet (#…
cursoragent May 9, 2026
bbe0605
docs(complexity): clarify work-class consistency dominate direction
cursoragent May 9, 2026
98defe0
test(v3): ratchet complexity_summary_work_class_consistent (Log vs Li…
cursoragent May 9, 2026
765aadd
fix(v3): name T-LAS budget lattice; reject sub-cubic ClassPolynomial …
cursoragent May 9, 2026
1941d3e
docs(complexity): de-confuse inline review anchor ~493 vs work-class …
cursoragent May 9, 2026
444316f
chore(v3): refresh parse_corpus_manifest for std/algebra.dag
cursoragent May 9, 2026
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
2 changes: 2 additions & 0 deletions .cargo/config.toml
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,5 @@ jobs = 2 # max parallel rustc/linker invocations per ca

[env]
RUST_TEST_THREADS = { value = "1", force = false } # max parallel test threads per binary
# v3-compiler bootstrap/integration tests exhaust default thread stacks in debug builds.
RUST_MIN_STACK = { value = "16777216", force = false }
2 changes: 1 addition & 1 deletion docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -290,7 +290,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 89 | `section_ref_substrate_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | SectionRef disjoint sum (DeclarationScope / NodeScope) in `src/v3/std/lens_application.dag` |
| 90 | `lens_enforcement_carrier_landed` | substrate-shape | T-Lens-Application-Surface | CONSUMER_LANDED (Slice A receipt PR #2145) | parametric `LensEnforcement<Output, Budget>` + `EnforceableLens<Output, Budget>` carriers in `src/v3/std/lens_application.dag`; per-lens data instances co-located with each lens land in Slice B |
| 91 | `enforce_violation_routing_landed` | structural-fold | T-Lens-Application-Surface | DECLARED — substrate routing surface landed PR #2145 (`DiagnosticSeverity = Error` + `EnforcedApplication.diagnostic_severity` + `LensEnforcement.violates`); CONSUMER_LANDED requires the fold-pass consumer per design doc §10 step 2 — deferred to Slice B | Enforce-mode violation routing through `DiagnosticSeverity` per design §3 + INVARIANTS C-8 |
| 92 | `complexity_violation_compile_error_demonstrated` | demonstration | T-Lens-Application-Surface | DECLARED (added to §"Acceptance" 2026-05-06) | apply_lens(complexity, fn, Enforce) fires compile error |
| 92 | `complexity_violation_compile_error_demonstrated` | demonstration | T-Lens-Application-Surface | RECEIPT (`t_las_complexity_contract_demo.dag` + `t_las_complexity_contract_compile_error_test.rs`) | `EnforcedApplication` + `complexity_enforceable`; `complexity_of` > `ClassLog` ⇒ `ParseError` “lens enforcement violation” |
| 93 | `crdt_cost_basis_demonstrated` | demonstration | T-Lens-Application-Surface | DECLARED (added to §"Acceptance" 2026-05-06) | CRDT cost basis via apply_lens |
| 94 | `memory_peak_cost_basis_demonstrated` | demonstration | T-Lens-Application-Surface | **CONSUMER_LANDED + PASSING** (#1954 — `memory_peak_cost` + cementing demo; **Enforce**: `memory_peak_enforcement_violates` is true iff `!dominates(declared_budget, observed_peak)` (budget covers peak in the `SymbolicCost` order; ties + incomparable cases unit-pinned); **`SizeVariable`** matches `src/v3/std/algebra.dag` incl. optional `display_name`; parser `apply_lens(cost, …, Enforce { dimension: Memory, … })` still awaits gate #91) | memory-peak cost basis |
| 95 | `opt_in_iteration_parallelism_via_lens_application_demonstrated` | demonstration | T-Lens-Application-Surface → **R4-CARVED (C1)** | **CARVED to R4** per `docs/r4-carve-out-routing.md` C1 cascade with `parallelism_lens_behaviorally_complete` — Pass requires parallelism lens BEHAVIORALLY COMPLETE (`docs/design-lens-application-surface.md` §4.4 / §7); **not** R3 thesis-close load-bearing |
Expand Down
4 changes: 2 additions & 2 deletions docs/thesis/compiler-std-consolidation.md
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ Baseline (2026-04-22, measured via `grep -cE "^type [A-Z]"` after the tokenizer
| `src/v3/compiler/operators.dag` | 0 | — |
| `src/v3/compiler/pipeline.dag` | 3 | positive-def |
| `src/v3/compiler/regen.dag` | 1 | positive-def |
| `src/v3/lenses/complexity.dag` | 4 | 4 positive-def (`Certainty`, `ComplexitySummary`, `ComplexityEntry`, `DominanceOutcome`); return surface is imported `v3.std.lookup::Lookup` (not a lens-local `type` decl) |
| `src/v3/lenses/complexity.dag` | 5 | 5 positive-def (`Certainty`, `ComplexitySummary`, `ComplexityEntry`, `DominanceOutcome`, `ComplexityEnforcedApplication` — T-LAS `EnforcedApplication` alias); return surface is imported `v3.std.lookup::Lookup` (not a lens-local `type` decl) |
| `src/v3/lenses/cost.dag` | 3 | 3 positive-def (`CostBasisKind`, `CostBasisDeclaration`, `SymbolicCostEntry`); return surface is imported `v3.std.lookup::Lookup<SymbolicCost>` (not a lens-local `type` decl) |
| `src/v3/lenses/idempotency.dag` | 0 | — |
| `src/v3/lenses/infer_helpers.dag` | 4 | 3 in-ratchet (`TemplateArgumentsMatch`, `TemplateArgumentCursor`, `NormalizedInstantiationArgs` — workaround-shaped coproduct scaffolds with named dissolution triggers) + 1 positive-def (`TemplateArgumentBinding = Conflict \| NoOp \| Append \| ReplaceAt` — semantic carrier); template-argument presence uses imported `Lookup<DeclarationId>` |
Expand All @@ -151,7 +151,7 @@ Baseline (2026-04-22, measured via `grep -cE "^type [A-Z]"` after the tokenizer
| `src/v3/lenses/unused_parameters.dag` | 1 | positive-def (`UnusedParameter`) |
| `src/v3/lenses/variant_payload.dag` | 2 | both positive-def (`VariantPayloadShape` domain type + `VariantPayloadShapeLookup` — 3-variant carrier with `NotPayloadProduct` semantic distinction, not generic Lookup) |

**Primary ratchet count today: 3** (0 strict 2-variant Lookup-pattern carriers on lens surfaces — `complexity`, `cost`, and `infer_helpers` import `v3.std.lookup::Lookup` + 3 workaround-shaped infer-helper coproducts: `TemplateArgumentsMatch`, `TemplateArgumentCursor`, `NormalizedInstantiationArgs`). The tokenizer migration removed 6 compiler-local type declarations by moving them to `src/v3/std/tokenize.dag` (25 → 19). Consolidation tranche 2 removed 14 by moving the parse-surface family to `src/v3/std/parse_surface.dag` (19 → 5). The SG-4b callable-instantiation normalization cluster adds `NormalizedInstantiationArgs` as a tracked workaround carrier (Option-as-enum, paired to dissolve alongside `TemplateArgumentsMatch` when the lens→Rust emitter lands verified `T?` / `Bool` return mappings). The complexity lens completion slice widens the positive-def API from the old `CostEntry` row to `Certainty`, `ComplexitySummary`, `ComplexityEntry`, and `DominanceOutcome` while keeping the generic presence carrier imported from `v3.std.lookup`. All lens-local types now classified — `structural_resolution.dag`'s two record types (`UnresolvedArrowBody`, `NameKeyedReference`) are positive-def lens-API carrying the lens's findings.
**Primary ratchet count today: 3** (0 strict 2-variant Lookup-pattern carriers on lens surfaces — `complexity`, `cost`, and `infer_helpers` import `v3.std.lookup::Lookup` + 3 workaround-shaped infer-helper coproducts: `TemplateArgumentsMatch`, `TemplateArgumentCursor`, `NormalizedInstantiationArgs`). The tokenizer migration removed 6 compiler-local type declarations by moving them to `src/v3/std/tokenize.dag` (25 → 19). Consolidation tranche 2 removed 14 by moving the parse-surface family to `src/v3/std/parse_surface.dag` (19 → 5). The SG-4b callable-instantiation normalization cluster adds `NormalizedInstantiationArgs` as a tracked workaround carrier (Option-as-enum, paired to dissolve alongside `TemplateArgumentsMatch` when the lens→Rust emitter lands verified `T?` / `Bool` return mappings). The complexity lens completion slice widens the positive-def API from the old `CostEntry` row to `Certainty`, `ComplexitySummary`, `ComplexityEntry`, `DominanceOutcome`, and `ComplexityEnforcedApplication` while keeping the generic presence carrier imported from `v3.std.lookup`. All lens-local types now classified — `structural_resolution.dag`'s two record types (`UnresolvedArrowBody`, `NameKeyedReference`) are positive-def lens-API carrying the lens's findings.

End state: 0. Each migration lane reduces the count; positive-definition types track growth separately and are not bounded downward by this ratchet.

Expand Down
3 changes: 2 additions & 1 deletion scripts/check-compiler-std-ratchet.sh
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,9 @@ POSITIVE_ROWS=(
"src/v3/compiler/pipeline.dag:PipelineStageBinding"
"src/v3/compiler/regen.dag:LensRegistryEntry"
"src/v3/lenses/complexity.dag:Certainty"
"src/v3/lenses/complexity.dag:ComplexitySummary"
"src/v3/lenses/complexity.dag:ComplexityEnforcedApplication"
"src/v3/lenses/complexity.dag:ComplexityEntry"
"src/v3/lenses/complexity.dag:ComplexitySummary"
"src/v3/lenses/complexity.dag:DominanceOutcome"
"src/v3/lenses/cost.dag:CostBasisKind"
"src/v3/lenses/cost.dag:CostBasisDeclaration"
Expand Down
7 changes: 4 additions & 3 deletions scripts/check-test-timeout.sh
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,9 @@
# (default scripts/slow-test-exemptions.txt).
# TEST_TIMEOUT_MAX_EXEMPTIONS
# Ratchet floor for active exemption entries
# (default 41, captured 2026-05-09 with two
# `cost_lens_symbolic_consumer_test::*` rows). Lower this
# (default 42, captured 2026-05-09: main's 41 incl. two
# `cost_lens_symbolic_consumer_test::*` rows plus gate #92
# T-LAS demo line). Lower this
# value in the same PR that removes exemptions.

set -euo pipefail
Expand All @@ -56,7 +57,7 @@ log_file_arg=${1:-}
budget_ms=${2:-${TEST_TIMEOUT_MS:-2000}}
pkg=${TEST_TIMEOUT_PACKAGE:-v3-compiler}
exempt_file=${TEST_TIMEOUT_EXEMPT:-scripts/slow-test-exemptions.txt}
max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-41}
max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-42}

script_dir=$(cd "$(dirname "$0")" && pwd)
repo_root=$(cd "$script_dir/.." && pwd)
Expand Down
3 changes: 3 additions & 0 deletions scripts/ci-merge/sg0-pr-body-append.2340.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
SG-0 hand-path delta: +4

SG-0 pairing: (b) https://github.com/gunb-ai/gunbc/issues/1952
2 changes: 1 addition & 1 deletion scripts/regen_runtime_mirrors.py
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@


# Structural mirror of `src/v3/std/lookup.dag`: `Lookup` + `miss_int_lookup` /
# `hit_int_lookup`. `lens_cost_generated` does **not** call these fns — emit
# `hit_int_lookup`. `complexity_lens_generated` does **not** call these fns — emit
# (`lookup_monomorphized_constructor_emit` in `rust_target.rs`) lowers std callables to
# `Lookup::Miss` / `::Hit` — but the fns are still the correct `crate::dag`
# surface for the `.dag` names and avoid any "helper missing in Rust" confusion.
Expand Down
2 changes: 2 additions & 0 deletions scripts/slow-test-exemptions.txt
Original file line number Diff line number Diff line change
Expand Up @@ -78,4 +78,6 @@ sg6_hand_authored_census_test::sg6_regen_lens_cli_smoke_regenerates_named_entry_

t_demo_fixture_test::t_demo_canonical_suites_are_runner_visible # ROADMAP T-Demo (Lane M): cold `compile_to_dag` on full `t_demo_fixtures.dag` + two `TestRunner::run_suite` passes; ~2.6–3.3s wall on isolated/filtered runs (above 2s Phase-0 ratchet). `compile_fixture` uses `cached_compile_to_dag`; module `OnceLock` still shares one `Dag` across sibling tests. Dissolution: delete this line and lower `TEST_TIMEOUT_MAX_EXEMPTIONS` in the same commit once `RUSTC_BOOTSTRAP=1 cargo test -p v3-compiler t_demo_canonical_suites_are_runner_visible -- -Z unstable-options --report-time` shows <=2000ms wall on cold ubuntu-latest after fixture slimming or shared-runner warming (TESTING.md).

t_las_complexity_contract_compile_error_test::complexity_violation_compile_error_demonstrated # ROADMAP gate #92 / issue #1952: T-LAS `compile_to_dag` demo fixture with prepended complexity authority + 64MiB stack thread — cold CI ~14s wall. Dissolution: delete this line and lower `TEST_TIMEOUT_MAX_EXEMPTIONS` in `scripts/check-test-timeout.sh` in the same commit once `RUSTC_BOOTSTRAP=1 cargo test -p v3-compiler complexity_violation_compile_error_demonstrated -- -Z unstable-options --report-time` reports <=2000ms wall on cold CI after shared `OnceLock` / slimmer demo (TESTING.md Phase-0 ratchet pattern; cf. `t_demo_canonical_suites_are_runner_visible` above).

thesis_validation_test::kf_1_structural_list_operation_ordering_holds # KF-1 thesis validation remains compile-heavy on CI runners; TESTING.md test-shape paydown owns future decomposition, not TM-0.
4 changes: 2 additions & 2 deletions src/v3/compiler/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -362,8 +362,8 @@ fn main() {
// Tell Cargo to re-run the script if any staged std/spec/compiler file
// changes. Without this, adding a new file wouldn't trigger a
// rebuild and bootstrap would silently miss it.
println!("cargo:rerun-if-changed={}", std_dir.display());
println!("cargo:rerun-if-changed={}", spec_dir.display());
println!("cargo:rerun-if-changed={}", std_dir.display());
println!("cargo:rerun-if-changed={}", compiler_dir.display());
println!("cargo:rerun-if-changed={}", extdeps_dir.display());
println!("cargo:rerun-if-changed={}", gunbc_dir.display());
Expand Down Expand Up @@ -496,7 +496,7 @@ fn main() {
"src/v3/compiler/src/dag_value_body_generated.rs",
"src/v3/compiler/src/diagnostics_generated.rs",
"src/v3/compiler/src/infer_helpers_generated.rs",
"src/v3/compiler/src/lens_cost_generated.rs",
"src/v3/compiler/src/complexity_lens_generated.rs",
"src/v3/compiler/src/lens_cost_symbolic_generated.rs",
"src/v3/compiler/src/lens_cost_target_realization_generated.rs",
"src/v3/compiler/src/lens_effect_enumeration_generated.rs",
Expand Down
2 changes: 1 addition & 1 deletion src/v3/compiler/regen.dag
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ type LensRegistryEntry {
data lens_cost_entry: LensRegistryEntry = {
name: "cost"
lens_file: "src/v3/lenses/complexity.dag"
generated_file: "src/v3/compiler/src/lens_cost_generated.rs"
generated_file: "src/v3/compiler/src/complexity_lens_generated.rs"
}

data lens_cost_symbolic_entry: LensRegistryEntry = {
Expand Down
Loading
Loading