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

Both LLVM and Haskell backends work. Zero regressions on the UI test suite with the LLVM backend (1162/1162 baseline). Zero regressions on the UI test suite with the Haskell backend as well. LLVM backend execution ~13x faster (3h vs ~38h, with with 2 workers). Haskell backend execution around the same (10.5 h vs 10 h, with 2 workers again).

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.
• Split top-level lookup functions into concrete (regular [function]) and symbolic ([no-evaluators]) using markdown selectors. In concrete execution, dispatch to map lookups; in symbolic execution, per-program axioms bridge to lookupXKore.
• Generate bridge axioms for lookupFunction, lookupTy, lookupAlloc, and #getBlocks to delegate from the [no-evaluators] wrapper to lookupXKore in the Haskell definition.
• Convert all [no-evaluators] functions that call lookupTyKore directly to concrete/symbolic split with MaybeMap parameter: #getBlocks, readTyConstInt, #staticArrayLenBits, getTyOf, #metadataSize, #metadataSizeAux, #typeProjection, #pointeeProjection, #pointeeProjectionTarget, getArrayElemTypeInfo, #lookupMaybeTy, #sizeOf, #alignOf, #isStaticU8Array, #convertMetadata, #projectedCallTy, #extractOperandType, #decodeValue, #neededBytesForOffsets, #decodeFieldsWithOffsets, #elemSize, #decodeEnumDirectFields, #decodeArrayAllocation, #decodeArrayElements, #decodeSliceAllocation. (multiple commits)
• Update expected test output for new configuration cells.
• Fix test infrastructure for shared LLVM definition (test_decode_value, test_cli_prove_add_module_*).

[mariaKt]

Relevant discussion on slack

[dkcumming]

Nice I like it a lot! I went through each commit and it all makes sense. It is unfortunate there needs to be so much duplication of code for the symbolic and concrete cases. Maybe there would be some solution for that in the future, but it is not too much of a cost to bear for now for the massive performance increase. I think there is a way to remove printing the cells entirely too, not just with noMap replaced. But that is not a big deal for now either.