From 19117fe72ed3afc9f62e6fcd4b8cc6d0a224f9aa Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 12 Feb 2022 19:04:26 +0000 Subject: [PATCH 1/9] k-distribution/pyk/ktool.py: add ability to proveClaim with lemmas --- k-distribution/src/main/scripts/lib/pyk/ktool.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index 75860e58dbe..2e4e400427a 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/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') From 05156dcc14e2977824b46c88a0f2ea8e12179208 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 12 Feb 2022 19:05:00 +0000 Subject: [PATCH 2/9] k-distribution/tests/pyk: add test of KProve().proveClaim(lemmas = ...) --- .../pyk/emit-json-spec-tests/emit_json_spec_test.py | 13 ++++++++++++- .../tests/pyk/emit-json-spec-tests/verification.k | 8 ++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py index 90a7f30a4da..95da3c10c65 100644 --- a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py +++ b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py @@ -4,7 +4,7 @@ import unittest from pathlib import Path -from pyk.kast import KApply, KClaim, KDefinition, KRequire, KVariable +from pyk.kast import KApply, KAtt, KClaim, KDefinition, KRequire, KRule, KToken, KVariable from pyk.kastManip import rewriteAnywhereWith from pyk.ktool import KProve @@ -73,6 +73,17 @@ def test_prove(self): # Then self.assertEqual(result['label'], '#Top') + def test_prove_claim_with_lemmas(self): + # When + new_lemma = KRule(KToken('pred1(3) => true requires pred1(4)', None), att=KAtt(atts={'simplification': ''})) + new_claim = KClaim(KToken(' foo => bar ... $n |-> 3 requires pred1(4)', None)) + result1 = self.kprove.proveClaim(new_claim, 'claim-with-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'] diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/verification.k b/k-distribution/tests/pyk/emit-json-spec-tests/verification.k index ce3b23c6cc7..33212cbcba2 100644 --- a/k-distribution/tests/pyk/emit-json-spec-tests/verification.k +++ b/k-distribution/tests/pyk/emit-json-spec-tests/verification.k @@ -8,5 +8,13 @@ endmodule module VERIFICATION imports VERIFICATION-SYNTAX imports IMP + + syntax Bool ::= pred1 ( Int ) [function, functional, klabel(pred1), symbol, no-evaluators] + syntax KItem ::= "foo" | "bar" + + rule foo => bar ... + ... $n |-> N ... + requires pred1(N) + endmodule From a3f9fb0d58f334068f9d6849b4039b5f9178efaf Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 12 Feb 2022 19:10:09 +0000 Subject: [PATCH 3/9] k-distribution/tests/pyk: better name for pyk prove test --- .../tests/pyk/emit-json-spec-tests/emit_json_spec_test.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py index 95da3c10c65..0b3f9821223 100644 --- a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py +++ b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py @@ -77,7 +77,7 @@ def test_prove_claim_with_lemmas(self): # When new_lemma = KRule(KToken('pred1(3) => true requires pred1(4)', None), att=KAtt(atts={'simplification': ''})) new_claim = KClaim(KToken(' foo => bar ... $n |-> 3 requires pred1(4)', None)) - result1 = self.kprove.proveClaim(new_claim, 'claim-with-lemma') + result1 = self.kprove.proveClaim(new_claim, 'claim-without-lemma') result2 = self.kprove.proveClaim(new_claim, 'claim-with-lemma', lemmas = [new_lemma]) # Then From 78d57e5b95bc685cc385196beeaa1698ca4556f7 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 12 Feb 2022 19:16:11 +0000 Subject: [PATCH 4/9] k-distribution/tests/pyk: slightly more structure to KTokens --- .../tests/pyk/emit-json-spec-tests/emit_json_spec_test.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py index 0b3f9821223..47cfc06aa46 100644 --- a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py +++ b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py @@ -75,8 +75,8 @@ def test_prove(self): def test_prove_claim_with_lemmas(self): # When - new_lemma = KRule(KToken('pred1(3) => true requires pred1(4)', None), att=KAtt(atts={'simplification': ''})) - new_claim = KClaim(KToken(' foo => bar ... $n |-> 3 requires pred1(4)', None)) + new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''})) + new_claim = KClaim(KToken(' foo => bar ... $n |-> 3 ', 'TCellFragment'), requires=KToken('pred1(4)', 'Bool')) result1 = self.kprove.proveClaim(new_claim, 'claim-without-lemma') result2 = self.kprove.proveClaim(new_claim, 'claim-with-lemma', lemmas = [new_lemma]) From 25a7b4b5ca927b66171ea2694ac99dba59eee3c8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 12 Feb 2022 23:06:03 +0000 Subject: [PATCH 5/9] k-distribution/pyk/kast: more compact printing of claims/rules without requires/ensures clauses --- k-distribution/src/main/scripts/lib/pyk/kast.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index 19c6fa537e0..57fe68d7559 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/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 From a6185e6d8f11d6865c3596171569d8d66deeeb07 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 15 Feb 2022 17:09:12 +0000 Subject: [PATCH 6/9] k-distribution/tests/pyk: add simple-proofs testing harness --- k-distribution/tests/pyk/Makefile | 5 ++- .../tests/pyk/emit_json_spec_test.py | 11 ----- .../tests/pyk/k-files/imp-verification.k | 8 ---- .../tests/pyk/k-files/simple-proofs.k | 18 ++++++++ .../tests/pyk/simple_proofs_test.py | 41 +++++++++++++++++++ 5 files changed, 63 insertions(+), 20 deletions(-) create mode 100644 k-distribution/tests/pyk/k-files/simple-proofs.k create mode 100644 k-distribution/tests/pyk/simple_proofs_test.py diff --git a/k-distribution/tests/pyk/Makefile b/k-distribution/tests/pyk/Makefile index f9019276020..c47eee9800a 100644 --- a/k-distribution/tests/pyk/Makefile +++ b/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) diff --git a/k-distribution/tests/pyk/emit_json_spec_test.py b/k-distribution/tests/pyk/emit_json_spec_test.py index 563d0f28e59..f5cf72eb620 100644 --- a/k-distribution/tests/pyk/emit_json_spec_test.py +++ b/k-distribution/tests/pyk/emit_json_spec_test.py @@ -64,17 +64,6 @@ def test_prove(self): # Then self.assertEqual(result['label'], '#Top') - def test_prove_claim_with_lemmas(self): - # When - new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''})) - new_claim = KClaim(KToken(' foo => bar ... $n |-> 3 ', 'TCellFragment'), requires=KToken('pred1(4)', 'Bool')) - 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'] diff --git a/k-distribution/tests/pyk/k-files/imp-verification.k b/k-distribution/tests/pyk/k-files/imp-verification.k index 8193b52fd83..05feebccf0b 100644 --- a/k-distribution/tests/pyk/k-files/imp-verification.k +++ b/k-distribution/tests/pyk/k-files/imp-verification.k @@ -8,13 +8,5 @@ endmodule module IMP-VERIFICATION imports IMP-VERIFICATION-SYNTAX imports IMP - - syntax Bool ::= pred1 ( Int ) [function, functional, klabel(pred1), symbol, no-evaluators] - syntax KItem ::= "foo" | "bar" - - rule foo => bar ... - ... $n |-> N ... - requires pred1(N) - endmodule diff --git a/k-distribution/tests/pyk/k-files/simple-proofs.k b/k-distribution/tests/pyk/k-files/simple-proofs.k new file mode 100644 index 00000000000..bbcefdd07f0 --- /dev/null +++ b/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 $PGM:KItem + .Map + + syntax Bool ::= pred1 ( Int ) [function, functional, klabel(pred1), symbol, no-evaluators] + syntax KItem ::= "foo" | "bar" + + rule foo => bar ... + ... 3 |-> N ... + requires pred1(N) + +endmodule diff --git a/k-distribution/tests/pyk/simple_proofs_test.py b/k-distribution/tests/pyk/simple_proofs_test.py new file mode 100644 index 00000000000..28e7831fae5 --- /dev/null +++ b/k-distribution/tests/pyk/simple_proofs_test.py @@ -0,0 +1,41 @@ +import json +from pathlib import Path + +from kprove_test import KProveTest +from pyk.kast import KApply, KAtt, KClaim, KDefinition, KRequire, KRule, KToken, KVariable +from pyk.kastManip import rewriteAnywhereWith + + +class EmitJsonSpecTest(KProveTest): + DEFN_DIR = 'definitions/simple-proofs/haskell/simple-proofs-kompiled' + MAIN_FILE_NAME = 'simple-proofs.k' + USE_DIR = '.emit-json-spec-test' + INCLUDE_DIRS = ['k-files'] + SPEC_FILE = 'specs/simple-proofs/looping-spec.json' + + def setUp(self): + super().setUp() + + @staticmethod + def _update_symbol_table(symbol_table): + pass + + def test_prove_claim_with_lemmas(self): + # When + new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''})) + new_claim = KClaim(KToken(' foo => bar ... 3 |-> 3 ', 'TCellFragment'), requires=KToken('pred1(4)', 'Bool')) + 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('', [KVariable('CONFIG'), KVariable('_')]), KVariable('CONFIG') + return rewriteAnywhereWith(rule, term) From df9c7cc4a06a3a3fa12eff02603582756969c65e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 15 Feb 2022 17:10:50 +0000 Subject: [PATCH 7/9] k-distribution/tests/pyk: minimize imports --- k-distribution/tests/pyk/emit_json_spec_test.py | 2 +- k-distribution/tests/pyk/simple_proofs_test.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/tests/pyk/emit_json_spec_test.py b/k-distribution/tests/pyk/emit_json_spec_test.py index f5cf72eb620..395de8bc5b7 100644 --- a/k-distribution/tests/pyk/emit_json_spec_test.py +++ b/k-distribution/tests/pyk/emit_json_spec_test.py @@ -2,7 +2,7 @@ from pathlib import Path from kprove_test import KProveTest -from pyk.kast import KApply, KAtt, KClaim, KDefinition, KRequire, KRule, KToken, KVariable +from pyk.kast import KApply, KClaim, KDefinition, KRequire, KVariable from pyk.kastManip import rewriteAnywhereWith diff --git a/k-distribution/tests/pyk/simple_proofs_test.py b/k-distribution/tests/pyk/simple_proofs_test.py index 28e7831fae5..7767ca59895 100644 --- a/k-distribution/tests/pyk/simple_proofs_test.py +++ b/k-distribution/tests/pyk/simple_proofs_test.py @@ -2,7 +2,7 @@ from pathlib import Path from kprove_test import KProveTest -from pyk.kast import KApply, KAtt, KClaim, KDefinition, KRequire, KRule, KToken, KVariable +from pyk.kast import KApply, KAtt, KClaim, KRule, KToken, KVariable from pyk.kastManip import rewriteAnywhereWith From 9594d5e2b7ce27f7628e772c21ca4b2348df5480 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 15 Feb 2022 17:29:21 +0000 Subject: [PATCH 8/9] k-distribution/tests/pyk: correct test name --- k-distribution/tests/pyk/simple_proofs_test.py | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/k-distribution/tests/pyk/simple_proofs_test.py b/k-distribution/tests/pyk/simple_proofs_test.py index 7767ca59895..a3f0fa0ff0f 100644 --- a/k-distribution/tests/pyk/simple_proofs_test.py +++ b/k-distribution/tests/pyk/simple_proofs_test.py @@ -6,12 +6,11 @@ from pyk.kastManip import rewriteAnywhereWith -class EmitJsonSpecTest(KProveTest): +class SimpleProofTest(KProveTest): DEFN_DIR = 'definitions/simple-proofs/haskell/simple-proofs-kompiled' MAIN_FILE_NAME = 'simple-proofs.k' - USE_DIR = '.emit-json-spec-test' + USE_DIR = '.simple-proof-test' INCLUDE_DIRS = ['k-files'] - SPEC_FILE = 'specs/simple-proofs/looping-spec.json' def setUp(self): super().setUp() From dd82baf01a6e6b3c4bf23918174e5ea63124f804 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 15 Feb 2022 10:32:55 -0700 Subject: [PATCH 9/9] Update k-distribution/tests/pyk/simple_proofs_test.py MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tamás Tóth --- k-distribution/tests/pyk/simple_proofs_test.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/k-distribution/tests/pyk/simple_proofs_test.py b/k-distribution/tests/pyk/simple_proofs_test.py index a3f0fa0ff0f..0df7e47bbf8 100644 --- a/k-distribution/tests/pyk/simple_proofs_test.py +++ b/k-distribution/tests/pyk/simple_proofs_test.py @@ -20,9 +20,11 @@ def _update_symbol_table(symbol_table): pass def test_prove_claim_with_lemmas(self): - # When + # Given new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''})) new_claim = KClaim(KToken(' foo => bar ... 3 |-> 3 ', '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])