Conversation
…ape allowlist, label ratchet (PVL-001 EV-6a) #4139, stacked on EV-5a (#4122). - A token-level Lean scan: comments (nested) and string/char literals are blanked first. It finds `sorry admit axiom native_decide implemented_by extern unsafe partial` in ProvableContracts/** and the root. Measured on the tree: exactly the spec's 7 `axiom` decls, nothing else. - escape-allowlist.yaml `{file, decl, kind, reason, ticket, confirmed_by}`: - unlisted escapes, entries without reason/ticket, and STALE entries are RED; - `confirmed_by: pending` is PENDING, RED only under --strict. The 7 axioms are DRAFTED from their own doc comments as pending. Two of them (NF4 nf4_lut_monotone/bounded) carry a false "Status: proved" comment; their reasons say so. - Roots, per the cop's ruling on #4139: - an exact-name `lean_theorem:` (`ProvableContracts.<...>.<decl>`) that names no theorem is MISSING-ROOT, rc 1; - an unresolved LABEL is held by a non-increasing ratchet (unresolved-label-baseline.txt, 1128 lines seeded): a new one fails BY NAME; one that now resolves fails until `--update-baseline` removes it, and that flag never adds a line. - Axioms.lean (generated; `gen-axioms --check` is its freshness gate): a `run_cmd` SUBSET pin over `Lean.collectAxioms` for each of the 164 bound theorems in the root's import cone. The pinned set is formalization.yaml status.axioms (default propext, Classical.choice, Quot.sound) plus the allowlisted axioms. Capstones get an exact `#guard_msgs in #print axioms`. 85 bound theorems sit in orphan modules (ORPHANED-ROOT): `lake env lean` cannot see a module `lake build` never built, and EV-5c drains them. FOUND: cooperative-matrix-gemm-v1's f16_error_bound cited ProvableContracts.CooperativeMatrix.f16_accumulation_error_bound as its lean_theorem. It is an AXIOM ("Status: axiom ... not proved in Lean4"), so this was a false L4 claim. The reference is withdrawn to a `none -- ...` note; `pv extract contracts --check` is unchanged (rc 0). Measured on lambda, pinned toolchain, built tree: - `pv discharge check <lean> --contracts contracts` (lake elaboration included): rc 0; `ok lake env lean Axioms.lean`; 164 pinned. - `--strict`: rc 1, 7 PENDING, as the spec's accept requires. - Spec mutation `axiom pvl_mutation : False` used by alibi_slope_real_pos: the scan is RED (ESCAPE ... pvl_mutation), and the rebuilt tree's pin is RED ("AXIOMS ...alibi_slope_real_pos: [ProvableContracts.Alibi.pvl_mutation] outside the pinned set"). Restored. Tests: - lib: 16 discharge unit tests. - tests/pvl_discharge_check.rs: 13 end-to-end rows, including the spec's two mutations (a planted axiom; @[implemented_by] on a def). Refs #4139 #4083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…) -- unresolved-labels.json, never written by the gate
Built to the cop's relay of PVL-001 infra#992 (round 2):
- The set lives in `$LEAN/unresolved-labels.json` `{command, labels:
[{contract, label}]}`, and the ratchet is keyed on that SET. Only a label
NOT in it is rc 1, by name. A listed label that resolves now is reported
(`RESOLVED-LABEL (n) still listed`), not failed.
- `pv discharge check` NEVER writes the file; `--update-baseline` is gone.
`make label-ratchet` (`pv discharge label-ratchet`) is the only writer. It
rewrites the set DOWNWARD: a resolved label leaves, a new one is reported
rc 1 and left OUT, and a missing file is seeded. Seeded from the tree:
1128 labels.
- MISSING-ROOT also covers `capstones:` in formalization.yaml that name no
theorem.
- `lean_theorem: none...` stays a sentinel (references_of).
Tests:
- lib: 19 discharge unit tests.
- pvl_discharge_check.rs: 14 rows. New: check never writes the label set,
and label-ratchet only shrinks it (seed, green, resolved-is-not-red,
removal, a returning label is not re-admitted); a capstone naming no
theorem is MISSING-ROOT, and a real capstone gets its exact
`#guard_msgs` pin.
- Real tree: `pv discharge check <lean> --no-lake` -> rc 0, 7 PENDING,
UNRESOLVED-LABEL (1128) (listed 1128), 164 pinned / 85 ORPHANED-ROOT.
Refs #4139
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ls when it cannot recover its whole plan (#4108 review ph5) Gemini ph5 lane 1: (1) grep -L/-l skips an UNREADABLE file exactly like a missing one, so the universe check now requires present AND readable (row 36, chmod 000; skipped as root). Its suggested `|| exit 1` on guards="$(universe_for_subset)" was not taken: grep -L and xargs exit non-zero on correct runs. (2) --dry-run now compares to_run+skipped to the in-memory planned count before answering (row 37: the plan emptied between write and read-back -> rc 1). Case table 40/40; real dry-run and check_guards_are_wired unaffected; bashrs +1 PERF002 misfire only; check_bashrs_gate and check_shell_lint_ratchet PASS. Pmat-Ticket: PMAT-4108 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Refs #4139 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…degraded: same-family) on e6cf9f1 Docs only, no code change. docs/audits/quorum-PMAT-4076.json holds the three lanes: model measured from modelUsage, session ids, verdicts, findings, and the round history. docs/audits/impl-PMAT-4076-receipt.md is the implementation receipt: probe on the real corpus, verification table, mutants, open non-blocking notes. Pmat-Ticket: PMAT-4076 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…`worlds`; VU-INV-003's formula says something These are the two non-blocking notes from round 3 (e6cf9f1, AGREED 3/3). The cop ruled they land as their own reviewed commit, not at the fold. - contracts/ontology.yaml `readers.worlds`: `ontology/sigma.rs` → `ontology/sigma.rs, lint/valid_under_gate.rs`. All three lanes noted the new gate is the first code that INTERPRETS `worlds`, and every other Σ key names every consumer. The contract's reference line is updated to match. - contracts/ont-valid-under-v1.yaml VU-INV-003: `valid_under(c) ≠ ∅ ⇒ len(keys(..)) ≥ 1` was a tautology (lane 1). It now reads `valid_under(c) ≠ ⊥ ⇒ len(keys(valid_under(c))) ≥ 1`: a PRESENT block has at least one key. `⊥` is declared in Σ ("bottom — undefined"), so the sigma gate accepts the glyph. The rule itself was already enforced (PV-ONT-013 on `{}`). Checks: `pv validate` on the contract; `--gate sigma/relations/valid-under` Pass on the corpus; `pv extract contracts --check` 0 (graph unchanged); census unchanged; check_ont_ratchet PASS; aprender-contracts --lib 1718/0; contracts-cli ont2b_sigma_gate 8/0 and ont7_valid_under_gate 13/0. Pmat-Ticket: PMAT-4076 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…th `-- --lib`, and the integration test is not a lib test cargo-mutants runs `-- --lib`, so a mutant in commands/discharge.rs or in the contract_walk verdict mapping is killed only by a LIB test; tests/pvl_discharge_check.rs never counts. Adds 5 lib tests: - the decline/reject exit codes and words, and Display; - gen-axioms write + --check freshness + decline; - check accept/reject/pending/--strict/zero-roots decline; - label-ratchet writes; - the Lean elaboration verdict, through a fake lake (0 accepts, 1 rejects, absent declines, --no-lake skips it, and a prior failure is not cleared). `elaborate` now takes the lake path, so the tests never touch PATH. Refs #4139 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…he first (flock-guarded, always()) One #4046 shard left 64G of target on gx10: nothing deleted a run's target when its job ended. The ticket's first design, an always() rm of the job's run dir, is refused. The dir is keyed per RUN, and ci_reclaim_target_dirs.sh measured two jobs of one run on two runners of one host sharing it, with windows overlapping by 21-29 min. Deleting at one job's end could remove a live sibling's tree. Cop ruling (A): last-one-out. scripts/ci_run_target_release.sh: - register writes <dir>/.live/<token>; - release removes this job's marker and deletes the tree only when no marker remains; - all three, including the delete itself, run under one flock on <dir>.lock, a sibling on the same host-local fs. A job killed before its release keeps the tree, and the next run's start-of-job reclaim stays the backstop. Case table (--self-test), including the cop's must-RED: 8 races of two jobs finishing together, each exactly one delete. Without the flock the same table shows double deletes in 3 of 3 runs (measured). ci.yml, workspace-test-shard and guard-cargo: - register after the run dir is created (non-fatal); - release as the last step, if: always(), deleting through the build image because the tree holds root-owned files. A plain rm as the runner user gets Permission denied (measured end to end with a root-owned tree). The step logs du before/after, and a cleanup never fails the build; - the case table runs as a step beside the reclaim planner's. Today each job's dir is its own (shards keyed <PR>-s<N>, guard-cargo -guards). Last-one-out stays correct for a re-run that reuses the RUN_ID and for any future re-key that shares again. Known and kept: one 0-byte run-<id>.lock per job-run stays in the PR parent. The reclaim planner sweeps only directories, and unlinking a lock others may be waiting on would let two jobs hold "the" lock on different inodes. Size split, measured on gx10's two largest live shard dirs (16-17G each): rlib/rmeta 57-59%, test executables ~30% (92-98 of them, ~53MB each), .so 6-7%, build/ ~5%, incremental ~0. Debug info dominates both large kinds, so the lever to measure next is debug = "line-tables-only" for the test build, not strip (which touches only the 30%). NOT MEASURED here: the lever's before/after on the same shard. Pmat-Ticket: PMAT-4102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…d, so no unreachable branch remains The first gx10 mutation pass (d720624) had the lib unit tests MISS every on-disk path: Tree::load, cone, collect_lean, parse_file. Only the integration test reached them, and CI mutates with `-- --lib`. - 22 new lib tests build temp trees: nested dirs and non-.lean files, the transitive cone and the orphan, label/exact-name binding, pins vs ORPHANED-ROOT, capstones, zero-roots decline vs failure, stale/missing Axioms.lean, sidecar readers, the label-ratchet seed/shrink/never-add, private theorems. - generate() now returns {text, tree, binding, allow, form}; check() reuses them. The allowlist and formalization readers used to run twice, and check's second error branch could never fire. An unreadable escape-allowlist.yaml or formalization.yaml now declines in one place. - render_labels builds its JSON without json! (its expansion unwraps; clippy disallowed-methods). Output is byte-identical: `make label-ratchet` leaves unresolved-labels.json unchanged. discharge lib tests 41, CLI lib 5, pvl_discharge_check 14; clippy -D warnings clean. Refs #4139 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d -- no workflow edit; plus a real-tree probe row - tests/pvl_discharge_check.rs gains the_real_lean_tree_passes_the_ev_6a_probe: on the REAL lean dir, `gen-axioms --check` rc 0 and `check --no-lake` rc 0 with PENDING (7), and check leaves unresolved-labels.json byte-identical (the gate never writes it; infra#992). - ci/explicit-test-commands.d/460-aprender-contracts-cli-pvl-discharge-check.cmd, the directory the CI already runs (as 300-...-pvl-zero-contracts.cmd does), so the target is not dark. The cop suggested this route instead of a ci.yml edit. scripts/tree_reader_tests.txt re-derived by `check_tree_reader_tests.sh --update` (143 wired, unwired ledger unchanged at 39); check_tree_reader_tests.sh and check_explicit_test_commands.sh (+ self-test 72 rows) PASS. pvl_discharge_check: 15 rows pass. Refs #4139 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ways() release deletes on failure (REVERT ME) Pmat-Ticket: PMAT-4102
…comparison mutants gx10 mutation pass (820e852): `<`->`<=` and `>`->`>=` in owner() SURVIVED. They are equivalent: an escape token is never at the same index as a declaration keyword. owner() now splits once at `d.at <= i`. An `axiom` token IS its declaration's keyword (at == i), so moving that boundary changes the answer, and escape_owner_rules sees it. Behaviour unchanged: 41 discharge lib tests pass. Refs #4139 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…them (#4112) Batching folds each author branch into a release/** branch by a direct PUSH, and no PR is opened. ci.yml fired only for main/master, so guard-tree and guard-cargo first ran on the release->main integration PR: drift reached 0.69.1 and was caught at release time, not at the fold that caused it. Operator-approved option B (2026-09-24, relayed verbatim by the cop aprender-cf: "1. recommended approved"): - on.push.branches gains 'release/**'. - Every job except guard-tree and guard-cargo carries `if: !(push && startsWith(ref, 'refs/heads/release/'))`: ci, workspace-test-shard, mac-check, vendored-schemas, determinism, determinism-compare. workspace-test and gate keep `always()`, ANDed with it. The rest were already pull_request-only. A fold never pays for workspace-test, and the run's conclusion is red iff a guard job is red (gate is skipped there, since it would read the skipped jobs as failures). - Both guard jobs' comparand step unshallows on a release push. A depth-1 checkout cannot name merge-base(origin/main, HEAD), and scripts/lib/resolve_base.sh refuses a single-parent fold outright without it. Measured: ~11 s, 159 MB for the full history, after which the merge-base resolves. A push runs the ci.yml of the pushed tree, so this covers release branches cut from main after it lands. Guard: scripts/check_ci_release_fold_scope.sh evaluates every job's `if:` for pull_request, push->main and push->release, and refuses any expression shape it cannot evaluate. - R1: release/** is in the push trigger. - R2: exactly the two guard jobs run on a release push, and neither needs a skipped job. - R3: both guard jobs unshallow. - Self-test: 8/8, including 6 planted mutants, each RED for its own reason. - Must-RED: main's ci.yml fails it with 11 violations. - actionlint: the same 2 pre-existing findings as main, none new. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… the aggregate Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…job (gx10-pool2, run 35963100366) The planted step failed (exit 1), and the release step ran anyway, printing 'released: deleted /mnt/nvme-raid0/targets/aprender-ci/4150/run-35963100366-guards'. The dir is gone on gx10, checked from the host. Pmat-Ticket: PMAT-4102
… sibling's release The round-1 delegate raised this; no lane did. register was non-fatal (`|| echo ::warning::`), and its comment said a missing marker "can only make the tree deletable sooner". Sooner is the defect: if this job's register failed while a sibling shared the dir, the sibling's release would see no marker for it and delete this job's LIVE tree. That is the one thing the design promises never to do. Latent today (each job's dir is its own), and real on any shared key. Now a failing register fails the step (GitHub's default `bash -e`; no `set +e` precedes it in either job). A job that cannot register must not build on a shared tree. release stays non-fatal: a cleanup never fails the build. Pmat-Ticket: PMAT-4102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… waiter never locks a stale file Round 2 (lane gemini-3.1-pro, measured): one 0-byte run-<id>.lock per job-run leaked. The reclaim planner sweeps only directories, and I had kept the file deliberately, because unlinking a flock file lets a waiter lock the OLD inode while a newcomer locks the NEW one. The standard lock-file-with-unlink protocol fixes both: after every acquire, locked() checks that the fd's inode is still the path's, and re-opens and re-locks if not. The last release, still holding the lock, unlinks it. New cases: - the last release leaves no lock file. RED if the unlink is dropped; - must-RED: A holds the old inode, W waits on it, A unlinks while a newcomer N takes the fresh file, A releases. W must register only after N releases. Without the inode re-check, W registers while N holds the lock, which is two holders (3 of 3 runs, measured). My first draft of that case was VACUOUS: N was forked inside A's subshell and inherited A's fd 8, so the old lock stayed held until N exited and W waited either way. N now closes fd 8 first. The dropped-flock mutant still gives double deletes. Pmat-Ticket: PMAT-4102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
e6cf9f1 (A) and c9314e0 (B) Docs only, no code change. This follows the operator rule of 2026-09-24: every quorum is 2 agy non-Claude lanes + 1 Claude Code lane on claude-haiku-4-5 (the cop overrides receipt-lint on the haiku seat). There is one receipt per round per head, not composed: - A: e6cf9f1 vs 49fe19c, the whole ONT-7 change. gemini-3.1-pro-high PASS, gemini-3.8-flash-high PASS, claude-haiku-4-5 PASS. - B: c9314e0 vs 3913e2f, the follow-up (Σ readers.worlds, VU-INV-003). The same three PASS. The implementation receipt is updated to match: the two follow-up notes are marked done under receipt B, and the stated-schema note is kept. Pmat-Ticket: PMAT-4076 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… created Round 3 passed 3/3 (2 agy gemini + 1 haiku). The delegate then found an edge no lane had caught. locked() creates <dir>.lock to take the lock, and do_release's early "already gone" return never unlinked it. So a job whose register failed, or a re-run after a reclaim, left a 0-byte lock: the abnormal-path version of the leak round 2 found. It now unlinks, still holding the lock, and a new case covers it (RED when the unlink is removed). Pmat-Ticket: PMAT-4102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… the autopilot carries the rest before the tag (#3459) Part 2 of #3459, per the cop's ruling (the narrowing is approved on condition that nothing is silently left behind): - check_milestone_cut.sh --must-carry: RED only on an open issue labelled must-carry; every other open item is listed TO CARRY. Strict mode is unchanged, and it stays the final gate: a tagged milestone with ANY open item is RED (new self-test row S27: an unlabelled open issue left in a milestone is RED under strict). - scripts/release/carry_milestone_items.sh (new): moves every open non-must-carry item to the next release's milestone when that release's "EPIC: release train <next>" lists it, otherwise to `backlog`, each with a one-line slipped_from comment. It refuses (rc 1, writes nothing) while any must-carry issue is open. - autopilot.sh cut_tag: must-carry verdict -> carry -> strict verify (the existing call, byte-identical) -> tag. The move lives in the autopilot; the gate only verifies. - check_tag_step_gated.sh: asserts that order, that must-carry rc 1/2 and carry rc 2 never tag, and adds mutants M4 (must-carry verdict discarded) and M5 (carry call deleted); both turn it RED. Label `must-carry` created on paiml/aprender ("Blocks the release cut of its milestone (check_milestone_cut.sh)"). Refs #3459 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Pmat-Ticket: PMAT-4108 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e1e2 (tree = d1dc6c3) Pmat-Ticket: PMAT-4102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…t-release # Conflicts: # docs/roadmaps/roadmap.yaml
… shape; merge-main patch identity Pmat-Ticket: PMAT-4102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…t armable Pmat-Ticket: PMAT-4108 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…1 haiku seat gemini-3.1-pro-high PASS, gemini-3.8-flash-high PASS (both model_measured), receipt-lint ok. claude-haiku-4-5 seat PASS; its brief sha256 bb78d696…2697 equals the agy round's prompt.md (cop ruling (a), until #363). Round 1 was killed by its owner shell (rc=143, no artifact) and archived. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nk() cannot hang (#4139) gx10 cargo-mutants on 820e852 (141/270 at the time) left 8 MISSED + 5 TIMEOUT: - blank(): the index loop hung under `skip == 0`->`!=`, `i += 1`->`*=`/`-=`, `i += skip`->`*=`/`-=` -- a timeout, which scripts/mutants_diff_gate.sh (#4142) counts as a survivor. Now a `for` over enumerate() with an `until` mark: no mutation of the stepping can loop forever. - the `'` guard (prev is an ident char): row a_prime_after_an_identifier_... (`x'y'` is one name; `f 'y'` is a literal). - line comment `- i` -> `+ i`: row a_line_comment_ends_at_its_own_newline_... (comment not at offset 0, code after it). - block_comment_len `k + 1 < len` -> `<=` / `k * 1`: row an_unterminated_ block_comment_... (these index past the end on an unclosed /-). - name_lit `c == '_'`: `A._x.y'` stays bare, `x-y` is quoted. - judge_labels `resolved > 0` -> `>=`: nothing resolved, no RESOLVED line. - owner `<`/`>` were already removed by 4841bf1 (partition_point). discharge lib tests 44/0; clippy -D warnings clean. The kill of each row is proven by the full rerun on this head (gx10), not claimed here. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…pro-high + sonnet-5 + haiku-4-5, one brief) Evidence only; the judged diff is 9a6bc00. Sonnet nit 1 (--json gains mode/to_carry in strict mode; the verdict is unchanged) is recorded in the claude-lanes sidecar, per the cop. Nit 2 is filed as its own ticket. Refs #3459 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…4317) check_no_silent_truncation.sh reached B3 with the v0.69.3 merge-back (5fa13fe). lean/build.sh and check_workspace_test_waits_on_guard_tree.sh were written on B3 before it existed, so guard-tree turns red on: lean/build.sh:38,86 m.group(4)[:100] (86 is its own mutant row) lean/build.sh:41 errs[:3] check_workspace_test_waits_on_guard_tree.sh:110,112 out.strip()[:200] Each now says how much it dropped with a computed count: a clip() helper ("... and N more chars") and "... and N more error(s)" for the error list. guard_tree --no-cargo on fe0acaf: no_silent_truncation FAIL -> PASS (81 candidates, all baselined). lean build.sh --self-test green, with the our-warning-ignored mutant still killed. waits_on_guard_tree green. Remaining local FAIL: baseline_ratchets (bashrs 7.4.2 vs 7.4.1), which is local to this host and matched the pristine batch control. Refs #4317 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…han roots Merges GH-4347-dpo-on-nf4@9018366cf. Quorum on 9018366: 3/3 PASS (sonnet-5, haiku-4-5, sonnet-5 lane 3') degraded: same-family (agy lane void: LANE ISOLATION VIOLATED). roadmap.yaml regenerated by make roadmap-aggregate (PMAT-4347 fragment added). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…controls (#3142) conleche.sh exports the tree with lean4export pinned to the tree's exact toolchain and checks it with con-leche (pinned), a second kernel sharing no code with Lean's C++ kernel or pv. Every run first proves the oracle can say no: a one-file axiom module must come back RED and a trivial theorem must be accepted. build.sh runs before export, because a stale .lake exported the pre-#4347 DPO axiom (measured, con-leche declined it). Verdicts: 0 ACCEPT / 1 RED (rejection or non-standard axiom) / 2 not a verdict (unsupported feature, OOM, unpinned toolchain, control failed). Heavy steps run under agent.slice MemoryMax/CPUQuota caps. Measured on lambda at 9018366: controls ok, 402163 declarations accepted (--verified), 7:11 wall, 5.7 GB max RSS. --self-test 9/9. Advisory; nightly workflow wiring awaits cop approval. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… Lean tree (#3142) Runs crates/aprender-contracts-staging/lean/conleche.sh on the clean-room pool at ~02:23 UTC. Nothing requires the job; a red run blocks no PR or release. Exit 1 (RED: rejected declaration or escape axiom) and exit 2 (NOT A VERDICT) both turn the run red with an annotation naming which. elan is not in the pool image, so the job installs a pinned elan v4.2.4 (sha256-checked) into its own /mnt/nvme-raid0/ci-cache dir; toolchains, pins and the Mathlib cache persist there, serialized by a concurrency group. Install step exercised locally: sha OK, toolchain resolved from lean-toolchain. Guards: runner labels, env defined, path filters, no hosted runners, leanchecker scoped, actionlint -- all pass. Workflow edit approved by the cop (aprender-77) pending 3/3 quorum. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…eason; pins reset (#3142 quorum r1) Quorum round 1 findings (agy lane, void on isolation but substantive; sonnet): - The negative control passed on judge==1, which a crash (exit 1) also yields: it now requires con-leche exit 2 naming escape_ax. - con-leche exit 1 with INTERNAL PANIC is NOT A VERDICT, not RED (row 8). - pin() force-checks-out, resets --hard and cleans the reused clone (keeping lake's .lake cache), then asserts a clean status. Measured: a planted edit to ConLeche.lean and a stray Stray.lean were gone after the run, which still accepted 402163 decls (7:43, 5.8 GB). - build.sh exit 2 (declined) is named as a decline, not "stale oleans". Correction to c0ffd92's message: "path filters" and "leanchecker scoped" were guards run over the tree and passing; neither is a property of this schedule-only workflow. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…y; an uncapped run says so (#3142 quorum r2) Quorum round 2 findings (sonnet x2): - ACCEPT had no floor: "accepted 0 declarations" passed. judge takes a floor, and the tree run passes the positive control's count (the core library alone, 52954): an empty or truncated export is NOT A VERDICT. Self-test rows for 0, equal-to-floor and above-floor. - capped() fell back to uncapped silently. The cap mode is now probed once in the main flow and printed there ("capped: ..." or "UNCAPPED: ..."). Measured: a first cut printed the warning inside capped(), which every caller redirects -- it landed in build-*.log, twice (the subshell dropped the once-flag), and never in the run's output. - exit 1: 'rejected' is read before 'INTERNAL PANIC' (row 12). Measured, full run with systemd-run stubbed to fail inside a capped outer unit: controls ok (floor 52954), ACCEPT 402163, 7:04, 5.8 GB. Probe both ways + unpinned toolchain -> rc 2. --self-test 14/14. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ndently re-verified (#4071) The prior quorum was at 27315ed. 9fad260, the clippy --all-targets fix, came after it, and only moves tests (owl.rs production lines are byte-identical). Re-verified in a fresh worktree: the lib and CLI tests, the probe, make oracle-owl-check (roundtrip, kinds, ELK), and the row's mutation planted independently, which is RED in both arms. The author's session (aprender-19 [c630e1]) has ended; aprender-75 took the row at the cop's direction. Open dependency: paiml/infra#965 (the ELK pin and the JVM declaration). Pmat-Ticket: PMAT-4071 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit a7f491c)
…tribution (#4071) The round counts: one round, 3/3 gemini PASS at 9fad260. The isolation exit-3 is shown benign by measurement: every moved ref belongs to a foreign worktree, and the lane clones came back byte-identical. Pmat-Ticket: PMAT-4071 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit f5a3dfe)
Freezes spec §2–§5, the analysis code (stats.rs), the analysis plan and prompt v1 under prereg_sha ef51087dc79b… before any measurement (S-1). New crate aprender-review-experiment (publish = false); harness CLI is an example, not a [[bin]]. Planted §3 edit turns prereg-check and FALSIFY-REX-PREREG-001 RED; restore → GREEN. Receipt: docs/audits/rex-001/rex-00-receipt.md. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…(replaces eff7153 B1 reject) DEGRADED, honest: pmat consulted (cli + stdio mcp rc 0), cuda consulted (fixture-path false positive, no-authority-found), crux consulted; mutation and antigravity unreachable. Guard ACCEPTs (throwaway-key run). Left unsigned for the CI signer, which also signs 98's fe0acaf receipt. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…#4356 Phase 0: no declared label admits apr-serve review jobs on any host; cells stay NotRun{NoDeclaredExecutor} until infra#1088 lands. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
guard-cargo refused at 41488ee (run 36108193130): 456, 460 and 470 were each shared by an apr-cli/ev11 entry from main and an ONT entry from the fold — ambiguous order. Move the ONT entries to the free ordinals 457, 463 and 472; nothing references the filenames. check_explicit_test_commands now PASSes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ation check — Refs #4357 corpus_version review-corpus-v1@787d2026256cc08b. P 50 (cargo-mutants listing, markers stripped), R 50 (revert-the-fix, comment-only hunks dropped), G 50 (green, unreverted, pre-cutoff). 45 dev / 105 test; 70 test defect items. Diffs are outside git (items-v1.tar sha256 70dffe56…). Contracts review-corpus-v1 (FALSIFY-RCV-001..003) and review-corpus-contamination-v1 (FALSIFY-RCC-001..003); planted train leak RED (rc=101) -> GREEN. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…FY-RXR-001..003) — Refs #4358 Harness drives apr serve /v1/chat/completions at greedy/seed 4354/512 tokens, never truncates (context refusal -> NotRun{ContextOverflow}), seeded run order + 10% rerun. Scorer denominators are the EXPECTED item set; raw outputs are sha-checked and the verdict re-parsed. Receipts verify with minisign when --pubkey is given. Three falsifiers planted RED and restored GREEN (docs/audits/rex-001/rex-03-receipt.md). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… arms on (#3712) model_ladder_cells.judge has been NOT ARMED on every receipt because no producer emitted `cells`, and the inventory carried no context_length, thinking evidence or memory terms to derive the owed set from. - scripts/lib/model_ladder_cells_produce.py: enrich — apr inspect -> arch, context_length, thinking modes, template sha, weights/KV bytes (workspace left null: apr's own capacity arithmetic decides fit, never a guess here) measure — one row per owed (model, rung, verb, mode), the owed set from the judge's own owed_rungs(); needle at token 0, question last; run/chat/serve/code under the fleet GPU flock; apr's prompt_tokens corrects the density guess (3 tries); capacity refusals keep apr's required/available bytes. - model_ladder_cells.owed_rungs(): one generator shared by judge and producer, so they cannot disagree about what is owed. - model_ladder.sh: enrich always; measure behind --cells / MODEL_LADDER_CELLS=1 (nightly only — it is huge); gpu_mem_* on the receipt. - check_ladder_cells_producer.sh: fake apr, 8 cases through the real judge, 6 planted producer mutants each killed (115 s). Known gaps, reported not hidden: `apr code --output-format json` carries no backend so code cells cannot pass; chat/code print no prompt_tokens (rows borrow run's, labelled prompt_tokens_source); no ttft; the `declared` rung leaves no room to generate against the judge's prompt_tokens >= tok. Pmat-Ticket: PMAT-3712 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… v2b/3712-cells-producer
… v2b/3712-cells-producer
…03) — 6/6 NotRun{NoDeclaredExecutor}, S-7 — Refs #4359
Every §2.1 cell has exactly one admission row; a silent cell rejects the file, Admitted
needs a parity receipt at or above a cited threshold, and no admitted cell raises S-7
(`rex admission-check` exits 10). With infra#1088 open, all six cells are NotRun, so S-7
fires and the experiment STOPs. The §7 premise "apr parity vs llama.cpp" is false at
v0.69.3 (GPU-vs-CPU only); the oracle is an explicit field. The S-6 operator ruling is
recorded in the receipt.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… ruling 2026-09-25 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> # Conflicts: # README.md # contracts/census.json
…acts (pv-sat) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
Author
|
Folded: superseded by #4431 (B3 contracts/ONT/docs batch, re-cut onto main). Every file change in this source is present there. Closed per cop PRCAP ruling (cap 10); branch not deleted. |
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
2 participants
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.
Emergency fold B3 (contracts / ONT / docs), operator 2026-09-24: "We FIRST RIGHT NOW, emergency merge all 80 into 4 batches., the enforce 10 max rule going forward."
Folded sources (each merged
--no-ff, history kept)Closes #4191
Closes #4207
Closes #4108
Closes #4112
Closes #3177
Closes #4081
Closes #4080
Closes #4198
Closes #4071
Closes #4074
Closes #4122
Closes #4075
Refs #4102
Refs #4175
Refs #4070
Refs #4139
Refs #3997
Refs #4002
Refs #3994
Refs #4000
Refs #3999
Refs #4001
Refs #4201
Refs #4202
Parked (branch kept; re-enters via the next like-batch)
unanchored_but_bindablefrom 297 to 298. The fold was reverted out of the batch.chore/0.69.1-merge-back, which is 678 commits ahead of main (its PR chore: 0.69.1 merge-back — release/0.69.1-batch-2 + rc/0.69.1-x (X2) into main #4046 is closed). They touch CRUX files that do not exist on main (scripts/crux_vllm/*,scripts/lib/crux_cells_*, the README "Verified this release" section), so they cannot fold without the merge-back itself.Batch resolution
NAMED_GATEShas 11 entries.contract_walkexit-1 errors: ObligationsRejected + GateRejected + DischargeRejected (all three kept).workspace-test:needs: [guard-tree, workspace-test-shard](ci(workspace-test): shards wait on guard-tree, so a RED guard stops burning shard runner time (#3177) #4196) plus the release-push skip from ci.yml guards never run on PRs into release/** (or on fold pushes), so batch folds skip guard-cargo/guard-tree until the integration PR #4112.batch_fold.sh --regen), plus the pv-sat witness (make contracts) andtree_reader_tests.txt --update. There are 54 stalecli.rs:Nrows insurface_audit.csv, each re-derived from itsCommands::<Variant>.Local evidence (on this head)
make contracts: rc 0; aprender-contracts lib 1904 passed.cargo test -p aprender-contracts-cli: rc 0.cargo clippy -p aprender-contracts -p aprender-contracts-cli --all-targets -D warnings: rc 0.cargo fmt --all --check0 ·cargo deny check advisories0.Workflow change: #4150, #4163 and #4196 edit
.github/workflows/, so this batch needs a 3/3 quorum and the cop merges it.keep-open: #3994 #3997 #3999 #4000 #4001 #4002 (epics, Refs only)
ont-delta: resolves ONT-2c + ONT-4d + ONT-4e + ONT-5 land together; the PVL-001 EV-2/3/5a/6a/6c/7b/8a/10/11 gates land.
Folded: #3142 PVL-F7 advisory con-leche nightly (9ef6d39, merge of fd06d80)
.github/workflows/conleche-nightly.yml(advisory, cron + dispatch, clean-room pool, no runner-host or secret changes) +crates/aprender-contracts-staging/lean/conleche.sh.degraded: same-family(agy void twice on isolation):/mnt/nvme-raid0/tmp/pvl-a-q3142/VERDICT.md. Evidence:/mnt/nvme-raid0/tmp/pvl-a-3142/EVIDENCE.md(3 runs, 402163 decls accepted).Fixes #4199
🤖 Generated with Claude Code
Closes #4238