From 4cdded27c0a122918f99f257769232e0d7d2dede Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Sun, 3 Nov 2024 09:31:31 -0800 Subject: [PATCH] Generalize the signature for induct and inductWith Coding the transition as a relation is simpler to use in realistic scenarios. --- CHANGES.md | 9 +++--- Data/SBV/Tools/Induction.hs | 32 +++++++++++-------- .../SBV/Examples/ProofTools/Fibonacci.hs | 9 +++--- .../SBV/Examples/ProofTools/Strengthen.hs | 18 +++++------ Documentation/SBV/Examples/ProofTools/Sum.hs | 9 +++--- 5 files changed, 40 insertions(+), 37 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d87a3b710..0b19371ef 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -33,11 +33,12 @@ * SBV now prints the elements of uninterpreted sorts more simply for z3. Previously, we simply used the name z3 produced, which looked like @T!val!i@ for the uninterpreted type @T@, we know convert it to @T_i@. - * [BACKWARDS COMPATIBILITY] Changed the signature of the functions bmc (and bmcWith) so they take - the transition as a relation, instead of a function returning multiple values. This generalizes - the use cases, and it is easy to translate from existing applications. Simply change your old + * [BACKWARDS COMPATIBILITY] Changed the signature of the functions bmc (and bmcWith), induct (and inductWith) + functions, so they take the transition as a relation, instead of a function returning multiple values. This + generalizes the use cases, and it is easy to translate from existing applications. Simply change your old 'State -> [State]' function to 'State -> State -> SBool', which can be achieved by - 'newTrans s1 s2 = s2 `sElem` oldTrans s1'. + 'newTrans s1 s2 = s2 `sElem` oldTrans s1', though you probably want to code this in a more readable way + depending on the actual transition relation you want to model. ### Version 10.12, 2024-08-11 diff --git a/Data/SBV/Tools/Induction.hs b/Data/SBV/Tools/Induction.hs index f145a4d6a..b68bc6f33 100644 --- a/Data/SBV/Tools/Induction.hs +++ b/Data/SBV/Tools/Induction.hs @@ -69,7 +69,7 @@ instance Show InductionStep where -- * A 'Failed' result in a 'PartialCorrectness' step means that the invariant holds, but assuming the -- termination condition the goal still does not follow. That is, the partial correctness -- does not hold. -data InductionResult a = Failed InductionStep a +data InductionResult a = Failed InductionStep (a, a) | Proven -- | Show instance for 'InductionResult', diagnostic purposes only. @@ -86,7 +86,7 @@ induct :: (Show res, Queriable IO st, res ~ QueryResult st) => Bool -- ^ Verbose mode -> Symbolic () -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.) -> (st -> SBool) -- ^ Initial condition - -> (st -> [st]) -- ^ Transition relation + -> (st -> st -> SBool) -- ^ Transition relation -> [(String, st -> SBool)] -- ^ Strengthenings, if any. The @String@ is a simple tag. -> (st -> SBool) -- ^ Invariant that ensures the goal upon termination -> (st -> (SBool, SBool)) -- ^ Termination condition and the goal to establish @@ -99,21 +99,21 @@ inductWith :: (Show res, Queriable IO st, res ~ QueryResult st) -> Bool -> Symbolic () -> (st -> SBool) - -> (st -> [st]) + -> (st -> st -> SBool) -> [(String, st -> SBool)] -> (st -> SBool) -> (st -> (SBool, SBool)) -> IO (InductionResult res) inductWith cfg chatty setup initial trans strengthenings inv goal = try "Proving initiation" - (\s -> initial s .=> inv s) + (\s _ -> initial s .=> inv s) (Failed (Initiation Nothing)) $ strengthen strengthenings $ try "Proving consecution" - (\s -> sAnd (inv s : [st s | (_, st) <- strengthenings]) .=> sAll inv (trans s)) + (\s s' -> sAnd (inv s : s `trans` s' : [st s | (_, st) <- strengthenings]) .=> inv s') (Failed (Consecution Nothing)) $ try "Proving partial correctness" - (\s -> let (term, result) = goal s in inv s .&& term .=> result) + (\s _ -> let (term, result) = goal s in inv s .&& term .=> result) (Failed PartialCorrectness) (msg "Done" >> return Proven) @@ -127,24 +127,28 @@ inductWith cfg chatty setup initial trans strengthenings inv goal = check p = runSMTWith cfg $ do setup - query $ do st <- create - constrain $ sNot (p st) + query $ do s <- create + s' <- create + constrain $ sNot (p s s') cs <- checkSat case cs of Unk -> error "Solver said unknown" DSat{} -> error "Solver returned a delta-sat result" Unsat -> return Nothing - Sat -> do io $ msg "Failed:" - ex <- project st - io $ msg $ show ex - return $ Just ex + Sat -> do io $ msg "Failed in state:" + exS <- project s + io $ msg $ show exS + io $ msg "Transitioning to:" + exS' <- project s' + io $ msg $ show exS' + return $ Just (exS, exS') strengthen [] cont = cont strengthen ((nm, st):sts) cont = try ("Proving strengthening initiation : " ++ nm) - (\s -> initial s .=> st s) + (\s _ -> initial s .=> st s) (Failed (Initiation (Just nm))) $ try ("Proving strengthening consecution: " ++ nm) - (\s -> st s .=> sAll st (trans s)) + (\s s' -> sAnd [st s, s `trans` s'] .=> st s') (Failed (Consecution (Just nm))) (strengthen sts cont) diff --git a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs index 0b415d2d1..636f2b6c7 100644 --- a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs +++ b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs @@ -81,11 +81,10 @@ fibCorrect = induct chatty setup initial trans strengthenings inv goal initial S{i, k, m, n} = i .== 0 .&& k .== 1 .&& m .== 0 .&& n .>= 0 -- We code the algorithm almost literally in SBV notation: - trans :: S SInteger -> [S SInteger] - trans st@S{i, k, m, n} = [ite (i .< n) - st { i = i + 1, k = m + k, m = k } - st - ] + trans :: S SInteger -> S SInteger -> SBool + trans S{i, k, m, n} S{i = i', k = k', m = m', n = n'} = (i', k', m', n') .== ite (i .< n) + (i+1, m+k, k, n) + (i, k, m, n) -- No strengthenings needed for this problem! strengthenings :: [(String, S SInteger -> SBool)] diff --git a/Documentation/SBV/Examples/ProofTools/Strengthen.hs b/Documentation/SBV/Examples/ProofTools/Strengthen.hs index a3ac5dda8..21f809338 100644 --- a/Documentation/SBV/Examples/ProofTools/Strengthen.hs +++ b/Documentation/SBV/Examples/ProofTools/Strengthen.hs @@ -57,7 +57,7 @@ instance Fresh IO (S SInteger) where -- | We parameterize over the transition relation and the strengthenings to -- investigate various combinations. -problem :: (S SInteger -> [S SInteger]) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer)) +problem :: (S SInteger -> S SInteger -> SBool) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer)) problem trans strengthenings = induct chatty setup initial trans strengthenings inv goal where -- Set this to True for SBV to print steps as it proceeds -- through the inductive proof @@ -83,12 +83,12 @@ problem trans strengthenings = induct chatty setup initial trans strengthenings goal _ = (sTrue, sTrue) -- | The first program, coded as a transition relation: -pgm1 :: S SInteger -> [S SInteger] -pgm1 S{x, y} = [S{x = x+1, y = y+x}] +pgm1 :: S SInteger -> S SInteger -> SBool +pgm1 S{x, y} S{x = x', y = y'} = x' .== x+1 .&& y' .== y+x -- | The second program, coded as a transition relation: -pgm2 :: S SInteger -> [S SInteger] -pgm2 S{x, y} = [S{x = x+y, y = y+x}] +pgm2 :: S SInteger -> S SInteger -> SBool +pgm2 S{x, y} S{x = x', y = y'} = x' .== x+y .&& y' .== y+x -- * Examples @@ -97,7 +97,7 @@ pgm2 S{x, y} = [S{x = x+y, y = y+x}] -- >>> ex1 -- Failed while establishing consecution. -- Counter-example to inductiveness: --- S {x = -1, y = 1} +-- (S {x = -1, y = 1},S {x = 0, y = 0}) ex1 :: IO (InductionResult (S Integer)) ex1 = problem pgm1 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] @@ -117,7 +117,7 @@ ex2 = problem pgm1 strengthenings -- >>> ex3 -- Failed while establishing consecution. -- Counter-example to inductiveness: --- S {x = -1, y = 1} +-- (S {x = -1, y = 1},S {x = 0, y = 0}) ex3 :: IO (InductionResult (S Integer)) ex3 = problem pgm2 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] @@ -128,7 +128,7 @@ ex3 = problem pgm2 strengthenings -- >>> ex4 -- Failed while establishing consecution for strengthening "x >= 0". -- Counter-example to inductiveness: --- S {x = 0, y = -1} +-- (S {x = 0, y = -1},S {x = -1, y = -1}) ex4 :: IO (InductionResult (S Integer)) ex4 = problem pgm2 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] @@ -139,7 +139,7 @@ ex4 = problem pgm2 strengthenings -- >>> ex5 -- Failed while establishing consecution for strengthening "x >= 0". -- Counter-example to inductiveness: --- S {x = 0, y = -1} +-- (S {x = 0, y = -1},S {x = -1, y = -1}) -- -- Note how this was sufficient in 'ex2' to establish the invariant for the first -- program, but fails for the second. diff --git a/Documentation/SBV/Examples/ProofTools/Sum.hs b/Documentation/SBV/Examples/ProofTools/Sum.hs index ed998f326..8c5ded93b 100644 --- a/Documentation/SBV/Examples/ProofTools/Sum.hs +++ b/Documentation/SBV/Examples/ProofTools/Sum.hs @@ -70,11 +70,10 @@ sumCorrect = induct chatty setup initial trans strengthenings inv goal initial S{s, i, n} = s .== 0 .&& i .== 0 .&& n .>= 0 -- We code the algorithm almost literally in SBV notation: - trans :: S SInteger -> [S SInteger] - trans st@S{s, i, n} = [ite (i .<= n) - st { s = s+i, i = i+1 } - st - ] + trans :: S SInteger -> S SInteger -> SBool + trans S{s, i, n} S{s = s', i = i', n = n'} = (s', i', n') .== ite (i .<= n) + (s+i, i+1, n) + (s , i , n) -- No strengthenings needed for this problem! strengthenings :: [(String, S SInteger -> SBool)]