Skip to content
Snippets Groups Projects
nier_to_onnx.t 712 B
Newer Older
Test verify
  $ . ./setup_env.sh

  $ bin/pyrat.py --version
  PyRAT 1.1

  $ caisar verify --format whyml --prover=PyRAT --ltag=NIER --onnx-out-dir="out" - 2>&1 <<EOF
  > theory NIER_to_ONNX
  >   use ieee_float.Float64
  >   use model.Model
  >   use model.NN
  >   constant nn: model nn = read_model "TestNetworkONNX.onnx"
  > 
  >   goal G:
  >     forall i: vector t.
  >       has_length i 3 ->
  >       (0.5:t) .<= i[0] .<= (0.5:t) ->
  >       (0.5:t) .< (nn @@ i)[0] .< (0.5:t)
  [DEBUG]{NIER} Wrote NIER as ONNX in file 'out/onnx_nn.nier.onnx'
  Initializer name 12 has data 0.135