From dc0c17eca9f8a98d49314d43e8d27f4e9526e203 Mon Sep 17 00:00:00 2001
From: Aymeric Varasse <aymeric.varasse@cea.fr>
Date: Wed, 28 Jun 2023 18:05:36 +0200
Subject: [PATCH] [records] Add AIMOS amplitude type to stdlib
---
stdlib/caisar.mlw | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 8ff1b9d..31d5dbc 100644
--- a/stdlib/caisar.mlw
+++ b/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
--
GitLab