search

Orbis-Tertius / Orbis

A general-purpose layer 2 zk-rollup scaling solution for Cardano
Apache License 2.0
21 stars 1 forks source link

Write a Rust circuit code generator #83

Open morganthomas opened 2 years ago

morganthomas commented 2 years ago

Write a program which takes a Halo 2 circuit represented as a Coq value and outputs Rust code for building and interacting with that circuit.

morganthomas commented 2 years ago

Use Coq extraction to build a circuit as a Haskell value, then write codegen in Haskell?

Coq extraction to Rust? https://github.com/pirapira/coq2rust (This is very old. Would not work with recent versions of Rust.)