0 | ||| The content of this module is based on the paper
  1 | ||| Applications of Applicative Proof Search
  2 | ||| by Liam O'Connor
  3 | ||| https://doi.org/10.1145/2976022.2976030
  4 |
  5 | module Search.CTL
  6 |
  7 | import Data.So
  8 | import Data.Nat
  9 | import Data.List.Quantifiers
 10 | import Decidable.Equality
 11 |
 12 | import public Search.Negation
 13 | import public Search.HDecidable
 14 | import public Search.Properties
 15 |
 16 | %default total
 17 |
 18 | ------------------------------------------------------------------------
 19 | -- Type and some basic functions
 20 |
 21 | ||| Labeled transition diagram
 22 | public export
 23 | record Diagram (labels : Type) (state : Type) where
 24 |   constructor TD
 25 |   ||| Transition function
 26 |   transFn : (labels, state) -> List (labels, state)
 27 |   ||| Initial state
 28 |   iState : labels
 29 |
 30 | %name Diagram td,td1,td2
 31 |
 32 | ||| Parallel composition of transition diagrams
 33 | public export
 34 | pComp :  {Lbls1, Lbls2 : _} -> {Sts : _}
 35 |       -> (td1 : Diagram Lbls1 Sts)
 36 |       -> (td2 : Diagram Lbls2 Sts)
 37 |       -> Diagram (Lbls1, Lbls2) Sts
 38 | pComp (TD transFn1 iState1) (TD transFn2 iState2) =
 39 |   TD compTransFn (iState1, iState2)
 40 |   where
 41 |     compTransFn : ((Lbls1, Lbls2), Sts) -> List ((Lbls1, Lbls2), Sts)
 42 |     compTransFn = (\ ((l1, l2), st) =>
 43 |                     map (\ (l1', st') => ((l1', l2), st')) (transFn1 (l1, st)) ++
 44 |                     map (\ (l2', st') => ((l1, l2'), st')) (transFn2 (l2, st)))
 45 |
 46 | ||| A process which always increases the shared number.
 47 | public export
 48 | HiHorse : Diagram () Nat
 49 | HiHorse = TD transFn ()
 50 |   where
 51 |     transFn : ((), Nat) -> List ((), Nat)
 52 |     transFn (l, st) = [(l, (S st))]
 53 |
 54 | ||| A process which always decreases the shared number.
 55 | public export
 56 | LoRoad : Diagram () Nat
 57 | LoRoad = TD transFn ()
 58 |   where
 59 |     transFn : ((), Nat) -> List ((), Nat)
 60 |     transFn (l, st) = [(l, pred st)]
 61 |
 62 | -- different formulation of LTE, see also:
 63 | -- https://agda.github.io/agda-stdlib/Data.Nat.Base.html#4636
 64 | -- thanks @gallais!
 65 | public export
 66 | data LTE' : (n : Nat) -> (m : Nat) -> Type where
 67 |   LTERefl : LTE' m m
 68 |   LTEStep : LTE' n m -> LTE' n (S m)
 69 |
 70 | ||| Convert LTE' to LTE
 71 | lteAltToLTE : {m : _} -> LTE' n m -> LTE n m
 72 | lteAltToLTE {m=0} LTERefl = LTEZero
 73 | lteAltToLTE {m=(S k)} LTERefl = LTESucc (lteAltToLTE LTERefl)
 74 | lteAltToLTE {m=(S m)} (LTEStep s) = lteSuccRight (lteAltToLTE s)
 75 |
 76 |
 77 | parameters (Lbls, Sts : Type)
 78 |   ||| A computation tree (corecursive rose tree?)
 79 |   public export
 80 |   data CT : Type where
 81 |     At : (Lbls, Sts) -> Inf (List CT) -> CT
 82 |
 83 |   ||| Given a transition diagram and a starting value for the shared state,
 84 |   ||| construct the computation tree of the given transition diagram.
 85 |   public export
 86 |   model : Diagram Lbls Sts -> (st : Sts) -> CT
 87 |   model (TD transFn iState) st = follow (iState, st)
 88 |     where
 89 |       follow : (Lbls, Sts) -> CT
 90 |
 91 |       followAll : List (Lbls, Sts) -> List CT
 92 |
 93 |       follow st = At st (Delay (followAll (transFn st)))
 94 |
 95 |       followAll [] = []
 96 |       followAll (st :: sts) = follow st :: followAll sts
 97 |
 98 |   ||| A formula has a bound (for Bounded Model Checking; BMC) and a computation
 99 |   ||| tree to check against.
100 |   public export
101 |   Formula : Type
102 |   Formula = (depth : Nat) -> (tree : CT) -> Type
103 |
104 |   ||| A tree models a formula if there exists a depth d0 for which the property
105 |   ||| holds for all depths d >= d0.
106 |   -- Called "satisfies" in the paper
107 |   public export
108 |   data Models : (m : CT) -> (f : Formula) -> Type where
109 |     ItModels : (d0 : Nat) -> ({d : Nat} -> (d0 `LTE'` d) -> f d m) -> Models m f
110 |
111 |   ------------------------------------------------------------------------
112 |   -- Depth invariance
113 |
114 |   ||| Depth-invariance (DI) is when a formula cannot be falsified by increasing
115 |   ||| the search depth.
116 |   public export
117 |   record DepthInv (f : Formula) where
118 |     constructor DI
119 |     prf : {n : Nat} -> {m : CT} -> f n m -> f (S n) m
120 |
121 |   ||| A DI-formula holding for a specific depth means the CT models the formula
122 |   ||| in general (we could increase the search depth and still be fine).
123 |   public export
124 |   diModels :  {n : Nat} -> {m : CT} -> {f : Formula} -> {auto d : DepthInv f}
125 |            -> (p : f n m) -> Models m f
126 |   diModels {n} {f} {m} @{(DI diPrf)} p = ItModels n (\ q => diLTE p q)
127 |     where
128 |       diLTE : {n, n' : _} -> f n m -> (ltePrf' : n `LTE'` n') -> f n' m
129 |       diLTE p LTERefl = p
130 |       diLTE p (LTEStep x) = diPrf (diLTE p x)
131 |
132 |   ||| A trivially true (TT) formula.
133 |   public export
134 |   data TrueF : Formula where
135 |     TT : {n : _} -> {m : _} -> TrueF n m
136 |
137 |   ||| A tt formula is depth-invariant.
138 |   public export
139 |   %hint
140 |   TrueDI : DepthInv TrueF
141 |   TrueDI = DI (const TT)
142 |
143 |   ------------------------------------------------------------------------
144 |   -- Guards
145 |
146 |   namespace Guards
147 |     ||| The formula `Guarded g` is true when the current state satisfies the
148 |     ||| guard `g`.
149 |     public export
150 |     data Guarded : (g : (st : Sts) -> (l : Lbls) -> Type) -> Formula where
151 |       Here :  {st : _} -> {l : _}
152 |            -> {ms : Inf (List CT)} -> {depth : Nat}
153 |            -> {g : _}
154 |            -> (guardOK : g st l)
155 |            -> Guarded g depth (At (l, st) ms)
156 |
157 |     ||| Guarded expressions are depth-invariant as the guard does not care about
158 |     ||| depth.
159 |     public export
160 |     %hint
161 |     diGuarded : {p : _} -> DepthInv (Guarded p)
162 |     diGuarded {p} = DI prf
163 |       where
164 |         prf : {n : _} -> {m : _} -> Guarded p n m -> Guarded p (S n) m
165 |         prf (Here x) = Here x   -- can be interactively generated!
166 |
167 |   ------------------------------------------------------------------------
168 |   -- Conjunction / And
169 |
170 |   ||| Conjunction of two `Formula`s
171 |   public export
172 |   record AND' (f, g : Formula) (depth : Nat) (tree : CT) where
173 |     constructor MkAND' --: {n : _} -> {m : _} -> f n m -> g n m -> (AND' f g) n m
174 |     fst : f depth tree
175 |     snd : g depth tree
176 |
177 |   ||| Conjunction is depth-invariant
178 |   public export
179 |   %hint
180 |   diAND' :  {f, g : Formula}
181 |          -> {auto p : DepthInv f}
182 |          -> {auto q : DepthInv g}
183 |          -> DepthInv (AND' f g)
184 |   diAND' @{(DI diP)} @{(DI diQ)} = DI (\ a' => MkAND' (diP a'.fst) (diQ a'.snd))
185 |
186 |   ------------------------------------------------------------------------
187 |   -- Always Until
188 |
189 |   namespace AU
190 |     ||| A proof that for all paths in the tree, f holds until g does.
191 |     public export
192 |     data AlwaysUntil : (f, g : Formula) -> Formula where
193 |       ||| We've found a place where g holds, so we're done.
194 |       Here : {t : _} -> {n : _} -> g n t -> AlwaysUntil f g (S n) t
195 |
196 |       ||| If f still holds and we can recursively show that g holds for all
197 |       ||| possible subpaths in the CT, then all branches have f hold until g
198 |       ||| does.
199 |       There :  {st : _} -> {infCTs : Inf _} -> {n : _}
200 |             -> f n (At st infCTs)
201 |             -> All ((AlwaysUntil f g) n) (Force infCTs)
202 |             -> AlwaysUntil f g (S n) (At st infCTs)
203 |
204 |     ||| Provided `f` and `g` are depth-invariant, AlwaysUntil is
205 |     ||| depth-invariant.
206 |     public export
207 |     %hint
208 |     diAU :  {f,g : _} -> {auto p : DepthInv f} -> {auto q : DepthInv g}
209 |          -> DepthInv (AlwaysUntil f g)
210 |     diAU @{(DI diP)} @{(DI diQ)} = DI prf
211 |       where
212 |         prf :  {d : _} -> {t : _}
213 |             -> AlwaysUntil f g d t
214 |             -> AlwaysUntil f g (S d) t
215 |         prf (Here au) = Here (diQ au)
216 |         prf (There au aus) = There (diP au) (mapAllAU aus)
217 |           where
218 |             -- `All.mapProperty` erases the list and so won't work here
219 |             mapAllAU :  {d : _} -> {lt : _}
220 |                      -> All (AlwaysUntil f g d) lt
221 |                      -> All (AlwaysUntil f g (S d)) lt
222 |             mapAllAU [] = []
223 |             mapAllAU (au :: aus) = (prf au) :: mapAllAU aus
224 |
225 |
226 |   ------------------------------------------------------------------------
227 |   -- Exists Until
228 |
229 |   namespace EU
230 |     ||| A proof that somewhere in the tree, there is a path for which f holds
231 |     ||| until g does.
232 |     public export
233 |     data ExistsUntil : (f, g : Formula) -> Formula where
234 |       ||| If g holds here, we've found a branch where we can stop.
235 |       Here : {t : _} -> {n : _} -> g n t -> ExistsUntil f g (S n) t
236 |
237 |       ||| If f holds here and any of the further branches have a g, then there
238 |       ||| is a branch where f holds until g does.
239 |       There :  {st : _} -> {infCTs : Inf _} -> {n : _}
240 |             -> f n (At st infCTs)
241 |             -> Any (ExistsUntil f g n) (Force infCTs)
242 |             -> ExistsUntil f g (S n) (At st infCTs)
243 |
244 |     ||| Provided `f` and `g` are depth-invariant, ExistsUntil is
245 |     ||| depth-invariant.
246 |     public export
247 |     %hint
248 |     diEU :  {f, g : _} -> {auto p : DepthInv f} -> {auto q : DepthInv g}
249 |          -> DepthInv (ExistsUntil f g)
250 |     diEU @{(DI diP)} @{(DI diQ)} = DI prf
251 |       where
252 |         prf :  {d : _} -> {t : _}
253 |             -> ExistsUntil f g d t
254 |             -> ExistsUntil f g (S d) t
255 |         prf (Here eu) = Here (diQ eu)
256 |         prf (There eu eus) = There (diP eu) (mapAnyEU eus)
257 |           where
258 |             -- `Any.mapProperty` erases the list and so won't work here
259 |             mapAnyEU :  {d : _} -> {lt : _}
260 |                      -> Any (ExistsUntil f g d) lt
261 |                      -> Any (ExistsUntil f g (S d)) lt
262 |             mapAnyEU (Here y) = Here (prf y)
263 |             mapAnyEU (There x) = There (mapAnyEU x)
264 |
265 |
266 |   ------------------------------------------------------------------------
267 |   -- Finally, Completed, and the finite forms of Global
268 |
269 |   ||| "Always finally" means that for all paths, the formula f will eventually
270 |   ||| hold.
271 |   |||
272 |   ||| This is equivalent to saying `A [TT U f]` (where TT is trivially true).
273 |   public export
274 |   AlwaysFinally : Formula -> Formula
275 |   AlwaysFinally f = AlwaysUntil TrueF f
276 |
277 |   ||| "Exists finally" means that for some pathe, the formula f will eventually
278 |   ||| hold.
279 |   |||
280 |   ||| This is equivalent to saying `E [TT U f]` (where TT is trivially true).
281 |   public export
282 |   ExistsFinally : Formula -> Formula
283 |   ExistsFinally f = ExistsUntil TrueF f
284 |
285 |   ||| A completed formula is a formula for which no more successor states exist.
286 |   public export
287 |   data Completed : Formula where
288 |     IsCompleted :  {st : _} -> {n : _} -> {infCTs : Inf _}
289 |                 -> (Force infCTs) === []
290 |                 -> Completed n (At st infCTs)
291 |
292 |   ||| A completed formula is depth-invariant (there is nothing more to do).
293 |   public export
294 |   %hint
295 |   diCompleted : DepthInv Completed
296 |   diCompleted = DI prf
297 |     where
298 |       prf : {d : _} -> {t : _} -> Completed d t -> Completed (S d) t
299 |       prf (IsCompleted p) = IsCompleted p
300 |
301 |   ||| We can only handle always global checks on finite paths.
302 |   public export
303 |   AlwaysGlobal : (f : Formula) -> Formula
304 |   AlwaysGlobal f = AlwaysUntil f (f `AND'` Completed)
305 |
306 |   ||| We can only handle exists global checks on finite paths.
307 |   public export
308 |   ExistsGlobal : (f : Formula) -> Formula
309 |   ExistsGlobal f = ExistsUntil f (f `AND'` Completed)
310 |
311 |
312 |   ------------------------------------------------------------------------
313 |   -- Proof search (finally!)
314 |
315 |   ||| Model-checking is a half-decider for the formula `f`
316 |   public export
317 |   MC : (f : Formula) -> Type
318 |   MC f = (t : CT) -> (d : Nat) -> HDec (f d t)
319 |
320 |   ||| Proof-search combinator for guards.
321 |   public export
322 |   now :  {g : (st : Sts) -> (l : Lbls) -> Type}
323 |       -> {hdec : _}
324 |       -> {auto p : AnHDec hdec}
325 |       -> ((st : Sts) -> (l : Lbls) -> hdec (g st l))
326 |       -> MC (Guarded g)
327 |   now f (At (l, st) ms) d = [| Guards.Here (toHDec (f st l)) |]
328 |
329 |   ||| Check if the current state has any successors.
330 |   public export
331 |   isCompleted : MC Completed
332 |   isCompleted (At st ms) _ = IsCompleted <$> isEmpty (Force ms)
333 |     where
334 |       ||| Half-decider for whether a list is empty
335 |       isEmpty : {x : _} -> (n : List x) -> HDec (n === [])
336 |       isEmpty [] = yes Refl
337 |       isEmpty (_ :: _) = no
338 |
339 |   ||| Conjunction of model-checking procedures.
340 |   public export
341 |   mcAND' : {f, g : Formula} -> MC f -> MC g -> MC (f `AND'` g)
342 |   mcAND' mcF mcG t d = [| MkAND' (mcF t d) (mcG t d) |]
343 |
344 |   ||| Proof-search for `AlwaysUntil`.
345 |   |||
346 |   ||| Evaluates the entire `Inf (List CT)` of the state-space, since we need
347 |   ||| `f U g` to hold across every path.
348 |   public export
349 |   auSearch : {f, g : Formula} -> MC f -> MC g -> MC (AlwaysUntil f g)
350 |   auSearch _ _ _ Z = no
351 |   auSearch p1 p2 t@(At st ms) (S n) =  [| AU.Here  (p2 t n) |]
352 |                                    <|> [| AU.There (p1 t n) rest |]
353 |     where
354 |       -- in AlwaysUntil searches, we have to check the entire `Inf (List CT)`
355 |       rest : HDec (All (AlwaysUntil f g n) (Force ms))
356 |       rest = HDecidable.List.all (toList ms) (\ m => auSearch p1 p2 m n)
357 |
358 |   ||| Proof-search for `ExistsUntil`.
359 |   |||
360 |   ||| `Inf` over the state-space, since `E [f U g]` holds as soon as `f U g` is
361 |   ||| found.
362 |   public export
363 |   euSearch : {f, g : Formula} -> MC f -> MC g -> MC (ExistsUntil f g)
364 |   euSearch _ _ _ Z = no
365 |   euSearch p1 p2 t@(At st ms) (S n) =  [| EU.Here  (p2 t n) |]
366 |                                    <|> [| EU.There (p1 t n) rest |]
367 |     where
368 |       rest : HDec (Any (ExistsUntil f g n) ms)
369 |       rest = HDecidable.List.any (Force ms) (\ m => euSearch p1 p2 m n)
370 |
371 |   ||| Proof-search for Exists Finally
372 |   public export
373 |   efSearch : {f : _} -> MC f -> MC (ExistsFinally f)
374 |   efSearch g = euSearch (\ _, _ => yes TT) g
375 |
376 |   ||| Proof-search for Always Finally
377 |   public export
378 |   afSearch : {f : _} -> MC f -> MC (AlwaysFinally f)
379 |   afSearch g = auSearch (\ _, _ => yes TT) g
380 |
381 |   ||| Proof-search for Exists Global
382 |   public export
383 |   egSearch : {f : _} -> MC f -> MC (ExistsGlobal f)
384 |   egSearch g = euSearch g (g `mcAND'` isCompleted)
385 |
386 |   ||| Proof-search for Always Global
387 |   public export
388 |   agSearch : {f : _} -> MC f -> MC (AlwaysGlobal f)
389 |   agSearch g = auSearch g (g `mcAND'` isCompleted)
390 |
391 |
392 | ------------------------------------------------------------------------
393 | -- Proof search example
394 |
395 | ||| This CT is a model of composing the `HiHorse` and `LoRoad` programs.
396 | public export
397 | tree : CT ((), ()) Nat
398 | tree = model ((), ()) Nat (HiHorse `pComp` LoRoad) 0
399 |
400 | ||| A half-decider for proving that there exists a path where the shared
401 | ||| `HiHorse || LoRoad` state reaches 10.
402 | public export
403 | reaches10 : ?   -- HDec (ExistsFinally [...])
404 | reaches10 =
405 |   efSearch ((), ()) Nat
406 |       (now ((), ()) Nat
407 |           (\st, _ => fromDec $ decEq st 10)) tree 20
408 |
409 | ||| Prove that the shared state of `HiHorse || LoRoad` reaches 10, using the
410 | ||| previously defined half-decider.
411 | export
412 | r10Proof : Models ((), ()) Nat
413 |               CTL.tree
414 |               (ExistsFinally ((), ()) Nat
415 |                   (Guarded ((), ()) Nat (\ st, _ => st === 10)))
416 | r10Proof = diModels ((), ()) Nat (reaches10.evidence Oh)
417 |
418 |