Repository navigation
v4 B1-CANON: design the canonical-form clause in-header (not delegated) - #3157
Conversation
Operator-ratified 2026-05-15: the canonical-form clause was deferred to a T-1 worker relay. Every consumer (B1, A3, T-15, T-20, T-21, AGENT-1's content-addressed Diff) rests on it — too load-bearing to delegate. Now designed + ratified as the B1-CANON block in std/node.dag's header; T-1 IMPLEMENTS content_hash = merkle_fold ∘ canonical to it, does not redesign. 6-point contract: (1) post-normalize domain; (2) α-equivalence via K-1 (De Bruijn for bound, opaque identity for free); (3) child order is ALGEBRA-DERIVED not hand-flagged — default SEQUENCED, commutative only where algebra proves it (fail-closed: over-fire safe, collision = silent correctness bug); (4) recursion by-reference, name-ref hashed by Symbol identity never inlined (totality on `type T = … T …`); (5) structural catamorphism, decidable, Merkle ⇒ shared sub-Nodes hash once (dedup free); (6) no incidental ordering. DECISIONS.md B1 row + Part 3 updated. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ntracts Derisk (operator-requested). The Ex.1-4 worked examples proved correctness; these prove the MINIMALITY claim is falsifiable and bind its real gates: - Ex.R1 (effectful local edit): minimal IFF the effect algebra is fine-grained — an effect-GRANULARITY property, not effect-lens strength (B3 makes effects structural/read, so the lens is strong by construction; coarse effects are the open risk). Contract on lens/effect.dag. - Ex.R2 (widely-shared sub-node, partial change): minimal IFF infer emits NODE-PRECISE use→def edges to the consumed sub-Node. The dominant gate — more load-bearing than the effect lens. Contract on compiler/04_infer.dag (T-9). - Ex.R3: "what counts as changed" is retired-safe by B1-CANON (#3157) — fail-closed sequenced default ⇒ worst case over-fire, never a missed change. No residual research risk on Diff granularity. Consumes section sharpened with the two implied contracts + the B1-CANON Merkle dependency. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
79cc7076· Trigger:schedule - Thinking:
141s wall
BLOCKING (1)
Root Cause
src/v4/std/node.dagB1-CANON combines equality-only Symbols with a sort-by-child-hash normalizer → define canonicalization over labeled child entries with a declared order-independent fold or structural tie/collision policy before T-1 implements content_hash.
Non-blocking — Strengths
src/v4/DECISIONS.mdThe ledger correctly pulls the canonical-form clause back into the substrate authority instead of leaving this load-bearing B1 contract to worker discretion.
| // 3. CHILD ORDER IS ALGEBRA-DERIVED, never hand-flagged (the subtle, | ||
| // highest-risk point). Whether a node's children are SEQUENCED | ||
| // (order is content) or COMMUTATIVE (order quotiented — canonical | ||
| // sorts those children by their own recursive content_hash) is |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Review metadata
1. Story of the diffThis PR moves the canonical-form decision for v4 2. Invariant categories
2.5. Top-down PM intent reviewCompliant. The PR preserves the high-level intent: it strengthens the single-authority substrate direction by locating the canonical-form contract in 3. VerdictREQUEST_CHANGES. The PR is directionally right and mostly clean, but B1-CANON is substrate authority for every content-addressed consumer, so the hash-only sort rule must specify collision/tie behavior before landing. A one-sentence fix in the contract may be enough if it makes the normal form total and fail-closed. |
…ANGES)
Both findings valid; fixed structurally rather than patched.
Finding 1 (node.dag:~478 ByPosition{index:Int} admits negatives): drop
EdgeSelector/ByPosition entirely. Path = List<Symbol> — each step
descends the Named edge keyed by that opaque Symbol. No ordinal exists,
so the negative/out-of-range illegal state is structurally impossible
(dissolved, not deferred to path resolution). Positional-connective
children are reached by replacing the enclosing Named subtree (the safe
over-fire #3157 blesses); surgical positional addressing is a future
operator-ratified extension (consumes-nothing root has no Nat; recursive
Peano = A1 STOP).
Finding 2 (node.dag:~514 Diff=List<Edit> validity via external
predicate): drop the set / pairwise-independence / parallel-positions
framing and paths_independent/diff_well_formed. Diff = ORDERED List<Edit>
applied SEQUENTIALLY; any List<Edit> is a valid rewrite program (no
representable illegal state). A non-resolving Edit => fail-closed
Diagnostic at apply time (operational, not a type-level illegal state);
apply_diff is a fold, all-or-nothing.
Both refine the operator-ratified shape — flagged in DECISIONS.md D1
PROPOSED-for-operator-eye for confirm/redirect.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from the signature (B3), never aggregated coarse — a granularity invariant (coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set Consumes/Ex.R1 cross-ref + DECISIONS B-5 row. Subsume #3153 (v4-affected-set-design, no worker — operator-directed): its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded into affected_set.dag as the T-21 design contract, reconciled to the now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4 (04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153 superseded; recommend close. DECISIONS #3153-subsumed row. B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) — Lean first, termination theorem class; Coq deferred second-prover probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred. STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note. Includes the already-committed origin/main merge (204b855: #3158 PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping D1/B-4/PROOF-1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
B-3 (operator-greenlit): strike "child order is ALGEBRA-DERIVED". The commutative-quotient is structurally foreclosed two independent ways — (a) no sort key: Hash is opaque/equality-only (K-1/B1), "sort by content_hash" inexpressible; (b) algebra unreachable: canonical/ content_hash are pure folds in the consumes-nothing root, std/algebra .dag Consumes node.dag (reading back = the D1 cycle class) and inhabitance is bound by infer (T-9), downstream of canonical's pre-infer domain. So child order = `children`-list order unconditionally — the correct closure of a decidable system (INVARIANTS:31), not a defect. Only field-permutation dedup is lost (over-fire = safe; missed-change foreclosed). T-2/algebra.dag needs no change — point 3 was mislayered, not deficient. Point 3 rewritten, point 6 de-qualified, DECISIONS B1-CANON prose updated. Also resolves the origin/main merge: DECISIONS B1 row merged (keeps both #3157's B1-CANON-block-is-operator-designed framing and main's Hash-re-homed-to-node.dag + structural-caching-consumer). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Valid (P2/audit-trail) — fixed in the latest commit. The dates were internally correct (the B1-CANON clause is operator-ratified 2026-05-15 at node.dag:92 / DECISIONS:43; the B-3 point-3 amendment is 2026-05-16) — but node.dag:113 phrased B-3 as "operator-ratified 2026-05-16" without stating it amends the 2026-05-15 clause, so it read as two timestamps for one ratification. Reframed both sites to make the relationship explicit: "B-3 — an amendment to the 2026-05-15 B1-CANON clause, not a separate ratification; B-3 itself operator-ratified 2026-05-16" (node.dag point-3 + the DECISIONS B1-CANON prose). One audit trail, no apparent conflict; the substance is unchanged. — sent from valiant-boar-161 |
…NTS) Valid P2/audit-trail finding. The dates were internally correct (B1-CANON clause = 2026-05-15; B-3 point-3 amendment = 2026-05-16) but node.dag:113 phrased B-3 as "operator-ratified 2026-05-16" without saying it AMENDS the 2026-05-15 clause — reading as two conflicting timestamps for one ratification. Reframed both node.dag point-3 and the DECISIONS B1-CANON prose: B-3 is explicitly an amendment (2026-05-16) to the 2026-05-15 B1-CANON clause, NOT a separate ratification. Single audit trail, no apparent conflict. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
a85b22cb· Trigger:schedule - Thinking:
184s wall
BLOCKING (1)
Root Cause
src/v4/std/node.dagThe canonical-form contract assigns bound-reference structure that the Node atom carrier cannot encode → either add a substrate-representable bound-reference shape or restate content_hash as an environmented fold that does not claim to materialize canonical : Node -> Node.
Non-blocking — Strengths
src/v4/DECISIONS.mdThe ledger now makes B1-CANON the substrate authority and keeps T-1 in implementation mode rather than delegating a load-bearing design decision.
| // normalized kernel (the 4 sugar forms already dissolved). Raw | ||
| // parse trees are out of domain — sugar variance cannot reach the | ||
| // hash because it is gone before canonicalization. | ||
| // 2. α-EQUIVALENCE (K-1). A BOUND occurrence is replaced by its |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…3157 BLOCKING) Verified against current code: B-3 (64bf5a7) already REMOVED the commutative-sort-by-content_hash; child order is unconditionally `children`-list order, so the finding's premise ("B1-CANON sorts commutative children by content_hash") describes pre-B-3 behavior and its nondeterminism concern is already foreclosed (no sort exists). But the reviewer's argument is a genuine THIRD independent reason the old commutative-quotient was unsound, so it is folded into point-3's foreclosure rationale as reason (c): distinct labeled children can share an identical child subtree (`{a:Int,b:Int}` ⇒ equal child content_hash) and K-1 gives the label Symbol equality-only (no order) ⇒ no deterministic tie-break ⇒ incidental-order fallback (P2/P4). Strengthens B-3 (not contradicts); the BLOCKING is incorporated, not stale-dismissed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Verified against current code (not stale-dismissed) — and incorporated. The finding's premise ("B1-CANON sorts commutative children only by child content_hash") describes the pre-B-3 behavior. B-3 (commit But your hash-collision argument is a genuine third independent reason the old commutative-quotient was unsound — sharper than B-3's reason (a) ("no — sent from valiant-boar-161 |
|
Review metadata
1. Story of the diffThis PR turns B1’s canonical-form clause from something a T-1 worker would “encode per relay” into a substrate-level, in-header design authority. The actual canonical contract is six-point and deterministic: canonicalization is post-normalize only ( 2. Invariant categories
Compliant — this touches substrate authority, but in the expected place:
Compliant — boundary discipline / single authority is handled by making B1-CANON “Designed + ratified HERE, not a worker-relay choice” (
N/A — no Rust implementation, functions, methods, error/result shapes, globals, or helper placement changed. The eventual T-1 implementation should follow the project’s data + pure-function style, but this PR only names the pure contract (
N/A — no executable canonicalization or hash implementation is added, so there is no behavior to test in this PR. The test obligation belongs to the later T-1 implementation of
Compliant — the diff records a locked/ractified design rather than silently diverging from one. It explicitly says B1-CANON is separate from A1 (
Compliant — I do not see a new scaffold, TODO, bridge, or temporary representation. The only staged boundary is explicitly bounded: T-1 is named as the implementer of the already-fixed contract, not a co-authoring bridge ( 2.5. Top-down PM intent reviewCompliant — the highest-level v4 authority says the active program is v4 and thesis claims apply to the v4 substrate, while the thesis also frames correctness as structural facts carried by the program model rather than hand-maintained behavior. chatgpt-review-6a3c5bc6-9dce-48… chatgpt-review-6a3c5bc6-9dce-48… This PR preserves that intent: it moves a load-bearing canonical identity decision into 3. VerdictAPPROVE — The diff cleanly centralizes B1 canonical-form authority in |
|
Valid — fixed (verified against current code, not stale-dismissed). Point 2 did state, under Fix: α-equivalence is reframed as a property of the — sent from valiant-boar-161 |
…-Node rewrite (briansrls #3157 BLOCKING) Valid (verified current code). Point 2 said canonical:Node->Node "A BOUND occurrence is replaced by its binder-relative De Bruijn position" — but Atom{identity:Symbol} is the ONLY identifier carrier; there is no De Bruijn Node and adding one is an A1 closed-kernel STOP, so that rewrite is unrepresentable (the α-fact had no Node carrier; INVARIANTS P2/P4). Fix: De Bruijn / binder-relative identity is a property of the `merkle_fold` in `content_hash = merkle_fold ∘ canonical`, NOT a materialized canonical Node. The fold tracks binder scope and hashes a bound occurrence binder-relatively (free Symbol by opaque K-1 identity); the De Bruijn position is a transient fold-local value contributing to a Hash, never a Node — so the α-fact lives where it CAN (the fold's Hash codomain), representable, no carrier gap. `canonical:Node->Node` keeps only the representable normalizations (domain, child order). node.dag point 2 + DECISIONS B1-CANON prose harmonized. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Already addressed — verified against current code, not stale-dismissed. codex reviewed
The fix took the second option verbatim. Current node.dag point-2:
That is precisely an environmented (binder-scope-tracking) fold whose codomain is — sent from valiant-boar-161 |
…#3162) * WIP: v4 design * v4 D1: Diff/Path structural-delta vocabulary over Node Side-session-ratified B-1. EdgeSelector/Path/Edit/Diff data types in std/node.dag (DATA ONLY; A1-clean — Node stays the sole recursive type; B1/Hash precedent for substrate-tier placement). Operations (subterm_at/apply_diff -> Result<Node,Diagnostic>, paths_independent/ diff_well_formed) contracted into lens/application.dag header — forced off node.dag by the diagnostic.dag->node.dag cycle (Correction= Suggested(Node)); the node.dag "consumers fail-close" discipline. affected_set.dag consumes the type. DECISIONS.md Part-1 row D1 carries the data/op-split PROPOSED sub-point for operator confirmation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * v4 D1: dissolve two P2 illegal-state surfaces (codex #3162 REQUEST_CHANGES) Both findings valid; fixed structurally rather than patched. Finding 1 (node.dag:~478 ByPosition{index:Int} admits negatives): drop EdgeSelector/ByPosition entirely. Path = List<Symbol> — each step descends the Named edge keyed by that opaque Symbol. No ordinal exists, so the negative/out-of-range illegal state is structurally impossible (dissolved, not deferred to path resolution). Positional-connective children are reached by replacing the enclosing Named subtree (the safe over-fire #3157 blesses); surgical positional addressing is a future operator-ratified extension (consumes-nothing root has no Nat; recursive Peano = A1 STOP). Finding 2 (node.dag:~514 Diff=List<Edit> validity via external predicate): drop the set / pairwise-independence / parallel-positions framing and paths_independent/diff_well_formed. Diff = ORDERED List<Edit> applied SEQUENTIALLY; any List<Edit> is a valid rewrite program (no representable illegal state). A non-resolving Edit => fail-closed Diagnostic at apply time (operational, not a type-level illegal state); apply_diff is a fold, all-or-nothing. Both refine the operator-ratified shape — flagged in DECISIONS.md D1 PROPOSED-for-operator-eye for confirm/redirect. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: add Practice-4 dissolution receipt; fix RATIFIED/PROPOSED contradiction (#3162 BLOCKING) BLOCKING (codex via briansrls relay, vs pre-fix sha a06a066 — verified against current HEAD): - "D1 sum vocabulary without coproduct receipt": the EdgeSelector sum was already deleted in 7c91f73, but the DECISION not to have a positional selector is itself a Practice-4 dissolution requiring the formal 4-pattern ledger (algebra.dag precedent). Added the receipt to std/node.dag D1 (🟢 GREEN terminal: positional addressing subsumed by enclosing-Named-subtree replacement; not a deferred gap). - "root-status driving the index carrier": resolved by the same dissolution — there is no index carrier; the receipt documents why none is needed (vs the reviewer's Nat/Fin suggestion) and why a future surgical form is an explicit operator-ratified extension. Non-blocking: DECISIONS.md D1 row no longer carries a "confirm or redirect" clause inside a RATIFIED row — refinements are stated as encoded-via-PR-review (the normal channel), not an open fork. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: fix stale EdgeLabel cross-reference in node.dag header (cursor #3162 editorial) The D1 header block cited "lines ~221-230" for the no-stored-index discipline, but adding the D1 header block shifted line numbers — that range is now `Connective`. Re-anchored by construct name + corrected approx lines: `type EdgeLabel` ~284 and its "deliberately NO stored index" rationale ~278. Editorial only; cursor APPROVE on this PR. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 B-4: affected_set R2 node-precise-resolution contract Encodes the B-4 cross-cutting decision (operator-greenlit): affected_set minimality requires 04_infer resolution to bind each use-site name-ref to the EXACT declaration Node (not module/scope). The use->def graph is derived by traversal over already-resolved name-references, NOT a 5th InferredFacts field (IR-1-safe; same derive-don't-store discipline as content_hash/D1). Coarse resolution = correct but maximally over-fires. Reciprocal header contracts: 04_infer.dag B-4 block + affected_set.dag Consumes note. DECISIONS.md Part-1 row B-4. Scaffold headers only; no bodies. Continues the v4 design-survey on the session branch alongside D1 (operator sequences/carves at manual merge). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 B-5 + subsume #3153 + B-2 (lean.dag PROOF-1 model) B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from the signature (B3), never aggregated coarse — a granularity invariant (coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set Consumes/Ex.R1 cross-ref + DECISIONS B-5 row. Subsume #3153 (v4-affected-set-design, no worker — operator-directed): its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded into affected_set.dag as the T-21 design contract, reconciled to the now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4 (04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153 superseded; recommend close. DECISIONS #3153-subsumed row. B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) — Lean first, termination theorem class; Coq deferred second-prover probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred. STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note. Includes the already-committed origin/main merge (204b855: #3158 PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping D1/B-4/PROOF-1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * v4 B-4: correct the use→def carrier (Symbol/K-1, not resolved_type) — #3162 BLOCKING Valid P2/Practice-3 finding (briansrls inline @ 04_infer.dag:54): resolved_type is the node's TYPE; many declarations share a type, so it is lossy for binding identity — the use→def fact had no named forward carrier. Corrected: the carrier is the post-resolution opaque Symbol (K-1) on the name-ref Atom, AUTHORED by 03_resolve.dag (binding = Symbol equality, node.dag name_occurrences pattern). 04_infer is preserve-only (no 5th InferredFacts field, IR-1-safe); affected_set derives by Symbol-equality traversal. Fixed consistently across 04_infer.dag B-4 block, new 03_resolve.dag B-4 authority note, affected_set.dag Consumes note, DECISIONS.md B-4 row. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * WIP: v4 design * v4 C5-2 emit-locality + T-9 infer keystone contracts (operator-ratified) C5-2 (emit-locality): emit is structurally local — a D1 apply_diff at Path p re-emits ONLY p's subtree. Per operator code-as-data steer: locality is Node-relative, NOT file-relative; a file is a convenience projection, the substrate anchors no semantic on the file concept; non-local emit = declared normalization at the enclosing NODE scope, never "file scope". The C5↔D1 hinge (AGENT-1 faithful re-emit). 05_emit.dag header + Owns + DECISIONS C5-2 row. T-9 A+B: A — Find decidable by construction (closed declared-inhabitance candidate set, not a synthesized search; structural descent ⇒ the inferencer terminates; empty = decidable fail-closed Diagnostic). B — single-file discipline is the 03_resolve scope boundary (env/scope/ lookup/binding belongs to 03_resolve per B-4; infer owns only Find + cardinality + diagnostic precision). 04_infer.dag header + DECISIONS T-9 row. Receipts: in-header (operator decision; status quo, no change). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: complete the Practice-4 receipt — add Pattern 5 (#3162 codex REQUEST_CHANGES) Valid finding. docs/modeling-discipline.md:112 requires FIVE dissolution patterns; the node.dag #3160 operator-ratified receipts already use 5. The D1 receipt did only 4 (I wrongly followed algebra.dag's older 4-pattern style). Added Pattern 5 (Parameterized family) — FAILS: ByName/ByPosition are not one mechanical F<X> over a declared set (different payload types + addressing semantics; mirror EdgeLabel's genuine 2-variant discriminant, not an enumerated copy à la Homomorphism-per-algebra); no source set to project over (Practice-7 N/A); post-dissolution one constructor = not a family. "four" → "five". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 C5-1 + C5-3 (operator-ratified) — node-level round-trip law + spec-provable F C5-1: the bidirectional_roundtrip TestClaim asserts ingest∘emit=id_Node via B1 content_hash (meaning round-trips), NOT text-byte identity. Text-level fidelity recorded as a DEFERRED orthogonal future layer (a trivia sidecar outside Node/content_hash, partial; the C5-fidelity Declared-normalized dispositions are its forward hook — node-level adoption preserves it zero-rework). Non-orthogonal route (lexical in the Node) explicitly rejected. C5-3: F = the spec-provable meaning core; spec silence ⇒ out of F (Declared-normalized or Fail-closed). Conservative/fail-safe — the spec decides, modeler has no discretion; per-language non-F shrinkage declared up front, not discovered at test time. Encoded: lens/testgen.dag C5-1/C5-3 header block + DECISIONS C5-1/C5-3 rows. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4: reconcile PROOF-1 row with L-4 — DECISIONS.md self-consistency (cursor #3162 APPROVE_WITH_COMMENTS) Valid NON-BLOCKING finding: B-2 added lean.dag + the L-4 row but the PROOF-1 row still ended "**NO new file** (closed-tree invariant)", contradicting L-4 (which lands extdeps/languages/lean.dag). Reconciled: PROOF-1's framing (#3158) added no file (framing-only, deferred the model "lands later"); that deferred model subsequently lands as lean.dag per B-2/L-4. One coherent story; PROOF-1 row now cross-refs L-4 and states "No contradiction" explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
600f1c53· Trigger:schedule - Thinking:
171s wall
BLOCKING (1)
Root Cause
src/v4/std/node.dagα-equivalence moved into an environmented fold while the B1 Merkle contract stayed context-free → state the binder-environment key in the fold/dedup contract or narrow “hash once” to closed sub-Nodes.
Non-blocking — Strengths
src/v4/DECISIONS.mdThe ledger now correctly makes B1-CANON the in-header authority and keeps T-1 as implementer rather than designer.
| // it terminates by Node finiteness and is decidable | ||
| // (feedback_decidability_invariant; the same A2-implicit descent | ||
| // `node_well_formed` uses). `content_hash = merkle_fold ∘ | ||
| // canonical`; structurally-shared sub-Nodes hash ONCE — content- |
There was a problem hiding this comment.
BLOCKING: B1-CANON makes bound-occurrence hashing depend on the fold's binder environment, so claiming structurally shared sub-Nodes hash once as a context-free Merkle consequence is unsound under INVARIANTS P2/P4 unless the environment is part of the fold/memo key or dedup is limited to closed sub-Nodes.
1 participant
Summary
Operator-ratified 2026-05-15. The canonical-form clause — the total deterministic normal form B1's
content_hashfolds over — was previously deferred ("T-1 worker encodes per relay"). It is the single most load-bearing definition in the substrate (B1, A3, T-15, T-20, T-21, and AGENT-1's content-addressed Diff all rest on it). Pulled back from delegation and designed + ratified as the B1-CANON block instd/node.dag's header. T-1 implementscontent_hash = merkle_fold ∘ canonicalto this contract; it does not redesign it.The 6-point contract
Atoms hashed by Symbol identity, never inlined ⇒content_hashtotal ontype T = … T ….Changes
std/node.dag—B1-CANONheader block + Owns entryDECISIONS.md— B1 row + Part 3 note updated (designed-here, not delegated)Header design contract only (T-1 implements). Separate authority from A1 (per ratified B1). No code change — v2 bridge parses clean.
Test plan
cargo fmt --all --checkcleanv2-compiler compile --source-root src/v4 --target dag→ 0 diagnostics🤖 Generated with Claude Code