spec(t27mcp): seal_verdict -- the seal receipt of t27_spec (#10066)

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 <parent dir>_<module>.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:<hex>" 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;
+}