optirs_core/privacy/enhanced_audit/
model_checking.rs

1//! Bounded invariant model checking over the declared system model.
2//!
3//! # What is and is not implemented
4//!
5//! `ModelChecker` used to be a constructor with no other methods, and the
6//! engine that owned it reported "all properties verified" for every input.
7//! What is implemented here is an *honest subset*: bounded reachability
8//! checking of state invariants, plus a small, fully specified atomic
9//! predicate language. Anything outside that subset -- liveness, fairness,
10//! nested temporal operators, the full CTL/LTL grammar -- returns
11//! [`OptimError::UnsupportedOperation`] naming the unsupported construct,
12//! never a vacuous success.
13//!
14//! # Specification language
15//!
16//! ```text
17//! spec       := "AG(" atom ")" | "INV(" atom ")" | atom
18//! atom       := comparison | flag | "finite(" term ")" | "!" atom
19//! comparison := term op number          op := "<=" | "<" | ">=" | ">" | "=="
20//! term       := "epsilon" | "delta" | "var:" identifier
21//! flag       := "data_minimization" | "purpose_limitation" | "storage_limitation"
22//! ```
23//!
24//! `AG` (or `INV`) means "on all paths, globally" -- exactly the invariant
25//! semantics that bounded reachability decides. A bare atom is treated as an
26//! invariant as well, which is the reading `PropertyType::Invariant` implies.
27
28use crate::error::{OptimError, Result};
29use scirs2_core::numeric::Float;
30use std::collections::{HashMap, HashSet, VecDeque};
31use std::fmt::Debug;
32
33use super::types::{PropertyType, SystemProperty, SystemState, TransitionFunction};
34
35/// Default cap on the number of states explored before the checker gives up.
36pub const DEFAULT_STATE_BOUND: usize = 100_000;
37
38/// A term that can be read out of a system state.
39#[derive(Debug, Clone, PartialEq, Eq)]
40pub enum Term {
41    /// The epsilon budget of the state's privacy context.
42    Epsilon,
43    /// The delta budget of the state's privacy context.
44    Delta,
45    /// A named state variable.
46    Variable(String),
47}
48
49/// A comparison operator.
50#[derive(Debug, Clone, Copy, PartialEq, Eq)]
51pub enum CompareOp {
52    /// Less than or equal.
53    LessOrEqual,
54    /// Strictly less.
55    Less,
56    /// Greater than or equal.
57    GreaterOrEqual,
58    /// Strictly greater.
59    Greater,
60    /// Exact equality of the IEEE-754 value.
61    Equal,
62}
63
64/// A boolean flag of the privacy context.
65#[derive(Debug, Clone, Copy, PartialEq, Eq)]
66pub enum ContextFlag {
67    /// `PrivacyContext::data_minimization`.
68    DataMinimization,
69    /// `PrivacyContext::purpose_limitation`.
70    PurposeLimitation,
71    /// `PrivacyContext::storage_limitation`.
72    StorageLimitation,
73}
74
75/// An atomic state predicate.
76#[derive(Debug, Clone, PartialEq)]
77pub enum StatePredicate {
78    /// `term op number`
79    Compare {
80        /// Left-hand term read from the state.
81        term: Term,
82        /// Comparison operator.
83        op: CompareOp,
84        /// Right-hand constant.
85        value: f64,
86    },
87    /// `finite(term)`
88    Finite(Term),
89    /// A boolean privacy-context flag.
90    Flag(ContextFlag),
91    /// Logical negation.
92    Not(Box<StatePredicate>),
93}
94
95impl StatePredicate {
96    /// Parse a specification string into an invariant predicate.
97    ///
98    /// Returns [`OptimError::UnsupportedOperation`] for syntactically valid
99    /// temporal logic this checker cannot decide, and
100    /// [`OptimError::InvalidParameter`] for text that is not a specification
101    /// at all.
102    pub fn parse(specification: &str) -> Result<Self> {
103        let trimmed = specification.trim();
104        let inner = if let Some(rest) = strip_wrapper(trimmed, "AG") {
105            rest
106        } else if let Some(rest) = strip_wrapper(trimmed, "INV") {
107            rest
108        } else {
109            for unsupported in ["AF", "AX", "AU", "EG", "EF", "EX", "EU", "G", "F", "X", "U"] {
110                if strip_wrapper(trimmed, unsupported).is_some() {
111                    return Err(OptimError::UnsupportedOperation(format!(
112                        "the temporal operator `{unsupported}` in specification `{specification}` \
113                         is not decided by this checker; only invariants (`AG(...)` / `INV(...)`) \
114                         are supported"
115                    )));
116                }
117            }
118            trimmed
119        };
120        Self::parse_atom(inner.trim(), specification)
121    }
122
123    /// Parse an atomic predicate (with optional leading `!`).
124    fn parse_atom(text: &str, full: &str) -> Result<Self> {
125        if let Some(rest) = text.strip_prefix('!') {
126            return Ok(Self::Not(Box::new(Self::parse_atom(rest.trim(), full)?)));
127        }
128        if let Some(rest) = strip_wrapper(text, "finite") {
129            return Ok(Self::Finite(parse_term(rest.trim(), full)?));
130        }
131        match text {
132            "data_minimization" => return Ok(Self::Flag(ContextFlag::DataMinimization)),
133            "purpose_limitation" => return Ok(Self::Flag(ContextFlag::PurposeLimitation)),
134            "storage_limitation" => return Ok(Self::Flag(ContextFlag::StorageLimitation)),
135            _ => {}
136        }
137
138        // Longest operators first so `<=` is not read as `<`.
139        for (token, op) in [
140            ("<=", CompareOp::LessOrEqual),
141            (">=", CompareOp::GreaterOrEqual),
142            ("==", CompareOp::Equal),
143            ("<", CompareOp::Less),
144            (">", CompareOp::Greater),
145        ] {
146            if let Some(position) = text.find(token) {
147                let left = text[..position].trim();
148                let right = text[position + token.len()..].trim();
149                let value: f64 = right.parse().map_err(|_| {
150                    OptimError::InvalidParameter(format!(
151                        "the right-hand side `{right}` of specification `{full}` is not a number"
152                    ))
153                })?;
154                return Ok(Self::Compare {
155                    term: parse_term(left, full)?,
156                    op,
157                    value,
158                });
159            }
160        }
161
162        Err(OptimError::UnsupportedOperation(format!(
163            "specification `{full}` is not an atomic predicate this checker understands; see the \
164             grammar in `privacy::enhanced_audit::model_checking`"
165        )))
166    }
167
168    /// Evaluate the predicate in a state.
169    pub fn evaluate<T: Float + Debug + Send + Sync + 'static>(
170        &self,
171        state: &SystemState<T>,
172    ) -> Result<bool> {
173        match self {
174            Self::Compare { term, op, value } => {
175                let left = read_term(term, state)?;
176                Ok(match op {
177                    CompareOp::LessOrEqual => left <= *value,
178                    CompareOp::Less => left < *value,
179                    CompareOp::GreaterOrEqual => left >= *value,
180                    CompareOp::Greater => left > *value,
181                    CompareOp::Equal => left == *value,
182                })
183            }
184            Self::Finite(term) => Ok(read_term(term, state)?.is_finite()),
185            Self::Flag(flag) => Ok(match flag {
186                ContextFlag::DataMinimization => state.privacy_params.data_minimization,
187                ContextFlag::PurposeLimitation => state.privacy_params.purpose_limitation,
188                ContextFlag::StorageLimitation => state.privacy_params.storage_limitation,
189            }),
190            Self::Not(inner) => Ok(!inner.evaluate(state)?),
191        }
192    }
193}
194
195/// Strip a `name(...)` wrapper, returning the contents.
196fn strip_wrapper<'a>(text: &'a str, name: &str) -> Option<&'a str> {
197    let rest = text.strip_prefix(name)?;
198    let rest = rest.trim_start();
199    let rest = rest.strip_prefix('(')?;
200    rest.strip_suffix(')')
201}
202
203/// Parse a term.
204fn parse_term(text: &str, full: &str) -> Result<Term> {
205    match text {
206        "epsilon" => Ok(Term::Epsilon),
207        "delta" => Ok(Term::Delta),
208        _ => match text.strip_prefix("var:") {
209            Some(name) if !name.is_empty() => Ok(Term::Variable(name.to_string())),
210            _ => Err(OptimError::InvalidParameter(format!(
211                "`{text}` in specification `{full}` is not a term (expected `epsilon`, `delta` or \
212                 `var:<name>`)"
213            ))),
214        },
215    }
216}
217
218/// Read a term out of a state.
219fn read_term<T: Float + Debug + Send + Sync + 'static>(
220    term: &Term,
221    state: &SystemState<T>,
222) -> Result<f64> {
223    match term {
224        Term::Epsilon => Ok(state.privacy_params.epsilon_budget),
225        Term::Delta => Ok(state.privacy_params.delta_budget),
226        Term::Variable(name) => {
227            let value = state.variables.get(name).ok_or_else(|| {
228                OptimError::InvalidState(format!(
229                    "state `{}` has no variable named `{name}`, so the property cannot be decided",
230                    state.id
231                ))
232            })?;
233            value.to_f64().ok_or_else(|| {
234                OptimError::InvalidState(format!(
235                    "variable `{name}` of state `{}` cannot be represented as f64",
236                    state.id
237                ))
238            })
239        }
240    }
241}
242
243/// Outcome of checking one property.
244#[derive(Debug, Clone)]
245pub struct ModelCheckOutcome {
246    /// Name of the checked property.
247    pub property: String,
248    /// Whether the invariant held in every reachable state.
249    pub holds: bool,
250    /// Number of distinct states explored.
251    pub states_explored: usize,
252    /// Identifier of the first state violating the invariant, if any.
253    pub counterexample: Option<String>,
254}
255
256/// System model for verification.
257pub struct SystemModel<T: Float + Debug + Send + Sync + 'static> {
258    /// Declared initial states.
259    states: Vec<SystemState<T>>,
260    /// Named transition relations.
261    transitions: HashMap<String, TransitionFunction<T>>,
262}
263
264impl<T: Float + Debug + Send + Sync + 'static> SystemModel<T> {
265    /// Create an empty model.
266    pub fn new() -> Self {
267        Self {
268            states: Vec::new(),
269            transitions: HashMap::new(),
270        }
271    }
272
273    /// Add an initial state.
274    pub fn add_initial_state(&mut self, state: SystemState<T>) {
275        self.states.push(state);
276    }
277
278    /// Register a transition relation.
279    pub fn add_transition(&mut self, transition: TransitionFunction<T>) {
280        self.transitions.insert(transition.name.clone(), transition);
281    }
282
283    /// Number of declared initial states.
284    pub fn initial_state_count(&self) -> usize {
285        self.states.len()
286    }
287
288    /// Number of registered transitions.
289    pub fn transition_count(&self) -> usize {
290        self.transitions.len()
291    }
292
293    /// Bounded breadth-first exploration of the reachable state space,
294    /// checking `predicate` in every state.
295    ///
296    /// States are deduplicated by identifier. Exceeding `state_bound` is an
297    /// error, not a pass: an unfinished exploration proves nothing.
298    pub fn check_invariant(
299        &self,
300        predicate: &StatePredicate,
301        state_bound: usize,
302    ) -> Result<(bool, usize, Option<String>)> {
303        if self.states.is_empty() {
304            return Err(OptimError::InvalidState(
305                "the system model declares no initial state, so no property can be decided"
306                    .to_string(),
307            ));
308        }
309
310        let mut seen: HashSet<String> = HashSet::new();
311        let mut queue: VecDeque<SystemState<T>> = VecDeque::new();
312        for state in &self.states {
313            if seen.insert(state.id.clone()) {
314                queue.push_back(state.clone());
315            }
316        }
317
318        let mut explored = 0usize;
319        while let Some(state) = queue.pop_front() {
320            explored += 1;
321            if explored > state_bound {
322                return Err(OptimError::ResourceError(format!(
323                    "the reachable state space exceeded the exploration bound of {state_bound} \
324                     states; the property is undecided (not verified)"
325                )));
326            }
327            if !predicate.evaluate(&state)? {
328                return Ok((false, explored, Some(state.id.clone())));
329            }
330            for transition in self.transitions.values() {
331                for successor in (transition.logic)(&state) {
332                    if seen.insert(successor.id.clone()) {
333                        queue.push_back(successor);
334                    }
335                }
336            }
337        }
338
339        Ok((true, explored, None))
340    }
341}
342
343impl<T: Float + Debug + Send + Sync + 'static> Default for SystemModel<T> {
344    fn default() -> Self {
345        Self::new()
346    }
347}
348
349/// Bounded invariant model checker.
350pub struct ModelChecker<T: Float + Debug + Send + Sync + 'static> {
351    /// The system under check.
352    model: SystemModel<T>,
353    /// Properties to check.
354    properties: Vec<SystemProperty>,
355    /// Exploration bound.
356    state_bound: usize,
357}
358
359impl<T: Float + Debug + Send + Sync + 'static> ModelChecker<T> {
360    /// Create an empty checker with the default exploration bound.
361    pub fn new() -> Self {
362        Self {
363            model: SystemModel::new(),
364            properties: Vec::new(),
365            state_bound: DEFAULT_STATE_BOUND,
366        }
367    }
368
369    /// Replace the exploration bound.
370    pub fn set_state_bound(&mut self, state_bound: usize) -> Result<()> {
371        if state_bound == 0 {
372            return Err(OptimError::InvalidParameter(
373                "the state exploration bound must be positive".to_string(),
374            ));
375        }
376        self.state_bound = state_bound;
377        Ok(())
378    }
379
380    /// Mutable access to the system model.
381    pub fn model_mut(&mut self) -> &mut SystemModel<T> {
382        &mut self.model
383    }
384
385    /// Register a property to check.
386    ///
387    /// The specification is parsed immediately, so an unsupported property is
388    /// rejected at registration rather than silently passing later.
389    pub fn add_property(&mut self, property: SystemProperty) -> Result<()> {
390        match property.property_type {
391            PropertyType::Invariant | PropertyType::Safety => {
392                let _ = StatePredicate::parse(&property.specification)?;
393                self.properties.push(property);
394                Ok(())
395            }
396            PropertyType::Liveness | PropertyType::Temporal => {
397                Err(OptimError::UnsupportedOperation(format!(
398                    "property `{}` is a {:?} property; this checker decides invariants only, and \
399                     will not report an undecided property as verified",
400                    property.name, property.property_type
401                )))
402            }
403        }
404    }
405
406    /// Number of registered properties.
407    pub fn property_count(&self) -> usize {
408        self.properties.len()
409    }
410
411    /// Check one property.
412    pub fn check_property(&self, property: &SystemProperty) -> Result<ModelCheckOutcome> {
413        match property.property_type {
414            PropertyType::Invariant | PropertyType::Safety => {}
415            PropertyType::Liveness | PropertyType::Temporal => {
416                return Err(OptimError::UnsupportedOperation(format!(
417                    "property `{}` is a {:?} property; deciding it needs a full temporal-logic \
418                     model checker, which is not implemented here",
419                    property.name, property.property_type
420                )))
421            }
422        }
423        let predicate = StatePredicate::parse(&property.specification)?;
424        let (holds, explored, counterexample) =
425            self.model.check_invariant(&predicate, self.state_bound)?;
426        Ok(ModelCheckOutcome {
427            property: property.name.clone(),
428            holds,
429            states_explored: explored,
430            counterexample,
431        })
432    }
433
434    /// Check every registered property.
435    ///
436    /// An empty property set is an error: "zero properties checked" is not the
437    /// same claim as "the system is correct".
438    pub fn check_all(&self) -> Result<Vec<ModelCheckOutcome>> {
439        if self.properties.is_empty() {
440            return Err(OptimError::InvalidState(
441                "no properties are registered with the model checker; there is nothing to verify"
442                    .to_string(),
443            ));
444        }
445        self.properties
446            .iter()
447            .map(|property| self.check_property(property))
448            .collect()
449    }
450}
451
452impl<T: Float + Debug + Send + Sync + 'static> Default for ModelChecker<T> {
453    fn default() -> Self {
454        Self::new()
455    }
456}
457
458#[cfg(test)]
459mod tests {
460    use super::*;
461    use crate::privacy::enhanced_audit::types::PrivacyContext;
462
463    fn context(epsilon: f64) -> PrivacyContext {
464        PrivacyContext {
465            epsilon_budget: epsilon,
466            delta_budget: 1e-6,
467            privacy_mechanism: "dp_sgd".to_string(),
468            data_minimization: true,
469            purpose_limitation: true,
470            storage_limitation: false,
471        }
472    }
473
474    fn state(id: &str, spent: f64) -> SystemState<f64> {
475        let mut variables = HashMap::new();
476        variables.insert("spent".to_string(), spent);
477        SystemState {
478            id: id.to_string(),
479            variables,
480            privacy_params: context(spent),
481        }
482    }
483
484    /// A chain of `steps` states, each spending 0.5 more epsilon.
485    fn spending_model(steps: usize) -> SystemModel<f64> {
486        let mut model = SystemModel::new();
487        model.add_initial_state(state("s0", 0.0));
488        let limit = steps;
489        model.add_transition(TransitionFunction {
490            name: "spend".to_string(),
491            logic: Box::new(move |current: &SystemState<f64>| {
492                let step = current
493                    .id
494                    .strip_prefix('s')
495                    .and_then(|rest| rest.parse::<usize>().ok())
496                    .unwrap_or(0);
497                if step >= limit {
498                    Vec::new()
499                } else {
500                    vec![state(&format!("s{}", step + 1), (step + 1) as f64 * 0.5)]
501                }
502            }),
503        });
504        model
505    }
506
507    #[test]
508    fn an_invariant_that_holds_is_reported_as_holding() {
509        let model = spending_model(4);
510        let predicate = match StatePredicate::parse("AG(var:spent <= 2.0)") {
511            Ok(predicate) => predicate,
512            Err(err) => panic!("parse failed: {err}"),
513        };
514        let (holds, explored, counterexample) =
515            match model.check_invariant(&predicate, DEFAULT_STATE_BOUND) {
516                Ok(outcome) => outcome,
517                Err(err) => panic!("check failed: {err}"),
518            };
519        assert!(holds);
520        assert_eq!(explored, 5, "s0..s4 inclusive");
521        assert!(counterexample.is_none());
522    }
523
524    #[test]
525    fn an_invariant_that_is_violated_yields_a_counterexample() {
526        let model = spending_model(4);
527        let predicate = match StatePredicate::parse("AG(var:spent <= 1.0)") {
528            Ok(predicate) => predicate,
529            Err(err) => panic!("parse failed: {err}"),
530        };
531        let (holds, _explored, counterexample) =
532            match model.check_invariant(&predicate, DEFAULT_STATE_BOUND) {
533                Ok(outcome) => outcome,
534                Err(err) => panic!("check failed: {err}"),
535            };
536        assert!(!holds, "spending reaches 2.0, which violates <= 1.0");
537        assert_eq!(counterexample.as_deref(), Some("s3"));
538    }
539
540    #[test]
541    fn exceeding_the_state_bound_is_an_error_not_a_pass() {
542        let model = spending_model(1000);
543        let predicate = match StatePredicate::parse("AG(var:spent >= 0.0)") {
544            Ok(predicate) => predicate,
545            Err(err) => panic!("parse failed: {err}"),
546        };
547        let outcome = model.check_invariant(&predicate, 10);
548        assert!(
549            outcome.is_err(),
550            "an unfinished exploration must not report success"
551        );
552    }
553
554    #[test]
555    fn a_model_with_no_initial_state_cannot_decide_anything() {
556        let model: SystemModel<f64> = SystemModel::new();
557        let predicate = match StatePredicate::parse("data_minimization") {
558            Ok(predicate) => predicate,
559            Err(err) => panic!("parse failed: {err}"),
560        };
561        assert!(model.check_invariant(&predicate, 10).is_err());
562    }
563
564    #[test]
565    fn liveness_and_temporal_properties_are_refused_explicitly() {
566        let mut checker: ModelChecker<f64> = ModelChecker::new();
567        let outcome = checker.add_property(SystemProperty {
568            name: "eventually_terminates".to_string(),
569            specification: "AF(var:spent >= 2.0)".to_string(),
570            property_type: PropertyType::Liveness,
571        });
572        let message = match outcome {
573            Err(err) => err.to_string(),
574            Ok(()) => panic!("a liveness property must not be accepted"),
575        };
576        assert!(message.contains("invariants only"), "got: {message}");
577    }
578
579    #[test]
580    fn unsupported_temporal_operators_are_named_in_the_error() {
581        let outcome = StatePredicate::parse("EF(var:spent >= 1.0)");
582        let message = match outcome {
583            Err(err) => err.to_string(),
584            Ok(_) => panic!("EF must not parse"),
585        };
586        assert!(message.contains("EF"), "got: {message}");
587    }
588
589    #[test]
590    fn checking_with_no_registered_properties_is_an_error() {
591        let checker: ModelChecker<f64> = ModelChecker::new();
592        assert!(
593            checker.check_all().is_err(),
594            "zero properties checked must not read as verified"
595        );
596    }
597
598    #[test]
599    fn the_checker_runs_registered_invariants_end_to_end() {
600        let mut checker: ModelChecker<f64> = ModelChecker::new();
601        {
602            let model = checker.model_mut();
603            model.add_initial_state(state("s0", 0.0));
604            model.add_transition(TransitionFunction {
605                name: "spend".to_string(),
606                logic: Box::new(|current: &SystemState<f64>| {
607                    if current.id == "s0" {
608                        vec![state("s1", 3.0)]
609                    } else {
610                        Vec::new()
611                    }
612                }),
613            });
614        }
615        let ok = checker.add_property(SystemProperty {
616            name: "budget_bounded".to_string(),
617            specification: "AG(epsilon <= 1.0)".to_string(),
618            property_type: PropertyType::Safety,
619        });
620        assert!(ok.is_ok());
621
622        let outcomes = match checker.check_all() {
623            Ok(outcomes) => outcomes,
624            Err(err) => panic!("check_all failed: {err}"),
625        };
626        assert_eq!(outcomes.len(), 1);
627        assert!(!outcomes[0].holds, "s1 spends 3.0 > 1.0");
628        assert_eq!(outcomes[0].counterexample.as_deref(), Some("s1"));
629    }
630
631    #[test]
632    fn every_atom_of_the_grammar_evaluates() {
633        let good = state("ok", 0.25);
634        let cases: [(&str, bool); 9] = [
635            ("epsilon <= 1.0", true),
636            ("epsilon > 1.0", false),
637            ("delta < 0.001", true),
638            ("var:spent == 0.25", true),
639            ("finite(var:spent)", true),
640            ("data_minimization", true),
641            ("purpose_limitation", true),
642            ("storage_limitation", false),
643            ("!storage_limitation", true),
644        ];
645        for (specification, expected) in cases {
646            let predicate = match StatePredicate::parse(specification) {
647                Ok(predicate) => predicate,
648                Err(err) => panic!("`{specification}` failed to parse: {err}"),
649            };
650            let value = match predicate.evaluate(&good) {
651                Ok(value) => value,
652                Err(err) => panic!("`{specification}` failed to evaluate: {err}"),
653            };
654            assert_eq!(value, expected, "specification `{specification}`");
655        }
656    }
657
658    #[test]
659    fn a_missing_state_variable_is_an_error_not_false() {
660        let predicate = match StatePredicate::parse("var:absent <= 1.0") {
661            Ok(predicate) => predicate,
662            Err(err) => panic!("parse failed: {err}"),
663        };
664        assert!(predicate.evaluate(&state("s", 0.0)).is_err());
665    }
666
667    #[test]
668    fn nonsense_specifications_are_rejected() {
669        assert!(StatePredicate::parse("this is not a predicate").is_err());
670        assert!(StatePredicate::parse("epsilon <= not_a_number").is_err());
671        assert!(StatePredicate::parse("unknown_term <= 1.0").is_err());
672    }
673}
optirs_core/privacy/enhanced_audit/model_checking.rs

optirs_core/privacy/enhanced_audit/
model_checking.rs
