Hello everyone – it’s nice to meet you. My name is Jan Gorzny and I am a researcher at Quantstamp. I am delighted to share with you that our application in the title, “Improved Lightweight Formal Verification of Halo2 Proof Systems” was accepted for a Zcash minor grant!
I will be leading this effort at Quantstamp, and in the coming days we will ramp up our contributions to this grant. We’ll staff the project and allocate time, and look at the first deliverables in the grant. The work is a continuation of work that we had accepted to the SMT 2023 conference earlier this year, and we are excited to be able to enhance the tool with this grant. The work will likely be merged into this repository.
If you have any questions or comments, please don’t hesitate to ask. Looking forward to providing you with more substantial updates as the work progresses.
10 Likes
As I am a new user, I could only add two links to the post initially. So here is the paper paper accepted to SMT 2023, in case anyone is interested.
5 Likes
this is cool i guess. wish u luck to improve security and remove possibility for bugs.
Hey everyone,
Just wanted to share a quick update. Jan has been incredibly busy with other commitments in the last few months, leading to a quieter period here. With that context, I’ll be stepping in to lead our efforts moving forward and giving updates about our progress.
Despite the silence, our project hasn’t been standing still. We’ve made significant progress focusing on the architecture and optimization of the project.
I’m sharing this document on our progress so far and what we’re planning to do in the next steps.
I’m here for any questions or thoughts you might want to share. Your continued support is crucial as we take these next steps together. Stay tuned for updates and developments coming your way soon.
Best,
2 Likes
I’m not specifically interested in exactly what those code bits say in those images, but they are very blurry.
2 Likes
Thanks, I removed the unnecessary rust-specific code. I’m trying to show an abstraction of data flow from the circuit to the analyzer.
2 Likes
That isn’t to say that I didn’t like the code in there, I was just saying the images were blurry. I just didn’t want it to come off like accusatory, perhaps.
sry and thank you
2 Likes
It was fair 
The code was not clear
2 Likes
Hey everyone,
This month, we’ve made substantial progress in enhancing the efficiency of our circuit analysis tool, particularly concerning how we manage lookup tables, which are one of the most extensive parts analyzed in SMT solver.
Our initial approach involves analyzing circuits with all lookup constraints fully applied. This method ensures thorough analysis with no false positives but is also very extensive. We keep this original approach serving as a baseline benchmark.
The two new approaches introduced for handling lookups are:
Efficient Range Checks via functions:
To improve efficiency, we’ve refined our methodology to include functions that perform range checks for lookup entries. This approach not only reduces computational overhead but also opens doors for more sophisticated pre-processing techniques that can further enhance analysis efficiency.
Abstracted Lookups:
We have also explored simplifying lookups during the initial analysis phase by treating them abstractly. This method allows for quick identification of potential under-constrained areas, which are then rigorously verified in detailed post-processing to ensure accuracy.
Further Optimizations:
Optimizing Lookup Table Processing:
Conceptually, lookup tables function by identifying specific tuples, and treating these tuples as sets where the order and repetition are irrelevant. Originally, our system processed these tables as-is, including duplicates, which could lead to inefficiencies. We’ve now optimized this by removing duplicate rows from lookup tables before integrating them into the SMT solver, thereby streamlining the verification process and reducing unnecessary computations.
Matching Equivalent Lookups:
A new method has been introduced to detect equivalent lookup tables within the circuit analysis process. By recognizing and reusing identical tables, this approach helps reduce redundancy in the solver’s operations. It ensures that tables sharing identical data sets—irrespective of their order or frequency—are not unnecessarily duplicated, further minimizing the set of SMT constraints required.
These updates are part of our ongoing efforts to enhance both the speed and accuracy of our tool, ensuring it remains well-equipped to handle complex circuit analyses efficiently. We value the community’s input as we continue to refine our methodologies.
2 Likes