Skip to content

checks_pass accepts a fully vacuous suite (every test ran 0 asserts) #8693

Closed

Description

@gHashTag

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 --save records tests.vacuous, which test_report already counts.
  • Spec: checks_pass(failed_zero, forced, tests_total, invariants, vacuous) passes only when (tests_total - vacuous) + invariants > 0.
  • Frontier and remint_keeps read 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 --reseal and not reused by frontier.
  • t27c test-report specs/verified/seal_identity.t27 passes, 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 --save is run, Then the seal record includes tests.vacuous equal to the total test count and checks_pass evaluates to false, so the spec is not sealed.
  • Given an existing seal record without a tests.vacuous field (created before this change), When frontier or remint_keeps reads 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.t27 which tests the vacuous case, When t27c test-report specs/verified/seal_identity.t27 runs, 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.

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions