search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

#push-options accepts --using_facts_from but shouldn't since it doesn't reset the solver #1614

Closed msprotz closed 5 years ago

msprotz commented 5 years ago

Thanks,

Jonathan

mtzguido commented 5 years ago

Sorry for the delay. I'm tempted to just make #push-options and #pop-options reset the solver too.

Perhaps #set-options too? As things are now, the "reset" in #reset-options has two meanings: 1) reset the options to their original values, 2) restart the SMT solver. We could always reset the solver, but maybe that has a non-negligible performance cost, I'm trying it out to see now.

mtzguido commented 5 years ago

Tried that change (everything resets the solver) out in guido_1614, and CI seemed to land in about the same ballpark.

@nikswamy @aseemr, how do you guys feel about it? I expect it should bring about less headaches, but I might be missing something.

mtzguido commented 5 years ago

We discussed this a bit today, without a very clear consensus. A tricky bit is if resetting options is allowed within a #push or not.

Here are a few alternatives:

1) #push-options only takes "settable" options, so nothing that requires to reset the solver. We do not allow #reset-options when inside a #push.

2) Similar to (1), but #reset-options will pop the entire option stack into a singleton.

3) Similar to (1), but we keep track of resets. Then, if we #push, #reset, and #pop, the pop must reset the solver al well to return to the previous state.

4) Always reset the solver, for #push, #pop, #reset and #set.

5) Detect when, for any kind of option-setting pragma, some "solver-sensitive" option changed and reset only in that case.

My personal opinion is that (1) through (3) are confusing for users, and it's unclear whether reset means "return to the default values" or "reset the solver" (it's currently both). I see (4) much more pleasant for users, who then need not care about it. Nevertheless, resetting too much might be slow, so (5) could improve on that area.

A downside I see with (5) is that users might inadvertedly reset the solver, but I don't think it's serious.

mtzguido commented 5 years ago

I'll start implementing option 5 and report back. I'll also document the behaviour so we can discuss it between all of us before merging it.

We might also consider adding a #restart-solver for power users.

mtzguido commented 5 years ago

Btw, here's a list of the 30 files with the most option setting pragmas in Everest:

     20 hacl-star/code/poly1305_32/Hacl.Spe.Poly1305_32.fst
     20 hacl-star/code/poly1305/Hacl.Spe.Poly1305_64.fst
     20 mitls-fstar/src/tls/HandshakeMessages.fst
     21 hacl-star/code/salsa-family/Spec.Chacha20_vec1.Lemmas.fst
     22 FStar/examples/low-level/crypto/Crypto.Symmetric.Poly1305.fst
     22 FStar/ulib/FStar.ModifiesGen.fst
     22 hacl-star/code/ed25519/Hacl.Impl.Ed25519.Sign.Steps.fst
     22 hacl-star/code/poly1305_32/Hacl.Spec.Poly1305_32.fst
     22 hacl-star/snapshots/ecc-star/bignum_proof/modulo_p25519_64.fst
     23 FStar/examples/low-level/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst
     23 FStar/ulib/FStar.Buffer.fst
     23 FStar/ulib/FStar.Math.Lemmas.fst
     24 hacl-star/code/bignum/Hacl.Spec.Bignum.Fproduct.fst
     25 hacl-star/code/experimental/hmac/Hacl.HMAC.SHA2_256.Incremental.fst
     25 hacl-star/code/hash/Hacl.Impl.SHA2_256.Lemmas.fst
     26 hacl-star/code/hash/Hacl.Impl.SHA2_384.Lemmas.fst
     26 hacl-star/code/poly1305/Hacl.Spec.Poly1305_64.fst
     27 hacl-star/code/hash/Hacl.Impl.SHA2_512.Lemmas.fst
     27 hacl-star/code/poly1305/Hacl.Spec.Bignum.AddAndMultiply.fst
     29 FStar/examples/doublylinkedlist/DoublyLinkedList.fst
     31 hacl-star/code/curve25519/Hacl.Spec.Bignum.Fsquare.fst
     32 FStar/ulib/FStar.UInt128.fst
     32 hacl-star/code/curve25519/Hacl.Spec.EC.AddAndDouble.fst
     33 hacl-star/code/poly1305_32/Hacl.Spec.Bignum.AddAndMultiply.fst
     35 mitls-fstar/src/tls/Extensions.fst
     36 FStar/examples/low-level/crypto/Crypto.Symmetric.Poly1305.Lemmas.fst
     43 hacl-star/code/salsa-family/Hacl.Impl.Chacha20.Vec128.fst
     44 hacl-star/code/hash/Hacl.Impl.SHA2_256.fst
     48 hacl-star/code/hash/Hacl.Impl.SHA2_384.fst
     48 hacl-star/code/hash/Hacl.Impl.SHA2_512.fst

