Struct KernelCall 

pub struct KernelCall { /* private fields */ }

A token that lives exactly as long as ONE outermost kernel call, and that a cache BORROWS.

The soundness rule a conversion or type cache has to obey is not a style note, so it is not written as one. A cache that outlives the environment it decided under is the kernel certifying a judgement that no longer holds, and the way to make that unwritable is to give the cache a lifetime it cannot escape:

use logicaffeine_kernel::term_store::{KernelCall, TypeCache};

let call = KernelCall::begin();
assert!(call.is_outermost());
let types: TypeCache<'_, u32> = TypeCache::new(&call);
assert_eq!((types.hits(), types.misses()), (0, 0));

TypeCache<'call, _> borrows &'call KernelCall, so it cannot be put in a static (that needs 'static), and it cannot be put in a Context without giving Context a lifetime parameter — a change every call site would see and a reviewer could not miss. KernelCall is neither Send nor Sync, so it cannot be smuggled into a global through a Mutex either. The comment becomes a compile error:

use logicaffeine_kernel::term_store::{KernelCall, TypeCache};

fn outlive() -> TypeCache<'static, u32> {
    let call = KernelCall::begin();
    TypeCache::new(&call)
}

fn send<T: Send>() {}
send::<logicaffeine_kernel::term_store::KernelCall>();

What actually invalidates a cached judgement, corrected

Wave 2 recorded this as “Context::pop_scope REMOVES definitions”. That is wrong, and the correction matters because it is the one that says where the danger really is. pop_scope reverts the four ATTRIBUTE databases — instances, coercions, simp rules, hints — and explicitly never a declaration; a def written inside a section survives its end. The call that genuinely removes one is Context::displace, which every add_inductive, add_definition and declare runs on the name it is about to bind, so re-declaring a name deletes the previous definition of it — and a conversion decided while that body was in force is then a stale POSITIVE.

The good news, and the reason a per-call cache needs nothing else: every kernel entry point takes &Context. A shared reference cannot be displaced, extended in place, or popped. So within one outermost kernel call the global environment is FIXED, and only the LOCAL bindings vary — by Context::extend, which returns a NEW Context and may SHADOW. Locals are what EnvId keys; globals need nothing but this lifetime.

Implementations

impl KernelCall

pub fn begin() -> Self

Open a kernel call. The token must be held on the stack for as long as any cache keyed under it.

pub fn is_outermost(&self) -> bool

Whether this is the OUTERMOST kernel call on this thread — the only place a cache should be created, because a cache created deeper is thrown away on every ascent and buys nothing.

pub fn depth() -> usize

How many kernel calls are live on this thread.

Trait Implementations

impl Default for KernelCall

fn default() -> Self

Returns the “default value” for a type.

impl Drop for KernelCall

fn drop(&mut self)

Executes the destructor for this type.