From e60102ac26e80138105b7a723a3cb7217b905854 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 12:12:50 +0700 Subject: [PATCH] spec(t27mcp): seal_verdict -- the seal receipt of t27_spec (#10066) t27_spec hands out a spec; this hands out the receipt for it. The verdict (verified, stale, unsealed, vacuous, failing, forced, unknown) is decided by specs/verified/seal_check.t27 (seal_check_alg, fail closed) with PART_* codes from specs/verified/reuse.t27; this spec only maps the answer onto words and adds three things the checker lacks: a seal whose recorded spec_path is another path is no seal of this spec (case twins, #8540), the byte-for-byte comparison of two sha256 strings, and the vacuous verdict. 9 tests, 0 vacuous; six mutations each fail 1-2 tests. Compiled to wasm for gHashTag/t27-mcp on the lab. Co-Authored-By: Claude Sonnet 5.5 --- specs/t27mcp/seal_verdict.t27 | 173 ++++++++++++++++++++++++++++++++++ 1 file changed, 173 insertions(+) create mode 100644 specs/t27mcp/seal_verdict.t27 diff --git a/specs/t27mcp/seal_verdict.t27 b/specs/t27mcp/seal_verdict.t27 new file mode 100644 index 0000000000..9f2c21f1dc --- /dev/null +++ b/specs/t27mcp/seal_verdict.t27 @@ -0,0 +1,173 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/t27mcp/seal_verdict.t27 -- the seal receipt of t27_spec in the t27 MCP server (gHashTag/t27-mcp): what a +; spec's seal says about the spec an agent is about to reuse. See #10066 (epic), the validated-code contract: +; t27_find and t27_spec hand out code, this hands out the receipt for it. +; -- +; The rules are not written here. specs/verified/seal_check.t27 decides what a seal's parts mean (fail closed: +; a part that cannot be compared is UNKNOWN, a forced seal is never a pass, a seal that failed a test is a +; failure) and specs/verified/reuse.t27 owns the PART_* codes. This file calls seal_check_alg() and maps its +; answer onto the words an agent reads. It adds three things the checker does not have: +; - the seal belongs to the asked spec: the seal file name is _.json, so two specs can +; derive one name (gHashTag/t27#8540). A seal whose recorded spec_path is another path is no seal of this one. +; - the digest comparison: the server hashes the current source, this compares the two "sha256:" strings +; byte for byte. A string that is not that shape is not an observed part. +; - vacuous: a green seal with no test, or with a test that asserts nothing, verifies nothing. +; The seal records the hashes of the four generated backends too. The server cannot regenerate them, so they are +; passed as PART_SAME: "fresh" here means the spec bytes are the sealed bytes, nothing more. `t27c seal --verify` +; is the full check. +; -- +; Verdicts, in the order they are decided: unsealed, unknown, stale, forced, failing, vacuous, verified. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module T27mcpSealVerdict; + +use verified::reuse; +use verified::seal_check; + +/// seal_verdict() answers; the index into VERDICT_NAME and VERDICT_NOTE. +pub const SV_UNSEALED : u32 = 1; +pub const SV_UNKNOWN : u32 = 2; +pub const SV_STALE : u32 = 3; +pub const SV_FORCED : u32 = 4; +pub const SV_FAILING : u32 = 5; +pub const SV_VACUOUS : u32 = 6; +pub const SV_VERIFIED : u32 = 7; + +pub const VERDICT_NAME : [8]str = [ + "none", "unsealed", "unknown", "stale", "forced", "failing", "vacuous", "verified" +]; + +pub const VERDICT_NOTE : [8]str = [ + "", + "No seal of this spec: nobody has run its tests into a receipt. Run t27c test-report before you rely on it.", + "The seal cannot be compared with the source (no or unknown digest). Treat as unverified.", + "The source changed after the seal. The seal says nothing about this text; reseal it before you rely on it.", + "The seal was forced past failing tests. It is not a pass.", + "The sealed run had failing tests.", + "The seal holds no test that asserts anything, so it verifies nothing.", + "The source is the sealed source and its sealed tests passed." +]; + +/// The length of a string. +pub fn str_len(s: string) -> u32 { + return (s.len as u32); +} + +/// 1 when a and b are the same bytes, 0 otherwise. +pub fn same_bytes(a: string, b: string) -> u32 { + var n : u32 = str_len(a); + if (n != str_len(b)) { return 0; } + var i : u32 = 0; + while (i < n) { + if ((a[i] as u32) != (b[i] as u32)) { return 0; } + i = i + 1; + } + return 1; +} + +/// ALG_SHA256 when h is "sha256:" and 64 more characters, 0 for any other shape. +pub fn hash_alg(h: string) -> u8 { + if (str_len(h) != 71) { return 0; } + var pre : string = "sha256:"; + var i : u32 = 0; + while (i < 7) { + if ((h[i] as u32) != (pre[i] as u32)) { return 0; } + i = i + 1; + } + return ALG_SHA256; +} + +/// The spec part of the seal: MISSING when either digest is not a sha256 string, else SAME or DIFF. +pub fn spec_part(recorded: string, current: string) -> u8 { + if (hash_alg(recorded) != ALG_SHA256) { return PART_MISSING; } + if (hash_alg(current) != ALG_SHA256) { return PART_MISSING; } + if (same_bytes(recorded, current) == 1) { return PART_SAME; } + return PART_DIFF; +} + +/// 1 when the source the server hashed is the source the seal recorded. +pub fn is_fresh(recorded: string, current: string) -> u32 { + if (spec_part(recorded, current) == PART_SAME) { return 1; } + return 0; +} + +/// The verdict on one seal. has_seal is 0 when no seal file was found. The test counts come from the seal's +/// tests object; an absent vacuous count is 0, an absent tests object is total 0. +pub fn seal_verdict(has_seal: u32, seal_path: string, path: string, recorded: string, current: string, total: u32, passed: u32, failed: u32, failing_n: u32, vacuous: u32, forced: u32) -> u32 { + if (has_seal == 0) { return SV_UNSEALED; } + if (same_bytes(seal_path, path) == 0) { return SV_UNSEALED; } + var green : bool = false; + if (failed + failing_n == 0) { + if (passed == total) { green = true; } + } + var c : u8 = seal_check_alg(hash_alg(recorded), spec_part(recorded, current), PART_SAME, PART_SAME, PART_SAME, PART_SAME, green, forced != 0); + if (c == CHECK_SPEC_DIFF) { return SV_STALE; } + if (c == CHECK_FORCED) { return SV_FORCED; } + if (c == CHECK_FAILED) { return SV_FAILING; } + if (verdict_pass(c) == false) { return SV_UNKNOWN; } + if (total == 0) { return SV_VACUOUS; } + if (vacuous > 0) { return SV_VACUOUS; } + return SV_VERIFIED; +} + +pub const H_A : string = "sha256:66cc87ba315b75ba80b51b6813d84cb238149e6e75a4f1f55a5fec4915be7c1f"; +pub const H_B : string = "sha256:66cc87ba315b75ba80b51b6813d84cb238149e6e75a4f1f55a5fec4915be7c1e"; + +test "a seal of this spec, the same bytes, passing tests is verified" { + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 0, 0, 0) == SV_VERIFIED; + assert is_fresh(H_A, H_A) == 1; +} + +test "no seal file is unsealed" { + assert seal_verdict(0, "", "specs/a/x.t27", "", H_A, 0, 0, 0, 0, 0, 0) == SV_UNSEALED; +} + +test "case twin: a seal recorded for another path is not a seal of this spec" { + assert seal_verdict(1, "specs/b/x.t27", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 0, 0, 0) == SV_UNSEALED; + assert seal_verdict(1, "specs/a/X.t27", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 0, 0, 0) == SV_UNSEALED; + assert seal_verdict(1, "", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 0, 0, 0) == SV_UNSEALED; +} + +test "negative control: one changed digit makes the seal stale, not fresh" { + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_B, 3, 3, 0, 0, 0, 0) == SV_STALE; + assert is_fresh(H_A, H_B) == 0; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_B, 3, 1, 2, 2, 0, 1) == SV_STALE; +} + +test "fail closed: a digest that is not sha256 is unknown, never fresh" { + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", "", H_A, 3, 3, 0, 0, 0, 0) == SV_UNKNOWN; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, "", 3, 3, 0, 0, 0, 0) == SV_UNKNOWN; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", "md5:66cc87ba315b75ba80b51b6813d84cb238149e6e75a4f1f55a5fec4915be7c1f", H_A, 3, 3, 0, 0, 0, 0) == SV_UNKNOWN; + assert is_fresh("", "") == 0; +} + +test "a forced seal is forced, a failing seal is failing" { + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 0, 0, 1) == SV_FORCED; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 2, 1, 0, 0, 0) == SV_FAILING; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 1, 0, 0) == SV_FAILING; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 1, 0, 0, 0, 0) == SV_FAILING; +} + +test "a green seal with no test, or with a test that asserts nothing, is vacuous" { + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 0, 0, 0, 0, 0, 0) == SV_VACUOUS; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 3, 0, 0, 1, 0) == SV_VACUOUS; +} + +test "the order: failing outranks vacuous, forced outranks failing" { + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 2, 1, 0, 2, 0) == SV_FAILING; + assert seal_verdict(1, "specs/a/x.t27", "specs/a/x.t27", H_A, H_A, 3, 2, 1, 0, 0, 1) == SV_FORCED; +} + +test "the word table agrees with the codes" { + assert VERDICT_NAME[SV_UNSEALED] == "unsealed"; + assert VERDICT_NAME[SV_STALE] == "stale"; + assert VERDICT_NAME[SV_VERIFIED] == "verified"; + assert str_len(VERDICT_NOTE[SV_VERIFIED]) > 0; + assert hash_alg(H_A) == ALG_SHA256; + assert hash_alg("sha256:") == 0; +} + +invariant only_verified_is_a_pass { + assert SV_VERIFIED == 7; + assert SV_UNSEALED < SV_VERIFIED; +}