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

[Stevengre]

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

Branch	Duration
origin/master	~57s
issue/no-llvm-kompile-perf-regression	~288s

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	Current branch
Total rewrite steps	798	857 (586 + 271)
Booster steps	798 (100%)	793 (92.5%)
Kore-RPC fallback	0 (0%)	64 (7.5%)

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

Count	Rule	Source
44x	#resolvedExecStmt consumer (execStmt)	kmir.md:113
8x	#resolvedOperandConstant consumer	rt/data.md:133
4x	#resolvedCastTransmute consumer	rt/data.md:758
2x	#resolvedDiscriminant consumer	rt/data.md:1191
2x	#resolvedCastPtrToPtr consumer	rt/data.md:1502
2x	#resolvedSetupCalleeClosure consumer	kmir.md
1x	#resolvedCastTransmute (MaybeUninit)	rt/data.md:1877
1x	#resolvedCastTransmute (MaybeUninit)	rt/data.md:1864

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)