​Jan 14

I wrote a fast Fenwick tree library for my flash cards app: https://git.unnamed.website/sdc/tree/fenwick.c

The operation "Search for largest index with prefix sum less than or equal to s" isn't a common thing that people do with Fenwick trees so I had to read an arXiv paper about it.

The nice thing about Fenwick trees is that they're only a few lines of code but... on the other hand they use crazy incomprehensive bit hacks!

fenwick.c - sdc - C port of SD, a very efficient flash cards app

Show thread​Jan 14
I haven't done benchmarks to confirm this, but Fenwick trees should use 1/4 the memory of segtrees and be somewhat faster since they use for loops and bit hacks instead of recursion.
Show thread​Jan 14
The other weird thing about the "search for largest index with prefix sum less than or equal to s" operation is that it views the Fenwick array as an implicit binary tree while the update and query ops view the array as (two different) binomial trees. So maybe the tagline for Fenwick trees should be "One array. Three trees."
Show thread​Jan 14
And here's a Fenwick the squirrel who I folded 1.5 years ago. I guess his name is because he lives in a Fenwick tree or something. When I folded him last year, I told my friends there was a squirrel in my room and they thought a real squirrel was running around wrecking havok in my room 🤣
Show thread​Jan 15

Welp, somehow I gaslighted myself into thinking that squirrel's name was Fenwick. It's actually Segtree and the real Fenwick is a rabbit.

Anyways, today my friend Isaac (https://slightknack.dev) convinced me to organize my random Fenwick tree ramblings into a blog post and he also drew a nice diagram for my post! https://unnamed.website/posts/fenwick-trees-awesome/

Featuring fake calculus, insane Python programs, and one liner bit hacks!

Home — Isaac Clayton

A cozy little corner of the web.

Show thread​Mar 13
Fenwick trees are dangerously fast, I propose we start researching A[i] xrisk
Show thread​Mar 13
Hmmm maybe I should try formally verifying my Fenwick trees post using Dafny... it's only 5 lines of code, how hard could it be?? (top words said before major disasters)
Show thread​Mar 16
HOW HARD COULD IT BE? 1000 lines and 15 hours of work later, now I know
Show thread​Mar 16
New (absurdly long and insane) blog post about formally verifying Fenwick trees using Dafny, feat. Kublai the camel, Fenwick the rabbit, SHL the fox, and a proof of 0 == 1! https://unnamed.website/posts/formally-verifying-fenwick-trees/
Formally Verifying Fenwick Trees

Formally verifying the Fenwick tree data structure using Dafny and Kublai the camel

Show thread​Mar 24

I severely underestimated the difficulty of the challenge problems I posed at the end of that blog post...

What I expected:
★☆☆ <15 minutes
★★☆ <1 hour
★★★ <3 hours

In reality:
★☆☆ <1 hour
★★☆ eh it'll take an afternoon
★★★ DO NOT ATTEMPT

Show thread​Mar 24
I'm trying to challenge 5: "Implement prefix search and prove it." and I wrote a 100 line Dafny proof but it's so nasty and hacky that I don't wanna ever post that monstrosity on my blog
Show thread​Mar 24
Cleaned it up and will blog about it tonight 😃
Show thread​Mar 25
New sequel to my formally verifying Fenwick trees post, feat. Kublai, using Dafny in #Rust, and more proofs: https://unnamed.website/posts/actually-useful-formal-verification/
Doing Something Actually Useful With Formal Verification

Using my formally verified Fenwick trees library for a flash cards app in Rust

Show thread​Apr 10
Another new post in my Fenwick trees/Dafny series! This time I proved the time complexity of Fenwick trees: https://unnamed.website/posts/proving-fenwick-trees-fast/
Proving That Fenwick Trees are Fast

Using Dafny to formally verify the time complexity of Fenwick trees

Show thread​Apr 20
I have a particularly nasty Dafny proof that the reverse of the reverse of a linked list is the list itself: 158 lines of pure pain. Should I write it up as a blog post, or is it too scary?
Show thread​Apr 20

Learning Lean right now and I think Dafny seriously spoiled me since it was a struggle even to define the lsb function from my Fenwick post:

def lsb (i : Nat) : Nat :=
if i == 0 then 0 else if i % 2 == 1 then 1 else 2 * lsb (i / 2)
termination_by i
decreasing_by
cases i
· simp
contradiction
· simp_all [Nat.div_lt_self]

Show thread​Apr 20
grinding the Lean game https://adam.math.hhu.de/#/g/leanprover-community/nng4 right now, tbh it's a bit boring since I know all these things would be trivial to do in Dafny
Show thread​Apr 20

Yay finally finished in 150 minutes, other than the Fermat's Last Theorem level!

Sadly, I still have no idea how to use Lean 4.

Show thread​Apr 20
Someone needs to make a crossover of the Lean Natural Number Game and Touhou
Show thread​Apr 20
Help I really succ at this game... *intense peano music intensifies*
Show thread​Apr 22
I hope someday they make a set-theoretic sequel to Piano Tiles called Peano Tiles
Show thread​Apr 22
written in Lean ofc
Show thread​Apr 22
Show thread​Apr 23
I bet a week later after learning more Lean I'm gonna come back and make a version with the roles swapped
Show thread​Apr 24

Yay I proved my first "theorem" using Lean: the property lsb i ≤ i for the lsb function in Fenwick trees https://git.unnamed.website/leantest/tree/Main.lean?id=c86a44de06312ad58439038bec182efd2391e919#n41

But yeah it was excruciatingly hard since it was my first time without handholding from a book or guide but hopefully it'll get way easier over time.

Main.lean - leantest - Random Lean experiments

Show thread​Apr 24
I think Lean and Dafny have rotted my brain... they're the only languages I take seriously nowadays, everything else just feels weak in comparison
Show threadrdivyanshuApr 24
@xy gestures xkcd 435
Abhinav 🌏May 31
Show thread​
@rdivyanshu
May 31 at 5:01pmWeb
Show thread​May 31
@rdivyanshu I apologize in advance for my ridiculously bad handwriting