The type of `/\` and related connectives does not reflect their left-to-right bias (Was: The typechecking of `l_and` as a lazy operator is unsound)

[857b]

In F*, the type-checking of l_and (⋀) reflects its laziness. That is in p ⋀ q, the type-checking of q can assume that p holds. Hence it is possible to write:

let hd_ge0 (l : list int) : prop = length l > 0 /\ index l 0 >= 0

However this is not reflected by the signature of l_and (in prims.fs):

type l_and (p: logical) (q: logical) : logical = squash (pair p q)

q is declared as a total logical but it should be Pure logical (requires p) (ensures fun _ -> True) (or squash p -> logical).

One can extract a proof of ⊥ from this:

module Main
open FStar.Tactics


type prop_with_pre (p : Type0) (pf : squash p) : Type0
  = | PropWithPre

let lazy_and : Type0
  = False /\ prop_with_pre False ()


type this_type (t : Type) = | ThisType

let and_right (p0 p1 : Type0) (_ : this_type (p0 /\ p1)) : Type0
  = p1

let pwp_False : Type0
  = _ by (apply (`and_right);
          // [this_type (?p0 /\ ?p1)]
          exact (`(ThisType #lazy_and)))


// Just an utility function
type display_term (#a : Type) (x : a) = unit

let _ : display_term pwp_False
  = _ by (norm [delta_only [`%pwp_False; `%and_right]];
          dump "pwp_False"; // prop_with_pre l_False ()
          exact (`()))


let extract_pre (p : Type0) (pf : squash p) (_ : this_type (prop_with_pre p pf))
  : squash p
  = pf

let absurd : squash False
  = _ by (apply (`extract_pre);
          // [this_type (prop_with_pre l_False ?pf)]
          exact (`(ThisType #pwp_False)))

It may seem similar to https://github.com/FStarLang/FStar/issues/2635 but I think there is an independent problem here since lazy_and already 'contains' a judgement ⊢ prop_with_pre False () : logical hence ⊢ () : squash False. The remaining part is only here to extract this term (I'm not aware of any way to do it without tactics however).

Given their signatures the same issue probably also affects l_or and l_imp.

As a side remark, I also noticed that functions operating on logical formulas often do not take this lazyness into account. For instance q does not assumes p in move_requires, so I was expecting the following to fail:

let test (l : list int) (h : unit -> Lemma (requires length l > 0) (ensures index l 0 >= 0))
  : unit
  = FStar.Classical.move_requires #unit h ()

~~But it turns out that it is also accepted.~~ It is indeed rejected (I had tested it after having derived ⊥).

[nikswamy]

The fixes in PR #2639 prevent the final exploit in these examples that allow extracting a proof of False. As such, I'm removing the unsoundness label. However, I agree that being able to construct terms such as prop_with_pre l_False () is very slippery, and we are working on a patch that revises the way these left-biased connectives are checked, reflecting the hypothesis of the LHS in the typing of the RHS, i.e., /\ will have a type similar to p:Type -> (_:squash p -> Type) -> Type.