Expand description
Primitive API classification for verifier transfer functions.
The staged verifier still needs semantic summaries for compiler/std primitives whose MIR body does not expose the address or memory effect we want to reason about. This module keeps the name-based recognition in one small registry. Higher layers translate the classified primitive into dependency summaries, forward effects, and SMT assumptions.
Enumsยง
- Primitive
Call - Std/core primitive calls with verifier-specific transfer functions.