diff --git a/key.core/build.gradle b/key.core/build.gradle index 26f2e0a6ab7..0f2aa5bedff 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -285,3 +285,17 @@ tasks.register("testRAP", Test) { sourceSets.test.java.srcDirs(rapDir) sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key) + +// Measurement probe for the lemma reuse potential of One Step Simplifier applications +// (see de.uka.ilkd.key.rule.lemma.OssLemmaReuseProbe). Not part of the regular test suite. +tasks.register('runOssReuseProbe', Test) { + group = "verification" + description = "Measures potential lemma reuse of OSS applications on example proofs." + useJUnitPlatform { includeTags 'performance' } + filter { includeTestsMatching "de.uka.ilkd.key.rule.lemma.OssLemmaReuseProbe" } + testClassesDirs = sourceSets.test.output.classesDirs + classpath = sourceSets.test.runtimeClasspath + systemProperty "key.disregardSettings", "true" + maxHeapSize = "4g" + testLogging.showStandardStreams = true +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java index 27fc080a30b..a92c6cae07d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java @@ -18,6 +18,8 @@ import de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring; import de.uka.ilkd.key.rule.label.TermLabelPolicy; import de.uka.ilkd.key.rule.label.TermLabelRefactoring; +import de.uka.ilkd.key.rule.lemma.AddLiteralsLemmaIntroductionRule; +import de.uka.ilkd.key.rule.lemma.OssLemmaIntroductionRule; import de.uka.ilkd.key.rule.merge.MergeRule; import de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler; import de.uka.ilkd.key.strategy.ModularJavaDLStrategyFactory; @@ -180,7 +182,9 @@ protected ImmutableList initBuiltInRules() { .prepend(LoopApplyHeadRule.INSTANCE).prepend(JmlAssertRule.ASSERT_INSTANCE) .prepend(JmlAssertRule.ASSUME_INSTANCE) .prepend(SetStatementRule.INSTANCE) - .prepend(ObserverToUpdateRule.INSTANCE); + .prepend(ObserverToUpdateRule.INSTANCE) + .prepend(AddLiteralsLemmaIntroductionRule.INSTANCE) + .prepend(OssLemmaIntroductionRule.INSTANCE); // contract insertion rule, ATTENTION: ProofMgt relies on the fact // that Contract insertion rule is the FIRST element of this list! diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java index 41ee259f925..299e45a0b07 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.proof.RuleAppListener; import de.uka.ilkd.key.proof.init.ContractPO; import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.rule.lemma.GeneratedLemmaJustification; import de.uka.ilkd.key.speclang.Contract; import org.key_project.prover.rules.RuleApp; @@ -196,6 +197,15 @@ public void updateProofStatus() { } } + // revert status of all "presumably closed" proofs that use a generated lemma taclet + // whose soundness proof obligation has not been created or has not been closed + for (Proof p : presumablyClosed) { + if (hasUnprovenGeneratedLemma(p, new LinkedHashSet<>())) { + p.mgt().proofStatus = ProofStatus.CLOSED_BUT_LEMMAS_LEFT; + presumablyClosed = presumablyClosed.remove(p); + } + } + // revert status of all "presumably closed" proofs for which at least one // used contract is definitely not proven to "lemmas left" boolean changed = true; @@ -224,6 +234,31 @@ public void updateProofStatus() { } + /** + * Checks (transitively through the soundness proofs) whether the given proof relies on a + * taclet generated by a {@link de.uka.ilkd.key.rule.lemma.LemmaTacletGenerator} whose + * soundness proof obligation has not been created, has been disposed, or is not closed. + * Soundness proofs live in a copied initial configuration and are therefore inspected + * directly instead of via their (possibly never updated) proof status. + */ + private static boolean hasUnprovenGeneratedLemma(Proof p, Set visited) { + if (!visited.add(p)) { + return false; + } + for (RuleApp ruleApp : p.mgt().cachedRuleApps) { + if (p.mgt().getJustification(ruleApp) instanceof GeneratedLemmaJustification just) { + final Proof soundnessProof = just.getSoundnessProof(); + if (soundnessProof == null || soundnessProof.isDisposed() + || !soundnessProof.closed() + || hasUnprovenGeneratedLemma(soundnessProof, visited)) { + return true; + } + } + } + return false; + } + + public void ruleApplied(RuleApp r) { RuleJustification rj = getJustification(r); if (rj == null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustification.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustification.java index aa3f25fe863..32837b6f79f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustification.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustification.java @@ -6,4 +6,18 @@ public interface RuleJustification { boolean isAxiomJustification(); + + /** + * Returns true iff this justification is local to the proof it was created in, e.g. because + * it refers to the proof node that introduced the justified rule. Proof-local justifications + * are not carried over when an initial configuration is copied for another proof: they would + * reference foreign proof nodes there, and the stale entries would collide with the rule + * (re-)introductions of the new proof (dynamically introduced rules such as {@code \addrule} + * taclets or generated lemmas register their justification when they are introduced). + * + * @return true iff this justification must not survive an initial-configuration copy + */ + default boolean isProofLocal() { + return false; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationByAddRules.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationByAddRules.java index ac3c30f846b..81cfdd355f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationByAddRules.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationByAddRules.java @@ -21,6 +21,12 @@ public record RuleJustificationByAddRules(Node node, boolean isAxiom) implements @Override public boolean isAxiomJustification() { return isAxiom; } + @Override + public boolean isProofLocal() { + // refers to the node of its proof at which the rule was introduced + return true; + } + public RuleApp motherTaclet() { return node.getAppliedRuleApp(); } public String toString() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java index 6008e87d1c3..697c93a012a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java @@ -55,7 +55,15 @@ public void removeJustificationFor(Rule rule) { public RuleJustificationInfo copy() { RuleJustificationInfo info = new RuleJustificationInfo(); - info.rule2Justification.putAll(rule2Justification); + for (Map.Entry entry : rule2Justification.entrySet()) { + // proof-local justifications (dynamically introduced rules such as addrule taclets + // or generated lemmas) refer to nodes of the proof they were created in; carrying + // them into a copied configuration would leave stale entries there that collide + // with the rule (re-)introductions of the new proof + if (!entry.getValue().isProofLocal()) { + info.rule2Justification.put(entry.getKey(), entry.getValue()); + } + } return info; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index e5817e32ee8..c28ad491c6d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -323,7 +323,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { * @param newSequent sequent * @return the formula in the sequent, or null if not found */ - private PosInOccurrence findInNewSequent(PosInOccurrence oldPos, + protected PosInOccurrence findInNewSequent(PosInOccurrence oldPos, Sequent newSequent) { SequentFormula oldFormula = oldPos.sequentFormula(); Semisequent semiSeq = oldPos.isInAntec() ? newSequent.antecedent() diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java index 9329c7c1a17..f2242c610fc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java @@ -7,6 +7,7 @@ import java.util.LinkedHashSet; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.VariableSV; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.QuantifiableVariable; @@ -75,6 +76,14 @@ private boolean correct(JTerm t) { for (int i = 0, ar = t.arity(); i < ar; i++) { for (int j = 0, sz = t.varsBoundHere(i).size(); j < sz; j++) { final QuantifiableVariable qv = t.varsBoundHere(i).get(j); + if (!(qv instanceof VariableSV)) { + // the uniqueness restriction is about schema variables (see class comment): + // a doubly bound schema variable would have to match the same quantified + // variable everywhere and the taclet would almost never apply. Concrete + // bound variables, as they occur in taclets generated from proof formulas, + // may legitimately be bound several times (they stem from the same sequent). + continue; + } if (boundVars.contains(qv)) { return false; } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java index 35c6d0fd325..e2977085be9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java @@ -88,6 +88,17 @@ public static final class Protocol extends ArrayList { private TacletIndex[] indices; private Map[] notSimplifiableCaches; private boolean active; + /** + * In transparent mode (strategy option {@link StrategyProperties#OSS_TRANSPARENT}), this + * rule itself is never applicable and no taclets are taken over from the goals' rule + * indices: lemma-eligible formulas are simplified via + * {@link de.uka.ilkd.key.rule.lemma.OssLemmaIntroductionRule} (an inspectable, separately + * provable taclet per aggregated simplification), and all other formulas are simplified by + * the ordinary strategy with the individual rules. The simplifier machinery stays active + * solely as the computation core of the lemma generator (see + * {@link #computeSimplification(Goal, PosInOccurrence, Protocol)}). + */ + private boolean transparent; // ------------------------------------------------------------------------- // constructors @@ -149,7 +160,9 @@ private ImmutableList tacletsForRuleSet(Proof proof, String ruleSetName, } if (accept) { - appsTakenOver = appsTakenOver.prepend(app); + if (!transparent) { + appsTakenOver = appsTakenOver.prepend(app); + } result = result.prepend(tac); } } @@ -164,7 +177,10 @@ private ImmutableList tacletsForRuleSet(Proof proof, String ruleSetName, assert Immutables.isDuplicateFree(result) : "If this fails unexpectedly, add a call to Immutables.removeDuplicates."; - // remove apps in appsTakenOver from taclet indices of all goals + // Remove apps in appsTakenOver from taclet indices of all goals. In transparent mode + // nothing is taken over: the captured rule sets remain available to the ordinary + // strategy (formulas outside the lemma fragment are simplified by individual, visible + // rule applications), and the indices built here serve only the lemma generator. for (NoPosTacletApp app : appsTakenOver) { for (Goal goal : proof.allGoals()) { goal.ruleAppIndex().removeNoPosTacletApp(app); @@ -538,16 +554,24 @@ private synchronized void refresh(Proof proof) { settings = ProofSettings.DEFAULT_SETTINGS; } - final boolean newActive = settings.getStrategySettings().getActiveStrategyProperties() - .get(StrategyProperties.OSS_OPTIONS_KEY).equals(StrategyProperties.OSS_ON); + final Object ossMode = settings.getStrategySettings().getActiveStrategyProperties() + .get(StrategyProperties.OSS_OPTIONS_KEY); + final boolean newActive = StrategyProperties.OSS_ON.equals(ossMode) + || StrategyProperties.OSS_TRANSPARENT.equals(ossMode); + final boolean newTransparent = StrategyProperties.OSS_TRANSPARENT.equals(ossMode); - if (active != newActive || lastProof != proof || // The setting or proof has changed. - (isShutdown() && !proof.closed())) { // A closed proof was pruned. + if (active != newActive || transparent != newTransparent || lastProof != proof + // The setting or proof has changed. + || (isShutdown() && !proof.closed())) { // A closed proof was pruned. + // restore any taken-over taclets before re-initializing: switching between the + // opaque and the transparent mode changes whether the captured rule sets are + // removed from the goals' rule indices, and initIndices alone would not rebuild + // for an unchanged proof + shutdownIndices(); active = newActive; + transparent = newTransparent; if (active && proof != null && !proof.closed()) { initIndices(proof); - } else { - shutdownIndices(); } } } @@ -571,8 +595,13 @@ public static void refreshOSS(Proof proof) { } } - @Override - public boolean isApplicable(Goal goal, PosInOccurrence pio) { + /** + * Tells whether the simplifier machinery could simplify the formula at the given position, + * regardless of the transparent mode partition (see {@link #isApplicable(Goal, + * PosInOccurrence)}). This is the applicability notion used by + * {@link de.uka.ilkd.key.rule.lemma.OssLemmaGenerator}. + */ + public boolean canSimplify(Goal goal, PosInOccurrence pio) { // abort if switched off if (!active) { return false; @@ -594,6 +623,19 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) { null); } + @Override + public boolean isApplicable(Goal goal, PosInOccurrence pio) { + // In transparent mode this rule performs no simplification at all: lemma-eligible + // formulas are handled by the lemma introduction rule, and all other formulas are + // simplified by the ordinary strategy with the individual rules (which stay in the + // goals' rule indices, see tacletsForRuleSet). The simplifier machinery remains active + // solely as the computation core of the lemma generator. + if (transparent) { + return false; + } + return canSimplify(goal, pio); + } + @Override public synchronized @NonNull ImmutableList apply(Goal goal, RuleApp ruleApp) { @@ -668,6 +710,51 @@ public String toString() { return displayName(); } + /** + * Result of a one-step-simplification computation performed by + * {@link #computeSimplification(Goal, PosInOccurrence, Protocol)}. + * + * @param simplified the fully simplified sequent formula + * @param numAppliedRules the number of rule applications aggregated in the result + * @param usedContextFormulas the positions of the context formulas used by replace-known + * steps (the assumptions the result depends on; empty if the simplification is a pure + * equivalence transformation) + */ + public record SimplificationResult(SequentFormula simplified, int numAppliedRules, + ImmutableList usedContextFormulas) { + } + + /** + * Computes the overall simplification result for the formula at the given position exactly as + * an application of this rule would, but without modifying the goal or the proof. This is the + * side-effect-free core of the one step simplifier, usable by clients that want to capture + * the aggregated transformation in a different form (e.g., as a generated lemma taclet). + * + *

+ * Requires the simplifier to be active for the goal's proof (see {@link #refreshOSS(Proof)}). + * + * @param goal the goal whose sequent provides the context formulas for replace-known + * @param pos the position of the (top level) formula to simplify + * @param protocol if non-null, the performed rule applications are reported to this protocol + * @return the simplification result, or {@code null} if the simplifier is not active for this + * proof or the formula cannot be simplified + */ + public synchronized SimplificationResult computeSimplification(Goal goal, + PosInOccurrence pos, Protocol protocol) { + if (!active || indices == null || goal.proof() != lastProof) { + return null; + } + // a rule app is required for term label instantiation during replace-known + final OneStepSimplifierRuleApp ruleApp = createApp(pos, goal.proof().getServices()); + final Instantiation inst = + computeInstantiation(pos, goal.sequent(), protocol, goal, ruleApp); + if (inst.getCf() == null || inst.getCf().equals(pos.sequentFormula())) { + return null; + } + return new SimplificationResult(inst.getCf(), inst.getNumAppliedRules(), + inst.getIfInsts()); + } + /** * Gets an immutable set containing all the taclets captured by the OSS. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/AddLiteralsLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/AddLiteralsLemmaGenerator.java new file mode 100644 index 00000000000..cfdcb9ec8eb --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/AddLiteralsLemmaGenerator.java @@ -0,0 +1,86 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.math.BigInteger; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.IntegerLDT; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.AbstractTermTransformer; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.RewriteTaclet; +import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.prover.rules.RuleSet; +import org.key_project.prover.sequent.PosInOccurrence; + +import org.jspecify.annotations.NullMarked; + +/** + * Toy lemma generator used to evaluate the taclet-generating transformer approach: for a sum of + * two integer literals it produces the ground rewrite taclet {@code \find(i + j) \replacewith(k)} + * with {@code k} the literal denoting the sum. + * + *

