Repository navigation
Unblock orphaned gunbc#10600 (branch session/warm-ant-80-provenance): floor FloorDiscoveryRefused on a test-marked decl in dag/test/manual/emission_provenance_specimen_red.dag, plus stage0-mirrors lib.rs drift, plus three symbol citations - #10819
Closed
gunbai-bot[bot] wants to merge 88 commits into
Closed
gunbai-bot[bot] wants to merge 88 commits into
gunbai-bot[bot] wants to merge 88 commits into
Conversation
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md a_live_authority_name_carries_a_superseded_claim Ledger-Repair-Judged: docs/design-rung-drops.md
Initial six model controls passed in remote invocation cd04ed16-ffb1-475d-a852-a4e4117e813d. Expanded coverage controls are running; later transaction/address type additions are not yet validated. Production capture, serialization and fixture-deletion execution remain unwired.
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md a_live_authority_name_carries_a_superseded_claim Ledger-Repair-Judged: docs/design-rung-drops.md
…ive helper The DAG compiler reports 'no field decl_name on type Empty' when using map(origin => origin.decl_name) on a FreeMonoid<DeclarationRef> bound from a match-arm destructure. Work around by using explicit type-annotated recursive helper functions that match Empty/Cons directly rather than relying on the higher-order map method. Add imports for FreeMonoid, Cons, Empty (from std.algebra), DeclarationRef (from std.decl_ref), and String (from std.types).
Names both specimens: - gunbc#10600: observed |> map(origin => origin.decl_name) on FreeMonoid<DeclarationRef> from match-arm destructure, element type arrives as Empty - gunbc#10625: rows |> any(row => row.label) on FreeMonoid<ApplicationRow> from match-arm destructure, same mechanism Files the row in dag/gunbc/recurring_failure_mode/match_bound_element_type_mask.dag and registers it in the roster.
…h recursive helper" This reverts commit c41ba93.
Specimen: gunbc#10600's emission_provenance_test compares observed origin identities by joining decl_name fields into a string and comparing to a literal, rather than asserting each field (module_path, decl_name, field) individually. Also correct match_bound_element_type_mask row with precise locations and remove 'fixed' claim for unmerged #10625.
…onsumer gap §4b(3) stale bound: updated v1_claim_scoped_witness_batch_deleted_note in ci_layer_roots.dag from 'five entries' to 'nine (ten after #10600)', reflecting the actual population under src/v1/tests/claim. §6 consumer gap: added note to emission_provenance_extent_test.dag naming the missing consumer capability (emitter path constructing EmissionContribution from real output text) as deferred to the emitter lane.
Resolve roster.dag conflict: keep all 162 main rows + 2 new rows (match_bound_element_type_mask, string_comparison_type_identity) appended last. The PR's original deletions of 4 roster rows are restored by taking main's version.
…r lambdas The floor refused emission_module_loss_is_separate_from_declaration_loss for the same match-bound field access that match_bound_element_type_mask files. Bind rows at function scope and walk Cons instead of parking or deleting the claim. Co-authored-by: Cursor <cursoragent@cursor.com>
std.emission_provenance landed with no producer: git grep EmissionContribution
over dag and src returned only the type's own module and hand-built fixtures.
This is the named later change DESIGN.md section 3c admits that deferral for.
The site is v2.compiler.emit_module, not src/v1/05_emit_rust.dag. The required
floor resolves modules from --source-root dag and --source-root src/v2 only, so
a floor-required control over the v1 emitter is unreachable by construction --
evidence that executes on no required lane. emit_module is the reachable real
emitter path and it already has production consumers (emit_family under
src/v2/test/claim/execution/native_selected_witness_bundle_production.dag).
emit_module_text and emit_family_text are now DERIVED from the contribution
tree via emission_contribution_source rather than concatenating strings beside
it, so the bytes and their provenance have one authority (section 3) and this
is a real production consumer rather than a second test-only reader. All three
arms are constructed by the emitter, none a stand-in:
EmissionAuthoredFragment the separator, whose bytes are the literal
declared at emit_module_decl_separator
EmissionSourceComposition the module fold, plus one per declaration
EmissionUnobservedFragment v2.compiler.emit returns Medium<String>: the fold
observes the bytes but emit reports no
contribution structure for them, so those origins
genuinely are not observed at this seam
The unobserved arm records missing ORIGINS, never a missing emission -- a
rejected declaration still refuses, so this is not a section 5 absorbing
fallback. Its next-rung trigger is v2.compiler.emit itself returning an
EmissionContribution; when that lands the arm flips to Authored/Composition and
the arm census becomes the regression control rather than retiring (4b(4)).
The instrument for the emission change is
v2.test.emit.emit_module_contribution: it rebuilds the prior repeated-append
concatenation directly over emit() inside the control and asserts byte equality
against the production path over 0, 1, 2 and 3 declarations, with a separator
placement specimen proving that equality can go red.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018KYhBKKpP3tA1UWT7U23da
The .dag parser refused a data value that began on the line after its =, which cascaded into every following annotation reading as subjectless and refused the whole floor with ChangedWitnessObservationFailed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018KYhBKKpP3tA1UWT7U23da
…ting a fact this lane removed review 62147, both findings. emit_family_contribution was a hand-copy of the module fold differing only in how an element becomes a contribution, so that difference is now a parameter: emit_contribution_composition is the single accumulation, and a fix to the seed, the append order or the composition wrap cannot land on one and miss the other (DESIGN.md S2/S6). The stall row subject still read 'no emitter path constructs these values from real output text' and 'No production consumer constructs these values from real emitted output', which this lane falsifies. The stall itself stands -- its second leg, the specimen_red map compiling under dag/test/claim, is untouched and is now what the grounding names -- but a declared subject may not assert a fact that is no longer true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018KYhBKKpP3tA1UWT7U23da
review 62152. The trigger still named the emitter-path control as part of the capability it waits on while the subject and grounding said that leg was discharged -- a grain mismatch inside one row, and DESIGN.md S4b(3) makes the trigger the whole check. It now names only the remaining capability, the specimen_red map compiling under dag/test/claim, and records the discharged leg rather than continuing to require it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018KYhBKKpP3tA1UWT7U23da
…on left to heal
Both sides appended one row at the same list tail, in two authored
cons-chain rosters. Kept BOTH rows in each -- an append-carrier conflict
has no side to pick, and picking one deletes a subject rather than
resolving a disagreement.
guarantee_stall eval_steps_outside_the_reading_coproduct_stall (main)
+ emission_provenance_missing_consumer (ours)
recurring_failure_mode capability_arrives_outside_the_converged_path (main)
+ match_bound_element_type_mask (ours)
Verified by identity join against BOTH parents, not by count: rows lost
from main = 0, rows lost from ours = 0 (53+54 -> 55, 168+168 -> 169).
docs/design-failure-modes.md is a generated projection and refused with
GeneratedArtifactConcurrentDivergence. Took the base side verbatim per
the path's declared repair route and did NOT stage the worktree bytes,
which were the ours side. Not regenerated locally: heal derives it from
the merged authorities and the generated-artifact gate must then agree
on that exact head.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V
Executing the control refused at resolve: the n<=0 branch returned Empty while the other branches returned list literals, which the resolver reads as Coproduct(FreeMonoid) vs Container(List, InferredTree). Same for the empty golden, which is a String rather than a monoid unit here. Found by running the witness, which is the point: this is exactly the class a typecheck-and-grep pass reports as finished. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018KYhBKKpP3tA1UWT7U23da
…unb-ai/gunbc into session/vivid-ferret-845-emission-contribution
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md match_bound_element_type_mask Ledger-Repair-Judged: docs/design-rung-drops.md
…gger Keep the capability sentence; name the landing change beside it via climbs_when_awaiting so the frontier has an owner without putting a node URI in the capability field. Co-authored-by: Cursor <cursoragent@cursor.com>
Keep ferret's stall subject: the emitter path now constructs all three arms. Drop climbs_when_awaiting for adhoc-29d4969b-2f7 — that landing is this merge. Co-authored-by: Cursor <cursoragent@cursor.com>
The unmarked fn is discovery-visible without being an enrolled claim; TestMarkedDecl is the refusal a test marker would hit. The recursive builder fold is what emit_module_contribution consumes; the generic EmissionAppendOperation fold remains unbuilt language capability, not a stand-in we shipped. Co-authored-by: Cursor <cursoragent@cursor.com>
…tall The shipped fold remains terminal for emit_module_contribution. The unbuilt contract climbs when append on Coproduct(FreeMonoid) is well-typed, sufficient for the operation-only fold to typecheck and execute — not when a PR merges or the builder fold stays green. Co-authored-by: Cursor <cursoragent@cursor.com>
…ration stall" This reverts commit 6d97048.
The previous generic-operations wording was capability-grained but interpretive. This trigger names a condition a reader can check, retired by that capability and observed execution, not by a PR merge or the shipped builder fold staying green. Co-authored-by: Cursor <cursoragent@cursor.com>
…pairs The Coproduct(FreeMonoid) refusal at c86bba3 was match_bound_element_type_mask (Cons walk at function scope), not append; monomorphic apply helpers instantiate R at the public boundary. Ported onto the three-arm EmissionContribution type. Co-authored-by: Cursor <cursoragent@cursor.com>
…eturn The trigger named a language capability that is not the blocker. The residual that still stalls is emit returning Medium<String> rather than EmissionContribution. Co-authored-by: Cursor <cursoragent@cursor.com>
The single helper refuses: join sees Primitive()/Primitive(R) and the empty list is not a collection. compose<R> still applies through unresolved R; the three monomorphic helpers stay until that public-site gap climbs. Co-authored-by: Cursor <cursoragent@cursor.com>
At 04ebf8e the census was the one specimen that went red: TypeError: fold_list expects a list, got Null emission_contribution_fold's algebra is now fn(EmissionContribution) -> EmissionAppendOperation<R> and supplies no materialized children, so the old two-argument read lambda received nothing to fold. The other four specimens stayed green, which is the useful half of the signal: byte identity, separator placement, read materialization and origin location all survive the fold port unchanged. The census now increments through composed append operations, with one monomorphic emc_apply_count giving the boundary call a declared type -- the same shape std.emission_provenance uses for its own boundaries. Verified at 04ebf8e: green, and still discriminating -- deleting the authored separator fragment from emit_module_decl_contribution takes it red. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018KYhBKKpP3tA1UWT7U23da
The specimen_red trigger must not retire resolution/correspondence types that still have only fixture readers. Own row; existing emission_provenance_test claims do not fire it. Co-authored-by: Cursor <cursoragent@cursor.com>
emission_members_by_address and EmissionModuleAddressAmbiguous have no reader outside the defining module, not even a test. State that in the subject rather than leaving it to grep. Co-authored-by: Cursor <cursoragent@cursor.com>
Keep both roster tails. Generated docs/design-failure-modes.md is the merge-base projection; heal derives the merged authorities. Co-authored-by: Cursor <cursoragent@cursor.com>
The merge left the base projection so heal could derive it. The ledger now includes match_bound_element_type_mask and restores the two main rows the base file had dropped. Co-authored-by: Cursor <cursoragent@cursor.com>
emit_module consumes the contribution fold. Resolution/correspondence types had only same-diff fixtures; a stall does not admit that debt. Co-authored-by: Cursor <cursoragent@cursor.com>
Identity join: 172 rows here, 171 on main, comm -23 empty, only match_bound_element_type_mask added. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
|
Closing: this is the dashboard auto-open on Leaving it open was not neutral. It had a live CI run ( Nothing here needs re-review, and flipping it ready would have re-reviewed already-landed work. No follow-up is being invented on this vehicle; the auto-title wording is leftover stall text, not new implementation. — sent from bright-ram-778 |
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
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.
Auto-opened by session-dashboard for session
zesty-swift-227.Pushing to
session/warm-ant-80-provenanceadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan