feat(cse): full slotStore CSE pipeline passes end-to-end test

Complete pipeline: callee proof → cover path extraction → summary rule
generation via cterm_build_rule → add-module injection → caller reuse.

Key implementation details:
- Uses cterm_build_rule (same as APRProver dependency rules) for
  properly structured KRule with full config cell nesting
- Rule LHS: #execTerminatorCall ~> CONT with function name constraint
- Rule RHS: #setLocalValue(DEST, RET) ~> #continueAt(TARGET)
- Summary injected via CTermSymbolic.add_module(), backend applies
  automatically — no custom_step needed
- Test: double(x)=x+x, callee has 1 cover + 1 stuck (overflow),
  summary rule generated and reuse proof passes

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: Stevengre

kmir/src/kmir/_cse.py

@@ -18,6 +18,8 @@
 
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KRewrite, KSequence, KSort, KToken, KVariable, Subst
+from pyk.kast.att import Atts as AttKeys
+from pyk.kast.att import AttEntry, KAtt
 from pyk.kast.outer import KFlatModule, KImport, KRule
 from pyk.kast.prelude.ml import mlAnd, mlEqualsTrue
 from pyk.proof.reachability import APRProof
@@ -277,70 +279,80 @@ def generate_summary_rules(
     return rules
 
 
+_EXEC_TERMINATOR_CALL = '#execTerminatorCall(_,_,_,_,_,_,_)_KMIR-CONTROL-FLOW_KItem_Ty_MonoItemKind_Operands_Place_MaybeBasicBlockIdx_UnwindAction_Span'
+_SET_LOCAL_VALUE = '#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation'
+_CONTINUE_AT = '#continueAt(_)_KMIR-CONTROL-FLOW_KItem_MaybeBasicBlockIdx'
+_GET_FUNCTION_NAME = 'getFunctionName(_)_KMIR-CONTROL-FLOW_String_MonoItemKind'
+_EQ_STRING = '_==String__STRING-COMMON_Bool_String_String'
+
+
 def _build_summary_rule(
     callee_name: str,
     path: CoverPath,
     path_idx: int,
     init_cterm: CTerm,
 ) -> KRule | None:
-    """Build one K rule for a single execution path."""
+    """Build one K rule for a single execution path.
+
+    Uses cterm_build_rule to construct a properly-structured rule from
+    init CTerm (at function call) → final CTerm (after return).
+    The init CTerm's K_CELL is #execTerminatorCall(...) and the final
+    CTerm's K_CELL is #setLocalValue(DEST, RET) ~> #continueAt(TARGET).
+    """
+    from pyk.cterm.cterm import cterm_build_rule
+
     if path.return_value is None:
         _LOGGER.warning(f'CSE: no return value for {callee_name} path {path_idx}, skipping')
         return None
 
-    # Variables for the rule LHS pattern
-    func_var = KVariable('FUNC', sort=KSort('MonoItemKind'))
-    args_var = KVariable('ARGS', sort=KSort('Operands'))
-    dest_var = KVariable('DEST', sort=KSort('Place'))
-    target_var = KVariable('TARGET', sort=KSort('MaybeBasicBlockIdx'))
-    unwind_var = KVariable('_UNWIND', sort=KSort('UnwindAction'))
-    span_var = KVariable('_SPAN', sort=KSort('Span'))
-    ty_var = KVariable('_TY', sort=KSort('Ty'))
-
-    # LHS: #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, _SPAN)
-    lhs_k = KApply(
-        '#execTerminatorCall',
-        [ty_var, func_var, args_var, dest_var, target_var, unwind_var, span_var],
-    )
-
-    # RHS: #setLocalValue(DEST, RET_VALUE) ~> #execBlockIdx(TARGET)
-    rhs_k = KSequence(
-        [
-            KApply('#setLocalValue', [dest_var, path.return_value]),
-            KApply('#execBlockIdx', [target_var]),
-        ]
-    )
+    # Variables for the rule
+    func_var = KVariable('CSE_FUNC')
+    dest_var = KVariable('CSE_DEST')
+    target_var = KVariable('CSE_TARGET')
+    cont_var = KVariable('CSE_CONT')
+
+    # Build init CTerm: same as init_cterm but with K_CELL = #execTerminatorCall ~> CONT
+    lhs_k = KSequence([
+        KApply(_EXEC_TERMINATOR_CALL, [
+            KVariable('CSE_TY'), func_var, KVariable('CSE_ARGS'),
+            dest_var, target_var, KVariable('CSE_UNWIND'), KVariable('CSE_SPAN'),
+        ]),
+        cont_var,
+    ])
 
-    # Build the rule body as a <k> cell rewrite
-    body = KApply('<generatedTop>', [
-        KApply('<kmir>', [
-            KRewrite(lhs_k, rhs_k),  # <k> cell rewrite — simplified, will need full config
-        ])
+    # Build final CTerm: same config but K_CELL = #setLocalValue(DEST, RET) ~> #continueAt(TARGET)
+    rhs_k = KSequence([
+        KApply(_SET_LOCAL_VALUE, [dest_var, path.return_value]),
+        KApply(_CONTINUE_AT, [target_var]),
     ])
 
-    # For now, build requires clause with function name match
-    func_name_check = KApply(
-        '_==String_',
-        [
-            KApply('getFunctionName', [func_var]),
-            KToken(f'"{callee_name}"', KSort('String')),
-        ],
-    )
+    # Use the init_cterm config as the base, replace K_CELL
+    from pyk.kast.manip import set_cell
+
+    init_config = set_cell(init_cterm.config, 'K_CELL', lhs_k)
+    final_config = set_cell(init_cterm.config, 'K_CELL', rhs_k)
+
+    # Build requires: getFunctionName(FUNC) ==String "callee_name" andBool path constraints
+    func_name_check = KApply(_EQ_STRING, [
+        KApply(_GET_FUNCTION_NAME, [func_var]),
+        KToken(f'"{callee_name}"', KSort('String')),
+    ])
 
-    # Combine function name check with path constraints
-    requires_clauses = [func_name_check]
-    requires_clauses.extend(path.constraints)
+    constraints: list[KInner] = [mlEqualsTrue(func_name_check)]
+    constraints.extend(path.constraints)
 
-    requires = mlEqualsTrue(mlAnd(requires_clauses)) if len(requires_clauses) > 1 else mlEqualsTrue(requires_clauses[0])
+    init_cterm_rule = CTerm(init_config, tuple(constraints))
+    final_cterm_rule = CTerm(final_config)
 
     rule_label = f'cse-summary-{_sanitize_name(callee_name)}-path-{path_idx}'
 
-    return KRule(
-        body=body,
-        requires=requires,
-        ensures=KToken('true', KSort('Bool')),
-        att={'priority': '30', 'label': rule_label},
+    rule, _subst = cterm_build_rule(
+        rule_label,
+        init_cterm_rule,
+        final_cterm_rule,
+        priority=30,
     )
+    return rule
 
 
 def _sanitize_name(name: str) -> str:

kmir/src/tests/integration/test_integration.py

@@ -950,8 +950,40 @@ def test_cse_callee_proof(tmp_path: Path) -> None:
     # become summary rules. The caller's constraints will exclude error paths.
 
     # Step 3: Extract cover paths and verify return value extraction
-    from kmir._cse import extract_cover_paths
+    from kmir._cse import build_summary_module, extract_cover_paths, generate_summary_rules
 
     cover_paths = extract_cover_paths(callee_proof)
     assert len(cover_paths) > 0, 'Should extract at least one cover path'
     assert cover_paths[0].return_value is not None, 'Cover path should have a return value'
+
+    # Step 4: Generate summary rules
+    init_cterm = callee_proof.kcfg.node(callee_proof.init).cterm
+    rules = generate_summary_rules('double', cover_paths, init_cterm)
+    assert len(rules) > 0, 'Should generate at least one summary rule'
+
+    # Step 5: Build summary module
+    module = build_summary_module('double', rules)
+    assert module is not None
+    assert len(module.sentences) > 0
+
+    # Step 6: Prove caller with summary via add-module
+    from pyk.cterm import cterm_symbolic
+    from pyk.kcfg.explore import KCFGExplore
+    from pyk.proof.reachability import APRProver
+
+    from kmir._prove import apr_proof_from_smir
+    from kmir.kmir import KMIRSemantics
+
+    reuse_proof = apr_proof_from_smir(kmir_instance, 'cse-reuse', smir_info, start_symbol='main', proof_dir=tmp_path)
+    with cterm_symbolic(
+        kmir_instance.definition,
+        kmir_instance.definition_dir,
+        llvm_definition_dir=kmir_instance.llvm_library_dir,
+        simplify_each=30,
+    ) as cts:
+        module_name = cts.add_module(module, name_as_id=True)
+        kcfg_explore = KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
+        prover = APRProver(kcfg_explore, execute_depth=10000)
+        prover.advance_proof(reuse_proof, max_iterations=1000)
+
+    assert reuse_proof.passed, f'CSE reuse proof should pass, status={reuse_proof.status}'