|
1 | 1 | // SPDX-License-Identifier: PMPL-1.0-or-later |
2 | 2 | // Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
3 | | -// ABI module for phronesiser — Idris2 proof types for Phronesis interface correctness. |
| 3 | +// |
| 4 | +// ABI module for phronesiser — Rust-side type definitions mirroring the Idris2 |
| 5 | +// formal proofs for Phronesis interface correctness. |
| 6 | +// |
| 7 | +// These types define the core domain model for deontic constraint evaluation: |
| 8 | +// - DeonticModality: The three modalities (obligation, permission, prohibition). |
| 9 | +// - Constraint: A fully resolved constraint ready for evaluation. |
| 10 | +// - AgentAction: An action the agent is attempting to perform. |
| 11 | +// - AuditDecision: The outcome of evaluating an action against constraints. |
| 12 | +// - EvaluationResult: The complete result including decision and reasoning. |
| 13 | + |
| 14 | +use serde::{Deserialize, Serialize}; |
| 15 | +use std::fmt; |
| 16 | + |
| 17 | +// --------------------------------------------------------------------------- |
| 18 | +// DeonticModality — the three pillars of deontic logic |
| 19 | +// --------------------------------------------------------------------------- |
| 20 | + |
| 21 | +/// The three fundamental modalities of deontic logic, mirroring the Idris2 |
| 22 | +/// ABI definition in `src/interface/abi/Types.idr`. |
| 23 | +/// |
| 24 | +/// - `Obligation`: The agent MUST perform the action. |
| 25 | +/// - `Permission`: The agent MAY perform the action. |
| 26 | +/// - `Prohibition`: The agent MUST NOT perform the action. |
| 27 | +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] |
| 28 | +#[repr(u8)] |
| 29 | +pub enum DeonticModality { |
| 30 | + /// The agent is required to perform the action. |
| 31 | + Obligation = 0, |
| 32 | + /// The agent is allowed (but not required) to perform the action. |
| 33 | + Permission = 1, |
| 34 | + /// The agent is forbidden from performing the action. |
| 35 | + Prohibition = 2, |
| 36 | +} |
| 37 | + |
| 38 | +impl fmt::Display for DeonticModality { |
| 39 | + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { |
| 40 | + match self { |
| 41 | + DeonticModality::Obligation => write!(f, "OBLIGATION"), |
| 42 | + DeonticModality::Permission => write!(f, "PERMISSION"), |
| 43 | + DeonticModality::Prohibition => write!(f, "PROHIBITION"), |
| 44 | + } |
| 45 | + } |
| 46 | +} |
| 47 | + |
| 48 | +impl From<&crate::manifest::ConstraintKind> for DeonticModality { |
| 49 | + fn from(kind: &crate::manifest::ConstraintKind) -> Self { |
| 50 | + match kind { |
| 51 | + crate::manifest::ConstraintKind::Obligation => DeonticModality::Obligation, |
| 52 | + crate::manifest::ConstraintKind::Permission => DeonticModality::Permission, |
| 53 | + crate::manifest::ConstraintKind::Prohibition => DeonticModality::Prohibition, |
| 54 | + } |
| 55 | + } |
| 56 | +} |
| 57 | + |
| 58 | +// --------------------------------------------------------------------------- |
| 59 | +// Constraint — a resolved constraint ready for runtime evaluation |
| 60 | +// --------------------------------------------------------------------------- |
| 61 | + |
| 62 | +/// A fully resolved constraint that the evaluation engine checks at runtime. |
| 63 | +/// |
| 64 | +/// This is the ABI-level representation, distinct from the manifest-level |
| 65 | +/// `manifest::Constraint` which is a serialisation format. The ABI constraint |
| 66 | +/// carries a compiled condition predicate. |
| 67 | +#[derive(Debug, Clone, Serialize, Deserialize)] |
| 68 | +pub struct Constraint { |
| 69 | + /// Unique identifier for this constraint. |
| 70 | + pub name: String, |
| 71 | + |
| 72 | + /// The deontic modality governing this constraint. |
| 73 | + pub modality: DeonticModality, |
| 74 | + |
| 75 | + /// The entity the constraint applies to (e.g. "agent", "subsystem"). |
| 76 | + pub subject: String, |
| 77 | + |
| 78 | + /// The action being constrained (e.g. "delete-records", "send-email"). |
| 79 | + pub action: String, |
| 80 | + |
| 81 | + /// An optional condition string. When `None`, the constraint applies |
| 82 | + /// unconditionally. When `Some(pred)`, the constraint only applies |
| 83 | + /// when `pred` evaluates to true in the current context. |
| 84 | + pub condition: Option<String>, |
| 85 | + |
| 86 | + /// Numeric priority for conflict resolution. Higher values win. |
| 87 | + pub priority: i32, |
| 88 | +} |
| 89 | + |
| 90 | +impl From<&crate::manifest::Constraint> for Constraint { |
| 91 | + fn from(mc: &crate::manifest::Constraint) -> Self { |
| 92 | + Constraint { |
| 93 | + name: mc.name.clone(), |
| 94 | + modality: DeonticModality::from(&mc.kind), |
| 95 | + subject: mc.subject.clone(), |
| 96 | + action: mc.action.clone(), |
| 97 | + condition: mc.condition.clone(), |
| 98 | + priority: mc.priority, |
| 99 | + } |
| 100 | + } |
| 101 | +} |
| 102 | + |
| 103 | +// --------------------------------------------------------------------------- |
| 104 | +// AgentAction — an action the agent is attempting to perform |
| 105 | +// --------------------------------------------------------------------------- |
| 106 | + |
| 107 | +/// Represents an action that an agent is requesting permission to perform. |
| 108 | +/// The constraint engine evaluates this against all applicable constraints. |
| 109 | +#[derive(Debug, Clone, Serialize, Deserialize)] |
| 110 | +pub struct AgentAction { |
| 111 | + /// The agent performing the action. |
| 112 | + pub agent_name: String, |
| 113 | + |
| 114 | + /// The action the agent wants to perform (must match constraint `action` fields). |
| 115 | + pub action: String, |
| 116 | + |
| 117 | + /// The subject/target of the action (must match constraint `subject` fields). |
| 118 | + pub subject: String, |
| 119 | + |
| 120 | + /// Key-value context that condition predicates are evaluated against. |
| 121 | + /// For example: `{"user-consent-given": "true", "data-classification": "public"}`. |
| 122 | + pub context: std::collections::HashMap<String, String>, |
| 123 | +} |
| 124 | + |
| 125 | +// --------------------------------------------------------------------------- |
| 126 | +// AuditDecision — the outcome of constraint evaluation |
| 127 | +// --------------------------------------------------------------------------- |
| 128 | + |
| 129 | +/// The decision produced by the constraint engine for a given action. |
| 130 | +/// |
| 131 | +/// - `Permitted`: The action is allowed (no prohibitions apply, or an explicit |
| 132 | +/// permission overrides). |
| 133 | +/// - `Denied`: The action violates one or more prohibitions in strict mode. |
| 134 | +/// - `Escalated`: The violated constraint has priority >= the escalation |
| 135 | +/// threshold, requiring human review. |
| 136 | +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] |
| 137 | +#[repr(u8)] |
| 138 | +pub enum AuditDecision { |
| 139 | + /// The action is permitted to proceed. |
| 140 | + Permitted = 0, |
| 141 | + /// The action is denied due to constraint violation. |
| 142 | + Denied = 1, |
| 143 | + /// The action requires human escalation before proceeding. |
| 144 | + Escalated = 2, |
| 145 | +} |
| 146 | + |
| 147 | +impl fmt::Display for AuditDecision { |
| 148 | + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { |
| 149 | + match self { |
| 150 | + AuditDecision::Permitted => write!(f, "PERMITTED"), |
| 151 | + AuditDecision::Denied => write!(f, "DENIED"), |
| 152 | + AuditDecision::Escalated => write!(f, "ESCALATED"), |
| 153 | + } |
| 154 | + } |
| 155 | +} |
| 156 | + |
| 157 | +// --------------------------------------------------------------------------- |
| 158 | +// EvaluationResult — full evaluation output with reasoning |
| 159 | +// --------------------------------------------------------------------------- |
| 160 | + |
| 161 | +/// The complete result of evaluating an agent action against the constraint set. |
| 162 | +/// |
| 163 | +/// Includes the decision, reasoning trail, and references to the constraints |
| 164 | +/// that influenced the outcome. |
| 165 | +#[derive(Debug, Clone, Serialize, Deserialize)] |
| 166 | +pub struct EvaluationResult { |
| 167 | + /// The action that was evaluated. |
| 168 | + pub action: AgentAction, |
| 169 | + |
| 170 | + /// The final decision: permitted, denied, or escalated. |
| 171 | + pub decision: AuditDecision, |
| 172 | + |
| 173 | + /// Human-readable reasoning explaining why the decision was reached. |
| 174 | + pub reasoning: Vec<String>, |
| 175 | + |
| 176 | + /// Names of constraints that applied to this evaluation. |
| 177 | + pub applicable_constraints: Vec<String>, |
| 178 | + |
| 179 | + /// Names of constraints that were violated (empty if permitted). |
| 180 | + pub violated_constraints: Vec<String>, |
| 181 | + |
| 182 | + /// ISO-8601 timestamp of the evaluation. |
| 183 | + pub timestamp: String, |
| 184 | +} |
| 185 | + |
| 186 | +#[cfg(test)] |
| 187 | +mod tests { |
| 188 | + use super::*; |
| 189 | + |
| 190 | + #[test] |
| 191 | + fn test_deontic_modality_display() { |
| 192 | + assert_eq!(DeonticModality::Obligation.to_string(), "OBLIGATION"); |
| 193 | + assert_eq!(DeonticModality::Permission.to_string(), "PERMISSION"); |
| 194 | + assert_eq!(DeonticModality::Prohibition.to_string(), "PROHIBITION"); |
| 195 | + } |
| 196 | + |
| 197 | + #[test] |
| 198 | + fn test_audit_decision_display() { |
| 199 | + assert_eq!(AuditDecision::Permitted.to_string(), "PERMITTED"); |
| 200 | + assert_eq!(AuditDecision::Denied.to_string(), "DENIED"); |
| 201 | + assert_eq!(AuditDecision::Escalated.to_string(), "ESCALATED"); |
| 202 | + } |
| 203 | + |
| 204 | + #[test] |
| 205 | + fn test_deontic_modality_repr() { |
| 206 | + assert_eq!(DeonticModality::Obligation as u8, 0); |
| 207 | + assert_eq!(DeonticModality::Permission as u8, 1); |
| 208 | + assert_eq!(DeonticModality::Prohibition as u8, 2); |
| 209 | + } |
| 210 | + |
| 211 | + #[test] |
| 212 | + fn test_audit_decision_repr() { |
| 213 | + assert_eq!(AuditDecision::Permitted as u8, 0); |
| 214 | + assert_eq!(AuditDecision::Denied as u8, 1); |
| 215 | + assert_eq!(AuditDecision::Escalated as u8, 2); |
| 216 | + } |
| 217 | + |
| 218 | + #[test] |
| 219 | + fn test_constraint_from_manifest() { |
| 220 | + let mc = crate::manifest::Constraint { |
| 221 | + name: "no-delete".into(), |
| 222 | + kind: crate::manifest::ConstraintKind::Prohibition, |
| 223 | + subject: "agent".into(), |
| 224 | + action: "delete".into(), |
| 225 | + condition: Some("data-critical".into()), |
| 226 | + priority: 80, |
| 227 | + }; |
| 228 | + let c = Constraint::from(&mc); |
| 229 | + assert_eq!(c.modality, DeonticModality::Prohibition); |
| 230 | + assert_eq!(c.name, "no-delete"); |
| 231 | + assert_eq!(c.condition, Some("data-critical".into())); |
| 232 | + } |
| 233 | +} |
0 commit comments