From 0bd1222cabc4ba96b77c87ee6155ca51d0b5fc91 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 18:23:52 +0700 Subject: [PATCH] claw: specs/claw/evidence.t27 -- the Evidence law every TRI CLAW and t27 MCP fact obeys (Closes #10412) Every published fact (check-run line, SARIF result, review suggestion, MCP tool answer row) is an Evidence record: claim text and strength, the instrument that measured it, source span, full seal digest, coverage (complete/partial/unknown) and one of the four T27F labels. Five rules, each a test block: coverage is read only from its exact word and a missing one is refused, never defaulted; unknown stays unknown and caps a composition at partial; parses/typechecks never becomes holds; ready/covered only over rows on one full seal digest; a publish is verified only by a read-back after the final write. evidence_pins.t27 pins every explicit length to .len and the labels to specs/t27f/spec_graph.t27. Idea from REA's Evidence model; no REA code. Lab: spec-status IMPLEMENTED; test-report 12/12 and 4/4, 0 vacuous; 6 of 6 mutants killed by the test of their rule; gen-c lowers and cc compiles the result. Co-Authored-By: Claude Opus 5.5 --- specs/claw/evidence.t27 | 560 +++++++++++++++++++++++++++++++++++ specs/claw/evidence_pins.t27 | 87 ++++++ 2 files changed, 647 insertions(+) create mode 100644 specs/claw/evidence.t27 create mode 100644 specs/claw/evidence_pins.t27 diff --git a/specs/claw/evidence.t27 b/specs/claw/evidence.t27 new file mode 100644 index 0000000000..25b0ba1436 --- /dev/null +++ b/specs/claw/evidence.t27 @@ -0,0 +1,560 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/claw/evidence.t27 -- the Evidence law: the one shape every fact TRI CLAW and the t27 MCP +; server publish must take before it is published (#10412; epic #9271). A fact is a check-run line, +; a SARIF result, a review suggestion, or one row of an MCP tool answer. Each is an Evidence record: +; claim what the fact says (its text) and how strong it is (CL_PARSES < CL_TYPECHECKS < +; CL_HOLDS), plus the instrument that measured it (parser, typechecker, test-report) +; with the runtime assert and failure counts that instrument printed; +; span the file and the line range the fact is about; +; seal the full seal digest of the spec it was measured against (sha256: + 64 hex); +; coverage how much of the question the fact covers: complete, partial or unknown; +; label how it was inferred: exact, derived, suggested or unknown -- the four T27F labels, +; same values as specs/t27f/spec_graph.t27 (pinned in specs/claw/evidence_pins.t27). +; -- +; The idea comes from the Evidence model of REA (morluto/rea, rea-agents 6.7.0, MIT): coverage is a +; required field that may say "unknown"; unknown stays unknown instead of becoming invented +; certainty; readiness requires comparable cited evidence; and a published artifact's identity is +; rechecked after the final write. Only the idea is taken. The five rules, each one a test below: +; R1 coverage is required and read only from its exact word; a missing or prose value is +; refused (COV_MISSING), never defaulted to complete; +; R2 an unknown input stays unknown, and anything composed from an unknown is at best partial; +; labels compose to the weakest input; +; R3 "parses" or "typechecks" never becomes "holds": t27c's typecheck stays ok on a spec that +; asserts 1 > 2, so CL_HOLDS needs a test-report with at least one runtime assert and none +; failed; +; R4 "ready" and "covered" are declared only over comparable rows: every cited row well formed +; and on the same full seal digest; a 12-digit display prefix is a label, not a digest; +; R5 a published artifact is verified only by a digest read back AFTER its final write. +; -- +; Fail closed, never guess: every check answers a refusal code, and nothing here upgrades a value. +; gen-c lowers str to const char* and cannot express .len, so every string carries its length +; (the specs/claw/gates.t27 idiom); the pins that tie each length to the bytes live in +; specs/claw/evidence_pins.t27, a test-only module. str_eq and has_prefix come from +; specs/claw/text.t27. +; The honest limit: this is the law, not its wiring. No emitter builds Evidence records yet -- +; sarif_feed, suggest_feed, t27f_gate and the t27mcp tools adopt it one by one, each in its own PR. +; ASCII only (L3). phi^2 + 1/phi^2 = 3 | TRINITY + +module ClawEvidence; + +use claw::text; + +/// Coverage: how much of the question one fact covers. COV_MISSING is what a reader answers for an +/// absent or unrecognised field; it is a refusal, never a fourth coverage. +pub const COV_COMPLETE : u8 = 0; +pub const COV_PARTIAL : u8 = 1; +pub const COV_UNKNOWN : u8 = 2; +pub const COV_KINDS : u8 = 3; +pub const COV_MISSING : u8 = 255; +pub const COV_NAMES : [3]str = ["complete", "partial", "unknown"]; +pub const COV_NAME_LENS : [3]usize = [8, 7, 7]; + +/// Inference labels: the four of T27F, in the same order and with the same values as +/// specs/t27f/spec_graph.t27 LABEL_*. A larger value is a weaker label. +pub const LABEL_EXACT : u8 = 0; +pub const LABEL_DERIVED : u8 = 1; +pub const LABEL_SUGGESTED : u8 = 2; +pub const LABEL_UNKNOWN : u8 = 3; +pub const LABEL_KINDS : u8 = 4; +pub const LABEL_MISSING : u8 = 255; +pub const LABEL_NAMES : [4]str = ["exact", "derived", "suggested", "unknown"]; +pub const LABEL_NAME_LENS : [4]usize = [5, 7, 9, 7]; + +/// Claim strength, weakest first. CL_HOLDS means the spec's own asserts held when run. +pub const CL_PARSES : u8 = 0; +pub const CL_TYPECHECKS : u8 = 1; +pub const CL_HOLDS : u8 = 2; +pub const CL_NONE : u8 = 255; + +/// The instrument that measured a fact. Each one implies the ones before it: a spec t27c ran +/// tests on was parsed and typechecked first. +pub const PR_PARSER : u8 = 0; +pub const PR_TYPECHECKER : u8 = 1; +pub const PR_TEST_REPORT : u8 = 2; +pub const PR_NONE : u8 = 255; + +/// The full seal digest, as .trinity/seals/*.json writes spec_hash: sha256: and 64 lowercase hex. +pub const SEAL_PREFIX : str = "sha256:"; +pub const SEAL_PREFIX_LEN : usize = 7; +pub const SEAL_LEN : usize = 71; + +/// check_record answers OK or the first rule the record breaks, in this order. +pub const EV_OK : u8 = 0; +pub const EV_ERR_CLAIM_TEXT : u8 = 1; +pub const EV_ERR_COVERAGE : u8 = 2; +pub const EV_ERR_LABEL : u8 = 3; +pub const EV_ERR_SPAN : u8 = 4; +pub const EV_ERR_SEAL : u8 = 5; +pub const EV_ERR_OVERCLAIM : u8 = 6; +pub const EV_ERR_UNKNOWN_COMPLETE : u8 = 7; +pub const EV_ERR_SUGGESTED_HOLDS : u8 = 8; + +/// recheck verdicts for a published artifact. +pub const PUB_VERIFIED : u8 = 0; +pub const PUB_MISMATCH : u8 = 1; +pub const PUB_UNCHECKED : u8 = 2; + +/// One published fact. +pub struct Evidence { + text : str, + text_len : usize, + claim : u8, + proof : u8, + asserts : u32, + fails : u32, + path : str, + path_len : usize, + line_lo : u32, + line_hi : u32, + seal : str, + seal_len : usize, + coverage : u8, + label : u8, +} + +/// The rows one declaration cites, folded one row at a time by cite. seal is the first kept row's +/// digest; mixed turns true when a later kept row names another one. +pub struct Citation { + rows : u32, + refused : u32, + kept : u32, + seal : str, + seal_len : usize, + mixed : bool, + coverage : u8, + label : u8, +} + +/// Coverage named by the field word w[0..n). Only the three exact lowercase words are read; +/// "", "Complete", "fully covered" and every other text answer COV_MISSING (R1). +pub fn coverage_of(w : str, n : usize) -> u8 { + for k in 0..3 { + if (str_eq(w, n, COV_NAMES[k], COV_NAME_LENS[k])) { return (k) as u8; } + } + return COV_MISSING; +} + +/// Label named by the field word w[0..n); LABEL_MISSING for any other text. +pub fn label_of(w : str, n : usize) -> u8 { + for k in 0..4 { + if (str_eq(w, n, LABEL_NAMES[k], LABEL_NAME_LENS[k])) { return (k) as u8; } + } + return LABEL_MISSING; +} + +pub fn coverage_valid(c : u8) -> bool { + return c < COV_KINDS; +} + +pub fn label_valid(l : u8) -> bool { + return l < LABEL_KINDS; +} + +/// Coverage of a fact composed from two (R2): complete only when both are complete, unknown only +/// when both are unknown, partial otherwise -- so an unknown input caps the result at partial and +/// nothing composes an unknown into complete. A missing input stays a refusal. +pub fn compose_coverage(a : u8, b : u8) -> u8 { + if (coverage_valid(a) == false) { return COV_MISSING; } + if (coverage_valid(b) == false) { return COV_MISSING; } + if (a == b) { return a; } + return COV_PARTIAL; +} + +/// Label of a fact composed from two (R2): the weaker one, so an unknown input stays unknown. +pub fn compose_label(a : u8, b : u8) -> u8 { + if (label_valid(a) == false) { return LABEL_MISSING; } + if (label_valid(b) == false) { return LABEL_MISSING; } + if (a > b) { return a; } + return b; +} + +fn hex_lower(b : u8) -> bool { + if (b >= '0' and b <= '9') { return true; } + if (b >= 'a' and b <= 'f') { return true; } + return false; +} + +/// A full seal digest: exactly sha256: and 64 lowercase hex digits. A display prefix, an +/// uppercase digest or an empty field is refused -- two of those could look equal and not be. +pub fn seal_ok(s : str, n : usize) -> bool { + if (n != SEAL_LEN) { return false; } + if (has_prefix(s, n, SEAL_PREFIX, SEAL_PREFIX_LEN) == false) { return false; } + var i : usize = SEAL_PREFIX_LEN; + while (i < n) { + if (hex_lower(s[i]) == false) { return false; } + i += 1; + } + return true; +} + +/// A span: a non-empty repo-relative path and lines lo..hi with 1 <= lo <= hi. +pub fn span_ok(path : str, path_len : usize, lo : u32, hi : u32) -> bool { + if (path_len == 0) { return false; } + if (path[0] == '/') { return false; } + if (lo < 1) { return false; } + if (hi < lo) { return false; } + return true; +} + +/// The strongest claim an instrument's output supports (R3). A typechecker never supports more +/// than CL_TYPECHECKS, whatever the spec asserts; a test-report supports CL_HOLDS only with at +/// least one runtime assert and no failure -- a vacuous or red run supports CL_TYPECHECKS. +pub fn strongest_claim(proof : u8, asserts : u32, fails : u32) -> u8 { + if (proof == PR_TEST_REPORT) { + if (asserts > 0 and fails == 0) { return CL_HOLDS; } + return CL_TYPECHECKS; + } + if (proof == PR_TYPECHECKER) { return CL_TYPECHECKS; } + if (proof == PR_PARSER) { return CL_PARSES; } + return CL_NONE; +} + +/// Whether the instrument's output supports the claim. +pub fn claim_supported(claim : u8, proof : u8, asserts : u32, fails : u32) -> bool { + if (claim > CL_HOLDS) { return false; } + const most : u8 = strongest_claim(proof, asserts, fails); + if (most == CL_NONE) { return false; } + return claim <= most; +} + +/// The first rule the record breaks, or EV_OK. +pub fn check_record(e : Evidence) -> u8 { + if (e.text_len == 0) { return EV_ERR_CLAIM_TEXT; } + if (coverage_valid(e.coverage) == false) { return EV_ERR_COVERAGE; } + if (label_valid(e.label) == false) { return EV_ERR_LABEL; } + if (span_ok(e.path, e.path_len, e.line_lo, e.line_hi) == false) { return EV_ERR_SPAN; } + if (seal_ok(e.seal, e.seal_len) == false) { return EV_ERR_SEAL; } + if (claim_supported(e.claim, e.proof, e.asserts, e.fails) == false) { return EV_ERR_OVERCLAIM; } + if (e.label == LABEL_UNKNOWN and e.coverage == COV_COMPLETE) { return EV_ERR_UNKNOWN_COMPLETE; } + if (e.label == LABEL_SUGGESTED and e.claim == CL_HOLDS) { return EV_ERR_SUGGESTED_HOLDS; } + return EV_OK; +} + +pub fn record_ok(e : Evidence) -> bool { + return check_record(e) == EV_OK; +} + +/// A citation with no row yet. Nothing can be declared over it. +pub fn no_citation() -> Citation { + return Citation { + rows: 0, + refused: 0, + kept: 0, + seal: "", + seal_len: 0, + mixed: false, + coverage: COV_MISSING, + label: LABEL_MISSING, + }; +} + +/// Cite one more row. A row that breaks a rule is counted as refused and taints the citation; a +/// kept row on another digest than the first marks it mixed; coverage and label compose (R2). +pub fn cite(c : Citation, e : Evidence) -> Citation { + if (record_ok(e) == false) { + return Citation { + rows: c.rows + 1, + refused: c.refused + 1, + kept: c.kept, + seal: c.seal, + seal_len: c.seal_len, + mixed: c.mixed, + coverage: c.coverage, + label: c.label, + }; + } + if (c.kept == 0) { + return Citation { + rows: c.rows + 1, + refused: c.refused, + kept: 1, + seal: e.seal, + seal_len: e.seal_len, + mixed: c.mixed, + coverage: e.coverage, + label: e.label, + }; + } + var mixed : bool = c.mixed; + if (str_eq(c.seal, c.seal_len, e.seal, e.seal_len) == false) { mixed = true; } + return Citation { + rows: c.rows + 1, + refused: c.refused, + kept: c.kept + 1, + seal: c.seal, + seal_len: c.seal_len, + mixed: mixed, + coverage: compose_coverage(c.coverage, e.coverage), + label: compose_label(c.label, e.label), + }; +} + +/// R4: every cited row is well formed and on one seal digest, and there is at least one. +pub fn comparable(c : Citation) -> bool { + if (c.rows == 0) { return false; } + if (c.refused > 0) { return false; } + if (c.mixed) { return false; } + return c.kept == c.rows; +} + +/// "ready" may be published only over comparable rows that do not all stand on unknown coverage. +pub fn may_declare_ready(c : Citation) -> bool { + if (comparable(c) == false) { return false; } + return c.coverage != COV_UNKNOWN; +} + +/// "covered" may be published only over comparable rows whose composed coverage is complete. A +/// row labelled unknown can never be complete (EV_ERR_UNKNOWN_COMPLETE), so it blocks this too. +pub fn may_declare_covered(c : Citation) -> bool { + if (comparable(c) == false) { return false; } + return c.coverage == COV_COMPLETE; +} + +/// R5: the digest of a published artifact, read back after its writes. read_seq and +/// final_write_seq number the events of one publish in order; a read-back that does not come +/// strictly after the final write says nothing about what was published and answers +/// PUB_UNCHECKED, as does a missing read-back or a malformed expected digest. A malformed or +/// different read-back is PUB_MISMATCH. +pub fn recheck(expected : str, expected_len : usize, readback : str, readback_len : usize, read_seq : u32, final_write_seq : u32) -> u8 { + if (seal_ok(expected, expected_len) == false) { return PUB_UNCHECKED; } + if (readback_len == 0) { return PUB_UNCHECKED; } + if (read_seq <= final_write_seq) { return PUB_UNCHECKED; } + if (seal_ok(readback, readback_len) == false) { return PUB_MISMATCH; } + if (str_eq(expected, expected_len, readback, readback_len)) { return PUB_VERIFIED; } + return PUB_MISMATCH; +} + +// --------------------------------------------------------------------------------------------- +// Fixtures: two real seal digests (specs/base/types.t27 and specs/math/constants.t27 as sealed in +// .trinity/seals), and the 12-digit display prefix t27f_gate shows for the first. + +pub const SEAL_A : str = "sha256:3c2fb2a2edf20e90bc76798fb5d12690b2f60fc0f5bbf2f6052936e22d6e62e2"; +pub const SEAL_B : str = "sha256:57187e7afda1d88167b2af0382ad7f0623aa6b269ba020a78e3ffeebba1161bb"; +pub const SEAL_A_SHOWN : str = "3c2fb2a2edf2"; +pub const SEAL_A_SHOWN_LEN : usize = 12; +pub const FIX_PATH : str = "specs/claw/sarif.t27"; +pub const FIX_PATH_LEN : usize = 20; +pub const FIX_TEXT : str = "spec typechecks"; +pub const FIX_TEXT_LEN : usize = 15; + +/// A well-formed typechecker row on seal s, with the given coverage and label. +fn row(s : str, s_len : usize, cov : u8, lab : u8) -> Evidence { + return Evidence { + text: FIX_TEXT, + text_len: FIX_TEXT_LEN, + claim: CL_TYPECHECKS, + proof: PR_TYPECHECKER, + asserts: 0, + fails: 0, + path: FIX_PATH, + path_len: FIX_PATH_LEN, + line_lo: 42, + line_hi: 57, + seal: s, + seal_len: s_len, + coverage: cov, + label: lab, + }; +} + +/// The same row, claiming what proof says with the given counts. +fn claiming(e : Evidence, claim : u8, proof : u8, asserts : u32, fails : u32) -> Evidence { + return Evidence { + text: e.text, + text_len: e.text_len, + claim: claim, + proof: proof, + asserts: asserts, + fails: fails, + path: e.path, + path_len: e.path_len, + line_lo: e.line_lo, + line_hi: e.line_hi, + seal: e.seal, + seal_len: e.seal_len, + coverage: e.coverage, + label: e.label, + }; +} + +test r1_missing_coverage_is_refused_not_defaulted { + // An empty field, a capitalised word and prose are all refused; nothing reads as complete. + assert coverage_of("", 0) == COV_MISSING; + assert coverage_of("Complete", 8) == COV_MISSING; + assert coverage_of("fully covered", 13) == COV_MISSING; + assert coverage_of("complete coverage of all rules", 30) == COV_MISSING; + assert coverage_of("complete", 8) == COV_COMPLETE; + // A record whose coverage was never set is refused at the coverage rule, before anything else + // about it is believed. + const e = row(SEAL_A, SEAL_LEN, COV_MISSING, LABEL_EXACT); + assert check_record(e) == EV_ERR_COVERAGE; + assert record_ok(e) == false; + // And a missing coverage does not compose into a value either. + assert compose_coverage(COV_COMPLETE, COV_MISSING) == COV_MISSING; +} + +test r1_every_coverage_and_label_word_round_trips { + for k in 0..3 { + assert coverage_of(COV_NAMES[k], COV_NAME_LENS[k]) == (k) as u8; + } + for k in 0..4 { + assert label_of(LABEL_NAMES[k], LABEL_NAME_LENS[k]) == (k) as u8; + } + assert label_of("Exact", 5) == LABEL_MISSING; + assert label_of("", 0) == LABEL_MISSING; +} + +test r2_unknown_never_composes_into_complete { + var a : u8 = 0; + while (a < COV_KINDS) { + var b : u8 = 0; + while (b < COV_KINDS) { + const c = compose_coverage(a, b); + if (a == COV_UNKNOWN or b == COV_UNKNOWN) { + assert c != COV_COMPLETE; + } + if (a != b) { + assert c == COV_PARTIAL; + } + b += 1; + } + a += 1; + } + // The unknown input stays unknown; mixed with anything known it is at best partial. + assert compose_coverage(COV_UNKNOWN, COV_UNKNOWN) == COV_UNKNOWN; + assert compose_coverage(COV_COMPLETE, COV_UNKNOWN) == COV_PARTIAL; + assert compose_coverage(COV_COMPLETE, COV_COMPLETE) == COV_COMPLETE; +} + +test r2_labels_compose_to_the_weakest { + var a : u8 = 0; + while (a < LABEL_KINDS) { + var b : u8 = 0; + while (b < LABEL_KINDS) { + const l = compose_label(a, b); + assert l >= a; + assert l >= b; + if (a == LABEL_UNKNOWN or b == LABEL_UNKNOWN) { + assert l == LABEL_UNKNOWN; + } + b += 1; + } + a += 1; + } + assert compose_label(LABEL_EXACT, LABEL_MISSING) == LABEL_MISSING; +} + +test r2_an_unknown_label_cannot_claim_complete_coverage { + const e = row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_UNKNOWN); + assert check_record(e) == EV_ERR_UNKNOWN_COMPLETE; + const p = row(SEAL_A, SEAL_LEN, COV_PARTIAL, LABEL_UNKNOWN); + assert check_record(p) == EV_OK; +} + +test r3_typecheck_ok_never_becomes_holds { + // The spec asserts 1 > 2: t27c's typecheck is still ok. That row may say "typechecks"; it may + // not say "holds". + const tc = row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_EXACT); + assert check_record(tc) == EV_OK; + assert strongest_claim(PR_TYPECHECKER, 0, 0) == CL_TYPECHECKS; + assert check_record(claiming(tc, CL_HOLDS, PR_TYPECHECKER, 0, 0)) == EV_ERR_OVERCLAIM; + assert check_record(claiming(tc, CL_HOLDS, PR_PARSER, 0, 0)) == EV_ERR_OVERCLAIM; + assert check_record(claiming(tc, CL_TYPECHECKS, PR_PARSER, 0, 0)) == EV_ERR_OVERCLAIM; + // Run the tests: the failing assert is a failure, so still no "holds". + assert check_record(claiming(tc, CL_HOLDS, PR_TEST_REPORT, 1, 1)) == EV_ERR_OVERCLAIM; + // A vacuous run (zero runtime asserts) proves nothing either. + assert check_record(claiming(tc, CL_HOLDS, PR_TEST_REPORT, 0, 0)) == EV_ERR_OVERCLAIM; + // Only a green, non-vacuous test-report supports it. + assert check_record(claiming(tc, CL_HOLDS, PR_TEST_REPORT, 3, 0)) == EV_OK; + // And no instrument at all supports nothing. + assert claim_supported(CL_PARSES, PR_NONE, 0, 0) == false; +} + +test r3_a_suggested_row_never_says_holds { + const s = row(SEAL_A, SEAL_LEN, COV_PARTIAL, LABEL_SUGGESTED); + assert check_record(claiming(s, CL_HOLDS, PR_TEST_REPORT, 3, 0)) == EV_ERR_SUGGESTED_HOLDS; + assert check_record(claiming(s, CL_TYPECHECKS, PR_TEST_REPORT, 3, 0)) == EV_OK; +} + +test r4_ready_and_covered_need_one_seal { + var c : Citation = no_citation(); + assert may_declare_ready(c) == false; + c = cite(c, row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_EXACT)); + c = cite(c, row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_DERIVED)); + assert comparable(c) == true; + assert may_declare_ready(c) == true; + assert may_declare_covered(c) == true; + assert c.label == LABEL_DERIVED; + // One more row measured against another seal: not comparable, nothing may be declared. + const d = cite(c, row(SEAL_B, SEAL_LEN, COV_COMPLETE, LABEL_EXACT)); + assert d.mixed == true; + assert may_declare_ready(d) == false; + assert may_declare_covered(d) == false; +} + +test r4_a_display_prefix_is_not_a_digest { + assert seal_ok(SEAL_A, SEAL_LEN) == true; + assert seal_ok(SEAL_A_SHOWN, SEAL_A_SHOWN_LEN) == false; + assert seal_ok("", 0) == false; + var c : Citation = cite(no_citation(), row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_EXACT)); + c = cite(c, row(SEAL_A_SHOWN, SEAL_A_SHOWN_LEN, COV_COMPLETE, LABEL_EXACT)); + assert c.refused == 1; + assert comparable(c) == false; + assert may_declare_ready(c) == false; +} + +test r4_covered_needs_complete_coverage_on_every_row { + var c : Citation = cite(no_citation(), row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_EXACT)); + c = cite(c, row(SEAL_A, SEAL_LEN, COV_PARTIAL, LABEL_UNKNOWN)); + assert comparable(c) == true; + assert may_declare_ready(c) == true; + assert may_declare_covered(c) == false; + // Every row unknown: comparable, but neither ready nor covered. + var u : Citation = cite(no_citation(), row(SEAL_B, SEAL_LEN, COV_UNKNOWN, LABEL_UNKNOWN)); + u = cite(u, row(SEAL_B, SEAL_LEN, COV_UNKNOWN, LABEL_DERIVED)); + assert comparable(u) == true; + assert u.coverage == COV_UNKNOWN; + assert may_declare_ready(u) == false; + assert may_declare_covered(u) == false; +} + +test r5_recheck_reads_the_digest_after_the_final_write { + // Rendered, written at event 2, read back at event 3: verified. + assert recheck(SEAL_A, SEAL_LEN, SEAL_A, SEAL_LEN, 3, 2) == PUB_VERIFIED; + // Read back at event 2, then written again at event 4: the read-back says nothing. + assert recheck(SEAL_A, SEAL_LEN, SEAL_A, SEAL_LEN, 2, 4) == PUB_UNCHECKED; + assert recheck(SEAL_A, SEAL_LEN, SEAL_A, SEAL_LEN, 4, 4) == PUB_UNCHECKED; + // The final write changed the bytes: mismatch. + assert recheck(SEAL_A, SEAL_LEN, SEAL_B, SEAL_LEN, 5, 4) == PUB_MISMATCH; + // A truncated read-back is a mismatch, not a match on the prefix. + assert recheck(SEAL_A, SEAL_LEN, SEAL_A_SHOWN, SEAL_A_SHOWN_LEN, 5, 4) == PUB_MISMATCH; + // No read-back at all, or nothing to compare with: unchecked. + assert recheck(SEAL_A, SEAL_LEN, "", 0, 5, 4) == PUB_UNCHECKED; + assert recheck("", 0, SEAL_A, SEAL_LEN, 5, 4) == PUB_UNCHECKED; +} + +test span_and_claim_text_are_required { + const e = row(SEAL_A, SEAL_LEN, COV_COMPLETE, LABEL_EXACT); + assert span_ok(e.path, e.path_len, 0, 3) == false; + assert span_ok(e.path, e.path_len, 9, 3) == false; + assert span_ok("/etc/x", 6, 1, 1) == false; + assert span_ok("", 0, 1, 1) == false; + assert span_ok(e.path, e.path_len, 7, 7) == true; + const blank = Evidence { + text: "", + text_len: 0, + claim: CL_PARSES, + proof: PR_PARSER, + asserts: 0, + fails: 0, + path: FIX_PATH, + path_len: FIX_PATH_LEN, + line_lo: 1, + line_hi: 1, + seal: SEAL_A, + seal_len: SEAL_LEN, + coverage: COV_COMPLETE, + label: LABEL_EXACT, + }; + assert check_record(blank) == EV_ERR_CLAIM_TEXT; +} diff --git a/specs/claw/evidence_pins.t27 b/specs/claw/evidence_pins.t27 new file mode 100644 index 0000000000..d4d2a72424 --- /dev/null +++ b/specs/claw/evidence_pins.t27 @@ -0,0 +1,87 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/claw/evidence_pins.t27 -- the pins for specs/claw/evidence.t27 (#10412). +; evidence.t27 carries every string length explicitly (COV_NAME_LENS, LABEL_NAME_LENS, +; SEAL_PREFIX_LEN, SEAL_LEN and the fixture lengths) because the gen-c backend lowers str to +; const char* and cannot express .len; a wrong number there would miscompare silently, since +; every lookup inside evidence.t27 reads the same wrong number. .len derives the length from the +; bytes, so the pins live here, in a test-only module that is never passed to gen-c (the +; specs/claw/gates_pins.t27 pattern). +; It also pins the four labels to the T27F graph schema, specs/t27f/spec_graph.t27: same values, +; same names, so "the same four as T27F" is checked, not asserted in prose. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module ClawEvidencePins; + +use claw::evidence; +use t27f::spec_graph::LABEL_EXACT; +use t27f::spec_graph::LABEL_DERIVED; +use t27f::spec_graph::LABEL_SUGGESTED; +use t27f::spec_graph::LABEL_UNKNOWN; +use t27f::spec_graph::LABEL_KINDS; +use t27f::spec_graph::LABEL_NAMES; + +test word_lens_pin_their_bytes { + // Loop vars, not literal indices: a literal index lets the checker fold the compare at + // compile time and the test passes with zero runtime asserts (#6509). + for k in 0..3 { + assert evidence::COV_NAME_LENS[k] == evidence::COV_NAMES[k].len; + } + for k in 0..4 { + assert evidence::LABEL_NAME_LENS[k] == evidence::LABEL_NAMES[k].len; + } +} + +test seal_lens_pin_their_bytes { + var p : str = evidence::SEAL_PREFIX; + assert evidence::SEAL_PREFIX_LEN == p.len; + var a : str = evidence::SEAL_A; + var b : str = evidence::SEAL_B; + assert evidence::SEAL_LEN == a.len; + assert evidence::SEAL_LEN == b.len; + var s : str = evidence::SEAL_A_SHOWN; + assert evidence::SEAL_A_SHOWN_LEN == s.len; + var f : str = evidence::FIX_PATH; + assert evidence::FIX_PATH_LEN == f.len; + var t : str = evidence::FIX_TEXT; + assert evidence::FIX_TEXT_LEN == t.len; +} + +test fixtures_are_what_their_names_say { + // The display prefix really is the first digest's first 12 hex digits, so r4's refusal is a + // refusal of a true prefix and not of unrelated bytes. + var a : str = evidence::SEAL_A; + var s : str = evidence::SEAL_A_SHOWN; + for i in 0..12 { + assert s[i] == a[evidence::SEAL_PREFIX_LEN + i]; + } + // And the two digests differ, so r4's mixed citation is really mixed. + assert evidence::seal_ok(a, a.len) == true; + var b : str = evidence::SEAL_B; + assert evidence::seal_ok(b, b.len) == true; + var diff : u32 = 0; + for i in 0..71 { + if (a[i] != b[i]) { diff += 1; } + } + assert diff > 0; +} + +test labels_are_the_t27f_four { + var e : u8 = evidence::LABEL_EXACT; + var d : u8 = evidence::LABEL_DERIVED; + var g : u8 = evidence::LABEL_SUGGESTED; + var u : u8 = evidence::LABEL_UNKNOWN; + var n : u8 = evidence::LABEL_KINDS; + assert e == LABEL_EXACT; + assert d == LABEL_DERIVED; + assert g == LABEL_SUGGESTED; + assert u == LABEL_UNKNOWN; + assert n == LABEL_KINDS; + for k in 0..4 { + var mine : str = evidence::LABEL_NAMES[k]; + var theirs : str = LABEL_NAMES[k]; + assert mine.len == theirs.len; + for i in 0..mine.len { + assert mine[i] == theirs[i]; + } + } +}