machine_check/
verify.rs

1use crate::{ExecError, ExecResult, FullMachine};
2use log::{info, warn};
3use machine_check_common::{
4    check::KnownConclusion,
5    iir::{description::IMachine, property::IProperty},
6    ExecStats,
7};
8use machine_check_exec::{Framework, Strategy};
9
10/// Verifies the given system with given arguments.
11///
12/// If verifying the inherent property, false is returned if it does not hold.
13///
14/// If verifying a standard property and the inherent property is not assumed,
15/// it is verified first. If it does not hold, it is an execution error.
16pub fn verify<M: FullMachine>(
17    abstract_system: M::Abstr,
18    machine: IMachine,
19    prop: Option<IProperty>,
20    assume_inherent: bool,
21    strategy: Strategy,
22) -> ExecResult {
23    // Short-circuit error on assumption of the inherent property that we are trying to verify.
24    if prop.is_none() && assume_inherent {
25        return ExecResult {
26            result: Err(ExecError::VerifiedInherentAssumed),
27            stats: ExecStats::default(),
28        };
29    }
30
31    // Construct the framework.
32    let mut framework = Framework::<M>::new(abstract_system, machine, strategy);
33
34    // Verify the inherent property first if not assumed.
35    let inherent_result = if assume_inherent {
36        None
37    } else {
38        if prop.is_some() {
39            info!("Verifying the inherent property first.");
40        } else {
41            info!("Verifying the inherent property.");
42        }
43        let inherent_property = machine_check_machine::inherent_property();
44        Some(framework.verify(&inherent_property))
45    };
46
47    let Some(property) = prop else {
48        // Inherent property verification only.
49        // Print info and return the inherent property verification result.
50        // The property should be verified as the short-circuit was done previously.
51        return ExecResult {
52            result: inherent_result.expect("Inherent property should not be assumed"),
53            stats: framework.info(),
54        };
55    };
56
57    // Standard property verification.
58
59    if let Some(inherent_result) = inherent_result {
60        match inherent_result {
61            Ok(KnownConclusion::True) => {
62                // Inherent holds, we can continue.
63                info!("The inherent property holds, proceeding to the given property.");
64            }
65            Ok(KnownConclusion::False) => {
66                return ExecResult {
67                    result: Err(ExecError::InherentPanic),
68                    stats: framework.info(),
69                };
70            }
71            Ok(KnownConclusion::Dependent) => {
72                return ExecResult {
73                    result: Err(ExecError::InherentPanicDependent),
74                    stats: framework.info(),
75                };
76            }
77            Err(_) => {
78                // return the errors
79                return ExecResult {
80                    result: inherent_result,
81                    stats: framework.info(),
82                };
83            }
84        }
85    } else {
86        warn!("Assuming that the inherent property holds. If it does not, the verification result will be unusable.");
87    }
88
89    info!("Verifying the given property.");
90
91    // verify the property, assuming no panic can occur
92    let result = framework.verify(&property);
93
94    // also return framework stats
95    ExecResult {
96        result,
97        stats: framework.info(),
98    }
99}
machine_check/verify.rs

machine_check/
verify.rs
