Module rcu_objects 

Allocation identity and ownership resources for RCU proofs.

Verified Properties

Each registration receives a fresh allocation ID within its domain. Persistent block information preserves that ID across publications, including after the physical address is reused. A separate linear permission belongs to the same registration and will be consumed by the retirement protocol.

Registration records identity only: neither block information nor a base retire permission grants access to the allocation or permission to reclaim it. A registered object can retain a client-defined linear resource, whose meaning remains the client’s responsibility.

Structs

RcuBaseRetirePerm

Unique base permission retained until the allocation is retired.

RcuBlockInfo

Persistent identity of one registered allocation, without physical ownership.

RcuDomainAuth

Authoritative allocation registry for one RCU protection domain.

RcuOwnedObject

One allocation’s registration paired with a linear client resource.

Functions

lemma_registration_distinguishes_reused_address

Type Aliases

RcuRegistration

Persistent identity and linear base retire permission from one registration.