[examples] Update mnist specification.

examples/mnist/mnist.why

+theory MNIST
+  use ieee_float.Float64
+  use int.Int
+  use nn.NeuralNetwork
+  use dataset.DatasetCSV
+  use robust.RobustDatasetCSV
+
+  constant min_label : label_ = 0
+  constant max_label : label_ = 9
+
+  predicate valid_label (l: label_) =
+    RobustDatasetCSV.valid_label min_label max_label l
+
+  goal robustness:
+    let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
+    let dataset = read_dataset_csv "csv/mnist_test.csv" in
+    let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
+    robust valid_label nn dataset eps
+end

examples/mnist/property.why

-theory MNIST
-  use ieee_float.Float64
-  use int.Int
-  use interpretation.Vector
-  use interpretation.NeuralNetwork
-  use interpretation.Dataset
-
-  type image = vector t
-  type label_ = int
-
-  predicate valid_image (i: image) =
-    forall v: index. valid_index i v -> (0.0: t) .<= i[v] .<= (1.0: t)
-
-  predicate valid_label (l: label_) = 0 <= l <= 9
-
-  predicate advises (n: nn) (i: image) (l: label_) =
-    valid_label l ->
-    forall j: int. valid_label j ->  j <> l -> (n@@i)[l] .> (n@@i)[j]
-
-  predicate bounded_by_epsilon (i: image) (eps: t) =
-    forall v: index. valid_index i v -> .- eps .<= i[v] .<= eps
-
-  predicate robust_around (n: nn) (eps: t) (l: label_) (i: image) =
-    forall perturbed_image: image.
-      has_length perturbed_image (length i) ->
-      valid_image perturbed_image ->
-      let perturbation = perturbed_image - i in
-      bounded_by_epsilon perturbation eps ->
-      advises n perturbed_image l
-
-  predicate robust (n: nn) (d: dataset label_ image) (eps: t) =
-    Dataset.forall_ d (robust_around n eps)
-
-  goal robustness:
-    let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
-    let dataset = read_dataset "csv/mnist_test.csv" CSV in
-    let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
-    robust nn dataset eps
-end