Struct OnceImpl 

pub struct OnceImpl<V: 'static, F: ValueInvariant<V>> { /* private fields */ }

A synchronization primitive which can nominally be written to only once.

This type is a thread-safe Once, and can be used in statics. In many simple cases, you can use [LazyLock<T, F>] instead to get the benefits of this type with less effort: LazyLock<T, F> “looks like” &T because it initializes with F on deref! Where OnceLock shines is when LazyLock is too simple to support a given case, as LazyLock doesn’t allow additional inputs to its function after you call [LazyLock::new(|| ...)].

A OnceLock can be thought of as a safe abstraction over uninitialized data that becomes initialized once written.

Examples

static MY_ONCE: Once<i32> = Once::new();

let value = MY_ONCE.get();
assert(value.is_some());   // unsatisfied precondition, as MY_ONCE is uninitialized.

Implementations

impl<V: 'static, F: ValueInvariant<V>> OnceImpl<V, F>

pub closed spec fn wf(&self) -> bool

impl<V, F: ValueInvariant<V>> OnceImpl<V, F>

pub closed spec fn inv(&self) -> F

pub const exec fn new(Ghost(f): Ghost<F>) -> r : Self

ensures

r.wf(),

r.inv() == f,

Creates a new uninitialized Once.

pub exec fn init(&self, v: V)

requires

F::inv(v),

self.wf(),

Initializes the Once with the given value v.

pub exec fn get<'a>(&'a self) -> r : Option<&'a V>

requires

self.wf(),

ensures

self.wf(),

r matches Some(res) ==> F::inv(*res),

Try to get the value stored in the Once. A Option::Some is returned if the cell is initialized; otherwise, Option::None is returned.

Trait Implementations

impl<V, F: ValueInvariant<V>> Send for OnceImpl<V, F>

impl<V, F: ValueInvariant<V>> Sync for OnceImpl<V, F>