feat(t27o): obligation ledger -- per-fn status, oracle outcomes, proof strength, stale keys; no fn is unknown coverage

specs/tools/t27o/ledger.t27

@@ -0,0 +1,229 @@
+// SPDX-License-Identifier: Apache-2.0
+; specs/tools/t27o/ledger.t27 -- the obligation ledger of a t27o conversion: one status per converted
+; function, one outcome per oracle run, one verdict per file, and the key that says when a recorded
+; verdict is stale. golden.t27 decides whether a whole spec is golden; this spec decides what each
+; function's evidence is worth before golden.t27 counts it.
+; --
+; The patterns come from REA (morluto/rea b83b9ca, read as a reference, not linked):
+;   - an empty set of obligations is unknown, never ready (src/domain/
+;     reconstructionObligationLedgerIntegrity.ts:62). t27o printed "coverage 100%" for a file
+;     with no fn at all; rust_convert.t27 put_report now prints unknown there and points here;
+;   - one status per function by a fixed precedence: out of scope, blocked, contradicted,
+;     unknown, unowned, then implemented or verified (ReconstructionObligationLedgerEvaluation.ts:452);
+;   - oracle outcomes pass, fail, unknown, unsupported, truncated, skipped, and only pass counts
+;     (docs/reconstruction-readiness.md:47). The t27o harness drops a sample on a panic, a
+;     non-finite float or an unprintable string without counting it; a dropped sample makes the
+;     run truncated, not passed;
+;   - a weaker proof never closes a stronger requirement (ReconstructionObligationAuthority.ts:15):
+;     a translated test does not stand in for the oracle where the oracle is required;
+;   - a recorded verdict is keyed by the source digest, the converter version and the std table
+;     version; a change of any one makes it stale (reconstructionCoverage.ts:101).
+; --
+; Unknown is not absent: every function below that lacks the facts to decide returns an UNKNOWN
+; value with its own name, and no UNKNOWN is ever counted as verified or ready.
+; ASCII only (L3)
+; phi^2 + 1/phi^2 = 3 | TRINITY
+
+module T27oLedger;
+
+; --- Oracle outcomes. Only ORC_PASS counts as evidence. ----------------------------------------
+
+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 : [6]str = ["pass", "fail", "unknown", "unsupported", "truncated", "skipped"];
+
+; --- Proof strength, weakest first. A proof satisfies a requirement of equal or lower strength. --
+
+pub const PROOF_NONE : u32 = 0;
+; The body was replaced by an existing t27 fn with the same input and output contract (#8963).
+pub const PROOF_REUSE : u32 = 1;
+; A translated #[test] passed against the converted body.
+pub const PROOF_TEST : u32 = 2;
+; Every sample the oracle (the original compiled by rustc) produced agreed with the converted body.
+pub const PROOF_ORACLE : u32 = 3;
+
+; --- Function status, in the order of precedence fn_status() applies. -------------------------
+
+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 : [7]str = [
+    "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",
+];
+
+; --- Ledger verdict of one converted file. ---------------------------------------------------
+
+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 : [4]str = ["ready", "open", "failed", "unknown"];
+
+; --- Recorded-verdict key. Bump a version whenever its table or its rules change. -------------
+
+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;
+
+; --- Decisions -------------------------------------------------------------------------------
+
+; 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.
+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;
+}
+
+; The strongest proof a function holds.
+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;
+}
+
+; The status of one function, by the fixed precedence. needs_oracle is true where a translated
+; test is not enough, for example a fn with a float result.
+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; }
+    var 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;
+}
+
+; The counts a report prints must add up to the functions seen; a report whose parts do not add up
+; is refused, not repaired.
+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;
+}
+
+; The verdict of a file from its status counts. No in-scope function is unknown, never ready.
+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;
+}
+
+; Whether a recorded verdict still holds. same_source is the caller's comparison of the full source
+; digests; a truncated digest is not a digest and must be passed as recorded == false.
+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;
+}
+
+; --- Tests ----------------------------------------------------------------------------------
+
+test an_oracle_run_passes_only_when_every_sample_agreed {
+    assert(oracle_outcome(true, 64, 64, 0, 0) == ORC_PASS);
+    assert(oracle_outcome(true, 64, 63, 1, 0) == ORC_FAIL);
+    assert(ORC_NAMES[ORC_PASS] == "pass");
+}
+
+test a_dropped_sample_truncates_the_run_and_a_disagreement_still_fails_it {
+    assert(oracle_outcome(true, 64, 60, 0, 4) == ORC_TRUNCATED);
+    assert(oracle_outcome(true, 64, 59, 1, 4) == ORC_FAIL);
+}
+
+test negative_control_nothing_sampled_or_nothing_compared_is_not_a_pass {
+    assert(oracle_outcome(true, 0, 0, 0, 0) == ORC_SKIPPED);
+    assert(oracle_outcome(false, 64, 64, 0, 0) == ORC_UNSUPPORTED);
+    assert(oracle_outcome(true, 64, 10, 0, 0) == ORC_UNKNOWN);
+    assert(oracle_outcome(true, 64, 0, 0, 0) == ORC_UNKNOWN);
+}
+
+test a_weaker_proof_never_closes_a_stronger_requirement {
+    assert(proof_satisfies(PROOF_ORACLE, PROOF_TEST));
+    assert(proof_satisfies(PROOF_TEST, PROOF_ORACLE) == false);
+    assert(proof_satisfies(PROOF_REUSE, PROOF_TEST) == false);
+    assert(proof_of(ORC_SKIPPED, 3, 2, true) == PROOF_REUSE);
+}
+
+test fn_status_follows_the_precedence {
+    assert(fn_status(true, true, true, ORC_FAIL, 1, 0, false, false) == FN_OUT_OF_SCOPE);
+    assert(fn_status(false, true, true, ORC_FAIL, 1, 0, false, false) == FN_BLOCKED);
+    assert(fn_status(false, false, true, ORC_FAIL, 0, 0, false, false) == FN_CONTRADICTED);
+    assert(fn_status(false, false, false, ORC_PASS, 2, 1, false, false) == FN_CONTRADICTED);
+    assert(fn_status(false, false, true, ORC_TRUNCATED, 0, 0, false, false) == FN_UNKNOWN);
+    assert(fn_status(false, false, true, ORC_SKIPPED, 0, 0, false, false) == FN_UNOWNED);
+}
+
+test a_float_fn_with_only_translated_tests_is_implemented_not_verified {
+    assert(fn_status(false, false, false, ORC_SKIPPED, 2, 2, false, true) == FN_IMPLEMENTED);
+    assert(fn_status(false, false, false, ORC_PASS, 2, 2, false, true) == FN_VERIFIED);
+    assert(fn_status(false, false, false, ORC_SKIPPED, 2, 2, false, false) == FN_VERIFIED);
+    assert(fn_status(false, false, false, ORC_SKIPPED, 0, 0, true, false) == FN_IMPLEMENTED);
+    assert(FN_NAMES[FN_IMPLEMENTED] == "implemented: converted, but no proof as strong as required");
+}
+
+test negative_control_a_file_with_no_in_scope_fn_is_unknown_not_ready {
+    assert(ledger_status(0, 0, 0, 0, 0, 0, 0, 0) == L_UNKNOWN);
+    assert(ledger_status(3, 3, 0, 0, 0, 0, 0, 0) == L_UNKNOWN);
+    assert(L_NAMES[L_UNKNOWN] == "unknown");
+}
+
+test the_ledger_verdict_fails_on_a_contradiction_and_is_ready_only_when_all_are_verified {
+    assert(ledger_status(5, 1, 0, 0, 0, 0, 0, 4) == L_READY);
+    assert(ledger_status(5, 0, 1, 0, 0, 0, 0, 4) == L_OPEN);
+    assert(ledger_status(5, 0, 1, 1, 0, 0, 0, 3) == L_FAILED);
+    assert(ledger_status(5, 0, 0, 0, 1, 0, 0, 4) == L_UNKNOWN);
+}
+
+test a_summary_that_does_not_add_up_is_refused {
+    assert(summary_adds_up(5, 1, 0, 0, 0, 0, 0, 4));
+    assert(summary_adds_up(5, 1, 0, 0, 0, 0, 0, 5) == false);
+    assert(ledger_status(5, 1, 0, 0, 0, 0, 0, 5) == L_UNKNOWN);
+}
+
+test a_recorded_verdict_goes_stale_when_any_part_of_its_key_changes {
+    assert(key_state(true, true, CONVERTER_VERSION, STD_TABLE_VERSION) == K_FRESH);
+    assert(key_state(false, true, CONVERTER_VERSION, STD_TABLE_VERSION) == K_NONE);
+    assert(key_state(true, false, CONVERTER_VERSION, STD_TABLE_VERSION) == K_STALE_SOURCE);
+    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);
+}

