Foundation Closure B1b: the services' coupled seat, the empty relation, and the derived watch set by heyoub · Pull Request #10 · freebatteryfactory/ThreadPak

heyoub · 2026-08-13T17:29:32Z

Foundation Closure B1b — services-crate type residue. Three ruled repairs against macros/macroc/, one commit each, branched from origin/main (f1f1f08).

Lead with what is not closed

Repair 3 departs from the docket, deliberately. The docket asked that pattern, instance, guard_name, scope_type and owner_facts stop leaving a cached plan stale. They are still unwatched. Watching them needs a roster seat each, and the trigger roster's cardinality is the declared invalidation magnitude — InvalidationLimit = 9, documented as "the trigger roster's own cardinality, since one trigger per kind is all that can be watched". Minting a kind per anchor is the mirroring roster the ruling forbids and pushes the set past its own bound; the alternative is one generic dependency-key seat plus a wider magnitude, which adds an identity vocabulary to the plane and moves a declared limit — and a limit moves only behind a realistic positive control and a first-over-limit negative one. That fork has an owner and this branch does not take it. What it does instead is make the gap counted by the compiler rather than remembered by prose.

Repair 1's exclusion is layered, not total. A private field stops every sibling module and every downstream crate (E0451); it does not stop a module declared inside the guard. No #[cfg(test)] module stands under any of the six guards, each guard file says so at its own declaration, and the reversal is owned by testpak from outside the crate.

Repair 2 is closed by a lane, not by a type. Nothing stops a later road inventing a third shape for "nothing was enumerated". What would carry it structurally is a mint whose material cannot be empty; the one seam that reaches it holds a NonEmptyBounded carry it flattens to a Vec first, and recovering that shape is a change to the diagnostics seam rather than to this mint.

The three repairs

1 — the coupled seat is named body, and the six seats go private. Six services families spelled band 00's AdmittedPrefix seat report, and spelled it pub. The rename follows the prose that was already there; the visibility was the defect — a one-field record whose one field is public is a record any holder can write, so a body one pass produced could be seated under a refusal no pass ever raised. Each home's mint moved into the type_guard.rs that is types.rs's own child and can name the seat; each home exposes one borrowed reader. The refusal/ home gained the type_guard.rs it had declared it did not need.

2 — derived_over(family, &[]) routes to the canonical empty relation. It derived a whole-body commitment over empty material and called it Complete, while nothing_enumerated() meant the same state with no identities. It routes rather than refuses, for the reason PlannedMembership::complete already records: a refusal would hand every caller a branch the one real caller cannot reach.

3 — the watch set is derived from the context. The defect was not the four triggers; it was that they were a roster written at a call site, standing beside a context declared elsewhere. Two such rosters existed and had already drifted differently. ProjectionContext::watch_set now derives the shared half by destructuring the context exhaustively, and plan_scope_guard_stamp destructures its anchors exhaustively. Two holes closed with seats the roster already declared: the target binding was never watched while TargetContractChanged sat unused, and the set is now deduplicated (an expansion-time context is decided against the same capture that caused it).

Reversals, all executed

Reversal	Evidence
Restore `pub` on a body seat	trybuild: "Expected test case to fail to compile, but it succeeded"
Delete the empty-relation routing	2 testpak lanes red; the other 7 in that file stay green
Plant a seat on `ProjectionContext`	`E0027` at `planning/anchor.rs`
Plant a seat on `ScopeGuardStampAnchors`	`E0027` at `pattern_stamp/plan.rs`
Make the target contribute no trigger	`every_context_identity_is_watched` red, alone
Remove the deduplication	2 laws red, one at a production plan site
Point the new ledger row at a missing fixture	`readme-obligations-join` FAIL, count drops 16→15

Denominators — measured on both trees

collection bodies: 27 coupled / 27 declared, unchanged (the gate reads seat types and struct visibility, not field names).
red twins (core): 15 discharged / 179 owed, unchanged.
tooling reversals: 15 → 16 discharged / 3 owed — intentional movement; the new compile-fail fixture is joined by a new obligation row, and the join is proven real.
Golden identity vectors and testpak's independent transcript lane: pass unchanged. No field name enters any encoding, and both existing plan sites produce the same watch SET as before, so no plan identity moves.

