quantrs2_circuit/verifier/
types.rs

1//! Common types and result structures for verification
2
3use super::config::VerifierConfig;
4use scirs2_core::Complex64;
5use serde::{Deserialize, Serialize};
6use std::collections::HashMap;
7use std::time::{Duration, SystemTime};
8
9/// Verification status
10#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
11pub enum VerificationStatus {
12    /// Circuit is verified correct
13    Verified,
14    /// Circuit has verification failures
15    Failed,
16    /// Verification incomplete due to timeout or resource limits
17    Incomplete,
18    /// Verification couldn't be performed
19    Unknown,
20    /// Verification in progress
21    InProgress,
22}
23
24/// Verification outcome
25#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
26pub enum VerificationOutcome {
27    /// Property holds
28    Satisfied,
29    /// Property violated
30    Violated,
31    /// Cannot determine (insufficient evidence)
32    Unknown,
33    /// Verification timeout
34    Timeout,
35    /// Verification error
36    Error { message: String },
37}
38
39/// Types of numerical evidence
40#[derive(Debug, Clone, Serialize, Deserialize)]
41pub enum EvidenceType {
42    /// Matrix norm measurement
43    MatrixNorm,
44    /// Eigenvalue analysis
45    Eigenvalue,
46    /// Fidelity measurement
47    Fidelity,
48    /// Entanglement measure
49    Entanglement,
50    /// Purity measurement
51    Purity,
52    /// Trace distance
53    TraceDistance,
54    /// Custom measurement
55    Custom { name: String },
56}
57
58/// Numerical evidence for verification
59#[derive(Debug, Clone, Serialize, Deserialize)]
60pub struct NumericalEvidence {
61    /// Evidence type
62    pub evidence_type: EvidenceType,
63    /// Measured value
64    pub measured_value: f64,
65    /// Expected value
66    pub expected_value: f64,
67    /// Deviation from expected
68    pub deviation: f64,
69    /// Statistical p-value if applicable
70    pub p_value: Option<f64>,
71}
72
73/// Error bounds for verification
74#[derive(Debug, Clone, Serialize, Deserialize)]
75pub struct ErrorBounds {
76    /// Lower bound
77    pub lower_bound: f64,
78    /// Upper bound
79    pub upper_bound: f64,
80    /// Confidence interval
81    pub confidence_interval: f64,
82    /// Standard deviation
83    pub standard_deviation: f64,
84}
85
86/// Violation severity levels
87#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
88pub enum ViolationSeverity {
89    /// Minor violation (within acceptable bounds)
90    Minor,
91    /// Moderate violation
92    Moderate,
93    /// Major violation
94    Major,
95    /// High severity violation
96    High,
97    /// Critical violation (circuit likely incorrect)
98    Critical,
99}
100
101/// Proof status
102#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
103pub enum ProofStatus {
104    /// Theorem proved
105    Proved,
106    /// Theorem disproved
107    Disproved,
108    /// Proof incomplete
109    Incomplete,
110    /// Proof timeout
111    Timeout,
112    /// Proof error
113    Error { message: String },
114}
115
116/// Proof steps
117#[derive(Debug, Clone, Serialize, Deserialize)]
118pub struct ProofStep {
119    /// Step description
120    pub description: String,
121    /// Rule or axiom used
122    pub rule: String,
123    /// Mathematical justification
124    pub justification: String,
125    /// Confidence in this step
126    pub confidence: f64,
127}
128
129/// Formal proof representation
130#[derive(Debug, Clone, Serialize, Deserialize)]
131pub struct FormalProof {
132    /// Proof tree
133    pub proof_tree: ProofTree,
134    /// Proof steps
135    pub steps: Vec<ProofStep>,
136    /// Axioms used
137    pub axioms_used: Vec<String>,
138    /// Proof confidence
139    pub confidence: f64,
140    /// Verification checksum
141    pub checksum: String,
142}
143
144/// Proof tree structure
145#[derive(Debug, Clone, Serialize, Deserialize)]
146pub struct ProofTree {
147    /// Root goal
148    pub root: ProofNode,
149    /// Proof branches
150    pub branches: Vec<Self>,
151}
152
153/// Proof tree node
154#[derive(Debug, Clone, Serialize, Deserialize)]
155pub struct ProofNode {
156    /// Goal statement
157    pub goal: String,
158    /// Applied rule
159    pub rule: Option<String>,
160    /// Subgoals
161    pub subgoals: Vec<String>,
162    /// Proof status
163    pub status: ProofStatus,
164}
165
166/// Counterexample for failed proofs
167#[derive(Debug, Clone, Serialize, Deserialize)]
168pub struct Counterexample {
169    /// Input values that cause failure
170    pub inputs: HashMap<String, f64>,
171    /// Expected vs actual output
172    pub expected_output: String,
173    /// `actual_output`: String,
174    pub actual_output: String,
175    /// Minimal counterexample flag
176    pub is_minimal: bool,
177}
178
179/// Proof complexity metrics
180#[derive(Debug, Clone, Serialize, Deserialize)]
181pub struct ProofComplexityMetrics {
182    /// Number of proof steps
183    pub step_count: usize,
184    /// Proof depth
185    pub proof_depth: usize,
186    /// Number of axioms used
187    pub axiom_count: usize,
188    /// Memory usage for proof
189    pub memory_usage: usize,
190    /// Proof verification time
191    pub verification_time: Duration,
192}
193
194/// Execution trace
195#[derive(Debug, Clone, Serialize, Deserialize)]
196pub struct ExecutionTrace {
197    /// Sequence of states
198    pub states: Vec<QuantumState>,
199    /// Sequence of transitions
200    pub transitions: Vec<StateTransition>,
201    /// Trace length
202    pub length: usize,
203    /// Trace properties
204    pub properties: HashMap<String, f64>,
205}
206
207/// Quantum state representation
208#[derive(Debug, Clone, Serialize, Deserialize)]
209pub struct QuantumState {
210    /// State vector
211    pub state_vector: Vec<Complex64>,
212    /// State properties
213    pub properties: HashMap<String, f64>,
214    /// Time stamp
215    pub timestamp: u64,
216    /// State metadata
217    pub metadata: HashMap<String, String>,
218}
219
220/// State transition
221#[derive(Debug, Clone, Serialize, Deserialize)]
222pub struct StateTransition {
223    /// Source state
224    pub source: usize,
225    /// Target state
226    pub target: usize,
227    /// Transition operation
228    pub operation: String,
229    /// Transition probability
230    pub probability: f64,
231    /// Transition time
232    pub time: f64,
233}
234
235/// State space statistics
236#[derive(Debug, Clone, Serialize, Deserialize)]
237pub struct StateSpaceStatistics {
238    /// Total number of states
239    pub total_states: usize,
240    /// Number of transitions
241    pub total_transitions: usize,
242    /// Maximum path length
243    pub max_path_length: usize,
244    /// Average path length
245    pub avg_path_length: f64,
246    /// State space diameter
247    pub diameter: usize,
248    /// Memory usage
249    pub memory_usage: usize,
250}
251
252/// Test outcome
253#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
254pub enum TestOutcome {
255    /// Test passed
256    Pass,
257    /// Test failed
258    Fail,
259    /// Test skipped
260    Skip,
261    /// Test error
262    Error { message: String },
263}
264
265/// Verification statistics
266#[derive(Debug, Clone, Serialize, Deserialize)]
267pub struct VerificationStatistics {
268    /// Total verification time
269    pub total_time: Duration,
270    /// Number of properties verified
271    pub properties_verified: usize,
272    /// Number of invariants checked
273    pub invariants_checked: usize,
274    /// Number of theorems proved
275    pub theorems_proved: usize,
276    /// Success rate
277    pub success_rate: f64,
278    /// Memory usage
279    pub memory_usage: usize,
280    /// Confidence statistics
281    pub confidence_stats: ConfidenceStatistics,
282}
283
284/// Confidence statistics
285#[derive(Debug, Clone, Serialize, Deserialize)]
286pub struct ConfidenceStatistics {
287    /// Average confidence
288    pub average_confidence: f64,
289    /// Minimum confidence
290    pub min_confidence: f64,
291    /// Maximum confidence
292    pub max_confidence: f64,
293    /// Confidence standard deviation
294    pub confidence_std_dev: f64,
295}
296
297/// Verification issue
298#[derive(Debug, Clone, Serialize, Deserialize)]
299pub struct VerificationIssue {
300    /// Issue type
301    pub issue_type: IssueType,
302    /// Issue severity
303    pub severity: IssueSeverity,
304    /// Issue description
305    pub description: String,
306    /// Location in circuit
307    pub location: Option<CircuitLocation>,
308    /// Suggested fix
309    pub suggested_fix: Option<String>,
310    /// Related evidence
311    pub evidence: Vec<NumericalEvidence>,
312}
313
314/// Issue types
315#[derive(Debug, Clone, Serialize, Deserialize)]
316pub enum IssueType {
317    /// Property violation
318    PropertyViolation,
319    /// Invariant violation
320    InvariantViolation,
321    /// Theorem proof failure
322    TheoremFailure,
323    /// Model checking failure
324    ModelCheckFailure,
325    /// Symbolic execution error
326    SymbolicExecutionError,
327    /// Numerical instability
328    NumericalInstability,
329    /// Performance issue
330    PerformanceIssue,
331}
332
333/// Issue severity
334#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
335pub enum IssueSeverity {
336    /// Low severity - informational
337    Low,
338    /// Medium severity - potential problem
339    Medium,
340    /// High severity - likely problem
341    High,
342    /// Critical severity - definite problem
343    Critical,
344}
345
346/// Circuit location
347#[derive(Debug, Clone, Serialize, Deserialize)]
348pub struct CircuitLocation {
349    /// Gate index
350    pub gate_index: usize,
351    /// Qubit indices
352    pub qubit_indices: Vec<usize>,
353    /// Circuit depth
354    pub depth: usize,
355}
356
357/// Verification metadata
358#[derive(Debug, Clone, Serialize, Deserialize)]
359pub struct VerificationMetadata {
360    /// Verification timestamp
361    pub timestamp: SystemTime,
362    /// Verifier version
363    pub verifier_version: String,
364    /// `SciRS2` version
365    pub scirs2_version: String,
366    /// Verification configuration
367    pub config: VerifierConfig,
368    /// Hardware information
369    pub hardware_info: HashMap<String, String>,
370}
371
372/// Proof strategies
373#[derive(Debug, Clone, Serialize, Deserialize)]
374pub enum ProofStrategy {
375    /// Direct proof
376    Direct,
377    /// Proof by contradiction
378    Contradiction,
379    /// Proof by induction
380    Induction,
381    /// Case analysis
382    CaseAnalysis,
383    /// Symbolic computation
384    SymbolicComputation,
385    /// Numerical verification
386    NumericalVerification,
387    /// Statistical testing
388    StatisticalTesting,
389}
390
391/// Error models for quantum error correction
392#[derive(Debug, Clone, Serialize, Deserialize)]
393pub enum ErrorModel {
394    /// Depolarizing noise
395    Depolarizing { probability: f64 },
396    /// Bit flip errors
397    BitFlip { probability: f64 },
398    /// Phase flip errors
399    PhaseFlip { probability: f64 },
400    /// Amplitude damping
401    AmplitudeDamping { gamma: f64 },
402    /// Custom error model
403    Custom {
404        description: String,
405        parameters: HashMap<String, f64>,
406    },
407}
408
409/// Expected output for algorithm verification
410#[derive(Debug, Clone, Serialize, Deserialize)]
411pub enum ExpectedOutput {
412    /// Classical bit string
413    ClassicalBits { bits: Vec<bool> },
414    /// Quantum state
415    QuantumState { state: Vec<Complex64> },
416    /// Probability distribution
417    ProbabilityDistribution { probabilities: Vec<f64> },
418    /// Measurement statistics
419    MeasurementStats { mean: f64, variance: f64 },
420}
421
422/// Proof obligations
423#[derive(Debug, Clone, Serialize, Deserialize)]
424pub struct ProofObligation {
425    /// Obligation name
426    pub name: String,
427    /// Preconditions
428    pub preconditions: Vec<String>,
429    /// Postconditions
430    pub postconditions: Vec<String>,
431    /// Proof steps
432    pub proof_steps: Vec<ProofStep>,
433}
434
435/// Test case for functional correctness
436#[derive(Debug, Clone, Serialize, Deserialize)]
437pub struct TestCase {
438    /// Input state
439    pub input: Vec<Complex64>,
440    /// Expected output
441    pub expected_output: Vec<Complex64>,
442    /// Test description
443    pub description: String,
444    /// Test weight
445    pub weight: f64,
446}
447
448/// Complexity class for scalability analysis
449#[derive(Debug, Clone, Serialize, Deserialize)]
450pub enum ComplexityClass {
451    /// Constant O(1)
452    Constant,
453    /// Logarithmic O(log n)
454    Logarithmic,
455    /// Linear O(n)
456    Linear,
457    /// Polynomial O(n^k)
458    Polynomial { degree: f64 },
459    /// Exponential O(2^n)
460    Exponential,
461}
quantrs2_circuit/verifier/types.rs

quantrs2_circuit/verifier/
types.rs
