Open
Conversation
…lock - Remove 230 lines of dead code across 3 files (16 unused definitions/lemmas identified via binary search against Z3 verification) - Fix write_buffer resize branch fold failure by adding 4 standalone Spec lemmas (contents_length, wf, prefix, coherence_transfer) and restructuring the resize write loop with bool-bound invariant for exit condition - Fix read_buffer loop body verification by adding read_step_invariant Spec lemma that bundles coherence extraction + Seq.upd reasoning - Remove --admit_smt_queries true block: full module now verifies with zero errors and zero admits (only platform_fits_u64 assume remains) Spec.fst: +5 lemmas (write_buffer_resize_*, read_step_invariant) Modular.fst: -41 lines (removed upd_at_different_index, wrap_decomposes) CircularBuffer.fst: -admit block, +lemma calls, restructured resize loop
- S2: Remove write_buffer_resize_contents_length (subsumed by write_buffer_resize_wf) - S3: Collapse gapless_preserved_by_resize from forall_intro+aux to () - S4: Collapse phys_log_coherent_seq_equal from forall_intro+aux to () - S6: Collapse lemma_resize_invariant_step: merge j<vi and j>vi branches - S7: Simplify read_step_invariant: remove redundant else branch structure - Simplify write_buffer_resize_prefix aux body All modules fully verified, 0 admits. Top-level specs unchanged. Spec.fst: 545 -> 516 lines (-29) CircularBuffer.fst: 756 -> 753 lines (-3) Total: -32 lines
Replace 3 predicate modes (is_circular_buffer, is_circular_buffer_ooo, is_circular_buffer_rm) with a single unified is_circular_buffer that always uses RangeMap-based gap tracking, modeled after msquic's recv_buffer.c design. Key changes: - Single is_circular_buffer cb rm st predicate (always RM-tracked) - create returns (circular_buffer & RM.range_map_t) - write_buffer uses absolute stream offsets with auto-resize - read_buffer works with RM predicate (copy-based) - read_zerocopy returns segment pointers with trade-based borrow - drain leaves RangeMap unchanged (absolute offset advantage) - Removed gapless predicate and all sequential-only code - Removed enter_ooo/enter_rm/exit_rm_to_ooo transitions - Added ranges_match_create_nones lemma for create verification Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Thin wrapper (no .fsti) that re-exports all CircularBuffer public functions. Required because modules with .fsti produce private krml symbols that KaRaMeL drops during reachability analysis. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When a Pulse module with .fsti defines a polymorphic type with an erased
parameter, krml's monomorphizer creates two incompatible C struct types:
node__range_() = { key, left, right } (from caller, () erased)
node__range_any = { key, value, left, right } (from impl, any erased)
The checker rejects the subtype check and silently drops 5 RangeMap
functions from the C output.
Run: ./extraction/repro_krml_bundle_bug.sh
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace multi-module reproducer with a single Pulse file that triggers the monomorphization type mismatch: AVLTree erased value param v is monomorphized as () in the caller but any in the implementation, creating incompatible C structs (3 vs 4 fields). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Drop-in replacement for AVL-based RangeMap with better cache locality and clean KaRaMeL extraction. Uses sorted Pulse.Lib.Vector of ranges with linear scan insert and automatic merge of overlapping intervals. Verified API surface: - range_vec_create / range_vec_free - range_vec_contiguous_from / range_vec_max_endpoint - range_vec_add (body with admits, proofs TODO) Spec bridge reuses Pulse.Lib.RangeMap.Spec unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Drop-in replacement: same API signatures, same spec bridge via Pulse.Lib.RangeMap.Spec. All verification conditions still pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Prevents KaRaMeL from trying to extract spec-only functions
(seq_all_valid, seq_to_spec, etc.) that use FStar.Seq which
has no C implementation.
KaRaMeL extraction now succeeds:
- All 7 public functions extracted to clean C
- range struct maps to { size_t start; size_t len; }
- No monomorphization bug (no .fsti = no erased type issue)
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Both helper functions now have verified implementations instead of admit(). Uses mutable boolean flag pattern for while loops to avoid Pulse's 'Cannot check relation with uvars' error with invariant b. vec_insert_at: push_back + shift-right loop + set at insertion point vec_remove_range: shift-left loop + pop_back loop Remaining admits only in range_vec_add spec bridge proofs. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Standalone benchmark for the extracted vector-based range tracker. Performance comparison with old AVL-based CB (full operations): - Old OOO writes (CB+AVL rangemap): ~500K ops/s - New range tracking only (vector): 170M-970M ops/s Sequential add: 554M-972M add/s OOO add: 170M-244M add/s Gap-fill add: 898M-967M add/s Queries: 784M-998M query/s Also updates RecvBufferWrapper.fst to use RangeVec and includes fresh KaRaMeL C extraction of RangeVec. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add capacity invariant to is_range_vec predicate (enables push_back without separate capacity precondition tracking) - Add add_range_all_before and add_range_insert_no_overlap lemmas to Spec.fst for bridging imperative add to recursive spec - Add seq_insert/seq_remove pure helper functions - Fix KaRaMeL extraction: use -library Pulse.Lib.Vector to avoid stack-allocated VLA bug in Vector extraction - Provide proper heap-allocated Vector stubs in krmlinit_rv.c - Reduce admits from 6 to 4 (removed capacity-related admits) Benchmark results (1000 iterations): Sequential add: 10-37M ops/s OOO add: 10-22M ops/s Queries: 347M ops/s Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add seq_to_spec bridge lemmas: snoc, append, slice, insert - Add forall_high_below_to_spec to lift range-level facts to spec - Strengthen search loop invariant with forall k<iv. high(s[k]) < offset - Make seq_insert/seq_remove total functions (avoid Pulse postcondition refinement issues) - Strengthen vec_insert_at postcondition to track content (s' == seq_insert s i r) - Add add_range_skip_prefix lemma to Spec.fst for merge-case decomposition - Fill admits 1 & 2 (insert cases) using add_range_all_before and add_range_insert_no_overlap - Remaining admits: 2 in vec_insert_at (content tracking), 2 capacity, 2 merge case Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Strengthen merge loop invariant: mh > merged_low (strict) - Remove bounds admit: SZ.sub final_high merged_low now provable - Restructure merge case: single admit covers set+remove+spec bridge - 5 remaining admits: 2 vec_insert_at content, 2 capacity, 1 merge spec Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Spec.fst: - Add range_map_wf_sorted: transitive sortedness from wf - Add merge_absorbed_high: compute final merged endpoint - Add add_range_merge_step: unfold add_range merge branch - Add add_range_merge_scan: inductive merge characterization (when first k elements overlap, result is merged + suffix) RangeVec.fst: - Strengthen merge loop invariant to track overlap forall and exit condition (jv==n or mh < s[jv].start) - Add forall_overlap_to_spec bridge lemma Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Split add_range_merge_full into add_range_merge_suffix (inner chain: merge_step + merge_scan) and add_range_merge_full (skip_prefix + merge_suffix). This avoids Prims.subtype_of quantifier cascade that caused Z3 timeout at rlimit 200. Now verifies at rlimit 40 with split_queries always. Also adds range_map_wf_slice lemma (wf preserved through suffix slice). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add merge_loop_body_step bridge lemma (packages mah tracking + mh0 coverage) - Add exit_condition_to_spec bridge (lifts range-level exit to spec-level) - Add add_range_merge_full_explicit to Spec.fst (explicit mh0 for easier SMT matching) - Add merge_absorbed_high helpers: unfold_right, eq_max_last, mh0_covers_absorbed - Prove merge loop body verifies (was Error 19 at loop body) - Fill no-remove merge case admit (seq_upd_remove_spec + range_to_interval match) - Remaining admits: vec_insert_at content (2), vec_remove_range content (1), capacity invariants (2), remove-path merge (1, blocked on vec_remove_range) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add shift_set_is_seq_insert bridge lemma for shift-right + V.set - Strengthen shift-right loop invariant with prefix/shifted/exit tracking - Call bridge lemma BEFORE V.set (avoids complex Seq.upd expression in Pulse) - Prove else branch: snoc_is_seq_insert with explicit bounds assertions - Both branches of vec_insert_at now fully proved (no admits) - 3 remaining admits are all Class B capacity invariants (L746, L764, L864) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add size_bounded ghost fn to Vector (exports |s| <= cap from is_vector)
- Strengthen push_back postcondition: cap' ∈ {cap, 2*cap}
- Strengthen pop_back postcondition: capacity condition preserved
- Prove insert_capacity_condition bridge lemma (one admit for cap≥2^63)
- Prove all capacity admits in range_vec_add:
- L746 (append-at-end): via vec_insert_at capacity postcondition
- L764 (insert-no-overlap): via vec_insert_at capacity postcondition
- L864 (merge-remove): via vec_remove_range capacity postcondition
- Only remaining admit: edge case in insert_capacity_condition
requiring cap ≥ 2^63 (physically unreachable)
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the physically-unreachable admit() in insert_capacity_condition with a complete proof using: - assume val platform_is_64bit: 64-bit platform (SZ.fits_u64) - assume val max_range_vec_entries: entry count bound (≤ pow2 62) - SZ.fits_u64_implies_fits: derives SZ.fits(cap+cap) from cap < pow2 63 The proof: when cap = sz+1 ≤ max_range_vec_entries ≤ pow2 62, cap+cap ≤ 2·pow2_62 = pow2_63 < pow2_64, so SZ.fits(cap+cap). RangeVec.fst now has zero admits. The two assume vals are standard platform/physical constraints (64-bit, bounded entry count). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Change max_range_vec_entries from pow2_62 to pow2_62 + 1 (needed for strict inequality: n separated intervals <= pow2_62 < pow2_62 + 1) - Add drain_ranges_length: drain never increases interval count - Add wf_count_bound: n separated intervals span 2n-1 offsets minimum (inductive proof using gap >= 1 and count >= 1) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- RangeMap.Spec: drain_repr function + 5 lemmas (wf, bounded, length, mem_above, add_range_length) - CB.Spec: ranges_match_drain_repr bridge, drain_repr_preserves_rwp, repr_count_bound_gap for bounding interval count after writes - RangeVec: range_vec_drain implementation (remove or trim first entry), seq_to_spec_tail and seq_to_spec_upd0 bridge lemmas - CB.fst: Added Seq.length repr < max_range_vec_entries to is_circular_buffer Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Drain now calls range_vec_drain to remove/trim consumed intervals, keeping repr bounded and first.low >= bo invariant - All 3 write fold sites prove |repr'| < max via: add_range_first_low (first.low >= bo preserved) + repr_count_bound_gap (2*n <= al + 1) + al <= pow2_63 → n <= pow2_62 < pow2_62 + 1 = max - Added first.low >= bo conjunct to is_circular_buffer predicate - Fixed max_range_vec_entries to n == pow2 62 + 1 (exact bound needed) - RangeMap.Spec: added add_range_first_low inductive lemma 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.
A circular buffer that wraps around, and doubles in size when appending more than N elements.