+ * This covers the same ground as the system taclet {@code add_literals}, whose right-hand side is + * computed by the metaconstruct {@code #add} at application time and is therefore neither + * inspectable nor amenable to a soundness proof obligation. The taclets produced here are + * metaconstruct-free, so the standard lemma machinery applies. The system taclet remains in the + * rule base untouched; in particular it serves as the ground truth for discharging the generated + * proof obligations. + */ +@NullMarked +public final class AddLiteralsLemmaGenerator implements LemmaTacletGenerator { + + public static final AddLiteralsLemmaGenerator INSTANCE = new AddLiteralsLemmaGenerator(); + + private static final Name NAME = new Name("addLitLemma"); + + private AddLiteralsLemmaGenerator() { + } + + @Override + public Name name() { + return NAME; + } + + @Override + public boolean isApplicable(Goal goal, PosInOccurrence pio) { + final IntegerLDT integerLDT = + goal.proof().getServices().getTypeConverter().getIntegerLDT(); + final Term term = pio.subTerm(); + return term.op() == integerLDT.getAdd() + && term.sub(0).op() == integerLDT.getNumberSymbol() + && term.sub(1).op() == integerLDT.getNumberSymbol(); + } + + @Override + public GeneratedTaclet generate(Goal goal, PosInOccurrence pio) { + final Services services = goal.proof().getServices(); + final JTerm find = (JTerm) pio.subTerm(); + + final BigInteger left = + new BigInteger(AbstractTermTransformer.convertToDecimalString(find.sub(0), services)); + final BigInteger right = + new BigInteger(AbstractTermTransformer.convertToDecimalString(find.sub(1), services)); + final JTerm sum = services.getTermBuilder().zTerm(left.add(right).toString()); + + final RewriteTacletBuilder tb = new RewriteTacletBuilder<>(); + // the name is derived from the term content only, so that replay and reuse across + // branches resolve to the same taclet + tb.setName(MiscTools.toValidTacletName(NAME + "_" + left + "_" + right)); + tb.setDisplayName(NAME.toString()); + tb.setFind(find); + tb.addGoalTerm(sum); + final RuleSet generatedLemmaRS = + services.getNamespaces().ruleSets().lookup(new Name("generatedLemma")); + tb.addRuleSet(generatedLemmaRS != null ? generatedLemmaRS + : new RuleSet(new Name("generatedLemma"))); + return new GeneratedTaclet(tb.getTaclet(), 1); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/AddLiteralsLemmaIntroductionRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/AddLiteralsLemmaIntroductionRule.java new file mode 100644 index 00000000000..a854de71e37 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/AddLiteralsLemmaIntroductionRule.java @@ -0,0 +1,22 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import org.jspecify.annotations.NullMarked; + +/** + * Introduction rule for {@link AddLiteralsLemmaGenerator}: at a sum of two integer literals it + * introduces the ground rewrite taclet folding the sum, together with its soundness proof + * obligation. + */ +@NullMarked +public final class AddLiteralsLemmaIntroductionRule extends LemmaIntroductionRule { + + public static final AddLiteralsLemmaIntroductionRule INSTANCE = + new AddLiteralsLemmaIntroductionRule(); + + private AddLiteralsLemmaIntroductionRule() { + super(AddLiteralsLemmaGenerator.INSTANCE); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemma.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemma.java new file mode 100644 index 00000000000..e60a750e458 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemma.java @@ -0,0 +1,223 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.io.OutputStreamProofSaver; +import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.rule.RewriteTaclet; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate; +import de.uka.ilkd.key.settings.ProofSettings; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.ProofObligationCreator; + +import org.key_project.logic.Name; +import org.key_project.prover.sequent.Sequent; +import org.key_project.util.collection.DefaultImmutableSet; +import org.key_project.util.collection.ImmutableSet; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +/** + * A taclet created by a {@link LemmaTacletGenerator} together with its soundness proof. + * + *

+ * The soundness proof obligation is created lazily on first request and in particular + * not during the rule application that introduces the taclet: proof search must not pay + * for the proof obligation, and rule applications should not have side effects beyond the proof + * tree. As long as the soundness proof has not been created (or not been closed), any proof using + * the taclet is only closed modulo this lemma (see + * {@link de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt}). + */ +@NullMarked +public final class GeneratedLemma { + + private final RewriteTaclet taclet; + private final Proof mainProof; + private final GeneratedLemmaJustification justification; + private final int aggregatedSteps; + private @Nullable ProofAggregate soundnessProofAggregate; + private @Nullable Proof soundnessProof; + private boolean registeredInEnvironment; + + GeneratedLemma(RewriteTaclet taclet, Proof mainProof, Name generatorName, + int aggregatedSteps) { + this.taclet = taclet; + this.mainProof = mainProof; + this.justification = new GeneratedLemmaJustification(generatorName, this); + this.aggregatedSteps = aggregatedSteps; + } + + /** + * returns the number of base calculus steps the lemma aggregates (display and measurement + * metadata) + */ + public int aggregatedSteps() { + return aggregatedSteps; + } + + /** + * returns the justification of the taclet; the identical instance is (re-)registered whenever + * the lemma is introduced, since pruning removes the justification together with the + * goal-locally introduced taclet + */ + public GeneratedLemmaJustification justification() { + return justification; + } + + /** + * returns the generated taclet; within one proof there is exactly one taclet instance per + * lemma name (see {@link GeneratedLemmaRegistry}) + */ + public RewriteTaclet taclet() { + return taclet; + } + + /** + * returns the name of the generator that produced this lemma + */ + public Name generatorName() { + return justification.getGenerator(); + } + + /** + * A key identifying this lemma by its content, independent of the introduction point: + * printed find, assumptions (by polarity), and replacewith. Lemmas with the same content key + * denote the same simplification and are grouped for display (there may be many, one per + * introduction point / branch). Note that content-equal lemmas are still distinct taclets + * with their own soundness obligations, since their proof-local symbols may differ. + */ + public String contentKey() { + final Services services = mainProof.getServices(); + final StringBuilder key = new StringBuilder(); + key.append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels((JTerm) taclet.find(), services), services)); + final Sequent assumes = taclet.assumesSequent(); + for (final var sf : assumes.antecedent()) { + key.append("\n<= ").append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels((JTerm) sf.formula(), services), + services)); + } + for (final var sf : assumes.succedent()) { + key.append("\n=> ").append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels((JTerm) sf.formula(), services), + services)); + } + final JTerm rw = (JTerm) ((RewriteTacletGoalTemplate) taclet.goalTemplates().head()) + .replaceWith(); + key.append("\n~> ").append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels(rw, services), services)); + return key.toString(); + } + + /** + * returns the soundness proof if it has already been created, and {@code null} otherwise; the + * proof obligation is not created by this method + */ + public synchronized @Nullable Proof getSoundnessProofIfPresent() { + return soundnessProof; + } + + /** + * returns true iff the soundness proof obligation has been created and is not disposed + */ + public synchronized boolean isSoundnessProofPresent() { + return soundnessProof != null && !soundnessProof.isDisposed(); + } + + /** + * returns true iff the soundness proof obligation has been created and closed + */ + public synchronized boolean isProven() { + return isSoundnessProofPresent() && soundnessProof.closed(); + } + + /** + * returns the proof for the soundness proof obligation of the taclet, creating it (but + * not registering it in the proof environment) on first call + */ + public synchronized Proof getOrCreateSoundnessProof() { + return getOrCreateSoundnessProofAggregate().getFirstProof(); + } + + /** + * returns the proof aggregate for the soundness proof obligation of the taclet, creating it + * on first call. Creation does not register the obligation in the proof environment + * — a batch that proves and closes many obligations should not flood the environment (and a + * user interface) with closed side proofs. Registration is an explicit, separate step (see + * {@link #registerInEnvironment()}); the main proof's status tracks the obligation through + * this lemma regardless of registration. + */ + public synchronized ProofAggregate getOrCreateSoundnessProofAggregate() { + if (soundnessProof == null || soundnessProof.isDisposed()) { + soundnessProofAggregate = createSoundnessProof(); + soundnessProof = soundnessProofAggregate.getFirstProof(); + registeredInEnvironment = false; + } + return soundnessProofAggregate; + } + + /** + * Registers the soundness proof obligation in the main proof's environment (creating it + * first if necessary), so that a user interface listening on the environment displays and + * can drive it. Idempotent; does nothing if there is no environment. + * + * @return the registered aggregate + */ + public synchronized ProofAggregate registerInEnvironment() { + final ProofAggregate aggregate = getOrCreateSoundnessProofAggregate(); + final ProofEnvironment env = mainProof.getEnv(); + if (env != null && !registeredInEnvironment) { + env.registerProof(new GeneratedLemmaPO(taclet.name(), aggregate), aggregate); + registeredInEnvironment = true; + } + return aggregate; + } + + /** + * Creates the soundness proof obligation for the taclet, reusing the standard taclet lemma + * machinery. The proof runs in a copy of the main proof's initial configuration; the + * generated taclet itself is not part of that configuration, so it cannot be used to prove + * itself. + */ + private ProofAggregate createSoundnessProof() { + final InitConfig poConfig = mainProof.getInitConfig().deepCopy(); + // The soundness of a generated lemma must be established in the base calculus, using the + // individual rewrite rules the lemma aggregates. The one step simplifier is switched off + // entirely for the obligation: not only its transparent mode (which would discharge the + // obligation by generating and applying further lemmas — re-doing the very simplification + // it must justify, a circular and non-terminating justification), but also its opaque + // mode, which performs the same aggregated simplification in one hidden step and would + // therefore close the obligation by exactly the transformation under scrutiny. + disableOneStepSimplification(poConfig); + final ImmutableSet tacletsToProve = DefaultImmutableSet.nil().add(taclet); + + final ProofAggregate po = new ProofObligationCreator().create(tacletsToProve, + new InitConfig[] { poConfig }, DefaultImmutableSet.nil(), List.of()); + return po; + } + + /** + * Switches the one step simplifier off in the given configuration, so that the soundness + * proof is conducted in the base calculus (see {@link #createSoundnessProof()}). + */ + private static void disableOneStepSimplification(InitConfig config) { + final ProofSettings settings = config.getSettings(); + if (settings == null) { + return; + } + final StrategyProperties sp = + settings.getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_OFF); + settings.getStrategySettings().setActiveStrategyProperties(sp); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaJustification.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaJustification.java new file mode 100644 index 00000000000..5ea67fc06fe --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaJustification.java @@ -0,0 +1,81 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.mgt.RuleJustification; + +import org.key_project.logic.Name; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +/** + * Justification for a taclet created by a {@link LemmaTacletGenerator}: the taclet is a lemma + * whose validity is established by a dedicated soundness proof, not an axiom and not a consequence + * of the introducing rule application (which merely computed it). + */ +@NullMarked +public final class GeneratedLemmaJustification implements RuleJustification { + + private final Name generator; + private final GeneratedLemma lemma; + + public GeneratedLemmaJustification(Name generator, GeneratedLemma lemma) { + this.generator = generator; + this.lemma = lemma; + } + + @Override + public boolean isAxiomJustification() { + return false; + } + + @Override + public boolean isProofLocal() { + // tied to the introducing proof: the lemma and its soundness proof live there, and the + // justification is (re-)registered whenever the lemma is introduced + return true; + } + + /** + * returns the name of the generator that created the justified taclet + */ + public Name getGenerator() { + return generator; + } + + /** + * returns the justified lemma + */ + public GeneratedLemma getLemma() { + return lemma; + } + + /** + * returns the soundness proof for the justified taclet, or {@code null} if it has not been + * created yet + */ + public @Nullable Proof getSoundnessProof() { + return lemma.getSoundnessProofIfPresent(); + } + + /** + * returns true iff the soundness proof obligation of the justified taclet has been created + * and closed (possibly itself depending on further unproven lemmas, which is tracked by + * {@link de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt}) + */ + public boolean isProven() { + return lemma.isProven(); + } + + @Override + public String toString() { + final Proof soundnessProof = lemma.getSoundnessProofIfPresent(); + return "generated lemma (by " + generator + ", " + + (soundnessProof == null ? "soundness proof obligation not yet created" + : (soundnessProof.closed() ? "proven" : "soundness proof open")) + + ")"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaPO.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaPO.java new file mode 100644 index 00000000000..5c4bbfe0c13 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaPO.java @@ -0,0 +1,52 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.proof.init.ProofOblInput; + +import org.key_project.logic.Name; + +/** + * Proof obligation input for the soundness proof of a taclet created by a + * {@link LemmaTacletGenerator}. The proof obligation itself is created eagerly when the lemma is + * generated (see {@link GeneratedLemmaRegistry}); this class merely identifies it towards the + * proof environment. + */ +public class GeneratedLemmaPO implements ProofOblInput { + + private final Name tacletName; + private final ProofAggregate po; + + public GeneratedLemmaPO(Name tacletName, ProofAggregate po) { + this.tacletName = tacletName; + this.po = po; + } + + @Override + public String name() { + return "Taclet: " + tacletName; + } + + @Override + public void readProblem() { + // the proof obligation has already been constructed + } + + @Override + public ProofAggregate getPO() { + return po; + } + + @Override + public boolean implies(ProofOblInput po) { + return this == po; + } + + @Override + public KeYJavaType getContainerType() { + return null; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaRegistry.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaRegistry.java new file mode 100644 index 00000000000..6d2974d283d --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/GeneratedLemmaRegistry.java @@ -0,0 +1,213 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; + +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.RewriteTaclet; + +import org.key_project.logic.Name; +import org.key_project.prover.rules.RuleAbortException; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.LRUCache; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +/** + * Proof-local registry of the taclets created by {@link LemmaTacletGenerator}s. + * + *

+ * The registry guarantees that per proof there is exactly one taclet instance (and one soundness + * proof obligation) per lemma name. This makes repeated introductions of the same lemma — on + * sibling branches, or after pruning and redoing the introduction — resolve to the already + * existing taclet instead of creating duplicates. Reusing the identical taclet instance is also + * required by the rule justification bookkeeping, which rejects re-registration of a distinct + * rule under an existing name. + */ +@NullMarked +public final class GeneratedLemmaRegistry { + + private static final int VETO_CACHE_SIZE = 1000; + + private final Map lemmas = new LinkedHashMap<>(); + + /** + * Formulas for which lemma generation turned out not to be worthwhile (the aggregated + * transformation is a semantic no-op). Vetoed formulas are not offered for introduction + * again: without this, automation would not terminate. The veto is proof-local state — a + * JVM-wide cache would leak vetoes into the replay of a reloaded proof, where a formula + * vetoed late in the original run (in some branch context) would suppress the replay of an + * introduction recorded earlier (in another context). + */ + private final Map vetoed = new LRUCache<>(VETO_CACHE_SIZE); + + private GeneratedLemmaRegistry() { + } + + /** + * marks the formula as not worth a lemma (see {@link #vetoed}) + */ + public synchronized void veto(SequentFormula formula) { + vetoed.put(formula, Boolean.TRUE); + } + + /** + * returns true iff lemma generation has been vetoed for the given formula + */ + public synchronized boolean isVetoed(SequentFormula formula) { + return vetoed.get(formula) != null; + } + + /** + * returns the registry of the given proof, creating it on first access + */ + public static GeneratedLemmaRegistry get(Proof proof) { + GeneratedLemmaRegistry registry = proof.lookup(GeneratedLemmaRegistry.class); + if (registry == null) { + registry = new GeneratedLemmaRegistry(); + proof.register(registry, GeneratedLemmaRegistry.class); + } + return registry; + } + + /** + * returns the lemma generated by the given generator for the term at the given position. If a + * lemma of the same name has been generated before, the existing one is returned; otherwise + * the taclet is generated and registered with a {@link GeneratedLemmaJustification}. The + * soundness proof obligation is not created here but lazily on first request (see + * {@link GeneratedLemma#getOrCreateSoundnessProof()}), keeping it off the proof search path. + * + * @param goal the current goal + * @param pio the position of the term to be transformed + * @param generator the generator computing the lemma taclet + * @return the (possibly cached) generated lemma + */ + public synchronized GeneratedLemma getOrCreate(Goal goal, PosInOccurrence pio, + LemmaTacletGenerator generator) { + final Proof proof = goal.proof(); + final LemmaTacletGenerator.GeneratedTaclet generated = generator.generate(goal, pio); + final RewriteTaclet taclet = generated.taclet(); + + final GeneratedLemma existing = lemmas.get(taclet.name()); + if (existing != null) { + // a name hit must mean identical content: formulas on different branches can be + // equal in their printed form yet contain distinct proof-local symbol instances, + // and handing out a taclet for the wrong instances would produce a rule that never + // matches. Generators avoid this by making names unique per introduction where + // necessary; this check turns any residual name aliasing into a visible abort. + if (!existing.taclet().find().equals(taclet.find())) { + throw new RuleAbortException("generated lemma name aliasing: " + taclet.name() + + " already denotes a lemma with different content" + + " (distinct proof-local symbols?)"); + } + // pruning removes the justification together with the goal-locally introduced + // taclet; re-register the identical justification instance in that case + if (proof.getInitConfig().getJustifInfo() + .getJustification(existing.taclet()) == null) { + proof.getInitConfig().registerRule(existing.taclet(), existing.justification()); + } + return existing; + } + + final GeneratedLemma lemma = + new GeneratedLemma(taclet, proof, generator.name(), generated.aggregatedSteps()); + // The registry owns the generated-lemma namespace of its proof. A justification entry + // for this name that the registry does not know stems from a copied initial + // configuration (InitConfig.deepCopy copies the justification map): e.g. when a proof + // run in transparent mode is elaborated onto a fresh proof for transparent saving, the + // fresh configuration inherits the original run's lemma justifications, and the + // elaboration deliberately regenerates the same (replay-stable) names. Such foreign + // entries are replaced by this proof's own. + if (proof.getInitConfig().getJustifInfo().getJustification(taclet) != null) { + proof.getInitConfig().getJustifInfo().removeJustificationFor(taclet); + } + proof.getInitConfig().registerRule(taclet, lemma.justification()); + lemmas.put(taclet.name(), lemma); + return lemma; + } + + /** + * returns the lemma registered under the given name, or {@code null} if there is none + */ + public synchronized @Nullable GeneratedLemma lookup(Name name) { + return lemmas.get(name); + } + + /** + * returns all lemmas generated for this proof so far + */ + public synchronized Collection getLemmas() { + return Collections.unmodifiableCollection(lemmas.values()); + } + + /** + * returns the lemmas generated for this proof whose soundness proof obligation has not yet + * been discharged — either it has not been created, or it has been created but is not closed. + * These are the lemmas that the proof is still closed only modulo (see + * {@link de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt}). + * + * @return the missing lemmas, in generation order + */ + public synchronized List getMissingLemmas() { + final List missing = new ArrayList<>(); + for (final GeneratedLemma lemma : lemmas.values()) { + if (!lemma.isProven()) { + missing.add(lemma); + } + } + return missing; + } + + /** + * groups the generated lemmas by their generator, preserving generation order within each + * group + * + * @return a map from generator name to the lemmas it produced + */ + public synchronized Map> getLemmasByGenerator() { + final Map> byGenerator = new LinkedHashMap<>(); + for (final GeneratedLemma lemma : lemmas.values()) { + byGenerator.computeIfAbsent(lemma.generatorName(), k -> new ArrayList<>()).add(lemma); + } + return byGenerator; + } + + /** + * groups the given lemmas by their content key (see {@link GeneratedLemma#contentKey()}), so + * that lemmas denoting the same simplification (differing only in introduction point and + * proof-local symbol renaming) are collapsed. The order of first appearance is preserved. + * + * @param lemmas the lemmas to group + * @return a map from content key to the lemmas sharing it + */ + public static Map> groupByContent( + Collection lemmas) { + final Map> byContent = new LinkedHashMap<>(); + for (final GeneratedLemma lemma : lemmas) { + byContent.computeIfAbsent(lemma.contentKey(), k -> new ArrayList<>()).add(lemma); + } + return byContent; + } + + /** + * returns the registry of the given proof if one exists, without creating it; used by clients + * that only inspect (e.g. the user interface) and must not attach a registry to proofs that + * never generated a lemma + * + * @param proof the proof + * @return the registry, or {@code null} if the proof has no generated lemmas + */ + public static @Nullable GeneratedLemmaRegistry getIfPresent(Proof proof) { + return proof.lookup(GeneratedLemmaRegistry.class); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaElaboratingProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaElaboratingProofReplayer.java new file mode 100644 index 00000000000..4ed36b8cf56 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaElaboratingProofReplayer.java @@ -0,0 +1,137 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.util.HashSet; + +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; +import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.rule.TacletApp; + +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +/** + * A-posteriori proof elaboration ("mode 2" of the taclet-generating transformer approach): copies + * a proof onto a fresh proof of the same problem, replacing every eligible application of the one + * step simplifier by the two-step lemma form — an introduction of the generated taclet (see + * {@link OssLemmaGenerator}) followed by an ordinary application of that taclet. + * + *

+ * This decouples proof search from transparency: the proof is found with the fast opaque rule, + * and the finished proof is then elaborated into a form in which every aggregated simplification + * is a declarative, separately provable artifact. Simplifier applications that cannot be + * elaborated (formulas containing modal operators, or positions that cannot be relocated) are + * copied unchanged, so elaboration never fails a proof that copies cleanly. + */ +public class LemmaElaboratingProofReplayer extends CopyingProofReplayer { + + private int elaborated = 0; + private int copiedOss = 0; + + public LemmaElaboratingProofReplayer(Proof originalProof, Proof target) { + super(originalProof, target); + } + + /** + * Elaborates the original proof onto the target proof (a fresh proof of the same problem, + * open at its root). + * + * @param original the proof to elaborate + * @param target the fresh target proof; must have the same root sequent + * @return the replayer, for querying {@link #getElaboratedCount()} and + * {@link #getCopiedOssCount()} + */ + public static LemmaElaboratingProofReplayer elaborate(Proof original, Proof target) + throws IntermediateProofReplayer.BuiltInConstructionException { + final LemmaElaboratingProofReplayer replayer = + new LemmaElaboratingProofReplayer(original, target); + replayer.copy(original.root(), target.getOpenGoal(target.root()), new HashSet<>()); + return replayer; + } + + /** + * returns the number of one step simplifier applications replaced by introduction plus + * taclet application + */ + public int getElaboratedCount() { + return elaborated; + } + + /** + * returns the number of one step simplifier applications copied unchanged (not + * lemma-eligible) + */ + public int getCopiedOssCount() { + return copiedOss; + } + + @Override + protected ImmutableList reApplyRuleApp(Node node, Goal openGoal) + throws IntermediateProofReplayer.BuiltInConstructionException { + if (node.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp ossApp + && ossApp.posInOccurrence() != null) { + final PosInOccurrence pos = + findInNewSequent(ossApp.posInOccurrence(), openGoal.sequent()); + if (pos != null + && OssLemmaIntroductionRule.INSTANCE.isApplicable(openGoal, pos)) { + final ImmutableList result = elaborateOssStep(openGoal, pos); + if (result != null) { + elaborated++; + return result; + } + } + copiedOss++; + } + return super.reApplyRuleApp(node, openGoal); + } + + /** + * Replaces one simplifier application by lemma introduction plus taclet application. + * Returns the resulting goals, or {@code null} if the introduction is not possible (in which + * case the goal is untouched and the caller falls back to copying the original step). + */ + private ImmutableList elaborateOssStep(Goal openGoal, PosInOccurrence pos) { + final var services = openGoal.proof().getServices(); + + final ImmutableList afterIntro = openGoal + .apply(OssLemmaIntroductionRule.INSTANCE.createApp(pos, services)); + if (afterIntro == null) { + return null; + } + final Goal introGoal = afterIntro.head(); + + // the taclet introduced by the step just performed + final var introducedRules = introGoal.node().getLocalIntroducedRules().iterator(); + if (!introducedRules.hasNext()) { + throw new IllegalStateException( + "lemma introduction did not introduce a taclet at " + pos); + } + final NoPosTacletApp lemmaApp = introducedRules.next(); + + // the introduction step leaves the sequent unchanged, so the position stays valid + final NoPosTacletApp matched = lemmaApp.matchFind(pos, services); + if (matched == null) { + throw new IllegalStateException( + "generated lemma " + lemmaApp.taclet().name() + " does not match at " + pos); + } + TacletApp application = matched.setPosInOccurrence(pos, services); + if (!application.complete()) { + final ImmutableList instantiated = + application.findIfFormulaInstantiations(introGoal.sequent(), services); + if (instantiated.isEmpty()) { + throw new IllegalStateException("no assumption instantiation found for lemma " + + lemmaApp.taclet().name() + " although it was generated from this sequent"); + } + application = instantiated.head(); + } + return introGoal.apply(application); + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaIntroductionRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaIntroductionRule.java new file mode 100644 index 00000000000..fe804810b09 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaIntroductionRule.java @@ -0,0 +1,106 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.BuiltInRule; +import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp; +import de.uka.ilkd.key.rule.IBuiltInRuleApp; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.Name; +import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +/** + * Built-in rule that introduces a taclet computed by a {@link LemmaTacletGenerator} as a + * goal-local rule. + * + *

+ * The rule performs the introduction step only: it makes the generated taclet available + * on the resulting goal (registered with a {@link GeneratedLemmaJustification} pointing to its + * soundness proof obligation) but does not change the sequent. Actually rewriting with the lemma + * is an ordinary, separately recorded taclet application — this two-step structure is what makes + * the transformation inspectable and replayable. + * + *

+ * On proof replay, replaying an application of this rule re-runs the generator; since generators + * are deterministic in the term at the application position, the regenerated taclet carries the + * same name and the subsequent taclet application resolves against it. + */ +@NullMarked +public abstract class LemmaIntroductionRule implements BuiltInRule { + + private final LemmaTacletGenerator generator; + private final Name name; + + protected LemmaIntroductionRule(LemmaTacletGenerator generator) { + this.generator = generator; + this.name = new Name("introduce_" + generator.name()); + } + + public LemmaTacletGenerator getGenerator() { + return generator; + } + + @Override + public Name name() { + return name; + } + + @Override + public String toString() { + return displayName(); + } + + /** + * {@inheritDoc} + * + *

+ * The result must depend only on the formula at the position (and formula-keyed state such + * as the generator's veto bookkeeping), never on the goal-local rule indices: built-in rule + * applications are queued and may be executed after further rules changed the goal, and + * proof replay re-evaluates applicability freshly at the recorded position. An + * index-dependent condition would make recorded introductions unreplayable whenever the + * queued application was executed after the condition had changed. As a consequence, an + * introduction may occasionally be redundant (an equivalent lemma is already available); + * this is harmless, since lemma names are unique per introduction. + */ + @Override + public boolean isApplicable(Goal goal, @Nullable PosInOccurrence pio) { + return pio != null && generator.isApplicable(goal, pio); + } + + @Override + public boolean isApplicableOnSubTerms() { + return true; + } + + @Override + public IBuiltInRuleApp createApp(@Nullable PosInOccurrence pos, TermServices services) { + return new DefaultBuiltInRuleApp<>(this, pos); + } + + @Override + public @NonNull ImmutableList apply(Goal goal, RuleApp ruleApp) { + final PosInOccurrence pio = ruleApp.posInOccurrence(); + final GeneratedLemma lemma = + GeneratedLemmaRegistry.get(goal.proof()).getOrCreate(goal, pio, generator); + + final ImmutableList newGoals = goal.split(1); + final Goal newGoal = newGoals.head(); + final NoPosTacletApp tacletApp = NoPosTacletApp.createFixedNoPosTacletApp(lemma.taclet(), + SVInstantiations.EMPTY_SVINSTANTIATIONS, goal.proof().getServices()); + assert tacletApp != null : "generated lemma taclet could not be turned into a taclet app"; + newGoal.addNoPosTacletApp(tacletApp); + return newGoals; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaProver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaProver.java new file mode 100644 index 00000000000..834401f540f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaProver.java @@ -0,0 +1,153 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; + +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; +import de.uka.ilkd.key.util.MiscTools; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Batch-discharges the soundness proof obligations of generated lemmas: for each lemma it creates + * (if necessary) the obligation proof and runs automatic proof search with a step bound. Lemmas + * that close within the bound need no further attention; lemmas that do not are reported back so + * that they can be shown to the user for manual completion. + * + *

+ * Closed obligations are certificates and are deliberately not registered in the proof + * environment, so a batch over many obligations does not flood the environment (and an attached + * user interface) with closed side proofs; the main proof's status still tracks them through the + * lemmas. Obligations that remain open are registered (see + * {@link GeneratedLemma#registerInEnvironment()}) so that an attached user interface surfaces + * them for manual completion. + */ +@NullMarked +public final class LemmaProver { + + private static final Logger LOGGER = LoggerFactory.getLogger(LemmaProver.class); + + /** + * Outcome of a batch proving run. + * + * @param proven lemmas whose soundness obligation closed within the step bound + * @param remaining lemmas whose soundness obligation did not close (shown for manual work) + * @param saved the number of obligation proofs written to disk, or 0 if saving was disabled + */ + public record Result(List proven, List remaining, int saved) { + } + + /** + * Notified of the progress of a batch proving run, and asked whether to continue. + */ + @FunctionalInterface + public interface ProgressListener { + /** + * Called after each obligation has been processed. + * + * @param done the number of obligations processed so far + * @param total the total number of obligations + * @return {@code true} to continue, {@code false} to stop the batch (the remaining, + * unprocessed lemmas are not counted as {@code remaining} in the result) + */ + boolean progressed(int done, int total); + } + + private LemmaProver() { + } + + /** + * Attempts to discharge the soundness obligations of the given lemmas. + * + * @param lemmas the lemmas to prove + * @param maxSteps the automatic-mode step bound per obligation + * @param saveDir if non-null, a directory into which every obligation proof is saved + * @return the outcome + * @throws Exception if saving a proof fails + */ + public static Result proveAll(Collection lemmas, int maxSteps, + @Nullable Path saveDir) throws Exception { + return proveAll(lemmas, maxSteps, saveDir, null); + } + + /** + * Attempts to discharge the soundness obligations of the given lemmas, reporting progress. + * + * @param lemmas the lemmas to prove + * @param maxSteps the automatic-mode step bound per obligation + * @param saveDir if non-null, a directory into which every obligation proof is saved + * @param listener if non-null, notified after each obligation and asked whether to continue + * @return the outcome + * @throws Exception if saving a proof fails + */ + public static Result proveAll(Collection lemmas, int maxSteps, + @Nullable Path saveDir, @Nullable ProgressListener listener) throws Exception { + final List proven = new ArrayList<>(); + final List remaining = new ArrayList<>(); + int saved = 0; + int done = 0; + final int total = lemmas.size(); + + if (saveDir != null) { + Files.createDirectories(saveDir); + } + + for (final GeneratedLemma lemma : lemmas) { + if (lemma.isProven()) { + proven.add(lemma); + } else { + final Proof po = lemma.getOrCreateSoundnessProof(); + if (!po.closed()) { + try { + new AutomaticProver().start(po, maxSteps, -1); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } catch (RuntimeException e) { + // a single obligation whose automatic proof search fails must not abort + // the batch; it is reported as remaining for manual inspection + LOGGER.warn("automatic proof of lemma {} failed", + lemma.taclet().name(), e); + } + } + if (po.closed()) { + // a closed obligation is a certificate; it needs no further attention and is + // deliberately not registered in the environment, so a batch that proves many + // obligations does not flood the environment (and a user interface) with + // closed side proofs. The main proof's status still tracks it through the + // lemma. Only obligations that remain open are surfaced for manual work. + proven.add(lemma); + } else { + remaining.add(lemma); + lemma.registerInEnvironment(); + } + + if (saveDir != null) { + final Path file = saveDir.resolve( + MiscTools.toValidFileName(lemma.taclet().name().toString()) + ".proof"); + final String error = new ProofSaver(po, file).save(); + if (error != null) { + throw new IllegalStateException( + "saving lemma proof failed: " + error); + } + saved++; + } + } + done++; + if (listener != null && !listener.progressed(done, total)) { + break; + } + } + return new Result(proven, remaining, saved); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaTacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaTacletGenerator.java new file mode 100644 index 00000000000..5e7bf56de57 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/LemmaTacletGenerator.java @@ -0,0 +1,104 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.RewriteTaclet; + +import org.key_project.logic.Name; +import org.key_project.prover.sequent.PosInOccurrence; + +import org.jspecify.annotations.NullMarked; + +/** + * A generator that computes a specialized taclet capturing the effect of a programmatic + * transformation at a given position. Instead of performing the transformation directly on the + * proof (as {@link org.key_project.logic.op.TermTransformer term transformers} or many built-in + * rules do), the transformation is packaged as a taclet so that + *

    + *
  • the performed step is inspectable as a declarative artifact,
    • + *
  • its correctness can be established by a separate soundness proof registered in the same + * proof environment, and
    • + *
  • the taclet can be reused when the same transformation is required again.
    • + *
+ * + * Implementations must obey the following contract: + *
    + *
  • Context-freeness: the generated taclet must be sound in the empty context, i.e., its + * validity must not depend on branch-local knowledge. Hypotheses required for soundness have to be + * made explicit as {@code \assumes} clauses of the taclet.
    • + *
  • Provability: the taclet must lie in the fragment supported by the taclet soundness + * proof obligation machinery (see + * {@link de.uka.ilkd.key.taclettranslation.lemma.DefaultLemmaGenerator}): no variable conditions, + * no metaconstructs, no modalities.
    • + *
  • Determinism: replaying the introducing rule application (same node, same sequent) + * must regenerate an identical taclet, in particular the identical name. Purely content-derived + * names are only sound if the content cannot contain proof-local symbols: formulas on different + * branches can be equal in their printed form yet contain distinct program variable or skolem + * constant instances sharing the same name. Generators for such content must additionally + * qualify the name with a replay-stable introduction-point id (see + * {@link de.uka.ilkd.key.proof.Node#getUniqueTacletId()}).
    • + *
+ */ +@NullMarked +public interface LemmaTacletGenerator { + + /** + * returns the unique name of this generator + */ + Name name(); + + /** + * checks whether this generator can compute a lemma taclet for the term at the given position + * + * @param goal the current goal + * @param pio the position of the term to be transformed + * @return true iff {@link #generate(Goal, PosInOccurrence)} will succeed at the given position + */ + boolean isApplicable(Goal goal, PosInOccurrence pio); + + /** + * A generated taclet together with the number of base calculus steps it aggregates (display + * and measurement metadata; 1 if the transformation corresponds to a single step). + */ + record GeneratedTaclet(RewriteTaclet taclet, int aggregatedSteps) { + } + + /** + * Returns the term with all term labels removed (recursively). Name and content-grouping + * computations must work on label-free terms: labels are proof metadata whose serialization + * is not canonical (e.g. the sub-origins of merged origin labels are collected in identity + * order), so label-sensitive names would differ between a proof and its replayed or + * elaborated copy. + * + * @param term the term + * @param services services for term construction + * @return the term without any labels + */ + static de.uka.ilkd.key.logic.JTerm removeTermLabels(de.uka.ilkd.key.logic.JTerm term, + de.uka.ilkd.key.java.Services services) { + final de.uka.ilkd.key.logic.JTerm[] subs = + new de.uka.ilkd.key.logic.JTerm[term.arity()]; + boolean changed = term.hasLabels(); + for (int i = 0; i < term.arity(); i++) { + subs[i] = removeTermLabels(term.sub(i), services); + changed |= subs[i] != term.sub(i); + } + if (!changed) { + return term; + } + return services.getTermFactory().createTerm(term.op(), subs, term.boundVars(), + null); + } + + /** + * computes the lemma taclet for the term at the given position. The result must be + * deterministic in the content of the term at the position (see the class-level contract). + * + * @param goal the current goal + * @param pio the position of the term to be transformed + * @return the generated taclet with its aggregation count + */ + GeneratedTaclet generate(Goal goal, PosInOccurrence pio); +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/OssLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/OssLemmaGenerator.java new file mode 100644 index 00000000000..84232758d0e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/OssLemmaGenerator.java @@ -0,0 +1,221 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.charset.StandardCharsets; +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; +import java.util.HexFormat; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; +import de.uka.ilkd.key.proof.io.OutputStreamProofSaver; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.RewriteTaclet; +import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.logic.op.Modality; +import org.key_project.prover.rules.ApplicationRestriction; +import org.key_project.prover.rules.RuleAbortException; +import org.key_project.prover.rules.RuleSet; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NullMarked; + +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; + +/** + * Lemma generator capturing an aggregated one-step-simplification as a taclet: for a top level + * formula {@code F} that the {@link OneStepSimplifier} would simplify to {@code F'} using the + * context formulas {@code phi_1, ..., phi_k}, it produces the ground taclet + * + * 
+ * ossLemma_<hash> {
+ *     \assumes (phi_a1, ... ==> phi_s1, ...)   // the used context formulas, by polarity
+ *     \find (F) \replacewith (F')
+ *     \inSequentState                            // only if the assumes clause is nonempty
+ * }
+ *
+ * + * The pure rewrite steps aggregated by the simplifier are state-independent equivalences; the + * replace-known steps are only valid where the assumed formulas hold, which is exactly what the + * {@code \assumes} clause combined with the {@code \inSequentState} restriction enforces (the + * simplifier itself stops replace-known at update and modality boundaries). Without replace-known + * steps the taclet is an unrestricted equivalence rewrite. + * + *

+ * The taclet name is derived from a canonical serialization of find, assumptions, and + * replacewith, so replaying the introducing rule application reproduces the name, and a changed + * simplifier result surfaces as a missing taclet instead of a silently different rewrite. + * + *

+ * Formulas containing modal operators are not accepted: their taclets would fall outside the + * fragment supported by the taclet soundness proof obligation machinery. Symbolic execution + * formulas remain the business of the stock one step simplifier. + */ +@NullMarked +public final class OssLemmaGenerator implements LemmaTacletGenerator { + + public static final OssLemmaGenerator INSTANCE = new OssLemmaGenerator(); + + private static final Name NAME = new Name("ossLemma"); + + private OssLemmaGenerator() { + } + + @Override + public Name name() { + return NAME; + } + + @Override + public boolean isApplicable(Goal goal, PosInOccurrence pio) { + if (!pio.isTopLevel()) { + return false; + } + final GeneratedLemmaRegistry registry = + GeneratedLemmaRegistry.getIfPresent(goal.proof()); + if (registry != null && registry.isVetoed(pio.sequentFormula())) { + return false; + } + final OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(goal.proof()); + return simplifier != null && simplifier.canSimplify(goal, pio) + && !containsModality(pio.sequentFormula().formula()); + } + + @Override + public GeneratedTaclet generate(Goal goal, PosInOccurrence pio) { + final Services services = goal.proof().getServices(); + final OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(goal.proof()); + if (simplifier == null) { + throw new IllegalStateException( + "no one step simplifier found in profile of proof " + goal.proof().name()); + } + final OneStepSimplifier.SimplificationResult result = + simplifier.computeSimplification(goal, pio, new OneStepSimplifier.Protocol()); + if (result == null) { + GeneratedLemmaRegistry.get(goal.proof()).veto(pio.sequentFormula()); + throw new RuleAbortException("one step simplification of " + + pio.sequentFormula().formula() + + " produced no result (is the one step simplifier active for this proof?)"); + } + + final JTerm find = (JTerm) pio.sequentFormula().formula(); + final JTerm simplified = (JTerm) result.simplified().formula(); + + if (RENAMING_TERM_PROPERTY.equalsModThisProperty(find, simplified)) { + // the aggregated simplification only shuffles term labels or bound variable names; + // a lemma \find(F) \replacewith(F') with F == F' modulo those is worthless and, + // under automation, a source of non-termination + GeneratedLemmaRegistry.get(goal.proof()).veto(pio.sequentFormula()); + throw new RuleAbortException( + "one step simplification changes " + find + " only up to renaming/term labels"); + } + + ImmutableList assumesAntec = ImmutableList.nil(); + ImmutableList assumesSucc = ImmutableList.nil(); + for (final PosInOccurrence context : result.usedContextFormulas()) { + if (context.isInAntec()) { + assumesAntec = assumesAntec.append(context.sequentFormula()); + } else { + assumesSucc = assumesSucc.append(context.sequentFormula()); + } + } + + final RewriteTacletBuilder tb = new RewriteTacletBuilder<>(); + // the content hash is a human-recognizable prefix only; uniqueness comes from the + // introduction node's tree-structural id. Formulas on sibling branches can be equal in + // their printed form yet contain distinct proof-local symbol instances (program + // variables, skolem constants) sharing the same name, so a purely content-derived name + // would alias semantically different lemmas across branches. The node id is + // replay-stable (path and introduced-rule count), so replaying the introduction + // regenerates the same name. + tb.setName(MiscTools.toValidTacletName( + contentHashName(services, find, assumesAntec, assumesSucc, simplified) + "_" + + goal.node().getUniqueTacletId())); + tb.setDisplayName(NAME.toString()); + tb.setFind(find); + tb.addGoalTerm(simplified); + final RuleSet generatedLemmaRS = + services.getNamespaces().ruleSets().lookup(new Name("generatedLemma")); + tb.addRuleSet(generatedLemmaRS != null ? generatedLemmaRS + : new RuleSet(new Name("generatedLemma"))); + if (!assumesAntec.isEmpty() || !assumesSucc.isEmpty()) { + tb.setAssumesSequent(JavaDLSequentKit.createSequent(assumesAntec, assumesSucc)); + tb.setApplicationRestriction( + new ApplicationRestriction(ApplicationRestriction.IN_SEQUENT_STATE)); + } + try { + return new GeneratedTaclet(tb.getTaclet(), result.numAppliedRules()); + } catch (RuleAbortException e) { + throw e; + } catch (RuntimeException e) { + // taclet construction can be rejected for reasons rooted in taclet wellformedness + // checks; a failure must never abort automated proof search, so the formula is + // vetoed (no further introduction attempts) and the application aborted cleanly + GeneratedLemmaRegistry.get(goal.proof()).veto(pio.sequentFormula()); + throw new RuleAbortException( + "generating a lemma taclet for " + find + " failed: " + e.getMessage()); + } + } + + /** + * returns true iff the term contains a modal operator anywhere; such formulas fall outside + * the fragment supported by the taclet soundness proof obligation machinery and are + * therefore not lemma-eligible + */ + public static boolean containsModality(Term term) { + if (term.op() instanceof Modality) { + return true; + } + for (final Term sub : term.subs()) { + if (containsModality(sub)) { + return true; + } + } + return false; + } + + /** + * Derives the taclet name from a canonical serialization of the taclet content. The printed + * form is used instead of hash codes of the terms, since the latter are not guaranteed to be + * stable across JVM runs, and replay resolves the taclet by name. + */ + private static String contentHashName(Services services, JTerm find, + ImmutableList assumesAntec, ImmutableList assumesSucc, + JTerm replacewith) { + // hashed label-free: label serialization is not canonical (see + // LemmaTacletGenerator.removeTermLabels), and names must be reproducible on replay + final StringBuilder content = new StringBuilder(); + content.append("find:").append(OutputStreamProofSaver + .printTerm(LemmaTacletGenerator.removeTermLabels(find, services), services)); + for (final SequentFormula sf : assumesAntec) { + content.append("\nassumeA:").append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels((JTerm) sf.formula(), services), + services)); + } + for (final SequentFormula sf : assumesSucc) { + content.append("\nassumeS:").append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels((JTerm) sf.formula(), services), + services)); + } + content.append("\nreplacewith:").append(OutputStreamProofSaver.printTerm( + LemmaTacletGenerator.removeTermLabels(replacewith, services), services)); + + try { + final MessageDigest digest = MessageDigest.getInstance("SHA-256"); + final byte[] hash = digest.digest(content.toString().getBytes(StandardCharsets.UTF_8)); + return NAME + "_" + HexFormat.of().formatHex(hash, 0, 6); + } catch (NoSuchAlgorithmException e) { + throw new IllegalStateException("SHA-256 not available", e); + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/OssLemmaIntroductionRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/OssLemmaIntroductionRule.java new file mode 100644 index 00000000000..f3b85e02f44 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/OssLemmaIntroductionRule.java @@ -0,0 +1,21 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import org.jspecify.annotations.NullMarked; + +/** + * Introduction rule for {@link OssLemmaGenerator}: at a top level formula that the one step + * simplifier can simplify, it introduces the taclet capturing the aggregated simplification, + * together with its soundness proof obligation. + */ +@NullMarked +public final class OssLemmaIntroductionRule extends LemmaIntroductionRule { + + public static final OssLemmaIntroductionRule INSTANCE = new OssLemmaIntroductionRule(); + + private OssLemmaIntroductionRule() { + super(OssLemmaGenerator.INSTANCE); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/TransparentProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/TransparentProofSaver.java new file mode 100644 index 00000000000..1dc8318968b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/lemma/TransparentProofSaver.java @@ -0,0 +1,89 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Path; + +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.init.ProofOblInput; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.strategy.StrategyProperties; + +import org.jspecify.annotations.NullMarked; + +/** + * Saves a proof in its transparent form: the proof is elaborated onto a fresh proof of the same + * problem (see {@link LemmaElaboratingProofReplayer}), in which every lemma-eligible one step + * simplifier application is replaced by the introduction and application of a generated, + * separately provable taclet, and that proof is saved. + * + *

+ * The original proof is not modified. The elaborated proof lives in a copy of the original's + * initial configuration and is disposed after saving. + */ +@NullMarked +public final class TransparentProofSaver { + + /** + * Statistics of a transparent save. + * + * @param elaborated number of simplifier applications replaced by lemma introduction plus + * taclet application + * @param copiedOss number of simplifier applications copied unchanged (not lemma-eligible) + * @param lemmas number of distinct generated lemmas + */ + public record Result(int elaborated, int copiedOss, int lemmas) { + } + + private TransparentProofSaver() { + } + + /** + * Elaborates the given proof into its transparent form and saves it to the given file. + * + * @param proof the proof to save (left unmodified) + * @param file the target file + * @return statistics of the elaboration + * @throws Exception if the elaboration or saving fails + */ + public static Result save(Proof proof, Path file) throws Exception { + final InitConfig config = proof.getInitConfig().deepCopy(); + final Proof target = new Proof(proof.name().toString(), proof.root().sequent(), + proof.header(), config.createTacletIndex(), config.createBuiltInRuleIndex(), config); + try { + // proofs for generated proof obligations (e.g. contract POs) reference symbols that + // are not part of the problem header but are re-created from the proof obligation on + // loading; associate the elaborated proof with the same obligation so that saving + // emits the \proofObligation section and the saved file loads + final ProofOblInput po = + proof.getServices().getSpecificationRepository().getProofOblInput(proof); + if (po != null) { + target.getServices().getSpecificationRepository().registerProof(po, target); + } + // the lemma generator needs an active simplifier on the target proof + final StrategyProperties sp = + target.getSettings().getStrategySettings().getActiveStrategyProperties(); + if (StrategyProperties.OSS_OFF + .equals(sp.getProperty(StrategyProperties.OSS_OPTIONS_KEY))) { + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); + target.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + } + OneStepSimplifier.refreshOSS(target); + + final LemmaElaboratingProofReplayer replayer = + LemmaElaboratingProofReplayer.elaborate(proof, target); + + final String error = new ProofSaver(target, file).save(); + if (error != null) { + throw new IllegalStateException("saving transparent proof failed: " + error); + } + return new Result(replayer.getElaboratedCount(), replayer.getCopiedOssCount(), + GeneratedLemmaRegistry.get(target).getLemmas().size()); + } finally { + target.dispose(); + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index 2d0680f0089..86f20211379 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.lemma.OssLemmaIntroductionRule; import de.uka.ilkd.key.strategy.feature.*; import de.uka.ilkd.key.strategy.quantifierHeuristics.*; import de.uka.ilkd.key.strategy.termProjection.AssumptionProjection; @@ -27,6 +28,7 @@ import org.key_project.logic.Name; import org.key_project.prover.proof.ProofGoal; +import org.key_project.prover.proof.rulefilter.RuleFilter; import org.key_project.prover.proof.rulefilter.SetRuleFilter; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; @@ -80,18 +82,69 @@ public FOLStrategy(Proof proof, StrategyProperties strategyProperties) { approvalF = approvalDispatcher; } + /** + * The rule sets captured by the one step simplifier. In transparent mode these rules remain + * available to the strategy, but on formulas within the lemma fragment (no executable code) + * their applications are penalized so that the lemma path — which covers exactly those + * formulas with aggregated, separately provable steps — wins the scheduling race. The rules + * stay applicable (completeness): they still fire, as a last resort, on formulas the lemma + * path does not serve (e.g. vetoed ones). + */ + private static final Set OSS_CAPTURED_RULE_SETS = + Set.of("concrete", "concrete_java", "update_elim", "update_apply_on_update", + "update_apply", "update_join", "elimQuantifier"); + + /** + * Deliberately small: the penalty only needs to break the cost tie between the lemma path + * (introduction and lemma application at -11000) and the captured rules (concrete at + * -11000 plus depth scaling), so that aggregated lemmas win wherever they apply. It must + * NOT lift the captured rules above the enlarging/expanding rule band (around -2000): + * cost orderings such as "the empty-range rule of a bounded sum is cheaper than its + * unrolling rule" encode termination invariants of the strategy, and a large penalty + * inverts them (observed as an unbounded bounded-sum descent). + */ + private static final long TRANSPARENT_CAPTURED_PENALTY = 2000; + private Feature setUpGlobalF(RuleSetDispatchFeature d) { final Feature oneStepSimplificationF = oneStepSimplificationFeature(longConst(-11000)); - return add(d, oneStepSimplificationF); + return add(d, oneStepSimplificationF, transparentCapturedRuleSetPenalty()); } private Feature oneStepSimplificationFeature(Feature cost) { SetRuleFilter filter = new SetRuleFilter(); filter.addRuleToSet(MiscTools.findOneStepSimplifier(getProof())); + // in transparent mode, the lemma introduction rule takes the simplifier's place on + // lemma-eligible formulas and is costed identically + filter.addRuleToSet(OssLemmaIntroductionRule.INSTANCE); return ConditionalFeature.createConditional(filter, cost); } + private Feature transparentCapturedRuleSetPenalty() { + if (!transparentOss()) { + return longConst(0); + } + final RuleFilter capturedRuleSets = rule -> { + if (!(rule instanceof de.uka.ilkd.key.rule.Taclet taclet)) { + return false; + } + for (final RuleSet rs : taclet.getRuleSets()) { + if (OSS_CAPTURED_RULE_SETS.contains(rs.name().toString())) { + return true; + } + } + return false; + }; + return ConditionalFeature.createConditional(capturedRuleSets, + ifZero(applyTF(FocusFormulaProjection.INSTANCE, ff.notContainsExecutable), + longConst(TRANSPARENT_CAPTURED_PENALTY), longConst(0))); + } + + private boolean transparentOss() { + return StrategyProperties.OSS_TRANSPARENT + .equals(strategyProperties.getProperty(StrategyProperties.OSS_OPTIONS_KEY)); + } + private RuleSetDispatchFeature setupCostComputationF() { final RuleSetDispatchFeature d = new RuleSetDispatchFeature(); @@ -106,6 +159,11 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "concrete", add(longConst(-11000), ScaleFeature.createScaled(findDepthFeature, 10.0))); + // generated lemma taclets (transparent one step simplification) are scheduled exactly + // like the simplifications they aggregate + bindRuleSet(d, "generatedLemma", + add(longConst(-11000), + ScaleFeature.createScaled(findDepthFeature, 10.0))); bindRuleSet(d, "simplify", -4500); bindRuleSet(d, "simplify_enlarging", -2000); bindRuleSet(d, "simplify_ENLARGING", -1900); @@ -622,6 +680,13 @@ private boolean normalSplitting() { @Override public boolean isResponsibleFor(BuiltInRule rule) { - return rule instanceof OneStepSimplifier; + if (rule instanceof OneStepSimplifier) { + return true; + } + // in transparent mode, aggregated simplifications of lemma-eligible formulas are + // performed via generated lemma taclets: the strategy applies the introduction rule + // (the simplifier itself is never applicable then), and the introduced taclet is then + // applied through its "generatedLemma" rule set + return rule instanceof OssLemmaIntroductionRule && transparentOss(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategyFactory.java index 873eb4757b5..bc5e45af693 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategyFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategyFactory.java @@ -33,6 +33,16 @@ public class JavaCardDLStrategyFactory implements StrategyFactory { + "larger, but more transparent proof trees, since each
" + "simplification step is realized in one single rule
" + "application, with all instantiations clearly visible." + ""; + public static final String TOOL_TIP_OSS_TRANSPARENT = + "" + "One Step Simplification via generated lemma taclets:
" + + "each aggregated simplification of a formula without modal
" + + "operators is captured as a taclet that is introduced and
" + + "then applied, so the performed transformation is inspectable
" + + "and can be certified by a separate soundness proof.
" + + "Formulas containing modal operators are simplified by the
" + + "ordinary calculus rules in individual, visible steps; the
" + + "opaque OSS rule is never applied. Proofs are fully
" + + "transparent but larger and search is slower." + ""; public static final String TOOL_TIP_PROOF_SPLITTING_FREE = "" + "Split formulas (if-then-else expressions,
" + "disjunctions in the antecedent, conjunctions in
" @@ -147,7 +157,9 @@ private static OneOfStrategyPropertyDefinition getOssUsage() { new StrategyPropertyValueDefinition(StrategyProperties.OSS_ON, "Enabled", TOOL_TIP_OSS_ON), new StrategyPropertyValueDefinition(StrategyProperties.OSS_OFF, "Disabled", - TOOL_TIP_OSS_OFF)); + TOOL_TIP_OSS_OFF), + new StrategyPropertyValueDefinition(StrategyProperties.OSS_TRANSPARENT, "Transparent", + TOOL_TIP_OSS_TRANSPARENT)); } private static OneOfStrategyPropertyDefinition getProofSplitting() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java index 3ccc76b424e..781537bd777 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java @@ -71,6 +71,13 @@ public final class StrategyProperties extends Properties { public static final String OSS_OPTIONS_KEY = "OSS_OPTIONS_KEY"; public static final String OSS_ON = "OSS_ON"; public static final String OSS_OFF = "OSS_OFF"; + /** + * One step simplification in transparent mode: aggregated simplifications of formulas + * without modal operators are performed via generated, separately provable lemma taclets + * (see {@link de.uka.ilkd.key.rule.lemma.OssLemmaIntroductionRule}) instead of the opaque + * built-in rule; formulas outside that fragment are still simplified by the built-in rule. + */ + public static final String OSS_TRANSPARENT = "OSS_TRANSPARENT"; public static final String QUANTIFIERS_OPTIONS_KEY = "QUANTIFIERS_OPTIONS_KEY"; public static final String QUANTIFIERS_NONE = "QUANTIFIERS_NONE"; @@ -168,7 +175,8 @@ public final class StrategyProperties extends Properties { MPS_SKIP, MPS_NONE, DEP_OPTIONS_KEY, DEP_ON, DEP_OFF, QUERY_OPTIONS_KEY, QUERY_ON, QUERY_RESTRICTED, QUERY_OFF, QUERYAXIOM_OPTIONS_KEY, QUERYAXIOM_ON, QUERYAXIOM_OFF, NON_LIN_ARITH_OPTIONS_KEY, NON_LIN_ARITH_NONE, NON_LIN_ARITH_DEF_OPS, - NON_LIN_ARITH_COMPLETION, OSS_OPTIONS_KEY, OSS_ON, OSS_OFF, QUANTIFIERS_OPTIONS_KEY, + NON_LIN_ARITH_COMPLETION, OSS_OPTIONS_KEY, OSS_ON, OSS_OFF, OSS_TRANSPARENT, + QUANTIFIERS_OPTIONS_KEY, QUANTIFIERS_NONE, QUANTIFIERS_NON_SPLITTING, QUANTIFIERS_NON_SPLITTING_WITH_PROGS, QUANTIFIERS_INSTANTIATE, VBT_PHASE, VBT_SYM_EX, VBT_QUAN_INST, VBT_MODEL_GEN, CLASS_AXIOM_OFF, CLASS_AXIOM_DELAYED, CLASS_AXIOM_FREE, AUTO_INDUCTION_OPTIONS_KEY, diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java index f80d27928dc..1c502dcb1be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java @@ -270,6 +270,11 @@ private JTerm rebuild(Taclet taclet, JTerm term, TermServices services, qvars.add( (QuantifiableVariable) getInstantation(taclet, (VariableSV) qvar, services) .op()); + } else { + // A concrete (non-schematic) bound variable, as occurs in taclets generated from + // concrete proof formulas: keep it. Without this, a quantified subterm would be + // rebuilt with an empty bound-variable list and fail the arity check. + qvars.add(qvar); } } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key index b03574d0128..83aaf4d73c7 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key @@ -96,6 +96,9 @@ boolean_cases; alpha; concrete; + // taclets generated at proof time by lemma generators (transparent one step + // simplification); scheduled like the simplifications they aggregate + generatedLemma; try_apply_subst; type_hierarchy_def; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/OssLemmaReuseProbe.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/OssLemmaReuseProbe.java new file mode 100644 index 00000000000..91c5c77174a --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/OssLemmaReuseProbe.java @@ -0,0 +1,194 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.TreeSet; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.OutputStreamProofSaver; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Tag; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertNotNull; + +/** + * Measurement probe (not a regression test) for the lemma reuse hypothesis: the + * {@link GeneratedLemmaRegistry} acts as a result cache that the stock + * {@link OneStepSimplifier} does not have, so one-step-simplifications whose content (formula + * plus used context formulas) recurs within a proof would be computed once and replayed from the + * registry afterwards. + * + *

+ * The probe runs bounded automode with the stock simplifier on a selection of example problems, + * then keys every OSS application by the printed find formula and used context formulas — the + * same content key the lemma registry would use — and reports total vs. distinct applications, + * restricted to the lemma-eligible (modality-free) subset, together with the number of aggregated + * micro steps (protocol lengths) that a cache hit would have skipped. + * + *

+ * Run with: {@code ./gradlew :key.core:runOssReuseProbe} + */ +@Tag("performance") +public class OssLemmaReuseProbe { + + private static final String[] PROBLEMS = { + "standard_key/java_dl/arrayMax.key", + "standard_key/java_dl/arrayUpdateSimp.key", + "standard_key/arith/binomial1.key", + "standard_key/arith/computation.key", + "standard_key/arith/check_jdiv.key", + "firstTouch/05-ReverseArray/ReverseArray.key", + "heap/Map/existenceInfiniteMaps.key", + }; + + private static final int MAX_RULES = 20000; + private static final long TIMEOUT_MILLIS = 120000; + + private record Row(String problem, int nodes, boolean closed, int ossApps, int eligible, + int distinctEligible, long stepsTotal, long stepsSavable) { + } + + @Test + public void measureReusePotential() { + final Path examples = FindResources.getExampleDirectory(); + assertNotNull(examples, "example directory not found"); + + final List rows = new ArrayList<>(); + for (final String problem : PROBLEMS) { + final Path file = examples.resolve(problem); + if (!Files.exists(file)) { + System.out.println("SKIP (not found): " + problem); + continue; + } + try { + rows.add(measure(problem, file)); + } catch (Exception e) { + System.out.println("SKIP (failed): " + problem + " -- " + e); + } + } + + System.out.println(); + System.out.printf("%-45s %7s %6s %8s %9s %9s %8s %10s %10s%n", "problem", "nodes", + "closed", "ossApps", "eligible", "distinct", "hitRate", "microSteps", "savable"); + long ossApps = 0, eligible = 0, distinct = 0, steps = 0, savable = 0; + for (final Row r : rows) { + System.out.printf("%-45s %7d %6s %8d %9d %9d %7.1f%% %10d %10d%n", r.problem, r.nodes, + r.closed, r.ossApps, r.eligible, r.distinctEligible, hitRate(r), r.stepsTotal, + r.stepsSavable); + ossApps += r.ossApps; + eligible += r.eligible; + distinct += r.distinctEligible; + steps += r.stepsTotal; + savable += r.stepsSavable; + } + System.out.printf("%-45s %7s %6s %8d %9d %9d %7.1f%% %10d %10d%n", "TOTAL", "", "", + ossApps, eligible, distinct, + eligible == 0 ? 0.0 : 100.0 * (eligible - distinct) / eligible, steps, savable); + } + + private static double hitRate(Row r) { + return r.eligible == 0 ? 0.0 : 100.0 * (r.eligible - r.distinctEligible) / r.eligible; + } + + private static Row measure(String problem, Path file) throws Exception { + final KeYEnvironment env = KeYEnvironment.load(file); + try { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + OneStepSimplifier.refreshOSS(proof); + + try { + new AutomaticProver().start(proof, MAX_RULES, TIMEOUT_MILLIS); + } catch (InterruptedException e) { + // partial proofs are fine for the statistics + } + + final Map eligibleKeyCounts = new LinkedHashMap<>(); + final Map keySteps = new LinkedHashMap<>(); + int ossApps = 0; + int eligible = 0; + long stepsTotal = 0; + + final var nodes = proof.root().subtreeIterator(); + while (nodes.hasNext()) { + final Node node = nodes.next(); + if (!(node.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp app)) { + continue; + } + ossApps++; + final long protocolSize = app.getProtocol() == null ? 0 : app.getProtocol().size(); + stepsTotal += protocolSize; + + final JTerm find = (JTerm) app.posInOccurrence().sequentFormula().formula(); + if (OssLemmaGenerator.containsModality(find)) { + continue; + } + eligible++; + final String key = contentKey(proof, find, app.assumesInsts()); + eligibleKeyCounts.merge(key, 1, Integer::sum); + keySteps.merge(key, protocolSize, Long::sum); + } + + // micro steps that a result cache would have skipped: all but the first + // aggregation per distinct key + long stepsSavable = 0; + for (final Map.Entry entry : eligibleKeyCounts.entrySet()) { + final int count = entry.getValue(); + if (count > 1) { + stepsSavable += keySteps.get(entry.getKey()) / count * (count - 1); + } + } + + return new Row(problem, proof.countNodes(), proof.closed(), ossApps, eligible, + eligibleKeyCounts.size(), stepsTotal, stepsSavable); + } finally { + env.dispose(); + } + } + + /** + * The content key mirroring the lemma registry's reuse key: printed find formula plus the + * used context formulas with polarity (canonically ordered). + */ + private static String contentKey(Proof proof, JTerm find, + Iterable assumesInsts) { + final StringBuilder key = new StringBuilder(); + key.append(OutputStreamProofSaver.printTerm(find, proof.getServices())); + if (assumesInsts != null) { + final TreeSet assumed = new TreeSet<>(); + for (final PosInOccurrence context : assumesInsts) { + assumed.add((context.isInAntec() ? "A:" : "S:") + OutputStreamProofSaver + .printTerm((JTerm) context.sequentFormula().formula(), + proof.getServices())); + } + for (final String s : assumed) { + key.append('\n').append(s); + } + } + return key.toString(); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaElaboration.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaElaboration.java new file mode 100644 index 00000000000..eaceff8834f --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaElaboration.java @@ -0,0 +1,128 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * End-to-end test for {@link LemmaElaboratingProofReplayer} ("mode 2"): a proof is found with + * the fast opaque one step simplifier, then elaborated onto a fresh proof in which every + * lemma-eligible simplifier application is replaced by taclet introduction plus taclet + * application; non-eligible applications (modal operators) are copied unchanged. The elaborated + * proof closes, and all generated lemmas are certified by discharging their soundness proof + * obligations. + */ +public class TestLemmaElaboration { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + private static void activateOss(Proof proof) { + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + OneStepSimplifier.refreshOSS(proof); + } + + private static int countOssApps(Proof proof) { + int count = 0; + final var nodes = proof.root().subtreeIterator(); + while (nodes.hasNext()) { + if (nodes.next().getAppliedRuleApp() instanceof OneStepSimplifierRuleApp) { + count++; + } + } + return count; + } + + private static int countIntroApps(Proof proof) { + int count = 0; + final var nodes = proof.root().subtreeIterator(); + while (nodes.hasNext()) { + final Node node = nodes.next(); + if (node.getAppliedRuleApp() != null + && node.getAppliedRuleApp().rule() == OssLemmaIntroductionRule.INSTANCE) { + count++; + } + } + return count; + } + + @Test + public void testElaborateComputationProof() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + assertTrue(Files.exists(file), "example problem not found: " + file); + + try (KeYEnvironment env = KeYEnvironment.load(file); + KeYEnvironment targetEnv = + KeYEnvironment.load(file)) { + + // find the proof with the fast opaque simplifier + final Proof original = env.getLoadedProof(); + assertNotNull(original); + activateOss(original); + new AutomaticProver().start(original, 20000, 120000); + assertTrue(original.closed(), "automode did not close the original proof"); + final int originalOssApps = countOssApps(original); + assertTrue(originalOssApps > 0, + "test problem should exercise the one step simplifier"); + + // elaborate onto a fresh proof of the same problem + final Proof target = targetEnv.getLoadedProof(); + assertNotNull(target); + activateOss(target); + final LemmaElaboratingProofReplayer replayer = + LemmaElaboratingProofReplayer.elaborate(original, target); + + assertTrue(target.closed(), "elaborated proof did not close"); + assertTrue(replayer.getElaboratedCount() > 0, + "no simplifier application was elaborated"); + assertEquals(originalOssApps, + replayer.getElaboratedCount() + replayer.getCopiedOssCount(), + "every original simplifier application is either elaborated or copied"); + assertEquals(replayer.getCopiedOssCount(), countOssApps(target), + "only non-eligible simplifier applications remain in the elaborated proof"); + assertEquals(replayer.getElaboratedCount(), countIntroApps(target), + "each elaborated application contributes one introduction step"); + assertEquals(original.countNodes() + replayer.getElaboratedCount(), + target.countNodes(), + "each elaborated application adds exactly one node"); + + // certify: every generated lemma's soundness proof obligation closes + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(target); + System.out.printf( + "ELABORATION: ossApps=%d elaborated=%d copied=%d distinctLemmas=%d " + + "nodes %d -> %d%n", + originalOssApps, replayer.getElaboratedCount(), replayer.getCopiedOssCount(), + registry.getLemmas().size(), original.countNodes(), target.countNodes()); + assertFalse(registry.getLemmas().isEmpty()); + assertTrue(registry.getLemmas().size() <= replayer.getElaboratedCount(), + "reuse: at most one lemma per elaborated application"); + for (final GeneratedLemma lemma : registry.getLemmas()) { + final Proof po = lemma.getOrCreateSoundnessProof(); + new AutomaticProver().start(po, 10000, 60000); + assertTrue(po.closed(), + "soundness proof obligation of " + lemma.taclet().name() + + " did not close"); + } + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaIntroduction.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaIntroduction.java new file mode 100644 index 00000000000..00dfa4cd24c --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaIntroduction.java @@ -0,0 +1,154 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.proof.mgt.ProofStatus; +import de.uka.ilkd.key.proof.mgt.RuleJustification; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Name; +import org.key_project.logic.PosInTerm; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * End-to-end test for the taclet-generating transformer approach on the toy + * {@link AddLiteralsLemmaGenerator}: introduction of the generated taclet, its application, proof + * save/reload (replay), reuse of the taclet after pruning, the lazily created soundness proof + * obligation, and the proof status tracking of unproven lemmas. + */ +public class TestLemmaIntroduction { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + private static PosInOccurrence firstSuccedentSubTerm(Goal goal, int subTerm) { + final SequentFormula sf = goal.sequent().succedent().getFirst(); + return new PosInOccurrence(sf, PosInTerm.getTopLevel().down(subTerm), false); + } + + private static void applyLemma(Goal goal, NoPosTacletApp lemmaApp, PosInOccurrence pos, + Proof proof) { + final NoPosTacletApp matched = lemmaApp.matchFind(pos, proof.getServices()); + assertNotNull(matched, "generated taclet does not match its origin term"); + final TacletApp positioned = matched.setPosInOccurrence(pos, proof.getServices()); + goal.apply(positioned); + } + + @Test + public void testIntroduceApplyProveReloadAndReuse() throws Exception { + final KeYEnvironment env = KeYEnvironment + .load(TEST_CASE_DIRECTORY.resolve("lemmagen").resolve("addLiterals.key")); + try { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + + // step 1: introduce the lemma taclet at "5 + 7" (left of the equality) + final Goal root = proof.openGoals().head(); + final PosInOccurrence addPos = firstSuccedentSubTerm(root, 0); + assertTrue(AddLiteralsLemmaIntroductionRule.INSTANCE.isApplicable(root, addPos)); + root.apply(AddLiteralsLemmaIntroductionRule.INSTANCE.createApp(addPos, + proof.getServices())); + + final Name lemmaName = MiscTools.toValidTacletName("addLitLemma_5_7"); + final Goal afterIntro = proof.openGoals().head(); + final NoPosTacletApp lemmaApp = afterIntro.indexOfTaclets().lookup(lemmaName); + assertNotNull(lemmaApp, "introduced taclet not found in goal-local taclet index"); + + // the taclet is justified as a generated lemma, not as an axiom; the soundness + // proof obligation is not created during the rule application + final RuleJustification justification = + proof.getInitConfig().getJustifInfo().getJustification(lemmaApp.taclet()); + final GeneratedLemmaJustification lemmaJustification = + assertInstanceOf(GeneratedLemmaJustification.class, justification); + assertFalse(lemmaJustification.isAxiomJustification()); + assertNull(lemmaJustification.getSoundnessProof(), + "soundness proof obligation must not be created on the proof search path"); + + // step 2: apply the lemma; "5 + 7 = 12" becomes "12 = 12" + applyLemma(afterIntro, lemmaApp, firstSuccedentSubTerm(afterIntro, 0), proof); + + final Goal afterApply = proof.openGoals().head(); + final JTerm equality = + (JTerm) afterApply.sequent().succedent().getFirst().formula(); + assertEquals(equality.sub(1), equality.sub(0), + "lemma application should fold 5 + 7 to the literal 12"); + + // save and reload: replaying the introduction regenerates the taclet, the recorded + // taclet application resolves against it by name; note that no soundness proof + // exists at this point - replay does not depend on it + final Path proofFile = Files.createTempFile("addLitLemma", ".proof"); + try { + final String saveError = new ProofSaver(proof, proofFile).save(); + assertNull(saveError); + final KeYEnvironment reloadedEnv = + KeYEnvironment.load(proofFile); + try { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + assertEquals(proof.countNodes(), reloaded.countNodes(), + "reloaded proof does not replay to the same size"); + } finally { + reloadedEnv.dispose(); + } + } finally { + Files.deleteIfExists(proofFile); + } + + // prune to the root and re-introduce: the identical taclet instance is reused, + // no second justification is created + proof.pruneProof(proof.root()); + final Goal pruned = proof.openGoals().head(); + pruned.apply(AddLiteralsLemmaIntroductionRule.INSTANCE.createApp( + firstSuccedentSubTerm(pruned, 0), proof.getServices())); + final Goal afterReintro = proof.openGoals().head(); + final NoPosTacletApp reintroduced = afterReintro.indexOfTaclets().lookup(lemmaName); + assertNotNull(reintroduced); + final GeneratedLemma lemma = GeneratedLemmaRegistry.get(proof).lookup(lemmaName); + assertNotNull(lemma); + assertSame(lemma.taclet(), reintroduced.taclet(), + "re-introduction after pruning must reuse the cached taclet instance"); + assertEquals(1, GeneratedLemmaRegistry.get(proof).getLemmas().size()); + + // close the main proof using the lemma + applyLemma(afterReintro, reintroduced, firstSuccedentSubTerm(afterReintro, 0), + proof); + new AutomaticProver().start(proof, 1000, 30000); + assertTrue(proof.closed()); + + // the proof relies on the yet unproven lemma: closed, but lemmas left + proof.mgt().updateProofStatus(); + assertEquals(ProofStatus.CLOSED_BUT_LEMMAS_LEFT, proof.mgt().getStatus(), + "proof status must report the unproven generated lemma"); + + // create and discharge the soundness proof obligation + final Proof soundnessProof = lemma.getOrCreateSoundnessProof(); + assertSame(soundnessProof, lemma.getSoundnessProofIfPresent()); + new AutomaticProver().start(soundnessProof, 1000, 30000); + assertTrue(soundnessProof.closed(), "soundness proof obligation did not close"); + + // now the proof is closed without remaining lemmas + proof.mgt().updateProofStatus(); + assertEquals(ProofStatus.CLOSED, proof.mgt().getStatus()); + } finally { + env.dispose(); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaProverAndGrouping.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaProverAndGrouping.java new file mode 100644 index 00000000000..da060e217ff --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaProverAndGrouping.java @@ -0,0 +1,206 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.List; +import java.util.Map; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.logic.Name; +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * Tests the batch proving and content grouping that back the redesigned lemma dependency view: + * generated lemmas are grouped by generator and by content, and their soundness obligations are + * discharged in a bounded batch, with those that do not close reported for manual completion. + */ +public class TestLemmaProverAndGrouping { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + private static Proof transparentClosedSumAndMax( + KeYEnvironment env) throws Exception { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_TRANSPARENT); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + proof.setActiveStrategy( + proof.getServices().getProfile().getDefaultStrategyFactory().create(proof, sp)); + OneStepSimplifier.refreshOSS(proof); + new AutomaticProver().start(proof, 20000, 300000); + assertTrue(proof.closed()); + return proof; + } + + private static Proof transparentClosed(KeYEnvironment env, + int maxSteps) throws Exception { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_TRANSPARENT); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + proof.setActiveStrategy( + proof.getServices().getProfile().getDefaultStrategyFactory().create(proof, sp)); + OneStepSimplifier.refreshOSS(proof); + new AutomaticProver().start(proof, maxSteps, 300000); + assertTrue(proof.closed()); + return proof; + } + + @Test + public void testQuantifierLemmaObligationsGenerateAndClose() throws Exception { + // Regression for the DefaultLemmaGenerator bug: taclets whose find/replacewith contain + // concrete (non-schematic) quantifiers were rebuilt with an empty bound-variable list and + // failed the term arity check during proof-obligation generation. SumAndMax generates + // such lemmas. Their obligations must now both generate and close in the base calculus. + final Path file = TEST_CASE_DIRECTORY.resolve( + "../../../../../key.ui/examples/heap/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key"); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = transparentClosedSumAndMax(env); + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + + int quantifierLemmas = 0; + for (final GeneratedLemma lemma : registry.getLemmas()) { + if (!containsQuantifier((de.uka.ilkd.key.logic.JTerm) lemma.taclet().find())) { + continue; + } + quantifierLemmas++; + // generation must not throw (the bug), and the obligation must close + final Proof po = lemma.getOrCreateSoundnessProof(); + new AutomaticProver().start(po, 12000, 120000); + assertTrue(po.closed(), + "quantifier lemma obligation did not close: " + lemma.taclet().name()); + if (quantifierLemmas >= 3) { + break; // a few are enough for a regression guard + } + } + assertTrue(quantifierLemmas > 0, + "SumAndMax should generate lemmas containing quantifiers"); + } + } + + private static boolean containsQuantifier(de.uka.ilkd.key.logic.JTerm t) { + if (t.op() instanceof de.uka.ilkd.key.logic.op.Quantifier) { + return true; + } + for (int i = 0; i < t.arity(); i++) { + if (containsQuantifier(t.sub(i))) { + return true; + } + } + return false; + } + + @Test + public void testContentGroupingCollapsesDuplicates() throws Exception { + // SumAndMax generates many introduction-point-distinct lemmas that denote the same + // simplifications: content grouping must collapse them. + final Path file = TEST_CASE_DIRECTORY.resolve( + "../../../../../key.ui/examples/heap/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key"); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = transparentClosedSumAndMax(env); + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + + final Map> byGenerator = registry.getLemmasByGenerator(); + assertEquals(1, byGenerator.size(), "all lemmas come from the OSS generator"); + final List ossLemmas = + byGenerator.get(OssLemmaGenerator.INSTANCE.name()); + assertNotNull(ossLemmas); + assertEquals(registry.getLemmas().size(), ossLemmas.size()); + + final Map> byContent = + GeneratedLemmaRegistry.groupByContent(ossLemmas); + assertTrue(byContent.size() < ossLemmas.size(), + "content grouping should collapse duplicate simplifications (" + ossLemmas.size() + + " lemmas, " + byContent.size() + " distinct)"); + assertEquals(ossLemmas.size(), + byContent.values().stream().mapToInt(List::size).sum()); + } + } + + @Test + public void testBatchProvingUpdatesStatusWithoutFloodingEnvironment() throws Exception { + // Regression for the reported GUI issue: after batch-proving all lemmas, the depending + // proof must become CLOSED (not "closed but lemmas left") automatically, and the closed + // obligations must not be registered in the environment (no flooding of the task tree). + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = transparentClosed(env, 20000); + assertEquals(de.uka.ilkd.key.proof.mgt.ProofStatus.CLOSED_BUT_LEMMAS_LEFT, + proof.mgt().getStatus(), + "before proving the lemmas the proof is closed only modulo them"); + final int proofsBefore = proof.getEnv().getProofs().size(); + + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + final LemmaProver.Result result = + LemmaProver.proveAll(registry.getLemmas(), 10000, null); + assertTrue(result.remaining().isEmpty(), "all arith lemmas should close"); + + // status became CLOSED automatically (no explicit updateProofStatus call here) + assertEquals(de.uka.ilkd.key.proof.mgt.ProofStatus.CLOSED, proof.mgt().getStatus(), + "proving all lemmas must turn the proof status to CLOSED"); + // no closed obligation was registered in the environment + assertEquals(proofsBefore, proof.getEnv().getProofs().size(), + "closed obligations must not be registered in the environment"); + } + } + + @Test + public void testBatchProvingDischargesAndSaves() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = transparentClosed(env, 20000); + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + final List lemmas = + registry.getMissingLemmas(); + assertFalse(lemmas.isEmpty()); + + final Path saveDir = + Files.createDirectories(Path.of("build", "tmp", "lemmaProverTest")); + final LemmaProver.Result result = LemmaProver.proveAll(lemmas, 10000, saveDir); + + assertEquals(lemmas.size(), result.proven().size() + result.remaining().size()); + assertFalse(result.proven().isEmpty(), "arith lemmas should close"); + for (final GeneratedLemma lemma : result.proven()) { + assertTrue(lemma.isProven()); + // a closed obligation is a certificate and is deliberately NOT registered in the + // environment (no flooding of the task tree with closed side proofs) + assertFalse(proof.getEnv().getProofs().stream() + .anyMatch(pl -> pl.getFirstProof() == lemma.getSoundnessProofIfPresent()), + "a closed obligation must not be registered in the environment"); + } + assertTrue(registry.getMissingLemmas().size() <= result.remaining().size(), + "proven lemmas leave the missing set"); + assertEquals(lemmas.size(), result.saved(), "each obligation proof was saved"); + for (final GeneratedLemma lemma : lemmas) { + final Path expected = saveDir.resolve( + de.uka.ilkd.key.util.MiscTools.toValidFileName( + lemma.taclet().name().toString()) + ".proof"); + assertTrue(Files.exists(expected), "missing saved proof: " + expected); + Files.deleteIfExists(expected); + } + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaSoundnessNonCircular.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaSoundnessNonCircular.java new file mode 100644 index 00000000000..5f3e8640af2 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestLemmaSoundnessNonCircular.java @@ -0,0 +1,90 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * Guards the soundness of generated lemmas against circular justification: even when the main + * proof runs the one step simplifier in transparent mode, a lemma's soundness proof obligation + * must be discharged in the base calculus (opaque simplifier), never by generating and applying + * further lemmas — which would re-derive the very simplification the obligation is meant to + * justify, and never terminate. + */ +public class TestLemmaSoundnessNonCircular { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + public void testSoundnessProofUsesBaseCalculus() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, + StrategyProperties.OSS_TRANSPARENT); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + proof.setActiveStrategy(proof.getServices().getProfile() + .getDefaultStrategyFactory().create(proof, sp)); + OneStepSimplifier.refreshOSS(proof); + new AutomaticProver().start(proof, 20000, 120000); + assertTrue(proof.closed()); + + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + assertFalse(registry.getMissingLemmas().isEmpty()); + + for (final GeneratedLemma lemma : registry.getMissingLemmas()) { + final Proof po = lemma.getOrCreateSoundnessProof(); + + // the soundness proof runs in the base calculus with the one step simplifier + // switched off entirely (not even its opaque mode, which would close the + // obligation by the very aggregated simplification under scrutiny) + assertEquals(StrategyProperties.OSS_OFF, + po.getSettings().getStrategySettings().getActiveStrategyProperties() + .getProperty(StrategyProperties.OSS_OPTIONS_KEY), + "the soundness proof of " + lemma.taclet().name() + + " must run with the one step simplifier disabled"); + + new AutomaticProver().start(po, 10000, 60000); + assertTrue(po.closed(), + "soundness proof of " + lemma.taclet().name() + " did not close"); + + // it must not contain any lemma introduction or application (no circularity) + final var nodes = po.root().subtreeIterator(); + while (nodes.hasNext()) { + final Node node = nodes.next(); + final var app = node.getAppliedRuleApp(); + if (app == null) { + continue; + } + final String ruleName = app.rule().name().toString(); + assertFalse(ruleName.startsWith("introduce_ossLemma"), + "soundness proof of " + lemma.taclet().name() + + " introduces a lemma (circular)"); + assertFalse(ruleName.startsWith("ossLemma_"), + "soundness proof of " + lemma.taclet().name() + + " applies a generated lemma (circular): " + ruleName); + } + } + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestMissingLemmas.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestMissingLemmas.java new file mode 100644 index 00000000000..e1ba6da9ed4 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestMissingLemmas.java @@ -0,0 +1,108 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Path; +import java.util.List; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * Tests the "missing lemmas" bookkeeping that backs the Missing Lemmas tab of the proof + * management dialog: after a proof is elaborated (or found in transparent mode) it depends on + * generated lemmas whose soundness proof obligations are initially missing; creating and + * discharging those obligations removes them from the missing set and registers them in the + * proof environment. + */ +public class TestMissingLemmas { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + public void testMissingLemmasLifecycle() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + + try (KeYEnvironment env = KeYEnvironment.load(file); + KeYEnvironment targetEnv = + KeYEnvironment.load(file)) { + + final Proof original = env.getLoadedProof(); + assertNotNull(original); + final StrategyProperties sp = + original.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); + original.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + OneStepSimplifier.refreshOSS(original); + new AutomaticProver().start(original, 20000, 120000); + assertTrue(original.closed()); + + final Proof target = targetEnv.getLoadedProof(); + assertNotNull(target); + OneStepSimplifier.refreshOSS(target); + final LemmaElaboratingProofReplayer replayer = + LemmaElaboratingProofReplayer.elaborate(original, target); + assertTrue(target.closed()); + assertTrue(replayer.getElaboratedCount() > 0); + + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(target); + + // initially every generated lemma is missing (no soundness proof created yet) + final List missing = registry.getMissingLemmas(); + assertEquals(registry.getLemmas().size(), missing.size(), + "all generated lemmas are initially missing"); + assertFalse(missing.isEmpty()); + + // creating the obligation alone does not register it (a batch of closed obligations + // must not flood the environment) + final GeneratedLemma first = missing.get(0); + assertFalse(first.isSoundnessProofPresent()); + first.getOrCreateSoundnessProofAggregate(); + assertTrue(first.isSoundnessProofPresent()); + assertFalse(target.getEnv().getProofs().stream() + .anyMatch(pl -> pl.getFirstProof() == first.getSoundnessProofIfPresent()), + "creating the obligation must not register it in the environment"); + + // "load as side proof": registering surfaces it in the environment + final ProofAggregate aggregate = first.registerInEnvironment(); + final Proof soundnessProof = aggregate.getFirstProof(); + assertSame(target.getEnv(), soundnessProof.getEnv(), + "registered soundness proof lives in the main proof's environment"); + assertTrue(target.getEnv().getProofs().stream() + .anyMatch(pl -> pl.getFirstProof() == soundnessProof), + "registered soundness proof must be in the proof environment"); + // registering again does not duplicate it + first.registerInEnvironment(); + assertEquals(1, target.getEnv().getProofs().stream() + .filter(pl -> pl.getFirstProof() == soundnessProof).count()); + + // an open (not yet closed) soundness proof still counts as missing + assertTrue(registry.getMissingLemmas().contains(first), + "an unclosed soundness proof leaves the lemma in the missing set"); + + // discharge it: the lemma leaves the missing set + new AutomaticProver().start(soundnessProof, 10000, 60000); + assertTrue(soundnessProof.closed()); + assertTrue(first.isProven()); + assertFalse(registry.getMissingLemmas().contains(first), + "a proven lemma is no longer missing"); + assertEquals(missing.size() - 1, registry.getMissingLemmas().size()); + + // requesting the aggregate again returns the same proof (no duplicate side proof) + assertSame(soundnessProof, first.getOrCreateSoundnessProofAggregate().getFirstProof()); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestOssLemmaIntroduction.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestOssLemmaIntroduction.java new file mode 100644 index 00000000000..7f05c3815c2 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestOssLemmaIntroduction.java @@ -0,0 +1,214 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.logic.Name; +import org.key_project.logic.PosInTerm; +import org.key_project.prover.rules.ApplicationRestriction; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * End-to-end tests for {@link OssLemmaGenerator}: aggregated one-step-simplifications are + * captured as generated taclets, their soundness proof obligations are created and discharged, + * and the proofs replay after save/reload. Covered are a context-free simplification of an + * update-laden formula (pure equivalence rewrite, proof obligation containing updates) and a + * replace-known simplification (taclet with {@code \assumes} clause and in-sequent-state + * restriction, applied with assumption instantiation). + */ +public class TestOssLemmaIntroduction { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + /** + * Applies the taclet of the given app at the given position, instantiating its assumptions + * from the goal's sequent if necessary, and returns the resulting open goal. + */ + private static Goal applyTaclet(Goal goal, NoPosTacletApp app, PosInOccurrence pos) { + final Proof proof = goal.proof(); + final NoPosTacletApp matched = app.matchFind(pos, proof.getServices()); + assertNotNull(matched, "taclet " + app.taclet().name() + " does not match at " + pos); + TacletApp positioned = matched.setPosInOccurrence(pos, proof.getServices()); + if (!positioned.complete()) { + final var instantiated = positioned + .findIfFormulaInstantiations(goal.sequent(), proof.getServices()); + assertFalse(instantiated.isEmpty(), + "no assumption instantiation found for " + app.taclet().name()); + positioned = instantiated.head(); + } + goal.apply(positioned); + return proof.openGoals().head(); + } + + @Test + public void testOssLemmaWithAssumptions() throws Exception { + final KeYEnvironment env = KeYEnvironment + .load(TEST_CASE_DIRECTORY.resolve("lemmagen").resolve("ossLemmaAssumes.key")); + try { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + OneStepSimplifier.refreshOSS(proof); + + // p -> ((q & true) & p) ==> after impRight ==> p ==> (q & true) & p + final Goal root = proof.openGoals().head(); + final NoPosTacletApp impRight = + root.indexOfTaclets().lookup(new Name("impRight")); + assertNotNull(impRight); + final Goal afterImp = applyTaclet(root, impRight, new PosInOccurrence( + root.sequent().succedent().getFirst(), PosInTerm.getTopLevel(), false)); + + // introduce the lemma at (q & true) & p; the simplification uses the context + // formula p (replace-known), so the taclet carries an assumes clause and the + // in-sequent-state restriction + final PosInOccurrence target = new PosInOccurrence( + afterImp.sequent().succedent().getFirst(), PosInTerm.getTopLevel(), false); + assertTrue(OssLemmaIntroductionRule.INSTANCE.isApplicable(afterImp, target)); + afterImp.apply( + OssLemmaIntroductionRule.INSTANCE.createApp(target, proof.getServices())); + + final GeneratedLemma lemma = + GeneratedLemmaRegistry.get(proof).getLemmas().iterator().next(); + assertFalse(lemma.taclet().assumesSequent().isEmpty(), + "replace-known was used, so the taclet must record its assumptions"); + assertEquals(1, lemma.taclet().assumesSequent().antecedent().size(), + "exactly the context formula p is assumed (in the antecedent)"); + assertTrue(lemma.taclet().applicationRestriction() + .matches(ApplicationRestriction.IN_SEQUENT_STATE), + "assumption-carrying lemmas must be restricted to the sequent state"); + + // apply the lemma (with assumption instantiation): the formula becomes q + final Goal afterIntro = proof.openGoals().head(); + final NoPosTacletApp lemmaApp = + afterIntro.indexOfTaclets().lookup(lemma.taclet().name()); + assertNotNull(lemmaApp); + final Goal afterApply = applyTaclet(afterIntro, lemmaApp, new PosInOccurrence( + afterIntro.sequent().succedent().getFirst(), PosInTerm.getTopLevel(), false)); + assertEquals("q", + afterApply.sequent().succedent().getFirst().formula().toString(), + "simplification under the assumption p should yield q"); + + // the soundness proof obligation p -> (((q & true) & p) <-> q) closes + final Proof soundnessProof = lemma.getOrCreateSoundnessProof(); + new AutomaticProver().start(soundnessProof, 1000, 30000); + assertTrue(soundnessProof.closed(), "soundness proof obligation did not close"); + + // save and reload: both the introduction and the assumption-instantiated + // taclet application replay + final Path proofFile = Files.createTempFile("ossLemmaAssumes", ".proof"); + try { + final String saveError = new ProofSaver(proof, proofFile).save(); + assertNull(saveError); + final KeYEnvironment reloadedEnv = + KeYEnvironment.load(proofFile); + try { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + assertEquals(proof.countNodes(), reloaded.countNodes(), + "reloaded proof does not replay to the same size"); + } finally { + reloadedEnv.dispose(); + } + } finally { + Files.deleteIfExists(proofFile); + } + } finally { + env.dispose(); + } + } + + @Test + public void testOssLemmaOnUpdateFormula() throws Exception { + final KeYEnvironment env = KeYEnvironment + .load(TEST_CASE_DIRECTORY.resolve("lemmagen").resolve("ossLemma.key")); + try { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + OneStepSimplifier.refreshOSS(proof); + + // introduce the lemma at the top level succedent formula {i := 1}(i = 1) + final Goal root = proof.openGoals().head(); + final SequentFormula sf = root.sequent().succedent().getFirst(); + final PosInOccurrence topLevel = + new PosInOccurrence(sf, PosInTerm.getTopLevel(), false); + assertTrue(OssLemmaIntroductionRule.INSTANCE.isApplicable(root, topLevel), + "introduction rule not applicable - is the one step simplifier active?"); + root.apply( + OssLemmaIntroductionRule.INSTANCE.createApp(topLevel, proof.getServices())); + + // exactly one lemma has been generated; it is a context-free equivalence rewrite + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + assertEquals(1, registry.getLemmas().size()); + final GeneratedLemma lemma = registry.getLemmas().iterator().next(); + assertTrue(lemma.taclet().name().toString().startsWith("ossLemma_"), + "content-hash name expected, got: " + lemma.taclet().name()); + assertTrue(lemma.taclet().assumesSequent().isEmpty(), + "no replace-known steps involved, so the taclet must not have assumptions"); + assertNull(lemma.getSoundnessProofIfPresent()); + + // apply the lemma: the formula becomes true + final Goal afterIntro = proof.openGoals().head(); + final NoPosTacletApp lemmaApp = + afterIntro.indexOfTaclets().lookup(lemma.taclet().name()); + assertNotNull(lemmaApp, "introduced taclet not found in goal-local taclet index"); + final PosInOccurrence applyPos = new PosInOccurrence( + afterIntro.sequent().succedent().getFirst(), PosInTerm.getTopLevel(), false); + final NoPosTacletApp matched = lemmaApp.matchFind(applyPos, proof.getServices()); + assertNotNull(matched, "generated taclet does not match its origin formula"); + final TacletApp positioned = + matched.setPosInOccurrence(applyPos, proof.getServices()); + afterIntro.apply(positioned); + + final Goal afterApply = proof.openGoals().head(); + assertTrue( + afterApply.sequent().succedent().getFirst().formula().op() == proof.getServices() + .getTermBuilder().tt().op(), + "one step simplification of {i := 1}(i = 1) should yield true"); + + // the soundness proof obligation (with updates) is created and closes + final Proof soundnessProof = lemma.getOrCreateSoundnessProof(); + new AutomaticProver().start(soundnessProof, 1000, 30000); + assertTrue(soundnessProof.closed(), "soundness proof obligation did not close"); + + // save and reload: replaying the introduction re-runs the simplifier and + // regenerates the taclet under the same content-derived name + final Path proofFile = Files.createTempFile("ossLemma", ".proof"); + try { + final String saveError = new ProofSaver(proof, proofFile).save(); + assertNull(saveError); + final KeYEnvironment reloadedEnv = + KeYEnvironment.load(proofFile); + try { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + assertEquals(proof.countNodes(), reloaded.countNodes(), + "reloaded proof does not replay to the same size"); + } finally { + reloadedEnv.dispose(); + } + } finally { + Files.deleteIfExists(proofFile); + } + } finally { + env.dispose(); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentMode.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentMode.java new file mode 100644 index 00000000000..4a29b378942 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentMode.java @@ -0,0 +1,138 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * Tests for the {@code OSS_TRANSPARENT} strategy option ("mode 1"): automated proof search + * performs aggregated simplifications of lemma-eligible formulas via generated lemma taclets + * (introduction plus taclet application) instead of the opaque one step simplifier, which + * remains responsible for formulas containing modal operators. The resulting proof saves and + * replays. + */ +public class TestTransparentMode { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + private static void setOssMode(Proof proof, String mode) { + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, mode); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + // the active strategy caches its own property clone, so it must be renewed as well + proof.setActiveStrategy(proof.getServices().getProfile() + .getDefaultStrategyFactory().create(proof, sp)); + OneStepSimplifier.refreshOSS(proof); + } + + private record Counts(int oss, int intro, int lemmaApps) { + } + + private static Counts count(Proof proof) { + int oss = 0; + int intro = 0; + int lemmaApps = 0; + final var nodes = proof.root().subtreeIterator(); + while (nodes.hasNext()) { + final Node node = nodes.next(); + if (node.getAppliedRuleApp() == null) { + continue; + } + if (node.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp) { + oss++; + } else if (node.getAppliedRuleApp().rule() == OssLemmaIntroductionRule.INSTANCE) { + intro++; + } else if (node.getAppliedRuleApp().rule().name().toString() + .startsWith("ossLemma_")) { + lemmaApps++; + } + } + return new Counts(oss, intro, lemmaApps); + } + + @Test + public void testTransparentAutomode() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + assertTrue(Files.exists(file)); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + setOssMode(proof, StrategyProperties.OSS_TRANSPARENT); + + new AutomaticProver().start(proof, 20000, 120000); + assertTrue(proof.closed(), "automode in transparent mode did not close the proof"); + + final Counts counts = count(proof); + assertTrue(counts.intro() > 0, + "transparent mode should introduce lemma taclets during search"); + // most introductions lead to an application; a few lemmas may be obsoleted by an + // individual rule step rewriting the formula between introduction and application + // (the individual rules compete with the lemma path since they remain available) + assertTrue(counts.lemmaApps() > 0); + assertTrue(counts.lemmaApps() <= counts.intro()); + assertTrue(counts.intro() - counts.lemmaApps() <= counts.intro() / 2, + "too many introduced lemmas were never applied (intro=" + counts.intro() + + ", applied=" + counts.lemmaApps() + ")"); + // the opaque rule is never applied in transparent mode: formulas outside the lemma + // fragment are simplified by the ordinary strategy in individual, visible steps + assertEquals(0, counts.oss(), + "no opaque simplifier application may occur in transparent mode"); + + // the transparent proof saves and replays + final Path proofFile = Files.createTempFile("transparentMode", ".proof"); + try { + assertNull(new ProofSaver(proof, proofFile).save()); + try (KeYEnvironment reloadedEnv = + KeYEnvironment.load(proofFile)) { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + assertEquals(proof.countNodes(), reloaded.countNodes(), + "transparent proof does not replay to the same size"); + assertTrue(reloaded.closed()); + } + } finally { + Files.deleteIfExists(proofFile); + } + } + } + + @Test + public void testStockModeUnaffected() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + setOssMode(proof, StrategyProperties.OSS_ON); + + new AutomaticProver().start(proof, 20000, 120000); + assertTrue(proof.closed()); + + final Counts counts = count(proof); + assertTrue(counts.oss() > 0, "stock mode should still use the opaque simplifier"); + assertEquals(0, counts.intro(), + "stock mode must not introduce lemma taclets automatically"); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentModeBinarySearch.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentModeBinarySearch.java new file mode 100644 index 00000000000..d66b3afd2d4 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentModeBinarySearch.java @@ -0,0 +1,101 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * Regression test for the BinarySearch failures in transparent mode: lemmas whose find and + * assumes clauses share concrete bound variables (both stem from the same sequent) were rejected + * by the taclet builder's bound-uniqueness check — a restriction that only makes sense for + * schematic bound variables. That failure aborted automated search mid-run and made saving the + * transparent proof impossible. Now: transparent automode closes the proof, the transparent form + * saves and replays, and the lemma soundness obligations (including those with shared binders and + * assumptions) are generated and discharged. + */ +public class TestTransparentModeBinarySearch { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + public void testTransparentBinarySearchEndToEnd() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/firstTouch/06-BinarySearch/project.key"); + assertTrue(Files.exists(file)); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, + StrategyProperties.OSS_TRANSPARENT); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + proof.setActiveStrategy(proof.getServices().getProfile() + .getDefaultStrategyFactory().create(proof, sp)); + OneStepSimplifier.refreshOSS(proof); + + new AutomaticProver().start(proof, 30000, 300000); + assertTrue(proof.closed(), + "transparent automode did not close BinarySearch (previously aborted by the" + + " bound-uniqueness check)"); + + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + assertFalse(registry.getLemmas().isEmpty()); + + // the transparent form saves (previously failed with a TacletBuilderException) + // and replays to closed + final Path tmpDir = Files.createDirectories(Path.of("build", "tmp", "lemmaTests")); + final Path outFile = + Files.createTempFile(tmpDir, "binarySearchTransparent", ".proof"); + try { + // the proof is already transparent, so nothing is left to elaborate; saving is + // a faithful copy whose replay re-introduces the lemmas (this used to fail with + // the taclet builder's bound-uniqueness check) + TransparentProofSaver.save(proof, outFile); + try (KeYEnvironment reloadedEnv = + KeYEnvironment.load(outFile)) { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + assertTrue(reloaded.closed(), + "saved transparent BinarySearch proof did not replay to closed"); + int intros = 0; + final var nodes = reloaded.root().subtreeIterator(); + while (nodes.hasNext()) { + final var app = nodes.next().getAppliedRuleApp(); + if (app != null && app.rule() instanceof OssLemmaIntroductionRule) { + intros++; + } + } + assertTrue(intros > 0, + "reloaded transparent proof should contain lemma introductions"); + } + } finally { + Files.deleteIfExists(outFile); + } + + // all lemma soundness obligations generate; count how many close in the base + // calculus within the bound (the batch must be robust and must not throw) + final LemmaProver.Result result = + LemmaProver.proveAll(registry.getLemmas(), 10000, null); + assertTrue(result.remaining().isEmpty(), + "lemma obligations did not close: " + result.remaining().stream() + .map(l -> l.taclet().name().toString()).toList()); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentModeSumAndMax.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentModeSumAndMax.java new file mode 100644 index 00000000000..30a580e96e8 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentModeSumAndMax.java @@ -0,0 +1,128 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.rule.RewriteTaclet; +import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; +import static org.junit.jupiter.api.Assertions.*; + +/** + * Regression test for transparent mode on a heap/symbolic-execution scale proof (SumAndMax). + * Guards against two automation defects observed on this example: + *

    + *
  • dead re-introductions: formulas on sibling branches that are equal in their printed form + * but contain distinct proof-local symbol instances aliased to the same lemma, producing taclets + * that never match and an endless stream of introduction steps (fixed by qualifying lemma names + * with the replay-stable introduction-node id);
    • + *
  • no-op lemmas whose find and replacewith differ only in term labels or bound variable + * names (rejected by the generator).
    • + *
+ */ +public class TestTransparentModeSumAndMax { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + public void testTransparentAutomodeClosesSumAndMax() throws Exception { + final Path file = TEST_CASE_DIRECTORY.resolve( + "../../../../../key.ui/examples/heap/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key"); + assertTrue(Files.exists(file)); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, + StrategyProperties.OSS_TRANSPARENT); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + proof.setActiveStrategy(proof.getServices().getProfile() + .getDefaultStrategyFactory().create(proof, sp)); + OneStepSimplifier.refreshOSS(proof); + + new AutomaticProver().start(proof, 12000, 300000); + assertTrue(proof.closed(), "transparent automode did not close SumAndMax"); + + int intro = 0; + int lemmaApps = 0; + final var nodes = proof.root().subtreeIterator(); + while (nodes.hasNext()) { + final Node node = nodes.next(); + final var app = node.getAppliedRuleApp(); + if (app == null) { + continue; + } + if (app.rule() == OssLemmaIntroductionRule.INSTANCE) { + intro++; + } else if (app instanceof OneStepSimplifierRuleApp) { + fail("no opaque simplifier application may occur in transparent mode"); + } else if (app.rule().name().toString().startsWith("ossLemma_")) { + lemmaApps++; + final RewriteTaclet taclet = (RewriteTaclet) app.rule(); + final JTerm find = (JTerm) taclet.find(); + final JTerm replaceWith = (JTerm) ((RewriteTacletGoalTemplate) taclet + .goalTemplates().head()).replaceWith(); + assertFalse( + RENAMING_TERM_PROPERTY.equalsModThisProperty(find, replaceWith), + "no-op lemma applied: " + taclet.name()); + } + } + + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.get(proof); + assertTrue(intro > 0); + assertEquals(intro, registry.getLemmas().size(), + "every introduction must mint a fresh lemma - a mismatch means dead" + + " re-introductions of aliased lemmas"); + assertTrue(intro - lemmaApps <= intro / 4, + "most introduced lemmas should actually be applied (intro=" + intro + + ", applied=" + lemmaApps + ")"); + + // the introduction-node-qualified names must be replay-stable. The proof is saved + // inside the build tree: the problem has a boot classpath below the checkout, and + // the saver relativizes paths against the save location. + final Path tmpDir = Files.createDirectories(Path.of("build", "tmp", "lemmaTests")); + final Path proofFile = + Files.createTempFile(tmpDir, "sumAndMaxTransparent", ".proof"); + try { + assertNull(new ProofSaver(proof, proofFile).save()); + try (KeYEnvironment reloadedEnv = + KeYEnvironment.load(proofFile)) { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + if (!reloaded.closed() && reloadedEnv.getReplayResult() != null) { + // diagnostics on failure only + reloadedEnv.getReplayResult().getErrorList().stream().limit(3) + .forEach(t -> System.err.println("replay error: " + t + + (t.getCause() != null ? " caused by " + t.getCause() + : ""))); + } + assertTrue(reloaded.closed(), + "reloaded transparent SumAndMax proof did not replay to closed"); + assertEquals(proof.countNodes(), reloaded.countNodes()); + } + } finally { + Files.deleteIfExists(proofFile); + } + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentProofSaver.java b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentProofSaver.java new file mode 100644 index 00000000000..66d08603a76 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/lemma/TestTransparentProofSaver.java @@ -0,0 +1,95 @@ +/* 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 */ +package de.uka.ilkd.key.rule.lemma; + +import java.nio.file.Files; +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * Test for {@link TransparentProofSaver}: a proof found with the opaque one step simplifier is + * saved in its transparent form; the saved file loads, replays, is closed, and contains lemma + * introductions instead of the eligible opaque steps. The original proof is unchanged. + */ +public class TestTransparentProofSaver { + + private static final Path TEST_CASE_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + public void testSaveTransparentAndReload() throws Exception { + final Path file = TEST_CASE_DIRECTORY + .resolve("../../../../../key.ui/examples/standard_key/arith/computation.key"); + assertTrue(Files.exists(file)); + + try (KeYEnvironment env = KeYEnvironment.load(file)) { + final Proof proof = env.getLoadedProof(); + assertNotNull(proof); + final StrategyProperties sp = + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + sp.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + OneStepSimplifier.refreshOSS(proof); + + new AutomaticProver().start(proof, 20000, 120000); + assertTrue(proof.closed()); + final int originalNodes = proof.countNodes(); + + final Path outFile = Files.createTempFile("transparent", ".proof"); + try { + final TransparentProofSaver.Result result = + TransparentProofSaver.save(proof, outFile); + assertTrue(result.elaborated() > 0, "nothing was elaborated"); + assertTrue(result.lemmas() > 0); + + // the original proof is untouched + assertEquals(originalNodes, proof.countNodes()); + assertTrue(proof.closed()); + + // the saved transparent proof loads, replays, and is closed + try (KeYEnvironment reloadedEnv = + KeYEnvironment.load(outFile)) { + final Proof reloaded = reloadedEnv.getLoadedProof(); + assertNotNull(reloaded); + assertTrue(reloaded.closed(), "transparent proof did not replay to closed"); + assertEquals(originalNodes + result.elaborated(), reloaded.countNodes()); + + int intros = 0; + int oss = 0; + final var nodes = reloaded.root().subtreeIterator(); + while (nodes.hasNext()) { + final Node node = nodes.next(); + if (node.getAppliedRuleApp() == null) { + continue; + } + if (node.getAppliedRuleApp() + .rule() instanceof OssLemmaIntroductionRule) { + intros++; + } else if (node + .getAppliedRuleApp() instanceof OneStepSimplifierRuleApp) { + oss++; + } + } + assertEquals(result.elaborated(), intros); + assertEquals(result.copiedOss(), oss); + } + } finally { + Files.deleteIfExists(outFile); + } + } + } +} diff --git a/key.core/src/test/resources/testcase/lemmagen/addLiterals.key b/key.core/src/test/resources/testcase/lemmagen/addLiterals.key new file mode 100644 index 00000000000..d9ca26631b9 --- /dev/null +++ b/key.core/src/test/resources/testcase/lemmagen/addLiterals.key @@ -0,0 +1 @@ +\problem { 5 + 7 = 12 } diff --git a/key.core/src/test/resources/testcase/lemmagen/ossLemma.key b/key.core/src/test/resources/testcase/lemmagen/ossLemma.key new file mode 100644 index 00000000000..d06c70b7b00 --- /dev/null +++ b/key.core/src/test/resources/testcase/lemmagen/ossLemma.key @@ -0,0 +1,5 @@ +\programVariables { + int i; +} + +\problem { {i := 1} (i = 1) } diff --git a/key.core/src/test/resources/testcase/lemmagen/ossLemmaAssumes.key b/key.core/src/test/resources/testcase/lemmagen/ossLemmaAssumes.key new file mode 100644 index 00000000000..032536a8e07 --- /dev/null +++ b/key.core/src/test/resources/testcase/lemmagen/ossLemmaAssumes.key @@ -0,0 +1,6 @@ +\predicates { + p; + q; +} + +\problem { p -> ((q & true) & p) } diff --git a/key.ui/computation.key.csv b/key.ui/computation.key.csv new file mode 100644 index 00000000000..a3302d72131 --- /dev/null +++ b/key.ui/computation.key.csv @@ -0,0 +1,17 @@ +open goals;0 +Nodes;597 +Branches;3 +Interactive steps;0 +Symbolic execution steps;62 +Automode time;567ms +Avg. time per step;0.951ms +Rule applications +Quantifier instantiations;0 +One-step Simplifier apps;36 +SMT solver apps;0 +Dependency Contract apps;0 +Operation Contract apps;0 +Block/Loop Contract apps;0 +Loop invariant apps;0 +Merge Rule apps;0 +Total rule apps;705 diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java index d83cf09ba7a..1aa509881d7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java @@ -140,6 +140,17 @@ public final class Main implements Callable { description = "save all selected contracts for automatic execution") private boolean isSaveAllContracts = false; + /** + * If set, batch mode additionally saves each proof in its transparent form: eligible One + * Step Simplifier applications are elaborated into generated, separately provable lemma + * taclets (introduction plus taclet application). + */ + @Option(names = "--save-transparent", + description = "in batch mode, additionally save each proof in its transparent form " + + "(.transparent.proof): One Step Simplifier applications on formulas without " + + "modal operators are elaborated into generated, separately provable lemma taclets") + private boolean isSaveTransparent = false; + @Option(names = "--timeout", paramLabel = "INT", description = "timeout for each automatic proof of a problem in ms (default: " + LemmataAutoModeOptions.DEFAULT_TIMEOUT + ", i.e., no timeout)") @@ -350,6 +361,7 @@ public Integer call() throws Exception { } else { ui.setMacro(autoMacro); ui.setSaveOnly(isSaveAllContracts); + ConsoleUserInterfaceControl.setSaveTransparentProofs(isSaveTransparent); for (Path f : inputFiles) { ui.loadProblem(f); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/LemmaDependencyPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/LemmaDependencyPanel.java new file mode 100644 index 00000000000..2eb4080a060 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/LemmaDependencyPanel.java @@ -0,0 +1,393 @@ +/* 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 */ +package de.uka.ilkd.key.gui; + +import java.awt.BorderLayout; +import java.awt.FlowLayout; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.concurrent.atomic.AtomicBoolean; +import javax.swing.*; +import javax.swing.border.TitledBorder; +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.DefaultTreeModel; +import javax.swing.tree.TreePath; +import javax.swing.tree.TreeSelectionModel; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.lemma.GeneratedLemma; +import de.uka.ilkd.key.rule.lemma.GeneratedLemmaRegistry; +import de.uka.ilkd.key.rule.lemma.LemmaProver; + +import org.key_project.logic.Name; + +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Shows, for a single proof, the lemmas it depends on that were introduced by + * {@link de.uka.ilkd.key.rule.lemma.LemmaTacletGenerator lemma generators} (see the transparent + * mode of the One Step Simplifier). The lemmas are grouped by generator and, within a generator, + * collapsed by content, so that the many introduction-point-distinct instances of the same + * simplification appear as one row with a count. + * + *

+ * From here the user can load selected lemmas as side proofs (into the same proof environment, + * where they become visible and provable) or batch-discharge all lemmas of a generator: each + * obligation is proved with a step bound, those that do not close are kept for manual work, and + * the obligation proofs can optionally be saved. + */ +public final class LemmaDependencyPanel extends JPanel { + + private static final long serialVersionUID = 1L; + private static final Logger LOGGER = LoggerFactory.getLogger(LemmaDependencyPanel.class); + + private static final int DEFAULT_MAX_STEPS = 10000; + private static final int MAX_LABEL_LENGTH = 90; + + private final KeYMediator mediator; + private final DefaultMutableTreeNode root = new DefaultMutableTreeNode(); + private final DefaultTreeModel treeModel = new DefaultTreeModel(root); + private final JTree tree = new JTree(treeModel); + private final JButton loadButton = new JButton("Load selected as side proofs"); + private final JButton proveAllButton = new JButton("Prove all lemmas..."); + private @Nullable Proof proof; + private @Nullable Runnable onLoaded; + private @Nullable Runnable onStatusChanged; + + public LemmaDependencyPanel(KeYMediator mediator) { + super(new BorderLayout()); + this.mediator = mediator; + + tree.setRootVisible(false); + tree.setShowsRootHandles(true); + tree.getSelectionModel() + .setSelectionMode(TreeSelectionModel.DISCONTIGUOUS_TREE_SELECTION); + tree.addTreeSelectionListener(e -> updateButtons()); + + final JScrollPane scrollPane = new JScrollPane(tree); + scrollPane.setBorder(new TitledBorder("Lemmas this proof depends on")); + add(scrollPane, BorderLayout.CENTER); + + loadButton.addActionListener(e -> loadSelected()); + proveAllButton.addActionListener(e -> proveAll()); + final JPanel buttons = new JPanel(new FlowLayout(FlowLayout.RIGHT, 5, 5)); + buttons.add(proveAllButton); + buttons.add(loadButton); + add(buttons, BorderLayout.SOUTH); + + updateButtons(); + } + + /** + * Sets an action to run after lemmas have been loaded as side proofs (e.g. to close the + * enclosing dialog). + */ + public void setOnLoaded(Runnable onLoaded) { + this.onLoaded = onLoaded; + } + + /** + * Sets an action to run after the proven status of lemmas may have changed (e.g. to refresh + * the enclosing dialog's proof-status display). + */ + public void setOnStatusChanged(Runnable onStatusChanged) { + this.onStatusChanged = onStatusChanged; + } + + /** + * Shows the lemma dependencies of the given proof (clears the view for {@code null} or a + * proof without generated lemmas). + */ + public void setProof(@Nullable Proof proof) { + this.proof = proof; + refresh(); + } + + private void refresh() { + root.removeAllChildren(); + if (proof != null) { + final GeneratedLemmaRegistry registry = GeneratedLemmaRegistry.getIfPresent(proof); + if (registry != null) { + for (final Map.Entry> gen : registry + .getLemmasByGenerator().entrySet()) { + final DefaultMutableTreeNode genNode = + new DefaultMutableTreeNode(new GeneratorRow(gen.getKey(), gen.getValue())); + for (final List group : GeneratedLemmaRegistry + .groupByContent(gen.getValue()).values()) { + genNode.add(new DefaultMutableTreeNode(new ContentRow(group))); + } + root.add(genNode); + } + } + } + treeModel.reload(); + for (int i = 0; i < tree.getRowCount(); i++) { + tree.expandRow(i); + } + updateButtons(); + } + + private void updateButtons() { + final boolean hasLemmas = root.getChildCount() > 0; + proveAllButton.setEnabled(hasLemmas); + loadButton.setEnabled(!selectedLemmas().isEmpty()); + } + + /** Collects the lemmas of the selected tree nodes (generator or content rows). */ + private List selectedLemmas() { + final Set result = new LinkedHashSet<>(); + final TreePath[] paths = tree.getSelectionPaths(); + if (paths != null) { + for (final TreePath path : paths) { + final Object node = + ((DefaultMutableTreeNode) path.getLastPathComponent()).getUserObject(); + if (node instanceof GeneratorRow row) { + result.addAll(row.lemmas); + } else if (node instanceof ContentRow row) { + result.addAll(row.lemmas); + } + } + } + return new ArrayList<>(result); + } + + private List allLemmas() { + final List all = new ArrayList<>(); + for (int i = 0; i < root.getChildCount(); i++) { + final Object row = + ((DefaultMutableTreeNode) root.getChildAt(i)).getUserObject(); + if (row instanceof GeneratorRow gen) { + all.addAll(gen.lemmas); + } + } + return all; + } + + private void loadSelected() { + final List selected = selectedLemmas(); + if (selected.isEmpty()) { + return; + } + Proof first = null; + for (final GeneratedLemma lemma : selected) { + // register the obligation in the environment so the user can work on it; the user + // interface picks it up via the environment listener and adds it to the task tree + final Proof po = lemma.registerInEnvironment().getFirstProof(); + if (first == null) { + first = po; + } + } + if (first != null) { + mediator.getSelectionModel().setSelectedProof(first); + } + if (onLoaded != null) { + onLoaded.run(); + } + } + + private void proveAll() { + final List lemmas = allLemmas(); + if (lemmas.isEmpty()) { + return; + } + final ProveAllOptions options = ProveAllOptions.ask(this, lemmas.size()); + if (options == null) { + return; + } + + proveAllButton.setEnabled(false); + loadButton.setEnabled(false); + mediator.stopInterface(true); + + final ProgressDialog progressDialog = new ProgressDialog(lemmas.size()); + final AtomicBoolean cancelled = new AtomicBoolean(false); + progressDialog.onCancel(() -> cancelled.set(true)); + + final SwingWorker worker = + new SwingWorker<>() { + @Override + protected LemmaProver.Result doInBackground() throws Exception { + return LemmaProver.proveAll(lemmas, options.maxSteps(), options.saveDir(), + (done, total) -> { + publish(done); + return !cancelled.get(); + }); + } + + @Override + protected void process(List chunks) { + progressDialog.setProgress(chunks.get(chunks.size() - 1)); + } + + @Override + protected void done() { + progressDialog.dispose(); + mediator.startInterface(true); + try { + final LemmaProver.Result result = get(); + JOptionPane.showMessageDialog(LemmaDependencyPanel.this, + result.proven().size() + " of " + lemmas.size() + + " lemma(s) proved, " + result.remaining().size() + + " left open" + + (options.saveDir() != null + ? ", " + result.saved() + " proof(s) saved to " + + options.saveDir() + : "") + + ".", + "Prove Lemmas", JOptionPane.INFORMATION_MESSAGE); + } catch (Exception e) { + LOGGER.error("batch proving of lemmas failed", e); + JOptionPane.showMessageDialog(LemmaDependencyPanel.this, + "Batch proving failed:\n" + e.getMessage(), "Prove Lemmas", + JOptionPane.ERROR_MESSAGE); + } + refresh(); + // proving lemmas may have turned the depending proof from "closed but lemmas + // left" into "closed". Recompute the status explicitly (robust against the + // order in which proof-tree listeners handled the obligation-closed events) + // and let the enclosing dialog refresh its status display. + if (proof != null) { + proof.mgt().updateProofStatus(); + } + if (onStatusChanged != null) { + onStatusChanged.run(); + } + } + }; + worker.execute(); + progressDialog.setVisible(true); + } + + /** A small modeless progress dialog for the batch proving of lemmas. */ + private final class ProgressDialog extends JDialog { + private static final long serialVersionUID = 1L; + + private final JProgressBar bar; + private @Nullable Runnable cancelAction; + + ProgressDialog(int total) { + super(SwingUtilities.getWindowAncestor(LemmaDependencyPanel.this), "Proving Lemmas", + ModalityType.MODELESS); + bar = new JProgressBar(0, total); + bar.setStringPainted(true); + bar.setString("0 / " + total); + + final JButton cancel = new JButton("Cancel"); + cancel.addActionListener(e -> { + cancel.setEnabled(false); + bar.setString("cancelling after current lemma..."); + if (cancelAction != null) { + cancelAction.run(); + } + }); + + final JPanel content = new JPanel(new BorderLayout(8, 8)); + content.setBorder(BorderFactory.createEmptyBorder(12, 12, 12, 12)); + content.add(new JLabel("Discharging lemma soundness obligations..."), + BorderLayout.NORTH); + content.add(bar, BorderLayout.CENTER); + final JPanel south = new JPanel(new FlowLayout(FlowLayout.RIGHT, 0, 0)); + south.add(cancel); + content.add(south, BorderLayout.SOUTH); + setContentPane(content); + setDefaultCloseOperation(DO_NOTHING_ON_CLOSE); + pack(); + setLocationRelativeTo(getOwner()); + } + + void onCancel(Runnable action) { + this.cancelAction = action; + } + + void setProgress(int done) { + bar.setValue(done); + bar.setString(done + " / " + bar.getMaximum()); + } + } + + private static String truncate(String s) { + final String oneLine = s.replace('\n', ' '); + return oneLine.length() <= MAX_LABEL_LENGTH ? oneLine + : oneLine.substring(0, MAX_LABEL_LENGTH - 1) + "…"; + } + + private static String status(List lemmas) { + int proven = 0; + int created = 0; + for (final GeneratedLemma lemma : lemmas) { + if (lemma.isProven()) { + proven++; + } else if (lemma.isSoundnessProofPresent()) { + created++; + } + } + final StringBuilder sb = new StringBuilder(); + sb.append(proven).append('/').append(lemmas.size()).append(" proven"); + if (created > 0) { + sb.append(", ").append(created).append(" open"); + } + return sb.toString(); + } + + /** A generator grouping node. */ + private record GeneratorRow(Name generator, List lemmas) { + @Override + public String toString() { + final int distinct = GeneratedLemmaRegistry.groupByContent(lemmas).size(); + return generator + " — " + lemmas.size() + " lemma(s), " + distinct + + " distinct (" + status(lemmas) + ")"; + } + } + + /** A content-collapsed group of lemmas denoting the same simplification. */ + private record ContentRow(List lemmas) { + @Override + public String toString() { + final String label = truncate(lemmas.get(0).contentKey()); + return (lemmas.size() > 1 ? "×" + lemmas.size() + " " : "") + label + + " [" + status(lemmas) + "]"; + } + } + + /** Options gathered from the user before a batch proving run. */ + private record ProveAllOptions(int maxSteps, @Nullable Path saveDir) { + static @Nullable ProveAllOptions ask(java.awt.Component parent, int count) { + final JSpinner steps = new JSpinner( + new SpinnerNumberModel(DEFAULT_MAX_STEPS, 100, 1_000_000, 1000)); + final JCheckBox save = new JCheckBox("Save obligation proofs to a directory"); + final JPanel panel = new JPanel(new java.awt.GridLayout(0, 1, 4, 4)); + panel.add(new JLabel("Prove all " + count + + " lemma(s); lemmas not closing within the step bound stay open.")); + final JPanel stepsPanel = new JPanel(new FlowLayout(FlowLayout.LEFT, 5, 0)); + stepsPanel.add(new JLabel("Max. automatic steps per lemma:")); + stepsPanel.add(steps); + panel.add(stepsPanel); + panel.add(save); + + final int choice = JOptionPane.showConfirmDialog(parent, panel, "Prove Lemmas", + JOptionPane.OK_CANCEL_OPTION, JOptionPane.PLAIN_MESSAGE); + if (choice != JOptionPane.OK_OPTION) { + return null; + } + Path dir = null; + if (save.isSelected()) { + final JFileChooser chooser = new JFileChooser(); + chooser.setFileSelectionMode(JFileChooser.DIRECTORIES_ONLY); + chooser.setDialogTitle("Directory to save lemma proofs"); + if (chooser.showSaveDialog(parent) != JFileChooser.APPROVE_OPTION) { + return null; + } + dir = chooser.getSelectedFile().toPath(); + } + return new ProveAllOptions((Integer) steps.getValue(), dir); + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 57281711516..8d7f63e9a2d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -989,6 +989,7 @@ private JMenu createFileMenu() { fileMenu.add(editMostRecentFileAction); fileMenu.add(saveFileAction); fileMenu.add(saveBundleAction); + fileMenu.add(new SaveTransparentProofAction(this)); fileMenu.add(quickSaveAction); fileMenu.add(quickLoadAction); fileMenu.addSeparator(); @@ -1106,6 +1107,7 @@ public void menuCanceled(MenuEvent e) { proof.add(goalBack); proof.add(new PruneProofAction(this)); } + proof.add(new SaveTransparentProofAction(this, selected)); proof.add(new AbandonTaskAction(this, selected)); if (selected == null) { proof.addSeparator(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java index 747a755fbc7..b51c71d1769 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java @@ -70,6 +70,7 @@ public final class ProofManagementDialog extends JDialog { private JList proofList; private ContractSelectionPanel contractPanelByMethod; private ContractSelectionPanel contractPanelByProof; + private LemmaDependencyPanel lemmaDependencyPanel; private JButton startButton; private JButton cancelButton; private final KeYMediator mediator; @@ -142,7 +143,10 @@ public Component getListCellRendererComponent(JList list, Object value, int i return result; } }); - proofList.addListSelectionListener(e -> updateContractPanel()); + proofList.addListSelectionListener(e -> { + updateContractPanel(); + updateLemmaDependencyPanel(); + }); // create method list panel, scroll pane JPanel listPanelByMethod = new JPanel(); @@ -188,7 +192,16 @@ public void mouseClicked(MouseEvent e) { } }); contractPanelByProof.addListSelectionListener(e -> updateStartButton()); - listPanelByProof.add(contractPanelByProof); + + // the right-hand side of the "By Proof" tab shows, for the selected proof, both the + // contracts and the generated lemmas it depends on + lemmaDependencyPanel = new LemmaDependencyPanel(mediator); + lemmaDependencyPanel.setOnLoaded(() -> setVisible(false)); + lemmaDependencyPanel.setOnStatusChanged(this::updateGlobalStatus); + JTabbedPane byProofDetails = new JTabbedPane(); + byProofDetails.addTab("Contracts", contractPanelByProof); + byProofDetails.addTab("Lemmas", lemmaDependencyPanel); + listPanelByProof.add(byProofDetails); // create tabbed pane tabbedPane = new JTabbedPane(); @@ -199,6 +212,7 @@ public void mouseClicked(MouseEvent e) { if (proofList.getSelectedIndex() == -1 && proofList.getModel().getSize() > 0) { proofList.setSelectedIndex(0); } + updateLemmaDependencyPanel(); }); getContentPane().add(tabbedPane); @@ -250,6 +264,7 @@ public void dispose() { classTree = null; contractPanelByMethod = null; contractPanelByProof = null; + lemmaDependencyPanel = null; startButton = null; cancelButton = null; // ============================================ @@ -561,6 +576,18 @@ private void updateContractPanel() { updateStartButton(); } + private void updateLemmaDependencyPanel() { + if (lemmaDependencyPanel == null) { + return; + } + final ProofWrapper selected = proofList.getSelectedValue(); + Proof proof = selected != null ? selected.proof : null; + if (proof == null) { + proof = mediator.getSelectedProof(); + } + lemmaDependencyPanel.setProof(proof); + } + private void updateGlobalStatus() { // target icons diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java index 7faae53802b..741b3ea20d5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java @@ -305,11 +305,56 @@ private void checkPopup(MouseEvent e) { JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu( ContextMenuKind.PROOF_LIST, p, mediator); menu.show(e.getComponent(), e.getX(), e.getY()); + } else if (selPath != null + && selPath.getLastPathComponent() instanceof EnvNode envNode) { + delegateView.setSelectionPath(selPath); + final JPopupMenu menu = new JPopupMenu(); + final JMenuItem abandonAll = new JMenuItem("Abandon All Proofs of Environment"); + abandonAll.setToolTipText( + "Drop every proof loaded in this environment at once."); + abandonAll.addActionListener(ev -> abandonEnvironment(envNode)); + menu.add(abandonAll); + menu.show(e.getComponent(), e.getX(), e.getY()); } } } } + /** + * Abandons (disposes) all proofs of the given environment node after confirmation. Useful + * to clean up an environment that accumulated many proofs at once (e.g. lemma side proofs + * loaded in bulk) without abandoning them one by one. + * + * @param envNode the environment node whose proofs to abandon + */ + private void abandonEnvironment(EnvNode envNode) { + // collect the proofs first: disposing a proof removes its node from the tree, which + // would otherwise invalidate an in-progress traversal of the environment's children + final List proofs = new LinkedList<>(); + for (int i = 0, n = envNode.getChildCount(); i < n; i++) { + if (envNode.getChildAt(i) instanceof TaskTreeNode taskNode) { + for (final Proof p : taskNode.allProofs()) { + proofs.add(p); + } + } + } + if (proofs.isEmpty()) { + return; + } + if (!mediator.getUI().confirmTaskRemoval( + "Abandon all " + proofs.size() + " proof(s) of this environment?")) { + return; + } + if (mediator.isInAutoMode()) { + mediator.getUI().getProofControl().stopAutoMode(); + } + for (final Proof p : proofs) { + if (!p.isDisposed()) { + p.dispose(); + } + } + } + /** * a prooftree listener, so that it is known when the proof has closed diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveTransparentProofAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveTransparentProofAction.java new file mode 100644 index 00000000000..c56b6cb5225 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveTransparentProofAction.java @@ -0,0 +1,107 @@ +/* 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 */ +package de.uka.ilkd.key.gui.actions; + +import java.awt.Component; +import java.awt.event.ActionEvent; +import java.io.File; +import java.nio.file.Path; +import javax.swing.JFileChooser; +import javax.swing.JOptionPane; +import javax.swing.SwingWorker; + +import de.uka.ilkd.key.gui.KeYFileChooser; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.lemma.TransparentProofSaver; +import de.uka.ilkd.key.util.MiscTools; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Saves the selected proof in its transparent form: eligible one step simplifier applications + * are elaborated into generated, separately provable lemma taclets (introduction plus taclet + * application) before saving. The proof itself is left unchanged. + * + * @see TransparentProofSaver + */ +public final class SaveTransparentProofAction extends MainWindowAction { + + private static final long serialVersionUID = 1L; + private static final Logger LOGGER = + LoggerFactory.getLogger(SaveTransparentProofAction.class); + + /** + * The proof to save; if {@code null}, the currently selected proof is saved (used for the + * task list context menu, which acts on the proof under the mouse pointer). + */ + private final Proof proof; + + public SaveTransparentProofAction(MainWindow mainWindow) { + this(mainWindow, null); + } + + public SaveTransparentProofAction(MainWindow mainWindow, Proof proof) { + super(mainWindow); + this.proof = proof; + setName("Save Transparent Proof..."); + setTooltip("Save the proof with One Step Simplification steps elaborated into " + + "generated, separately provable lemma taclets."); + if (proof == null) { + mainWindow.getMediator().enableWhenProofLoaded(this); + } + } + + @Override + public void actionPerformed(ActionEvent e) { + final Proof toSave = + proof != null ? proof : mainWindow.getMediator().getSelectedProof(); + if (toSave == null) { + mainWindow.popupWarning("No proof.", "Oops..."); + return; + } + saveTransparent(mainWindow, toSave, mainWindow); + } + + /** + * Asks for a file name and saves the given proof in its transparent form (in the + * background, since elaboration replays the whole proof). + */ + public static void saveTransparent(MainWindow mainWindow, Proof proof, Component parent) { + final KeYFileChooser fileChooser = + KeYFileChooser.getFileChooser("Choose filename to save transparent proof"); + fileChooser.setSelectedFile(new File( + MiscTools.toValidFileName(proof.name().toString()) + ".transparent.proof")); + if (fileChooser.showSaveDialog(parent) != JFileChooser.APPROVE_OPTION) { + return; + } + final Path file = fileChooser.getSelectedFile().toPath(); + + mainWindow.setStatusLine("Elaborating proof into its transparent form ..."); + new SwingWorker() { + @Override + protected TransparentProofSaver.Result doInBackground() throws Exception { + return TransparentProofSaver.save(proof, file); + } + + @Override + protected void done() { + try { + final TransparentProofSaver.Result result = get(); + mainWindow.setStatusLine("Transparent proof saved to " + file + " (" + + result.elaborated() + " simplifier application(s) elaborated into " + + result.lemmas() + " lemma(s), " + result.copiedOss() + + " copied unchanged)"); + } catch (Exception exception) { + LOGGER.error("Saving transparent proof failed", exception); + mainWindow.setStatusLine("Saving transparent proof failed"); + JOptionPane.showMessageDialog(parent, + "Saving the transparent proof failed:\n" + exception.getMessage(), + "Save Transparent Proof", JOptionPane.ERROR_MESSAGE); + } + } + }.execute(); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java index 5bd3bc299bc..dbac1d03ff1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java @@ -309,12 +309,18 @@ private void init(MainWindow mainWindow, String stats) { JButton saveBundleButton = new JButton("Save proof bundle"); saveBundleButton .addActionListener(e -> mainWindow.getUserInterface().saveProofBundle(proof)); + JButton saveTransparentButton = new JButton("Save transparent proof"); + saveTransparentButton.setToolTipText("Save the proof with One Step Simplification " + + "steps elaborated into generated, separately provable lemma taclets."); + saveTransparentButton.addActionListener( + e -> SaveTransparentProofAction.saveTransparent(mainWindow, proof, this)); buttonPane.add(okButton); buttonPane.add(csvButton); buttonPane.add(htmlButton); buttonPane2.add(saveButton); buttonPane2.add(saveBundleButton); + buttonPane2.add(saveTransparentButton); // spotless:off /* diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java index 1046403af7d..00e4be425d4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java @@ -36,6 +36,7 @@ import de.uka.ilkd.key.proof.io.ProofSaver; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.IBuiltInRuleApp; +import de.uka.ilkd.key.rule.lemma.TransparentProofSaver; import de.uka.ilkd.key.scripts.ProofScriptEngine; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.util.ExceptionTools; @@ -429,6 +430,16 @@ public void reportWarnings(ImmutableSet warnings) { * @param keyProblemFile the key problem file * @return true, if successful */ + /** + * If set, {@link #saveProof(Object, Proof, Path)} additionally saves each proof in its + * transparent form (see {@link de.uka.ilkd.key.rule.lemma.TransparentProofSaver}). + */ + private static volatile boolean saveTransparentProofs = false; + + public static void setSaveTransparentProofs(boolean value) { + saveTransparentProofs = value; + } + public static boolean saveProof(Object result, Proof proof, Path keyProblemFile) { if (result instanceof Throwable) { throw new RuntimeException("Error in batchmode.", (Throwable) result); @@ -466,6 +477,21 @@ public static boolean saveProof(Object result, Proof proof, Path keyProblemFile) } catch (IOException e) { LOGGER.error("Failed to write proof stats", e); } + + if (saveTransparentProofs) { + final Path transparentFile = Path.of(baseName + ".transparent.proof"); + try { + final TransparentProofSaver.Result stats = + TransparentProofSaver.save(proof, transparentFile); + LOGGER.info( + "Transparent proof saved to {}: {} simplifier application(s) elaborated " + + "into {} lemma(s), {} copied unchanged", + transparentFile, stats.elaborated(), stats.lemmas(), stats.copiedOss()); + } catch (Exception e) { + LOGGER.error("Failed to save transparent proof", e); + return false; + } + } // Says true if all Proofs have succeeded, // or false if there is at least one open Proof return proof.openGoals().isEmpty(); diff --git a/lemmagen-demo.key b/lemmagen-demo.key new file mode 100644 index 00000000000..7026896ab20 --- /dev/null +++ b/lemmagen-demo.key @@ -0,0 +1,16 @@ +// Demo for the taclet-generating transformer spike (branch bubel/lemma-taclet-spike). +// +// Right-click exactly on a "5 + 7" subterm and apply "introduce_addLitLemma": +// a new node appears, the sequent is unchanged, but the goal-local taclet +// addLitLemma_5_7 { \find(5 + 7) \replacewith(12) } is now available. +// Right-click "5 + 7" again to apply it like any ordinary taclet. +// +// The same single introduction serves all three occurrences (and, after andRight, +// all branches below the introduction node). Introducing again after pruning or +// on a parallel branch reuses the identical taclet - no duplicate is created. + +\problem { + 5 + 7 = 12 + & 2 * (5 + 7) = 24 + & (5 + 7) + 1 = 13 +}