feat: add 12 CS algorithm implementations with correctness proofs#383
Open
brando90 wants to merge 12 commits intoleanprover:mainfrom
Open
feat: add 12 CS algorithm implementations with correctness proofs#383brando90 wants to merge 12 commits intoleanprover:mainfrom
brando90 wants to merge 12 commits intoleanprover:mainfrom
Conversation
…eteness proofs Add depth-first search on directed adjacency-list graphs with: - `dfsAux`/`dfs` implementation with fuel-based termination - `Reachable` inductive predicate for graph reachability - `dfs_soundness`: dfs returns true → target is reachable - `ReachableAvoiding` + `dfsAux_complete_avoiding`: completeness for simple paths - Unit tests on small graphs verified via `decide` Adapted from the VeriBench benchmark. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add breadth-first search on directed adjacency-list graphs with: - `bfsAux`/`bfs` returning shortest distance as `Option Nat` - `IsPath` inductive predicate for directed walks with path list - `IsPath.trans`/`IsPath.snoc` for path composition - `bfs_soundness`: BFS returns `some d` → a path of length `d` exists - Queue invariant `QueueInv` tracking path witnesses through BFS loop - Unit tests verified via `decide` Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- `binarySearchAux`/`binarySearch` with fuel-based termination - `binarySearch_found`: returned index points to target element - `binarySearch_bounds`: returned index is within array bounds - Unit tests verified via `decide` Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…oofs Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Proves sorted output, permutation preservation, and length preservation via extractMin properties (minimum bound, permutation, length decrease). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Proves sorted output, permutation preservation, and length preservation via partition properties (element bounds, permutation, length). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Proves sorted output, permutation preservation (via count equality), and length preservation using buildSorted and findMax properties. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Proves sublist of both inputs, length bounds, and self-LCS identity via fuel-based induction on the LCS computation. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Proves reflexivity (self-distance is 0), empty list properties, and upper bound (distance ≤ sum of lengths) via fuel-based induction. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…oofs Implements fuel-based Dijkstra's algorithm on weighted adjacency-list graphs. Includes extractMin, dijkstraAux, dijkstra, IsWeightedPath inductive definition, weighted_path_refl, and dijkstra_start_self theorem. All proofs complete (no sorry). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Implements fuel-based heap sort on lists of natural numbers with findLargest, heapify, buildMaxHeap, and heapSortAux. Proves swap_perm via count_set, heapSort_perm and heapSort_length. All proofs complete (no sorry). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
brando90
changed the title
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.
Summary
Adds 12 formally verified CS algorithm implementations ported from the VeriBench benchmark to CSLiB format. All proofs are complete (zero
sorry), all tests usedecide(notnative_decide). All files passlake build,lint-style, andmk_all.Sorting (6 files)
Graph (3 files)
Search (1 file)
Dynamic Programming (2 files)
Test plan
lake builddecidetests passlake exe lint-stylepasseslake exe mk_all --modulesucceeds🤖 Generated with Claude Code