planarian_policy/
proofs.rs

1//! The properties SPEC §7 and §17a ask of `decide`, proved about
2//! `decide_spec`; `decide` is proved equal to it (its `ensures`).
3
4use crate::*;
5#[allow(unused_imports)]
6use vstd::prelude::*;
7
8verus! {
9
10pub open spec fn is_reject(d: Decision) -> bool {
11    match d {
12        Decision::Reject(_) => true,
13        Decision::Allow { .. } => false,
14    }
15}
16
17/// AskFirst, or refused.
18pub open spec fn asks_or_rejects(d: Decision) -> bool {
19    match d {
20        Decision::Reject(_) => true,
21        Decision::Allow { tier, .. } => tier == Tier::AskFirst,
22    }
23}
24
25/// The tier's rank; a Reject ranks above every tier.
26pub open spec fn strictness(d: Decision) -> int {
27    match d {
28        Decision::Allow { tier, .. } => tier.rank() as int,
29        Decision::Reject(_) => 4,
30    }
31}
32
33/// `x` is the same Reject as `y`, or a tier at least as high as `y`'s.
34pub open spec fn at_least_as_strict(x: Decision, y: Decision) -> bool {
35    (is_reject(y) && x == y) || (!is_reject(x) && !is_reject(y) && strictness(x) >= strictness(y))
36}
37
38/// The approver class of an Allow; AnyApprover for a Reject.
39pub open spec fn approver_of(d: Decision) -> ApproverClass {
40    match d {
41        Decision::Allow { approver, .. } => approver,
42        Decision::Reject(_) => ApproverClass::AnyApprover,
43    }
44}
45
46/// AskFirst for an administrator, or refused.
47pub open spec fn asks_admin_or_rejects(d: Decision) -> bool {
48    match d {
49        Decision::Reject(_) => true,
50        Decision::Allow { tier, approver } => tier == Tier::AskFirst && approver == ApproverClass::Administrator,
51    }
52}
53
54/// The inputs agree on everything `decide` reads except the settings' `max_tier`.
55pub open spec fn same_but_autonomy(a: Input, b: Input) -> bool {
56    &&& *a.transition == *b.transition
57    &&& *a.facts == *b.facts
58    &&& a.known_good == b.known_good
59    &&& a.live_tested == b.live_tested
60    &&& *a.cumulative == *b.cumulative
61    &&& *a.authz == *b.authz
62    &&& a.settings.user_controllable_units == b.settings.user_controllable_units
63    &&& a.settings.user_controllable_changes == b.settings.user_controllable_changes
64    &&& a.settings.user_controllable_options == b.settings.user_controllable_options
65    &&& *a.tables == *b.tables
66    &&& *a.locked == *b.locked
67    &&& a.revert_to == b.revert_to
68}
69
70/// I5: the autonomy setting never turns a Reject into a tier or a tier into
71/// a Reject, never changes a Reject's reason, never yields a tier above itself
72/// other than AskFirst, and raising it never makes a decision stricter.
73pub proof fn i5_autonomy_never_touches_reject(a: Input, b: Input)
74    requires
75        same_but_autonomy(a, b),
76    ensures
77        uncapped_spec(a) == uncapped_spec(b),
78        is_reject(decide_spec(a)) == is_reject(decide_spec(b)),
79        is_reject(decide_spec(a)) ==> decide_spec(a) == decide_spec(b),
80        is_reject(decide_spec(a)) ==> decide_spec(a) == uncapped_spec(a),
81        !is_reject(decide_spec(a)) ==> (strictness(decide_spec(a)) <= a.settings.max_tier.rank()
82            || asks_or_rejects(decide_spec(a))),
83        // The autonomy setting never changes who may approve.
84        approver_of(decide_spec(a)) == approver_of(uncapped_spec(a)),
85        a.settings.max_tier.rank() <= b.settings.max_tier.rank() ==> at_least_as_strict(
86            decide_spec(a),
87            decide_spec(b),
88        ),
89{
90}
91
92/// I11 (classification): when this change's diff, or the session's
93/// cumulative diff, touches a non-Routine option, the decision is AskFirst
94/// or a Reject.
95pub proof fn i11_non_routine_session_asks(i: Input)
96    requires
97        cumulative_spec(i),
98    ensures
99        asks_or_rejects(decide_spec(i)),
100{
101}
102
103/// The inputs agree on everything except the session's cumulative diff.
104pub open spec fn same_but_session(a: Input, b: Input) -> bool {
105    &&& *a.transition == *b.transition
106    &&& *a.facts == *b.facts
107    &&& a.known_good == b.known_good
108    &&& a.live_tested == b.live_tested
109    &&& *a.authz == *b.authz
110    &&& *a.settings == *b.settings
111    &&& *a.tables == *b.tables
112    &&& *a.locked == *b.locked
113    &&& a.revert_to == b.revert_to
114}
115
116/// I11 (monotonicity): a change inside a session is decided at least as
117/// strictly as the same change on its own.
118pub proof fn i11_session_only_raises(a: Input, b: Input)
119    requires
120        same_but_session(a, b),
121        b.cumulative.options.entries@.len() == 0,
122    ensures
123        at_least_as_strict(decide_spec(a), decide_spec(b)),
124{
125    assert(!diff_non_routine(*b.tables, *b.cumulative));
126}
127
128/// The global floors (§11), for every transition kind.
129pub proof fn global_floors(i: Input)
130    ensures
131        i.facts.recovery == Recovery::NonReversible ==> asks_or_rejects(decide_spec(i)),
132        ((i.facts.disruption.session_loss || i.facts.disruption.data_interruption) && !(is_user(i.authz.actor)
133            && own_session(i.authz.actor, *i.facts))) ==> asks_or_rejects(decide_spec(i)),
134        (i.facts.disruption.connectivity_loss && !is_local(i.authz.actor)) ==> asks_or_rejects(decide_spec(i)),
135        (i.facts.other_sessions_affected && (i.facts.disruption.session_loss
136            || i.facts.disruption.connectivity_loss) && !is_admin(*i.authz)) ==> asks_or_rejects(decide_spec(i)),
137{
138}
139
140/// "Own session" is per session: a user whose other session (or no session)
141/// would be disrupted gets the floor, and so does a disruption whose sessions
142/// are not known.
143pub proof fn own_session_is_per_session(i: Input)
144    requires
145        i.facts.disruption.session_loss,
146        i.facts.affected_sessions@.len() != 1 || match i.authz.actor {
147            Actor::User { session, .. } => match session {
148                Some(s) => i.facts.affected_sessions@[0]@ != s@,
149                None => true,
150            },
151            _ => true,
152        },
153    ensures
154        asks_or_rejects(decide_spec(i)),
155{
156}
157
158/// I16 (the `decide` part): a transition whose target generation is below the
159/// security floor is AskFirst for an administrator, or refused, whatever the
160/// autonomy setting, the transition kind, or the caller.
161pub proof fn i16_below_floor_needs_administrator(i: Input)
162    requires
163        i.facts.below_security_floor,
164    ensures
165        asks_admin_or_rejects(decide_spec(i)),
166{
167}
168
169/// An Administrator approver class only ever comes with AskFirst.
170pub proof fn administrator_class_only_on_ask_first(i: Input)
171    ensures
172        approver_of(decide_spec(i)) == ApproverClass::Administrator ==> asks_or_rejects(decide_spec(i)),
173{
174}
175
176/// §11: a non-administrator's override of a Security-sensitive unit is held
177/// for an administrator, never rejected as unauthorized and never run on its
178/// own; other rejections (the core, a lock) still apply.
179pub proof fn security_override_held_for_administrator(i: Input)
180    requires
181        is_override(*i.transition),
182        i.facts.sensitivity.security,
183        is_user(i.authz.actor),
184        !is_admin(*i.authz),
185    ensures
186        decide_spec(i) != Decision::Reject(RejectReason::Unauthorized),
187        asks_admin_or_rejects(decide_spec(i)),
188{
189}
190
191/// §11 (owner gap G16, decided 2026-10-29): a restart of a Security-sensitive
192/// unit runs below AskFirst only when it restores a unit stopped outside
193/// Planarian and not attributed, and the unit is not also External, or is but
194/// has already failed; or when it restarts a failed network-security unit
195/// whose traffic is held (§12d; owner decision, Nov 2).
196pub proof fn security_restart_runs_alone_only_to_restore(i: Input)
197    requires
198        match *i.transition {
199            Transition::RestartUnit(_) => true,
200            _ => false,
201        },
202        i.facts.sensitivity.security,
203    ensures
204        match decide_spec(i) {
205            Decision::Allow { tier, .. } => tier != Tier::AskFirst ==> (i.facts.restores_unattributed_stop
206                && (!i.facts.sensitivity.external || i.facts.restarts_failed_unit)) || i.facts.restarts_held_unit,
207            _ => true,
208        },
209{
210}
211
212/// I19: no approver approves its own proposal, and an Administrator class is
213/// approved only by an administrator; nobody grants a capability to
214/// themselves or one they do not hold.
215pub proof fn i19_no_self_approval(approver: Authorization, proposer: PrincipalId, class: ApproverClass, g: Grant)
216    ensures
217        may_approve_spec(approver, proposer, class) ==> approver.principal != proposer && approver.capabilities.approve,
218        may_approve_spec(approver, proposer, ApproverClass::Administrator) ==> approver.capabilities.administrator,
219        may_grant_spec(approver, proposer, g) ==> approver.principal != g.to && approver.principal != proposer
220            && approver.capabilities.has(g.capability),
221{
222}
223
224/// Neither an agent principal with no journaled start (reserved), nor the
225/// model (until Phase B grants it anything), nor the unattributed actor is
226/// ever authorized: an inferred override never passes through `decide` (§11).
227pub proof fn agents_and_unattributed_are_refused(i: Input)
228    requires
229        i.authz.actor is Agent || i.authz.actor is Model || i.authz.actor is Unattributed,
230    ensures
231        decide_spec(i) == Decision::Reject(RejectReason::Unauthorized),
232{
233}
234
235/// I10, and probe tampering (§17a): a change to a canonical probe's
236/// definition never runs below AskFirst.
237pub proof fn i10_canonical_probe_changes_ask(i: Input)
238    requires
239        i.facts.touches_canonical_probe,
240    ensures
241        asks_or_rejects(decide_spec(i)),
242{
243}
244
245/// Unauthorized callers are refused before anything else is considered.
246pub proof fn unauthorized_is_refused_first(i: Input)
247    requires
248        !authorized_spec(*i.transition, *i.facts, *i.authz, *i.settings),
249    ensures
250        decide_spec(i) == Decision::Reject(RejectReason::Unauthorized),
251{
252}
253
254/// The core is never a target.
255pub proof fn core_is_never_a_target(i: Input)
256    requires
257        i.facts.touches_core || i.facts.sensitivity.core,
258    ensures
259        decide_spec(i) == Decision::Reject(RejectReason::CoreTarget) || decide_spec(i) == Decision::Reject(
260            RejectReason::Unauthorized,
261        ),
262{
263}
264
265/// Only an administrator can clear the recovery interlock (§12c).
266pub proof fn only_administrators_resolve(i: Input)
267    requires
268        i.transition is Resolve,
269    ensures
270        !is_reject(decide_spec(i)) ==> is_admin(*i.authz),
271{
272}
273
274/// A user who is not an administrator cannot change generations, drivers,
275/// models, snapshots or the store.
276pub proof fn users_cannot_change_generations(i: Input)
277    requires
278        is_user(i.authz.actor),
279        !i.authz.capabilities.administrator,
280        i.transition is SwitchGeneration || i.transition is Revert || i.transition is Rollback
281            || i.transition is LoadModel || i.transition is RestoreSnapshot || i.transition is CollectGarbage
282            || i.transition is BindDriver || i.transition is Resolve,
283    ensures
284        decide_spec(i) == Decision::Reject(RejectReason::Unauthorized),
285{
286}
287
288/// I14: the `caller` recorded in the derived facts carries no authority;
289/// only the daemon-established `Authorization` does.
290pub proof fn i14_facts_caller_is_not_authority(a: Input, b: Input)
291    requires
292        *a.transition == *b.transition,
293        a.facts.affected_units == b.facts.affected_units,
294        a.facts.sensitivity == b.facts.sensitivity,
295        a.facts.disruption == b.facts.disruption,
296        a.facts.recovery == b.facts.recovery,
297        a.facts.touches_manifest == b.facts.touches_manifest,
298        a.facts.touches_canonical_probe == b.facts.touches_canonical_probe,
299        a.facts.changes_desired == b.facts.changes_desired,
300        a.facts.touches_core == b.facts.touches_core,
301        a.facts.below_security_floor == b.facts.below_security_floor,
302        a.facts.other_sessions_affected == b.facts.other_sessions_affected,
303        a.facts.affected_sessions == b.facts.affected_sessions,
304        a.facts.restores_unattributed_stop == b.facts.restores_unattributed_stop,
305        a.facts.restarts_failed_unit == b.facts.restarts_failed_unit,
306        a.facts.removes_sensitivity == b.facts.removes_sensitivity,
307        a.facts.removes == b.facts.removes,
308        a.facts.removes_each == b.facts.removes_each,
309        a.facts.restarts_held_unit == b.facts.restarts_held_unit,
310        a.facts.config_diff == b.facts.config_diff,
311        a.known_good == b.known_good,
312        a.live_tested == b.live_tested,
313        *a.cumulative == *b.cumulative,
314        *a.authz == *b.authz,
315        *a.settings == *b.settings,
316        *a.tables == *b.tables,
317        *a.locked == *b.locked,
318        a.revert_to == b.revert_to,
319    ensures
320        decide_spec(a) == decide_spec(b),
321{
322}
323
324/// I17 (A, given root exists): root holds the administrator capability
325/// whatever the group file says, so the set of principals holding it is
326/// never empty; no change to the group can empty it.
327pub proof fn i17_administrators_never_empty(in_admin_group: bool)
328    ensures
329        administrator_spec(Some(0u32), in_admin_group),
330        exists|uid: Option<u32>| #[trigger] administrator_spec(uid, false),
331{
332    assert(administrator_spec(Some(0u32), false));
333}
334
335} // verus!
planarian_policy/proofs.rs

planarian_policy/
proofs.rs
