Repository navigation
seals: verdict-blocked specs compile and seal; 11 refused specs fixed, 30 blocked ones listed (Refs #8314) - #10370
Merged
Merged
Conversation
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>
…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>
…ing 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>
… 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>
…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>
…e branch side, resealed next) Refs #8314 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ster'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>
gHashTag
enabled auto-merge (squash)
October 18, 2026 09:47
Contributor
This was referenced Oct 18, 2026
Merged
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
…Status leaves the ledger, five specs resealed (Closes #10389) #10370 made specs parse that did not before, so Context, MatchResult, UnsubscribeResult and ProofTrace gained a second definition. Renamed on the side #10370 touched: LocalhostContext (security.t27), RouteMatchResult (router.t27), SchemaUnsubscribeResult (bus/schema.t27), CoaProofTrace and DatalogProofTrace. HttpStatus has one definition again, so its ledger line and classified row are dropped. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
…Status leaves the ledger, five specs resealed (Closes #10389) #10370 made specs parse that did not before, so Context, MatchResult, UnsubscribeResult and ProofTrace gained a second definition. Renamed on the side #10370 touched: LocalhostContext (security.t27), RouteMatchResult (router.t27), SchemaUnsubscribeResult (bus/schema.t27), CoaProofTrace and DatalogProofTrace. HttpStatus has one definition again, so its ledger line and classified row are dropped. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
…he ledger (Closes #10389) (#10390) * types ratchet: four newly parsed type names get their own names, HttpStatus leaves the ledger, five specs resealed (Closes #10389) #10370 made specs parse that did not before, so Context, MatchResult, UnsubscribeResult and ProofTrace gained a second definition. Renamed on the side #10370 touched: LocalhostContext (security.t27), RouteMatchResult (router.t27), SchemaUnsubscribeResult (bus/schema.t27), CoaProofTrace and DatalogProofTrace. HttpStatus has one definition again, so its ledger line and classified row are dropped. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * ledger: unsubscribe_result_create is no longer a duplicate body (Closes #10389) Co-Authored-By: Claude Sonnet 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
#10370 (Closes #10450) #10370 rewrote specs/ar/asp_solver.t27 and specs/ar/ternary_logic.t27 so they compile (#8980): Program is now fixed arrays with counts, Trit is i8, and the list functions take slices. The pinned source signatures and the Lean witness models were stale. The specs and gen-rust output are correct, so the expected signatures and the Lean models are updated to the real interfaces; ar_asp_solver stays unlowerable (string fields), and a new theorem pins the exact set of slice/usize functions that block ar_ternary_logic. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
#10370 (Closes #10450) (#10462) #10370 rewrote specs/ar/asp_solver.t27 and specs/ar/ternary_logic.t27 so they compile (#8980): Program is now fixed arrays with counts, Trit is i8, and the list functions take slices. The pinned source signatures and the Lean witness models were stale. The specs and gen-rust output are correct, so the expected signatures and the Lean models are updated to the real interfaces; ar_asp_solver stays unlowerable (string fields), and a new theorem pins the exact set of slice/usize functions that block ar_ternary_logic. 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.
Refs #8314
What this PR is
Branch
seal/verdict-blockedhad no PR. It carried the verdict fix (143 of the 153 verdict-blocked specs compile, pass and stop being vacuous) and a seal run with four problems. This PR adds two commits on top and answers all four. Noseal --forceanywhere; every seal below was produced byt27c frontier --resealon the Railway lab (~/t27-lanes/fs-lab.sh), nothing was built or tested on the Mac.8ae9de1ed.t27only: 10 specs declare string arrays as[N]strinstead of[N][]const u842040f96e.trinity/seals/*.json: 296 files (284 refreshed, 12 new)4ab200073.trinity/sealsconflicted, taken from the branch)6e5043b2eOnly
.t27and tool-written seal data are touched; no code in any other language.1. Refused specs: 11 (the brief said 10)
Reason for all of them:
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 primitive, and it reads[2][]const u8as an array of the aggregateconst u8.[N]stris the same slice type without][and passes. Fixed in.t27, same strings, same asserts, only the declared local type changed:config/schema,port/tools/{dedupe_identical_tests,published_figures,queen/feed_untested},runtime/{execute,process},server/router([][]const u8to[]str),tri/io/{filesystem,fs},tri/search/match, plusverify_trainer_c, which was refused too but needed no edit once its closure was resealed (so commit8ae9de1edsays "ten", the real number is eleven).All 11 now seal with every test passing and no backend rejected.
2. Stale seals
After the reseal
t27c seal-auditreportsSTALE (spec edited): 0. I saw 18 stale seals for 15 specs mid-run (the brief said 17); they were stale because the specs they describe were edited by the verdict commit and, for the refused ones, never resealed. They are gone: either resealed, or their legacy twin was refreshed by the same pass.3. Verdict count 10 to 32: not a regression
The 30 specs listed below are not among the 143 this branch changed, and their seals say
blocked: does not compile ...as before the branch.frontierranks rebuild reasons spec(1) > closure(2) > ... > verdict(5), so a spec with a stale hash or closure shows as "spec"/"closure" and its blocked verdict stays hidden. Each reseal pass clears spec/closure rebuilds, so the verdict bucket grows as it becomes visible: frontier went spec 193 / closure 90 / verdict 12 before the pass to spec 61 / closure 63 / verdict 30 after (final, on the tree merged with master). The brief's 32 and my 30 differ by a few specs whose state depends on which master the pass ran against; I could not reproduce 32 exactly.4. Malformed tar artifact filenames: cause found, fix is not in
.t27Two things combine:
extract_module_name(bootstrap/src/main.rs:5701) takes the first line that starts withmodule, so a spec with such a line in a string or doc produces seal names likesearch_[]const u8.json,"[]const u8".json,enrichment::youtube_transcript.json,tools_specs::port::tools.json. 526 seal files have odd characters (::, spaces, quotes,[],#).git status --porcelainis C-quoted by git (core.quotePath), so a name with"or a non-ASCII byte arrives as".trinity/seals/\"[]const...; handed totar -Tthe quotes become part of the name and tar fails withCannot stat. GNU tar 1.34 itself handles colons and spaces fine.Fix for the transport (used here, plain commands):
git ls-files -z -m -o --exclude-standard .trinity/seals | tar --null -T - -czf out.tgz. Fix for the names is a compiler change (module name from themoduledeclaration, not the first matching line), outside.t27, so only reported.Result of the seal run
frontier --reseal(no--force), run again after merging master: 0 refused,seal-auditSTALE 0. In the 324 committed seal files (296 + 28): 0 blocked, 0 forced, 0 vacuous, 0 failing tests.Still blocked: 30 specs, none changed by this branch
Reasons are the
tests.blockedtext in each seal (Zig compile error). The first group is a spec that refers to a name from another module that its generatedspec.zignever imports; the second is a spec that produces Zig the compiler rejects, which needs a t27c fix or a deeper rewrite.Undeclared identifier (missing import or helper in the spec):
specs/bus/pubsub.t27spec.zig:266:21 use of undeclared identifier 'bus'specs/config/load.t2778:34 undeclared 'config_schema'specs/runtime/instance.t27118:43 undeclared 'runtime_process'specs/file/operations.t2720:46 undeclared 'Result'specs/igla/race/bram_weights.t2765:11 undeclared 'read'specs/igla/race/cordic_top.t27137:11 undeclared 'latency'specs/igla/race/formal.t2755:29 undeclared 'RtlModule'specs/igla/race/opcodes.t27181:17 undeclared 'OP_ADD'specs/igla/race/ternary_dot_sw.t2797:5 undeclared 'latency_us'specs/ml/transformer/multi_head_attn.t27181:19 undeclared 'random_input'specs/tools/tri_to_t27_converter.t2782:19 undeclared 'trim'specs/enrichment/youtube_transcript.t2755:21 invalid builtin '@trim'Generated Zig is invalid or the type does not match (t27c gen-zig gap or a type fix in the spec):
specs/compiler/optimizer.t2721:5 duplicate enum member 'String'specs/compiler/stdlib.t27229:36 expected ',' after initializerspecs/compiler/typechecker.t2780:53 expected ',' after initializerspecs/igla/race/ternary_gemm.t27504:49 expected '}', found ':'specs/provider/stream.t27153:102 expected '}', found ':'specs/neural/forward_pass.t2739:37 expected ']', found ';'specs/fpga/mac.t27202:11 redeclaration of local constant 'a'specs/sync/index.t27180:29 unused capturespecs/test_framework/runner.t2784:29 unused function parameterspecs/lsp/client.t27145:339 expected '[]u8', found '*const [8:0]u8'specs/lsp/server.t2718:32 expected '[3]u8', found '*const [7:0]u8'specs/provider/adapters.t2722:36 expected '[3]u8', found '*const [3:0]u8'specs/provider/transform.t27215:33 expected '[]u8', found '*const [19:0]u8'specs/tri/utils/bytes.t2728:36 index syntax required for slice type '[]const u8'(blocked on master too)specs/tri/utils/logging.t2777:22 undeclared 'tag': theif (opt) |tag|capture is not lowered (blocked on master too)specs/tri/crypto/crypto.t2738:5 not yet implementedspecs/tri/encoding/json.t2753:18 no member 'parseValue' in 'spec.Parser'specs/depin/prove.t27unable to load 'TriSha256.zig': FileNotFound(closure file not generated)I did not fix these 30: each needs its own spec work (or a t27c change for the gen-zig group) and none belongs to the verdict-test fix this branch is about. They are the honest remaining list for #8314.
Not covered
docs/nona-03-manifest/*.md,specs/sandbox/sandbox.tri, ...) and 89 seals whose spec file no longer exists were already there; not touched.🤖 Generated with Claude Code