Skip to content

Commit

Permalink
Generalize the signature for induct and inductWith
Browse files Browse the repository at this point in the history 
Coding the transition as a relation is simpler to use in realistic scenarios.
  • Loading branch information
@LeventErkok
LeventErkok committed Nov 3, 2024
1 parent ad41023 commit 4cdded2
Show file tree
Hide file tree
Showing 5 changed files with 40 additions and 37 deletions.
9 changes: 5 additions & 4 deletions CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
32 changes: 18 additions & 14 deletions Data/SBV/Tools/Induction.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand All @@ -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)

Expand All @@ -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)
9 changes: 4 additions & 5 deletions Documentation/SBV/Examples/ProofTools/Fibonacci.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
18 changes: 9 additions & 9 deletions Documentation/SBV/Examples/ProofTools/Strengthen.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand All @@ -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)]
Expand All @@ -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)]
Expand All @@ -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)]
Expand All @@ -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.
Expand Down
9 changes: 4 additions & 5 deletions Documentation/SBV/Examples/ProofTools/Sum.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down

0 comments on commit 4cdded2

Please sign in to comment.