GraphAtlas evidence bundle

This is a copy of the evidence that the site shows for its proofs. The hashes and the proofs can be checked with tools that
you already have, and with no GraphAtlas code.

What is here

  proofs/       The 38 SMT-LIB files that the solvers decided. The first lines of each one say which statement it
                proves, which code it is about, and which source the rule comes from.
  results/      Records of our runs. Only crosscheck.json can be repeated with what is in this bundle.
                  proofs.json      Z3 as WebAssembly, and each statement broken on purpose and refuted.
                  crosscheck.json  A native Z3 and cvc5, run on the files in proofs/ unchanged, one answer per check.
                  parity.json      The calculation kernel on five JavaScript engines, with the digest of each fixture.
  SHA256SUMS    The SHA-256 of every other file.
  verify.sh     Checks the hashes, and decides the proofs again when z3 or cvc5 is installed.

How to check it

  sh verify.sh

or one file at a time

  z3 proofs/SM-01.smt2
  cvc5 --nl-cov proofs/SM-01.smt2

Every line of the answer has to be unsat. Each check assumes that the statement is false, and unsat means that no numbers
can make that so. cvc5 needs the option --nl-cov, which decides non-linear real arithmetic by covering it.

What it shows

  That each statement holds for every input its file allows, as decided by a solver that is not ours and that you can run.

What it does not show

  The proofs are about real numbers, and computers round. The kernel is tested against the proved rules on generated
  inputs, and that is a test and not a proof. A proof shows that the code does what its statement says. It does not show
  that the statement reads the regulation correctly. This bundle comes from a preview build, and the regulatory
  parameters in it are for demonstration.
