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 LLVM UI test suite (1162/1162 baseline). Zero regressions on the Haskell prove UI test suite so far (in progress). LLVM execution ~14x faster (5.5h with 1 worker, vs ~38h with with 2 workers)

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