[records] Add AIMOS amplitude type to stdlib

stdlib/caisar.mlw

@@ -24,11 +24,14 @@ theory DatasetClassification
   use ieee_float.Float64
   use int.Int
   use array.Array
+  use option.Option
 
   type features = array t
   type label_ = int
   type record = (features, label_)
   type dataset = array record
+  type amplitude_record = { start: int; stop: int; step: int }
+  type amplitude = option amplitude_record
 
   constant dataset: dataset
 
@@ -69,7 +72,7 @@ theory DatasetClassificationProps
   predicate cond_robust (m: model) (d: dataset) (eps: t) =
     correct m d /\ robust m d eps
 
-  predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (start: int) (stop: int) (step: int)
+  predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (ampli: amplitude)
 end
 
 theory NN