Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
9f96940
Ignore `dstep` to prove `addsnake` termination
ninioArtillero May 6, 2026
a0f181c
Refactor/optimize `dstep` by removing out-of-bound nodes
ninioArtillero May 6, 2026
c6c5a2e
Prove `dstep` reduces distance to goal
ninioArtillero May 6, 2026
9913704
Refactor `ses` to use wave-front wise search for the endpoint.
ninioArtillero May 6, 2026
5eda54d
`ses` termination proof
ninioArtillero May 6, 2026
d02c7fc
Move and reflect step functions in the top level to reduce spec
ninioArtillero Aug 3, 2026
d5ce740
Rename spec variable to match source
ninioArtillero Aug 3, 2026
1bf7759
Simplify workaround documentation
ninioArtillero Aug 3, 2026
29d584a
Reflect `_manhattanDistance` to allow PLE unfolding of `_wfDistanceTo…
ninioArtillero Aug 3, 2026
fa73761
Make explicit intermediate bound lemma
facundominguez Aug 5, 2026
1833e3a
Update documentation of lemmas and complete manual proof
ninioArtillero Aug 5, 2026
4da7122
Remove unnecessary metric related specs
ninioArtillero Aug 5, 2026
d6c363f
Remove unnecessary empty list equations from `getDiffBy` (revert #28)
ninioArtillero Aug 5, 2026
dcbab9b
Refactor `manhattanDistance` to take a `DL` argument
ninioArtillero Aug 5, 2026
34f28ed
Refine `_wfDistanceLowerBoundK` lemma documentation
ninioArtillero Aug 5, 2026
bad07b2
Add a benchmark with a larger size difference between the inputs
facundominguez Jul 9, 2026
cf592e0
Drop `withProof` in favor of `const` for lemmas
ninioArtillero Aug 6, 2026
ba57dff
Improve documentation related to `_wfDiags` invariant
ninioArtillero Aug 6, 2026
e7d2434
Prove `findEndpoint` (WIP)
ninioArtillero Aug 6, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions bench/bench.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,10 @@ doBenchMarks seed =
let rbools = randoms (mkStdGen seed) :: [Bool]
(s1000_1, rbools1) = splitAt 1000 rbools
(s1000_2, rbools2) = splitAt 1000 rbools1
in s1000_1 `deepseq` s1000_2 `deepseq` defaultMain [
bgroup "diff bool lists" $ [bench "1000 bools" $ nf (getDiff s1000_1) s1000_2]
]

s500_2 = take 500 s1000_2
in s1000_1 `deepseq` s1000_2 `deepseq` defaultMain
[ bgroup "diff bool lists"
[ bench "1000 bools" $ nf (getDiff s1000_1) s1000_2
, bench "1000/500 bools" $ nf (getDiff s1000_1) s500_2
]
]
Loading
Loading