No-LLVM-kompile approach causes 5x prove performance regression due to kore-rpc fallback

Problem

The issue/no-llvm-kompile-perf-regression branch (based on EXPERIMENT-no-llvm-kompile-updated) attempts to avoid LLVM kompile by splitting inline lookupTy/lookupAlloc/lookupFunction calls out of rule side conditions into two-step rules with #resolved* intermediate terms. This results in a ~5x performance regression in symbolic execution (prove) tests.

Benchmark: iterator-simple test

Root Cause Analysis

Proof topology is nearly identical (master: 3 nodes, current: 4 nodes), and total rewrite steps only increased ~7%. The real bottleneck is kore-rpc fallback:

Master's proof is handled entirely by the booster (fast). The current branch falls back to kore-rpc 64 times — each fallback is orders of magnitude slower than a booster step.

Fallback distribution by rule

Key finding: preserves-definedness is NOT the cause

Adding [preserves-definedness] to all #resolved* rules (both producers and consumers) did not reduce the fallback count. The 64 kore-rpc fallbacks remained identical.

Hypothesis: booster cannot evaluate side conditions on resolved intermediate terms

In master, rules like execStmt have side conditions such as notBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I)))) where the entire expression is evaluated in a single step with the LLVM backend. In the split version, the consumer rule has notBool #isUnionType(TYINFO) where TYINFO is already a concrete TypeInfo value. The booster appears unable to evaluate these function calls on concrete constructor terms, despite the functions being [function, total].

The pattern is consistent: the booster successfully executes the producer rule (which calls lookupTy etc.), but then falls back to kore-rpc for the consumer rule (which evaluates predicates on the resolved value).

Next Steps

1. Investigate why booster cannot evaluate side conditions on #resolved* consumer rules: The functions (#isUnionType, typeInfoVoidType =/=K, etc.) are [function, total] and should be evaluable. This may be a booster limitation with evaluating functions on concrete K terms that were produced by a previous rewrite step rather than by LLVM evaluation.
2. Address at the Haskell backend / booster level rather than continuing to work around it in mir-semantics:
   • Cached server: persistent K Haskell backend server to amortize startup costs
   • Static cell flags: mark configuration cells as static/immutable so the backend can skip unnecessary copying or matching
   • More efficient MAP operations: optimize MAP lookup/update in the Haskell backend

Acceptance Criteria

• Identify the booster limitation causing fallback on #resolved* consumer rules
• Solution implemented at Haskell backend / booster level (not mir-semantics)
• iterator-simple prove performance on par with or better than current master (~57s)

Start by examining the #resolved* consumer rules in kmir.md and rt/data.md, especially execStmt and the listed side conditions, then trace why the booster falls back to kore-rpc on concrete resolved terms. Use the iterator-simple benchmark to compare prove performance with master. Done means identifying the booster limitation, implementing the fix in the Haskell backend or booster, and reaching approximately the master runtime of 57 seconds.