Mastodawn

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.

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."

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 🤣

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.

Mar 13

Fenwick trees are dangerously fast, I propose we start researching A[i] xrisk

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)

Mar 16

HOW HARD COULD IT BE? 1000 lines and 15 hours of work later, now I know

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

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

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

Mar 24

Cleaned it up and will blog about it tonight 😃

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

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

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?

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]

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

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.

Someone needs to make a crossover of the Lean Natural Number Game and Touhou

Help I really succ at this game... *intense peano music intensifies*

Apr 22

I hope someday they make a set-theoretic sequel to Piano Tiles called Peano Tiles

written in Lean ofc

I bet a week later after learning more Lean I'm gonna come back and make a version with the roles swapped

Wait TIL the same guy created both Z3 and Lean, and Dafny is just "throw everything into Z3 and hope for the best" so maybe it's not Lean VS Dafny it's Lean ❤️ Dafny

Not only does Lean feel like the Rust of proof assistants, it literally *is* Rust: a Lean dev said "Our inofficial fallback design heuristic is "if we don't know what to do, do it like Rust"." and elan is the same code as rustup just with 's/rustup/elan/g' 's/cargo/lake/g' 's/rustc/lean/g'

I hope this makes the Rust fans try Lean

I should make some fan sites sometime:
- btrfs fan site where the entire site is just a btrfs send-ed file that you can btrfs receive
- Dafny fan site with a large gallery of proofs of false
- Lean fan site with an animified version of the natural number game
- Ali's fan site wait no that already exists that's just my current website

May 6

Alright I made the https://lean.unnamed.website/ and https://btrfs.unnamed.website/ fan sites

May 6

Honestly I'm starting to prefer the live interactivity of Lean over Jupyter notebooks (no hidden state!) (but Pluto.jl of course will forever still be my favorite)

May 6

I just realized I've been learning Lean for a few weeks now and I've just never compiled any of my programs since if you know the program is provably correct why would you ever run it? (Yeah I know I've made that joke a million times but it's kinda true)

Anyways I'm running `lake build` for the first time and it's compiling hundreds of mathlib stuff weeeeeeee

May 8

I just tried unsafe Lean (analogous to unsafe Rust) and welp that crashed the Lean server several times