Allow specifying lemmas in pyks KProve.proveClaim

k-distribution/src/main/scripts/lib/pyk/kast.py

@@ -407,14 +407,14 @@ def prettyPrintKast(kast, symbolTable, debug = False):
         if getAttribute(kast, 'label') is not None:
             ruleStr = ruleStr + '[' + getAttribute(kast, 'label') + ']:'
         ruleStr     = ruleStr + ' ' + body
-        requiresStr = ''
-        ensuresStr  = ''
         attsStr     = prettyPrintKast(kast['att'], symbolTable, debug = debug)
         if kast['requires'] is not None:
             requiresStr = 'requires ' + '\n  '.join(prettyPrintKastBool(kast['requires'], symbolTable, debug = debug).split('\n'))
+            ruleStr = ruleStr + '\n  ' + requiresStr
         if kast['ensures'] is not None:
             ensuresStr = 'ensures ' + '\n  '.join(prettyPrintKastBool(kast['ensures'], symbolTable, debug = debug).split('\n'))
-        return ruleStr + '\n  ' + requiresStr + '\n   ' + ensuresStr + '\n  ' + attsStr
+            ruleStr = ruleStr + '\n   ' + ensuresStr
+        return ruleStr + '\n  ' + attsStr
     if isKContext(kast):
         body        = indent(prettyPrintKast(kast['body'], symbolTable, debug = debug))
         contextStr  = 'context alias ' + body

k-distribution/src/main/scripts/lib/pyk/ktool.py

@@ -71,13 +71,13 @@ def prove(self, specFile, specModuleName, args = [], haskellArgs = [], logAxioms
             fatal('Proof took zero steps, likely the LHS is invalid: ' + str(specFile))
         return finalState
 
-    def proveClaim(self, claim, claimId, args = [], haskellArgs = [], logAxiomsFile = None, allowZeroStep = False):
+    def proveClaim(self, claim, claimId, lemmas = [], args = [], haskellArgs = [], logAxiomsFile = None, allowZeroStep = False):
         """Given a K claim, write the definition needed for the prover, and attempt to prove it.
 
         -   Input: KAST representation of a claim to prove, and an identifer for said claim.
         -   Output: KAST representation of final state the prover supplies for it.
         """
-        self._writeClaimDefinition(claim, claimId)
+        self._writeClaimDefinition(claim, claimId, lemmas = lemmas)
         return self.prove(self.useDirectory / (claimId.lower() + '-spec.k'), claimId.upper() + '-SPEC', args = args, haskellArgs = haskellArgs, logAxiomsFile = logAxiomsFile, allowZeroStep = allowZeroStep)
 
     def proveClaimNoBranching(self, claim, claimId, args = [], haskellArgs = [], logAxiomsFile = None, maxDepth = 1000, allowZeroStep = False):
@@ -96,7 +96,7 @@ def proveClaimNoBranching(self, claim, claimId, args = [], haskellArgs = [], log
         nextStates = flattenLabel('#Or', nextState)
         return (depth, nextStates)
 
-    def _writeClaimDefinition(self, claim, claimId, rule = False):
+    def _writeClaimDefinition(self, claim, claimId, lemmas = [], rule = False):
         """Given a K claim, write the definition file needed for the prover to it.
 
         -   Input: KAST representation of a claim to prove, and an identifier for said claim.
@@ -106,7 +106,7 @@ def _writeClaimDefinition(self, claim, claimId, rule = False):
         tmpModuleName = claimId.upper() if rule else (claimId.upper() + '-SPEC')
         tmpClaim      = tmpClaim.with_suffix('.k')
         with open(tmpClaim, 'w') as tc:
-            claimModule     = KFlatModule(tmpModuleName, [KImport(self.mainModule, True)], [claim])
+            claimModule     = KFlatModule(tmpModuleName, [KImport(self.mainModule, True)], lemmas + [claim])
             claimDefinition = KDefinition(tmpModuleName, [claimModule], requires = [KRequire(self.mainFileName)])
             tc.write(genFileTimestamp() + '\n')
             tc.write(self.prettyPrint(claimDefinition) + '\n\n')

k-distribution/tests/pyk/Makefile

@@ -54,10 +54,12 @@ FILE_DEPS =
 
 pytests = defn_test.py           \
           emit_json_spec_test.py \
+          simple_proofs_test.py  \
           unit_test.py
 
 defn_test.py.pytest:           FILE_DEPS = imp-verification/haskell.kompiled
 emit_json_spec_test.py.pytest: FILE_DEPS = imp-verification/looping-spec.json.json-spec
+simple_proofs_test.py.pytest:  FILE_DEPS = simple-proofs/haskell.kompiled
 
 test-pytest: $(pytests:=.pytest)
 
@@ -93,7 +95,8 @@ KOMPILE_BACKEND  = haskell
 KOMPILE_COVERAGE =
 KOMPILE_OPTS     =
 
-definitions := imp-verification/haskell
+definitions := imp-verification/haskell \
+               simple-proofs/haskell
 
 build-definitions: $(definitions:=.kompiled)
 

k-distribution/tests/pyk/k-files/simple-proofs.k

@@ -0,0 +1,18 @@
+requires "domains.md"
+
+module SIMPLE-PROOFS
+    imports INT
+    imports MAP
+    imports BOOL
+
+    configuration <k> $PGM:KItem </k>
+                  <state> .Map </state>
+
+    syntax Bool ::= pred1 ( Int ) [function, functional, klabel(pred1), symbol, no-evaluators]
+    syntax KItem ::= "foo" | "bar"
+
+    rule <k> foo => bar ... </k>
+         <state> ... 3 |-> N ... </state>
+      requires pred1(N)
+
+endmodule

k-distribution/tests/pyk/simple_proofs_test.py

@@ -0,0 +1,42 @@
+import json
+from pathlib import Path
+
+from kprove_test import KProveTest
+from pyk.kast import KApply, KAtt, KClaim, KRule, KToken, KVariable
+from pyk.kastManip import rewriteAnywhereWith
+
+
+class SimpleProofTest(KProveTest):
+    DEFN_DIR = 'definitions/simple-proofs/haskell/simple-proofs-kompiled'
+    MAIN_FILE_NAME = 'simple-proofs.k'
+    USE_DIR = '.simple-proof-test'
+    INCLUDE_DIRS = ['k-files']
+
+    def setUp(self):
+        super().setUp()
+
+    @staticmethod
+    def _update_symbol_table(symbol_table):
+        pass
+
+    def test_prove_claim_with_lemmas(self):
+        # Given
+        new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''}))
+        new_claim = KClaim(KToken('<k> foo => bar ... </k> <state> 3 |-> 3 </state>', 'TCellFragment'), requires=KToken('pred1(4)', 'Bool'))
+
+        # When
+        result1 = self.kprove.proveClaim(new_claim, 'claim-without-lemma')
+        result2 = self.kprove.proveClaim(new_claim, 'claim-with-lemma', lemmas = [new_lemma])
+
+        # Then
+        self.assertNotEqual(result1['label'], '#Top')
+        self.assertEqual(result2['label'], '#Top')
+
+
+def extract_claims(module):
+    return [claim for claim in module['localSentences'] if claim['node'] == 'KClaim']
+
+
+def eliminate_generated_top(term):
+    rule = KApply('<generatedTop>', [KVariable('CONFIG'), KVariable('_')]), KVariable('CONFIG')
+    return rewriteAnywhereWith(rule, term)