Newer
Older
$ bin/pyrat.py --version
PyRAT 1.1
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX
> use ieee_float.Float64
> use bool.Bool
> use int.Int
> use vector.Vector
> use nn.NeuralNetwork
> constant nn: nn = read_model "TestNetworkONNX.onnx" ONNX
>
> goal G:
> forall i: vector t.
> has_length i 3 ->
> (0.0:t) .<= i[0] .<= (0.5:t) ->
> (0.0:t) .< (nn@@i)[0] .< (0.5:t)
> end
> EOF
[DEBUG]{ProverSpec} Prover-tailored specification:
0.0 < y0 and y0 < 0.5
Goal G: Unknown ()