model(v4): ctrl#1533 phase-1 — value-carrier declarations (M-A) + identity laws (M-C) with executable witnesses

[briansrls]

Summary

Phase 1 (modeling) of ctrl#1533 (persistent-structures value representation), placed at the v4.std authority per the ctrl#1534 placement amendment (§3–4). Model-first: no host behavior changes — this PR declares the facts the phase-2 host carrier swap must implement and the laws it must preserve.

• M-A — carrier declarations (src/v4/std/value_carrier.dag, new): PersistenceKind (Ephemeral | Persistent — disambiguated from std.compute_fabric.PersistenceKind, which is storage durability), CarrierCost, CarrierDeclaration, and the two data values map_carrier (HAMT, Bagwell 2001) and list_carrier (RRB tree, Bagwell & Rompf 2011 — must realize the FreeMonoid algebra without per-site flattening). This is the "unified runtime representation" that the B-LIST-FREEMONOID-1 / B-MAP-LOOKUP-OPTION-C-1 interims dissolve against. The sharing law (sharing is unobservable) is declared as executable witnesses rather than a receipt type — a receipt type would have no constructor until phase 2 lands, and dead vocabulary is the Practice-4 failure mode.
• M-C — identity laws (src/v4/std/runtime.dag): IdentityEvidence = ReferenceIdentical | StructurallyCompared { equal: Bool } plus the identity_evidence_equal projection. Variant-is-data shape makes Law 1 (reference-identical ⇒ structurally equal) hold by construction — ReferenceIdentical has no equal: false arm to violate it. Law 2 (keyed-aggregate equality/hash are order-independent) is documented at the type and witnessed below.
• Executable law witnesses (src/v4/test/claim/std_grounding/value_carrier_laws.dag, new): 7 Bool witnesses with co-located UnifiedTestClaim glob-discovery registrations — sharing unobservability (list + map), insert-order / overwrite-path independence of map equality, FreeMonoid association unobservability, Law-1 projection, and carrier-declaration resolution. These are the behavior-preservation gate the phase-2 carrier swap must keep green.

Phase-0 receipts motivating the model (PR #4653, merged as c1cdc9b): v4 workloads make zero native mutation-builtin calls — copy cost rides the free_monoid_to_vec flatten chokepoint (185 calls / 770 items on the 7-witness gate); 21.8 MB / 219K allocations retained; 31.8K un-interned Strings.

Scope note: M-B (per-primitive cost facts on PrimitiveContract) and M-D (interning facts) are deferred to a follow-up PR — the PrimitiveContract extension shape deserves its own review.

Practice-4 disposition marks applied to both new coproducts (PersistenceKind 🟢 terminal, grounded in Driscoll–Sarnak–Sleator–Tarjan 1989; IdentityEvidence 🟢 terminal, variant-is-data already applied).

Test plan

• claim_batch --entry src/v4/test/claim/std_grounding/value_carrier_laws.dag --functions <all 7> --claim-run — 7/7 PASS (post-merge of origin/main provenance wave-2).
• python3 scripts/check_v4_layering_imports.py — OK.
• scripts/v4-testclaim-smoke-roster.sh — run post-merge with rebuilt release binaries: 15/15 groups green at flip time, including comprep_eval_by_execution (a failure there observed mid-development was verified pre-existing at the merge base — reproduced with this branch's files absent — and is fixed by main's provenance wave-2: global SpanIndex coherence across memoized parse cells (F1 prov threading + F2 span_index_merge + F4 edit_locus off-tree consumer) #4654, now merged in). The run was still grinding through wave-2's edit_locus_source_provenance_affected_set_wire witness (15+ min at 100% CPU; untouched by this diff) when the PR flipped ready; CI is authoritative.
• scripts/v4-claim-corpus-execution-map.sh — running post-merge, 51+ witnesses executed with no failures at flip time.

[briansrls]

Re claude/opus-4-7 review (REQUEST_CHANGES):

Finding 1 (missing empty_map/map_insert imports) — valid, fixed in fe4d4c6. Added import v4.std.collection { empty_map, map_insert } per the convention in map_lookup_miss_witness_violates.dag. Worth noting the gate was never unresolved — all 7 witnesses passed by execution before and after the fix (the v2 interpreter resolves these as builtins) — but the explicit import is the v4 source convention and now matches the rest of test/claim/.

Finding 2 (method-style .concat on list literals) — valid, fixed in fe4d4c6. Rewrote to free-function concat(a, b) matching the exclusive usage in v4/std/node.dag. (The method form did resolve and pass by execution — the v2 interpreter desugars method calls on lists — but there is zero precedent for it in v4 sources, so the free form is right.)

Finding 3 (witnesses are structural restatements, advisory) — partially addressed, remainder is phase-2 scope by design. Strengthened the insert-order witness to 3 keys across 3 insertion orders in the same commit. On the broader point: these phase-1 witnesses pin the language-observable laws (equality/sharing/association semantics) before any host change exists — that's the model-first sequencing from ctrl#1533/#1534. A witness that could detect leaked reference identity or exercise large-n boundaries requires the phase-2 carrier swap to exist first; the phase-2 PR is required to extend this gate with swap-specific probes (and the phase-0 measurement harness from #4653 provides the allocation-level observability these Bool witnesses intentionally don't duplicate).

All 7 witnesses pass post-fix via claim_batch. — sent from neat-ibex-297