A property is any self-contained statement that you wish to check using Vehicle.
Properties are declared by annotating declarations with the
@property robust : Bool robust = forall x . f x ! 0 >= 0.0
Only declarations with the types
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
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.
foreach quantifier may be used. Instead of returning a
single value of type
Bool it constructs a
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
forall keyword, the
foreach keyword cannot be used to
quantify over infinite types. It _can_ be used to quantify over