cargo xtask qualify — all 7 stages hold on a cargo clean build of the committed tree.

🤖 Generated with Claude Code

Greptile Summary

This change centralizes invalidation-watch derivation and improves target-binding coverage, but plans with multiple declared source causes watch only the first source. A later source can change without invalidating the plan that depends on it, so this should be corrected before merge.

Confidence Score: 4/5

Merge is not safe until multi-source plans invalidate when any contributing source declaration changes.

One verified correctness finding remains: the invalidation derivation omits every declared source after the first.

Files Needing Attention: macros/macroc/src/planning/anchor.rs

T-Rex Logs

What T-Rex did

T-Rex produced a finding-comment-proof for a posted P1 finding and attached four artifacts that enable review.
T-Rex produced a second finding-comment-proof for another P1 finding to document additional review work.
T-Rex executed the contract-validation tests with cargo test commands and confirmed the expected triggers and sources; both tests passed and the results supported the claimed missing trigger for a non-first declared source.

_{Ran code and verified through T-Rex}

Prompt To Fix All With AI

### Issue 1
macros/macroc/src/planning/anchor.rs:79-81
**Multi-source causes lose invalidation coverage**

`CauseAnchoring::Declarations` can contain more than one source declaration, but this branch emits `SourceDeclarationChanged` only for `declared.first()`. A plan built through `plan_scope_guard_stamp` retains all source identities while invalidating only when the first one changes; changes to later sources can leave a dependent plan appearing current. Represent every declared source in the invalidation set, or reject multi-source contexts until the invalidation contract can do so.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

