Skip to content

Population: inhabitance claim over the real row + declared runtime task - #13672

Closed
gunbai-bot[bot] wants to merge 2 commits into
integration/v1-closeoutfrom
work/population-inhabitance
Closed

gunbai-bot[bot] wants to merge 2 commits into
integration/v1-closeoutfrom
work/population-inhabitance

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Follow-up to #13664 (folded at 7fe66fb before this landed).

  • Adds the one inhabitance claim the supplied-value controls owe (DESIGN §3, the pairing obligation), and it can go red today: the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route runs the real route — emitted_subject_build_rows through emitted_subject_build_label_text must derive exactly the two labels the disjointness control supplies (the two compiler products of the 2026-10-09 ruling), and each must refuse as a population member through the real native_member_is_a_subject_row. Deleting the label fold, changing the subject roster, or breaking the predicate reds it. The same predicates also run over the real native_population_green_set; that row is [] until the first native adjudication (the plan's declared trigger), so those conjuncts are the real path's last execution for the row and carry no weight yet, and the annotation says so. (The first cut of this claim ran only over the empty row and could not fail; review 78409 caught it and it is gone.)
  • Declares the runtime task in the plan's Decisions: typed refusal reasons for the population predicates, trigger = first non-empty green set.
  • The roadmap row native-obligation-population (gunbc.roadmap.roadmap_authority) names the new claim in its execution contract.

Receipts (srv1, seed built from #13597's head, systemd-run --user --scope -p MemoryMax=30G -p MemorySwapMax=0, claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/native/native_obligation_population_witness_test.dag --functions <the four>):

  • at 589ceab: PASS ×4, exit 0.
  • mutation control (the first supplied label misspelled in the claim): FAIL the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route, exit 1.

Base is integration/v1-closeout, not main: native_obligation_population.dag exists on neither main nor can a main-based PR carry it until #13641 merges. Draft until then; retarget to main and mark ready after. Not a fold candidate (operator: no further folds beyond the corrected heads).

🤖 Generated with Claude Code

…asons runtime task declared

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review October 10, 2026 05:02
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Oct 10, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-10-10T05:04:13.425232Z 37ac5d3 Draft marked ready
ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@gunbai-bot
gunbai-bot Bot marked this pull request as draft October 10, 2026 05:09
…rive the supplied labels and each refuses as a member (review 78409)

Review 78409 found that the_real_population_row_passes_the_eligibility_and_disjointness_folds_the_real_route could never fail: both conjuncts ran over native_population_green_set, which is [] until the first native adjudication, so the claim was green for any predicate and any subject roster -- a decoration under DESIGN section 4b, and the roadmap row that enrolled it as evidence was rung inflation.

The claim is replaced by the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route. It runs the real route the supplied-value control pairs with: emitted_subject_build_rows, through emitted_subject_build_label_text, must derive exactly the two labels the disjointness control supplies (the two compiler products, operator ruling 2026-10-09), and each must refuse as a population member through the real native_member_is_a_subject_row. Deleting the label fold, changing the subject roster, or breaking the predicate reds it. The two conjuncts over the real green set stay as the real path's last execution for that row and are named as weightless until the first member lands, which is the plan's declared trigger.

The roadmap row's execution contract names the new function. list_length is imported by name rather than resolved by global uniqueness.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Oct 10, 2026

Copy link
Copy Markdown
Contributor Author

Review 78409 (claude, REQUEST_CHANGES on 37ac5d3) is right: the_real_population_row_passes_the_eligibility_and_disjointness_folds_the_real_route ran both conjuncts over native_population_green_set, which is [] until the first native adjudication, so it was green for any predicate and any subject roster, and the roadmap row enrolled a decoration as evidence (DESIGN §4b: ask whether the check's RED is authorable before writing the check).

Fixed at 589ceab by making the real-route claim discriminate today rather than deferring it:

  • the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route runs the real route the supplied-value control pairs with: emitted_subject_build_rows, through emitted_subject_build_label_text, must derive exactly the two labels the disjointness control supplies (//gunbc/instruments:self-host, //gunbc/instruments:v2-native-cli, the two compiler products of the 2026-10-09 ruling), and each must refuse as a population member through the real native_member_is_a_subject_row. Deleting the label fold, changing the subject roster, or breaking the predicate reds it. The two conjuncts over the real green set remain as the real path's last execution for that row and are named in the annotation as weightless until the first member lands (the plan's declared trigger).
  • The roadmap row's execution contract (gunbc.roadmap.roadmap_authority, node native-obligation-population) names the new function; the old name is gone from the tree.
  • list_length is imported by name.

Receipts (srv1, claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/native/native_obligation_population_witness_test.dag --functions <the four> with a seed built from #13597's head, under systemd-run --user --scope -p MemoryMax=30G -p MemorySwapMax=0):

  • the four claims: PASS a_host_judged_member_is_ineligible, PASS the_population_is_disjoint_from_the_emitted_subject_rows, PASS the_denominator_is_the_derived_universe_not_the_green_set, PASS the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route; claim_batch exit 0 at head 589ceab
  • mutation control, the first supplied label misspelled in the claim (self-hosted): FAIL the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route; claim_batch exit 1 — the claim goes red when the real route and the supplied value disagree, which is the discrimination the previous version lacked.

The PR stays a draft against integration/v1-closeout and is retargeted to main after #13641 lands, as its body says; it is not a fold candidate.

— sent from smart-gull-336

@gunbai-bot gunbai-bot Bot mentioned this pull request Oct 10, 2026
@gunbai-bot

gunbai-bot Bot commented Oct 10, 2026

Copy link
Copy Markdown
Contributor Author

Closing without landing, branch kept. This PR extends the native-obligation population plan that #13664 introduced (gunbc.plans.native_obligation_population and its witness). The operator's review 5477471759 on #13641 rules that #13664 is closed without folding ("preserve its branch for archaeology"; the closeout does not carry a parallel roadmap backlog), and the closeout composition reverted that fold at b5bd6a5, which is why this branch no longer merges: its base content is gone. The discriminating inhabitance claim here (589ceab, 4/4 with a mutation control) and the typed-refusal-reasons runtime task are preserved on work/population-inhabitance next to #13664's content at 7fe66fb; if the operator later decides the population programme lands on main, both reopen together on a main base.

— sent from smart-gull-336

@gunbai-bot gunbai-bot Bot closed this Oct 10, 2026
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.

0 participants