diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index b7a032ddc8..8418a67aad 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -94,6 +94,10 @@ import Kore.IndexedModule.IndexedModule import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools ( build ) +import Kore.Internal.MultiAnd + ( MultiAnd + ) +import qualified Kore.Internal.MultiAnd as MultiAnd import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Conditional (..) @@ -137,8 +141,10 @@ import Kore.Parser , parseKorePattern ) import Kore.Reachability - ( ProofStuck (..) + ( ProveClaimsResult (..) , SomeClaim + , StuckClaim (..) + , getConfiguration ) import qualified Kore.Reachability.Claim as Claim import Kore.Rewriting.RewritingVariable @@ -161,6 +167,9 @@ import Kore.Syntax.Definition , Sentence (..) ) import qualified Kore.Syntax.Definition as Definition.DoNotUse +import Kore.TopBottom + ( isTop + ) import Kore.Unparser ( unparse ) @@ -648,18 +657,20 @@ koreProve execOptions proveOptions = do specModule maybeAlreadyProvenModule - (exitCode, final) <- case proveResult of - Left ProofStuck { stuckPatterns, provenClaims } -> do - maybe - (return ()) - (lift . saveProven specModule provenClaims) - saveProofs + let ProveClaimsResult { stuckClaims, provenClaims } = proveResult + let (exitCode, final) + | noStuckClaims = success + | otherwise = stuckPatterns - & OrPattern.toTermLike - & failure - & return - Right () -> return success - + & OrPattern.toTermLike + & failure + where + noStuckClaims = isTop stuckClaims + stuckPatterns = + OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims) + getStuckConfig = + getRewritingPattern . getConfiguration . getStuckClaim + lift $ Foldable.for_ saveProofs $ saveProven specModule provenClaims lift $ renderResult execOptions (unparse final) return exitCode where @@ -685,10 +696,10 @@ koreProve execOptions proveOptions = do saveProven :: VerifiedModule StepperAttributes - -> [SomeClaim] + -> MultiAnd SomeClaim -> FilePath -> IO () - saveProven specModule provenClaims outputFile = + saveProven specModule (Foldable.toList -> provenClaims) outputFile = withFile outputFile WriteMode (`hPutDoc` unparse provenDefinition) where diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index ecf1542c5d..76c79fe365 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -38,9 +38,6 @@ import Control.Monad import Control.Monad.Catch ( MonadMask ) -import Control.Monad.Trans.Except - ( runExceptT - ) import Data.Coerce ( coerce ) @@ -106,7 +103,7 @@ import Kore.Reachability ( AllClaims (AllClaims) , AlreadyProven (AlreadyProven) , Axioms (Axioms) - , ProofStuck (..) + , ProveClaimsResult (..) , Rule (ReachabilityRewriteRule) , SomeClaim (..) , ToProve (ToProve) @@ -383,7 +380,7 @@ prove -- ^ The spec module -> Maybe (VerifiedModule StepperAttributes) -- ^ The module containing the claims that were proven in a previous run. - -> smt (Either ProofStuck ()) + -> smt ProveClaimsResult prove searchOrder breadthLimit @@ -410,7 +407,6 @@ prove (extractUntrustedClaims' claims) ) ) - & runExceptT where extractUntrustedClaims' :: [SomeClaim] -> [SomeClaim] extractUntrustedClaims' = filter (not . isTrusted) diff --git a/kore/src/Kore/Reachability.hs b/kore/src/Kore/Reachability.hs index c266b422f9..ab16e71217 100644 --- a/kore/src/Kore/Reachability.hs +++ b/kore/src/Kore/Reachability.hs @@ -6,10 +6,14 @@ License : NCSA module Kore.Reachability ( AllPathClaim (..) + , mkAllPathClaim , allPathRuleToTerm , OnePathClaim (..) + , mkOnePathClaim , onePathRuleToTerm , SomeClaim (..) + , mkSomeClaimAllPath + , mkSomeClaimOnePath , makeTrusted , lensClaimPattern , getConfiguration diff --git a/kore/src/Kore/Reachability/AllPathClaim.hs b/kore/src/Kore/Reachability/AllPathClaim.hs index 38bcd26d4d..5e489e9652 100644 --- a/kore/src/Kore/Reachability/AllPathClaim.hs +++ b/kore/src/Kore/Reachability/AllPathClaim.hs @@ -6,6 +6,7 @@ License : NCSA module Kore.Reachability.AllPathClaim ( AllPathClaim (..) + , mkAllPathClaim , allPathRuleToTerm , Rule (..) ) where @@ -29,10 +30,17 @@ import Kore.Debug import Kore.Internal.Alias ( Alias (aliasConstructor) ) +import Kore.Internal.OrPattern + ( OrPattern + ) +import Kore.Internal.Pattern + ( Pattern + ) import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.TermLike - ( Id (getId) + ( ElementVariable + , Id (getId) , TermLike , VariableName , weakAlwaysFinally @@ -71,6 +79,14 @@ newtype AllPathClaim = deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) deriving anyclass (Debug, Diff) +mkAllPathClaim + :: Pattern RewritingVariableName + -> OrPattern RewritingVariableName + -> [ElementVariable RewritingVariableName] + -> AllPathClaim +mkAllPathClaim left right existentials = + AllPathClaim (mkClaimPattern left right existentials) + instance Unparse AllPathClaim where unparse claimPattern' = unparse $ allPathRuleToTerm claimPattern' diff --git a/kore/src/Kore/Reachability/OnePathClaim.hs b/kore/src/Kore/Reachability/OnePathClaim.hs index e43829fbfb..22db7803e2 100644 --- a/kore/src/Kore/Reachability/OnePathClaim.hs +++ b/kore/src/Kore/Reachability/OnePathClaim.hs @@ -7,6 +7,7 @@ License : NCSA module Kore.Reachability.OnePathClaim ( OnePathClaim (..) , onePathRuleToTerm + , mkOnePathClaim , Rule (..) ) where @@ -26,10 +27,17 @@ import Kore.Debug import Kore.Internal.Alias ( Alias (aliasConstructor) ) +import Kore.Internal.OrPattern + ( OrPattern + ) +import Kore.Internal.Pattern + ( Pattern + ) import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.TermLike - ( Id (getId) + ( ElementVariable + , Id (getId) , TermLike , VariableName , weakExistsFinally @@ -76,6 +84,14 @@ onePathRuleToTerm :: OnePathClaim -> TermLike VariableName onePathRuleToTerm (OnePathClaim claimPattern') = claimPatternToTerm TermLike.WEF claimPattern' +mkOnePathClaim + :: Pattern RewritingVariableName + -> OrPattern RewritingVariableName + -> [ElementVariable RewritingVariableName] + -> OnePathClaim +mkOnePathClaim left right existentials = + OnePathClaim (mkClaimPattern left right existentials) + instance Unparse OnePathClaim where unparse claimPattern' = unparse $ onePathRuleToTerm claimPattern' diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index f78b9eef52..b0c2da4e8e 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -8,7 +8,9 @@ This should be imported qualified. module Kore.Reachability.Prove ( CommonClaimState - , ProofStuck (..) + , ProveClaimsResult (..) + , StuckClaim (..) + , StuckClaims , AllClaims (..) , Axioms (..) , ToProve (..) @@ -27,9 +29,6 @@ import qualified Control.Lens as Lens import Control.Monad ( (>=>) ) -import qualified Control.Monad as Monad - ( foldM_ - ) import Control.Monad.Catch ( MonadCatch , MonadMask @@ -39,9 +38,15 @@ import Control.Monad.Catch ) import Control.Monad.Except ( ExceptT - , withExceptT + , MonadError + , runExceptT ) import qualified Control.Monad.Except as Monad.Except +import Control.Monad.State.Strict + ( StateT + , runStateT + ) +import qualified Control.Monad.State.Strict as State import Data.Coerce ( coerce ) @@ -68,10 +73,10 @@ import Kore.Debug import Kore.Internal.Conditional ( Conditional (..) ) -import Kore.Internal.OrPattern - ( OrPattern +import Kore.Internal.MultiAnd + ( MultiAnd ) -import qualified Kore.Internal.OrPattern as OrPattern +import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.Pattern ( Pattern ) @@ -121,7 +126,7 @@ import Kore.Step.Transition ( runTransitionT ) import qualified Kore.Step.Transition as Transition -import Kore.Syntax.Variable +import Kore.TopBottom import Kore.Unparser import Log ( MonadLog (..) @@ -160,31 +165,36 @@ The action may throw an exception if the proof fails; the exception is a single @'Pattern' 'VariableName'@, the first unprovable configuration. -} -type Verifier m = ExceptT (OrPattern VariableName) m - -{- | Verifies a set of claims. When it verifies a certain claim, after the -first step, it also uses the claims as axioms (i.e. it does coinductive proofs). +type VerifierT = ExceptT StuckClaims -If the verification fails, returns an error containing a pattern that could -not be rewritten (either because no axiom could be applied or because we -didn't manage to verify a claim within the its maximum number of steps). +newtype AllClaims claim = AllClaims {getAllClaims :: [claim]} +newtype Axioms claim = Axioms {getAxioms :: [Rule claim]} +newtype ToProve claim = ToProve {getToProve :: [(claim, Limit Natural)]} +newtype AlreadyProven = AlreadyProven {getAlreadyProven :: [Text]} -If the verification succeeds, it returns (). --} -data ProofStuck = - ProofStuck - { stuckPatterns :: !(OrPattern VariableName) - , provenClaims :: ![SomeClaim] - } +newtype StuckClaim = StuckClaim { getStuckClaim :: SomeClaim } deriving (Eq, Ord, Show) deriving (GHC.Generic) deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) deriving anyclass (Debug, Diff) -newtype AllClaims claim = AllClaims {getAllClaims :: [claim]} -newtype Axioms claim = Axioms {getAxioms :: [Rule claim]} -newtype ToProve claim = ToProve {getToProve :: [(claim, Limit Natural)]} -newtype AlreadyProven = AlreadyProven {getAlreadyProven :: [Text]} +instance TopBottom StuckClaim where + isTop = const False + isBottom = const False + +type StuckClaims = MultiAnd StuckClaim + +type ProvenClaims = MultiAnd SomeClaim + +-- | The result of proving some claims. +data ProveClaimsResult = + ProveClaimsResult + { stuckClaims :: !StuckClaims + -- ^ The conjuction of stuck claims, that is: of claims which must still be + -- proven. If all claims were proved, then the remaining claims are @\\top@. + , provenClaims :: !ProvenClaims + -- ^ The conjunction of all claims which were proven. + } proveClaims :: forall simplifier @@ -199,7 +209,7 @@ proveClaims -> ToProve SomeClaim -- ^ List of claims, together with a maximum number of verification steps -- for each. - -> ExceptT ProofStuck simplifier () + -> simplifier ProveClaimsResult proveClaims breadthLimit searchOrder @@ -207,9 +217,15 @@ proveClaims axioms (AlreadyProven alreadyProven) (ToProve toProve) - = - proveClaimsWorker breadthLimit searchOrder claims axioms unproven - & withExceptT addStillProven + = do + (result, provenClaims) <- + proveClaimsWorker breadthLimit searchOrder claims axioms unproven + & runExceptT + & flip runStateT (MultiAnd.make stillProven) + pure ProveClaimsResult + { stuckClaims = either id (const MultiAnd.top) result + , provenClaims + } where unproven :: ToProve SomeClaim stillProven :: [SomeClaim] @@ -226,10 +242,6 @@ proveClaims then Right rule else Left claim - addStillProven :: ProofStuck -> ProofStuck - addStillProven stuck@ProofStuck { provenClaims } = - stuck { provenClaims = stillProven ++ provenClaims } - proveClaimsWorker :: forall simplifier . MonadSimplify simplifier @@ -242,22 +254,19 @@ proveClaimsWorker -> ToProve SomeClaim -- ^ List of claims, together with a maximum number of verification steps -- for each. - -> ExceptT ProofStuck simplifier () + -> ExceptT StuckClaims (StateT ProvenClaims simplifier) () proveClaimsWorker breadthLimit searchOrder claims axioms (ToProve toProve) = - Monad.foldM_ verifyWorker [] toProve + Foldable.traverse_ verifyWorker toProve where verifyWorker - :: [SomeClaim] - -> (SomeClaim, Limit Natural) - -> ExceptT ProofStuck simplifier [SomeClaim] - verifyWorker provenClaims unprovenClaim@(claim, _) = - withExceptT wrapStuckPattern $ do - proveClaim breadthLimit searchOrder claims axioms unprovenClaim - return (claim : provenClaims) - where - wrapStuckPattern :: OrPattern VariableName -> ProofStuck - wrapStuckPattern stuckPatterns = - ProofStuck { stuckPatterns, provenClaims } + :: (SomeClaim, Limit Natural) + -> ExceptT StuckClaims (StateT ProvenClaims simplifier) () + verifyWorker unprovenClaim@(claim, _) = do + proveClaim breadthLimit searchOrder claims axioms unprovenClaim + addProvenClaim claim + + addProvenClaim claim = + State.modify' (mappend (MultiAnd.singleton claim)) proveClaim :: forall simplifier @@ -269,7 +278,7 @@ proveClaim -> AllClaims SomeClaim -> Axioms SomeClaim -> (SomeClaim, Limit Natural) - -> ExceptT (OrPattern VariableName) simplifier () + -> ExceptT StuckClaims simplifier () proveClaim breadthLimit searchOrder @@ -300,16 +309,11 @@ proveClaim handleLimitExceeded :: Strategy.LimitExceeded (ProofDepth, CommonClaimState) - -> Verifier simplifier a - handleLimitExceeded (Strategy.LimitExceeded states) = - let finalPattern = - ClaimState.claimState lhsClaimStateTransformer . snd - <$> states - in - Monad.Except.throwError - . OrPattern.map getRewritingPattern - . OrPattern.fromPatterns - $ finalPattern + -> VerifierT simplifier a + handleLimitExceeded (Strategy.LimitExceeded states) = do + let extractStuckClaim = fmap StuckClaim . extractUnproven . snd + stuckClaims = mapMaybe extractStuckClaim states + Monad.Except.throwError (MultiAnd.make $ Foldable.toList stuckClaims) updateQueue = \as -> Strategy.unfoldSearchOrder searchOrder as @@ -322,16 +326,15 @@ proveClaim genericLength = fromIntegral . length throwUnproven - :: LogicT (Verifier simplifier) (ProofDepth, CommonClaimState) - -> Verifier simplifier [ProofDepth] + :: LogicT (VerifierT simplifier) (ProofDepth, CommonClaimState) + -> VerifierT simplifier [ProofDepth] throwUnproven acts = do (proofDepth, proofState) <- acts let maybeUnproven = extractUnproven proofState Foldable.for_ maybeUnproven $ \unproven -> do infoUnprovenDepth proofDepth - Monad.Except.throwError . OrPattern.fromPattern - $ (getRewritingPattern . getConfiguration) unproven + throwStuckClaim unproven pure proofDepth & Logic.observeAllT @@ -467,23 +470,24 @@ checkStuckConfiguration rule prim proofState = do isNot_Ceil_ (Not_ _ (Ceil_ _ _ _)) = True isNot_Ceil_ _ = False +throwStuckClaim :: MonadError StuckClaims m => SomeClaim -> m x +throwStuckClaim = Monad.Except.throwError . MultiAnd.singleton . StuckClaim + {- | Terminate the prover at the first stuck step. -} throwStuckClaims :: forall m rule . MonadLog m - => TransitionRule (Verifier m) rule + => TransitionRule (VerifierT m) rule (ProofDepth, ClaimState SomeClaim) - -> TransitionRule (Verifier m) rule + -> TransitionRule (VerifierT m) rule (ProofDepth, ClaimState SomeClaim) throwStuckClaims rule prim state = do state'@(proofDepth', proofState') <- rule prim state case proofState' of ClaimState.Stuck unproven -> do infoUnprovenDepth proofDepth' - Monad.Except.throwError $ OrPattern.fromPattern config - where - config = getConfiguration unproven & getRewritingPattern + throwStuckClaim unproven _ -> return state' {- | Modify a 'TransitionRule' to track the depth of a proof. diff --git a/kore/src/Kore/Reachability/SomeClaim.hs b/kore/src/Kore/Reachability/SomeClaim.hs index f6827f2b1b..b60ae2a34b 100644 --- a/kore/src/Kore/Reachability/SomeClaim.hs +++ b/kore/src/Kore/Reachability/SomeClaim.hs @@ -6,6 +6,8 @@ License : NCSA module Kore.Reachability.SomeClaim ( SomeClaim (..) + , mkSomeClaimOnePath + , mkSomeClaimAllPath , makeTrusted , getConfiguration , getDestination @@ -42,7 +44,8 @@ import Kore.Internal.Pattern ( Pattern ) import Kore.Internal.TermLike - ( VariableName + ( ElementVariable + , VariableName ) import Kore.Reachability.AllPathClaim import Kore.Reachability.Claim @@ -85,6 +88,22 @@ data SomeClaim deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) deriving anyclass (Debug, Diff) +mkSomeClaimAllPath + :: Pattern RewritingVariableName + -> OrPattern RewritingVariableName + -> [ElementVariable RewritingVariableName] + -> SomeClaim +mkSomeClaimAllPath left right existentials = + AllPath (mkAllPathClaim left right existentials) + +mkSomeClaimOnePath + :: Pattern RewritingVariableName + -> OrPattern RewritingVariableName + -> [ElementVariable RewritingVariableName] + -> SomeClaim +mkSomeClaimOnePath left right existentials = + OnePath (mkOnePathClaim left right existentials) + instance Unparse SomeClaim where unparse (OnePath rule) = unparse rule unparse (AllPath rule) = unparse rule diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 8bacc6d185..e4219e0e68 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -8,7 +8,7 @@ module Kore.Step.ClaimPattern ( ClaimPattern (..) , freeVariablesLeft , freeVariablesRight - , claimPattern + , mkClaimPattern , substitute , assertRefreshed , refreshExistentials @@ -174,12 +174,12 @@ instance HasFreeVariables ClaimPattern RewritingVariableName where -- and an 'OrPattern', representing the right hand side pattern. -- The list of element variables are existentially quantified -- in the right hand side. -claimPattern +mkClaimPattern :: Pattern RewritingVariableName -> OrPattern RewritingVariableName -> [ElementVariable RewritingVariableName] -> ClaimPattern -claimPattern left right existentials = +mkClaimPattern left right existentials = ClaimPattern { left , right diff --git a/kore/test/Test/Kore/Reachability/Claim.hs b/kore/test/Test/Kore/Reachability/Claim.hs index 767067d3fe..b6dd79ca3d 100644 --- a/kore/test/Test/Kore/Reachability/Claim.hs +++ b/kore/test/Test/Kore/Reachability/Claim.hs @@ -51,7 +51,7 @@ import Kore.Rewriting.RewritingVariable ) import Kore.Step.ClaimPattern ( ClaimPattern - , claimPattern + , mkClaimPattern ) import qualified Logic @@ -268,7 +268,7 @@ mkGoal existentialVars ) = - claimPattern leftPatt rightPatts existentialVars + mkClaimPattern leftPatt rightPatts existentialVars aToB :: ClaimPattern aToB = diff --git a/kore/test/Test/Kore/Reachability/Prove.hs b/kore/test/Test/Kore/Reachability/Prove.hs index 36372b2655..886fe7a7ed 100644 --- a/kore/test/Test/Kore/Reachability/Prove.hs +++ b/kore/test/Test/Kore/Reachability/Prove.hs @@ -1,22 +1,14 @@ module Test.Kore.Reachability.Prove - ( test_reachabilityVerification + ( test_proveClaims ) where import Prelude.Kore import Test.Tasty -import qualified Control.Lens as Lens -import Control.Monad.Trans.Except - ( runExceptT - ) -import qualified Data.Bifunctor as Bifunctor import Data.Default ( def ) -import Data.Generics.Product - ( field - ) import Data.Limit ( Limit (..) ) @@ -26,13 +18,8 @@ import Numeric.Natural import qualified Kore.Attribute.Axiom as Attribute import qualified Kore.Internal.Condition as Condition -import Kore.Internal.OrPattern - ( OrPattern - ) +import qualified Kore.Internal.MultiAnd as MultiAnd import qualified Kore.Internal.OrPattern as OrPattern -import Kore.Internal.Pattern as Conditional - ( Conditional (..) - ) import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( makeEqualsPredicate @@ -45,6 +32,7 @@ import qualified Kore.Internal.TermLike as TermLike import Kore.Reachability import Kore.Rewriting.RewritingVariable ( RewritingVariableName + , mkRewritingPattern , mkRuleVariable ) import Kore.Step.ClaimPattern @@ -67,1743 +55,610 @@ import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Simplification import Test.Tasty.HUnit.Ext -test_reachabilityVerification :: [TestTree] -test_reachabilityVerification = - [ testCase "OnePath: Runs zero steps" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - (Limit 0) - [simpleAxiom Mock.a Mock.b] - [simpleOnePathClaim Mock.a Mock.b] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "AllPath: Runs zero steps" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - (Limit 0) - [simpleAxiom Mock.a Mock.b] - [simpleAllPathClaim Mock.a Mock.b] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "Mixed: Runs zero steps" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - (Limit 0) - [simpleAxiom Mock.a Mock.b] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "OnePath: Breadth limit zero" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error a - actual <- proveClaims_ - (Limit 0) - Unlimited - [simpleAxiom Mock.a Mock.b] - [simpleOnePathClaim Mock.a Mock.b] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "AllPath: Breadth limit zero" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error a - actual <- proveClaims_ - (Limit 0) - Unlimited - [simpleAxiom Mock.a Mock.b] - [simpleAllPathClaim Mock.a Mock.b] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "Mixed: Breadth limit zero" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error a - actual <- proveClaims_ - (Limit 0) - Unlimited - [simpleAxiom Mock.a Mock.b] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "OnePath: Runs one step" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error b - -- Note that the check that we have reached the destination happens - -- at the beginning of each step. At the beginning of the first step - -- the pattern is 'a', so we didn't reach our destination yet, even if - -- the rewrite transforms 'a' into 'b'. We detect the success at the - -- beginning of the second step, which does not run here. - actual <- proveClaims_ - Unlimited - (Limit 1) - [simpleAxiom Mock.a Mock.b] - [simpleOnePathClaim Mock.a Mock.b] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "AllPath: Runs one step" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error b - -- Note that the check that we have reached the destination happens - -- at the beginning of each step. At the beginning of the first step - -- the pattern is 'a', so we didn't reach our destination yet, even if - -- the rewrite transforms 'a' into 'b'. We detect the success at the - -- beginning of the second step, which does not run here. - actual <- proveClaims_ - Unlimited - (Limit 1) - [simpleAxiom Mock.a Mock.b] - [simpleAllPathClaim Mock.a Mock.b] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "Mixed: Runs one step" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: error b - -- Note that the check that we have reached the destination happens - -- at the beginning of each step. At the beginning of the first step - -- the pattern is 'a', so we didn't reach our destination yet, even if - -- the rewrite transforms 'a' into 'b'. We detect the success at the - -- beginning of the second step, which does not run here. - actual <- proveClaims_ - Unlimited - (Limit 1) - [simpleAxiom Mock.a Mock.b] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "OnePath: Identity spec" $ do - -- Axioms: [] - -- Claims: a => a - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 1) - [] - [ simpleOnePathClaim Mock.a Mock.a ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Identity spec" $ do - -- Axioms: [] - -- Claims: a => a - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 1) - [] - [ simpleAllPathClaim Mock.a Mock.a ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Identity spec" $ do - -- Axioms: [] - -- Claims: a => a - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 1) - [] - [ simpleOnePathClaim Mock.a Mock.a - , simpleAllPathClaim Mock.a Mock.a - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Distinct spec" $ do - -- Axioms: [] - -- Claims: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - Unlimited - [] - [ simpleOnePathClaim Mock.a Mock.b ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "AllPath: Distinct spec" $ do - -- Axioms: [] - -- Claims: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - Unlimited - [] - [ simpleAllPathClaim Mock.a Mock.b ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "Mixed: Distinct spec" $ do - -- Axioms: [] - -- Claims: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - Unlimited - [] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "OnePath: b or c spec" $ do - -- Axioms: a => b - -- Claims: a => b #Or c - -- Expected: success - actual <- proveClaims_ - (Limit 2) - Unlimited - [ simpleAxiom Mock.a Mock.b ] - [ simpleOnePathClaim Mock.a (mkOr Mock.b Mock.c) ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: b or c spec" $ do - -- Axioms: a => b - -- Claims: a => b #Or c - -- Expected: success - actual <- proveClaims_ - (Limit 2) - Unlimited - [ simpleAxiom Mock.a Mock.b ] - [ simpleAllPathClaim Mock.a (mkOr Mock.b Mock.c) ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: b or c spec" $ do - -- Axioms: a => b - -- Claims: a => b #Or c - -- Expected: success - actual <- proveClaims_ - (Limit 2) - Unlimited - [ simpleAxiom Mock.a Mock.b ] - [ simpleAllPathClaim Mock.a (mkOr Mock.b Mock.c) - , simpleAllPathClaim Mock.a (mkOr Mock.b Mock.c) - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Everything is provable when we have cyclic rules" $ do - -- Axioms: a => a - -- Claims: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.a ] - [ simpleOnePathClaim Mock.a Mock.b ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Everything is provable when we have cyclic rules" $ do - -- Axioms: a => a - -- Claims: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.a ] - [ simpleAllPathClaim Mock.a Mock.b ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Everything is provable when we have cyclic rules" $ do - -- Axioms: a => a - -- Claims: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.a ] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Concurrent rules" $ do - -- Axioms: - -- a => b - -- a => c - -- Claims: a => b #Or c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 2) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.a Mock.c - ] - [ simpleOnePathClaim Mock.a (mkOr Mock.b Mock.c) ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Concurrent rules" $ do - -- Axioms: - -- a => b - -- a => c - -- Claims: a => b #Or c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 2) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.a Mock.c - ] - [ simpleAllPathClaim Mock.a (mkOr Mock.b Mock.c) ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Concurrent rules" $ do - -- Axioms: - -- a => b - -- a => c - -- Claims: a => b #Or c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 2) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.a Mock.c - ] - [ simpleOnePathClaim Mock.a (mkOr Mock.b Mock.c) - , simpleOnePathClaim Mock.a (mkOr Mock.b Mock.c) - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Returns first failing claim" $ do - -- Axiom: a => b or c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 1) - [simpleAxiom Mock.a (mkOr Mock.b Mock.c)] - [simpleOnePathClaim Mock.a Mock.d] - [] - assertEqual "" - (Left . OrPattern.fromTermLike $ Mock.b) - actual - , testCase "AllPath: Returns first failing claim" $ do - -- Axiom: a => b or c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 1) - [simpleAxiom Mock.a (mkOr Mock.b Mock.c)] - [simpleAllPathClaim Mock.a Mock.d] - [] - assertEqual "" - (Left . OrPattern.fromTermLike $ Mock.b) - actual - , testCase "Mixed: Returns first failing claim" $ do - -- Axiom: a => b or c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 1) - [simpleAxiom Mock.a (mkOr Mock.b Mock.c)] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left . OrPattern.fromTermLike $ Mock.b) - actual - , testCase "OnePath: Verifies one claim" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 2) - [simpleAxiom Mock.a Mock.b] - [simpleOnePathClaim Mock.a Mock.b] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Verifies one claim" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 2) - [simpleAxiom Mock.a Mock.b] - [simpleAllPathClaim Mock.a Mock.b] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Verifies one claim" $ do - -- Axiom: a => b - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 2) - [simpleAxiom Mock.a Mock.b] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Trusted claim cannot prove itself" $ do - -- Trusted Claim: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - (Limit 4) - [] - [ simpleOnePathTrustedClaim Mock.a Mock.b - , simpleOnePathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "AllPath: Trusted claim cannot prove itself" $ do - -- Trusted Claim: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - (Limit 4) - [] - [ simpleAllPathTrustedClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "Mixed: Trusted claim cannot prove itself" $ do - -- Trusted Claim: a => b - -- Expected: error a - actual <- proveClaims_ - Unlimited - (Limit 4) - [] - [ simpleOnePathTrustedClaim Mock.a Mock.b - , simpleOnePathClaim Mock.a Mock.b - , simpleAllPathTrustedClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.a) - actual - , testCase "OnePath: Verifies one claim multiple steps" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Claim: a => c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - ] - [simpleOnePathClaim Mock.a Mock.c] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Verifies one claim multiple steps" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Claim: a => c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - ] - [simpleAllPathClaim Mock.a Mock.c] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Verifies one claim multiple steps" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Claim: a => c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - ] - [ simpleOnePathClaim Mock.a Mock.c - , simpleAllPathClaim Mock.a Mock.c - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Verifies one claim stops early" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - ] - [simpleOnePathClaim Mock.a Mock.c] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Verifies one claim stops early" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - ] - [simpleAllPathClaim Mock.a Mock.c] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Verifies one claim stops early" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - ] - [ simpleOnePathClaim Mock.a Mock.c - , simpleAllPathClaim Mock.a Mock.c - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: Verifies one claim with branching" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr11(x) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom (Mock.functionalConstr11 (mkElemVar Mock.x)) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleOnePathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" (Right ()) actual - , testCase "AllPath: Verifies one claim with branching" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr11(x) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom (Mock.functionalConstr11 (mkElemVar Mock.x)) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleAllPathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" (Right ()) actual - , testCase "Mixed: Verifies one claim with branching" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr11(x) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom (Mock.functionalConstr11 (mkElemVar Mock.x)) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleOnePathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - , simpleAllPathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" (Right ()) actual - , testCase "OnePath: Partial verification failure" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: error constr11(x) and x != a - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleOnePathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" - ( Left . OrPattern.fromPattern - $ Conditional - { term = Mock.functionalConstr11 (mkElemVar Mock.x) - , predicate = - makeNotPredicate - (makeEqualsPredicate Mock.testSort - (mkElemVar Mock.x) - Mock.a - ) - , substitution = mempty - } - ) - actual - , testCase "AllPath: Partial verification failure" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: error constr11(x) and x != a - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleAllPathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" - ( Left . OrPattern.fromPattern - $ Conditional - { term = Mock.functionalConstr11 (mkElemVar Mock.x) - , predicate = - makeNotPredicate - (makeEqualsPredicate Mock.testSort - (mkElemVar Mock.x) - Mock.a - ) - , substitution = mempty - } - ) - actual - , testCase "Mixed: Partial verification failure" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: error constr11(x) and x != a - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleOnePathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - , simpleAllPathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" - ( Left . OrPattern.fromPattern - $ Conditional - { term = Mock.functionalConstr11 (mkElemVar Mock.x) - , predicate = - makeNotPredicate - (makeEqualsPredicate Mock.testSort - (mkElemVar Mock.x) - Mock.a - ) - , substitution = mempty - } - ) - actual - , testCase "OnePath: Stops at branching because of breadth limit" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: error constr11(x) and x != a - actual <- proveClaims_ - (Limit 1) - Unlimited - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleOnePathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" - ( Left . OrPattern.fromPatterns $ - [ Pattern.withCondition - (Mock.functionalConstr11 (mkElemVar Mock.x)) - (Condition.fromPredicate - (makeNotPredicate - (makeEqualsPredicate Mock.testSort - (mkElemVar Mock.x) - Mock.a - ) +test_proveClaims :: [TestTree] +test_proveClaims = + [ testGroup "runs zero steps with depth = 0" $ + let mkTest name mkSimpleClaim = + testCase name $ do + let claim = mkSimpleClaim Mock.a Mock.b + actual <- proveClaims_ + Unlimited + (Limit 0) + [simpleAxiom Mock.a Mock.b] + [claim] + [] + let expect = MultiAnd.singleton (StuckClaim claim) + assertEqual "" expect actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "runs zero steps with breadth = 0" $ + let mkTest name mkSimpleClaim = + testCase name $ do + let claim = mkSimpleClaim Mock.a Mock.b + actual <- proveClaims_ + (Limit 0) + Unlimited + [simpleAxiom Mock.a Mock.b] + [claim] + [] + let expect = MultiAnd.singleton (StuckClaim claim) + assertEqual "" expect actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "runs one step with depth = 1" $ + let mkTest name mkSimpleClaim = + testCase name $ do + let claim = mkSimpleClaim Mock.a Mock.b + actual <- proveClaims_ + Unlimited + (Limit 1) + [simpleAxiom Mock.a Mock.b] + [claim] + [] + -- Note that the check that we have reached the destination + -- happens at the beginning of each step. At the beginning + -- of the first step the pattern is 'a', so we didn't reach + -- our destination yet, even if the rewrite transforms 'a' + -- into 'b'. We detect the success at the beginning of the + -- second step, which does not run here. + let stuck = mkSimpleClaim Mock.b Mock.b + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "" expect actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves direct implication" $ + let mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 1) + [] + [mkSimpleClaim Mock.a Mock.a] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "does not prove implication without rewriting" $ + let mkTest name mkSimpleClaim = + testCase name $ do + let claim = mkSimpleClaim Mock.a Mock.b + actual <- proveClaims_ + Unlimited + Unlimited + [] + [claim] + [] + let expect = MultiAnd.singleton (StuckClaim claim) + assertEqual "" expect actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves by rewriting into disjunction" $ + let mkTest name mkSomeClaim = + testCase name $ do + actual <- proveClaims_ + (Limit 2) + Unlimited + [ simpleAxiom Mock.a Mock.b ] + [ mkSomeClaim + (Pattern.fromTermLike Mock.a) + (OrPattern.fromPatterns $ map Pattern.fromTermLike + [ Mock.b + , Mock.c + ] + ) + [] + ] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath + ] + , testGroup "proves anything with cyclic rules" $ + let mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 3) + [ simpleAxiom Mock.a Mock.a ] + [ mkSimpleClaim Mock.a Mock.b ] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves disjunction with non-deterministic rules" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.a Mock.c + ] + mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 2) + axioms + [ mkSimpleClaim Mock.a (mkOr Mock.b Mock.c) ] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "returns first stuck claim after disjunction" $ + let axioms = [simpleAxiom Mock.a (mkOr Mock.b Mock.c)] + mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 1) + axioms + [mkSimpleClaim Mock.a Mock.d] + [] + let stuck = mkSimpleClaim Mock.b Mock.d + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "" expect actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves one claim" $ + let axioms = [simpleAxiom Mock.a Mock.b] + mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 2) + axioms + [mkSimpleClaim Mock.a Mock.b] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "does not apply trusted claims in first step" $ + let mkTest name mkSimpleClaim = + testCase name $ do + let claim = mkSimpleClaim Mock.a Mock.b + actual <- proveClaims_ + Unlimited + (Limit 4) + [] + [makeTrusted claim, claim] + [] + let expect = MultiAnd.singleton (StuckClaim claim) + assertEqual "" expect actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves claim with multiple rewrites" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.b Mock.c + ] + mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 3) + axioms + [mkSimpleClaim Mock.a Mock.c] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "stops rewriting when claim is proven" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.b Mock.c + , simpleAxiom Mock.c Mock.d + ] + mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 3) + axioms + [mkSimpleClaim Mock.a Mock.c] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves claim with narrowed branch" $ + let axioms = + [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b + , simpleAxiom + (Mock.functionalConstr11 (mkElemVar Mock.x)) + Mock.b + , simpleAxiom + (Mock.functionalConstr10 (mkElemVar Mock.x)) + (Mock.functionalConstr11 (mkElemVar Mock.x)) + ] + mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 4) + axioms + [ mkSimpleClaim + (Mock.functionalConstr10 (mkElemVar Mock.x)) + Mock.b + ] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "reports only failed branch of proof" $ + let stuckCondition = + makeNotPredicate + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a ) - ) - , Pattern.withCondition - Mock.b - (Condition.assign (inject Mock.x) Mock.a) - ] - ) - actual - , testCase "AllPath: Stops at branching because of breadth limit" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: error constr11(x) and x != a - actual <- proveClaims_ - (Limit 1) - Unlimited - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleAllPathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" - ( Left . OrPattern.fromPatterns $ - [ Pattern.withCondition - (Mock.functionalConstr11 (mkElemVar Mock.x)) - (Condition.fromPredicate - (makeNotPredicate - (makeEqualsPredicate Mock.testSort - (mkElemVar Mock.x) - Mock.a + & Condition.fromPredicate + stuckConfig = + Pattern.withCondition + (Mock.functionalConstr11 (mkElemVar Mock.x)) + stuckCondition + & mkRewritingPattern + initialConfig = + Mock.functionalConstr10 (mkElemVar Mock.x) + & Pattern.fromTermLike + & mkRewritingPattern + finalConfigs = OrPattern.fromTermLike Mock.b + axioms = + [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b + , simpleAxiom + (Mock.functionalConstr10 (mkElemVar Mock.x)) + (Mock.functionalConstr11 (mkElemVar Mock.x)) + ] + mkTest name mkSomeClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 3) + axioms + [mkSomeClaim initialConfig finalConfigs []] + [] + let stuck = mkSomeClaim stuckConfig finalConfigs [] + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "" expect actual + in + [ mkTest "OnePath" mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath + ] + , testGroup "stops when breadth limit is exceeded" $ + let axioms = + [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b + , simpleAxiom + (Mock.functionalConstr10 (mkElemVar Mock.x)) + (Mock.functionalConstr11 (mkElemVar Mock.x)) + ] + stuckConfigs = + map mkRewritingPattern + [ Pattern.withCondition + (Mock.functionalConstr11 (mkElemVar Mock.x)) + (Condition.fromPredicate + (makeNotPredicate + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) ) ) - ) - , Pattern.withCondition - Mock.b - (Condition.assign (inject Mock.x) Mock.a) - ] - ) - actual - , testCase "Mixed: Stops at branching because of breadth limit" $ do - -- Axiom: constr11(a) => b - -- Axiom: constr10(x) => constr11(x) - -- Claim: constr10(x) => b - -- Expected: error constr11(x) and x != a - actual <- proveClaims_ - (Limit 1) - Unlimited - [ simpleAxiom (Mock.functionalConstr11 Mock.a) Mock.b - , simpleAxiom - (Mock.functionalConstr10 (mkElemVar Mock.x)) - (Mock.functionalConstr11 (mkElemVar Mock.x)) - ] - [ simpleOnePathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - , simpleAllPathClaim - (Mock.functionalConstr10 (mkElemVar Mock.x)) - Mock.b - ] - [] - assertEqual "" - ( Left . OrPattern.fromPatterns $ - [ Pattern.withCondition - (Mock.functionalConstr11 (mkElemVar Mock.x)) - (Condition.fromPredicate - (makeNotPredicate - (makeEqualsPredicate Mock.testSort - (mkElemVar Mock.x) - Mock.a - ) - ) - ) - , Pattern.withCondition - Mock.b - (Condition.assign (inject Mock.x) Mock.a) - ] - ) - actual - , testCase "OnePath: Verifies two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => c - -- Claim: d => e - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.c - , simpleOnePathClaim Mock.d Mock.e - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Verifies two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => c - -- Claim: d => e - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleAllPathClaim Mock.a Mock.c - , simpleAllPathClaim Mock.d Mock.e - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: Verifies two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => c - -- Claim: d => e - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleAllPathClaim Mock.a Mock.c - , simpleOnePathClaim Mock.d Mock.e - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: fails first of two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => e - -- Claim: d => e - -- Expected: error c - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.e - , simpleOnePathClaim Mock.d Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "AllPath: fails first of two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => e - -- Claim: d => e - -- Expected: error c - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleAllPathClaim Mock.a Mock.e - , simpleAllPathClaim Mock.d Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "Mixed: fails first of two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => e - -- Claim: d => e - -- Expected: error c - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.e - , simpleAllPathClaim Mock.d Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "OnePath: fails second of two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => c - -- Claim: d => c - -- Expected: error e - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.c - , simpleOnePathClaim Mock.d Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.e) - actual - , testCase "AllPath: fails second of two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => c - -- Claim: d => c - -- Expected: error e - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleAllPathClaim Mock.a Mock.c - , simpleAllPathClaim Mock.d Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.e) - actual - , testCase "Mixed: fails second of two claims" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: d => e - -- Claim: a => c - -- Claim: d => c - -- Expected: error e - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.c - , simpleAllPathClaim Mock.d Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.e) - actual - , testCase "OnePath: skips proven claim" $ do - -- Axiom: d => e - -- Claim: a => b - -- Claim: d => e - -- Already proven: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.b - , simpleOnePathClaim Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.b - ] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: skips proven claim" $ do - -- Axiom: d => e - -- Claim: a => b - -- Claim: d => e - -- Already proven: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.d Mock.e - ] - [ simpleAllPathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.d Mock.e - ] - [ simpleAllPathClaim Mock.a Mock.b - ] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: skips proven claim" $ do - -- Axiom: d => e - -- Claim: a => b - -- Claim: d => e - -- Already proven: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 3) - [ simpleAxiom Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.d Mock.e - ] - [ simpleOnePathClaim Mock.a Mock.b - ] - assertEqual "" - (Right ()) - actual - , testCase "OnePath: second proves first but fails" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => c - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleOnePathClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "AllPath: second proves first but fails" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => c - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleAllPathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "Mixed: second proves first but fails" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => c - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleOnePathClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "Mixed: different claim types so\ - \ second can't prove first" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => c - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "OnePath: first proves second but fails" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.b Mock.c - , simpleOnePathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "AllPath: first proves second but fails" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleAllPathClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "Mixed: first proves second but fails" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.b Mock.c - , simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "Mixed: first doesn't prove second\ - \ because they are different claim types" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "OnePath: trusted second proves first" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Trusted Claim: b => c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleOnePathTrustedClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: trusted second proves first" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Trusted Claim: b => c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleAllPathClaim Mock.a Mock.d - , simpleAllPathTrustedClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: trusted second proves first" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Trusted Claim: b => c - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleOnePathTrustedClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - , simpleAllPathTrustedClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: trusted second doesn't prove first\ - \ because of different claim types" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: a => d - -- Trusted Claim: b => c - -- Expected: error b - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathTrustedClaim Mock.b Mock.c - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "OnePath: trusted first proves second" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathTrustedClaim Mock.b Mock.c - , simpleOnePathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: trusted first proves second" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleAllPathTrustedClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed: trusted first doesn't proves second\ - \ because they are different claim types" $ do - -- Axiom: a => b - -- Axiom: c => d - -- Claim: b => c - -- Claim: a => d - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathTrustedClaim Mock.b Mock.c - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.b) - actual - , testCase "OnePath: Prefers using claims for rewriting" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => e - -- Expected: error e - -- first verification: a=>b=>e, - -- without second claim would be: a=>b=>c=>d - -- second verification: b=>c=>d, not visible here - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleOnePathClaim Mock.b Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.e) - actual - , testCase "AllPath: Prefers using claims for rewriting" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => e - -- Expected: error e - -- first verification: a=>b=>e, - -- without second claim would be: a=>b=>c=>d - -- second verification: b=>c=>d, not visible here - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.c Mock.d - ] - [ simpleAllPathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.e) - actual - , testCase "Mixed: Prefers using claims for rewriting" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => e - -- Expected: error e - -- first verification: a=>b=>e, - -- without second claim would be: a=>b=>c=>d - -- second verification: b=>c=>d, not visible here - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleOnePathClaim Mock.b Mock.e - , simpleAllPathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.e) - actual - , testCase "Mixed: Doesn't apply claim because of\ - \ different claim type" $ do - -- Axiom: a => b - -- Axiom: b => c - -- Axiom: c => d - -- Claim: a => d - -- Claim: b => e - -- Expected: error d - -- first verification: a=>b=>c=>d - -- second verification: b=>c=>d is now visible here - actual <- proveClaims_ - Unlimited - (Limit 4) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.c Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.b Mock.e - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.d) - actual - , testCase "OnePath: Provable using one-path; not provable\ - \ using all-path" $ do - -- Axioms: - -- a => b - -- a => c - -- Claim: a => b - -- Expected: success - actual <- proveClaims_ - Unlimited - (Limit 5) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.a Mock.c - ] - [ simpleOnePathClaim Mock.a Mock.b ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath: Provable using one-path; not provable\ - \ using all-path" $ do - -- Axioms: - -- a => b - -- a => c - -- Claim: a => b - -- Expected: error c - actual <- proveClaims_ - Unlimited - (Limit 5) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.a Mock.c - ] - [ simpleAllPathClaim Mock.a Mock.b ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "Mixed: Provable using one-path; not provable\ - \ using all-path" $ do - -- Axioms: - -- a => b - -- a => c - -- Claim: a => b - -- Expected: error c - actual <- proveClaims_ - Unlimited - (Limit 5) - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.a Mock.c - ] - [ simpleOnePathClaim Mock.a Mock.b - , simpleAllPathClaim Mock.a Mock.b - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "OnePath Priority: can get stuck by choosing second axiom" $ do - -- Axioms: - -- a => b - -- b => c - -- b => d - -- Claims: a => d - -- Expected: error c - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.b Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "AllPath Priority: can get stuck by choosing second axiom" $ do - -- Axioms: - -- a => b - -- b => c - -- b => d - -- Claims: a => d - -- Expected: error c - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.b Mock.d - ] - [ simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "Mixed Priority: can get stuck by choosing second axiom" $ do - -- Axioms: - -- a => b - -- b => c - -- b => d - -- Claims: a => d - -- Expected: error c - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simpleAxiom Mock.b Mock.c - , simpleAxiom Mock.b Mock.d - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "OnePath Priority: should succeed, prefering axiom with priority 1" $ do - -- Axioms: - -- a => b - -- b => c [priority(2)] - -- b => d [priority(1)] - -- Claims: a => d - -- Expected: success - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simplePriorityAxiom Mock.b Mock.c 2 - , simplePriorityAxiom Mock.b Mock.d 1 - ] - [ simpleOnePathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "AllPath Priority: should succeed, prefering axiom with priority 1" $ do - -- Axioms: - -- a => b - -- b => c [priority(2)] - -- b => d [priority(1)] - -- Claims: a => d - -- Expected: success - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simplePriorityAxiom Mock.b Mock.c 2 - , simplePriorityAxiom Mock.b Mock.d 1 - ] - [ simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "Mixed Priority: should succeed, prefering axiom with priority 1" $ do - -- Axioms: - -- a => b - -- b => c [priority(2)] - -- b => d [priority(1)] - -- Claims: a => d - -- Expected: success - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simplePriorityAxiom Mock.b Mock.c 2 - , simplePriorityAxiom Mock.b Mock.d 1 - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Right ()) - actual - , testCase "OnePath Priority: should fail, prefering axiom with priority 1" $ do - -- Axioms: - -- a => b - -- b => c [priority(2)] - -- b => d [priority(1)] - -- Claims: a => d - -- Expected: error c - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simplePriorityAxiom Mock.b Mock.d 2 - , simplePriorityAxiom Mock.b Mock.c 1 - ] - [ simpleOnePathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "AllPath Priority: should fail, prefering axiom with priority 1" $ do - -- Axioms: - -- a => b - -- b => c [priority(2)] - -- b => d [priority(1)] - -- Claims: a => d - -- Expected: error c - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simplePriorityAxiom Mock.b Mock.d 2 - , simplePriorityAxiom Mock.b Mock.c 1 - ] - [ simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual - , testCase "Mixed Priority: should fail, prefering axiom with priority 1" $ do - -- Axioms: - -- a => b - -- b => c [priority(2)] - -- b => d [priority(1)] - -- Claims: a => d - -- Expected: error c - actual <- proveClaims_ - Unlimited - Unlimited - [ simpleAxiom Mock.a Mock.b - , simplePriorityAxiom Mock.b Mock.d 2 - , simplePriorityAxiom Mock.b Mock.c 1 - ] - [ simpleOnePathClaim Mock.a Mock.d - , simpleAllPathClaim Mock.a Mock.d - ] - [] - assertEqual "" - (Left $ OrPattern.fromTermLike Mock.c) - actual + , Pattern.withCondition + Mock.b + (Condition.assign (inject Mock.x) Mock.a) + ] + initialPattern = + Pattern.fromTermLike + (Mock.functionalConstr10 (mkElemVar Mock.x)) + & mkRewritingPattern + finalPatterns = OrPattern.fromTermLike Mock.b + mkTest name mkSomeClaim = + testCase name $ do + actual <- proveClaims_ + (Limit 1) + Unlimited + axioms + [mkSomeClaim initialPattern finalPatterns []] + [] + let stuckClaims = + map + (\left -> mkSomeClaim left finalPatterns []) + stuckConfigs + expect = MultiAnd.make (StuckClaim <$> stuckClaims) + assertEqual "" expect actual + in + [ mkTest "OnePath" mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath + ] + , testGroup "proves two claims" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.b Mock.c + , simpleAxiom Mock.d Mock.e + ] + mkTest name mkSimpleClaim1 mkSimpleClaim2 = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 3) + axioms + [ mkSimpleClaim1 Mock.a Mock.c + , mkSimpleClaim2 Mock.d Mock.e + ] + [] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath, OnePath" simpleOnePathClaim simpleOnePathClaim + , mkTest "OnePath, AllPath" simpleOnePathClaim simpleAllPathClaim + , mkTest "AllPath, AllPath" simpleAllPathClaim simpleAllPathClaim + , mkTest "AllPath, OnePath" simpleAllPathClaim simpleOnePathClaim + ] + , testGroup "does not prove first of two claims" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.b Mock.c + , simpleAxiom Mock.d Mock.e + ] + right = OrPattern.fromTermLike Mock.e + mkTest name mkSomeClaim1 mkSomeClaim2 = + testCase name $ do + actual <- proveClaims_ Unlimited (Limit 3) axioms claims [] + assertEqual "" expect actual + where + claims = + [ mkSomeClaim1 (Pattern.fromTermLike Mock.a) right [] + , mkSomeClaim2 (Pattern.fromTermLike Mock.d) right [] + ] + stuck = mkSomeClaim1 (Pattern.fromTermLike Mock.c) right [] + expect = MultiAnd.singleton (StuckClaim stuck) + in + [ mkTest "OnePath" mkSomeClaimOnePath mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath mkSomeClaimAllPath + , mkTest "OnePath, AllPath" mkSomeClaimOnePath mkSomeClaimAllPath + , mkTest "AllPath, OnePath" mkSomeClaimAllPath mkSomeClaimOnePath + ] + , testGroup "does not prove second of two claims" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.b Mock.c + , simpleAxiom Mock.d Mock.e + ] + right = OrPattern.fromTermLike Mock.c + mkTest name mkSomeClaim1 mkSomeClaim2 = + testCase name $ do + actual <- proveClaims_ Unlimited (Limit 3) axioms claims [] + assertEqual "" expect actual + where + claims = + [ mkSomeClaim1 (Pattern.fromTermLike Mock.a) right [] + , mkSomeClaim2 (Pattern.fromTermLike Mock.d) right [] + ] + stuck = mkSomeClaim2 (Pattern.fromTermLike Mock.e) right [] + expect = MultiAnd.singleton (StuckClaim stuck) + in + [ mkTest "OnePath" mkSomeClaimOnePath mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath mkSomeClaimAllPath + , mkTest "OnePath, AllPath" mkSomeClaimOnePath mkSomeClaimAllPath + , mkTest "AllPath, OnePath" mkSomeClaimAllPath mkSomeClaimOnePath + ] + , testGroup "skips proven claim" $ + let mkTest name mkSimpleClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 3) + [] + [ mkSimpleClaim Mock.a Mock.b ] + [ mkSimpleClaim Mock.a Mock.b ] + assertEqual "" MultiAnd.top actual + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] + , testGroup "proves first claim circularly, but proving circularity fails" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.c Mock.d + ] + mkTest name mkSomeClaim = + testCase name $ do + actual <- proveClaims_ Unlimited (Limit 4) axioms claims [] + assertEqual "" expect actual + where + proven = + mkSomeClaim + (Pattern.fromTermLike Mock.a) + (OrPattern.fromTermLike Mock.d) + [] + circularity = + mkSomeClaim + (Pattern.fromTermLike Mock.b) + (OrPattern.fromTermLike Mock.c) + [] + claims = [proven, circularity] + stuck = circularity + expect = MultiAnd.singleton (StuckClaim stuck) + in + [ mkTest "OnePath" mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath + , testCase "does not use different claim types" $ do + actual <- proveClaims_ + Unlimited + (Limit 4) + axioms + [ simpleOnePathClaim Mock.a Mock.d + , simpleAllPathClaim Mock.b Mock.c + ] + [] + let stuck = + mkSomeClaimOnePath + (Pattern.fromTermLike Mock.b) + (OrPattern.fromTermLike Mock.d) + [] + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "" expect actual + ] + , testGroup "proves first claim with trusted circularity" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.c Mock.d + ] + proven mkSomeClaim = + mkSomeClaim + (Pattern.fromTermLike Mock.a) + (OrPattern.fromTermLike Mock.d) + [] + trusted mkSomeClaim = + mkSomeClaim + (Pattern.fromTermLike Mock.b) + (OrPattern.fromTermLike Mock.c) + [] + & makeTrusted + mkTest name mkSomeClaim = + testCase name $ do + actual <- proveClaims_ Unlimited (Limit 4) axioms claims [] + assertEqual "" MultiAnd.top actual + where + claims = [proven mkSomeClaim, trusted mkSomeClaim] + in + [ mkTest "OnePath" mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath + , testCase "does not use different claim types" $ do + -- Axiom: a => b + -- Axiom: c => d + -- Claim: a => d + -- Trusted Claim: b => c + -- Expected: error b + let claims = [proven mkSomeClaimOnePath, trusted mkSomeClaimAllPath] + actual <- proveClaims_ Unlimited (Limit 4) axioms claims [] + let stuck = + mkSomeClaimOnePath + (Pattern.fromTermLike Mock.b) + (OrPattern.fromTermLike Mock.d) + [] + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "" expect actual + ] + , testGroup "prefer claims over axioms" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.b Mock.c + , simpleAxiom Mock.c Mock.d + ] + proveable mkSomeClaim = + mkSomeClaim + (Pattern.fromTermLike Mock.a) + (OrPattern.fromTermLike Mock.d) + [] + misdirection mkSomeClaim = + mkSomeClaim + (Pattern.fromTermLike Mock.b) + (OrPattern.fromTermLike Mock.e) + [] + mkTest name mkSomeClaim = + testCase name $ do + actual <- proveClaims_ + Unlimited + (Limit 4) + axioms + claims + [] + assertEqual "" expect actual + where + claims = [proveable mkSomeClaim, misdirection mkSomeClaim] + stuck = + mkSomeClaim + (Pattern.fromTermLike Mock.e) + (OrPattern.fromTermLike Mock.d) + [] + expect = MultiAnd.singleton (StuckClaim stuck) + in + [ mkTest "OnePath" mkSomeClaimOnePath + , mkTest "AllPath" mkSomeClaimAllPath + ] + , testGroup "one-path claim about non-deterministic axioms" $ + let axioms = + [ simpleAxiom Mock.a Mock.b + , simpleAxiom Mock.a Mock.c + ] + claims mkSomeClaim = + [ mkSomeClaim + (Pattern.fromTermLike Mock.a) + (OrPattern.fromTermLike Mock.b) + [] + ] + claimsOnePath = claims mkSomeClaimOnePath + claimsAllPath = claims mkSomeClaimAllPath + in + [ testCase "proves one-path claim" $ do + actual <- proveClaims_ Unlimited (Limit 5) axioms claimsOnePath [] + assertEqual "" MultiAnd.top actual + , testCase "does not prove all-path claim" $ do + actual <- proveClaims_ Unlimited (Limit 5) axioms claimsAllPath [] + let stuck = + mkSomeClaimAllPath + (Pattern.fromTermLike Mock.c) + (OrPattern.fromTermLike Mock.b) + [] + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "" expect actual + ] + , testGroup "applies axioms in priority order" $ + let mkTest name mkSimpleClaim = + testCase name $ do + let claims = [mkSimpleClaim Mock.a Mock.d] + + actual1 <- proveClaims_ + Unlimited + Unlimited + [ simpleAxiom Mock.a Mock.b + , simplePriorityAxiom Mock.b Mock.c 2 + , simplePriorityAxiom Mock.b Mock.d 1 + ] + claims + [] + assertEqual "succeeds with preferred axiom" + MultiAnd.top + actual1 + + actual2 <- proveClaims_ + Unlimited + Unlimited + [ simpleAxiom Mock.a Mock.b + , simplePriorityAxiom Mock.b Mock.c 1 + , simplePriorityAxiom Mock.b Mock.d 2 + ] + claims + [] + let stuck = mkSimpleClaim Mock.c Mock.d + expect = MultiAnd.singleton (StuckClaim stuck) + assertEqual "fails with preferred axiom" expect actual2 + in + [ mkTest "OnePath" simpleOnePathClaim + , mkTest "AllPath" simpleAllPathClaim + ] ] simpleAxiom @@ -1849,30 +704,6 @@ simpleAllPathClaim simpleAllPathClaim left right = AllPath . AllPathClaim $ simpleClaim left right -simpleOnePathTrustedClaim - :: TermLike VariableName - -> TermLike VariableName - -> SomeClaim -simpleOnePathTrustedClaim left right = - Lens.set - (lensClaimPattern . field @"attributes" . field @"trusted") - (Attribute.Trusted True) - . OnePath - . OnePathClaim - $ simpleClaim left right - -simpleAllPathTrustedClaim - :: TermLike VariableName - -> TermLike VariableName - -> SomeClaim -simpleAllPathTrustedClaim left right = - Lens.set - (lensClaimPattern . field @"attributes" . field @"trusted") - (Attribute.Trusted True) - . AllPath - . AllPathClaim - $ simpleClaim left right - simplePriorityAxiom :: TermLike VariableName -> TermLike VariableName @@ -1904,7 +735,7 @@ proveClaims -> [Rule SomeClaim] -> [SomeClaim] -> [SomeClaim] - -> IO (Either ProofStuck ()) + -> IO ProveClaimsResult proveClaims breadthLimit depthLimit axioms claims alreadyProven = Kore.Reachability.proveClaims breadthLimit @@ -1913,7 +744,6 @@ proveClaims breadthLimit depthLimit axioms claims alreadyProven = (Axioms axioms) (AlreadyProven (map unparseToText2 alreadyProven)) (ToProve (map applyDepthLimit . selectUntrusted $ claims)) - & runExceptT & runSimplifier mockEnv where mockEnv = Mock.env @@ -1926,16 +756,14 @@ proveClaims_ -> [Rule SomeClaim] -> [SomeClaim] -> [SomeClaim] - -> IO (Either (OrPattern VariableName) ()) + -> IO StuckClaims proveClaims_ breadthLimit depthLimit axioms claims alreadyProven = do - stuck <- Test.Kore.Reachability.Prove.proveClaims - breadthLimit - depthLimit - axioms - claims - alreadyProven - return (toPattern stuck) - where - toPattern :: Either ProofStuck a -> Either (OrPattern VariableName) a - toPattern = Bifunctor.first stuckPatterns + ProveClaimsResult { stuckClaims } <- + Test.Kore.Reachability.Prove.proveClaims + breadthLimit + depthLimit + axioms + claims + alreadyProven + pure stuckClaims diff --git a/kore/test/Test/Kore/Repl/Interpreter.hs b/kore/test/Test/Kore/Repl/Interpreter.hs index 42323054c8..89da5fbc42 100644 --- a/kore/test/Test/Kore/Repl/Interpreter.hs +++ b/kore/test/Test/Kore/Repl/Interpreter.hs @@ -66,7 +66,7 @@ import Kore.Repl.State import Kore.Rewriting.RewritingVariable import Kore.Step.ClaimPattern ( ClaimPattern - , claimPattern + , mkClaimPattern ) import Kore.Step.RulePattern ( mkRewritingRule @@ -688,7 +688,7 @@ claimWithName leftTerm rightTerm name = right = Pattern.fromTermLike rightTerm & OrPattern.fromPattern - in claimPattern left right [] + in mkClaimPattern left right [] & Lens.set (field @"attributes" . typed @Attribute.Label) label where label = Attribute.Label . pure $ pack name diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 1efee1d9ce..3d56fb79bc 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -48,7 +48,7 @@ import Kore.Reachability import Kore.Rewriting.RewritingVariable import Kore.Step.ClaimPattern ( ClaimPattern - , claimPattern + , mkClaimPattern , refreshExistentials ) import qualified Kore.Step.RewriteStep as Step @@ -160,7 +160,7 @@ claimPatternFromPatterns -> Pattern VariableName -> ClaimPattern claimPatternFromPatterns patt1 patt2 = - claimPattern + mkClaimPattern ( patt1 & Pattern.mapVariables (pure mkRuleVariable) ) @@ -176,7 +176,7 @@ claimPatternFromTerms -> [ElementVariable VariableName] -> ClaimPattern claimPatternFromTerms term1 term2 existentials' = - claimPattern + mkClaimPattern ( term1 & Pattern.fromTermLike & Pattern.mapVariables (pure mkRuleVariable) diff --git a/kore/test/Test/Kore/Step/Rule/Common.hs b/kore/test/Test/Kore/Step/Rule/Common.hs index 1330ac6428..59e50fca19 100644 --- a/kore/test/Test/Kore/Step/Rule/Common.hs +++ b/kore/test/Test/Kore/Step/Rule/Common.hs @@ -22,13 +22,11 @@ import Kore.Internal.TermLike import qualified Kore.Internal.TermLike as TermLike import Kore.Reachability ( OnePathClaim (..) + , mkOnePathClaim ) import Kore.Rewriting.RewritingVariable ( mkRuleVariable ) -import Kore.Step.ClaimPattern - ( claimPattern - ) import Kore.Step.RulePattern ( RHS (RHS) , RewriteRule (RewriteRule) @@ -44,8 +42,7 @@ class RuleBase base rule where instance RuleBase Pair OnePathClaim where Pair (t1, p1) `rewritesTo` Pair (t2, p2) = - OnePathClaim - $ claimPattern + mkOnePathClaim (Pattern.fromTermAndPredicate t1' p1') (Pattern.fromTermAndPredicate t2' p2' & OrPattern.fromPattern) [] diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 4e351b221e..a5ddae3aad 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -71,7 +71,7 @@ import Kore.Sort ) import Kore.Step.ClaimPattern ( ClaimPattern (..) - , claimPattern + , mkClaimPattern ) import Kore.Step.Rule.Simplify import Kore.Step.RulePattern @@ -418,13 +418,13 @@ test_simplifyClaimRule = where rule1, rule2, rule2' :: ClaimPattern rule1 = - claimPattern + mkClaimPattern (Pattern.fromTermLike (Mock.f Mock.a)) (OrPattern.fromPatterns [Pattern.fromTermLike Mock.b]) [] rule1' = rule1 & requireDefined rule2 = - claimPattern + mkClaimPattern (Pattern.fromTermLike (Mock.g Mock.a)) (OrPattern.fromPatterns [Pattern.fromTermLike Mock.b]) [] diff --git a/test/save-proofs/test-1-spec.k b/test/save-proofs/test-1-spec.k index f6328eb5c0..e180b4a166 100644 --- a/test/save-proofs/test-1-spec.k +++ b/test/save-proofs/test-1-spec.k @@ -1,13 +1,12 @@ -// Two claims, one passes and is saved to a file, the other one fails. module VERIFICATION imports SAVE-PROOFS rule BB(X:Int) => CC(X:Int) endmodule +// This claim is proven and saved. module TEST-1-SPEC imports VERIFICATION rule BB(X:Int) => CC(X:Int) - rule AA(X:Int) => DD(X:Int) endmodule diff --git a/test/save-proofs/test-1-spec.k.out.golden b/test/save-proofs/test-1-spec.k.out.golden index a6484687fa..17a1d4510e 100644 --- a/test/save-proofs/test-1-spec.k.out.golden +++ b/test/save-proofs/test-1-spec.k.out.golden @@ -1,3 +1 @@ - - AA ( X ) ~> _DotVar1 ~> . - +#Top diff --git a/test/save-proofs/test-2-spec.k b/test/save-proofs/test-2-spec.k index 58b6a4cf28..bf8f7f517e 100644 --- a/test/save-proofs/test-2-spec.k +++ b/test/save-proofs/test-2-spec.k @@ -10,6 +10,8 @@ endmodule module TEST-2-SPEC imports VERIFICATION + // This claim would fail, but it is loaded from the saved claims. rule BB(X:Int) => CC(X:Int) + // This claim requires the first claim. rule AA(X:Int) => DD(X:Int) endmodule