Repository navigation
gunbc test: witness claims as targets (exact, :all, /...) - #13556
Conversation
Model: gunbc.target_invocation admit_test_operand gains a claim_universe parameter and a TestOperandClaimRoute arm (native universe asked first); ClaimRouteVerdict + claim_route_termination fold the member verdicts. gunbc.discovery_census claim_route_universe = //test/claim/..., the subtree site_label maps test.claim.* into. Set-form refusal now names both routes; its retirement trigger is satisfied for the claim population. Host: target_invocation_host routes claim-universe operands to run_claim_route -> cli_run::run_claim_route, which narrows the subject to the modules the pattern reaches, folds the floor's per-file discovery authority (floor_discovery_rows_over_sources, extracted from the required floor so both call one fold), and evaluates with run_claim_measured. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 160ef84fcb
ℹ️ 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".
| module_selected: &dyn Fn(&str) -> bool, | ||
| claim_selected: &dyn Fn(&str, &str) -> bool, | ||
| ) -> Result<Vec<ClaimRouteMember>, String> { | ||
| let index = process_shared_index(source_roots); |
There was a problem hiding this comment.
When the workspace index cannot be built—for example because a .dag file is unreadable or two files declare the same module—process_shared_index unwraps the fallible index builder and panics. Consequently, a claim-route invocation terminates as a Rust crash instead of reaching this function's Err path and producing the promised status-2 no-observation result; use try_process_shared_index and propagate its error.
Useful? React with 👍 / 👎.
| let (outcome, receipt) = run_claim_measured(&ctx, &closure_subject, &function); | ||
| v1_interpreter::eval_call_memo_frame_exit(&ctx); |
There was a problem hiding this comment.
For a :all or subtree selection, if one claim returns ClaimOutcome::Panicked, this loop continues evaluating subsequent functions in the same process and may publish their results as trustworthy. The evaluator's unwind boundary explicitly treats a panic as an unknown invariant violation, and the required-floor runner stops at that outcome; this route should likewise stop and mark the remaining selected claims unobserved/not attempted rather than emitting post-panic verdicts.
Useful? React with 👍 / 👎.
1 participant
What
gunbc test <label>now runs witness claims (test fn ... -> Boolintest.claim.*modules), labelled by the existing canonical claim labelgunbc.discovery_censussite_label(//test/claim/<module>:<fn>). Exact label,:all/:*, and/...subtrees under//test/claimare admitted. The exit contract is unchanged: 0 every selected claim held, 1 at least one did not hold, 2 no observation (unknown label, empty selection, refusal, or a non-verdict outcome).Model (
.dagfirst)gunbc.target_invocationadmit_test_operandnow takes aclaim_universeparameter and has aTestOperandClaimRoutearm. The native universe is checked first, then the claim universe, then the existing exact/set-form split.gunbc.discovery_censusclaim_route_universe=//test/claim/.... It is defined as the subtree thatsite_labelmapstest.claim.*modules into (a label-space fact, not a copy of the discovery roots).ClaimRouteVerdict+claim_route_termination: a definite failure dominates, and an unobserved member or an empty selection gives SubjectUnreached (2).//dag/test/claim/...) still refuse with 2.Host mirror
target_invocation_host::run_claim_route→cli_run::run_claim_route:floor_discovery_rows_over_sources. That function is extracted from the required floor, so both callers use one fold;run_claim_measured, the evaluation shared withclaim_batch. There is one context per entry module.//:requiredaggregate's question, and this verb reports what a named claim observed. eval_steps is reported on every line.Witnesses
test.claim.target_invocation_witness:an_exact_claim_label_admits_to_the_claim_routeclaim_set_forms_admit_to_the_claim_routeoperands_outside_the_claim_universe_do_not_admit_to_itthe_production_claim_universe_is_the_site_label_subtreethe_claim_route_termination_maps_to_the_three_exit_statusesa_set_form_refusal_names_both_routes_and_refuses_wideningEvery existing admission match has the new arm. Host unit tests
claim_route_termination_matches_the_modelandclaim_universe_containment_matches_the_modelpin the mirror.Executed evidence (fresh
target/release/gunbc)gunbc test //test/claim/target_invocation_witness:claim_set_forms_admit_to_the_claim_route→HELD eval_steps=1818, exit 0gunbc test //test/claim/discovery_census_witness:all→ 25 lines,25 held, 0 did not hold, exit 0gunbc test //test/claim/target_invocation_witness:all→ 56 claims,54 held, 2 did not hold, exit 1. All 8 new claims HELD. The 2 reds are pre-existing on main and come from stale literals in authorities this PR does not touch:the_instrument_target_and_its_binding_are_the_same_identityassertsinstrument_targets() |> count == 8while the registry now has 31, andthe_instrument_label_is_absent_from_the_derived_required_aggregatealso fails. The module is outside the required gate, so the floor never ran them. Left as found; this needs a separate fix.claim_set_forms_admit_to_the_claim_route→DID-NOT-HOLD ... outcome=Fail, exit 1. The change was then reverted.gunbc test //nope:x→no such target, exit 2.//test/claim/target_invocation_witness:no_such_claim→the pattern selected no discovered claim, exit 2.//dag/test/claim/...→ set-form refusal naming both routes, exit 2.cargo clippy --all-targets -- -D warningsclean;cargo fmt --all --checkclean;cargo test --release -p v1-compiler --lib native_route_termination_tests5/5.No generated artifacts or DESIGN projections are affected: no projected authority or CLI surface row changed.
🤖 Generated with Claude Code