From 980078dced1fbdcc4b06de714950875f1ba73b37 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 16 Aug 2026 15:08:29 +0200 Subject: [PATCH 1/7] first working implementation of JML lemmas and use_lemma instructions. --- key.core/src/main/antlr4/JmlLexer.g4 | 2 + key.core/src/main/antlr4/JmlParser.g4 | 8 +- .../uka/ilkd/key/java/SpecialJavaPrinter.java | 3 +- .../ast/declaration/MethodDeclaration.java | 6 + .../java/ast/declaration/ModifierKind.java | 1 + .../java/ast/statement/UseLemmaStatement.java | 63 ++++++++ .../ilkd/key/java/loader/JP2KeYConverter.java | 5 + .../MarkerStatementHelper.java | 4 + .../pipeline/JMLTransformer.java | 15 +- .../key/java/visitor/CreatingASTVisitor.java | 13 ++ .../ilkd/key/java/visitor/JavaASTVisitor.java | 5 + .../de/uka/ilkd/key/java/visitor/Visitor.java | 2 + .../uka/ilkd/key/logic/op/ProgramMethod.java | 4 + .../de/uka/ilkd/key/pp/PrettyPrinter.java | 25 +++ .../uka/ilkd/key/proof/init/JavaProfile.java | 1 + .../rule/UseLemmaStatementBuiltInRuleApp.java | 52 ++++++ .../ilkd/key/rule/UseLemmaStatementRule.java | 148 ++++++++++++++++++ .../rule/metaconstruct/IntroAtPreDefsOp.java | 4 + .../de/uka/ilkd/key/speclang/SLEnvInput.java | 2 + .../key/speclang/jml/JMLSpecExtractor.java | 2 +- .../pretranslation/TextualJMLLemmaDecl.java | 79 ++++++++++ .../pretranslation/TextualJMLMethodDecl.java | 53 ++----- .../TextualJMLMethodOrLemmaDecl.java | 63 ++++++++ .../TextualJMLUseLemmaStatement.java | 62 ++++++++ .../jml/translation/JMLSpecFactory.java | 23 +++ .../key/speclang/njml/TextualTranslator.java | 17 ++ .../ilkd/key/speclang/njml/Translator.java | 10 ++ .../key/scripts/DocumentationGenerator.java | 20 +++ .../njml/MethodlevelTranslatorTest.java | 5 +- .../util/collection/ImmutableArray.java | 21 ++- 30 files changed, 665 insertions(+), 53 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index d90a738ff3d..778bdc79b0f 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -70,6 +70,7 @@ PURE: 'pure'; RETURN_BEHAVIOR: 'return_' BEHAVIOR; FINAL: 'final'; MODEL: 'model'/* -> pushMode(expr)*/; +LEMMA: 'lemma' -> pushMode(expr); fragment Pred: '_redundantly'?; //suffix fragment Pfree: '_free'?; //suffix @@ -139,6 +140,7 @@ SEPARATES: 'separates' -> pushMode(expr); SET: 'set' -> pushMode(expr); SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr); SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr); +USE_LEMMA: 'use_lemma' -> pushMode(expr); VAR: 'var'; WHEN: 'when' Pred -> pushMode(expr); WORKING_SPACE: 'working_space' Pred -> pushMode(expr); diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index aed3866b353..1eacc0246ae 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -22,6 +22,7 @@ classlevel_element0: modifiers? (classlevel_element modifiers?); classlevel_element : class_invariant | accessible_clause | method_specification | method_declaration | field_declaration | represents_clause + | lemma_declaration | history_constraint | initially_clause | class_axiom | monitors_for_clause | readable_if_clause | writable_if_clause | datagroup_clause | set_statement | nowarn_pragma @@ -33,7 +34,7 @@ methodlevel_element : field_declaration | set_statement | merge_point_statement | loop_specification | assert_statement | assume_statement | nowarn_pragma | debug_statement | block_specification | block_loop_specification - | assert_statement | assume_statement + | assert_statement | assume_statement | use_lemma_statement ; modifiers: modifier+; @@ -157,13 +158,15 @@ name_clause: SPEC_NAME STRING_LITERAL SEMICOLON ; field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI_TOPLEVEL; method_declaration: typespec IDENT param_list (method_body=mbody_block | SEMI_TOPLEVEL); -mbody_block: LBRACE mbody_var* mbody_statement RBRACE; +mbody_block: LBRACE (mbody_var | assert_statement)* mbody_statement RBRACE; mbody_statement: RETURN expression SEMI_TOPLEVEL #mbody_return | IF LPAREN expression RPAREN (mbody_statement | mbody_block) ELSE (mbody_statement | mbody_block) #mbody_if ; mbody_var: VAR? IDENT EQUAL_SINGLE expression SEMI_TOPLEVEL; +lemma_declaration: LEMMA IDENT param_list assertionProof SEMI_TOPLEVEL; + param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN; param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*; history_constraint: CONSTRAINT expression; @@ -176,6 +179,7 @@ maps_into_clause: MAPS expression; nowarn_pragma: NOWARN expression; debug_statement: DEBUG expression; set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI_TOPLEVEL; +use_lemma_statement: USE_LEMMA postfixexpr SEMI_TOPLEVEL; merge_point_statement: MERGE_POINT (MERGE_PROC (proc=STRING_LITERAL))? diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java index c148c5b6a51..fa64ae601ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java @@ -94,7 +94,8 @@ private void print(List spec) { } case TextualJMLInitially c -> print(c.getModifiers(), c.getInv().first); case TextualJMLMergePointDecl c -> print(c.getModifiers(), c.getMergeProc()); - case TextualJMLMethodDecl c -> print(c.getModifiers(), c.getDecl()); + case TextualJMLMethodOrLemmaDecl c -> + print(c.getModifiers(), c.getMethodDefinition()); case TextualJMLModifierList c -> print(c.getModifiers()); case TextualJMLRepresents c -> print(c.getModifiers(), c.getRepresents().first); case TextualJMLSetStatement c -> print(c.getAssignment()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java index a4337f93c26..aa817cc1e9c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLemmaDecl; import de.uka.ilkd.key.speclang.njml.SpecMathMode; import org.key_project.util.ExtList; @@ -424,6 +425,11 @@ public boolean isModel() { return super.isModel(); } + public boolean isLemma() { + return attachedJml.stream().anyMatch(TextualJMLLemmaDecl.class::isInstance); + } + + @Override public int getStateCount() { return super.getStateCount(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java index 18afc540e0d..2ffacdfa121 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java @@ -55,6 +55,7 @@ public enum ModifierKind { JML_CODE("code"), JML_OT_PEER("peer"), JML_OT_REP("rep"), + JML_LEMMA("lemma"), JML_OT_READ_ONLY("read_only"); private final String codeRepresentation; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java new file mode 100644 index 00000000000..c0f45132dbe --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java @@ -0,0 +1,63 @@ +/* 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.java.ast.statement; + +import de.uka.ilkd.key.java.ast.PositionInfo; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.speclang.njml.JmlParser; + +/** + * JML use_lemma statement + * + * @author Mattias Ulbrich + */ +public class UseLemmaStatement extends JavaStatement { + + /** + * The parser context of the statement produced during parsing. + */ + private final JmlParser.PostfixexprContext context; + + /** Constructor used in recoderext */ + public UseLemmaStatement(JmlParser.PostfixexprContext context, PositionInfo positionInfo) { + super(positionInfo); + this.context = context; + } + + /** Constructor used when cloning */ + public UseLemmaStatement(UseLemmaStatement copyFrom) { + this(copyFrom.context, copyFrom.getPositionInfo()); + } + + /** + * Removes the attached parser context from this set statement + * + * @return the parser context that was attached + */ + public JmlParser.PostfixexprContext getParserContext() { + return context; + } + + /** {@inheritDoc} */ + @Override + public void visit(Visitor v) { + v.performActionOnUseLemmaStatement(this); + } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new IndexOutOfBoundsException("UseLemmaStatement has no program children"); + } + + @Override + protected int computeHashCode() { + return System.identityHashCode(this); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index 773c8bcbb0b..371707082a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -40,6 +40,7 @@ import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLUseLemmaStatement; import org.key_project.logic.MetaSpace; import org.key_project.logic.Namespace; @@ -775,6 +776,10 @@ public Object visit(KeYMarkerStatement n, Void arg) { KeyAst.SetStatementContext context = n.getData(MarkerStatementHelper.KEY_ASSIGN); yield new SetStatement(context, pi); } + case MarkerStatementHelper.KIND_USE_LEMMA -> { + TextualJMLUseLemmaStatement stm = n.getData(MarkerStatementHelper.KEY_USE_LEMMA); + yield new UseLemmaStatement(stm.getExpression(), pi); + } case MarkerStatementHelper.KIND_MERGE_POINT -> { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java index 6e390ca18b5..1d1328f814c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLUseLemmaStatement; import com.github.javaparser.ast.DataKey; @@ -20,6 +21,7 @@ public class MarkerStatementHelper { public static final int KIND_ASSUME = 2; public static final int KIND_SET = 3; public static final int KIND_MERGE_POINT = 4; + public static final int KIND_USE_LEMMA = 5; public static final DataKey KEY_ASSIGN = new DataKey<>() { }; @@ -27,4 +29,6 @@ public class MarkerStatementHelper { }; public static final DataKey KEY_ASSERT = new DataKey<>() { }; + public static final DataKey KEY_USE_LEMMA = new DataKey<>() { + }; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java index 6db5f5ed9ed..aacf4fccd70 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java @@ -191,7 +191,7 @@ public JMLTransformer(TransformationPipelineServices services) { * @return the new method declaration * @throws SLTranslationException */ - private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodDecl decl, + private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodOrLemmaDecl decl, @Nullable TextualJMLModifierList jmlModifiers) throws SLTranslationException { // prepend Java modifiers @@ -248,6 +248,13 @@ private Statement transformSetStatement(TextualJMLSetStatement stat) { return stmt; } + + private Statement transformUseLemmaStatement(TextualJMLUseLemmaStatement stat) { + KeYMarkerStatement stmt = new KeYMarkerStatement(KIND_USE_LEMMA); + stmt.setData(KEY_USE_LEMMA, stat); + return stmt; + } + private KeYMarkerStatement transformMergePointDecl(TextualJMLMergePointDecl stat) { KeYMarkerStatement mps = new KeYMarkerStatement(KIND_MERGE_POINT); mps.setData(KEY_MERGE_POINT, stat); @@ -294,7 +301,7 @@ private void transformClassLevelComments(TypeDeclaration td) throws SLTransla if (c instanceof TextualJMLFieldDecl fd) { // ghost/model field decl.: transform into "real" field decl. td.addMember(transformClassFieldDecl(fd)); - } else if (c instanceof TextualJMLMethodDecl md) { + } else if (c instanceof TextualJMLMethodOrLemmaDecl md) { // model method decl.: final MethodDeclaration decl = transformMethodDecl(md, jmlModifiers); jmlModifiers = null; // these are used now @@ -325,6 +332,8 @@ private void transformClassLevelComments(TypeDeclaration td) throws SLTransla String errorMessage = switch (c) { case TextualJMLSetStatement a -> "A set assignment only allowed inside of a method body"; + case TextualJMLUseLemmaStatement a -> + "A use_lemma statement is only allowed inside of a method body"; case TextualJMLMergePointDecl a -> "Merge points are only allowed inside of a method body"; case TextualJMLLoopSpec a -> @@ -442,6 +451,8 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName) // local ghost variable declaration! case TextualJMLFieldDecl field -> statement = transformVariableDecl(field); case TextualJMLSetStatement set -> statement = transformSetStatement(set); + case TextualJMLUseLemmaStatement ulema -> + statement = transformUseLemmaStatement(ulema); case TextualJMLMergePointDecl mergePointDecl -> statement = transformMergePointDecl(mergePointDecl); case TextualJMLAssertStatement assertStatement -> diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index 8a7e73b6849..1c974769cd7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -607,6 +607,19 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + @Override + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + // there are no AST elements below the use lemma statement, so we can use the copy + // constructor. + return new UseLemmaStatement(x); + } + }; + def.doAction(x); + } + @Override public void performActionOnReturn(Return x) { DefaultAction def = new DefaultAction(x) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index 10619d18977..972485a159d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -216,6 +216,11 @@ public void performActionOnSetStatement(SetStatement x) { doDefaultAction(x); } + @Override + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + doDefaultAction(x); + } + @Override public void performActionOnDefault(Default x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index 4cc400fdb05..701fbbc0bc2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -149,6 +149,8 @@ public interface Visitor { void performActionOnSetStatement(SetStatement x); + void performActionOnUseLemmaStatement(UseLemmaStatement x); + void performActionOnConditional(Conditional x); void performActionOnNewArray(NewArray x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java index 8be2ed213ab..b54c6d086c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java @@ -226,6 +226,10 @@ public boolean isModel() { return method.isModel(); } + public boolean isLemma() { + return method.isLemma(); + } + /** * Test whether the declaration is strictfp. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index 09348df07c7..22a1006765d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -1743,6 +1743,31 @@ public void performActionOnSetStatement(SetStatement x) { layouter.end(); } + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + layouter.print("//@ "); + layouter.keyWord("use_lemma"); + + layouter.beginRelativeC(); + layouter.brk(); + + if (services != null) { + var spec = + Objects.requireNonNull(services.getSpecificationRepository().getStatementSpec(x)); + JTerm lemma = spec.term(0); + layouter.print(printInLogicPrinter(lemma)); + } else { + var context = x.getParserContext(); + if (context != null) { + // remove all whitespaces (\n\f\t...) with an empty space + var text = context.getText(); + // text = text.substring(11, text.length() - 1); + layouter.print(text); + } + } + layouter.end(); + } + + public String printInLogicPrinter(JTerm t) { var lp = LogicPrinter.quickPrinter(services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); 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 dd04fd01632..4d0e743ef40 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 @@ -189,6 +189,7 @@ protected ImmutableList initBuiltInRules() { .prepend(LoopApplyHeadRule.INSTANCE).prepend(JmlAssertRule.ASSERT_INSTANCE) .prepend(JmlAssertRule.ASSUME_INSTANCE) .prepend(SetStatementRule.INSTANCE) + .prepend(UseLemmaStatementRule.INSTANCE) .prepend(ObserverToUpdateRule.INSTANCE); // contract insertion rule, ATTENTION: ProofMgt relies on the fact diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.java new file mode 100644 index 00000000000..400511fd71b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.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; + +import java.util.Objects; + +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NullMarked; + +/** + * The rule application for {@link de.uka.ilkd.key.java.statement.UseLemmaStatement} + * + * @author Julian Wiesler + */ +@NullMarked +public class UseLemmaStatementBuiltInRuleApp extends AbstractBuiltInRuleApp { + /** + * @param rule the rule being applied + * @param occurrence the position at which the rule is applied + */ + public UseLemmaStatementBuiltInRuleApp(UseLemmaStatementRule rule, PosInOccurrence occurrence) { + super(rule, Objects.requireNonNull(occurrence, "rule application needs a position"), null); + if (rule == null) { + throw new IllegalArgumentException(String.format( + "can only create an application for SetStatementRule, not for %s", rule)); + } + } + + @Override + public UseLemmaStatementBuiltInRuleApp replacePos(PosInOccurrence newPos) { + return new UseLemmaStatementBuiltInRuleApp(rule(), newPos); + } + + @Override + public IBuiltInRuleApp setAssumesInsts(ImmutableList ifInsts) { + // XXX: This is overridden in all subclasses to allow making ifInsts final + // when all usages of setIfInsts are corrected to use the result. + // Then a new instance has to be returned here. + setMutable(ifInsts); + return this; + } + + @Override + public UseLemmaStatementBuiltInRuleApp tryToInstantiate(Goal goal) { + return this; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java new file mode 100644 index 00000000000..4ad498e865f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java @@ -0,0 +1,148 @@ +/* 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; + +import java.util.Optional; + +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.MethodFrame; +import de.uka.ilkd.key.java.ast.statement.UseLemmaStatement; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.TermBuilder; +import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.logic.op.Transformer; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Name; +import org.key_project.logic.op.Modality; +import org.key_project.prover.rules.RuleAbortException; +import org.key_project.prover.rules.RuleApp; +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.NonNull; + +/** + * A rule for use_lemma statements. This turns a statement `use_lemma lemma(x)` to an assumption + * `lemma(x) = TRUE` which allows rules to be applied that set the expand the contract. + * + * @author Mattias Ulbrich + */ +public final class UseLemmaStatementRule implements BuiltInRule { + + /** + * The instance + */ + public static final UseLemmaStatementRule INSTANCE = new UseLemmaStatementRule(); + + /** + * The name of this rule + */ + private static final Name name = new Name("Use Lemma Statement"); + + private UseLemmaStatementRule() { + // no statements + } + + @Override + public boolean isApplicable(Goal goal, + PosInOccurrence occurrence) { + if (AbstractAuxiliaryContractRule.occursNotAtTopLevelInSuccedent(occurrence)) { + return false; + } + // abort if inside of transformer + if (Transformer.inTransformer(occurrence)) { + return false; + } + + JTerm target = (JTerm) occurrence.subTerm(); + if (target.op() instanceof UpdateApplication) { + target = UpdateApplication.getTarget(target); + } + final SourceElement activeStatement = JavaTools.getActiveStatement(target.javaBlock()); + return activeStatement instanceof UseLemmaStatement; + } + + @Override + public boolean isApplicableOnSubTerms() { + return false; + } + + @Override + public IBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices services) { + return new UseLemmaStatementBuiltInRuleApp(this, occurrence); + } + + @Override + public @NonNull ImmutableList apply(Goal goal, RuleApp ruleApp) + throws RuleAbortException { + if (!(ruleApp instanceof UseLemmaStatementBuiltInRuleApp)) { + throw new IllegalArgumentException("can only apply UseLemmaStatementBuiltInRuleApp"); + } + + final var services = goal.getOverlayServices(); + final TermBuilder tb = services.getTermBuilder(); + final PosInOccurrence occurrence = ruleApp.posInOccurrence(); + final JTerm formula = (JTerm) occurrence.subTerm(); + assert formula.op() instanceof UpdateApplication + : "Currently, this can only be applied if there is an update application in front of the modality"; + + JTerm update = UpdateApplication.getUpdate(formula); + JTerm target = UpdateApplication.getTarget(formula); + + UseLemmaStatement useLemmaStatement = + Optional.ofNullable(JavaTools.getActiveStatement(target.javaBlock())) + .filter(UseLemmaStatement.class::isInstance).map(UseLemmaStatement.class::cast) + .orElseThrow(() -> new RuleAbortException("not a JML set statement.")); + + final MethodFrame frame = JavaTools.getInnermostMethodFrame(target.javaBlock(), services); + final JTerm self = MiscTools.getSelfTerm(frame, services); + + var spec = services.getSpecificationRepository().getStatementSpec(useLemmaStatement); + + if (spec == null) { + throw new RuleAbortException( + "No specification for the set statement found in the specification repository."); + } + + var targetTerm = spec.getTerm(services, self, 0); + var assumption = tb.equals(targetTerm, tb.TRUE()); + + assert targetTerm.op() instanceof ProgramMethod pm && pm.isLemma(); + + JTerm updatedAssumption = tb.apply(update, assumption); + + JavaBlock javaBlock = JavaTools.removeActiveStatement(target.javaBlock(), services); + + JTerm term = + tb.prog(((Modality) target.op()).kind(), javaBlock, target.sub(0), target.getLabels()); + JTerm newTerm = tb.apply(update, term); + + ImmutableList result = goal.split(1); + result.head().changeFormula(new SequentFormula(newTerm), occurrence); + result.head().addFormula(new SequentFormula(updatedAssumption), true, true); + return result; + } + + @Override + public Name name() { + return name; + } + + @Override + public String displayName() { + return name.toString(); + } + + @Override + public String toString() { + return name.toString(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java index 86a6ba85cf9..4815c51b0ce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java @@ -192,6 +192,10 @@ public void performActionOnSetStatement(SetStatement x) { handleJmlStatement(x); } + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + handleJmlStatement(x); + } + private void handleJmlStatement(Statement x) { var spec = Objects.requireNonNull(services.getSpecificationRepository().getStatementSpec(x)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java index 44dec7429b0..1133703738e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java @@ -246,6 +246,8 @@ protected void doAction(final ProgramElement node) { jsf.translateJmlAssertCondition((JmlAssert) node, pm); } else if (node instanceof SetStatement) { jsf.translateSetStatement((SetStatement) node, pm); + } else if (node instanceof UseLemmaStatement useLemmaStatement) { + jsf.translateUseLemmaStatement(useLemmaStatement, pm); } } catch (ProofInputException e) { // Store the first exception that occurred diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java index 63e2ecda3c4..5f7487dda02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java @@ -295,7 +295,7 @@ public List extractMethodSpecs(IProgramMethod pm, boolean ParserRuleContext modelMethodDefinition = null; for (var c : constructs) { - if (c instanceof TextualJMLMethodDecl m) { + if (c instanceof TextualJMLMethodOrLemmaDecl m) { if (pm.getMethodDeclaration().containsModifier(ModifierKind.JML_MODEL)) { modelMethodDefinition = m.getMethodDefinition(); break; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.java new file mode 100644 index 00000000000..feba6cea7d6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.java @@ -0,0 +1,79 @@ +/* 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.speclang.jml.pretranslation; + +import java.util.Objects; + +import de.uka.ilkd.key.speclang.njml.JmlParser; + +import org.key_project.util.collection.ImmutableList; + +import org.antlr.v4.runtime.ParserRuleContext; + +/** + * A JML lemma declaration in textual form. + * + * This is a special case of a textual JML method declaration. + */ +public final class TextualJMLLemmaDecl extends TextualJMLMethodOrLemmaDecl { + private final JmlParser.Lemma_declarationContext lemmaDefinition; + + + public TextualJMLLemmaDecl(ImmutableList modifiers, + JmlParser.Lemma_declarationContext lemmaDefinition) { + super(modifiers.append(JMLModifier.MODEL)); + this.lemmaDefinition = lemmaDefinition; + setPosition(lemmaDefinition); + } + + public String getMethodName() { + return lemmaDefinition.IDENT().getText(); + } + + public ParserRuleContext getMethodDefinition() { + return lemmaDefinition; + } + + @Override + public String toString() { + return lemmaDefinition.getText(); + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + TextualJMLLemmaDecl that = (TextualJMLLemmaDecl) o; + return Objects.equals(lemmaDefinition, that.lemmaDefinition); + } + + @Override + public int hashCode() { + return Objects.hash(lemmaDefinition); + } + + public int getStateCount() { + if (modifiers.contains(JMLModifier.TWO_STATE)) { + return 2; + } + if (modifiers.contains(JMLModifier.NO_STATE)) { + return 0; + } + return 1; + } + + @Override + protected JmlParser.Param_listContext getParamListContext() { + return lemmaDefinition.param_list(); + } + + @Override + protected String getTypespecText() { + return "boolean"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java index 9b3aed84fea..f581d979471 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java @@ -4,23 +4,19 @@ package de.uka.ilkd.key.speclang.jml.pretranslation; import java.util.Objects; -import java.util.stream.Collectors; -import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; import de.uka.ilkd.key.speclang.njml.JmlParser; import org.key_project.util.collection.ImmutableList; -import org.key_project.util.java.StringUtil; import org.antlr.v4.runtime.ParserRuleContext; /** * A JML model method declaration in textual form. */ -public final class TextualJMLMethodDecl extends TextualJMLConstruct { +public final class TextualJMLMethodDecl extends TextualJMLMethodOrLemmaDecl { private final JmlParser.Method_declarationContext methodDefinition; - public TextualJMLMethodDecl(ImmutableList modifiers, JmlParser.Method_declarationContext methodDefinition) { super(modifiers); @@ -28,38 +24,16 @@ public TextualJMLMethodDecl(ImmutableList modifiers, setPosition(methodDefinition); } - public String getParsableDeclaration() { - String m = modifiers.stream().map(it -> { - if (JMLTransformer.JAVA_MODS.contains(it)) { - return it.toString(); - } else { - JMLModifier jmlModifier = JMLModifier.valueOf(it.name()); - if (jmlModifier == JMLModifier.NON_NULL || jmlModifier == JMLModifier.NULLABLE) { - return "/*@ " + jmlModifier + " @*/"; - } else { - return StringUtil.repeat(" ", it.toString().length()); - } - } - }).collect(Collectors.joining(" ")); - - String paramsString = methodDefinition.param_list().param_decl().stream() - .map(it -> (it.NULLABLE() != null ? "/*@ nullable @*/" - : it.NON_NULL() != null ? "/*@ non_null @*/" : "") - + " " + it.typespec().getText() + " " + it.p.getText() - + StringUtil.repeat("[]", it.LBRACKET().size())) - .collect(Collectors.joining(",")); - return String.format("%s %s %s (%s);", m, methodDefinition.typespec().getText(), - getMethodName(), paramsString); - } - - public JmlParser.Method_declarationContext getDecl() { - return methodDefinition; - } + // public JmlParser.Method_declarationContext getDecl() { + // return methodDefinition; + // } + @Override public String getMethodName() { return methodDefinition.IDENT().getText(); } + @Override public ParserRuleContext getMethodDefinition() { return methodDefinition; } @@ -86,14 +60,13 @@ public int hashCode() { return Objects.hash(methodDefinition); } - public int getStateCount() { - if (modifiers.contains(JMLModifier.TWO_STATE)) { - return 2; - } - if (modifiers.contains(JMLModifier.NO_STATE)) { - return 0; - } - return 1; + @Override + protected JmlParser.Param_listContext getParamListContext() { + return methodDefinition.param_list(); } + @Override + protected String getTypespecText() { + return methodDefinition.typespec().getText(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java new file mode 100644 index 00000000000..f63f916a62f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java @@ -0,0 +1,63 @@ +/* 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.speclang.jml.pretranslation; + +import java.util.stream.Collectors; + +import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; +import de.uka.ilkd.key.speclang.njml.JmlParser; + +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.java.StringUtil; + +import org.antlr.v4.runtime.ParserRuleContext; + +public abstract class TextualJMLMethodOrLemmaDecl extends TextualJMLConstruct { + + public TextualJMLMethodOrLemmaDecl(ImmutableList specModifiers) { + super(specModifiers); + } + + public String getParsableDeclaration() { + String m = modifiers.stream().map(it -> { + if (JMLTransformer.JAVA_MODS.contains(it)) { + return it.toString(); + } else { + JMLModifier jmlModifier = JMLModifier.valueOf(it.name()); + if (jmlModifier == JMLModifier.NON_NULL || jmlModifier == JMLModifier.NULLABLE) { + return "/*@ " + jmlModifier + " @*/"; + } else { + return StringUtil.repeat(" ", it.toString().length()); + } + } + }).collect(Collectors.joining(" ")); + + String paramsString = getParamListContext().param_decl().stream() + .map(it -> (it.NULLABLE() != null ? "/*@ nullable @*/" + : it.NON_NULL() != null ? "/*@ non_null @*/" : "") + + " " + it.typespec().getText() + " " + it.p.getText() + + StringUtil.repeat("[]", it.LBRACKET().size())) + .collect(Collectors.joining(",")); + return String.format("%s %s %s (%s);", m, getTypespecText(), + getMethodName(), paramsString); + } + + protected abstract JmlParser.Param_listContext getParamListContext(); + + protected abstract String getTypespecText(); + + public abstract String getMethodName(); + + public abstract ParserRuleContext getMethodDefinition(); + + public int getStateCount() { + if (modifiers.contains(JMLModifier.TWO_STATE)) { + return 2; + } + if (modifiers.contains(JMLModifier.NO_STATE)) { + return 0; + } + return 1; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java new file mode 100644 index 00000000000..dee02c371f0 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java @@ -0,0 +1,62 @@ +/* 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.speclang.jml.pretranslation; + +import java.util.List; + +import de.uka.ilkd.key.speclang.njml.JmlParser; + +import org.key_project.util.collection.ImmutableList; + +/** + * A JML "use_lemma" statement in textual form. + */ +public final class TextualJMLUseLemmaStatement extends TextualJMLConstruct { + + private final JmlParser.Use_lemma_statementContext statement; + + + public TextualJMLUseLemmaStatement(ImmutableList modifiers, + JmlParser.Use_lemma_statementContext statement) { + super(modifiers); + assert statement != null; + this.statement = statement; + } + + public boolean isSuitableExpression() { + JmlParser.PostfixexprContext postfix = statement.postfixexpr(); + JmlParser.PrimaryexprContext prim = postfix.primaryexpr(); + List primarysuffix = postfix.primarysuffix(); + if (primarysuffix.size() != 1) { + return false; + } + JmlParser.PrimarysuffixContext args = primarysuffix.get(0); + if (!(args instanceof JmlParser.PrimarySuffixCallContext)) { + return false; + } + return true; + } + + public JmlParser.PostfixexprContext getExpression() { + return statement.postfixexpr(); + } + + @Override + public String toString() { + return statement.toString(); + } + + @Override + public boolean equals(Object o) { + if (!(o instanceof TextualJMLUseLemmaStatement ss)) { + return false; + } + return modifiers.equals(ss.modifiers) && statement.equals(ss.statement); + } + + @Override + public int hashCode() { + return modifiers.hashCode() + statement.hashCode(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 16748c266ee..6749142e681 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -1596,6 +1596,29 @@ public void translateSetStatement(final SetStatement statement, final IProgramMe new SpecificationRepository.JmlStatementSpec(pv, ImmutableList.of(assignee, value))); } + + public void translateUseLemmaStatement(final UseLemmaStatement statement, + final IProgramMethod pm) + throws SLTranslationException { + final var pv = createProgramVariablesForStatement(statement, pm); + JmlParser.PostfixexprContext context = statement.getParserContext(); + var io = new JmlIO(services).context(Context.inMethod(pm, tb)).selfVar(pv.selfVar) + .parameters(pv.paramVars) + .resultVariable(pv.resultVar).exceptionVariable(pv.excVar).atPres(pv.atPres) + .atBefore(pv.atBefores); + JTerm lemmaCall = io.translateTerm(context); + + if(lemmaCall.op() instanceof ProgramMethod lpm && !lpm.isLemma()) { + throw new SLTranslationException( + "Invalid lemma call for use_lemma statement (only lemma invocations allowed): " + lemmaCall, + Location.fromToken(context.getStart())); + } + + services.getSpecificationRepository().addStatementSpec( + statement, + new SpecificationRepository.JmlStatementSpec(pv, ImmutableList.of(lemmaCall))); + } + /** * If the LHS of a set statement has been translated into a final term, this method undoes this * encoding since LHS need to be encoded as select terms for KeY's mechanisms to works. diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index 16b25347d77..1df50932dec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -496,6 +496,13 @@ public Object visitMethod_declaration(JmlParser.Method_declarationContext ctx) { return null; } + @Override + public Object visitLemma_declaration(JmlParser.Lemma_declarationContext ctx) { + TextualJMLLemmaDecl decl = new TextualJMLLemmaDecl(mods, ctx); + finishConstruct(decl); + return null; + } + @Override public Object visitSet_statement(JmlParser.Set_statementContext ctx) { TextualJMLSetStatement inv = new TextualJMLSetStatement(mods, ctx); @@ -503,6 +510,16 @@ public Object visitSet_statement(JmlParser.Set_statementContext ctx) { return null; } + public Object visitUse_lemma_statement(JmlParser.Use_lemma_statementContext ctx) { + TextualJMLUseLemmaStatement inv = new TextualJMLUseLemmaStatement(mods, ctx); + if (!inv.isSuitableExpression()) { + // TODO make sure this is amended by a position in the sources + throw new RuntimeException("use_lemma must go with a lemma invocation."); + } + finishConstruct(inv); + return null; + } + @Override public Object visitLoop_specification(JmlParser.Loop_specificationContext ctx) { loopContract = new TextualJMLLoopSpec(mods); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 9306427fd8e..aad148dd9aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -2369,6 +2369,7 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext return new SLExpression(tb.tt()); } + // TODO Is the following bit until `Object a = ...` really needed? String paramsString; List paramDecls = ctx.param_list().param_decl(); if (!paramDecls.isEmpty()) { @@ -2398,6 +2399,15 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext return termFactory.eq(apply, body); } + @Override + public SLExpression visitLemma_declaration(JmlParser.Lemma_declarationContext ctx) { + SLParameters params = visitParameters(ctx.param_list()); + SLExpression apply = lookupIdentifier(ctx.IDENT().getText(), null, params, ctx); + + SLExpression body = new SLExpression(termFactory.tb.TRUE()); + return termFactory.eq(apply, body); + } + @Override public SLExpression visitMbody_return(JmlParser.Mbody_returnContext ctx) { return accept(ctx.expression()); diff --git a/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java b/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java index 3249ade318f..016b9519a68 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java @@ -8,6 +8,21 @@ import de.uka.ilkd.key.util.KeYResourceManager; +/** + * Generates the Markdown documentation page for all registered KeY proof script commands. + *

