Skip to content

Conversation

@clarus
Copy link

@clarus clarus commented Aug 13, 2025

Here, we add code to pretty-print the constraints of the circuits and compare them with the ones we obtain in our formal models in Rocq. We worked on the branch_eq and sha256 modules. For sha256, we do not cover the constraints in Encoder and the bus constraints yet, but they should work also given more time (we can pretty-print them, but the corresponding code in Rocq is not ready yet).

The commands to run the project from the root folder and pretty-print the constraints on the standard output:

cargo run --package openvm-to-rocq -- print --circuit-type branch-eq
cargo run --package openvm-to-rocq -- print --circuit-type sha256

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants