t27o --check: t27b test judges first, t27c test-report only when t27b cannot (Closes #10525)

.trinity/seals/t27o_T27oLedger.json

@@ -1,24 +1,24 @@
 {
-  "built_by": "t27c-bootstrap@0.5.2+093bf4713",
+  "built_by": "t27c-bootstrap@0.5.2+9b556b7c3",
   "closure": [],
   "config": "gen=c,rust,verilog,zig;tests=zig",
-  "gen_hash_c": "sha256:e24216fdc74a9ce89cb28c14fa766d9053a8fa54f1875cd2453984c1c8bfbe1a",
-  "gen_hash_rust": "sha256:bdf7c3c46c68575b0dbe0946a236e02c4095dd0e74fdb5dfe7b71739122ec8b8",
-  "gen_hash_verilog": "sha256:11047a099497f53c3587106bdfbf5a745c59e2cad3126caa56452c2b7ccfe6d9",
-  "gen_hash_zig": "sha256:1b0a6e1521bc2127376ec5dcf5fee6532112d8e59f4ee2fd7c16d759f40e4782",
+  "gen_hash_c": "sha256:7718109194bbe93a643a14dc387c9a9ea965f5762a1a61273fb9e25f5a598488",
+  "gen_hash_rust": "sha256:c1b340dbe2e18469610447bce3edc48acde9c30b06544ad97038b5ddeb436793",
+  "gen_hash_verilog": "sha256:4463b9a8fcef3622b4e17271e74d188615cde707c432fa11efbcacfcce5612ae",
+  "gen_hash_zig": "sha256:edb095d112d0f61f6ab296e112409cab0fc978dc21acd18eeca6e7a3fc70d00f",
   "module": "T27oLedger",
   "ring": 12,
   "seal_schema": 2,
-  "sealed_at": "2026-10-18T09:33:11Z",
+  "sealed_at": "2026-10-18T16:37:38Z",
   "sealed_by": "t27c-bootstrap@0.5.2",
-  "spec_hash": "sha256:b2805052339f7f99f1d57e43444dd23ab2e006479fde6376245cba2b5690f66b",
+  "spec_hash": "sha256:03a101483be4dbd1be9f5e1dde9681ab01c513256138a0de37241b58db6b32d4",
   "spec_path": "specs/tools/t27o/ledger.t27",
   "tests": {
     "failed": 0,
     "failing": [],
     "forced": false,
-    "passed": 10,
-    "total": 10,
+    "passed": 12,
+    "total": 12,
     "vacuous": 0
   },
   "toolchain": {

cli/tri/src/fpga.rs

@@ -2890,13 +2890,6 @@ fn extract_source_from_lean(text: &str) -> Option<String> {
     None
 }
 
-/// Combined dashboard gate: the OSCFSEL selection is within the documented 0..7
-/// range and the PVT context is inside the operating envelope. Mirrors
-/// `cclk_variant_and_xadc_envelope_check` in Lean 4.
-fn cclk_variant_and_xadc_envelope_check(oscfsel: u8, ctx: &PvtContext) -> bool {
-    oscfsel <= 7 && pvt_context_inside_envelope(ctx)
-}
-
 /// Structs used to persist and report a single cold-POR sweep attempt.
 #[derive(serde::Serialize, serde::Deserialize)]
 struct SweepLog {

cli/tri/src/main.rs

@@ -54,6 +54,8 @@ mod gen_cache; // the gen-hash cache's eviction limit, for `tri hot caches` (#89
 mod bit_cache; // the bitstream cache's eviction limit, for `tri hot caches` (#8952)
 #[path = "../../../gen/rust/tri/hot/hot.rs"] #[allow(dead_code, unused_parens)]
 mod hot; // t27c gen-rust of specs/tri/hot/hot.t27 (#8870): every rule of `tri hot`
+#[path = "../../../gen/rust/tools/t27o/ledger.rs"] #[allow(dead_code, unused_parens, clippy::all)]
+mod t27o_ledger; // t27c gen-rust of specs/tools/t27o/ledger.t27: which runner's exit code is a verdict for `tri t27o --check` (#10525)
 #[path = "../../../gen/rust/tri/lanes/lanes.rs"] #[allow(dead_code, unused_parens)]
 mod lanes; // t27c gen-rust of specs/tri/lanes/lanes.t27: every rule of `tri lanes`
 #[path = "../../../gen/rust/tools/t27o/rust_convert.rs"] #[allow(dead_code, unused_parens, unused_mut, unused_variables, non_snake_case, unused_assignments, clippy::all)]
@@ -430,6 +432,7 @@ enum Commands {
         /// The module name; default the file's stem.
         #[arg(long)] name: Option<String>,
         #[arg(long)] oracle: bool,
+        /// Run the oracle and test the spec: `t27b test` judges, `t27c test-report` only when t27b cannot (specs/tools/t27o/ledger.t27).
         #[arg(long)] check: bool,
         /// The t27c binary; default target/release/t27c, then t27c on PATH.
         #[arg(long)] t27c: Option<String>,
@@ -1349,6 +1352,9 @@ fn cmd_t27o(file: &str, name: Option<&str>, oracle: bool, check: bool, t27c: Opt
     fs::create_dir_all("specs/t27o_check")?;
     fs::write(&path, [&spec[..m.min(spec.len())], &Command::new(&exe).output()?.stdout[..]].concat())?;
     println!("{}", path.display());
+    let b = ["target/release/t27b", "target/debug/t27b"].into_iter().find(|p| Path::new(p).exists()).unwrap_or("t27b"); // t27b judges first, t27c only when its exit is no verdict (specs/tools/t27o/ledger.t27, #10525)
+    let c = Command::new(b).arg("test").arg(&path).status().ok().and_then(|s| s.code()).unwrap_or(-1);
+    if !t27o_ledger::needs_reference(t27o_ledger::t27b_outcome(c)) { return Ok(c as u8); } eprintln!("t27o: {b} test exited {c} ({}), so t27c test-report judges instead", t27o_ledger::ORC_NAMES[t27o_ledger::t27b_outcome(c) as usize]);
     Ok(Command::new(mutate::resolve_t27c(t27c)).arg("test-report").arg(&path).status()?.code().unwrap_or(1) as u8)
 }
 

gen/rust/tools/t27o/ledger.rs

@@ -0,0 +1,218 @@
+// Generated from .t27 spec
+// DO NOT EDIT — generated by t27c
+// NOT LOWERED BY THIS BACKEND: 12 test(s), 0 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.
+
+pub const ORC_PASS: u32 = 0;
+
+pub const ORC_FAIL: u32 = 1;
+
+pub const ORC_UNKNOWN: u32 = 2;
+
+pub const ORC_UNSUPPORTED: u32 = 3;
+
+pub const ORC_TRUNCATED: u32 = 4;
+
+pub const ORC_SKIPPED: u32 = 5;
+
+pub const ORC_NAMES: [&'static str; 6] = ["pass", "fail", "unknown", "unsupported", "truncated", "skipped"];
+
+pub const PROOF_NONE: u32 = 0;
+
+pub const PROOF_REUSE: u32 = 1;
+
+pub const PROOF_TEST: u32 = 2;
+
+pub const PROOF_ORACLE: u32 = 3;
+
+pub const FN_OUT_OF_SCOPE: u32 = 0;
+
+pub const FN_BLOCKED: u32 = 1;
+
+pub const FN_CONTRADICTED: u32 = 2;
+
+pub const FN_UNKNOWN: u32 = 3;
+
+pub const FN_UNOWNED: u32 = 4;
+
+pub const FN_IMPLEMENTED: u32 = 5;
+
+pub const FN_VERIFIED: u32 = 6;
+
+pub const FN_NAMES: [&'static str; 7] = ["out of scope: a #[cfg] variant that is off on the default host", "blocked: the converter refused the body", "contradicted: an oracle sample or a translated test disagreed", "unknown: the oracle run was truncated or could not decide", "unowned: kept as a stub, there is no body to check", "implemented: converted, but no proof as strong as required", "verified: converted, with a proof as strong as required"];
+
+pub const L_READY: u32 = 0;
+
+pub const L_OPEN: u32 = 1;
+
+pub const L_FAILED: u32 = 2;
+
+pub const L_UNKNOWN: u32 = 3;
+
+pub const L_NAMES: [&'static str; 4] = ["ready", "open", "failed", "unknown"];
+
+pub const CONVERTER_VERSION: u32 = 1;
+
+pub const STD_TABLE_VERSION: u32 = 1;
+
+pub const K_FRESH: u32 = 0;
+
+pub const K_NONE: u32 = 1;
+
+pub const K_STALE_SOURCE: u32 = 2;
+
+pub const K_STALE_CONVERTER: u32 = 3;
+
+pub const K_STALE_STD: u32 = 4;
+
+pub const T27B_PASS: i32 = 0;
+
+pub const T27B_FAIL: i32 = 1;
+
+pub const T27B_UNSUPPORTED: i32 = 2;
+
+pub const T27B_FRONT_END: i32 = 3;
+
+pub const T27B_DISAGREE: i32 = 4;
+
+pub const T27B_CODEGEN_LIMIT: i32 = 5;
+
+pub fn t27b_outcome(code: i32) -> u32 {
+    if (code == T27B_PASS) {
+        return ORC_PASS;
+    }
+    if (code == T27B_FAIL) {
+        return ORC_FAIL;
+    }
+    if (code == T27B_UNSUPPORTED) {
+        return ORC_UNSUPPORTED;
+    }
+    if (code == T27B_CODEGEN_LIMIT) {
+        return ORC_UNSUPPORTED;
+    }
+    return ORC_UNKNOWN;
+}
+
+pub fn needs_reference(outcome: u32) -> bool {
+    if (outcome == ORC_PASS) {
+        return false;
+    }
+    if (outcome == ORC_FAIL) {
+        return false;
+    }
+    return true;
+}
+
+pub fn oracle_outcome(supported: bool, sampled: u32, agreed: u32, disagreed: u32, dropped: u32) -> u32 {
+    if (supported == false) {
+        return ORC_UNSUPPORTED;
+    }
+    if (disagreed > 0) {
+        return ORC_FAIL;
+    }
+    if (sampled == 0) {
+        return ORC_SKIPPED;
+    }
+    if (dropped > 0) {
+        return ORC_TRUNCATED;
+    }
+    if (((agreed + disagreed) + dropped) != sampled) {
+        return ORC_UNKNOWN;
+    }
+    if (agreed == 0) {
+        return ORC_UNKNOWN;
+    }
+    return ORC_PASS;
+}
+
+pub fn proof_of(oracle: u32, tests_recorded: u32, tests_passed: u32, reused: bool) -> u32 {
+    if (oracle == ORC_PASS) {
+        return PROOF_ORACLE;
+    }
+    if (tests_recorded > 0) {
+        if (tests_passed == tests_recorded) {
+            return PROOF_TEST;
+        }
+    }
+    if reused {
+        return PROOF_REUSE;
+    }
+    return PROOF_NONE;
+}
+
+pub fn proof_satisfies(actual: u32, required: u32) -> bool {
+    return (actual >= required);
+}
+
+pub fn fn_status(cfg_off: bool, refused: bool, stub: bool, oracle: u32, tests_recorded: u32, tests_passed: u32, reused: bool, needs_oracle: bool) -> u32 {
+    if cfg_off {
+        return FN_OUT_OF_SCOPE;
+    }
+    if refused {
+        return FN_BLOCKED;
+    }
+    if (oracle == ORC_FAIL) {
+        return FN_CONTRADICTED;
+    }
+    if (tests_passed < tests_recorded) {
+        return FN_CONTRADICTED;
+    }
+    if (oracle == ORC_TRUNCATED) {
+        return FN_UNKNOWN;
+    }
+    if (oracle == ORC_UNKNOWN) {
+        return FN_UNKNOWN;
+    }
+    if stub {
+        return FN_UNOWNED;
+    }
+    let mut required: u32 = PROOF_TEST;
+    if needs_oracle {
+        required = PROOF_ORACLE;
+    }
+    if proof_satisfies(proof_of(oracle, tests_recorded, tests_passed, reused), required) {
+        return FN_VERIFIED;
+    }
+    return FN_IMPLEMENTED;
+}
+
+pub fn summary_adds_up(total: u32, out_of_scope: u32, blocked: u32, contradicted: u32, unknown: u32, unowned: u32, implemented: u32, verified: u32) -> bool {
+    return (((((((out_of_scope + blocked) + contradicted) + unknown) + unowned) + implemented) + verified) == total);
+}
+
+pub fn ledger_status(total: u32, out_of_scope: u32, blocked: u32, contradicted: u32, unknown: u32, unowned: u32, implemented: u32, verified: u32) -> u32 {
+    if (summary_adds_up(total, out_of_scope, blocked, contradicted, unknown, unowned, implemented, verified) == false) {
+        return L_UNKNOWN;
+    }
+    if (total == out_of_scope) {
+        return L_UNKNOWN;
+    }
+    if (contradicted > 0) {
+        return L_FAILED;
+    }
+    if (unknown > 0) {
+        return L_UNKNOWN;
+    }
+    if (verified == (total - out_of_scope)) {
+        return L_READY;
+    }
+    return L_OPEN;
+}
+
+pub fn key_state(recorded: bool, same_source: bool, converter_version: u32, std_table_version: u32) -> u32 {
+    if (recorded == false) {
+        return K_NONE;
+    }
+    if (same_source == false) {
+        return K_STALE_SOURCE;
+    }
+    if (converter_version != CONVERTER_VERSION) {
+        return K_STALE_CONVERTER;
+    }
+    if (std_table_version != STD_TABLE_VERSION) {
+        return K_STALE_STD;
+    }
+    return K_FRESH;
+}
+

specs/tools/t27o/ledger.t27

@@ -83,8 +83,41 @@ pub const K_STALE_SOURCE : u32 = 2;
 pub const K_STALE_CONVERTER : u32 = 3;
 pub const K_STALE_STD : u32 = 4;
 
+; --- Which runner judges a converted spec (#10525). -------------------------------------------
+; `tri t27o --check` runs `t27b test` (t27b's native JIT) on the spec it wrote, and `t27c
+; test-report` (the reference, through Zig) only when t27b's run decided nothing. On rust_std.t27
+; the two gave the same 10/10 verdict in 0.89 s and 94 s (2026-10-18, the loaded bench Mac). Only
+; exit 0 (every test passed) and 1 (a test failed) are a verdict on the converted code; the other
+; codes are cli/t27b/README.md's "Exit codes" table, and each says t27b could not judge the spec.
+
+pub const T27B_PASS : i32 = 0;
+pub const T27B_FAIL : i32 = 1;
+pub const T27B_UNSUPPORTED : i32 = 2;
+pub const T27B_FRONT_END : i32 = 3;
+pub const T27B_DISAGREE : i32 = 4;
+pub const T27B_CODEGEN_LIMIT : i32 = 5;
+
 ; --- Decisions -------------------------------------------------------------------------------
 
+; The oracle outcome of one `t27b test` run of a converted spec, from its exit code. A construct
+; t27b lacks or a frame it cannot lay out is unsupported; a front-end error, a JIT that disagrees
+; with t27b's own interpreter, and any code outside the table (usage, I/O, a signal) are unknown.
+; Neither is ever a pass.
+pub fn t27b_outcome(code: i32) -> u32 {
+    if (code == T27B_PASS) { return ORC_PASS; }
+    if (code == T27B_FAIL) { return ORC_FAIL; }
+    if (code == T27B_UNSUPPORTED) { return ORC_UNSUPPORTED; }
+    if (code == T27B_CODEGEN_LIMIT) { return ORC_UNSUPPORTED; }
+    return ORC_UNKNOWN;
+}
+
+; Must t27c test-report run after t27b? Only when t27b's run is not a verdict.
+pub fn needs_reference(outcome: u32) -> bool {
+    if (outcome == ORC_PASS) { return false; }
+    if (outcome == ORC_FAIL) { return false; }
+    return true;
+}
+
 ; One oracle run of one function. sampled inputs were drawn; agreed and disagreed are the samples
 ; compared; dropped are the samples the harness could not compare (panic, non-finite float,
 ; unprintable string). A disagreement stands even in a truncated run.
@@ -227,3 +260,27 @@ test a_recorded_verdict_goes_stale_when_any_part_of_its_key_changes {
     assert(key_state(true, true, CONVERTER_VERSION + 1, STD_TABLE_VERSION) == K_STALE_CONVERTER);
     assert(key_state(true, true, CONVERTER_VERSION, STD_TABLE_VERSION + 1) == K_STALE_STD);
 }
+
+test only_t27b_pass_and_fail_are_verdicts_every_other_code_falls_back_to_t27c {
+    assert(t27b_outcome(T27B_PASS) == ORC_PASS);
+    assert(t27b_outcome(T27B_FAIL) == ORC_FAIL);
+    assert(t27b_outcome(T27B_UNSUPPORTED) == ORC_UNSUPPORTED);
+    assert(t27b_outcome(T27B_CODEGEN_LIMIT) == ORC_UNSUPPORTED);
+    assert(t27b_outcome(T27B_FRONT_END) == ORC_UNKNOWN);
+    assert(t27b_outcome(T27B_DISAGREE) == ORC_UNKNOWN);
+    assert(needs_reference(t27b_outcome(T27B_PASS)) == false);
+    assert(needs_reference(t27b_outcome(T27B_FAIL)) == false);
+    assert(needs_reference(t27b_outcome(T27B_UNSUPPORTED)));
+    assert(needs_reference(t27b_outcome(T27B_FRONT_END)));
+    assert(needs_reference(t27b_outcome(T27B_DISAGREE)));
+    assert(needs_reference(t27b_outcome(T27B_CODEGEN_LIMIT)));
+}
+
+test negative_control_a_code_outside_t27b_table_is_unknown_never_a_pass {
+    assert(t27b_outcome(64) == ORC_UNKNOWN);
+    assert(t27b_outcome(74) == ORC_UNKNOWN);
+    assert(t27b_outcome(133) == ORC_UNKNOWN);
+    assert(t27b_outcome(0 - 1) == ORC_UNKNOWN);
+    assert(needs_reference(t27b_outcome(0 - 1)));
+    assert(ORC_NAMES[t27b_outcome(T27B_DISAGREE)] == "unknown");
+}