Core primitive-resolution logic parameterized on the address table. See `from_env` (canonical) and `from_env_orig` (LEON) for the entry points.
(env: &KEnv<M>, a: &PrimAddrs)
| 1018 | /// — and build a synthetic `@<hex>` KId for each. That cascades into |
| 1019 | /// spurious `AppTypeMismatch` errors during original-constant |
| 1020 | /// verification. Regenerate stale hashes with |
| 1021 | /// `lake test -- rust-kernel-build-prim-origs`. |
| 1022 | pub fn from_env_orig(env: &KEnv<M>) -> Self { |
| 1023 | Self::from_env_with(env, &PrimAddrs::new_orig()) |
| 1024 | } |
| 1025 | |
| 1026 | /// Resolve canonical primitive KIds from an external address → name |
| 1027 | /// lookup. Lazy IxOn workers call this before any primitive has |
| 1028 | /// necessarily been faulted into their local KEnv, so Meta-mode KIds |
| 1029 | /// still use the real serialized Lean names instead of synthetic |
| 1030 | /// `@<hex>` fallbacks. |
| 1031 | pub fn from_addr_names<F>(mut name_for_addr: F) -> Self |