Carrying universes through to the SMT encoding

[nikswamy]

NB: This is a breaking change and projects that upgrade to this version of F may have to adjust their proofs

Background

In F* PR #2954, I mention work in progress to propagate universes to the SMT encoding.

In #2069, we note that WellFounded.axiom1 is incompatible with universe erasure in the SMT encoding.

In #3647, Gabriel points out that it one can directly exploit the erasure of universes in the SMT encoding to prove a contradiction.

This PR

So, in this PR, Gabriel revived an old incomplete branch where I started to add universes to the SMT encoding. I picked it up from there and propagated universes throughout the SMT encoding, getting things back to a point where the F* repo again verifies. This prevents the unsoundness in #3647.

Impact

The side-effect of this PR is that some proofs needed universe annotations, where previously they didn't. A common case is something like

let some_lemma () : Lemma (forall (a:Type u#a). p)

Previously, one could call some_lemma (), and F* would default the universe argument u#a to u#0, and since universes were erased anyway in the SMT encoding, this would suffice for a proof that required instantiating the quantifier for some type t say in Type u#1.

Now, in such cases, you have to explicit instantiate the universe at which you are invoking the lemma, i.e., some_lemma u#1 ()---since there is no way for F* to infer which universe to instantiate to in the caller's context.

Impact on other repos

• The main branches of Karamel, Pulse, and Steel repos work with this change.
• I have a branch of EverParse (_nik_smt_univs_2025) that also mostly works, but I have ~6 admits left there in discussion with @tahina-pro
• In HACL* PR Updates to HACL* in preparation for F* SMT encoding change hacl-star/hacl-star#1051, I reached a point where most proofs were working with proof_recovery, but it's not clear that HACL* will update to this branch of F* at the moment.

[gebner]

Something is still ignoring universes:

module Raise
#set-options "--print_implicits --print_universes"

// [raisable u#a u#b] iff [u#a <= u#b]
assume val raisable : p:prop { Type u#(max a b) } // hack to specify universe parameters for raisable

// (** [raise_t a] is an isomorphic copy of [a] (living in universe a) in universe [b] **)
assume val raise_t (t : Type u#a { raisable u#a u#b }) : Type u#b

[@@expect_failure]
assume val this_does_not_work_as_expected (a: Type u#a) (h: squash (raisable u#0 u#0)) : raise_t u#a u#b a

assume val this_should_not_work (a: Type u#a { raisable u#0 u#0 }) : raise_t u#a u#b a

The last line works, but the query raisable u#0 u#0 ==> raisable u#a u#b that should fail doesn't even make it to Z3.

[nikswamy]

thanks for the example, will have a look

[mtzguido]

Just noticed some weirdness when looking at the failures in SCIO*. The last definition fails:

open FStar.FunctionalExtensionality

let min2 (t : Type u#1) (x : t) : (int ^-> t) =
  on_domain _ (fun _ -> x)

let min3 (t : Type u#1) (x : int) : (t ^-> int) =
  on_domain _ (fun _ -> x)

let min4 (t : Type u#1) (x : t) : (t ^-> t) =
  on_domain _ (fun _ -> x)

let min' (b : Type0) (t : Type u#1) (x : t) : (b ^-> t) =
  on_domain b (fun _ -> x)

let min (t : Type u#1) (x : t) : ((unit -> Dv int) ^-> t) =
  // idempotence_on_domain u#0 u#1 #(unit -> Dv int) (fun _ -> x);
  on_domain (unit -> Dv int) (fun _ -> x)

Uncommenting the lemma call makes it work. Looks like the pattern for this lemma isn't being triggered when the type an effectful arrow? This should be a special case of min' .