From 711b5ae8d90438fd0057ec9c3c209936b210b83c Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Tue, 14 Jul 2026 23:54:10 -0400 Subject: [PATCH 01/28] v2 memory-control audit: space is unobservable, and required fields are unenforced Investigation (no source changes) into whether v2's memory management is "perfectly understood/controlled" ahead of the Realization switch. Every claim is green-by-execution or refuted-by-execution against da71e41d0, with a calibration control. Headline (F1, corpus-wide, NOT memory-specific): record-literal field PRESENCE and field TYPES are unchecked. `gunbc compile --target dag` (the compile-clean gate's own path) reports `0 diagnostics` for a CacheProvider with `eviction` omitted, for `eviction: 42`, for CostAccount missing 3 of 4 fields, and for DependencyView missing 3 of 4 with `kind: 999`. Calibration: a bogus field NAME hard-errors, so the typechecker runs -- it checks names only. Therefore materialization_ladder.dag:28's "CacheProvider cannot be written without an EvictionClass" is false by execution, and every "by construction, it's a required field" claim in the corpus rests on an unenforced property (DESIGN section 5, correctness-by-construction). Memory findings: - F2 (keystone): RealizationMeasureEffect has ONE variant, ObserveElapsedAtSubject. v2 has no effect that observes space, so CostAccount.space can never be Measured. - F7: FLAG D assigns memory-packing to `realize` over "per-node MEASURED peak RSS" (min(width, budget/peak); section 6-1 names the exit-137 failure mode). F2 makes that input unproducible -- `realize` is unbuildable as designed. - F6: of run = realize . materialize . dependency_view, `realize` and `dependency_view` have 0 definitions; materialize is analysis-only. spine.dag does not import v2.std.dependency; DependencyView is flat (no frames). - F4: space has no seq/par algebra; fleet_intent.dag:168 SUMS space over a sequential rollup (peak is max, not sum) and a witness asserts the sum. - F5: `eviction` has no reader; inverting every eviction class leaves 24/24 green. - F10 (ordering): claim_executor evaluates every v2 witness on the v1 tree-walker, so the only realized eviction is two hand-written v1 Rust mechanisms the ladder does not dispatch. Deleting v1 zeroes realized eviction while declared eviction stays green. Receipt: whole hermetic corpus green on a Raspberry Pi 3 (1837/1837 PASS, 554 entry groups) at VmSize 6.25 GB / 6.0 GB swapped, ~8.4 MB per entry, never released; 13 GB swap to finish. Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/plans/v2-memory-control-audit.md | 155 ++++++++++++++++++++++++++ 1 file changed, 155 insertions(+) create mode 100644 docs/plans/v2-memory-control-audit.md diff --git a/docs/plans/v2-memory-control-audit.md b/docs/plans/v2-memory-control-audit.md new file mode 100644 index 00000000000..a2706882daa --- /dev/null +++ b/docs/plans/v2-memory-control-audit.md @@ -0,0 +1,155 @@ +# v2 memory control — audit (2026-07-14) + +**Question (operator):** switching v2 to Realization; memory management should be *perfectly understood and controlled* at that point. Is it? + +**Answer: no — and the reason is not a memory bug.** v2 cannot **observe**, **compose**, or **refuse on** space, and the construction mechanism that the whole model leans on (required record fields) is **not enforced by the compiler**. Every claim below is green-by-execution or refuted-by-execution against `da71e41d0`, with a calibration control. v1 is treated only as displaced-cost evidence. + +Receipts: the whole hermetic corpus ran green on a Raspberry Pi 3 (`claim_batch --roster-from-discovery`, 554 entry groups, **1837/1837 PASS**) while the process reached **VmSize 6.25 GB / 6.0 GB swapped**, growing ~8.4 MB per entry, never released — 13 GB of swap to finish; stock config OOMs near entry ~350. Log: `.forensics/claim_full.log` (untracked). + +--- + +## F1 — record-literal field presence and types are UNCHECKED (the keystone; scope is corpus-wide) + +This is the largest finding and it is **not** scoped to memory. DESIGN §5's primary move is *"make the bad state **unwritable** — correctness by construction, not validation."* In this tree, the main construction device — a required record field — **does not exist in practice**. + +Executed against `gunbc compile --target dag` (the CI compile-clean gate's own path): + +| probe | expected | actual | +|---|---|---| +| `CacheProvider` — all fields, well-typed | compiles | `0 diagnostics` ✓ | +| `CacheProvider` — **`eviction` field omitted** | refuse | **`0 diagnostics`** ✗ | +| `CacheProvider` — **`eviction: 42`** (Int vs `EvictionClass`) | refuse | **`0 diagnostics`** ✗ | +| `CostAccount` — **3 of 4 fields omitted** | refuse | **`0 diagnostics`** ✗ | +| `DependencyView` — **3 of 4 omitted + `kind: 999`** | refuse | **`0 diagnostics`** ✗ | +| **calibration:** bogus field *name* | refuse | **hard error** ✓ — `field 'bogus_field_xyz' not found in type 'CacheProvider'` | + +The calibration proves the typechecker runs on this path. It checks field **names** only — never **presence**, never **types**. (`tier: 42` even survives typecheck and dies at *runtime*: `non-exhaustive pattern match on: 42`.) + +**Consequence.** `dag/std/materialization_ladder.dag:28` asserts *"Rule 3 (eviction) is by construction, not by check: `CacheProvider` cannot be written without an `EvictionClass`."* That sentence is **false by execution**. More broadly: **every "by construction, it's a required field" claim in the corpus rests on a property the compiler does not enforce.** This is worse than the §5 tell the operator named ("satisfied by editing the declaration while the realization lies") — here the *declaration itself* is unchecked. + +This belongs **on** ROADMAP ④'s path, not after it: Realization's guarantees are declared as record fields. + +→ **Dissolve-on:** field-presence + field-type checking in `04_infer`'s record-literal arm, with a discriminating RED per arm (omitted field; wrong-typed field), and a corpus sweep for literals currently relying on the hole. + +## F2 — v2 has no effect that can observe space + +`dag/std/realization_measurement.dag:25` — the **entire** realization-measurement effect coproduct: + +``` +type RealizationMeasureEffect + = ObserveElapsedAtSubject { subject: ContentHash, work_shape: String } +``` + +One variant. Time. `grep -rniE 'ObservePeak|PeakResident|peak_rss|rusage' dag src/v2` → prose only, zero carriers. The producing seed agrees: `PerformanceReceipt` (`src/v1/stage0/src/v1_interpreter.rs:8336`) is `{subject_key, work_shape, wall_nanos, eval_self_nanos, sample_count}` — **no memory field**. + +So **`CostAccount.space` with `basis: Measured` is not producible in v2.** Every space value in the tree is a literal or a passed-in parameter (`fleet_host_budget.dag:66` `space: cfg.mib_per_job`, `basis: Predicted`). + +This is why the 6.25 GB was *invisible to the model* rather than merely unfixed. Per §5, a deficit whose frequency is zero by construction never ranks for fixing. + +→ **Dissolve-on:** `ObservePeakResidentAtSubject` as a second variant on the existing effect (extends an existing authority — **not** a new one). + +## F3 — the space axis is modeled shallower than time, and cannot express retention + +`dag/std/realization_schedule.dag:23`: + +``` +type CostAccount { + time: Measure // full Measure: basis, scale, unit + space: ByteSize // naked scalar + power: Watt // naked scalar — watt(0) at 100% of construction sites + basis: CostBasis +} +``` + +DESIGN §2 cites `Cost = Time|Space|Energy → a record (every cost has all three)` as a *worked example of good decomposition*. In the tree only time is decomposed to depth; the record is currently the strongest evidence **for** the claim it falsifies. + +A scalar `ByteSize` **structurally cannot express the actual bug**: it cannot distinguish "allocated 8.4 MB and freed it" from "allocated 8.4 MB per entry and never released." CLAUDE.md's own thread says the failure axis is *"retention, not footprint"* — and the type has no way to say *retained*. + +Two §3 notes: the carrier says `Power`, DESIGN says `Energy`, and `Energy` is not a `Quantity` at all (`dag/std/measure.dag:6-31`) — the **doc** is the error (energy = power × time; time is already a field). And `power` is a phantom: `watt(count: 0)` everywhere. + +→ **Dissolve-on:** a retention/residency axis expressed as the **ladder's existing** eviction concept applied to the space quantity (`ScopeExit`/`SpacePacked`) — **not** a second retention taxonomy (that would be the §3 fork). + +## F4 — space has no algebra, and the one rollup applies time's rule (asserted as contract) + +`dag/std/realization_measurement.dag:74,86` give Time two composition rules — `time_measure_seq` (**add**) and `time_measure_par` (**max**). **Space has no peer.** + +`dag/gunbc/fleet_intent.dag:168` **sums** space across a receipt list: + +``` +space: byte_size(count: fold(receipts, init: 0, + f: (acc, receipt) => acc + byte_size_count(receipt.cost.space))) +``` + +Space is the **dual** of time: sequential steps release (peak = **max**), concurrent steps co-reside (peak = **add**). This applies the parallel rule to the serial axis. `dag/test/claim/realization_measurement_keystone_test.dag:63` asserts the sum **as the contract** — the §5 "enshrined degradation" pattern. + +→ **Dissolve-on:** `space_measure_seq` (max) / `space_measure_par` (add) as peers of the time rules; flip the witness. + +## F5 — eviction is a write-only label; no reader, no RED + +`eviction` appears at 5 sites in the ladder (type `:55`, field `:75`, ctors `:133`, `provider_row` param/passthrough `:146/:148`). **No reader anywhere in the corpus.** + +Executed perturbation: **every eviction class deliberately inverted** (CAS persistent → `ScopeExit`; in-process reference/copy/memo → `SpacePacked{"NONSENSE-no-such-budget"}`) → **24/24 witnesses still PASS**, identical to baseline. There is no discriminating RED for eviction. No function relates `tier`/`placement` to `eviction` (the "ScopeExit for scoped, SpacePacked for persistent" coherence rule is **not modeled at all**). + +**Blast radius is specific — the ladder is not vaporware.** Its *verdict* logic (plurality → LCA → discharge/refuse/accept) is genuinely inhabited and runs over the real emitted `ci.yml`, with real RED controls (`dag/gunbc/ci_materialization_gate.dag:45,61`; `floor_materialization.dag:89,98` with RED `floor_index_build_materialization_without_provider`). The **eviction dimension specifically** is hollow. + +## F6 — `run ≜ realize ∘ materialize ∘ dependency_view`: two of three do not exist + +``` +fn realize -> 0 definitions +fn dependency_view -> 0 definitions +fn run -> 0 definitions +fn materialize -> 1 (analysis-only; nothing executes off its verdicts) +``` + +`src/v2/std/spine.dag` **does not import `v2.std.dependency`** — its `critical_path_depth`/`independence_width` fold the Node *containment tree*, not the `DependencyView`. `DependencyView` (`src/v2/std/dependency.dag:36`) is flat — `{source, dependent, kind, usage_site}` — **no frames, no nesting**. ROADMAP ④'s "ONE *nested* DependencyView" is not inhabited; the tree already says so (`src/v2/compiler/materialization_carriers.dag:41` dissolve-on). + +Frames **are** inhabited (`materialization_ladder.dag:30-47`) and an LCA **is** computed (`frame_path_lca:220`, `group_obligation_lca:347`) — but at **outer** scopes only (CI run / shell / process), from hand-supplied `site: List`. **The eval frame — where the memory actually lives — has no `Frame` carrier.** + +## F7 — F2 blocks `realize`; the two findings are one keystone + +`execution-spine-design.md:146` (**FLAG D**) assigns memory-packing to `realize`, and is explicit that memory does **not** become the OS's problem: budget/packing is *"`realize`'s packing over a modeled host-fact set (budget + per-node **measured** peak RSS + placement)"*, `achievable_concurrency = min(independence_width, budget / peak)` (`:97`). §6-1 (`:100`) names the failure by exit code: *"**pack on measured peaks, never guessed** — a memory-blind scheduler that packs by count OOMs (the exit-137 failure mode)."* + +**`realize` requires measured peak. F2 says no effect can produce it.** `ObservePeakResidentAtSubject` is therefore the single blocking keystone: without it there is no measured space → no `realize` packing → no spine, and the `memory_governor`'s own dissolve-on (*"graph-derived per-node demand (`CostAccount.space` measured) replaces the reactive estimator"*, `src/v2/workflow/ci_floor_plan.dag:225`) **can never fire**. + +## F8 — "memory dissolves into process frames" is half true; the wrong half is the actionable one + +- **True:** no GC/arena/bytecode-VM is planned or wanted (`v1-run-stability-throughline.md:174`), and emit-on-demand **is** the declared exit for the interpreter's retention class (`:3`). Frames-as-processes bounds **lifetime** — that is exactly what `ScopeExit` ("eviction = frame exit, derived") names. +- **False:** it does not bound **footprint**, and the design refuses to let it. Already falsified in-tree: the floor's frames **are** processes today (`floor_materialization.dag:29` `claim_executor-process`), and the whole-corpus run still died — the governor packs to `memory.high` *by construction*, was forced to `forced_serial=1` with 474 back-offs, and *"dies by step-cap — **a time death caused by a memory shape**"* (`v1-run-stability-throughline.md:15`). + +**Process isolation bounds lifetime, not footprint.** The `min(width, budget/peak)` half of `realize` is precisely the part that does not dissolve — and it is unbuilt. + +## F9 — emit-on-demand: transport landed, artifact path absent + +ROADMAP.md:37 is unchecked. **(a) agreement**: real and good — `src/v2/compiler/emit_host.dag` does emit→build→run (`run_host_process:245`, `run_test_claim_emit_vs_eval:459`), 15 `emit_host_*_equals_eval` witnesses each with a discriminating RED, CI-gated. **(b) content-hash reuse: does not exist** — `TestClaimCacheKey` (`src/v2/compiler/05_eval.dag:925`) is a key with no store, no content hash, no reuse; `emit_on_demand` appears in **one** plan doc and **zero** carriers. The named first customer (parse census) is absent from code. + +## F10 — ORDERING CONSTRAINT: deleting v1 zeroes v2's realized memory control + +`claim_executor` imports the v1 tree-walker directly (`src/v1/stage0/src/bin/claim_executor.rs:26`, `make_eval_context:613`). **Every v2 witness, lens, `materialize` and `spine_receipt` included, evaluates on it.** v2 inherits `InterpContext` retention (`v1_interpreter.rs:1169`) wholesale. + +The **only** realized eviction in the tree is two hand-written v1 Rust mechanisms the ladder does **not** dispatch: +- `eval_call_memo_frame_exit` (`v1_interpreter.rs:900`), hand-called at 4 sites (`claim_batch.rs:458,638`; `claim_executor.rs:623,691`) — `dag/extdeps/realization/eval_memo.dag:28` self-declares `Scaffold { dissolves_to: RealizationDispatch }`, i.e. *the ladder does not drive me yet*. Its receipt records the regression it fixed: single-witness plateau ~3.4 GiB vs six-witness climb past ~20 GiB to **SIGKILL**. +- `enforce_size_bound` (`src/v1/stage0/src/resolved_graph_cache.rs:346`). + +> **On the day the seed is deleted, the tree's *realized* eviction goes to zero while its *declared* eviction stays green — and the ladder will not notice, because it never reads the field.** + +Compounding: `duplicate-work-graph-lens-design.md` **cancelled C3** — described verbatim as *"the resolve-store scope fix (first **derived** eviction; the 9 GB receipt)"* — on the grounds that *"the W4 9 GB resolve-store pain… is an ops fix, not a modeling target."* That was the one lane that would have made eviction derived. And `DESIGN.md:91` records eviction as *"(M2, the shelved #5886 projection) … staged behind measured triggers"* — but the trigger is a measurement (F2) that cannot be taken. + +--- + +## Ranked work (each denominated in displaced cost, §6) + +| # | Item | Authority | Displaced cost | +|---|---|---|---| +| **1** | **Field presence + type checking on record literals** (F1) | Existing — `04_infer` record-literal arm | Every "by construction" guarantee in the corpus, including all of ④'s. Cheapest known path to making the ladder's own claim true. | +| **2** | **`ObservePeakResidentAtSubject`** (F2) | Existing — extends `RealizationMeasureEffect` | The keystone. Unblocks `CostAccount.space: Measured` → `realize`'s `min(width, budget/peak)` → the governor's dissolve-on. Without it F7 is unbuildable. | +| **3** | **`space_measure_seq`/`_par`** (F4) | Existing — peers of the time rules | Fixes a live bug asserted as contract; any width fold reading the rollup mis-predicts peak. | +| **4** | **Retention axis** — peak vs steady-state (F3) | Existing — the ladder's eviction concept, **not** a new taxonomy | The 9 GB retain-forever store *is* this concept missing. A scalar cannot express it. | +| **5** | **`MemoryBudgetExceeded { observed, budget, subject }`** | Existing pattern — mirrors `EvalBudgetExceeded` (`v1_interpreter.rs:660`) | Today OOM is untyped, uncounted death. Time got its tourniquet (270 min of billed silence → named red). Space still returns exit 137. | +| **6** | **Make the ladder *read* `eviction`** (F5) | Existing | A required field you never read controls nothing. Needs a tier↔eviction coherence rule + a RED. | +| **7** | **v1-deletion ordering** (F10) | Sequencing | Either 1–4 land first, or `memory_governor` migrates to a carrier, or v1 deletion is blocked. | + +**Not recommended:** a GC, an arena, or a bytecode VM. The design's rejection of these is correct and should stand. + +## Live §5 violation found in passing (unrelated to memory, same audit) + +`dag/std/realization_width.dag:108-111` and `:140-144`: budget unreadable → **fabricate a width** (`conservative_fallback_width`). ⊤-as-ignorance answered with a number — untyped, uncounted. Enshrined by two witnesses (`:271` `witness_stamp_unreadable_budget_falls_back_conservative`, `:276`). Should be `WidthUnknown { cause: BudgetUnreadable }` (the established third-arm pattern: `DescentUnknown`, `IdentityUnknown`). From 1b199dc3d096b1625785ac39f8d4df8e41a4d5ce Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Wed, 15 Jul 2026 00:01:09 -0400 Subject: [PATCH 02/28] Witness-realization plan: the v2 execution path (P0-P6), off the v1 crutch MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Companion to the memory-control audit. Anchor scenario (operator): emit witnesses to native code and schedule the runs with realization. Splits the "v1 crutch" into the execution crutch (every v2 witness evaluates on the v1 tree-walker) and the compiler crutch (self-hosting, separate lane); this plan removes the first without waiting for the second — the seed emitter is part of the artifact KEY, not the architecture. P0 field wall (audit F1, staged ledger->drain->wall) -> P1 space observable (ObservePeakResidentAtSubject; host physics already in claim_batch, unmodeled; space seq=max/par=add) -> P2 content-addressed artifact store (first real CacheProvider; first READER of eviction; ExistenceKeyed unwritable by shape) -> P3 emit-on-demand v0 (wrap emit_host with the store; ROADMAP's own a/b/c) -> P4 realize v0 (min(width, budget/measured_peak); CostUnknown -> width-1 maturation reserve; governor dissolve-on fires; ACCEPT = whole corpus on this 905MB Pi with flat VmSwap) -> P5 demands derived from dependency_view (materialize Share drives real reuse) -> P6 cutover + interpreted==native falsifier; F10 ordering constraint cleared. FLAGs for operator: A hermetic admissibility of pinned-toolchain builds; B artifact granularity (per-entry v0, module-grain derived later); C the C target (rows are cheap, the runtime realization is not; defer until a displaced cost names it). Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/plans/witness-realization-plan.md | 56 ++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 docs/plans/witness-realization-plan.md diff --git a/docs/plans/witness-realization-plan.md b/docs/plans/witness-realization-plan.md new file mode 100644 index 00000000000..12a3365133b --- /dev/null +++ b/docs/plans/witness-realization-plan.md @@ -0,0 +1,56 @@ +# Witness realization — the v2 execution path (plan) + +**Anchor scenario (operator, 2026-07-14):** emit witnesses to native code (Rust now; C stays a row-policy option) and use realization/materialization to schedule the runs. Companion to [v2-memory-control-audit.md](v2-memory-control-audit.md) — that doc is the findings; this one is the dependency-ordered work that discharges them. Nothing here waits on self-hosting. + +## Two crutches, separable + +"v1 as a crutch" is two distinct dependencies: + +1. **Execution crutch** — every v2 witness evaluates on the v1 tree-walker (`src/v1/stage0/src/bin/claim_executor.rs:26` imports `v1_interpreter`; audit F10). v2 has no execution path of its own. **This plan removes this one.** +2. **Compiler crutch** — the compiler binary is the v1 seed. Removing it is §1 self-hosting, a separate lane. Emit-on-demand deliberately RIDES the seed emitter (ROADMAP ④: *"emit a v2 closure to Rust via the seed"*) — the artifact is keyed by content hash, so WHICH emitter produced it is part of the **key**, never part of the architecture. + +The target pipeline, per witness run: + +``` +closure → ContentHash → artifact-store lookup + hit → run native → record receipt (wall + peak RSS, subject-keyed) + miss → resolve → emit (seed) → build (sccache-warm) → store → run → record +schedule = realize: min(independence_width, budget / measured_peak) [spine FLAG D] +``` + +## Economics (receipts: the 2026-07-14 whole-corpus Pi run, `.forensics/claim_full.log`) + +| Today (interpreted, v1) | Under this plan | +|---|---| +| resolve = 82.5 min, **87%** of the run; superlinear (fit exponent ~1.55 in closure size, 3.6× over linear) | paid once per content hash; a warm run pays source-hashing + exec | +| eval = 12.4 min tree-walked | native (S1 census receipt: compiled 1.1 ms linear vs interpreted DNF) | +| retention: VmSize 6.25 GB, ~8.4 MB/entry, never released; 13 GB swap to finish | per-run process frames (`ScopeExit` realized by process exit) + `SpacePacked` store budget | +| OOM = untyped exit 137; governor reactive (474 back-offs, "time death caused by a memory shape") | packing on measured peaks; unknown-peak subjects run in a width-1 maturation reserve | + +## The steps + +**P0 — the field wall (audit F1).** Field **presence** + field **type** checking in `04_infer`'s record-literal arm. Realization's scheduling facts (`CostAccount`, `CacheProvider`, receipts) are all record literals; while presence/types are unchecked, every downstream derive can read garbage at `0 diagnostics`. Staged like the wrapper-retained frontier: (i) ledger mode — typed, counted roster of corpus violations; (ii) drain; (iii) hard wall. ACCEPT: the audit's four probes go red; corpus green after drain. Every roster row found in (i) is a latent bug today. + +**P1 — space becomes observable (F2, F4).** `ObservePeakResidentAtSubject` as a second variant on `RealizationMeasureEffect`. The host physics **already exists unmodeled** — `claim_batch` reads `getrusage(RUSAGE_CHILDREN)` and prints `[measurement] children-max-rss` — so this is a mark-on-the-carrier step, not new physics. `PerformanceReceipt` gains the peak field. `space_measure_seq` = **max** / `space_measure_par` = **add** as peers of the time rules; the `fleet_intent.dag:168` sum fixed; the keystone witness flipped. ACCEPT: first `CostAccount.space` with `basis: Measured` produced by execution; RED: a seq-composition asserting sum goes red. + +**P2 — the artifact store: the corpus's first REAL `CacheProvider`.** `ArtifactKey = hash(closure source set, emitter id, target, toolchain)`. `ArtifactTier`/`ContentKeyed`, `SpacePacked{budget}` — and the store's budget enforcer is the first **reader** of `eviction` in the tree (F5). `ExistenceKeyed` unwritable by shape: the key *is* the hash; presence/mtime never consulted (#6352 wall, by construction this time). ACCEPT: put/get/evict receipts. REDs: source mutation → new key → miss (stale never served); budget breach → drop + **counted** recompute. + +**P3 — emit-on-demand v0 (ROADMAP §1's own accept criteria).** Wrap the landed `emit_host` transport (15 `emit_host_*_equals_eval` witnesses with REDs) with the P2 store. First customer per ROADMAP: the parse census / one witness family. ACCEPT: (a) interpreted==native agreement witness; (b) second-run zero-compile store-hit receipt; (c) the interpreter's surviving roles named + bounded. Needs FLAG A. + +**P4 — `realize` v0: the memory-packed scheduler.** Inputs: the runnable set; per-subject `CostAccount` (Measured from P1 receipts of prior runs; typed `CostUnknown` for first-timers); a **typed** host-budget read (unreadable → refuse — retiring `conservative_fallback_width`, the audit's live §5 finding). Law: `min(independence_width, budget/peak)` (spine FLAG D). Unknown-peak subjects run in a width-1 maturation reserve, then their receipt converts them — this is the `memory_governor`'s admission logic made predictive and modeled, and its dissolve-on (*"graph-derived per-node demand replaces the reactive estimator"*) finally fires. **ACCEPT on this Pi:** the whole hermetic corpus completes on 905 MB with flat VmSwap — the machine where memory-blind packing dies is the standing RED control. Exit-137 becomes a refusal class, not a death. + +**P5 — demands derived, not hand-typed.** `dependency_view` over the roster: N entries sharing a closure = plurality ≥2 across isolation → memo obligation at the LCA → discharged by the P2 provider. `materialize`'s `Share` verdict drives actual reuse for the first time; `materialization_carriers.dag:41`'s dissolve-on fires. ACCEPT: zero duplicate builds measured across a run. + +**P6 — cutover + falsifier; F10 cleared.** `SubstrateInputsOnly` witnesses route native. A nightly sampled interpreted==native falsifier (the affected-set-falsifier pattern) keeps the agreement honest. The interpreter is retained for compile-time eval + bootstrap receipts only, each a counted frontier row with its dissolution trigger. The v1-deletion ordering constraint dissolves correctly: eviction and scheduling authority now live in P2/P4 carriers, not in v1 Rust. + +**Horizon — verdict-level Share.** `TestClaimCacheKey` (`src/v2/compiler/05_eval.dag:925`) gets its store: a pure witness whose closure hash is unchanged makes the *run itself* a `Share`. Affected-set selection then becomes a derived special case of materialization instead of a parallel mechanism. + +## FLAGs (operator sign-off) + +- **FLAG A — hermetic admissibility of builds.** `emit_host_run_transport` refuses under hermetic mode today. Ruling needed: (1) a build from substrate-only inputs with a **pinned toolchain in the key** is a derived realization, admissible hermetically (recommended); or (2) builds happen only in a wet/record lane and hermetic runs consume the prebuilt store. +- **FLAG B — artifact granularity.** v0 = one binary per entry closure (simple; sccache dedups at the object level underneath). Module-grain shared artifacts come later, DERIVED by ladder plurality at module grain — not hand-chosen now. +- **FLAG C — C as a target.** C = authoring `extdeps/languages/c` rows (the §4 one-grammar-both-directions architecture keeps this open at constant price) **plus** a realization story for the `v1_rt`/persistent-carrier runtime — that second half is the real cost, and today it has zero displaced-cost justification. Rust is proven (census receipt). Defer until a pain names it (e.g. hosts where the Rust toolchain is prohibitive). + +## Non-goals + +GC / arena / bytecode VM / JIT (the design's standing rejection — correct, keep it). New interpreted-workload features. v1 emitter investment beyond what P3 consumes. From 44b596cdd65b3f8117fda375b8ae9d9333d88d58 Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Wed, 15 Jul 2026 00:18:01 -0400 Subject: [PATCH 03/28] Bind witness-realization plan into the doc graph (de-orphan; caught by #6654's restored wall) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reviewing gunbc#6654 in this branch's context proved its restored never-skip tooth by execution: doc_graph_has_no_orphan_docs ran RED here — the two plan docs this branch adds were a mutually-linked island unreachable from any root, exactly the class #6654's correction note describes (its own doc merged orphaned the same way under the false SubstrateInputsOnly stamp). Fix per #6654's staging precedent: one bind row in the most-related carrier — ci_floor_plan.dag, whose adaptive-width note's dissolve-on ("CostAccount.space measured replaces the reactive estimator") is precisely what the plan's P4 lands. The row reaches witness-realization-plan.md, which links the audit, so both docs are reachable from one bind. Receipts: doc_graph_has_no_orphan_docs false->true, doc_graph_has_no_dangling_links true, entry compile of the edited module 0 diagnostics. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v2/workflow/ci_floor_plan.dag | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 2f6d69edac0..20824b9aebe 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -222,6 +222,8 @@ fn corpus_source_roots() -> List { witness_layer_roots } +data witness_realization_plan_doc_provenance: String = "bind: docs/plans/witness-realization-plan.md — the staged path off the execution crutch (P0 field wall, P1 ObservePeakResidentAtSubject + space seq=max/par=add, P2 content-addressed artifact store, P4 realize packing min(width, budget/measured_peak)); its P4 is the adaptive-width note's own dissolve-on made concrete (graph-derived per-node demand from MeasuredBy receipts demotes the governor to a safety net). The plan links its companion audit (v2-memory-control-audit.md — space unobservable; eviction write-only; F10 v1-deletion ordering). Hand-authored staging bind per the doc-reachability wall (gunbc#6654 restored its never-skip tooth; that wall caught these very docs as orphans pre-merge, gunbc#6663); dissolves into a registered gunbc.plan.Plan row when P1 lands." + data gunbc_ci_adaptive_width_note: String = "Adaptive width (operator ruling 2026-07-12, superseding the pinned-cap regime): the plan no longer authors spawn widths or per-shard byte predictions — the retired machinery was gunbc_ci_corpus_discovery_spawn_width_cap (pinned 1 after the run 28999086030 width=2 OOM), the per-plan *_plan_spawn_width fns the executor evaluated by name, and the gunbc.ci_floor_measurement width folds over hand-edited peak samples (pins freezing derivations: stale samples predated the enrollment flip, and the base-overhead re-measure chased its own tail — the July OOM/wedge regime). The executor now governs concurrency at run time: v1_compiler::memory_governor admits workers AIMD-style against the slot's OWN declared budget (memory.high else memory.max else MemAvailable else MemTotal — MemAvailable precedes MemTotal on uncapped hosts because the kernel's availability estimate excludes the co-tenant baseline that let run 29180195694 reach physical RAM; GUNBC_MEMORY_BUDGET_BYTES to override). Admission is paced (at most one worker whose front-loaded index-build cost has not yet landed), predictive (the run measures its first worker's share over the pool baseline and admits only while current + share fits under high-water), and ceilinged at half the budget — the maturation reserve: the 2026-07-12 run series proved admitted demand matures minutes after admission at ~7x its digest-time footprint, so reactive arms alone always observe it too late and half the pipe stays reserved for in-flight growth. The creep-episode edge (memory.current high-water, PSI some avg10, swap growth) halves the window AND holds admissions — early congestion is TCP's ECN, not a stop-and-hope — while hard events halve it again (memory.events high/oom_kill deltas) and memory.current crossing the declared budget itself collapses the window to one (the reachable loss signal on uncapped hosts, where memory.events never fires); the width-1 progress floor still guarantees forward motion. The window re-grows additively on calm completions. Every hold/back-off is typed, counted, and surfaced in the [governor] receipt line (DESIGN §5: loud bounded degradation, never an absorbing widen). Dissolve-on: graph-derived per-node demand (CostAccount.space measured, the realization-measurement lane) replaces the reactive estimator and the governor demotes to a safety net." data gunbc_ci_fast_lane_rule_note: String = "Fast-lane 5-second rule (operator ruling 2026-07-12): a witness whose OWN eval takes 5 seconds or longer does not run in per-PR discovery — it lives under a long/ test dir (dag/test/claim/long/, src/v2/test/claim/long/), excluded from discovery at dir grain (gunbc.ci_layer_roots) and triggered independently (local recipe: claim_batch --source-root dag --source-root src/v2 --entry --functions ; scheduled-lane enrollment rides the falsifier follow-on). Enforcement is by execution, not census: the executor arms a cooperative per-witness eval deadline from the budget row below (v1_interpreter EvalBudgetExceeded — a typed FAIL row naming the over-budget witness; the bound unwinds from INSIDE eval because in-process worker threads have no kill authority, the Phase A governor lesson). The deadline arms at eval start, so resolve/index cost is infra and never counted against the witness (the operator's carve-out: 'assuming the infra isn't the problem'). This is also the wedge tourniquet: an unbounded eval that previously burned the 270-minute step cap in billed silence (run 29183446733: 243 of 270 minutes after the last progress line, zero witnesses completed) now fails red in seconds with its name in the log. Dissolve-on: per-witness declared cost envelopes (the witness-cost-locality admission law) replace the blanket lane budget with declared rows." From 6968b742154c377e76e021dc3349d58b6a6a0eaa Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Wed, 15 Jul 2026 01:01:59 -0400 Subject: [PATCH 04/28] P0 field wall (authority half): MissingField diagnostic + presence check + kernel-vs-declared type tier in infer_record_lit and direct call args MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit .dag authority edits only (generated .rs regen follows in the landing commit): - v1.std.core: MissingField { field, type_name, span } variant + span/message arms (auto-hard via the _ catch-alls in the blocking classifiers) - v1.compiler.infer: presence check in infer_record_lit — every declared field that is not CardOptional and carries no default must appear in the literal; missing -> MissingField at the literal's name_span, gated on a resolvable authority (tn_str nonempty, struct_fields nonempty) - v1.compiler.infer: kernel_value_declared_type_mismatch — a kernel-typed value (Int/String/Bool/Float/...) against a differently-named declared formal fires TypeMismatch unless dag_can_cast sanctions it; wired into BOTH the record-field arm (after the existing string-for-optional-coproduct reject, preserved byte-identical) and direct_call_arg_type_mismatch (calls get the same tier) Receipts: audit probes B/C/D classes (omitted eviction / eviction:42 / kernel-vs- nominal) — RED verification lands with the rebuilt binary; regen on the pre-merge base was surgical (95 written, 2 changed: v1_compiler_infer.rs +159, v1_std_core.rs +21). Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v1/00_core.dag | 3 ++ src/v1/04_infer.dag | 72 ++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 71 insertions(+), 4 deletions(-) diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index dff88253066..fe54acce78a 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -143,6 +143,7 @@ type CompilerDiagnostic | ArityMismatch { name: String, expected: Int, got: Int, span: SourceSpan } | VariantNotFound { variant: String, type_name: String, span: SourceSpan } | FieldNotFound { field: String, type_name: String, span: SourceSpan } + | MissingField { field: String, type_name: String, span: SourceSpan } | NonExhaustiveMatch { missing: List, span: SourceSpan } | CircularDependency { modules: List, span: SourceSpan } | DuplicateModule { name: String, span: SourceSpan } @@ -173,6 +174,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan { ArityMismatch { name: _, expected: _, got: _, span: s } => s VariantNotFound { variant: _, type_name: _, span: s } => s FieldNotFound { field: _, type_name: _, span: s } => s + MissingField { field: _, type_name: _, span: s } => s NonExhaustiveMatch { missing: _, span: s } => s CircularDependency { modules: _, span: s } => s DuplicateModule { name: _, span: s } => s @@ -196,6 +198,7 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String { ArityMismatch { name: n, expected: e, got: g, span: _ } => concat("type ", n, " expects ", to_string(value: e), " type arguments, got ", to_string(value: g)) VariantNotFound { variant: v, type_name: t, span: _ } => concat("variant '", v, "' not found in type '", t, "'") FieldNotFound { field: f, type_name: t, span: _ } => concat("field '", f, "' not found in type '", t, "'") + MissingField { field: f, type_name: t, span: _ } => concat("missing required field '", f, "' in literal of type '", t, "'") NonExhaustiveMatch { missing: ms, span: _ } => concat("non-exhaustive match: missing variant(s) ", join(ms, separator: ", ")) CircularDependency { modules: ms, span: _ } => concat("circular dependency detected: ", join(ms, separator: " -> ")) DuplicateModule { name: n, span: _ } => concat("duplicate module declaration: '", n, "'") diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index e4fa3eb2890..d31e63bd152 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -1,6 +1,6 @@ module v1.compiler.infer -import std.types { SourceSpan, container_param_name } +import std.types { SourceSpan, container_param_name, is_kernel_type } import std.coercion { dag_can_cast, is_dag_cast_domain_type } import v1.std.core { Node, InternTable, @@ -22,7 +22,7 @@ import v1.std.core { has_inferred, is_compiler_error, InferredNode, Resolved, CompilerError, TypeVariable, Cardinality, Required, CardOptional, ErrorNode, make_error_node, is_error_diagnostic, - InternalError, TypeMismatch, VariantCollision, SoleConstructorViolation, UnresolvedType, FieldNotFound, + InternalError, TypeMismatch, VariantCollision, SoleConstructorViolation, UnresolvedType, FieldNotFound, MissingField, resource_use_name_at, resource_use_resource, kernel_type_set, is_kernel_type, is_child_accessor_in_model, is_tree_size_reducing, is_property_contraction, @@ -738,6 +738,31 @@ fn nominal_call_arg_brand_mismatch(formal: Node, actual: Node, source_indices: M && !is_declared_container_alias_spelling(name: actual_name) } +fn kernel_value_declared_type_mismatch(formal: Node, actual: Node, type_env: TypeEnv, source_indices: Map) -> Bool { + if formal.connective == Arrow || actual.connective == Arrow || (actual.children |> count) > 0 { + false + } else { + let actual_name = authored_name_at(source_indices: source_indices, node: actual) + if is_kernel_type(name: actual_name) == false { + false + } else { + let formal_name = authored_name_at(source_indices: source_indices, node: formal) + if formal_name == "" || formal_name == actual_name || dag_can_cast(source_type: actual_name, target_type: formal_name) { + false + } else { + if is_kernel_type(name: formal_name) { + true + } else { + match lookup_type_by_name(env: type_env, name: formal_name) { + Present { value: decl } => (decl.connective == Conj || decl.connective == Disj) && (decl.children |> count) > 0 + Absent => false + } + } + } + } + } +} + fn container_element_nominal_brand_mismatch( formal: Node, actual: Node, @@ -776,6 +801,8 @@ fn direct_call_arg_type_mismatch( nominal_call_arg_brand_mismatch(formal: formal, actual: actual, source_indices: source_indices) || container_element_nominal_brand_mismatch( formal: formal, actual: actual, type_env: type_env, module_name: module_name, source_indices: source_indices) + || kernel_value_declared_type_mismatch( + formal: formal, actual: actual, type_env: type_env, source_indices: source_indices) } } @@ -2911,6 +2938,28 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa Present { value: tn } => tn Absent => "" } + let si_presence = scope.type_env.source_indices + let missing_field_diags = if tn_str == "" || (struct_fields |> count) == 0 { + [] + } else { + struct_fields + |> filter(sf => + let sf_type = match sf.inferred { + Present { value: Resolved { node: rt } } => rt + _ => field_node_type_expr(n: sf) + } + sf_type.return_cardinality != CardOptional + && sf.body == none + && (field_inits |> any(fi => field_init_node_name_at(n: fi, source_indices: si_presence) == authored_name_at(source_indices: si_presence, node: sf))) == false) + |> map(sf => make_error_node( + diagnostic: MissingField { + field: authored_name_at(source_indices: si_presence, node: sf), + type_name: tn_str, + span: name_span + }, + module_name: scope.module_name + )) + } let fi_infer_results = map(field_inits, fi => let fi_name = field_init_node_name_at(n: fi, source_indices: scope.type_env.source_indices) @@ -2957,7 +3006,22 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa module_name: scope.module_name )] } else { - [] + let expected_required = match lookup_type_for(env: scope.type_env, node: with_required_cardinality(n: expected_node)) { + Present { value: resolved } => resolved + Absent => with_required_cardinality(n: expected_node) + } + let formal_peeled = peel_nominal_alias_identity(n: expected_required, env: scope.type_env, module_name: scope.module_name) + let actual_peeled = peel_nominal_alias_identity(n: got_node, env: scope.type_env, module_name: scope.module_name) + if kernel_value_declared_type_mismatch(formal: formal_peeled, actual: actual_peeled, type_env: scope.type_env, source_indices: scope.type_env.source_indices) { + [type_mismatch_error( + expected: node_type_shape(n: formal_peeled, source_indices: scope.type_env.source_indices), + got: node_type_shape(n: actual_peeled, source_indices: scope.type_env.source_indices), + span: ar_typed.span, + module_name: scope.module_name + )] + } else { + [] + } } Absent => [] } @@ -3046,7 +3110,7 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa ) InferResult { typed: texpr, - diagnostics: concat(concat(fi_diags, type_diags), sole_ctor_diags) + diagnostics: concat(concat(concat(fi_diags, type_diags), sole_ctor_diags), missing_field_diags) } } } From 513a7b968a9b3181e50e61c305e714241d305059 Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Wed, 15 Jul 2026 11:35:32 -0400 Subject: [PATCH 05/28] P0 field wall: FP-class narrowings + regen sync + RED/GREEN witness suite Narrowings found by the closure-scoped ledger (56 -> 0 on the ladder closure): - presence trusts only real field authorities: record_lit_instantiated_fields (generic + annotation), direct non-generic Conj decl children, or the variant-owner path; the record_lit_alias_struct_fields fallback leaked a generic alias's TYPE ARGUMENTS as "fields" (52/56 of the first ledger: every Measure alias literal) - aliases now abstain - kernel tier unwraps where-refinements to their base before comparing (type NonEmptyStr = String where non_empty parses as an anonymous Conj with one child + type_annotation; String literals legitimately inhabit it, 4/56) and excludes equal structural-carrier templates (brands) Receipts (rebuilt binary, by execution): - complete CacheProvider literal: 0 diagnostics - eviction omitted: exactly 1 MissingField naming field + type - eviction: 42: exactly 1 TypeMismatch (Coproduct(EvictionClass) vs Primitive(Int)) - CostAccount missing 3/4: exactly 3 MissingField (generic instantiation path) - DependencyView kind:999: TypeMismatch + 3 MissingField - call args get the same tier: wants(e: 9) where e: Ev refuses - diagnostics_witness record_field_walls suite: 5 REDs + 3 GREENs (optional-field omission, dag_can_cast Int->Float, complete literal), exit 0 New suite registered in the diagnostics witness bin + transport row + claim test fn (diagnostics_record_field_walls_hold). Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/test/claim/diagnostics_test.dag | 5 + dag/tools/diagnostics_witness_transport.dag | 5 + src/v1/04_infer.dag | 33 ++- src/v1/stage0/src/bin/diagnostics_witness.rs | 139 ++++++++- src/v1/stage0/src/cli_run.rs | 288 ++++++++++--------- src/v1/stage0/src/compiler_tests.rs | 2 - src/v1/stage0/src/v1_compiler_infer.rs | 199 ++++++++++++- src/v1/stage0/src/v1_std_core.rs | 21 ++ 8 files changed, 536 insertions(+), 156 deletions(-) diff --git a/dag/test/claim/diagnostics_test.dag b/dag/test/claim/diagnostics_test.dag index 7edc7c62d31..aa610bb95f2 100644 --- a/dag/test/claim/diagnostics_test.dag +++ b/dag/test/claim/diagnostics_test.dag @@ -6,6 +6,7 @@ import tools.diagnostics_witness_transport { run_diagnostics_type_and_arity_witness, run_diagnostics_empty_list_context_witness, run_diagnostics_constructor_owner_witness, + run_diagnostics_record_field_walls_witness, } import std.logic { Bool } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -31,3 +32,7 @@ test fn diagnostics_empty_list_context_holds() -> Bool { test fn diagnostics_constructor_owner_walls_hold() -> Bool { run_diagnostics_constructor_owner_witness() } + +test fn diagnostics_record_field_walls_hold() -> Bool { + run_diagnostics_record_field_walls_witness() +} diff --git a/dag/tools/diagnostics_witness_transport.dag b/dag/tools/diagnostics_witness_transport.dag index e298297f7dd..155b59f21bf 100644 --- a/dag/tools/diagnostics_witness_transport.dag +++ b/dag/tools/diagnostics_witness_transport.dag @@ -8,6 +8,7 @@ data diagnostics_reexport_surface_suite: String = "reexport_surface" data diagnostics_type_and_arity_suite: String = "type_and_arity" data diagnostics_empty_list_context_suite: String = "empty_list_context" data diagnostics_constructor_owner_suite: String = "constructor_owner" +data diagnostics_record_field_walls_suite: String = "record_field_walls" fn run_diagnostics_suite(suite: String) -> Bool { run_witness_bin( @@ -36,3 +37,7 @@ fn run_diagnostics_empty_list_context_witness() -> Bool { fn run_diagnostics_constructor_owner_witness() -> Bool { run_diagnostics_suite(suite: diagnostics_constructor_owner_suite) } + +fn run_diagnostics_record_field_walls_witness() -> Bool { + run_diagnostics_suite(suite: diagnostics_record_field_walls_suite) +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 987cc8023e0..84a5960f53b 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -1,6 +1,6 @@ module v1.compiler.infer -import std.types { SourceSpan, container_param_name, is_kernel_type } +import std.types { SourceSpan, container_param_name } import std.coercion { dag_can_cast, is_dag_cast_domain_type } import v1.std.core { Node, InternTable, @@ -743,13 +743,21 @@ fn kernel_value_declared_type_mismatch(formal: Node, actual: Node, type_env: Typ if formal.connective == Arrow || actual.connective == Arrow || (actual.children |> count) > 0 { false } else { + let formal_base = if formal.connective == Conj && formal.type_annotation != none && (formal.children |> count) == 1 { + match formal.children |> first { + Present { value: refinement_base } => refinement_base + Absent => formal + } + } else { formal } let actual_name = authored_name_at(source_indices: source_indices, node: actual) if is_kernel_type(name: actual_name) == false { false } else { - let formal_name = authored_name_at(source_indices: source_indices, node: formal) + let formal_name = authored_name_at(source_indices: source_indices, node: formal_base) if formal_name == "" || formal_name == actual_name || dag_can_cast(source_type: actual_name, target_type: formal_name) { false + } else if structural_carrier_template_name(n: formal_base, source_indices: source_indices) == structural_carrier_template_name(n: actual, source_indices: source_indices) { + false } else { if is_kernel_type(name: formal_name) { true @@ -2940,10 +2948,27 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa Absent => "" } let si_presence = scope.type_env.source_indices - let missing_field_diags = if tn_str == "" || (struct_fields |> count) == 0 { + let presence_fields = if tn_str == "" { + [] + } else { + match record_lit_instantiated_fields(type_name: type_name, expected: expected, scope: scope) { + Present { value: inst_fields } => inst_fields + Absent => + match lookup_type_by_name(env: scope.type_env, name: tn_str) { + Present { value: decl } => + if decl.connective == Conj && (decl.params |> count) == 0 && (decl.children |> count) > 0 { + decl.children + } else { + [] + } + Absent => record_lit_expected_fields(type_name: type_name, scope: scope) + } + } + } + let missing_field_diags = if tn_str == "" || (presence_fields |> count) == 0 { [] } else { - struct_fields + presence_fields |> filter(sf => let sf_type = match sf.inferred { Present { value: Resolved { node: rt } } => rt diff --git a/src/v1/stage0/src/bin/diagnostics_witness.rs b/src/v1/stage0/src/bin/diagnostics_witness.rs index 46c315b8329..5322036cc29 100644 --- a/src/v1/stage0/src/bin/diagnostics_witness.rs +++ b/src/v1/stage0/src/bin/diagnostics_witness.rs @@ -26,6 +26,7 @@ const SUITE_REEXPORT_SURFACE: &str = "reexport_surface"; const SUITE_TYPE_AND_ARITY: &str = "type_and_arity"; const SUITE_EMPTY_LIST_CONTEXT: &str = "empty_list_context"; const SUITE_CONSTRUCTOR_OWNER: &str = "constructor_owner"; +const SUITE_RECORD_FIELD_WALLS: &str = "record_field_walls"; fn fail(msg: impl std::fmt::Display) -> ExitCode { eprintln!("diagnostics_witness: {msg}"); @@ -427,14 +428,150 @@ fn suite_cases(suite: &str) -> Result, String> { "constructor_owner_ruling_walls", constructor_owner_ruling_walls, )]), + SUITE_RECORD_FIELD_WALLS => Ok(vec![( + "record_literal_field_walls", + record_literal_field_walls, + )]), _ => Err(format!( "unknown suite '{suite}'; expected one of: {SUITE_IMPORT_RESOLUTION}, \ {SUITE_REEXPORT_SURFACE}, {SUITE_TYPE_AND_ARITY}, {SUITE_EMPTY_LIST_CONTEXT}, \ - {SUITE_CONSTRUCTOR_OWNER}" + {SUITE_CONSTRUCTOR_OWNER}, {SUITE_RECORD_FIELD_WALLS}" )), } } +/// P0 field walls (witness-realization plan P0 / memory-control audit F1): a record +/// literal must carry every required declared field (MissingField), and a kernel-typed +/// value cannot fill a differently-named declared formal (TypeMismatch) — in record +/// fields and direct call args alike. Greens pin the sanctioned skips: optional +/// fields and dag_can_cast pairs (Int->Float). +fn record_literal_field_walls(module_index: &ModuleIndex) { + // RED: omitted required field on a record literal + let missing = "module fieldwall_missing\n\ + type Ev = EvA | EvB { n: Int, m: Int }\n\ + type Prov { id: String, ev: Ev }\n\ + data p: Prov = Prov { id: \"x\" }\n"; + let missing_result = compile_multi(module_index, &[("fieldwall_missing.dag", missing)]); + let missing_diags: Vec<_> = missing_result + .diagnostics + .iter() + .filter(|d| matches!(&*d.diagnostic, CompilerDiagnostic::MissingField { .. })) + .collect(); + assert!( + !missing_diags.is_empty(), + "expected MissingField for omitted 'ev', got: {:?}", + diagnostic_messages(&missing_result) + ); + let missing_msg = diagnostic_to_message(missing_diags[0].diagnostic.clone()); + assert!(missing_msg.contains("ev"), "field name: {missing_msg}"); + assert!(missing_msg.contains("Prov"), "type name: {missing_msg}"); + + // RED: omitted required field on a coproduct-variant literal + let variant_missing = "module fieldwall_variant\n\ + type Ev = EvA | EvB { n: Int, m: Int }\n\ + data v: Ev = EvB { n: 1 }\n"; + let variant_result = compile_multi(module_index, &[("fieldwall_variant.dag", variant_missing)]); + let variant_diags: Vec<_> = variant_result + .diagnostics + .iter() + .filter(|d| matches!(&*d.diagnostic, CompilerDiagnostic::MissingField { .. })) + .collect(); + assert!( + !variant_diags.is_empty(), + "expected MissingField for omitted 'm' on variant literal, got: {:?}", + diagnostic_messages(&variant_result) + ); + + // RED: kernel value where a declared coproduct is expected (field) + let wrong_typed = "module fieldwall_wrongtype\n\ + type Ev = EvA | EvB { n: Int, m: Int }\n\ + type Prov { id: String, ev: Ev }\n\ + data q: Prov = Prov { id: \"x\", ev: 42 }\n"; + let wrong_result = compile_multi(module_index, &[("fieldwall_wrongtype.dag", wrong_typed)]); + let wrong_diags: Vec<_> = wrong_result + .diagnostics + .iter() + .filter(|d| matches!(&*d.diagnostic, CompilerDiagnostic::TypeMismatch { .. })) + .collect(); + assert!( + !wrong_diags.is_empty(), + "expected TypeMismatch for ev: 42, got: {:?}", + diagnostic_messages(&wrong_result) + ); + + // RED: kernel-vs-kernel mismatch (Int where String declared) + let kernel_kernel = "module fieldwall_kernel\n\ + type Prov2 { id: String }\n\ + data k: Prov2 = Prov2 { id: 7 }\n"; + let kernel_result = compile_multi(module_index, &[("fieldwall_kernel.dag", kernel_kernel)]); + assert!( + kernel_result + .diagnostics + .iter() + .any(|d| matches!(&*d.diagnostic, CompilerDiagnostic::TypeMismatch { .. })), + "expected TypeMismatch for id: 7 where String declared, got: {:?}", + diagnostic_messages(&kernel_result) + ); + + // RED: kernel value where a declared coproduct is expected (direct call arg) + let call_arg = "module fieldwall_callarg\n\ + type Ev = EvA | EvB { n: Int, m: Int }\n\ + fn wants(e: Ev) -> Int { 7 }\n\ + fn call_bad() -> Int { wants(e: 9) }\n"; + let call_result = compile_multi(module_index, &[("fieldwall_callarg.dag", call_arg)]); + assert!( + call_result + .diagnostics + .iter() + .any(|d| matches!(&*d.diagnostic, CompilerDiagnostic::TypeMismatch { .. })), + "expected TypeMismatch for wants(e: 9), got: {:?}", + diagnostic_messages(&call_result) + ); + + // GREEN: complete literal compiles with neither wall firing + let complete = "module fieldwall_green\n\ + type Ev = EvA | EvB { n: Int, m: Int }\n\ + type Prov { id: String, ev: Ev }\n\ + data g: Prov = Prov { id: \"x\", ev: EvA }\n"; + let complete_result = compile_multi(module_index, &[("fieldwall_green.dag", complete)]); + assert!( + !complete_result.diagnostics.iter().any(|d| matches!( + &*d.diagnostic, + CompilerDiagnostic::MissingField { .. } | CompilerDiagnostic::TypeMismatch { .. } + )), + "complete literal must stay green, got: {:?}", + diagnostic_messages(&complete_result) + ); + + // GREEN: optional field may be omitted + let optional = "module fieldwall_opt\n\ + type Opt { a: Int, b: Int? }\n\ + data o: Opt = Opt { a: 1 }\n"; + let optional_result = compile_multi(module_index, &[("fieldwall_opt.dag", optional)]); + assert!( + !optional_result + .diagnostics + .iter() + .any(|d| matches!(&*d.diagnostic, CompilerDiagnostic::MissingField { .. })), + "optional field omission must stay green, got: {:?}", + diagnostic_messages(&optional_result) + ); + + // GREEN: dag_can_cast pair (Int literal for Float field) is sanctioned + let cast_ok = "module fieldwall_cast\n\ + type Fl { x: Float }\n\ + data f: Fl = Fl { x: 3 }\n"; + let cast_result = compile_multi(module_index, &[("fieldwall_cast.dag", cast_ok)]); + assert!( + !cast_result + .diagnostics + .iter() + .any(|d| matches!(&*d.diagnostic, CompilerDiagnostic::TypeMismatch { .. })), + "Int-for-Float must stay green via dag_can_cast, got: {:?}", + diagnostic_messages(&cast_result) + ); +} + fn run_suite(module_index: &ModuleIndex, suite: &str) -> Result<(), String> { for (name, test) in suite_cases(suite)? { let index = module_index.clone(); diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 3f5d3c7f12c..1a414380cac 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -7470,8 +7470,7 @@ fn test_claim_selection_has_node_corpus( ]), "RoundTripClaim" => all_nodes(&[variant_field(ctx, fields, "input").expect("input")]), "DiagnosticClaim" => { - variant_field(ctx, fields, "input") - .is_some_and(|v| value_is_node(v, ctx)) + variant_field(ctx, fields, "input").is_some_and(|v| value_is_node(v, ctx)) } _ => false, } @@ -8794,157 +8793,160 @@ pub fn run_discovery_corpus_with_options( spawn_target_width, ); } - let queue: std::sync::Arc>>> = - std::sync::Arc::new(Mutex::new( - groups - .into_iter() - .map(|g| g.iter().map(|&i| rows[i].clone()).collect()) - .collect(), - )); - let abort = std::sync::Arc::new(AtomicBool::new(false)); - let source_roots_owned = source_roots.to_vec(); - let selection_for_workers = options.node_frontier_selection; - let fast_lane_budget_for_workers = options.fast_lane_eval_budget_ms; - let mut handles = Vec::new(); - let mut worker_ordinal: usize = 0; - loop { - if abort.load(Ordering::SeqCst) || queue.lock().unwrap().is_empty() { - break; - } - match governor.try_admit() { - crate::memory_governor::AdmitDecision::Admit { .. } => {} - crate::memory_governor::AdmitDecision::Hold(_) => { - std::thread::sleep(std::time::Duration::from_millis(150)); - continue; - } - } - let queue_for_worker = queue.clone(); - let abort_for_worker = abort.clone(); - let governor_for_worker = governor.clone(); - let roots = source_roots_owned.clone(); - let seeds = diff_edits.clone(); - let paths = changed_paths.clone(); - let keys = whole_tree_published_keys.clone(); - let spawn_target_width = governor.current_target_width(); - let cross_worker_store_for_worker = if spawn_target_width > 1 { - Some(cross_worker_store.clone()) - } else { - None - }; - if worker_ordinal == 0 && spawn_target_width <= 1 { - eprintln!( + let queue: std::sync::Arc>>> = + std::sync::Arc::new(Mutex::new( + groups + .into_iter() + .map(|g| g.iter().map(|&i| rows[i].clone()).collect()) + .collect(), + )); + let abort = std::sync::Arc::new(AtomicBool::new(false)); + let source_roots_owned = source_roots.to_vec(); + let selection_for_workers = options.node_frontier_selection; + let fast_lane_budget_for_workers = options.fast_lane_eval_budget_ms; + let mut handles = Vec::new(); + let mut worker_ordinal: usize = 0; + loop { + if abort.load(Ordering::SeqCst) || queue.lock().unwrap().is_empty() { + break; + } + match governor.try_admit() { + crate::memory_governor::AdmitDecision::Admit { .. } => {} + crate::memory_governor::AdmitDecision::Hold(_) => { + std::thread::sleep(std::time::Duration::from_millis(150)); + continue; + } + } + let queue_for_worker = queue.clone(); + let abort_for_worker = abort.clone(); + let governor_for_worker = governor.clone(); + let roots = source_roots_owned.clone(); + let seeds = diff_edits.clone(); + let paths = changed_paths.clone(); + let keys = whole_tree_published_keys.clone(); + let spawn_target_width = governor.current_target_width(); + let cross_worker_store_for_worker = if spawn_target_width > 1 { + Some(cross_worker_store.clone()) + } else { + None + }; + if worker_ordinal == 0 && spawn_target_width <= 1 { + eprintln!( "run_discovery_corpus: cross_worker_store withheld (governor target_width={spawn_target_width}) — per-index typed cache until width > 1" ); - } - // Narration style for this worker: shard_id = spawn ordinal (a stable hue in the - // interleaved stream); spawn-time target width > 1 shows the ▎shard tag — a width-1 - // admission window has no interleaving to disambiguate. - let style = ShardStyle { - shard_id: worker_ordinal, - shard_count: governor.current_target_width(), - color: floor_color, - stream: floor_stream, - }; - worker_ordinal += 1; - handles.push(std::thread::spawn( - move || -> Result, String> { - // The slot was granted by try_admit on the pump thread; the guard owns the - // matching release so a panicking worker cannot wedge admissions. - let mut slot = crate::memory_governor::AdmittedSlot::from_admitted( - governor_for_worker.clone(), - ); - // Process-scoped typed_module_cache when governor width > 1; private cold - // index at width=1 (CI budget — cross-worker-typecheck-share-design §7). - let index = match cross_worker_store_for_worker { - Some(store) => build_multi_entry_index_with_shared_caches(&roots, store), - None => build_multi_entry_index(&roots), + } + // Narration style for this worker: shard_id = spawn ordinal (a stable hue in the + // interleaved stream); spawn-time target width > 1 shows the ▎shard tag — a width-1 + // admission window has no interleaving to disambiguate. + let style = ShardStyle { + shard_id: worker_ordinal, + shard_count: governor.current_target_width(), + color: floor_color, + stream: floor_stream, }; - let runner = if selection_for_workers != NodeFrontierSelectionMode::Off { - match resolve_entry_with_index(&index, FLOOR_RUNNER_ENTRY) { - Ok((graph, source_indices)) => { - Some(make_eval_context(&graph, source_indices, execution_mode)) - } - Err(msg) => { - abort_for_worker.store(true, Ordering::SeqCst); - return Err(format!( - "floor runner resolve failed in worker ({msg}) — declared \ + worker_ordinal += 1; + handles.push(std::thread::spawn( + move || -> Result, String> { + // The slot was granted by try_admit on the pump thread; the guard owns the + // matching release so a panicking worker cannot wedge admissions. + let mut slot = crate::memory_governor::AdmittedSlot::from_admitted( + governor_for_worker.clone(), + ); + // Process-scoped typed_module_cache when governor width > 1; private cold + // index at width=1 (CI budget — cross-worker-typecheck-share-design §7). + let index = match cross_worker_store_for_worker { + Some(store) => { + build_multi_entry_index_with_shared_caches(&roots, store) + } + None => build_multi_entry_index(&roots), + }; + let runner = if selection_for_workers != NodeFrontierSelectionMode::Off { + match resolve_entry_with_index(&index, FLOOR_RUNNER_ENTRY) { + Ok((graph, source_indices)) => { + Some(make_eval_context(&graph, source_indices, execution_mode)) + } + Err(msg) => { + abort_for_worker.store(true, Ordering::SeqCst); + return Err(format!( + "floor runner resolve failed in worker ({msg}) — declared \ affected-set machinery must resolve; no silent \ run-everything fallback" - )); - } - } - } else { - None - }; - // The front-loaded admission cost (index build + runner resolve) has - // landed and is visible to the creep signals: unblock admission pacing. - slot.note_first_cost_paid(); - let mut worker_summaries = Vec::new(); - loop { - // Multiplicative decrease drains here: a worker between groups retires - // when concurrency sits above the (possibly just-halved) window. - if governor_for_worker.should_retire() - || abort_for_worker.load(Ordering::SeqCst) - { - break; - } - let Some(group_rows) = queue_for_worker.lock().unwrap().pop_front() else { - break; - }; - match run_discovery_rows( - &group_rows, - &index, - execution_mode, - selection_for_workers, - &paths, - &seeds, - runner.as_ref(), - keys.clone(), - fast_lane_budget_for_workers, - style, - ) { - Ok(summary) => { - worker_summaries.push(summary); - slot.note_unit_complete(); - } - Err(e) => { - abort_for_worker.store(true, Ordering::SeqCst); - return Err(e); + )); + } + } + } else { + None + }; + // The front-loaded admission cost (index build + runner resolve) has + // landed and is visible to the creep signals: unblock admission pacing. + slot.note_first_cost_paid(); + let mut worker_summaries = Vec::new(); + loop { + // Multiplicative decrease drains here: a worker between groups retires + // when concurrency sits above the (possibly just-halved) window. + if governor_for_worker.should_retire() + || abort_for_worker.load(Ordering::SeqCst) + { + break; + } + let Some(group_rows) = queue_for_worker.lock().unwrap().pop_front() + else { + break; + }; + match run_discovery_rows( + &group_rows, + &index, + execution_mode, + selection_for_workers, + &paths, + &seeds, + runner.as_ref(), + keys.clone(), + fast_lane_budget_for_workers, + style, + ) { + Ok(summary) => { + worker_summaries.push(summary); + slot.note_unit_complete(); + } + Err(e) => { + abort_for_worker.store(true, Ordering::SeqCst); + return Err(e); + } + } } - } + Ok(worker_summaries) + }, + )); + } + let mut summaries = Vec::new(); + let mut first_err: Option = None; + for handle in handles { + match handle + .join() + .map_err(|_| "discovery corpus worker thread panicked".to_string()) + { + Ok(Ok(worker_summaries)) => summaries.extend(worker_summaries), + Ok(Err(e)) | Err(e) => first_err = first_err.or(Some(e)), } - Ok(worker_summaries) - }, - )); - } - let mut summaries = Vec::new(); - let mut first_err: Option = None; - for handle in handles { - match handle - .join() - .map_err(|_| "discovery corpus worker thread panicked".to_string()) - { - Ok(Ok(worker_summaries)) => summaries.extend(worker_summaries), - Ok(Err(e)) | Err(e) => first_err = first_err.or(Some(e)), - } - } - if let Some(e) = first_err { - return Err(e); - } - // The pump exits when the queue is empty OR on abort; with no error the queue must be - // fully drained (workers only exit early on retire/abort, and the pump re-admits while - // items remain), so an undrained queue here is a scheduler bug — refuse, never under-run. - let leftover = queue.lock().unwrap().len(); - if leftover > 0 { - return Err(format!( + } + if let Some(e) = first_err { + return Err(e); + } + // The pump exits when the queue is empty OR on abort; with no error the queue must be + // fully drained (workers only exit early on retire/abort, and the pump re-admits while + // items remain), so an undrained queue here is a scheduler bug — refuse, never under-run. + let leftover = queue.lock().unwrap().len(); + if leftover > 0 { + return Err(format!( "adaptive discovery pool exited with {leftover} undrained entry-group(s) and no \ worker error — scheduler invariant violated; refusing a partial corpus" )); - } - Ok(attach_deferred_discovery_rows( - merge_discovery_summaries(summaries), - deferred_rows, - )) + } + Ok(attach_deferred_discovery_rows( + merge_discovery_summaries(summaries), + deferred_rows, + )) } }; } diff --git a/src/v1/stage0/src/compiler_tests.rs b/src/v1/stage0/src/compiler_tests.rs index deee0115cc1..1bb622a3dbf 100644 --- a/src/v1/stage0/src/compiler_tests.rs +++ b/src/v1/stage0/src/compiler_tests.rs @@ -1737,7 +1737,6 @@ mod compiler_tests { source_indices.clone(), intern_table.clone(), std::rc::Rc::new(HashMap::new()), - crate::v1_compiler_infer_env::empty_symbol_index(), ); let env_elapsed = t_env.elapsed(); let rss_after_env = get_rss_bytes(); @@ -1776,7 +1775,6 @@ mod compiler_tests { source_indices.clone(), intern_table.clone(), std::rc::Rc::new(HashMap::new()), - crate::v1_compiler_infer_env::empty_symbol_index(), ); let full_elapsed = t_full.elapsed(); let rss_after = get_rss_bytes(); diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index e5924727516..500c597f9e1 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -120,8 +120,8 @@ use crate::v1_rt::{VecCompat, VecJoin}; use crate::v1_std_core::CallSemantics::{LookupCallSemantics, PlainCallSemantics}; use crate::v1_std_core::Cardinality::{CardOptional, Required}; use crate::v1_std_core::CompilerDiagnostic::{ - FieldNotFound, InternalError, SoleConstructorViolation, TypeMismatch, UnresolvedType, - VariantCollision, + FieldNotFound, InternalError, MissingField, SoleConstructorViolation, TypeMismatch, + UnresolvedType, VariantCollision, }; use crate::v1_std_core::Connective::{Arrow, Conj, Disj, NoConnective}; use crate::v1_std_core::ExprData::{ @@ -1262,6 +1262,71 @@ pub fn nominal_call_arg_brand_mismatch( } } +pub fn kernel_value_declared_type_mismatch( + formal: Rc, + actual: Rc, + type_env: Rc, + source_indices: Rc>>, +) -> bool { + if (((formal.connective.clone() == Connective::Arrow) + || (actual.connective.clone() == Connective::Arrow)) + || ((actual.children.clone().len() as i64) > 0)) + { + false + } else { + { + let formal_base = if (((formal.connective.clone() == Connective::Conj) + && (formal.type_annotation.clone() != None)) + && ((formal.children.clone().len() as i64) == 1)) + { + match formal.children.clone().first().cloned() { + Some(refinement_base) => refinement_base.clone(), + None => formal.clone(), + } + } else { + formal.clone() + }; + let actual_name = authored_name_at(source_indices.clone(), actual.clone()); + if (is_kernel_type(actual_name.clone()) == false) { + false + } else { + { + let formal_name = authored_name_at(source_indices.clone(), formal_base.clone()); + if (((formal_name.clone() == "".to_string()) + || (formal_name.clone() == actual_name.clone())) + || dag_can_cast(actual_name.clone(), formal_name.clone())) + { + false + } else { + if (structural_carrier_template_name( + formal_base.clone(), + source_indices.clone(), + ) == structural_carrier_template_name( + actual.clone(), + source_indices.clone(), + )) { + false + } else { + if is_kernel_type(formal_name.clone()) { + true + } else { + match lookup_type_by_name(type_env.clone(), formal_name.clone()) { + Some(decl) => { + (((decl.connective.clone() == Connective::Conj) + || (decl.connective.clone() == Connective::Disj)) + && ((decl.children.clone().len() as i64) > 0)) + } + None => false, + } + } + } + } + } + } + } + } +} + pub fn container_element_nominal_brand_mismatch( formal: Rc, actual: Rc, @@ -1312,7 +1377,7 @@ pub fn direct_call_arg_type_mismatch( if (type_node_is_callable(formal.clone()) || type_node_is_callable(actual.clone())) { false } else { - (nominal_call_arg_brand_mismatch(formal.clone(), actual.clone(), source_indices.clone()) + ((nominal_call_arg_brand_mismatch(formal.clone(), actual.clone(), source_indices.clone()) || container_element_nominal_brand_mismatch( formal.clone(), actual.clone(), @@ -1320,6 +1385,12 @@ pub fn direct_call_arg_type_mismatch( module_name.clone(), source_indices.clone(), )) + || kernel_value_declared_type_mismatch( + formal.clone(), + actual.clone(), + type_env.clone(), + source_indices.clone(), + )) } } @@ -5870,6 +5941,80 @@ pub fn infer_record_lit( Some(tn) => tn.clone(), None => "".to_string(), }; + let si_presence = scope.type_env.clone().source_indices.clone(); + let presence_fields = if (tn_str.clone() == "".to_string()) { + Rc::new(vec![]) + } else { + match record_lit_instantiated_fields(type_name.clone(), expected.clone(), scope.clone()) + { + Some(inst_fields) => inst_fields.clone(), + None => match lookup_type_by_name(scope.type_env.clone(), tn_str.clone()) { + Some(decl) => { + if (((decl.connective.clone() == Connective::Conj) + && ((decl.params.clone().len() as i64) == 0)) + && ((decl.children.clone().len() as i64) > 0)) + { + decl.children.clone() + } else { + Rc::new(vec![]) + } + } + None => record_lit_expected_fields(type_name.clone(), scope.clone()), + }, + } + }; + let missing_field_diags = if ((tn_str.clone() == "".to_string()) + || ((presence_fields.clone().len() as i64) == 0)) + { + Rc::new(vec![]) + } else { + Rc::new({ + let mut __result = Vec::new(); + for sf in Rc::new({ + let mut __result = Vec::new(); + for sf in presence_fields.clone().iter().cloned() { + if { + let sf_type = match sf.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { node: rt, .. }) => rt.clone(), + _ => field_node_type_expr(sf.clone()), + }; + (((sf_type.return_cardinality.clone() != Cardinality::CardOptional) + && (sf.body.clone() == None)) + && ({ + let mut __found = false; + for fi in field_inits.clone().iter().cloned() { + if (field_init_node_name_at( + fi.clone(), + si_presence.clone(), + ) == authored_name_at(si_presence.clone(), sf.clone())) + { + __found = true; + break; + } + } + __found + } == false)) + } { + __result.push(sf); + } + } + __result + }) + .iter() + .cloned() + { + __result.push(make_error_node( + Rc::new(CompilerDiagnostic::MissingField { + field: authored_name_at(si_presence.clone(), sf.clone()), + type_name: tn_str.clone(), + span: name_span.clone(), + }), + scope.module_name.clone(), + )); + } + __result + }) + }; let fi_infer_results = Rc::new({ let mut __result = Vec::new(); for fi in field_inits.clone().iter().cloned() { @@ -5981,7 +6126,46 @@ pub fn infer_record_lit( )]) } } else { - Rc::new(vec![]) + { + let expected_required = match lookup_type_for( + scope.type_env.clone(), + with_required_cardinality(expected_node.clone()), + ) { + Some(resolved) => resolved.clone(), + None => with_required_cardinality(expected_node.clone()), + }; + let formal_peeled = peel_nominal_alias_identity( + expected_required.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + let actual_peeled = peel_nominal_alias_identity( + got_node.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + if kernel_value_declared_type_mismatch( + formal_peeled.clone(), + actual_peeled.clone(), + scope.type_env.clone(), + scope.type_env.clone().source_indices.clone(), + ) { + Rc::new(vec![type_mismatch_error( + node_type_shape( + formal_peeled.clone(), + scope.type_env.clone().source_indices.clone(), + ), + node_type_shape( + actual_peeled.clone(), + scope.type_env.clone().source_indices.clone(), + ), + ar_typed.span.clone(), + scope.module_name.clone(), + )]) + } else { + Rc::new(vec![]) + } + } } } None => Rc::new(vec![]), @@ -6190,8 +6374,11 @@ pub fn infer_record_lit( Rc::new(InferResult { typed: texpr.clone(), diagnostics: v1_rt::concat( - v1_rt::concat(fi_diags.clone(), type_diags.clone()), - sole_ctor_diags.clone(), + v1_rt::concat( + v1_rt::concat(fi_diags.clone(), type_diags.clone()), + sole_ctor_diags.clone(), + ), + missing_field_diags.clone(), ), }) } diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index 80053cc31bc..a7707b74b8c 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -384,6 +384,11 @@ pub enum CompilerDiagnostic { type_name: String, span: Rc, }, + MissingField { + field: String, + type_name: String, + span: Rc, + }, NonExhaustiveMatch { missing: Rc>, span: Rc, @@ -445,6 +450,7 @@ impl CompilerDiagnostic { CompilerDiagnostic::ArityMismatch { span: __val, .. } => __val.clone(), CompilerDiagnostic::VariantNotFound { span: __val, .. } => __val.clone(), CompilerDiagnostic::FieldNotFound { span: __val, .. } => __val.clone(), + CompilerDiagnostic::MissingField { span: __val, .. } => __val.clone(), CompilerDiagnostic::NonExhaustiveMatch { span: __val, .. } => __val.clone(), CompilerDiagnostic::CircularDependency { span: __val, .. } => __val.clone(), CompilerDiagnostic::DuplicateModule { span: __val, .. } => __val.clone(), @@ -480,6 +486,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { CompilerDiagnostic::ArityMismatch { span: s, .. } => s.clone(), CompilerDiagnostic::VariantNotFound { span: s, .. } => s.clone(), CompilerDiagnostic::FieldNotFound { span: s, .. } => s.clone(), + CompilerDiagnostic::MissingField { span: s, .. } => s.clone(), CompilerDiagnostic::NonExhaustiveMatch { span: s, .. } => s.clone(), CompilerDiagnostic::CircularDependency { span: s, .. } => s.clone(), CompilerDiagnostic::DuplicateModule { span: s, .. } => s.clone(), @@ -595,6 +602,20 @@ pub fn diagnostic_to_message(d: Rc) -> String { ), "'".to_string(), ), + CompilerDiagnostic::MissingField { + field: f, + type_name: t, + .. + } => v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat("missing required field '".to_string(), f.clone()), + "' in literal of type '".to_string(), + ), + t.clone(), + ), + "'".to_string(), + ), CompilerDiagnostic::NonExhaustiveMatch { missing: ms, .. } => v1_rt::concat( "non-exhaustive match: missing variant(s) ".to_string(), ms.clone().join(&", ".to_string()), From b13be208ceb6d0ce52500bd9b295e7b3a9d72449 Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Wed, 15 Jul 2026 13:17:41 -0400 Subject: [PATCH 06/28] P0 field wall: whole-tree ledger 568 -> 45 (three FP classes dissolved) Round-1 whole-tree ledger: 568. Three classes root-caused and dissolved: - none-sentinel: `none` into optional coproduct fields infers as Unit (462/568). Unit excluded from the kernel tier - the Value::Null/Absent grounding is its own open thread (DESIGN model-realization fork note); firing there would be an error arm where grounding is owed. - refinement-decl misclassification: `type X = String where p` decls read as records by the final arm when the call path's substitution strips the annotation; excluded via refinement-over-actual shape test. - homonym variants: flat lookup_type_by_name resolved openai's FunctionCall TYPE for github/expressions' FunctionCall VARIANT literals; presence now consults variant_owner_node first - the same disambiguator that stamps parent_enum, so presence agrees with what the literal BECOMES. Round-2 residue: 45 counted rows (roster: .forensics/p0_drain_roster.txt, local), awaiting drain + three operator rulings: 1. `discriminant(v: X {})` empty-literal tag-reference idiom (16+ sites, src/v2/std/compilers/target_model.dag) - sanction zero-field literals as tag references, or mint a first-class variant-tag carrier? 2. String literal into a Secret field (filesystem_write_closure_scale_witness) - fix the test, or is a String->Secret construction sanctioned anywhere? 3. `Coproduct(FreeMonoid)` vs String (01_tokenize) - if String grounds FreeMonoid, the escape is a dag_cast_rules row, not a source edit. Genuine partial-literal TPs confirmed: RunnableDiscoveryBatch witnesses omit exclude_substrings + discovery_scope_dirs (eval null-fills today); plus MarkdownSpellings/OrderingComparison/EqualityComparison/etc. rows. Probes and the record_field_walls suite stay green through all three fixes. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v1/04_infer.dag | 37 +++++++++----- src/v1/stage0/src/v1_compiler_infer.rs | 67 ++++++++++++++++++++------ 2 files changed, 78 insertions(+), 26 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 84a5960f53b..c54293360a7 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -750,7 +750,7 @@ fn kernel_value_declared_type_mismatch(formal: Node, actual: Node, type_env: Typ } } else { formal } let actual_name = authored_name_at(source_indices: source_indices, node: actual) - if is_kernel_type(name: actual_name) == false { + if is_kernel_type(name: actual_name) == false || actual_name == "Unit" { false } else { let formal_name = authored_name_at(source_indices: source_indices, node: formal_base) @@ -763,7 +763,14 @@ fn kernel_value_declared_type_mismatch(formal: Node, actual: Node, type_env: Typ true } else { match lookup_type_by_name(env: type_env, name: formal_name) { - Present { value: decl } => (decl.connective == Conj || decl.connective == Disj) && (decl.children |> count) > 0 + Present { value: decl } => + let decl_is_refinement_over_actual = decl.connective == Conj && (decl.children |> count) == 1 + && (decl.type_annotation != none + || (match decl.children |> first { + Present { value: refinement_child } => authored_name_at(source_indices: source_indices, node: refinement_child) == actual_name + Absent => false + })) + (decl.connective == Conj || decl.connective == Disj) && (decl.children |> count) > 0 && decl_is_refinement_over_actual == false Absent => false } } @@ -2951,17 +2958,25 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa let presence_fields = if tn_str == "" { [] } else { - match record_lit_instantiated_fields(type_name: type_name, expected: expected, scope: scope) { - Present { value: inst_fields } => inst_fields + match variant_owner_node(scope: scope, name: tn_str) { + Present { value: variant_owner } => + match variant_owner.children |> filter(v => authored_name_at(source_indices: si_presence, node: v) == tn_str) |> first { + Present { value: variant_node } => variant_node.children + Absent => [] + } Absent => - match lookup_type_by_name(env: scope.type_env, name: tn_str) { - Present { value: decl } => - if decl.connective == Conj && (decl.params |> count) == 0 && (decl.children |> count) > 0 { - decl.children - } else { - [] + match record_lit_instantiated_fields(type_name: type_name, expected: expected, scope: scope) { + Present { value: inst_fields } => inst_fields + Absent => + match lookup_type_by_name(env: scope.type_env, name: tn_str) { + Present { value: decl } => + if decl.connective == Conj && (decl.params |> count) == 0 && (decl.children |> count) > 0 { + decl.children + } else { + [] + } + Absent => record_lit_expected_fields(type_name: type_name, scope: scope) } - Absent => record_lit_expected_fields(type_name: type_name, scope: scope) } } } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 500c597f9e1..e6b241c8841 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -1287,7 +1287,9 @@ pub fn kernel_value_declared_type_mismatch( formal.clone() }; let actual_name = authored_name_at(source_indices.clone(), actual.clone()); - if (is_kernel_type(actual_name.clone()) == false) { + if ((is_kernel_type(actual_name.clone()) == false) + || (actual_name.clone() == "Unit".to_string())) + { false } else { { @@ -1312,9 +1314,24 @@ pub fn kernel_value_declared_type_mismatch( } else { match lookup_type_by_name(type_env.clone(), formal_name.clone()) { Some(decl) => { - (((decl.connective.clone() == Connective::Conj) + let decl_is_refinement_over_actual = + (((decl.connective.clone() == Connective::Conj) + && ((decl.children.clone().len() as i64) == 1)) + && ((decl.type_annotation.clone() != None) + || match decl.children.clone().first().cloned() + { + Some(refinement_child) => { + (authored_name_at( + source_indices.clone(), + refinement_child.clone(), + ) == actual_name.clone()) + } + None => false, + })); + ((((decl.connective.clone() == Connective::Conj) || (decl.connective.clone() == Connective::Disj)) && ((decl.children.clone().len() as i64) > 0)) + && (decl_is_refinement_over_actual.clone() == false)) } None => false, } @@ -5945,21 +5962,41 @@ pub fn infer_record_lit( let presence_fields = if (tn_str.clone() == "".to_string()) { Rc::new(vec![]) } else { - match record_lit_instantiated_fields(type_name.clone(), expected.clone(), scope.clone()) - { - Some(inst_fields) => inst_fields.clone(), - None => match lookup_type_by_name(scope.type_env.clone(), tn_str.clone()) { - Some(decl) => { - if (((decl.connective.clone() == Connective::Conj) - && ((decl.params.clone().len() as i64) == 0)) - && ((decl.children.clone().len() as i64) > 0)) - { - decl.children.clone() - } else { - Rc::new(vec![]) + match variant_owner_node(scope.clone(), tn_str.clone()) { + Some(variant_owner) => match Rc::new({ + let mut __result = Vec::new(); + for v in variant_owner.children.clone().iter().cloned() { + if (authored_name_at(si_presence.clone(), v.clone()) == tn_str.clone()) { + __result.push(v); } } - None => record_lit_expected_fields(type_name.clone(), scope.clone()), + __result + }) + .first() + .cloned() + { + Some(variant_node) => variant_node.children.clone(), + None => Rc::new(vec![]), + }, + None => match record_lit_instantiated_fields( + type_name.clone(), + expected.clone(), + scope.clone(), + ) { + Some(inst_fields) => inst_fields.clone(), + None => match lookup_type_by_name(scope.type_env.clone(), tn_str.clone()) { + Some(decl) => { + if (((decl.connective.clone() == Connective::Conj) + && ((decl.params.clone().len() as i64) == 0)) + && ((decl.children.clone().len() as i64) > 0)) + { + decl.children.clone() + } else { + Rc::new(vec![]) + } + } + None => record_lit_expected_fields(type_name.clone(), scope.clone()), + }, }, } }; From 5e8cd86eba32cdd110956b08eb902bf651771834 Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Wed, 15 Jul 2026 13:24:30 -0400 Subject: [PATCH 07/28] P0 status + three open operator rulings recorded in the plan doc The rulings block the final ~25-row drain; recorded with sites, options, and recommendations so the lane is resumable from the doc alone. Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/plans/witness-realization-plan.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/docs/plans/witness-realization-plan.md b/docs/plans/witness-realization-plan.md index 12a3365133b..40468ef59ef 100644 --- a/docs/plans/witness-realization-plan.md +++ b/docs/plans/witness-realization-plan.md @@ -31,6 +31,15 @@ schedule = realize: min(independence_width, budget / measured_peak) [spine FLA **P0 — the field wall (audit F1).** Field **presence** + field **type** checking in `04_infer`'s record-literal arm. Realization's scheduling facts (`CostAccount`, `CacheProvider`, receipts) are all record literals; while presence/types are unchecked, every downstream derive can read garbage at `0 diagnostics`. Staged like the wrapper-retained frontier: (i) ledger mode — typed, counted roster of corpus violations; (ii) drain; (iii) hard wall. ACCEPT: the audit's four probes go red; corpus green after drain. Every roster row found in (i) is a latent bug today. +> **P0 STATUS (2026-07-15, session lively-heron-614 — commits `6968b7421`, `513a7b968`, `b13be208c`):** wall LANDED in the v1 authority (`src/v1/04_infer.dag`: presence via trusted field authorities only; `kernel_value_declared_type_mismatch` tier wired into record fields AND `direct_call_arg_type_mismatch`; new `MissingField` diagnostic in `v1.std.core`). All four audit probes RED with located diagnostics; `diagnostics_witness record_field_walls` suite (5 REDs + 3 GREENs) green; whole-tree ledger **568 → 45** after three FP classes dissolved by root cause (none-sentinel `Unit` ×462 — excluded pending the `Value::Null` grounding thread; refinement-decl misclassification; homonym variants — presence now consults `variant_owner_node` first, agreeing with `parent_enum` stamping). Wall already caught real rot: `RunnableDiscoveryBatch` witness literals omit `exclude_substrings`/`discovery_scope_dirs` (eval null-fills today). +> +> **BLOCKED on three operator rulings** (then ~25 rows drain mechanically; roster = round-2 whole-tree ledger, reproduce with `gunbc compile --source-root dag --source-root src/v2 --target dag`): +> 1. **Empty-literal tag idiom** — `discriminant(v: PrefixToken {})`, 16+ sites in `src/v2/std/compilers/target_model.dag`: (a) sanction zero-field literals as tag references (named exemption, dissolve-on = a first-class variant-tag carrier; partial literals stay red) — RECOMMENDED; or (b) mint the tag carrier now and migrate the sites. +> 2. **String into a `Secret` field** — `dag/test/claim/filesystem_write_closure_scale_witness.dag:302`: (a) fix the test via the sanctioned Secret constructor (RECOMMENDED — name it); (b) a `String→Secret` cast row would gut the type. +> 3. **String vs `Coproduct(FreeMonoid)`** — `src/v2/compiler/01_tokenize.dag:2875`: the text-duality question. (a) if String grounds `FreeMonoid` (the Nat/Int pattern applied to text), add `{from_type: "String", to_type: "FreeMonoid"}` to `dag_cast_rules` — one row in the modeled authority; (b) if `FreeMonoid` stays structural, fix the site. Genuinely the operator's modeling call. +> +> Also in the residue: a probable real bug — `Primitive(Bool)` into a `FreeMonoid` container (`dag/gunbc/tools/card_intake.dag:5890`) — and partial-literal TPs in `fleet_converge_emit_test` (7), `MarkdownSpellings`, `OrderingComparison`/`EqualityComparison`, `AlgebraInverseCompose`/`AlgebraPrimitive`, `MethodIdent`/`CallIdent`, `live_deploy/emit`, `seed_debt_bundle_item_2_floor_scope`. + **P1 — space becomes observable (F2, F4).** `ObservePeakResidentAtSubject` as a second variant on `RealizationMeasureEffect`. The host physics **already exists unmodeled** — `claim_batch` reads `getrusage(RUSAGE_CHILDREN)` and prints `[measurement] children-max-rss` — so this is a mark-on-the-carrier step, not new physics. `PerformanceReceipt` gains the peak field. `space_measure_seq` = **max** / `space_measure_par` = **add** as peers of the time rules; the `fleet_intent.dag:168` sum fixed; the keystone witness flipped. ACCEPT: first `CostAccount.space` with `basis: Measured` produced by execution; RED: a seq-composition asserting sum goes red. **P2 — the artifact store: the corpus's first REAL `CacheProvider`.** `ArtifactKey = hash(closure source set, emitter id, target, toolchain)`. `ArtifactTier`/`ContentKeyed`, `SpacePacked{budget}` — and the store's budget enforcer is the first **reader** of `eviction` in the tree (F5). `ExistenceKeyed` unwritable by shape: the key *is* the hash; presence/mtime never consulted (#6352 wall, by construction this time). ACCEPT: put/get/evict receipts. REDs: source mutation → new key → miss (stale never served); budget breach → drop + **counted** recompute. From 50c11865a0565e046d64abd0a7c96d7c77e80abf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 17:36:42 +0000 Subject: [PATCH 08/28] WIP: v2 memory control audit --- src/v1/stage0/src/compiler_tests.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/v1/stage0/src/compiler_tests.rs b/src/v1/stage0/src/compiler_tests.rs index 1bb622a3dbf..deee0115cc1 100644 --- a/src/v1/stage0/src/compiler_tests.rs +++ b/src/v1/stage0/src/compiler_tests.rs @@ -1737,6 +1737,7 @@ mod compiler_tests { source_indices.clone(), intern_table.clone(), std::rc::Rc::new(HashMap::new()), + crate::v1_compiler_infer_env::empty_symbol_index(), ); let env_elapsed = t_env.elapsed(); let rss_after_env = get_rss_bytes(); @@ -1775,6 +1776,7 @@ mod compiler_tests { source_indices.clone(), intern_table.clone(), std::rc::Rc::new(HashMap::new()), + crate::v1_compiler_infer_env::empty_symbol_index(), ); let full_elapsed = t_full.elapsed(); let rss_after = get_rss_bytes(); From b4c45eef068eaf231791f7ad545b94ed0cc9505e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 18:38:18 +0000 Subject: [PATCH 09/28] WIP: v2 memory control audit --- src/v1/04_infer.dag | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index d2864a2efa7..3f5758b5352 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2923,6 +2923,8 @@ fn type_has_sole_constructor(type_name: String, scope: InferScope) -> Bool { } } +data zero_field_variant_tag_reference_frontier_note: String = "P0 field-wall frontier (operator Ruling 1a, 2026-07-15): a ZERO-field literal of a coproduct VARIANT (field_inits empty AND variant_owner_node != none) is sanctioned as a TAG REFERENCE, not a construction — the `discriminant(v: PrefixToken {})` idiom (16+ sites in src/v2/std/compilers/target_model.dag) names a variant to obtain its stable tag identity without materializing a value. Presence checking is skipped for exactly this shape; PARTIAL literals (any field present) stay red, and zero-field literals of NON-variant records (variant_owner_node == none) stay red — so the audit F1 probes (CacheProvider/CostAccount partial literals) are unaffected. This is a decidable structural exemption (not an absorbing fallback: it refuses precisely, never widens on failure). DISSOLVE-ON: a first-class variant-tag carrier that types the discriminant argument position, at which point the exemption is deleted and the sites migrate to the carrier." + fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpan, name_span: SourceSpan, scope: InferScope, expected: Node?) -> InferResult { let struct_fields = match type_name { Present { value: tn } => @@ -2986,7 +2988,9 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa } } } - let missing_field_diags = if tn_str == "" || (presence_fields |> count) == 0 { + let is_zero_field_variant_tag_reference = (field_inits |> count) == 0 + && variant_owner_node(scope: scope, name: tn_str) != none + let missing_field_diags = if tn_str == "" || (presence_fields |> count) == 0 || is_zero_field_variant_tag_reference { [] } else { presence_fields From a3e13c6d44e7b0833cf87d1a5d1b423dc777fbf8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 18:48:48 +0000 Subject: [PATCH 10/28] WIP: v2 memory control audit --- dag/std/coercion.dag | 14 +++++---- ...filesystem_write_closure_scale_witness.dag | 2 +- dag/test/claim/markdown_roundtrip_test.dag | 1 + dag/test/claim/markdown_source_emit_test.dag | 1 + .../realization_schedule_witness_test.dag | 2 ++ ...runnable_resource_profile_witness_test.dag | 2 ++ .../seed_debt_bundle_item_2_floor_scope.dag | 8 +++-- src/v2/extdeps/languages/dag.dag | 3 +- src/v2/workflow/ci_floor_plan.dag | 29 ++++++++++--------- 9 files changed, 40 insertions(+), 22 deletions(-) diff --git a/dag/std/coercion.dag b/dag/std/coercion.dag index efad350bf83..c9f33807a16 100644 --- a/dag/std/coercion.dag +++ b/dag/std/coercion.dag @@ -34,12 +34,16 @@ type CastSyntax { cast_rules: List } +data grounded_primitive_coproduct_cast_note: String = "The Int->Nat and String->FreeMonoid rows are GROUNDED identities, not hollow casts (operator Ruling 3, 2026-07-15): a Nat IS an Int (numeric tower grounded construction-side #5428, Zero->Int(0)/Succ->Int(k+1), native form == modeled form) and a String IS a FreeMonoid (std.string_type: type String = FreeMonoid — strings over an alphabet are the free monoid). So an Int literal where a Nat is expected, and a String literal where a FreeMonoid is expected, are the same value at the kernel level; the wall's kernel_value_declared_type_mismatch consults dag_can_cast and correctly stops flagging them. NON-grounded primitive->coproduct straddles stay red by construction: Bool->FreeMonoid (card_intake), String->Doc (live_deploy), String->AuthScheme (auth) are genuine site bugs with no cast row." + data dag_cast_rules: List = [ - { from_type: "Int", to_type: "Int" }, - { from_type: "Int", to_type: "Float" }, - { from_type: "Float", to_type: "Int" }, - { from_type: "Float", to_type: "Float" }, - { from_type: "Bool", to_type: "Int" }, + { from_type: "Int", to_type: "Int" }, + { from_type: "Int", to_type: "Float" }, + { from_type: "Float", to_type: "Int" }, + { from_type: "Float", to_type: "Float" }, + { from_type: "Bool", to_type: "Int" }, + { from_type: "Int", to_type: "Nat" }, + { from_type: "String", to_type: "FreeMonoid" }, ] fn dag_can_cast(source_type: String, target_type: String) -> Bool { diff --git a/dag/test/claim/filesystem_write_closure_scale_witness.dag b/dag/test/claim/filesystem_write_closure_scale_witness.dag index c23fc859d45..0c7d8095f8d 100644 --- a/dag/test/claim/filesystem_write_closure_scale_witness.dag +++ b/dag/test/claim/filesystem_write_closure_scale_witness.dag @@ -7,7 +7,7 @@ data filesystem_write_closure_scale_anchor: ResourceHandle = ResourceHandle { type: "filesystem", resource_id: "closure-scale-witness", key: "scale", - cap: "" + cap: "" as Secret } func witness_filesystem_write_survives_name_collision() -> Bool { diff --git a/dag/test/claim/markdown_roundtrip_test.dag b/dag/test/claim/markdown_roundtrip_test.dag index 0f2a90cc470..175e5438474 100644 --- a/dag/test/claim/markdown_roundtrip_test.dag +++ b/dag/test/claim/markdown_roundtrip_test.dag @@ -96,6 +96,7 @@ fn spellings_override(bullet: String, separator: String) -> MarkdownSpellings { blockquote_marker: commonmark_gfm_spellings.blockquote_marker, list_indent: commonmark_gfm_spellings.list_indent, block_separator: separator, + thematic_break: commonmark_gfm_spellings.thematic_break, } } diff --git a/dag/test/claim/markdown_source_emit_test.dag b/dag/test/claim/markdown_source_emit_test.dag index a4b39e5d24c..3874396d05c 100644 --- a/dag/test/claim/markdown_source_emit_test.dag +++ b/dag/test/claim/markdown_source_emit_test.dag @@ -190,6 +190,7 @@ fn perturbed_bullet_spellings() -> MarkdownSpellings { blockquote_marker: commonmark_gfm_spellings.blockquote_marker, list_indent: commonmark_gfm_spellings.list_indent, block_separator: commonmark_gfm_spellings.block_separator, + thematic_break: commonmark_gfm_spellings.thematic_break, } } diff --git a/dag/test/claim/realization_schedule_witness_test.dag b/dag/test/claim/realization_schedule_witness_test.dag index e7c3369ed7d..90ff6160bbe 100644 --- a/dag/test/claim/realization_schedule_witness_test.dag +++ b/dag/test/claim/realization_schedule_witness_test.dag @@ -30,6 +30,8 @@ fn synthetic_correct_schedule() -> List> { explicit_entries: [] node_frontier_selection: SelectionOff profile: runnable_resource_profile_negligible() + exclude_substrings: [] + discovery_scope_dirs: [] }, RunnableSingleClaim { entry: gate_entry, function: "emit_host_gate_passes", profile: runnable_resource_profile_negligible() } ] diff --git a/dag/test/claim/runnable_resource_profile_witness_test.dag b/dag/test/claim/runnable_resource_profile_witness_test.dag index a572705ae57..3f9561e425d 100644 --- a/dag/test/claim/runnable_resource_profile_witness_test.dag +++ b/dag/test/claim/runnable_resource_profile_witness_test.dag @@ -72,6 +72,8 @@ fn witness_corpus_never_forbids_co_residence() -> Bool { memory: runnable_memory_substantial(), execution_mode: Wet ) + exclude_substrings: [] + discovery_scope_dirs: [] } !runnable_forbids_corpus_co_residence(r: corpus) } diff --git a/dag/test/claim/seed_debt_bundle_item_2_floor_scope.dag b/dag/test/claim/seed_debt_bundle_item_2_floor_scope.dag index f6ac534e1f2..351b657aa80 100644 --- a/dag/test/claim/seed_debt_bundle_item_2_floor_scope.dag +++ b/dag/test/claim/seed_debt_bundle_item_2_floor_scope.dag @@ -6,7 +6,8 @@ import std.realization_schedule { Runnable, RunnableDiscoveryBatch, ScheduleWitnessEntry, - CorpusWitnessKind + CorpusWitnessKind, + runnable_resource_profile_negligible } import std.measure { HardwareThreadCount, hardware_thread_count } import std.types { List } @@ -27,7 +28,10 @@ fn seed_debt_floor_scope_batches() -> List> { source_roots: witness_layer_roots, scan_dirs: [], explicit_entries: seed_debt_witness_entries(), - node_frontier_selection: SelectionOff + node_frontier_selection: SelectionOff, + exclude_substrings: [], + discovery_scope_dirs: [], + profile: runnable_resource_profile_negligible() } ]] } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 66792d2cb61..42c70e6e5a3 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -5001,7 +5001,8 @@ fn dag_bodied_fn_target_model( lex: dag_lex(), binding_spellings: dag_binding_spellings(), token_class_emit_transforms: target_model_emit_transforms_empty, - authority_source_text: spec.authority_source_text + authority_source_text: spec.authority_source_text, + runtime_row: target_emit_host_runtime_row_unconfigured } } } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 60860055d3c..fc075ffb42a 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -16,7 +16,7 @@ import gunbc.ci_gate { import v2.std.algebra { filter, length, list_snoc_item, skip, zip_map } import v2.std.collection { List, Optional, Absent, Present } import v2.std.dependency { DataDependsOn, ResourceDependsOn, DependencyView } -import v2.std.node { Atom, Node, TypeNode } +import v2.std.node { Atom, Node, TypeNode, SyntheticOccurrence } import v2.std.text { String } import std.types { ContentHash, Int } import std.nat { Nat } @@ -70,7 +70,8 @@ data floor_self_host_realized_comparison_claims_entry: String = "src/v2/workflow data floor_corpus_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_corpus } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } fn entry_kind_is_execution(w: ScheduleWitnessEntry) -> Bool { @@ -108,15 +109,15 @@ fn corpus_plan_nodes(spec: CiSpec) -> List { fn gate_node(g: Gate) -> Node { match g { - EmitHostGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_emit } }, children: [] } - LayeringImportsGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_layering } }, children: [] } - ExtdepsExternalAuthorityGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_extdeps_external_authority } }, children: [] } - DagCompileCleanGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_compile } }, children: [] } - GeneratedArtifactDriftGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_generated_artifact } }, children: [] } - SourceRootIngestGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_sourceingest } }, children: [] } - RegenVerifyGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_regen_verify } }, children: [] } - SelfHostReadsRealBytesGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_self_host_reads_real_bytes } }, children: [] } - SelfHostStalenessGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_self_host_staleness } }, children: [] } + EmitHostGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_emit } }, children: [], occurrence_id: SyntheticOccurrence } + LayeringImportsGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_layering } }, children: [], occurrence_id: SyntheticOccurrence } + ExtdepsExternalAuthorityGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_extdeps_external_authority } }, children: [], occurrence_id: SyntheticOccurrence } + DagCompileCleanGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_compile } }, children: [], occurrence_id: SyntheticOccurrence } + GeneratedArtifactDriftGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_generated_artifact } }, children: [], occurrence_id: SyntheticOccurrence } + SourceRootIngestGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_sourceingest } }, children: [], occurrence_id: SyntheticOccurrence } + RegenVerifyGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_regen_verify } }, children: [], occurrence_id: SyntheticOccurrence } + SelfHostReadsRealBytesGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_self_host_reads_real_bytes } }, children: [], occurrence_id: SyntheticOccurrence } + SelfHostStalenessGate => Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_gate_self_host_staleness } }, children: [], occurrence_id: SyntheticOccurrence } } } @@ -268,7 +269,8 @@ fn corpus_runnable_for(spec: CiSpec) -> Runnable { data execution_corpus_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_execution_corpus } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } fn execution_corpus_runnable_for(spec: CiSpec) -> Runnable { @@ -290,7 +292,8 @@ fn execution_corpus_runnable_for(spec: CiSpec) -> Runnable { data bin_witness_corpus_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^gunbc_floor_bin_witness_corpus } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data bin_witness_corpus_note: String = "The bin-execution witness batch: the declared Wet lane for witnesses whose fns execute compiled seed witness binaries (gunbc.ci_layer_roots bin_witness_wet_entries — see bin_witness_wet_note there). They ran silently wet inside the discovery corpus until the hermetic flip; now the discovery batch is Hermetic and these rows keep their per-PR coverage under an explicit Wet profile (spawns_host_compiler: the runner may cargo-build a missing witness bin locally; in CI the build job prebuilds them). Enrolled only when the spec runs live discovery (bin_witness_corpus_enrolled), so regen/emit-determinism/synthetic specs carry no bin batch." From 43dd899ffca1c7824e667dbd5132c4a73b483e90 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 18:59:17 +0000 Subject: [PATCH 11/28] WIP: v2 memory control audit --- dag/gunbc/auth/patterns.dag | 3 ++- dag/gunbc/tools/card_intake.dag | 10 ++++------ .../src/bin/compile_clean_floor_skip_witness.rs | 4 +--- src/v1/stage0/src/cli_run.rs | 9 +++++++-- src/v1/stage0/src/std_coercion.rs | 11 ++++++++++- src/v1/stage0/src/v1_compiler_infer.rs | 14 +++++++++++++- 6 files changed, 37 insertions(+), 14 deletions(-) diff --git a/dag/gunbc/auth/patterns.dag b/dag/gunbc/auth/patterns.dag index 33d1a843876..d9cabd6eb0d 100644 --- a/dag/gunbc/auth/patterns.dag +++ b/dag/gunbc/auth/patterns.dag @@ -4,6 +4,7 @@ import std.resources { Filesystem, Network, AuthContext } import std.types { AccessToken, AuthScheme, + Bearer, NonEmptyStr } import extdeps.cloud.gcp.gcp { @@ -46,7 +47,7 @@ pattern credential_chain( service_account: ServiceAccountEmail?, secret_name: NonEmptyStr, project_id: GcpProjectId, - scheme: String = "Bearer", + scheme: AuthScheme = Bearer, header_name: String?, source_id: NonEmptyStr, required_scopes: List, diff --git a/dag/gunbc/tools/card_intake.dag b/dag/gunbc/tools/card_intake.dag index ce706c74cd3..43e22f304ea 100644 --- a/dag/gunbc/tools/card_intake.dag +++ b/dag/gunbc/tools/card_intake.dag @@ -196,12 +196,10 @@ func intake_binder( ) } - flags = for r in results { - match r.disposition { - ReadyToList => false - NeedsReview { reasons: _ } => true - } - } + flags = map(results, r => match r.disposition { + ReadyToList => false + NeedsReview { reasons: _ } => true + }) return { total: count(results), flagged: count_true(flags: flags) } } diff --git a/src/v1/stage0/src/bin/compile_clean_floor_skip_witness.rs b/src/v1/stage0/src/bin/compile_clean_floor_skip_witness.rs index 61979724362..28fdf0d0174 100644 --- a/src/v1/stage0/src/bin/compile_clean_floor_skip_witness.rs +++ b/src/v1/stage0/src/bin/compile_clean_floor_skip_witness.rs @@ -2,9 +2,7 @@ use std::process::ExitCode; -use v1_compiler::cli_run::{ - documentation_only_floor_skip_label_for_ci, workspace_root, -}; +use v1_compiler::cli_run::{documentation_only_floor_skip_label_for_ci, workspace_root}; fn main() -> ExitCode { std::env::set_current_dir(workspace_root()).expect("chdir to workspace root"); diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index b2b70543d26..9b75511822c 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -1632,7 +1632,9 @@ pub fn documentation_only_floor_skip_label_for_ci() -> String { } match floor_git_diff_name_status_range() { Err(msg) => { - eprintln!("documentation-only floor skip: diff observation failed ({msg}) — full floor"); + eprintln!( + "documentation-only floor skip: diff observation failed ({msg}) — full floor" + ); RUN_FULL_FLOOR_LABEL.to_string() } Ok((changed_paths, _departed)) => { @@ -9962,7 +9964,10 @@ new file mode 100644 } } lying.sort(); - eprintln!("lying SubstrateInputsOnly stamps (G1 carrier closure): {}", lying.len()); + eprintln!( + "lying SubstrateInputsOnly stamps (G1 carrier closure): {}", + lying.len() + ); for (entry, carrier) in &lying { eprintln!(" {entry} -> {carrier}"); } diff --git a/src/v1/stage0/src/std_coercion.rs b/src/v1/stage0/src/std_coercion.rs index 075e24fe4b9..d6d3a15ac9a 100644 --- a/src/v1/stage0/src/std_coercion.rs +++ b/src/v1/stage0/src/std_coercion.rs @@ -49,10 +49,19 @@ pub struct CastSyntax { pub cast_rules: Rc>>, } +pub fn grounded_primitive_coproduct_cast_note() -> String { + thread_local! { + static CACHED: String = { + "The Int->Nat and String->FreeMonoid rows are GROUNDED identities, not hollow casts (operator Ruling 3, 2026-07-15): a Nat IS an Int (numeric tower grounded construction-side #5428, Zero->Int(0)/Succ->Int(k+1), native form == modeled form) and a String IS a FreeMonoid (std.string_type: type String = FreeMonoid — strings over an alphabet are the free monoid). So an Int literal where a Nat is expected, and a String literal where a FreeMonoid is expected, are the same value at the kernel level; the wall's kernel_value_declared_type_mismatch consults dag_can_cast and correctly stops flagging them. NON-grounded primitive->coproduct straddles stay red by construction: Bool->FreeMonoid (card_intake), String->Doc (live_deploy), String->AuthScheme (auth) are genuine site bugs with no cast row.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn dag_cast_rules() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"from_type": "Int", "to_type": "Int"}, {"from_type": "Int", "to_type": "Float"}, {"from_type": "Float", "to_type": "Int"}, {"from_type": "Float", "to_type": "Float"}, {"from_type": "Bool", "to_type": "Int"}])) + serde_json::from_value(serde_json::json!([{"from_type": "Int", "to_type": "Int"}, {"from_type": "Int", "to_type": "Float"}, {"from_type": "Float", "to_type": "Int"}, {"from_type": "Float", "to_type": "Float"}, {"from_type": "Bool", "to_type": "Int"}, {"from_type": "Int", "to_type": "Nat"}, {"from_type": "String", "to_type": "FreeMonoid"}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index f27c0a9d431..786fdc46337 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -5909,6 +5909,15 @@ pub fn type_has_sole_constructor(type_name: String, scope: Rc) -> bo } } +pub fn zero_field_variant_tag_reference_frontier_note() -> String { + thread_local! { + static CACHED: String = { + "P0 field-wall frontier (operator Ruling 1a, 2026-07-15): a ZERO-field literal of a coproduct VARIANT (field_inits empty AND variant_owner_node != none) is sanctioned as a TAG REFERENCE, not a construction — the `discriminant(v: PrefixToken {})` idiom (16+ sites in src/v2/std/compilers/target_model.dag) names a variant to obtain its stable tag identity without materializing a value. Presence checking is skipped for exactly this shape; PARTIAL literals (any field present) stay red, and zero-field literals of NON-variant records (variant_owner_node == none) stay red — so the audit F1 probes (CacheProvider/CostAccount partial literals) are unaffected. This is a decidable structural exemption (not an absorbing fallback: it refuses precisely, never widens on failure). DISSOLVE-ON: a first-class variant-tag carrier that types the discriminant argument position, at which point the exemption is deleted and the sites migrate to the carrier.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn infer_record_lit( type_name: Option, field_inits: Rc>>, @@ -6006,8 +6015,11 @@ pub fn infer_record_lit( }, } }; - let missing_field_diags = if ((tn_str.clone() == "".to_string()) + let is_zero_field_variant_tag_reference = (((field_inits.clone().len() as i64) == 0) + && (variant_owner_node(scope.clone(), tn_str.clone()) != None)); + let missing_field_diags = if (((tn_str.clone() == "".to_string()) || ((presence_fields.clone().len() as i64) == 0)) + || is_zero_field_variant_tag_reference.clone()) { Rc::new(vec![]) } else { From 9f55fafab594f2369fc4a12d6c953069f1e8fe7e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 19:09:48 +0000 Subject: [PATCH 12/28] WIP: v2 memory control audit --- src/v1/04_infer.dag | 7 ++++++- src/v1/stage0/src/v1_compiler_infer.rs | 22 +++++++++++++++++++++- 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 3f5758b5352..48f627b7562 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -836,7 +836,12 @@ fn direct_call_arg_mismatch_diags( let formal_raw = param_node_type_expr(n: pair.second) let formal_subst = substitute_generics(n: formal_raw, subst: call_subst, source_indices: source_indices) let formal = peel_nominal_alias_identity(n: formal_subst, env: type_env, module_name: module_name) - match typed_args |> skip(pair.first) |> first { + let param_name = authored_name_at(source_indices: source_indices, node: pair.second) + let matched_arg = match typed_args |> filter(ta => arg_has_name(arg: ta, name: param_name, source_indices: source_indices)) |> first { + Present { value: named_ta } => Present { value: named_ta } + Absent => typed_args |> skip(pair.first) |> first + } + match matched_arg { Present { value: ta } => let actual_raw = resolved_type(n: arg_value(n: ta)) let actual = peel_nominal_alias_identity(n: actual_raw, env: type_env, module_name: module_name) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 786fdc46337..3437270cce1 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -1447,7 +1447,27 @@ pub fn direct_call_arg_mismatch_diags( type_env.clone(), module_name.clone(), ); - match typed_args.clone().get(pair.0.clone() as usize).cloned() { + let param_name = authored_name_at(source_indices.clone(), pair.1.clone()); + let matched_arg = match Rc::new({ + let mut __result = Vec::new(); + for ta in typed_args.clone().iter().cloned() { + if arg_has_name( + ta.clone(), + param_name.clone(), + source_indices.clone(), + ) { + __result.push(ta); + } + } + __result + }) + .first() + .cloned() + { + Some(named_ta) => Some(named_ta.clone()), + None => typed_args.clone().get(pair.0.clone() as usize).cloned(), + }; + match matched_arg.clone() { Some(ta) => { let actual_raw = resolved_type(arg_value(ta.clone())); let actual = peel_nominal_alias_identity( From 9edb9288f4a4ab75bbe57f5fb1484ec3f48a91d1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 19:21:50 +0000 Subject: [PATCH 13/28] WIP: v2 memory control audit --- dag/std/coercion.dag | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/dag/std/coercion.dag b/dag/std/coercion.dag index c9f33807a16..2bba9fca564 100644 --- a/dag/std/coercion.dag +++ b/dag/std/coercion.dag @@ -34,20 +34,24 @@ type CastSyntax { cast_rules: List } -data grounded_primitive_coproduct_cast_note: String = "The Int->Nat and String->FreeMonoid rows are GROUNDED identities, not hollow casts (operator Ruling 3, 2026-07-15): a Nat IS an Int (numeric tower grounded construction-side #5428, Zero->Int(0)/Succ->Int(k+1), native form == modeled form) and a String IS a FreeMonoid (std.string_type: type String = FreeMonoid — strings over an alphabet are the free monoid). So an Int literal where a Nat is expected, and a String literal where a FreeMonoid is expected, are the same value at the kernel level; the wall's kernel_value_declared_type_mismatch consults dag_can_cast and correctly stops flagging them. NON-grounded primitive->coproduct straddles stay red by construction: Bool->FreeMonoid (card_intake), String->Doc (live_deploy), String->AuthScheme (auth) are genuine site bugs with no cast row." +data grounded_primitive_coproduct_cast_note: String = "The Int->Nat and String->FreeMonoid identities are GROUNDED, not hollow casts (operator Ruling 3, 2026-07-15): a Nat IS an Int (numeric tower grounded construction-side #5428, Zero->Int(0)/Succ->Int(k+1), native form == modeled form) and a String IS a FreeMonoid (std.string_type: type String = FreeMonoid — strings over an alphabet are the free monoid). They live in their OWN list, NOT in dag_cast_rules, on purpose: dag_can_cast consults BOTH lists so the wall's kernel_value_declared_type_mismatch stops flagging an Int literal where a Nat is expected (and a String where a FreeMonoid is expected); but is_dag_cast_domain_type reads ONLY dag_cast_rules, so grounding a primitive to a coproduct does NOT drag that coproduct into the explicit-`as`-cast validation domain. Folding them into dag_cast_rules would make Nat/String cast-domain types and newly REJECT pre-existing well-typed casts whose reverse rule is absent (`Nat as Int` in bmc_onboard, `Int as String` in srv3/host_effect were skipped before because their far type was not a domain type) — a regression, not the intent. NON-grounded primitive->coproduct straddles stay red by construction: Bool->FreeMonoid (card_intake), String->Doc (live_deploy), String->AuthScheme (auth) are genuine site bugs with no identity." data dag_cast_rules: List = [ - { from_type: "Int", to_type: "Int" }, - { from_type: "Int", to_type: "Float" }, - { from_type: "Float", to_type: "Int" }, - { from_type: "Float", to_type: "Float" }, - { from_type: "Bool", to_type: "Int" }, + { from_type: "Int", to_type: "Int" }, + { from_type: "Int", to_type: "Float" }, + { from_type: "Float", to_type: "Int" }, + { from_type: "Float", to_type: "Float" }, + { from_type: "Bool", to_type: "Int" }, +] + +data grounded_primitive_coproduct_identities: List = [ { from_type: "Int", to_type: "Nat" }, { from_type: "String", to_type: "FreeMonoid" }, ] fn dag_can_cast(source_type: String, target_type: String) -> Bool { - dag_cast_rules |> any(r => r.from_type == source_type && r.to_type == target_type) + (dag_cast_rules |> any(r => r.from_type == source_type && r.to_type == target_type)) + || (grounded_primitive_coproduct_identities |> any(r => r.from_type == source_type && r.to_type == target_type)) } fn is_dag_cast_domain_type(name: String) -> Bool { From 4efcc3cf1017b18095a102f6e9b60207381cd37f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 19:26:54 +0000 Subject: [PATCH 14/28] Ruling 3: separate grounded identities from cast-domain to fix as-cast regression MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Placing Int→Nat / String→FreeMonoid in dag_cast_rules made Nat and String into cast-DOMAIN types (is_dag_cast_domain_type), which newly triggered `as`-cast validation of pre-existing well-typed casts whose reverse rule is absent — `Nat as Int` (bmc_onboard), `Int as String` (srv3_os_install, host_effect_realize) — reddening the floor compile-clean gate. Those casts were skipped before because their far type was not a domain type. Move the two grounded identities into their own list that dag_can_cast consults (so kernel_value_declared_type_mismatch still stops flagging an Int where a Nat / a String where a FreeMonoid is expected), while is_dag_cast_domain_type continues reading only dag_cast_rules — so the explicit-`as`-cast validation domain is unchanged. Verified: the CI gate's own closure (floor_effect_gate_witness.dag) now compiles clean, whole-tree ledger stays 0, record_field_walls witnesses green. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v1/stage0/src/std_coercion.rs | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/src/v1/stage0/src/std_coercion.rs b/src/v1/stage0/src/std_coercion.rs index d6d3a15ac9a..873266a9a53 100644 --- a/src/v1/stage0/src/std_coercion.rs +++ b/src/v1/stage0/src/std_coercion.rs @@ -52,7 +52,7 @@ pub struct CastSyntax { pub fn grounded_primitive_coproduct_cast_note() -> String { thread_local! { static CACHED: String = { - "The Int->Nat and String->FreeMonoid rows are GROUNDED identities, not hollow casts (operator Ruling 3, 2026-07-15): a Nat IS an Int (numeric tower grounded construction-side #5428, Zero->Int(0)/Succ->Int(k+1), native form == modeled form) and a String IS a FreeMonoid (std.string_type: type String = FreeMonoid — strings over an alphabet are the free monoid). So an Int literal where a Nat is expected, and a String literal where a FreeMonoid is expected, are the same value at the kernel level; the wall's kernel_value_declared_type_mismatch consults dag_can_cast and correctly stops flagging them. NON-grounded primitive->coproduct straddles stay red by construction: Bool->FreeMonoid (card_intake), String->Doc (live_deploy), String->AuthScheme (auth) are genuine site bugs with no cast row.".to_string() + "The Int->Nat and String->FreeMonoid identities are GROUNDED, not hollow casts (operator Ruling 3, 2026-07-15): a Nat IS an Int (numeric tower grounded construction-side #5428, Zero->Int(0)/Succ->Int(k+1), native form == modeled form) and a String IS a FreeMonoid (std.string_type: type String = FreeMonoid — strings over an alphabet are the free monoid). They live in their OWN list, NOT in dag_cast_rules, on purpose: dag_can_cast consults BOTH lists so the wall's kernel_value_declared_type_mismatch stops flagging an Int literal where a Nat is expected (and a String where a FreeMonoid is expected); but is_dag_cast_domain_type reads ONLY dag_cast_rules, so grounding a primitive to a coproduct does NOT drag that coproduct into the explicit-`as`-cast validation domain. Folding them into dag_cast_rules would make Nat/String cast-domain types and newly REJECT pre-existing well-typed casts whose reverse rule is absent (`Nat as Int` in bmc_onboard, `Int as String` in srv3/host_effect were skipped before because their far type was not a domain type) — a regression, not the intent. NON-grounded primitive->coproduct straddles stay red by construction: Bool->FreeMonoid (card_intake), String->Doc (live_deploy), String->AuthScheme (auth) are genuine site bugs with no identity.".to_string() }; } CACHED.with(|c: &String| c.clone()) @@ -61,7 +61,17 @@ pub fn grounded_primitive_coproduct_cast_note() -> String { pub fn dag_cast_rules() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"from_type": "Int", "to_type": "Int"}, {"from_type": "Int", "to_type": "Float"}, {"from_type": "Float", "to_type": "Int"}, {"from_type": "Float", "to_type": "Float"}, {"from_type": "Bool", "to_type": "Int"}, {"from_type": "Int", "to_type": "Nat"}, {"from_type": "String", "to_type": "FreeMonoid"}])) + serde_json::from_value(serde_json::json!([{"from_type": "Int", "to_type": "Int"}, {"from_type": "Int", "to_type": "Float"}, {"from_type": "Float", "to_type": "Int"}, {"from_type": "Float", "to_type": "Float"}, {"from_type": "Bool", "to_type": "Int"}])) + .expect("valid data definition") + }; + } + CACHED.with(|c: &Rc>>| c.clone()) +} + +pub fn grounded_primitive_coproduct_identities() -> Rc>> { + thread_local! { + static CACHED: Rc>> = { + serde_json::from_value(serde_json::json!([{"from_type": "Int", "to_type": "Nat"}, {"from_type": "String", "to_type": "FreeMonoid"}])) .expect("valid data definition") }; } @@ -69,7 +79,7 @@ pub fn dag_cast_rules() -> Rc>> { } pub fn dag_can_cast(source_type: String, target_type: String) -> bool { - { + ({ let mut __found = false; for r in dag_cast_rules().iter().cloned() { if ((r.from_type.clone() == source_type.clone()) @@ -80,7 +90,18 @@ pub fn dag_can_cast(source_type: String, target_type: String) -> bool { } } __found - } + } || { + let mut __found = false; + for r in grounded_primitive_coproduct_identities().iter().cloned() { + if ((r.from_type.clone() == source_type.clone()) + && (r.to_type.clone() == target_type.clone())) + { + __found = true; + break; + } + } + __found + }) } pub fn is_dag_cast_domain_type(name: String) -> bool { From ea34a33c0f3e4378f9023445d3ca53908b8b6592 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 19:39:51 +0000 Subject: [PATCH 15/28] WIP: v2 memory control audit --- dag/gunbc/tools/card_intake.dag | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/tools/card_intake.dag b/dag/gunbc/tools/card_intake.dag index 43e22f304ea..70e03a9f33d 100644 --- a/dag/gunbc/tools/card_intake.dag +++ b/dag/gunbc/tools/card_intake.dag @@ -196,10 +196,12 @@ func intake_binder( ) } - flags = map(results, r => match r.disposition { - ReadyToList => false - NeedsReview { reasons: _ } => true - }) + flags = for r in results { + [match r.disposition { + ReadyToList => false + NeedsReview { reasons: _ } => true + }] + } return { total: count(results), flagged: count_true(flags: flags) } } From 0f2339e127060f43f51ab74b05a56c41f833a760 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 20:20:16 +0000 Subject: [PATCH 16/28] WIP: v2 memory control audit --- .../manual/find_witness_project_to_core_controls.dag | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag b/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag index d2e38c9298e..d23931bcb85 100644 --- a/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag +++ b/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag @@ -313,10 +313,12 @@ fn i32_value_set_interval_first() -> Node { label: Named { name: ^integer_value_set_field_kind }, target: Node { kind: TypeNode { connective: Atom { identity: ^integer_value_set_kind_interval } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } } - ] + ], + occurrence_id: SyntheticOccurrence } } @@ -356,7 +358,8 @@ fn unbounded_value_set_with_extra_field() -> Node { label: Named { name: ^integer_value_set_field_kind }, target: Node { kind: TypeNode { connective: Atom { identity: ^integer_value_set_kind_unbounded } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } }, Edge { From d81c57aacd90b23005b74e8e681796a4cde424e7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 20:30:49 +0000 Subject: [PATCH 17/28] WIP: v2 memory control audit --- .../claim/manual/find_witness_project_to_core_controls.dag | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag b/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag index d23931bcb85..3c177e602a1 100644 --- a/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag +++ b/src/v2/test/claim/manual/find_witness_project_to_core_controls.dag @@ -366,7 +366,8 @@ fn unbounded_value_set_with_extra_field() -> Node { label: Named { name: ^integer_value_set_field_extra }, target: Node { kind: TypeNode { connective: Atom { identity: ^integer_value_set_field_extra } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } } ], From 50c464635347c3bdbea452a34f07a1d2a78e45ce Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 20:41:18 +0000 Subject: [PATCH 18/28] WIP: v2 memory control audit --- .../claim/module_resolution_plan_witness_test.dag | 14 +++++++++----- .../test/claim/realization_runner_witness_test.dag | 8 +++++--- src/v2/workflow/batch_runner.dag | 11 +++++++---- 3 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/v2/test/claim/module_resolution_plan_witness_test.dag b/src/v2/test/claim/module_resolution_plan_witness_test.dag index 4575a6b220a..05fa18a08c2 100644 --- a/src/v2/test/claim/module_resolution_plan_witness_test.dag +++ b/src/v2/test/claim/module_resolution_plan_witness_test.dag @@ -4,7 +4,7 @@ import v2.lens.module_graph { ImportResolutionFact, ModuleDeclarationFact } import v2.std.algebra { length } import v2.std.collection { List } import v2.std.dependency { DependencyView } -import v2.std.node { Atom, Node, TypeNode } +import v2.std.node { Atom, Node, TypeNode, SyntheticOccurrence } import v2.std.text { String } import v2.workflow.executor { ExecutorBatch, executor_job_for_node } import v2.workflow.realization_runner { @@ -27,22 +27,26 @@ import v2.workflow.module_resolution_plan { data module_fixture_a_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^module_fixture_a } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data module_fixture_b_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^module_fixture_b } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data module_fixture_c_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^module_fixture_c } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data module_fixture_d_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^module_fixture_d } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data module_fixture_declarations: List = [ diff --git a/src/v2/test/claim/realization_runner_witness_test.dag b/src/v2/test/claim/realization_runner_witness_test.dag index 31571b1d90c..cb857f417b7 100644 --- a/src/v2/test/claim/realization_runner_witness_test.dag +++ b/src/v2/test/claim/realization_runner_witness_test.dag @@ -3,7 +3,7 @@ module v2.test.claim.realization_runner_witness import v2.std.algebra { length } import v2.std.collection { List } import v2.std.dependency { DataDependsOn, DependencyView } -import v2.std.node { Atom, Node, TypeNode } +import v2.std.node { Atom, Node, TypeNode, SyntheticOccurrence } import v2.workflow.executor { ExecutorBatch, ExecutorJob, @@ -43,12 +43,14 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data runner_test_a_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^runner_test_a } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data runner_test_b_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^runner_test_b } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data runner_test_a_to_b: DependencyView = DependencyView { diff --git a/src/v2/workflow/batch_runner.dag b/src/v2/workflow/batch_runner.dag index 79b18cf2c81..091bb756bfb 100644 --- a/src/v2/workflow/batch_runner.dag +++ b/src/v2/workflow/batch_runner.dag @@ -4,7 +4,7 @@ import v2.std.algebra { fold_list_right, length, list_snoc_item } import v2.std.collection { List } import v2.std.dependency { DataDependsOn, DependencyView } import v2.std.logic { Bool } -import v2.std.node { Atom, Node, Symbol, TypeNode } +import v2.std.node { Atom, Node, Symbol, TypeNode, SyntheticOccurrence } import v2.std.text { String } import v2.workflow.executor { ExecutorBatch, @@ -23,17 +23,20 @@ data bre_suite_entry: String = "src/v2/workflow/affected_set_ci_runner_test.dag" data bre_core_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^bre_core_symbol } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data bre_a_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^bre_a_symbol } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data bre_b_node: Node = Node { kind: TypeNode { connective: Atom { identity: ^bre_b_symbol } }, - children: [] + children: [], + occurrence_id: SyntheticOccurrence } data bre_core_to_a_dependency: DependencyView = DependencyView { From 5d37829d7bcd9ff3fbde96c1f33c102c26a35e1a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 20:51:50 +0000 Subject: [PATCH 19/28] WIP: v2 memory control audit --- src/v2/extdeps/languages/rust.dag | 1 + src/v2/extdeps/languages/rust_wire_serde.dag | 1 + 2 files changed, 2 insertions(+) diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index 60e63ce52b7..880edcdc142 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -1518,6 +1518,7 @@ fn rust_free_monoid_collection_apply_vec() -> TargetGenericApply { surface: ^rust_collection_surface_vec, open: ^rust_token_lt, separator: ^rust_token_comma, + field_label_separator: optional_absent(), close: ^rust_token_gt } } diff --git a/src/v2/extdeps/languages/rust_wire_serde.dag b/src/v2/extdeps/languages/rust_wire_serde.dag index 8be2e3062e0..390c8900fc7 100644 --- a/src/v2/extdeps/languages/rust_wire_serde.dag +++ b/src/v2/extdeps/languages/rust_wire_serde.dag @@ -323,6 +323,7 @@ fn rust_wire_serde_target_model(naming: VariantNaming) -> TargetModel { lex: rust_ws_lex(), binding_spellings: empty_map(), authority_source_text: rust_ws_authority_source_text(naming: naming), + token_class_emit_transforms: empty_map(), runtime_row: target_emit_host_runtime_row_unconfigured } } From e818e295944306874424bb9e957dfda11fa4de50 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 21:02:33 +0000 Subject: [PATCH 20/28] WIP: v2 memory control audit --- dag/gunbc/auth/patterns.dag | 4 +++- src/v2/test/claim/manual/infer_ground_add.dag | 7 +++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/auth/patterns.dag b/dag/gunbc/auth/patterns.dag index d9cabd6eb0d..9ad65cafa2f 100644 --- a/dag/gunbc/auth/patterns.dag +++ b/dag/gunbc/auth/patterns.dag @@ -41,13 +41,15 @@ fn build_token(payload: Secret, scheme: AuthScheme, header_name: String, source_ { token: payload, scheme: scheme, expires_at: none } } +data default_credential_scheme: AuthScheme = Bearer + pattern credential_chain( runtime: AuthRuntime, audience: NonEmptyStr, service_account: ServiceAccountEmail?, secret_name: NonEmptyStr, project_id: GcpProjectId, - scheme: AuthScheme = Bearer, + scheme: AuthScheme = default_credential_scheme, header_name: String?, source_id: NonEmptyStr, required_scopes: List, diff --git a/src/v2/test/claim/manual/infer_ground_add.dag b/src/v2/test/claim/manual/infer_ground_add.dag index c7d5611bce4..40c69c1201d 100644 --- a/src/v2/test/claim/manual/infer_ground_add.dag +++ b/src/v2/test/claim/manual/infer_ground_add.dag @@ -65,11 +65,13 @@ import v2.std.runtime { InterpretationAlgebra, InterpretationStructureWitness, LoopInterpreter, + MatchInterpreter, RuntimePrimitive, RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + runtime_reject_match_arm } import v2.std.witness { Holds, Violates } @@ -165,7 +167,8 @@ fn infer_receipt_interpretation() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: infer_receipt_bind_value - } + }, + match: MatchInterpreter { choose_arm: runtime_reject_match_arm } } } From 243f80eb42c31041eaa92e18d42733c9ec1cd369 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 21:12:51 +0000 Subject: [PATCH 21/28] WIP: v2 memory control audit --- .tmp_witness/flag_count_witness.dag | 22 ++++++++++++++++++++++ dag/gunbc/tools/card_intake.dag | 17 +++++------------ 2 files changed, 27 insertions(+), 12 deletions(-) create mode 100644 .tmp_witness/flag_count_witness.dag diff --git a/.tmp_witness/flag_count_witness.dag b/.tmp_witness/flag_count_witness.dag new file mode 100644 index 00000000000..2bb0af0991e --- /dev/null +++ b/.tmp_witness/flag_count_witness.dag @@ -0,0 +1,22 @@ +module flag_count_witness + +type RiskReason = UnmatchedCard | HighValue + +type IntakeDisposition + = ReadyToList + | NeedsReview { reasons: List } + +data results: List<{ disposition: IntakeDisposition }> = [ + { disposition: ReadyToList }, + { disposition: NeedsReview { reasons: [] |> list_push(HighValue) } }, + { disposition: ReadyToList }, + { disposition: NeedsReview { reasons: [] |> list_push(UnmatchedCard) } }, + { disposition: ReadyToList } +] + +fn flagged_count() -> Int { + fold(results, init: 0, f: (acc, r) => match r.disposition { + ReadyToList => acc + NeedsReview { reasons: _ } => acc + 1 + }) +} diff --git a/dag/gunbc/tools/card_intake.dag b/dag/gunbc/tools/card_intake.dag index 70e03a9f33d..b48b72c778a 100644 --- a/dag/gunbc/tools/card_intake.dag +++ b/dag/gunbc/tools/card_intake.dag @@ -104,11 +104,6 @@ fn assess_intake( if count(reasons) == 0 { ReadyToList } else { NeedsReview { reasons: reasons } } } -fn count_true(flags: List) -> Int { - fold(flags, init: 0, f: (acc, b) => if b { acc + 1 } else { acc }) -} - - func recognize_binder_photo( photo_path: FilePath, model: String = default_recognition_model @@ -196,14 +191,12 @@ func intake_binder( ) } - flags = for r in results { - [match r.disposition { - ReadyToList => false - NeedsReview { reasons: _ } => true - }] - } + flagged = fold(results, init: 0, f: (acc, r) => match r.disposition { + ReadyToList => acc + NeedsReview { reasons: _ } => acc + 1 + }) - return { total: count(results), flagged: count_true(flags: flags) } + return { total: count(results), flagged: flagged } } func list_card_sku( From 8b5e02d27da7b06ed9e1032e8b9e4821c9857b47 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 21:18:56 +0000 Subject: [PATCH 22/28] card_intake: fold via fn helper (fixes List> truthy bug); rm scratch .tmp_witness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The [match ...] for-body built List> (eval_for_each is map, not flat-map); lists are truthy so count_true returned total always (cursor REQUEST_CHANGES 38458, a §5 silent-wrong-answer). Replaced with a fn helper count_flagged that folds over results directly — fold resolves in a fn body (matching the deleted count_true), proven by execution: 2 NeedsReview of 5 returns 2 (old form returned 5). Also removes the accidentally-committed .tmp_witness scratch file (review 38465). Co-Authored-By: Claude Opus 4.8 (1M context) --- .tmp_witness/flag_count_witness.dag | 22 ---------------------- dag/gunbc/tools/card_intake.dag | 16 ++++++++++------ 2 files changed, 10 insertions(+), 28 deletions(-) delete mode 100644 .tmp_witness/flag_count_witness.dag diff --git a/.tmp_witness/flag_count_witness.dag b/.tmp_witness/flag_count_witness.dag deleted file mode 100644 index 2bb0af0991e..00000000000 --- a/.tmp_witness/flag_count_witness.dag +++ /dev/null @@ -1,22 +0,0 @@ -module flag_count_witness - -type RiskReason = UnmatchedCard | HighValue - -type IntakeDisposition - = ReadyToList - | NeedsReview { reasons: List } - -data results: List<{ disposition: IntakeDisposition }> = [ - { disposition: ReadyToList }, - { disposition: NeedsReview { reasons: [] |> list_push(HighValue) } }, - { disposition: ReadyToList }, - { disposition: NeedsReview { reasons: [] |> list_push(UnmatchedCard) } }, - { disposition: ReadyToList } -] - -fn flagged_count() -> Int { - fold(results, init: 0, f: (acc, r) => match r.disposition { - ReadyToList => acc - NeedsReview { reasons: _ } => acc + 1 - }) -} diff --git a/dag/gunbc/tools/card_intake.dag b/dag/gunbc/tools/card_intake.dag index b48b72c778a..308de5ea5eb 100644 --- a/dag/gunbc/tools/card_intake.dag +++ b/dag/gunbc/tools/card_intake.dag @@ -104,6 +104,15 @@ fn assess_intake( if count(reasons) == 0 { ReadyToList } else { NeedsReview { reasons: reasons } } } +fn count_flagged( + rs: List<{ card_name: String, disposition: IntakeDisposition, product_id: Int, market_price: Float? }> +) -> Int { + fold(rs, init: 0, f: (acc, r) => match r.disposition { + ReadyToList => acc + NeedsReview { reasons: _ } => acc + 1 + }) +} + func recognize_binder_photo( photo_path: FilePath, model: String = default_recognition_model @@ -191,12 +200,7 @@ func intake_binder( ) } - flagged = fold(results, init: 0, f: (acc, r) => match r.disposition { - ReadyToList => acc - NeedsReview { reasons: _ } => acc + 1 - }) - - return { total: count(results), flagged: flagged } + return { total: count(results), flagged: count_flagged(rs: results) } } func list_card_sku( From 39dc933a1314cfad0f5fd1d4cf7e8c7209b88b5e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 21:31:03 +0000 Subject: [PATCH 23/28] WIP: v2 memory control audit --- dag/gunbc/auth/patterns.dag | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/dag/gunbc/auth/patterns.dag b/dag/gunbc/auth/patterns.dag index 9ad65cafa2f..f8b80011b66 100644 --- a/dag/gunbc/auth/patterns.dag +++ b/dag/gunbc/auth/patterns.dag @@ -41,15 +41,12 @@ fn build_token(payload: Secret, scheme: AuthScheme, header_name: String, source_ { token: payload, scheme: scheme, expires_at: none } } -data default_credential_scheme: AuthScheme = Bearer - pattern credential_chain( runtime: AuthRuntime, audience: NonEmptyStr, service_account: ServiceAccountEmail?, secret_name: NonEmptyStr, project_id: GcpProjectId, - scheme: AuthScheme = default_credential_scheme, header_name: String?, source_id: NonEmptyStr, required_scopes: List, @@ -80,7 +77,7 @@ pattern credential_chain( return { token: build_token( payload: utf8_secret_from_access_payload(payload: secret.payload), - scheme: scheme, + scheme: Bearer, header_name: header_name, source_id: source_id, required_scopes: required_scopes From cdd60dfe1fba1ea6e0cdcd04c20c012a1d9c0485 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 21:38:58 +0000 Subject: [PATCH 24/28] Wire P0 field-wall witness into CI + reconcile plan-doc drain status MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Enroll diagnostics_record_field_walls_hold in ci_layer_roots.bin_witness_wet_entries (diagnostics_test.dag is discovery-excluded, so the P0 RED/GREEN control had no live floor consumer — cursor REQUEST_CHANGES 38476 finding 1, a §5 inert-witness gap). - Update witness-realization-plan.md P0 STATUS: three rulings RESOLVED (Path A), ledger 568→45→0, compile-clean --target dag green at 0, discovery-corpus drain documented (finding 2 — the doc's stale 45 vs the now-drained tree). Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/gunbc/ci_layer_roots.dag | 1 + docs/plans/witness-realization-plan.md | 12 ++++++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 29235914e1e..b2b6023850f 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -82,6 +82,7 @@ data bin_witness_wet_entries: List = [ bin_wet(entry: "dag/test/claim/diagnostics_test.dag", f: "diagnostics_type_and_arity_holds"), bin_wet(entry: "dag/test/claim/diagnostics_test.dag", f: "diagnostics_empty_list_context_holds"), bin_wet(entry: "dag/test/claim/diagnostics_test.dag", f: "diagnostics_constructor_owner_walls_hold"), + bin_wet(entry: "dag/test/claim/diagnostics_test.dag", f: "diagnostics_record_field_walls_hold"), bin_wet(entry: "dag/test/claim/effects_rest_transport_parse_witness_test.dag", f: "effects_rest_transport_parse_keystone_holds"), bin_wet(entry: "dag/test/claim/emit_host_typed_smoke_test.dag", f: "emit_host_golden_is_nonempty_holds"), bin_wet(entry: "dag/test/claim/emit_host_typed_smoke_test.dag", f: "emit_host_golden_length_matches_declared_count_holds"), diff --git a/docs/plans/witness-realization-plan.md b/docs/plans/witness-realization-plan.md index 40468ef59ef..bbdbf87f411 100644 --- a/docs/plans/witness-realization-plan.md +++ b/docs/plans/witness-realization-plan.md @@ -31,14 +31,14 @@ schedule = realize: min(independence_width, budget / measured_peak) [spine FLA **P0 — the field wall (audit F1).** Field **presence** + field **type** checking in `04_infer`'s record-literal arm. Realization's scheduling facts (`CostAccount`, `CacheProvider`, receipts) are all record literals; while presence/types are unchecked, every downstream derive can read garbage at `0 diagnostics`. Staged like the wrapper-retained frontier: (i) ledger mode — typed, counted roster of corpus violations; (ii) drain; (iii) hard wall. ACCEPT: the audit's four probes go red; corpus green after drain. Every roster row found in (i) is a latent bug today. -> **P0 STATUS (2026-07-15, session lively-heron-614 — commits `6968b7421`, `513a7b968`, `b13be208c`):** wall LANDED in the v1 authority (`src/v1/04_infer.dag`: presence via trusted field authorities only; `kernel_value_declared_type_mismatch` tier wired into record fields AND `direct_call_arg_type_mismatch`; new `MissingField` diagnostic in `v1.std.core`). All four audit probes RED with located diagnostics; `diagnostics_witness record_field_walls` suite (5 REDs + 3 GREENs) green; whole-tree ledger **568 → 45** after three FP classes dissolved by root cause (none-sentinel `Unit` ×462 — excluded pending the `Value::Null` grounding thread; refinement-decl misclassification; homonym variants — presence now consults `variant_owner_node` first, agreeing with `parent_enum` stamping). Wall already caught real rot: `RunnableDiscoveryBatch` witness literals omit `exclude_substrings`/`discovery_scope_dirs` (eval null-fills today). +> **P0 STATUS (2026-07-15 — LANDED, drained to 0, hard wall live; session lively-heron-614 → cool-newt-143):** wall LANDED in the v1 authority (`src/v1/04_infer.dag`: presence via trusted field authorities only; `kernel_value_declared_type_mismatch` tier wired into record fields AND `direct_call_arg_type_mismatch`; new `MissingField` diagnostic in `v1.std.core`). All four audit probes RED with located diagnostics; `diagnostics_witness record_field_walls` suite (5 REDs + 3 GREENs) green **and CI-wired** (`diagnostics_record_field_walls_hold` enrolled in `ci_layer_roots.bin_witness_wet_entries`, since `diagnostics_test.dag` is discovery-excluded). The wall is a **hard wall**: `MissingField` is interpreter-blocking, so batch-1 `dag_compile_clean_gate` (`--target dag`) reds on any residue — and that gate is now **green at 0** (`gunbc compile --source-root dag --source-root src/v2 --target dag` → `0 diagnostics`; whole-tree ledger **568 → 45 → 0**; the 909-file discovery-leaf sweep → 0 field-wall errors). > -> **BLOCKED on three operator rulings** (then ~25 rows drain mechanically; roster = round-2 whole-tree ledger, reproduce with `gunbc compile --source-root dag --source-root src/v2 --target dag`): -> 1. **Empty-literal tag idiom** — `discriminant(v: PrefixToken {})`, 16+ sites in `src/v2/std/compilers/target_model.dag`: (a) sanction zero-field literals as tag references (named exemption, dissolve-on = a first-class variant-tag carrier; partial literals stay red) — RECOMMENDED; or (b) mint the tag carrier now and migrate the sites. -> 2. **String into a `Secret` field** — `dag/test/claim/filesystem_write_closure_scale_witness.dag:302`: (a) fix the test via the sanctioned Secret constructor (RECOMMENDED — name it); (b) a `String→Secret` cast row would gut the type. -> 3. **String vs `Coproduct(FreeMonoid)`** — `src/v2/compiler/01_tokenize.dag:2875`: the text-duality question. (a) if String grounds `FreeMonoid` (the Nat/Int pattern applied to text), add `{from_type: "String", to_type: "FreeMonoid"}` to `dag_cast_rules` — one row in the modeled authority; (b) if `FreeMonoid` stays structural, fix the site. Genuinely the operator's modeling call. +> **The three operator rulings — RESOLVED (Path A: drain to 0, keep the hard wall):** +> 1. **Empty-literal tag idiom** — took (a): `is_zero_field_variant_tag_reference` in `infer_record_lit` sanctions a zero-field literal *only* when it names a variant owner (`variant_owner_node`); partial literals and non-variant zero-field records stay red. Dissolve-on = a first-class variant-tag carrier (`zero_field_variant_tag_reference_frontier_note`). +> 2. **String into a `Secret` field** — took (a): the test constructs the value via the sanctioned explicit `"" as Secret` cast (`filesystem_write_closure_scale_witness.dag`), not a `String→Secret` rule. +> 3. **String vs `Coproduct(FreeMonoid)`** — grounded: `Int→Nat` and `String→FreeMonoid` are **grounded identities** in their own `grounded_primitive_coproduct_identities` list (`dag/std/coercion.dag`), consulted by `dag_can_cast` but **not** `is_dag_cast_domain_type`, so the tower unblocks without dragging `Nat`/`FreeMonoid` into `as`-cast validation (which would regress pre-existing `Nat as Int` / `Int as String` sites). Non-grounded straddles (`Bool→FreeMonoid`, `String→AuthScheme`, `String→Doc`) stay red by construction. > -> Also in the residue: a probable real bug — `Primitive(Bool)` into a `FreeMonoid` container (`dag/gunbc/tools/card_intake.dag:5890`) — and partial-literal TPs in `fleet_converge_emit_test` (7), `MarkdownSpellings`, `OrderingComparison`/`EqualityComparison`, `AlgebraInverseCompose`/`AlgebraPrimitive`, `MethodIdent`/`CallIdent`, `live_deploy/emit`, `seed_debt_bundle_item_2_floor_scope`. +> **Discovery-corpus drain (beyond the compile closure — the wall fires on every compiled file, incl. discovery-only test/manual leaves that local whole-tree compile never reaches):** `occurrence_id: SyntheticOccurrence` on `Node` fixtures (`find_witness_project_to_core_controls`, `batch_runner`, `module_resolution_plan_witness_test`, `realization_runner_witness_test`); `field_label_separator` / `token_class_emit_transforms` on the Rust emit models (`rust.dag`, `rust_wire_serde.dag`); `InterpretationAlgebra.match: MatchInterpreter { choose_arm: runtime_reject_match_arm }` (`infer_ground_add`); `card_intake` disposition count moved into a `fn count_flagged` that `fold`s over results (the earlier `[match …]` for-body built `List>` — `eval_for_each` is a map, not flat-map — and lists are truthy, so the count equalled total always; **fixed and proven by execution**, 2 of 5 → 2, old form → 5); and `credential_chain`'s `scheme` param — a stringly `"Bearer"` nickname the wall exposed as a latent `String→AuthScheme` mismatch, and non-CLI-expressible as an enum — dropped, `build_token` now takes the `Bearer` literal directly (§4 CLI boundary). **P1 — space becomes observable (F2, F4).** `ObservePeakResidentAtSubject` as a second variant on `RealizationMeasureEffect`. The host physics **already exists unmodeled** — `claim_batch` reads `getrusage(RUSAGE_CHILDREN)` and prints `[measurement] children-max-rss` — so this is a mark-on-the-carrier step, not new physics. `PerformanceReceipt` gains the peak field. `space_measure_seq` = **max** / `space_measure_par` = **add** as peers of the time rules; the `fleet_intent.dag:168` sum fixed; the keystone witness flipped. ACCEPT: first `CostAccount.space` with `basis: Measured` produced by execution; RED: a seq-composition asserting sum goes red. From 8c14232e432bccf8469ca7e78a195880885fa795 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 22:05:36 +0000 Subject: [PATCH 25/28] WIP: v2 memory control audit --- .../serialize_applied_diff_swap_operands_test.dag | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/v2/lens/application/serialize_applied_diff_swap_operands_test.dag b/src/v2/lens/application/serialize_applied_diff_swap_operands_test.dag index 9d9e9418396..e25b09b12b2 100644 --- a/src/v2/lens/application/serialize_applied_diff_swap_operands_test.dag +++ b/src/v2/lens/application/serialize_applied_diff_swap_operands_test.dag @@ -166,18 +166,6 @@ fn serialize_applied_diff_loop_body_claim_holds() -> Bool { && serialize_loop_patch_carrier_holds() } -fn serialize_applied_diff_loop_body_claim_rhs() -> Bool { - serialize_applied_diff_loop_body_claim_holds() -} - -data claim_serialize_applied_diff_loop_body: TestClaim = EqualsClaim { - label: "lens.application_serializer/serialize_diff_as_source_patch: loop body edit re-emits distinct canonical source", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: true, - rhs: serialize_applied_diff_loop_body_claim_rhs(), - classification: TestClassification { tier: Tier1, layer: Unit } -} - test fn serialize_applied_diff_loop_body_holds() -> Bool { serialize_applied_diff_loop_body_claim_holds() } From 9c9b47b5eec3189cbeaa633774b669295eaf0e38 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 22:26:28 +0000 Subject: [PATCH 26/28] WIP: v2 memory control audit --- .../execution/add_arrow_eval_by_execution_test.dag | 3 +++ .../claim/execution/bind_eval_by_execution_test.dag | 7 ++++++- .../claim/execution/branch_eval_by_execution_test.dag | 7 ++++++- .../claim/execution/emit_host_add_equals_eval_test.dag | 9 +++++++-- .../execution/emit_host_loop_equals_eval_test.dag | 9 +++++++-- .../claim/execution/loop_eval_by_execution_test.dag | 7 ++++++- .../execution/rust_emit_host_call_equals_eval_test.dag | 9 +++++++-- .../generated/idempotent_operation_conformance.dag | 9 +++++++-- .../claim/generated/language_behavior_equivalence.dag | 9 +++++++-- .../manual/dissolution_subsumption_reverification.dag | 7 ++++++- src/v2/test/claim/manual/eval_runtime.dag | 7 ++++++- .../manual/test_claim_cache_digest_sensitivity.dag | 10 +++++++++- 12 files changed, 77 insertions(+), 16 deletions(-) diff --git a/src/v2/test/claim/execution/add_arrow_eval_by_execution_test.dag b/src/v2/test/claim/execution/add_arrow_eval_by_execution_test.dag index 562b16a9b68..18956f3f143 100644 --- a/src/v2/test/claim/execution/add_arrow_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/add_arrow_eval_by_execution_test.dag @@ -210,6 +210,9 @@ fn add_arrow_eval_lazy_arm_interpretation() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: add_arrow_eval_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } diff --git a/src/v2/test/claim/execution/bind_eval_by_execution_test.dag b/src/v2/test/claim/execution/bind_eval_by_execution_test.dag index a04084c0abd..3db0fb22556 100644 --- a/src/v2/test/claim/execution/bind_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/bind_eval_by_execution_test.dag @@ -78,7 +78,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.witness { Holds, Witness } import v2.std.verdict { Pass } @@ -230,6 +232,9 @@ fn bind_interpretation() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: bind_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } diff --git a/src/v2/test/claim/execution/branch_eval_by_execution_test.dag b/src/v2/test/claim/execution/branch_eval_by_execution_test.dag index bd1b1f24064..c22f5fd3fed 100644 --- a/src/v2/test/claim/execution/branch_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/branch_eval_by_execution_test.dag @@ -78,7 +78,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.witness { Holds, Witness } import v2.std.verdict { Pass } @@ -302,6 +304,9 @@ fn branch_interpretation() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: branch_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } diff --git a/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag index 2a4170ee823..b981abd28b3 100644 --- a/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag @@ -61,7 +61,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.verdict { BuildFailed, @@ -162,7 +164,10 @@ fn emit_eval_interpretation(call_primitive: fn(Node, List, Evaluat transform: TransformInterpreter { call_primitive: call_primitive }, branch: BranchInterpreter { choose_branch: emit_eval_choose_branch }, loop: LoopInterpreter { step_loop: emit_eval_step_loop }, - bind: BindInterpreter { bind_value: emit_eval_bind_value } + bind: BindInterpreter { bind_value: emit_eval_bind_value }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm + } } } diff --git a/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag index 3b2ee6604b7..7965858f5bd 100644 --- a/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag @@ -56,7 +56,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.verdict { BuildFailed, Deferred, Pass, RunFailed, SemanticMismatch, Verdict } import v2.std.verification { @@ -202,7 +204,10 @@ fn emit_loop_eval_interpretation() -> InterpretationAlgebra { transform: TransformInterpreter { call_primitive: emit_loop_eval_call_primitive }, branch: BranchInterpreter { choose_branch: emit_loop_eval_choose_branch }, loop: LoopInterpreter { step_loop: emit_loop_eval_step_loop }, - bind: BindInterpreter { bind_value: emit_loop_eval_bind_value } + bind: BindInterpreter { bind_value: emit_loop_eval_bind_value }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm + } } } diff --git a/src/v2/test/claim/execution/loop_eval_by_execution_test.dag b/src/v2/test/claim/execution/loop_eval_by_execution_test.dag index 780c9e003c8..4cd5d132874 100644 --- a/src/v2/test/claim/execution/loop_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/loop_eval_by_execution_test.dag @@ -85,7 +85,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.witness { Holds, Witness } import v2.std.verdict { Pass } @@ -242,6 +244,9 @@ fn loop_interpretation() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: loop_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } diff --git a/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag b/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag index a9d26b1ee48..a354970c64c 100644 --- a/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag +++ b/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag @@ -52,7 +52,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.verdict { BuildFailed, Deferred, Pass, RunFailed, SemanticMismatch, Verdict } import v2.std.verification { @@ -151,7 +153,10 @@ fn emit_call_eval_interpretation( transform: TransformInterpreter { call_primitive: call_primitive }, branch: BranchInterpreter { choose_branch: emit_call_eval_choose_branch }, loop: LoopInterpreter { step_loop: emit_call_eval_step_loop }, - bind: BindInterpreter { bind_value: emit_call_eval_bind_value } + bind: BindInterpreter { bind_value: emit_call_eval_bind_value }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm + } } } diff --git a/src/v2/test/claim/generated/idempotent_operation_conformance.dag b/src/v2/test/claim/generated/idempotent_operation_conformance.dag index 865ff2c3eaf..f6b338d1a01 100644 --- a/src/v2/test/claim/generated/idempotent_operation_conformance.dag +++ b/src/v2/test/claim/generated/idempotent_operation_conformance.dag @@ -48,7 +48,9 @@ import v2.std.runtime { LoopInterpreter, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.verdict { Pass, Deferred, SemanticMismatch, BuildFailed, RunFailed } import v2.std.verification { @@ -140,7 +142,10 @@ fn idempotent_operation_eval_context() -> EvalContext { }, bind: BindInterpreter { bind_value: idempotent_operation_bind_value - } + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm + } }, structure_witness: idempotent_operation_interpretation_structure_witness() ) diff --git a/src/v2/test/claim/generated/language_behavior_equivalence.dag b/src/v2/test/claim/generated/language_behavior_equivalence.dag index e98096ec311..b8da1f9ede2 100644 --- a/src/v2/test/claim/generated/language_behavior_equivalence.dag +++ b/src/v2/test/claim/generated/language_behavior_equivalence.dag @@ -45,7 +45,9 @@ import v2.std.runtime { RuntimePrimitiveValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.witness { Holds, Violates } @@ -182,7 +184,10 @@ fn lbe_eval_context() -> EvalContext { }, bind: BindInterpreter { bind_value: lbe_bind_value - } + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm + } }, structure_witness: lbe_interpretation_structure_witness() ) diff --git a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag index 140821e8f4c..11b4576024d 100644 --- a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag +++ b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag @@ -62,7 +62,9 @@ import v2.std.runtime { RuntimeUnitValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.verification { EqualsClaim, @@ -350,6 +352,9 @@ fn subsumption_interpretation() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: subsumption_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } diff --git a/src/v2/test/claim/manual/eval_runtime.dag b/src/v2/test/claim/manual/eval_runtime.dag index 5d9a4fa9772..cbaa91b59b1 100644 --- a/src/v2/test/claim/manual/eval_runtime.dag +++ b/src/v2/test/claim/manual/eval_runtime.dag @@ -61,7 +61,9 @@ import v2.std.runtime { RuntimeUnitValue, RuntimeValue, ValueInterpreter, - ValueRepresentationModel + ValueRepresentationModel, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.machine { Byte } import v2.std.node { @@ -257,6 +259,9 @@ fn eval_interpretation_algebra() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: eval_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } diff --git a/src/v2/test/claim/manual/test_claim_cache_digest_sensitivity.dag b/src/v2/test/claim/manual/test_claim_cache_digest_sensitivity.dag index bfbd4453831..2f220104570 100644 --- a/src/v2/test/claim/manual/test_claim_cache_digest_sensitivity.dag +++ b/src/v2/test/claim/manual/test_claim_cache_digest_sensitivity.dag @@ -47,7 +47,9 @@ import v2.std.runtime { RuntimeUnitValue, RuntimeValue, TransformInterpreter, - ValueInterpreter + ValueInterpreter, + MatchInterpreter, + runtime_reject_match_arm } import v2.std.integer { int_add, int_mul, int_negate } import v2.std.node { @@ -410,6 +412,9 @@ fn tcc_interp_stub_allocate_body() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: v2_eval_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } @@ -430,6 +435,9 @@ fn tcc_interp_stub_call_body() -> InterpretationAlgebra { }, bind: BindInterpreter { bind_value: v2_eval_bind_value + }, + match: MatchInterpreter { + choose_arm: runtime_reject_match_arm } } } From 7093996c135370ce73191c7d8f4ad99a62f4ef1b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 22:37:00 +0000 Subject: [PATCH 27/28] WIP: v2 memory control audit --- .../claim/manual/bash_command_fold_runner.dag | 182 ++++++++++++------ .../manual/fold_call_closure_emit_test.dag | 4 +- .../manual/gha_workflow_yaml_fold_runner.dag | 14 +- .../manual/sql_create_table_fold_runner.dag | 32 +-- 4 files changed, 154 insertions(+), 78 deletions(-) diff --git a/src/v2/test/claim/manual/bash_command_fold_runner.dag b/src/v2/test/claim/manual/bash_command_fold_runner.dag index 70cc842bcf3..48078db77cb 100644 --- a/src/v2/test/claim/manual/bash_command_fold_runner.dag +++ b/src/v2/test/claim/manual/bash_command_fold_runner.dag @@ -1,6 +1,6 @@ module v2.test.manual.bash_command_fold_runner -import std.realization_schedule { Runnable, RunnableSingleClaim } +import std.realization_schedule { Runnable, RunnableSingleClaim, runnable_resource_profile_negligible } import v2.std.collection { List } data bash_fold_test_entry: String = "src/v2/test/claim/bash_command_fold_test.dag" @@ -10,243 +10,303 @@ fn bash_command_fold_plan() -> List> { [ RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_relation_row_true_witness_holds" + function: "bash_fold_relation_row_true_witness_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_command_single_lit_true_holds" + function: "bash_fold_command_single_lit_true_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_command_multi_lit_echo_hi_holds" + function: "bash_fold_command_multi_lit_echo_hi_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_command_var_ref_x_holds" + function: "bash_fold_command_var_ref_x_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_command_arbitrary_grep_triple_holds" + function: "bash_fold_command_arbitrary_grep_triple_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_command_arbitrary_var_home_holds" + function: "bash_fold_command_arbitrary_var_home_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_command_arbitrary_lit_quote_escape_holds" + function: "bash_fold_command_arbitrary_lit_quote_escape_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_wrong_production_rejects_oracle_holds" + function: "bash_fold_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_direct_serialize_single_lit_true_holds" + function: "bash_fold_direct_serialize_single_lit_true_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_direct_serialize_multi_lit_echo_hi_holds" + function: "bash_fold_direct_serialize_multi_lit_echo_hi_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_direct_serialize_var_ref_x_holds" + function: "bash_fold_direct_serialize_var_ref_x_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_emitted_tree_differs_on_wrong_fixture_holds" + function: "bash_fold_emitted_tree_differs_on_wrong_fixture_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_exit_code_42_holds" + function: "bash_fold_exit_code_42_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_exit_code_0_holds" + function: "bash_fold_exit_code_0_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_exit_wrong_production_rejects_oracle_holds" + function: "bash_fold_exit_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_assign_lit_foo_bar_holds" + function: "bash_fold_assign_lit_foo_bar_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_assign_var_x_home_holds" + function: "bash_fold_assign_var_x_home_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_assign_lit_quote_escape_holds" + function: "bash_fold_assign_lit_quote_escape_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_assign_wrong_production_rejects_oracle_holds" + function: "bash_fold_assign_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_and_then_true_false_holds" + function: "bash_fold_and_then_true_false_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_or_else_true_false_holds" + function: "bash_fold_or_else_true_false_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_pipe_echo_hi_wc_holds" + function: "bash_fold_pipe_echo_hi_wc_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_and_then_wrong_production_rejects_oracle_holds" + function: "bash_fold_and_then_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_pipe_wrong_production_rejects_oracle_holds" + function: "bash_fold_pipe_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_pipe_and_then_left_holds" + function: "bash_fold_pipe_and_then_left_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_pipe_three_stage_holds" + function: "bash_fold_pipe_three_stage_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_subshell_true_holds" + function: "bash_fold_subshell_true_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_subshell_multi_stmt_holds" + function: "bash_fold_subshell_multi_stmt_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_subshell_nested_and_then_holds" + function: "bash_fold_subshell_nested_and_then_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_if_true_then_echo_holds" + function: "bash_fold_if_true_then_echo_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_if_multi_then_holds" + function: "bash_fold_if_multi_then_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_if_then_pipe_soundness_holds" + function: "bash_fold_if_then_pipe_soundness_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_subshell_wrong_production_rejects_oracle_holds" + function: "bash_fold_subshell_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_if_wrong_production_rejects_oracle_holds" + function: "bash_fold_if_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_stderr_null_holds" + function: "bash_fold_with_redir_stderr_null_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_stdout_and_stderr_null_holds" + function: "bash_fold_with_redir_stdout_and_stderr_null_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_stdout_to_stderr_holds" + function: "bash_fold_with_redir_stdout_to_stderr_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_redir_to_file_var_holds" + function: "bash_fold_with_redir_redir_to_file_var_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_heredoc_holds" + function: "bash_fold_heredoc_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_wrong_spellings_rejects_oracle_holds" + function: "bash_fold_with_redir_wrong_spellings_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_heredoc_wrong_spellings_rejects_oracle_holds" + function: "bash_fold_heredoc_wrong_spellings_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_wrong_production_rejects_oracle_holds" + function: "bash_fold_with_redir_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_heredoc_wrong_production_rejects_oracle_holds" + function: "bash_fold_heredoc_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_with_redir_pipe_soundness_holds" + function: "bash_fold_with_redir_pipe_soundness_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_orch_emit_holds" + function: "bash_fold_raw_line_orch_emit_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_x_eq_holds" + function: "bash_fold_raw_line_x_eq_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_cmdsubst_holds" + function: "bash_fold_raw_line_cmdsubst_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_paren_holds" + function: "bash_fold_raw_line_paren_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_quoted_holds" + function: "bash_fold_raw_line_quoted_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_mktemp_holds" + function: "bash_fold_raw_line_mktemp_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_trailing_nl_holds" + function: "bash_fold_raw_line_trailing_nl_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_wrong_spellings_rejects_oracle_holds" + function: "bash_fold_raw_line_wrong_spellings_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_raw_line_wrong_production_rejects_oracle_holds" + function: "bash_fold_raw_line_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_negation_subshell_false_holds" + function: "bash_fold_negation_subshell_false_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_negation_subshell_rawline_holds" + function: "bash_fold_negation_subshell_rawline_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_negation_wrong_spellings_rejects_oracle_holds" + function: "bash_fold_negation_wrong_spellings_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_negation_wrong_production_rejects_oracle_holds" + function: "bash_fold_negation_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_env_prefixed_lit_t_holds" + function: "bash_fold_env_prefixed_lit_t_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_env_prefixed_wrong_spellings_rejects_oracle_holds" + function: "bash_fold_env_prefixed_wrong_spellings_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: bash_fold_test_entry, - function: "bash_fold_env_prefixed_wrong_production_rejects_oracle_holds" + function: "bash_fold_env_prefixed_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() } ] ] diff --git a/src/v2/test/claim/manual/fold_call_closure_emit_test.dag b/src/v2/test/claim/manual/fold_call_closure_emit_test.dag index 45e4d6ca2ff..0b0a36046da 100644 --- a/src/v2/test/claim/manual/fold_call_closure_emit_test.dag +++ b/src/v2/test/claim/manual/fold_call_closure_emit_test.dag @@ -49,6 +49,7 @@ import v2.std.compilers.target_model { value_expr_projection_bundle_node } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -186,7 +187,8 @@ fn fold_call_target_model() -> TargetModel { lex: ts_fn_add_lex_rules(), binding_spellings: ts_binding_spellings(), token_class_emit_transforms: target_model_emit_transforms_empty, - authority_source_text: ts_source_text_authority() + authority_source_text: ts_source_text_authority(), + runtime_row: target_emit_host_runtime_row_unconfigured } } diff --git a/src/v2/test/claim/manual/gha_workflow_yaml_fold_runner.dag b/src/v2/test/claim/manual/gha_workflow_yaml_fold_runner.dag index 7b0a2f3b793..d3825016ffc 100644 --- a/src/v2/test/claim/manual/gha_workflow_yaml_fold_runner.dag +++ b/src/v2/test/claim/manual/gha_workflow_yaml_fold_runner.dag @@ -1,6 +1,6 @@ module v2.test.manual.gha_workflow_yaml_fold_runner -import std.realization_schedule { Runnable, RunnableSingleClaim } +import std.realization_schedule { Runnable, RunnableSingleClaim, runnable_resource_profile_negligible } import v2.std.collection { List } data gha_fold_structural_test_entry: String = "src/v2/test/claim/gha_workflow_yaml_fold_structural_test.dag" @@ -12,19 +12,23 @@ fn gha_workflow_yaml_fold_plan() -> List> { [ RunnableSingleClaim { entry: gha_fold_structural_test_entry, - function: "gha_fold_relation_row_job_witness_holds" + function: "gha_fold_relation_row_job_witness_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: gha_fold_serialize_test_entry, - function: "gha_fold_pilot_job_byte_identical_holds" + function: "gha_fold_pilot_job_byte_identical_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: gha_fold_serialize_test_entry, - function: "gha_fold_wrong_production_rejects_oracle_holds" + function: "gha_fold_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: gha_fold_serialize_test_entry, - function: "gha_fold_flat_steps_perturbation_rejects_oracle_holds" + function: "gha_fold_flat_steps_perturbation_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() } ] ] diff --git a/src/v2/test/claim/manual/sql_create_table_fold_runner.dag b/src/v2/test/claim/manual/sql_create_table_fold_runner.dag index f94891d197d..3dc834a105a 100644 --- a/src/v2/test/claim/manual/sql_create_table_fold_runner.dag +++ b/src/v2/test/claim/manual/sql_create_table_fold_runner.dag @@ -1,6 +1,6 @@ module v2.test.manual.sql_create_table_fold_runner -import std.realization_schedule { Runnable, RunnableSingleClaim } +import std.realization_schedule { Runnable, RunnableSingleClaim, runnable_resource_profile_negligible } import v2.std.collection { List } data sql_fold_test_entry: String = "src/v2/test/claim/sql_create_table_fold_test.dag" @@ -10,43 +10,53 @@ fn sql_create_table_fold_plan() -> List> { [ RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_relation_row_single_col_witness_holds" + function: "sql_fold_relation_row_single_col_witness_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_create_table_single_col_holds" + function: "sql_fold_create_table_single_col_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_create_table_two_col_holds" + function: "sql_fold_create_table_two_col_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_create_table_with_pk_holds" + function: "sql_fold_create_table_with_pk_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_wrong_production_rejects_oracle_holds" + function: "sql_fold_wrong_production_rejects_oracle_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_direct_serialize_single_col_holds" + function: "sql_fold_direct_serialize_single_col_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_oracle_rejects_unsupported_drop_table_holds" + function: "sql_fold_oracle_rejects_unsupported_drop_table_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_oracle_rejects_parameterized_numeric_type_holds" + function: "sql_fold_oracle_rejects_parameterized_numeric_type_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_two_col_uses_recursive_list_production_holds" + function: "sql_fold_two_col_uses_recursive_list_production_holds", + profile: runnable_resource_profile_negligible() }, RunnableSingleClaim { entry: sql_fold_test_entry, - function: "sql_fold_single_col_uses_leaf_list_production_holds" + function: "sql_fold_single_col_uses_leaf_list_production_holds", + profile: runnable_resource_profile_negligible() } ] ] From 95f706298d2203c69acf8bae42fd6547674e2a42 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 22:50:27 +0000 Subject: [PATCH 28/28] WIP: v2 memory control audit --- .../claim/generated/language_behavior_equivalence.dag | 5 ++--- .../cross_language_add_python_to_typescript_test.dag | 7 ++++--- src/v2/test/claim/manual/ingest_bridge_test.dag | 7 ++++--- .../manual/validate_then_compile_public_terminal.dag | 8 ++++---- 4 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/v2/test/claim/generated/language_behavior_equivalence.dag b/src/v2/test/claim/generated/language_behavior_equivalence.dag index b8da1f9ede2..dc19f1e3bcb 100644 --- a/src/v2/test/claim/generated/language_behavior_equivalence.dag +++ b/src/v2/test/claim/generated/language_behavior_equivalence.dag @@ -30,8 +30,7 @@ import v2.std.diagnostic { Outcome, Rejected, Unavailable, - diagnostics_singleton -} + diagnostics_singleton, node_locus } import v2.std.node { Atom, Hash, Node, Symbol, TypeNode, SyntheticOccurrence } import v2.std.runtime { BindInterpreter, @@ -102,7 +101,7 @@ fn lbe_runtime_value() -> RuntimeValue { fn lbe_runtime_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: ^lbe_interpretation_rejected, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: AmbiguousIntent } } } diff --git a/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag b/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag index 3889592a55e..1848d5f012b 100644 --- a/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag +++ b/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag @@ -53,6 +53,7 @@ import v2.std.verification { manual_claim_anchor } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.effects { atom_node } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -216,8 +217,8 @@ fn cross_language_bridge_realized_input(ok: Bool) -> Symbol { data claim_cross_language_add_python_to_typescript_module_compiles: TestClaim = CompilesClaim { label: "manual/cross_language: python->ts add-slice end-to-end matrix claim compiles", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - input: ^ingest_bridge_hermetic_fixture_parse_tree, - expected_value: ^ingest_bridge_hermetic_fixture_parse_tree, + input: atom_node(s: ^ingest_bridge_hermetic_fixture_parse_tree), + expected_value: atom_node(s: ^ingest_bridge_hermetic_fixture_parse_tree), classification: TestClassification { tier: Tier1, layer: Integration } } @@ -225,6 +226,6 @@ data claim_cross_language_parse_tree_bridge_realized: TestClaim = CompilesClaim label: "manual/cross_language: ParseTree->TargetModel bridge realized (#4801) — typed check Holds (was fail-closed)", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), input: cross_language_bridge_realized_input(ok: parse_tree_to_target_model_bridge_realized()), - expected_value: ^cross_language_bridge_realized, + expected_value: atom_node(s: ^cross_language_bridge_realized), classification: TestClassification { tier: Tier1, layer: Unit } } diff --git a/src/v2/test/claim/manual/ingest_bridge_test.dag b/src/v2/test/claim/manual/ingest_bridge_test.dag index ae700418a22..e28732ea2c7 100644 --- a/src/v2/test/claim/manual/ingest_bridge_test.dag +++ b/src/v2/test/claim/manual/ingest_bridge_test.dag @@ -61,6 +61,7 @@ import v2.std.verification { manual_claim_anchor } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.effects { atom_node } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -279,8 +280,8 @@ fn ingest_bridge_realized_input(ok: Bool) -> Symbol { data claim_ingest_bridge_module_compiles: TestClaim = CompilesClaim { label: "manual/ingest_bridge: forward interpreter bridge claim compiles", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - input: ^ingest_fixture_start, - expected_value: ^ingest_fixture_start, + input: atom_node(s: ^ingest_fixture_start), + expected_value: atom_node(s: ^ingest_fixture_start), classification: TestClassification { tier: Tier1, layer: Integration } } @@ -288,6 +289,6 @@ data claim_ingest_bridge_realized: TestClaim = CompilesClaim { label: "manual/ingest_bridge: ParseTree frontier -> forward-selected emit-side core node -> canonical IR by execution (Option A; row-driven, fail-closed, forward-deterministic)", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), input: ingest_bridge_realized_input(ok: ingest_bridge_realized()), - expected_value: ^ingest_bridge_realized, + expected_value: atom_node(s: ^ingest_bridge_realized), classification: TestClassification { tier: Tier1, layer: Integration } } diff --git a/src/v2/test/claim/manual/validate_then_compile_public_terminal.dag b/src/v2/test/claim/manual/validate_then_compile_public_terminal.dag index 970cdafc44f..2791044aee8 100644 --- a/src/v2/test/claim/manual/validate_then_compile_public_terminal.dag +++ b/src/v2/test/claim/manual/validate_then_compile_public_terminal.dag @@ -118,15 +118,15 @@ fn claim_rejecting_lens_is_compile_lens_gate_rejected( data claim_validate_then_compile_module_compiles: TestClaim = CompilesClaim { label: "manual/validate_then_compile: validate_then_compile public terminal module compiles", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - input: ^claim_validate_then_compile_module, - expected_value: ^claim_validate_then_compile_module, + input: claim_symbol_node(s: ^claim_validate_then_compile_module), + expected_value: claim_symbol_node(s: ^claim_validate_then_compile_module), classification: TestClassification { tier: Tier1, layer: Unit } } data claim_empty_lenses_skips_gate: TestClaim = EqualsClaim { label: "manual/validate_then_compile: empty lens list does not compile_lens_gate_reject (infer/compile-core Rejected OK)", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: ^claim_validate_then_compile_module, + lhs: claim_symbol_node(s: ^claim_validate_then_compile_module), rhs: claim_validate_then_compile_skips_gate_passes(), classification: TestClassification { tier: Tier1, layer: Unit } } @@ -148,7 +148,7 @@ fn claim_validate_then_compile_skips_gate_passes() -> Node { data claim_rejecting_lens_blocks_before_compile: TestClaim = EqualsClaim { label: "manual/validate_then_compile: required lens Rejected blocks before compile-core", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: ^claim_validate_then_compile_module, + lhs: claim_symbol_node(s: ^claim_validate_then_compile_module), rhs: claim_rejecting_lens_blocks_passes(), classification: TestClassification { tier: Tier1, layer: Unit } }