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.