planarian_schema/
authz.rs

1//! Principals, capabilities and failure posture (§8, §11, §12d).
2
3use crate::ids::{PrincipalId, TxnId};
4use crate::unit::Actor;
5use serde::{Deserialize, Serialize};
6use vstd::prelude::*;
7
8// The authorization types `policy` reads, visible to its proofs.
9verus! {
10
11#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
12#[derive(Serialize, Deserialize)]
13#[verifier::external_derive]
14pub enum Capability {
15    /// Act on units in one's own `Scope::User`.
16    OwnScope,
17    /// Act on units in `services.planarian.userControllable`.
18    UserControllable,
19    Administrator,
20    /// Approve others' AskFirst proposals within one's other capabilities (I19).
21    Approve,
22    /// Propose catalog / model-catalog entries (the only non-human grants in B).
23    Catalog,
24    ModelCatalog,
25    /// Human-only through B; `Merge` needs two distinct approvers.
26    Manifest,
27    Merge,
28}
29
30/// A set of `Capability` values, as flags so the proofs can read it (as
31/// `Sensitivities`). Serialized as the list of members in declaration order.
32#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
33pub struct Capabilities {
34    pub own_scope: bool,
35    pub user_controllable: bool,
36    pub administrator: bool,
37    pub approve: bool,
38    pub catalog: bool,
39    pub model_catalog: bool,
40    pub manifest: bool,
41    pub merge: bool,
42}
43
44impl Capabilities {
45    pub open spec fn has(self, c: Capability) -> bool {
46        match c {
47            Capability::OwnScope => self.own_scope,
48            Capability::UserControllable => self.user_controllable,
49            Capability::Administrator => self.administrator,
50            Capability::Approve => self.approve,
51            Capability::Catalog => self.catalog,
52            Capability::ModelCatalog => self.model_catalog,
53            Capability::Manifest => self.manifest,
54            Capability::Merge => self.merge,
55        }
56    }
57
58    pub fn contains(&self, c: Capability) -> (r: bool)
59        ensures r == self.has(c),
60    {
61        match c {
62            Capability::OwnScope => self.own_scope,
63            Capability::UserControllable => self.user_controllable,
64            Capability::Administrator => self.administrator,
65            Capability::Approve => self.approve,
66            Capability::Catalog => self.catalog,
67            Capability::ModelCatalog => self.model_catalog,
68            Capability::Manifest => self.manifest,
69            Capability::Merge => self.merge,
70        }
71    }
72}
73
74/// Computed by the daemon for each call from `SO_PEERCRED`, logind, group
75/// membership and journaled grants. Never read from a proposal (I14).
76#[derive(Clone, Debug, PartialEq, Eq)]
77#[derive(Serialize, Deserialize)]
78#[verifier::external_derive]
79pub struct Authorization {
80    pub principal: PrincipalId,
81    pub actor: Actor,
82    pub capabilities: Capabilities,
83}
84
85#[derive(Clone, Debug, PartialEq, Eq)]
86#[derive(Serialize, Deserialize)]
87#[verifier::external_derive]
88pub struct Grant {
89    pub to: PrincipalId,
90    pub capability: Capability,
91    pub approved_by: PrincipalId,
92    pub txn: TxnId,
93}
94
95} // verus!
96
97/// The failure posture, declared in the generation (§12d). Phase A ships Standard.
98#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
99pub enum Posture {
100    Relaxed,
101    #[default]
102    Standard,
103    Guarded,
104    Sealed,
105}
106
107#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
108pub enum FailureClass {
109    /// `planariad` did not reach ready within the boot-ready timeout, or was masked or stopped.
110    Absent,
111    /// Reached ready, then died and exhausted its restart budget.
112    Crashed,
113    /// Core hash, journal chain, boot report or signature check failed.
114    Integrity,
115}
116
117impl Capabilities {
118    pub fn of(items: &[Capability]) -> Capabilities {
119        let mut c = Capabilities::default();
120        for i in items {
121            match i {
122                Capability::OwnScope => c.own_scope = true,
123                Capability::UserControllable => c.user_controllable = true,
124                Capability::Administrator => c.administrator = true,
125                Capability::Approve => c.approve = true,
126                Capability::Catalog => c.catalog = true,
127                Capability::ModelCatalog => c.model_catalog = true,
128                Capability::Manifest => c.manifest = true,
129                Capability::Merge => c.merge = true,
130            }
131        }
132        c
133    }
134
135    pub fn members(&self) -> Vec<Capability> {
136        use Capability::*;
137        [OwnScope, UserControllable, Administrator, Approve, Catalog, ModelCatalog, Manifest, Merge]
138            .into_iter()
139            .filter(|c| self.contains(*c))
140            .collect()
141    }
142}
143
144impl Serialize for Capabilities {
145    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
146        self.members().serialize(s)
147    }
148}
149
150impl<'de> Deserialize<'de> for Capabilities {
151    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
152        Ok(Capabilities::of(&Vec::<Capability>::deserialize(d)?))
153    }
154}
planarian_schema/authz.rs

planarian_schema/
authz.rs
