Start a Tactics V2

[mtzguido]

This PR introduces a new version of the tactics engine, with differences to (mostly) the representation of terms. The change is heavily disruptive to pretty much everything, so we are staging it by maintaining a .V1 namespace of Tactics and Reflection, which retains exactly the previous behaviour, and a V2 with new changes. V2, for now, has to be explicitly asked for by open FStar.Tactics.V2 or any submodule thereof.

The two versions can interoperate, the underlying effect is the same, but the relevant view types and primitives can be different. Some files are totally agnostic to the version, such as FStar.Tactics.SMT and FStar.Tactics.Visit (which is now implemented with V2, but just exposes visit_tm : (term -> Tac term) -> term -> Tac term),

V2 is very explicit about opening/closing names, freshness, etc. This is now all implemented in userspace (FStar.Tactics.NamedView), and marked as a plugin so it runs fast.

Another significant change is the autogeneration of embeddings for most inductive types, so many more functions can be easily made into plugins. Also typeclasses are moved higher up in the dependency chain and even used within tactic libraries (FStar.Tactics.MApply.fst).

For now, I think V2 should be considered experimental and subject to change, but I would like to get this into the repo as it's a big change that could diverge.

Karamel needs a tiny patch to ignore a new module, FStar.Syntax.Syntax, in ulib/ (which is an interface for the compiler's FStar.Syntax.Syntax). We may move all of the F* compiler sources into the FStar.Compiler namespace to make this easier to maintain, but not on this PR.

I have a steel branch that works with V2.
For hacl-star I haven't yet ported to V2, but confirmed that it works as before with V1.
Will post an everest green later.

[mtzguido]

Everest run will be here https://github.com/mtzguido/everest/actions/runs/5238573630

[mtzguido]

Some things to think about:

• I think typeclass resolution can be abstracted behind an interface if it's always used as a plugin. This would reduce the dependencies imposed into clients, which can be pretty huge. See this:
  depgraph-FStar.Tactics.Typeclasses.fst.pdf
• For plugins, it may be useful to have a check that will ignore the compiled plugin if the underlying term changed (we could check the hash, transitively across dependencies). It can reduce shots in the foot, but should also be optional using the old one can be useful (e.g. bootstrapping a tiny change to typeclasses).
• Automatically loading a plugin right after typechecking it should not be super hard.

[mtzguido]

This PR also introduces an FStar.Tactics.SMT module with tactics to tweak the SMT context of individual assertions, like so:

      assert (loc_disjoint (loc_union l (loc_addresses true r0 (Set.singleton a0))) (loc_of_aloc b))
          by (let open FStar.Tactics.V2.Builtins in
              let open FStar.Tactics.SMT in
              set_rlimit 64;
              set_options "--z3cliopt 'smt.qi.eager_threshold=5'";
              ())

there are also getters/setters for fuel/ifuel.