|
| 1 | +(* SPDX-License-Identifier: MPL-2.0 *) |
| 2 | +(* SPDX-FileCopyrightText: 2024-2026 hyperpolymath (Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>) *) |
| 3 | + |
| 4 | +(** xfail pin harness for the soundness ledger (docs/SOUNDNESS.adoc, property 5). |
| 5 | +
|
| 6 | + Each pin asserts the DESIRED behaviour of a known soundness hole. Because the |
| 7 | + hole is still present, the assertion currently FAILS — which is the expected |
| 8 | + state, reported as [XFAIL-OK]. The day the hole is fixed, the assertion |
| 9 | + PASSES, which is unexpected and reported as [XPASS]: the process exits |
| 10 | + non-zero (so [dune runtest] and the gate both go red) with a message telling |
| 11 | + the engineer to update the ledger row rather than silence the pin. |
| 12 | +
|
| 13 | + Polarity / fail-closed contract: |
| 14 | + - pin body raises [Xfail] when the desired behaviour is NOT met (hole |
| 15 | + present) -> XFAIL-OK (exit 0 contribution) |
| 16 | + - pin body returns normally (desired behaviour met, hole gone) |
| 17 | + -> XPASS (exit 1) |
| 18 | + - pin body raises ANY OTHER exception (parse error, missing fixture, …) |
| 19 | + -> XERROR (exit 1) — pin infrastructure is broken, |
| 20 | + so we fail closed rather than mistake it for an |
| 21 | + expected failure. |
| 22 | +
|
| 23 | + The shell gate (tools/check-soundness-ledger.sh, property 5) runs this |
| 24 | + executable, asserts every pin named by a `residual (pinned)` / `open |
| 25 | + (tracked)` ledger row reports XFAIL-OK, and surfaces XPASS as the distinct |
| 26 | + "is the hole fixed?" alarm. *) |
| 27 | + |
| 28 | +open Affinescript |
| 29 | + |
| 30 | +exception Xfail of string |
| 31 | + |
| 32 | +(* Locate test/e2e/fixtures across the run contexts we care about: |
| 33 | + AFFINE_FIXTURES override (the gate sets this), the dune-test sandbox |
| 34 | + (cwd = _build/default/test/xfail, fixtures at ../e2e/fixtures via the |
| 35 | + source_tree dep), cwd = test/, and cwd = repo root. Fail closed if none. *) |
| 36 | +let fixtures_dir = |
| 37 | + let cands = |
| 38 | + (match Sys.getenv_opt "AFFINE_FIXTURES" with Some d -> [ d ] | None -> []) |
| 39 | + @ [ "../e2e/fixtures"; "e2e/fixtures"; "test/e2e/fixtures" ] |
| 40 | + in |
| 41 | + match List.find_opt Sys.file_exists cands with |
| 42 | + | Some d -> d |
| 43 | + | None -> |
| 44 | + failwith |
| 45 | + "xfail: cannot locate test/e2e/fixtures (set AFFINE_FIXTURES to its path)" |
| 46 | + |
| 47 | +let fixture name = Filename.concat fixtures_dir name |
| 48 | + |
| 49 | +let parse path = |
| 50 | + try Parse_driver.parse_file path |
| 51 | + with e -> failwith ("parse " ^ path ^ ": " ^ Printexc.to_string e) |
| 52 | + |
| 53 | +let resolve_symbols prog = |
| 54 | + let loader = Module_loader.create (Module_loader.default_config ()) in |
| 55 | + match Resolve.resolve_program_with_loader prog loader with |
| 56 | + | Ok (rctx, _) -> rctx.symbols |
| 57 | + | Error (e, _) -> failwith ("resolve: " ^ Resolve.show_resolve_error e) |
| 58 | + |
| 59 | +(* ---- Pin: #555 / #623 — interpreter non-tail single-shot resume ---------- |
| 60 | + `let x = op(); x + 100` with `op() => resume(5)` should yield 105 once the |
| 61 | + continuation is reified; the shallow tree-walking interpreter yields 5. *) |
| 62 | +let test_resume_nontail_xfail () = |
| 63 | + let path = fixture "handle_resume_nontail.affine" in |
| 64 | + let prog = parse path in |
| 65 | + let _ = resolve_symbols prog in |
| 66 | + let v = |
| 67 | + match Interp.eval_program prog with |
| 68 | + | Error e -> failwith ("eval: " ^ Value.show_eval_error e) |
| 69 | + | Ok env -> ( |
| 70 | + match Value.lookup_env "main" env with |
| 71 | + | Error _ -> failwith "no `main` binding" |
| 72 | + | Ok f -> ( |
| 73 | + match Interp.apply_function f [] with |
| 74 | + | Ok v -> v |
| 75 | + | Error e -> failwith ("apply main: " ^ Value.show_eval_error e))) |
| 76 | + in |
| 77 | + match v with |
| 78 | + | Value.VInt 105 -> () (* desired met -> XPASS: the hole is fixed *) |
| 79 | + | Value.VInt 5 -> |
| 80 | + raise (Xfail "non-tail resume returns 5, not 105 (shallow continuation)") |
| 81 | + | other -> |
| 82 | + raise |
| 83 | + (Xfail ("non-tail resume returned " ^ Value.show_value other ^ ", not 105")) |
| 84 | + |
| 85 | +(* ---- Pin: #555-stub / #624 — Lean backend drops `return` ------------------ |
| 86 | + The agreed remedy (#624) is to fail loud on early `return`; today |
| 87 | + `codegen_lean` returns Ok and silently lowers the body to `:= ()`. *) |
| 88 | +let test_stub_backend_return_xfail () = |
| 89 | + let path = fixture "stub_backend_return_dropped.affine" in |
| 90 | + let prog = parse path in |
| 91 | + let symbols = resolve_symbols prog in |
| 92 | + match Lean_codegen.codegen_lean prog symbols with |
| 93 | + | Error _ -> () (* desired met -> XPASS: the backend now fails loud *) |
| 94 | + | Ok _ -> |
| 95 | + raise |
| 96 | + (Xfail |
| 97 | + "Lean_codegen.codegen_lean returned Ok; early `return` silently dropped") |
| 98 | + |
| 99 | +let pins = |
| 100 | + [ ("test_resume_nontail_xfail", |
| 101 | + "#555/#623 interp non-tail resume -> 5 not 105", test_resume_nontail_xfail); |
| 102 | + ("test_stub_backend_return_xfail", |
| 103 | + "#555-stub/#624 Lean drops `return`", test_stub_backend_return_xfail) ] |
| 104 | + |
| 105 | +let () = |
| 106 | + let bad = ref false in |
| 107 | + List.iter |
| 108 | + (fun (name, reason, body) -> |
| 109 | + match try `Ok (body ()) with Xfail m -> `Xfail m | e -> `Err (Printexc.to_string e) with |
| 110 | + | `Xfail _ -> Printf.printf "XFAIL-OK %s -- %s\n" name reason |
| 111 | + | `Ok () -> |
| 112 | + bad := true; |
| 113 | + Printf.printf |
| 114 | + "XPASS %s -- pin passed; is the hole fixed? update docs/SOUNDNESS.adoc\n" |
| 115 | + name |
| 116 | + | `Err m -> |
| 117 | + bad := true; |
| 118 | + Printf.printf "XERROR %s -- pin infrastructure failed: %s\n" name m) |
| 119 | + pins; |
| 120 | + flush stdout; |
| 121 | + if !bad then exit 1 else exit 0 |
0 commit comments