From 73a6a4ea933be05734c080d737c218086e91711e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 17 Nov 2025 14:35:33 +1100 Subject: [PATCH 1/5] WIP extend krule_to_kore to generate valid function equations --- pyk/src/pyk/konvert/_kast_to_kore.py | 79 +++++++++++++++++++++++++++- 1 file changed, 78 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 1f667e2752..c1caa7d788 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -25,6 +25,7 @@ EVar, Implies, Import, + In, MLPattern, MLQuant, Module, @@ -280,7 +281,14 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: 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: + elif Atts.SIMPLIFICATION in krule.att: + # Canonical shape of a simplification equation + # \implies( + # requires, + # \equals( + # lhs, + # \and(rhs, ensures) + # ) axiom_sort = SortVar('R') axiom_vars = (axiom_sort,) kast_lhs_constraints_bool = [ @@ -304,6 +312,58 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: 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) + else: # i.e., is_functional and not a simplification + # canonical shape of a function equation (not simplification!) + # \implies( + # \and(requires, argument_predicates), + # \equals(lhs_with_args_replaced, \and(rhs, ensures)) + # ) + # arg.predicates are \and chains of \in(VAR, ARG) ending in \top + # the actual arg.s are replaced by VAR_1..n in the LHS's function application + # requires and ensures are \\top if empty or \and-ed \equals(.., \dv("true")) + 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 + ] + assert isinstance(kast_lhs_body, KApply) + kore_requires_antecedent: Pattern = Top(top_level_kore_sort) + if kast_lhs_constraints_bool is not None: + kore_requires_antecedent = Equals( + KORE_BOOL, + axiom_sort, + kast_to_kore(definition, andBool(kast_lhs_constraints_bool), sort=BOOL), + KORE_TRUE, + ) + # make argument predicates + if not kast_lhs_body.args: + kore_fct_antecedent: Pattern = kore_requires_antecedent + else: + arg_predicates, arg_vars = _mk_arg_vars(definition, top_level_kore_sort, kast_lhs_body.args) + kore_fct_antecedent = And( + axiom_sort, + ( + kore_requires_antecedent, + arg_predicates, + ), + ) + kore_lhs_body = kast_to_kore(definition, KApply(kast_lhs_body.label, arg_vars), sort=top_level_k_sort) + + kore_ensures = 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_fct_antecedent, kore_consequent) # Make adjustments to Rule attributes att = krule.att.discard([Atts.PRODUCTION, Atts.UNIQUE_ID, Atts.SOURCE, Atts.LOCATION]) @@ -322,6 +382,23 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: return Axiom(vars=axiom_vars, pattern=kore_axiom, attrs=attrs) +def _mk_arg_vars(definition: KDefinition, sort: Sort, args: tuple[KInner, ...]) -> tuple[Pattern, list[KInner]]: + + def sort_of(arg: KInner) -> Sort: + return sort # fixme! + + def ksort_of(arg: KInner) -> KSort: + raise Exception('FIXME') + + preds = [ + In(sort_of(arg), sort, EVar(name, sort_of(arg)), kast_to_kore(definition, arg, ksort_of(arg))) + for (arg, name) in zip(args, [f'var_{i}' for i in range(1, 43)], strict=False) + ] + + # fixme! + return (Top(sort), []) + + def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Module: kore_axioms: list[Sentence] = [] for sent in kflatmodule.sentences: From 60ee0c55a50903b3b4915df309b4de009988968f Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 17 Nov 2025 17:42:31 +1100 Subject: [PATCH 2/5] mangle function app, generate arg.matching predicate with fresh variables --- pyk/src/pyk/konvert/_kast_to_kore.py | 37 ++++++++++++++++++---------- 1 file changed, 24 insertions(+), 13 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index c1caa7d788..e8dd5dc945 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -339,15 +339,15 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: if not kast_lhs_body.args: kore_fct_antecedent: Pattern = kore_requires_antecedent else: - arg_predicates, arg_vars = _mk_arg_vars(definition, top_level_kore_sort, kast_lhs_body.args) + kore_arg_predicates, new_kore_app = _mangle_app(definition, top_level_kore_sort, kast_lhs_body) kore_fct_antecedent = And( axiom_sort, ( kore_requires_antecedent, - arg_predicates, + kore_arg_predicates, ), ) - kore_lhs_body = kast_to_kore(definition, KApply(kast_lhs_body.label, arg_vars), sort=top_level_k_sort) + kore_lhs_body = new_kore_app kore_ensures = Top(top_level_kore_sort) if kast_rhs_constraints: @@ -382,21 +382,32 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: return Axiom(vars=axiom_vars, pattern=kore_axiom, attrs=attrs) -def _mk_arg_vars(definition: KDefinition, sort: Sort, args: tuple[KInner, ...]) -> tuple[Pattern, list[KInner]]: +def _mangle_app(definition: KDefinition, sort: Sort, app: KApply) -> tuple[Pattern, Pattern]: - def sort_of(arg: KInner) -> Sort: - return sort # fixme! - - def ksort_of(arg: KInner) -> KSort: - raise Exception('FIXME') + ksorts = _argument_sorts(definition, app) + assert len(ksorts) == len(app.args) + var_names = [f'F_ARG_{i}' for i in range(1, 42)] # arbitrary limit + assert len(ksorts) <= len(var_names) # fail if too many arguments preds = [ - In(sort_of(arg), sort, EVar(name, sort_of(arg)), kast_to_kore(definition, arg, ksort_of(arg))) - for (arg, name) in zip(args, [f'var_{i}' for i in range(1, 43)], strict=False) + In( + _ksort_to_kore(ksort), + sort, + EVar(name, _ksort_to_kore(ksort)), + kast_to_kore(definition, arg, ksort), + ) + for (arg, ksort, name) in zip(app.args, ksorts, var_names, strict=False) ] - # fixme! - return (Top(sort), []) + new_app = kast_to_kore( + definition, + KApply( + app.label, + [KVariable(name, sort) for (sort, name) in zip(ksorts, var_names, strict=False)], + ), + ) + + return (And(sort, preds), new_app) def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Module: From dd91925e71269dcc03e8ccc485d10af93841a201 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 17 Nov 2025 19:54:43 +1100 Subject: [PATCH 3/5] avoid underscore in var name (:scratch-head:) --- pyk/src/pyk/konvert/_kast_to_kore.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index e8dd5dc945..9209d391ec 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -386,7 +386,7 @@ def _mangle_app(definition: KDefinition, sort: Sort, app: KApply) -> tuple[Patte ksorts = _argument_sorts(definition, app) assert len(ksorts) == len(app.args) - var_names = [f'F_ARG_{i}' for i in range(1, 42)] # arbitrary limit + var_names = [f'F-ARG-{i}' for i in range(1, 42)] # arbitrary limit assert len(ksorts) <= len(var_names) # fail if too many arguments preds = [ From 065d6c1fa9d26df6409111e3406bc53c571f4cd0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 17 Nov 2025 20:08:07 +1100 Subject: [PATCH 4/5] update test expectation (kore from a kompiled module) --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 4 ++-- 1 file 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 7833c1df84..dc36c70562 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -591,11 +591,11 @@ ), ( 'SIMPLE-PROOFS.simple-func', - 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")]""", + r"""axiom{R} \implies{R}(\and{R}(\top{R}(), \top{R}()), \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{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")]""", + r"""axiom{R} \implies{R}(\and{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX:SortInt{}, \dv{SortInt{}}("0")), \dv{SortBool{}}("true")), \and{R}(\in{SortInt{}, R}(X0:SortInt{}, VarX:SortInt{}), \top{R}())), \equals{SortInt{},R}(LblleqZero{}(X0:SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("0"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-req-1"), priority{}("50")]""" ), ( 'SIMPLE-PROOFS.simple-func-simplification', From ae0245e1d20040e33436be2519c5db5d704ccac3 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 17 Nov 2025 20:10:43 +1100 Subject: [PATCH 5/5] formatting --- pyk/src/tests/integration/konvert/test_simple_proofs.py | 4 ++-- 1 file 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 dc36c70562..3239d74f32 100644 --- a/pyk/src/tests/integration/konvert/test_simple_proofs.py +++ b/pyk/src/tests/integration/konvert/test_simple_proofs.py @@ -591,11 +591,11 @@ ), ( 'SIMPLE-PROOFS.simple-func', - r"""axiom{R} \implies{R}(\and{R}(\top{R}(), \top{R}()), \equals{SortInt{}, R}(LblsimpleFunc{}(), \and{SortInt{}}(\dv{SortInt{}}("3"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func"), priority{}("50")]""" + r"""axiom{R} \implies{R}(\and{R}(\top{R}(), \top{R}()), \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{R} \implies{R}(\and{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX:SortInt{}, \dv{SortInt{}}("0")), \dv{SortBool{}}("true")), \and{R}(\in{SortInt{}, R}(X0:SortInt{}, VarX:SortInt{}), \top{R}())), \equals{SortInt{},R}(LblleqZero{}(X0:SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("0"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-req-1"), priority{}("50")]""" + r"""axiom{R} \implies{R}(\and{R}(\equals{SortBool{}, R}(Lbl'Unds-LT-Eqls'Int'Unds'{}(VarX:SortInt{}, \dv{SortInt{}}("0")), \dv{SortBool{}}("true")), \and{R}(\in{SortInt{}, R}(X0:SortInt{}, VarX:SortInt{}), \top{R}())), \equals{SortInt{},R}(LblleqZero{}(X0:SortInt{}), \and{SortInt{}}(\dv{SortInt{}}("0"), \top{SortInt{}}()))) [label{}("SIMPLE-PROOFS.simple-func-req-1"), priority{}("50")]""", ), ( 'SIMPLE-PROOFS.simple-func-simplification',