Merge pull request #6 from FStarLang/update_nightly_2026-04-29

Update nightly 2026 04 29

Author: nikswamy

.gitignore

@@ -17,3 +17,6 @@ krml/
 
 # Binary F* install (created by ./setup.sh binary)
 /fstar/
+bench/results/
+bench/BENCHMARK_REPORT.txt
+bench/repros/

autoclrs/ch02-getting-started/CLRS.Ch02.InsertionSort.Impl.fst

@@ -72,7 +72,7 @@ fn insertion_sort
       prefix_sorted s (SZ.v vj) /\
       // Complexity: comparisons so far <= vj*(vj-1)/2
       vc >= reveal c0 /\
-      vc <= reveal c0 + op_Multiply (SZ.v vj) (SZ.v vj - 1) / 2
+      vc <= reveal c0 + op_Star (SZ.v vj) (SZ.v vj - 1) / 2
     )
   decreases (SZ.v len `Prims.op_Subtraction` SZ.v !j)
   {
@@ -118,8 +118,8 @@ fn insertion_sort
           Seq.index s_inner k1 <= Seq.index s_inner k2) /\
         // Complexity: vc + vi bounded
         vc_inner >= reveal c0 /\
-        vc_inner <= reveal c0 + op_Multiply (SZ.v vj) (SZ.v vj - 1) / 2 + SZ.v vj + 1 - SZ.v vi /\
-        (not vcont ==> vc_inner <= reveal c0 + op_Multiply (SZ.v vj) (SZ.v vj - 1) / 2 + SZ.v vj)
+        vc_inner <= reveal c0 + op_Star (SZ.v vj) (SZ.v vj - 1) / 2 + SZ.v vj + 1 - SZ.v vi /\
+        (not vcont ==> vc_inner <= reveal c0 + op_Star (SZ.v vj) (SZ.v vj - 1) / 2 + SZ.v vj)
       )
     decreases (SZ.v !i)
     {

autoclrs/ch02-getting-started/CLRS.Ch02.InsertionSort.Lemmas.fst

@@ -28,4 +28,4 @@ let lemma_combine_sorted_regions
   = ()
 
 let lemma_triangle_step (vj: nat)
-  = assert (op_Multiply vj (vj - 1) + op_Multiply 2 vj == op_Multiply vj (vj + 1))
+  = assert (op_Star vj (vj - 1) + op_Star 2 vj == op_Star vj (vj + 1))

autoclrs/ch02-getting-started/CLRS.Ch02.InsertionSort.Lemmas.fsti

@@ -32,4 +32,4 @@ val lemma_combine_sorted_regions
 
 val lemma_triangle_step (vj: nat)
   : Lemma (requires vj >= 1)
-          (ensures op_Multiply vj (vj - 1) / 2 + vj == op_Multiply (vj + 1) vj / 2)
+          (ensures op_Star vj (vj - 1) / 2 + vj == op_Star (vj + 1) vj / 2)

autoclrs/ch02-getting-started/CLRS.Ch02.InsertionSort.Spec.fst

@@ -14,5 +14,5 @@ module Seq = FStar.Seq
 //SNIPPET_START: complexity_bounded
 let complexity_bounded (cf c0: nat) (n: nat) : prop =
   cf >= c0 /\
-  cf - c0 <= op_Multiply n (n - 1) / 2
+  cf - c0 <= op_Star n (n - 1) / 2
 //SNIPPET_END: complexity_bounded

autoclrs/ch02-getting-started/CLRS.Ch02.MergeSort.Complexity.fst

@@ -1,6 +1,5 @@
 module CLRS.Ch02.MergeSort.Complexity
 
-open FStar.Mul
 
 (** 
   Complexity analysis for merge sort from CLRS Chapter 2.

autoclrs/ch02-getting-started/CLRS.Ch02.MergeSort.Complexity.fsti

@@ -5,7 +5,6 @@
 *)
 module CLRS.Ch02.MergeSort.Complexity
 
-open FStar.Mul
 
 /// Ceiling of log base 2
 val log2_ceil (n: pos) : nat

autoclrs/ch02-getting-started/CLRS.Ch02.MergeSort.Impl.fst

@@ -35,6 +35,8 @@ module GR = Pulse.Lib.GhostReference
 module SZ = FStar.SizeT
 module Seq = FStar.Seq
 
+#set-options "--split_queries always"
+
 // ================================================================
 // Helper: copy range between arrays
 // ================================================================
@@ -86,7 +88,7 @@ fn copy_range
 // Merge Implementation
 // ================================================================
 
-#push-options "--z3rlimit 20 --fuel 2 --ifuel 1"
+#push-options "--z3rlimit 10 --fuel 2 --ifuel 1 --split_queries always"
 
 //SNIPPET_START: merge_sig
 fn merge

autoclrs/ch02-getting-started/CLRS.Ch02.MergeSort.Lemmas.fst

@@ -82,7 +82,7 @@ let seq_merge_permutation (s1 s2: Seq.seq int)
 // Merge preserves sortedness
 // ================================================================
 
-#push-options "--z3rlimit 2 --fuel 2 --ifuel 1"
+#push-options "--z3rlimit 2 --fuel 2 --ifuel 1 --split_queries always"
 
 let rec seq_merge_all_ge (v: int) (s1 s2: Seq.seq int)
   : Lemma (requires all_ge v s1 /\ all_ge v s2)

autoclrs/ch04-divide-conquer/CLRS.Ch04.MatrixMultiply.Impl.fst

@@ -15,7 +15,6 @@ open Pulse.Lib.Pervasives
 open Pulse.Lib.Array
 open FStar.SizeT
 open Pulse.Lib.Reference
-open FStar.Mul
 open FStar.Classical
 open CLRS.Ch04.MatrixMultiply.Spec