SMT Encoding issue (forcing thunked names)

[jaybosamiya]

Opening a GitHub issue to better track this. Original message below.

---

I faced a curious issue in one of the proofs within code that I was writing in Vale, and thus decided to try to track it down.

The error message:

(Error) Unexpected output from Z3: (error "line 314252 column 61: Wrong number of arguments (1) passed to function (declare-fun Vale.Transformers.Locations.location () Term)")
(error "line 314297 column 61: Wrong number of arguments (1) passed to function (declare-fun Vale.Transformers.Locations.location () Term)")
(error "line 314310 column 60: Wrong number of arguments (1) passed to function (declare-fun Vale.Transformers.Locations.location () Term)")
....(similar lines for a _quite_ a while)....

The relevant code (and exact commit) in question: https://github.com/project-everest/hacl-star/blob/0cf2bf040d75763c02566425839e099f4c260172/vale/code/lib/transformers/Vale.Transformers.InstructionReorderSanityChecks.fst#L22-L32

What is weirder is that if I re-run F* on the file, it succeeds. This is because it ends up using hints, and this allows it to succeed somehow (even though it failed the first time around?!).

This bug tends to manifest even without Vale specific flags (i.e., without Vale's --z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 --max_fuel 1 --max_ifuel 1 --initial_ifuel 0 --smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr wrapped), so none of them are the issue.

Trying to debug this issue, I --log_queriesd the file, and clearly, .smt2 had the following code in it:

;;;;;;;;;;;;;;;;Constructor
(declare-fun Vale.Transformers.Locations.location () Term)

(earlier in the file) and

(Vale.Transformers.Locations.location Dummy_value)

(later in the file, in a lot of places).

Clearly, the function doesn't want to argue with a dummy :slightly_smiling_face: Seriously though, a Dummy_value is being passed where no argument was expected.

So I searched the F* code base for Dummy_value, and src/smtencoding/FStar.SMTEncoding.Term.fs has a nice explanation of why it exists, and when it is used. All looks well and good, at least as per the English explanation in the comments. The trouble seems to be the code, which throws a Dummy_value when it shouldn't be doing so. And that is where I stopped understanding what is going wrong.

I have tried to make a smaller example that demonstrates this failing behavior but have been unable to do so yet. Hopefully the above description is sufficient to understand what the bug is.

[mtzguido]

This is still present, and I suspect related to friending 'Vale.Transformers.Location', since I can't minimize that bit away.

[mtzguido]

Slight minimization for this file:

module Vale.Transformers.InstructionReorderSanityChecks

open Vale.X64.Instructions_s
open Vale.X64.Machine_s
open Vale.X64.InsLemmas
open Vale.Transformers.InstructionReorder

open Vale.Transformers.Locations
friend Vale.Transformers.Locations

let ins_exchange_sanity_check1_1 : unit =
  let _ = (make_instr ins_IMul64 (OReg rRax) (OReg rRbx)) in
  ()

still requiring other Vale modules.