Struct PolicyCell 

pub struct PolicyCell { /* private fields */ }

The run policy in force for one run (crates/runtime/spec/PolicyTake.lean §8-62, runtime D28).

One writer and many readers. A change that reaches the run at any safe point waits in the cell, and the run’s driver loop puts the last one in force at SafePoint::BeforeWave and nowhere else; the write gates hold a PolicyReader that they ask once per write. So every call of one wave is judged under one policy, the one in force when the wave began.

Implementations

impl PolicyCell

pub fn new(start: RunPolicy) -> PolicyCell

The cell a run opens with, holding run_started.policy.

pub fn reader(&self) -> PolicyReader

A read-only view of the policy in force, for a write gate.

Trait Implementations

impl Debug for PolicyCell

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

Formats the value using the given formatter.