From 188f7ba5282a3b957cdcb0268f9abcdf877af00c Mon Sep 17 00:00:00 2001 From: JKTKops Date: Wed, 21 Jul 2021 19:55:37 +0000 Subject: [PATCH 1/5] Potentially fix logic, but some tests fail --- kore/src/Kore/Reachability/Claim.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs index f382475080..3639bab4c3 100644 --- a/kore/src/Kore/Reachability/Claim.hs +++ b/kore/src/Kore/Reachability/Claim.hs @@ -590,8 +590,11 @@ simplify' :: Strategy.TransitionT (AppliedRule claim) m claim simplify' lensClaimPattern claim = do claim' <- simplifyLeftHandSide claim - let sideCondition = extractSideCondition claim' - simplifyRightHandSide lensClaimPattern sideCondition claim' + let substitution = Pattern.substitution $ claim' Lens.^. lensClaimPattern.field @"left" + sideCondition = extractSideCondition claim' + noLeftSubst = claim' & lensClaimPattern.field @"left".field @"substitution" Lens..~ mempty + appliedSubst = noLeftSubst & lensClaimPattern Lens.%~ ClaimPattern.applySubstitution substitution + simplifyRightHandSide lensClaimPattern sideCondition appliedSubst where extractSideCondition = SideCondition.fromConditionWithReplacements From 785bb8a8e6b229ecacf44c9fd6681cc1a08a30fd Mon Sep 17 00:00:00 2001 From: JKTKops Date: Fri, 23 Jul 2021 15:55:22 +0000 Subject: [PATCH 2/5] Update tests, new integration test --- kore/src/Kore/Reachability/Claim.hs | 14 +++++++++----- .../Test/Kore/Reachability/OnePathStrategy.hs | 2 +- kore/test/Test/Kore/Reachability/Prove.hs | 2 +- test/issue-2740/Makefile | 2 ++ test/issue-2740/either-spec.k | 7 +++++++ test/issue-2740/either-spec.k.out.golden | 1 + test/issue-2740/either.k | 18 ++++++++++++++++++ 7 files changed, 39 insertions(+), 7 deletions(-) create mode 100644 test/issue-2740/Makefile create mode 100644 test/issue-2740/either-spec.k create mode 100644 test/issue-2740/either-spec.k.out.golden create mode 100644 test/issue-2740/either.k diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs index 3639bab4c3..e1d42bb69e 100644 --- a/kore/src/Kore/Reachability/Claim.hs +++ b/kore/src/Kore/Reachability/Claim.hs @@ -590,12 +590,16 @@ simplify' :: Strategy.TransitionT (AppliedRule claim) m claim simplify' lensClaimPattern claim = do claim' <- simplifyLeftHandSide claim - let substitution = Pattern.substitution $ claim' Lens.^. lensClaimPattern.field @"left" - sideCondition = extractSideCondition claim' - noLeftSubst = claim' & lensClaimPattern.field @"left".field @"substitution" Lens..~ mempty - appliedSubst = noLeftSubst & lensClaimPattern Lens.%~ ClaimPattern.applySubstitution substitution - simplifyRightHandSide lensClaimPattern sideCondition appliedSubst + let claim'' = Lens.over lensClaimPattern applySubstOnRightHandSide claim' + sideCondition = extractSideCondition claim'' + simplifyRightHandSide lensClaimPattern sideCondition claim'' where + applySubstOnRightHandSide claimPat = + let substitution = Pattern.substitution $ Lens.view (field @"left") claimPat + noLeftSubst = Lens.set (field @"left" . field @"substitution") mempty claimPat + appliedSubst = ClaimPattern.applySubstitution substitution noLeftSubst + in appliedSubst + extractSideCondition = SideCondition.fromConditionWithReplacements . Pattern.withoutTerm diff --git a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs index 38715883a2..5a534589ad 100644 --- a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs +++ b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs @@ -810,7 +810,7 @@ test_onePathStrategy = left' = Pattern.withCondition Mock.a - (Condition.assign (inject Mock.x) Mock.a) + (Condition.assign (inject Mock.x) Mock.a){ substitution = mempty } right = Pattern.withCondition (TermLike.mkElemVar Mock.x) diff --git a/kore/test/Test/Kore/Reachability/Prove.hs b/kore/test/Test/Kore/Reachability/Prove.hs index f645e7d394..26c40b67ef 100644 --- a/kore/test/Test/Kore/Reachability/Prove.hs +++ b/kore/test/Test/Kore/Reachability/Prove.hs @@ -428,7 +428,7 @@ test_proveClaims = ) , Pattern.withCondition Mock.b - (Condition.assign (inject Mock.x) Mock.a) + (Condition.assign (inject Mock.x) Mock.a){ Condition.substitution = mempty } ] initialPattern = Pattern.fromTermLike diff --git a/test/issue-2740/Makefile b/test/issue-2740/Makefile new file mode 100644 index 0000000000..a72c5f37d2 --- /dev/null +++ b/test/issue-2740/Makefile @@ -0,0 +1,2 @@ +DEF = either +include $(CURDIR)/../include.mk \ No newline at end of file diff --git a/test/issue-2740/either-spec.k b/test/issue-2740/either-spec.k new file mode 100644 index 0000000000..68054942ef --- /dev/null +++ b/test/issue-2740/either-spec.k @@ -0,0 +1,7 @@ +module EITHER-SPEC + imports EITHER + + claim run(E,I) => done(E) ... + requires I >Int 0 + ensures P(E,I) +endmodule diff --git a/test/issue-2740/either-spec.k.out.golden b/test/issue-2740/either-spec.k.out.golden new file mode 100644 index 0000000000..17a1d4510e --- /dev/null +++ b/test/issue-2740/either-spec.k.out.golden @@ -0,0 +1 @@ +#Top diff --git a/test/issue-2740/either.k b/test/issue-2740/either.k new file mode 100644 index 0000000000..848615f4e8 --- /dev/null +++ b/test/issue-2740/either.k @@ -0,0 +1,18 @@ +module EITHER + imports INT + + syntax KItem ::= run ( Either, Int ) | done ( Either ) + rule run(Left(), _I) => done(Left()) + rule run(Right(), _I) => done(Right()) + + syntax Either ::= Left() | Right() + syntax Bool ::= P( Either , Int ) [function] + + rule P(Left(),I) => true + requires I >Int 0 + rule P(Right(),I) => true + requires I >Int 0 + rule P(_E,I) => false + requires I <=Int 0 + +endmodule From 549ced4316bb840539b19165a2e5b3c602026a6d Mon Sep 17 00:00:00 2001 From: github-actions Date: Fri, 23 Jul 2021 15:57:44 +0000 Subject: [PATCH 3/5] Format with fourmolu --- kore/src/Kore/Reachability/Claim.hs | 2 +- kore/test/Test/Kore/Reachability/OnePathStrategy.hs | 2 +- kore/test/Test/Kore/Reachability/Prove.hs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs index e1d42bb69e..0282de8453 100644 --- a/kore/src/Kore/Reachability/Claim.hs +++ b/kore/src/Kore/Reachability/Claim.hs @@ -598,7 +598,7 @@ simplify' lensClaimPattern claim = do let substitution = Pattern.substitution $ Lens.view (field @"left") claimPat noLeftSubst = Lens.set (field @"left" . field @"substitution") mempty claimPat appliedSubst = ClaimPattern.applySubstitution substitution noLeftSubst - in appliedSubst + in appliedSubst extractSideCondition = SideCondition.fromConditionWithReplacements diff --git a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs index 5a534589ad..2ea21621e8 100644 --- a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs +++ b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs @@ -810,7 +810,7 @@ test_onePathStrategy = left' = Pattern.withCondition Mock.a - (Condition.assign (inject Mock.x) Mock.a){ substitution = mempty } + (Condition.assign (inject Mock.x) Mock.a){substitution = mempty} right = Pattern.withCondition (TermLike.mkElemVar Mock.x) diff --git a/kore/test/Test/Kore/Reachability/Prove.hs b/kore/test/Test/Kore/Reachability/Prove.hs index 26c40b67ef..350b050268 100644 --- a/kore/test/Test/Kore/Reachability/Prove.hs +++ b/kore/test/Test/Kore/Reachability/Prove.hs @@ -428,7 +428,7 @@ test_proveClaims = ) , Pattern.withCondition Mock.b - (Condition.assign (inject Mock.x) Mock.a){ Condition.substitution = mempty } + (Condition.assign (inject Mock.x) Mock.a){Condition.substitution = mempty} ] initialPattern = Pattern.fromTermLike From 39d414a450c3236af23c07ca4ae7df14bc9c7a30 Mon Sep 17 00:00:00 2001 From: JKTKops Date: Mon, 26 Jul 2021 17:09:27 +0000 Subject: [PATCH 4/5] update integration tests that output affected configs --- test/issue-2221/test-issue-2221.sh.out.golden | 37 +- test/issue-2244/test-issue-2244.sh.out.golden | 316 ++++++++---------- test/issue-2740/either-spec.k | 10 +- test/issue-2740/either.k | 4 - 4 files changed, 162 insertions(+), 205 deletions(-) diff --git a/test/issue-2221/test-issue-2221.sh.out.golden b/test/issue-2221/test-issue-2221.sh.out.golden index f438df9b12..04dba5204f 100644 --- a/test/issue-2221/test-issue-2221.sh.out.golden +++ b/test/issue-2221/test-issue-2221.sh.out.golden @@ -1,33 +1,10 @@ -/* Created: Kore.Internal.OrPattern.toTermLike */ -/* Spa */ -\and{SortGeneratedTopCell{}}( +/* Fl Fn D Sfa */ +Lbl'-LT-'generatedTop'-GT-'{}( + /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), /* Fl Fn D Sfa */ - Lbl'-LT-'generatedTop'-GT-'{}( - /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), - /* Fl Fn D Sfa */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{} - ), - /* Fl Fn D Sfa Cl */ - Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")) + Lbl'-LT-'generatedCounter'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{} ), - /* Spa */ - \and{SortGeneratedTopCell{}}( - /* Spa */ - \equals{SortMyList{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa */ Var'Unds'0:SortMyList{}, - /* Fl Fn D Sfa */ - Lbl'UndsUndsUnds'LIST-SIZER-SYNTAX'Unds'MyList'Unds'Int'Unds'MyList{}( - /* Fl Fn D Sfa */ Var'Unds'E:SortInt{}, - /* Fl Fn D Sfa Cl */ - Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}() - ) - ), - /* Spa */ - \equals{SortMyList{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa */ VarL:SortMyList{}, - /* Fl Fn D Sfa Cl */ - Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}() - ) - ) + /* Fl Fn D Sfa Cl */ + Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")) ) \ No newline at end of file diff --git a/test/issue-2244/test-issue-2244.sh.out.golden b/test/issue-2244/test-issue-2244.sh.out.golden index e3bd16b3c9..11476beae5 100644 --- a/test/issue-2244/test-issue-2244.sh.out.golden +++ b/test/issue-2244/test-issue-2244.sh.out.golden @@ -1,202 +1,178 @@ /* Created: Kore.Internal.OrPattern.toTermLike */ /* Spa */ \and{SortGeneratedTopCell{}}( - /* Created: Kore.Internal.OrPattern.toTermLike */ - /* Spa */ - \and{SortGeneratedTopCell{}}( + /* Fl Fn D Sfa */ + Lbl'-LT-'generatedTop'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'generatedTop'-GT-'{}( + Lbl'-LT-'michelsonTop'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'michelsonTop'-GT-'{}( - /* Fl Fn D Sfa */ - Lbl'-LT-'paramtype'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'24:SortPreType{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'paramvalue'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'25:SortPreData{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'storagetype'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'26:SortPreType{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'storagevalue'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'27:SortPreData{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'mybalance'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'28:SortMutez{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'myamount'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'29:SortMutez{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'mynow'-GT-'{}( - /* Fl Fn D Sfa */ - Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( - /* Fl Fn D Sfa */ Var'Unds'30:SortInt{} - ) - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'myaddr'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'31:SortAddress{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'knownaddrs'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'32:SortMap{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'sourceaddr'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'33:SortAddress{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'senderaddr'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'34:SortAddress{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'mychainid'-GT-'{}( - /* Fl Fn D Sfa */ - Lbl'Hash'ChainId'LParUndsRParUnds'MICHELSON-COMMON'Unds'ChainId'Unds'MichelsonBytes{}( - /* Fl Fn D Sfa */ Var'Unds'35:SortMichelsonBytes{} - ) - ), + Lbl'-LT-'paramtype'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'24:SortPreType{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'paramvalue'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'25:SortPreData{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'storagetype'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'26:SortPreType{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'storagevalue'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'27:SortPreData{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'mybalance'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'28:SortMutez{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'myamount'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'29:SortMutez{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'mynow'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'nonce'-GT-'{}( - /* Fl Fn D Sfa */ - Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( - /* Fl Fn D Sfa */ Var'Unds'36:SortInt{} - ) - ), + Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( + /* Fl Fn D Sfa */ Var'Unds'30:SortInt{} + ) + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'myaddr'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'31:SortAddress{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'knownaddrs'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'32:SortMap{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'sourceaddr'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'33:SortAddress{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'senderaddr'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'34:SortAddress{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'mychainid'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'bigmaps'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'37:SortMap{} - ), + Lbl'Hash'ChainId'LParUndsRParUnds'MICHELSON-COMMON'Unds'ChainId'Unds'MichelsonBytes{}( + /* Fl Fn D Sfa */ Var'Unds'35:SortMichelsonBytes{} + ) + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'nonce'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'script'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'38:SortPreData{} - ), - /* Fl Fn D Sfa Cl */ - Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), + Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( + /* Fl Fn D Sfa */ Var'Unds'36:SortInt{} + ) + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'bigmaps'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'37:SortMap{}), + /* Fl Fn D Sfa */ + Lbl'-LT-'script'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'38:SortPreData{} + ), + /* Fl Fn D Sfa Cl */ + Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), + /* Fl Fn D Sfa */ + Lbl'-LT-'stack'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'stack'-GT-'{}( + /* Inj: */ inj{SortStack{}, SortInternalStack{}}( /* Fl Fn D Sfa */ - /* Inj: */ inj{SortStack{}, SortInternalStack{}}( + Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}( /* Fl Fn D Sfa */ - Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}( + Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}( + /* Fl Fn D Sfa Cli */ + /* Inj: */ inj{SortNumTypeName{}, SortTypeName{}}( + /* Fl Fn D Sfa Cl */ + Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}() + ), /* Fl Fn D Sfa */ - Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}( - /* Fl Fn D Sfa Cli */ - /* Inj: */ inj{SortNumTypeName{}, SortTypeName{}}( - /* Fl Fn D Sfa Cl */ - Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}() - ), + /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa */ - /* Inj: */ inj{SortInt{}, SortData{}}( + Lbl'UndsPlus'Int'Unds'{}( /* Fl Fn D Sfa */ - Lbl'UndsPlus'Int'Unds'{}( - /* Fl Fn D Sfa */ - Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( - /* Fl Fn D Sfa */ - VarL:SortInternalList{}, - /* Fl Fn D Sfa Cl */ - \dv{SortInt{}}("0") - ), + Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( /* Fl Fn D Sfa */ - Lbl'UndsPlus'Int'Unds'{}( - /* Fl Fn D Sfa */ VarI:SortInt{}, - /* Fl Fn D Sfa Cl */ - \dv{SortInt{}}("1") - ) + VarL:SortInternalList{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") + ), + /* Fl Fn D Sfa */ + Lbl'UndsPlus'Int'Unds'{}( + /* Fl Fn D Sfa */ VarI:SortInt{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) - ), - /* Fl Fn D Sfa Cl */ - Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}() - ) - ) - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'inputstack'-GT-'{}( - /* Fl Fn D Sfa */ - Lbl'LBraUndsRBraUnds'UNIT-TEST-COMMON-SYNTAX'Unds'LiteralStack'Unds'StackElementList{}( - /* Fl Fn D Sfa */ Var'Unds'39:SortStackElementList{} + ) + ), + /* Fl Fn D Sfa Cl */ + Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}() ) - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'expected'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'40:SortOutputStack{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'pre'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'41:SortBlockList{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'post'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'42:SortBlockList{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'invs'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'43:SortMap{}), - /* Fl Fn D Sfa */ - Lbl'-LT-'symbols'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'44:SortMap{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'returncode'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'45:SortInt{} - ), - /* Fl Fn D Sfa */ - Lbl'-LT-'assumeFailed'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'46:SortBool{} - ), + ) + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'inputstack'-GT-'{}( /* Fl Fn D Sfa */ - Lbl'-LT-'trace'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'47:SortK{}) + Lbl'LBraUndsRBraUnds'UNIT-TEST-COMMON-SYNTAX'Unds'LiteralStack'Unds'StackElementList{}( + /* Fl Fn D Sfa */ Var'Unds'39:SortStackElementList{} + ) ), /* Fl Fn D Sfa */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{} - ) + Lbl'-LT-'expected'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'40:SortOutputStack{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'pre'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'41:SortBlockList{}), + /* Fl Fn D Sfa */ + Lbl'-LT-'post'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'42:SortBlockList{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'invs'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'43:SortMap{}), + /* Fl Fn D Sfa */ + Lbl'-LT-'symbols'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'44:SortMap{}), + /* Fl Fn D Sfa */ + Lbl'-LT-'returncode'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'45:SortInt{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'assumeFailed'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'46:SortBool{} + ), + /* Fl Fn D Sfa */ + Lbl'-LT-'trace'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'47:SortK{}) ), + /* Fl Fn D Sfa */ + Lbl'-LT-'generatedCounter'-GT-'{}( + /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{} + ) + ), + /* Sfa */ + \not{SortGeneratedTopCell{}}( /* Sfa */ - \not{SortGeneratedTopCell{}}( - /* Sfa */ - \equals{SortInt{}, SortGeneratedTopCell{}}( + \equals{SortInt{}, SortGeneratedTopCell{}}( + /* Fl Fn D Sfa */ + Lbl'UndsPlus'Int'Unds'{}( /* Fl Fn D Sfa */ - Lbl'UndsPlus'Int'Unds'{}( - /* Fl Fn D Sfa */ - Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( - /* Fl Fn D Sfa */ VarL:SortInternalList{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* Fl Fn D Sfa */ - Lbl'UndsPlus'Int'Unds'{}( - /* Fl Fn D Sfa */ VarI:SortInt{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") - ) + Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( + /* Fl Fn D Sfa */ VarL:SortInternalList{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa */ Lbl'UndsPlus'Int'Unds'{}( - /* Fl Fn D Sfa */ - Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( - /* Fl Fn D Sfa */ VarL:SortInternalList{}, - /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") - ), - /* Fl Fn D Sfa */ VarI:SortInt{} + /* Fl Fn D Sfa */ VarI:SortInt{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) - ) - ) - ), - /* Spa */ - \equals{SortInternalList{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa */ VarIntList:SortInternalList{}, - /* Fl Fn D Sfa */ - Lbl'UndsSClnSClnUndsUnds'MICHELSON-COMMON'Unds'InternalList'Unds'WrappedData'Unds'InternalList{}( - /* Fl Fn D Sfa */ - Lbl'LSqBUndsRSqBUnds'MICHELSON-COMMON'Unds'WrappedData'Unds'Data{}( - /* Fl Fn D Sfa */ VarE:SortData{} ), - /* Fl Fn D Sfa */ VarL:SortInternalList{} + /* Fl Fn D Sfa */ + Lbl'UndsPlus'Int'Unds'{}( + /* Fl Fn D Sfa */ + Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( + /* Fl Fn D Sfa */ VarL:SortInternalList{}, + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") + ), + /* Fl Fn D Sfa */ VarI:SortInt{} + ) ) ) ) \ No newline at end of file diff --git a/test/issue-2740/either-spec.k b/test/issue-2740/either-spec.k index 68054942ef..95780a818c 100644 --- a/test/issue-2740/either-spec.k +++ b/test/issue-2740/either-spec.k @@ -1,6 +1,14 @@ -module EITHER-SPEC +module VERIFICATION imports EITHER + syntax KItem ::= run ( Either, Int ) | done ( Either ) + rule run(Left(), _I) => done(Left()) + rule run(Right(), _I) => done(Right()) +endmodule + +module EITHER-SPEC + imports VERIFICATION + claim run(E,I) => done(E) ... requires I >Int 0 ensures P(E,I) diff --git a/test/issue-2740/either.k b/test/issue-2740/either.k index 848615f4e8..5c4682eb01 100644 --- a/test/issue-2740/either.k +++ b/test/issue-2740/either.k @@ -1,10 +1,6 @@ module EITHER imports INT - syntax KItem ::= run ( Either, Int ) | done ( Either ) - rule run(Left(), _I) => done(Left()) - rule run(Right(), _I) => done(Right()) - syntax Either ::= Left() | Right() syntax Bool ::= P( Either , Int ) [function] From 4d10db3fb5c0b7a59c8ababfa630ed968d9e0a92 Mon Sep 17 00:00:00 2001 From: JKTKops Date: Tue, 27 Jul 2021 14:55:15 +0000 Subject: [PATCH 5/5] simplify construction of Patterns in tests --- kore/test/Test/Kore/Reachability/OnePathStrategy.hs | 4 +--- kore/test/Test/Kore/Reachability/Prove.hs | 4 +--- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs index 2ea21621e8..b629938ee0 100644 --- a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs +++ b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs @@ -808,9 +808,7 @@ test_onePathStrategy = ) ) left' = - Pattern.withCondition - Mock.a - (Condition.assign (inject Mock.x) Mock.a){substitution = mempty} + Pattern.fromTermLike Mock.a right = Pattern.withCondition (TermLike.mkElemVar Mock.x) diff --git a/kore/test/Test/Kore/Reachability/Prove.hs b/kore/test/Test/Kore/Reachability/Prove.hs index 350b050268..0c2b3eea76 100644 --- a/kore/test/Test/Kore/Reachability/Prove.hs +++ b/kore/test/Test/Kore/Reachability/Prove.hs @@ -426,9 +426,7 @@ test_proveClaims = ) ) ) - , Pattern.withCondition - Mock.b - (Condition.assign (inject Mock.x) Mock.a){Condition.substitution = mempty} + , Pattern.fromTermLike Mock.b ] initialPattern = Pattern.fromTermLike