1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
//! Oracle property identifiers.
//!
//! A `Property` names a specific verifiable claim about an operation. The
//! cross-product emitter uses these to label generated test routes.
use crate::spec::types::{DeclaredLaw, OpSpec, OracleKind};
/// A verifiable claim about an operation that an oracle can confirm or refute.
#[derive(Debug, Clone)]
pub enum Property {
/// A declared algebraic law holds for this operation.
DeclaredLawHolds {
/// The law being verified.
law: DeclaredLaw,
},
/// A spec-table row matches the CPU reference.
SpecTableRowMatches {
/// Zero-based index into the spec table.
row_index: usize,
},
/// A specific input matches the CPU reference byte-for-byte.
PointParity {
/// Index of the input in the generated test set.
input_index: usize,
},
/// A composition preserves a declared law.
CompositionPreservesLaw {
/// The law that composition must preserve.
law: DeclaredLaw,
},
/// An arbitrary property check described by a string.
PropertyCheck {
/// Human-readable description of the property being checked.
description: String,
},
}
/// Resolved oracle handle returned by [`resolve`].
pub struct ResolvedOracle {
kind: OracleKind,
}
impl ResolvedOracle {
/// The oracle kind selected for this property.
pub fn kind(&self) -> OracleKind {
self.kind
}
}
/// Resolve the appropriate oracle for an operation + property pair.
///
/// Priority order:
/// 1. Spec-level `oracle_override` always wins.
/// 2. Law properties → `OracleKind::Law`.
/// 3. Spec-table properties → `OracleKind::SpecTable`.
/// 4. Composition properties → `OracleKind::Composition`.
/// 5. Everything else → `OracleKind::CpuReference` (point parity).
pub fn resolve(spec: &OpSpec, property: &Property) -> ResolvedOracle {
let kind = if let Some(override_kind) = spec.oracle_override {
override_kind
} else {
match property {
Property::DeclaredLawHolds { .. } => OracleKind::Law,
Property::SpecTableRowMatches { .. } => OracleKind::SpecTable,
Property::CompositionPreservesLaw { .. } => OracleKind::Composition,
Property::PointParity { .. } | Property::PropertyCheck { .. } => {
OracleKind::CpuReference
}
}
};
ResolvedOracle { kind }
}