+ * The output is written to {@code System.out} and is intended to be committed to the + * {@code key-docs} repository. + *

+ * Usage: + *

    + *
  • Without arguments: prints Markdown to standard output.
    • + *
  • With one argument: redirects output to the given file path.
    • + *
+ * To update the documentation in {@code key-docs}, run this generator and redirect/write the + * result to the target Markdown file in that repository. This is + * `key-docs/docs/user/ProofScripts/commands.md`. + */ public class DocumentationGenerator { private static String branch; @@ -79,6 +94,11 @@ private static void printHeader() { There *named* and *positional* arguments. Named arguments need to be prefixed by their name and a colon. Positional arguments are given in the order defined by the command. Optional arguments are enclosed in square brackets. + + !!! note "Document generation" + + This document is generated by the class `DocumentGenerator`. Look for that in the sources + to find out how to produce a new revision of this document. """, new Date(), branch, version, sha1); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java index 885dfd5f2df..7cc6e1d78e1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java @@ -9,6 +9,7 @@ import java.util.stream.Stream; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodOrLemmaDecl; import org.antlr.v4.runtime.CommonTokenStream; import org.junit.jupiter.api.DynamicTest; @@ -87,7 +88,7 @@ model nullable Object foo(nullable Nullable n) { assertTrue(translationOpt.isPresent(), "No model method declaration found"); final var methodDecl = - ((TextualJMLMethodDecl) translationOpt.get()).getParsableDeclaration(); + ((TextualJMLMethodOrLemmaDecl) translationOpt.get()).getParsableDeclaration(); assertTrue(methodDecl.contains("/*@ nullable @*/ Object"), "Return value is not nullable"); assertTrue(methodDecl.contains("/*@ nullable @*/ Nullable n"), "Parameter is not nullable"); } @@ -136,7 +137,7 @@ model non_null Object foo(non_null Nullable n) { assertTrue(translationOpt.isPresent(), "No model method declaration found"); final var methodDecl = - ((TextualJMLMethodDecl) translationOpt.get()).getParsableDeclaration(); + ((TextualJMLMethodOrLemmaDecl) translationOpt.get()).getParsableDeclaration(); assertTrue(methodDecl.contains("/*@ non_null @*/ Object"), "Return value is not non_null"); assertTrue(methodDecl.contains("/*@ non_null @*/ Nullable n"), "Parameter is not non_null"); diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index 5f7c68a5218..b0e84b86783 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -76,6 +76,21 @@ public ImmutableArray(@NonNull Collection list) { content = (S[]) list.toArray(); } + /** + *

+ * creates a new immutable array with the contents of the given list. + *

+ *

+ * The order of elements is defined by the collection. + *

+ * + * @param list a non-null collection (order is preserved) + */ + @SuppressWarnings("unchecked") + public ImmutableArray(@NonNull ImmutableList list) { + content = (S[]) list.toArray(Object.class); + } + /** * gets the element at the specified position * @@ -211,11 +226,7 @@ public void remove() { * @return This element converted to an {@link ImmutableList}. */ public ImmutableList toImmutableList() { - ImmutableList ret = ImmutableList.nil(); - for (S s : this) { - ret = ret.prepend(s); - } - return ret.reverse(); + return ImmutableList.fromArray(content); } /** From 5327310557a736f886e80782a6e919ad9702e63c Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 16 Aug 2026 15:38:06 +0200 Subject: [PATCH 2/7] adding test cases for JML lemmas --- .../jml/translation/JMLSpecFactory.java | 5 ++-- .../speclang/jml/TestJMLPreTranslator.java | 28 +++++++++++++++++-- .../njml/exceptional/IllegalUseLemma.java | 21 ++++++++++++++ 3 files changed, 49 insertions(+), 5 deletions(-) create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 6749142e681..2f34ff9f33b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -1608,9 +1608,10 @@ public void translateUseLemmaStatement(final UseLemmaStatement statement, .atBefore(pv.atBefores); JTerm lemmaCall = io.translateTerm(context); - if(lemmaCall.op() instanceof ProgramMethod lpm && !lpm.isLemma()) { + if (lemmaCall.op() instanceof ProgramMethod lpm && !lpm.isLemma()) { throw new SLTranslationException( - "Invalid lemma call for use_lemma statement (only lemma invocations allowed): " + lemmaCall, + "Invalid lemma call for use_lemma statement (only lemma invocations allowed): " + + lemmaCall, Location.fromToken(context.getStart())); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java index c165b32c3a8..eaea6d167e1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java @@ -3,9 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.speclang.jml; -import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase; +import de.uka.ilkd.key.speclang.jml.pretranslation.*; import de.uka.ilkd.key.speclang.njml.*; import org.key_project.util.collection.ImmutableList; @@ -15,6 +13,7 @@ import org.junit.jupiter.api.Test; import static de.uka.ilkd.key.speclang.njml.JmlLexer.*; +import static org.assertj.core.api.Assertions.assertThat; import static org.junit.jupiter.api.Assertions.*; @@ -269,4 +268,27 @@ public void testFailure2() { @ requires (;((;;);();();(();;;(;))); @*/""")); } + + @Test + public void testLemmaDefinition() { + ImmutableList constructs = parseMethodSpec(""" + /*@ requires n >= 2; + @ ensures 3*n*n >= 7; + @ static lemma someLemma(int n) \\by { + @ assert n >= 3 ==> 3*(n-1)*(n-1) >= 7 \\by { use_lemma someLemma(n-1); auto; } + @ auto; + @ }; + @*/"""); + + assertThat(constructs.get(0)).isInstanceOf(TextualJMLSpecCase.class); + TextualJMLSpecCase contract = (TextualJMLSpecCase) constructs.get(0); + assertThat(contract.getClauses()).hasSize(2); + + assertThat(constructs.get(1)).isInstanceOf(TextualJMLLemmaDecl.class); + TextualJMLLemmaDecl lemma = (TextualJMLLemmaDecl) constructs.get(1); + assertThat(lemma.getMethodName()).isEqualTo("someLemma"); + assertThat(lemma.getStateCount()).isEqualTo(1); + assertThat(lemma.getModifiers()).contains(JMLModifier.MODEL); + assertThat(lemma.getModifiers()).contains(JMLModifier.STATIC); + } } diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java new file mode 100644 index 00000000000..769bafef86b --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java @@ -0,0 +1,21 @@ +// exceptionClass: SLTranslationException +// msgContains: Invalid lemma call for use_lemma statement (only lemma invocations allowed) +// position: 19/23 +// verbose: true +// broken: false + +/* If there is no error message, this would close illegally. */ + +class IllegalUseLemma { + /*@ model boolean fakeLemma() { + @ return false; + @ } + @*/ + + boolean anything; + + /*@ ensures anything; */ + void m() { + //@ use_lemma fakeLemma(); + } +} From 460003107ae5c79a2839cd7e618c4822e7a8edca Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 16 Aug 2026 17:12:13 +0200 Subject: [PATCH 3/7] towards macro support for scripts in lemmas. --- .../LemmaAndModelMethodScriptMacro.java | 139 ++++++++++++++++++ .../uka/ilkd/key/macros/ScriptAwareMacro.java | 3 +- 2 files changed, 141 insertions(+), 1 deletion(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java new file mode 100644 index 00000000000..104ec87b0d8 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java @@ -0,0 +1,139 @@ +package de.uka.ilkd.key.macros; + +import de.uka.ilkd.key.control.UserInterfaceControl; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.njml.JmlParser; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.tree.ParseTree; +import org.key_project.logic.op.Function; +import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class LemmaAndModelMethodScriptMacro extends AbstractProofMacro { + + private static final String ID = "[A-Za-z_$0-9.]+"; + private static final Pattern NAME_PATTERN = + Pattern.compile(ID+ "\\[(" + ID + "::" + ID + ")\\(.*\\)\\].JML model_behavior operation contract.\\d+"); + + public LemmaAndModelMethodScriptMacro() { } + + @Override + public String getName() { + return "lemma-script-auto-macro"; + } + + @Override + public String getCategory() { + return null; + } + + @Override + public String getDescription() { + return "Apply scripts in lemmas and model methods"; + } + + @Override + public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { + // only applicable on the root of the proof + // todo change this to allow for subproofs of lemmas and model methods + if(!goals.stream().allMatch(g -> g.node() == proof.root())) + return false; + + String name = proof.name().toString(); + Matcher m = NAME_PATTERN.matcher(name); + return m.matches(); + } + + @Override + public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { + String name = proof.name().toString(); + Matcher m = NAME_PATTERN.matcher(name); + if (!m.matches()) + throw new RuntimeException("This macro was not applicable"); + + Services services = proof.getServices(); + String lemmaName = m.group(1); + Function function = services.getNamespaces().functions().lookup(lemmaName); + if(function instanceof ProgramMethod pm && pm.isModel()) { + if(pm.isLemma()) { + return applyToLemma(uic, goals.head(), pm); + } else { + return applyToModel(uic, goals.head(), pm); + } + } else { + return new ProofMacroFinishedInfo(this, goals); + } + } + + private ProofMacroFinishedInfo applyToLemma(UserInterfaceControl uic, Goal root, ProgramMethod pm) { + return new ProofMacroFinishedInfo(this, ImmutableList.of(root)); + } + + private ProofMacroFinishedInfo applyToModel(UserInterfaceControl uic, Goal root, ProgramMethod pm) { + TextualJMLMethodDecl methodDecl = (TextualJMLMethodDecl) pm.getMethodDeclaration().getAttachedJml().stream(). + filter(TextualJMLMethodDecl.class::isInstance).findAny().get(); + JmlParser.Method_declarationContext ctx = + (JmlParser.Method_declarationContext) methodDecl.getMethodDefinition(); + + CutTree cutTree = extractCutTree(ctx.method_body); + + // replicate cutTree and apply proofs on the leaves. + + return new ProofMacroFinishedInfo(this, ImmutableList.of(root)); + } + + private CutTree extractCutTree(ParserRuleContext ctx) { + JmlParser.Mbody_statementContext stmCtx; + List localHistory; + + switch(ctx) { + case JmlParser.Mbody_blockContext block -> { + localHistory = block.children.stream(). + filter(x -> x instanceof JmlParser.Mbody_varContext + || x instanceof JmlParser.Assert_statementContext). + toList(); + stmCtx = block.mbody_statement(); + } + case JmlParser.Mbody_statementContext stm -> { + localHistory = List.of(); + stmCtx = stm; + } + default -> throw new IllegalStateException("Unexpected value: " + ctx); + } + + if(stmCtx instanceof JmlParser.Mbody_ifContext ifCtx) { + var cond = ifCtx.getChild(ParserRuleContext.class, 0); + var thenBr = ifCtx.getChild(ParserRuleContext.class, 1); + var elseBr = ifCtx.getChild(ParserRuleContext.class, 2); + + CutTree thenTree = extractCutTree(thenBr); + CutTree elseTree = extractCutTree(elseBr); + + if (thenTree.hasAssertions() || elseTree.hasAssertions()) { + return new CutTree(localHistory, cond, thenTree, elseTree); + } + } + return new CutTree(localHistory); + } + + record CutTree(List localHistory, ParserRuleContext cond, CutTree thenTree, CutTree elseTree) { + + public CutTree(List localHistory) { + this(localHistory, null, null, null); + } + + public boolean hasAssertions() { + return thenTree != null && thenTree.hasAssertions() || elseTree != null && elseTree.hasAssertions() || + localHistory.stream().anyMatch(x -> x instanceof JmlParser.Assert_statementContext); + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java index f27bd5e89c1..43e2f7104d9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java @@ -40,6 +40,7 @@ public class ScriptAwareMacro extends SequentialProofMacro { private final ProofMacro autoMacro = new SymbolicExecutionOnlyMacro(); + private final ProofMacro lemmaScriptMacro = new LemmaAndModelMethodScriptMacro(); private final ApplyScriptsMacro applyMacro = new ApplyScriptsMacro(new TryCloseMacro()); @Override @@ -64,6 +65,6 @@ public String getDescription() { @Override protected ProofMacro[] createProofMacroArray() { - return new ProofMacro[] { autoMacro, applyMacro }; + return new ProofMacro[] { autoMacro, lemmaScriptMacro, applyMacro }; } } From d1aae0b2615da7d0a8e8380db7e15f658e5a9fd3 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 16 Aug 2026 20:10:22 +0200 Subject: [PATCH 4/7] towards models and lemma proof scripts --- .../ilkd/key/macros/ApplyScriptsMacro.java | 284 +----------------- .../LemmaAndModelMethodScriptMacro.java | 165 +++++++++- 2 files changed, 157 insertions(+), 292 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java index 9fd345eaf09..c9035d4c20e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java @@ -10,40 +10,25 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.java.JavaTools; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.SourceElement; import de.uka.ilkd.key.java.ast.statement.JmlAssert; -import de.uka.ilkd.key.java.ast.statement.MethodFrame; -import de.uka.ilkd.key.logic.DefaultVisitor; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.*; -import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.JmlAssertBuiltInRuleApp; import de.uka.ilkd.key.scripts.ProofScriptEngine; import de.uka.ilkd.key.scripts.ScriptCommandAst; -import de.uka.ilkd.key.scripts.ScriptException; -import de.uka.ilkd.key.scripts.TermWithHoles; -import de.uka.ilkd.key.speclang.njml.JmlLexer; -import de.uka.ilkd.key.speclang.njml.JmlParser; -import de.uka.ilkd.key.speclang.njml.JmlParser.ProofArgContext; -import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdCaseContext; -import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdContext; -import de.uka.ilkd.key.util.MiscTools; -import org.key_project.logic.Term; import org.key_project.logic.op.Modality; import org.key_project.prover.engine.ProverTaskListener; import org.key_project.prover.engine.TaskStartedInfo; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; -import org.key_project.util.java.StringUtil; import org.key_project.util.lookup.Property; -import org.key_project.util.parsing.Location; import org.antlr.v4.runtime.ParserRuleContext; import org.jspecify.annotations.NonNull; @@ -77,7 +62,7 @@ public class ApplyScriptsMacro extends AbstractProofMacro { private static final Logger LOGGER = LoggerFactory.getLogger(ApplyScriptsMacro.class); public static final Property> USER_DATA_JML_OBTAIN_VAR_MAP = - new Property<>("jml.obtainVarMap"); + JmlProofScriptSupport.USER_DATA_JML_OBTAIN_VAR_MAP; private final @Nullable ProofMacro fallBackMacro; @@ -107,51 +92,6 @@ public boolean canApplyTo(Proof proof, ImmutableList<@NonNull Goal> goals, || goals.exists(g -> getJmlAssert(g.node()) != null); } - /** - * A wrapper for a {@link JTerm} that contains obtain variables which need to be resolved - * before the term can be used in proof script execution. - *

