diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index 1f667e2752..9209d391ec 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: + 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, + kore_arg_predicates, + ), + ) + kore_lhs_body = new_kore_app + + 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,34 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: return Axiom(vars=axiom_vars, pattern=kore_axiom, attrs=attrs) +def _mangle_app(definition: KDefinition, sort: Sort, app: KApply) -> tuple[Pattern, Pattern]: + + 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( + _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) + ] + + 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: kore_axioms: list[Sentence] = [] for sent in kflatmodule.sentences: diff --git a/pyk/src/tests/integration/konvert/test_simple_proofs.py b/pyk/src/tests/integration/konvert/test_simple_proofs.py index 7833c1df84..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}(\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',