specs/tools/t27o/rust_convert.t27

@@ -7353,8 +7353,13 @@ pub fn put_report(st: []usize, out: []u8) -> void {
         put_num(st, out, st[NCFG]);
         puts(st, out, " cfg-off fn dropped; ");
     }
+    // No fn seen is unknown, never 100%: an empty set of obligations proves nothing (ledger.t27).
+    if (st[NFN] == 0) {
+        puts(st, out, "coverage unknown: no fn seen\n");
+        return;
+    }
     puts(st, out, "coverage ");
-    if (st[NFN] == 0) { puts(st, out, "100"); } else { put_num(st, out, st[NOK] * 100 / st[NFN]); }
+    put_num(st, out, st[NOK] * 100 / st[NFN]);
     puts(st, out, "%\n");
 }
 
@@ -7651,6 +7656,16 @@ test the_whole_file_has_a_header_and_a_report {
     assert(out_is(n, &out, 0, "// SPDX-License-Identifier: Apache-2.0\n; Demo.t27 -- converted from Rust by t27o (Ouroboros), specs/tools/t27o/rust_convert.t27; read it before it lands.\n; ASCII only (L3)\n\nmodule Demo;\n\n/// One.\nconst ONE : u64 = 1000;\n\nfn neg(x: i32) -> i32 {\n    return -x;\n}\n\n// t27o: refused fn bad (line 4): macro `vec` at line 4\n\nfn bad() -> void {\n}\n\n// t27o: 2 fn seen, 1 converted (0 of 0 tests), 1 refused (1 kept as stubs); coverage 50%\n"));
 }
 
+test negative_control_a_file_with_no_fn_reports_unknown_coverage_not_100 {
+    var out : [1024]u8 = undefined;
+    var st : [1024]usize = [0] ** 1024;
+    const n : usize = convert("/// One.\nconst ONE: u64 = 1_000;", "Demo", &out, &st);
+    const tail : []const u8 = "// t27o: 0 fn seen, 0 converted (0 of 0 tests), 0 refused (0 kept as stubs); coverage unknown: no fn seen\n";
+    assert(n > tail.len);
+    assert(out_is(n, &out, n - tail.len, tail));
+    assert(st[NFN] == 0);
+}
+
 test the_output_size_is_counted_past_a_small_buffer {
     var out : [8]u8 = undefined;
     var st : [1024]usize = [0] ** 1024;