README.md

xmss-jasmin

• XMSSMT-SHA2_20/2_256

[partial_prover]
name = "Alt-Ergo"
path = "/home/rui/.opam/default/bin/alt-ergo"
version = "2.5.4"

[partial_prover]
name = "CVC4"
path = "/usr/local/bin/cvc4"
version = "1.8"

[partial_prover]
name = "Z3"
path = "/home/rui/.opam/default/bin/z3"
version = "4.13.0"

Proofs

make -C proof/ check_spec

make -C proof/ check_xmss_xmssmt_proof

make -C proof/ check_correctness_proof 

# weak check mode: smt calls are assumed to succeed
make -C proof/ check_correctness_proof ECADDFLAGS="-pragmas Proofs:weak"