Struct RevocationState 

pub struct RevocationState { /* private fields */ }

Revocation epoch tracking

Corresponds to Lean: structure RevocationState

INVARIANTS:

• caps is sorted by CapId, no duplicate IDs
• caps[i].0 == caps[i].1.id() for all entries (keys match cap IDs)
• Parent IDs are always less than child IDs (ParentLt)
• Valid capabilities have valid parents (ValidParentPresent)
• children_index is consistent with parent relationships in caps (ChildrenIndexConsistent)
• children_index is complete: every cap with a parent is in the index (ChildrenIndexComplete)

Implementations

impl RevocationState

pub fn empty() -> Self

Create empty revocation state

Corresponds to Lean: def RevocationState.empty : RevocationState

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

Helper: Find insertion point for sorted insert using binary search

Check if capability exists and is valid

Corresponds to Lean: def RevocationState.is_valid

pub fn get(&self, cap_id: CapId) -> Option<&Capability>

Get a capability by ID

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

Check if the table contains a capability

pub fn revoke(&self, cap_id: CapId) -> Self

Revoke capability by ID (single cap only)

Corresponds to Lean: def RevocationState.revoke

Returns the new state with the capability revoked. If the capability doesn’t exist, returns the state unchanged.

pub fn revoke_mut(&mut self, cap_id: CapId) -> Result<(), KernelError>

Revoke capability by ID (mutating version)

Errors

Returns KernelError::CapNotFound if the capability ID is not in the table.

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

Check if ancestorId is in the parent chain of capId

Corresponds to Lean: def RevocationState.has_ancestor

Uses a fuel parameter for termination (ParentLt guarantees termination with fuel = capId).

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

Check if cap_id is in the revoke set (id == cap_id OR has cap_id as ancestor)

Corresponds to Lean: def RevocationState.in_revoke_set

pub fn revoke_transitive(&self, cap_id: CapId) -> Self

Revoke capability and all descendants transitively

Corresponds to Lean: def RevocationState.revoke_transitive

Sets valid=false on capId and any cap whose parent chain includes capId.

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

Revoke capability and all descendants transitively (mutating version)

pub fn insert(&self, cap: Capability) -> Result<Self, KernelError>

Insert a capability (returns error on collision)

Corresponds to Lean: def RevocationState.insert

SECURITY: This function MUST check for ID collision to maintain the uniqueness invariant and prevent capability forgery via replacement.

Also maintains children_index for O(log n) revocation.

Errors

Returns KernelError::CapIdCollision if a capability with the same ID already exists.

pub fn insert_mut(&mut self, cap: Capability) -> Result<(), KernelError>

Insert a capability (mutating version)

Also maintains children_index for O(log n) revocation.

Errors

Returns KernelError::CapIdCollision if a capability with the same ID already exists.

pub fn revoke_transitive_fast(&self, cap_id: CapId) -> Self

Add a child to the children_index (maintains sorted order)

Rebuilds the index using only Vec::new/push/len and array indexing. Semantically identical to the production version above. Revoke capability and all descendants transitively (O(k) optimized)

Corresponds to Lean: def RevocationState.revoke_transitive_fast

Uses children_index for O(k) traversal where k = number of descendants.

pub fn revoke_transitive_fast_mut( &mut self, cap_id: CapId, ) -> Result<(), KernelError>

Revoke capability and all descendants transitively (O(k) optimized, mutating)

Errors

Returns KernelError::CapNotFound if the capability does not exist.

pub fn epoch(&self) -> u64

Get the current revocation epoch

pub fn cap_count(&self) -> usize

Get the number of capabilities

pub fn valid_caps(&self) -> Vec<(CapId, Capability)>

Get all valid capabilities

pub fn cap_ids(&self) -> Vec<CapId>

Get all capability IDs

pub fn iter(&self) -> Iter<'_, (CapId, Capability)>

Iterate over all capabilities

Returns a slice iterator over (CapId, Capability) pairs. This provides compatibility with code that uses .iter() on the caps.

pub fn any_valid_targeting(&self, target: ResourceId) -> bool

Check if any valid capability targets the given resource

SECURITY: This check is CRITICAL for apply_free. If any valid capability targets an address, freeing that address would create a USE-AFTER-FREE vulnerability (dangling capability).

Corresponds to Lean: Memory safety guard in apply_free

Trait Implementations

impl Clone for RevocationState

fn clone(&self) -> RevocationState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RevocationState

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

Formats the value using the given formatter.

impl Default for RevocationState

fn default() -> Self

Returns the “default value” for a type.