vyre_spec/verification.rs
1//! Frozen verification-evidence records attached to declared algebraic laws.
2
3use crate::float_type::FloatType;
4
5/// Evidence attached to a declared law in the frozen data contract.
6///
7/// Example: `Verification::WitnessedU32 { seed: 7, count: 1024 }` records a
8/// deterministic witness run for a full-width integer law.
9#[derive(Clone, Debug, Eq, PartialEq)]
10#[non_exhaustive]
11pub enum Verification {
12 /// Exhaustively verified over the `u8` input domain.
13 ExhaustiveU8,
14 /// Exhaustively verified over the `u16` input domain.
15 ExhaustiveU16,
16 /// Witnessed over `u32` using a deterministic seed and count.
17 WitnessedU32 {
18 /// Deterministic random seed used by the proof engine.
19 seed: u64,
20 /// Number of witnesses checked; coverage rejects zero.
21 count: u64,
22 },
23 /// Exhaustively verified for a restricted floating-point type.
24 ExhaustiveFloat {
25 /// Floating-point format covered by the exhaustive pass.
26 typ: FloatType,
27 },
28}
29
30impl Verification {
31 /// Return the witness count for witnessed variants, or `None` for
32 /// exhaustive variants.
33 #[must_use]
34 pub fn witness_count(&self) -> Option<u64> {
35 match self {
36 Self::WitnessedU32 { count, .. } => Some(*count),
37 _ => None,
38 }
39 }
40}