vyre-spec 0.1.1

Frozen data contracts for vyre — OpSpec, AlgebraicLaw, Category, IntrinsicTable
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

//! Completeness check for the frozen invariant catalog.

use std::collections::BTreeSet;

use crate::{engine_invariant::InvariantId, invariants::invariants};

/// Return true when every I1..I15 invariant appears exactly once.
#[must_use]
pub fn catalog_is_complete() -> bool {
    let known_ids = InvariantId::iter().collect::<BTreeSet<_>>();
    let catalog_ids = invariants()
        .iter()
        .map(|inv| inv.id.clone())
        .collect::<BTreeSet<_>>();
    catalog_ids == known_ids
}