anoma / zkp-compiler-shootout Goto Github PK
View Code? Open in Web Editor NEWEvaluating & benchmarking ZKP compilation strategies.
Home Page: https://anoma.github.io/zkp-compiler-shootout/
License: GNU General Public License v3.0
Evaluating & benchmarking ZKP compilation strategies.
Home Page: https://anoma.github.io/zkp-compiler-shootout/
License: GNU General Public License v3.0
The current structure of having Sudoku
folder with the risc0
code was fine before, however I wish to scale up the repo, and have multiple similar folders per idea. Thus I propose the following folder structure
It seems like running the benchmarker takes 15 minutes on my machine. I need to reduce the number of repeat tests from 100 to 20.
Currently we are using criterion to test rust programs. This programs seems quite nice for benchmarking programs, however I should conduct a study of available benchmarking tools.
Another important consideration is how do we benchmark programs not written in rust? It would be cool if we can get a csv file out of the times, and import it into some system, which does the statistical projection for us. This way all our statistics look and feel consistent.
Currently I've added a Blake2 benchmark for risc0
, but it would be nice to get a good basis of hash functions bench marked:
Known hashing functions to benchmark and compare
It would be great to get contributions for all ZKVM machines. Ideally we can get all the machines to have the same algorithm, so we can compare speeds more easily.
I should also verify the answer somehow.
For the Blake 3: Miden
example I take it on faith value that I'm feeding the inputs correct and getting the correct output
as seen in #16, there is no easy way to jump to a label without affecting the call stack. This demands that abstractions like loop
or if
after their termination, will have to have their exit code labels be placed after the label they were called from.
(def nonsense-example
(tagbody
:nonesense-entry-point
(dup 0)
(if (begin (push 2) add)
(begin (push 3) add))
;; In real code, this is generated by if, not written in code explicitly
:after-if
(push 4)
(loop swap (push 3) add swap)
;; In real code, this is generated by loop, not written in code explicitly
:after-loop
(dup 0)
(push 100)
lt skiz recurse return))
This should generate code to look something like
nonsense-entry-point:
dup0
skiz
call if-wraper
after-if:
push 4
call loop
after-loop:
dup0
push 100
lt skiz recurse return
if-wraper: ...
loop: ....
where loop
and if-wrapper:
are filled in with their proper code. However note where after-if:
and after-loop:
come. Their ordering was set to be after whatever the current block at the time was!
This behavior is not trivial to implement, as we can not rely on all gotos
's to get the ordering naturally like a SSA style control flow graph.
In fact, due to how ordering works, we have to make sure we move down the any labels that were created before the continues-at
point to the end, as the if/loop return label may have labels that already implicitly follow it!
We therefore have to carefully remember this ordering ourselves. Thankfully I propose the following solutions:
This solution is simpler than the second solution and is more elegant, however it needs some build up.
When we say something like (loop swap (push 3) add swap)
, how we think of the control graph, is that it calls
into some loop boiler plate with the user logic inside, then it returns back to the caller.
Thus instead of thinking of concepts like loop
and if
as primitives or like a normal instruction, we can think of it like a higher order procedure!
Namely, an invocation of loop
or if
creates a brand new procedure, with the code the user specified being inside the generated procedure.
Since these blocks always call
and return
they are safe to move anywhere. This completely removes any need for reordering logic.
All that needs to happen from the code standpoint is:
labels
with a notion of created procedures that we accumulate.We change tlabels
from being just a a list of blocks, to being a record containing the following fields.
label
of a block to the block itself.:front
, :end
, or nil. For current blocks without labels, telling them where they go in the orderingWhat the 4.
point does, is when we finalize the block, we will move all nodes between the current node and what follows to the end.
Thus if we have
:a :b :c :d :e
and we say :d
follows :a
, then the ordering list will now look like
:a :d :e :b :c
This method is slow and is O(n^2)
in the number of explicit follows. However if this is found to slow down the speed of compilation, then I can implement a O(n)
method by some sort of numbering.
An important means of combination for tlables
is appending an instruction or a set of instructions to the front.
This will serve as the modified version of my existing triton:cons-instructions-to-labels
opcode
(push, call, etc.):
:front
enum
is.consing a label
consing a label
tlabels
:
tlabels
is not empty:
gensym
an unique label for the current block.tlabels
's current block as our own, along with its enum valueAlso there are two versions of Halo2, via IPA and KZG. Is it possible to plugin both backends?
Merkle Proofs are a common use case for ZKP languages. It would be great to have benchmarks comparing the speed with a Merkle inclusion proof
We can do this on a per backend basis, so we can slowly add one backend at a time.
Currently my code generator for Triton is quite primitive. I would like the following to be made
if
create new labels to continue at, it is important to be able to compose this with code that comes nextCurrently due to compiler tool chain versions, risc0 is now disabled.
I'd ideally get this working again.
Cairo is a rather neat project, we should add it to the benchmark.
However, Cairo has a few ways of operating so we should test the following provers
For the compiler I recommend using
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.