From d7a95df4d9b33d5c7945eb19b94dd5818be113aa Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 13 Nov 2025 12:31:59 +1100 Subject: [PATCH 01/10] refactor kore rule generation to prepare changes --- kmir/src/kmir/kmir.py | 15 ++++++++++++++- kmir/src/kmir/kompile.py | 23 +++++++---------------- 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index c5d629c62..408173e2d 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -11,6 +11,7 @@ from pyk.cterm import CTerm, cterm_symbolic from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable, Subst from pyk.kast.manip import abstract_term_safely, split_config_from +from pyk.kast.outer import KFlatModule, KImport from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore from pyk.kcfg.semantics import DefaultSemantics @@ -261,8 +262,20 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: break_every_step=opts.break_every_step, ) + # produce a module for the lookup functions + from .kompile import make_kore_rules + + equations = make_kore_rules(kmir, smir_info) + _LOGGER.debug(f'Made {len(equations)} equations') + prog_module = KFlatModule(name='KMIR-PROGRAM', imports=(KImport('KMIR'),)) + with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: - prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules) + prover = APRProver( + kcfg_explore, + execute_depth=opts.max_depth, + cut_point_rules=cut_point_rules, + extra_module=prog_module, + ) prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index e6bcaaa33..c6486f818 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -19,6 +19,7 @@ from typing import Any, Final from pyk.kast import KInner + from pyk.kore.syntax import Axiom from .smir import SMIRInfo @@ -117,7 +118,7 @@ def kompile_smir( target_dir.mkdir(parents=True, exist_ok=True) kmir = KMIR(HASKELL_DEF_DIR) - rules = _make_kore_rules(kmir, smir_info) + rules = make_kore_rules(kmir, smir_info) _LOGGER.info(f'Generated {len(rules)} function equations to add to `definition.kore') if symbolic: @@ -216,7 +217,7 @@ def kompile_smir( return KompiledConcrete(llvm_dir=target_llvm_path) -def _make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[str]: # generates kore syntax directly as string +def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: equations = [] # kprint tool is too chatty @@ -275,7 +276,7 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: return functions -def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> str: +def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> Axiom: from pyk.kore.rule import FunctionRule from pyk.kore.syntax import App, SortApp @@ -296,17 +297,7 @@ def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInne uid='fubar', label='fubaz', ) - return '\n'.join( - [ - '', - '', - ( - f'// {fun}({kmir.pretty_print(arg)})' - + (f' => {kmir.pretty_print(result)}' if len(kmir.pretty_print(result)) < 1000 else '') - ), - rule.to_axiom().text, - ] - ) + return rule.to_axiom() def _decode_alloc(smir_info: SMIRInfo, raw_alloc: Any) -> tuple[KInner, KInner]: @@ -326,7 +317,7 @@ def _decode_alloc(smir_info: SMIRInfo, raw_alloc: Any) -> tuple[KInner, KInner]: return alloc_id_term, value.to_kast() -def _insert_rules_and_write(input_file: Path, rules: list[str], output_file: Path) -> None: +def _insert_rules_and_write(input_file: Path, rules: list[Axiom], output_file: Path) -> None: with open(input_file, 'r') as f: lines = f.readlines() @@ -337,7 +328,7 @@ def _insert_rules_and_write(input_file: Path, rules: list[str], output_file: Pat # Insert rules before the endmodule line new_lines.append(f'\n// Generated from file {input_file}\n\n') - new_lines.extend(rules) + new_lines.extend([ax.text for ax in rules]) new_lines.append('\n' + last_line) # Write to output file From fca2df7b825f7e7389ef52affead2a5f4ecb64d7 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 13 Nov 2025 13:26:12 +1100 Subject: [PATCH 02/10] WIP adding default equations in python --- kmir/src/kmir/kompile.py | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index c6486f818..8953b4d44 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -218,7 +218,7 @@ def kompile_smir( def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: - equations = [] + equations = _default_equations(kmir) # kprint tool is too chatty kprint_logger = logging.getLogger('pyk.ktool.kprint') @@ -248,6 +248,30 @@ def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: return equations +def _default_equations(kmir) -> list[Axiom]: + from pyk.kast.inner import KToken, KVariable + + unknown_function = KApply( + 'MonoItemKind::MonoItemFn', + ( + KApply('symbol(_)_LIB_Symbol_String', (KToken('"** UNKNOWN FUNCTION **"', KSort('String')),)), + KApply('defId(_)_BODY_DefId_Int', (KVariable('TY', KSort('Int')),)), + KApply('noBody_BODY_MaybeBody', ()), + ), + ) + default_function = _mk_equation( + kmir, 'lookupFunction', KApply('ty', (KVariable('TY'),)), 'Ty', unknown_function, 'MonoItemKind' + ) + default_alloc = _mk_equation( + kmir, 'lookupAlloc', KVariable('ID'), 'AllocId', KApply('InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KVariable('ID'),)), 'Evaluation' + ) + default_ty = _mk_equation( + kmir, 'lookupTy', KApply('ty', (KVariable('_TY'),)), 'Ty', KApply('TypeInfo::VoidType', ()), 'TypeInfo' + ).let_attrs("priority(99)") + + return [default_function, default_alloc, default_ty] + + def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: functions: dict[int, KInner] = {} From 04b9c3e44919f1fa74158a68610a54409a8ede17 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 13 Nov 2025 20:43:03 +1100 Subject: [PATCH 03/10] Default equations in generated module --- kmir/src/kmir/kompile.py | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 8953b4d44..17e2d5b0a 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -250,6 +250,7 @@ def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: def _default_equations(kmir) -> list[Axiom]: from pyk.kast.inner import KToken, KVariable + from pyk.kore.syntax import App unknown_function = KApply( 'MonoItemKind::MonoItemFn', @@ -261,13 +262,18 @@ def _default_equations(kmir) -> list[Axiom]: ) default_function = _mk_equation( kmir, 'lookupFunction', KApply('ty', (KVariable('TY'),)), 'Ty', unknown_function, 'MonoItemKind' - ) + ).let_attrs(((App('owise')),)) default_alloc = _mk_equation( - kmir, 'lookupAlloc', KVariable('ID'), 'AllocId', KApply('InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KVariable('ID'),)), 'Evaluation' - ) + kmir, + 'lookupAlloc', + KVariable('ID'), + 'AllocId', + KApply('InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KVariable('ID'),)), + 'Evaluation', + ).let_attrs(((App('owise')),)) default_ty = _mk_equation( kmir, 'lookupTy', KApply('ty', (KVariable('_TY'),)), 'Ty', KApply('TypeInfo::VoidType', ()), 'TypeInfo' - ).let_attrs("priority(99)") + ).let_attrs(((App('owise')),)) return [default_function, default_alloc, default_ty] From da67a905e84f436ccb8eff63c06437ff50c2058d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 13 Nov 2025 21:00:39 +1100 Subject: [PATCH 04/10] remove default equations from K code --- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index f45ca88b7..9e3b4808b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -133,26 +133,17 @@ The basic operations of reading and writing those values can use K's "heating" a These functions are global static data accessed from many places, and will be extended for the particular program. -**TODO find a better home for these definitions.** ```k // // function store, Ty -> MonoItemFn - syntax MonoItemKind ::= lookupFunction ( Ty ) [function, total, symbol(lookupFunction)] - // ------------------------------------------------------------ - rule lookupFunction(ty(TY)) => monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(TY), noBody) [owise] // HACK - // cannot be total without a default "error" element. `Ty` is key for both functions and data. + syntax MonoItemKind ::= lookupFunction ( Ty ) [function, total, symbol(lookupFunction), no-evaluators] // // static allocations: AllocId -> AllocData (Value or error) - syntax Evaluation ::= lookupAlloc ( AllocId ) [function, total, symbol(lookupAlloc)] - // ----------------------------------------------------------- - rule lookupAlloc(ID) => InvalidAlloc(ID) [owise] - - syntax Evaluation ::= InvalidAlloc ( AllocId ) + syntax Evaluation ::= lookupAlloc ( AllocId ) [function, total, symbol(lookupAlloc), no-evaluators] + | InvalidAlloc ( AllocId ) // error marker // // static information about the base type interning in the MIR: Ty -> TypeInfo - syntax TypeInfo ::= lookupTy ( Ty ) [function, total, symbol(lookupTy)] - // ----------------------------------------------------- - rule lookupTy(_TY) => typeInfoVoidType [owise] // HACK + syntax TypeInfo ::= lookupTy ( Ty ) [function, total, symbol(lookupTy), no-evaluators] ``` ```k From b0094d5aed2984e392a9b34b6e74a80a26c5ce96 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 14 Nov 2025 10:01:12 +1100 Subject: [PATCH 05/10] FAILING attempt to create equations in kast and convert to kore late --- kmir/src/kmir/kmir.py | 2 +- kmir/src/kmir/kompile.py | 45 ++++++++++++++-------------------------- 2 files changed, 16 insertions(+), 31 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 408173e2d..256ecc941 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -267,7 +267,7 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: equations = make_kore_rules(kmir, smir_info) _LOGGER.debug(f'Made {len(equations)} equations') - prog_module = KFlatModule(name='KMIR-PROGRAM', imports=(KImport('KMIR'),)) + prog_module = KFlatModule(name='KMIR-PROGRAM', sentences=equations, imports=(KImport('KMIR'),)) with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: prover = APRProver( diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 17e2d5b0a..e888996ad 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -8,8 +8,10 @@ from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KSort +from pyk.kast.outer import KRule from pyk.kast.prelude.kint import intToken from pyk.kast.prelude.string import stringToken +from pyk.konvert import krule_to_kore from .build import HASKELL_DEF_DIR, LLVM_DEF_DIR, LLVM_LIB_DIR from .kmir import KMIR @@ -118,7 +120,7 @@ def kompile_smir( target_dir.mkdir(parents=True, exist_ok=True) kmir = KMIR(HASKELL_DEF_DIR) - rules = make_kore_rules(kmir, smir_info) + rules = [krule_to_kore(kmir.definition, r) for r in make_kore_rules(kmir, smir_info)] _LOGGER.info(f'Generated {len(rules)} function equations to add to `definition.kore') if symbolic: @@ -217,7 +219,7 @@ def kompile_smir( return KompiledConcrete(llvm_dir=target_llvm_path) -def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: +def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[KRule]: equations = _default_equations(kmir) # kprint tool is too chatty @@ -248,9 +250,9 @@ def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: return equations -def _default_equations(kmir) -> list[Axiom]: +def _default_equations(kmir) -> list[KRule]: + from pyk.kast.att import AttEntry, Atts, KAtt from pyk.kast.inner import KToken, KVariable - from pyk.kore.syntax import App unknown_function = KApply( 'MonoItemKind::MonoItemFn', @@ -262,7 +264,7 @@ def _default_equations(kmir) -> list[Axiom]: ) default_function = _mk_equation( kmir, 'lookupFunction', KApply('ty', (KVariable('TY'),)), 'Ty', unknown_function, 'MonoItemKind' - ).let_attrs(((App('owise')),)) + ).let_att(KAtt((AttEntry(Atts.OWISE, ()),))) default_alloc = _mk_equation( kmir, 'lookupAlloc', @@ -270,10 +272,10 @@ def _default_equations(kmir) -> list[Axiom]: 'AllocId', KApply('InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KVariable('ID'),)), 'Evaluation', - ).let_attrs(((App('owise')),)) + ).let_att(KAtt((AttEntry(Atts.OWISE, ()),))) default_ty = _mk_equation( kmir, 'lookupTy', KApply('ty', (KVariable('_TY'),)), 'Ty', KApply('TypeInfo::VoidType', ()), 'TypeInfo' - ).let_attrs(((App('owise')),)) + ).let_att(KAtt((AttEntry(Atts.OWISE, ()),))) return [default_function, default_alloc, default_ty] @@ -306,28 +308,11 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: return functions -def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> Axiom: - from pyk.kore.rule import FunctionRule - from pyk.kore.syntax import App, SortApp - - arg_kore = kmir.kast_to_kore(arg, KSort(arg_sort)) - fun_app = App('Lbl' + fun, (), (arg_kore,)) - result_kore = kmir.kast_to_kore(result, KSort(result_sort)) - - assert isinstance(fun_app, App) - rule = FunctionRule( - lhs=fun_app, - rhs=result_kore, - req=None, - ens=None, - sort=SortApp('Sort' + result_sort), - arg_sorts=(SortApp('Sort' + arg_sort),), - anti_left=None, - priority=50, - uid='fubar', - label='fubaz', - ) - return rule.to_axiom() +def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> KRule: + from pyk.kast.inner import KRewrite + + fun_app = KApply(fun, (arg,)) + return KRule(body=KRewrite(fun_app, result)) def _decode_alloc(smir_info: SMIRInfo, raw_alloc: Any) -> tuple[KInner, KInner]: @@ -358,7 +343,7 @@ def _insert_rules_and_write(input_file: Path, rules: list[Axiom], output_file: P # Insert rules before the endmodule line new_lines.append(f'\n// Generated from file {input_file}\n\n') - new_lines.extend([ax.text for ax in rules]) + new_lines.extend([ax.text + '\n' for ax in rules]) new_lines.append('\n' + last_line) # Write to output file From 66e159adbbdfd85600fc41f3272b0b0a11294640 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 18 Nov 2025 18:24:42 +1100 Subject: [PATCH 06/10] Revert "FAILING attempt to create equations in kast and convert to kore late" This reverts commit b0094d5aed2984e392a9b34b6e74a80a26c5ce96. --- kmir/src/kmir/kmir.py | 2 +- kmir/src/kmir/kompile.py | 43 +++++++++++++++++++++++++++------------- 2 files changed, 30 insertions(+), 15 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 256ecc941..408173e2d 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -267,7 +267,7 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: equations = make_kore_rules(kmir, smir_info) _LOGGER.debug(f'Made {len(equations)} equations') - prog_module = KFlatModule(name='KMIR-PROGRAM', sentences=equations, imports=(KImport('KMIR'),)) + prog_module = KFlatModule(name='KMIR-PROGRAM', imports=(KImport('KMIR'),)) with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: prover = APRProver( diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index e888996ad..e1411d6af 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -8,10 +8,8 @@ from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KSort -from pyk.kast.outer import KRule from pyk.kast.prelude.kint import intToken from pyk.kast.prelude.string import stringToken -from pyk.konvert import krule_to_kore from .build import HASKELL_DEF_DIR, LLVM_DEF_DIR, LLVM_LIB_DIR from .kmir import KMIR @@ -120,7 +118,7 @@ def kompile_smir( target_dir.mkdir(parents=True, exist_ok=True) kmir = KMIR(HASKELL_DEF_DIR) - rules = [krule_to_kore(kmir.definition, r) for r in make_kore_rules(kmir, smir_info)] + rules = make_kore_rules(kmir, smir_info) _LOGGER.info(f'Generated {len(rules)} function equations to add to `definition.kore') if symbolic: @@ -219,7 +217,7 @@ def kompile_smir( return KompiledConcrete(llvm_dir=target_llvm_path) -def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[KRule]: +def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[Axiom]: equations = _default_equations(kmir) # kprint tool is too chatty @@ -250,9 +248,9 @@ def make_kore_rules(kmir: KMIR, smir_info: SMIRInfo) -> list[KRule]: return equations -def _default_equations(kmir) -> list[KRule]: - from pyk.kast.att import AttEntry, Atts, KAtt +def _default_equations(kmir) -> list[Axiom]: from pyk.kast.inner import KToken, KVariable + from pyk.kore.syntax import App unknown_function = KApply( 'MonoItemKind::MonoItemFn', @@ -264,7 +262,7 @@ def _default_equations(kmir) -> list[KRule]: ) default_function = _mk_equation( kmir, 'lookupFunction', KApply('ty', (KVariable('TY'),)), 'Ty', unknown_function, 'MonoItemKind' - ).let_att(KAtt((AttEntry(Atts.OWISE, ()),))) + ).let_attrs(((App('owise')),)) default_alloc = _mk_equation( kmir, 'lookupAlloc', @@ -272,10 +270,10 @@ def _default_equations(kmir) -> list[KRule]: 'AllocId', KApply('InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KVariable('ID'),)), 'Evaluation', - ).let_att(KAtt((AttEntry(Atts.OWISE, ()),))) + ).let_attrs(((App('owise')),)) default_ty = _mk_equation( kmir, 'lookupTy', KApply('ty', (KVariable('_TY'),)), 'Ty', KApply('TypeInfo::VoidType', ()), 'TypeInfo' - ).let_att(KAtt((AttEntry(Atts.OWISE, ()),))) + ).let_attrs(((App('owise')),)) return [default_function, default_alloc, default_ty] @@ -308,11 +306,28 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: return functions -def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> KRule: - from pyk.kast.inner import KRewrite - - fun_app = KApply(fun, (arg,)) - return KRule(body=KRewrite(fun_app, result)) +def _mk_equation(kmir: KMIR, fun: str, arg: KInner, arg_sort: str, result: KInner, result_sort: str) -> Axiom: + from pyk.kore.rule import FunctionRule + from pyk.kore.syntax import App, SortApp + + arg_kore = kmir.kast_to_kore(arg, KSort(arg_sort)) + fun_app = App('Lbl' + fun, (), (arg_kore,)) + result_kore = kmir.kast_to_kore(result, KSort(result_sort)) + + assert isinstance(fun_app, App) + rule = FunctionRule( + lhs=fun_app, + rhs=result_kore, + req=None, + ens=None, + sort=SortApp('Sort' + result_sort), + arg_sorts=(SortApp('Sort' + arg_sort),), + anti_left=None, + priority=50, + uid='fubar', + label='fubaz', + ) + return rule.to_axiom() def _decode_alloc(smir_info: SMIRInfo, raw_alloc: Any) -> tuple[KInner, KInner]: From 8362adcc2ea8744f7003fb57e494f852ddcff5d0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 18 Nov 2025 20:26:08 +1100 Subject: [PATCH 07/10] Upload program module before proving (no llvm-kompile) for proofs --- kmir/src/kmir/kmir.py | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 408173e2d..6ffd56995 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -16,11 +16,13 @@ from pyk.kcfg.explore import KCFGExplore from pyk.kcfg.semantics import DefaultSemantics from pyk.kcfg.show import NodePrinter +from pyk.kore.syntax import Import, Module from pyk.ktool.kprove import KProve from pyk.ktool.krun import KRun from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofNodePrinter +from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR from .cargo import cargo_get_smir_json from .kast import ConcreteMode, RandomMode, SymbolicMode, make_call_config from .kparse import KParse @@ -33,7 +35,7 @@ from pyk.cterm.show import CTermShow from pyk.kast.inner import KInner - from pyk.kore.syntax import Pattern + from pyk.kore.syntax import Axiom, Pattern, Sentence from pyk.utils import BugReport from .options import DisplayOpts, ProveRSOpts @@ -136,7 +138,9 @@ def parser(self) -> Parser: return Parser(self.definition) @contextmanager - def kcfg_explore(self, label: str | None = None, terminate_on_thunk: bool = False) -> Iterator[KCFGExplore]: + def kcfg_explore( + self, label: str | None = None, terminate_on_thunk: bool = False, equations: list[Axiom] | None = None + ) -> Iterator[KCFGExplore]: with cterm_symbolic( self.definition, self.definition_dir, @@ -145,6 +149,9 @@ def kcfg_explore(self, label: str | None = None, terminate_on_thunk: bool = Fals id=label if self.bug_report is not None else None, # NB bug report arg.s must be coherent simplify_each=30, ) as cts: + if equations is not None: + sentences: list[Sentence] = [Import('KMIR'), *equations] + cts._kore_client.add_module(Module('KMIR-PROGRAM', sentences), name_as_id=True) yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics(terminate_on_thunk=terminate_on_thunk)) def run_smir( @@ -208,9 +215,7 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: apr_proof = APRProof.read_proof_data(opts.proof_dir, label) smir_info = SMIRInfo.from_file(target_path / 'smir.json') - kmir = KMIR.from_kompiled_kore( - smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path - ) + kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) else: _LOGGER.info(f'Constructing initial proof: {label}') if opts.smir: @@ -232,9 +237,7 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: _LOGGER.info(f'missing-bodies-present={has_missing} count={len(missing_body_syms)}') _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}') - kmir = KMIR.from_kompiled_kore( - smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path - ) + kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) apr_proof = kmir.apr_proof_from_smir( label, smir_info, start_symbol=opts.start_symbol, proof_dir=opts.proof_dir @@ -266,15 +269,19 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: from .kompile import make_kore_rules equations = make_kore_rules(kmir, smir_info) - _LOGGER.debug(f'Made {len(equations)} equations') - prog_module = KFlatModule(name='KMIR-PROGRAM', imports=(KImport('KMIR'),)) - - with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: + _LOGGER.info(f'Adding {len(equations)} equations in a fresh module') + # kcfg_explore will auto-add a module `KMIR-PROGRAM`, + # use that module for the proof by uploading another one that imports it + proof_module = KFlatModule('KMIR-PROVE', imports=(KImport('KMIR-PROGRAM'),)) + + with kmir.kcfg_explore( + label, equations=equations, terminate_on_thunk=opts.terminate_on_thunk + ) as kcfg_explore: prover = APRProver( kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules, - extra_module=prog_module, + extra_module=proof_module, ) prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof From 83c476419e107aa85f08eefc56ad18706b0c1e9c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 18 Nov 2025 20:39:21 +1100 Subject: [PATCH 08/10] no llvm-kompile when symbolic=true in KMIR.from_kompiled_kore --- kmir/src/kmir/kompile.py | 40 ++++------------------------------------ 1 file changed, 4 insertions(+), 36 deletions(-) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index e1411d6af..27a6e09c1 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -122,43 +122,11 @@ def kompile_smir( _LOGGER.info(f'Generated {len(rules)} function equations to add to `definition.kore') if symbolic: - # Create output directories - target_llvmdt_path = target_llvm_lib_path / 'dt' - - _LOGGER.info(f'Creating directories {target_llvmdt_path} and {target_hs_path}') - target_llvmdt_path.mkdir(parents=True, exist_ok=True) + # no llvm-kompile required, HS backend will evaluate the static data lookups + # Create output directory + _LOGGER.info(f'Creating directory {target_hs_path}') target_hs_path.mkdir(parents=True, exist_ok=True) - # Process LLVM definition - _LOGGER.info('Writing LLVM definition file') - llvm_def_file = LLVM_LIB_DIR / 'definition.kore' - llvm_def_output = target_llvm_lib_path / 'definition.kore' - _insert_rules_and_write(llvm_def_file, rules, llvm_def_output) - - # Run llvm-kompile-matching and llvm-kompile for LLVM - # TODO use pyk to do this if possible (subprocess wrapper, maybe llvm-kompile itself?) - # TODO align compilation options to what we use in plugin.py - import subprocess - - _LOGGER.info('Running llvm-kompile-matching') - subprocess.run( - ['llvm-kompile-matching', str(llvm_def_output), 'qbaL', str(target_llvmdt_path), '1/2'], check=True - ) - _LOGGER.info('Running llvm-kompile') - subprocess.run( - [ - 'llvm-kompile', - str(llvm_def_output), - str(target_llvmdt_path), - 'c', - '-O2', - '--', - '-o', - target_llvm_lib_path / 'interpreter', - ], - check=True, - ) - # Process Haskell definition _LOGGER.info('Writing Haskell definition file') hs_def_file = HASKELL_DEF_DIR / 'definition.kore' @@ -174,7 +142,7 @@ def kompile_smir( shutil.copytree(file_path, target_hs_path / file_path.name, dirs_exist_ok=True) kompile_digest.write(target_dir) - return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=target_llvm_lib_path) + return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=LLVM_LIB_DIR) else: target_llvmdt_path = target_llvm_path / 'dt' From 870d69706c8775d27c388c619b9e89e315664772 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 19 Nov 2025 11:52:47 +1100 Subject: [PATCH 09/10] Revert "Upload program module before proving (no llvm-kompile) for proofs" This reverts commit 8362adcc2ea8744f7003fb57e494f852ddcff5d0. --- kmir/src/kmir/kmir.py | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 6ffd56995..408173e2d 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -16,13 +16,11 @@ from pyk.kcfg.explore import KCFGExplore from pyk.kcfg.semantics import DefaultSemantics from pyk.kcfg.show import NodePrinter -from pyk.kore.syntax import Import, Module from pyk.ktool.kprove import KProve from pyk.ktool.krun import KRun from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofNodePrinter -from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR from .cargo import cargo_get_smir_json from .kast import ConcreteMode, RandomMode, SymbolicMode, make_call_config from .kparse import KParse @@ -35,7 +33,7 @@ from pyk.cterm.show import CTermShow from pyk.kast.inner import KInner - from pyk.kore.syntax import Axiom, Pattern, Sentence + from pyk.kore.syntax import Pattern from pyk.utils import BugReport from .options import DisplayOpts, ProveRSOpts @@ -138,9 +136,7 @@ def parser(self) -> Parser: return Parser(self.definition) @contextmanager - def kcfg_explore( - self, label: str | None = None, terminate_on_thunk: bool = False, equations: list[Axiom] | None = None - ) -> Iterator[KCFGExplore]: + def kcfg_explore(self, label: str | None = None, terminate_on_thunk: bool = False) -> Iterator[KCFGExplore]: with cterm_symbolic( self.definition, self.definition_dir, @@ -149,9 +145,6 @@ def kcfg_explore( id=label if self.bug_report is not None else None, # NB bug report arg.s must be coherent simplify_each=30, ) as cts: - if equations is not None: - sentences: list[Sentence] = [Import('KMIR'), *equations] - cts._kore_client.add_module(Module('KMIR-PROGRAM', sentences), name_as_id=True) yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics(terminate_on_thunk=terminate_on_thunk)) def run_smir( @@ -215,7 +208,9 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: apr_proof = APRProof.read_proof_data(opts.proof_dir, label) smir_info = SMIRInfo.from_file(target_path / 'smir.json') - kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) + kmir = KMIR.from_kompiled_kore( + smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path + ) else: _LOGGER.info(f'Constructing initial proof: {label}') if opts.smir: @@ -237,7 +232,9 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: _LOGGER.info(f'missing-bodies-present={has_missing} count={len(missing_body_syms)}') _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}') - kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) + kmir = KMIR.from_kompiled_kore( + smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path + ) apr_proof = kmir.apr_proof_from_smir( label, smir_info, start_symbol=opts.start_symbol, proof_dir=opts.proof_dir @@ -269,19 +266,15 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: from .kompile import make_kore_rules equations = make_kore_rules(kmir, smir_info) - _LOGGER.info(f'Adding {len(equations)} equations in a fresh module') - # kcfg_explore will auto-add a module `KMIR-PROGRAM`, - # use that module for the proof by uploading another one that imports it - proof_module = KFlatModule('KMIR-PROVE', imports=(KImport('KMIR-PROGRAM'),)) - - with kmir.kcfg_explore( - label, equations=equations, terminate_on_thunk=opts.terminate_on_thunk - ) as kcfg_explore: + _LOGGER.debug(f'Made {len(equations)} equations') + prog_module = KFlatModule(name='KMIR-PROGRAM', imports=(KImport('KMIR'),)) + + with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: prover = APRProver( kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules, - extra_module=proof_module, + extra_module=prog_module, ) prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof From 9e72956f61520907743a8d752a51366d67b1a141 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 19 Nov 2025 11:53:45 +1100 Subject: [PATCH 10/10] do not use extra_module in prover invocation --- kmir/src/kmir/kmir.py | 9 --------- 1 file changed, 9 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 408173e2d..60ca1909b 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -11,7 +11,6 @@ from pyk.cterm import CTerm, cterm_symbolic from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable, Subst from pyk.kast.manip import abstract_term_safely, split_config_from -from pyk.kast.outer import KFlatModule, KImport from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore from pyk.kcfg.semantics import DefaultSemantics @@ -262,19 +261,11 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: break_every_step=opts.break_every_step, ) - # produce a module for the lookup functions - from .kompile import make_kore_rules - - equations = make_kore_rules(kmir, smir_info) - _LOGGER.debug(f'Made {len(equations)} equations') - prog_module = KFlatModule(name='KMIR-PROGRAM', imports=(KImport('KMIR'),)) - with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore: prover = APRProver( kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules, - extra_module=prog_module, ) prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof