Properties
Basics
A property is any self-contained statement that you wish to check using Vehicle.
Properties are declared by annotating declarations with the @property
annotation:
@property
robust : Bool
robust = forall x . f x ! 0 >= 0.0
Only declarations with the types Bool
, Vector Bool n
or Tensor Bool n
may
be annotated as properties. In the latter case, Vehicle will report the status of each
element of the Vector
or Tensor
individually.
The foreach
quantifier
A common use of the forall
quantifier is to assert that a
predicate holds over every element of a dataset, e.g.
@dataset
trainingDataset : List (Tensor Rat [28, 28])
...
robust : Bool
robust = forall x in trainingDataset . robustAround x
The problem with this formulation of the specification is that Vehicle will only report whether the network is robust around all the elements in the dataset. This is unlikely to be true.
Instead the foreach
quantifier may be used. Instead of returning a
single value of type Bool
it constructs a Tensor
of Bool
values. When used a property, Vehicle will therefore report
on the verification status of each individual element.
@dataset
trainingDataset : List (Tensor Rat [28, 28])
...
robust : List Bool
robust = foreach x in trainingDataset . robustAround x
Unlike the forall
keyword, the foreach
keyword cannot be used to
quantify over infinite types. It _can_ be used to quantify over Index
types.