Carrying universes through to the SMT encoding

.github/workflows/check-friends.yml

@@ -23,6 +23,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - name: Checkout karamel
         uses: actions/checkout@master
@@ -61,6 +62,8 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
+
 
       # krml test needs node
       - uses: actions/setup-node@v4
@@ -89,6 +92,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - name: Checkout steel
         uses: actions/checkout@master
@@ -121,6 +125,8 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
+
 
       - uses: mtzguido/gci-download@master
         with:
@@ -150,6 +156,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -182,6 +189,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - name: Build (after setting up cargo env)
         run: . $HOME/.cargo/env && make -C pulse -skj$(nproc)
@@ -208,6 +216,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -243,6 +252,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -284,6 +294,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -323,6 +334,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -347,6 +359,7 @@ jobs:
         uses: actions/checkout@master
         with:
           path: everparse/
+          ref: _nik_smt_univs_2025
           repository: project-everest/everparse
 
       - name: Build
@@ -378,6 +391,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -424,6 +438,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -463,6 +478,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -497,6 +513,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -540,6 +557,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -578,6 +596,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -621,6 +640,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: mtzguido/gci-download@master
         with:
@@ -654,6 +674,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - name: Checkout steel
         uses: actions/checkout@master
@@ -687,6 +708,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: actions/checkout@master
         with:
@@ -712,6 +734,7 @@ jobs:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
       - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
 
       - uses: actions/checkout@master
         with:

Makefile

@@ -463,6 +463,10 @@ test-1: override FSTAR_EXE := $(abspath stage1/out/bin/fstar.exe)
 test-1: stage1
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)
 
+_unit-tests-1: override FSTAR_EXE := $(abspath stage1/out/bin/fstar.exe)
+_unit-tests-1: stage1
+	$(MAKE) _unit-tests FSTAR_EXE=$(FSTAR_EXE)
+
 test-2: override FSTAR_EXE := $(abspath stage2/out/bin/fstar.exe)
 test-2: stage2
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)

examples/algorithms/BinarySearch.fst

