RFC / KEP-1: Taclet-generating transformers (lemmas instead of metaconstructs, built-in rules, etc.)

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
+}

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<BuiltInRule> 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!

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<Proof> 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) {

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;
+    }
 }

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() {

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<RuleKey, RuleJustification> 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;
     }
 }

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()

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 {

key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java

@@ -88,6 +88,17 @@ public static final class Protocol extends ArrayList<RuleApp> {
     private TacletIndex[] indices;
     private Map<JTerm, JTerm>[] 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<Taclet> 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<Taclet> 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<Goal> 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<PosInOccurrence> 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).
+     *
+     * <p>
+     * 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.
      *