diff --git a/specs/tools/t27o/ledger.t27 b/specs/tools/t27o/ledger.t27 new file mode 100644 index 0000000000..d05b21b29c --- /dev/null +++ b/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); +} diff --git a/specs/tools/t27o/rust_convert.t27 b/specs/tools/t27o/rust_convert.t27 index 46e6de8a35..6c9020836c 100644 --- a/specs/tools/t27o/rust_convert.t27 +++ b/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;