Crate planarian_policy 

Planarian policy (SPEC §11): one pure function from a transition and the facts the executor derived to a Decision.

decide has no Proposal parameter, so nothing a proposer writes can reach it except the transition itself (I14). Its order:

1. authorization (§11 caller identity and capabilities),
2. hard rejections (core target, catalog, locked option, allowlists),
3. the per-transition table, then the global floors (including the security floor, which asks an administrator: I16),
4. cumulative-session classification (I11),
5. the autonomy setting, which can only raise a tier to AskFirst and never touches a Reject (I5).

Verified with Verus (SPEC §17a): decide is proved equal to decide_spec, and the properties are proved about decide_spec in proofs. Sets of names are vectors searched linearly, because vstd specifies BTreeSet only for key types with an ordering spec, which String lacks (docs/deviations.md). Run: cargo verus verify -p planarian-policy.

Modules

proofs

The properties SPEC §7 and §17a ask of decide, proved about decide_spec; decide is proved equal to it (its ensures).

Structs

Input

Everything decide reads.

Settings

Owner settings (not manifest options, not proposal fields).

Tables

Shipped tables. Hashed into PolicyVersion.

Constants

POLICY_REVISION

Bumped by hand whenever the decision logic changes; part of PolicyVersion.

Functions

admin_if_exec 🔒

allow_exec 🔒

any_locked

any_non_routine

ask_if_exec 🔒

authorization_of

The authorization of a non-user actor: no capabilities (§11).

authorized

base_tier 🔒

contains_change

contains_model

contains_str

decide

floors 🔒

gen_eq 🔒

is_admin_exec 🔒

is_administrator

is_local_exec 🔒

is_under

is_user_exec 🔒

may_approve

may_grant

override_exec 🔒

own_session_exec 🔒

policy_version

sec_or_ext_exec 🔒

str_eq 🔒

unit_ok_exec 🔒

user_authorization

Phase A’s capability grants (§11): every user acts on their own scope and the user-controllable units; root and planarian-admin members are administrators and approvers. I17 holds because root always is (is_administrator; the proof is proofs::i17_administrators_never_empty).

vetted_exec 🔒