Recursion boxes through a handle, and a value copy is deep

[TheLazyCat00]

Closes #154. Implements #156 (narrow scope — see Decision 3). Absorbs #158.

A recursive member is now an ordinary member that the compiler boxes — a fixed-size handle stored inline, payload in the scope's dynamic region, exactly as a List's backing store is placed. A recursive member therefore owns its child instead of guesting it, and the motivating program from the issue compiles as written:

type Operation = #struct { left Expr; right Expr; op Operator; }
type Expr = #variant { op Operation; intLit String; }

program Expr = Expr.op(Operation(Expr.intLit("3"), Expr.intLit("2"), Operator.add))

There is no new syntax. The programmer writes left Expr; boxing happens because inline placement does not exist for that member, and placement was already an unobservable implementation decision (memory.md §3.5). & now means aliasing and only aliasing.

Boxing is available on both sides of the # axis, so a value sum may recurse too. That half arrived late, from review, and is Decision 3.

---

Decisions

1. A boxed payload has no size class

The dynamic region's blocks looked like power-of-two classes beginning at 128 bytes, and the first version of this PR extended that ladder downward to a 16-byte floor so small nodes would not waste most of a block.

That was the wrong reading of the region. §3.2's free stacks are keyed by exact byte size, created on demand; powers of two appear only because a list doubles. They were never a classification imposed on what the region holds.

A boxed payload never grows, so there is nothing for a class to absorb. It now asks for exactly its type's size, aligned to that type's alignment requirement — a twelve-byte node occupies twelve bytes. The floor, the ladder, and the question of how many classes belong under 128 all disappear.

Alignment is stated per kind instead of derived from size: a growable backing store is cache-line aligned as before, a boxed payload takes its type's own alignment, and the frontier is rounded up before it is bumped.

The one cost: exact sizes never pool across different sizes, where a class would have. That lands the right way here — a sum is laid out at its widest case plus tag, so every node of one type is the same size, and a discarded subtree returns precisely the block the next node wants. Classes pool heterogeneous churn; a tree is not that.

Three consequences of dropping classes were caught in review and fixed in 2891b02: reuse stacks keyed by size alone could hand a block to a type needing stronger alignment (now keyed by (size, alignment)); an oversized span sized by truncating division would under-allocate a payload that is not a whole number of chunks (now ceil); and §3.6 still carried the retired four-classes-below-128 paragraph.

2. Which members get boxed — required on a cycle, permitted off one

The containment graph here has three edges: Expr.op reaches Operation, and both Operation.left and Operation.right reach back to Expr. Several different cuts make every type finite, so "box the recursive member" does not name one answer. Minimal cutting is not unique, which would make a type's layout depend on an ordering nobody wrote down.

Boxing is therefore required wherever an edge lies on a cycle: order-independent, decidable from the declarations, no search. The cost is that a two-type cycle boxes on both hops, so descending one level of an Expr tree costs two indirections where a hand-tuned scheme would charge one. Named as a cost in both adt.md §4 and the story.

The rule first said boxed "exactly when" an edge lies on a cycle. Review pushed on that, and the biconditional was stronger than this change needs — it forbids an implementation from boxing a member it has good reason to box. The clearest case is a sum whose widest case dwarfs its common ones: one fat case costs every instance that footprint, and an array of a thousand such values pays it a thousand times over.

257c8da relaxes it: required where no finite inline layout exists, permitted elsewhere, chosen per type. Nothing observes the difference — no operator exposes a type's footprint, and §3.5 already states that placement is not language-visible. Because the choice is per type rather than per instance, uniform stride (generics.md §7) holds either way.

Why a leaf does not rescue inline layout (2342b53, answering a direct review question). Every value of a recursive type is finite — a Nat bottoms out at zero — and it is tempting to conclude the type could be laid out inline. It cannot, and the spec previously only asserted "infinite size" without engaging the objection. adt.md §4 now separates the two: layout is fixed per type, settled before any value exists, so the question is what one stride must be for every value at once. size(Nat) = tag + size(Nat) has no finite solution, and no stride can be taken from the deepest value because there is no deepest value — one Nat holds three nodes, the next three million, and uniform stride requires both to be the same size. The leaf terminates a value, not the type's size equation.

3. A value copy is deep, so a value type may recurse

Review asked directly whether recursive variants would not also work with value types, and pointed out that the example the spec used to justify the ban proves nothing: Expr's # is already forced by intLit String. That was right, and isolating the rule with an all-value-payload pair left nothing behind it.

The ban rested on two objections, and 804631f follows from both being withdrawn:

• A teardown obligation. This conflated the anchor tracking a reference type needs — so a guest can tell whether its host died — with knowing when a value dies. The latter is lexical (lifetimes.md §2.1 plus overwrite), and memory.md §3.2 already specifies the recursive block-return walk for reference hosts.
• A concurrent snapshot that was use-after-free. That assumed freeing can unmap, which this arena never does while a reader could run: §4.1's water tower keeps the scope alive and §3.2 unmaps only at drain. A block freed mid-walk is recycled inside a live mapping, so a stale read yields garbage rather than an invalid access.

What remained was a cost list, not a blocker. So type Nat = variant { zero Unit; succ Nat; } is now legal.

A value copy is deep (memory.md §2.3). Copying an existing value copies its inline bytes plus a fresh allocation and recursive copy of every boxed payload it owns, so two values never share a node. For a value with no boxed member — every value type written so far — this is exactly the inline byte copy it has always been.

The #-field and &-field bans stay, on the maintainer's reason, which is sharper than the one it replaces. A reference type exists in order not to be copied: it has one host, a stable identity guests resolve through, and it reaches a new place by being moved. A value holding one could only mint a second identity (so guests silently fail to follow) or share it (so hosting is no longer single). List and String are covered by the same sentence. This answers #156's question 4 in the negative and leaves question 5 open there.

