Repository navigation
feat(t27o): obligation ledger -- per-fn status, oracle outcomes, proof strength, stale keys; no fn is unknown coverage - #10251
Merged
Merged
Conversation
…f strength, stale keys; no fn is unknown coverage ledger.t27 (module T27oLedger) carries the REA patterns (morluto/rea, read as a reference) into t27o: - an empty set of obligations is unknown, never ready; - one status per converted fn by a fixed precedence: out of scope, blocked, contradicted, unknown, unowned, implemented, verified; - oracle outcomes pass / fail / unknown / unsupported / truncated / skipped, only pass counts, and a dropped sample makes a run truncated rather than passed; - proof strength none < reuse < test < oracle; a weaker proof never closes a stronger requirement (a float fn needs the oracle, a translated test is not enough); - a file verdict ready / open / failed / unknown, refused when its counts do not add up; - a recorded verdict keyed by source, converter version and std table version. rust_convert.t27: put_report printed "coverage 100%" for a file with no fn at all. It now prints "coverage unknown: no fn seen", with a negative-control test. rust_convert does not call ledger.t27 yet; wiring it into the report is a follow-up. Refs #10066 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
gHashTag
enabled auto-merge (squash)
October 18, 2026 06:13
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
…7c emits
specs/t27f/spec_graph{,_derive,_export,_fold}.t27 and specs/tools/t27o/rust_convert.t27 changed on
master without a reseal (rust_convert in #10251), which kept spec-guards and seal coverage red on
master. specs/igla/own_model{,_board}.t27 were sealed earlier in this branch by a compiler older than
master's. All 7 resealed with t27c built from this tree (no --force). On the lab, with that binary:
tools/check_seal_currency.py 0 stale of 2732; tools/check_seal_coverage.py OK, 2610 hold, 122
known-broken already in seal_baseline.txt.
Refs #8314
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
* seals: reseal 279 specs so t27c frontier reuses more Tool-written seals only (.trinity/seals/*.json), produced on the lab with t27c frontier --reseal and, for legacy v1-sealed specs that --reseal never touches, t27c seal --save, keeping a seal only when it is schema 2, has no failing tests, is not forced and is not vacuous (the same rule as si::remint_keeps). No --force. Specs whose tests fail, whose generated Zig does not compile, or whose reseal the silicon-receipt guard refuses were left alone. Refs #8314 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * seals: reseal 7 specs whose seals no longer describe what master's t27c emits specs/t27f/spec_graph{,_derive,_export,_fold}.t27 and specs/tools/t27o/rust_convert.t27 changed on master without a reseal (rust_convert in #10251), which kept spec-guards and seal coverage red on master. specs/igla/own_model{,_board}.t27 were sealed earlier in this branch by a compiler older than master's. All 7 resealed with t27c built from this tree (no --force). On the lab, with that binary: tools/check_seal_currency.py 0 stale of 2732; tools/check_seal_coverage.py OK, 2610 hold, 122 known-broken already in seal_baseline.txt. Refs #8314 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
…, 30 blocked ones listed (Refs #8314) (#10370) * seals: reseal 279 specs so t27c frontier reuses more Tool-written seals only (.trinity/seals/*.json), produced on the lab with t27c frontier --reseal and, for legacy v1-sealed specs that --reseal never touches, t27c seal --save, keeping a seal only when it is schema 2, has no failing tests, is not forced and is not vacuous (the same rule as si::remint_keeps). No --force. Specs whose tests fail, whose generated Zig does not compile, or whose reseal the silicon-receipt guard refuses were left alone. Refs #8314 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * seals: reseal 7 specs whose seals no longer describe what master's t27c emits specs/t27f/spec_graph{,_derive,_export,_fold}.t27 and specs/tools/t27o/rust_convert.t27 changed on master without a reseal (rust_convert in #10251), which kept spec-guards and seal coverage red on master. specs/igla/own_model{,_board}.t27 were sealed earlier in this branch by a compiler older than master's. All 7 resealed with t27c built from this tree (no --force). On the lab, with that binary: tools/check_seal_currency.py 0 stale of 2732; tools/check_seal_coverage.py OK, 2610 hold, 122 known-broken already in seal_baseline.txt. Refs #8314 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * specs: 143 of the 153 verdict-blocked specs compile, pass and stop being vacuous t27c frontier counted 153 specs under rebuild reason `verdict`: their generated Zig did not compile or their tests failed, so no seal could be saved and frontier rebuilt them every run. 143 now compile with every test passing and 0 vacuous passes, checked with t27c test-report on the lab. The fixes are .t27 only: - Zig-isms the lowering cannot take (for-captures, `!=` on structs, untyped array literals, missing casts, undeclared helpers) rewritten into constructs it lowers. - Stubs whose tests expected behaviour were given that behaviour; placeholder asserts became real. - Where a test's expected value was provably wrong it was changed, with the reason recorded in the PR, for example: bus/schema "lsp_request" length 10 -> 11, "running" 6 -> 7; igla/race/ ternary_mac a sign error -2147483520 -> 2147483520; tri/utils/time 1010 -> 1011; sync/schema reconcile enum 5 -> 4. 10 specs are left unchanged because they need a compiler feature, another spec or an owner call: tri/encoding/json, igla/race/{bram_weights,cordic_top,formal,opcodes}, enrichment/youtube_transcript, tools/tri_to_t27_converter, tri/crypto/crypto, physics/formula_discovery, depin/prove. Seals for these specs and their direct importers come in the next commit. Refs #8314 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * specs: ten specs declare their string arrays as [N]str so gen-verilog accepts them and they can be sealed The reseal run on this branch refused ten specs: "refusing to seal ...: 1 of 4 backends rejected it". gen-verilog (detect_unsupported_verilog_locals) rejects a local whose type contains "][" and whose element is not a primitive, and it reads `[2][]const u8` as an array of the aggregate `const u8`. The previous commit wrote its test fixtures that way. `[N]str` means the same slice type, has no "][" and passes the check. Same strings, same asserts, only the local's declared type changes in config/schema, port/tools/{dedupe_identical_tests,published_figures,queen/feed_untested}, runtime/{execute,process}, server/router, tri/io/{filesystem,fs}, tri/search/match. Refs #8314 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * seals: reseal 296 seal files after the verdict fixes; no stale seal, no refused spec left Output of `t27c frontier --reseal` on the Railway lab (no --force) on top of the [N]str commit. 284 existing seals refreshed, 12 new. None is blocked, forced, vacuous or has a failing test. Eleven specs were refused before (not ten: verify_trainer_c was refused as well); they now seal with every test passing. `t27c seal-audit` reports STALE 0 afterwards. The 29 specs whose seal says "blocked: does not compile" are untouched: their blocked seals are unchanged by this branch and the frontier only shows them as "verdict" once their spec and closure rebuilds are gone (10 -> 29 is that surfacing, not a regression). Reasons are in the PR body. Refs #8314 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * seals: reseal 28 seals after merging master, so the branch matches master's compiler Master moved by 32 commits (gen-zig open-ended slices, new specs). Seal conflicts were taken from the branch in the merge; this is the frontier reseal on the Railway lab afterwards (no --force): 28 seal files refreshed, none blocked, forced, vacuous or failing. seal-audit reports STALE 0. Refs #8314 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
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
1 participant
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.
What
specs/tools/t27o/ledger.t27(moduleT27oLedger) is the obligation ledger of a t27o conversion. It decides what each converted fn's evidence is worth beforegolden.t27counts it:oracle_outcomeproof_of,proof_satisfiesfn_statusledger_status,summary_adds_upkey_stateCONVERTER_VERSIONandSTD_TABLE_VERSION. A change in any one makes it stale.rust_convert.t27:put_reportprintedcoverage 100%for a file with no fn at all. It now printscoverage unknown: no fn seen. A negative-control test covers this.Where the patterns come from
REA (morluto/rea b83b9ca), read as a reference and run on the lab against itself and against t27c. Nothing from it is linked or copied. The source file of each pattern is named in the spec header. REA's own self-analysis marked its inventory
partialand its t27c analysis listed functions/types/behavior as not recovered. Both are the same honesty rule this spec encodes: unknown is a value with a name, not an absence.Evidence (lab, t27c 0.5.2, zig 0.16.0, HEAD 3200b2a)
t27c test-report specs/tools/t27o/ledger.t27: 10 of 10 pass, 0 vacuous.t27c test-report specs/tools/t27o/rust_convert.t27: 66 of 66 pass, 0 vacuous, including the new test.coverage 100%Not done
rust_convert.t27does not callledger.t27yet. The report still prints its own counts. Wiring the per-fn status and the file verdict into the report line, and into the oracle harness's dropped-sample count, is a follow-up.Refs #10066
🤖 Generated with Claude Code