rapx/verify/smt_check/
valid_num.rs

1//! SMT lowering for the `ValidNum` safety property.
2//!
3//! `ValidNum` carries one or more numeric predicates, for example:
4//!
5//! ```text
6//! ValidNum(i < len)
7//! ValidNum(size_of(T) * len <= isize::MAX)
8//! ```
9//!
10//! This module only rebinds callee-side contract expressions to the concrete
11//! checkpoint arguments and converts them to common SMT predicates.  The shared
12//! backend discharges the query by checking whether the negated predicate is
13//! satisfiable under the forward path facts.
14
15use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
16use crate::verify::{contract::Property, helpers::Checkpoint, verifier::ForwardVisitResult};
17
18/// Check `ValidNum` by lowering all predicates to a common predicate obligation.
19pub(crate) fn check<'tcx>(
20    checker: &SmtChecker<'tcx>,
21    checkpoint: &Checkpoint<'tcx>,
22    property: &Property<'tcx>,
23    forward: &ForwardVisitResult<'tcx>,
24) -> SmtCheckResult {
25    let Some(smt_predicates) = checker.property_numeric_smt_predicates(checkpoint, property) else {
26        return SmtCheckResult::unknown("ValidNum predicate could not be lowered to SMT");
27    };
28
29    checker.prove_obligation(
30        checkpoint,
31        forward,
32        SmtObligation::Predicate {
33            predicates: smt_predicates,
34        },
35    )
36}
rapx/verify/smt_check/valid_num.rs

rapx/verify/smt_check/
valid_num.rs