@@ -106,13 +106,15 @@ let hint1 y a = ()
 val hint2 : t:(seq int) -> a:int -> mid:int
   -> Lemma
        (requires
-          (forall i1 i2. (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
+          (forall i1 i2.
+            {:pattern index t i1; index t i2}
+             (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
           (0 <= mid) /\
           (mid < length t) /\
           (index t mid < a))
        (ensures
           (forall p. (((0 <= p) /\ (p < length t) /\ (index t p = a) /\ (p <= mid)) ==> False)))
-let hint2 t a mid = hint1 (index t mid) a
+let hint2 t a mid = ()
 
 val hint3 : y:int -> a:int -> Lemma
   (requires True)
@@ -122,7 +124,9 @@ let hint3 y a = ()
 val hint4 : t:(seq int) -> a:int -> mid:int
   -> Lemma
        (requires
-          (forall i1 i2. (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
+          (forall i1 i2. 
+              {:pattern index t i1; index t i2} 
+            (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
           (0 <= mid) /\
           (mid < length t) /\
           (a < index t mid))

examples/crypto/Sig.fst

@@ -32,7 +32,7 @@ type sk   = lbytes sksize
 
 assume val fdh_rsa: sk -> text -> Tot sig_t
 
-assume new type key_prop : pk -> text -> Type
+assume val key_prop : pk -> text -> Type0
 type prop_pk (p:(text -> Type)) = k:pk{key_prop k == p}
 
 assume val sk_to_pk : sk -> Tot pk

examples/data_structures/BinaryTreesEnumeration.fsti

@@ -235,16 +235,17 @@ let memP_concatMap_intro #a #b (x: a) (y: b) (f:a -> list b) (l: list a) :
       can I get rid of them without cluttering the rest of the proof with many
       copies of the same function?  Can I infer them by unifying with the
       current “goal”? *)
-let product_complete (#a #b: Type) (l1: list a) (l2: list b) x1 x2 :
+module T = FStar.Tactics
+let product_complete (#a:Type u#a) (#b: Type u#b) (l1: list a) (l2: list b) x1 x2 :
   Lemma (List.memP x1 l1 ==>
          List.memP x2 l2 ==>
          List.memP (x1, x2) (product #a l1 l2)) =
     let x = (x1, x2) in
     let unfold f2 x1 = fun x2 -> (x1, x2) in
-    let f1 = fun x1 -> List.Tot.map (f2 x1) l2 in
+    let unfold f1 = fun x1 -> List.Tot.map (f2 x1) l2 in
     let l = f1 x1 in
     let ls = List.Tot.map f1 l1 in
-    assert (product l1 l2 == List.Tot.concatMap f1 l1);
+    assert (product l1 l2 == List.Tot.concatMap f1 l1) by (T.trefl());
 
     memP_map_intro (f2 x1) x2 l2
       <: Lemma (List.memP x2 l2 ==> List.memP x l);

examples/data_structures/LowStar.Lens.Buffer.fsti

@@ -189,11 +189,11 @@ val mk (#a:_) (#p:_) (#q:_) (b:B.mbuffer a p q) (f:flavor b) (snap:HS.mem{B.live
   : Tot (l:buffer_lens b f{(lens_of l).snapshot == snap})
 
 /// `elim_inv`: Revealing the abstract invariant of buffer lenses
-val elim_inv (#a:_) (#p:_) (#q:_) 
+val elim_inv (#a:Type) (#p:_) (#q:_) 
              (#b:B.mbuffer a p q)
              (#f:flavor b)
              (bl:buffer_lens b f)
-  : Lemma (reveal_inv();
+  : Lemma (reveal_inv u#0 u#0 ();
           (forall (h:HS.mem).{:pattern (lens_of bl).invariant (lens_of bl).x h}
            let l = lens_of bl in
            (exists h'.{:pattern mk b f h'} B.live h' b /\ bl == mk b f h') /\

examples/data_structures/LowStar.Lens.Tuple2.fst

@@ -294,7 +294,7 @@ let elim_tup2_inv
        (bl1:LB.buffer_lens b1 f1)
        (bl2:LB.buffer_lens b2 f2{composable (LB.lens_of bl1) (LB.lens_of bl2)})
    : Lemma (let t = mk_tup2 bl1 bl2 in
-            reveal_inv();
+            reveal_inv u#0 u#0 ();
             (forall h. {:pattern inv (lens_of t) h}
               inv (lens_of t) h ==>
               (LB.lens_of bl1).invariant b1 h /\

examples/data_structures/LowStar.Lens.fsti

@@ -225,7 +225,7 @@ effect LensST (a:Type)
 
 /// `reveal_inv`: Revealing the abstract invariant
 val reveal_inv (_:unit)
-  : Lemma ((forall #a #b (l:hs_lens a b) h. {:pattern inv l h}
+  : Lemma ((forall (#a:Type u#a) (#b:Type u#b) (l:hs_lens a b) h. {:pattern inv l h}
             inv l h <==>
             (l.invariant l.x h /\
              B.modifies (as_loc l.footprint) l.snapshot h /\

examples/data_structures/RBTreeIntrinsic.fst

@@ -383,6 +383,7 @@ val balanceLB_preserves_sort : #h:nat -> #c:color -> a:almostNode h -> x:int ->
   (requires almostNode_sorted a /\ sorted b /\ chain (almostNode_max a) x (min b))
   (ensures  hiddenTree_sorted (balanceLB a x b))
 let balanceLB_preserves_sort #h #c left z d = ()
+#restart-solver
 
 val balanceRB_preserves_sort : #h:nat -> #c:color -> a:rbnode h c -> x:int -> b:almostNode h ->
   Lemma 

examples/doublylinkedlist/DoublyLinkedList.fst

@@ -1221,7 +1221,7 @@ let lemma_dll_links_contained (#t:Type) (h0:heap) (d:dll t) (i:nat) :
     lemma_unsnoc_is_last nl
 
 #set-options "--z3rlimit 10 --initial_ifuel 2"
-
+#restart-solver
 let lemma_dll_links_disjoint (#t:Type) (h0:heap) (d:dll t) (i:nat) :
   Lemma
     (requires (
@@ -1964,8 +1964,8 @@ let dll_append (#t:Type) (d1 d2:dll t) :
 
 #reset-options
 
-#set-options "--z3rlimit 60 --max_fuel 2 --max_ifuel 1"
-
+#set-options "--z3rlimit 200 --max_fuel 2 --max_ifuel 1 --query_stats --split_queries no --z3smtopt '(set-option :smt.qi.eager_threshold 5)'"
+#restart-solver
 let dll_split_using (#t:Type) (d:dll t) (e:pointer (node t)) :
   StackInline (dll t * dll t)
     (requires (fun h0 ->

examples/doublylinkedlist/DoublyLinkedListIface.fst

@@ -604,7 +604,7 @@ let dll_insert_at_tail #t d n =
 #reset-options
 
 #set-options "--z3rlimit 80 --max_fuel 2 --max_ifuel 1"
-
+#push-options "--z3rlimit_factor 4"
 let dll_insert_before #t n' d n =
   let h00 = HST.get () in
   HST.push_frame ();
@@ -693,7 +693,7 @@ let dll_insert_before #t n' d n =
   // assert (as_payload_list h11 d == l_insert_before'
   //           (as_list h00 d `L.index_of` n') (as_payload_list h00 d) (g_node_val h00 n));
   ()
-
+#pop-options
 #reset-options
 
 #set-options "--z3rlimit 80 --max_fuel 2 --max_ifuel 1"

examples/dsls/bool_refinement/BoolRefinement.fst

@@ -4,8 +4,7 @@ module R = FStar.Reflection.V2
 module L = FStar.List.Tot
 open FStar.List.Tot
 
-#set-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"
-
+#set-options "--z3smtopt '(set-option :smt.qi.eager_threshold 20)' --z3smtopt '(set-option :smt.arith.nl false)'"
 let var = nat
 let index = nat
 
@@ -126,6 +125,7 @@ let rec close_exp' (e:src_exp) (v:var) (n:nat)
 
 let open_exp e v = open_exp' e v 0
 let close_exp e v = close_exp' e v 0
+#restart-solver
 
 let rec open_close' (e:src_exp) (x:var) (n:nat { ln' e (n - 1) })
   : Lemma (open_exp' (close_exp' e x n) x n == e)
@@ -607,6 +607,7 @@ let rec extend_env_l_lookup_bvar (g:R.env) (sg:src_env) (x:var)
 
 //key lemma about src types: Their elaborations are closed
 #push-options "--z3rlimit_factor 4 --fuel 8 --ifuel 2"
+#restart-solver
 let rec src_refinements_are_closed_core
                        (n:nat)
                        (e:src_exp {ln' e (n - 1) && closed e}) 
@@ -1146,7 +1147,8 @@ let rec src_typing_freevars #f (sg:src_env) (e:src_exp) (t:s_ty) (d:src_typing f
       src_typing_freevars _ _ _ dbody
 #pop-options
 
-#push-options "--z3rlimit_factor 4"
+#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2"
+#restart-solver
 let rec src_typing_renaming (#f:RT.fstar_top_env)
                             (sg sg':src_env)
                             (x:var { None? (lookup sg x) && None? (lookup sg' x) })
@@ -1259,6 +1261,7 @@ let rec src_typing_renaming (#f:RT.fstar_top_env)
       in
       let dt = src_ty_ok_renaming _ _ _ _ _ _ dt in
       T_If _ _ _ _ _ _ _ _ db dt1 dt2 st1 st2 dt
+#pop-options
 
 let sub_typing_weakening #f (sg sg':src_env) 
                          (x:var { None? (lookup sg x) && None? (lookup sg' x) })
@@ -1323,6 +1326,8 @@ let sub_typing_weakening #f (sg sg':src_env)
 
       | _ -> admit ())
 
+#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2"
+#restart-solver
 let rec src_typing_weakening #f (sg sg':src_env) 
                              (x:var { None? (lookup sg x) && None? (lookup sg' x) })
                              (b:binding)
@@ -1518,6 +1523,8 @@ let freevars_refinement (e:R.term) (bv0:_)
   = ()
 #pop-options
 
+#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2"
+#restart-solver
 let rec soundness (#f:RT.fstar_top_env)
                   (#sg:src_env { src_env_ok sg } ) 
                   (#se:src_exp { ln se })
@@ -1673,7 +1680,9 @@ and src_ty_ok_soundness (#f:RT.fstar_top_env)
      in
      freevars_refinement (elab_exp e) bv0;
      RT.T_Refine (extend_env_l f sg) x RT.bool_ty refinement' _ _ _ _ bool_typing dr
+#pop-options
 
+#restart-solver
 let soundness_lemma (f:RT.fstar_top_env)
                     (sg:src_env { src_env_ok sg }) 
                     (se:src_exp { ln se })