From a87d5ded3d04153a3e6ae64d6575dfccf44f2a27 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 01:38:22 +0000 Subject: [PATCH 01/27] pyk/ktool/{claim_loader,kprove}: rename KProve.{get_claim_modules => parse_modules} --- pyk/src/pyk/ktool/claim_loader.py | 6 +++--- pyk/src/pyk/ktool/kprove.py | 18 +++++++++--------- .../integration/kprove/test_emit_json_spec.py | 2 +- pyk/src/tests/integration/proof/test_imp.py | 8 ++++---- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/pyk/src/pyk/ktool/claim_loader.py b/pyk/src/pyk/ktool/claim_loader.py index 451bccff393..96757fd1268 100644 --- a/pyk/src/pyk/ktool/claim_loader.py +++ b/pyk/src/pyk/ktool/claim_loader.py @@ -69,9 +69,9 @@ def load_claims( if not cache_hit: _LOGGER.info('Generating claim modules') - module_list = self._kprove.get_claim_modules( - spec_file=spec_file, - spec_module_name=spec_module_name, + module_list = self._kprove.parse_modules( + file_path=spec_file, + module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector, type_inference_mode=type_inference_mode, diff --git a/pyk/src/pyk/ktool/kprove.py b/pyk/src/pyk/ktool/kprove.py index 8abb039ca91..a65a474dbc1 100644 --- a/pyk/src/pyk/ktool/kprove.py +++ b/pyk/src/pyk/ktool/kprove.py @@ -255,19 +255,19 @@ def prove_claim( depth=depth, ) - def get_claim_modules( + def parse_modules( self, - spec_file: Path, - spec_module_name: str | None = None, + file_path: Path, + module_name: str | None = None, include_dirs: Iterable[Path] = (), md_selector: str | None = None, type_inference_mode: TypeInferenceMode | None = None, ) -> KFlatModuleList: - with self._temp_file(prefix=f'{spec_file.name}.parsed.json.') as ntf: + with self._temp_file(prefix=f'{file_path.name}.parsed.json.') as ntf: _kprove( - spec_file=spec_file, + spec_file=file_path, kompiled_dir=self.definition_dir, - spec_module_name=spec_module_name, + spec_module_name=module_name, include_dirs=include_dirs, md_selector=md_selector, output=KProveOutput.JSON, @@ -288,9 +288,9 @@ def get_claim_index( md_selector: str | None = None, type_inference_mode: TypeInferenceMode | None = None, ) -> ClaimIndex: - module_list = self.get_claim_modules( - spec_file=spec_file, - spec_module_name=spec_module_name, + module_list = self.parse_modules( + file_path=spec_file, + module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector, type_inference_mode=type_inference_mode, diff --git a/pyk/src/tests/integration/kprove/test_emit_json_spec.py b/pyk/src/tests/integration/kprove/test_emit_json_spec.py index db0f24da335..7302b751127 100644 --- a/pyk/src/tests/integration/kprove/test_emit_json_spec.py +++ b/pyk/src/tests/integration/kprove/test_emit_json_spec.py @@ -31,7 +31,7 @@ def _update_symbol_table(symbol_table: SymbolTable) -> None: @pytest.fixture def spec_module(self, kprove: KProve) -> KFlatModule: spec_file = K_FILES / 'looping-spec.k' - kfml = kprove.get_claim_modules(spec_file) + kfml = kprove.parse_modules(spec_file) module = kfml.modules[0] claim = module.claims[0] claim = claim.let(body=remove_generated_cells(claim.body), att=EMPTY_ATT) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 55ef85ca96a..90dca214a1e 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -893,7 +893,7 @@ def test_all_path_reachability_prove( tmp_path_factory: TempPathFactory, ) -> None: proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, @@ -930,7 +930,7 @@ def test_terminal_node_subsumption( claim_id: str = 'terminal-node-subsumption' cut_rules: Iterable[str] = [] proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, @@ -1441,7 +1441,7 @@ def test_all_path_reachability_prove_parallel( create_prover: Callable[[int, Iterable[str]], Prover], ) -> None: proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, @@ -1480,7 +1480,7 @@ def test_all_path_reachability_prove_parallel_resources( claim_id = 'addition-1' proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, From fc07a70cf3ef5466c821995daa56f54b9af5b0c6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 04:24:11 +0000 Subject: [PATCH 02/27] pyk/konvert/_kast_to_kore: minor refactoring --- pyk/src/pyk/konvert/_kast_to_kore.py | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 4ee6f28fe95..31b5013df16 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -208,17 +208,11 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: top_level_kore_sort = SortApp('SortGeneratedTopCell') top_level_k_sort = KSort('GeneratedTopCell') + + kore_lhs = kast_to_kore(definition, krule_lhs, sort=top_level_k_sort) # The backend does not like rewrite rules without a precondition - if len(krule_lhs_constraints) > 0: - kore_lhs: Pattern = kast_to_kore(definition, krule_lhs, sort=top_level_k_sort) - else: - kore_lhs = And( - top_level_kore_sort, - ( - kast_to_kore(definition, krule_lhs, sort=top_level_k_sort), - Top(top_level_kore_sort), - ), - ) + if len(krule_lhs_constraints) == 0: + kore_lhs = And(top_level_kore_sort, (kore_lhs, Top(top_level_kore_sort))) kore_rhs: Pattern = kast_to_kore(definition, krule_rhs, sort=top_level_k_sort) From be60d212d9ef53c3dec460942ef2456b78bf27bb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 05:02:52 +0000 Subject: [PATCH 03/27] pyk/tests/konvert/test_simple_proofs: add failing test of konverting a functional rule --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 4 ++++ pyk/src/tests/integration/test-data/k-files/simple-proofs.k | 3 +++ 2 files changed, 7 insertions(+) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 4c4421ff89b..713a0363a2b 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -536,6 +536,10 @@ 'SIMPLE-PROOFS.foo-to-baz-owise', r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})))), Var'Unds'Gen0 : SortStateCell{}, Var'Unds'Gen1 : SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBaz{}, SortKItem{}}(Lblbaz{}()), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})))), Var'Unds'Gen0 : SortStateCell{}, Var'Unds'Gen1 : SortGeneratedCounterCell{})) [priority{}("200"), label{}("SIMPLE-PROOFS.foo-to-baz-owise")]""", ), + ( + 'SIMPLE-PROOFS.simple-func', + r"""axiom{} \rewrites{SortKItem{}}(\and{SortKItem{}}(LblsimpleFunc{}(), \top{SortKItem{}}()), inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3"))) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func")]""", + ), ) KRULE_TO_KORE_EXPLICIT_DATA: Final = ( diff --git a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k index 81375ad158c..38e40ccb5f0 100644 --- a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k +++ b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k @@ -50,4 +50,7 @@ module SIMPLE-PROOFS syntax Foo ::= abcd(K) [symbol(abcd)] + syntax KItem ::= simpleFunction() [symbol(simpleFunc), function, total] + rule [simple-func]: simpleFunction() => 3 + endmodule From 967b79ae461d6ae42cf28ea5fcae3a107ef4eb04 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 05:03:12 +0000 Subject: [PATCH 04/27] pyk/kast/outer: add simple table of function labels to KDefinition --- pyk/src/pyk/kast/outer.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 5e48cab209a..a543dca40e1 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1117,6 +1117,11 @@ def functions(self) -> tuple[KProduction, ...]: """Returns the `KProduction` which are function declarations transitively imported by the main module of this definition.""" return tuple(func for module in self.modules for func in module.functions) + @cached_property + def function_labels(self) -> tuple[str, ...]: + """Returns the label names of all the `KProduction` which are function symbols for all modules in this definition.""" + return tuple(func.klabel.name for func in self.functions if func.klabel is not None) + @cached_property def constructors(self) -> tuple[KProduction, ...]: """Returns the `KProduction` which are constructor declarations transitively imported by the main module of this definition.""" From dd4a8b3704121193e979752860e77301f8a6fb0d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 05:03:28 +0000 Subject: [PATCH 05/27] pyk/konvert/_kast_to_kore: support simple translation of functional rules to kore --- pyk/src/pyk/konvert/_kast_to_kore.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 31b5013df16..a0e11918e0a 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -206,8 +206,11 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: krule_lhs = mlAnd([krule_lhs_config] + krule_lhs_constraints) krule_rhs = mlAnd([krule_rhs_config] + krule_rhs_constraints) - top_level_kore_sort = SortApp('SortGeneratedTopCell') + # Assume it's a semantic rule, but more specific sort for functional rules top_level_k_sort = KSort('GeneratedTopCell') + if isinstance(krule_lhs_config, KApply) and krule_lhs_config.label.name in definition.function_labels: + top_level_k_sort = definition.sort_strict(krule_lhs_config) + top_level_kore_sort = _ksort_to_kore(top_level_k_sort) kore_lhs = kast_to_kore(definition, krule_lhs, sort=top_level_k_sort) # The backend does not like rewrite rules without a precondition From a1b6e4d641c7d610053a28efacaeaaa55eb7d7c8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 05:29:32 +0000 Subject: [PATCH 06/27] pyk/tests/integration/konvert/test_simple_proofs: sss --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 2 +- pyk/src/tests/integration/test-data/k-files/simple-proofs.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 713a0363a2b..a80f20f86d4 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -538,7 +538,7 @@ ), ( 'SIMPLE-PROOFS.simple-func', - r"""axiom{} \rewrites{SortKItem{}}(\and{SortKItem{}}(LblsimpleFunc{}(), \top{SortKItem{}}()), inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3"))) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblsimpleFunc{}(), \top{SortInt{}}()), \dv{SortInt{}}("3")) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func")]""", ), ) diff --git a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k index 38e40ccb5f0..da071b55a71 100644 --- a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k +++ b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k @@ -50,7 +50,7 @@ module SIMPLE-PROOFS syntax Foo ::= abcd(K) [symbol(abcd)] - syntax KItem ::= simpleFunction() [symbol(simpleFunc), function, total] + syntax Int ::= simpleFunction() [symbol(simpleFunc), function, total] rule [simple-func]: simpleFunction() => 3 endmodule From 2f7fe10a34789a342911ee7689cf7803e4fd51cb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 11:51:25 +0000 Subject: [PATCH 07/27] pyk/tests/integration/konvert/test_simple_proofs: add test of requires clause translation for functional rule --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index a80f20f86d4..d3173bd8761 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -540,6 +540,10 @@ 'SIMPLE-PROOFS.simple-func', r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblsimpleFunc{}(), \top{SortInt{}}()), \dv{SortInt{}}("3")) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func")]""", ), + ( + 'SIMPLE-PROOFS.simple-func-req-1', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX : SortInt{}, \dv{SortInt{}}("0")))), \dv{SortInt{}}("0")) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func-req-1")]""", + ), ) KRULE_TO_KORE_EXPLICIT_DATA: Final = ( From 30c4274148c275177fbe09788e714b375f519a52 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 11:55:27 +0000 Subject: [PATCH 08/27] pyk/tests/integration/konvert/test_simple_proofs: add test of simplification rules to konvert --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index d3173bd8761..9c0987b6925 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -544,6 +544,14 @@ 'SIMPLE-PROOFS.simple-func-req-1', r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX : SortInt{}, \dv{SortInt{}}("0")))), \dv{SortInt{}}("0")) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func-req-1")]""", ), + ( + 'SIMPLE-PROOFS.simple-func-simplification', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [label{}("SIMPLE-PROOFS.simple-func-simplification"), simplification{}("")]""", + ), + ( + 'SIMPLE-PROOFS.simple-func-simplification-prio', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [label{}("SIMPLE-PROOFS.simple-func-simplification-prio"), simplification{}("38")]""", + ), ) KRULE_TO_KORE_EXPLICIT_DATA: Final = ( From 8092e50e542e9287a33601ce53ae01c81e250f7f Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 9 Nov 2024 11:58:18 +0000 Subject: [PATCH 09/27] pyk/tests/integration/konvert/test_simple_proofs: priority attribute after others --- .../tests/integration/konvert/test_simple_proofs.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 9c0987b6925..636fba557ec 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -526,23 +526,23 @@ KRULE_TO_KORE_DATA: Final = ( ( 'SIMPLE-PROOFS.foo-to-bar', - r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'DotVar2 : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{}))), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'DotVar2 : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [priority{}("50"), label{}("SIMPLE-PROOFS.foo-to-bar")]""", + r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'DotVar2 : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{}))), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'DotVar2 : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [label{}("SIMPLE-PROOFS.foo-to-bar"), priority{}("50")]""", ), ( 'SIMPLE-PROOFS.foo-to-bar-false', - r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \and{SortGeneratedTopCell{}}(\equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{})), \bottom{SortGeneratedTopCell{}}())), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [priority{}("30"), label{}("SIMPLE-PROOFS.foo-to-bar-false")]""", + r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \and{SortGeneratedTopCell{}}(\equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{})), \bottom{SortGeneratedTopCell{}}())), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [label{}("SIMPLE-PROOFS.foo-to-bar-false"), priority{}("30")]""", ), ( 'SIMPLE-PROOFS.foo-to-baz-owise', - r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})))), Var'Unds'Gen0 : SortStateCell{}, Var'Unds'Gen1 : SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBaz{}, SortKItem{}}(Lblbaz{}()), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})))), Var'Unds'Gen0 : SortStateCell{}, Var'Unds'Gen1 : SortGeneratedCounterCell{})) [priority{}("200"), label{}("SIMPLE-PROOFS.foo-to-baz-owise")]""", + r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})))), Var'Unds'Gen0 : SortStateCell{}, Var'Unds'Gen1 : SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBaz{}, SortKItem{}}(Lblbaz{}()), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'DotVar1 : SortK{})))), Var'Unds'Gen0 : SortStateCell{}, Var'Unds'Gen1 : SortGeneratedCounterCell{})) [label{}("SIMPLE-PROOFS.foo-to-baz-owise"), priority{}("200")]""", ), ( 'SIMPLE-PROOFS.simple-func', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblsimpleFunc{}(), \top{SortInt{}}()), \dv{SortInt{}}("3")) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblsimpleFunc{}(), \top{SortInt{}}()), \dv{SortInt{}}("3")) [label{}("SIMPLE-PROOFS.simple-func"), priority{}("50")]""", ), ( 'SIMPLE-PROOFS.simple-func-req-1', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX : SortInt{}, \dv{SortInt{}}("0")))), \dv{SortInt{}}("0")) [priority{}("50"), label{}("SIMPLE-PROOFS.simple-func-req-1")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX : SortInt{}, \dv{SortInt{}}("0")))), \dv{SortInt{}}("0")) [label{}("SIMPLE-PROOFS.simple-func-req-1"), priority{}("50")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification', From d3ccdfedd967f6b401e642322c575679eb57149e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 01:02:47 +0000 Subject: [PATCH 10/27] pyk/kast/manip: allow bool_to_ml_pred to specify the target sort --- pyk/src/pyk/kast/manip.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kast/manip.py b/pyk/src/pyk/kast/manip.py index 7a56ab62e60..30c59421b6c 100644 --- a/pyk/src/pyk/kast/manip.py +++ b/pyk/src/pyk/kast/manip.py @@ -102,15 +102,15 @@ def fun(term: KInner) -> KInner: return fun -def bool_to_ml_pred(kast: KInner) -> KInner: +def bool_to_ml_pred(kast: KInner, sort: str | KSort = GENERATED_TOP_CELL) -> KInner: def _bool_constraint_to_ml(_kast: KInner) -> KInner: if _kast == TRUE: return mlTop() if _kast == FALSE: return mlBottom() - return mlEqualsTrue(_kast) + return mlEqualsTrue(_kast, sort=sort) - return mlAnd([_bool_constraint_to_ml(cond) for cond in flatten_label('_andBool_', kast)]) + return mlAnd([_bool_constraint_to_ml(cond) for cond in flatten_label('_andBool_', kast)], sort=sort) def ml_pred_to_bool(kast: KInner, unsafe: bool = False) -> KInner: From 8dbaa741390fce934d5fdf36abca281137b32835 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 01:03:38 +0000 Subject: [PATCH 11/27] pyk/konvert/_kast_to_kore: allow translating functional rules from Kast to Kore --- pyk/src/pyk/konvert/_kast_to_kore.py | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index a0e11918e0a..eff5462dc68 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -201,10 +201,6 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: krule_body = krule.body krule_lhs_config = extract_lhs(krule_body) krule_rhs_config = extract_rhs(krule_body) - krule_lhs_constraints = [bool_to_ml_pred(c) for c in flatten_label('_andBool_', krule.requires) if not c == TRUE] - krule_rhs_constraints = [bool_to_ml_pred(c) for c in flatten_label('_andBool_', krule.ensures) if not c == TRUE] - krule_lhs = mlAnd([krule_lhs_config] + krule_lhs_constraints) - krule_rhs = mlAnd([krule_rhs_config] + krule_rhs_constraints) # Assume it's a semantic rule, but more specific sort for functional rules top_level_k_sort = KSort('GeneratedTopCell') @@ -212,13 +208,23 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: top_level_k_sort = definition.sort_strict(krule_lhs_config) top_level_kore_sort = _ksort_to_kore(top_level_k_sort) - kore_lhs = kast_to_kore(definition, krule_lhs, sort=top_level_k_sort) + krule_lhs_constraints = [ + bool_to_ml_pred(c, sort=top_level_k_sort) for c in flatten_label('_andBool_', krule.requires) if not c == TRUE + ] + krule_rhs_constraints = [ + bool_to_ml_pred(c, sort=top_level_k_sort) for c in flatten_label('_andBool_', krule.ensures) if not c == TRUE + ] + + kast_lhs = mlAnd([krule_lhs_config] + krule_lhs_constraints, sort=top_level_k_sort) + kast_rhs = mlAnd([krule_rhs_config] + krule_rhs_constraints, sort=top_level_k_sort) + + kore_lhs = kast_to_kore(definition, kast_lhs, sort=top_level_k_sort) + kore_rhs = kast_to_kore(definition, kast_rhs, sort=top_level_k_sort) + # The backend does not like rewrite rules without a precondition - if len(krule_lhs_constraints) == 0: + if not isinstance(kore_lhs, And): kore_lhs = And(top_level_kore_sort, (kore_lhs, Top(top_level_kore_sort))) - kore_rhs: Pattern = kast_to_kore(definition, krule_rhs, sort=top_level_k_sort) - prio = krule.priority attrs = [App(symbol='priority', sorts=(), args=(String(str(prio)),))] if Atts.LABEL in krule.att: From 7492dd12cd95991357e697b34cd45ca5729d84e0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 01:04:22 +0000 Subject: [PATCH 12/27] pyk/tests/integration/k-files/simple-proofs.k: add more examples of functional rules to translate --- .../tests/integration/test-data/k-files/simple-proofs.k | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k index da071b55a71..d7a5a5bc5b7 100644 --- a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k +++ b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k @@ -51,6 +51,15 @@ module SIMPLE-PROOFS syntax Foo ::= abcd(K) [symbol(abcd)] syntax Int ::= simpleFunction() [symbol(simpleFunc), function, total] + | leqZero(Int) [symbol(leqZero), function, total] rule [simple-func]: simpleFunction() => 3 + rule [simple-func-req-1]: leqZero(X) => 0 requires X <=Int 0 + rule [simple-func-req-2]: leqZero(X) => 1 requires 0 1 requires 0 1 requires 0 1 requires 0 1 requires 0 true requires 0 false [simplification, smt-lemma] endmodule From 1ba2eece9da742f586ff1c4e1222f98620778279 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 01:36:49 +0000 Subject: [PATCH 13/27] pyk/konvert/_kast_to_kore: factor out attribute konversion --- pyk/src/pyk/konvert/_kast_to_kore.py | 24 +++++++++++++++---- .../integration/konvert/test_simple_proofs.py | 6 ++--- 2 files changed, 22 insertions(+), 8 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index eff5462dc68..811c98220b5 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -21,6 +21,7 @@ from typing import Final from ..kast import KInner + from ..kast.att import AttEntry from ..kast.outer import KDefinition, KFlatModule, KImport from ..kore.syntax import Pattern, Sentence, Sort @@ -225,11 +226,16 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: if not isinstance(kore_lhs, And): kore_lhs = And(top_level_kore_sort, (kore_lhs, Top(top_level_kore_sort))) - prio = krule.priority - attrs = [App(symbol='priority', sorts=(), args=(String(str(prio)),))] - if Atts.LABEL in krule.att: - label = krule.att[Atts.LABEL] - attrs.append(App(symbol='label', sorts=(), args=(String(label),))) + # Make adjustments to Rule attributes + att = krule.att.discard([Atts.PRODUCTION, Atts.UNIQUE_ID, Atts.SOURCE, Atts.LOCATION]) + if Atts.PRIORITY not in att: + if Atts.OWISE in att: + att = att.update([Atts.PRIORITY(200)]) + att = att.discard([Atts.OWISE]) + else: + att = att.update([Atts.PRIORITY(50)]) + attrs = [_katt_to_kore(att_entry) for att_entry in att.entries()] + axiom = Axiom( vars=(), pattern=Rewrites( @@ -252,6 +258,14 @@ def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Mo return Module(name=kflatmodule.name, sentences=(imports + kore_axioms)) +def _katt_to_kore(att_entry: AttEntry) -> App: + match att_entry.key: + case Atts.LABEL | Atts.PRIORITY: + return App(symbol=att_entry.key.name, sorts=(), args=(String(str(att_entry.value)),)) + case _: + raise ValueError(f'Do not know how to convert AttEntry to Kore: {att_entry}') + + def _kimport_to_kore(kimport: KImport) -> Import: return Import(module_name=kimport.name, attrs=()) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 636fba557ec..40aee672436 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -530,7 +530,7 @@ ), ( 'SIMPLE-PROOFS.foo-to-bar-false', - r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \and{SortGeneratedTopCell{}}(\equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{})), \bottom{SortGeneratedTopCell{}}())), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [label{}("SIMPLE-PROOFS.foo-to-bar-false"), priority{}("30")]""", + r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \and{SortGeneratedTopCell{}}(\equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{})), \bottom{SortGeneratedTopCell{}}())), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [priority{}("30"), label{}("SIMPLE-PROOFS.foo-to-bar-false")]""", ), ( 'SIMPLE-PROOFS.foo-to-baz-owise', @@ -546,11 +546,11 @@ ), ( 'SIMPLE-PROOFS.simple-func-simplification', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [label{}("SIMPLE-PROOFS.simple-func-simplification"), simplification{}("")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-prio', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [label{}("SIMPLE-PROOFS.simple-func-simplification-prio"), simplification{}("38")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}("38"), label{}("SIMPLE-PROOFS.simple-func-simplification-prio")]""", ), ) From d33b9bcf0d937ce36e15bf94bfc4cb2c91d9bd6e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 01:44:02 +0000 Subject: [PATCH 14/27] pyk/konvert/_kast_to_kore: add support for converting SIMPLIFICATION attribute --- pyk/src/pyk/konvert/_kast_to_kore.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 811c98220b5..57eec2e7e49 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -232,7 +232,7 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: if Atts.OWISE in att: att = att.update([Atts.PRIORITY(200)]) att = att.discard([Atts.OWISE]) - else: + elif Atts.SIMPLIFICATION not in att: att = att.update([Atts.PRIORITY(50)]) attrs = [_katt_to_kore(att_entry) for att_entry in att.entries()] @@ -260,7 +260,7 @@ def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Mo def _katt_to_kore(att_entry: AttEntry) -> App: match att_entry.key: - case Atts.LABEL | Atts.PRIORITY: + case Atts.LABEL | Atts.PRIORITY | Atts.SIMPLIFICATION: return App(symbol=att_entry.key.name, sorts=(), args=(String(str(att_entry.value)),)) case _: raise ValueError(f'Do not know how to convert AttEntry to Kore: {att_entry}') From 183044ad6ef4c3f4b091f711835d41fa395561f1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 04:55:01 +0000 Subject: [PATCH 15/27] pyk/kast/att: add smt-lemma and symbolic attributes --- pyk/src/pyk/kast/att.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index 820eb97968f..5840146ba0a 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -339,9 +339,11 @@ class Atts: SEQSTRICT: Final = AttKey('seqstrict', type=_ANY) SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY) SOURCE: Final = AttKey('org.kframework.attributes.Source', type=_PATH) + SMTLEMMA: Final = AttKey('smt-lemma', type=_NONE) STRICT: Final = AttKey('strict', type=_ANY) SYMBOL: Final = AttKey('symbol', type=_STR) SYNTAX_MODULE: Final = AttKey('syntaxModule', type=_STR) + SYMBOLIC: Final = AttKey('symbolic', type=OptionalType(_STR)) TERMINALS: Final = AttKey('terminals', type=_STR) TOKEN: Final = AttKey('token', type=_NONE) TOTAL: Final = AttKey('total', type=_NONE) From d091d9d3acc679791fa284d4750d3158d90cc3e8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 04:56:40 +0000 Subject: [PATCH 16/27] pyk/konvert/kast_to_kore: support more translation of kast attributes to kore --- pyk/src/pyk/konvert/_kast_to_kore.py | 9 +++++++- .../integration/konvert/test_simple_proofs.py | 22 ++++++++++++++++++- .../test-data/k-files/simple-proofs.k | 1 + 3 files changed, 30 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 57eec2e7e49..024c17566ff 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -260,8 +260,15 @@ def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Mo def _katt_to_kore(att_entry: AttEntry) -> App: match att_entry.key: - case Atts.LABEL | Atts.PRIORITY | Atts.SIMPLIFICATION: + case Atts.LABEL | Atts.PRIORITY: return App(symbol=att_entry.key.name, sorts=(), args=(String(str(att_entry.value)),)) + case Atts.SIMPLIFICATION: + args = () if not att_entry.value else (String(str(att_entry.value)),) + return App(symbol=att_entry.key.name, sorts=(), args=args) + case Atts.SYMBOLIC | Atts.CONCRETE: + return App(symbol=att_entry.key.name, sorts=(), args=()) + case Atts.SMTLEMMA: + return App(symbol=att_entry.key.name, sorts=(), args=()) case _: raise ValueError(f'Do not know how to convert AttEntry to Kore: {att_entry}') diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 40aee672436..28fa9688b67 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -546,12 +546,32 @@ ), ( 'SIMPLE-PROOFS.simple-func-simplification', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-prio', r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}("38"), label{}("SIMPLE-PROOFS.simple-func-simplification-prio")]""", ), + ( + 'SIMPLE-PROOFS.simple-func-simplification-concrete-noarg', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), concrete{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete-noarg")]""", + ), + ( + 'SIMPLE-PROOFS.simple-func-simplification-concrete', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), concrete{}(VarX:SortInt), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete")]""", + ), + ( + 'SIMPLE-PROOFS.simple-func-simplification-symbolic', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), symbolic{}(VarX:SortInt)]""", + ), + ( + 'SIMPLE-PROOFS.simple-func-simplification-comm', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), comm{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-comm")]""", + ), + ( + 'SIMPLE-PROOFS.simple-func-simplification-smt-lemma', + r"""axiom{} \rewrites{SortBool{}}(\and{SortBool{}}(Lbl'UndsEqlsEqls'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("0")), \top{SortBool{}}()), \dv{SortBool{}}("false")) [simplification{}(), smt-lemma{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma")]""", + ), ) KRULE_TO_KORE_EXPLICIT_DATA: Final = ( diff --git a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k index d7a5a5bc5b7..b9ae8f94028 100644 --- a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k +++ b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k @@ -57,6 +57,7 @@ module SIMPLE-PROOFS rule [simple-func-req-2]: leqZero(X) => 1 requires 0 1 requires 0 1 requires 0 1 requires 0 1 requires 0 1 requires 0 true requires 0 Date: Sun, 10 Nov 2024 07:14:27 +0000 Subject: [PATCH 17/27] pyk/kast/outer: typo in comment --- pyk/src/pyk/kast/outer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index a543dca40e1..7efb2e3a52f 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1399,7 +1399,7 @@ def _add_ksequence_under_k_productions(_kast: KInner) -> KInner: return top_down(_add_ksequence_under_k_productions, kast) def sort_vars(self, kast: KInner, sort: KSort | None = None) -> KInner: - """Return the original term with all the variables having there sorts added or specialized, failing if recieving conflicting sorts for a given variable.""" + """Return the original term with all the variables having the sorts added or specialized, failing if recieving conflicting sorts for a given variable.""" if type(kast) is KVariable and kast.sort is None and sort is not None: return kast.let(sort=sort) From 76d33e9c2ff0b0b60dbf2c44fa2ac352d4c3826a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 17:09:25 +0000 Subject: [PATCH 18/27] pyk/tests/integration/{simple-proofs.k,test_simple_proofs.py}: update tests to working version --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 8 ++++---- .../tests/integration/test-data/k-files/simple-proofs.k | 4 +++- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 28fa9688b67..11659df9d36 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -558,15 +558,15 @@ ), ( 'SIMPLE-PROOFS.simple-func-simplification-concrete', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), concrete{}(VarX:SortInt), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete")]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), concrete{}(VarX : SortInt{}), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-symbolic', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), symbolic{}(VarX:SortInt)]""", + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), symbolic{}(VarX : SortInt{})]""", ), ( - 'SIMPLE-PROOFS.simple-func-simplification-comm', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), comm{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-comm")]""", + 'SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars', + r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(Lblleq{}(VarX : SortInt{}, Var'Unds'Y : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars"), symbolic{}(VarX : SortInt{}, Var'Unds'Y : SortInt{})]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-smt-lemma', diff --git a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k index b9ae8f94028..3d384944077 100644 --- a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k +++ b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k @@ -52,6 +52,8 @@ module SIMPLE-PROOFS syntax Int ::= simpleFunction() [symbol(simpleFunc), function, total] | leqZero(Int) [symbol(leqZero), function, total] + | leq(Int, Int) [symbol(leq), function, total] + rule leq(_,_) => 0 rule [simple-func]: simpleFunction() => 3 rule [simple-func-req-1]: leqZero(X) => 0 requires X <=Int 0 rule [simple-func-req-2]: leqZero(X) => 1 requires 0 1 requires 0 1 requires 0 1 requires 0 true requires 0 1 requires 0 false [simplification, smt-lemma] endmodule From b90e65dbe46855388c6cba76ff58d5124dc0d3cd Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 10 Nov 2024 17:10:08 +0000 Subject: [PATCH 19/27] pyk/konvert/_kast_to_kore: correctly handle conversion of variables in concrete/symbolic attribute too --- pyk/src/pyk/konvert/_kast_to_kore.py | 40 ++++++++++++++++------------ 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 024c17566ff..f4eb887d57b 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -5,8 +5,8 @@ from typing import TYPE_CHECKING from ..kast import Atts -from ..kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable, top_down -from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label +from ..kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, top_down +from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, var_occurrences from ..kast.outer import KRule from ..kore.prelude import SORT_K from ..kore.syntax import DV, And, App, Axiom, EVar, Import, MLPattern, MLQuant, Module, Rewrites, SortApp, String, Top @@ -199,6 +199,7 @@ def _inject(definition: KDefinition, term: KInner, sort: KSort) -> KInner: # 'krule' should have sorts on variables def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: + krule_body = krule.body krule_lhs_config = extract_lhs(krule_body) krule_rhs_config = extract_rhs(krule_body) @@ -219,13 +220,19 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: kast_lhs = mlAnd([krule_lhs_config] + krule_lhs_constraints, sort=top_level_k_sort) kast_rhs = mlAnd([krule_rhs_config] + krule_rhs_constraints, sort=top_level_k_sort) - kore_lhs = kast_to_kore(definition, kast_lhs, sort=top_level_k_sort) - kore_rhs = kast_to_kore(definition, kast_rhs, sort=top_level_k_sort) + kast_rule_sorted = definition.sort_vars(KRewrite(kast_lhs, kast_rhs)) + kast_lhs_sorted = extract_lhs(kast_rule_sorted) + kast_rhs_sorted = extract_rhs(kast_rule_sorted) + + kore_lhs = kast_to_kore(definition, kast_lhs_sorted, sort=top_level_k_sort) + kore_rhs = kast_to_kore(definition, kast_rhs_sorted, sort=top_level_k_sort) # The backend does not like rewrite rules without a precondition if not isinstance(kore_lhs, And): kore_lhs = And(top_level_kore_sort, (kore_lhs, Top(top_level_kore_sort))) + kore_rule = Rewrites(sort=top_level_kore_sort, left=kore_lhs, right=kore_rhs) + # Make adjustments to Rule attributes att = krule.att.discard([Atts.PRODUCTION, Atts.UNIQUE_ID, Atts.SOURCE, Atts.LOCATION]) if Atts.PRIORITY not in att: @@ -234,18 +241,10 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: att = att.discard([Atts.OWISE]) elif Atts.SIMPLIFICATION not in att: att = att.update([Atts.PRIORITY(50)]) - attrs = [_katt_to_kore(att_entry) for att_entry in att.entries()] - axiom = Axiom( - vars=(), - pattern=Rewrites( - sort=top_level_kore_sort, - left=kore_lhs, - right=kore_rhs, - ), - attrs=attrs, - ) - return axiom + attrs = [_krule_att_to_kore(att_entry, var_occurrences(kast_rule_sorted)) for att_entry in att.entries()] + + return Axiom(vars=(), pattern=kore_rule, attrs=attrs) def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Module: @@ -258,7 +257,7 @@ def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Mo return Module(name=kflatmodule.name, sentences=(imports + kore_axioms)) -def _katt_to_kore(att_entry: AttEntry) -> App: +def _krule_att_to_kore(att_entry: AttEntry, kast_rule_vars: dict[str, list[KVariable]]) -> App: match att_entry.key: case Atts.LABEL | Atts.PRIORITY: return App(symbol=att_entry.key.name, sorts=(), args=(String(str(att_entry.value)),)) @@ -266,7 +265,14 @@ def _katt_to_kore(att_entry: AttEntry) -> App: args = () if not att_entry.value else (String(str(att_entry.value)),) return App(symbol=att_entry.key.name, sorts=(), args=args) case Atts.SYMBOLIC | Atts.CONCRETE: - return App(symbol=att_entry.key.name, sorts=(), args=()) + if not att_entry.value: + return App(symbol=att_entry.key.name, sorts=(), args=()) + kore_vars = [] + for var_name in att_entry.value.split(','): + if var_name not in kast_rule_vars: + raise ValueError(f'Variable in {att_entry.key} not present in rule: {var_name}') + kore_vars.append(_kvariable_to_kore(kast_rule_vars[var_name][0])) + return App(symbol=att_entry.key.name, sorts=(), args=tuple(kore_vars)) case Atts.SMTLEMMA: return App(symbol=att_entry.key.name, sorts=(), args=()) case _: From 1af260b20baee865b7abc0d67ff216cefc79e235 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 Nov 2024 05:37:32 +0000 Subject: [PATCH 20/27] pyk/tests/integration/konvert/test_simple_proofs: update tests --- .../integration/konvert/test_simple_proofs.py | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 11659df9d36..e0ffe407ee0 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -538,39 +538,39 @@ ), ( 'SIMPLE-PROOFS.simple-func', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblsimpleFunc{}(), \top{SortInt{}}()), \dv{SortInt{}}("3")) [label{}("SIMPLE-PROOFS.simple-func"), priority{}("50")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(\dv{SortBool{}}("true"), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblsimpleFunc{}(), \and{SortInt{}}(\dv{SortInt{}}("3"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func"), priority{}("50")]""", ), ( 'SIMPLE-PROOFS.simple-func-req-1', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX : SortInt{}, \dv{SortInt{}}("0")))), \dv{SortInt{}}("0")) [label{}("SIMPLE-PROOFS.simple-func-req-1"), priority{}("50")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX : SortInt{}, \dv{SortInt{}}("0")), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("0"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-req-1"), priority{}("50")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-prio', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}("38"), label{}("SIMPLE-PROOFS.simple-func-simplification-prio")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}("38"), label{}("SIMPLE-PROOFS.simple-func-simplification-prio")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-concrete-noarg', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), concrete{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete-noarg")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), concrete{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete-noarg")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-concrete', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), concrete{}(VarX : SortInt{}), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), concrete{}(VarX : SortInt{}), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-symbolic', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(LblleqZero{}(VarX : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), symbolic{}(VarX : SortInt{})]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), symbolic{}(VarX : SortInt{})]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars', - r"""axiom{} \rewrites{SortInt{}}(\and{SortInt{}}(Lblleq{}(VarX : SortInt{}, Var'Unds'Y : SortInt{}), \equals{SortBool{}, SortInt{}}(\dv{SortBool{}}("true"), Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}))), \dv{SortInt{}}("1")) [simplification{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars"), symbolic{}(VarX : SortInt{}, Var'Unds'Y : SortInt{})]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(Lblleq{}(VarX : SortInt{}, Var'Unds'Y : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars"), symbolic{}(VarX : SortInt{}, Var'Unds'Y : SortInt{})]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-smt-lemma', - r"""axiom{} \rewrites{SortBool{}}(\and{SortBool{}}(Lbl'UndsEqlsEqls'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("0")), \top{SortBool{}}()), \dv{SortBool{}}("false")) [simplification{}(), smt-lemma{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(\dv{SortBool{}}("true"), \dv{SortBool{}}("true")), \equals{SortBool{}, R}(Lbl'UndsEqlsEqls'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("0")), \and{SortBool{}}(\dv{SortBool{}}("false"), \top{SortBool{}}()))) [simplification{}(""), smt-lemma{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma")]""", ), ) From ff1d21fcb7cec8970d4aad1c0a71e401d2a2f093 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 Nov 2024 05:39:39 +0000 Subject: [PATCH 21/27] pyk/tests/integration/proof/test_imp: update function argument names --- pyk/src/tests/integration/proof/test_imp.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 90dca214a1e..3ad17c599c9 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -893,7 +893,7 @@ def test_all_path_reachability_prove( tmp_path_factory: TempPathFactory, ) -> None: proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, @@ -930,7 +930,7 @@ def test_terminal_node_subsumption( claim_id: str = 'terminal-node-subsumption' cut_rules: Iterable[str] = [] proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, @@ -1441,7 +1441,7 @@ def test_all_path_reachability_prove_parallel( create_prover: Callable[[int, Iterable[str]], Prover], ) -> None: proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, @@ -1480,7 +1480,7 @@ def test_all_path_reachability_prove_parallel_resources( claim_id = 'addition-1' proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') - spec_modules = kprove.parse_modules(Path(spec_file), spec_module_name=spec_module) + spec_modules = kprove.parse_modules(Path(spec_file), module_name=spec_module) spec_label = f'{spec_module}.{claim_id}' proofs = APRProof.from_spec_modules( kprove.definition, From f394c778c578a57ba3e948cc65e88eb75537376e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 Nov 2024 05:51:43 +0000 Subject: [PATCH 22/27] pyk/konvert/_kast_to_kore: working conversion of K functional rules to kore --- pyk/src/pyk/konvert/_kast_to_kore.py | 130 ++++++++++++++++++++------- 1 file changed, 98 insertions(+), 32 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index f4eb887d57b..8b4aa85212e 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -6,13 +6,32 @@ from ..kast import Atts from ..kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, top_down -from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, var_occurrences +from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, ml_pred_to_bool, var_occurrences from ..kast.outer import KRule +from ..kore.prelude import BOOL as KORE_BOOL from ..kore.prelude import SORT_K -from ..kore.syntax import DV, And, App, Axiom, EVar, Import, MLPattern, MLQuant, Module, Rewrites, SortApp, String, Top +from ..kore.prelude import TRUE as KORE_TRUE +from ..kore.syntax import ( + DV, + And, + App, + Axiom, + Equals, + EVar, + Implies, + Import, + MLPattern, + MLQuant, + Module, + Rewrites, + SortApp, + SortVar, + String, + Top, +) from ..prelude.bytes import BYTES, pretty_bytes_str from ..prelude.k import K_ITEM, K, inj -from ..prelude.kbool import TRUE +from ..prelude.kbool import BOOL, TRUE, andBool from ..prelude.ml import mlAnd from ..prelude.string import STRING, pretty_string from ._utils import munge @@ -204,34 +223,84 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: krule_lhs_config = extract_lhs(krule_body) krule_rhs_config = extract_rhs(krule_body) - # Assume it's a semantic rule, but more specific sort for functional rules - top_level_k_sort = KSort('GeneratedTopCell') - if isinstance(krule_lhs_config, KApply) and krule_lhs_config.label.name in definition.function_labels: - top_level_k_sort = definition.sort_strict(krule_lhs_config) - top_level_kore_sort = _ksort_to_kore(top_level_k_sort) - - krule_lhs_constraints = [ - bool_to_ml_pred(c, sort=top_level_k_sort) for c in flatten_label('_andBool_', krule.requires) if not c == TRUE - ] - krule_rhs_constraints = [ - bool_to_ml_pred(c, sort=top_level_k_sort) for c in flatten_label('_andBool_', krule.ensures) if not c == TRUE - ] + is_functional = isinstance(krule_lhs_config, KApply) and krule_lhs_config.label.name in definition.function_labels - kast_lhs = mlAnd([krule_lhs_config] + krule_lhs_constraints, sort=top_level_k_sort) - kast_rhs = mlAnd([krule_rhs_config] + krule_rhs_constraints, sort=top_level_k_sort) + top_level_k_sort = KSort('GeneratedTopCell') if not is_functional else definition.sort_strict(krule_lhs_config) + top_level_kore_sort = _ksort_to_kore(top_level_k_sort) + # Do sort inference on the entire rule at once + kast_lhs = mlAnd( + [krule_lhs_config] + + [ + bool_to_ml_pred(constraint, sort=top_level_k_sort) + for constraint in flatten_label('_andBool_', krule.requires) + if not constraint == TRUE + ], + sort=top_level_k_sort, + ) + kast_rhs = mlAnd( + [krule_rhs_config] + + [ + bool_to_ml_pred(constraint, sort=top_level_k_sort) + for constraint in flatten_label('_andBool_', krule.ensures) + if not constraint == TRUE + ], + sort=top_level_k_sort, + ) kast_rule_sorted = definition.sort_vars(KRewrite(kast_lhs, kast_rhs)) - kast_lhs_sorted = extract_lhs(kast_rule_sorted) - kast_rhs_sorted = extract_rhs(kast_rule_sorted) - kore_lhs = kast_to_kore(definition, kast_lhs_sorted, sort=top_level_k_sort) - kore_rhs = kast_to_kore(definition, kast_rhs_sorted, sort=top_level_k_sort) - - # The backend does not like rewrite rules without a precondition - if not isinstance(kore_lhs, And): - kore_lhs = And(top_level_kore_sort, (kore_lhs, Top(top_level_kore_sort))) - - kore_rule = Rewrites(sort=top_level_kore_sort, left=kore_lhs, right=kore_rhs) + kast_lhs_body, *kast_lhs_constraints = flatten_label('#And', extract_lhs(kast_rule_sorted)) + kast_rhs_body, *kast_rhs_constraints = flatten_label('#And', extract_rhs(kast_rule_sorted)) + kore_lhs_body = kast_to_kore(definition, kast_lhs_body, sort=top_level_k_sort) + kore_rhs_body = kast_to_kore(definition, kast_rhs_body, sort=top_level_k_sort) + + axiom_vars: tuple[SortVar, ...] = () + kore_axiom: Pattern + if not is_functional: + kore_lhs_constraints = [ + kast_to_kore(definition, kast_lhs_constraint, sort=top_level_k_sort) + for kast_lhs_constraint in kast_lhs_constraints + ] + kore_rhs_constraints = [ + kast_to_kore(definition, kast_rhs_constraint, sort=top_level_k_sort) + for kast_rhs_constraint in kast_rhs_constraints + ] + kore_lhs_constraint: Pattern = Top(top_level_kore_sort) + if len(kore_lhs_constraints) == 1: + kore_lhs_constraint = kore_lhs_constraints[0] + elif len(kore_lhs_constraints) > 1: + kore_lhs_constraint = And(top_level_kore_sort, kore_lhs_constraints) + kore_lhs = And(top_level_kore_sort, [kore_lhs_body, kore_lhs_constraint]) + kore_rhs = ( + kore_rhs_body + if not kore_rhs_constraints + else And(top_level_kore_sort, [kore_rhs_body] + kore_rhs_constraints) + ) + kore_axiom = Rewrites(sort=top_level_kore_sort, left=kore_lhs, right=kore_rhs) + else: + axiom_sort = SortVar('R') + axiom_vars = (axiom_sort,) + kast_lhs_constraints_bool = [ + ml_pred_to_bool(kast_lhs_constraint) for kast_lhs_constraint in kast_lhs_constraints + ] + kore_antecedent = Equals( + KORE_BOOL, axiom_sort, kast_to_kore(definition, andBool(kast_lhs_constraints_bool), sort=BOOL), KORE_TRUE + ) + kore_ensures: Pattern = Top(top_level_kore_sort) + if kast_rhs_constraints: + kast_rhs_constraints_bool = [ + ml_pred_to_bool(kast_rhs_constraint) for kast_rhs_constraint in kast_rhs_constraints + ] + kore_ensures = Equals( + KORE_BOOL, + top_level_kore_sort, + kast_to_kore(definition, andBool(kast_rhs_constraints_bool), sort=BOOL), + KORE_TRUE, + ) + kore_consequent = Equals( + top_level_kore_sort, axiom_sort, kore_lhs_body, And(top_level_kore_sort, [kore_rhs_body, kore_ensures]) + ) + kore_axiom = Implies(axiom_sort, kore_antecedent, kore_consequent) # Make adjustments to Rule attributes att = krule.att.discard([Atts.PRODUCTION, Atts.UNIQUE_ID, Atts.SOURCE, Atts.LOCATION]) @@ -244,7 +313,7 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: attrs = [_krule_att_to_kore(att_entry, var_occurrences(kast_rule_sorted)) for att_entry in att.entries()] - return Axiom(vars=(), pattern=kore_rule, attrs=attrs) + return Axiom(vars=axiom_vars, pattern=kore_axiom, attrs=attrs) def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Module: @@ -259,11 +328,8 @@ def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Mo def _krule_att_to_kore(att_entry: AttEntry, kast_rule_vars: dict[str, list[KVariable]]) -> App: match att_entry.key: - case Atts.LABEL | Atts.PRIORITY: + case Atts.LABEL | Atts.PRIORITY | Atts.SIMPLIFICATION: return App(symbol=att_entry.key.name, sorts=(), args=(String(str(att_entry.value)),)) - case Atts.SIMPLIFICATION: - args = () if not att_entry.value else (String(str(att_entry.value)),) - return App(symbol=att_entry.key.name, sorts=(), args=args) case Atts.SYMBOLIC | Atts.CONCRETE: if not att_entry.value: return App(symbol=att_entry.key.name, sorts=(), args=()) From 610949c6b6eb481e222ddb428487bedb25c40747 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 Nov 2024 05:52:23 +0000 Subject: [PATCH 23/27] pyk/reachability: support adding extra Kast modules to proof context --- pyk/src/pyk/proof/reachability.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 762f98c32d2..d7e706ca939 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -714,6 +714,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): direct_subproof_rules: bool assume_defined: bool kcfg_explore: KCFGExplore + extra_module: KFlatModule | None def __init__( self, @@ -725,6 +726,7 @@ def __init__( fast_check_subsumption: bool = False, direct_subproof_rules: bool = False, assume_defined: bool = False, + extra_module: KFlatModule | None = None, ) -> None: self.kcfg_explore = kcfg_explore @@ -736,11 +738,19 @@ def __init__( self.fast_check_subsumption = fast_check_subsumption self.direct_subproof_rules = direct_subproof_rules self.assume_defined = assume_defined + self.extra_module = extra_module def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() def init_proof(self, proof: APRProof) -> None: + main_module_name = self.main_module_name + if self.extra_module: + _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, self.extra_module) + _LOGGER.warning(f'_kore_module: {_kore_module.text}') + self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True) + main_module_name = self.extra_module.name + def _inject_module(module_name: str, import_name: str, sentences: list[KRule]) -> None: _module = KFlatModule(module_name, sentences, [KImport(import_name)]) _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, _module) @@ -759,7 +769,7 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRule]) - ] circularity_rule = proof.as_rule(priority=20) - _inject_module(proof.dependencies_module_name, self.main_module_name, dependencies_as_rules) + _inject_module(proof.dependencies_module_name, main_module_name, dependencies_as_rules) _inject_module(proof.circularities_module_name, proof.dependencies_module_name, [circularity_rule]) for node_id in [proof.init, proof.target]: From cbdc23cc15a851a5c6f73685015ec24eac2cdde8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 Nov 2024 04:11:06 +0000 Subject: [PATCH 24/27] pyk/konvert/_kast_to_kore: make sure to sort attribute entries first --- pyk/src/pyk/konvert/_kast_to_kore.py | 5 ++++- .../integration/konvert/test_simple_proofs.py | 16 ++++++++-------- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 8b4aa85212e..b32d42ad923 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -311,7 +311,10 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: elif Atts.SIMPLIFICATION not in att: att = att.update([Atts.PRIORITY(50)]) - attrs = [_krule_att_to_kore(att_entry, var_occurrences(kast_rule_sorted)) for att_entry in att.entries()] + attrs = [ + _krule_att_to_kore(att_entry, var_occurrences(kast_rule_sorted)) + for att_entry in sorted(att.entries(), key=(lambda a: a.key.name)) + ] return Axiom(vars=axiom_vars, pattern=kore_axiom, attrs=attrs) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index e0ffe407ee0..2497491560d 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -530,7 +530,7 @@ ), ( 'SIMPLE-PROOFS.foo-to-bar-false', - r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \and{SortGeneratedTopCell{}}(\equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{})), \bottom{SortGeneratedTopCell{}}())), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [priority{}("30"), label{}("SIMPLE-PROOFS.foo-to-bar-false")]""", + r"""axiom{} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{}), \and{SortGeneratedTopCell{}}(\equals{SortBool{}, SortGeneratedTopCell{}}(\dv{SortBool{}}("true"), Lblpred1{}(VarN : SortInt{})), \bottom{SortGeneratedTopCell{}}())), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'Unds'SIMPLE-PROOFS'Unds'KItem{}(), Var'Unds'RestK : SortK{})), Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), inj{SortInt{}, SortKItem{}}(VarN : SortInt{})), Var'Unds'RestState : SortMap{})), Var'Unds'DotVar0 : SortGeneratedCounterCell{})) [label{}("SIMPLE-PROOFS.foo-to-bar-false"), priority{}("30")]""", ), ( 'SIMPLE-PROOFS.foo-to-baz-owise', @@ -546,31 +546,31 @@ ), ( 'SIMPLE-PROOFS.simple-func-simplification', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification"), simplification{}("")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-prio', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}("38"), label{}("SIMPLE-PROOFS.simple-func-simplification-prio")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification-prio"), simplification{}("38")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-concrete-noarg', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), concrete{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete-noarg")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [concrete{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete-noarg"), simplification{}("")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-concrete', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), concrete{}(VarX : SortInt{}), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [concrete{}(VarX : SortInt{}), label{}("SIMPLE-PROOFS.simple-func-simplification-concrete"), simplification{}("")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-symbolic', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), symbolic{}(VarX : SortInt{})]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(LblleqZero{}(VarX : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic"), simplification{}(""), symbolic{}(VarX : SortInt{})]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(Lblleq{}(VarX : SortInt{}, Var'Unds'Y : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [simplification{}(""), label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars"), symbolic{}(VarX : SortInt{}, Var'Unds'Y : SortInt{})]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-'Int'Unds'{}(\dv{SortInt{}}("0"), VarX : SortInt{}), \dv{SortBool{}}("true")), \equals{SortInt{}, R}(Lblleq{}(VarX : SortInt{}, Var'Unds'Y : SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("1"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification-symbolic-2vars"), simplification{}(""), symbolic{}(VarX : SortInt{}, Var'Unds'Y : SortInt{})]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification-smt-lemma', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(\dv{SortBool{}}("true"), \dv{SortBool{}}("true")), \equals{SortBool{}, R}(Lbl'UndsEqlsEqls'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("0")), \and{SortBool{}}(\dv{SortBool{}}("false"), \top{SortBool{}}()))) [simplification{}(""), smt-lemma{}(), label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma")]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(\dv{SortBool{}}("true"), \dv{SortBool{}}("true")), \equals{SortBool{}, R}(Lbl'UndsEqlsEqls'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("0")), \and{SortBool{}}(\dv{SortBool{}}("false"), \top{SortBool{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma"), simplification{}(""), smt-lemma{}()]""", ), ) From 1a3918fa95278d5544df5b35b8eefd963e11c514 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 21 Nov 2024 01:32:47 +0000 Subject: [PATCH 25/27] pyk/kast/{outer,manip}: changes from code-review --- pyk/src/pyk/kast/manip.py | 4 ++-- pyk/src/pyk/kast/outer.py | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/kast/manip.py b/pyk/src/pyk/kast/manip.py index 30c59421b6c..4f4056d703a 100644 --- a/pyk/src/pyk/kast/manip.py +++ b/pyk/src/pyk/kast/manip.py @@ -105,9 +105,9 @@ def fun(term: KInner) -> KInner: def bool_to_ml_pred(kast: KInner, sort: str | KSort = GENERATED_TOP_CELL) -> KInner: def _bool_constraint_to_ml(_kast: KInner) -> KInner: if _kast == TRUE: - return mlTop() + return mlTop(sort=sort) if _kast == FALSE: - return mlBottom() + return mlBottom(sort=sort) return mlEqualsTrue(_kast, sort=sort) return mlAnd([_bool_constraint_to_ml(cond) for cond in flatten_label('_andBool_', kast)], sort=sort) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 7efb2e3a52f..9a68863d1a9 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -15,7 +15,7 @@ from ..prelude.kbool import TRUE from ..prelude.ml import ML_QUANTIFIERS -from ..utils import FrozenDict, POSet, filter_none, single, unique +from ..utils import FrozenDict, POSet, filter_none, not_none, single, unique from .att import EMPTY_ATT, Atts, Format, KAst, KAtt, WithKAtt from .inner import ( KApply, @@ -1120,7 +1120,7 @@ def functions(self) -> tuple[KProduction, ...]: @cached_property def function_labels(self) -> tuple[str, ...]: """Returns the label names of all the `KProduction` which are function symbols for all modules in this definition.""" - return tuple(func.klabel.name for func in self.functions if func.klabel is not None) + return tuple(not_none(func.klabel).name for func in self.functions) @cached_property def constructors(self) -> tuple[KProduction, ...]: From 830aaec8196967bcf23cf7a0416269434dde8b93 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 21 Nov 2024 12:58:49 +0000 Subject: [PATCH 26/27] pyk/tests/{test_simple_proofs.py,simple-proofs.k}: use valid K definition to avoid issues --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 2 +- pyk/src/tests/integration/test-data/k-files/simple-proofs.k | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 2497491560d..f807e7ef3c7 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -570,7 +570,7 @@ ), ( 'SIMPLE-PROOFS.simple-func-simplification-smt-lemma', - r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(\dv{SortBool{}}("true"), \dv{SortBool{}}("true")), \equals{SortBool{}, R}(Lbl'UndsEqlsEqls'Int'Unds'{}(\dv{SortInt{}}("1"), \dv{SortInt{}}("0")), \and{SortBool{}}(\dv{SortBool{}}("false"), \top{SortBool{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma"), simplification{}(""), smt-lemma{}()]""", + r"""axiom{R} \implies{R}(\equals{SortBool{}, R}(\dv{SortBool{}}("true"), \dv{SortBool{}}("true")), \equals{SortBool{}, R}(Lbl'UndsEqlsEqls'Int'Unds'{}(Lblleq{}(Var'Unds'Gen0 : SortInt{}, Var'Unds'Gen1 : SortInt{}), \dv{SortInt{}}("0")), \and{SortBool{}}(\dv{SortBool{}}("false"), \top{SortBool{}}()))) [label{}("SIMPLE-PROOFS.simple-func-simplification-smt-lemma"), simplification{}(""), smt-lemma{}()]""", ), ) diff --git a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k index 3d384944077..6c361cdb91d 100644 --- a/pyk/src/tests/integration/test-data/k-files/simple-proofs.k +++ b/pyk/src/tests/integration/test-data/k-files/simple-proofs.k @@ -52,7 +52,7 @@ module SIMPLE-PROOFS syntax Int ::= simpleFunction() [symbol(simpleFunc), function, total] | leqZero(Int) [symbol(leqZero), function, total] - | leq(Int, Int) [symbol(leq), function, total] + | leq(Int, Int) [symbol(leq), function, total, smtlib(leq)] rule leq(_,_) => 0 rule [simple-func]: simpleFunction() => 3 rule [simple-func-req-1]: leqZero(X) => 0 requires X <=Int 0 @@ -63,6 +63,6 @@ module SIMPLE-PROOFS rule [simple-func-simplification-concrete]: leqZero(X) => 1 requires 0 1 requires 0 1 requires 0 false [simplification, smt-lemma] + rule [simple-func-simplification-smt-lemma]: leq(_,_) ==Int 0 => false [simplification, smt-lemma] endmodule From 359eb3f023fe073d9ba32567623609bc93c801c5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 21 Nov 2024 13:04:19 +0000 Subject: [PATCH 27/27] pyk/konvert/_kast_to_kore: formatting --- pyk/src/pyk/konvert/_kast_to_kore.py | 1 - 1 file changed, 1 deletion(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index b32d42ad923..fb36d334785 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -218,7 +218,6 @@ def _inject(definition: KDefinition, term: KInner, sort: KSort) -> KInner: # 'krule' should have sorts on variables def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: - krule_body = krule.body krule_lhs_config = extract_lhs(krule_body) krule_rhs_config = extract_rhs(krule_body)