Notes

Written word.

Formally Verifying Jolt Bytecode Expansions

Ari

Money For Nothing Monads For Free

Ari

Proof Complexity Notes

Working notes on proof complexity (potentially incomplete and/or wrong)

Ari

Compiling RISCV-SAIL Into Lean4 Cpuu

Notes from getting local transpilation working from source.

Ari
joltcompilers

Lost in Translation

Ari

Sumchecks Bloody Sumchecks

Ari
sumcheckjoltpythontooling

Anatomy Of A Jolt Sumcheck

Ari
sumcheckstreamingjolt

Small Scalar Binding

Ari
sumcheckmontgomery-mults

Tracked Types

Ari
sumcheckmontgomery-mults

Algorithms For Montgomery Multiplication

Ari
joltalgebramontgomery-multiplication

Montgomery Multiplication: Theory Vs Practice

Ari, Squirrel
instrumentationjolt