Update submodules.

[brianhuffman]

No description provided.

[brianhuffman]

Just waiting on CI now. For some reason the blst tests have been timing out, although from the logs it appears that they are progressing normally up until the point they are canceled by the CI system.

[brianhuffman]

Here's the relevant bit of the CI log at the point where the blst proof times out:

2021-03-03T14:56:48.7248690Z [14:56:48.724] Assume override blst_sha256_bcopy
2021-03-03T14:56:48.7637331Z [14:56:48.763] Assume override blst_sha256_bcopy
2021-03-03T14:56:48.8008692Z [14:56:48.800] Assume override blst_sha256_emit
2021-03-03T14:56:48.8111415Z [14:56:48.810] Assume override blst_sha256_hcopy
2021-03-03T14:56:48.8142797Z [14:56:48.813] Loading file "/workdir/proof/types.saw"
2021-03-03T15:34:30.4472963Z ##[error]The operation was canceled.
2021-03-03T15:34:30.4574461Z Post job cleanup.
2021-03-03T15:34:30.9909543Z There is no image to save.

You can see that the last thing the script does is to assume some overrides for blst_sha256 functions, then load types.saw. Then it produces no further output until the process is killed some 38 minutes later.

At this point in the blst proof, it is running keygen.saw. The next saw-script command that produces output should be a call to crucible_llvm_unsafe_assume_spec, which should print "Assume override mulx_mont_sparse_256". The only things in between this and the include "types.saw" line are let declarations and import statements (which import cryptol modules).

The only explanation I can imagine for why the proof script would hang at this point is that z3 is getting stuck on one of the goals that arises from typechecking the cryptol modules.

[chameco]

I've encountered a similar problem in the past when using z3 4.8.9 (GaloisInc/cryptol#965), but the CI appears to be using 4.8.8.

[brianhuffman]

I've narrowed it down a bit. The proof-script seems to hang at the point when it gets to the second import statement. There is probably something to do with how I've adapted saw-core to deal with the cryptol persist-solver patch, which is also affected by the z3 version. I guess I'll be spending today trying to figure this out.

[weaversa]

Seeing as you're using SHA, the answer may be here: GaloisInc/cryptol#559

[brianhuffman]

Here's how to reproduce the bug locally without involving blst:

• Compile saw-script in this branch (commit bd7edfd or e58f096)
• Make sure the z3 in your path is version 4.8.8
• Go to the top-level directory of the cryptol-specs repo
• Run saw and enter the following two commands at the REPL:

sawscript> import "Primitive/Keyless/Hash/SHA256.cry"
sawscript> import "Primitive/Symmetric/KDF/HKDF256.cry"

SAW will hang after the second import command, with z3 using lots of CPU.

Running the second import command by itself works just fine (the second module imports the first). Running the two commands in the other order also works. Running the two commands with z3-4.8.10 also works. Importing those two modules in that order in the cryptol repl works as well.

[brianhuffman]

This is a bug in z3-4.8.8. If you give the contents of CryptolTC.z3 plus the following SMT script to z3-4.8.8, it will get stuck at the 4th check-sat command. If you use an earlier or later z3 version, or if you rename the declared variables to avoid reusing names, then the proof will complete normally.

(push 1 )
  (declare-fun kv0 () InfNat )
  (assert (cryVar kv0 ) )
  (declare-fun kv1 () InfNat )
  (assert (cryVar kv1 ) )
  (declare-fun kv2 () InfNat )
  (assert (cryVar kv2 ) )
  (assert (cryAssume (cryFin kv0 ) ) )
  (assert (cryAssume (cryFin kv1 ) ) )
  (assert (cryAssume (cryFin kv2 ) ) )
  (push 1 )
    (assert (cryProve (cryGeq (cryMax (cryWidth kv0 ) (cryWidth kv1 ) ) (cryWidth kv1 ) ) ) )
    (check-sat )
  (pop 1 )
  (push 1 )
    (assert (cryProve (cryGeq (cryMax (cryWidth kv0 ) (cryWidth kv1 ) ) (cryWidth kv0 ) ) ) )
    (check-sat )
  (pop 1 )
(pop 1 )
(push 1 )
  (declare-fun kv0 () InfNat )
  (assert (cryVar kv0 ) )
  (declare-fun kv1 () InfNat )
  (assert (cryVar kv1 ) )
  (declare-fun kv2 () InfNat )
  (assert (cryVar kv2 ) )
  (declare-fun kv3 () InfNat )
  (assert (cryVar kv3 ) )
  (assert (cryAssume (cryFin kv3 ) ) )
  (assert (cryAssume (cryFin kv0 ) ) )
  (assert (cryAssume (cryFin kv1 ) ) )
  (assert (cryAssume (cryFin kv2 ) ) )
  (assert (cryAssume (cryGeq kv0 kv3 ) ) )
  (assert (cryAssume (cryGeq (cryMul (cryNat 255 ) kv3 ) kv2 ) ) )
  (assert (cryAssume (cryGeq kv2 (cryAdd (cryNat 1 ) kv3 ) ) ) )
  (assert (cryAssume (cryFin kv0 ) ) )
  (assert (cryAssume (cryFin kv1 ) ) )
  (assert (cryAssume (cryFin kv3 ) ) )
  (assert (cryAssume (cryGeq (cryNat 32 ) (cryWidth (cryAdd (cryNat 1 ) (cryAdd kv1 kv3 ) ) ) ) ) )
  (assert (cryAssume (cryGeq (cryNat 64 ) (cryWidth (cryMul (cryNat 8 ) kv0 ) ) ) ) )
  (assert (cryAssume (cryGeq (cryNat 64 ) (cryWidth (cryAdd (cryNat 513 ) (cryAdd kv1 kv3 ) ) ) ) ) )
  (push 1 )
    (assert (cryProve (cryGeq (cryCeilDiv kv2 kv3 ) (cryNat 2 ) ) ) )
    (check-sat )
  (pop 1 )
  (push 1 )
    (assert (cryProve (cryGeq (cryMul (cryCeilDiv kv2 kv3 ) kv3 ) kv2 ) ) )
    (check-sat )
  (pop 1 )
(pop 1 )
(exit )

[brianhuffman]

Finding a version of z3 that works for the blst proofs is turning out to be rather difficult. Version 4.8.8 has the bug I described above, and causes the keygen.saw proof script to hang while importing a cryptol module. Version 4.8.9 has a separate bug (probably the same as GaloisInc/cryptol#965) that causes memory_safety.saw to hang while importing a different cryptol module. And version 4.8.10 has yet another regression that causes one of the proof commands in functional_proofs.saw to take forever.