Tidying lax vs admit, options vs environment

[mtzguido]

Internally, there are many different toggles that imply we are not fully verifying a file.

We can be running with --lax or --admit_smt_queries true set, which are part of the option state. They are independent, so we sometimes need to check both, or at least it is unclear which one to check. Further, the typechecker environment has two fields lax and admit, which also have unclear meaning. They mostly follow the options, but not always. This PR tries to bring some order to these things.

The main changes are:

• --lax is not settable within a file, only from the CLI. This option implies that we will admit all queries and only produce .checked.lax files.
• The env.lax field is removed. When needed, we just check Options.lax(), which is constant throughout an invocation.
• The env.admit field is now populated from the optionstate before checking each top-level decl.
• We do not check Options.admit_smt_queries() during typechecking any more, only env.admit.
• We always do 2-phase typechecking, unless --lax. This has one undesirable implication: when loading a dependency that does not have a checked file, we will do 2-phase checking, which is roughly 2x slower. This does make it more consistent though, and eliminates some bugs from ever popping up:

  • 2589

  • 2611

  • 1567

  • 3286

  • And probably more

If we want to only do 1-phase checking for dependencies, I think the clean way is adding a checking_dependency field in the environment and branch on that. Previously the condition was Env.should_verify env, which is rather misleading.

Also, we have a "dummy" SMT solver used during the tests. This seems fine right now, it's only used for fstar_tests.exe and when --lax is set, but it's another point where VCs could be dropped.

This was motivated also by the Pulse checker running with lax=true during flycheck and causing spurious errors. I will post follow up patches for always running tactics without admit/lax, and for preventing these flycheck spurious errors.

[mtzguido]

Related to the discussion today, the extension does seem to be sending a LaxCheck query. Here's the output after adding this conditional failwith and restarting F* with flycheck in the extension.

[mtzguido]

Ah.. that's because it's compiler sources, running with --lax, and then we set LaxCheck unconditionally. In normal F* files it only happens with Ctrl+Shift+dot. Nevermind.