Notes
Written word.
Formally Verifying Jolt Bytecode Expansions
Money For Nothing Monads For Free
Proof Complexity Notes
Working notes on proof complexity (potentially incomplete and/or wrong)
Compiling RISCV-SAIL Into Lean4 Cpuu
Notes from getting local transpilation working from source.
Lost in Translation
Sumchecks Bloody Sumchecks
Anatomy Of A Jolt Sumcheck
Small Scalar Binding
Tracked Types
Algorithms For Montgomery Multiplication
Montgomery Multiplication: Theory Vs Practice
-
-
-
Proof Complexity Notes
Working notes on proof complexity (potentially incomplete and/or wrong)
-
Compiling RISCV-SAIL Into Lean4 Cpuu
Notes from getting local transpilation working from source.
-
-
-
-
-
-
-
- Formally Verifying Jolt Bytecode Expansions
- Money For Nothing Monads For Free
- Proof Complexity Notes
- Compiling RISCV-SAIL Into Lean4 Cpuu
- Lost in Translation
- Sumchecks Bloody Sumchecks
- Anatomy Of A Jolt Sumcheck
- Small Scalar Binding
- Tracked Types
- Algorithms For Montgomery Multiplication
- Montgomery Multiplication: Theory Vs Practice