search

hacl-star / merkle-tree

A verified Merkle Tree, built as a standalone project on top of EverCrypt
6 stars 5 forks source link

Bumping another rlimit #19

Closed mtzguido closed 7 months ago

mtzguido commented 7 months ago

Everest upgrade failed on CI machine... but it works locally for me. Trying an rlimit bump on the failed file to see if it fixes it.

gebner commented 7 months ago

FWIW I'm seeing similar timeouts locally, not on that file but on others:

* Error 19 at /home/gebner/fstar_dataset/projects/merkle-tree/src/MerkleTree.New.High.Correct.Base.fst(387,2-390,64):
  - Could not prove post-condition
  - Try with --query_stats to get more details
  - See also /home/gebner/fstar_dataset/projects/merkle-tree/src/MerkleTree.New.High.Correct.Base.fst(381,18-381,75)

Verified module: MerkleTree.New.High.Correct.Base
1 error was reported (see above)

* Error 19 at /home/gebner/fstar_dataset/projects/merkle-tree/src/MerkleTree.Low.fst(1828,12-1828,14):
  - Assertion failed
  - Try with --query_stats to get more details
  - See also LowStar.BufferOps.fst(44,22-44,32)

Verified module: MerkleTree.Low
1 error was reported (see above)

The absolutely weird thing is that they check just fine the second time. @mtzguido Do you have any idea what could be going on here?

mtzguido commented 7 months ago

Ouch.. somehow this file is weird behaving differently on different systems. I wonder if we're hitting some weird z3 non-deterministic corner.

As for the it working the second time, that is probably since the Makefile here sets --record_hints. So, on a first unsuccesful run, you may still modify the hints file. The next time around, z3 will be in a slightly different state (maybe a proof now works via hints), and you may avoid a timeout.

Could you capture the smt2 file for the failing run with --log_queries? Maybe it can point us to a discrepancy.

gebner commented 7 months ago

Okay, I've run F* with log_queries. The results are somewhat surprising:

I'm sending you the output via email.