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

src/v4/std/runtime.dag

@@ -80,6 +80,45 @@ type RuntimeValueNodeProjection
   = RuntimeValueNodeProjected { node: Node }
   | RuntimeValueNodeUnrepresentable
 
+// ctrl#1533 M-C at the v4.std authority (placement per ctrl#1534 §3.3):
+// identity-of-values laws the hosts implementing RuntimeValue must obey.
+// Grounded in referential transparency of the total λ-fragment (INVARIANTS
+// P1 kernel-calculus worked example): a value denotes its structure, so two
+// references to one allocation cannot disagree — identity-of-values is a
+// theorem there, not a choice.
+//
+// Law 1 (soundness, one-way): reference-identical ⇒ structurally equal.
+//   Reference-distinct implies NOTHING. This is what licenses a host to
+//   short-circuit deep equality on shared subtrees (and what the v2 pure-call
+//   memo and CanonKey address-keying already rely on implicitly).
+// Law 2 (order-independence): equality and hashing of keyed aggregates are
+//   functions of the entry SET — the same entries yield equal values and
+//   equal hashes regardless of insertion or iteration order
+//   (hash_fields_commutative in the v2 host implements this).
+// Executable witnesses: v4.test.claim.std_grounding.value_carrier_laws —
+// these must stay green across any carrier swap (ctrl#1533 phase-2 gate).
+//
+// 🟢 terminal — Practice 4 (docs/modeling-discipline.md §4) — variant-is-data
+// (pattern 3) already applied: a three-arm sum (ReferenceIdentical /
+// StructurallyEqual / StructurallyDistinct) would let an inhabitant claim
+// reference identity WITHOUT structural equality; folding the structural
+// verdict into a Bool payload makes Law 1 hold by construction —
+// ReferenceIdentical carries no equal:false arm to violate it. Remaining
+// arms are mutually exclusive observations (how identity was established),
+// not coordinates. Patterns 1,2,4,5 N/A.
+type IdentityEvidence
+  = ReferenceIdentical
+  | StructurallyCompared { equal: Bool }
+
+// Law-1 projection: the equality verdict an IdentityEvidence licenses.
+// Reference identity short-circuits to true — that IS Law 1.
+fn identity_evidence_equal(evidence: IdentityEvidence) -> Bool {
+  match evidence {
+    ReferenceIdentical => true
+    StructurallyCompared { equal: eq } => eq
+  }
+}
+
 fn runtime_value_resolved_type(value: RuntimeValue) -> Node {
   match value {
     RuntimePrimitive { value: p } => p.primitive_type

src/v4/std/value_carrier.dag

@@ -0,0 +1,94 @@
+// src/v4/std/value_carrier.dag
+// Scope: declared structural-persistence and sharing facts for the runtime
+//   collection carriers — ctrl#1533 M-A, placed at the v4.std authority per
+//   the ctrl#1534 placement amendment (§3–4). The v2 host interpreter
+//   IMPLEMENTS these facts (ctrl#1533 phase 2); emitted Rust implements the
+//   same facts by ownership analysis (move + copy-on-write). Neither layer is
+//   the authority; this module is.
+// Status: model-first. Phase-0 receipts (gunbc PR #4653): v4 workloads make
+//   zero native mutation-primitive calls — v4 collections are closure-chain
+//   maps and FreeMonoid trees, so the host copy cost rides the
+//   free_monoid_to_vec flatten chokepoint. The carrier facts below are the
+//   "unified runtime representation" the B-LIST-FREEMONOID-1 and
+//   B-MAP-LOOKUP-OPTION-C-1 interims (v4.std.collection) dissolve against.
+// Anchors: Driscoll–Sarnak–Sleator–Tarjan, "Making Data Structures
+//   Persistent" (JCSS 1989); Okasaki, "Purely Functional Data Structures"
+//   (1998); Bagwell, "Ideal Hash Trees" (2001); Bagwell & Rompf, "RRB-Trees"
+//   (2011). Production consensus: Clojure/Scala collections; Rust im/rpds.
+
+module v4.std.value_carrier
+
+import v4.std.node { Symbol }
+
+// Structural persistence of a value carrier under update: a Persistent
+// carrier leaves every prior version valid (the new version structurally
+// shares unchanged substructure with its predecessor); an Ephemeral carrier
+// invalidates the prior version, so an immutable-value host must copy it in
+// full before updating — the quadratic-allocation term ctrl#1533 measured.
+// Distinct concept from std.compute_fabric.PersistenceKind (storage
+// durability across restarts): same word, different DAG-ancestor — this one
+// hangs off value-update semantics, not infrastructure lifecycle.
+// 🟢 terminal — Practice 4 (docs/modeling-discipline.md §4) — the distinction
+// is grounded in external authority (Driscoll–Sarnak–Sleator–Tarjan 1989's
+// definition of a persistent structure), not an interim of ours. Step-2: the
+// arms are mutually exclusive properties of one carrier under update, not
+// coordinates over another axis. Patterns 1–5 N/A: no payloads to unify, no
+// richer named source; the carrier itself is an external structure referenced
+// by Symbol, so there is nothing here to dissolve into.
+type PersistenceKind = Ephemeral | Persistent
+
+// Symbolic work bounds in the std.primitives PrimitiveContract `work`
+// convention (n = collection size). Declared per carrier so per-primitive
+// cost facts (ctrl#1533 M-B) derive from the carrier instead of floating.
+type CarrierCost {
+  update_work: String
+  lookup_work: String
+}
+
+// A carrier declaration binds an abstract collection to the host structure
+// implementing it, its persistence kind, and the cost facts that persistence
+// kind grounds. The interpreter and emitted code are both implementations of
+// these declarations; disagreement about update cost resolves by reading the
+// data values below, not by reading host source.
+type CarrierDeclaration {
+  collection: Symbol
+  carrier: Symbol
+  persistence: PersistenceKind
+  cost: CarrierCost
+}
+
+// Map<K,V> carrier: hash array mapped trie (Bagwell 2001), persistent per
+// Driscoll–Sarnak–Sleator–Tarjan 1989.
+data map_carrier: CarrierDeclaration = {
+  collection: ^map_collection,
+  carrier: ^hash_array_mapped_trie,
+  persistence: Persistent,
+  cost: { update_work: "log32 n", lookup_work: "log32 n" }
+}
+
+// List<T> carrier: relaxed radix balanced tree (Bagwell & Rompf 2011) or a
+// catenable structure consistent with FreeMonoid<T> (Okasaki 1998) — the
+// carrier must realize the FreeMonoid algebra without per-site flattening
+// (the free_monoid_to_vec chokepoint the phase-0 receipts identified as the
+// actual copy path on v4 workloads).
+data list_carrier: CarrierDeclaration = {
+  collection: ^list_collection,
+  carrier: ^relaxed_radix_balanced_tree,
+  persistence: Persistent,
+  cost: { update_work: "log n", lookup_work: "log n" }
+}
+
+// The sharing law: structural sharing between values is UNOBSERVABLE at the
+// language level. A value denotes its structure alone; whether two
+// structurally equal values occupy one allocation or two changes cost, never
+// meaning. This law is what makes a carrier swap behavior-preserving by
+// construction, and it is the claim the ctrl#1533 phase-2 verification must
+// keep green. Host values are thread-confined (Rc-discipline): sharing never
+// introduces concurrent observation, so the law has no hidden
+// synchronization premise.
+//
+// The law is declared as EXECUTABLE WITNESSES, not a data type
+// (v4.test.claim.std_grounding.value_carrier_laws): a sharing-receipt type
+// would have no constructor until the phase-2 swap lands, and dead vocabulary
+// is the Practice-4 failure mode. If phase 2 needs a receipt, it lands with
+// its first producer.

src/v4/test/claim/std_grounding/value_carrier_laws.dag

@@ -0,0 +1,137 @@
+// src/v4/test/claim/std_grounding/value_carrier_laws.dag
+// Scope: executable witnesses for the value-carrier laws (ctrl#1533 M-A
+//   sharing law, M-C identity laws; authority: v4.std.value_carrier and
+//   v4.std.runtime.IdentityEvidence). These are the behavior-preservation
+//   gate for the ctrl#1533 phase-2 host carrier swap: every witness here must
+//   hold under the current host AND under any replacement carrier.
+// Discovery: T-22 runner enumerates src/v4/test/claim/** recursively.
+
+module v4.test.claim.std_grounding.value_carrier_laws
+
+import v4.std.collection { empty_map, map_insert }
+import v4.std.runtime { ReferenceIdentical, StructurallyCompared, identity_evidence_equal }
+import v4.std.value_carrier { Ephemeral, Persistent, list_carrier, map_carrier }
+import v4.std.verification { BoolWitness, BoolWitnessClaim, UnifiedTestClaim }
+
+// ── Sharing law (M-A): sharing is unobservable ────────────────────────────
+// An aliased value (one allocation reachable twice) and a freshly built
+// structural twin are indistinguishable by language-level observation.
+
+fn sharing_unobservable_list_holds() -> Bool {
+  let shared = [1, 2, 3]
+  let aliased = concat(shared, shared)
+  let fresh = [1, 2, 3, 1, 2, 3]
+  aliased == fresh
+}
+
+fn sharing_unobservable_map_holds() -> Bool {
+  let base = empty_map() |> map_insert("k", 1)
+  let alias = base
+  alias == (empty_map() |> map_insert("k", 1))
+}
+
+// ── Identity law 2 (M-C): keyed-aggregate equality is order-independent ──
+// The same entries yield equal maps regardless of insertion order.
+
+fn map_equality_insert_order_independent_holds() -> Bool {
+  let abc = empty_map() |> map_insert("a", 1) |> map_insert("b", 2) |> map_insert("c", 3)
+  let cba = empty_map() |> map_insert("c", 3) |> map_insert("b", 2) |> map_insert("a", 1)
+  let bca = empty_map() |> map_insert("b", 2) |> map_insert("c", 3) |> map_insert("a", 1)
+  (abc == cba) && (abc == bca)
+}
+
+// Upsert is last-write-wins independent of the path taken to the same final
+// entry set (the lattice-meet grounding from std.effects).
+fn map_equality_overwrite_path_independent_holds() -> Bool {
+  let direct = empty_map() |> map_insert("a", 2)
+  let overwritten = empty_map() |> map_insert("a", 1) |> map_insert("a", 2)
+  direct == overwritten
+}
+
+// ── FreeMonoid representation law: association shape is unobservable ─────
+// List<T> = FreeMonoid<T>: differently associated concatenations of the same
+// element sequence are EQUAL values. This is the law that lets a carrier keep
+// concatenation as structure (no per-site flattening through the
+// free_monoid_to_vec chokepoint — the actual copy path phase-0 measured).
+fn freemonoid_association_unobservable_holds() -> Bool {
+  let left_assoc = concat(concat([1], [2]), [3])
+  let right_assoc = concat([1], concat([2], [3]))
+  let flat = [1, 2, 3]
+  (left_assoc == flat) && (right_assoc == flat)
+}
+
+// ── Identity law 1 (M-C): reference-identical ⇒ structurally equal ───────
+// By the variant-is-data shape of IdentityEvidence, ReferenceIdentical has no
+// equal:false arm; the projection makes the short-circuit explicit.
+fn identity_law1_projection_holds() -> Bool {
+  let ref_identical = identity_evidence_equal(evidence: ReferenceIdentical)
+  let compared_equal = identity_evidence_equal(evidence: StructurallyCompared { equal: true })
+  let compared_distinct = identity_evidence_equal(evidence: StructurallyCompared { equal: false })
+  ref_identical && compared_equal && !compared_distinct
+}
+
+// ── Carrier declarations are persistent (M-A data values resolve) ────────
+fn declared_carriers_are_persistent_holds() -> Bool {
+  let map_persistent = match map_carrier.persistence {
+    Persistent => true
+    Ephemeral => false
+  }
+  let list_persistent = match list_carrier.persistence {
+    Persistent => true
+    Ephemeral => false
+  }
+  map_persistent && list_persistent
+}
+
+// ── Glob-discovery registrations (consolidation #4553 Phase 2) ────────────
+// Co-located BoolWitnessClaim markers so discovery finds each witness
+// without a central roster.
+
+data unified_claim_sharing_unobservable_list: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: sharing_unobservable_list_holds
+  }
+}
+
+data unified_claim_sharing_unobservable_map: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: sharing_unobservable_map_holds
+  }
+}
+
+data unified_claim_map_equality_insert_order_independent: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: map_equality_insert_order_independent_holds
+  }
+}
+
+data unified_claim_map_equality_overwrite_path_independent: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: map_equality_overwrite_path_independent_holds
+  }
+}
+
+data unified_claim_freemonoid_association_unobservable: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: freemonoid_association_unobservable_holds
+  }
+}
+
+data unified_claim_identity_law1_projection: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: identity_law1_projection_holds
+  }
+}
+
+data unified_claim_declared_carriers_are_persistent: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/std_grounding/value_carrier_laws.dag",
+    function: declared_carriers_are_persistent_holds
+  }
+}