Granted: Improved Lightweight Formal Verification of Halo2 Proof Systems

Community Grants Minor Grants
1

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.

11 Likes
2

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.

6 Likes
3

this is cool i guess. wish u luck to improve security and remove possibility for bugs.

1 Like
4

Congratulations!

1 Like
5

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,

3 Likes
6

I’m not specifically interested in exactly what those code bits say in those images, but they are very blurry.

3 Likes
7

Thanks, I removed the unnecessary rust-specific code. I’m trying to show an abstraction of data flow from the circuit to the analyzer.

3 Likes
8

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.:sweat_smile: sry and thank you

3 Likes
9

It was fair :smile: The code was not clear

3 Likes
10

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.

3 Likes
11

Hey everyone,

Here’s an update on the progress we’ve made this past month on our circuit analysis tool. Our focus has been on enhancing user functionality, improving the efficiency of our analysis processes, and refining our benchmarking methodology. Here are the highlights:

Enhanced User Functionality:

We’ve introduced new command-line interface (CLI) options, allowing users to customize their analysis experience by specifying profiles, analysis types, lookup methods, verification methods, and iteration counts. These updates are aimed at providing more flexibility and control to the users.

Improved Benchmarking with Criterion Framework:

Our benchmarking process has been significantly upgraded with the integration of the Criterion framework. This new approach delivers more accurate and automated performance measurements, helping us better understand and improve our tool’s efficiency. The new benchmarks offer detailed insights through various output formats, including visual reports.

New Benchmark Scenarios:

We have added new benchmark scenarios to evaluate the performance of different methods for handling lookups. This helps us identify the most efficient techniques and refine our approach accordingly.

Functional Separation in Analysis:

We’ve refined our analysis tool to separate the creation and preprocessing phases from the main analysis phase. This separation allows us to better isolate and optimize different parts of the process, ensuring more precise performance measurements.

Reduction of False Negatives:

By incorporating fixed values into permutation cycles within our abstract interpretation framework, we’ve been able to reduce false negatives. This enhancement improves the overall accuracy and reliability of our tool.

Community Engagement:

We have also reviewed several community pull requests. It has been exciting to see the community’s engagement and contributions to the project.

These updates are part of our ongoing efforts to make our circuit analysis tool more efficient, accurate, and user-friendly. We appreciate the community’s support and feedback as we continue to refine and improve our methodologies.

Thank you for your continued interest and support!

3 Likes
12

Excited to see the new changes!

1 Like
13

Hello everyone,

I’m excited to share some updates on our ongoing efforts with our analyzer.

Firstly, our team has been diligently working on developing solutions to reduce false negatives in the abstract interpretation of Halo2 circuits. This work has included exploring abstract interpretation on copy constraints and PLONKish lookups. I’m thrilled to report that our solution was recently accepted at CASCON. CASCON is a premier conference in computer science that encourages collaboration between academics and industry partners in a wide range of topcis, including blockchain technologies. For a closer look at our approach, the pre-print is attached right here in the forum.

In addition to this, we’ve been actively evaluating our tool across various Halo2 circuits and gadgets, identifying and addressing edge cases, and implementing effective solutions.

As we move into August, our focus is on evaluating and finalizing the key deliverables we’ve set out in the initial grant.

Please feel free to reach out with any questions or comments you might have. Your feedback is invaluable as we continue to advance in our research.

Looking forward to keeping you updated with our progress.
Abstract_Interpretation_CASCON2024.pdf (239.5 KB)

2 Likes