split(#4502 PR-2): ONT-10 rest — everything in #4502 outside the contracts layer (stacked on #4587) - #4588
Open
noahgift wants to merge 217 commits into
Open
split(#4502 PR-2): ONT-10 rest — everything in #4502 outside the contracts layer (stacked on #4587)#4588noahgift wants to merge 217 commits into
noahgift wants to merge 217 commits into
Conversation
…200 EV-7a, PMAT-4347, GH-4122 EV-5a Takes the aprender-contracts / -cli / -staging trees and the additive aprender-common cli_roles module from #4502's r7 A head 0be7c00, plus the cooperative-matrix delete (#4347) and the PVL ci/explicit-test-commands.d rows. Workspace versions stay at main's. Generated files are excluded (discharge-summary.json, Lean Axioms pin); 98 regenerates them as the single writer. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…key) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ire); generated ontology files stay main's Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Everything in #4502's diff that PR-1 does not carry. PR-1 ∪ PR-2 = #4502, less the generated files 98 regenerates as the single writer: census.json, contracts.nt, shapes.ttl, ontology.ofn, tbox-report.json, discharge-summary.json, Lean Axioms.lean, and the README contract counts (kept at main's 1837). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…m from the delete pass) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…_prefill_whole_again, identical prompt 3x, reused 0, no restore Quorum at 0be7c00 (gemini): the PMAT-4445 AC names this test and 3 turns; the head had it as forget_prefix_drops_the_checkpoint_so_a_repeat_prefills_whole with 2. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ames #4502 renamed ten shipped [[bin]]s to aprender-* but the ledger kept the old names, so check_binary_debt.sh read each rename as one NEW plus one STALE (10+10, #4502 defects row 4). Re-key the bin field only; class, target and the legacy_names counters are unchanged (a rename is not a merge/delete decision, and counters move only through the ratchet). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 50ab758)
… row 5, clippy -D warnings) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit afb58c0)
bashrs SEC001 flagged `eval "$*"` in the self-test's row() (#4502 defects row 10). row() now runs "$@" directly; the four mutations that need a redirect or two steps become named functions. All 15 rows keep their wanted rc and needle, so each RED row still proves its mutation bit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 8a003ed)
…w files — m52 refused 458 and 481 apr-format-golden-fixtures 458 -> 459 and aprender-facade-e2e 481 -> 483, both free ordinals, so the ont8-evidence-gate (458) and pvl-comparator (481) fragments #4502 added keep their slots and pvl-comparator still runs before pvl-challenge (482). Command content unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 1630322)
… builds --locked) L0 exception: fixes running job --locked (run 36388075483, mac-check job 108817628569). The build.rs env_key build-dep lines added provable-contracts edges without re-resolving the lock; cargo check --locked failed on the stale lock at b4ebf93. Edges only, no new packages. Receipt: intel cargo check --workspace --all-targets --locked rc=0, 0 errors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… — elan 4 refuses to reinstall Row 13, run 36353187094 x86-main: step 1 failed in 0.1s with "error: 'leanprover/lean4:v4.29.0-rc4' is already installed". No judged file was missing. elan >= 4 (4.2.0 on the fleet) exits 1 on `toolchain install` of an installed toolchain, so the step passes once per host and fails every run after that. Install only when the toolchain is missing from `elan toolchain list` (first column, so a "(default)" suffix still matches), and decide that inside the same flock, so two jobs cannot both see it missing and race. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit de92271)
…(tree-reader drift)
workspace-test-shard step 7 (check_tree_reader_tests) failed in run 36388847584:
PR-1 adds aprender-contracts{,-cli} test targets without their registry rows.
Moves #4502's 12 contracts-cli .cmd wiring files into PR-1 instead of parking
11 targets in the unwired baseline (baseline unchanged), carries fb's m52
ordinal renames (457->459 golden-fixtures, 480->483 facade-e2e) that the moved
457/480 files need, and regenerates scripts/tree_reader_tests.txt.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Agent: aprender-88
…-debt re-key) Local run of the wired contracts-cli targets on PR-1 failed (ont4b_shapes_gate, shapes_vacuity, ont_entity_properties, ...: 'entity.type has no Σ entity_type_target_class mapping'): PR-1 carried #4502's contracts code but not its tests/fixtures/ont updates (164 files). Moves them in. Row 4: cherry-picked 50ab758 (contracts/binary-debt-v1.yaml re-key). (cherry picked from commit 50ab758) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: aprender-88
roadmap aggregate, pv census, pv extract (contracts.nt + shapes.ttl) and the README CONTRACT_COUNT blocks, regenerated with the pv built from this tree; fixed points asserted: make roadmap-aggregate-check, pv extract --check, readme_sync.sh --check. Agent: aprender-88
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: aprender-88 # Conflicts: # README.md
… file (ENOTDIR) — chmod 0o555 does not stop root, CI runs as root Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: aprender-01 (cherry picked from commit 3e65448) Agent: aprender-88
… gate runs (#4502 row 2) lint_passes_on_real_contracts requires the refinement gate to RUN whenever CI is set; the gate compares HEAD with merge-base(HEAD, origin/main), else the origin/main tip. The workspace-test-shard section clones at depth 1 and only the tier step's pull_request arm fetched a main, so workflow_dispatch / merge_group / push shards had no base and shard 3 panicked "the refinement gate declined" (run 36384418038). Per the operator ruling (2026-09-28 09:41): pin the EVENT's base commit -- pull_request.base.sha, merge_group.base_sha, push's `before` -- as refs/remotes/origin/main; the origin/main tip only for workflow_dispatch. A missing or zero base fails the step with ::error (no silent skip). Placed after the tier step, whose pull_request arm would otherwise overwrite origin/main with main's tip. ci.yml is unchanged: it has no generator; fat_driver reads ci/sections.yml at run time. Agent: aprender-41 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit cd587d6a5b317467b4eac3b5c10b65ecf2656f8a) Agent: aprender-88
…ontracts tests read shard 1 of run 36391942814 failed ont2c_tracked_ofn_and_report_are_fresh: contracts/ontology.ofn and tbox-report.json are required-tracked writer outputs of contracts/ontology.yaml. PR-1's ontology.yaml is byte-identical to #4502 integ (f7858ca), so integ's outputs are the fresh ones; taken with the PVL discharge summary + Lean axioms the discharge-check target reads. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Agent: aprender-88
…e ordinals 761/762 (#4502 row 3) Shard1 step 13 REFUSEd two ordinals that each named two fragments: 458 (apr-format-golden-fixtures + contracts-cli ont8_evidence_gate) and 481 (facade-e2e + contracts-cli pvl_comparator). A shared ordinal leaves the run order ambiguous. The two contracts-cli fragments move to 761 and 762. Both commands are byte-identical; nothing else names these files. check_explicit_test_commands.sh --check: base origin/fb/4502-a-diag rc=1 (2 REFUSE), this commit rc=0 (101 fragments, no shared ordinal). Refs #4502 Agent: aprender-cb Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 59d6911a04a30b5f609fb67c11ca1aba32ad4381) Agent: aprender-88
…he lock
Diag run 36384418038 (x86-main): "P1 band-lock: the lock was still held
after release". flock(1) hands its lock fd to the holder bash, and the
holder's `sleep` inherits it. On TERM the holder killed the sleep and
exited without waiting for it. gpu_band_release waits only for the queue
process, so under load a sleep that was still dying kept the lock held
after release returned.
- gpu_band_lock.sh: the TERM trap now waits for the sleep. The sleep
starts before the ready file is written, so a TERM (sent only after
ready) always finds $s set.
- check_release_host_receipts.sh: P1 uses a sleep that takes 0.3 s to
die on TERM, like a loaded runner, so the row fails every time on the
old lib instead of only when the scheduler is unlucky.
Evidence: repro loop with the slow sleep, 10/10 held on the old lib and
0/10 with the fix (plain sleep: 0/5). Full self-test: rc=1 on the old
lib ("FAIL P1 band-lock: the lock was still held after release"); rc=0
with the fix (94 rows and mutants, band-lock-any-class killed).
Agent: aprender-6b
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
(cherry picked from commit 7a8b939)
Agent: aprender-88
…usal-ok fixture follows the contract - pv_surface_gate: #4502 carries VS-COUNT-001 (#2648) in validator.rs with no row in the decision table, so every_rule_in_the_validator_source_appears_in_the_table failed. Add a Case: one obligation, stated total 2, Error. - ont_refusal_receipt: #4502 changed contracts/refusal-receipt-v1.yaml but not its byte-for-byte copy in tests/fixtures/ont/refusal-ok; copy it. Agent: aprender-fb Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 036beee) Agent: aprender-88
…ce is not vacuous; shapes_n 66; all 8 refusal fixtures - extract:binary (ONT-4g) refused every [workspace] root whose snapshot is absent, even one whose manifests declare zero bin targets. The ont fixtures (code-bound, ...) are such roots, so PV-ONT-012 turned the shapes gate red there (ont4b2_code_lean_w3c 343). Refuse only when the census names targets; new unit test for the 0-bin root, the 3-target absent-snapshot test stays red. - ont4b_shapes_gate (338): the later ONT-10 slices added nine binary shapes; name them, 57 -> 66 (measured by `pv extract contracts --check` at 036beee). - ont_refusal_receipt (430): the other seven refusal-* fixtures carry the contract too; copy it to all. Agent: aprender-fb Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 23122d3) Agent: aprender-88
…! names it, and it does not parse Carried from #4431 (42f84fb, GH-4197). #4502 had the deletion, but PR-2 (the #4502 split) did not, so the file was left without a carrier. It is the one file under crates/ that fails kani_assume's fail-closed token count (unbalanced } at :35). Agent: aprender-59 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 353e1d64e84f7872b14c5a67078d18dec062b785) Agent: aprender-88
… surface ledger surface_audit.csv carried every contracts-pv row twice (identical, all columns), a merge artifact: 943 rows / 894 keys. The duplicates double-counted low_and_uncovered (242 vs the comparand's floor 204, G2.3), tripped the T2 pairing lines and the m10 baseline re-derivation. One copy of each kept: dogfood_baseline.py --check PASSED, check_dogfood_coverage.sh green. Refs #4502 Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
noahgift
disabled auto-merge
October 1, 2026 08:34
…nd that the mutants rules are off on purpose until #4648 Quorum lane finding (q-4587c, sonnet): the comment named ci/mutants-debt.tsv and scripts/check_mutants_debt_ratchet.sh as the blocking rule, but on a branch without #4647 neither exists. Same block text in #4647/#4587/#4588 so the three still merge without conflict. No check changed. Pmat-Ticket: PMAT-4646 Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…nd that the mutants rules are off on purpose until #4648 Quorum lane finding (q-4587c, sonnet): the comment named ci/mutants-debt.tsv and scripts/check_mutants_debt_ratchet.sh as the blocking rule, but on a branch without #4647 neither exists. Same block text in #4647/#4587/#4588 so the three still merge without conflict. No check changed. Pmat-Ticket: PMAT-4646 Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
noahgift
added a commit
that referenced
this pull request
Oct 1, 2026
…nd that the mutants rules are off on purpose until #4648 Quorum lane finding (q-4587c, sonnet): the comment named ci/mutants-debt.tsv and scripts/check_mutants_debt_ratchet.sh as the blocking rule, but on a branch without #4647 neither exists. Same block text in #4647/#4587/#4588 so the three still merge without conflict. No check changed. Pmat-Ticket: PMAT-4646 Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sonnet seat (agent:claude-sonnet-5-5/pr-4588-review), base 00052c0, no blocking findings (1 warning: base.ref interpolated in ci.yml, pre-existing trust boundary; notes: pre-push fail-open on rc 2, sampled review of a 1950-file diff). Pmat-Ticket: PMAT-4502 Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sonnet seat (agent:claude-sonnet-5-5/pr-4587-review), base 00052c0. Verdict DEGRADED (782-file diff sampled), 0 errors. The mutants rules being unreachable is the operator's C188(a) ratchet order; restore is #4648. Pmat-Ticket: PMAT-4502 Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
Author
|
quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false) {
"ticket": "PMAT-4502,PMAT-3715,PMAT-4431,PMAT-4073,PMAT-3712,PMAT-4445,PMAT-4083,PMAT-4189",
"head": "db80afca024f5abafe4e547e693d7faf1d54b330",
"width": 3,
"executor": "agy",
"agreed": false,
"auto_merge": {
"checked": true,
"was_armed": false,
"disarmed": false,
"note": "auto-merge not armed"
},
"lanes": [
{
"lane": 1,
"verdict": "PASS",
"findings": 0
},
{
"lane": 2,
"verdict": "FAIL",
"findings": 1
},
{
"lane": 3,
"verdict": "PASS",
"findings": 0
}
]
} |
Contributor
Author
|
quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false) {
"ticket": "PMAT-4502,PMAT-3715,PMAT-4431,PMAT-4073,PMAT-3712,PMAT-4445,PMAT-4083,PMAT-4189",
"head": "db80afca024f5abafe4e547e693d7faf1d54b330",
"width": 3,
"executor": "agy",
"agreed": false,
"auto_merge": {
"checked": true,
"was_armed": false,
"disarmed": false,
"note": "auto-merge not armed"
},
"lanes": [
{
"lane": 1,
"verdict": "PASS",
"findings": 1
},
{
"lane": 2,
"verdict": "PASS",
"findings": 1
},
{
"lane": 3,
"verdict": "FAIL",
"findings": 1
}
]
} |
Contributor
Author
|
quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false) {
"ticket": "PMAT-4502,PMAT-3715,PMAT-4431,PMAT-4073,PMAT-3712,PMAT-4445,PMAT-4083,PMAT-4189",
"head": "db80afca024f5abafe4e547e693d7faf1d54b330",
"width": 3,
"executor": "agy",
"agreed": false,
"auto_merge": {
"checked": true,
"was_armed": false,
"disarmed": false,
"note": "auto-merge not armed"
},
"lanes": [
{
"lane": 1,
"verdict": "PASS",
"findings": 1
},
{
"lane": 2,
"verdict": "PASS",
"findings": 4
},
{
"lane": 3,
"verdict": "FAIL",
"findings": 2
}
]
} |
… reviewed in #4647); PMAT-4445 title states the fix The quorum on this PR read the ci.yml mutants-debt ratchet block as an unauthorized gate change: no ticket in --ticket named it. It is the block #4647 adds and q-4647g agreed 3/3; operator rulings C188(a) and C192(1) put it in scope here. The PMAT-4502 entry now says so. PMAT-4445 title described the bug, and a review lane read it as a requirement twice (q-4588f/g). It now states the fix the diff makes. Local commit per C192(1); pushed once, with the merge of main, after #4647 merges. Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…lone crate; claimed kernel with 0 focus nodes fails Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… 8 scalars expand to banned Result::unwrap Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
noahgift
added a commit
that referenced
this pull request
Oct 1, 2026
…ops.rs The F2 union of #4588 x #4620 lost the closing brace of the #[cfg(test)] thread_local! block (98 { vs 97 }); cargo fmt --check rc 1 -> 0. Every PR head is fmt-clean; this defect exists only in the rehearsal (C205(2)). Agent: aprender-ca Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…s, K11 shapes.rs, K12 challenge.rs (cursor-free rewrites), K13 proof_status, K14 lint/extract K10/K11/K12 measured 14/14, 27/27, 50/50 caught; K13/K14 mutation runs were cut by the lambda reboot (NOT_MEASURED). Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…r that hunk only; A' mutants-table-scope kept Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…write failure Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…kills) Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> # Conflicts: # crates/aprender-contracts/src/lint/refines_gate_tests.rs # crates/aprender-contracts/src/lint/shapes_gate.rs
…ue (c213 m44: no evidence/ receipt exists for it) Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…c213 m27) Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sonnet seat (agent:claude-sonnet-5-5/pr-4587-review), base 430be65. Verdict DEGRADED: delta-only sample (32fc88e..HEAD) of a 784-file diff; duplication/agy/mutation not run on this head (not_measured). ci.yml merge hunk: comment-only, mutants-table-scope intact, no gate weakened. diff_patch_id c0ed4ceedd. Unsigned: the key is a CI secret. Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…derived; regenerated by pv census on intel) Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e regenerated census Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…0 uncited ratio reworded (c213 ADD) bashrs SEC010 flagged the two selftest mkdir -p "$d/..." lines (265/269); the subdir is now made by mk's optional 2nd arg. selftest 30/30, check_bashrs_gate 0. gpu_profile.rs:522 carried an uncited 27-34x ratio and seconds with no evidence/ receipt; reworded to point at #4590. check_perf_claims_cite_receipts 0. Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…po_graph_is_fresh) Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Reviewer agent:claude-sonnet-5-5/pr-4588-review; verdict DEGRADED (sampled delta); diff_patch_id 4eb8d194f48bb285b252161dc2765f6ea7e5893f; unsigned (B1, key is a CI secret). Pmat-Ticket: PMAT-4502 Agent: aprender-07 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
noahgift
enabled auto-merge
October 1, 2026 21:20
This branch has not been deployed
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.
Split PR-2 of 2 of #4502 (operator plan: the split is a MOVE of #4502). Stacked on #4587 (base
split/pvl-rows-0.70). Once #4587 merges, this PR retargets to main.What: the full #4502 r7 A
0be7c00372tree minus PR-1, plus fb's integ fixes (rows 4, 7, 10, 13; row 8 superseded by PR-1's full regen) and the #4445 AC test (forget_prefix_makes_the_same_prompt_prefill_whole_again, 3 turns).Coverage: fb's union check PASS, PR-1 e13e9eb ∪ PR-2 = #4502 with 0 missing and 0 extra (handoff 4502-union-receipt-postcut).
Generated files: taken from PR-1's
batch_fold.sh --regen(censusn_files1889; README CONTRACT_COUNT 1889,check_readme_claims.shrc0).ontology.ofn,tbox-report.json,discharge-summary.jsonandAxioms.leanare not included (98 is the single writer).Pre-push receipts: intel at 78bd48d:
cargo fmt --all --checkrc0,cargo check --workspace --all-targets --lockedrc0. 66's guard-tree on intel: 59 PASS, and all 6 merge-ref guards rc0.Once #4587 and this PR merge, #4502 closes with links.
🤖 Generated with Claude Code