diff --git a/.trinity/seals/verified_VerifiedSealIdentity.json b/.trinity/seals/verified_VerifiedSealIdentity.json index fd10028ebb..3bf3201185 100644 --- a/.trinity/seals/verified_VerifiedSealIdentity.json +++ b/.trinity/seals/verified_VerifiedSealIdentity.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+407bd6446", + "built_by": "t27c-bootstrap@0.5.2+c0d050148", "closure": [ { "spec": "specs/verified/independence.t27", @@ -11,23 +11,23 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:5951b1eb904503cfc8782af33cc899fcd205243d7980544ca69a65fd56c28070", - "gen_hash_rust": "sha256:c029bf84cd708e2e3b5b81ca88e881c7419e5409ef18bf28891603cd1367870f", - "gen_hash_verilog": "sha256:fe2e9dad3ca8e73d90a7663bc3bdc584e62d4c7c0df01ef38abcd36fa0d654f3", - "gen_hash_zig": "sha256:508a5a6cfc3149295e5ab773d4fd85828bbb93507f8bcb88bf811ab1bdd63def", + "gen_hash_c": "sha256:66b654d8ef2f0c8f84e2f7f701156b25c401b8aceb1b61634b02e7972a60a510", + "gen_hash_rust": "sha256:f1f99ae274ca3cba8fe0c76f309b4b8432986e005e311c7e4e32a870a80720b8", + "gen_hash_verilog": "sha256:722ae2305b03e37e82128f83f96a563e98de555b9db9dd0c6eb711e14280e2f0", + "gen_hash_zig": "sha256:d08aa38a15bcd235b5b7797977390b85ed1ebd5acd54759e2b3203fd50d213cc", "module": "VerifiedSealIdentity", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-10T16:56:24Z", + "sealed_at": "2026-10-18T05:54:56Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:a1d71dd73dbf914dae5e74e37fd39ab75a551185b0aa0e01fb8b8f5ccba1d5b4", + "spec_hash": "sha256:e130c8a418600afe5f97cb9acccf6fa6f7da9cb8c97d427b9c608609d22e7ba3", "spec_path": "specs/verified/seal_identity.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 15, - "total": 15, + "passed": 17, + "total": 17, "vacuous": 0 }, "toolchain": { diff --git a/bootstrap/gen/rust/verified/seal_identity.rs b/bootstrap/gen/rust/verified/seal_identity.rs index 2da39237f4..7966e810f7 100644 --- a/bootstrap/gen/rust/verified/seal_identity.rs +++ b/bootstrap/gen/rust/verified/seal_identity.rs @@ -1,6 +1,6 @@ // Generated from .t27 spec // DO NOT EDIT — generated by t27c -// NOT LOWERED BY THIS BACKEND: 15 test(s), 2 invariant(s), 0 function(s) with no body. +// NOT LOWERED BY THIS BACKEND: 17 test(s), 2 invariant(s), 0 function(s) with no body. // This backend emits declarations only. The spec's checks live in // the Zig and Verilog outputs; do not read this file as verified. @@ -73,9 +73,6 @@ pub fn remint_wants(decision: u8, has_seal: bool) -> bool { if (decision == REUSE) { return false; } - if (decision == REBUILD_MISSING) { - return (has_seal == false); - } return true; } diff --git a/specs/verified/seal_identity.t27 b/specs/verified/seal_identity.t27 index 1491ecda7f..4fa5df914b 100644 --- a/specs/verified/seal_identity.t27 +++ b/specs/verified/seal_identity.t27 @@ -94,13 +94,17 @@ pub fn checks_pass(failed_zero: bool, forced: bool, tests_total: u32, invariants /// The re-mint: `t27c frontier --reseal` seals again every spec remint_wants() names, and keeps the new /// seal only when remint_keeps() allows it; otherwise the old seal is written back. A stale part (spec, -/// closure, toolchain, config, verdict) is cured by sealing again, and so may a MISSING spec with no seal. -/// A MISSING spec that has never been sealed is tried too: on 2026-10-10, 44 of the 101 specs with no seal -/// at all passed their tests and had simply never been sealed (#8691). A MISSING spec that HAS a seal is -/// missing only through an import, and sealing it again changes nothing. +/// closure, toolchain, config, verdict) is cured by sealing again, and so is a MISSING one. MISSING is +/// tried whether or not a seal exists, and the same two gates decide what happens next. A spec that +/// has never been sealed: on 2026-10-10, 44 of the 101 specs with no seal at all passed their tests +/// and had simply never been sealed (#8691). A spec that HAS a seal, a legacy v1 record with no closure, +/// toolchain or config: MISSING says a part was never recorded, and sealing again records it. #10250 resealed +/// 279 such specs with direct `seal --save` runs, because this rule used to skip them. The guards stay where +/// they are: `seal --save` itself refuses a regression (blocked_reseal_allowed) and a new producer over silicon +/// receipts (silicon_queue.reseal_allowed), and a refusal writes the old seal back. A seal already at the +/// current schema comes out the same apart from when and by which build, and is not rewritten. pub fn remint_wants(decision: u8, has_seal: bool) -> bool { if (decision == REUSE) { return false; } - if (decision == REBUILD_MISSING) { return has_seal == false; } return true; } @@ -247,11 +251,33 @@ test remint_wants_only_a_stale_part { assert remint_wants(REBUILD_VERDICT, true) == true; } -test remint_wants_a_never_sealed_spec_but_not_an_import_gap { +test remint_wants_a_missing_spec_sealed_or_not { // never sealed: try it, remint_keeps decides assert remint_wants(REBUILD_MISSING, false) == true; - // sealed, missing only through an import: resealing it changes nothing - assert remint_wants(REBUILD_MISSING, true) == false; + // a legacy seal (#10250): sealing again records the closure, toolchain and config it lacks + assert remint_wants(REBUILD_MISSING, true) == true; + // a reused spec is still left alone, sealed or not + assert remint_wants(REUSE, true) == false; +} + +test a_missing_spec_with_a_v1_seal_is_resealed_only_where_remint_keeps_allows { + // the v2 re-seal of a v1 spec that passes: kept + assert remint_wants(REBUILD_MISSING, true) == true; + assert remint_keeps(2, true, false, 6, 0, 0, true) == true; + // the same spec when seal --save recorded a failure, a forced run, or a vacuous suite: old seal written back + assert remint_keeps(2, false, false, 6, 0, 0, true) == false; + assert remint_keeps(2, true, true, 6, 0, 0, true) == false; + assert remint_keeps(2, true, false, 6, 0, 6, true) == false; + // a seal that stayed at schema 1: not kept + assert remint_keeps(1, true, false, 6, 0, 0, true) == false; + // a seal file another spec owns: not kept + assert remint_keeps(2, true, false, 6, 0, 0, false) == false; +} + +test a_missing_spec_that_no_longer_compiles_keeps_its_passing_seal { + // the seal passed, the spec is blocked now: seal --save refuses without --force, so remint_keeps never sees it + assert blocked_reseal_allowed(true, false) == false; + assert blocked_reseal_allowed(false, false) == true; } test remint_keeps_a_v2_seal_whose_checks_ran {