Repository navigation
model: ctrl#1533 phase-1 follow-up — M-B carrier-cost facts on PrimitiveContract + M-D name-interning declarations - #4666
Merged
Merged
Conversation
Context-scoped MutationCounters on the copy-on-update primitives (map_insert/merge/list_push/concat/set ops: calls + entries copied — the triangular/quadratic receipt), thread-local flatten counters on the free_monoid_to_vec chokepoint (fires inside Value::eq, so no ctx; two fixed-size integers, not a cache), and a sharing-aware retained-value byte accounting walk (per-variant counts/bytes, visited-set dedup) on InterpContext. claim_batch prints the report under GUNBC_INTERP_STATS=1. Receipt on the real v4 gate workload (7 affected_testgen witnesses, all PASS): native mutation primitives 0 calls — v4 collections are closure chains + FreeMonoid trees, so the host copy cost rides the flatten chokepoint, confirming ctrl PR #1534's layer analysis. Retained: 21.8 MB / 219K allocations (Record 12.7MB with 48K sharing hits; 31K un-interned Strings) — the M-D interning/positional-record receipt baseline. Read-only tooling per ctrl#1533 phase 0; no semantic change to any evaluation path (counters + opt-in report only). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…latten in claim_batch Review #28288 (cursor/composer-2.5) on #4653: the copy-work counters mixed definitions across dispatch paths, breaking the single-receipt property (P2). - One definition per counter, by operation semantics, not dispatch path: add-one ops (map_insert/list_push/set_insert) count the receiver's pre-existing entries; merge ops (map_merge/list_concat/set_union) count both operands' entries. Method .concat/.append/.push buckets by what the arg IS (collection -> concat, atomic -> push); binop + and builtins agree. - set_union gets its own row (was folded into set_insert — same P2 class). - builtin map_merge instrumented (was counted on the method path only). - claim_batch fm_flatten row is now a delta sampled across the witness loop, matching the context-scoped counters next to it. Tests pin the unified semantics: concat counts both operands (9 for the 3⊕1 then 4⊕1 chain), atomic append lands in list_push with receiver-only copy-work, and neither bucket leaks into the other. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…arrier_laws; strengthen insert-order witness to 3 keys Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…iveContract + M-D name-interning declarations M-B: PrimitiveContract gains carrier_cost: CarrierCostSensitivity. 12 carrier-sensitive primitives declare both arms (ephemeral = copy-before- update, what the v2 interpreter does today; persistent = the declared M-A carrier cost); 49 carrier-insensitive primitives marked explicitly. M-D: name-interning facts at the v4.std.value_carrier authority — type/ variant/field names are references into the resolved graph's declared name set; positional-record layout derives from this fact (phase 3 implements). New witness name_interning_covers_all_domains_holds (8/8 green). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
ctrl#1533 phase-1 follow-up: the two fact families deferred from #4660 — M-B (per-primitive carrier-cost facts) and M-D (name-interning facts). Model-only, no host behavior changes; this completes the phase-1 modeling so the phase-2 host carrier swap and phase-3 interning/positional-records land as implementations of declared facts.
dsl/std/primitives.dag):PrimitiveContractgainscarrier_cost: CarrierCostSensitivity = CarrierInsensitive | CarrierSensitive { ephemeral_work, persistent_work }. Per the M7 single-authority note in ctrl#1533, the facts live on the existing contract data values — no parallel cost table. 12 primitives are carrier-sensitive: the five mutation primitives the proposal names (map_insert,map_merge,list_push,concat,append) pluswith(record update — host-implemented as a map merge; Record sharing was 12.7 MB in the phase-0 receipts) and six reads whose cost the carrier changes (map_get,map_contains_key,lookup,get,first,last) — the read extension follows directly from M-A'sCarrierCost.lookup_work. The remaining 49 contracts are explicitlyCarrierInsensitive. The ephemeral arms are what the v2 interpreter does today (copy-before-update — the quadratic term phase 0 measured); the persistent arms agree with the M-A carrier declarations (log32 nHAMT /log nRRB) and are what phase 2 must implement. The existingwork/output_sizefields keep their historical convention (ownership-aware emitted-code path).src/v4/std/value_carrier.dag): type/variant/field names are drawn from closed, compile-time-known sets (M4: closed sets are enums, not strings) — declared asNameDomain(🟢 terminal) + threeNameInterningDeclarationdata values naming each domain's authority (the resolved graph's declared name set) and the host representation duty (interned_symbol_id; field names additionallypositional_slot_in_declared_field_order). The positional-record layout — the largest per-instance saving in the phase-0 receipts (31.8K un-interned Strings) — thereby derives from a declared fact rather than being a hand-rolled optimization. v4.std.runtime already encodes the fact structurally (RuntimeFieldValue.field: Symbol); the v2 host's owned-String names are the implementation gap phase 3 closes.name_interning_covers_all_domains_holds(one declaration perNameDomainarm) with co-located discovery registration — the suite is now 8/8 green.Both new coproducts (
CarrierCostSensitivity,NameDomain) carry 🟢 terminal Practice-4 marks with pattern-by-pattern justification.This completes phase 1 of ctrl#1533. Next: phase 2 (host carrier swap — HAMT/RRB behind the
Valueenum surface, gated on the value_carrier_laws witnesses staying green plus the phase-0 measurement delta) and phase 3 (interning + positional records, implementing M-D), independent of each other per the proposal.Test plan
claim_batch --entry src/v4/test/claim/std_grounding/value_carrier_laws.dag --functions <all 8> --claim-run— 8/8 PASS.std.primitivesmatchedmap_insert_contract/list_push_contract/fold_contractcarrier_costpayloads — PASS (entry not committed; M-B facts are dsl/std-side and outside the v4-only smoke runner's source root).cargo test -p v2-compiler-tests -- shared_primitives_parses_strict— ok (the strict-parse gate coveringdsl/std/primitives.dag).python3 scripts/check_v4_layering_imports.py— OK.dsl/std/primitives.dag(t_impossiblebugs_unenumerated_effects_test) asserts acontains("filesystem_read_contract")that is unaffected.