Skip to content

t27b vacuous: delete 22 empty generated spec stubs (Closes #8052) - #8054

Merged
gHashTag merged 2 commits into
masterfrom
claude/t27b-vacuous-stubs-8052
Oct 9, 2026
Merged

gHashTag merged 2 commits into
masterfrom
claude/t27b-vacuous-stubs-8052

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 9, 2026

Copy link
Copy Markdown
Owner

Closes #8052
Refs #6063

Lab run 7a07828 (master, https://t27b-lab-production.up.railway.app/runs/7a07828fc8d65c9626f76018c0884a8f01e87ab7.json) has 142 specs the reference passes and t27b passes with 0 runtime asserts (pass_vacuous). This PR deletes the 22 of them that are empty generated stubs.

Deleted specs, each with the proof it was empty

Every file below was checked with the same rule: after removing blank lines and ///; comments, the only lines left are module <Name>;, use base::types; and use math::constants; -- no const, fn, struct, enum, test, invariant or bench. Each had 0 tests, 0 invariants and 0 asserts in run 7a07828.

spec module non-comment lines
specs/ml/activation/silu_swish_vbt_activation.t27 SiluSwishVbt 3: module + 2 use
specs/sacred/cosmology.t27 TriCosmology 3: module + 2 use
specs/sacred/dark_matter.t27 DarkMatter 3: module + 2 use
specs/sacred/gravity.t27 TriGravity 3: module + 2 use
specs/sacred/monopoles.t27 TriMonopoles 3: module + 2 use
specs/sacred/quantum.t27 TriQuantum 3: module + 2 use
specs/sacred/quantum_gravity.t27 QuantumGravity 3: module + 2 use
specs/sacred/superconductivity.t27 TriSuperconductivity 3: module + 2 use
specs/tri/agent/agent_run.t27 AgentRun 3: module + 2 use
specs/tri/agent/agents.t27 Agents 3: module + 2 use
specs/tri/agent/autonomous_universe.t27 AutonomousUniverse 3: module + 2 use
specs/tri/agent/experience_hooks.t27 ExperienceHooks 3: module + 2 use
specs/tri/agent/memory.t27 AgentMemory 3: module + 2 use
specs/tri/collections/context.t27 TriContext 3: module + 2 use
specs/tri/net/cloud.t27 TriCloud 3: module + 2 use
specs/tri/pipeline/cloud_orchestrator.t27 CloudOrchestrator 3: module + 2 use
specs/tri/pipeline/pipeline.t27 TriPipeline 3: module + 2 use
specs/tri/pipeline/spec_parser.t27 TriSpecParser 3: module + 2 use
specs/tri/pipeline/workflow_executor.t27 WorkflowExecutor 3: module + 2 use
specs/tri/pipeline/workflow_parser.t27 WorkflowParser 3: module + 2 use
specs/tri/utils/arrow_time.t27 ArrowTime 3: module + 2 use
specs/tri/utils/colors.t27 TriColors 3: module + 2 use

Also removed

  • 50 seals in .trinity/seals/ whose spec_path is one of the 22 specs (seals are keyed by spec_path; tools/check_seal_coverage.py fails on a seal whose spec is gone). None of them is in tools/seal_baseline.txt.
  • 22 rows in docs/reports/t27b_expectations.json: master's ledger minus exactly those rows (all pass_vacuous, so max_not_pass does not move; no duplicate paths).

Why nothing depends on them

  • git grep of each path and module name over specs/, tools/, scripts/, .github/, bootstrap/, cli/, docs/: no use of them, no generated file under gen/, no row in suite_expectations.json, no open PR touching them (checked the file lists of all open PRs).
  • Remaining hits are reports and ledgers that list files (docs/reports/WAVE_LOOP_*, CORPUS-CENSUS-W737.tsv, data/W569/W600 lists) and tools/oracle/baseline.tsv. The oracle's ratchet compares only the pass count against its 189 floor (the 2026-10-08 nightly passed 1105 of 1600), and the oracle job is continue-on-error, so the baseline is left as its own tool wrote it.
  • #7828 (graph memory epic) already says specs/tri/agent/memory.t27 "MUST be removed or replaced".

Check with the repo's tool

python3 scripts/tri_loop/t27b.py ratchet (= tri t27b ratchet):

  • run 7a07828 against master's ledger: UNEXPECTED FAILURE 11, UNEXPECTED PASS 2, UNLISTED 80, STALE 3, MOVED 3
  • run 7a07828 with the 22 results removed (what the lab sees after this merges) against this branch's ledger: the same line, finding for finding

So the PR adds no ratchet finding; master's ledger is already red for other reasons (another bless is in flight).

Not in this PR

Three more specs are empty in the same way but an open issue names them in its scope and criteria, so they stay: specs/tri/math/math.t27 (#7746), specs/tri/math/measurement.t27 (#2101), specs/tri/utils/string.t27 (#8013, #6654, #2665, #2433, #2526).

Expected effect

Next lab run at master: vacuous 142 -> 120, reference denominator 1213 -> 1191, t27b checked passes unchanged (899 of 1213 -> 899 of 1191).

Files: 22 .t27 deletions, 50 seal deletions (tool-written), 1 ledger edit (tool-written data), 1 NOW entry. No hand-written code.

🤖 Generated with Claude Code

The 22 specs carry only comments, `module X;`, `use base::types;` and
`use math::constants;` -- no const, fn, struct, enum, test, invariant or
bench. Lab run 7a07828 counts each as a reference pass that t27b passes
with 0 runtime asserts (pass_vacuous). Nothing imports or generates from
them.

Also removed: their 50 seals (matched by spec_path) and their 22 rows in
docs/reports/t27b_expectations.json. Expected on the next lab run:
vacuous 142 -> 120, reference denominator 1213 -> 1191.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@gHashTag
gHashTag enabled auto-merge (squash) October 9, 2026 07:19
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 07:48:31 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 43
PRs with All Checks Green 7
READY 0
FAILING 43
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 43 + 0 + 0 = 43, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=3c0ade9e73e4 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag

gHashTag commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

Auto-merge is off; this PR is held for the owner's decision. The 22 files are empty stubs: module plus two use lines. But several look like intentional placeholders, for example the whole of specs/sacred/*. Deleting them also lowers the vacuous-pass count, so the owner should decide whether they go.

@gHashTag
gHashTag enabled auto-merge (squash) October 9, 2026 10:09
docs/reports/t27b_expectations.json conflicted with master's ledger
(be97577). Resolved from master's side: master's ledger minus exactly the
22 rows of the deleted stubs (all pass_vacuous); no row is added and no
other row changes. No seal of a deleted stub came back on master.

Closes #8052

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 11:37:25 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 42
PRs with All Checks Green 8
READY 0
FAILING 42
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 42 + 0 + 0 = 42, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=3c0ade9e73e4 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag
gHashTag merged commit f06b128 into master Oct 9, 2026
29 of 32 checks passed
gHashTag pushed a commit that referenced this pull request Oct 9, 2026
… (Refs #8222, Closes #7370)

test-ratchet was red on this PR (and on master): #8054 deleted 22 empty
spec stubs, but proofs/lean4/Trinity/IcarusLowerable/Completeness.lean
still modelled them, so corpus_classifier_matches_lean_completeness
found 26 envs without specs. #8223 fixes it; this is its two files,
byte-identical to its head ad0b510, so it no-ops once #8223 lands.

cargo test -p t27c --test icarus_lowerable
corpus_classifier_matches_lean_completeness: ok.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
gHashTag added a commit that referenced this pull request Oct 9, 2026
#8222) (#8223)

Since #8054, test-ratchet has been red on every PR. The cause is
corpus_classifier_matches_lean_completeness, which reported 26 envs
without matching specs where it expects 4. The other 22 were the env,
module and theorem triples of the empty generated stubs that #8054
deleted.

Completeness.lean loses those 66 definitions (418 lines). Nothing else
referenced them, and none was in lean_completeness_mismatches.json.

The test's anti-vacuity floor moves from 245 to 223. That is exactly the
22 deleted theorems: deletion, not a theorem going quiet. The four
Lean-only witnesses stay as they are.

Local check: cargo test --release -p t27c --test icarus_lowerable gives
359 passed. The test failed on master with the same message CI shows.

Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

t27b vacuous: delete 22 empty generated spec stubs (module and use lines only)

2 participants