Search.CTL

(source)

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
https://doi.org/10.1145/2976022.2976030

Reexports

import public Search.Negation
import public Search.HDecidable
import public Search.Properties

Definitions

record Diagram : Type -> Type -> Type

  Labeled transition diagram

Totality: total
Visibility: public export
Constructor:

TD : ((labels, state) -> List (labels, state)) -> labels -> Diagram labels state

Projections:

.iState : Diagram labels state -> labels

  Initial state

.transFn : Diagram labels state -> (labels, state) -> List (labels, state)

  Transition function

.transFn : Diagram labels state -> (labels, state) -> List (labels, state)

  Transition function

Totality: total
Visibility: public export

transFn : Diagram labels state -> (labels, state) -> List (labels, state)

  Transition function

Totality: total
Visibility: public export

.iState : Diagram labels state -> labels

  Initial state

Totality: total
Visibility: public export

iState : Diagram labels state -> labels

  Initial state

Totality: total
Visibility: public export

pComp : {Lbls1 : Type} -> {Lbls2 : Type} -> {Sts : Type} -> Diagram Lbls1 Sts -> Diagram Lbls2 Sts -> Diagram (Lbls1, Lbls2) Sts

  Parallel composition of transition diagrams

Totality: total
Visibility: public export

HiHorse : Diagram () Nat

  A process which always increases the shared number.

Totality: total
Visibility: public export

LoRoad : Diagram () Nat

  A process which always decreases the shared number.

Totality: total
Visibility: public export

data LTE' : Nat -> Nat -> Type

Totality: total
Visibility: public export
Constructors:

LTERefl : LTE' m m
LTEStep : LTE' n m -> LTE' n (S m)

data CT : Type -> Type -> Type

  A computation tree (corecursive rose tree?)

Totality: total
Visibility: public export
Constructor:

At : (Lbls : Type) -> (Sts : Type) -> (Lbls, Sts) -> Inf (List CT) -> CT

Hints:

(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AlwaysUntil f g)
(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (ExistsUntil f g)

model : (Lbls : Type) -> (Sts : Type) -> Diagram Lbls Sts -> Sts -> CT

  Given a transition diagram and a starting value for the shared state,
  construct the computation tree of the given transition diagram.

Totality: total
Visibility: public export

Formula : Type -> Type -> Type

  A formula has a bound (for Bounded Model Checking; BMC) and a computation
  tree to check against.

Totality: total
Visibility: public export

data Models : (Lbls : Type) -> (Sts : Type) -> CT -> Formula -> Type

  A tree models a formula if there exists a depth d0 for which the property
  holds for all depths d >= d0.

Totality: total
Visibility: public export
Constructor:

ItModels : (Lbls : Type) -> (Sts : Type) -> (d0 : Nat) -> (LTE' d0 d -> f d m) -> Models m f

record DepthInv : (Lbls : Type) -> (Sts : Type) -> Formula -> Type

  Depth-invariance (DI) is when a formula cannot be falsified by increasing
  the search depth.

Totality: total
Visibility: public export
Constructor:

DI : (Lbls : Type) -> (Sts : Type) -> (f n m -> f (S n) m) -> DepthInv f

Projection:

.prf : (Lbls : Type) -> (Sts : Type) -> DepthInv f -> f n m -> f (S n) m

Hints:

(Lbls : Type) -> (Sts : Type) -> DepthInv TrueF
(Lbls : Type) -> (Sts : Type) -> DepthInv (Guarded p)
(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AND' f g)
(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AlwaysUntil f g)
(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (ExistsUntil f g)
(Lbls : Type) -> (Sts : Type) -> DepthInv Completed

.prf : (Lbls : Type) -> (Sts : Type) -> DepthInv f -> f n m -> f (S n) m

Totality: total
Visibility: public export

prf : (Lbls : Type) -> (Sts : Type) -> DepthInv f -> f n m -> f (S n) m

Totality: total
Visibility: public export

diModels : (Lbls : Type) -> (Sts : Type) -> DepthInv f => f n m -> Models m f

  A DI-formula holding for a specific depth means the CT models the formula
  in general (we could increase the search depth and still be fine).

Totality: total
Visibility: public export

data TrueF : (Lbls : Type) -> (Sts : Type) -> Formula

  A trivially true (TT) formula.

Totality: total
Visibility: public export
Constructor:

TT : (Lbls : Type) -> (Sts : Type) -> TrueF n m

Hint:

(Lbls : Type) -> (Sts : Type) -> DepthInv TrueF

TrueDI : (Lbls : Type) -> (Sts : Type) -> DepthInv TrueF

  A tt formula is depth-invariant.

Totality: total
Visibility: public export

data Guarded : (Lbls : Type) -> (Sts : Type) -> (Sts -> Lbls -> Type) -> Formula

  The formula `Guarded g` is true when the current state satisfies the
  guard `g`.

Totality: total
Visibility: public export
Constructor:

Here : (Lbls : Type) -> (Sts : Type) -> g st l -> Guarded g depth (At (l, st) ms)

Hint:

(Lbls : Type) -> (Sts : Type) -> DepthInv (Guarded p)

diGuarded : (Lbls : Type) -> (Sts : Type) -> DepthInv (Guarded p)

  Guarded expressions are depth-invariant as the guard does not care about
  depth.

Totality: total
Visibility: public export

record AND' : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula -> Nat -> CT -> Type

  Conjunction of two `Formula`s

Totality: total
Visibility: public export
Constructor:

MkAND' : (Lbls : Type) -> (Sts : Type) -> f depth tree -> g depth tree -> AND' f g depth tree

Projections:

.fst : (Lbls : Type) -> (Sts : Type) -> AND' f g depth tree -> f depth tree
.snd : (Lbls : Type) -> (Sts : Type) -> AND' f g depth tree -> g depth tree

Hint:

(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AND' f g)

.fst : (Lbls : Type) -> (Sts : Type) -> AND' f g depth tree -> f depth tree

Totality: total
Visibility: public export

fst : (Lbls : Type) -> (Sts : Type) -> AND' f g depth tree -> f depth tree

Totality: total
Visibility: public export

.snd : (Lbls : Type) -> (Sts : Type) -> AND' f g depth tree -> g depth tree

Totality: total
Visibility: public export

snd : (Lbls : Type) -> (Sts : Type) -> AND' f g depth tree -> g depth tree

Totality: total
Visibility: public export

diAND' : (Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AND' f g)

  Conjunction is depth-invariant

Totality: total
Visibility: public export

data AlwaysUntil : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula -> Formula

  A proof that for all paths in the tree, f holds until g does.

Totality: total
Visibility: public export
Constructors:

Here : (Lbls : Type) -> (Sts : Type) -> g n t -> AlwaysUntil f g (S n) t

  We've found a place where g holds, so we're done.

There : (Lbls : Type) -> (Sts : Type) -> f n (At st infCTs) -> All (AlwaysUntil f g n) (Force infCTs) -> AlwaysUntil f g (S n) (At st infCTs)

  If f still holds and we can recursively show that g holds for all
  possible subpaths in the CT, then all branches have f hold until g
  does.

Hint:

(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AlwaysUntil f g)

diAU : (Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (AlwaysUntil f g)

  Provided `f` and `g` are depth-invariant, AlwaysUntil is
  depth-invariant.

Totality: total
Visibility: public export

data ExistsUntil : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula -> Formula

  A proof that somewhere in the tree, there is a path for which f holds
  until g does.

Totality: total
Visibility: public export
Constructors:

Here : (Lbls : Type) -> (Sts : Type) -> g n t -> ExistsUntil f g (S n) t

  If g holds here, we've found a branch where we can stop.

There : (Lbls : Type) -> (Sts : Type) -> f n (At st infCTs) -> Any (ExistsUntil f g n) (Force infCTs) -> ExistsUntil f g (S n) (At st infCTs)

  If f holds here and any of the further branches have a g, then there
  is a branch where f holds until g does.

Hint:

(Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (ExistsUntil f g)

diEU : (Lbls : Type) -> (Sts : Type) -> DepthInv f => DepthInv g => DepthInv (ExistsUntil f g)

  Provided `f` and `g` are depth-invariant, ExistsUntil is
  depth-invariant.

Totality: total
Visibility: public export

AlwaysFinally : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula

  "Always finally" means that for all paths, the formula f will eventually
  hold.
  
  This is equivalent to saying `A [TT U f]` (where TT is trivially true).

Totality: total
Visibility: public export

ExistsFinally : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula

  "Exists finally" means that for some pathe, the formula f will eventually
  hold.
  
  This is equivalent to saying `E [TT U f]` (where TT is trivially true).

Totality: total
Visibility: public export

data Completed : (Lbls : Type) -> (Sts : Type) -> Formula

  A completed formula is a formula for which no more successor states exist.

Totality: total
Visibility: public export
Constructor:

IsCompleted : (Lbls : Type) -> (Sts : Type) -> (Force infCTs) = [] -> Completed n (At st infCTs)

Hint:

(Lbls : Type) -> (Sts : Type) -> DepthInv Completed

diCompleted : (Lbls : Type) -> (Sts : Type) -> DepthInv Completed

  A completed formula is depth-invariant (there is nothing more to do).

Totality: total
Visibility: public export

AlwaysGlobal : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula

  We can only handle always global checks on finite paths.

Totality: total
Visibility: public export

ExistsGlobal : (Lbls : Type) -> (Sts : Type) -> Formula -> Formula

  We can only handle exists global checks on finite paths.

Totality: total
Visibility: public export

MC : (Lbls : Type) -> (Sts : Type) -> Formula -> Type

  Model-checking is a half-decider for the formula `f`

Totality: total
Visibility: public export

now : (Lbls : Type) -> (Sts : Type) -> AnHDec hdec => ((st : Sts) -> (l : Lbls) -> hdec (g st l)) -> MC (Guarded g)

  Proof-search combinator for guards.

Totality: total
Visibility: public export

isCompleted : (Lbls : Type) -> (Sts : Type) -> MC Completed

  Check if the current state has any successors.

Totality: total
Visibility: public export

mcAND' : (Lbls : Type) -> (Sts : Type) -> MC f -> MC g -> MC (AND' f g)

  Conjunction of model-checking procedures.

Totality: total
Visibility: public export

auSearch : (Lbls : Type) -> (Sts : Type) -> MC f -> MC g -> MC (AlwaysUntil f g)

  Proof-search for `AlwaysUntil`.
  
  Evaluates the entire `Inf (List CT)` of the state-space, since we need
  `f U g` to hold across every path.

Totality: total
Visibility: public export

euSearch : (Lbls : Type) -> (Sts : Type) -> MC f -> MC g -> MC (ExistsUntil f g)

  Proof-search for `ExistsUntil`.
  
  `Inf` over the state-space, since `E [f U g]` holds as soon as `f U g` is
  found.

Totality: total
Visibility: public export

efSearch : (Lbls : Type) -> (Sts : Type) -> MC f -> MC (ExistsFinally f)

  Proof-search for Exists Finally

Totality: total
Visibility: public export

afSearch : (Lbls : Type) -> (Sts : Type) -> MC f -> MC (AlwaysFinally f)

  Proof-search for Always Finally

Totality: total
Visibility: public export

egSearch : (Lbls : Type) -> (Sts : Type) -> MC f -> MC (ExistsGlobal f)

  Proof-search for Exists Global

Totality: total
Visibility: public export

agSearch : (Lbls : Type) -> (Sts : Type) -> MC f -> MC (AlwaysGlobal f)

  Proof-search for Always Global

Totality: total
Visibility: public export

tree : CT

  This CT is a model of composing the `HiHorse` and `LoRoad` programs.

Totality: total
Visibility: public export

reaches10 : HDec (ExistsFinally (\depth, tree => Guarded (\st, l => st = 10) depth tree) 20 tree)

  A half-decider for proving that there exists a path where the shared
  `HiHorse || LoRoad` state reaches 10.

Totality: total
Visibility: public export

r10Proof : Models tree (ExistsFinally (Guarded (\st, {_:8706} => st = 10)))

  Prove that the shared state of `HiHorse || LoRoad` reaches 10, using the
  previously defined half-decider.

Totality: total
Visibility: export