Repository navigation
Guarantee lane: open-candidate honesty, anchored baseline, FrontierAccepted, closure door, v2 split (post-merge verdict) - #7500
Merged
Merged
Conversation
The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rections adopted, receipts verified
Adopted (all verified on main this pass):
- Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not
statically propagated: v2.std.refinement exists, NonEmptyList fixture +
green cardinality_fold_propagation_test exist, and
refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the
carrier proves nothing). New Sec 4b: the operator independently
re-directed this exact guarantee on 2026-07-04
(interface-summary-declared-use-arity.md Sec 3.1, "hard error in the
language") — the intent is not lost; the lattice design pass (FLAG E)
never started.
- Failure history rewritten (Sec 2): the exemption dates to 2026-06-08
(a13fb57), pre-bankruptcy; correctness-dimensions.md marked type
safety "Yes (blocking)" while return position was unchecked — so the
ledger overstated, then the auditable contract was deleted. The
pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a
deliberate total semantics, not a priced-out wall.
- Status vocabulary widened to the review's 11-state lattice; v2 terminal
calibrated (validate_then_compile door + loop-bound wall are real;
InferredTree is still not a proof boundary); application-arity row added
(formal-driven walk, positional fallback for misspelled labels,
ArityMismatch is constructor-arity); PatternLookupBlocked's silent []
arm confirmed (PatternDynamic does diagnose — review corrected there).
- Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5
behaviors" is stale against v2.std.node's six (Match) — the guarantee
authority lands as .dag rows, never hand-edited prose.
- Sequencing reconciled to 7 stages: claims authority + expecting-red
probe corpus together; zero-resolution method wall now, ambiguity wall
census-first; cardinality vertical slice third.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…el (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…guarantee-ladder roadmap section
Corrections, each verified against main before adoption:
1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record
specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque
... every proof-carrier is presently forgeable") was false as stated;
corrected to an audited-status claim: sole_constructor is the
candidate wall, completeness for generic carriers unverified. The
earlier keyword-set inference is withdrawn in the Sec 10 ledger.
2. Subject grain: rung honesty is measured at a declared acceptance
boundary; a class's rung is the MINIMUM across in-scope paths (the
interpreter refuses the mislabeled call that order_typed_call_args
reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1
carrier gains subject_grain/acceptance_boundary/compile_mode/
realization_target/covered_population.
3. Seed rungs demoted: return/data/generic, field-through-generics,
exhaustiveness, cardinality, full ==-class, and L4 all to
UnknownUnmeasured (compile admission proven is not runtime
disposition proven); census marked specimen-denominated; unknown-
method R0 scoped to the interpretation path.
4. Dissolution on climb amended in DESIGN 4b: production handling
dissolves; the RED + positive controls REMAIN enrolled as the
evidence the higher rung stays real.
5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows +
witness-test fixture migrated); the guarantee-recovery row now
carries BOTH anchors typed, not one typed + one in prose. Carrier
note records that List admits [] — the exact cardinality gap the
ladder tracks — with the doc-graph witnesses as the interim wall.
6. cardinality_fold_propagation_test relabeled everywhere as manual
value-level specimens (length homomorphism over literals + runtime
refine_byte); "not new design" softened to the accurate scope
statement; the roadmap cardinality node re-briefed accordingly.
7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a
generic dimension mechanism; extension-vs-redesign is an open audit
question that roadmap pricing must carry.
8. Sec 1 "was not built" -> "never completed as an exhaustive
acceptance contract"; Sec 11 queue updated (correctness-dimensions
done; sole_constructor completeness audit added).
Additions (operator direction): ROADMAP gains the "Guarantee ladder —
climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes
in ticket format with dependency edges (probe corpus gates the four
floor walls; carrier gates cardinality slice, emitters, prevalence;
exemption removal gates on the call-shape + inhabitance walls). The
capability node is the sole_constructor completeness audit. State-vs-
work split recorded on the carrier: rung STATE lives in the Stage-1
claims carrier and is emitted (ladder-census-emitters node); roadmap
nodes track CLIMBS.
Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md
projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap
authority 35/35, model 9/9, focus 12/12.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…bol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ruction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…icket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ne, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
review 45545 verified and fixed: the finding was correct — the operator's spine routes all P0 obligations through the closure door and the grid marks the cardinality seam (P0.2) and ambiguity (part of resolved identity) as required-R2, so the first edge set would have let the door certify its headline over two required-open judgments. floor-method-ambiguity-wall and cardinality-vertical-slice are now prerequisites of compiler-accepted-obligation-closure, residual prevalence depends on the door alone, and the closure/residual boundaries plus doc Stage 6b record the correction. Authority 38/38, focus 12/12, page 28/28, drift 8/8, regen clean. — sent from cool-badger-514 |
…gunbc into session/cool-badger-514
Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
review 45558 verified and fixed at ec15d71: sec 7b's behavior-count passage was still present-tense ("the live authority's count is wrong") after this PR corrected the authority — exactly the stale-claim shape the PR closes elsewhere. The passage now records the drift as found-and-corrected (2026-07-31), keeps the specimen's evidentiary value in past tense (the decidability denominator drifted silently in prose for an unknown period — the argument for modeling the guarantee where a lens can read it), and leaves the Match-promotion adjudication question explicitly with the sec 11 queue. The one remaining '5 behaviors' string in the doc is the quoted historical wording inside that past-tense record. — sent from cool-badger-514 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Executes all six items of the operator's post-merge verdict on #7489, each verified against live state before adoption (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash-merge;
v2.std.node.Behaviorconfirmed six-membered).Disclosure: changes the design and roadmap authorities
gunbc.design_document(→ DESIGN.md) andgunbc.roadmap_authority+gunbc.roadmap_identity(→ ROADMAP.md), regenerated viamain_wet, never hand-edited.The six items
main's disposition (compile-time method existence unenforced outside existing paths) separately from the open candidate's evidence (narrow R2 for established receiver surfaces + a typedMethodExistenceUndecidedfrontier). Recorded in the §10 ledger as rung inflation via open-PR state, my transcription error.guarantee-baseline-prevalencecarriesanchor_commit 6c6e2dcb8587d73350ac252f5b07a6b50d684485— content-addressed and reproducible after in-flight branches merge, so walls sequence after the baseline node without racing a live tree.FrontierAccepted(P0): the disposition's fifth state — typed, located, counted, but the phase result is stillAccepted(not R1, not silent below-floor). Added to the carrier ticket, §12 Stage 1b (with both live specimens), and the DESIGN §4b tail.floor-parse-formation-wall(separator silence + the if-block misparse, closing the claim-without-track gap),floor-record-construction-wall(the record-completeness class the inhabitance wall doesn't own), andcompiler-accepted-obligation-closure(the P0.0 terminal: acceptance refuses when a Required path is Unmeasured/BelowFloor/FrontierAccepted/consumer-less).v2-phase-carrierssplit into five staged nodes — self-grounding frontier (← open v2 no longer treats source identity as semantic grounding (P0: protect the replacement compiler) #7485) → Translate refusal → inferred-tree completeness → per-kind derivation coverage → target realization gate (also ← identity join) — with its identity as the registry's first tombstone (superseded_bythe frontier node, landed in the same change per the tombstone law). The method ← join edge is deleted per the verdict's sequencing nuance: zero-resolution decides absence over the union of current admissible sources; the join gates only the >1 wall and realization completeness. Residual prevalence reroutes through the closure door.6 connectives + 6 behaviorswith the members named — the denominator the decidability argument divides by now matchesv2.std.node.Behavior.ladder-census-emitters.Verified by execution
authority 38/38 · identity 9/9 (first tombstone passes the deliberately count-free tombstone claims) · focus 12/12 · model 9/9 · page 28/28 (all 23 ladder briefs within the 100-word law) · spawner 16/16 · drift 8/8 · doc-graph 11/11 · ROADMAP.md + DESIGN.md regenerated via
main_wet.🤖 Generated with Claude Code