Obtained with: grep -rn '#\(set\|reset\|push|\pop\)-options' | cut -d: -f1 | sort | uniq -c | sort -n | tail -n 30

msprotz commented 5 years ago

Can you run this on the freshest fstar-master branch of HACL*? This should allow you to filter out the old code with grep -v '/old/'

mtzguido commented 5 years ago

Here it is:

      7 secure_api/aead/Crypto.AEAD.MAC_Wrapper.Invariant.fst
      7 vale/code/arch/x64/interop/Interop_Printer.fst
      7 vale/code/arch/x64/interop/Sha_update_bytes_stdcall.fst
      7 vale/code/crypto/aes/GCTR.fst
      7 vale/code/crypto/aes/x64/X64.GCMdecrypt.vaf
      7 vale/code/crypto/aes/x64/X64.GCMencrypt.vaf
      7 vale/code/crypto/poly1305/x64/X64.Poly1305.Math.fst
      8 vale/code/arch/x64/X64.Leakage.fst
      8 vale/code/arch/x64/X64.Leakage_Ins.fst
      8 vale/code/lib/math/Math.Lemmas.Int.fst
      8 vale/code/thirdPartyPorts/rfc7748/curve25519/x64/X64.FastSqr.vaf
      8 vale/obj/code/arch/Arch.Types.fst.dump
      8 vale/obj/external/Spec.Lib.fst
      9 apps/experimental/pneutube/Hacl.Tube.Send.fst
     10 secure_api/merkle_tree/MerkleTree.New.High.Correct.Path.fst
     10 secure_api/uf1cma/Crypto.Symmetric.MAC.fst
     10 vale/code/arch/x64/X64.Memory.fst
     10 vale/code/thirdPartyPorts/rfc7748/curve25519/x64/X64.FastUtil.vaf
     11 secure_api/aead/Crypto.AEAD.EnxorDexor.fst
     11 secure_api/merkle_tree/MerkleTree.New.High.Correct.Rhs.fst
     11 secure_api/utils/Crypto.Symmetric.Bytes.fst
     11 vale/obj/external/FStar.Endianness.fst
     12 secure_api/uf1cma/Crypto.Symmetric.UF1CMA.fst
     13 apps/experimental/pneutube/Hacl.Tube.fst
     14 secure_api/aead/Crypto.AEAD.Invariant.fst
     15 secure_api/aead/Crypto.AEAD.Wrappers.CMA.fst
     15 vale/code/thirdPartyPorts/rfc7748/curve25519/x64/X64.FastHybrid.vaf
     16 secure_api/aead/Crypto.AEAD.Encoding.fst
     17 secure_api/hkdf/Crypto.HMAC.fst
     38 secure_api/merkle_tree/MerkleTree.New.Low.fst
mtzguido commented 5 years ago

Option (4) is implemented in guido_1614. It should not be hard to do (5), I'll get on it soon. This also uncovered some weird bugs with --using_facts_from. See commits 34ebaf14856574ed9451914905611db58709a7c9, 0cbf3355f9d535c43a26069e293a7b808ef1552a and ab826a6e9a976eca4494b41afea4d59c050733d9.