Struct CpuLocalAuth 

pub struct CpuLocalAuth<V> { /* private fields */ }

Authoritative logical contents of one CPU-local object.

The domain is fixed at allocation time. Updating a value requires both this authority and the matching CpuLocalPointsTo, so the executable invariant cannot change a CPU’s entry without its exclusive per-CPU permission.

Implementations

impl<V> CpuLocalAuth<V>

pub proof fn new(initial: Map<CpuId, V>) -> tracked res : (CpuLocalAuth<V>, CpuLocalPointsToSet<V>)

ensures

res.0.id() == res.1.id(),

res.0@ == initial,

res.1@ == initial,

res.0.cpus() == initial.dom(),

res.1.cpus() == initial.dom(),

Allocates proof state for CPU-local contents described by initial.

Allocation returns the authoritative state and exclusive ownership of every points-to resource. No executable storage is allocated by this proof function.

pub closed spec fn id(&self) -> Loc

Identity shared by the authority and all of its points-to resources.

pub open spec fn cpus(&self) -> Set<CpuId>

{ self@.dom() }

CPUs represented by this CPU-local object.

pub open spec fn value(&self, cpu: CpuId) -> V

recommends

self.cpus().contains(cpu),

{ self@[cpu] }

The value currently associated with cpu.

pub open spec fn covers(&self, cpus: Set<CpuId>) -> bool

{ self.cpus() == cpus }

Whether this authority contains exactly the configured CPU set.

Trait Implementations

impl<V> View for CpuLocalAuth<V>

closed spec fn view(&self) -> Self::V

type V = Map<CpuId, V>