RFC / KEP-1: Taclet-generating transformers (lemmas instead of metaconstructs, built-in rules, etc.)#3893
Draft
unp1 wants to merge 20 commits into
Draft
RFC / KEP-1: Taclet-generating transformers (lemmas instead of metaconstructs, built-in rules, etc.)#3893unp1 wants to merge 20 commits into
unp1 wants to merge 20 commits into
Conversation
unp1
added
the
RFC
Instead of performing many proof steps programmatically (term transformers, built-in rules), a LemmaTacletGenerator packages the transformation as a specialized, metaconstruct-free taclet. A LemmaIntroductionRule (built-in) introduces the generated taclet goal-locally together with a soundness proof obligation created via the existing taclet lemma machinery; rewriting with the lemma is then an ordinary, separately recorded taclet application. Design properties validated by the end-to-end test: - two-step recording (builtin introduction + taclet app) saves and replays; replaying the introduction re-runs the deterministic generator, and the recorded taclet application resolves against the regenerated taclet by its content-derived name - the taclet carries a GeneratedLemmaJustification pointing to its soundness proof (not an axiom, not justified by the introducing rule) - per-proof GeneratedLemmaRegistry guarantees one taclet instance and one proof obligation per lemma name (reuse across branches and after pruning) - the soundness proof obligation closes automatically Toy generator: AddLiteralsLemmaGenerator folds sums of integer literals, mirroring the add_literals/#add system taclet whose right-hand side is computed by Java code at application time. The system taclet stays untouched. Created with AI tooling support
…racking Two refinements to the taclet-generating transformer spike: 1. The soundness proof obligation of a generated lemma is no longer created during the introducing rule application but lazily on first request (GeneratedLemma.getOrCreateSoundnessProof). Rule application - and thus proof search - now only pays for building the taclet and inserting it into the goal-local index; PO creation and discharge become a deferrable batch concern. (A name-recorder probe showed the *AtPre newnames on the introduction node predate the rule application - they are load-time proposals flushed by the first applied rule, pre-existing KeY behavior unrelated to PO creation.) 2. ProofCorrectnessMgt now tracks generated lemmas: a closed proof that used a lemma taclet whose soundness proof is missing, disposed, or open is downgraded to CLOSED_BUT_LEMMAS_LEFT (transitively through the soundness proofs, which live in copied init configs and are inspected directly). The pass runs before the contract fixpoint so dependent contract proofs observe the downgrade. Fixed along the way: ProofPruner removes the justification of goal-locally introduced taclets on pruning; the registry now re-registers the identical justification instance when a cached lemma is re-introduced. The end-to-end test covers laziness, replay-before-PO, the pruning path, and both proof status transitions. Created with AI tooling support
Extract a public entry point computeSimplification(Goal, PosInOccurrence, Protocol) returning the aggregated simplification result (simplified formula, number of applied rules, used context formulas) without modifying goal or proof. This is the OSS core computation exactly as apply() performs it, usable by clients that want to capture the aggregated transformation in a different form (e.g., as a generated lemma taclet). No change to the rule's own behavior; requires the simplifier to be active for the proof. Created with AI tooling support
…taclets
OssLemmaGenerator packages an aggregated one-step-simplification F ~> F' as
a ground rewrite taclet: the context formulas used by replace-known steps
become an \assumes clause combined with \inSequentState (mirroring the
discipline OSS itself follows: replace-known stops at update and modality
boundaries); without replace-known the taclet is an unrestricted equivalence
rewrite. Introduced interactively via OssLemmaIntroductionRule (registered in
JavaProfile; automation-inert), reusing the LemmaIntroductionRule two-step
recording.
Taclet names are content-derived: SHA-256 over a canonical serialization of
find, assumptions (with polarity), and replacewith - term hash codes are not
guaranteed stable across JVM runs, and replay resolves taclets by name.
Including the result means a changed simplifier outcome surfaces on reload
as a missing taclet rather than a silently different rewrite.
Generator applicability excludes formulas containing modal operators (outside
the lemma PO fragment); update-laden formulas are supported - the end-to-end
test discharges the proof obligation ({i:=1}(i=1)) <-> true, confirming
UpdateApplication passes the taclet lemma translation. Second test covers the
assumes-carrying case including assumption-instantiated application and
save/reload replay of both steps.
Created with AI tooling support
Runs bounded automode with the stock one step simplifier on a selection of example problems, keys every OSS application by the registry's content key (printed find formula + used context formulas with polarity), and reports total vs. distinct applications restricted to the lemma-eligible (modality-free) subset, plus the aggregated micro steps a result cache would have skipped. Findings on the current selection: 91% of OSS applications are lemma-eligible; 35% of eligible applications are content-duplicates (check_jdiv 46%, ReverseArray 24%, arrayMax 18%); 13.5% of aggregated micro steps are savable (a lower bound - cache hits also skip the fixpoint's unsuccessful scanning, invisible post-hoc). The lemma path is performance neutral-to-positive while adding inspectability and provability. Created with AI tooling support
LemmaElaboratingProofReplayer copies a proof onto a fresh proof of the same problem, replacing every lemma-eligible one step simplifier application by the two-step lemma form (introduce_ossLemma + generated taclet application); non-eligible applications (modal operators, unlocatable positions) are copied unchanged, so elaboration never fails a proof that copies cleanly. This decouples proof search from transparency: search runs with the fast opaque rule, the finished proof is elaborated into a form where every aggregated simplification is a declarative, separately provable artifact. Position relocation uses AbstractProofReplayer.findInNewSequent (widened to protected), which compares modulo proof irrelevancy - strict term equality fails as soon as term labels diverge between original and elaborated proof. End-to-end test on standard_key/arith/computation.key: 36 OSS applications, 16 elaborated (exactly the modality-free subset), 20 copied, 16 generated lemmas all certified by discharging their soundness proof obligations, the elaborated proof closes, and each elaborated step adds exactly one node (597 -> 613). Created with AI tooling support
Three user-facing integrations of the taclet-generating transformer machinery for the One Step Simplifier. Strategy option: One Step Simplification gains a third value 'Transparent' (OSS_TRANSPARENT) besides Enabled/Disabled. In transparent mode the simplifier machinery stays active but yields lemma-eligible (modality-free) formulas to OssLemmaIntroductionRule, which the strategy applies in its place (costed identically via the OSS feature; the introduced concrete-ruleset taclet is then applied normally). Formulas with modal operators are still simplified by the opaque rule. OneStepSimplifier.isApplicable now partitions on transparent mode; canSimplify exposes the unpartitioned notion for the generator. The lemma introduction rule gained a guard so an already-available lemma is not re-introduced (avoids non-termination under automation). CLI: --save-transparent additionally writes <file>.transparent.proof in batch mode via the new TransparentProofSaver (elaborates onto a fresh proof of the same problem and saves; original untouched). GUI: SaveTransparentProofAction in the File menu, the proof/task-list context menu, and as a button in the proof-closed statistics dialog (background worker, status-line feedback). Created with AI tooling support
Extends the proof management dialog (the proof obligation browser) with a 'Missing Lemmas' tab listing, for the selected proof, the generated lemmas it still depends on whose soundness proof obligation has not been discharged (not created, or created but open). Entries can be selected individually or all at once and loaded as side proofs into the same proof environment, where they appear in the task tree and can be proved like any other obligation. Core support: - GeneratedLemma retains the soundness ProofAggregate and exposes getOrCreateSoundnessProofAggregate() (what a UI registers), plus isSoundnessProofPresent()/isProven() status. - GeneratedLemmaRegistry.getMissingLemmas() enumerates the not-yet-proven lemmas; getIfPresent(proof) inspects without attaching a registry. GUI: - MissingLemmasPanel (multi-select list, 'Select all' / 'Load selected as side proofs'); creating an aggregate registers it in the environment (done by GeneratedLemma) and the panel adds it to the UI via registerProofAggregate. - ProofManagementDialog gains the tab, refreshed from the selected proof. Test TestMissingLemmas drives the lifecycle headlessly: all lemmas initially missing, creating a side proof registers it in the environment and leaves the (open) lemma missing, discharging it removes it from the missing set, and re-requesting returns the same proof (no duplicate). Created with AI tooling support
Transparent automode on SumAndMax ran away: thousands of introduce_ossLemma steps, taclets that never applied, visually no-op lemmas, proof not closing (12000-node cap: 11200 introductions, 59 lemma applications, open). Root cause 1 - lemma name aliasing across branches: 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. The purely content-derived (print-based) lemma names aliased such formulas, so the registry handed branch B a taclet built from branch A's instances; it could never match, and every automation round re-introduced it. Fix: OSS lemma names are qualified with the introduction node's tree-structural id (Node.getUniqueTacletId, the mechanism QueryExpand uses), which is replay-stable, branch-distinguishing, and prune-consistent. Within-branch reuse is unaffected (the introduced taclet is inherited and applied). The registry additionally verifies on every name hit that the cached taclet's find equals the regenerated one, turning any residual aliasing into a RuleAbortException instead of a dead taclet. Root cause 2 - semantic no-op lemmas: aggregated simplifications whose result equals the formula up to renaming and term labels produced worthless lemmas and kept the formula eligible forever. The generator now rejects them and vetoes the formula; the veto is proof-local state in the registry (a JVM-wide cache would leak vetoes into the replay of a reloaded proof). Root cause 3 - index-dependent applicability: the previous guard against re-introduction consulted the goal-local taclet index in isApplicable. Rule applications are queued, so the original run could legitimately record an introduction that the guard would reject when re-evaluated freshly - which is exactly what proof replay does, making a few recorded introductions unreplayable. Built-in applicability is now pure in the formula; occasional redundant introductions are harmless (unique names) and replay faithfully. SumAndMax with transparent automode now closes (2568 nodes, 241 introductions = 241 distinct lemmas, 229 applied, opaque OSS only on modality formulas, no no-op lemmas) and the saved proof replays to closed; kept as regression test TestTransparentModeSumAndMax. Created with AI tooling support
Circularity (soundness bug): a generated lemma's soundness proof obligation inherited the main proof's strategy settings. In transparent mode that meant the obligation was discharged by generating and applying further lemmas - re-deriving the very simplification it must justify from first principles, a circular and non-terminating justification (probe: 2 introductions + 1 lemma application inside the obligation proof). GeneratedLemma now forces the opaque one step simplifier on the proof-obligation configuration, so soundness is established in the base calculus. Regression test TestLemmaSoundnessNonCircular asserts the obligation runs OSS_ON and contains no introduce_ossLemma / ossLemma_ steps. Duplicate task-tree entries: creating a lemma soundness proof registers it in the proof environment, and the user interface already listens on the environment (proofRegistered -> registerProofAggregate -> task tree). The Missing Lemmas panel registered it a second time explicitly; that call is removed. The panel now also runs an onLoaded action so the proof management dialog closes after loading (previously it stayed open). Created with AI tooling support
Replaces the flat, dialog-global 'Missing Lemmas' tab with a per-proof dependency view living beside the used contracts, and organizes the many generated lemmas for overview. Placement: the 'By Proof' tab's right pane is now a Contracts | Lemmas tabbed pane, both scoped to the selected proof (the top-level Missing Lemmas tab is gone). This mirrors the used-contracts dependency view for lemmas. Overview: LemmaDependencyPanel shows the selected proof's lemmas as a tree grouped by generator and, within each generator, collapsed by content (GeneratedLemmaRegistry.groupByContent) - the many introduction-point-distinct instances of the same simplification appear as one row with a count and a proven/open status. On SumAndMax this turns ~241 flat rows into a handful of distinct simplification shapes. Actions: - 'Load selected as side proofs' creates the obligation proofs for the selected generator/content rows (registered in the environment, shown in the task tree). - 'Prove all lemmas...' batch-discharges via the new core LemmaProver: each obligation is proved with a user-chosen step bound (default 10000); obligations that do not close stay open for manual work; the obligation proofs can optionally be saved to a directory. Runs in the background; robust to a single obligation whose automatic search fails. Core additions (headless-tested in TestLemmaProverAndGrouping): GeneratedLemma.generatorName()/contentKey(); GeneratedLemmaRegistry.getLemmasByGenerator()/groupByContent(); LemmaProver. Created with AI tooling support
…igations Two soundness-relevant fixes to the generated-lemma proof obligations. (1) DefaultLemmaGenerator dropped concrete bound variables. Its rebuild() kept a quantifier's bound variable only when it was a schema variable (VariableSV); hand-written taclets only ever bind schema variables, so this was never exercised. Lemmas generated from concrete proof formulas, however, contain concrete quantifiers (\forall i; ... over a LogicVariable), and those bound variables were dropped, so a quantified subterm was rebuilt with an empty bound-variable list and failed the term arity check - a TermCreationException during obligation generation (not a rule soundness problem and not automation, as first suspected). rebuild() now passes concrete bound variables through unchanged. The change is inert for schema-variable taclets; ProveRulesTest (203 standard taclet proofs) still passes, and SumAndMax's quantifier lemmas now both generate and close (regression test testQuantifierLemmaObligationsGenerateAndClose). (2) The obligation is now proved with the one step simplifier switched off entirely, not merely downgraded from transparent to opaque. Opaque OSS still performs the same aggregated simplification in one hidden step, which would close a lemma's obligation by exactly the transformation under scrutiny. With OSS off, soundness is established from the individual base-calculus rewrite rules the lemma aggregates. Created with AI tooling support
Four defects found by GUI testing on BinarySearch (contract PO, transparent
mode), each with a distinct root cause:
(1) BoundUniquenessChecker rejected generated lemmas whose find and assumes
clauses share bound variables ('A bound SchemaVariable variables occurs both
in assumes and find clauses'). The restriction exists - per the checker's own
documentation - for schematic bound variables, which would have to match the
identical quantified variable everywhere so that the taclet would almost
never apply. Taclets generated from proof formulas legitimately share
concrete LogicVariable binders between assumes and find (both stem from the
same sequent). The check now applies to schema variables only. This is the
third schematic-only assumption uncovered by generated concrete taclets
(after DefaultLemmaGenerator's binder handling and the naming/aliasing
issue).
(2) The same exception, thrown out of lemma generation during automated
search, aborted the strategy mid-run ('stops after 95 steps').
OssLemmaGenerator.generate now converts any taclet-construction failure into
a veto of the formula plus a clean RuleAbortException; automated search can
no longer be halted by a generation failure.
(3) InitConfig.deepCopy copied proof-local justifications. Entries that
reference nodes of the source proof (addrule taclets such as
replaceKnownSelect, generated lemmas) collided with rule re-introductions
when a proof is elaborated or replayed onto a copied configuration ('A rule
named ... has already been registered') - a pre-existing hazard for stock
addrule taclets as well. RuleJustification gains isProofLocal() (true for
RuleJustificationByAddRules and GeneratedLemmaJustification), and
RuleJustificationInfo.copy() skips proof-local entries. The lemma registry
additionally replaces foreign same-name entries defensively.
(4) TransparentProofSaver produced unloadable files for proofs of generated
proof obligations: PO-created program variables are not part of the problem
header, and without the \proofObligation section the saved file cannot
re-create them. The elaborated proof is now registered with the original's
ProofOblInput, so saving emits the obligation section and the file loads.
Regression test TestTransparentModeBinarySearch covers the full workflow:
transparent automode closes, the transparent form saves and replays to
closed including the lemma introductions, and every lemma soundness
obligation closes in the base calculus. Full key.core suite passes.
Created with AI tooling support
Replaces the hybrid transparent mode (opaque OSS on modality formulas) by a fully transparent one, following the observation that the opaque residue was almost exclusively update-prefix simplification in front of modalities (probe on SumAndMax: 38 of 39 opaque applications on update-application formulas; ~460 of ~480 aggregated micro steps from the update rule sets). In transparent mode the one step simplifier now - is applicable nowhere (previously it kept handling modality formulas), and - no longer takes the captured rule set taclets out of the goals' rule indices (appsTakenOver stays empty); its internal indices still serve as the computation core of the lemma generator. Formulas outside the lemma fragment are thus simplified by the ordinary strategy in individual, fully visible steps - transparent proofs contain no opaque aggregation of any kind. (For contrast: an opaque OSS step persists nothing about the rules it aggregated - only position and used context formulas are saved, and replay re-runs the whole fixpoint trusting that the current rule base reproduces the result.) Fixed in passing: refresh() short-circuited on mode flips for an unchanged proof - the loader's initial refresh (opaque, default settings) had already captured the taclets, and switching to transparent neither restored them nor rebuilt, leaving goals without simplification rules entirely (automode saturated after a few steps). refresh() now shuts down (restoring any taken-over taclets) before re-initializing on any state change. computation.key: 775 nodes with OSS off, 728 fully transparent (15 introductions, 10 lemma applications; a few lemmas are obsoleted by individual steps between introduction and application - scheduling to be tuned in a follow-up), 597 opaque. Old transparent proofs containing opaque modality-OSS steps no longer replay (pre-release format change). Created with AI tooling support
Tunes the fully transparent mode so that aggregated lemmas, not individual rule applications, perform the simplification wherever the lemma path applies. Baseline measurements (computation/SumAndMax/BinarySearch) showed 23-35% of introductions wasted and 130-145 captured-rule-set singles firing on modality-free formulas. Scheduling: - Generated lemma taclets carry the new rule set 'generatedLemma' (declared in ruleSetsDeclarations.key), bound like 'concrete' (-11000 plus depth scaling), so a blanket treatment of the captured rule sets cannot penalize the lemma applications themselves. - In transparent mode, applications of the seven OSS-captured rule sets are penalized on formulas without executable code (focus-conditional feature) - exactly where the lemma path competes; symbolic-execution scheduling is untouched, and the rules remain applicable everywhere (completeness). - The penalty is deliberately small (+2000): it only breaks the cost tie with the lemma path. A large penalty inverts cost orderings that encode termination invariants of the strategy - observed as an unbounded bounded-sum descent, where the unrolling rule (enlarging, about -2000) outranked its penalized empty-range counterpart (concrete) forever. Determinism (found by elaborating a transparent proof onto a fresh copy): - The simplifier's captured-taclet indices were built in set-iteration order; when several rules match at one position, proof instances of the same problem could simplify differently. The taclets are now sorted by name before index construction. - The sub-origins of merged origin term labels are collected in object identity order, so the printed form of otherwise identical terms differs between proof instances. Lemma names and content-grouping keys are now computed from label-stripped terms (LemmaTacletGenerator.removeTermLabels); labels are proof metadata, and lemma identity is secured by the introduction-node id. Also: GeneratedLemma.aggregatedSteps() records how many base calculus steps a lemma aggregates (measurement and display metadata; the generator returns a GeneratedTaclet record). Results: wasted introductions 0 on all three examples (from 5/55/66), captured singles on modality-free formulas roughly halved (rest are legitimate last-resort applications), total aggregated coverage increased, node counts and closure unchanged. Full key.core suite passes. Created with AI tooling support
…atus Two GUI defects reported on BinarySearch: after 'Prove all lemmas' the depending proof still showed 'closed but lemmas left' even though all lemmas were proven, and the batch registered all obligations, flooding the task tree with closed side proofs. The proof status was in fact correct at the model level (proving a lemma obligation triggers the depending proof's status recomputation, which reads the obligation proof object, not its environment registration). The dialog simply never refreshed: updateGlobalStatus runs once when the dialog opens. Changes: - GeneratedLemma separates obligation creation from environment registration. getOrCreateSoundnessProofAggregate now only creates; registerInEnvironment (idempotent) registers so a user interface surfaces the obligation. - LemmaProver registers only obligations that remain open (for manual work); closed obligations are certificates and stay unregistered, so a batch does not flood the environment. The depending proof's status still tracks them. - LemmaDependencyPanel: 'Load selected as side proofs' registers explicitly; after 'Prove all lemmas' it recomputes the depending proof's status (robust against proof-tree listener ordering) and refreshes the dialog's status display via a callback. Regression testBatchProvingUpdatesStatusWithoutFloodingEnvironment: proving all lemmas turns the status to CLOSED automatically and leaves the environment's proof count unchanged. Created with AI tooling support
Right-clicking an environment node in the Loaded Proofs tree now offers 'Abandon All Proofs of Environment', which disposes every proof of that environment after a single confirmation. Previously an environment that had accumulated many proofs (e.g. lemma side proofs loaded in bulk from the proof management dialog) could only be cleared by abandoning each proof individually or restarting KeY. The proofs are collected before disposing, since disposing a proof removes its node from the tree. Created with AI tooling support
Batch proving many lemma obligations gave no feedback while it ran. It now shows a small modeless progress dialog with a progress bar (done / total) and a Cancel button. LemmaProver.proveAll gained a progress listener that reports after each obligation and can request cancellation (the remaining, unprocessed lemmas are then simply not attempted); the existing three-argument overload delegates to it with no listener. The panel drives the bar via the SwingWorker's publish/process and disposes the dialog when done. Created with AI tooling support
unp1
force-pushed
the
bubel/lemma-taclet-spike
branch
from
bf9bf19 to
118a542
Compare
unp1
changed the title
Member
|
There was also a wiki entry on this from the discussion in 2019: https://git.key-project.org/key/key/-/wikis/Taclet-Generation-Language |
unp1
added a commit
to KeYProject/key-docs
that referenced
this pull request
Jul 5, 2026
Member
Author
Thanks! I put the link at the top of PR description. |
unp1
force-pushed
the
bubel/lemma-taclet-spike
branch
from
6329c14 to
ee3e2b7
Compare
Removes two batch-mode proof outputs (lemmagen-demo.auto*.proof) and a statistics CSV that were swept in by a broad 'git add' while wiring up the OSS lemma generator. Only the intentional demo problem lemmagen-demo.key remains. Created with AI tooling support
unp1
force-pushed
the
bubel/lemma-taclet-spike
branch
from
ee3e2b7 to
4294be3
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Status: RFC / proof-of-concept.
Companion documentation (concept, GUI walkthrough,
beyond-OSS): https://keyproject.github.io/key-docs/keps/kep-0001-taclet-generating-transformers/.
Reference to Discussion 2019 (original idea @wadoon): Taclet generation Language (at the moment internal only)
Addresses similar issue as #3707 by @Drodt but from a different angle
KEP moniker coined by @WolframPfeifer ;-)
Motivation
Several parts of KeY perform many calculus steps at once in Java: term
transformers (metaconstructs like
#add) and built-in rules like the One StepSimplifier (OSS).
Their advantage is performance and the ability to perform complex transformations.
But they are implemented in Java and therefore harder to inspect as a taclet.
This PR explores a middle path: instead of a transformer that mutates the
proof, a generator produces a specialized, metaconstruct-free taclet
that captures the transformation. It is introduced (a recorded step),
applied (an ordinary recorded taclet application), and provable (a
soundness obligation is created and discharged in the base calculus). The
performed transformation becomes an inspectable, separately certifiable
artifact — and a changed result surfaces immediately, because the recorded
name hashes the outcome.
The state of the implementation is suitable for trying it out and discussing
whether to carry it forward or not. It is not finalized. Also the show case in
this example is the OSS, the framework is more general and not restricted to OSS.
In principle one could write complex transformations that establish Groebner bases in
one step and proof that transformation later correct as part of the soundness proof
obligation for the taclet.
What this changes, at a glance
de.uka.ilkd.key.rule.lemma— the framework:LemmaTacletGenerator(contract: context-free via
\assumes, in the provable fragment,deterministic content-derived names),
LemmaIntroductionRule(built-in),GeneratedLemmaRegistry,GeneratedLemma(lazy soundness obligation),LemmaProver(batch discharge),TransparentProofSaver,LemmaElaboratingProofReplayer(a-posteriori elaboration).OssLemmaGenerator+OneStepSimplifier.computeSimplification(...)— OSS asthe first real generator (a pure extract-method exposing its core; no change
to opaque OSS behavior).
ProofCorrectnessMgttracks unproven generated lemmas(
CLOSED_BUT_LEMMAS_LEFT).generator + content, batch-provable),
Save Transparent Proof…, and an"abandon all proofs of an environment" cleanup.
--save-transparent.Two proof steps
p & true & (q | true) -> true & p, OSS Enabled:Same problem, OSS Transparent:
How generators map to lemmas
OssLemmaGeneratorturns an aggregatedF ↝ F'into a ground taclet; thecontext formulas of OSS's replace-known steps become an
\assumesclause with\inSequentState(mirroring OSS's own discipline). Modality-containingformulas are outside the provable fragment and stay with the ordinary calculus.
Obligations are created lazily (off the search path) and proved with OSS off from the individual base rules the lemma aggregates, never by the aggregation under scrutiny.
Two operating modes
Transparentstrategy option. In transparent mode OSS isapplicable nowhere and does not steal its rule sets from the goals, so
modality-free formulas go through generated lemmas while everything else is
simplified by the ordinary calculus in individual steps. Proofs contain no
opaque OSS node at all. A small focus-conditional cost penalty makes the
lemma path win the scheduling race on eligible formulas without disturbing
symbolic-execution scheduling.
finished proof into a transparent one (this is what "Save Transparent Proof"
does). Search stays fast; transparency is produced on demand.
Design points for discussion
No proof-format migration; folding intro+apply into one node would be a
view filter (not in this PR).
proofs load and replay-to-closed, but replay re-runs the generator; the
content-hash names make this deterministic, and a changed result fails loudly
("taclet not found"). Serializing the taclets — so a checker needs only the
taclet text + its obligation and the generator drops out of the trusted base
— is the natural next step, deliberately out of scope.
lemma-eligible; program modalities are not. Generalizing update-prefix
simplification (schematizing the unchanged modality kernel) would widen the
fragment and is a designed follow-up, not built here.
proof formulas legitimately re-bind concrete variables; the check's own
documentation says the restriction is about schema variables, so this aligns
code with intent rather than weakening an invariant.
Trying it out
./gradlew :key.ui:run, loadlemmagen-demo.key, right-click a5 + 7subterm →introduce_addLitLemma, then apply the generated taclet.proof, inspect the
ossLemma_…steps; open Proof Management → By Proof →Lemmas to prove the obligations.
./gradlew :key.ui:run --args="--auto --save-transparent <file>.key"../gradlew :key.core:runOssReuseProbe.Testing
New tests under
de.uka.ilkd.key.rule.lemmacover: introduction / application /obligation / replay / reuse (toy); OSS lemmas with and without assumptions,
including update-formula obligations; transparent-mode automode on
computation / SumAndMax / BinarySearch (and that stock mode is unchanged);
non-circular obligations (OSS off); quantifier-obligation generation (regression
for the
DefaultLemmaGeneratorfix); a-posteriori elaboration; batch proving,content grouping, status transition and no-flooding.
ProveRulesTestconfirmsthe shared translation change is inert for the standard taclet base.
Not for merge as-is / follow-ups
lemmagen-demo.keysits at the repo root for reviewer convenience; move underkey.ui/examples/(or drop) before merge.\rulesserialization of generated taclets (generator-independent checking).No proof loadedselection-listener crash exposed by bulk-abandon isfixed upstream in Fix GUI crashes when no proof is loaded, and remove dead MainWindowTabbedPane #3892 (not duplicated here).
Code with AI tooling support.