SMTPats in currified Lemmas are not encoded to SMT

[R1kM]

Consider the following minimal code snippet (done with @W95Psp and @TWal)

assume val p: int -> int -> prop

assume val test: x:int -> y:int -> Lemma (p x y) [SMTPat (p x y)]
assume val test2: x:int -> Tot (y:int -> Lemma (p x y) [SMTPat (p x y)])

While these two functions should conceptually be the same, they lead to different behaviours when trying to use them. In particular, we observed that when only having test2 in the context, the SMTPat was not triggered, not allowing the automatic verification of p x y, while the behaviour with test was the expected one.

When looking at the SMT encodings of both these functions, the encoding of test is very concise (41 lines of smt2) and intuitive and includes the pattern annotation for SMTPat (p x y), while the encoding for test2 is much longer (299 lines), includes a lot of extra information and patterns (my possibly incorrect understanding is that it is used to show that the partial application is well-typed), and does not seem to have the pattern annotation corresponding to SMTPat (p x y).

Should the SMT encodings of both these functions be similar, maybe through some canonicalization of the F* term before being encoded to SMT?

This situation occured when trying to generate this lemma using F's reflection facilities. The currently exposed term API Tv_Arrow (in FStar.Reflection.Data) does not allow to have multi-binder arrows, while the underlying term representation Tm_arrow does. It thus currently does not seem possible to generate lemmas with SMTPats and multiple arguments using reflection in F.

[nikswamy]

This reminds me of https://github.com/FStarLang/FStar/pull/2305

If we offered FStar.Syntax.Util.canon_arrow through the reflection API that might unblock the scenario described in the last para above.

We might try to systematically using canon_arrow in the SMT encoding. It's worth trying, though that is likely to be more disruptive to programs that rely on the current behavior.

[R1kM]

I'd be curious about the second part, it seems like it could also optimize heavily some of the current VCs.

Regarding your first suggestion, do you mean to expose this in the reflection API, or to do this automatically in the hand-written Reflection modules?

[nikswamy]

1. For the first, I was thinking the easiest would be to offer FStar.Reflection.canon_arrow and you can call it explicitly when needed.

2. I doubt it would optimize existing VCs much. I don't think many existing programs use this explicitly curried lemma style. But, it's worth trying.

Both items are relatively small changes. Do you want to try it?

[R1kM]

Sure, I can give it a shot.

Regarding 1, I'm wondering if there are usecases where we would not want to have canonicalization, especially if the SMT encoding is not ideal? Exposing it to the user is a first step, but I wonder if it will remain too niche, hidden in a reflection module.

[R1kM]

We discussed this during today's F developers meeting. The conclusion was that the way forward might be to revive a variant of #2305, but applied during reflection (inside pack) instead of during extraction. In short, we want to apply canon_arrow by default when packing a term from its reflection view to an actual F term. The rationale is that this behaviour seems to be the behaviour commonly expected: it solves the specific issue here, i.e., by correctly encoding lemmas as functions that should be fully applied thus encoding their SMTPats, and it also reduces the size of the SMT encoding compared to the fully currified version.

@nikswamy mentioned that there might be some specific uses where the currified version is the expected one, but this seems to be uncommon. We decided that, for such expert uses, we will be exposing a different function (named for instance pack_currified_arrow) that would not use canon_arrow, with a small description trying to explain what the difference and expected use is.

[R1kM]

Below is a small example (courtesy of @TWal) of how the behavior presented in this issue can cause issues with reflection. With the current behavior, the SMTPat is not triggered, making the generated lemma annoying to use.

open FStar.Tactics

assume val p: int -> int -> prop

/// Generates a lemma with signature `val lem (x y:int) : Lemma (p x y) [SMTPat (p x y)]`
let gen_lemma () : Tac decls =
  let lemma_name = List.Tot.snoc (moduleof (top_env ()), "lem") in
  let x_binder = fresh_binder_named "x" (`int) in
  let x_term = binder_to_term x_binder in
  let y_binder = fresh_binder_named "y" (`int) in
  let y_term = binder_to_term y_binder in

  let all_binders = [x_binder; y_binder] in

  let lemma_requires = (`True) in
  let lemma_ensures = (`(fun () -> (p (`#x_term) (`#y_term)))) in
  let lemma_smtpat = (`[smt_pat (p (`#x_term) (`#y_term))]) in
  let lemma_comp = (pack_comp (C_Lemma lemma_requires lemma_ensures lemma_smtpat)) in
  let lemma_type = mk_arr all_binders lemma_comp in

  let lemma_val = mk_abs all_binders (`(admit())) in

  let lemma_letbinding = pack_lb ({
    lb_fv = pack_fv lemma_name;
    lb_us = [];
    lb_typ = lemma_type;
    lb_def = lemma_val;
  }) in
  [pack_sigelt (Sg_Let false [lemma_letbinding])]

%splice [lem] (gen_lemma ())

let f (x y:int) : Lemma (p x y) = ()

[mtzguido]

I just noticed that this does not work with the new view

open FStar.Tactics.V2

assume val p: int -> int -> prop

/// Generates a lemma with signature `val lem (x y:int) : Lemma (p x y) [SMTPat (p x y)]`
let gen_lemma () : Tac decls =
  let lemma_name = List.Tot.snoc (moduleof (top_env ()), "lem") in
  let x_binder = fresh_binder_named "x" (`int) in
  let x_term = binder_to_term x_binder in
  let y_binder = fresh_binder_named "y" (`int) in
  let y_term = binder_to_term y_binder in

  let all_binders = [x_binder; y_binder] in

  let lemma_requires = (`True) in
  let lemma_ensures = (`(fun () -> (p (`#x_term) (`#y_term)))) in
  let lemma_smtpat = (`[smt_pat (p (`#x_term) (`#y_term))]) in
  let lemma_comp = (pack_comp (C_Lemma lemma_requires lemma_ensures lemma_smtpat)) in
  let lemma_type = mk_arr all_binders lemma_comp in

  let lemma_val = mk_abs all_binders (`(admit())) in

  let lemma_letbinding = ({
    lb_fv = pack_fv lemma_name;
    lb_us = [];
    lb_typ = lemma_type;
    lb_def = lemma_val;
  }) in
  [pack_sigelt (Sg_Let {isrec=false; lbs=[lemma_letbinding]})]

%splice [lem] (gen_lemma ())

let f (x y:int) : Lemma (p x y) = () // fails