From ed029c99ace25515ac97a808d969a8357fbca195 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 16 Jun 2026 23:16:28 +0200 Subject: [PATCH 1/5] feat: parametric cast function + cast insertion in taclet application Add cast.key (cast<[E]>(any) -> E + simplification taclets), TermBuilder.cast, and restore the cast insertion in RewriteTacletExecutor (getMaxSort port) so a replacewith result that doesn't fit its position is wrapped in a cast. --- .github/PULL_REQUEST_TEMPLATE/casts.md | 36 ++++++++++++++ .../key_project/rusty/logic/TermBuilder.java | 20 ++++++++ .../rustydl/RewriteTacletExecutor.java | 32 ++++++++++--- .../key_project/rusty/proof/rules/cast.key | 48 +++++++++++++++++++ .../rusty/proof/rules/ruleSetDeclarations.key | 1 + .../rusty/proof/rules/standardRustRules.key | 1 + 6 files changed, 131 insertions(+), 7 deletions(-) create mode 100644 .github/PULL_REQUEST_TEMPLATE/casts.md create mode 100644 keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key diff --git a/.github/PULL_REQUEST_TEMPLATE/casts.md b/.github/PULL_REQUEST_TEMPLATE/casts.md new file mode 100644 index 00000000000..9b5b9eca9b2 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE/casts.md @@ -0,0 +1,36 @@ +# Casts in the logic + cast insertion during taclet application + +## What + +Adds the cast machinery legacy KeY uses to keep terms well-sorted, ported to the +parametric-function style (no sort-depending functions): + +- **`cast.key`** — a parametric `cast<[E]>(any) -> E` function (first-order; + counterpart of `ghost<[E]>`/`read<[E]>`) with its simplification taclets + (`castDel`, nested-cast collapse), included after `firstOrderRules`; + `cast_deletion` ruleset registered. +- **`TermBuilder.cast(Sort, Term)`** — builds `cast<[sort]>(t)` by instantiating + the parametric `cast` at the target sort. +- **`RewriteTacletExecutor`** — computes the per-position required sort + (`getMaxSort`, a `TermHelper` port) and, when a replacewith result doesn't fit, + wraps it in a cast — restoring the previously stubbed/commented-out logic. + +## Open question for maintainers ⚠️ + +Six `RunAllProofs` cases fail to **replay** (e.g. `man-loop-mul.proof`): + +``` +Could not apply applyEq — Unknown instantiations for \assumes. 0 candidates. +``` + +The cast insertion changes the term representation (loose terms now appear as +`cast<[…]>(…)`), so proofs saved under the *old* representation no longer match. +`cast.key` and `TermBuilder.cast` are inert; only the executor insertion changes +terms — which is its purpose. + +**Please decide:** + +1. **Adopt** the well-sorted representation → re-save the 6 affected proofs + (`man-loop-mul.proof` and siblings under `testcase/examples/`). *(expected)* +2. **Too disruptive** → gate the executor cast insertion behind a flag, or keep + only `cast.key` + `TermBuilder.cast` for explicit use by taclets. diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java b/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java index b7e2fccc900..9709773ba5a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java @@ -54,6 +54,26 @@ public TermFactory tf() { return tf; } + private static final Name CAST_NAME = new Name("cast"); + + /// Builds `cast<[sort]>(term)`, reinterpreting `term` as `sort` via the parametric `cast` + /// function (see cast.key). Returns `term` unchanged when it already has that sort, or when the + /// `cast` operator is not declared. + public Term cast(Sort sort, Term term) { + if (term.sort() == sort) { + return term; + } + ParametricFunctionDecl decl = + services.getNamespaces().parametricFunctions().lookup(CAST_NAME); + if (decl == null) { + return term; + } + ImmutableList args = + ImmutableSLList.nil().prepend(new SortArg(sort)); + ParametricFunctionInstance castFn = ParametricFunctionInstance.get(decl, args); + return tf.createTerm(castFn, term); + } + // ------------------------------------------------------------------------- // constructors for special classes of term operators // ------------------------------------------------------------------------- diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java index 45cf4a5a072..33f629f0c1b 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java @@ -6,12 +6,15 @@ import org.key_project.logic.IntIterator; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.op.SortedOperator; import org.key_project.logic.sort.Sort; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentChangeInfo; import org.key_project.prover.sequent.SequentFormula; import org.key_project.rusty.Services; +import org.key_project.rusty.logic.RustyDLTheory; +import org.key_project.rusty.logic.op.IfThenElse; import org.key_project.rusty.proof.Goal; import org.key_project.rusty.rule.MatchConditions; import org.key_project.rusty.rule.RuleApp; @@ -101,8 +104,7 @@ private Term replace(Term term, Term with, PosInOccurrence posOfFind, IntIterato final Term[] subs = new Term[term.arity()]; term.subs().arraycopy(0, subs, 0, term.arity()); - final Sort newMaxSort = maxSort; // TODO? TermHelper.getMaxSort(term, - // indexOfNextSubTerm); + final Sort newMaxSort = getMaxSort(term, indexOfNextSubTerm); subs[indexOfNextSubTerm] = replace(term.sub(indexOfNextSubTerm), with, posOfFind, it, mc, newMaxSort, goal, services, ruleApp); @@ -112,12 +114,28 @@ private Term replace(Term term, Term with, PosInOccurrence posOfFind, IntIterato with = syntacticalReplace(with, posOfFind, mc, goal, ruleApp, services); - /* - * if (!with.sort().extendsTrans(maxSort)) { - * with = services.getTermBuilder().cast(maxSort, with); - * } - */ + // If the replacewith result does not fit the sort required at this position, wrap it in a + // cast so the surrounding term stays well-sorted (mirrors KeY's RewriteTacletExecutor). + if (!with.sort().extendsTrans(maxSort)) { + with = services.getTermBuilder().cast(maxSort, with); + } return with; } + + /// The maximal sort allowed at the `i`-th argument of `term` (port of KeY's + /// `TermHelper.getMaxSort`): a formula stays a formula, the branches of an if-then-else may + /// carry the if-then-else's own sort, and otherwise the operator's declared argument sort. + private static Sort getMaxSort(Term term, int i) { + if (term.sub(i).sort() == RustyDLTheory.FORMULA) { + return RustyDLTheory.FORMULA; + } + if (term.op() instanceof IfThenElse && i > 0) { + return term.sort(); + } + if (term.op() instanceof SortedOperator sortedOp) { + return sortedOp.argSort(i); + } + return term.sub(i).sort(); + } } diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key new file mode 100644 index 00000000000..3ff00f2f4df --- /dev/null +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key @@ -0,0 +1,48 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ + +/* + * Casts in the logic. + * + * A parametric cast function `cast<[E]>(any) -> E` reinterprets a value of any + * sort as the type parameter `E` (the counterpart of the parametric `ghost<[E]>` + * / `read<[E]>` functions). It is meant to be inserted by the taclet-application + * logic (RewriteTacletExecutor) so that a replacewith result of the top sort + * `any` is given the concrete sort required by its position. + * + * The taclets are adapted from the cast family of legacy KeY's genericRules.key + * (castDel, nested-cast collapse). They are deliberately conservative. + */ + +\sorts { + \generic alpha; + \generic beta; +} + +\functions { + cast<[E]>(any) -> E; +} + +\schemaVariables { + \term any castArg; + \term alpha castAlphaArg; +} + +\rules { + // genericRules.key: castDel + // A cast to a sort the argument already has is the identity. `castAlphaArg : alpha` only + // matches an argument whose sort already fits `alpha`, so a genuine narrowing cast is not removed. + castDel { + \find(cast<[alpha]>(castAlphaArg)) + \replacewith(castAlphaArg) + \heuristics(simplify, cast_deletion) + }; + + // genericRules.key: nested-cast collapse — the outer cast determines the sort. + castCast { + \find(cast<[alpha]>(cast<[beta]>(castArg))) + \replacewith(cast<[alpha]>(castArg)) + \heuristics(simplify, cast_deletion) + }; +} diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key index 81f8845eab5..8aeea3a95f5 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key @@ -33,6 +33,7 @@ split_cond; simplify; + cast_deletion; simplify_enlarging; simplify_ENLARGING; // Simplification rules which make formulas much bigger // and therefore should be used less frequently than diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key index 43db1710452..6e2b10bbad1 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key @@ -8,6 +8,7 @@ // general propositional and first-order rules \include propRule; \include firstOrderRules; +\include cast; \include ifThenElseRules; \include formulaNormalizationRules; \include updateRules; From 7427d247cd8ad3cceb09877d939f3e372d058148 Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 17 Jun 2026 09:52:28 +0200 Subject: [PATCH 2/5] Remove PR template --- .github/PULL_REQUEST_TEMPLATE/casts.md | 36 -------------------------- 1 file changed, 36 deletions(-) delete mode 100644 .github/PULL_REQUEST_TEMPLATE/casts.md diff --git a/.github/PULL_REQUEST_TEMPLATE/casts.md b/.github/PULL_REQUEST_TEMPLATE/casts.md deleted file mode 100644 index 9b5b9eca9b2..00000000000 --- a/.github/PULL_REQUEST_TEMPLATE/casts.md +++ /dev/null @@ -1,36 +0,0 @@ -# Casts in the logic + cast insertion during taclet application - -## What - -Adds the cast machinery legacy KeY uses to keep terms well-sorted, ported to the -parametric-function style (no sort-depending functions): - -- **`cast.key`** — a parametric `cast<[E]>(any) -> E` function (first-order; - counterpart of `ghost<[E]>`/`read<[E]>`) with its simplification taclets - (`castDel`, nested-cast collapse), included after `firstOrderRules`; - `cast_deletion` ruleset registered. -- **`TermBuilder.cast(Sort, Term)`** — builds `cast<[sort]>(t)` by instantiating - the parametric `cast` at the target sort. -- **`RewriteTacletExecutor`** — computes the per-position required sort - (`getMaxSort`, a `TermHelper` port) and, when a replacewith result doesn't fit, - wraps it in a cast — restoring the previously stubbed/commented-out logic. - -## Open question for maintainers ⚠️ - -Six `RunAllProofs` cases fail to **replay** (e.g. `man-loop-mul.proof`): - -``` -Could not apply applyEq — Unknown instantiations for \assumes. 0 candidates. -``` - -The cast insertion changes the term representation (loose terms now appear as -`cast<[…]>(…)`), so proofs saved under the *old* representation no longer match. -`cast.key` and `TermBuilder.cast` are inert; only the executor insertion changes -terms — which is its purpose. - -**Please decide:** - -1. **Adopt** the well-sorted representation → re-save the 6 affected proofs - (`man-loop-mul.proof` and siblings under `testcase/examples/`). *(expected)* -2. **Too disruptive** → gate the executor cast insertion behind a flag, or keep - only `cast.key` + `TermBuilder.cast` for explicit use by taclets. From 8ccce14643ade9957fa8a812e6f5f0c072490c5e Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 17 Jun 2026 09:53:45 +0200 Subject: [PATCH 3/5] Simplify list operation --- .../src/main/java/org/key_project/rusty/logic/TermBuilder.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java b/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java index 9709773ba5a..5e69a37a3d7 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java @@ -68,8 +68,7 @@ public Term cast(Sort sort, Term term) { if (decl == null) { return term; } - ImmutableList args = - ImmutableSLList.nil().prepend(new SortArg(sort)); + ImmutableList args = ImmutableSLList.singleton(new SortArg(sort)); ParametricFunctionInstance castFn = ParametricFunctionInstance.get(decl, args); return tf.createTerm(castFn, term); } From 4d27a10d0cbab39d81ff8b9df3e534f4846a853d Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 17 Jun 2026 10:01:55 +0200 Subject: [PATCH 4/5] Remove incorrect cast rule --- .../resources/org/key_project/rusty/proof/rules/cast.key | 7 ------- 1 file changed, 7 deletions(-) diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key index 3ff00f2f4df..b641c37ccb9 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key @@ -38,11 +38,4 @@ \replacewith(castAlphaArg) \heuristics(simplify, cast_deletion) }; - - // genericRules.key: nested-cast collapse — the outer cast determines the sort. - castCast { - \find(cast<[alpha]>(cast<[beta]>(castArg))) - \replacewith(cast<[alpha]>(castArg)) - \heuristics(simplify, cast_deletion) - }; } From fd3e4a5a2cd59d67eab6b91facb297633d25cb2f Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 17 Jun 2026 10:39:42 +0200 Subject: [PATCH 5/5] Fix loop type computation --- .../rusty/ast/expr/InfiniteLoopExpression.java | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java index 0ce6ffefce0..5ae9b318d38 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java @@ -12,6 +12,7 @@ import org.key_project.rusty.ast.Label; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.ast.abstraction.Never; +import org.key_project.rusty.ast.abstraction.TupleType; import org.key_project.rusty.ast.abstraction.Type; import org.key_project.rusty.ast.visitor.RustyASTWalker; import org.key_project.rusty.ast.visitor.Visitor; @@ -87,10 +88,11 @@ private Type computeType(Services services) { return Never.INSTANCE; } var breaksIt = breaks.iterator(); - Type tyMax = breaksIt.next().type(services); + Expr expr = breaksIt.next().expr(); + Type tyMax = expr == null ? TupleType.UNIT : expr.type(services); while (breaksIt.hasNext()) { - var b = breaksIt.next(); - var ty = b.type(services); + expr = breaksIt.next().expr(); + var ty = expr == null ? TupleType.UNIT : expr.type(services); if (ty == Never.INSTANCE) { continue; }