Map cells with static data for LLVM kompile

[mariaKt]

This PR introduces a dual lookup mechanism for static data, using a MaybeMap sort, aiming to avoid per-program LLVM kompile in concrete execution. Program-specific data (functions, types, allocations) is stored in Map cells for LLVM execution, while the existing no-evaluators Kore functions are preserved for the Haskell/booster backend.

Status

LLVM backend works. Haskell/booster backend has a blocking issue, with details in 'booster-lookup-issue.mdandbooster-lookup-issue-proof.txt`.

Commits

• Add MaybeMap sort (noMap | someMap(Map)) and new <functions>, <types>, <memory> cells to the configuration.
• Rename existing lookupFunction/lookupTy/lookupAlloc to lookupFunctionKore/lookupTyKore/lookupAllocKore (keeping [no-evaluators]).
• Add map-based lookup functions (lookupFunctionMap, lookupTyMap, lookupAllocMap) using orDefault for missing keys.
• Add top-level wrapper functions lookupFunction(MaybeMap, Ty) etc. that dispatch to Kore or Map versions.
• Update all rewrite rules in kmir.md and rt/data.md to read the new cells and use the wrapper functions.
• Add symbol(MaybeMap::noMap) and symbol(MaybeMap::someMap) attributes for clean Python integration.
• Build the map cell contents in Python (_make_smir_maps) and skip LLVM kompile in concrete execution.
• Strip map cell contents from Kore output before pretty printing (replace with noMap via top_down KORE traversal).
• Explicitly initialize the map cells to noMap in the symbolic call config to have concrete values instead of unbound Kore variables.

booster-lookup-issue.md
booster-lookup-issue-proof.txt

[mariaKt]

Relevant discussion on slack