fix(v2): structural-key Map== via native data repr keyed by Value-equality authority by briansrls · Pull Request #4564 · gunb-ai/gunbc

briansrls · 2026-06-08T19:45:22Z

What

A finite Map<K,V> is a finite set of key→value pairs, so whole-map == is extensional set equality — decidable even for non-String keys. Previously a structural (non-String) key dropped the native Value::Map fast path into the .dag closure form Map { lookup: fn }, whose Closure field has no PartialEq arm, so any structural-key Map == was false even vs itself — the root cause of the false affected_set frontier == receipts (#4560 worked around it per-key).

Model decision

Map is realized natively as data keyed by CanonKey, which wraps the original key Value (so keys/iteration recover real keys) and:

Eq delegates to Value::eq — the single equality authority (P2). No parallel equality. Only Hash is derived, and it is made consistent with Value::eq: FreeMonoid alias (Str ≡ List ≡ Empty/Cons chain), +0.0 == -0.0, order-independent record/variant fields, type_name ignored (matching Value::eq).
A value is a valid key iff reflexive under Value::eq (v == v) — rejects closures / fn / NaN through the same authority.

Fail-closed boundaries (P3)

map_insert with an invalid key returns Err (was Ok(None) → silent fall-through to the closure form).
value_to_json returns Err on a non-String map key (no Display-collapse of Int(1) vs Str("1")).
match_pattern bridges a present coproduct value to Some { value: v } (symmetric with the existing non-Variant value→Some bridge) so std map_get's Some/None match works over native maps holding coproduct values.

Evidence (by execution)

The four affected_set Excluded/rerun receipts go red→green (excluded_propagation_proof, irt1_excluded_propagation_receipt, dimension_seed_rerun, irt1_dimension_seed_receipt).
New discriminating witness manual/map_structural_key_equality.dag (self-eq, equal-eq, distinct-key ≠, distinct-value ≠, shadow=latest), wired into v4_roster_pilot (also corrects a pre-existing roster row-count drift 42→44).
Suite-delta = 0: cargo test -p v2-compiler-tests is identical 571 pass / 24 pre-existing pipeline:: fails on HEAD and branch; map_lookup_dual_dispatch (incl. raw lookup builtin) green; fmt + clippy clean.

Scope note

Touches only src/v2/stage0/src/v2_interpreter.rs (bootstrap interpreter) + additive test claim. The std Map type stays the PartialFunction observation interface; full dissolution (a finite-relation std Map type) remains tracked load-bearing work.

🤖 Generated with Claude Code

briansrls

Review metadata

Provider / model: codex / unknown
Commit: dbb4e2c7 · Trigger: schedule
Thinking: 275s wall

BLOCKING (3)

Root Cause

src/v2/stage0/src/v2_interpreter.rs CanonKey hand-rolls a separate canonicalization instead of deriving from the same equality normalization used by Value::eq → normalize keys through one Value-equality canonical form or reject until that authority exists.
src/v2/stage0/src/v2_interpreter.rs eval_builtin conflates “not this builtin” with “this builtin saw invalid input” → return Err at the recognized native-map invalid-key boundary.
src/v2/stage0/src/v2_interpreter.rs value_to_json still assumes map keys are string-authoritative after this PR makes native maps structurally keyed → either reject non-string-key maps at the JSON boundary or encode them through an injective representation.

⚠️ The structural-map direction is right, but these key-authority and boundary cases need to be closed before merge.

Sign in to view

+                return false;
+            }
+            out.push('f');
+            out.push_str(&f.to_bits().to_string());


Sign in to view

+                    result.insert(ck, (*v).clone());
+                    Ok(Some(Value::Map(Rc::new(result))))
+                }
+                None => Ok(None),


Sign in to view

            let obj: serde_json::Map<String, serde_json::Value> = m
                .iter()
-                .map(|(k, v)| (k.clone(), value_to_json(v)))
+                .map(|(k, v)| (format!("{}", k.key), value_to_json(v)))


