feat: acir_formal_proofs #6947
feat: acir_formal_proofs #6947
Conversation
|
Thank you for your contribution to the Noir language. Please do not force push to this branch after the Noir team have started review of this PR. Doing so will only delay us merging your PR as we will need to start the review process from scratch. Thanks for your understanding. |
| @@ -28,7 +28,7 @@ impl<T> Id<T> { | |||
| /// | |||
| /// This is private so that we can guarantee ids created from this function | |||
| /// point to valid T values in their external maps. | |||
| fn new(index: u32) -> Self { | |||
| pub(crate) fn new(index: u32) -> Self { | |||
There was a problem hiding this comment.
Why?
It was changed in #6807 from pub(crate) to private. I can not use test_new instead, because of #[cfg(test)] attribute. I need Id for function building.
|
|
||
| /// Creates an SSA function for truncate operations | ||
| fn truncate_function(variable_type: Type) -> Ssa { | ||
| // truncate v0: field 10, 20?.. |
There was a problem hiding this comment.
Why the question mark?
I wasn't sure what the third argument (max_bit_size) of the Truncate opcode does. Fixed.
| pub struct InstructionArtifacts { | ||
| /// Name of the instruction | ||
| pub instruction_name: String, | ||
|
|
||
| /// SSA representation formatted as "acir(inline) {...}" | ||
| pub formatted_ssa: String, | ||
|
|
||
| /// JSON serialized SSA | ||
| pub serialized_ssa: String, | ||
|
|
||
| /// Gzipped bytes of ACIR program | ||
| pub serialized_acir: Vec<u8>, | ||
| } |
There was a problem hiding this comment.
This looks quite specific to the use case you have. Could it live in the new crate you created?
There was a problem hiding this comment.
This looks quite specific to the use case you have. Could it live in the new crate you created?
No, InstructionArtifacts needs to stay in noirc_evaluator since its implementation uses internal methods and structs of this crate. I don't know how to move this struct to the new crate without breaking the current architecture, if I understand you correctly
There was a problem hiding this comment.
Right, I see even FunctionBuilder is only pub(crate). Maybe there is a case for making that public, as a more general purpose SSA related utility, than making InstructionArtifacts part of the public interface, given its limited scope. I could be wrong, just seeing different serialised SSA formats in it seems overly specific to how you are generating the inputs for the verification, not something anyone else will use.
There was a problem hiding this comment.
I can try to move the entire ssa_verification crate into the noirc_evaluator crate -- this way we wouldn't need to expose anything. However, I'm not sure if this is the right approach since ssa_verification is very specific.
There was a problem hiding this comment.
I agree, I don’t think that’s the right approach either. Maybe @TomAFrench can weigh in on how important it is to keep things private to the crate?
| FLAGS: | ||
| -d, --dir <PATH> Output directory for test artifacts [default: ../../../../../barretenberg/cpp/src/barretenberg/acir_formal_proofs/artifacts/]" |
There was a problem hiding this comment.
I think clap creates these on its own.
Description
The ACIR formal verification. Combines a test generator in the Noir repository with a formal verifier in Barretenberg to mathematically prove the correctness of ACIR instructions using SMT solving. Verifies range of operations including 127-bit arithmetic (addition, subtraction, multiplication), 126-bit division, bitwise operations (though currently limited to 32-bit for AND/OR/XOR), shift operations, field operations (ADD, MUL, DIV), and comparison operations
Additional Context
aztec-packages PR
Documentation*
Check one:
PR Checklist*
cargo fmton default settings.