Struct PluginMeta 

pub struct PluginMeta {
    pub level: SecurityLevel,
    pub held_caps: Vec<CapId>,
}

Plugin security metadata (extractable)

Corresponds to Lean: structure PluginMeta

INVARIANT: held_caps is sorted, no duplicates

Fields

level: SecurityLevel

Security level of this plugin

held_caps: Vec<CapId>

Capabilities held by this plugin (sorted Vec)

Implementations

impl PluginMeta

pub fn empty() -> Self

Create empty plugin metadata (Public level, no capabilities)

Corresponds to Lean: def PluginMeta.empty

pub fn grant_cap(&mut self, cap_id: CapId)

Grant a capability to this plugin (maintains sorted order)

Corresponds to Lean: def PluginMeta.grant_cap Production version: uses binary_search for efficiency

pub fn revoke_cap(&mut self, cap_id: CapId)

Corresponds to Lean: def PluginMeta.grant_cap Uses while-index loops only. Revoke a capability from this plugin

Corresponds to Lean: def PluginMeta.revoke_cap

pub fn holds_cap(&self, cap_id: CapId) -> bool

Check if plugin holds a capability

Corresponds to Lean: def PluginMeta.holds_cap

Trait Implementations

impl Clone for PluginMeta

fn clone(&self) -> PluginMeta

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PluginMeta

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for PluginMeta

fn default() -> Self

Returns the “default value” for a type.

impl PartialEq for PluginMeta

fn eq(&self, other: &PluginMeta) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for PluginMeta

impl StructuralPartialEq for PluginMeta