_{Reviews (2): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

Greptile also left 1 inline comment on this PR.

…rite one What this does not establish: a private field excludes SIBLINGS, not descendants. `E0451` stops `establish.rs` beside the guard, every other module in the services, and every crate downstream — it does not stop a module declared INSIDE the guard, which would construct as freely as the mint does. So a `#[cfg(test)] mod` under any of these guards would reopen exactly what the guard closes, the six guard files say so at their own declarations, and the reversal that carries the claim is testpak's, from outside the crate, where the exclusion is total. Six services families spelled band 00's coupled seat `report` and spelled it `pub`. The name was accidental: every one of those six field docs already explained the seat using the word "body", the closure struct's own summary line reads "The closure refusal family body", and core spells the same seat `body` in twenty-one places. The name is now the one the prose was already using. The visibility was the defect. The coupled seat keeps a carry and its posture together; it does not, by itself, keep a body and the seam that established it together. A one-field record whose one field is public is a record any holder can write, so a body one pass produced could be seated under a refusal no pass ever raised — and the record would read exactly like one a seam returned. The six seats are private, each home's mint moved to the `type_guard.rs` that is `types.rs`'s own child and can therefore name the seat, and each home exposes one borrowed reader for the consumers that exist: the diagnostics projection, the proof surface, and testpak's own lanes. Borrowed and never owned, for the reason band 00 borrows its carry. The refusal home gains the `type_guard.rs` it previously declared it did not need. Its README said no seat was private and therefore no invariant nucleus existed; one seat is private now, so the nucleus exists, and `establish.rs` — which held nothing but the three mints — is that file under its real name. The reversal: `a-services-refusal-body-reseated-by-literal.rs` builds a real body through the public guarded road and writes it into a second refusal by literal. It refuses with `E0451`. Restoring `pub` on the seat makes trybuild report "Expected test case to fail to compile, but it succeeded", so the fixture is proving the visibility rather than sitting green beside it. Denominator: the coupling gate reads seat TYPES and struct visibility, not field names or field visibility, so it reads 27 coupled / 27 declared before and after — measured on both trees rather than argued. No canonical byte moves: no field name enters any encoding, and the identity golden vectors and testpak's independent transcript lane are untouched and pass unchanged. Deleted: `macros/macroc/src/refusal/establish.rs`; the six `pub` field declarations; the five sibling-module body mints in `establish.rs`/`prove.rs` and the five `refused` helpers that called them across a module boundary; and the three module-doc claims that the body road "lives in type_guard.rs" while it did not. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…l one Unproven by this commit: nothing here stops a LATER road from inventing a third shape for the same state. The claim is closed over the two roads that exist — the deriving one and the single-cause one — and it is closed by a lane that compares them, not by a type that would make a second shape unbuildable. What would carry it structurally is a road whose material cannot be empty, and the one seam that reaches this road holds a `NonEmptyBounded` carry it currently flattens to a `Vec` before handing over; recovering that shape is a change to the diagnostics seam rather than to this mint, and it is not made here. `RelatedSet::derived_over(family, &[])` derived a whole-body commitment over empty material and called the result `Complete`. `RelatedSet::nothing_enumerated` represents the same state — the road looked and there was nothing to enumerate — carrying no identity at all. Two distinguishable values for one state: two diagnostics that both enumerated nothing compared UNEQUAL, and a reader who learned to recognize one shape did not recognize the other. Worse at the identity level, because the derived commitment's preimage is the empty framing, which is the same 32 bytes for every empty set at that family — a name for the state rather than for the refusal. Empty material now routes to the canonical value. It routes rather than refuses, and the reason is the one `PlannedMembership::complete` already records: a refusal here would hand every caller an error branch that the one real caller cannot reach and therefore has no honest value to fill, and a caller with no honest value writes the nearest one. That is how a second representation arrives in the first place. `nothing_enumerated` is documented as what it was already ruled to be: a lawful empty relation, not a missing set, not a set that failed to build, and not a truncation that dropped everything — a truncation names a bound and a non-zero count, and this names neither because neither happened. The seat is testpak's, because this is a behavioural claim about the services and the services cannot judge it: a producer comparing its own two roads agrees for the reason it exists. Two lanes land in the independent file. The population is the DOMAIN rather than a sample — all 256 family tags are asked, so a routing that held for the tag this file happens to use and failed for another is caught here rather than by whoever met the other tag first. The reversal names the value instead of describing it: the lane's own encoder rebuilds the whole-body commitment over empty material from the published grammar, and requires that no road hands it out. Reversal activation, executed: deleting the routing turns both new lanes red — "family 0 answers empty material with a second representation" and "the derived road still carries a whole-body commitment over empty material". The other seven lanes in that file stay GREEN under the same deletion, which is the evidence that only the empty case moved: every non-empty derivation, the truncation posture, the independent re-derivation, and the crafted aliasing case are byte-identical either way. The identity golden vectors and the transcript lane are untouched and pass unchanged; the coupling denominator reads 27 coupled / 27 declared. Deleted: the second representation. No check, no assertion, and no law is added in its place — the road that produced it no longer produces it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Not closed by this commit, and it is a departure from what the docket asked for. The pattern, the instantiation, the two typed arguments and the cited owner facts are still unwatched. Watching them needs a roster seat each, and the trigger roster's cardinality IS the declared invalidation magnitude — `InvalidationLimit` is nine because "one trigger per kind is all that can be watched". Minting a kind per anchor is the mirroring roster the ruling forbids and pushes the set past its own bound; the alternative is one generic dependency-key seat plus a wider magnitude, which adds an identity vocabulary to the plane and moves a declared limit, and a limit moves only behind a realistic positive control and a first-over-limit negative one. That is a fork with an owner, and this commit does not take it. What it does instead is make the gap COUNTED rather than remembered. The defect was not the four triggers. It was that they were a roster written at a call site, standing beside a context declared elsewhere, kept in step by whoever remembered. Two such rosters existed and had already drifted differently — and neither drift was visible from either site. `ProjectionContext::watch_set` derives the shared half from the context's own seats. It destructures the context exhaustively, so the population is read off the declaration rather than listed: sources reach a cause trigger, graph a graph trigger, profile and generator their own, target the contract trigger where one is bound, and `profile_version` is bound aside with the reason — a version is not an identity and every roster seat watches one. `plan_scope_guard_stamp` destructures `ScopeGuardStampAnchors` exhaustively for the same reason, and each of its eleven bindings now says where its anchor reaches the plan: the context to the watch set, pattern and instance and the two arguments to the kind content, the three origin nodes to the trail, the stamped unit to the membership, the traced subject and the owner facts to the decision trace. Two holes closed with seats the roster already declared. The target binding was never watched, so a plan bound to a host contract carried no trigger for the contract it was bound to while `TargetContractChanged` sat unused — invisible because every context in the tree is target-free, and the old control's demo context was one of them. And the watch set is deduplicated: an expansion-time context is decided against the same capture that caused it, so its cause and graph triggers are one trigger, and the derivation home's roster skipped the graph one by hand to avoid stating a kind twice. That knowledge now lives in the derivation instead of at the call site. Reversals, all four executed. Planting a seat on `ProjectionContext` refuses at `planning/anchor.rs` with `E0027: pattern does not mention field`; planting one on `ScopeGuardStampAnchors` refuses the same way at `pattern_stamp/plan.rs` — the completeness claim is the compiler's, and the laws are positive controls beside it. Making the target contribute no trigger reddens `every_context_identity_is_watched` and nothing else. Removing the deduplication reddens `the_watch_set_never_states_one_kind_twice` AND `derive_refusal::the_one_road_closes_before_it_emits`, which is the evidence that the dedup is load-bearing at a production plan site rather than only in a control. Denominators, measured rather than argued. Both existing plan sites produce the same SET as before — the pattern-stamp law still reads four triggers, the derivation law still reads three — so no plan identity moves and no canonical byte moves. Every pre-existing test passes unchanged. The coupling gate reads 27 coupled / 27 declared. The fifth trigger only ever appears for a target-bound context, and the tree has none. Deleted: both hand-written `vec![…]` watch rosters, and the claim in `pattern_stamp/plan.rs` that the watch set "covers the SHARED CONTEXT completely" — which was false for the target binding at the moment it was written. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

coderabbitai · 2026-08-13T17:29:47Z

Warning

Review limit reached

@heyoub, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 88 minutes

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 8ba00150-b847-4c4a-81ef-02a8a2f550bc

📥 Commits

Reviewing files that changed from the base of the PR and between 04883fe and b8f42a1.

📒 Files selected for processing (36)

macros/macroc/README.md
macros/macroc/src/closure/README.md
macros/macroc/src/closure/prove.rs
macros/macroc/src/closure/type_guard.rs
macros/macroc/src/closure/types.rs
macros/macroc/src/composition/README.md
macros/macroc/src/composition/establish.rs
macros/macroc/src/composition/type_guard.rs
macros/macroc/src/composition/types.rs
macros/macroc/src/derive_refusal/diagnose.rs
macros/macroc/src/derive_refusal/plan.rs
macros/macroc/src/diagnostics/type_guard.rs
macros/macroc/src/explanation_protocol/README.md
macros/macroc/src/explanation_protocol/establish.rs
macros/macroc/src/explanation_protocol/type_guard.rs
macros/macroc/src/explanation_protocol/types.rs
macros/macroc/src/laws.rs
macros/macroc/src/pattern_stamp/plan.rs
macros/macroc/src/planning/README.md
macros/macroc/src/planning/anchor.rs
macros/macroc/src/refusal/README.md
macros/macroc/src/refusal/mod.rs
macros/macroc/src/refusal/type_guard.rs
macros/macroc/src/refusal/types.rs
macros/macroc/src/template/README.md
macros/macroc/src/template/establish.rs
macros/macroc/src/template/type_guard.rs
macros/macroc/src/template/types.rs
macros/macroc/src/trigger_view/README.md
macros/macroc/src/trigger_view/establish.rs
macros/macroc/src/trigger_view/type_guard.rs
macros/macroc/src/trigger_view/types.rs
testpak/tests/compile-fail/a-services-refusal-body-reseated-by-literal.rs
testpak/tests/compile-fail/a-services-refusal-body-reseated-by-literal.stderr
testpak/tests/failed_seat_refusals.rs
testpak/tests/related_set_identity_levels.rs

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

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

…ypes

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b8f42a1666

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-08-13T22:06:39Z

@@ -19,7 +33,7 @@ impl ProjectionPlanning {
    /// refusing never needs an error road of its own.
    pub fn established(issue: ProjectionPlanningIssue) -> Self {


Restrict refusal constructors to establishing seams

Because this constructor remains pub, any downstream crate can still mint ProjectionPlanning from an arbitrary issue; it can also reconstruct an existing body by cloning the issues exposed through body() and calling the public co_established. The new private field and compile-fail fixture therefore prevent only struct-literal syntax, not the forged or reseated refusal bodies this change claims to make unrepresentable. Make these construction roads crate-restricted and expose only constructors tied to the actual establishing operations.

AGENTS.md reference: AGENTS.md:L89-L97

Useful? React with 👍 / 👎.

greptile-apps · 2026-08-13T22:10:58Z

+        CauseAnchoring::Declarations(declared) => InvalidationTrigger::SourceDeclarationChanged {
+            watched: *declared.first(),
+        },


Multi-source causes lose invalidation coverage

CauseAnchoring::Declarations can contain more than one source declaration, but this branch emits SourceDeclarationChanged only for declared.first(). A plan built through plan_scope_guard_stamp retains all source identities while invalidating only when the first one changes; changes to later sources can leave a dependent plan appearing current. Represent every declared source in the invalidation set, or reject multi-source contexts until the invalidation contract can do so.

Artifacts

Single-source baseline test output

Executed the one-source pattern-stamp plan test and recorded that the sole carried source has a matching source-declaration trigger, establishing the baseline.

Two-source invalidation test output

Executed the two-source pattern-stamp plan test and printed two carried source identities with only the first source-declaration trigger, confirming the omission.

Exact review test source

Captured the complete Rust test source containing the review-only single-source baseline and multi-source reproduction harnesses.

Review test source excerpt

Captured the executed source excerpt showing the exact multi-source assertions and printed observed values.

_{Ran code and verified through T-Rex}

Prompt To Fix With AI

This is a comment left during a code review. Path: macros/macroc/src/planning/anchor.rs Line: 79-81 Comment: **Multi-source causes lose invalidation coverage** `CauseAnchoring::Declarations` can contain more than one source declaration, but this branch emits `SourceDeclarationChanged` only for `declared.first()`. A plan built through `plan_scope_guard_stamp` retains all source identities while invalidating only when the first one changes; changes to later sources can leave a dependent plan appearing current. Represent every declared source in the invalidation set, or reject multi-source contexts until the invalidation contract can do so. --- For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

Heyoub and others added 3 commits August 13, 2026 13:27

Merge remote-tracking branch 'origin/main' into foundation-services-t…

b8f42a1

…ypes

heyoub marked this pull request as ready for review August 13, 2026 22:03

chatgpt-codex-connector Bot reviewed Aug 13, 2026

View reviewed changes

heyoub merged commit 9cc8e90 into main Aug 13, 2026
3 checks passed

greptile-apps Bot reviewed Aug 13, 2026

View reviewed changes

heyoub mentioned this pull request Aug 14, 2026

Artifact: B4 law disposition manifest v1 — 289 laws, TrueResidue = 0 #19

Open

heyoub deleted the foundation-services-types branch August 14, 2026 17:55

Navigation Menu

Uh oh!

Foundation Closure B1b: the services' coupled seat, the empty relation, and the derived watch set - #10

Foundation Closure B1b: the services' coupled seat, the empty relation, and the derived watch set#10
heyoub merged 4 commits into
mainfrom
foundation-services-types

heyoub commented Aug 13, 2026 •

edited by greptile-apps Bot

Loading

Uh oh!

coderabbitai Bot commented Aug 13, 2026 •

edited

Loading

Review limit reached

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Aug 13, 2026

Uh oh!

Uh oh!

greptile-apps Bot Aug 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

		@@ -19,7 +33,7 @@ impl ProjectionPlanning {
		/// refusing never needs an error road of its own.
		pub fn established(issue: ProjectionPlanningIssue) -> Self {

Uh oh!

Conversation

heyoub commented Aug 13, 2026 • edited by greptile-apps Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Lead with what is not closed

The three repairs

Reversals, all executed

Denominators — measured on both trees

Greptile Summary

Confidence Score: 4/5

T-Rex Logs

Uh oh!

coderabbitai Bot commented Aug 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

greptile-apps Bot Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

heyoub commented Aug 13, 2026 •

edited by greptile-apps Bot

Loading

coderabbitai Bot commented Aug 13, 2026 •

edited

Loading