1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Tools.Induction
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Induction engine for state transition systems. See the following examples
-- for details:
--
-- * "Documentation.SBV.Examples.ProofTools.Strengthen": Use of strengthening
-- to establish inductive invariants.
--
-- * "Documentation.SBV.Examples.ProofTools.Sum": Proof for correctness of
-- an algorithm to sum up numbers,
--
-- * "Documentation.SBV.Examples.ProofTools.Fibonacci": Proof for correctness of
-- an algorithm to fast-compute fibonacci numbers, using axiomatization.
-----------------------------------------------------------------------------
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Tools.Induction (
InductionResult(..), InductionStep(..), induct, inductWith
) where
import Data.SBV
import Data.SBV.Control
import Data.List (intercalate)
import Control.Monad (when)
-- | A step in an inductive proof. If the tag is present (i.e., @Just nm@), then
-- the step belongs to the subproof that establishes the strengthening named @nm@.
data InductionStep = Initiation (Maybe String)
| Consecution (Maybe String)
| PartialCorrectness
-- | Show instance for 'InductionStep', diagnostic purposes only.
instance Show InductionStep where
show (Initiation Nothing) = "initiation"
show (Initiation (Just s)) = "initiation for strengthening " ++ show s
show (Consecution Nothing) = "consecution"
show (Consecution (Just s)) = "consecution for strengthening " ++ show s
show PartialCorrectness = "partial correctness"
-- | Result of an inductive proof, with a counter-example in case of failure.
--
-- If a proof is found (indicated by a 'Proven' result), then the invariant holds
-- and the goal is established once the termination condition holds. If it fails, then
-- it can fail either in an initiation step or in a consecution step:
--
-- * A 'Failed' result in an 'Initiation' step means that the invariant does /not/ hold for
-- the initial state, and thus indicates a true failure.
--
-- * A 'Failed' result in a 'Consecution' step will return a state /s/. This state is known as a
-- CTI (counterexample to inductiveness): It will lead to a violation of the invariant
-- in one step. However, this does not mean the property is invalid: It could be the
-- case that it is simply not inductive. In this case, human intervention---or a smarter
-- algorithm like IC3 for certain domains---is needed to see if one can strengthen the
-- invariant so an inductive proof can be found. How this strengthening can be done remains
-- an art, but the science is improving with algorithms like IC3.
--
-- * 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
| Proven
-- | Show instance for 'InductionResult', diagnostic purposes only.
instance Show a => Show (InductionResult a) where
show Proven = "Q.E.D."
show (Failed s e) = intercalate "\n" [ "Failed while establishing " ++ show s ++ "."
, "Counter-example to inductiveness:"
, intercalate "\n" [" " ++ l | l <- lines (show e)]
]
-- | Induction engine, using the default solver. See "Documentation.SBV.Examples.ProofTools.Strengthen"
-- and "Documentation.SBV.Examples.ProofTools.Sum" for examples.
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
-> [(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
-> IO (InductionResult res) -- ^ Either proven, or a concrete state value that, if reachable, fails the invariant.
induct = inductWith defaultSMTCfg
-- | Induction engine, configurable with the solver
inductWith :: (Show res, Queriable IO st, res ~ QueryResult st)
=> SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(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)
(Failed (Initiation Nothing))
$ strengthen strengthenings
$ try "Proving consecution"
(\s -> sAnd (inv s : [st s | (_, st) <- strengthenings]) .=> sAll inv (trans s))
(Failed (Consecution Nothing))
$ try "Proving partial correctness"
(\s -> let (term, result) = goal s in inv s .&& term .=> result)
(Failed PartialCorrectness)
(msg "Done" >> return Proven)
where msg = when chatty . putStrLn
try m p wrap cont = do msg m
res <- check p
case res of
Just ex -> return $ wrap ex
Nothing -> cont
check p = runSMTWith cfg $ do
setup
query $ do st <- create
constrain $ sNot (p st)
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
strengthen [] cont = cont
strengthen ((nm, st):sts) cont = try ("Proving strengthening initiation : " ++ nm)
(\s -> initial s .=> st s)
(Failed (Initiation (Just nm)))
$ try ("Proving strengthening consecution: " ++ nm)
(\s -> st s .=> sAll st (trans s))
(Failed (Consecution (Just nm)))
(strengthen sts cont)
|