…ality authority A finite Map<K,V> is a finite set of key→value pairs, so whole-map `==` is extensional set equality — decidable even for non-String keys. Previously a structural (non-String) key dropped the native Value::Map fast path into the .dag closure form `Map { lookup: fn }`, whose Closure field has no PartialEq arm, so any structural-key `Map ==` was false (even a value vs itself) — the root cause of the false affected_set frontier `==` receipts. Native maps now key by CanonKey, which uses the original key Value as the key: - Eq DELEGATES to Value::eq (single equality authority, P2) — no parallel equality. Only Hash is derived, made consistent with Value::eq (FreeMonoid alias, +0.0==-0.0, order-independent record/variant fields, type_name ignored). - A value is a valid key iff reflexive under Value::eq (v == v); closures/fn/NaN are rejected through the same authority. map_insert fails closed (P3) on an invalid key instead of falling through to the closure form. - value_to_json fails closed (P3) on a non-String map key (no Display-collapse of distinct keys like Int(1) vs Str("1")). - match_pattern bridges a present coproduct value to `Some { value: v }` (symmetric with the existing non-Variant value→Some bridge), so std map_get's Some/None match works over a native map holding coproduct values. Greens the four affected_set Excluded/rerun receipts by execution (red→green), adds a discriminating witness (manual/map_structural_key_equality.dag) wired into v4_roster_pilot, and corrects a pre-existing roster row-count drift (42→44). Suite-delta = 0 (v2-compiler-tests: identical 571 pass / 24 pre-existing pipeline:: fails on HEAD and branch). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

briansrls · 2026-06-08T20:31:29Z

Addressed all 3 BLOCKING findings from the codex review (dbb4e2c7) — pushed in ab9efed1:

CanonKey was a second equality authority (P2) — fixed. CanonKey::Eq now delegates to Value::eq (self.key == other.key); the canonical-string encoding is gone. Only Hash is derived, and it is made consistent with Value::eq: +0.0/-0.0 normalize to the same bits, and the FreeMonoid alias is honored via free_monoid_to_vec so Str / List / Empty-Cons chains that flatten equally hash equally (records/variants hash field-commutatively, type_name omitted — matching Value::eq). Key validity is now v == v (reflexivity under the single authority), rejecting closures/fn/NaN. New witness asserts Int(1) key ≠ Str("1") key and +0.0/shadow cases.
map_insert conflated "not this builtin" with "invalid input" (P3) — fixed. A recognized native [Value::Map, k, v] with an unkeyable k now returns Err (fail-closed) instead of Ok(None); Ok(None) is reserved for a non-Map receiver.
value_to_json assumed string-authoritative keys (P3) — fixed. value_to_json is now fallible and returns Err on any non-String map key, so distinct keys can never collapse into one JSON object key.

Evidence: the four affected_set Excluded/rerun receipts go red→green by execution; map_lookup_dual_dispatch (incl. the raw lookup builtin returning Int(7)) stays green; cargo test -p v2-compiler-tests suite-delta = 0 (identical 571 pass / 24 pre-existing pipeline:: fails on HEAD vs branch); fmt + clippy clean.

briansrls · 2026-06-08T21:12:41Z

Valid finding — fixed (the Some bridge narrowing) plus a symmetric gap it surfaced.

1. Some bridge too broad (:1255) — narrowed. It now excludes the absent arms:
if name == "Some" && variant_name != "Some" && variant_name != "Violates" && variant_name != "None" && variant_name != "none". A Violates (or nominal None) no longer matches Some; it falls through to the None arm (via the Violates → None bridge / nominal None match), so an absent witness can never be fabricated as present (P3).

2. Symmetric value → Holds gap (regression your finding led me to) — fixed. Because native maps now return the raw present value (not Holds-wrapped), a -> Witness-annotated .lookup consumer matching Holds/Violates (e.g. parse_table_lookup, lookup_table) had a value → Some bridge but no value → Holds bridge → non-exhaustive match on: <present value>. I added the symmetric present-value → Holds bridge (Variant + non-Variant) with the same absent-arm exclusions; Null (miss) still routes to Violates. This was caught by map_lookup_miss_witness_violates (which the .dag roster runs but cargo test -p v2-compiler-tests does not).

Verification: map_lookup_miss_witness_violates green again; all 44 v4 roster claim-run witnesses pass; gunbc compile --source-root src/v4 = 0 diagnostics; v2-compiler-tests suite-delta = 0; fmt + clippy clean. Pushed in the latest commit on session/merry-stag-540.

— sent from merry-stag-540

briansrls

Review metadata

Provider / model: codex / unknown
Commit: d97fc792 · Trigger: schedule
Thinking: 332s wall

