Search.CTL


   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 prf aus)
 217 |           where
 218 |             -- `All.mapProperty` erases the list and so won't work here
 219 |             mapAllAU :  {d : _} -> {lt : _}
 220 |                      -> (prf : AlwaysUntil f g d t -> AlwaysUntil f g (S d) t)
 221 |                      -> All (AlwaysUntil f g d) lt
 222 |                      -> All (AlwaysUntil f g (S d)) lt
 223 |             mapAllAU prf [] = []
 224 |             mapAllAU prf (au :: aus) = (prf au) :: mapAllAU prf aus
 225 | 
 226 | 
 227 |   ------------------------------------------------------------------------
 228 |   -- Exists Until
 229 | 
 230 |   namespace EU
 231 |     ||| A proof that somewhere in the tree, there is a path for which f holds
 232 |     ||| until g does.
 233 |     public export
 234 |     data ExistsUntil : (f, g : Formula) -> Formula where
 235 |       ||| If g holds here, we've found a branch where we can stop.
 236 |       Here : {t : _} -> {n : _} -> g n t -> ExistsUntil f g (S n) t
 237 | 
 238 |       ||| If f holds here and any of the further branches have a g, then there
 239 |       ||| is a branch where f holds until g does.
 240 |       There :  {st : _} -> {infCTs : Inf _} -> {n : _}
 241 |             -> f n (At st infCTs)
 242 |             -> Any (ExistsUntil f g n) (Force infCTs)
 243 |             -> ExistsUntil f g (S n) (At st infCTs)
 244 | 
 245 |     ||| Provided `f` and `g` are depth-invariant, ExistsUntil is
 246 |     ||| depth-invariant.
 247 |     public export
 248 |     %hint
 249 |     diEU :  {f, g : _} -> {auto p : DepthInv f} -> {auto q : DepthInv g}
 250 |          -> DepthInv (ExistsUntil f g)
 251 |     diEU @{(DI diP)} @{(DI diQ)} = DI prf
 252 |       where
 253 |         prf :  {d : _} -> {t : _}
 254 |             -> ExistsUntil f g d t
 255 |             -> ExistsUntil f g (S d) t
 256 |         prf (Here eu) = Here (diQ eu)
 257 |         prf (There eu eus) = There (diP eu) (mapAnyEU prf eus)
 258 |           where
 259 |             -- `Any.mapProperty` erases the list and so won't work here
 260 |             mapAnyEU :  {d : _} -> {lt : _}
 261 |                      -> (prf : ExistsUntil f g d t -> ExistsUntil f g (S d) t)
 262 |                      -> Any (ExistsUntil f g d) lt
 263 |                      -> Any (ExistsUntil f g (S d)) lt
 264 |             mapAnyEU prf (Here x) = Here (prf x)
 265 |             mapAnyEU prf (There x) = There (mapAnyEU prf x)
 266 | 
 267 | 
 268 |   ------------------------------------------------------------------------
 269 |   -- Finally, Completed, and the finite forms of Global
 270 | 
 271 |   ||| "Always finally" means that for all paths, the formula f will eventually
 272 |   ||| hold.
 273 |   |||
 274 |   ||| This is equivalent to saying `A [TT U f]` (where TT is trivially true).
 275 |   public export
 276 |   AlwaysFinally : Formula -> Formula
 277 |   AlwaysFinally f = AlwaysUntil TrueF f
 278 | 
 279 |   ||| "Exists finally" means that for some pathe, the formula f will eventually
 280 |   ||| hold.
 281 |   |||
 282 |   ||| This is equivalent to saying `E [TT U f]` (where TT is trivially true).
 283 |   public export
 284 |   ExistsFinally : Formula -> Formula
 285 |   ExistsFinally f = ExistsUntil TrueF f
 286 | 
 287 |   ||| A completed formula is a formula for which no more successor states exist.
 288 |   public export
 289 |   data Completed : Formula where
 290 |     IsCompleted :  {st : _} -> {n : _} -> {infCTs : Inf _}
 291 |                 -> (Force infCTs) === []
 292 |                 -> Completed n (At st infCTs)
 293 | 
 294 |   ||| A completed formula is depth-invariant (there is nothing more to do).
 295 |   public export
 296 |   %hint
 297 |   diCompleted : DepthInv Completed
 298 |   diCompleted = DI prf
 299 |     where
 300 |       prf : {d : _} -> {t : _} -> Completed d t -> Completed (S d) t
 301 |       prf (IsCompleted p) = IsCompleted p
 302 | 
 303 |   ||| We can only handle always global checks on finite paths.
 304 |   public export
 305 |   AlwaysGlobal : (f : Formula) -> Formula
 306 |   AlwaysGlobal f = AlwaysUntil f (f `AND'` Completed)
 307 | 
 308 |   ||| We can only handle exists global checks on finite paths.
 309 |   public export
 310 |   ExistsGlobal : (f : Formula) -> Formula
 311 |   ExistsGlobal f = ExistsUntil f (f `AND'` Completed)
 312 | 
 313 | 
 314 |   ------------------------------------------------------------------------
 315 |   -- Proof search (finally!)
 316 | 
 317 |   ||| Model-checking is a half-decider for the formula `f`
 318 |   public export
 319 |   MC : (f : Formula) -> Type
 320 |   MC f = (t : CT) -> (d : Nat) -> HDec (f d t)
 321 | 
 322 |   ||| Proof-search combinator for guards.
 323 |   public export
 324 |   now :  {g : (st : Sts) -> (l : Lbls) -> Type}
 325 |       -> {hdec : _}
 326 |       -> {auto p : AnHDec hdec}
 327 |       -> ((st : Sts) -> (l : Lbls) -> hdec (g st l))
 328 |       -> MC (Guarded g)
 329 |   now f (At (l, st) ms) d = [| Guards.Here (toHDec (f st l)) |]
 330 | 
 331 |   ||| Check if the current state has any successors.
 332 |   public export
 333 |   isCompleted : MC Completed
 334 |   isCompleted (At st ms) _ = IsCompleted <$> isEmpty (Force ms)
 335 |     where
 336 |       ||| Half-decider for whether a list is empty
 337 |       isEmpty : {x : _} -> (n : List x) -> HDec (n === [])
 338 |       isEmpty [] = yes Refl
 339 |       isEmpty (_ :: _) = no
 340 | 
 341 |   ||| Conjunction of model-checking procedures.
 342 |   public export
 343 |   mcAND' : {f, g : Formula} -> MC f -> MC g -> MC (f `AND'` g)
 344 |   mcAND' mcF mcG t d = [| MkAND' (mcF t d) (mcG t d) |]
 345 | 
 346 |   ||| Proof-search for `AlwaysUntil`.
 347 |   |||
 348 |   ||| Evaluates the entire `Inf (List CT)` of the state-space, since we need
 349 |   ||| `f U g` to hold across every path.
 350 |   public export
 351 |   auSearch : {f, g : Formula} -> MC f -> MC g -> MC (AlwaysUntil f g)
 352 |   auSearch _ _ _ Z = no
 353 |   auSearch p1 p2 t@(At st ms) (S n) =  [| AU.Here  (p2 t n) |]
 354 |                                    <|> [| AU.There (p1 t n) rest |]
 355 |     where
 356 |       -- in AlwaysUntil searches, we have to check the entire `Inf (List CT)`
 357 |       rest : HDec (All (AlwaysUntil f g n) (Force ms))
 358 |       rest = HDecidable.List.all (toList ms) (\ m => auSearch p1 p2 m n)
 359 | 
 360 |   ||| Proof-search for `ExistsUntil`.
 361 |   |||
 362 |   ||| `Inf` over the state-space, since `E [f U g]` holds as soon as `f U g` is
 363 |   ||| found.
 364 |   public export
 365 |   euSearch : {f, g : Formula} -> MC f -> MC g -> MC (ExistsUntil f g)
 366 |   euSearch _ _ _ Z = no
 367 |   euSearch p1 p2 t@(At st ms) (S n) =  [| EU.Here  (p2 t n) |]
 368 |                                    <|> [| EU.There (p1 t n) rest |]
 369 |     where
 370 |       rest : HDec (Any (ExistsUntil f g n) ms)
 371 |       rest = HDecidable.List.any (Force ms) (\ m => euSearch p1 p2 m n)
 372 | 
 373 |   ||| Proof-search for Exists Finally
 374 |   public export
 375 |   efSearch : {f : _} -> MC f -> MC (ExistsFinally f)
 376 |   efSearch g = euSearch (\ _, _ => yes TT) g
 377 | 
 378 |   ||| Proof-search for Always Finally
 379 |   public export
 380 |   afSearch : {f : _} -> MC f -> MC (AlwaysFinally f)
 381 |   afSearch g = auSearch (\ _, _ => yes TT) g
 382 | 
 383 |   ||| Proof-search for Exists Global
 384 |   public export
 385 |   egSearch : {f : _} -> MC f -> MC (ExistsGlobal f)
 386 |   egSearch g = euSearch g (g `mcAND'` isCompleted)
 387 | 
 388 |   ||| Proof-search for Always Global
 389 |   public export
 390 |   agSearch : {f : _} -> MC f -> MC (AlwaysGlobal f)
 391 |   agSearch g = auSearch g (g `mcAND'` isCompleted)
 392 | 
 393 | 
 394 | ------------------------------------------------------------------------
 395 | -- Proof search example
 396 | 
 397 | ||| This CT is a model of composing the `HiHorse` and `LoRoad` programs.
 398 | public export
 399 | tree : CT ((), ()) Nat
 400 | tree = model ((), ()) Nat (HiHorse `pComp` LoRoad) 0
 401 | 
 402 | ||| A half-decider for proving that there exists a path where the shared
 403 | ||| `HiHorse || LoRoad` state reaches 10.
 404 | public export
 405 | reaches10 : ?   -- HDec (ExistsFinally [...])
 406 | reaches10 =
 407 |   efSearch ((), ()) Nat
 408 |       (now ((), ()) Nat
 409 |           (\st, _ => fromDec $ decEq st 10)) tree 20
 410 | 
 411 | ||| Prove that the shared state of `HiHorse || LoRoad` reaches 10, using the
 412 | ||| previously defined half-decider.
 413 | export
 414 | r10Proof : Models ((), ()) Nat
 415 |               CTL.tree
 416 |               (ExistsFinally ((), ()) Nat
 417 |                   (Guarded ((), ()) Nat (\ st, _ => st === 10)))
 418 | r10Proof = diModels ((), ()) Nat (reaches10.evidence Oh)
 419 | 
 420 |