tokitai-operator 0.1.0

//! Domain-level contract primitives.
//!
//! `Contract`, `ContractId`, `ContractSet`, `Claim`, `Condition`,
//! `Evidence`, `Scope` are the abstract data types that the
//! operator layer uses to express "what does this op require" and
//! "what does this op provide". The contract set is read by the
//! planner when discharging obligations and by the verifier when
//! generating the `audit_report`.
//!
//! Public types: `Contract`, `ContractId`, `ContractSet`, `Claim`,
//! `Condition`, `Evidence`, `Scope`.
//!
//! Source-of-truth: this file is the only place the contract
//! primitives are declared. The op modules (`src/op/*.rs`)
//! consume them through the `pub use` re-export in
//! `src/op/contract.rs`.
//!
use std::collections::BTreeSet;

#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct ContractId(pub u64);

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum Claim {
    Associative,
    Commutative,
    Distributive,
    HasIdentity,
    HasInverse,
    Exact,
    Approximate,
    Deterministic,
    Local,
    CoverPreserving,
    RestrictionCompatible,
    Gluable,
    NonArchimedeanNorm,
    ValuationIdentity(String),
    PrecisionPreserved,
    PrecisionLossBounded(u32),
    BackendSemantic(String),
    /// A finite field specification: prime p and extension degree k.
    /// The element type is F_{p^k}; the modulus polynomial is
    /// provided by the domain at construction time.
    FiniteFieldSpec {
        prime: u64,
        extension_degree: usize,
    },
    Custom(String),
}

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum Scope {
    Domain(String),
    Object(String),
    Operator(String),
    Rewrite(String),
    Backend(String),
    Global,
}

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum Evidence {
    Axiom,
    Derived,
    Checked,
    Tested,
    ExternalProof(String),
    UnsafeAssumption,
}

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Condition {
    pub description: String,
}

impl Condition {
    pub fn new(description: impl Into<String>) -> Self {
        Self {
            description: description.into(),
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Contract {
    pub id: ContractId,
    pub claim: Claim,
    pub scope: Scope,
    pub evidence: Evidence,
    pub conditions: Vec<Condition>,
}

impl Contract {
    pub fn new(id: ContractId, claim: Claim, scope: Scope, evidence: Evidence) -> Self {
        Self {
            id,
            claim,
            scope,
            evidence,
            conditions: Vec::new(),
        }
    }
}

#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct ContractSet {
    contracts: BTreeSet<Contract>,
}

impl ContractSet {
    pub fn new() -> Self {
        Self::default()
    }

    pub fn from_iter(contracts: impl IntoIterator<Item = Contract>) -> Self {
        Self {
            contracts: contracts.into_iter().collect(),
        }
    }

    pub fn insert(&mut self, contract: Contract) {
        self.contracts.insert(contract);
    }

    pub fn contains_claim(&self, claim: &Claim) -> bool {
        self.contracts
            .iter()
            .any(|contract| &contract.claim == claim)
    }

    pub fn iter(&self) -> impl Iterator<Item = &Contract> {
        self.contracts.iter()
    }

    pub fn extend(&mut self, other: ContractSet) {
        self.contracts.extend(other.contracts);
    }

    pub fn is_empty(&self) -> bool {
        self.contracts.is_empty()
    }
}