|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | +//! The Echidna dispatch seam. |
| 5 | +//! |
| 6 | +//! A backend's `check_file` can run one of two ways, both returning the SAME |
| 7 | +//! [`Outcome`] contract: |
| 8 | +//! * [`Dispatch::Local`] — shell out to the tool directly (the default, and |
| 9 | +//! the fully-real baseline). |
| 10 | +//! * [`Dispatch::Echidna`] — route to the Echidna multi-prover orchestrator |
| 11 | +//! (Zig-API, port 8090) which runs the check elsewhere and returns the |
| 12 | +//! verdict. |
| 13 | +//! |
| 14 | +//! **Honest-stub discipline.** Echidna's orchestrator repo/API is unconfirmed |
| 15 | +//! (it may not exist yet), and this seam explicitly *does not block on Echidna |
| 16 | +//! existing*. Rather than invent an unverifiable HTTP contract and risk |
| 17 | +//! fabricating a verdict, the Echidna route is an honest stub: it returns an |
| 18 | +//! [`Outcome`] with `available: false` / [`Verdict::Unavailable`] and a clear |
| 19 | +//! reason — never a made-up result. This mirrors the estate precedent |
| 20 | +//! (cicd-squabbler's webhook server "exits EX_UNAVAILABLE rather than fake |
| 21 | +//! OK"). Wiring the real orchestrator client (feature-gated) is the follow-on, |
| 22 | +//! gated on Echidna's confirmed API. |
| 23 | +//! |
| 24 | +//! The value delivered now is the *seam*: one indirection point where a route |
| 25 | +//! is chosen, with the `Outcome` contract preserved, so adding the real client |
| 26 | +//! later touches only [`Dispatch::run`] — no backend or caller changes. |
| 27 | +
|
| 28 | +use crate::prover::{Backend, BackendKind, Outcome, Verdict}; |
| 29 | +use anyhow::{bail, Result}; |
| 30 | +use std::path::Path; |
| 31 | + |
| 32 | +/// How a check is dispatched. |
| 33 | +pub enum Dispatch { |
| 34 | + /// Shell out to the tool locally (default; fully real). |
| 35 | + Local, |
| 36 | + /// Route to the Echidna orchestrator at `base_url` (honest stub for now). |
| 37 | + Echidna { base_url: String }, |
| 38 | +} |
| 39 | + |
| 40 | +impl Dispatch { |
| 41 | + /// The conventional Echidna orchestrator endpoint. |
| 42 | + pub const DEFAULT_ECHIDNA_URL: &'static str = "http://127.0.0.1:8090"; |
| 43 | + |
| 44 | + /// Parse a `--dispatch` value: `local` (default), `echidna`, or |
| 45 | + /// `echidna=<url>`. |
| 46 | + pub fn parse(s: &str) -> Result<Dispatch> { |
| 47 | + if let Some((head, url)) = s.split_once('=') { |
| 48 | + if head == "echidna" { |
| 49 | + return Ok(Dispatch::Echidna { |
| 50 | + base_url: url.to_string(), |
| 51 | + }); |
| 52 | + } |
| 53 | + } else if s == "echidna" { |
| 54 | + return Ok(Dispatch::Echidna { |
| 55 | + base_url: Self::DEFAULT_ECHIDNA_URL.to_string(), |
| 56 | + }); |
| 57 | + } else if s == "local" { |
| 58 | + return Ok(Dispatch::Local); |
| 59 | + } |
| 60 | + bail!("unknown --dispatch `{s}` (known: local, echidna, echidna=<url>)") |
| 61 | + } |
| 62 | + |
| 63 | + /// Run `backend`'s check via the chosen route. The `Outcome` contract is |
| 64 | + /// identical regardless of route. |
| 65 | + pub fn run(&self, backend: &dyn Backend, file: &Path, include_root: &Path) -> Result<Outcome> { |
| 66 | + match self { |
| 67 | + Dispatch::Local => backend.check_file(file, include_root), |
| 68 | + Dispatch::Echidna { base_url } => Ok(echidna_stub(backend.kind(), base_url)), |
| 69 | + } |
| 70 | + } |
| 71 | +} |
| 72 | + |
| 73 | +/// The honest Echidna stub: the seam is wired and returns the standard |
| 74 | +/// `Outcome` shape, but reports `Unavailable` with a reason instead of |
| 75 | +/// fabricating a verdict. |
| 76 | +fn echidna_stub(kind: BackendKind, base_url: &str) -> Outcome { |
| 77 | + Outcome { |
| 78 | + available: false, |
| 79 | + exit_code: None, |
| 80 | + ok: false, |
| 81 | + output_tail: format!( |
| 82 | + "echidna dispatch seam is wired ({base_url}) but the orchestrator \ |
| 83 | + client is not built in this configuration; no verdict fabricated" |
| 84 | + ), |
| 85 | + kind, |
| 86 | + verdict: Verdict::Unavailable, |
| 87 | + } |
| 88 | +} |
| 89 | + |
| 90 | +#[cfg(test)] |
| 91 | +mod tests { |
| 92 | + use super::*; |
| 93 | + use crate::prover::{Agda, Smt}; |
| 94 | + |
| 95 | + #[test] |
| 96 | + fn parse_dispatch_values() { |
| 97 | + assert!(matches!(Dispatch::parse("local").unwrap(), Dispatch::Local)); |
| 98 | + match Dispatch::parse("echidna").unwrap() { |
| 99 | + Dispatch::Echidna { base_url } => assert_eq!(base_url, Dispatch::DEFAULT_ECHIDNA_URL), |
| 100 | + _ => panic!("expected echidna"), |
| 101 | + } |
| 102 | + match Dispatch::parse("echidna=http://host:9000").unwrap() { |
| 103 | + Dispatch::Echidna { base_url } => assert_eq!(base_url, "http://host:9000"), |
| 104 | + _ => panic!("expected echidna with url"), |
| 105 | + } |
| 106 | + assert!(Dispatch::parse("nonsense").is_err()); |
| 107 | + } |
| 108 | + |
| 109 | + #[test] |
| 110 | + fn echidna_route_is_an_honest_stub_never_fabricates() { |
| 111 | + // The seam preserves the backend's kind but reports Unavailable with |
| 112 | + // a reason — it must never claim Proven/Refuted it did not obtain. |
| 113 | + let d = Dispatch::parse("echidna").unwrap(); |
| 114 | + let tmp = tempfile::tempdir().unwrap(); |
| 115 | + let f = tmp.path().join("q.smt2"); |
| 116 | + std::fs::write(&f, "(check-sat)\n").unwrap(); |
| 117 | + let out = d.run(&Smt::z3(), &f, tmp.path()).unwrap(); |
| 118 | + assert_eq!(out.verdict, Verdict::Unavailable); |
| 119 | + assert!(!out.available); |
| 120 | + assert_eq!(out.kind, BackendKind::Solver, "kind is preserved"); |
| 121 | + assert!(out.output_tail.contains("echidna")); |
| 122 | + assert!(out.output_tail.contains("no verdict fabricated")); |
| 123 | + } |
| 124 | + |
| 125 | + #[test] |
| 126 | + fn local_route_delegates_to_the_backend() { |
| 127 | + // Local dispatch is exactly backend.check_file — same honesty either |
| 128 | + // way (present ⇒ real verdict; absent ⇒ Unavailable). |
| 129 | + let d = Dispatch::Local; |
| 130 | + let tmp = tempfile::tempdir().unwrap(); |
| 131 | + let f = tmp.path().join("X.agda"); |
| 132 | + std::fs::write(&f, "module X where\n").unwrap(); |
| 133 | + let via_dispatch = d.run(&Agda, &f, tmp.path()).unwrap(); |
| 134 | + let direct = Agda.check_file(&f, tmp.path()).unwrap(); |
| 135 | + assert_eq!(via_dispatch.available, direct.available); |
| 136 | + assert_eq!(via_dispatch.verdict, direct.verdict); |
| 137 | + } |
| 138 | +} |
0 commit comments