BLOCKING (1)

Root Cause

src/v2/stage0/src/v2_interpreter.rs structural-key membership canonicalization collapsed arity validation into key normalization → keep the one-argument diagnostic boundary, then call CanonKey::new on the provided key.

⚠️ One fail-closed regression remains in the new structural-key contains path.

Sign in to view

            Value::Map(m) => {
-                let key = expect_str(args.first(), "contains")?;
-                Ok(Value::Bool(m.contains_key(&key)))
+                let key = args.first().cloned().unwrap_or(Value::Null);


…canonicalization Addresses codex (d97fc79) BLOCKING: the structural-key `contains`/`has` path collapsed arity validation into key normalization — a missing key argument was silently coerced to `Value::Null` and answered as a membership result instead of a typed diagnostic (P3 fail-closed). Now arity is validated first (missing key → typed error), then the provided key is canonicalized via `CanonKey::new`; an un-keyable present key (closure/fn/NaN) cannot be a map member (insert rejects it) so it soundly answers false. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

briansrls · 2026-06-08T21:30:53Z

Status against the latest HEAD (df7e3f08):

contains/has missing-arg (codex d97fc792 BLOCKING; also claude-opus-4-7's note) — fixed in df7e3f08. The one-argument diagnostic boundary is restored: a missing key argument is now a typed error (P3), validated before canonicalization; the provided key is then CanonKey::new'd. An un-keyable present key answers false (it can never be a map member — insert rejects it), not a fabricated result.
map_insert invalid key → Ok(None) fall-through (P3) — already fixed in ab9efed1 (returns Err); the relay was against the stale dbb4e2c7. Verified in current code.
value_to_json non-String key Display-collapse (P3) — already fixed in ab9efed1 (value_to_json is fallible and returns Err on a non-String map key). Verified in current code.
CanonKey second equality authority (P2) — already fixed in ab9efed1 (Eq delegates to Value::eq; only Hash derived). Verified.

Also resolved the main merge conflict in v4_roster_pilot.dag (row-count → 46) via a merge commit.

Verification on HEAD: map_structural_key_equality + map_lookup_miss_witness_violates green; all 46 v4 roster claim-run witnesses pass; gunbc compile --source-root src/v4 = 0 diagnostics; map_lookup_dual_dispatch 4/4; fmt + clippy clean.

— sent from merry-stag-540

briansrls

Review metadata

Provider / model: codex / unknown
Commit: df7e3f08 · Trigger: schedule
Thinking: 284s wall

✅ No blocking concerns in the mixed v2 implementation and v4 claim-roster changes.

…e, bidirectional coercion, self-host, Map, PROV, carrier-axis) (#4605) * docs: design — termination checker (fuel-elimination lane C1) Checker-not-discoverer design for replacing remaining/fuel threading in 06_translate with validated descent proofs: carrier upgrades in v4.std.cardinality (lexicographic TerminationProof + ProofEdge port), SCC checker ported from dsl/std/{termination,graph}.dag onto v4.std.dependency, serialize_type_expr_* cluster as the minimal slice, fuel-triad dissolution ratchet (40 remaining-params / 20 guards -> 0). https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: design — general value-set lattice (non-integer containment) Closed description family (Empty/Universal/IntegerInterval/Enumeration/ Product/TaggedUnion) with anchor-gated structural containment, semantic strictness replacing R1's syntactic !=, integer_value_set fold-in per its own dissolve-on-arrival marker, R1/R2 as the executing consumers, and the decidability carve stated honestly (predicate refinements stay refusal). https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: design — bidirectional emit/ingest as one declared coercion relation One FormalGrammar production-row set per target, both directions derived as interpreters over the same rows; production selection = find_witness over a closed candidate set; four static bidirectionality obligations (slot bijection, forward/backward determinism, declared quotient); inverse-aware constraints on emit ladder T3-T6; home-language add-subset slice with round-trip claim as the inverse proof. Notes dangling CP-1b anchors (TASKS.md, design-v4-compiler-homomorphism.md). https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: design — self-host fixed point (v4 bootstrap ratchet) Precise oracle (stage1==stage2 bit-identical over a declared artifact set, DB-8 prerequisite, located divergence diffs), hand_maintained_src as declared data + census sweep with per-entry dissolution triggers, four-stage plan honoring the emit-ladder gate (stage A buildable now: zip-fold equality wiring + census; B per-module convergence ladder; C whole-compiler promotion, operator-gated pins; D diverse double- compilation). Notes SELF_HOSTING.md path drift (lives in src/v3/). https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: design — Map representation unification (extensional data, one equality authority) Map<K,V> re-shaped from stored-closure partial function to finite extensional entry data (the P1 nickname fix); map_get signature preserved, body honest; PartialFunction<K,V> carrier for the intensional concept with derivable one-way map->function projection; v2 raw_map_lookup dual-dispatch chokepoint + match_pattern bridge delete; closes B-MAP-LOOKUP-OPTION-C-1, B-LOOKUP-1, finite-set-uniqueness markers in one landing. #4564 runtime semantics are the regression floor; iteration-order (DB-8) escalated as Q-M1. https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: designs — provenance occurrence-id anchoring (PROV/T-8) + carrier-core-axis decision memo PROV: opaque occurrence id stamped on Node (brand-channel playbook), span data off-tree in a per-compile SpanIndex keyed by id, reusing Locus/Extent ByteRange as the span carrier; one equality-exclusion rule at the single equality authority; carried/derived transport receipts; fail-closed Unanchored/NoEnclosingOccurrence outcomes. Written as input to the HELD operator scoping decision. Carrier axis: decision criterion (functional dependency => coincidence obligation, not a sixth axis; independent pair => ModelCoreFactAxisCarrier) with a measure-first census as the front door; folding into Encoding rejected on both branches. https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: tracking memo — Optional match-surface consistency (T3 root-cause, lane adhoc-ce8d7ae6) Records the measured T3 root-cause (substrate-consistency defect, not the positional-vs-labeled model question — the witness never compiled) and registers conditional #9 (Optional-representation unification, sibling of #5 Map). Branch criterion: surface flavor => bounded arm-normalization sweep; deep flavor => #9, co-landing with the Map map_get/match_pattern bridge. Grounds the defect class at collection.dag:28/112 (canonical Present|Absent vs Some/None arms over a Witness-typed value). Flavor unmeasured; the lane reports it. https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: apply operator rulings to design open questions (2026-06-09) Q-B1: commitment reframed as the four obligations, not a formalism — grammar formalisms are modeled data; PEG may exist as parse-only; bidirectional verdict = passing obligations 1-4. Q-M1: canonical key order IS the Map representation (one order, plain structural equality, DB-8 by construction; no insertion-order concept). Q-V2: no new CoercionMismatchKind variant (fewer variants for now). Q-T2: gate-in-infer confirmed; checker made relocation-cheap by construction (pure substrate function; infer holds only the gating wire). Q-S2: wave-1 artifact set = emitted .rs; committed-.rs-era transition noted as its own lane re-declaring the compare set. Q-S3: pin rotation operator-GO only, confirmed. https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs(termination): FunctionRef/call-graph audit — producer does not exist; T-9 rides #4581 Audited 2026-06-09 against the live tree: call-graph extraction is not readable as substrate facts today, three layers deep — (1) zero production writers of dependency_binds_to_edge (4 lens fixtures only; dependency.dag's own T-9 marker confirmed unbuilt); (2) resolve_atom materializes canonicalized spelling, not reference (spelling re-join would rebuild the channel BRAND is dissolving); (3) no stage produces ComputationNode trees and no FunctionRef carrier is landed — call sites have no v4 representation. Fix: T-9 BindsTo materialization lands as a rider on #4581's binding_id stamping (same write, same seam), serving the dependency classifier, structural_resolution lens, and this checker with one producer. Slice step 2 now gated on that producer. https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: sizing — COMPREP (function bodies in the v4 pipeline) Measured: the THESIS computation substrate is consumable shapes with zero producers — no stage builds ComputationNode trees, no FunctionRef carrier landed, eval's Transform arm is a call_primitive slot, and the mvp1 'emitted add fn' is a TypeNode Arrow signature (the T0/RTADD/T1 receipts are type-expr-tier). Sized as a first-class node: wave 0 carriers ride #4581 binding_id + the T-9 rider (no new FunctionRef carrier, fewer variants; body = Arrow.body per E-9); wave 1 keystone = source-ingested add body through parse/resolve/infer/eval by execution (~PROV-sized); waves 2-4 behaviors/translate/breadth. Gates SELFHOST facets 1-2 (co-equal with SPINE), termination-checker layer 3, emit ladder T4+, STAGE-ADOPTION. Recommends honest relabeling of T0/RTADD/T1 as signature-tier in the dep graph. Cross-linked from the termination design's prerequisite section. https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: portfolio-review fixes — Node identity-channel authority + four seam closures New: design-node-identity-channels.md — single P2 authority for Node- carried fields and equality participation (binding_id IN / occurrence id OUT / BindsTo rides the binding_id channel); #4581 is the linchpin seam; landing order fixed; allocator-determinism obligation flagged to #4581 (DB-8/fixed-point back door). PROV Q-P2 resolved against it; COMPREP wave 0 lands through it. Seam closures: Map Q-M1 reconciled to canonical-order-is-representation (insertion-order draft withdrawn; canonical total order on keys named as the introduced requirement); map_get/match_pattern bridge deletion ownership assigned to the Map landing with the Optional sweep explicitly excluding the site (deep flavor => one co-landed PR); value-set de-gated from the termination checker (structurally terminating; checker validates it later, nothing waits). https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 * docs: fix doc_refs CI (regen doc-chain) + resolve T3 dual-authority seam - docs/thesis/doc-authority.md: regenerate embedded doc-chain via check_doc_refs.py --write-graph (new design docs joined the graph; the stale chain was the doc_refs CI failure). - design-bidirectional-coercion.md §6: precedence note — rows-not- closures remains the direction authority; the T3 fold-carrier binding decision (incl. positional/labeled discipline) lands only after the one bounded run, with design-optional-surface.md §4 as the single authority for sequencing (review thread r3384485736). https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4 --------- Co-authored-by: Claude <noreply@anthropic.com>

Brian Searls added 2 commits June 8, 2026 19:45

WIP: personal

cfc3270

WIP: personal

dbb4e2c

briansrls commented Jun 8, 2026

View reviewed changes

Brian Searls and others added 4 commits June 8, 2026 20:06

WIP: personal

077d9bb

WIP: personal

396ab38

WIP: personal

8e526cf

briansrls changed the title ~~personal~~ fix(v2): structural-key Map== via native data repr keyed by Value-equality authority Jun 8, 2026

briansrls marked this pull request as ready for review June 8, 2026 20:31

Brian Searls added 2 commits June 8, 2026 20:55

WIP: personal

5e5623a

WIP: personal

42ed177

WIP: personal

d97fc79

briansrls commented Jun 8, 2026

View reviewed changes

Comment thread src/v2/stage0/src/v2_interpreter.rs Outdated

Value::Map(m) => {

let key = expect_str(args.first(), "contains")?;

Ok(Value::Bool(m.contains_key(&key)))

let key = args.first().cloned().unwrap_or(Value::Null);

This comment was marked as resolved.

Sign in to view

briansrls merged commit 43b7516 into main Jun 8, 2026
9 checks passed

briansrls deleted the session/merry-stag-540 branch June 8, 2026 22:12

briansrls commented Jun 8, 2026

View reviewed changes

briansrls mentioned this pull request Jun 9, 2026

docs: hard-problem design docs (termination checker, value-set lattice, bidirectional coercion, self-host, Map, PROV, carrier-axis) #4605

Merged

briansrls mentioned this pull request Jun 10, 2026

Optional dissolve (FULL, stage0-green) — awaiting sign-off receipts + still-raven review before undraft #4606

Merged

Navigation Menu

Repository navigation

fix(v2): structural-key Map== via native data repr keyed by Value-equality authority - #4564

fix(v2): structural-key Map== via native data repr keyed by Value-equality authority#4564
briansrls merged 10 commits into
mainfrom
session/merry-stag-540

briansrls commented Jun 8, 2026 •

edited

Loading

Uh oh!

briansrls left a comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented Jun 8, 2026

Uh oh!

briansrls commented Jun 8, 2026

Uh oh!

briansrls left a comment

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented Jun 8, 2026

Uh oh!

Uh oh!

briansrls left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

Model decision

Fail-closed boundaries (P3)

Evidence (by execution)

Scope note

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented Jun 8, 2026

Uh oh!

briansrls commented Jun 8, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented Jun 8, 2026

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented Jun 8, 2026 •

edited

Loading