- * Obtain variables are placeholders (represented as {@link LocationVariable}) that are - * bound to concrete values during script execution via {@code __obtain} commands. This - * record defers the resolution of these variables until the term is actually needed, - * ensuring proper sequencing where obtain variables must be bound before use. - *

- */ - record ObtainAwareTerm(JTerm term) { - /** - * Resolves all obtain variables in this term by replacing them with their bound - * values from the given obtain map. - * - * @param obtainMap a mapping from obtain variables ({@link LocationVariable}) to their - * bound values ({@link JFunction}); variables not present in this map will - * cause an error if they appear in the term - * @param services the proof services used for term factory operations - * @return a new {@link JTerm} with all obtain variables replaced by their resolved values - * @throws RuntimeException if the term contains an obtain variable that has not been - * bound yet (i.e., appears in the term before being obtained) - */ - JTerm resolve(Map obtainMap, Services services) { - OpReplacer pvr = new OpReplacer(obtainMap, services.getTermFactory()); - JTerm result = pvr.replace(term); - assertNoObtainVarsLeft(result, obtainMap); - return result; - } - - private void assertNoObtainVarsLeft(JTerm term, - Map obtainMap) { - var v = new DefaultVisitor() { - @Override - public void visit(Term visited) { - if (obtainMap.containsKey(term.op())) { - throw new RuntimeException( - "Use of obtain variable before it being obtained: " + term.op()); - } - } - }; - term.execPreOrder(v); - } - } - private static JmlAssert getJmlAssert(Node node) { if (node == null || node.parent() == null) { return null; @@ -171,36 +111,6 @@ private static JmlAssert getJmlAssert(Node node) { return null; } - private static @Nullable OpReplacer getUpdateReplacer(Goal goal) { - RuleApp ruleApp = goal.node().parent().getAppliedRuleApp(); - Term appliedOn = ruleApp.posInOccurrence().subTerm(); - if (appliedOn.op() instanceof UpdateApplication) { - var update = UpdateApplication.getUpdate((JTerm) appliedOn); - Map updates = new LinkedHashMap<>(); - Services services = goal.proof().getServices(); - collectUpdates(update, updates, services); - return new OpReplacer(updates, services.getTermFactory()); - } - return null; - } - - private static void collectUpdates(JTerm update, Map updates, Services services) { - switch (update.op()) { - case ElementaryUpdate eu -> - updates.put(services.getTermBuilder().var((ProgramVariable) eu.lhs()), - update.sub(0)); - - case UpdateJunctor uj -> { - collectUpdates(update.sub(0), updates, services); - collectUpdates(update.sub(1), updates, services); - } - - default -> - throw new IllegalStateException( - "Unexpected update operation: " + update.op().getClass()); - } - } - private static JavaBlock getJavaBlock(Goal goal) { RuleApp ruleApp = goal.node().parent().getAppliedRuleApp(); JTerm appliedOn = (JTerm) ruleApp.posInOccurrence().subTerm(); @@ -232,25 +142,15 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, KeyAst.JMLProofScript proofScript = jmlAssert.getAssertionProof(); Map termMap = - getTermMap(jmlAssert, getJavaBlock(goal), proof.getServices()); + JmlProofScriptSupport.getTermMapForAssert(jmlAssert, getJavaBlock(goal), proof.getServices()); // We heavily rely on that variables have been computed before, otherwise this will // raise an NPE. Map obtainMap = - makeObtainVarMap(jmlAssert.collectVariablesInProof(null)); - OpReplacer updateReplacer = getUpdateReplacer(goal); + JmlProofScriptSupport.makeObtainVarMap(jmlAssert.collectVariablesInProof(null)); + OpReplacer updateReplacer = JmlProofScriptSupport.getUpdateReplacer(goal); List renderedProof = - renderProof(proofScript, termMap, updateReplacer, proof.getServices()); - ProofScriptEngine pse = new ProofScriptEngine(proof); - pse.setInitiallySelectedGoal(goal); - pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap); - pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class, - oat -> oat.resolve(obtainMap, goal.proof().getServices())); - // TODO: Perhaps have holes also in JML? - pse.getStateMap().getValueInjector().addConverter(TermWithHoles.class, - ObtainAwareTerm.class, - oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices()))); - pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class, - oat -> Boolean.parseBoolean(oat.term.toString())); + JmlProofScriptSupport.renderProof(proofScript, termMap, updateReplacer, proof.getServices()); + ProofScriptEngine pse = JmlProofScriptSupport.prepareEngine(proof, goal, obtainMap); LOGGER.debug("---- Script"); LOGGER.debug(renderedProof.stream() .map(ScriptCommandAst::asCommandLine) @@ -274,175 +174,5 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, return new ProofMacroFinishedInfo(this, proof); } - - private Map getTermMap(JmlAssert jmlAssert, JavaBlock javaBlock, - Services services) { - SpecificationRepository.@Nullable JmlStatementSpec jmlspec = - services.getSpecificationRepository().getStatementSpec(jmlAssert); - if (jmlspec == null) { - throw new IllegalStateException( - "No specification found for JML assert statement at " + jmlAssert); - } - ImmutableList terms = ImmutableList.of(); - for (int i = jmlspec.terms().size() - 1; i >= 1; i--) { - terms = terms.prepend(correctSelfVar(i, javaBlock, jmlspec, services)); - } - ImmutableList jmlExprs = jmlAssert.collectTerms().tail(); - Map result = new IdentityHashMap<>(); - assert terms.size() == jmlExprs.size(); - for (int i = 0; i < terms.size(); i++) { - result.put(jmlExprs.get(i), terms.get(i)); - } - return result; - } - - /** - * For some reason, the self variable in the spec is not the same as the self variable and needs - * to - * be corrected. - */ - private JTerm correctSelfVar(int index, JavaBlock javaBlock, - SpecificationRepository.JmlStatementSpec spec, Services services) { - final MethodFrame frame = JavaTools.getInnermostMethodFrame(javaBlock, services); - final JTerm self = MiscTools.getSelfTerm(frame, services); - return spec.getTerm(services, self, index); - - } - - private Map makeObtainVarMap( - ImmutableList locationVariables) { - HashMap result = new LinkedHashMap<>(); - for (LocationVariable lv : locationVariables) { - result.put(lv, null); - } - return result; - } - - private static List renderProof(KeyAst.JMLProofScript script, - Map termMap, @Nullable OpReplacer update, Services services) - throws ScriptException { - List result = new ArrayList<>(); - // Push current settings onto the settings stack - result.add(new ScriptCommandAst("set", Map.of("stack", "push"), List.of())); - // Prepare by resolving the update - result.add(new ScriptCommandAst("oss", Map.of("recentOnly", true), List.of())); - for (ProofCmdContext proofCmdContext : script.ctx.proofCmd()) { - result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); - } - // Pop settings stack to restore old settings - result.add(new ScriptCommandAst("set", Map.of("stack", "pop"), List.of())); - return result; - } - - private static List renderProofCmd(ProofCmdContext ctx, - Map termMap, - @Nullable OpReplacer update, Services services) throws ScriptException { - List result = new ArrayList<>(); - - // Push the current branch context - result.add(new ScriptCommandAst("branches", Map.of(), List.of("push"))); - - // Compose the command itself - if (ctx.obtain != null) { - ScriptCommandAst command = renderObtainCommand(ctx, termMap, update, services); - result.add(command); - } else { - ScriptCommandAst command = renderRegularCommand(ctx, termMap, update, services); - result.add(command); - } - - // handle followup proofCmd if present - JmlParser.ProofCmdSuffixContext suffix = ctx.proofCmdSuffix(); - if (suffix != null) { - if (!suffix.proofCmd().isEmpty()) { - result.add(new ScriptCommandAst("branches", Map.of(), List.of("single"))); - for (ProofCmdContext proofCmdContext : suffix.proofCmd()) { - result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); - } - } - - // handle proofCmdCases if present - for (ProofCmdCaseContext pcase : suffix.proofCmdCase()) { - String label = StringUtil.stripQuotes(pcase.label.getText()); - result.add(new ScriptCommandAst("branches", Map.of("branch", label), - List.of("select"))); - for (ProofCmdContext proofCmdContext : pcase.proofCmd()) { - result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); - } - } - } - - // Pop the branch stack - result.add(new ScriptCommandAst("branches", Map.of(), List.of("pop"))); - - return result; - } - - private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, - Map termMap, - @Nullable OpReplacer update, Services services) throws ScriptException { - Map named = new HashMap<>(); - - String argName = switch (ctx.obtKind.getType()) { - case JmlLexer.SUCH_THAT -> "such_that"; - case JmlLexer.EQUAL_SINGLE -> "equals"; - case JmlLexer.FROM_GOAL -> "from_goal"; - default -> throw new ScriptException("Unknown obtain kind: " + ctx.obtKind.getText()); - }; - - named.put("var", ctx.var.getText()); - - if (ctx.expression() == null) { - named.put(argName, true); - } else { - JmlParser.ExpressionContext exp = ctx.expression(); - Object value; - if (isStringLiteral(exp)) { - value = StringUtil.stripQuotes(exp.getText()); - } else { - value = termMap.get(exp); - if (update != null) { - // Wrap in update application if an update is present - value = update.replace((JTerm) value); - } - } - named.put(argName, value); - } - - return new ScriptCommandAst("__obtain", named, List.of(), Location.fromToken(ctx.start)); - } - - private static @NonNull ScriptCommandAst renderRegularCommand(ProofCmdContext ctx, - Map termMap, @Nullable OpReplacer update, Services services) { - Map named = new HashMap<>(); - List positional = new ArrayList<>(); - for (ProofArgContext argContext : ctx.proofArg()) { - Object value; - JmlParser.ExpressionContext exp = argContext.expression(); - if (isStringLiteral(exp)) { - value = StringUtil.stripQuotes(exp.getText()); - } else { - value = termMap.get(exp); - if (update != null) { - // Wrap in update application if an update is present - value = update.replace((JTerm) value); - } - } - if (value instanceof JTerm term) { - value = new ObtainAwareTerm(term); - } - if (argContext.argLabel != null) { - named.put(argContext.argLabel.getText(), value); - } else { - positional.add(value); - } - } - return new ScriptCommandAst(ctx.cmd.getText(), named, positional, - Location.fromToken(ctx.start)); - } - - - private static boolean isStringLiteral(JmlParser.ExpressionContext ctx) { - return ctx.start == ctx.stop && ctx.start.getType() == JmlParser.STRING_LITERAL; - } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java index 104ec87b0d8..dc97bea7f51 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java @@ -1,23 +1,52 @@ package de.uka.ilkd.key.macros; +import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.UserInterfaceControl; +import de.uka.ilkd.key.java.JavaTools; import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.nparser.KeyAst; 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.rule.JmlAssertBuiltInRuleApp; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptCommandAst; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLemmaDecl; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.njml.JmlIO; import de.uka.ilkd.key.speclang.njml.JmlParser; import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.tree.ParseTree; +import org.key_project.logic.Name; import org.key_project.logic.op.Function; +import org.key_project.logic.op.Modality; +import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; +import java.util.ArrayList; import java.util.List; +import java.util.Map; import java.util.regex.Matcher; import java.util.regex.Pattern; +import de.uka.ilkd.key.proof.OpReplacer; +import org.key_project.util.collection.Pair; + public class LemmaAndModelMethodScriptMacro extends AbstractProofMacro { private static final String ID = "[A-Za-z_$0-9.]+"; @@ -41,6 +70,65 @@ public String getDescription() { return "Apply scripts in lemmas and model methods"; } + record CutTree(List localHistory, JmlParser.ExpressionContext cond, CutTree thenTree, CutTree elseTree) { + + private static final Name CUT_TACLET_NAME = new Name("cut"); + + public CutTree(List localHistory) { + this(localHistory, null, null, null); + } + + public boolean hasAssertions() { + return thenTree != null && thenTree.hasAssertions() || elseTree != null && elseTree.hasAssertions() || + localHistory.stream().anyMatch(x -> x instanceof JmlParser.Assert_statementContext); + } + + public void splitAndExecuteScripts(UserInterfaceControl uic, Goal goal) { + if(!hasAssertions()) { + return; + } + List collectedHistory = new ArrayList<>(); + for (ParseTree parseTree : localHistory) { + switch(parseTree) { + case JmlParser.Mbody_varContext varCtx -> collectedHistory.add(varCtx); + case JmlParser.Assert_statementContext assertCtx -> { + Pair goals = doCut(collectedHistory, goal, assertCtx.expression()); + executeScriptsOnAssertion(uic, goals.second, assertCtx.assertionProof()); + goal = goals.first; + } + default -> throw new IllegalStateException("Unexpected value: " + parseTree); + } + } + if(cond != null) { + Pair goals = doCut(collectedHistory, goal, cond); + thenTree.splitAndExecuteScripts(uic, goals.first); + elseTree.splitAndExecuteScripts(uic, goals.second); + } + } + + private Pair doCut(List assignments, Goal goal, JmlParser.ExpressionContext expression) { + if(!assignments.isEmpty()) { + throw new UnsupportedOperationException("Assignments are not yet supported here"); + } + + Taclet cut = goal.proof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(CUT_TACLET_NAME); + TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut); + SchemaVariable sv = app.uninstantiatedVars().iterator().next(); + + // todo ... + JTerm term = new JmlIO(goal.proof().getServices()).translateTerm(expression); + JTerm formula = goal.proof().getServices().getTermBuilder().convertToFormula(term); + + app = app.addCheckedInstantiation(sv, formula, goal.proof().getServices(), true); + ImmutableList goals = goal.apply(app); + assert goals.size() == 2; + return new Pair<>(goals.get(0), goals.get(1)); + } + } + + + @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { // only applicable on the root of the proof @@ -70,27 +158,85 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, Imm return applyToModel(uic, goals.head(), pm); } } else { + // do nothing if this is not a lemma or model method, but return the goals unchanged return new ProofMacroFinishedInfo(this, goals); } } private ProofMacroFinishedInfo applyToLemma(UserInterfaceControl uic, Goal root, ProgramMethod pm) { + // Currently treat lemmas the same way: if an attached JML assert script is present + // at the current goal, execute it using the shared support. + TextualJMLLemmaDecl methodDecl = (TextualJMLLemmaDecl) pm.getMethodDeclaration().getAttachedJml().last(); + JmlParser.Lemma_declarationContext ctx = + (JmlParser.Lemma_declarationContext) methodDecl.getMethodDefinition(); + executeScriptsOnAssertion(uic, root, ctx.assertionProof()); return new ProofMacroFinishedInfo(this, ImmutableList.of(root)); } private ProofMacroFinishedInfo applyToModel(UserInterfaceControl uic, Goal root, ProgramMethod pm) { - TextualJMLMethodDecl methodDecl = (TextualJMLMethodDecl) pm.getMethodDeclaration().getAttachedJml().stream(). - filter(TextualJMLMethodDecl.class::isInstance).findAny().get(); + TextualJMLMethodDecl methodDecl = (TextualJMLMethodDecl) pm.getMethodDeclaration().getAttachedJml().head(); JmlParser.Method_declarationContext ctx = (JmlParser.Method_declarationContext) methodDecl.getMethodDefinition(); CutTree cutTree = extractCutTree(ctx.method_body); - // replicate cutTree and apply proofs on the leaves. + cutTree.splitAndExecuteScripts(uic, root); return new ProofMacroFinishedInfo(this, ImmutableList.of(root)); } + private static void executeScriptsOnAssertion(UserInterfaceControl uic, Goal goal, JmlParser.AssertionProofContext assertionProofContext) { + JmlAssert jmlAssert = getJmlAssert(goal.node()); + if (jmlAssert == null || jmlAssert.getAssertionProof() == null) { + return; + } + KeyAst.JMLProofScript proofScript = jmlAssert.getAssertionProof(); + JavaBlock javaBlock = getJavaBlock(goal); + Map termMap = + JmlProofScriptSupport.getTermMapForAssert(jmlAssert, javaBlock, goal.proof().getServices()); + Map obtainMap = + JmlProofScriptSupport.makeObtainVarMap(jmlAssert.collectVariablesInProof(null)); + OpReplacer updateReplacer = JmlProofScriptSupport.getUpdateReplacer(goal); + try { + List rendered = JmlProofScriptSupport.renderProof(proofScript, termMap, updateReplacer, goal.proof().getServices()); + ProofScriptEngine pse = JmlProofScriptSupport.prepareEngine(goal.proof(), goal, obtainMap); + pse.execute((AbstractUserInterfaceControl) uic, rendered); + } catch (de.uka.ilkd.key.scripts.ScriptException e) { + throw new RuntimeException(e); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + } + + private static JmlAssert getJmlAssert(Node node) { + if (node == null || node.parent() == null) { + return null; + } + RuleApp ruleApp = node.parent().getAppliedRuleApp(); + if (ruleApp instanceof JmlAssertBuiltInRuleApp) { + JTerm target = (JTerm) ruleApp.posInOccurrence().subTerm(); + if (target.op() instanceof UpdateApplication) { + target = UpdateApplication.getTarget(target); + } + final SourceElement activeStatement = JavaTools.getActiveStatement(target.javaBlock()); + if (activeStatement instanceof JmlAssert jmlAssert + && jmlAssert.getAssertionProof() != null) { + return jmlAssert; + } + } + return null; + } + + private static JavaBlock getJavaBlock(Goal goal) { + RuleApp ruleApp = goal.node().parent().getAppliedRuleApp(); + JTerm appliedOn = (JTerm) ruleApp.posInOccurrence().subTerm(); + if (appliedOn.op() instanceof UpdateApplication) { + appliedOn = UpdateApplication.getTarget(appliedOn); + } + assert appliedOn.op() instanceof Modality; + return appliedOn.javaBlock(); + } + private CutTree extractCutTree(ParserRuleContext ctx) { JmlParser.Mbody_statementContext stmCtx; List localHistory; @@ -111,7 +257,7 @@ private CutTree extractCutTree(ParserRuleContext ctx) { } if(stmCtx instanceof JmlParser.Mbody_ifContext ifCtx) { - var cond = ifCtx.getChild(ParserRuleContext.class, 0); + var cond = ifCtx.getChild(JmlParser.ExpressionContext.class, 0); var thenBr = ifCtx.getChild(ParserRuleContext.class, 1); var elseBr = ifCtx.getChild(ParserRuleContext.class, 2); @@ -125,15 +271,4 @@ private CutTree extractCutTree(ParserRuleContext ctx) { return new CutTree(localHistory); } - record CutTree(List localHistory, ParserRuleContext cond, CutTree thenTree, CutTree elseTree) { - - public CutTree(List localHistory) { - this(localHistory, null, null, null); - } - - public boolean hasAssertions() { - return thenTree != null && thenTree.hasAssertions() || elseTree != null && elseTree.hasAssertions() || - localHistory.stream().anyMatch(x -> x instanceof JmlParser.Assert_statementContext); - } - } } From bc45c57fc662aa31ff9aa90d38aeba2e38350b42 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 17 Aug 2026 12:03:00 +0200 Subject: [PATCH 5/7] towards advanced proof scripts. The first scripts work. --- .../key/macros/JmlProofScriptSupport.java | 356 ++++++++++++++++++ .../key/macros/LemmaMethodScriptMacro.java | 120 ++++++ ...Macro.java => ModelMethodScriptMacro.java} | 60 ++- .../uka/ilkd/key/macros/ScriptAwareMacro.java | 5 +- .../java/de/uka/ilkd/key/nparser/KeyAst.java | 2 +- .../java/de/uka/ilkd/key/proof/NodeInfo.java | 2 +- .../uka/ilkd/key/scripts/BranchesCommand.java | 2 +- .../de/uka/ilkd/key/scripts/CutCommand.java | 5 +- .../de/uka/ilkd/key/scripts/EngineState.java | 15 + .../ilkd/key/scripts/InstantiateCommand.java | 6 + .../uka/ilkd/key/scripts/ObtainCommand.java | 100 ++++- .../key/scripts/OneStepSimplifierCommand.java | 4 + .../uka/ilkd/key/scripts/UseLemmaCommand.java | 157 ++++++++ .../de/uka/ilkd/key/speclang/njml/JmlIO.java | 9 +- ...de.uka.ilkd.key.scripts.ProofScriptCommand | 3 +- 15 files changed, 805 insertions(+), 41 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java rename key.core/src/main/java/de/uka/ilkd/key/macros/{LemmaAndModelMethodScriptMacro.java => ModelMethodScriptMacro.java} (89%) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java b/key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java new file mode 100644 index 00000000000..82d71cb4219 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java @@ -0,0 +1,356 @@ +/* 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.macros; + +import java.util.*; + +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.java.ast.statement.MethodFrame; +import de.uka.ilkd.key.logic.DefaultVisitor; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.OpReplacer; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.mgt.SpecificationRepository; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptCommandAst; +import de.uka.ilkd.key.scripts.ScriptException; +import de.uka.ilkd.key.scripts.TermWithHoles; +import de.uka.ilkd.key.speclang.njml.JmlIO; +import de.uka.ilkd.key.speclang.njml.JmlLexer; +import de.uka.ilkd.key.speclang.njml.JmlParser; +import de.uka.ilkd.key.speclang.njml.JmlParser.ProofArgContext; +import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdCaseContext; +import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdContext; +import de.uka.ilkd.key.speclang.njml.SpecMathMode; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Term; +import org.key_project.prover.rules.RuleApp; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.java.StringUtil; +import org.key_project.util.lookup.Property; +import org.key_project.util.parsing.Location; + +import org.antlr.v4.runtime.ParserRuleContext; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +/** + * Utilities for rendering and executing JML proof scripts across different macros. + * This class centralizes common functionality so macros like ApplyScriptsMacro and + * LemmaAndModelMethodScriptMacro can share logic without duplication. + */ +public final class JmlProofScriptSupport { + + private JmlProofScriptSupport() { + // utility + } + + public static final Property> USER_DATA_JML_OBTAIN_VAR_MAP = + new Property<>("jml.obtainVarMap"); + + /** + * Wrapper around a JTerm that defers resolution of obtain variables until use. + */ + public record ObtainAwareTerm(JTerm term) { + JTerm resolve(Map obtainMap, Services services) { + OpReplacer pvr = new OpReplacer(obtainMap, services.getTermFactory()); + JTerm result = pvr.replace(term); + assertNoObtainVarsLeft(result, obtainMap); + return result; + } + + private void assertNoObtainVarsLeft(JTerm term, + Map obtainMap) { + var v = new DefaultVisitor() { + @Override + public void visit(Term visited) { + if (obtainMap.containsKey(term.op())) { + throw new RuntimeException( + "Use of obtain variable before it being obtained: " + term.op()); + } + } + }; + term.execPreOrder(v); + } + } + + /** + * Create an obtain variable map with all provided variables initialized to null. + */ + public static Map makeObtainVarMap( + ImmutableList locationVariables) { + HashMap result = new LinkedHashMap<>(); + for (LocationVariable lv : locationVariables) { + result.put(lv, null); + } + return result; + } + + /** + * Creates an OpReplacer that applies the update found on the goal's applied rule app, if any. + */ + public static OpReplacer getUpdateReplacer(Goal goal) { + Node parent = goal.node().parent(); + if(parent == null) { + // we can also operate on the root ... + return null; + } + RuleApp ruleApp = parent.getAppliedRuleApp(); + org.key_project.logic.Term appliedOn = ruleApp.posInOccurrence().subTerm(); + if (appliedOn.op() instanceof UpdateApplication) { + var update = UpdateApplication.getUpdate((JTerm) appliedOn); + Map updates = new LinkedHashMap<>(); + Services services = goal.proof().getServices(); + collectUpdates(update, updates, services); + return new OpReplacer(updates, services.getTermFactory()); + } + return null; + } + + private static void collectUpdates(JTerm update, Map updates, Services services) { + switch (update.op()) { + case ElementaryUpdate eu -> + updates.put(services.getTermBuilder().var((ProgramVariable) eu.lhs()), + update.sub(0)); + + case UpdateJunctor uj -> { + collectUpdates(update.sub(0), updates, services); + collectUpdates(update.sub(1), updates, services); + } + + default -> + throw new IllegalStateException( + "Unexpected update operation: " + update.op().getClass()); + } + } + + /** + * Render a JML proof script into a list of script command ASTs. + */ + public static List renderProof(KeyAst.JMLProofScript script, + Map termMap, @Nullable OpReplacer update, Services services) + throws ScriptException { + List result = new ArrayList<>(); + // Push current settings onto the settings stack + result.add(new ScriptCommandAst("set", Map.of("stack", "push"), List.of())); + // Prepare by resolving the update + result.add(new ScriptCommandAst("oss", Map.of("recentOnly", true), List.of())); + for (ProofCmdContext proofCmdContext : script.ctx.proofCmd()) { + result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); + } + // Pop settings stack to restore old settings + result.add(new ScriptCommandAst("set", Map.of("stack", "pop"), List.of())); + return result; + } + + private static List renderProofCmd(ProofCmdContext ctx, + Map termMap, + @Nullable OpReplacer update, Services services) throws ScriptException { + List result = new ArrayList<>(); + + // Push the current branch context + result.add(new ScriptCommandAst("branches", Map.of(), List.of("push"))); + + // Compose the command itself + if (ctx.obtain != null) { + ScriptCommandAst command = renderObtainCommand(ctx, termMap, update, services); + result.add(command); + } else { + ScriptCommandAst command = renderRegularCommand(ctx, termMap, update, services); + result.add(command); + } + + // handle followup proofCmd if present + JmlParser.ProofCmdSuffixContext suffix = ctx.proofCmdSuffix(); + if (suffix != null) { + if (!suffix.proofCmd().isEmpty()) { + result.add(new ScriptCommandAst("branches", Map.of(), List.of("single"))); + for (ProofCmdContext proofCmdContext : suffix.proofCmd()) { + result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); + } + } + + // handle proofCmdCases if present + for (ProofCmdCaseContext pcase : suffix.proofCmdCase()) { + String label = StringUtil.stripQuotes(pcase.label.getText()); + result.add(new ScriptCommandAst("branches", Map.of("branch", label), + List.of("select"))); + for (ProofCmdContext proofCmdContext : pcase.proofCmd()) { + result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); + } + } + } + + // Pop the branch stack + result.add(new ScriptCommandAst("branches", Map.of(), List.of("pop"))); + + return result; + } + + private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, + Map termMap, + @Nullable OpReplacer update, Services services) throws ScriptException { + Map named = new HashMap<>(); + + String argName = switch (ctx.obtKind.getType()) { + case JmlLexer.SUCH_THAT -> "such_that"; + case JmlLexer.EQUAL_SINGLE -> "equals"; + case JmlLexer.FROM_GOAL -> "from_goal"; + default -> throw new ScriptException("Unknown obtain kind: " + ctx.obtKind.getText()); + }; + + named.put("var", ctx.var.getText()); + + if (ctx.expression() == null) { + named.put(argName, true); + } else { + JmlParser.ExpressionContext exp = ctx.expression(); + Object value; + if (isStringLiteral(exp)) { + value = StringUtil.stripQuotes(exp.getText()); + } else { + value = termMap.get(exp); + if (update != null) { + // Wrap in update application if an update is present + value = update.replace((JTerm) value); + } + } + if (value instanceof JTerm term) { + value = new ObtainAwareTerm(term); + } + named.put(argName, value); + } + + return new ScriptCommandAst("__obtain", named, List.of(), Location.fromToken(ctx.start)); + } + + private static @NonNull ScriptCommandAst renderRegularCommand(ProofCmdContext ctx, + Map termMap, @Nullable OpReplacer update, Services services) { + Map named = new HashMap<>(); + List positional = new ArrayList<>(); + for (ProofArgContext argContext : ctx.proofArg()) { + Object value; + JmlParser.ExpressionContext exp = argContext.expression(); + if (isStringLiteral(exp)) { + value = StringUtil.stripQuotes(exp.getText()); + } else { + value = termMap.get(exp); + if (update != null) { + // Wrap in update application if an update is present + value = update.replace((JTerm) value); + } + } + if (value instanceof JTerm term) { + value = new ObtainAwareTerm(term); + } + if (argContext.argLabel != null) { + named.put(argContext.argLabel.getText(), value); + } else { + positional.add(value); + } + } + return new ScriptCommandAst(ctx.cmd.getText(), named, positional, + Location.fromToken(ctx.start)); + } + + private static boolean isStringLiteral(JmlParser.ExpressionContext ctx) { + return ctx.start == ctx.stop && ctx.start.getType() == JmlParser.STRING_LITERAL; + } + + /** + * Build a map from JML expression contexts to corresponding JTerms for a JML assert. + */ + public static Map getTermMapForAssert(JmlAssert jmlAssert, + JavaBlock javaBlock, Services services) { + SpecificationRepository.@org.jspecify.annotations.Nullable JmlStatementSpec jmlspec = + services.getSpecificationRepository().getStatementSpec(jmlAssert); + if (jmlspec == null) { + throw new IllegalStateException( + "No specification found for JML assert statement at " + jmlAssert); + } + ImmutableList terms = ImmutableList.of(); + for (int i = jmlspec.terms().size() - 1; i >= 1; i--) { + terms = terms.prepend(correctSelfVar(i, javaBlock, jmlspec, services)); + } + ImmutableList jmlExprs = jmlAssert.collectTerms().tail(); + Map result = new IdentityHashMap<>(); + assert terms.size() == jmlExprs.size(); + for (int i = 0; i < terms.size(); i++) { + result.put(jmlExprs.get(i), terms.get(i)); + } + return result; + } + + private static JTerm correctSelfVar(int index, JavaBlock javaBlock, + SpecificationRepository.JmlStatementSpec spec, Services services) { + final MethodFrame frame = JavaTools.getInnermostMethodFrame(javaBlock, services); + final JTerm self = MiscTools.getSelfTerm(frame, services); + return spec.getTerm(services, self, index); + } + + /** + * Prepare a ProofScriptEngine with the standard obtain-variable converters and initial state. + */ + public static ProofScriptEngine prepareEngine(Proof proof, Goal initiallySelected, + Map obtainMap) { + ProofScriptEngine pse = new ProofScriptEngine(proof); + pse.setInitiallySelectedGoal(initiallySelected); + pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap); + pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class, + oat -> oat.resolve(obtainMap, initiallySelected.proof().getServices())); + // TODO: Perhaps have holes also in JML? + pse.getStateMap().getValueInjector().addConverter(TermWithHoles.class, + ObtainAwareTerm.class, + oat -> new TermWithHoles( + oat.resolve(obtainMap, initiallySelected.proof().getServices()))); + pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class, + oat -> Boolean.parseBoolean(oat.term.toString())); + return pse; + } + + + public static JmlIO prepareJmlIO(Services services, ProgramMethod pm) { + JmlIO io = new JmlIO(services); + if(!pm.isStatic()) { + io.selfVar((LocationVariable) services.getNamespaces().programVariables().lookup("self")); + } + io.classType(pm.getContainerType()); + // FIXME: Make this respect the right math mode (but this is not soundess-critical) + io.specMathMode(SpecMathMode.BIGINT); + // check if this lookup is necessary at all ... + ImmutableList instParams = pm.collectParameters().map(param -> (LocationVariable)services.getNamespaces().programVariables().lookup(param.name())); + io.parameters(instParams); + return io; + } + + public static Map createTermMap( + JmlParser.@Nullable ExpressionContext assertedCond, + KeyAst.JMLProofScript script, + List assignments, + ProgramMethod pm, + JmlIO io, + Services services) { + ImmutableList obtainedVars = script.getObtainedProgramVars(io); + io.parameters(io.getParamVars().prepend(obtainedVars)); + ImmutableList collectedTerms = script.collectTerms(); + if(assertedCond != null) { + collectedTerms = collectedTerms.prepend(assertedCond); + } + Map termMap = new IdentityHashMap<>(); + for (JmlParser.ExpressionContext ectx : collectedTerms) { + JTerm term = io.translateTerm(ectx); + termMap.put(ectx, term); + } + return termMap; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java new file mode 100644 index 00000000000..c76ce879efb --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java @@ -0,0 +1,120 @@ +package de.uka.ilkd.key.macros; + +import de.uka.ilkd.key.control.AbstractUserInterfaceControl; +import de.uka.ilkd.key.control.UserInterfaceControl; +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.OpReplacer; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import de.uka.ilkd.key.rule.JmlAssertBuiltInRuleApp; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptCommandAst; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLemmaDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.njml.JmlIO; +import de.uka.ilkd.key.speclang.njml.JmlParser; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.tree.ParseTree; +import org.key_project.logic.Name; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Modality; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.engine.TaskStartedInfo; +import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.Pair; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import java.util.stream.Collectors; + +public class LemmaMethodScriptMacro extends AbstractProofMacro { + + private static final Logger LOGGER = LoggerFactory.getLogger(LemmaMethodScriptMacro.class); + + public static final String ID = "[A-Za-z_$0-9.]+"; + public static final Pattern NAME_PATTERN = + Pattern.compile(ID + "\\[(" + ID + "::" + ID + ")\\(.*\\)\\].JML model_behavior operation contract.\\d+"); + + public LemmaMethodScriptMacro() { + } + + @Override + public String getName() { + return "lemma-script-auto-macro"; + } + + @Override + public String getCategory() { + return null; + } + + @Override + public String getDescription() { + return "Apply scripts in lemmas and model methods"; + } + + public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { + return ModelMethodScriptMacro.canApplyTo(proof, goals, posInOcc, true); + } + + @Override + public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { + ProgramMethod pm = ModelMethodScriptMacro.extractModelMethod(proof); + assert pm != null : "If canApplyTo gives true, this cannot happen"; + + Goal goal = goals.head(); + + // Currently treat lemmas the same way: if an attached JML assert script is present + // at the current goal, execute it using the shared support. + TextualJMLLemmaDecl methodDecl = + (TextualJMLLemmaDecl) pm.getMethodDeclaration().getAttachedJml().stream().filter(TextualJMLLemmaDecl.class::isInstance).findAny().get(); + JmlParser.Lemma_declarationContext ctx = + (JmlParser.Lemma_declarationContext) methodDecl.getMethodDefinition(); + + JmlIO io = JmlProofScriptSupport.prepareJmlIO(proof.getServices(), pm); + KeyAst.JMLProofScript proofScript = new KeyAst.JMLProofScript(ctx.assertionProof()); + Map termMap = JmlProofScriptSupport.createTermMap(null, proofScript, List.of(), pm, io, proof.getServices()); + + // We heavily rely on that variables have been computed before, otherwise this will + // raise an NPE. + Map obtainMap = + JmlProofScriptSupport.makeObtainVarMap(proofScript.getObtainedProgramVars(null)); + OpReplacer updateReplacer = JmlProofScriptSupport.getUpdateReplacer(goal); + List renderedProof = + JmlProofScriptSupport.renderProof(proofScript, termMap, updateReplacer, proof.getServices()); + ProofScriptEngine pse = JmlProofScriptSupport.prepareEngine(proof, goal, obtainMap); + LOGGER.debug("---- Script"); + LOGGER.debug(renderedProof.stream() + .map(ScriptCommandAst::asCommandLine) + .collect(Collectors.joining("\n"))); + LOGGER.debug("---- End Script"); + + pse.execute((AbstractUserInterfaceControl) uic, renderedProof); + + return new ProofMacroFinishedInfo(this, proof); + + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ModelMethodScriptMacro.java similarity index 89% rename from key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java rename to key.core/src/main/java/de/uka/ilkd/key/macros/ModelMethodScriptMacro.java index dc97bea7f51..3bc02947083 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaAndModelMethodScriptMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ModelMethodScriptMacro.java @@ -6,7 +6,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.SourceElement; import de.uka.ilkd.key.java.ast.statement.JmlAssert; -import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.op.JFunction; @@ -29,6 +28,7 @@ import de.uka.ilkd.key.speclang.njml.JmlParser; import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.tree.ParseTree; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.logic.op.Modality; @@ -47,17 +47,17 @@ import de.uka.ilkd.key.proof.OpReplacer; import org.key_project.util.collection.Pair; -public class LemmaAndModelMethodScriptMacro extends AbstractProofMacro { +public class ModelMethodScriptMacro extends AbstractProofMacro { private static final String ID = "[A-Za-z_$0-9.]+"; private static final Pattern NAME_PATTERN = Pattern.compile(ID+ "\\[(" + ID + "::" + ID + ")\\(.*\\)\\].JML model_behavior operation contract.\\d+"); - public LemmaAndModelMethodScriptMacro() { } + public ModelMethodScriptMacro() { } @Override public String getName() { - return "lemma-script-auto-macro"; + return "model-method-script-auto-macro"; } @Override @@ -70,6 +70,48 @@ public String getDescription() { return "Apply scripts in lemmas and model methods"; } + @Override + public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { + return canApplyTo(proof, goals, posInOcc, false); + } + + /** + * shared code with {@link LemmaMethodScriptMacro} to determine if the macro + * can be applied to the given proof and goals. + */ + static boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc, boolean expectLemma) { + // only applicable on the root of the proof + // todo change this to allow for subproofs of lemmas and model methods + if (!goals.stream().allMatch(g -> g.node() == proof.root())) + return false; + + ProgramMethod pm = extractModelMethod(proof); + if (pm != null) { + return pm.isLemma() == expectLemma; + } + return false; + } + + /** + * shared code with {@link LemmaMethodScriptMacro} to extract the model method from the proof name + * @param proof proof object whose name is to be parsed + * @return null or the model method behind the proof obligation + */ + static @Nullable ProgramMethod extractModelMethod(Proof proof) { + String name = proof.name().toString(); + Matcher m = NAME_PATTERN.matcher(name); + if(!m.matches()) { + return null; + } + Services services = proof.getServices(); + String lemmaName = m.group(1); + Function function = services.getNamespaces().functions().lookup(lemmaName); + if (function instanceof ProgramMethod pm && pm.isModel()) { + return pm; + } + return null; + } + record CutTree(List localHistory, JmlParser.ExpressionContext cond, CutTree thenTree, CutTree elseTree) { private static final Name CUT_TACLET_NAME = new Name("cut"); @@ -129,17 +171,7 @@ private Pair doCut(List assignments, Goa - @Override - public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - // only applicable on the root of the proof - // todo change this to allow for subproofs of lemmas and model methods - if(!goals.stream().allMatch(g -> g.node() == proof.root())) - return false; - String name = proof.name().toString(); - Matcher m = NAME_PATTERN.matcher(name); - return m.matches(); - } @Override public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java index 43e2f7104d9..dc70b839c75 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java @@ -40,7 +40,8 @@ public class ScriptAwareMacro extends SequentialProofMacro { private final ProofMacro autoMacro = new SymbolicExecutionOnlyMacro(); - private final ProofMacro lemmaScriptMacro = new LemmaAndModelMethodScriptMacro(); + private final ProofMacro lemmaScriptMacro = new LemmaMethodScriptMacro(); + private final ProofMacro modelMethodScriptMacro = new ModelMethodScriptMacro(); private final ApplyScriptsMacro applyMacro = new ApplyScriptsMacro(new TryCloseMacro()); @Override @@ -65,6 +66,6 @@ public String getDescription() { @Override protected ProofMacro[] createProofMacroArray() { - return new ProofMacro[] { autoMacro, lemmaScriptMacro, applyMacro }; + return new ProofMacro[] { autoMacro, lemmaScriptMacro, modelMethodScriptMacro, applyMacro }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 7d608d9c74f..af5e9043641 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -247,7 +247,7 @@ public Void visitProofCmd(JmlParser.ProofCmdContext ctx) { ProgramElementName name = new ProgramElementName(ctx.var.getText()); collectedVars = collectedVars.prepend(new LocationVariable(name, type, true)); } - return null; + return super.visitProofCmd(ctx); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java index 9bb8c690572..b3f880c299a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java @@ -88,7 +88,7 @@ public class NodeInfo { private String notes; /** Information about changes respective to the parent of this node. */ - private SequentChangeInfo sequentChangeInfo; + private @Nullable SequentChangeInfo sequentChangeInfo; public NodeInfo(Node node) { this.node = node; diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java index a9dc8f557f5..af328945eb9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java @@ -136,7 +136,7 @@ private Goal findGoalByName(Node root, String branch) throws ScriptException { int number = 1; while (it.hasNext()) { Node node = it.next(); - String label = node.getNodeInfo().getBranchLabel(); + String label = state.getLabel(node); if (label == null) { label = "Case " + number; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java index 7fb7396fc97..5847959a30e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java @@ -6,6 +6,7 @@ import java.util.List; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; @@ -16,6 +17,7 @@ import org.key_project.logic.op.sv.SchemaVariable; import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.key_project.util.collection.ImmutableList; /** * The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the @@ -55,7 +57,8 @@ static void execute(EngineState state, Parameters args) throws ScriptException { state.getProof().getServices().getTermBuilder().convertToFormula(args.formula); app = app.addCheckedInstantiation(sv, formula, state.getProof().getServices(), true); - state.getFirstOpenAutomaticGoal().apply(app); + ImmutableList goals = state.getFirstOpenAutomaticGoal().apply(app); + state.labelGoals(goals, "false", "true"); } @Documentation(category = "Fundamental", value = """ diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java index ef33be520e2..38a3b95d3e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java @@ -63,6 +63,8 @@ public class EngineState { private final PLookup userData = new PLookup(); + private final Map labelMap = new HashMap<>(); + /** * If set to true, outputs all commands to observers and console. Otherwise, only shows explicit * echo messages. @@ -377,4 +379,17 @@ ExprEvaluator getEvaluator() { public PLookup getUserData() { return userData; } + + public void labelGoals(ImmutableList goals, String... labels) { + if (goals.size() != labels.length) { + throw new IllegalStateException("The produced goals and their labels must habe same cardinality."); + } + for(int i = 0; i < labels.length; i++) { + labelMap.put(goals.get(i).node().serialNr(), labels[i]); + } + } + + public @Nullable String getLabel(Node node) { + return labelMap.getOrDefault(node.serialNr(), node.getNodeInfo().getBranchLabel()); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java index 361a73814f6..9bef446d077 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.scripts; +import java.util.List; import java.util.Objects; import de.uka.ilkd.key.java.Services; @@ -221,6 +222,11 @@ public String getName() { return "instantiate"; } + @Override + public List getAliases() { + return List.of("inst"); + } + @Documentation(category = "Fundamental", value = """ Instantiate a universally quantified formula (in the antecedent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java index dc7eb462f5c..909c107b143 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java @@ -89,8 +89,17 @@ public void execute(ScriptCommandAst ast) private JTerm executeFromGoal(LocationVariable var) throws ScriptException { Goal goal = state.getFirstOpenAutomaticGoal(); - // This works under the assumption that the last succedent formula is the "goal" formula. - SequentFormula sequentFormula = goal.node().sequent().succedent().getLast(); + // Pick the most recently changed succedent formula as the goal formula. + var sci = goal.node().getNodeInfo().getSequentChangeInfo().getSemisequentChangeInfo(false); + SequentFormula sequentFormula; + if (!sci.addedFormulas().isEmpty()) { + sequentFormula = sci.addedFormulas().get(0); + } else if (!sci.modifiedFormulas().isEmpty()) { + sequentFormula = sci.modifiedFormulas().get(0).newFormula(); + } else { + // Fallback to last succedent if no change info is available + sequentFormula = goal.node().sequent().succedent().getLast(); + } JTerm formula = (JTerm) sequentFormula.formula(); while (formula.op() instanceof UpdateApplication) { formula = formula.sub(1); @@ -124,26 +133,79 @@ private JTerm executeFromGoal(LocationVariable var) throws ScriptException { return app.instantiations().getInstantiation(sk); } - private SequentFormula identifySequentFormula(Node node) { - SemisequentChangeInfo changes = - node.getNodeInfo().getSequentChangeInfo().getSemisequentChangeInfo(false); - ImmutableList added = changes.addedFormulas(); - if (!added.isEmpty()) { - if (added.size() == 1) { - return added.get(0); - } - } else { - ImmutableList modified = changes.modifiedFormulas(); - if (modified.size() == 1) { - return modified.get(0).newFormula(); + private JTerm executeSuchThat(LocationVariable var, @Nullable JTerm suchThat) + throws ScriptException { + if (suchThat == null) { + throw new ScriptException("'such_that' must not be null"); + } + + Services services = state().getProof().getServices(); + var tb = services.getTermBuilder(); + + // 1) Replace program variable by a fresh logical variable in the condition. + String base = var.name().toString(); + String lvName = VariableNameProposer.DEFAULT.getNameProposal(base, services, null); + LogicVariable lv = new LogicVariable(new Name(lvName), var.sort()); + + JTerm progVarTerm = tb.var(var); + JTerm lvTerm = tb.var(lv); + JTerm condWithLv = OpReplacer.replace(progVarTerm, lvTerm, suchThat, + services.getTermFactory(), state().getProof()); + + // 2) Ensure it is a formula + JTerm asFormula = tb.convertToFormula(condWithLv); + + // 3) Existentially quantify and cut on it + JTerm exFormula = tb.ex(lv, asFormula); + + Taclet cut = state.getProof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(new Name("cut")); + TacletApp cutApp = NoPosTacletApp.createNoPosTacletApp(cut); + SchemaVariable cutSv = cutApp.uninstantiatedVars().iterator().next(); + cutApp = cutApp.addCheckedInstantiation(cutSv, exFormula, services, true); + ImmutableList goals = state.getFirstOpenAutomaticGoal().apply(cutApp); + + // 4) On the antecedent branch, apply exLeft to introduce a Skolem constant + TermComparisonWithHoles cmp = new TermComparisonWithHoles(exFormula); + Goal antecedentGoal = null; + SequentFormula targetSf = null; + for (Goal g : goals) { + var matches = cmp.findTopLevelMatchesInSequent(g.node().sequent()); + for (var m : matches) { + if (Boolean.TRUE.equals(m.first)) { + antecedentGoal = g; + targetSf = m.second; + break; + } } + if (antecedentGoal != null) break; } - throw new IllegalStateException( - "Multiple or no formulas modified or added in last step, cannot identify sequent formula to skolemize."); - } + if (antecedentGoal == null || targetSf == null) { + throw new ScriptException("Could not locate antecedent \\exists-formula after cut."); + } + + FindTaclet exLeft = (FindTaclet) state.getProof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(new Name("exLeft")); + PosInOccurrence pio = new PosInOccurrence(targetSf, PosInTerm.getTopLevel(), true); + MatchConditions mc = new MatchConditions(); + TacletApp exApp = PosTacletApp.createPosTacletApp(exLeft, mc, pio, services); + + var schemaVars = ImmutableSet.from(exLeft.collectSchemaVars()); + SchemaVariable u = getSV(schemaVars, "u"); + SchemaVariable b = getSV(schemaVars, "b"); + SchemaVariable sk = getSV(schemaVars, "sk"); + + exApp = exApp.addInstantiation(u, + services.getTermBuilder().tf().createTerm(targetSf.formula().boundVars().get(0)), + true, services); + exApp = exApp.addInstantiation(b, targetSf.formula().sub(0), true, services); + + String skName = VariableNameProposer.DEFAULT.getNameProposal(base, services, null); + exApp = exApp.createSkolemConstant(skName, sk, + targetSf.formula().boundVars().get(0).sort(), true, services); - private JTerm executeSuchThat(LocationVariable var, @Nullable JTerm suchThat) { - throw new UnsupportedOperationException("such_that not yet supported in obtain."); + antecedentGoal.apply(exApp); + return exApp.instantiations().getInstantiation(sk); } private JTerm executeEquals(LocationVariable var, @Nullable JTerm equals) diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java index 1aefe9ccb8c..74fd6f45dba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java @@ -41,6 +41,10 @@ public void execute(ScriptCommandAst command) throws ScriptException, Interrupte if (Boolean.TRUE.equals(arguments.recentOnly)) { SequentChangeInfo sci = goal.node().getNodeInfo().getSequentChangeInfo(); + if(sci == null) { + // sci is null for the root node ... + return; + } var ante = sci.addedFormulas(true) .prepend(sci.modifiedFormulas(true).map(FormulaChangeInfo::newFormula)); applyOSS(ante, goal, true); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java new file mode 100644 index 00000000000..d2adfb4ee9b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java @@ -0,0 +1,157 @@ +/* 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.scripts; + +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.scripts.meta.Argument; +import de.uka.ilkd.key.scripts.meta.Documentation; +import de.uka.ilkd.key.rule.FindTaclet; +import de.uka.ilkd.key.rule.PosTacletApp; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.key_project.logic.Name; +import org.key_project.logic.PosInTerm; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.Taclet; +import org.key_project.util.collection.ImmutableList; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.prover.proof.rulefilter.TacletFilter; + +import java.util.List; +import java.util.NoSuchElementException; + +/** + * The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the + * id "#2" + */ +public class UseLemmaCommand extends AbstractCommand { + private static final Name INTRO_TACLET_NAME = new Name("intro"); + + public UseLemmaCommand() { + super(Parameters.class); + } + + @Override + public String getName() { + return "use_lemma"; + } + + @Override + public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException { + var args = state().getValueInjector().inject(new Parameters(), arguments); + execute(state(), args); + } + + static void execute(EngineState state, Parameters args) throws ScriptException { + de.uka.ilkd.key.rule.Taclet intro = state.getProof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(INTRO_TACLET_NAME); + TacletApp app = NoPosTacletApp.createNoPosTacletApp(intro); + + // Explicitly instantiate skolem with the concrete sort of the term (e.g., boolean), + // then instantiate schema variable "t" with the provided term. + var services = state.getProof().getServices(); + SchemaVariable sk = getSV(app, "sk"); + SchemaVariable t = getSV(app, "t"); + + // Use a deterministic name for the skolem; the specific name is not important here. + app = app.createSkolemConstant("use_lemma_sk", sk, args.term.sort(), true, services); + app = app.addCheckedInstantiation(t, args.term, services, true); + + // Apply the intro rule (adds equality to antecedent) + Goal goalAfterIntro = state.getFirstOpenAutomaticGoal(); + ImmutableList afterIntro = goalAfterIntro.apply(app); + Goal workGoal = afterIntro.head(); + + // Identify the added equality sequent formula and apply the Contract_axiom_for_* taclet on the left-hand term + SequentFormula eqFormula = workGoal.sequent().getFormulaByNr(1); + var posLeftTerm = new PosInOccurrence(eqFormula, PosInTerm.getTopLevel().down(0), true); + + // Query taclet apps at/below the method call position that start with "Contract_axiom_for_" + var index = workGoal.ruleAppIndex(); + TacletFilter contractAxiomFilter = new TacletFilter() { + @Override + protected boolean filter(Taclet taclet) { + return taclet.name().toString().startsWith("Contract_axiom_for_"); + } + }; + var matchingApps = index.getTacletAppAtAndBelow(contractAxiomFilter, posLeftTerm, services); + if (matchingApps.isEmpty()) { + throw new ScriptException("No applicable Contract_axiom_for_* rule found at the lemma/method call term."); + } + TacletApp contractApp = matchingApps.head(); + var completedContractApp = contractApp.tryToInstantiate(services); + if (completedContractApp != null) { + contractApp = completedContractApp; + } + ImmutableList afterContract = workGoal.apply(contractApp); + + // Hide the equality we introduced + if (afterContract != null && !afterContract.isEmpty()) { + for (Goal g2 : afterContract) { + try { + SequentFormula changed = identifyAddedOrModifiedSequentFormula(g2); + hideAntecedentFormula(g2, changed); + } catch (Exception ignore) { + // best-effort hiding; skip if not identifiable + } + } + } else { + hideAntecedentFormula(workGoal, eqFormula); + } + } + + private static SchemaVariable getSV(TacletApp app, String name) throws ScriptException { + for (SchemaVariable sv : app.uninstantiatedVars()) { + if (sv.name().toString().equals(name)) { + return sv; + } + } + throw new ScriptException("intro taclet: schema variable '" + name + "' not found"); + } + + // Determine which sequent formula got added or modified by the last step on this goal + private static SequentFormula identifyAddedOrModifiedSequentFormula(Goal goal) { + var changes = goal.node().getNodeInfo().getSequentChangeInfo().getSemisequentChangeInfo(false); + var added = changes.addedFormulas(); + if (!added.isEmpty()) { + return added.get(0); + } + var modified = changes.modifiedFormulas(); + if (!modified.isEmpty()) { + return modified.get(0).newFormula(); + } + throw new NoSuchElementException("Cannot identify added or modified sequent formula after intro."); + } + + private static void hideAntecedentFormula(Goal g, SequentFormula toHide) { + // hide_left applies to antecedent + var tac = g.proof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(new Name("hide_left")); + var pio = new PosInOccurrence(toHide, PosInTerm.getTopLevel(), true); + TacletApp app = PosTacletApp.createPosTacletApp((FindTaclet) tac, SVInstantiations.EMPTY_SVINSTANTIATIONS, pio, + g.proof().getServices()); + // instantiate the single schema variable of hide rule with the full formula + SchemaVariable sv = app.uninstantiatedVars().iterator().next(); + app = app.addCheckedInstantiation(sv, (JTerm) toHide.formula(), g.proof().getServices(), true); + g.apply(app); + } + + @Documentation(category = "Fundamental", value = """ + The cut command makes a case distinction (a cut) on a formula on the current proof goal. + From within JML scripts, the alias 'assert' is more common than using 'cut'. + If followed by a `\\by proof` suffix in JML, it refers the sequent where + the cut formula is introduced to the succedent (i.e. where it is to be established). + """) + public static class Parameters { + @Argument + @Documentation("The lemma to invoke") + public @MonotonicNonNull JTerm term; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java index 920da1e5ea3..5bac579bbc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java @@ -376,13 +376,20 @@ public JmlIO specMathMode(@NonNull SpecMathMode specMathMode) { } /** - * Sets the current list of known parameter. Can also be used to give additionally variables. + * Sets the current list of known parameter. Can also be used to give additional variables. */ public JmlIO parameters(ImmutableList params) { this.paramVars = params; return this; } + /** + * Gets the list of known parameters (and additional variables). + */ + public @Nullable ImmutableList getParamVars() { + return paramVars; + } + /** * Sets the variable that is used to store exceptions. */ diff --git a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand index 5390423b7d6..d5eef82a154 100644 --- a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand +++ b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand @@ -40,4 +40,5 @@ de.uka.ilkd.key.scripts.AllCommand de.uka.ilkd.key.scripts.HideCommand de.uka.ilkd.key.scripts.UnhideCommand de.uka.ilkd.key.scripts.BranchesCommand -de.uka.ilkd.key.scripts.CheatCommand \ No newline at end of file +de.uka.ilkd.key.scripts.CheatCommand +de.uka.ilkd.key.scripts.UseLemmaCommand \ No newline at end of file From c6e6d3c1ebd72454dcbaba25da554c1c3d5603a7 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 17 Aug 2026 21:54:47 +0200 Subject: [PATCH 6/7] adding verifythis 2025 challenge 1 to the repository --- .../MinExcludant.java | 71 ++++++++++++++++++ .../verifyThis2025-Challenge-1.pdf | Bin 0 -> 38164 bytes 2 files changed, 71 insertions(+) create mode 100644 key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java create mode 100644 key.ui/examples/heap/verifyThis25_01_minExcludant/verifyThis2025-Challenge-1.pdf diff --git a/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java b/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java new file mode 100644 index 00000000000..0166a20a696 --- /dev/null +++ b/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java @@ -0,0 +1,71 @@ + +class MinExcludant0 { + + /*@ requires (\forall int n; 0 <= n < s.length; (\exists int m; 0 <= m < s.length; (\bigint)s[m] == n)); + @ ensures (\forall int k; 0 <= k < s.length; (\bigint)s[k] < s.length); + @ // measured_by s.length; + @ static no_state lemma nospace(\seq s) \by { + @ oss; macro "nosplit-prop"; + @ obtain \bigint N \from_goal; + @ cut s.length == 0 \by { + @ case "true": + @ auto; // the base case is simple and obvious + @ case "false": + @ obtain \bigint sm \such_that (\bigint)s[sm] == s.length - 1 && 0 <= sm < s.length \by { + @ oss; macro "nosplit-prop"; + @ inst var:"n" with:s.length-1; + @ auto; + @ } + @ obtain \seq t = s[0 .. sm] + s[sm+1 .. s.length]; + @ use_lemma nospace(t); + @ assert (\forall int n; 0 <= n < t.length; (\exists int m; 0<=m sm && (\bigint)t[m1-1] == n1 \by auto; + @ macro "nosplit-prop"; + @ inst var: "m" with: m1-1; + @ auto; + @ } + @ cut N <= sm \by { + @ case "true": // the easy case: up to the split point + @ auto; + @ case "false": // tricky bit if behind the element that was removed. + @ oss; + @ inst var: "k" with: N-1; + @ auto; + @ } + @ } + @ }; + @*/ + + /*@ normal_behaviour + @ ensures (\forall int k; 0 <= k < a.length; a[k] != \result); + @ ensures (\forall int u; 0 <= u < \result; (\exists int j; 0 <= j < a.length; a[j] == u)); + @ assignable \strictly_nothing; + @*/ + static int mex0(int[] a) { + int n = a.length; + + /*@ maintaining 0 <= v <= n; + @ maintaining (\forall int u; 0 <= u < v; (\exists int j; 0 <= j < a.length; a[j] == u)); + @ decreases n - v; + @ assignable \strictly_nothing; + @*/ + for (int v = 0; v < n; v++) { + int i = 0; + /*@ maintaining 0 <= i <= n; + @ maintaining (\forall int k; 0 <= k < i; a[k] != v); + @ decreases n - i; + @ assignable \strictly_nothing; + @*/ + while (i < n && a[i] != v) + i++; + + if (i == n) + return v; + + //@ use_lemma nospace(\array2seq(a)); + } + return n; + } +} diff --git a/key.ui/examples/heap/verifyThis25_01_minExcludant/verifyThis2025-Challenge-1.pdf b/key.ui/examples/heap/verifyThis25_01_minExcludant/verifyThis2025-Challenge-1.pdf new file mode 100644 index 0000000000000000000000000000000000000000..0f05242d29785844fe462aa8589c29af845d5ee6 GIT binary patch literal 38164 zcmcHh1zeO(_c#vI9g1{^bSw+Y0#ef5B_PexUD60h2~yG>(xJ41q@=V+3(_5mbjW`f zJiXF%S!l3Woj?TrPra(N6++E!ChlP82!$}QvbA#cRDifcY=xjBKpUWAsY_~T z$SO&z3jxd^=EiQeuFz^FWff6PbxCMRRZ~_{19}w`)ex6~UL_!|5K~tPH%D75=$sH) zJ7Wt7bk6G;oFOhQQV#a6E<&!(ZqR9+fjpd0bd=p(9o<}|tZX4dBGe)nJk*@j4kp$Z zf`R}Ah`oiYB{djYqXvKixI&z%0aCWmaU~$84rUNxVGI{nXNa*KhDZ7id7nL9H_(E< zhnJJclvwZi?q>ajccn2Z5D&F3csbh*uELN!z%UR~+GH$@s=+84AWHHe!ZH*7t6f$U$`{y1pW*)QxwOa&p8;L4O=`{Y&Zz>c$D zQMy&_(ZGaL&@CgMZvlQYw`$@BdI`Muk6cClk!d2Ovyr49jM`d`pyk}ZbUk2KqcG3G zCS+qIjkIn0T~5y2zQuCk}MW7;%PLn|wt2>J4})oj@k@b!F< zRRwY4A-OGC&B%ba6m_9#=lW}z*TG)~1nPV;hGsk@4pK+jflic(w~5euc(aCZ-5!sV zj6HOG`^d$So!GRLQ9E1!@3TolQ6&o~LMHGI?PHshy-so;R#5V4Qq7F~RM`-BJf|6f zYKakbMj38fF4*aS=qoNkdR-a{~wS(o+NSLqCf5_n&ECJDxwH?pM-ToH#1ZQl~N5l+R!^)ypD@8eZz z8ieOq)8Xni%BV}&;Y&BkmAb#2x`R%d8@`8m;RDW7_iwL+n>J=cVi9O(Za0ml~?V z({$5#D7ste>pVbw< ztSi*3-AAA_x|K>Rcu+j--q#V*fv-HpX|$xwylyg0=5l9+xwuY~k`F8FJsqP`T-I*T z=kNV^Lpa|+I5DW$a?b;;DJDA@LbBtVyc*2cFG*GfFeuBN9``tG!ig&wDd~(n>dWnR zL)g1D%8aQl2);r9q1ght@z)7^ z7Je!`&+1i?q*W1v_IS$se9)V6`{jr8F=I~YA&T=%ZRY&r)H9uhSYN%9If$jYeegz| zf|3Y{iSOsgy|)Wsc~y0<1oZX;KEFygykL zywgQc4q;b2^c)(-Pfw4XU zo(t=)-ZdWp3U36H^2=M6s(v*|xfi#K+auf#c04+}W>O=kn1ol#<{B9As~d{eb=|EW zrVK}IdEUJ=$*d6?RkQK##01=b_^C>S&{bKDR3F)V=v)o~v0f6rQc|-7lzC+k(>mM_ zr<~o0K6h7e`aZ>XrO^gp!}xcPHhBXu^ObLX3p?;Fn;Cc-;cXP)Qczy5Z#N8HtkzEqL@NJSrILa%V5Gfsx6fk;2&1FDomdBlB5 zuymJZzI{q_gZVH&mW&&{TpqqNZ<*i}p-~@mcRHr5&lo;I*(~>EBf5Kih_m%)#r62%Y4_)5J<=yB%sk->Bo^hsFOKwJh@97-?+(> zBdM)sf3JI>lwZAZ2oDoyV<}iHGtce=;mdI3_$M6-fRH?o=8C~jOxS9V=VrA#!w(sN zRAnVfoL;#`a`tzHP&S=Qgl*{`ye1F)l!ZiZIWCB0XA~=tA*N^Zo57bL?qM~P}S0%jp#1;_QU!8djLs4nh7R`!skw-mRy z1^ek;BHvR69QL zG)(0=ly_dNAD4yrM}v|l2=>5e0`CHEvqaW3e+%}9+-s?pdO~8{B7mG)qGad^!E*GF zRr7ADI^bq8413Q?cZf18?S=GVM5ZZ%G?L;et>qz-r^~(N`9rP1TacBl4_|!4;isO9 z;SMCRTG{C@6BdIf5jQhnUin6FW7FP4P1y3zf{NDxk|17@w>nMZLpv`8r&0C! zyjb95Uo~zZyg$N28>?sUq|gI^u;g=7AY#|YPXSvF4H9Y4V)S>e%gd{Xr|D@s~0q=8f^xO?9^Dv1`QZ%eNL}c zn~_lomL>ZpM~FS|I^_V19Z!f4QQm4RSAV!q{|RGbY--cwn>l$Vr)cLvHNsWkd2*pw zpHh?MTe^;b_*L>dRjOkVZJ9k|_=f$Q&&=-zjlM~nz8^^w>zLkcNwaS5+J6tpg0sFh-l&AxM*req)QLE+{RIz?3o{aZ zj^drb7b?uAD(hRrq*ApNcsP99#q4EBPbt^#5^7_(J;(lKRvx;!=>+4>gAi>&_ z0Hn7IF7e$1%1uNkvwcpV?mJIcnC#$WfVm#Y%qgSk&#o8pR>rZ>T!GK?V-eytV&dZh zGCNk7StL=?pqRgqiH`~n@nAx+DYs1+VctMV)t~ELio>QCs9}Nn|6ZDcyJ2!-ooaKrJ|(ANzek)YHVlejHQ1T#&to6Yqp7 zlJFAf!(u>)e|-qlO2M%%e^V_qbaoloL_H6U-X!bjy4#BAi)i4H&wh^LUuR*fkdFtNMjoHm*yudR9iUd(GeqHKYn8HBL6uP} z%Ki{S5w}RkBWXDodWE^O6s*N#bu{4Yf}r%_F_Fh67~NXZ3$WR>H=gc0EliB~rhZ_P zlTuY1@>IBV`@GEXi2cc=O`?Yt*wfEJd&^bzQzWXFe2D|dnRJe@?bCq;mzKWUZkaXH%ZrN={eqxV5DS{f%|G*!iGSoG zkY2TWqIL3_Ynor#juNvSdG_$`RM?vD9qAY1GLzLxXxMr_p}_}UW<@n;!=H|8&Y0@_ zCAzha)YU6ZBW@%49xtt0E*kYa8eM?+eYe`(*J}HlunaoFZ_`hr;#>sOp9miu)hxYL z+%0xjU)S4HlOZ*JskcNmtLAH~M~*v1b~$NGUv;?AQ2n8CTu|MmuA9fpp$@f4@SIwj zUG*@#aHoHlKSP$RT4*r#yozGp!mdwFdWmMV2ExC+X5HtUzElU{U$(I6bAE9LT6aRE z{=mA>96wExg|gY;<;y|B=d2POYL5MMI<|OGFYkX&&k#}u&S_X0M(JX+azxQQ$Y{zE z1DNc1IX)T6BQi3I=#BM)JCH@t{|4gc1<~(Wvr{p%@!ys|C*QyOoGfk*5$qM$i;d$w z-HRP%)!&Paa{T)Ai)R+0N))HLiQc_CaTSC*b99dw_}1k}N9mCWM7p1?&zKrUexzj8 z#~Az+TI`u8s5g#!PfIV6D=0fNDPt1DonUZ;!Ai}3fO?JagK>;U=$Av#e)W^DamsT2 zv{l{2jBt|vZP`j3^>L_&e5E)CeNGe_Zw`Psyc6|w*b&QCNH{*zPaaGXKFL^}>ohVH znP@8Q=I>?uFyF(_EAi!OJh`$vW*;6n|FR%SZeTzLQRYqB0G#qJtBYuO4mr=DEY2y3 zkBFi>S0vr6z`p)d_)OiF$IS>&WO2p$Ka?ZRqC73AO60P>yQo-*G4XsR77e)idN}u3 zH7|;Ep%$Pl|}I|`l>2yaDe`LH1~J6yl5gpV~Laf*x4Gk8+nFkT+xb1?<*89kRmZc zgl!J)ts>0d%3Z$)uKya5BNnbw*^3Jqb9f^oalYSfJ$G5~Syf}W5u=Owvnadp{obyE z`T{&lmu9655r+>C?hBHd9vPD`$(?1J-f7_vaL;D#e707jd}2}T87)T`=WO^Y^hBg? zgQiBhaf>VhM-%7%01gjF$w3|CxxvIS>J>6VaqAYu-t1>W0a}73Az-No*cAi>^J4t0 z^WvpUY2k}|AEV;zy;xMZ4Nx;zXC=~$F`#dG$(^~IF+j{lj|J~{KZ||ZG(_gDYT9#!fN8_7c=H3JPJxC~`m<`L@$n6dWbz^c z`=Ykv-5OJp7P|9do!in(w`rV_Z~1~-U9?0tKsqJTg0;Crwh8WBZ)Hm2a)%RC;JM6? zEi*8!DUXr93yEH2z8+&A8Gl+Pjn^vh@s#JO6q!QREZu@zined~H~WHEyY5-{pj#_Z zX-230eD-m~=a26n$A>uztaVAaOjxq8r$DV&G$Kqcxmk&o(K9 z@!bzZc<6{t!SlXDaH3%HtJCl*jYW_OawZ>1ddEQ0rLt!^77vRNF}esim`xd%@}E~2lULmg>^xUDBlAR9S@#BSBpgQqX=shW7rq z*B;u1+SN3O(+GUlrNP-{@2pjclC`!_1LeG;rGT^k9_ZsL(#3Htr=={pcc_ySke54U zF?-PiMvyz4dYhi0KjW0NYAyvoe1Jv#uy&z6LLYsgvA%K%FV!hB;wlq+B%f0GQuL{F zCVF1UK2r9Gp&9)7!jZm>e=H6eo~qGh0gebTG6i8jmxosu6`6o<&FwX?wKZW{r*^f= zXd`Tgu2Y9GKA&x#dD-(3;agNP*==H?kKU=TLc+v}t+R`g;Vz1vwp&wW^dv0$@PvIM zqa93=5JEz=e;6(IrYKk%y*Nb`vg|pNN`|a3O-M-}kG=BMe<<%3^PP%d>3oUZZq4|y z2R60GOjNiF?k@Ic?li4kN#~zASitOZG|2N(*1Ak}Rra1vL%A69^?kUxYI8is<#2N) zhO!wWswB1YPgM4`OAQx@<6`b1c+Ig(vBg1JO=j?Wk&YT_pFR;Km_o3~$9n^4Mqfsz z+h$T=zV%wA%e!AM9X^DOP2AAutr5lx-oC@bcWL(o`GdWE;lGy!x7ZJ0nWjnMTAP^T zA3ZP!&!^{Q*r`*#e7>J)jar{9L$ z7DWx^)Q8Lal;ER+OI`38OA4n)BG~B1E~uHwn~a2HoV4y`g-HXJrghIEY2}l0*Y4Ef zFp(SW7*>S@i}7Wm-A>%|>7dGy8G!G9zz`gUXm^@t_gj) zU{1s09;GZt^b+8rPnHY%xE!(#)gbz^W}P@45M(l$-);8or0tB>hf0xy<{fs$_-Fim z)mV)OOqiNuV7jZgz|2RCL5+FJnFH1a7L(H~iDO-0X8}Ez-SEK~SlGRZ zZH}j7E+3t5yO(4>JyLw(NIZ|{IlDEWuQ|@VeLJ;>d>U;WT<-hy9x~}Zc5V~uDxC() ztQD7Sn4cad?#4TKPU6i}Fk{~L>3YEM?7sY zhYeL_<-uXhrYv55)8Uk7GZ_f?C0RJq@jEHDK>T^HTm^*rzn$Ju4-62`d{mLLv=`~? zY=9A93bA9u8!nxbC)0>#SONLOZW1&PXXScDfOCBtK4!s_r@naXJDWGNUg$>k@&KA{ zc`3xs+x78d+uGV{f#CG5C(U_npW?|^3%-wR`G^N>_q%Qn$)SJ!pi`UypH9xM{`ks0 zxwU7M_aTPA($0t78GKx;*AxjSUAlg4`x9* z>Bu3EU*n8_&f}DTWYM~VyK;~zx1{@$=;c#KZLF1asUY!-*jIcX^JjO9Cj+cR9FPQs z-f*weDeM~g`AJdXjhVM98-l143f#r&z7V@nhVv$Xu(i%YzSK?i7Q-vatkukUacso- z$fA~1jN%t|%UnEsYDnH^SOXSNYt(qVXrW5AK-$KqeZf?>3H|vpvx2H~_>>BH?&#@f zRT7>{4%ter=0)lI(O#WH9n7|)%ew@@LgNG?PpfwcL@+#SSpD#=f}lS>Gpv3b9p_To z7iimQoxb0URI1c{P{Qbu>c@jc9~HSS*Jsd>P72Cf$U!zDo}p`nPa2$l5lJlaH~~Fe z`0lh%7OlQf{WrJv+FynFwOn96?%#gxFK73Uoi}dYf8*BRs`#{ZxFaS^`wYaoI$86PdB-Qva z?SdEEp0eR0Yi(gc{J6Gy`mO}q=jD^toGYu*3`5<~pb;~)vjKh76|w`f+HZr0G`iTp z!?aMPSzrD#a8^SW@2o(`$yFWv+pfn6JFGlu<213~I^*iT^RTrB4yxmA_+5Pr>8xJ= zgoz*{(RBnseYvpcn&Q-cK0Km4aJbhdl;>rE)6J|2RBW_|Yn5E7k zjmdm~Tlc)Z&*skd{@XHoMU}P1DIGEsoY&btio4c45l8j?&$N$GIFr}T=AYvvhHSUk zsB5UVVT@{9*SlKfP^c+o+s}MydtvA5R+MPIln%BPGqN8$Ove&2sM*GMBlVdR5@uHz zBAt&3Nu8Tg7^*Y2pmAzcbYrNHPt;gF~1%B8)KqVi977@kD6#*s*^T^JOh`J2%2L^%yh?Yid;ZsZk;>5f9?fZ*U z{1nd+zBOQ{F{1~sK+ZCqrWcsLFD>olER@P73rof-07&6yRz;lzx1Ox{s+uacCI@Ur zeNmRrDIjWyR;4>zoe2HFL(Zkrs+0;a9Vhbu8_vD}iEb?=Af-p+#o zoD$o?nyAJqq%BEWM?nN)Y7g37{A53j7O5-5^6Mzw+fVrbzMAJcKh6;(#C8ae(wEhG z-VJ)qm5Y^m>vW$CE}D*hA2DO3xMdPof+9#=*)tWZDB5$LIiI-t%>@Mo&O-_OstvP@ z3|_hIV^6wJ-1KQ#5gb+}ev6E7AK@tv*Vb6quQa$L$;tOGX+B*F0%DDvJyWD{ShD+;9}vnY z=n?rah=NP?!TZf@oD*z5^7GMw$1mLE4rXmK4i7_KIfvJ-(q)*O;UKS>gz!mNM|P+> z9c->jGUWn0Qdqk`)Tgl!n9uuCY%ZO3UlEJQll0BDk*!Ze4Rt-KaOD@QJ9;$R@_`}d z>EA5^Ow(Z&fgi;G%OHUMh;ubO9U%Y}=w3cR5n^U#Eau=rtp^K(!9Xr*UVbip41k)0 zD|BC;niC4;46%2m=7w1gXf?#e!Ohte;sP})D$Wk3>JV2w0Q6J=H9!O6;R@|1>ESA^ ze%+Pp+Sp(KU`GU~x%jU8LwEQAqW1O7*L3xaXA-1 zv;y`B(5e34;d_l8H;gpbbN_+Pbz0yiKHN7>GW@^B=MQTACJ*;Dy>8G4#*rW7ff66e zPwH!ix=;h;t;}4g^)P-s(=`>RJ>y{u-N$jk04O^`>_tssr%|Z&u4jav=&*tbf+ED#*bF)lH4oP> z;{IeT@DI#?F!s01U;xxbsm+aTU7$xneo4WNRqUGT*W!Z#5OZ)ggB~BbmRcZmI&o?} z*mH0~i!uONn4p@vQtNT?aB*<)@==3%IXQSZLDXD4{2aVI)L=dk2at;!3M&C|fr9-+ z{DF=xH9s#04<8>VHM9dike8F%-p$q)3a9R7;tJCl1uJ`-KXCh{WKaoJ19D?rKbYDL z35K!pCuP-uAPnI3JWx|lO@S52GH7-sJE|?CgL5o}%T-Q_ssPSU_ShLl* zKp0#<`}1SKR09eJ1Y!WMQ&oS=c`eHSea;&badTmC|D5Q*4tn!JZgl@|eXbw&Cn93T zE)bZa0aV3Ql_eEe#TC_cfSlKs0m=YVXDdfn2WM*FwFUSg5-@0}>9BHkaTT{Tc81y^ z1>>JZUVebKm6@xhiyj6qFN`?<<%98G+F4yKcRqhrjy)VC4HX2=v+QMeSXze&0)2nVUnPCK_s!^)NUAc2@RoF8Y6rdM#*w zWrL`atfDN84T`e=z=j_JcdcxHWdkqY4L zd>{rzO^xqw^6`Uw|A-jR4FQ3ce+mdS4>!y<{I7^ztKnY}Q-wuF?E0(j=Jo$7+ORQxj0hbW zsvbAT{BPyIL0)70x7t6A_ZQs%51hI-UVr7(0~K9SbsZR|{z1CAuUE5wHZowIo16mv z<`gdo*6BZf{)G|Yxi-^KYCx|bFl;2)FYJz+6Sfj?LRTgpYCa$@H4m5zR*&(c2M8)y zAWlANZs>#ZTzdduFl-S3@$vj0sCB)j{FPeTs^apBsxXBE|5f3*{tK-@{D062TK=VQ zVBr5n;cl#>zn2O*NexjMEht`M4}e^M#q7tD`H$*$6EPsy4O0Lm?0;n8pH>21ZrJcQ zKR{0K^+NM+I1PgFlZO-POW)9MZm3@k8xVHoheqMoZNEnY{i=cWjbuuk^b{P3@nx0Q4WUfE&aGb>pGd;WyqlNpz$9vz-?T537axUe{OXvt364 zusdE@-8CF9515+gHw2Iqdix6;cIAQjR8T2pH#k$-LXHz#jb6beVjdl7)u=865RK*p zP&>m(%?C4s|B{b?u!EZqYKfp;|Ddk`Jr~0A9Vd}*DX*;*o?3qurGAnKMBc?#r{8dH9WA^{~v_} z%0P2-fVmYkVt^K`ZivbCI`UUVS5{WkmQw#=D*x_P!?f^!RduMKz{t-7jg@YGZ<3xH z2ou?#A1D*}!2Hk!?9Y}HbiHK3V1S%Z8uP=X;iuGrp+=VPS~_4Ie-HGl1mh~tk9rs+ zj0@aQ%EFL=Sy5OE7`k%8O8h*~_znic%Yy;CLX8A3H`Gu-zaXfkh1S3zVKYFlH~0uu zi$8nP|AC>`VaZK~!kpqi!j@~(s$^^j`G?>}44PPhMyTviS%QTsyqrAxu=gFHZ*72} zc@P&}%OzIUvBTy^~5 zxQ7zwG~?K-8h-BN81ayPIRzUw1kQMaylw`LEucJ%aAolB#B9@?2L_2a5AxtRL8l)CWz$jR2!*Uwiw&t)1Nx7=PTK!I|g%{bNBU%4zG|YVhp0M#e*h^|T}X#csUt@8i3J=+8cT zUkS!1Ym80s=X>iudi43p8*(4#hit3gJo!k7;p)EFKluk?fvMxaF)M$Kh<}R;2x?Nm z;NK?YFQNkelUaenT_?M)&B}ig6<*+fl@!-U4u6uBzhs_3Hx|BsZ%=^yf3hd_a5BH` z2{J4R@WYx!oH(7b|F$M#c+IyPabN$iCh%NvaChJkpr*tfYDrECBW92H4tC1mTMv$1 zHxZ93j*SS?Qftf7QhGbO+9OucjxiZ0&u^b&3377jRy|3{E=jFy(TVV&;|Ko`82xpQLDwLvQX=GcJutz~U{vN?WA`#vZXy;NWf7pa% z1X-=Wv-vtR@Nd}s_x!>&quHUa?QubqxI9o7AIuN>Wf!=ihT!J{0B4Djtf)9zU0o>$^WKF0h&hKbI&F2x?J&uQbL0V>?HPvx~948NdW! zV(bhsaW*!E*h0)*f0UeI>)LhE2IBg=8e0C*URBRU@ra}7V()jx`z5hgD}m)auJ%Cp!L|J!4iW|y;`@TChM^hO;$c4 z@*)Hl1mi?bWfotyLV5BR*D?*4KU*FV(Wk+S{45oA6rW zY&>W_u8OO59-LaEYQ8#e@ppiysiH+f2sjxX;NZYq{pO#7PYwaTb*&noL~E5o1LuA! z#>v64OuJNXtaC!TN+HAdks%}{q`dvc(69Adc2a%x#|Z$n<49wluz|2k=ld!DS#FDp znYYJltb|NNC1@tBmCq)X`0j9Y;FvI0MocP}(L4-S4zKOFXCm~Kq%y$qZhF|W4s#Ps zVCE~@f?Mk0SJWLy;;%ZGOhA?CuV}jPSkd*`qh2u{;o&?XqoMf}?)h;2Nmv-&G_pLh zS82W$vRLJ?-ichi{f-fZg>RZGEo(>o>!h>5djgwHs_=P?krgE3kvd=oi+)^iEm*mW zgCb3^ZpJ-*hjIpQMxf4r8VEfX3Fs=PSQDw}o*Pp$w_!%)-sEgdrpR=qO&Sc36R=Ey z26D<3)|`BjZ;-a_X*HV0}S{>B&fwZB`jW{-k?>jQc4MYBHl-W*#O}G)~{s z{&)x~#J3<=T?1k_kmtXNAkIai=qlxkt>R`hT%EB<%ZUZ z1wn&X$LvY!<}H=V-F3>T&~+Qo;Y!bIBb~A@XWsRR=n|{aaMTBnc*o$_ENk!Olm0Iq`Nh`d^W^T)FbORv+4$eysh7 zz}(?d8-b~;c+jCBcQ-+4SB$7kuO|*;(37|))PVOsk2k@wc`$^9Y(4{}ryl?$qq1~O zfy9UO&uKL9DElB%-w-7ir2T-iIvyi-R;%_cwaSdG z^xmzP{Fhxaw3|6}^~E7iml~EFOwfYDf>eb^c4Oc^t|E3T*M52_&0RIw7J^4!dxD{g z7&j6oQC&_ZGdt4eM_eRMLJrX$x>$bWwsPOYS6K|@pddgZ@2jmK4xsLcyg5SZP@5G2 zVe-7Ef@nquH56AP(i^<|uDWIAAr@Ln>|snQ6TfJ>1YIF-@c~O{2(SuH0)&(Z%{ww`5-cFvuqN!BK9HC$qXR_?Ajd(ax zs4v2s7DKEEOh@1;jZG|Jd0fJYukEIc`sl4SYi0x5%!Lh#^Zo6wh7qCDYvzU+j40|S zOM*LyB`D@*R}Y-$K8Rq-%E~8v4#@RYe`PfIkgaXW&ug#cwZinmfvP$|@P(vJ=isiq zR>iDW>9Nzqvx+VDK@P+eg{G%nX~;?URFN51`(nB6n1a0|>@NtETTNH{+ubLRP8B5b zWEDk7P6hMu)K z$D>mC?WB+9D}x4KZ>=u0E6~vov0Krqd+0bidU!ZG>b&mN&@x}_4OubobDHyV0i;e^ zTm?&l%=~HiHQYf9V}f|OZLAVrJ*e zVN@_|liWN?eOXC7Q#MmQH&pb2?0tk{!;5#tDGG`M?0$Hk1oxIGi{dFUEH1^(tc0zy z3Yp*onR@pwh#`Zq$^hHR=1$L1pP>X~MH*XocYB=mVvIKigoG6bh9_nMRpNL2PgZE? zJQ3=T44le#p9ffcCS%)kCd1j_rfD$V$ezJ5D;`5tb3Zd*!sYrzG62t)>~#N*8oKm6 zlG!Q*WcKjmr{RYmYs~cn!J7$3JDQS5J-4SYhYidC5}$P>Tz!r5TawtQTO04aIC@c8 z5YnbC;qYmRxrcOk{d+ydNqxQk!m))zEw$(CorJKcsRep%hP(MCc%q`rn0XO>l!g+y zEvVyOr%#a1QHbRAJgRq4B0>#@?Nb0Xw$)7QfuHC+Rpb)-YBAib8+1G8y(iT(@Snr& zKcZ#;>^jmmL^m;Pd`#IO-<8at-dEeT=ZGMS$#e6kZyc};)G^xZx4LSkP_!n}{oaLc zIl##;Li}kSzdCgMj9s{fyUTH2ce!&7Fpm+hz8dB*(Xi{7RSTGydKE4!GuaGe*QYFr z2_!p|9WDG^2OiHXGk&^k;ckesxu?mS79D(FS4LNcD{YY`TJc#A@pc5m)kBS#G~{3ngDT;> zXnXITI|@^}*o$Vcj@A`)r=%?=Oq~h3PfnsM=^13Rg0g}3BC+AowUpmMII@F8p-GRjJtQp{1T-RDP&t zPwaub#(A~BJwEDk2bD$45?XNTx%0i3s*kWOC5d!TCe9)y`YPo!TO zomYvjo$k$JF&DI9!;)ish#TF{3K;L!zMst zbu#@DWirfYtH?_-mWc9G-inUihvXCNpGPiqR5S6(()vAoYgm;s3uK~YmVEl;;xOgO zT$C~)2JC47%6m)MWyaI}Yy8z6U$|^zI01#j;uk01?tGOIcC=R?2pp%>7-POT<0@B@ zkwYOMFj{6nILmKwOj!I*mnWFqX1)JDxLe4Aw4yev5$7s9W}u(aHbNR;cotjFT#-!0 zKfO%1`LN*2L-hgr?A=)>y_(&KohS~6pi~>?J3enpt(8{_*qBvDJ}F=^D=wIWo_Dov zNgLzb9TL0ZHXi(L5TseBc{VczL3)hWar{Hvr{JZj{bqhWyT( zV+|oCJvWzcCu%b~TRG|i5-fq)VjilI0k>|^+(JO-Mep?$>%sJdrvb#lp%+o_Aw1QM zudT?|FO^>FYp5-3sJ7p7Z5f^sard1Xp}eXDyt!Kb-TwY%@h4yd!aG(Zy`WzMc}bv^2Np%+wC@hdC*-$U5{7mDzZ{mM|0_y zxt|2F(xN*}XI>%M3M7W@w8p*4nACf~LKxBX%&r}5s`rY|mbGh5_(`zo+^Zeq0IQAB zif>0>I6_%z!4eldAHYKPUVuz|9@h5)K_c8NFCsGI#Bb%Jh^KurUMuu#7Y}C&yj4M@ zwKu^^QUHC!$fBs~xv(Yo84cP_16*Xku90(KpAw>7HYg;Wbk{edS9Rj#_R~}TILYa$ z30gTEEsTT&>QdLovD;7VO^L{ZmKySKandM;mtTlxmQ|k}#yhgaedUtkM_X1YA7}dd zFj1P^_@(qKZ@N73wS>80E(hZGB+^bxf*K)UJcgH3ru+Al19B?Mn?2{BvpznactOye zU(HRRqY*5ljoj(sWivQTBt3%n{27WH@_JvXtS*aw9GnMmRAsOFw0t1my9PD*9kCzX zNLqut_S>>R4crI>v7Uf9TF*?jQWLUurvz*TrJyz&+BA+gAwiGNMRVh~%*LEI72P#n z8rNjsVJcs-m(J^i(Bz4acatbLJ|R!?py9^AdsMGjVP;W{B#@0!E)GDfd?e!a!u;Tv= zF8|hL2|U4eYv%_yOkDb8rQTk3hV@|5PnrvC9Pa`0Gxri*NSZzb=c0=E<}p`CEq@;3 zU3+kDV0)zS&|yOZG9&B6!;VZ)0ZQWGJ)`gqN?`<7tERkUcz*G6p`M7KoK%o>c2(vU z(ufpq;Sn;Wa|j_`JssIjI=d!y;kcxGZfEVG3L-;5VgCyj4FZ=K^XiuH2Lw6=%PfUB zIO-F0yj8ObZnfn2f$>pgqgVG1i8thowk6bcMu>NpSiA39NJXO{4492Z2|vTU z*S2JX26p4`;uEDRc+VLMdSTMIeN5YmnVtXLsYG3#s<6R?oSjN~(b&Ke?3JOi#@(6S zn()RZ&Sb%KjpVAkjqF7y#M)!9Mr|@F8}0>l)zb^qnQy4B&mJn0yPzoXY;PrIhGGuS z+<8r&%omXOj>)f#i;0j#Hz_X@p6 zw#;9alUXCY2@XTMMEK+%gkNl3#_VJjZ;Xv8hi^c0SFF!-l{(+Bm<`v!c`blUf+!%TbXru8C&u8vZ zBT}fBuWbt5)$oe_7%}c7BdtVhM}#{fql7dsz7(^iEAS8rQ~32>hrqWf1% zA~EP56PQz}NkViuNOU#fxS~AsiDxpRN_}cUGh}|pMe)<5@G-@O zDUts-<~)m%`v8^kghs(Zsm9ncJ4Kb9vOSf)p9>tyAqvm74C2^kr==V#{H)bHO z8f)sdEYsn17ses;Psx3_IeM1xUp2_X4>UP&$~kLJGAIU>HW6#)#=BK#(T z^mBdNz4b${B0}HVMBuQ{TazTz7cAbVKSsm%E=^DgwBWVKY#t3TD5gL49}RhmW*Dxi z%EsOca2-9|)zT(Q!e?B;A0cyJYk!3QHQ0fVrIucWL*`zyLs8%CqD$Pf?oE;T)z+Xb zOP=hp*v6t$^fuQ>@fAZI^531kr*I@Vm zv%d!Ycak^Uwcp#wZb#T$h`_thP2_{`A0fXsk@a;gv*zu;Q@}QnEqhw2J7Am0i&uF; zd)>#oiXy8H)52L_&p(9rfA+sxCeojp%V1sGD4))l8;EUht~s|o{<=c$?=@B3u%)q# zr#6Xm_<36x>j`foZtdQR>Rfzl#RnnNXM$PeL=mSxlu9TlaP#uqxPNCI?D)yQ;oRR( zH~w-HiL~n?v{4V1BvBpSTP=i*xg^0POyM=Q019)&UX*=~>UXFz-oh&w9m70c*_e<`L{)b&1W?b(`%2Sg^IJc7bCM_Ot&k&eCd(&k%|9x0tIN39V zmxW-O6IYaee26xbjYBd~J<3St5$hW0Sqem#=N;|;*Vj#DkUXdQqm1Os7*Hl z(%ndRZ&Es?TR^%yB&Ay#2|-fn5>zB5@5Zl;@0|0y=idGB$68~JG3Quo)-wlVzAq0@ zGMh2$3z)|Mu?gusL5Yt19X=#?{>}2stS}N>j@)1h=Zdw}u=%JGoa5_cw26=ktX^R( z%uFND-A5}&cL?>Lk!NUCPdYLyTM$3vcmPki0^2pHirpa@?T*Abbl=hAe>Mmwf9GZq zUX>mx$ctr#`gEgxVAP#w1Wnsie$Fu%0aPDyrBh*K;n$NiRK_cdJc*$Dgn(4~aeO>e z@3h|AN2^tYx=r&=pGw~v>Wgo#Z&YPqW{^uK<&0E4vke44$%-$zXx!|haj`TTip&Uo zBjcW?xRy;!OY@TbM&wFu8&zhk5g~nNGqBerFab$ItWKtSB!)*neb+puG}RetJ?W*M z8~Z+gl!37Ea8YUp!wDDHTQ0Q)!4ItpUq6?GT4DLx=nF1YM~)9dWw(HctHyKSpl@Jm zgAe6cMJB6f?3YnnDbFqY&pW1H-+MxGGI!Su2ns$BM4bCe)4&WvxuR1zHED6@k z!IP<26&uq3Vyv!H=XrX^+^xqlhDS#RwXBvT((1S>GDFm$(D+lU|9Nf2^mRgr1VU7x z4P#JEoLvTw^Fc#W=_#-iTd1x(wV5vPv+lsYznKN&iFt(frGA01WlJau%hxtiJ9Ovf z&FS{V^!n!;!`{y~6MPJ6#m%R9cJW0OB2Q_*lrrfCom)JhGvyB}RQ8-F-yB4HGd+a|XOBFqTc8QN79 zdyldAo>pACW+cAyIJ2=l*tS8FMgy%syXR`d z2c-PyJ{aZIC$TasZ>(o@IRNYmys}hvT<##l>$|dF`@Mf(5x%Ed|0heruj$%-FGY7xaH$55xeH02zQh0G1dH(15KBMzFQvpCsn*IUBcW8b73G zSpN{y`7;6IHuvJ+LOZvqnLjQfxA*_oiwHZI>&HbTL&HN=#jU-=((h>nN8~D*;d9+0 zCKua^cE@*)mJ*I7;S>RWQgbwW6lub<30}C!d#C#c6`*6(IkDd9c8Y))8uSU%88cae z^hoENSE5a9zhG18g28Q@y3IYu%Swuy$?P`!w-!2YXXN zc8SAtJ}MbgVXLrc9#He}sl?IHJ)DYs6(^;y8v2wgRRO7uoJ9}Ja!2LR+j$mV5}rOm zytwks?C{E&ydW!ymAM!)3{{mpwYHju2i{34HQeC2Xfm5eGZHa1`*P?0LosL7r(PX7y-UOano2!_W5%!Jhp~OOj>0PyEZ!9%fN(eDY%IlY8hF%YNyHAVN6(nb2mo!P zR-suVD?SyugV58idBb4vq4&-cnl(n0&4U87iCGoFH#D1BUvGLs(oQ?J;3Ah9%L%R- z&QKmXR#cN>F3;N^oI)zlWu_)6=^yu*qCG~q7(MjUV%#Ho&1ECexDwNGZI@786E~G# zcF5#kf>e>&13jlnG+SrD(`r(Nt6H{vO^bB>ZZokk^^LvJ)zw^dsN+4K*V^wNR(wR- zJn7>`l&N;sdpQFbm?iHoc;}B~^+1EfIC5h)v~wBiwevVVik;Ahx^>TyVZ{P#Yt}WD zfI!o~O+WEzP#W@;d1v!w@4?~6H$wH`*82%_l}=vw_w$*wOJqjvbU zXKlDx)qMI^1z#Spww}8&kj|)>xFGBi{iS0V<~eq?5qAl%a3{0P#<(y_`BI`n3ze`AHY ziLN}XMu!p8fW{lQ-jzVku>;S1enlDhN&`)~a8SM*kVtZ7dQ3HpRfrjO0P1*NZr&YIjI_m} zm*mQ-CEk@KHlcU!X5mGwVG4h{J5OwBsN_+gzTjP_U`UY;Ia+)*pJpLrvD`f`8qTfJ zXVIwIO*Az>eub#qS7ywq?1Hq8Bdsdp$V&NyO{pR8fyTSA_KvU)OPn=ZA98Dg&9zDf z?RqBYdn!cS3t@{w#I%-!9*u=6-Q;KqkMT59O3H4 zk1~sj(;d)o#8VbQio+7D&&A(W-LNe9IwY*<2Ufr+4{@z~Vj!IUdgf-DdoQAgtp;dg!b%tPFH3P94zCYGL)V^(RTw|!lovKa|@%y zNAD9@iRkIu?vRv!@*{`fnxg~BC-#CJAn6|;;HF^tsBWV8V7(=BHgx1%*dDH^cSCj+&fG=!1whR!r#5!@79u@F ztl9M0PnmJm?gl--`tk{HyG^mI{MqXb+&Y!L_XuyKG`Jn2gA-+f3&odI;Rs%*sFFQQ zODEocN9J|?M&NS{myF}Rj><*NDHn+~o5CJ^uv92RY)KwR0?7#@CBj#c%&gR`eJT?k z>9d}%bo|E>&Itof53e4EdxYNzJmnVx-KR=TX%^2@@}2bB*^kEWF7I;=dH{D}L)jjw z%iON4O?fYvG?B4s^33)VNWXJW*O{DfxrXnGkoi&KOPXz;y0t3$F1iJhO5AD>^Ez|N z2YB?+!JV9vHub*$W{ zDIncs!P7K+&CLe667qa{#EI}RgM;mQuIjRu&_6jcInYDbgigtNlRLGK;h{m7nFa$z zm`%O@j0yLh5K>McZqc^ImsAC#r>ZIi|E8rXBnYc5qFID0Nj=LC%2l`_wS*G{liZ#oq!*Xe~3vASkBk*1qf9cL?XZ+iZU(5e>kk(0T7Dlw0R-i2NVI6rB_`IcUed2l3IkTd}|KM`=^%AL(w4D6sKlJC@6 z*T04rx#}X!Ax%+$ViHGW2fS@Ax4}@A~ouC9A#AuiVsJ)QuJ0#0ZI0 z+W^J8DBh;)FM%z*IW+K->FoFqYNQ8?@y~1qb>F~@hCpvk(-@<0A%wn2N|DtE2z4gupz)rIMMudaHmSy6EgRQ z{GWy)@726bPj5UN&U2VWgs$(^7N6XUa_2|0RM#9eFGj`h%m13v-zl!VsNnca_6$B2 zzNM(}GgfN*24lgF%fcYKG9y?`W(5=XV@8nLC5mzlN508bUXromy(AGLAZR6DZfa9q z7$wmn+{zK&U_FS09u?NBdDND5@6J=%;(LB|ONX}6^&ndJB`|h(Sv4>mw==Q<%802b z$iF6j8zQx?U0pbKla$DJjt$o}qg7$LY}ka%3w734tA>g`J}O>%ad01QlVzAA^eDZ~ytH|Lwzn4=aNI`y(TwfZM&JG;H^% z3Q+%R=lDyyKkT66?Vly=yd%I21}^kp?Ii!_9REMk`(0rN1pY0x-vi+JdwT!viLD=Z zpFf=7`p?g>z|QjjxcjWvv{Y5qXlR!ZS^B7onzRsLwj`4qCI;he5lgcm;gk-mnb?{PZG6v%Xf?@v zrN31%jd=}Rd^-02V&Ow$haTL}`)C|wgxn+&t`@fHD-N=1pR;v`5O`UQ zPmQnP-Zj!aV;stOA!3_vrkuurX+=;UJTGILx2e2P@~(vJEvglLef)XQx!=4*MXtJv zb#eV$-d!;(?E1`k;U=YrDgZ^64OzLO*Gg+8idHzZg>)*>iMX`bk%Y3@?`gVJPE^}F zrLmaZZHlVJx`i)FPO|1tArRhT(of+dM>4N7Ct{wuq`NL+uI2S(%4+gCuJn#c$4ko` zkiP72f8w;1Sg%q_X4zj5O&cAP&XjJ)bN_Ln3@Qygz`dHSBWv0j3J$IqJ-8qJkmfT*j9TuPMQVjk*P}RQDW3q5Nd~>cYn*RNaIQW zDkRuKmMc8fNr6d>)I~fQuZ(Rni@^M(QR56ra`GnVHDH)b)M9X=3av&kEM+}`ri25Q)ZtROe;!w_We}%m-2@{ua4tQv~9XIcprt45Xjh@SD%)$>HFEIq}l8D zcdSY7iCT$Y@p||{^FyBVqbLsFbV`JN0ffg6V>Vu|ZLTtFYO*Z(RlS^5s?*8%KqEm= z7uWs)?HEqMSls+A_8F;m_I>#o(vtl>FnIvAgQnR*je8f}m%ux-Ooxg42j~kZk?ykw zW@J7+yU=s&hl`}9nM_SjiLX-o+PBH}!UZMmgs2#eP$`AfFv6ktlf%qg>xj_&z7c(f z_<82X-zz4x75c)1v#9N7!0ynDrw5Pw-43AqqS5n7Pbv${(^X+C3N|Fmd}2kke*<}t*Kf)aUik58^T(%t zO_$$9_x$K9oOC{YG`EO}EhG{_Ly{a(@SX7!^A-zKp}pD`I1-51vtX&0V4o+9&l74i zPHT9qaW6C*4Wq z;)!iI;oW80NfSNww;sZN`mMnYDHG_mu^n8kL1a5#?*%2#Ef1f)IMzU^-gh9;mIR>Z zZiz_O;#nf?bl@R%P;=%DF~sS3j(=RFN~9TjLPYK)!vFJSTDp+~=D&{5ypY1v6i9yr3jD@!S z82uNSb^<3F2Gqs0nTnJP%^B2uTm)m$(Frapj*(d~tCFN?8;Pku;`z!_K7$O8T0FlS ztTXZXen3Cr1V=3v>y~+qMF{>I;g5OZFZyx-qe|eK&yE67^dID`n^fI);N0k}(AxOl zzVT&UtX!5V8kDQS2!OHngl!cW80%Sb)DCpXR1J-Mrh7#tzNYoY@paiwqg#d6O5xt_ z#`vkijWfQgz4U>uCnJmSAw>Gp5~8eegGeoTgEC|2KOK^THFy?k6Vbj+Yz|93S9^@S zb<&N4{1&%Ul;w!?DuoK6c>VD!DU$qm%M^Eyi8*3KiKPKbapX9MoKDn2qfEuCDnXYE z7O_hPdXBFYhBbGHTvF(ea#vLJa%WuWmP#4J{oMx?nUlV1IQp|UJcGzjCBS=_SS3(@-+VS3OBrnALx?a8K?RIAktv zmz+%PA=zsp`{ac+jthxeQ7Eb1ysTpiO-B26BicASv^EoOrlSoz4uRhNB!_x39mNQ{U%AZw@H8Gyc>X1P_nhG!#BM!wDUr;w*4Hh6A z8P_Wf%7v-p+0nU^x39rl*DogTVX=fv>f|Glt(;OeI<%|I42d^7P4;i-1xNc8T+p-oJo1OF zZFWuZ@eZ{qd4ncrLjv!$ShLJLKdE8U@u!AmVM-}i+BUy^2}d%GSQ3jMy;Cw5e*bYs zvfuy%P2Z5Se@)F*$OJdX$G6g0Xf5^F#vA9vbuZXXFH&55;1y=;E%SH@bVV&9#!Bmj z1)#;&uf??r-!S=ufz#aH*Zub9JcI*}`#DaRg$b7!Sa^o%TsjQOg^b1Xz zBpLu>)si%d`0=pTx|kTgMa0m8d=^u&f8IEb)|&ajggw&3FB&bO`(gJF(B@H}Qe@LL zC!xa$sK!fKRX3J=MFLP?wotAU#tYV`f1Y^W<9trrX_sMB9;q(pLG_YghuFn+-db}l zGI$`LMRhB-p|(yGpIg1Z*I@E95lRUM)+iY^#Js2wfl=91r(44pVNTdx*K(8*D8geL z28anuCY5atb(JYPfL1?$;x@+57@AcseKeMq% z1<1jwbT#10F{5IOGb^oyht+FoDcvfNLEOvktGQ<)Q^XU!-Q7?{>_Nrirs{7G3%|ir zuQamqM-pJ~%psdyBPL|`M7C2*SrFeawR8+fQWw(T;y}E#X!;{aM{-+3)hY&}NAAQS zb4SY##Rd}B=qZ1d9 zEson^j4ui|Moy1*D~pb;c`Nu{t>)J?8xyf_aHIlH>`Y=O$e&IjVAu15pzp|2lkdwu zKI$59oqhmj)^W+2e#ohf$(0dgwk_50iBX2ekq&4)jn0{iPe;G{5`3O3Icyo@G{?`e z74q#4Fb4JDs7*N?dpK7zP8##|h0bT}wZ2v!Ts|3T&LV--2n!m)@F2C|)aE_(dMcGs z#4%_vbQY!kKByw6KO0kfzzf1BBX@KX1($GV?sTb%QJnc(5{uEcuaN8Bvv%~Fp;sKH zqD&%=QQd;m7Kd{r)5xV6yPh!0 zG<=O0PX*q{Cta#V=Z;_OEqqaNsc3jP!otc>S;>bmBA0@Xn}Z@B9dB0H7jzL1W`C+R z;J=G1rsLjHiki|w2smk^tCv)JtbHkIr3bLI6*UBU0*ZFKre3Q75A9R z%G#(0x5r1*&JlyQbIeRSA?I=qP992RxCetkL`qtp8OUkx6TlZ!_4gkFdMz&3GRsC8 z1^9Mf*}9}H8+X$H1}2fVdbRzZ@ZlPm80aiH=N>-!h~0LSZh~g1c;J)H$&I~=1H8hixDb-Sxv6uwQctnDctS{eC3?j!H34zOs*u^ie>qjk=$ zN%LUDt*5+D$%SVqDg~ktEg7zD<=1cPWK7Rim?D$x#vie4+fv)=L)LvgUbfXU;;scYct5;CzlF(Ar0I`otT zp}5T8S@XEjiS5F5U3x@4c5d=nH3sA$5lf-|a8qGM>ymB$j)(LEriJ!!A(FXAHIin` z5o%QVtNlE)%G_TKPSE7jZoD21Jo+NG=abgR0oG*fHd0JxC`(~b!aAYseVhDQ$Ur$g z%Pr|l8tGg3y7c2}VS@GWqI-sntwZ@enPc)0?SbQQ2N~beWfOUqon`C=s);*d3|>+| z2#vUoJ4olD9xed^85w~(uAYH`ipranvXhQ;lDYWm_h;Ogfy>ugl+FINnxgD_Mu@KB z@?93V+1z(3Ah&d^1220CYBL8lcJX&At*cF_8{roU3@QD6EwMA9sC-@_^q4-H$g=v; zf(GY@6AWSLOa4bJx=DG`I&1PC^4p%>zdjf)LTE>?6tsZ%EHIXk)bSo^l48^w<(NV z!VCQqZinQ;47AYDJR#fm4n8`v2LPHH{JEwB?Q(OfgN5xB$xRb`hh50swH$I6O(2ia)9qiy4RO^>)Sa zaT1|=_qm#gkHz+(|!a&VcTf=6RQ*FuV>RlB&RbbHFpQg(_R zNla+m7j*Ovpwags8J(^E{n+m>H^B&(NOl#}a3taZXFFyKO)ob0zG&N3@lq473ah89 zrj9;qIykWl30q^>?YJvWpbPw$$lWc3#D5aG`yIyX@6a6(1WN&d;a_nB|Bl_=!utGm zV&{7<=HC!fTs$ynkAH%9Kv; zD(20Cpjc;JDdq!oBXjw1ZT#eL{HjJ*T`R=4SL%3*aBxNTp#{)4n{>*@8~eOYr4v&^&`=`jzdcA=Zbw$G=M zuOaBhCg2AbT|<3$Yx(yY?eCzRPZ;T}A?K|FhbTWMS2gkFU2Inw@Llm5`?h`aIa(zH zy>vW4xrrlsQ3LjxejY>Ba9$a4K5Kum=fTcz*46`DOPwA;FuQ+9xi(yGJj3oYqWU^Z zYsALny;*BYY9x1UqSos(VCD#^8DedG>TtQyYoI+)#*AZaq?m|%7k8~QAFN=qVA9s} z9K$;PVmM~N0Kx(-c1+)&t<)?yi;Q|Aw8bA%+XMdy5`|25&@*63eJI(+x64dVShOSG zB=443Mw2mV29Hf27O#+6zT_&)Cb7W(E%F6)7LkvF&)F9hgmGzE&ZU;zg!M{1D!0#l zNENf<3rhNU205pQ$#JH`fCU=|@pRF|AoehR@&HZ$&fD=zR;VZmzu%@vPYH_$jl@AQ z#c?!^R!$wyl=H&5}C?)dqO4aAnHEXy*dS>@rIFnC0E3(oF%}3&oJh-94 z{hz`IzE)IY!0{+hpevzp#PlkNb4Sp8oLk(yOo!#wL^~=i^$}f?VHQXlJ38uI%q^lW zSNhb1LvXnPzF7jqkcZ`C5ClnvjZHqNWai=m2C4kj=MQiI=!`9tFVL)|O3SPn?D-no#|#v;+MXPSoZ+V{&u7<5*>gY| zp+P?WJ4Zdi&mnLU*LnO|ffP>34@GxIpKrU|LohA{m65(;f+&`>_dFLBk!c{0?+MNb zrE=zmZ_H@D-)riuB|FFFqGJ+qGD9vuZ9ef{R)^hgLRQLQ!6T1dZ-8kmK%leFpG#lP z#0I>__rg4&X9Gt5i;*U$r(~Xk{>syf#6j6y+1aE*+l9H6jmhnra<`~Z(u)!rca z$!H6TFOKRUrvq8DoeCh?pW!$Rj2e94v{zliz$GD(GDa4#?Gy@RuZTgyhxZoGFD@)g=qh^M(xUm7+T8{8HtYd>MaOnfDck}MQ#6s&T6wkZTn4RR+ zE9}aC^S+3V6oiXE1IZ-BUpT5oM;c=9Dy$Z%WoGdK0!tZAut?$F;V^IzK35SEn$T{D zcy$gLtA=nde?f#03+(SmB}y)?3Wa2U4ps@Tp(-ww4dggxqF&M&G{jqITxVZxf6h>A zZf_+osQy9my(52bpmWAjzr+SNT-feuRT?U6nwL{T-1;y~`u0le-_0>&{H@a9cmZ zMvOr_%R-{_BpNAeGOr_x!pURK2h$H??^M#vj43DM#XbS!<#jg1xcjcuPfk@=BUvW_@XDGtTZFyz#4ej!-F_W5%*GZ{!XN%AxJ35wVAvP zfz2>q&_ui@LCz0-;MoR}j%y3UAnTc7j58W-GyDltfy~X!puLIXHw8InfeZGM@z+P@ zYD*O)m(GoCB6Lw%a*G4A_JwPB^-Ray4yC2-FM1Tno~6n?M$vghkEI01tH+19WvxB! zLS|$ra3rduD#1~7>9|+sDoAgdm9XZqKq{Cw@I*F0P5IiFk*zkHHC(f%$?r^A&3J zNR?4va|rB^paOYzP+&bV-w=uQ{CxQCozTFrS47l2v_1-9XC==-1P?GC6=E7BtT|ZT z?~rm%;6I*WxPI=HMa7I$sH7keTIHohR}QZr@E>_CQk$_H_Us~%J3@%-R}$s1RBoSa4LP; zXjvWGF53x8opru=L9~$KDeiqK)wGkXlvVKIo;F(pO+jH{eqE`PhO=U+Bw>@Z6eB9D zZ`Nx*$0e_->Y8dK-UyqKXsP{%UdPxMwJ%wjJE1WA`}Dl8v*)!ncsG5=(-wR zIb{Pg5<6=m)4qbWml^OjNykRF*bb~)f-(6qkL7Yv*#>oge}CTwoLc3u;+<$JZ-l05O!prZLM zLzdgSyu|Lt47lwRM6J+g7moa9;Z8cOwrn>>(Nu93WD*j0c?sV4g>^0wzmhYvz}p(F z`%1Wzn|vsi2o!6+qK&}K{?aCzyDW}qI-C=7^f^w+l%n7ERdRB`HO@7Bk)^f*kwgNb zd}m3r<*_8bjz(&hj{2fPdOtz_Luoj&MgZa@!u_X<&=2l+SjJ5(CKqhoUQ%WcOY@0t z8uw~mO86dh1+~itHi5m!SGCC1yw|t*`Rrl9-Hk zbLPaHAN%;rW8Ul1g6VH~V-)hLe5hy4o*65-ROo^|=9gO=+@34sZq_TNLm#QP0KR~H z!NNZ6C5P4S^T0XDoTd{K9{~r0)MWd|>{!Vt+Ab;j_5X0`FPz*EBSDy z%jDVqjdXiQZ+OUy?O2K{LtMv*)jAkCz;sV$)}{y6CP@^oDaHeH=+DU!=bmIt!1w2d z?y-3eI972)evY)k@Ccq7+uW4*uj9KMb(4_}j(9kXv4Y6s;~(*@f4y6EhP+1NJW#@{ z06o)2;|r&IhObShY%Z-f{M?pcpOkAJ!D*VqJ6wMg?6{aaAHwTMF2=e~$HgSxnSV2n zIIqN4pOCayU|UlCiv6mq<;WnQ-{(fazG}9Xta#>SW1%{~7F`dNl(GMzjZ-@us+-xi z;fr!L_U)l(Z5L3225e$Mvwea&0zuonn%<8{z+v3Tq7Bf&B}NyrE*31_-C5cvn+S_Ak_35Da$v?~M(=kh_DSF$_SF!pPLz(oTT>b4v$3 zg{6rAy#}WoP|iWj)WTBA)5%oDQ(o2B)7qHFgkDGxm0!pZMuBX~>Tc-3YG!Ez!&7vo zfWZt4P>CtaN>be_xbwQ(I@rQ!dnnv(ZS0(R-392soAAP}Z^Zz5itj2=YXN#qIYkPn zy}gaKC5+pNjfV}y3SwuWFmr<8AiLQ+SyO=6xaeU;I+>X9D#O^J{wNT3CqQojg*xy8 z0B&w>Y;Npq_D<#i5Gl9e^qq5<-Mhnx#c3dt=Q1W-UTW^MfGPX4nNfXQ!%gyuyWX8FK@X9I%SK>UE8v{1hrJvQ}#y|;<8;2%%_zD4B++`96E zYkz)~A0+?gEUYE|{heXW_vcIV!*qCIgiMxZ9^x=~OhGUZ%*6_Xu!6W%!605vc3w_S zW+0ds2;>L+q6uqin5o!zRL%dy^asr!OzoXiVI4qF)=Bgj9G!OA1e&&9n4{7Y6=FKf#?DMS%a7u|Luo^i<8awj%#8JfZ?3pR_P3D6A;W1 z6JuU8dna2%C~W9BIKW`L4R3qnZHIw%F4#k;B@6*o@cXb3v4Q?^VPkpQL3wQq?aT$} z-C0dc%?w>^pfLUKJ;%oK&x`N+fPcz>T^ZlDpuN){#i*D%{#D+urr#gkn*MD7yEge} zwERCh^ixUy(%rv{V6y=1Lj(SvV+2tt{y+Wx{}uGl#0rD<7NB>#oi=|1`TilA_t#9p z@L$XnjIj9GZ4<$|!0j+&5a+!eqd*wV3mC-7{(X4T1A+7~HP|rzA2d{NdkzCkRm25q zVefQ%1;eYig0Y<4Uj8-T++P1V?il`MU^4zqUFHrOrneaT?5MXR;*TGUhXLjlg&D=4 zG8hdS>}79%6n1~g*txiG7p|XVKnOPspZHf9mt{V6i03z37?$v_wlJyy82{SO zwqOv)Emy=(<$*xlw_FQ9$zZkKa-setgAu*`{vIGM$gg@p2+u8N*-y4W9*$d%f}dm{ z*jY0e{?Jb{AP+Z;-{5B%h#d@LE%;dmHyz5^Q$e09Tr0Vxn3AFH21H*z`nsP>%vd|!I&FvDG+{@!MGKEkwG|aA;5pugHdPv zRvtGP#>Drt9xS+hdrtBvTM(=~SQPjt8IT9e_1m|HaNe@g{HzC~@Aypy0sr>xfjsQL z)d2!SAiw$yV!!3+`MC}dj7#QMUqCSGiQnE0!VTj(`Pmi>0^Rbc{Nytj#KrxqEtnnr zTU&x*@%>-@gYjVS{Mt`p-2jFH@pBz8+KAuU7se3tn}6&us-7R-7wTjPqmXcdF>z7= zR4hGBVeN&#zd3S|m_w4Iqf1#E!ANHhV`;uJdk65JeIA|Me732~Sk5C~Wt u1mp&Bf`B4GFt;d|I7sk+*3i49sC0%JIzhirR_rj`10X6bt%QOk>i+@e7g8Yr literal 0 HcmV?d00001 From 76193eac25d17ce0900855981900a903aa0530fc Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 18 Aug 2026 09:59:56 +0200 Subject: [PATCH 7/7] remark on the verifythis 25 example --- .../heap/verifyThis25_01_minExcludant/MinExcludant.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java b/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java index 0166a20a696..e86e3b613ed 100644 --- a/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java +++ b/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java @@ -1,4 +1,6 @@ +// TODO: Add a .key file that runs auto; and then z3 on all remaining open goals. + class MinExcludant0 { /*@ requires (\forall int n; 0 <= n < s.length; (\exists int m; 0 <= m < s.length; (\bigint)s[m] == n)); @@ -64,8 +66,8 @@ static int mex0(int[] a) { if (i == n) return v; - //@ use_lemma nospace(\array2seq(a)); } + //@ use_lemma nospace(\array2seq(a)); return n; } }