Repository navigation
checks_pass accepts a fully vacuous suite (every test ran 0 asserts) #8693
Description
checks_pass (seal_identity.t27, #8374) refuses a seal whose spec has no tests and no invariants, because "0 failed" of nothing is not a pass. It still accepts a suite in which every test is vacuous: it passed with 0 runtime asserts executed (#6509 counts these).
Seen on 2026-10-10 among never-sealed specs that pass:
specs/numeric/requant_boundary.t27: 1 of 1 tests vacuous.specs/port/trinity/src/tri-api/claude_md.t27: 6 of 6 tests vacuous.
Sealed, frontier would reuse them as verified, although nothing was checked at run time.
Proposal
- Seal record:
seal --saverecordstests.vacuous, whichtest_reportalready counts. - Spec:
checks_pass(failed_zero, forced, tests_total, invariants, vacuous)passes only when(tests_total - vacuous) + invariants > 0. - Frontier and
remint_keepsread it. A seal without the field is read as 0 vacuous, so old seals keep their meaning until resealed.
Acceptance criteria
- A spec whose every test is vacuous and which has no invariant is not kept by
--resealand not reused by frontier. t27c test-report specs/verified/seal_identity.t27passes, including a test that names the vacuous case.- Hand-written lines do not grow.
Boundary
specs/verified/seal_identity.t27
bootstrap/gen/rust/verified/seal_identity.rs
bootstrap/src/service.rs
bootstrap/src/main.rs
User Scenarios
- Given a spec file where every test is vacuous (0 runtime asserts executed) and no invariants exist, When
seal --saveis run, Then the seal record includestests.vacuousequal to the total test count andchecks_passevaluates to false, so the spec is not sealed. - Given an existing seal record without a
tests.vacuousfield (created before this change), When frontier orremint_keepsreads it, Then the missing field is treated as 0 vacuous tests, preserving the seal's original meaning until the spec is resealed. - Given
specs/verified/seal_identity.t27which tests the vacuous case, Whent27c test-report specs/verified/seal_identity.t27runs, Then the command exits 0 and the test that names the vacuous case passes.
Requirements
FR-001: seal --save MUST record tests.vacuous in the seal record using the count already produced by test_report.
FR-002: checks_pass(failed_zero, forced, tests_total, invariants, vacuous) MUST return true only when (tests_total - vacuous) + invariants > 0.
FR-003: Frontier MUST read tests.vacuous from seal records and treat a missing field as 0, so old seals remain valid until resealed.
FR-004: remint_keeps MUST read tests.vacuous from seal records with the same default of 0 for missing fields.
FR-005: A spec whose every test is vacuous and which has no invariant MUST NOT be kept by --reseal and MUST NOT be reused by frontier.
FR-006: t27c test-report specs/verified/seal_identity.t27 MUST pass including a test that names the vacuous case.
FR-007: The change MUST NOT increase hand-written lines of code.
Activity
frontier --reseal tries a never-sealed spec; 39 of them pass and are …
audit: a reused verdict whose rerun checked nothing is poisoned (Closes