Subtyping and unification in the tactics engine requires re-checking solutions (Was: The unification in tactics is unsound)

[857b]

On can prove ⊥ using the unification of uvars in tactics (F* https://github.com/FStarLang/FStar/commit/a46a208c59b502b427e300e7a9e7b7cf9fb58ad7):

module Main
open FStar.Tactics

#set-options "--ifuel 0 --fuel 0"

let prove_False
      (pf : squash False)
      (_  : (pf0 : squash False) -> squash (eq2 #(squash False) pf ()))
  : squash False
  = pf

let absurd : squash False
  = _ by (// |- ?pf : squash l_False
          apply (`prove_False);
          let pf0 = intro () in
          // (pf0 : squash l_False) |- _ : ?pf == ()
          trefl ())

This proof seems to rely on the following points:

• When building terms by unification, F* does not retype them. Here, after unifying ?pf to (), there is no check ⊢ () : squash False. This is (I believe) intentional, it avoids generating unnecessary guards that have already been checked (or that are no longer provable if their proofs have been erased by normalization).
• When unifying an uvar, one must check that the assigned term does not depend on any binder that was not present in the context of the uvar. Here ?pf is introduced at top-level so it cannot depend on pf0. However F* seems to apply only a syntactic check, which is not sound since there can be implicit dependencies in the typing judgment. Here pf0 is used in (pf0 : squash False) ⊢ () : squash False, even if does not appear explicitly in (). Note that the unification fails if one replaces eq2 #(squash False) pf () with eq2 #(squash False) pf pf0 in prove_False (since this introduces an explicit dependency).

[857b]

The second check of https://github.com/FStarLang/FStar/pull/2639 is currently not strong enough. Firstly, one should check not only the types with refinements but also the datatypes without inhabitants:

module S1
open FStar.Tactics

#set-options "--ifuel 0 --fuel 0"

let prove_False
      (e : empty)
      // The [() : squash False] of [false_elim] depends on [e]
      (_ : squash (e == false_elim ()))
  : squash False
  = ()

let absurd : squash False
  = _ by (
    apply (`prove_False);
    dump ""; // |- _ : squash (?e == false_elim ())
    // e does not appear as a bound variable ?
    trefl ())

In fact even skipping the check for inhabited types allows one to build ill-typed terms at top-level, which can lead to a contradiction.

module S2
open FStar.Tactics

#set-options "--ifuel 0 --fuel 0"

let int_false_elim
      (i : int)
      (_ : squash False -> squash (i == false_elim ()))
  : int
  = i

let int0 : int
  = _ by (
    apply (`int_false_elim);
    let _ = intro () in trefl ())


type display_term (#a : Type) (x : a) = unit

let _ : display_term int0
  = _ by (norm [delta_only [`%int0; `%int_false_elim]];
          dump "int0"; // false_elim ()
          exact (`()))


let absurd_omega2 (_ : squash False) : bool
  =
    let omega (b : bool) : bool
      = not ((coerce_eq #bool #(bool -> bool) () b) b)
    in
    omega (coerce_eq #(bool -> bool) #bool () omega)

let build_omega2
      (w : bool)
      (_ : squash False -> squash (w == absurd_omega2 ()))
  = w

let omega2 : bool
  = _ by (
    apply (`build_omega2);
    let _ = intro () in trefl ())

let omega2_red () : Lemma (omega2 == not omega2)
  = ()

let absurd : squash False
  = omega2_red ()

Both examples are accepted by https://github.com/FStarLang/FStar/pull/2639/commits/9cf417ad7bdd870278664efd018a99e1fe335da6. Also, I noticed in the first example that the first argument e of prove_False does not appear as a bound variable in the dump of the goal for the second argument although it is necessary to type false_elim (). EDIT: this is expected since the formal argument e is replaced by the given argument (the uvar ?e at this point). But this makes me realize that the issue here is slightly different from the original one. Here the instantiation for ?e (false_elim ()) implicitly depends on ?e itself.

[nikswamy]

Thanks for all the work on this @857b! This is really appreciated. As you can see, @aseemr and I have been trying to find an acceptable fix. For some context, the issue is that the tactic engine is designed to not re-typecheck the terms it computes. However, as you are pointing out, this is unsound when combining unification and subtyping. So, we're trying to add checks in again, but trying to also find a balance where we don't needless check everything repeatedly.

With @aseemr's latest patches, I'm hopeful we'll at least be able to address and close this class of bug with more stringent but still selective checks.

However, your issues may also be pointing out that it may be time to re-think some of the design choices in the tactic engine to more systematically prevent this kind of bug by construction, while also not letting performance degrade too much.

[nikswamy]

We have merged PR #2639, with comments there stating that although our current patches are designed to prevent this kind of exploit, we are still working on a more definitive fix. So, although I have removed the unsoundness label, since the examples here no longer yield a proof of false, I am keeping the issue open until we have completed our better fix.

[aseemr]

Closing this issue (see #2747).