aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
3 daysAdd semi-blank Fenwick proof files if people/LLMs want to try writing it them...HEADmasterAnthony Wang
2025-05-07Fix slow verification with z3 4.13Anthony Wang
2025-04-28Slight tweak for range_query proof (unfortunately labels @ syntax doesn't wor...Anthony Wang
2025-04-28Turn on tty echo at end of programAnthony Wang
2025-04-27Also mention Android supportAnthony Wang
2025-04-27Add Haiku support (kinda)Anthony Wang
2025-04-19Add simple benchmark code, compile to a Go library too since it's faster than...Anthony Wang
2025-04-19Revert "Seems like {:isolate_assertions} is no longer needed for update?"•••This reverts commit 214cf0a903690e14d7692a14c10aa3acef9adb0c. Anthony Wang
2025-04-12GCC is available in the Nix stdenv by defaultAnthony Wang
2025-04-10Rebuild Python library tooAnthony Wang
2025-04-10Add nixfmt-tree formatterAnthony Wang
2025-04-10Add Nix flake instructionsAnthony Wang
2025-04-10Add Nix flakeAnthony Wang
2025-04-10Seems like {:isolate_assertions} is no longer needed for update?Anthony Wang
2025-04-10Prove time complexity of update, query, and range_queryAnthony Wang
2025-03-27Link to Dafny-Rust docsAnthony Wang
2025-03-27TODO: nativeType only works for newtypeAnthony Wang
2025-03-272x perf boost by restricting lsb_fast inputsAnthony Wang
2025-03-26Add more Dafny TODOsAnthony Wang
2025-03-26Add (super slow) Dafny-generated Python library tooAnthony Wang
2025-03-266x speedup by using bitwise ops when i fits in 32 bitsAnthony Wang
2025-03-25fenwick.dfy is 1-indexed not 0-indexedAnthony Wang
2025-03-25Rebuild fenwick.rsAnthony Wang
2025-03-25Adjust loop invariantAnthony Wang
2025-03-25Simplify search proof and remove unnecessary ghost varAnthony Wang
2025-03-24More comments for searchAnthony Wang
2025-03-24Don't need to manually label where each lemma is usedAnthony Wang
2025-03-24Add more usage instructions of Dafny Fenwick libraryAnthony Wang
2025-03-24Compile fenwick.dfy into a Rust libraryAnthony Wang
2025-03-24Clean up proof some moreAnthony Wang
2025-03-24Make the binary search slightly less scuffedAnthony Wang
2025-03-24Add some more comments yayAnthony Wang
2025-03-24Very ugly proof of range_queryAnthony Wang
2025-03-24Really ugly and nasty proof of search operationAnthony Wang
2025-03-17A few more proof commentsAnthony Wang
2025-03-16Bump up lsb_correct to bv16 to match blog post, link to stuffAnthony Wang
2025-03-16Merge query invariant into one lineAnthony Wang
2025-03-16Some small style changesAnthony Wang
2025-03-15Use int instead of nat for perf reasonsAnthony Wang
2025-03-15More helpful commentsAnthony Wang
2025-03-15Delete unused code, add more helpful commentsAnthony Wang
2025-03-15Should be correct but slowAnthony Wang
2025-03-15Yay it almost worksAnthony Wang
2025-03-14This stuff doesn't work so gonna try a different approachAnthony Wang
2025-03-14Yeah something's fishy about this proof, weirdAnthony Wang
2025-03-14weird (wrong?) proof???Anthony Wang
2025-03-14wait wtfffffffffffffffffAnthony Wang
2025-03-14Clean up Fenwick proofAnthony Wang
2025-03-14YaaYYAYAYAYYAY it worksAnthony Wang
2025-03-14Almost done!Anthony Wang
generated by cgit v1.2.3 (git 2.49.0) at 2025-06-02 13:03:26 +0000