Update nightly 2026 04 29#6
Merged
Merged
Conversation
- Remove all 'open FStar.Mul' (257 files) — FStar.Mul is no longer needed - Replace op_Multiply with op_Star (45 files) — renamed in Prims - Fix tuple type syntax: * -> & in type position (7 files) - CountingSort.ImplTest: split chained comparisons for new parser - Heap.Complexity: add build_heap_ops_explicit to work around lambda normalization - BFS.Impl: bump z3rlimit 20->40 - DFS.Impl: add assertion hints for white_scan_zero - IterativeBFS: bump z3rlimit 60->80 - MaxFlow.Lemmas: bump z3rlimit 20->40 - JarvisMarch.Impl: bump z3rlimit 10->30 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fixes needed for FStarLang/FStar@276817c2e3 (_nik_avoid_uvar_abstraction HEAD): - BFS.Impl: remove ill-typed pure assertion with erased multiplication, bump z3rlimit 40->60 - TopologicalSort.Impl: remove ill-typed pure assertions with erased multiplication (same pattern as BFS) - KMP: add explicit refinement assertions before Bridge.extend_maximality calls, bump z3rlimit 20->80 (prefix_function) and 20->80 (kmp_search) - Heap.Impl: use outer-scope variable s0 instead of s_cur in SZ.fits - RodCutting.Extended: bump z3rlimit 10->40 - ModExpLR.Impl: bump z3rlimit 10->40 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Removed lemma_mod_add_assoc which required fuel 8 and used rlimit 4.7/5.0 (very fragile). Replaced all call sites with FStar.Math.Lemmas.lemma_mod_plus_distr_l which has the exact same statement and verifies instantly at fuel 2. Also targeted lemma_tail_update and lemma_tail_dequeue to use more precise arguments to lemma_mod_plus_distr_l, reducing rlimit usage from ~2.0 to near zero. Queue.Impl.fst total verification time: 15.9s -> 10.8s Max individual query: 850ms/fuel 8 -> all under 100ms/fuel 2 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Split the pigeonhole contradiction into a helper lemma (path_len_cycle_false) so Z3 queries are smaller. This reduces the max rlimit usage from 6.18/8 to 2.0/5 and removes the need for a --z3rlimit 8 push-options. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… extension The inner verification loop needed Z3 help to extend the forall/exists invariant properties from k < vj to k < vj + 1. Added a combined pure helper lemma (inner_loop_invariant_step) that breaks the quantifier reasoning into a smaller, manageable proof step. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- JarvisMarch.Impl.fst: reduce rlimit 60 -> 20 by adding explicit jarvis_loop_step lemma call in the loop body - JarvisMarch.fst: reduce rlimit 40 -> 30 for extend_valid_jarvis_hull - GrahamScan.fst: reduce rlimit 20 -> 10 by calling all_left_turns_sz_prefix - JarvisMarch.Lemmas.fst: add --split_queries always to fix Warning 349 on find_next_aux_beats_all Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Added explicit assert statements in both branches of the case split to help Z3 instantiate the universally quantified preconditions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…d --ifuel 2 transfer_smaller_slice and transfer_strictly_larger_slice were fragile: - transfer_smaller_slice failed at ifuel 1 due to Z3 context pollution from prior lemmas, then retried at ifuel 2 (~2.5s total with non-determinism) - transfer_strictly_larger_slice showed similar instability Fix: Add #restart-solver before each to clear accumulated Z3 context, and #push-options "--ifuel 2" for deterministic Seq.slice quantifier matching. Results (3 consecutive runs, all deterministic): - transfer_larger_slice: ~445ms (unchanged, no restart needed) - transfer_smaller_slice: ~275ms (was ~2500ms with retry) - transfer_strictly_larger_slice: ~555ms (was ~421ms but now deterministic) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- MergeSort.Lemmas.fst: add --split_queries always to fix Warning 349 where seq_merge_sorted proof relied on implicit query splitting - MergeSort.Impl.fst: add module-level #set-options "--split_queries always" (needed because Pulse VCs don't respect split_queries in #push-options) and reduce merge function rlimit from 20 to 10 All proofs pass cleanly with no warnings. Max used rlimit is ~7.5 (well within the 10 limit). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Added a pure helper lemma that bridges the Pulse inner loop result to Spec.kmp_step_result, plus explicit assertions for spec invariants from kmp_count_step. This breaks the large VC into smaller pieces that Z3 can handle within rlimit 80. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
KaRaMeL fix (FStar/karamel/lib/Simplify.ml):
- Added bounds check 'i < List.length ts' before 'List.nth ts i = TUnit'
in the unused parameter elimination pass (line 236)
- Without this check, List.nth crashes with 'Failure("nth")' when the
callee's arrow type has fewer type stages than actual arguments, which
occurs with Pulse-extracted code containing ghost/erased parameters
Proof optimization (CLRS.Ch11.HashTable.Impl.fst):
- Added lemma_seq_upd_identity with SMTPat: proves that writing back the
same value at an index is a no-op (Seq.upd s i (Seq.index s i) == s)
- This eliminates the fragile hash_insert while-loop query that previously
failed on first attempt (5.0/5 rlimit) and relied on automatic splitting
- After the fix: query succeeds directly with 2.5/5 rlimit (50% utilization)
All 8 F* files verify, KaRaMeL extraction succeeds, all 7 C tests pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…t_vc Match the same options used in RabinKarp.Spec.fst for the rabin_karp_matches_no_false_negatives proof. The --split_queries always combined with --ext no:optimize_let_vc and rlimit 400 allows Z3 to verify the recursive call precondition. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add prims_compat.c/h shim bridging F*2's Prims_op_Star to krmllib's Prims_op_Multiply for integer multiplication - Update Makefile: add prims_compat.c to EXTRA_C_SOURCES and -add-include for prims_compat.h to suppress implicit declaration warning - Add ImplTest.md documenting all 6 passing concrete execution tests: Binary Search (3), Matrix Multiply (1), Kadane Max Subarray (2) All F* verification and C extraction/test targets pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Split the monolithic relax_round_pred_ok (which used 85/120 rlimit, ~46s) into three smaller lemmas: - relax_round_pred_consistent: proves pred_consistent preservation (rlimit 20) - relax_round_pred_visited: proves predecessors remain visited (rlimit 15) - relax_round_pred_ok: trivial composition of the above (rlimit 10) Also bump dijkstra function rlimit from 20 to 30 for adequate margin on a pre-existing borderline query (was 16.8/20, now ~19/30). Max rlimit usage across ch24 reduced from 85 to ~19. No admits, no assumes, all proofs complete. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add helper lemmas to decompose the invariant preservation proof into small, focused steps that Z3 can handle at low rlimit: - step_bridge_bit0/bit1: Bridge lemmas that take concrete values matching the Pulse computation, avoiding expensive Z3 let-binding matching against step_result_lemma's nested let-bound conclusion. - inv_preservation_k_pos: Proves mask/2 = pow2(k-1) and connects d_new to the invariant formula for the new mask when k > 0. - inv_preservation_terminal: Proves d_new = mod_exp_spec when mask = pow2(0) = 1 (terminal case). - pow2_gt_one_implies_pos: Establishes k > 0 when pow2(k) > 1, needed for the kv-1 nat typing in Pulse. In the loop body, explicit assert(pure(...)) statements spell out each invariant clause individually (bit parity, mask equality, d value, bounds), so Z3 doesn't need to decompose the lemma postconditions while simultaneously proving invariant preservation. Before: max query 34s, used rlimit 32.8/40 After: max query 534ms, used rlimit 1.5/10 (with --z3refresh) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add -include ch32_shims.h to CC_EXTRA_FLAGS so the shim is picked up during compilation of extracted C code. - Add Prims_op_Star -> Prims_op_Multiply define in ch32_shims.h to bridge F* nightly's new op_Star name with krmllib's op_Multiply. - Add ImplTest.md documenting concrete execution results: all 3 algorithms (Naive, KMP, Rabin-Karp) extract to C, compile, and pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Impl.fst: reduce z3rlimit from 40 to 25 (max used: 21.3) - ImplTest.fst: reduce z3rlimit from 160 to 15 (max used: 8.2) - Spec.fst: add boundary lemmas for fw_inner_j/i/outer base cases (useful for future proof optimization) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ries warning DFS.Impl.fst: The dfs_visit function previously needed --z3rlimit 400 with --fuel 2. Reducing fuel to 1 prevents Z3 from redundantly unfolding recursive definitions (the needed facts are already provided by explicit lemma calls in the loop body), cutting the worst query from rlimit 98.9 to 43.4. The new setting is --z3rlimit 60 --fuel 1 --ifuel 1. Verified robust with --z3refresh (worst query uses rlimit 43.4/60). TopologicalSort.Impl.Defs.fst: Add explicit --split_queries always around pn_combined_step to suppress Warning 349 (implicit split_queries). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Restructure perm_count_blocks and final_perm to avoid QI explosion from nested quantifiers by: - Making blocks_filled opaque to hide the nested forall from Z3 - Using targeted reveal/extraction helpers - Factoring count_out_of_range into a small helper Key improvements (used rlimit): - perm_count_blocks: 320 → 5.6 (57x reduction) - final_perm: 128 → <2 - phase4_b_step: option 100→30 (uses 20.9) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
PSS.Lemmas.fst: Factor sorted_permutation_equal into a higher-order inductive helper that takes the recursive call as a parameter. This separates the expensive quantifier VC (is_sorted + is_permutation + count_occ at fuel 2) from the recursive skeleton (fuel 0). Reduces rlimit from 20 (used 11.6) to 5 (used 4.2). QS.Lemmas.fst: Reduce count_range_eq from rlimit 10 to 5, perm_unchanged_lower/upper_bound from rlimit 15 to 5 with split_queries. Add Seq.lemma_index_slice to upper_bound for explicit slice-index connection. QS.Impl.fst: Add reveal_perm helper to isolate reveal_opaque from the caller's Z3 context. Reduce perm_lower/upper_bound_forall from rlimit 15 to 5. Replace direct reveal_opaque calls with reveal_perm. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- MatrixChain.Impl: reduce rlimit 20 → 10 by adding lemma_mul_fits helper and reordering index bound lemma calls before SizeT multiplications (max used rlimit: 7.049 → 6.212) - RodCutting.Impl: reduce max used rlimit 9.607 → 4.321 by lowering fuel 2→1, adding accum_max_step explicit unfolding lemma, and #restart-solver (eliminates dp_correct quantifier cascade) - RodCutting.Extended: reduce rlimit 40 → 10 (max used was < 2.4) - RodCutting.Spec: add accum_max_step one-step unfolding lemma for fuel-free proofs All files verify with no admits, no assumes, max rlimit ≤ 10. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adapt proofs to work with the latest F* nightly which has regressions in Z3's handling of arithmetic in quantifier-heavy contexts. Key changes: - maybe_discover_then_proof: reduce rlimit from 1200 to 80 by adding helper lemmas (lemma_queue_prefix_upd, lemma_seq_upd_preserves_nonzero, lemma_count_sum_arith) that isolate simple facts from the quantified context so Z3 doesn't get overwhelmed - bfs_explore_neighbors: bump rlimit 10 -> 20 - bfs_residual: bump rlimit 40 -> 80, add #restart-solver to avoid Z3 context pollution from earlier functions No admits, no assumes, no spec changes. Max rlimit is 80. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- make_min_siblings (Complete.fst): 300 -> 100 via single/double swap helpers - greedy_exchange (Spec.fst): 100 -> 50 via single/double swap helpers - replace_siblings_changes_count (Complete.fst): 80 -> 10 - merge_bundle_step_aux (PQForest.fst): 80 -> 60 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Documents extraction pipeline and test outcomes: - Activity Selection: PASS (count=2, sel=[0,2]) - Huffman Tree: PASS (cost=8, WPL-optimal, input preserved) - Huffman Codec: verified but not extracted (htree not C-representable) All 30 modules verify without admits or assumes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Major reductions: - phase4_content_step_order: 200 → 20 (extracted order_step_for_v helper) - order_step_for_v: new top-level helper at 160 (isolated from orchestrator) - phase4_content_step_multiset: 160 → 80 - phase4_final_sorted_on_digit: 120 → 15 - phase4_final_perm: 200 → 10 - phase4_content_inv_init: 100 → 5 - phase4_pos_bounds: 80 → 20 - content_step_key_multiset: 80 → 15 - stability_witness: 80 → 5 - digit_count_phase_step: 60 → 30 - write_pos_outside_smaller: 60 → 15 - write_pos_outside_larger: 60 → 10 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
RadixSort.Spec.fst: - lemma_stable_sort_preserves_order: 200 → 5 - get_lower_ordering: 100 → 10 - find_input_witnesses: 100 → 5 - All other 50 → 5 RadixSort.Stability.fst: - lemma_stable_pass_preserves_ordering: 200 → 120 - stable_preserves_lower_order_pair: 80 → 5 - sorted_on_to_up_to_inductive: 50 → 5 - extend_exists_case: 50 → 10 RadixSort.MultiDigit.fst: - All rlimit 100 → 5 - All rlimit 80 → 10-20 - All rlimit 60 → 5 - All rlimit 50 → 20 CountingSort.Lemmas.fst: - phase2_pos_bound: 100 → 30 - phase2_step: 100 → 30 - count_le_length_le: 50 → 30 - final_perm: 50 → 30 - write_extend_sorted: 40 → 5 BucketSort.Lemmas.fst: - bucket_sort: 100 → 40 - concat_sorted_ordered: 60 → 5 - sum_filter_lengths_cons: 40 → 10 - create_all_buckets_perm: 40 → 5 CountingSort.StableLemmas.fst: - All rlimit 50 → 10 (post previous commit) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Impl.fst: Reduce heapsort z3rlimit from 80 to 70 by adding swap_length hint to the extract-max loop body (max query rlimit dropped from 67 to 59) - Lemmas.fst: Fix flaky extract_extends_sorted_upto by adding --z3rlimit 10 (query 38 needs >5 with --split_queries always) - Lemmas.fst: Fix Warning 349 in perm_prefix_bounded_aux_upto by adding --split_queries always - Lemmas.fst/fsti: Add swap_unchanged_above helper lemma - Lemmas.fst/fsti: Add extract_step_lemma combining per-iteration proof work (available for future optimization) All files verified cleanly with --z3refresh (no flaky proofs). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- DigitSortLemmas: phase4_c_inv_init 50→5, phase4_c_step 60→10 - FullSort: all rlimit 50→5 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fix verification failures caused by the nightly upgrade: - connected_implies_vbw_positive: restart solver, use fuel 0 with explicit intermediate assertions to avoid quantifier cascade from 13 forall preconditions at fuel 2. - kruskal_spanning_step_count: restart solver, use fuel 0 (same cascade issue with high-fuel quantifier instantiation). - ImplTest: bump options to fuel 4 + rlimit 800 + z3refresh + no:optimize_let_vc. Higher fuel needed to unfold weighted_edges_from_arrays for the runtime-to-ghost bridge proof. z3refresh avoids a Z3 4.13.3 assertion violation in accumulated solver state. No admits or assumes added. No spec changes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The install-fstar script expects just the date (e.g., 2026-04-29) for --nightly --version, not the full tag (nightly-2026-04-29). Passing the full tag caused the script to construct 'nightly-nightly-2026-04-29', downloading a non-existent asset. Also fix unbound variable $tag → $branch in install_pulse_mk info message. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.