Harness hardening: flown-scenario capture cross-check key, fail-closed inject staging, fail-closed AllowBatchExecution parse - #1397
Open
vl3c wants to merge 6 commits into
Open
Harness hardening: flown-scenario capture cross-check key, fail-closed inject staging, fail-closed AllowBatchExecution parse#1397vl3c wants to merge 6 commits into
vl3c wants to merge 6 commits into
Conversation
… + docs) 1. Ledger capture cross-check armable on FLOWN scenarios: manifest entries may declare utWindow = [lo, hi]; unmatched_captured_awards matches a windowed entry to a captured award whose UT falls inside the inclusive bounds instead of requiring exact seq_key equality (which a flown spec can never satisfy - CL-2 measured ut 119.7/119.9/119.8 across three runs of one craft). Opt-in per entry, zero committed specs declare one, one-to-one per (entry, pool) consumption and pinned-first ordering preserved (exact-key entries additionally sort ahead of windows), M-B2 independence untouched. 2. HARNESS-INJECT-FAILS-OPEN: run.py staging now asserts the injection POSTCONDITION (non-empty Parsek/Recordings/, plus rp_b9_root.sfs for rewind-b9) and fails CLOSED as terminal INVALID(stage-inject-noop) pre-boot, non-retryable, naming the likely cause and one-line remedy. 3. HLIB-ALLOWBATCH-NONLITERAL-FAILS-OPEN: a non-literal AllowBatchExecution argument resolves fail-closed (allow_batch=false) with an <unresolved:...> marker reported by unresolved_ingame_declarations, instead of silently reading batch-allowed. Tree recount unchanged: 542 declarations, zero markers. Suites: lib 927 OK, provision 203 OK (5 skipped), missions/lib 1103 OK. No committed scenario's verdict moves: the new key is behind a knob no committed spec declares, and the staging change only reclassifies runs that previously burned a boot to fail on a misdirecting subkind.
- MINOR-1: the greedy candidate order's secondary key is now acceptance WIDTH (exact key = 0, window = hi-lo) instead of exact-vs-window, so a wide window can no longer strand a narrower window's award (probe S1); exact-before-window falls out of the same rule. - MINOR-2: the residual pinned-wide-vs-unpinned-exact greedy limit is documented in the ordering comment + arming checklist and pinned by a test (fail-closed: a false unexpected row, never a false green). - MINOR-3: documented the repMode=nominal migration caveat (ut -> utWindow forces ut=null, which moves the entry in compute_expected's accumulation order under a nonlinear rep curve) on ManifestEntry.ut_window and in the arming checklist. - MINOR-4: validate_ledger_expectations now mirrors the oracle's structural utWindow rules pre-launch, so a window typo reds as spec-invalid in seconds instead of surfacing as PARSEK-FAIL(ledger) after a full flight. - NIT-1: _manifest_entry_to_dict serializes stockReason (and the artifact round-trips through parse_manifest_entries; test added). Suites: lib 931 OK, provision 203 OK (5 skipped), missions/lib 1103 OK.
Owner
Author
Independent adversarial review recordAn independent reviewer agent (fresh context, did not write the code) reviewed this PR in a scratch clone across two rounds. Round 1 ( Verdict: no BLOCKER, no MAJOR; 4 MINOR + 6 NIT. Fixes (
Round 2 ( Final verdict: CLEAN. Follow-ups deliberately not taken here (filed in the review, all pre-existing or unreachable): extending the pre-launch mirror to malformed Generated by Claude Code |
… postcondition Two live-testable claims of PR #1397 walked against the real game. The first needed no change; the second is the documented operator action and is the ONE deliberate committed verdict change here. HARNESS-INJECT-FAILS-OPEN, live-proven closed (no code change needed). Run in a worktree where Source/Parsek.Tests had never been built - the deterministic trigger the entry identifies. S1.5-rewind-loop terminated in ONE SECOND, pre-boot (kspExit.code=null, collectLogs.ran=false, driver.steps=[]), INVALID stage-inject-noop, attempt 1 with no _a2 retry, and the error named both cause and remedy - while the injector itself still exited 0, which is exactly the fail-open being closed (run 2026-07-31_1626). Running the named remedy verbatim then staged, booted and went green on attempt 1 in 63 s (run 2026-07-31_1627). CL-2-pod-impact-ledger is now the FIRST committed spec to arm captureCrossCheck, and the only one declaring a utWindow. Walked as known-gate 3's checklist, one flight per step, all PASS attempt 1: 2026-07-31_1630 baseline, spec unchanged 3 awards UNEXPECTED (report-only), ut 12.5 / 19.1 / 119.9 2026-07-31_1638 utWindows, still report ZERO unexpected; reportOnly 3 -> 0 2026-07-31_1645 captureCrossCheck = gate PASS, hardDivergences=0 reportOnly=0 The windows are the mission's phase bounds - [0, 60] for the two ascent Progression awards, [100, 140] for the VesselLoss impact - and the three flights are their own justification: the second Progression measured 19.1 / 19.0 / 19.1 across them, so an exact-UT pin would have red the very next flight. Expected totals did not move (funds=529600.0 science=100.0 rep=-7.999829000000001, verified offline against the baseline flight's capturedRaw before spending a flight, and measured identical on both): CL-2's entries are all ut-less so _sort_key ordering is untouched, and all three rep entries are repMode="applied" so the nonlinear curve is not re-entered - the review's ordering caveat verified inert rather than assumed. The funds milestone entry stays window-free; KSP logs no funds award, so it is never capture-matched. The two whole-set guards become explicit allowlists naming CL-2 with that evidence, so a second spec arming the gate still reds until its own evidence is recorded, plus new cells pinning the phase bounds and replaying the measured award set through the real matcher (including a stray-award probe proving the gate still bites). CL-2's own cell now pins GATE as the recorded decision. Stale "declared by ZERO committed specs" claims in hlib, run.py and the docs corrected. No C# touched. Suites: lib 932, provision 203 (5 skipped), missions/lib 1105, all OK; dotnet test 19490 passed / 1 skipped / 0 failed.
…dger gate The review's in-pattern follow-up to MINOR-4. validate_ledger_expectations mirrored the oracle's utWindow rules but still passed a malformed per-entry `ut` (true / "x" / nan / inf) and an entry that is not a table at all - all six shapes measured passing ADMIT and then hard-failing as a manifest-parse-error PARSEK-FAIL(ledger) AFTER the flight, which is the same burned-flight economics utWindow and the stage-inject postcondition already closed. The gate now mirrors the oracle for the three ENTRY-SHAPE keys an author hand-writes off a capturedRaw readout - entry-is-a-table, ut, utWindow - in the SAME ORDER, so an entry carrying both a bad ut and a window blames the ut on both sides rather than the mutual exclusion. WhatThePreLaunchGateMirrorsTests sweeps the two implementations against each other over the whole malformed-shape space in BOTH directions (a run-time-only rejection costs a flight; a pre-launch-only rejection would refuse a spec the oracle accepts), pins that both sides name the same key, and asserts every committed spec still passes the widened gate. The sweep has teeth: run against the pre-fix hlib it reports 6 divergences, 0 against this one. Deliberately still run-time, recorded in that class's docstring so the boundary stays a decision rather than an oversight: kind, provenance, amountKind, the state-dependent-facet author-constant rule, the rep magnitude cap, seq, stockReason and the funds fill-from-capture ambiguity - value/semantic rules, the last of which genuinely cannot be judged before the produced log exists. Suites: lib 937, provision 203 (5 skipped), missions/lib 1105, all OK.
…ate, close the evidence gap A 4-agent clean-context review panel over the previous three commits returned 1 HIGH, 6 MEDIUM and a set of wrong numbers, several in my own reasoning. HIGH - the armed windows were bounded in the WRONG CLOCK. The cross-check matches a captured award's raw Planetarium `ut=`, which is `fixtureUT(9.06) + padDwell + T+`, but the spec's rationale reasoned about the FLIGHT. Pad dwell is wall-clock (game time runs 1:1, no warp), so the [100, 140] impact ceiling left ~20 s of headroom against `mission_runner.CONNECT_BUDGET_SECONDS = 30.0` - and `should_retry` never retries a PARSEK-FAIL, so one slow kRPC connect would have red the nightly with no absorption, looking exactly like a real ledger regression. Reproduced against the real matcher: +21 s of dwell reds a correct flight while the save diff stays green, i.e. a pure false red. Bounds corrected to [0, 100] / [100, 400] and verified to cost NO discrimination (an extra VesselLoss at ut 150 and an out-of-phase Progression both still red). The corrected spec was RE-FLOWN: `2026-07-31_1759`, PASS attempt 1, 180 s - and it earned its keep, its awards landing at ut 12.8 / 19.3 / 120.2, all three moved again with the impact above every prior run's 119.7-119.9. MEDIUM - the armed gate could not see an ABSENT capture. It reds on an award it cannot explain, so a capture yielding zero awards was unmatched-empty and GREEN - the same no-op-gate fail-open the spec says the gate exists to close. Two stock award lines are now required logContracts, making capture non-emptiness a positive grep-stable assertion. Both verified to match real archived lines before flying. MEDIUM - the pre-launch gate now DELEGATES to oracle.parse_manifest_entries rather than mirroring a chosen subset. The "shape vs value/semantic" boundary I documented did not survive review: the oracle with captured=None rejects every rule deterministically, and `seq` / `stockReason` are pure type rules hand-written on every CL-2 entry. My stated justification was also self-contradicting - it rested on the funds fill rule needing the log, while oracle.py's own comment says that path is unreachable against a real log. One carve-out remains (funds fill, which reads the captured pool, so raising it pre-launch would refuse a spec the oracle could accept). Twelve shapes now red pre-boot instead of costing a flight, and an unbounded-integer `ut` no longer raises OverflowError out of validate_spec - which has no try/except and would have aborted the WHOLE batch instead of one spec. MEDIUM - guard holes in my own tests: nothing pinned the armed entries' `stockReason` (dropping both silently widened the gate to "any +1 rep in window", demonstrated with a ContractReward probe), and the stray-award probe was degenerate (the stray was appended after the three measured awards had consumed every entry, so it was insensitive to the very bounds it claimed to test - a [0,10000] widening gave an identical result). Both fixed, plus a manifest-length pin, a connect-budget headroom assertion, and `.ut:` with the colon (`.ut` is a substring of `.utWindow`, so the ordering claim was unpinned). LOW - the armed flight left no artifact proving it was armed: `crossCheck=` was emitted only inside the per-unmatched-award loop, so `_1645`'s verifier block was byte-identical to the report-mode run before it. It is now on the unconditional ledgerOracle line, and `crossCheck=gate` is archived in the re-flight above. Numbers corrected, all verified against artifacts: the sweep finds 12 divergences against the pre-fix hlib, not 6; the impact UT is on record for SIX runs, not four; the first Progression is NOT constant (12.0 / 12.4 / 12.5 / 12.8); CL-2 is not "the only scenario measured producing reputation" (CL-1 earns the identical three awards - the real reason is that CL-1 carries no ledger block and is forbidden one); and provision reports no skips here. Stale "no committed spec declares/arms" claims corrected in hlib, run.py and both docs, including the comment that justified the acceptance-width sort key as inert - it is live now. Suites: lib 939, provision 203, missions/lib 1107, all OK; dotnet test 19490 passed / 1 skipped / 0 failed with no C# changed.
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.
One focused PR closing three fail-open/mechanism items, now with both of its live-testable claims proven against the real game, and with the ledger capture cross-check ARMED on the one scenario that can carry it.
Everything except that arming lands report-only or behind knobs no committed spec declares. The arming is the ONE deliberate committed verdict change, it is the documented operator action for known-gate 3, and it is backed by FOUR flights rather than by argument. No other verdict moved, and no C# was touched anywhere in this PR.
Live proof 1 - HARNESS-INJECT-FAILS-OPEN really does fail closed
Run in a fresh worktree where
Source/Parsek.Testshad never been built - the deterministic trigger the todo entry identifies.Parsekwas built from its own dir and the harness instance provisioned (drift=0), so the only thing missing was the test assembly.Run
2026-07-31_1626_S1.5-rewind-loop-wallSeconds=0(wall-clock 19:26:47 -> 19:26:48), and every claimed postcondition holds, proven from the result JSON rather than asserted:stage-inject-noop"verdict": "INVALID", "subkind": "stage-inject-noop"kspExit={"code": null, "killed": false},collectLogs={"path": null, "ran": false},driver.steps=[]attempt=1; zero_a2files inresults/[Error][Stage]line above, verbatimNote
exit=0on that line: the injector still reported success. That is precisely the fail-open being closed, captured live.The named remedy, run verbatim, is the whole fix.
dotnet build Source/Parsek.Tests, then re-invoke:Run
2026-07-31_1627_S1.5-rewind-loop, PASS attempt 1, 63 s. No divergence from the claim, so no driver fix was needed.Live proof 2 - the flown-scenario arming path, walked end to end
The known-gate 3 checklist run verbatim on
CL-2-pod-impact-ledger, one flight per step, so each step's claim rests on its own run:2026-07-31_1630manifest-capture stockLines=3 deduped=3 seamRejected=0; all three awards UNEXPECTED (report-only) at ut 12.5 / 19.1 / 119.9utWindows declared, stillreport2026-07-31_1638unexpected stock awardlines;ledgerOracle hardDivergences=0 reportOnly=0(wasreportOnly=3)captureCrossCheck = "gate"2026-07-31_1645hardDivergences=0 reportOnly=0, gate live2026-07-31_1759mismatches=0,crossCheck=gatearchived; awards at ut 12.8 / 19.3 / 120.2Step 1's
capturedRaw, which is what the windows were authored from:The three flights are their own argument for phase bounds over pins. The second
Progressionaward measured 19.1, then 19.0, then 19.1 across them - it moved between two runs of the same craft on the same afternoon - and the impact has measured 119.7 / 119.8 / 119.9 over six archived runs - then 120.2 on the post-review re-flight, a new high. An exact-UT pin would have red the very next flight. The declared windows are[0, 100](ascent) and[100, 400](impact) - see the review section below for why the first draft's[0, 60]/[100, 140]was measured against the wrong clock and had to be corrected before merge. The funds milestone entry (seq=3) is deliberately left window-free: KSP logs no funds award, so it is never capture-matched.The expected totals did not move, which is the review's ordering caveat (b) verified rather than assumed:
oracle-expected funds=529600.0 science=100.0 rep=-7.999829000000001, identical on steps 1 and 2. CL-2's entries are allut-less so_sort_keyordering is untouched, and all three rep entries arerepMode="applied"so the nonlinear curve is not re-entered. This was checked offline against step 1's realcapturedRawbefore spending step 2's flight (3 unmatched -> 0, totals byte-identical), which is the same burned-flight economics the rest of this PR is about.Guards updated to match: the two whole-set cells are now explicit allowlists naming CL-2 with its arming evidence (
test_only_the_armed_allowlist_arms_the_capture_cross_check,test_only_the_armed_allowlist_declares_a_ut_window), so a second spec arming the gate still reds until its own evidence is recorded. New cells pin the phase bounds, replay the measured award set through the real matcher, and probe that the armed gate still bites (the first version of that probe was degenerate - see the review section). CL-2's own cell now pins GATE as the recorded decision with the run ids.Item 1 - the ledger capture cross-check is armable on FLOWN scenarios
Finding (CL-2's first live capture, 2026-07-30):
hlib.unmatched_captured_awardsjoined captured awards to seam entries on a UT-valuedseq_key. A flown spec cannot pin that UT, so all three of CL-2's correctly-declared awards reported "unexpected", andcaptureCrossCheck = "gate"was unarmable exactly where it matters.Fix (windowed-UT, chosen over amount-only / reason-only joins): a manifest entry may declare
utWindow = [lo, hi](inclusive;oracle.parse_manifest_entries->ManifestEntry.ut_window). A windowed entry matches a captured award whose UT falls inside the bounds instead of requiring exactseq_keyequality. A window is what a flown spec CAN honestly declare - mission phase bounds are stable across runs even though the exact UT is not - and unlike the other two options the spec still constrains when the award may land.Preserved invariants (all pinned by tests):
compute_expectednever reads it; a captured amount is never summed into EXPECTED; the seam-declared-vs-save diff is untouched.stockReasonentries try first; within each group, entries try in acceptance-WIDTH order (exact key = 0, window = hi-lo), so neither a window over an exact entry nor a wide window over a narrow one can greedily strand the award the tighter entry names.lo > hi, malformed shapes, andut+utWindowtogether all reject at parse time and pre-launch (the pre-launch half now delegates to the oracle outright - see the review section).test_hlib.py::FlownScenarioUtWindowCorroborationTests(15 cells) pins the CL-2 shape end-to-end from the real log idiom with the measured lines as literals.Item 2 - HARNESS-INJECT-FAILS-OPEN fails closed at stage time
The item that burned three full flights (S1.5 attempt 1, both V1-map-dwell flights). Driver-side only:
run.py::stage_fixturenow asserts the injection postcondition after the injector returns, whatever its exit code -_inject_postcondition_missingrequires a non-emptyParsek/Recordings/for both presets plusParsek/RewindPoints/rp_b9_root.sfsforrewind-b9. A miss is terminal INVALID(stage-inject-noop) pre-boot, with the error naming the likely cause and remedy. Deliberately not inRETRYABLE_INVALID_SUBKINDS: the miss is deterministic per worktree, so a retry would reproduce the V1-map-dwell double-flight burn.--no-buildstays on the injector, exactly as the todo's DO-NOT demands; the check is mechanism-independent, so the hidden coupling torun_analyzer's building side effect no longer matters.Covered by
test_run_smoke.py::InjectPostconditionTeststhrough the fake-KSP harness, and now live-proven above.Item 3 - HLIB-ALLOWBATCH-NONLITERAL-FAILS-OPEN
hlib._resolve_bool_default_trueread anything not literallyfalseas batch-allowed. It now resolves only absent / literaltrue/ literalfalse; anything else returns None, whichparse_ingame_test_declarationsmaps to fail-closedallow_batch = Falseplus an<unresolved:...>marker reported byunresolved_ingame_declarations, so the sync gate reds on the declaration itself.Whole-tree recount with the parser itself, identical to the pre-branch parser over the same tree:
Zero markers => every committed argument is literal => the fail-closed branch is dead code against today's tree by construction.
Item 4 (new) - the pre-launch ledger gate now mirrors the oracle's
utand non-table rulesThe review's in-pattern follow-up to MINOR-4.
validate_ledger_expectationsmirrored the oracle'sutWindowrules but still passed a malformed per-entryut(true/"x"/nan/inf) and an entry that is not a table at all. Measured before the fix - all six shapes pass ADMIT and then hard-fail after the flight as a manifest-parse-errorPARSEK-FAIL(ledger):The gate now mirrors the oracle for the three ENTRY-SHAPE keys an author hand-writes off a
capturedRawreadout - entry-is-a-table,ut,utWindow- in the same order, so an entry carrying both a badutand a window blames theuton both sides rather than the mutual exclusion.WhatThePreLaunchGateMirrorsTestssweeps the two implementations against each other over the whole malformed-shape space in both directions (a run-time-only rejection costs a flight; a pre-launch-only rejection would refuse a spec the oracle accepts), pins that both sides name the same key, and asserts every committed spec still passes the widened gate. The sweep has teeth: run against the pre-fixhlibit reports 6 divergences, 0 against this one.Deliberately still run-time, recorded in that class's docstring so the boundary stays a decision rather than an oversight:
kind,provenance,amountKind, the state-dependent-facet author-constant rule, the rep magnitude cap,seq,stockReason, and the funds fill-from-capture ambiguity (the last genuinely cannot be judged before the produced log exists).Validation
No C# changed;
dotnet testis proof it stayed green. All committed specs still validate through the real gates, and the two verdict-neutrality whole-set cells now assert the armed allowlist rather than the empty set - CL-2 is in it, deliberately, with its evidence.Docs in the same commits (per commit, not per PR): CHANGELOG (harness style - the reward check is now enforcing on the crew-loss scenario, the first armed gate of its kind, plus the widened pre-launch gate),
autotest-status.md(new session header, known-gate 3's arming paragraph rewritten from "declared by ZERO committed specs" to the armed-allowlist record with the three flights, CL-2's row), and both todo entries struck with their live-proof and arming records. Stale "no committed spec arms/declares" claims inhlib.pyandrun.pycorrected in the same pass.Review panel (4 independent clean-context agents) and what it changed
A four-agent panel with disjoint mandates reviewed the three arming/live-proof commits. It returned 1 HIGH, 6 MEDIUM and a set of wrong numbers, several in the reasoning above. All are fixed in
3a9f020b5, and the corrected spec was re-flown.HIGH - the windows were bounded in the wrong clock. The cross-check matches a captured award's raw Planetarium
ut=, which isfixtureUT(9.06) + padDwell + T+, but the spec's rationale reasoned about the flight. Pad dwell is wall-clock (game time runs 1:1, no warp), so the[100, 140]ceiling left ~20 s of headroom againstmission_runner.CONNECT_BUDGET_SECONDS = 30.0, andshould_retrynever retries a PARSEK-FAIL. Reproduced: +21 s of dwell reds a correct flight while the save diff stays green - a pure false red. Corrected to[0, 100]/[100, 400], verified to cost no discrimination.The re-flight vindicated it.
2026-07-31_1759, PASS attempt 1, 180 s, awards at ut 12.8 / 19.3 / 120.2 - all three moved again and the impact set a new high above every prior run (119.7-119.9).MEDIUM - the armed gate could not see an ABSENT capture. Zero captured awards means unmatched-empty means GREEN: the same no-op-gate fail-open the spec says the gate exists to close. Two stock award lines are now required logContracts, both verified against real archived lines before flying.
MEDIUM - the pre-launch gate now DELEGATES to
oracle.parse_manifest_entries. The "shape vs value/semantic" boundary documented above did not survive review: the oracle withcaptured=Nonerejects every rule deterministically, andseq/stockReasonare pure type rules hand-written on every CL-2 entry. The stated justification was self-contradicting - it rested on the funds fill rule needing the log, whileoracle.py's own comment says that path is unreachable against a real log. One carve-out remains (funds fill reads the captured pool; raising it pre-launch would refuse a spec the oracle could accept). 12 shapes now red pre-boot, not 6, and an unbounded-integerutno longer raisesOverflowErrorout ofvalidate_spec- which has notry/exceptand would have aborted the whole batch.MEDIUM - guard holes in the new tests. Nothing pinned the armed entries'
stockReason(dropping both silently widens the gate to "any +1 rep in window"); the stray-award probe was degenerate (appended after all entries were consumed, so a[0, 10000]widening gave an identical result). Both fixed, plus a manifest-length pin, a connect-budget headroom assertion, and.ut:with the colon.LOW - the armed flight left no artifact proving it was armed.
crossCheck=was emitted only inside the per-unmatched-award loop, so_1645's verifier block was byte-identical to the report-mode run before it. Now on the unconditional line;crossCheck=gateis archived in the re-flight.Numbers corrected (all re-verified against artifacts): 12 divergences not 6; the impact UT is on record for six runs not four; the first
Progressionis not constant (12.0 / 12.4 / 12.5 / 12.8); CL-2 is not "the only scenario measured producing reputation" - CL-1 earns the identical three awards, and the real reason is that CL-1 carries no ledger block and is forbidden one; provision reports no skips here. Stale "no committed spec declares/arms" claims fixed inhlib,run.pyand both docs - including the comment that justified the acceptance-width sort key as inert, which is live now.Final validation: lib 939, provision 203, missions/lib 1107, all OK;
dotnet test19490 passed / 1 skipped / 0 failed with no C# changed.