Minimal example: hints that don't replay

[s-zanella]

Here's a minimal example of recorded hints that don't replay.
This seem to happen a lot in larger examples (see e.g. #893).

$ cat M.fst
module M
let n = 1ul

$ bin/fstar.exe M.fst --hint_info --record_hints
(./M.fst(2,0-2,11))
	Query (M.n, 1)	succeeded in 674 milliseconds with fuel 2 and ifuel 1
Verified module: M (790 milliseconds)
All verification conditions discharged successfully

$ bin/fstar.exe M.fst --hint_info --use_hints
(/Users/anonymous/fstar/M.fst) digest is valid; using hints db.
(./M.fst(2,0-2,11))
	Query (M.n, 1)	failed (with hint) in 61 milliseconds with fuel 2 and ifuel 1
(./M.fst(2,0-2,11))
	Query (M.n, 1)	succeeded in 651 milliseconds with fuel 2 and ifuel 1
Hint-info (./M.fst(2,0-2,11)): Replay failed in 61 milliseconds
Verified module: M (881 milliseconds)
All verification conditions discharged successfully

$ cat M.fst.hints
[
  "69Qǎ\u0010Q????7?\u001d?",
  [
    [
      "M.n",
      1,
      2,
      1,
      [
        "@query", "b2t_def", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ]
  ]
]

$ z3 --version
Z3 version 4.5.0 - 64 bit

Looking at the Z3 queries using --log_queries I didn't notice anything odd. Looks like everything in the computed unsat core is in the query used to replay the hint.

@wintersteiger Do you mind having a look to see if this is an issue with the F* encoding or internal to Z3?
queries.zip

[wintersteiger]

Sweet! Thanks for the small example! I'm back from vacation and will take a look at this immediately.

[s-zanella]

Discussed this briefly with Christoph, who has been working on a long-term solution in the cwinter_checked_hints branch.

An easy work around that already works with F* master and the Z3 nightly build (https://github.com/Z3Prover/bin/tree/master/nightly) is to pass --z3cliopt "smt.core.extend_patterns=true smt.core.extend_patterns.max_distance=1" to F*, which will in turn pass these options to Z3 and will result in a larger unsat-core and a replayable hint.

[nikswamy]

I don't think this is a bug.

[wintersteiger]

"Performance bug" :-)

[nikswamy]

So, it seems that Z3 is not reported two important assertions in the unsat core.

If I add these two assertions back in manually:

;;;;;;;;;;;;;;;;Correspondence of recursive function to instrumented version
(assert (! (forall ((@x0 Term))
                   (! (= (Prims.pow2 @x0)
                         (Prims.pow2.fuel_instrumented MaxFuel
                                                       @x0))
                      

                      :pattern ((Prims.pow2 @x0))
                      :qid fuel_correspondence_Prims.pow2.fuel_instrumented))
           :named fuel_correspondence_Prims.pow2.fuel_instrumented))

;;;;;;;;;;;;;;;;Fuel irrelevance
(assert (! (forall ((@u0 Fuel) (@x1 Term))
                   (! (= (Prims.pow2.fuel_instrumented (SFuel @u0)
                                                       @x1)
                         (Prims.pow2.fuel_instrumented ZFuel
                                                       @x1))
                      

                      :pattern ((Prims.pow2.fuel_instrumented (SFuel @u0)
                                                              @x1))
                      :qid fuel_irrelevance_Prims.pow2.fuel_instrumented))
           :named fuel_irrelevance_Prims.pow2.fuel_instrumented))

then the proof is easily replayed.

[nikswamy]

Here's a rough sketch of what's going on:

We need to prove:

                         (Prims.op_LessThanOrEqual (BoxInt 0)
                                                   (FStar.UInt.max_int (BoxInt 32))

We have:

;;;;;;;;;;;;;;;;Equation for FStar.UInt.max_int
(assert (! (forall ((@x0 Term))
                   (! (= (FStar.UInt.max_int @x0)
                         (Prims.op_Subtraction (Prims.pow2 @x0)
                                               (BoxInt 1)))
                      

                      :pattern ((FStar.UInt.max_int @x0))
                      :qid equation_FStar.UInt.max_int))
           :named equation_FStar.UInt.max_int))

So, this crucially involves reasoning about (Prims.pow2 (BoxInt 32))

Which is provided by this lemma:

;;;;;;;;;;;;;;;;Lemma: FStar.UInt.pow2_values
(assert (! (forall ((@x0 Term))
                   (! (implies (HasType @x0
                                        Prims.nat)
                               (let ((@lb1 @x0)) (ite (= @lb1
                                                         (BoxInt 0))

                                                      ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(11,11-11,14); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                      (= (Prims.pow2 @x0)
                                                         (BoxInt 1))

                                                      (ite (= @lb1
                                                              (BoxInt 1))

                                                           ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(12,11-12,14); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                           (= (Prims.pow2 @x0)
                                                              (BoxInt 2))

                                                           (ite (= @lb1
                                                                   (BoxInt 8))

                                                                ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(13,11-13,16); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                (= (Prims.pow2 @x0)
                                                                   (BoxInt 256))

                                                                (ite (= @lb1
                                                                        (BoxInt 16))

                                                                     ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(14,11-14,18); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                     (= (Prims.pow2 @x0)
                                                                        (BoxInt 65536))

                                                                     (ite (= @lb1
                                                                             (BoxInt 31))

                                                                          ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(15,11-15,23); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                          (= (Prims.pow2 @x0)
                                                                             (BoxInt 2147483648))

                                                                          (ite (= @lb1
                                                                                  (BoxInt 32))

                                                                               ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(16,11-16,23); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                               (= (Prims.pow2 @x0)
                                                                                  (BoxInt 4294967296))

                                                                               (ite (= @lb1
                                                                                       (BoxInt 63))

                                                                                    ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(17,11-17,32); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                                    (= (Prims.pow2 @x0)
                                                                                       (BoxInt 9223372036854775808))

                                                                                    (ite (= @lb1
                                                                                            (BoxInt 64))

                                                                                         ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(18,11-18,33); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                                         (= (Prims.pow2 @x0)
                                                                                            (BoxInt 18446744073709551616))

                                                                                         (implies (= @lb1
                                                                                                     (BoxInt 128))

                                                                                                  ;; def=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(19,12-19,49); use=D:\workspace\everest\FStar\ulib\FStar.UInt.fst(22,4-22,15)
                                                                                                  (= (Prims.pow2 @x0)
                                                                                                     (BoxInt 340282366920938463463374607431768211456))
                                                                                                  )))))))))))
                      

                      :pattern ((Prims.pow2.fuel_instrumented ZFuel
                                                              @x0))
                      :qid lemma_FStar.UInt.pow2_values))
           :named lemma_FStar.UInt.pow2_values))

But notice that its pattern has a (Prims.pow2.fuel_instrumented ZFuel @x0)

Not (Prims.pow2 @x0)

So, the only way to complete this proof from here is to rely first on fuel_correspondence_Prims.pow2.fuel_instrumented and then on fuel_irrelevance_Prims.pow2.fuel_instrumented, which provides the term needed to trigger lemma_FStar.UInt.pow2_values.

Now, I can apply various ad hoc patches on the the F* side, e.g., always including the fuel_correspondence and fuel_irrelevance assertions when replaying a hint. Tweaking the encoding of the lemma so that the pattern uses pow2 rather than pow2.fuel_instrumented. But, that feels a bit random.

@wintersteiger : Do you have an explanation for why Z3 is not reporting those two crucial assertions in the unsat core?

[s-zanella]

I believe this is exactly the situation the optionsmt.core.extend_patterns=true attempts to address: extend the unsat core with terms that may trigger quantifier instances. This is often too brutal as even when setting smt.core.extend_patterns.max_distance=1 you get a core that is substantially larger than the unsat core without this option.

[wintersteiger]

As @s-zanella says, this is one of those situations where the term/quantifier instance dependencies aren't tracked. Your analysis matches what I have so far; I can get the proof go through if I magically (recorded) know the right terms, otherwise it needs the additional quantifiers. I'm currently digging into the code base to see whether we can track at least simple dependencies efficiently.

[nikswamy]

To me, this is not the canonical situation of an assertion only contributing patterns and hence not included in the unsat core. This seems to me a possible bug in z3 reporting an unsat core that's really not unsat. How can you prove unsat without the fuel irrelevance and fuel correspondence assertions?