Thread by @liamzebedee

Haha so I've actually written another note on STARK's (for mere mortals).

Basically I wanted to figure out - how hard is it to implement this fantasy alien technology, recursive proofing?

To do this, I had to understand a couple of areas.

Link: hackmd.io/@liamzebedee/H…

https://twitter.com/lordOfAFew/status/1591820008061272066

What does the data structure of a STARK proof actually look like?

I went and reverse-engineered/read the code of a Circom verifier and Starkware's codebase.

From this, I was able to tell I had no idea what was going on. Why is there a separate trace and constraint merkle tree, AND the FRI? So I tried to research how STARK's are actually generated, to understand the domain.

How are STARK proofs actually generated?

There's this amazing guide here which this is directly lifted from (I mention this clearly in the notes)
aszepieniec.github.io/stark-anatomy/…

Super great read, especially around the "interpolation" step.

So now I understood the context of some additional concepts - the trace polynomial, the AIR constraints - I began to write them out.

The trace -> arithmetic equations -> interpolated into some polynomials -> combined into a single compositional polynomial

Still I didn't understand why trace/constraints/FRI were all separate data fields - I thought using a STARK was just validating one equation?

So the next logical place to look - ZK-STARK’s - how are they _actually_ verified?

This made a lot more sense - the computation is expressed as both the trace (registers) and the constraints (program counter++). Both are polynomials which we read from, and combine into a single poly, which we verify the low-degreeness of.

A good lot of this knowledge is directly picked from the Winterfell verifier documentation (incode), which I knew was good from working on Giza with Max. The rest came from the original ethSTARK spec for the EF.

It's awesome to finally understand how the verification works, because it's really quite simple in the end (7 steps, mostly computation).

There were a couple new concepts I had to learn - the composition polynomial, the random linear combination

Still no idea what LDE was!

I shot this doc to a mate, who I was already asking how hard it would be to implement verification. He comes back with a question I hadn't even thought of --

"the most difficult thing for me to understand about STARKS is why the FRI protocol converging implies the initial claim"

Basically - how can proving low-degreeness be related to proving the satisfiability of the polynomial?

Well that, we worked out today ;)

Basically - it's a mix of a foundational theorem in polynomial interpolation, which relates degree/roots, and a method to blow up the computational space to make it secure for some n. bits parameter (which is LDE!)

https://twitter.com/liamzebedee/status/1591785700327919617

Experimenting with different ways of sharing + communicating. Last thread on STARK's was an actual realtime thread as I drank 50 coffees and just dived-deep into the whitepaper. This one was more post-hoc. Probably not as riveting to write the story retroactively, but hey! lfg