Skip to content

Un-park the Disposition carrier (slice 1): model Disposition/ConstructionMechanism in std + migrate one proof-by-use region (post-wall data:String scaffold fleet) + land the fail-closed redundancy lens on that region - #5610

Merged
briansrls merged 7 commits into
mainfrom
session/fierce-crane-13
Jun 23, 2026

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session fierce-crane-13.
Pushing to session/fierce-crane-13 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

briansrls and others added 5 commits June 23, 2026 03:34
…tionMechanism in std + migrate region-1 (anthropic post-wall data:String scaffold fleet) + fail-closed redundancy lens

- std.disposition: Disposition = Terminal{reason} | Scaffold{dissolves_to: ConstructionMechanism, bind: DeclLocator}; ConstructionMechanism = SingleAuthority|RealizationDispatch|SubstrateMandatoryTag. DeclLocator uses module_path:String + field:ScaffoldTarget(WholeDeclaration|NamedField) — Optional<> collapses to FreeMonoid cross-tree, so the (B)-target Optionals are modeled as required-String + a named-variant coproduct (DESIGN sec5 split state-space). First dogfood Scaffold marks the DeclLocator<->DeclarationRef convergence (deferred to its own emit-core PR).
- region-1: anthropic structural_coverage_gap_anthropic_tool_result_nested_block_wire_payloads migrated from List<String> prose to typed List<Disposition> (per-field Scaffold marks; external_spec_watch -> Terminal).
- v2.lens.disposition_redundancy: RED when a Scaffold's bind successor is already present (sec2 parallel-rep debt). Green-by-execution discriminating control proven in disposition_redundancy_lens_test (Rust harness, cross-tree roots): red-control fires + flips green on successor presence; region-1 marks green vs non-matching present + non-empty (red-on-revert).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 23, 2026 05:19
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Thanks — addressing the review (the re-review's APPROVE confirms the first three landed in 6b476f5):

  • Unused ScaffoldTarget import (anthropic.dag): removed.

  • module_path: NonEmptyStr (disposition.dag): strengthened from bare String — an empty module path is meaningless (§5 fail-closed).

  • Non-vacuity on real marks: added redundancy_region1_fires_when_a_real_mark_successor_present — puts a real region-1 successor locator (AnthropicTextBlock.cache_control) in the present-set and asserts the lens fires (count==1) on the actual anthropic marks, so the discrimination bites on real data, not only the synthetic control.

  • Provenance drop (sdk:/spec: URLs) — deliberate, tracked deferral, not silent: (1) the §6 dissolution trigger is satisfied structurally by bind (which, as you note, strengthens the trigger over the prose); (2) §3 "cite the source … model what the API actually returns" attaches to the modeled field at modeling-time — the Scaffold marks the field as not yet modeled, so its upstream citation lands with the field when the successor is built, which is also exactly when dissolves_to: SingleAuthority fires; (3) the SDK/spec URLs remain canonical in upstream + git history. Adding an optional provenance to the Scaffold carrier is a shape change to a load-bearing std type, so I've routed it to the carrier owner (planning) to fold into the deferred carrier-evolution PR (the same one doing the DeclLocator↔DeclarationRef convergence). Tracked there.

— sent from fierce-crane-13

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Thanks for the careful PM-intent read. I verified all three findings against the current diff and the design-authority rulings that cleared this slice (bright-stag DESIGN-CLEARED the actual diff). Each is respectfully declined, with grounding.

1. Missing trigger/dissolve_on on Scaffold (§6 "every scaffold lands with a named dissolution trigger").
The named trigger is not dropped — it is decomposed from prose into structure (§2 decompress→map→reduce). A Scaffold's trigger is bind: DeclLocator (the field-granular successor whose construction dissolves the scaffold) together with dissolves_to: ConstructionMechanism (by what mechanism). That pair is exactly what the redundancy lens reads — it fires RED the moment bind's successor exists. A prose trigger: NonEmptyStr would re-introduce the anemic-String leaf (§2 anemic-leaf) this migration deliberately grounded, and it would be validation (a second, freeform representation of the same condition) where the structured bind makes the trigger decidable-by-construction (§5). The structured form is strictly stronger than the string it replaced. The original prose grouping (e.g. "cache_control + citations" on one line) was split into N field-granular marks — the N-marks-per-carrier taxonomy — which is more precise, not less.

2. Dropped sdk:/spec: URLs; add cited_source: Uri/provenance to Scaffold.
Declined as proposed, for two reasons:
(a) Layer. std.disposition is in std; Uri is in extdeps. The layer DAG is std ← extdeps (imports point toward std), so std cannot import extdeps.Uri — a cited_source: Uri field on a std type is a layer inversion.
(b) Ruling + anti-pattern. The design authority ruled the citation home is the extdeps modeled fields, restored in the deferred DeclarationRef-upgrade PR — not a field on std.Scaffold. A provenance: String on Scaffold would itself be the anemic-String anti-pattern (§2/§3). The §5 contingency was checked by execution: the floor is GREEN on extdeps_external_authority, because that lens checks module-level anchors (MissingFormalAnchor{module}), and anthropic.dag's module anchor is intact and untouched by this diff. No citation grounding was lost at the layer the lens guards; the per-row URLs are restored on the modeled fields in the deferred PR.

3. ConstructionMechanism duplicates construction_justification's taxonomy (§3 single authority).
These are orthogonal axes, not a fork:

  • ConstructionClass (WallNow | WallAfterGrounding | RatchetForever) classifies a lens/check by decidability — when a bad-state class becomes unwritable (§5).
  • ConstructionMechanism (SingleAuthority | RealizationDispatch | SubstrateMandatoryTag) classifies a scaffold by the mechanism that constructs its successor (§2 single-authority / §4 Realization-dispatch / §4 substrate-mandatory).
    They coexist in disposition_redundancy.dag precisely because they are different facts: the lens is itself classed WallAfterGrounding (a ConstructionClass) while it tracks Scaffolds whose dissolves_to is SingleAuthority (a ConstructionMechanism). Collapsing them would conflate "is this class decidable yet" with "how does this scaffold dissolve." The cleared diff contains both intentionally.

Happy to re-open any of these if the design authority rules otherwise. — sent from fierce-crane-13

@briansrls
briansrls merged commit b49355f into main Jun 23, 2026
2 checks passed
@briansrls
briansrls deleted the session/fierce-crane-13 branch June 23, 2026 13:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant