logicaffeine_tv/
verdict.rs

1//! Result types for the translation validator.
2
3use logicaffeine_compile::ParseError;
4
5/// Why building a symbolic summary failed.
6#[derive(Debug)]
7pub enum TvError {
8    /// The source did not parse.
9    Parse(ParseError),
10    /// The program uses a construct outside the supported Verifiable Core.
11    Unsupported(String),
12}
13
14/// Outcome of cross-validating the LOGOS encoder against the tree-walking interpreter
15/// on one program (the meta-soundness check, `work/PE_IMPROVE.md §4.2`).
16#[derive(Debug, Clone, PartialEq, Eq)]
17pub enum SoundnessReport {
18    /// The encoder's symbolic summary provably matches the interpreter's observable
19    /// behavior (outputs and error/no-error).
20    Agrees,
21    /// The encoder and interpreter disagree — an encoder bug (or a genuine miscompile,
22    /// if the encoder is trusted). The detail localizes the divergence.
23    Disagrees {
24        /// Human-readable description of the divergence.
25        detail: String,
26    },
27    /// The program is outside the Verifiable Core, so the encoder did not model it.
28    /// Soundly excluded from the check — never reported as agreement.
29    Unsupported {
30        /// Which construct fell outside the fragment.
31        reason: String,
32    },
33    /// The source failed to parse (should not occur for well-formed corpus programs).
34    ParseFailed {
35        /// Parser diagnostic.
36        detail: String,
37    },
38    /// A nondeterministic program: for every seed in the sweep, the seeded encoder provably
39    /// matched the seeded interpreter (`Select` winners drawn from the same SplitMix64).
40    /// This is the seeded-replay analog of [`Self::Agrees`].
41    SeedReplayAgrees,
42    /// A nondeterministic program where the seeded encoder and interpreter diverged at some
43    /// seed — caught by the per-seed cross-check, so never a false agreement.
44    SeedReplayDisagrees {
45        /// Which seed diverged and how.
46        detail: String,
47    },
48}
logicaffeine_tv/verdict.rs

logicaffeine_tv/
verdict.rs
