diff --git a/ChangeLog.md b/ChangeLog.md index 4d86ab97a..6651797cc 100644 --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,9 @@ # Changelog for Vehicle +## Version 0.15 + +* Added functions `min` and `max` over rationals. + ## Version 0.14.1 * Removed `Explicit` as a command line compilation target option as it never worked. diff --git a/docs/language/tips-and-tricks.rst b/docs/language/tips-and-tricks.rst index bf9947852..6e3df0926 100644 --- a/docs/language/tips-and-tricks.rst +++ b/docs/language/tips-and-tricks.rst @@ -72,9 +72,6 @@ calculate the maximum score and then require it to be less than 0.2: .. code-block:: agda - max : Rat -> Rat -> Rat - max x y = if x <= y then x else y - largestScore : Tensor Rat [10] -> Rat largestScore xs = fold max 0 xs @@ -82,9 +79,9 @@ calculate the maximum score and then require it to be less than 0.2: isUncertainAbout x = largestScore (classify x) <= 0.2 However, this definition would experience an exponential blow-up when -compiled down to low-level verification queries, as each branch of the -10 :code:`if` statements would need to be explored. In total 1024 queries -would be generated. +compiled down to low-level verification queries, as :code:`max` is compiled down +to an :code:`if` statement and each branch of the 10 :code:`if` statements would +need to be explored. In total 1024 queries would be generated. This blow-up can be avoided by instead using a "relational" approach to encoding the constraint, instead stating that all classes scores must be less diff --git a/vehicle/lib/std.vcl b/vehicle/lib/std.vcl index 83aff8c5c..9caf210a8 100644 --- a/vehicle/lib/std.vcl +++ b/vehicle/lib/std.vcl @@ -13,6 +13,16 @@ typeAnn t a = a notBoolOp2 : (A -> B -> Bool) -> (A -> B -> Bool) notBoolOp2 f x y = not (f x y) +-------------------------------------------------------------------------------- +-- Orderings +-------------------------------------------------------------------------------- + +min : {{HasLeq a a}} -> a -> a -> a +min x y = if x <= y then x else y + +max : {{HasLeq a a}} -> a -> a -> a +max x y = if y <= x then x else y + -------------------------------------------------------------------------------- -- List -------------------------------------------------------------------------------- diff --git a/vehicle/tests/golden/compile/simple-minmax/Marabou.err.golden b/vehicle/tests/golden/compile/simple-minmax/Marabou.err.golden new file mode 100644 index 000000000..6a294b269 --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/Marabou.err.golden @@ -0,0 +1,12 @@ + +Warning: In property 'p', at least one of the generated queries were found to contain a strict inequality (i.e. constraints of the form 'x < y'). Unfortunately the Marabou query format only supports non-strict inequalities (i.e. constraints of the form 'x <= y'). + +In order to provide support, Vehicle has automatically converted the strict inequalities to non-strict inequalites. This is not sound, but errors will be at most the floating point epsilon used by the verifier, which is usually very small (e.g. 1e-9). However, this may lead to unexpected behaviour (e.g. loss of the law of excluded middle). + +See https://github.com/vehicle-lang/vehicle/issues/74 for further details. + + +Warning: In property 'p', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. + In queries 1, 2, 3 and 4: + f₀[input]!0 - no lower or upper bound + diff --git a/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query1.txt.golden b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query1.txt.golden new file mode 100644 index 000000000..7e7aa7d81 --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query1.txt.golden @@ -0,0 +1,7 @@ +// WARNING: This file was generated automatically by Vehicle +// and should not be modified manually! +// Metadata: +// - Marabou query format version: unknown +// - Vehicle version: 0.14.1+dev ++y0 -y1 <= 0.0 +y0 <= 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query2.txt.golden b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query2.txt.golden new file mode 100644 index 000000000..31d5dc6f4 --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query2.txt.golden @@ -0,0 +1,7 @@ +// WARNING: This file was generated automatically by Vehicle +// and should not be modified manually! +// Metadata: +// - Marabou query format version: unknown +// - Vehicle version: 0.14.1+dev +-y0 +y1 <= 0.0 +y1 <= 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query3.txt.golden b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query3.txt.golden new file mode 100644 index 000000000..644bf978f --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query3.txt.golden @@ -0,0 +1,7 @@ +// WARNING: This file was generated automatically by Vehicle +// and should not be modified manually! +// Metadata: +// - Marabou query format version: unknown +// - Vehicle version: 0.14.1+dev +-y0 +y1 <= 0.0 +y0 >= 1.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query4.txt.golden b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query4.txt.golden new file mode 100644 index 000000000..d7f897e94 --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query4.txt.golden @@ -0,0 +1,7 @@ +// WARNING: This file was generated automatically by Vehicle +// and should not be modified manually! +// Metadata: +// - Marabou query format version: unknown +// - Vehicle version: 0.14.1+dev ++y0 -y1 <= 0.0 +y1 >= 1.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p.vcl-plan.golden b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p.vcl-plan.golden new file mode 100644 index 000000000..9b81427a3 --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p.vcl-plan.golden @@ -0,0 +1,871 @@ +{ + "queryMetaData": { + "tag": "NonTrivial", + "contents": { + "tag": "Query", + "contents": { + "queries": { + "unDisjunctAll": [ + { + "variableReconstruction": [ + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + }, + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "SolveTensorEquality", + "contents": [ + { + "userTensorVarName": "x", + "userTensorVarDimensions": [ + 1 + ] + }, + { + "constantValue": { + "value": [ + { + "numerator": 0, + "denominator": 1 + } + ], + "tag": "Tensor", + "shape": [ + 1 + ] + }, + "coefficients": [ + [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "numerator": 1, + "denominator": 1 + } + ] + ] + } + ] + } + ], + "queryAddress": [ + { + "propertyName": "p", + "propertyIndices": [], + "propertyID": 0 + }, + 1 + ], + "metaNetwork": { + "variables": [ + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + ], + "networkEntries": [ + { + "metaNetworkEntryName": "f", + "metaNetworkEntryInfo": { + "networkType": { + "outputTensor": { + "dimensions": [ + 2 + ], + "baseType": [] + }, + "inputTensor": { + "dimensions": [ + 1 + ], + "baseType": [] + } + }, + "networkFilepath": "fake.onnx" + } + } + ] + } + }, + { + "variableReconstruction": [ + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + }, + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "SolveTensorEquality", + "contents": [ + { + "userTensorVarName": "x", + "userTensorVarDimensions": [ + 1 + ] + }, + { + "constantValue": { + "value": [ + { + "numerator": 0, + "denominator": 1 + } + ], + "tag": "Tensor", + "shape": [ + 1 + ] + }, + "coefficients": [ + [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "numerator": 1, + "denominator": 1 + } + ] + ] + } + ] + } + ], + "queryAddress": [ + { + "propertyName": "p", + "propertyIndices": [], + "propertyID": 0 + }, + 2 + ], + "metaNetwork": { + "variables": [ + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + ], + "networkEntries": [ + { + "metaNetworkEntryName": "f", + "metaNetworkEntryInfo": { + "networkType": { + "outputTensor": { + "dimensions": [ + 2 + ], + "baseType": [] + }, + "inputTensor": { + "dimensions": [ + 1 + ], + "baseType": [] + } + }, + "networkFilepath": "fake.onnx" + } + } + ] + } + }, + { + "variableReconstruction": [ + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + }, + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "SolveTensorEquality", + "contents": [ + { + "userTensorVarName": "x", + "userTensorVarDimensions": [ + 1 + ] + }, + { + "constantValue": { + "value": [ + { + "numerator": 0, + "denominator": 1 + } + ], + "tag": "Tensor", + "shape": [ + 1 + ] + }, + "coefficients": [ + [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "numerator": 1, + "denominator": 1 + } + ] + ] + } + ] + } + ], + "queryAddress": [ + { + "propertyName": "p", + "propertyIndices": [], + "propertyID": 0 + }, + 3 + ], + "metaNetwork": { + "variables": [ + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + ], + "networkEntries": [ + { + "metaNetworkEntryName": "f", + "metaNetworkEntryInfo": { + "networkType": { + "outputTensor": { + "dimensions": [ + 2 + ], + "baseType": [] + }, + "inputTensor": { + "dimensions": [ + 1 + ], + "baseType": [] + } + }, + "networkFilepath": "fake.onnx" + } + } + ] + } + }, + { + "variableReconstruction": [ + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "ReconstructTensor", + "contents": [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + [ + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + }, + { + "tag": "NetworkRationalVar", + "contents": { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + } + ] + ] + }, + { + "tag": "SolveTensorEquality", + "contents": [ + { + "userTensorVarName": "x", + "userTensorVarDimensions": [ + 1 + ] + }, + { + "constantValue": { + "value": [ + { + "numerator": 0, + "denominator": 1 + } + ], + "tag": "Tensor", + "shape": [ + 1 + ] + }, + "coefficients": [ + [ + { + "tag": "NetworkTensorVar", + "contents": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "numerator": 1, + "denominator": 1 + } + ] + ] + } + ] + } + ], + "queryAddress": [ + { + "propertyName": "p", + "propertyIndices": [], + "propertyID": 0 + }, + 4 + ], + "metaNetwork": { + "variables": [ + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 1 + ], + "networkName": "f", + "inputOrOutput": "Input", + "application": 0 + } + }, + { + "tensorIndices": [ + 1 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + }, + { + "tensorIndices": [ + 0 + ], + "originalVar": { + "startingIndex": 0, + "networkTensorVarDimensions": [ + 2 + ], + "networkName": "f", + "inputOrOutput": "Output", + "application": 0 + } + } + ], + "networkEntries": [ + { + "metaNetworkEntryName": "f", + "metaNetworkEntryInfo": { + "networkType": { + "outputTensor": { + "dimensions": [ + 2 + ], + "baseType": [] + }, + "inputTensor": { + "dimensions": [ + 1 + ], + "baseType": [] + } + }, + "networkFilepath": "fake.onnx" + } + } + ] + } + } + ] + }, + "negated": true + } + } + } +} \ No newline at end of file diff --git a/vehicle/tests/golden/compile/simple-minmax/fake.onnx b/vehicle/tests/golden/compile/simple-minmax/fake.onnx new file mode 100644 index 000000000..94f52176a --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/fake.onnx @@ -0,0 +1 @@ +FAKE ONNX NETWORK diff --git a/vehicle/tests/golden/compile/simple-minmax/spec.vcl b/vehicle/tests/golden/compile/simple-minmax/spec.vcl new file mode 100644 index 000000000..acec7a366 --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/spec.vcl @@ -0,0 +1,6 @@ +@network +f : Vector Rat 1 -> Vector Rat 2 + +@property +p : Bool +p = forall x . 0 <= min (f x ! 0) (f x ! 1) and max (f x ! 0) (f x ! 1) <= 1 diff --git a/vehicle/tests/golden/compile/simple-minmax/test.json b/vehicle/tests/golden/compile/simple-minmax/test.json new file mode 100644 index 000000000..c7800face --- /dev/null +++ b/vehicle/tests/golden/compile/simple-minmax/test.json @@ -0,0 +1,14 @@ +[ + { + "name": "Marabou", + "run": "vehicle compile -s spec.vcl -t MarabouQueries -o Marabou.queries/ --network f:fake.onnx", + "needs": ["spec.vcl", "fake.onnx"], + "produces": [ + "Marabou.queries/*.txt", + "Marabou.queries/p.vcl-plan" + ], + "ignore": { + "lines": ".*\"fileHash\".*" + } + } +]