F* cannot invert a pair under some specific conditions?

In order to have better hygiene in my proofs, I tried to make a few of my functions opaque to SMT, in order to force F* to use their lemmas with SMT patterns. When doing so, some proofs did break, and I had to add let (_, _) = ... in in my proof (which looks useless), or augment the ifuel (a bit annoying because it can make proofs more slow, when I'm trying to stabilize them).

I minimized my problem below, it seems to happen in some very specific cases, however it happened naturally in my code in several places. The problem is that the lemma g_lemma doesn't verify, however a few lines are commented with //, if we un-comment them then the lemma g_lemma passes. It is not a weirdness of opaque_to_smt, the problem also arises if we assume f and f_lemma.

#set-options "--fuel 1 --ifuel 1"

assume val state: Type0

(* monad of stateful functions that can fail *)
type m a = state -> (option a & state)

(* bind *)
val (let*): #a:Type -> #b:Type -> x:m a -> f:(a -> m b) -> m b
let (let*) #a #b x f st =
  let (opt_x', st) = x st in
  match opt_x' with
  | None -> (None, st)
  | Some x' -> (
    let (y, st) = f x' st in
    (y, st)
  )

val return: #a:Type -> a -> m a
let return #a x st = (Some x, st)

(* remove the opaque_to_smt and it works *)
[@@ "opaque_to_smt"]
val f: m unit
let f = return ()

val f_lemma:
  st:state ->
  Lemma
  (ensures (
    let (out, st_out) = f st in
    (* note that any information on `out` is useless for `g_lemma` *)
    //out == Some () /\
    st == st_out
  ))
let f_lemma st =
  reveal_opaque (`%f) f

val g: m unit
let g =
  let* x = f in
  (* `g_lemma` works if we replace `x` (of type `unit`) with `()` *)
  match x with
  | () -> return x
  (* note that this wildcard pattern is unreachable *)
  //| _ -> return x

(* it is not clear why an ifuel of 2 would be useful *)
//#push-options "--ifuel 2"
val g_lemma:
  st:state ->
  Lemma
  (ensures (
    let (_, st_out) = g st in
    st == st_out
  ))
let g_lemma st =
  f_lemma st;
  (* this `let` is not used. It doesn't work if we replace `(_, _)` by `_` *)
  //let (_, _) = f st in
  ()

Here is another minimized example that I stumbled upon, which uses a simple monad (state monad that doesn't fail)

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

assume val state: Type0
assume val invariant: state -> prop

// A simple state monad
type m a = state -> (a & state)

val (let*): #a:Type -> #b:Type -> x:m a -> f:(a -> m b) -> m b
let (let*) #a #b x f st =
  let (x', st) = x st in
  let (y, st) = f x' st in
  (y, st)

val return: #a:Type -> a -> m a
let return #a x st =
  (x, st)

// A monadic function that returns an nat
assume val f: m nat

// This lemma proves that it doesn't modify the state
assume val f_lemma:
  st:state ->
  Lemma
  (ensures (
    let (_, st_out) = f st in
    st == st_out
  ))
  [SMTPat (f st)]

// Another monadic function
assume val g: nat -> m unit

// This lemma proves that it preserves the state invariant
assume val g_lemma:
  i:nat -> st:state ->
  Lemma
  (requires invariant st)
  (ensures (
    let ((), st_out) = g i st in
    invariant st_out
  ))
  [SMTPat (g i st)]

// This function combines the two functions above
val h: m unit
let h =
  let* i = f in
  g i

// This lemma verifies with an ifuel of 1, although there doesn't seem to be a reason for it
// #push-options "--ifuel 1"
val h_lemma:
  st:state ->
  Lemma
  (requires
    invariant st
  )
  (ensures (
    let (_, st_out) = h st in
    invariant st_out
  ))
let h_lemma st =
  // Without the commented line below, this lemma won't verify.
  // To prove that it isn't a problem of instantiating the SMT pattern,
  // we instantiate the lemma explicitly and it still doesn't work
  f_lemma st;
  // let (_, _) = f st in
  ()

Hi @TWal, it has to do with how the match in g is written:

match x with
| () -> return ()

Solver needs to reduce this match to be able to prove g_lemma. To reduce this match, the solver needs to prove that x = (), where x = Some? (Mktuple2?._1 (f st)). If the solver can derive x:unit, then it can derive x = () (there is such an axiom in the encoding) and proceed with reducing the match (if f is not opaque, then the solver can also derive this from the definition of f). To derive x:unit, solver needs to invert the typing of f st : option unit & st. But this needs two inversions, one for & and one for option, and hence the ifuel of 2.

I think this explains various variations. E.g.,

If we add the postcondition out == Some (), then the proof works, the solver can derive x = () from this.
If we make the match in g as match x with | _ -> return (), then the proof works, since the solver doesn't have to prove x = (), it is a wildcard pattern.
When we add let (_, _) = f st, then it adds an equality Mktuple2 x st1 = f st in the context, from which the solver can derive Mktuple2 x st1 : option unit & st. The typing elimination for Mktuple2 gives x : option unit without consuming any ifuel, and so this works with ifuel 1.

Interesting, thank you for the detailed answer! It definitely clashes with my internal model of F* hence I have a few follow-up questions.

About ifuel and pairs: in my mind, pairs (or records) didn't usually need ifuel, such as in this example:

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

type t2 = int & int

val f2: t2 -> t2
let f2 x =
  match x with
  | (x1, x2) -> (x2, x1)

// We can prove things on pairs with an ifuel of 0 (instead of 1)
val f2_lemma:
  x:t2 -> Lemma (f2 (f2 x) == x)
let f2_lemma x = ()

And if we nest pairs, we need one less ifuel than the nesting depth, giving the intuition that "the first pair is free"

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

type t3 = int & (int & int)

val f3: t3 -> t3
let f3 x =
  match x with
  | (x1, (x2, x3)) -> (x2, (x3, x1))

// We can prove things on pairs with an ifuel of 1 (instead of 2)
val f3_lemma:
  x:t3 -> Lemma (f3 ( f3 (f3 x)) == x)
let f3_lemma x = ()

But indeed this example needs an ifuel of 2 and it clashes a bit with the intuition above that "the first pair is free":

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

type t1 = option int & int

val f1: t1 -> t1
let f1 x =
  match x with
  | (Some x1, x2) -> (Some x2, x1)
  | (None, x2) -> (None, x2)

val f1_lemma:
  x:t1 -> Lemma (f1 (f1 x) == x)
let f1_lemma x = ()

What is happening?

I tried to add some allow_inversion in the proof of g_lemma in the first example, and see what happens on the ifuel:

allow_inversion (option unit); brings the ifuel down to 1 (sounds okay, although conflicting with the intuition that "inverting the first pair is free"
allow_inversion (option unit & state); only works with an ifuel of 2, hence seems to be useless
using both allow_inversion (option unit); and allow_inversion (option unit & state); bring the ifuel down to 0

It is a bit weird, because allowing inversion on the pair option unit & state doesn't do anything unless we also allow inversion on option unit? I am testing this because I am tempted to add an SMTPat on m a to allow inversion on option a & state, which seems safe while allowing me to keep ifuels low (this strategy works well on the second example).

Something interesting is that allow_inversion (option unit); do something useful, but invertOption unit; doesn't help at all here.

And finally, I am surprised that the solver has trouble proving that x has type unit. The types #a and #b of (let*) are resolved to a = unit and b = unit, which directly implies that x has type unit?

Thanks!

hi @TWal

Thanks for these examples; they are interesting and revealing.

Explaining the current behavior

Your intuition about the "first pair is free" is not something in my mental model. But, it is indeed how things behave, at least to a certain extent. Here's what's going on

Tuples in the SMT encoding are set up to enable inversion without any ifuel. However, the typing of the sub-terms that result from such an inversion do require ifuel. Here's an excerpt of the encoding of tuple2:

;;;;;;;;;;;;;;;;inversion axiom
;;; Fact-ids: Name FStar.Pervasives.Native.tuple2; Namespace FStar.Pervasives.Native; Name FStar.Pervasives.Native.Mktuple2; Namespace FStar.Pervasives.Native
(assert (! 
         ;; def=c:\cygwin64\home\nswamy\workspace\everest\FStar\bin\..\ulib\FStar.Pervasives.Native.fst(59,5-59,11); use=c:\cygwin64\home\nswamy\workspace\everest\FStar\bin\..\ulib\FStar.Pervasives.Native.fst(59,5-59,11)
         (forall ((@u0 Fuel) (@x1 Term) (@x2 Term) (@x3 Term))
                 (! (implies (HasTypeFuel @u0
                                          @x1
                                          (FStar.Pervasives.Native.tuple2 @x2
                                                                          @x3))
                             (and (is-FStar.Pervasives.Native.Mktuple2 @x1)
                                  (= @x2
                                     (FStar.Pervasives.Native.Mktuple2__a @x1))
                                  (= @x3
                                     (FStar.Pervasives.Native.Mktuple2__b @x1))))

                    :pattern ((HasTypeFuel @u0
                                           @x1
                                           (FStar.Pervasives.Native.tuple2 @x2
                                                                           @x3)))
                    :qid fuel_guarded_inversion_FStar.Pervasives.Native.tuple2))

         :named fuel_guarded_inversion_FStar.Pervasives.Native.tuple2))

Notice the implication and pattern are just on HasTypeFuel @u0---this quantifier can be instantiated with @u0=ZFuel. In contrast, the inversion axiom for other inductives (e.g., option) can only be instantiated with fuel (SFuel _). Note, the name and qid of this axiom are misleading: they are not fuel_guarded.

On the other hand, inverting the typing of the data constructor Mktuple2 is guarded by ifuel (as are other axioms, like the subterm ordering for the components of a pair).

;;;;;;;;;;;;;;;;data constructor typing elim
;;; Fact-ids: Name FStar.Pervasives.Native.tuple2; Namespace FStar.Pervasives.Native; Name FStar.Pervasives.Native.Mktuple2; Namespace FStar.Pervasives.Native
(assert (! 
         ;; def=c:\cygwin64\home\nswamy\workspace\everest\FStar\bin\..\ulib\FStar.Pervasives.Native.fst(59,22-59,30); use=c:\cygwin64\home\nswamy\workspace\everest\FStar\bin\..\ulib\FStar.Pervasives.Native.fst(59,22-59,30)
         (forall ((@u0 Fuel) (@x1 Term) (@x2 Term) (@x3 Term) (@x4 Term) (@x5 Term) (@x6 Term))
                 (! (implies (HasTypeFuel (SFuel @u0)
                                          (FStar.Pervasives.Native.Mktuple2 @x1
                                                                            @x2
                                                                            @x3
                                                                            @x4)
                                          (FStar.Pervasives.Native.tuple2 @x5
                                                                          @x6))
                             (and (HasTypeFuel @u0
                                               @x6
                                               Tm_type)
                                  (HasTypeFuel @u0
                                               @x4
                                               @x6)
                                  (HasTypeFuel @u0
                                               @x5
                                               Tm_type)
                                  (HasTypeFuel @u0
                                               @x3
                                               @x5)
                                  (HasTypeFuel @u0
                                               @x1
                                               Tm_type)
                                  (HasTypeFuel @u0
                                               @x2
                                               Tm_type)
                                  (HasTypeFuel @u0
                                               @x3
                                               @x1)
                                  (HasTypeFuel @u0
                                               @x4
                                               @x2)))

                    :pattern ((HasTypeFuel (SFuel @u0)
                                           (FStar.Pervasives.Native.Mktuple2 @x1
                                                                             @x2
                                                                             @x3
                                                                             @x4)
                                           (FStar.Pervasives.Native.tuple2 @x5
                                                                           @x6)))
                    :qid data_elim_FStar.Pervasives.Native.Mktuple2))

         :named data_elim_FStar.Pervasives.Native.Mktuple2))

This means that your first example can be proven with ifuel=0, since it amounts to proving something like

(implies (HasType x (tuple2 int int))
             (= x (Mktuple2 int int (proj_b (Mktuple2 int int (proj_b x) (proj_a x)) (proj_a (Mktuple2 int int (proj_b x) (proj_a x)))))

for which we don't need the data_elim axiom; just the inversion of tuple2 will do (since the equations for proj_a and proj_b are also independent of typing).

On the other hand, your second example with nested pairs fails, since it requires typing on the projected elements of a pair. Actually, here's a simpler one that fails:

type t3 = int & (int & int)

let f3 (x:t3) = 
  match x with
  | (x1, (x2, x3)) -> (x1, (x2, x3))

val f3_lemma (x:t3) : Lemma (f3 x == x)
#push-options "--fuel 0 --ifuel 0"
let f3_lemma x = ()

That's because what needs to be proven is roughly:

(implies (HasType x (tuple2 int (tuple2 int int))
             (= x (Mktuple2 int int (proj_a x)
                                                (Mktuple2 int int (proj_a (proj_b x)) (proj_b (proj_b x)))

And to "reduce" that proj_a (proj_b x), the solver needs to dervice that (proj_b x) = Mktuple2 _ _ _ _ or, HasType (tuple2 int int) (proj_b x)), for which it needs the fuel-guarded data_elim axiom.

You third example with options is similar.

I hope this explains the current behavior.

Revising the tuple encodings

We should consider changing the all the inversion axioms on tuples (of all arities) to not be guarded by fuel. This would remove the illusion of "first pair is free". The intention is to allow unbounded inversions of tupleN. And the inversion of tupleN typing is explicitly not guarded by fuel to enable this. But the fuel guards on the other axioms prevent the inversion from being fully usable beyond the first application.

Indeed, if I remove the (SFuel @u0) guard on the data_elim axiom, then Theophile's first two example (pairs and nested pairs) go through with ifuel=0. The third example which involves pair containing an option requires ifuel=1, since the pair inversion is free, but the inversion of the option requires one unit of ifuel.

Whether or not we can change this easily is really a question of impact on existing developments. I can try a regression build to see what happens.

I was thinking of a different fix. That the first example goes through with ifuel 0 and second with ifuel 1 is intuitive to me. The first one does not require any data constructor typing inversion, while the second one requires one such typing inversion.

The unintuitive one for me is the option one which requires ifuel 2.

In the encoding, there are two kinds of inversions, one for the typing of data constructors and one for the inductive typing itself. The first one is guarded with ifuel and that makes sense to me, since it is deriving new typing hypotheses.

The second one, e.g., if x:option t then Some? x || None? x, is asymmetric for tuples and options. For tuples, it doesn't require any ifuel (>= 0), for options it requires ifuel > 0. In the code it seems to depend on the # of data constructors.

I was wondering if we can make it so that the inversion of the inductive typing can be made to not have ifuel at all for all inductives, like the tuples. Then the third example should also go through with ifuel 1, similar to the second example.

The reason inversion on inductives like option is guarded by ifuel is to avoid polluting the solver's context with disjunctions.

For single constructor inductives, like tuples, there are no disjunctions---so that's why the typing inversion of tuples isn't fuel guarded.

Of course, for truly "inductive" inductives, like list, omitting the ifuel guard on typing inversion will lead to infinitely many inversions really flooding the context with case splits.

Of course, for truly "inductive" inductives, like list, omitting the ifuel guard on typing inversion will lead to infinitely many inversions really flooding the context with case splits.

@aseemr correctly pointed out (offline) that only removing fuel guards from typing inversion wouldn't actually lead to infinite regress, since the inversion of data constructors would still be guarded by ifuel.

Thank you for the detailed explanations! ifuel definitely didn't work as I expected.

To test my new understanding, I tested the following example that works with an ifuel of 1 (instead of 0, contrary to the similar example I gave above)

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

type t2 = unit & unit

val f2: t2 -> t2
let f2 x =
  match x with
  | (x1, x2) -> (x2, x1)

val f2_lemma:
  x:t2 -> Lemma (f2 x == x)
let f2_lemma x = ()

That being said, I don't know what should be the outcome of this issue? I guess it would be interesting to test what would happen if the inversion of single-constructor inductives (e.g. tuples, records) were not guarded by ifuel. But we can also close it without action, now that I understand ifuel a little bit better, I can use it for better proof engineering in my developments.

I guess it would be interesting to test what would happen if the inversion of single-constructor inductives (e.g. tuples, records) were not guarded by ifuel.

This is what I'm trying now

hi @TWal,

I have an F branch nik_3076 that is green on the F repo. It removes fuel guards on inversions of single-constructor types. Your examples are captured in tests/bug-reports/Bug3076.fst and they no longer require ifuel to invert tuples.

Would you be able to try this branch on your development to see how it fares?

Meanwhile, I have some regressions with this branch and proofs in Pulse.Checker that I have to chase down.

I tested on my projects, I have a few queries on MLS* that started to split that were fixed by bumping rlimits. The fix works on my original problem, so this would be okay for me! I also fixed my original problem on master by allowing inversions with SMTPats.

FStarLang / FStar

F* cannot invert a pair under some specific conditions? #3076

Explaining the current behavior

Revising the tuple encodings