4. Construction is not a copy, and overwrite has an order (from #158)

Merged from #158, which fixed three findings from the review on f6f7ca5.

Direct construction. §2.3 originally said a value is copied whenever "bound into a fresh slot," which read as: build Nat.succ(...) as a temporary, copy it into its parent, copy the finished thing into the binding — quadratic. The rule now splits on place-ness. A place expression denotes existing storage and is copied when bound elsewhere; a non-place expression produces a fresh value and MUST construct directly in its eventual destination, recursively through product construction, value-variant case forms, function results, and match arms.

v Vector2 = Vector2(Int(3), Int(4)) // constructs v, v.x, and v.y directly
w Vector2 = v                        // copies the existing value in v

Overwrite ordering. An overwrite evaluates its right-hand side against the destination's pre-overwrite state. If the source is the destination or anything reached through it, the replacement is completed before the old occupant dies and its blocks are returned, so x = x and x = x.child cannot erase their own source. §3.2 previously returned blocks "before the replacement becomes live," which had the ordering backwards for overlapping cases; it now defers to §2.3.

Snapshot allocation. §4.4 said the reader allocates from the writer's size stacks while memory.md §3.5 says a copy allocates in the destination scope — a straight contradiction. Destination wins: a snapshot is an ordinary deep copy into its fresh binding, and reader and writer contend only when they actually share an arena. Blocks stay provisional until the final version check, and a rejected attempt returns every block it allocated before retrying.

Discriminant validation. A fourth walk rule ahead of the span check: all structure-directing metadata is untrusted before the final version check. A variant discriminant must name a declared case before dispatch; likewise any count or length deciding which child handles exist. The depth bound is per attempt.

2342b53 then reconciled two passages #158 left describing the pre-#158 rule: adt.md §4 claimed a recursive value type walks and reallocates on every store into fresh storage (true only for binding an existing place), and memory.md §6 read as though passing a value parameter were the copy.

5. Why the # axis got smaller

# now decides identity, aliasing, and copy-versus-move. It no longer decides whether a type may contain itself, because that question belongs to layout, and layout answers it the same way for both kinds. foundations.md §7, types.md §2.1–§2.2, and adt.md §1/§3 are reworded accordingly, and boxed hosting member is generalized to boxed member.

A boxed payload's nature follows the member's declared type, not the enclosing kind — off-cycle boxing lets a #struct box a value-typed member, and that payload must not gain a backpointer or become guestable. memory.md §3.3 splits the two questions: what the payload is follows the declared type; what becomes of it on move, copy, or death follows the enclosing kind.

6. One rule, one home

The exact-size rule was stated three times across memory.md §3.2 and §3.6, with the rationale twice. §3.2 now owns sizing, alignment and reuse; §3.6 keeps only the two-part handle/payload representation. Consolidating exposed a contradiction from 2891b02: §3.2 rekeyed the reuse stacks to (size, alignment) in one paragraph while the next still read "keyed by byte size alone." Fixed.

---

One thing in the issue that did not survive contact with the spec

The issue says "a constructor result is a hosting verb result — a legal move-source (lifetimes.md §1.2)". That is right for Operation(...), but Expr.intLit("3") is not a verb result: adt.md §3.2 is emphatic that naming a variant case is built-in syntax with no verb behind it, and §1.2 listed only two move-source forms. §1.2 now lists a #variant case form as a third, on the same terms as a hosting verb result. A value variant case form is still excluded, and for a reason that survives Decision 3: a value sum is copied rather than hosted, so there is no hosting to transfer.

---

Changes

File	What changed
spec/memory.md	§1 overview; §2.3 the deep value copy — copy-versus-direct-construction, overwrite ordering, destruction; §2.10 rewritten: the ban is about copying, recursion explicitly not barred; §3.1 regions and exact-size oversized spans; §3.2 allocation keyed by (size, alignment), value-slot overwrite ordering; §3.3 boxed member on both sides of the axis, keyed on the declared type; §3.5 placement, recursive relocation, value-copy allocation; §3.6 handle/payload representation; §6 summary rows
spec/adt.md	§1 bullet; §3 both sums may recurse (Nat/Peano both legal) plus value-sum construction by copy; §4 rewritten — why a leaf does not rescue inline layout, boxing available to both kinds, ownership as hosting or value-ownership, costs corrected for direct construction; §7 comparison row; §8 summary rows
spec/concurrency.md	§4.2 boxed values are still alias-free; §4.4 the deep snapshot — untrusted metadata and discriminant validation, bounded walk with complete-span validation, destination-scope allocation, provisional blocks returned on retry; summary row
spec/foundations.md	§1 bullet, §5, §7 — # is identity, aliasing, and copy-versus-move; recursion available to both kinds; deep-copy bullet; summary row
spec/types.md	§1 bullet, §2.1, §2.2, §2.5, §3.9, summary rows
spec/lifetimes.md	§1.2 #variant case form as a move-source and the reworded value-form exclusion; §2.1 value death points and recursive block return
spec/syntax.md	§2.4 mould example, §2.10 recursion example
spec/glossary.md	§3.2 and §3.30 reworded; §3.39 boxed hosting member → boxed member; new §3.40 deep value copy; new §3.41 move-source
stories/memory.md	New chapter: "What a copy is for, and the ban that survived it"
stories/adt.md	New chapter: "The sum that could not contain itself"
README.md	Both stories-table rows extended

Validation

All three CLAUDE.md guards, run with -R on the directory, re-run at 2342b53:

• retired generics forms — no output
• bare-symbol guest source — four hits, all pre-existing and legitimate per CLAUDE.md: three deliberate // ILLEGAL: examples (memory.md:172, memory.md:181, lifetimes.md:27) and one grammar metavariable (syntax.md:20)
• receiver — the single expected hit, the chapter-title pointer at functions.md:37

Story append-only check against origin/main, both files: no output, additions only — including across the #158 merge, since the chapters it edited are this branch's own unmerged drafts.

Anchors: every spec→story pointer, story→story link, and pinned in-prose permalink was verified to resolve by script.

bench/

No change, and none made speculatively. bench/zane_bench.c models the allocator, not the type system. The shapes this change produces are already in it: Test 3 exercises mixed 8/16/32/64-byte allocation with random-order free, and Test 10 is an ownership tree of ~4000 individually allocated nodes torn down post-order.

Still open

• A size-driven placement mechanism. Decision 2 lets an implementation box a fat case; it gives a programmer no way to ask for it. Not yet filed.
• Runtime destination scope. Review raised that the destination arena of a store cannot always be determined statically, and that a value could instead begin in its construction arena and relocate at runtime. The motivating example moves a symbol from inside a conditional branch, which lifetimes.md §1.3 already forbids independently — so making it legal is a change to the move model, not a clarification here. Worth its own issue.
• The wider reopening in Deep value copy, so a value type can own a boxed payload #156 — whether # reduces to identity and aliasing alone, and whether a deep-copied List inside a value type should be legal.
• This branch carries one unrelated commit, d06d2e0 docs(meta): guard the receiver-to-subject rename, which predates this work and only adds a validation guard to CLAUDE.md. Happy to split it out if preferred.

Summary by CodeRabbit

• Documentation
  • Clarified recursive type behavior for value and reference types, including compiler-managed boxing and ownership.
  • Documented deep-copy semantics for recursive values and move semantics for recursive references.
  • Updated examples and terminology to use Operation and ordinary recursive members instead of explicit reference fields.
  • Expanded memory, lifetime, concurrency, syntax, glossary, and ADT guidance for allocation, relocation, destruction, snapshots, and safety.
  • Added contribution guidance favoring “subject” terminology in new specification prose.

[coderabbitai]

Important

Review skipped

Auto incremental reviews are disabled on this repository.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: f42c0e2b-8073-4264-a8c5-4574149386c1

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

Note

Reviews paused

It looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the reviews.auto_review.auto_pause_after_reviewed_commits setting.

Use the following commands to manage reviews:

• @coderabbitai resume to resume automatic reviews.
• @coderabbitai review to trigger a single review.

Use the checkboxes below for quick actions:

• ▶️ Resume reviews
• 🔍 Trigger review

📝 Walkthrough

Walkthrough

The specification changes recursive members from explicit & references to compiler-boxed hosting fields. It defines ownership, deep copying, dynamic allocation, relocation, lifetime, concurrency, updated examples, and terminology validation.

Changes

Recursive hosting model

Layer / File(s)	Summary
Recursive ADT contract spec/adt.md, spec/syntax.md	Recursive members use owned hosting values. Operation replaces BinOp, and the compiler boxes members in recursive cycles.
Type and lifetime rules spec/foundations.md, spec/types.md, spec/lifetimes.md, spec/glossary.md, stories/adt.md, README.md	The specification defines boxed ownership, deep value copies, variant move-sources, recursive destruction, and the separate role of & for aliasing.
Dynamic boxed payload memory spec/memory.md, stories/memory.md	Boxed payloads use dynamic-region allocation with exact-size and alignment-aware reuse. Rehosting and destruction recursively process owned payloads.
Boxed value concurrency spec/concurrency.md	Snapshots validate boxed offsets and depth, copy payloads recursively, reclaim provisional allocations, and may retry under concurrent writes.
Terminology validation CLAUDE.md	A grep-based check restricts new receiver terminology and requires subject in new prose.

Estimated code review effort: 3 (Moderate) | ~25 minutes

Sequence Diagram(s)

sequenceDiagram
  participant ExprConstructor
  participant Operation
  participant DynamicRegion
  participant DestinationScope
  ExprConstructor->>Operation: construct nested Expr hosting values
  Operation->>DynamicRegion: allocate boxed recursive payloads
  DynamicRegion-->>Operation: return fixed-size handles
  Operation->>DestinationScope: rehost the recursive value
  DestinationScope->>DynamicRegion: recursively relocate owned payloads

Loading

Possibly related issues

• Deep value copy, so a value type can own a boxed payload #156: Covers deep-copying value types that own recursively boxed payloads and the related memory, concurrency, and type semantics.

Possibly related PRs

• zane-lang/spec#147: Introduces related recursive boxed payload allocation, copying, relocation, and teardown rules.
• zane-lang/spec#150: Revises the same recursive boxing and memory semantics across the specification.
• zane-lang/spec#158: Shares the recursive boxed-value copying and snapshot updates in the memory, concurrency, and story specifications.

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Out of Scope Changes check	⚠️ Warning	The CLAUDE.md validation guard is unrelated to the recursive boxing objectives in issue #154.	Remove the unrelated CLAUDE.md validation-guard changes or move them to a separate pull request.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly summarizes the main changes: compiler-boxed recursion and deep value copies.
Linked Issues check	✅ Passed	The changes satisfy issue #154 by replacing owned recursive & fields with boxed hosting handles and enabling direct recursive construction.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch claude/player-pointer-aliasing-frj4ae

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[coderabbitai]

Actionable comments posted: 6

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@spec/glossary.md`:
- Around line 257-261: Add a living story pointer immediately after the
“Canonical home” line in the “boxed hosting field” glossary entry and before the
separator, linking to the relevant integrated ADT or memory story using the
existing `> **Story:**` format.
- Around line 257-261: Clarify the definition of “boxed hosting field” to
explicitly include variant case payloads such as Expr.op, Expr.flip, and
Expr.parenthesized, or consistently rename the term to “boxed hosting member”
throughout the entry. Keep the ownership, layout, and recursive-type semantics
unchanged.
- Line 188: Update the Meaning definition to limit fixed-size-region allocation
to handles materialized in scope-level slots. Clarify that handles embedded
within boxed or other dynamic payloads remain part of their containing dynamic
blocks, including nested boxed children, while preserving the existing rehosting
behavior.

In `@spec/lifetimes.md`:
- Around line 35-42: Update the variant-case move-source descriptions in section
1.2 so only case forms producing a `#variant` qualify as hosting move sources;
explicitly exclude value-variant cases from both the normative bullet and the
summary explanation, preserving their copy semantics.

In `@spec/syntax.md`:
- Around line 185-189: Clarify the Expr variant definition by adding a precise
reference to the implicit boxing rule for recursive hosting fields such as
Operation.left and Operation.right. Reconcile the §2.10 discussion around stored
references and &Tree so it distinguishes compiler boxing for field storage from
explicit reference aliasing, without implying these fields are inline recursive
values or invalid.

In `@stories/adt.md`:
- Around line 119-150: Restore the previous recursive-storage chapter, including
the explicit-& rules, Leaves workaround, and rooted-in-a-field explanation,
without altering its historical wording. Append the compiler-boxed
hosting-fields decision as a new chapter after the restored content, preserving
both accounts as an append-only story.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 9cc1c168-13c6-4309-987e-39b8ad83813a

📥 Commits

Reviewing files that changed from the base of the PR and between d50c9aa and 42e8364.

📒 Files selected for processing (11)

• CLAUDE.md
• README.md
• spec/adt.md
• spec/foundations.md
• spec/glossary.md
• spec/lifetimes.md
• spec/memory.md
• spec/syntax.md
• spec/types.md
• stories/adt.md
• stories/memory.md

[TheLazyCat00]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[coderabbitai]

Actionable comments posted: 4

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (2)

spec/memory.md (2)

393-393: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

Remove the remaining boxed-payload size classes.

Line 393 still calls shared byte sizes “classes,” and Lines 407-408 state that sub-128 classes exist. This conflicts with Lines 344-346 and 405, which require exact type-size allocation with no class or floor. Keep powers-of-two sizes for growable backing stores only. Describe boxed reuse through exact byte-size stacks.

Also applies to: 405-409

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/memory.md` at line 393, Update the dynamic block-size description to
remove “classes” and any implication of sub-128 size buckets or flooring.
Require exact type-size allocation for boxed payloads, retain powers-of-two
sizing only for growable backing stores, and describe boxed reuse as stacks
keyed by exact byte size.

---

580-586: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

Correct the boxed-field placement summary.

Line 581 says the handle is inline “with its instance in the dynamic region.” The handle is inline with the enclosing host. Only the boxed payload named by the handle is in the dynamic region. The enclosing host can be a fixed-size scope slot or a dynamic payload. Rewrite this row to match Sections 3.3 and 3.5.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/memory.md` around lines 580 - 586, Rewrite the “Boxed hosting field” row
to state that the fixed-size handle is stored inline with its enclosing host,
which may be a fixed-size scope slot or a dynamic payload; only the boxed
payload referenced by the handle resides in the dynamic region. Preserve the
existing recursive-type rationale and compiler-selection behavior, aligning the
wording with Sections 3.3 and 3.5.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@spec/memory.md`:
- Line 405: Update Section 3.1’s oversized-span allocation rule to round up to
enough 1 MiB chunks to cover the entire payload, using ceil(block_size / 1 MiB)
rather than truncating integer division. Preserve exact sizing for boxed
payloads while ensuring payloads just over a MiB boundary receive an additional
chunk.
- Around line 342-346: The dynamic-region reuse policy must preserve alignment,
not only exact byte size. Update the size_stack reuse logic described in the
dynamic allocation and return sections to key blocks by both size and alignment,
or validate alignment before reusing a block and fall back to frontier
allocation when it does not satisfy the request.

In `@spec/syntax.md`:
- Around line 284-289: Add a `> **Story:**` pointer immediately before the
section separator in the recursive-storage discussion, linking to the applicable
story chapter heading. Keep the existing explanation of compiler boxing and `&`
aliasing unchanged.

In `@stories/adt.md`:
- Line 150: Rewrite the paragraph’s cycle example to accurately describe the
graph: acknowledge both back edges, explain that removing Expr.op alone breaks
the cycle, and that breaking it through child edges requires removing both
Operation.left and Operation.right; alternatively, replace it with a genuinely
single-back-edge example while preserving the rule that every member edge on a
cycle is boxed.

---

Outside diff comments:
In `@spec/memory.md`:
- Line 393: Update the dynamic block-size description to remove “classes” and
any implication of sub-128 size buckets or flooring. Require exact type-size
allocation for boxed payloads, retain powers-of-two sizing only for growable
backing stores, and describe boxed reuse as stacks keyed by exact byte size.
- Around line 580-586: Rewrite the “Boxed hosting field” row to state that the
fixed-size handle is stored inline with its enclosing host, which may be a
fixed-size scope slot or a dynamic payload; only the boxed payload referenced by
the handle resides in the dynamic region. Preserve the existing recursive-type
rationale and compiler-selection behavior, aligning the wording with Sections
3.3 and 3.5.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 06769c7c-c45a-435f-9f18-9e1a05dec60c

📥 Commits

Reviewing files that changed from the base of the PR and between 42e8364 and d06b6ad.

📒 Files selected for processing (9)

• README.md
• spec/adt.md
• spec/foundations.md
• spec/glossary.md
• spec/lifetimes.md
• spec/memory.md
• spec/syntax.md
• stories/adt.md
• stories/memory.md

[TheLazyCat00]

what does that mean? can value types not store things in variants?

[TheLazyCat00]

Value types can absolutely be stored in variants — that bullet was badly worded and read as a much wider restriction than it is. Fixed in 68bc769.

Two separate things were running together:

• What a variant may hold. A #variant case payload can be any type. A value variant can hold value payloads. Neither is affected here.
• Whether a variant may lead back to itself. Only that is restricted, and only for the value form.

And "only a reference type may own boxed storage" was assertion, not reason. The reason is that a box is ownership. A boxed payload lives in the dynamic region and something has to decide when it dies; that something is a host. A value type has no host, no anchor, and no destruction tracking (memory.md §2.10), and it is copied by a mechanical inline write. Give it a box and the copy has exactly two options, both fatal:

• copy the handle — two values now name one payload, so a value is aliased, which is the thing §2.10 exists to prevent and which concurrency.md §4 leans on when it lets a value be shared by snapshot and mutated concurrently; and nothing hosts the payload, so nothing frees it;
• copy the payload — assignment becomes allocating and costs time proportional to the structure, which is not what "copied as an ordinary inline value" means.

§2.10 now states that reasoning where the rule lives, with an illegal example alongside the existing two, and the bullet here says what is and is not restricted.

---

Generated by Claude Code

[TheLazyCat00]

would recursive variants not also work with value types? my example only used #variant because it had intLit which is a String which is itself a reference type.

[TheLazyCat00]

You're right about the example, and it was doing real damage — fixed in 68bc769.

Expr is a #variant for two independent reasons and the section only claimed one. intLit String forces it on its own: String is a reference type and a value sum may not carry one (memory.md §2.10). So a reader who checks the example against the rule finds it proves nothing about recursion. §3 now says that outright and isolates the rule with a pair whose payloads are all value types:

type Nat = variant { zero Unit; succ Nat; }        // ILLEGAL: a value sum cannot lead back to itself
type Peano = #variant { zero Unit; succ Peano; }   // legal: `succ` is a boxed hosting member

On the substance — no, recursion does not work for value types, and it is not an accident of how the rule was written. Boxing is the only finite layout for a self-reference, and a boxed payload is owned storage in the dynamic region. A value type has no host, no anchor, no destruction tracking, and is copied by a mechanical inline write. That copy would have to either duplicate the handle, leaving two values naming one payload with nothing hosting it, or duplicate the payload, making assignment allocating and tree-sized. The first aliases a value, which is exactly what concurrency.md §4 relies on being impossible; the second is not a value copy. Full reasoning is in the reply on the §1 bullet.

If you want value recursion anyway, the thing to attack is the copy rule, not this section — a value sum could recurse if a value copy were allowed to be deep. That is a much bigger change (it gives value types a teardown obligation and makes assignment fallible), so I have not touched it. Say the word and I will open an issue rather than bury it here.

---

Generated by Claude Code

[TheLazyCat00]

Correcting my own reply above: "it gives value types a teardown obligation" is wrong and withdrawn, along with a second objection I raised after it. Both are now tracked in #156.

• Teardown. I conflated the anchor tracking a reference type needs — so a guest can tell whether its host died — with knowing when a value dies. The latter is lexical (lifetimes.md §2.1 plus overwrite), so the teardown walk is code emitted at a known point, and memory.md §3.2 already specifies that exact recursive block-return for reference hosts. Nothing new to invent, and a loop does not leak: overwrite frees and immediately repops the same exact-size stack.
• The concurrent snapshot. I then argued it was use-after-free needing hazard pointers or epoch reclamation. That assumed freeing can unmap memory, which this arena never does while a reader could run — §4.1's water tower keeps the scope alive and §3.2 unmaps only at drain, so a freed block is recycled inside a live mapping. A stale read yields garbage, not an invalid access, which is the same failure class the flat case already retries through.

What actually survives: an allocating O(structure) =, and for spawn readers a bounded walk with offset validation, allocator contention on the per-scope size stacks, and O(structure) retry cost. Real, but ordinary — not a reclamation scheme.

Nothing here changes this PR; adt.md §4 and memory.md §2.10 describe the language as it stands. Flagging it so the thread does not leave a withdrawn argument standing as the reason.

---

Generated by Claude Code

[TheLazyCat00]

You were right, and my "no" is now reversed in the spec. 804631f and d0cd470.

Once both of my objections were withdrawn there was nothing holding the ban up — what was left was a cost list, and I had been reading it as an impossibility. So:

type Nat = variant { zero Unit; succ Nat; }        // now legal
type Peano = #variant { zero Unit; succ Peano; }   // still legal

A value copy is deep (memory.md §2.3). Copying a value copies its inline bytes plus a fresh allocation and recursive copy of every boxed payload it owns, so two values never share a node. A value with no boxed member — every value type anyone has written — is still copied by copying its bytes, unchanged. Boxing itself is now available on both sides of the # axis (memory.md §3.3): in a reference type the boxed member hosts its child, in a value type the value owns it outright.

The #-field and &-field bans stay, on your reason rather than the one the spec had. "Copying would silently duplicate hosting" was vague; a reference type exists in order not to be copied is the actual argument, and it also explains why a List field stays out. memory.md §2.10 now states it in those terms — duplicate the object and you mint a second identity that guests do not follow, share it and hosting is no longer single.

What # decides is therefore smaller than it was: identity, aliasing, and copy-versus-move. Not whether a type may contain itself — that turned out to be a layout question, and layout answers it the same way for both kinds.

Costs are stated where they land rather than buried. Copying such a value allocates and is O(structure), and a spawn snapshot of one has to validate offsets and stop at a depth bound, allocates from the scope's size stacks, and retries at O(structure) (concurrency.md §4.4). Two chapters record how we got here — "What a copy is for, and the ban that survived it" and "The sum that could not contain itself" — including the fact that the merged claim transitively-value therefore non-recursive was a non sequitur we had not examined.

#156 stays open for the part I did not do: whether a deep-copied List inside a value type should be legal, and whether # reduces to identity and aliasing alone. That reaches foundations.md and wants its own change.

---

Generated by Claude Code

[TheLazyCat00]

i feel like we're repeating ourselves often. there should be one source of truth which should simple be referenced when needed

[TheLazyCat00]

Agreed, and it was worse than repetition — consolidating it exposed a contradiction. Fixed in 68bc769.

The exact-size rule was stated three times, with the rationale twice:

• §3.2 ¶3 — the rule, plus why a growable store's power-of-two sizes are a consequence of doubling rather than a classification;
• §3.6 ¶ here — the same sizing and alignment restated;
• §3.6 ¶ following — a whole paragraph re-arguing why a boxed payload has no class;
• §3.6 ¶ after that — the alignment rule a third time, plus frontier rounding already given in §3.2 ¶2.

§3.2 is "Allocation, reuse, and teardown", so it owns sizing, alignment and reuse. §3.6 now describes only what is specific to the two-part handle/payload representation and defers: "the payload is one reference-type instance, sized and aligned as §3.2 specifies". The re-argument paragraph is gone — the rationale lives in §3.2 and, at length, in the story chapter.

The contradiction: 2891b02 rekeyed the reuse stacks to (size, alignment) in §3.2 ¶2, but ¶4 still read "The stacks are keyed by byte size alone". Two paragraphs apart, flatly contradicting each other, and I would not have seen it while the rule was scattered over two sections. ¶4 now keys on both.

Also dropped "size class" from the two handle passages (§3.6 ¶1 and growth rule 5) in favour of "block size", since the region has no classes and the word was left over from when it did.

---

Generated by Claude Code

[TheLazyCat00]

i feel like this is a confusing introduction. maybe first start with what the issue was and then explain the change

[TheLazyCat00]

Fair — it opened by telling you what the fuse wasn't, which only lands if you already know the size argument that comes two paragraphs later. Reordered in 68bc769.

It now opens on the program that did not compile, says it was rejected and why, walks into Leaves, and only then names the fuse:

That is what lit the fuse — not a size calculation, but noticing what we had to write in order to use a variant at all.

So the negation arrives after you have seen both things it distinguishes, instead of before either. Nothing else in the chapter moved; the rest already runs problem → diagnosis → deeper mistake → fix → costs.

(The chapter is unmerged on this branch, so reordering it is not an append-only violation — the diff against main is still additions-only, verified.)

---

Generated by Claude Code

[TheLazyCat00]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[coderabbitai]

Actionable comments posted: 6

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

spec/lifetimes.md (1)

35-42: 🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick win

Add a move-source glossary entry. spec/glossary.md has no entry for this normative term. Define #variant case forms and link to lifetimes.md §1.2.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/lifetimes.md` around lines 35 - 42, Add a normative “move-source” entry
to spec/glossary.md, defining the term and covering direct host symbols, hosting
verb results, and `#variant` case forms. Link the entry to lifetimes.md §1.2,
including the distinction that only reference-sum `#variant` cases qualify.

Source: Coding guidelines

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@spec/concurrency.md`:
- Around line 129-132: Update the boxed-member snapshot walk to validate each
handle’s complete payload span before any typed dereference, including bounds,
payload size, live-region containment, and alignment. Abort the walk and retry
through the existing version-check path whenever validation fails, rather than
interpreting recycled bytes. Extend the summary near the existing walk rules to
explicitly include these payload-span checks.

In `@spec/foundations.md`:
- Around line 90-92: The descriptions conflate ordinary value-parameter
borrowing with deep-copy operations. In spec/foundations.md lines 90-92, remove
“passed” from the copy-operation list or limit it to explicitly copy-producing
bindings; in spec/adt.md line 169, replace “every argument pass” with stores
into fresh storage and payload construction, preserving ordinary argument
passing as read-only borrowing.

In `@spec/memory.md`:
- Around line 327-328: Update the fixed-size region bullet to limit boxed-member
handles to those materialized in scope-level slots. Clarify in the dynamic
region description that nested boxed handles remain within their owning dynamic
payload block.
- Line 345: Update the oversized-span description to say its handle stores the
exact block size rather than a size class, and include the alignment if that
metadata is stored by the handle. Keep the existing segmented-offset and
exact-size reuse behavior unchanged.
- Around line 389-392: Define boxed payload behavior from the member’s declared
type, not the enclosing type: in spec/memory.md at lines 389-392, preserve
separate reference-typed and value-typed rules for backpointers, guesting,
identity, deep copying, relocation, and destruction; update the corresponding
glossary definition in spec/glossary.md at lines 257-260 to match this canonical
distinction.

In `@stories/adt.md`:
- Line 142: Update the explanation in the “inlining is the wrong default”
passage to preserve the fixed-layout invariant: state that a variant has a fixed
size determined by its tag and largest case, and identify the actual failure as
an inline recursive cycle having no finite layout. Remove wording that implies
sum types generally lack a settled size.

---

Outside diff comments:
In `@spec/lifetimes.md`:
- Around line 35-42: Add a normative “move-source” entry to spec/glossary.md,
defining the term and covering direct host symbols, hosting verb results, and
`#variant` case forms. Link the entry to lifetimes.md §1.2, including the
distinction that only reference-sum `#variant` cases qualify.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 8057025d-d9bc-4e72-8524-239623a05bfa

📥 Commits

Reviewing files that changed from the base of the PR and between d06b6ad and d0cd470.

📒 Files selected for processing (11)

• README.md
• spec/adt.md
• spec/concurrency.md
• spec/foundations.md
• spec/glossary.md
• spec/lifetimes.md
• spec/memory.md
• spec/syntax.md
• spec/types.md
• stories/adt.md
• stories/memory.md

[TheLazyCat00]

Review addressed in f6f7ca5 — five of six taken, one taken in part.

Boxed payload semantics follow the declared member type (memory.md §3.3, glossary.md §3.39). This was the real bug and I had it backwards. My wording keyed everything on the enclosing type's kind, which breaks precisely where off-cycle boxing is permitted: a #struct may box a value-typed member, and my text would have handed that payload a backpointer and made it guestable. §3.3 now splits the two questions, because two different types answer them — what the payload is follows the member's own declared type (identity, backpointer, guestability), while what becomes of it on move, copy, or death follows the enclosing kind (hosted, or owned and deep-copied).

The snapshot walk validates a payload span, not an offset (concurrency.md §4.4). Correct, and my rule was too weak: an offset landing inside a live region does not prove that a payload's worth of bytes fits before the region ends. The walk now must check base, size, and alignment before any typed read, and aborts rather than interpreting the bytes when that fails. Generation and type-identity checks stay unavailable, as the analysis says — exact-(size, alignment) reuse means a recycled block can be a legitimate block of the same shape — which is why span validation plus the depth bound plus the version check is the whole contract.

memory.md §3.1 — both taken. Fixed-size region scoped to handles materialized in scope-level slots, with nested handles stated as part of their owning dynamic block; and the oversized-span handle now records its exact block size and alignment, since the region has no size classes left.

stories/adt.md — taken. "A sum does not [have one settled size]" did contradict fixed layout. A variant is its tag plus its widest case, one fixed size; what actually fails is following that chain around a cycle. Reworded to say that, keeping the passage's point that the size is not readable from the member in front of you.

move-source glossary entry — added as §3.41. Reasonable here specifically because §1.2 gained a third form in this PR.

Partly declined: the value-parameter conflation. The substance is right and is fixed — adt.md §4 said "every assignment, argument pass, and return", and a value-type parameter is a read-only borrow (memory.md §2.9), so passing one is not a copy at all. I found the same slip in two more places you did not flag, memory.md §2.10 and glossary.md §3.2, and fixed all three to say "bound into a fresh slot". But the foundations.md §7 half of the finding is incorrect: that passage says "copied on assignment" and "copying such a value allocates and walks its structure" — the word "passed" does not appear in it, so there was nothing to remove.

All three CLAUDE.md guards re-run clean at f6f7ca5, and the story append-only check against origin/main is additions-only on both files.

---

Generated by Claude Code

[TheLazyCat00]

It needs to be explained why recursive variants require to be boxed. As far as i understand it, it would also be possible to inline recursive variants, because all recursive variants have leafs at some point; they're not infinitely recursive.

[TheLazyCat00]

(comment by ChatGPT)

I like the overall direction, including the order-independent cycle-boxing rule and allowing recursive value types through deep copy. Reviewing the current head (f6f7ca5), I found three load-bearing gaps that should be settled before merge:

1. Define direct initialization and overwrite ordering for deep values. memory.md §2.3 says declarations, assignments, stores, and returns copy a value; adt.md §3 says Nat.succ(n) deep-copies n; and a value-variant case form is explicitly not a move-source. Taken literally, two Nat = Nat.succ(Nat.succ(...)) copies each inner temporary into its parent and then copies the completed temporary again into two, making ordinary recursive construction quadratic. The overwrite rule also returns the destination's owned blocks before the replacement becomes live, so x = x and an RHS projected from the destination need explicit copy-before-destroy semantics. Please specify direct construction/copy elision for fresh value-producing forms and state that RHS materialization completes before destination teardown, or define the intended alternative explicitly.

2. Reconcile snapshot allocation with destination-scope placement. concurrency.md §4.4 says a deep snapshot allocates from “the same per-scope size stacks the writer is pushing to,” but memory.md §3.5 says a value copy allocates each boxed payload in the destination scope's dynamic region. A snap binding inside spawned work generally belongs to a different scope from the shared value being mutated. Either specify a source-scope staging allocation, or change the contention/synchronization rule to describe the actual destination stack.

3. Validate discriminants before traversing stale bytes. The new span, alignment, live-region, and depth checks prevent invalid address walks, but a recursive variant requires reading its tag before the walker knows which child handles exist. Until the final version check succeeds, that tag is untrusted and may be torn or come from a recycled occupant. Require validation of every variant/enum discriminant—and any other structural metadata needed to locate child handles—before case dispatch or typed interpretation.

Non-blocking: the unrelated CLAUDE.md terminology guard is already acknowledged in the PR body; splitting it would keep this PR's scope cleaner.

[TheLazyCat00]

Your second point is important and i dont think we should try to determine the destination scope, as that's not always possible. For example, consider an io dependent if statement:

car Car()
garage Garage()
boat Boat()
if (input() == "garage") {
  garage.car = car
}
else {
  boat.car = car
}

I think it should instead just start in the initial scope and just move during runtime, instead of trying to statically determine the destination scope.

[TheLazyCat00]

(comment by ChatGPT)

Regarding Manuel's two surrounding comments:

Why recursive members cannot stay inline

The fact that each runtime value eventually reaches a leaf does not give the type a finite inline size. Layout has to be fixed before any value exists and cannot depend on its eventual depth. For a declaration such as:

type Nat = variant { zero Unit; succ Nat; }

an inline layout would require the storage for Nat to contain the full storage for another Nat, which must contain another full Nat, and so on. Equivalently, its size equation contains itself with no finite solution. A particular value may have only three nodes, but another may have three million; there is no fixed maximum depth from which one inline stride can be derived.

It would be possible only under a different language model where values have runtime-dependent sizes and containers store variable-stride elements. That would contradict Zane's fixed-layout and uniform-stride foundations. The PR should explain this distinction explicitly: the leaf terminates a value, not the recursive type's compile-time layout.

Runtime destination scope

I agree that the runtime does not need to predict which control-flow branch will execute. A value can begin in the arena where it is constructed; when a particular destination store executes, its owned blocks can be relocated or deep-copied into that destination's arena at runtime. “Destination scope” should describe the destination of the store that actually executes, not a scope selected by compile-time control-flow prediction.

There is a separate conflict with the current lifetime rules, however: the example moves car, declared outside the if, from inside a nested branch. lifetimes.md §1.3 currently forbids exactly that—moves must occur in the symbol's declaration block, specifically to avoid conditional and flow-dependent host changes. Making this example legal would therefore be a broader change to the move model, not merely a clarification in this PR.

For the snapshot finding in my review, the narrower issue remains: a deep snapshot is a copy into its fresh snapshot binding, so its blocks should belong to that binding's scope. The current statement that the reader allocates from “the same per-scope size stacks the writer is pushing to” appears to place them in the source/writer arena instead. The spec should either state why reader and writer necessarily share an arena or change this to the snapshot destination's arena.

---

Attribution: This comment and review #pullrequestreview-4842777435 were written by ChatGPT through the connected GitHub tool, not manually authored by Manuel. I will prefix every further GitHub comment I post with (comment by ChatGPT).

[TheLazyCat00]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[coderabbitai]

Actionable comments posted: 2

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

spec/memory.md (1)

419-419: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

Qualify when values are copied instead of rehosted.

Section 3.3 makes the enclosing type control movement of a boxed payload. Section 3.5 also relocates every block owned by a reference host. The unqualified sentence at Line 419 can make an off-cycle value-typed boxed member appear to deep-copy during reference-host rehosting. Limit this rule to a value that is itself copied into a new slot.

Proposed clarification

-A value reaches a new scope by being copied rather than rehosted, and the same recursion applies to its blocks:
+When a value itself is copied into a new slot, it reaches the new scope by copying rather than rehosting, and the same recursion applies to its blocks:

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/memory.md` at line 419, Revise the value-copying statement in Section
3.3 so it applies only when the value itself is copied into a new slot or scope.
Clarify that this rule does not govern boxed members relocated during
reference-host rehosting, whose movement follows the enclosing type and
ownership rules in Sections 3.3 and 3.5.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@spec/adt.md`:
- Line 179: Clarify the recursive value-copy rule in spec/adt.md at line 179 by
qualifying “a return of one” as returning an existing value or place, while
preserving that fresh non-place results construct directly. Apply the same
clarification to the “return stores” wording in stories/adt.md at line 171,
specifying that these stores originate from existing values.

In `@spec/concurrency.md`:
- Around line 133-134: Update the depth-bound rules so exhaustion is a terminal
snapshot failure after provisional allocations are cleaned up, rather than a
retryable stale-data failure. In spec/concurrency.md lines 133-134, state this
cleanup and terminal behavior; update the retry summary at spec/concurrency.md
lines 191-191 to limit retries to retryable validation or version failures;
align stories/memory.md lines 225-225 with the same terminal depth-failure rule.

---

Outside diff comments:
In `@spec/memory.md`:
- Line 419: Revise the value-copying statement in Section 3.3 so it applies only
when the value itself is copied into a new slot or scope. Clarify that this rule
does not govern boxed members relocated during reference-host rehosting, whose
movement follows the enclosing type and ownership rules in Sections 3.3 and 3.5.

🪄 Autofix

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 4115e959-b5bc-4326-b595-f75886335ef2

📥 Commits

Reviewing files that changed from the base of the PR and between d0cd470 and 2342b53.

📒 Files selected for processing (6)

• spec/adt.md
• spec/concurrency.md
• spec/glossary.md
• spec/memory.md
• stories/adt.md
• stories/memory.md

[coderabbitai]

🩺 Stability & Availability | 🟠 Major | 🏗️ Heavy lift

Make depth exhaustion a terminal result instead of a retry.

All three passages treat a depth-limit failure like stale data. A valid value deeper than the bound can never succeed, so the reader can retry indefinitely.

• spec/concurrency.md#L133-L134: define depth exhaustion as a terminal snapshot failure after provisional cleanup.
• spec/concurrency.md#L191-L191: update the summary so retries apply only to retryable validation or version failures.
• stories/memory.md#L225-L225: align the story with the terminal depth-failure rule.

📍 Affects 2 files

• spec/concurrency.md#L133-L134 (this comment)
• spec/concurrency.md#L191-L191
• stories/memory.md#L225-L225

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/concurrency.md` around lines 133 - 134, Update the depth-bound rules so
exhaustion is a terminal snapshot failure after provisional allocations are
cleaned up, rather than a retryable stale-data failure. In spec/concurrency.md
lines 133-134, state this cleanup and terminal behavior; update the retry
summary at spec/concurrency.md lines 191-191 to limit retries to retryable
validation or version failures; align stories/memory.md lines 225-225 with the
same terminal depth-failure rule.

[TheLazyCat00]

Round addressed in 940f297 — two taken, one raised rather than decided.

Taken: the return-store qualification (adt.md §4, stories/adt.md). Correct. Listing "a return" among the O(structure) operations contradicts the rule that a fresh non-place result constructs in its destination — a return of an existing value is a copy, a return of a freshly built one is not. Both passages now say the source must be an existing value.

Taken: memory.md §3.5. Also correct, and a sharper catch than it looks. "A value reaches a new scope by being copied rather than rehosted" sat immediately after the reference-host relocation rule, so it read as though a value-typed payload owned by a #struct through an off-cycle boxed member would be deep-copied when that host is rehosted. It is relocated with its host — what becomes of a boxed payload follows the enclosing type's kind (§3.3). Now scoped to the value that is itself copied, with that pointer made explicit.

---

Raised, not taken: depth exhaustion as a terminal failure.

The hole is real. A legal value deeper than the bound fails validation on every attempt, so "retry" never converges — that is a livelock, not a stale read, and the three passages do currently lump it in with torn data.

But I don't think the proposed fix can be applied as a wording change, because it adds an observable failure mode that snap does not have. §4.4's promise is a tear-free snapshot that never blocks and always succeeds. Zane has no silent failures, so a snapshot that can terminally fail would have to become abortable — ?/?? on snap VarType = shared — and that is a change to the surface and to what §4.4 guarantees, not a clarification of it. Worth a deliberate decision.

Three ways out, as I see them:

1. Terminal failure, as proposed. snap becomes abortable. Honest, but it puts an error path on the one read that was specified never to have one, and every spawn reader of a boxed value now carries a handler.
2. Bound the walk by something a legal structure cannot exceed. The writer publishes its structure's depth alongside the version; the reader bounds on that. Exceeding it then always means recycled bytes, which is genuinely retryable, and a legal deep value always succeeds. Keeps the §4.4 guarantee intact. Cost: the writer maintains a depth count, and every node insert or replace has to keep it current.
3. Cap depth as a language limit. Over-deep values become illegal to construct rather than un-snapshottable, moving the failure to construction where an error path already exists. Simplest to specify, but it puts an arbitrary constant in foundations.md-adjacent territory.

I lean toward 2 — it is the only one that does not add a failure where the spec promised none, and the depth count is cheap next to the allocation a deep copy already does. But this changes what snap guarantees either way, so it is your call rather than mine. Say which and I will write it up across §4.4, the summary row, and the memory story.

All three CLAUDE.md guards re-run clean at 940f297; story append-only check against origin/main is additions-only on both files.

---

Generated by Claude Code

[TheLazyCat00]

please make sure that the spec doesnt repeat itself. if there are two places where something is explained, it could happen that they drift apart

[TheLazyCat00]

why do we use Nat as the name for this example?

[TheLazyCat00]

i feel like we're saying too much stuff here, there should simply be one source of truth that explains variant and its boxing behaviour instead of explaining it in multiple places

[TheLazyCat00]

here too: is the glossary the right place to explain it or would it be better to simply link it?

[TheLazyCat00]

All three duplication points taken, in 7d2769c. You were right that it had spread — I audited every passage over 200 characters that mentions boxing or copying, and the two rules were each being argued at length in four or five files.

The general rule first. Canonical homes, which the glossary had already declared and the prose had quietly stopped respecting: recursion and boxing in adt.md §4, the deep value copy in memory.md §2.3, value-downstream enforcement in memory.md §2.10, representation in memory.md §3.3 and §3.6. Everywhere else now states only what is its own business and links for the rest.

foundations.md §7 — you were right, and the file says so itself. Its own preamble reads "It introduces no rules of its own — each foundation is specified canonically by another document, and this is the map." I had put a full re-derivation there: why a value cannot hold a reference type, what a boxed member is, why a deep copy makes recursion safe, what it costs. All of that is memory.md and adt.md's job. §7 now records one thing — that the axis does not decide recursion — and links adt.md §4.

glossary.md — same answer, same reason. §1 of that file says an entry gives "only a short summary, not the full rule." §3.39 had grown past 1200 characters, §3.2 and §3.40 past 800. All three are back to a summary plus the canonical-home line. The rule is now written once and named three times, instead of written four times.

Also trimmed for the same reason: adt.md §4 stopped re-deriving what a deep copy does (it keeps the recursion rule, which is its own), memory.md §2.10 keeps only why a boxed member does not violate the closure and drops the representation, and types.md §2.2's recursion sentence is now a pointer.

---

On Nat — a fair question, and I think the pairing is worse than the name.

Nat is the Peano encoding of the natural numbers: zero, or the successor of another Nat. I picked it because it is the smallest recursive type whose payloads are all value types, which is exactly what the example has to isolate — Expr cannot demonstrate the recursion rule, because its # is already forced by intLit String. Nat has nothing in it but the recursion.

Two things are wrong with it though, and the second is the real one:

1. The name assumes type-theory background. Nat/zero/succ is standard in that literature and opaque outside it.
2. Nat and Peano are the same concept under two names. "Peano" is literally the mathematician attached to Nat's encoding, so the pair reads as though the value form and the reference form are different ideas when the entire point is that they are the same structure differing only in #.

So I'd rather change it than defend it. Options, and it is your call on taste:

// A — plain English, no background assumed, same minimal shape
type Countdown = variant  { done Unit; more Countdown; }
type Chain     = #variant { done Unit; more Chain; }

// B — keep Nat, fix only the misleading second name
type Nat    = variant  { zero Unit; succ Nat; }
type NatRef = #variant { zero Unit; succ NatRef; }

I lean toward A: it drops the background assumption and the two names no longer pretend to be different concepts. Tell me which and I'll change it in adt.md §3 and the two story chapters that reference the pair.

Guards clean at 7d2769c; story append-only additions-only on both files. Still waiting on your pick for the depth-bound question in my previous comment.

---

Generated by Claude Code

[TheLazyCat00]

yes, i option A seems to be the best. also, the rule for one canonical home is in the contribution guidelines right? otherwise we'd have to state it there too

[TheLazyCat00]

Option A applied in 3df8c45:

type Countdown = variant  { done Unit; more Countdown; }
type Chain     = #variant { done Unit; more Chain; }

Renamed across adt.md §3 and §4, memory.md §2.3 and §2.10, and both story chapters on this branch. Nothing else in the spec used Nat, Peano, or succ, so there is no stray left behind.

On the guidelines — it is already there, so nothing to add. contributing/writing-spec-docs.md §8 says it outright:

Do not duplicate content between files — add it in the canonical place and cross-reference from others.

and §1 says the same from the other side: "If you need to mention a concept that is canonically specified elsewhere, keep the mention brief and add a cross-reference rather than restating it."

So I broke a rule that was already written down, rather than one that needed writing. Worth saying plainly, because it changes what the fix is: adding a fresh statement of the rule to the guidelines would be its own small instance of the problem — the same instruction in two places, free to drift. The guide is fine; the prose drifted away from it over many edits, each of which looked locally reasonable.

If you want a belt-and-braces guard, the thing that would actually catch it is mechanical rather than prose — something like flagging any passage outside a rule's canonical home that grows past a length threshold while restating it. That is not something a grep does well, and I would not add it to this PR, but it is the shape of what would have caught this drift.

Guards clean at 3df8c45; story append-only additions-only on both files.

Still open for you: the depth-bound question from two comments up, the four original review threads, and whether to split d06d2e0.

---

Generated by Claude Code

[TheLazyCat00]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[coderabbitai]

Actionable comments posted: 2

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

spec/memory.md (1)

402-402: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

Define guest creation from boxed variant payloads.

spec/adt.md defines variant-member reads as partial and abortable. The boxed-member rule says a reference-typed boxed payload may be guested from an enclosing field access, but it does not say whether a live live-case read such as Expr.op can mint &Operation, or whether that abortable access is a valid guest source. Specify this contract before using boxed variant payloads as guest sources.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/memory.md` at line 402, Clarify the boxed variant payload rule in the
guest-creation section around the member payload semantics: define whether a
live-case variant-member read such as Expr.op may create a guest reference to a
reference-typed boxed payload, and whether the partial/abortable read is an
admissible guest source. State the required behavior for absent or invalid
cases, and align the wording with the variant-member read rules in adt.md.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@spec/adt.md`:
- Around line 174-177: Define the containment-cycle predicate using only
owning/hosting edges, excluding explicit & guest members because their
fixed-size storage does not require boxing. Update the boxing rules in
spec/adt.md lines 174-177, spec/glossary.md lines 257-260, and spec/memory.md
lines 398-399 to consistently use this predicate; all three sites require the
corresponding wording change.

In `@stories/memory.md`:
- Line 225: Update the canonical snapshot rule in concurrency.md §4.4 to
explicitly define the observable result when the per-attempt depth bound is
reached: abort the attempt, roll back its allocations, and retry rather than
returning an incomplete snapshot. Align the wording in the memory story’s
snapshot description with that rule.

---

Outside diff comments:
In `@spec/memory.md`:
- Line 402: Clarify the boxed variant payload rule in the guest-creation section
around the member payload semantics: define whether a live-case variant-member
read such as Expr.op may create a guest reference to a reference-typed boxed
payload, and whether the partial/abortable read is an admissible guest source.
State the required behavior for absent or invalid cases, and align the wording
with the variant-member read rules in adt.md.

🪄 Autofix

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 5b7e7bd1-a507-43b2-809c-376cfa9c89d5

📥 Commits

Reviewing files that changed from the base of the PR and between 2342b53 and 3df8c45.

📒 Files selected for processing (7)

• spec/adt.md
• spec/foundations.md
• spec/glossary.md
• spec/memory.md
• spec/types.md
• stories/adt.md
• stories/memory.md

[coderabbitai]

🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail

echo "== files =="
git ls-files | rg '(^|/)spec/(adt|memory|glossary)\.md$|(^|/)stories/.*\.md$' || true

echo "== adt relevant =="
if [ -f spec/adt.md ]; then
  sed -n '1,240p' spec/adt.md | nl -ba | sed -n '130,210p'
fi

echo "== glossary boxed member =="
if [ -f spec/glossary.md ]; then
  sed -n '220,280p' spec/glossary.md | nl -ba | sed -n '1,80p'
fi

echo "== memory boxing relevant =="
if [ -f spec/memory.md ]; then
  sed -n '350,440p' spec/memory.md | nl -ba | sed -n '1,120p'
fi

echo "== search ownership/guest terms =="
rg -n '"(owning|guest|hosting|boxed|&T|&)"|ownership|guest-source|guest source|&T|& ' spec/adt.md spec/glossary.md spec/memory.md spec/*.md 2>/dev/null | head -200 || true

Repository: zane-lang/spec

Length of output: 578

---

🏁 Script executed:

#!/bin/bash
set -euo pipefail

echo "== adt relevant =="
sed -n '130,210p' spec/adt.md

echo "== glossary boxed member =="
sed -n '220,280p' spec/glossary.md

echo "== memory boxing relevant =="
sed -n '350,440p' spec/memory.md

echo "== search ownership/guest terms =="
rg -n '"(owning|guest|hosting|boxed|&T|&)"|ownership|guest-source|guest source|&T|& ' spec/adt.md spec/glossary.md spec/memory.md spec/*.md 2>/dev/null | head -200 || true

echo "== adt outline if available =="
ast-grep outline spec/adt.md --view compact 2>/dev/null || true

Repository: zane-lang/spec

Length of output: 50372

---

🏁 Script executed:

#!/bin/bash
set -euo pipefail

python3 - <<'PY'
from pathlib import Path

files = [Path("spec/adt.md"), Path("spec/glossary.md"), Path("spec/memory.md")]
needles = [
    "declared type can lead back to the enclosing type",
    "where the member's declared type can lead back to the enclosing type",
    "A boxed member is laid out the same way. A member whose declared type can lead back to the enclosing type",
    "contains back to",
    "&",
    "guest",
    "hosting",
    "owning",
    "boxed member",
]
lines = {p: tuple(p.read_text().splitlines()) for p in files}

for p in files:
    print(f"\n-- {p} --")
    for i, text in enumerate(lines[p], start=1):
        if any(needle in text for needle in needles):
            print(f"{i}: {text}")

for p in files:
    txt = "\n".join(lines[p])
    print(f"\n{p}: boxed-member occurrence count =", txt.count("boxed member") + txt.count("boxed Member") + txt.count("BOXED MEMBER"))
    print(f"{p}: ownership/containment phrased as containing guest edges? any guest containment cycle rule?")
    for needle in ["cycle of guests", "cycle of guests", "guest containment", "guest graph", "containment graph", "containment cycle"]:
        print("   ", needle, "=>", txt.count(needle))
PY

Repository: zane-lang/spec

Length of output: 50370

---

Define boxing by owning/hosting edges only.

& storage is fixed-size guest-only storage, so an explicit & back-edge must not trigger the required boxing rule. Define one containment-cycle predicate that covers owning/hosting members, then use it in:

• spec/adt.md#L174-L177
• spec/glossary.md#L257-L260
• spec/memory.md#L398-L399

📍 Affects 3 files

• spec/adt.md#L174-L177 (this comment)
• spec/glossary.md#L257-L260
• spec/memory.md#L398-L399

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/adt.md` around lines 174 - 177, Define the containment-cycle predicate
using only owning/hosting edges, excluding explicit & guest members because
their fixed-size storage does not require boxing. Update the boxing rules in
spec/adt.md lines 174-177, spec/glossary.md lines 257-260, and spec/memory.md
lines 398-399 to consistently use this predicate; all three sites require the
corresponding wording change.

[coderabbitai]

🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail

echo "Files matching relevant names:"
fd -a '^(memory|concurrency)\.md$' . | sed 's#^\./##'

echo
echo "Check git tracked matching files:"
git ls-files '*/memory.md' '*concurrency.md' | sed 's#^\./##'

echo
echo "Context around stories/memory.md line 225:"
if [ -f stories/memory.md ]; then
  nl -ba stories/memory.md | sed -n '205,245p'
fi

echo
 echo "Search per-attempt depth bound references:"
rg -n "depth|bound|exhaust|snapshot|concurrency|§4\.4|4\.4" stories/memory.md spec/concurrency.md 2>/dev/null || true

echo
if [ -f spec/concurrency.md ]; then
  echo "concurrency.md outline-like line numbers with relevant sections:"
  nl -ba spec/concurrency.md | sed -n '1,260p' | rg -n -C 2 "depth|bound|snapshot|reader|version|retry|alloc|allocation|rollback|reject|stale|aborted|invalid|concurrent|reads|takes|coherent" || true
fi

echo
if [ -f spec/concurrency.md ]; then
  echo "grep exact line locations:"
  grep -n -i "depth\|bound\|snapshot\|reader\|version\|retry\|alloc\|rollback\|reject\|stale\|invalid\|concurrent\|read" spec/concurrency.md || true
fi

Repository: zane-lang/spec

Length of output: 531

---

🌐 Web query:

zane-lang spec concurrency pinned anchor reads take a coherent snapshot

💡 Result:

There is no evidence in the Zane programming language specification (zane-lang) [1][2] regarding "pinned anchor reads" or "coherent snapshots" as part of its concurrency model. The terms "pinned," "coherent snapshot," and "concurrency" appearing together in technical contexts appear to be related to other domains, such as distributed systems snapshot protocols (e.g., in agent-coherence/agent-coherence [3][4]) or unrelated discussions regarding Rust/Zig pinning [5][6]. Zane is a recently created language (established March 2026) [1] and its documentation does not currently contain these specific concurrency-related primitives.

Citations:

• 1: https://github.com/zane-lang
• 2: https://github.laiyagushi.com/zane-lang
• 3: feat(coordinator): consistent multi-artifact snapshot sessions (read-side transaction layer) Cohexa-ai/agent-coherence#132
• 4: https://github.com/Cohexa-ai/agent-coherence/blob/main/formal/tla/Snapshot.tla
• 5: https://rust-lang.github.io/async-book/part-reference/pinning.html
• 6: Proposal: Pinned Structs ziglang/zig#7769

---

🏁 Script executed:

#!/bin/bash
set -euo pipefail

echo "Context around stories/memory.md line 225:"
if [ -f stories/memory.md ]; then
  sed -n '205,245p' stories/memory.md | cat -n
fi

echo
echo "Search per-attempt depth bound references:"
rg -n "depth|bound|exhaust|snapshot|concurrency|4\.4|§4\.4" stories/memory.md spec/concurrency.md stories/concurrency.md spec/memory.md 2>/dev/null || true

echo
echo "Concise relevant concurrency.md sections:"
if [ -f spec/concurrency.md ]; then
  sed -n '1,280p' spec/concurrency.md | cat -n
fi

echo
echo "Verify pinned GitHub anchor resolution:"
python3 - <<'PY'
import urllib.request, re, urllib.parse

sha = "b1abb87712607119a4f6d3962e1baeb22a2367ca"
url = f"https://raw.githubusercontent.com/zane-lang/spec/{sha}/spec/concurrency.md"
try:
    text = urllib.request.urlopen(url, timeout=15).read().decode("utf-8", "replace")
except Exception as e:
    print(f"fetch_error: {type(e).__name__}: {e}")
    raise SystemExit(1)

anchors = re.findall(r'<a href="#([^"]+)">', text, flags=re.I)
targets = [m.group(1) for m in re.finditer(r'(?<=[ \t<\[])?(?:4\.4|section)[:\s]*(.+?)(?:\]|$)', text, flags=re.I+re.S)]
targets = [a.strip(" -:–—_.\"'\n") for a in targets if a.strip()]
print("sha:", sha)
print("found_anchors:", len(anchors))
print("contains_44:", "44-reads-take-a-coherent-snapshot" in anchors or any(re.search(r'(?i)reads\s+t[aT]ke\s+a\s+coherent\s+snapshot', a) for a in anchors))
print("anchor_candidates:", [a for a in anchors if "reader" in a.lower() or "snapshot" in a.lower() or "concurrent" in a.lower() or a.startswith("4")][:20])
PY

Repository: zane-lang/spec

Length of output: 50370

---

🌐 Web query:

github zane-lang spec concurrency.md 4.4 reads take a coherent snapshot depth bound exhausted retry

💡 Result:

There is no official documentation or specific specification file named concurrency.md in the Zane programming language repository (zane-lang/spec) that contains a section "4.4 reads take a coherent snapshot depth bound exhausted retry" [1][2]. The phrase "reads take a coherent snapshot... depth bound exhausted retry" describes a common pattern in concurrent system design and database implementation, often found in projects handling atomic state snapshots [3][4][5]. In such systems: 1. Coherent Snapshot: To avoid reading inconsistent (torn) state when multiple values must be read together, a system captures an immutable snapshot or uses a validation protocol to ensure all data belongs to the same state version [3][4][6]. 2. Depth Bound: Because concurrent writers may frequently update the state, a reader might repeatedly detect an inconsistency. A "depth bound" (or attempt limit) is implemented to prevent indefinite spinning or livelock, forcing the operation to return an error if it cannot successfully capture a coherent snapshot within a set number of tries [3][4]. 3. Retry: The system attempts to re-read the data upon detecting a concurrent modification, typically by validating a sequence counter or revision number before and after the read [7][4][5]. While this logic appears in various technical contexts—such as the Zakura blockchain core [3][4], Linux kernel block drivers [5], and distributed data stores [7][8]—it is not a recognized feature of the Zane language specification. Zane is a developing language [9] with repositories for its compiler and specification [1], but it does not currently feature this specific concurrency pattern in its official documentation [1].

Citations:

• 1: https://github.com/zane-lang
• 2: https://github.laiyagushi.com/zane-lang/zane-cpp
• 3: bug: make multi-read RPC responses use atomic state snapshots zakura-core/zakura#360
• 4: fix(state)!: make gettxout use one coherent state view zakura-core/zakura#421
• 5: https://www.mail-archive.com/linux-kernel@vger.kernel.org/msg1561203.html
• 6: https://docs.rs/poise-discovery/latest/src/poise_discovery/snapshot.rs.html
• 7: https://github.com/Thejuampi/memris/blob/main/docs/CONCURRENCY.md
• 8: https://github.com/rqlite/rqlite/blob/f9d5a860/store/DESIGN.md
• 9: https://zane-lang.org/

---

Specify the result of snapshot depth exhaustion.

spec/concurrency.md §4.4 requires the snapshot walk to stop at a depth bound and treats handle offsets outside the payload span as aborts, but it does not define whether hitting the depth bound aborts and retries, fails the snapshot entirely, or returns a partial value. Add that observable behavior to the canonical concurrency rule so this story is not ambiguous about an unsafe or incomplete snapshot.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@stories/memory.md` at line 225, Update the canonical snapshot rule in
concurrency.md §4.4 to explicitly define the observable result when the
per-attempt depth bound is reached: abort the attempt, roll back its
allocations, and retry rather than returning an incomplete snapshot. Align the
wording in the memory story’s snapshot description with that rule.

[TheLazyCat00]

26f2fd3 — one taken as a real bug, one narrowed, one already pending your decision.

Taken: boxing must read owning edges only. This was a genuine self-contradiction, not a wording preference. The predicate said a member must be boxed when its declared type "can lead back to the enclosing type", over "a cycle in the containment graph" — and an &Node member's declared type does lead back, so read literally the rule required boxing a guest. Three lines below, the same section says a cycle of guests is a legal graph and exactly what & exists for. The two could not both hold.

The graph is now stated as one of owning edges — members that store an instance of their type, inline or boxed. A guest is fixed-size storage whatever it points at, so a cycle closed through & never triggers the rule. Stated once in adt.md §4, matched in glossary.md §3.39, and memory.md §3.3 now defers to §4 for the predicate rather than restating it — which also keeps it consistent with the de-duplication pass.

Narrowed: guests from a boxed variant payload. The finding is right that the contract is undefined, but the fix is not mine to invent. memory.md §3.3 claimed a reference-typed boxed payload "may be guested from the enclosing instance's field access under §2.8" — that asserts more than §2.8 settles for a #variant case, whose read is partial and abortable. I've narrowed it to say such a payload may be guested wherever §2.8 admits the access that reaches it, and that boxing neither grants nor withholds that, which is true and claims nothing extra.

The underlying question stands and predates this PR: is an abortable #variant case read a guest source at all? expr.op is not obviously "a field access whose base is a place" in §2.8's sense, because it may not fire. Boxing did not create that gap — a non-boxed #variant case payload raises it identically. I'd rather settle it in its own change against §2.8 and adt.md §3 than bolt an answer onto this one; say the word if you want it filed.

Already yours: depth exhaustion. This is the same issue I raised two comments up, now arriving from the story side. CodeRabbit proposes abort-rollback-retry, which is what §4.4 already implies — and that is precisely the livelock: a legal value deeper than the bound fails every attempt, so retrying never converges. Still the three-way choice I laid out (terminal failure and an abortable snap; a bound published with the version that a legal structure cannot exceed; or a language depth cap), and I still lean toward the second. Not re-deciding it here.

Guards clean at 26f2fd3; story append-only additions-only on both files.

---

Generated by Claude Code

[TheLazyCat00]

both stories currently jump right into "the decision that x is..." and "heres an example:". i think they should have a better introduction or say why they are there in the first place

[TheLazyCat00]

Taken, in c1fe9f0. The story guide already asks for exactly what you're describing and I hadn't done it — §3 says a chapter opens on "the situation that forced a choice — the cause", and §3.5 that the opening sentence should carry the reader across the seam from the chapter before. All four new chapters opened on the conclusion or straight into code instead.

Each now leads with the pressure:

• "The bindings that existed only to be pointed at" — the sum mould had been settled for a long while before anyone tried to build a tree out of one, and that is when it broke. Every rule involved had been agreed separately and looked reasonable alone; together they made the most ordinary thing a variant is for unwritable without inventing storage that models nothing.
• "The sum that could not contain itself" — boxing settled layout, but left one restriction standing on one side of the # axis. It looked as settled as the rest, until review asked why and the answer did not survive being said out loud.
• "The region takes the boxes" — a decision taken in one document arrives in another as a bill. Recursion became hosting on the ADT side and left this document holding the part nobody had costed; the opening now names what the chapter must settle — an address, a size, and the invariant it disturbs on the way.
• "What a copy is for" — a rule can look finished and still be resting on nothing, and the way you find out is that somebody asks why. This one was resting on two mistakes of mine. It also now links back to the chapter it follows, which it should have from the start.

Worth noting the first of those had already been reordered once, after your earlier "start with what the issue was" comment. That fix moved the code to the front of the problem rather than the solution — but it still opened on an example, so it did not actually answer what you were asking. This one does.

Prose only; no rule changed. Story append-only check against origin/main is additions-only on both files, and the new inter-chapter anchor resolves.

---

Generated by Claude Code

[TheLazyCat00]

stories are ok, i dont really care about the spec although i looked at it a bit. the most common way to find contradiction is when working with the spec, reviewing wont do much anyway and isnt worth the time, this is a fast moving spec

[TheLazyCat00]

Understood — and on that basis I've closed the last open question myself rather than leaving it parked for a review round that isn't going to happen. a8de602.

The depth bound is now derived, so exhaustion stays retryable. Both options I put to you were worse than they needed to be: terminal failure gives snap an error path §4.4 promises it never has, and publishing a writer-maintained depth costs bookkeeping on every mutation. Neither is necessary, because a bound already exists that no correct walk can reach — a legal walk descends through a distinct live block at every step, so the scope's live block count at the start of the attempt bounds any real structure's depth. Fix it there and exceeding it always means recycled bytes, never an honest value that is merely deep, so discarding and retrying converges. The runtime already knows that number, and no observable behaviour of snap changes.

The livelock the finding pointed at was real — an arbitrary bound does fail a legal deep value forever. A derived one cannot, which is why this resolves it without inventing a failure mode.

That leaves nothing blocked on you. For the record, the two items I'm not doing unless you say otherwise:

• The variant-case guest-source gap — whether an abortable #variant case read is a guest source under §2.8. Genuinely underspecified, but it predates this PR and an unboxed case payload raises it identically, so it belongs in its own change rather than widening this one.
• Splitting d06d2e0 — the CLAUDE.md guard commit CodeRabbit keeps flagging as out of scope. It's a one-line validation guard that predates this work; I'll leave it unless you want the history clean.

On your broader point: I think you're right that reviewing prose is a poor contradiction detector, and this PR is evidence for it — the contradictions that mattered surfaced from working the rules against each other, not from reading. The &-edge boxing bug, the memory.md §3.2 ordering, the two passages #158 left stale — each turned up by checking one rule against another file, not by proofreading. Worth knowing that's the technique that pays, since the greps in CLAUDE.md only catch retired forms, never a rule that quietly disagrees with another.

Guards clean at a8de602; story append-only additions-only on both files.

---

Generated by Claude Code