pub enum SoundnessReport {
Agrees,
Disagrees {
detail: String,
},
Unsupported {
reason: String,
},
ParseFailed {
detail: String,
},
SeedReplayAgrees,
SeedReplayDisagrees {
detail: String,
},
}Expand description
Outcome of cross-validating the LOGOS encoder against the tree-walking interpreter
on one program (the meta-soundness check, work/PE_IMPROVE.md §4.2).
Variants§
Agrees
The encoder’s symbolic summary provably matches the interpreter’s observable behavior (outputs and error/no-error).
Disagrees
The encoder and interpreter disagree — an encoder bug (or a genuine miscompile, if the encoder is trusted). The detail localizes the divergence.
Unsupported
The program is outside the Verifiable Core, so the encoder did not model it. Soundly excluded from the check — never reported as agreement.
ParseFailed
The source failed to parse (should not occur for well-formed corpus programs).
SeedReplayAgrees
A nondeterministic program: for every seed in the sweep, the seeded encoder provably
matched the seeded interpreter (Select winners drawn from the same SplitMix64).
This is the seeded-replay analog of Self::Agrees.
SeedReplayDisagrees
A nondeterministic program where the seeded encoder and interpreter diverged at some seed — caught by the per-seed cross-check, so never a false agreement.
Trait Implementations§
Source§impl Clone for SoundnessReport
impl Clone for SoundnessReport
Source§fn clone(&self) -> SoundnessReport
fn clone(&self) -> SoundnessReport
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read moreSource§impl Debug for SoundnessReport
impl Debug for SoundnessReport
Source§impl PartialEq for SoundnessReport
impl PartialEq for SoundnessReport
Source§fn eq(&self, other: &SoundnessReport) -> bool
fn eq(&self, other: &SoundnessReport) -> bool
self and other values to be equal, and is used by ==.impl Eq for SoundnessReport
impl StructuralPartialEq for SoundnessReport
Auto Trait Implementations§
impl Freeze for SoundnessReport
impl RefUnwindSafe for SoundnessReport
impl Send for SoundnessReport
impl Sync for SoundnessReport
impl Unpin for SoundnessReport
impl UnsafeUnpin for SoundnessReport
impl UnwindSafe for SoundnessReport
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<T> Downcast for Twhere
T: Any,
impl<T> Downcast for Twhere
T: Any,
§fn into_any(self: Box<T>) -> Box<dyn Any>
fn into_any(self: Box<T>) -> Box<dyn Any>
Box<dyn Trait> (where Trait: Downcast) to Box<dyn Any>. Box<dyn Any> can
then be further downcast into Box<ConcreteType> where ConcreteType implements Trait.§fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
Rc<Trait> (where Trait: Downcast) to Rc<Any>. Rc<Any> can then be
further downcast into Rc<ConcreteType> where ConcreteType implements Trait.§fn as_any(&self) -> &(dyn Any + 'static)
fn as_any(&self) -> &(dyn Any + 'static)
&Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &Any’s vtable from &Trait’s.§fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
&mut Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &mut Any’s vtable from &mut Trait’s.§impl<T> DowncastSync for T
impl<T> DowncastSync for T
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key and return true if they are equal.