feat: creating an SMT verification module #1932
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Rumata888
reviewed
Sep 13, 2023
| @@ -0,0 +1,2 @@ | |||
| #barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1) | |||
There was a problem hiding this comment.
Pleas remove this commented out line
Rumata888
reviewed
Sep 13, 2023
|
|
||
| /** | ||
| * @brief Get the CircuitSchema object | ||
| * @details Initialize the CircuitSchmea from the msgpack compatible buffer. |
Rumata888
reviewed
Sep 13, 2023
| * | ||
| * @param circuit_info | ||
| * @param s pointer to the global solver | ||
| * @param equal all the variables that should be equal in both circuits |
There was a problem hiding this comment.
- The list of names of variables which should be equal in both circuits (each is equal)
- The list of names of variables which should not be equal in both circuits (each is not equal)
- The list of variables, where at least one pair has to be equal
- The list of variables, where at least one pair has to be distinct
Rumata888
approved these changes
Sep 13, 2023
PhilWindle
pushed a commit
that referenced
this pull request
Sep 14, 2023
🤖 I have created a release *beep* *boop* --- <details><summary>aztec-packages: 0.7.1</summary> ## [0.7.1](aztec-packages-v0.7.0...aztec-packages-v0.7.1) (2023-09-14) ### Features * Build system handles dynamic deps first class. ([#2283](#2283)) ([f66077a](f66077a)) * Build_manifest default tweaks. ([#2287](#2287)) ([c8a5cfb](c8a5cfb)) * **build:** Build multi-architecture docker images for aztec-sandbox ([#2305](#2305)) ([8ee61b8](8ee61b8)) * Cli "unbox" command ([#2029](#2029)) ([26ab88f](26ab88f)) * Creating an SMT verification module ([#1932](#1932)) ([4642b61](4642b61)) * Token standard ([#2069](#2069)) ([5e8fbf2](5e8fbf2)) ### Bug Fixes * Ensure_note_hash_exists ([#2256](#2256)) ([271b060](271b060)) * Msgpack stack blowups on schema gen ([#2259](#2259)) ([1afc566](1afc566)) * Noir bootstrap ([#2274](#2274)) ([f85db49](f85db49)) * Workaround sequencer timeout ([#2269](#2269)) ([9fc3f3d](9fc3f3d)) ### Miscellaneous * Bump nargo to 0.11.1-aztec.0 ([#2298](#2298)) ([8b76a12](8b76a12)) * **ci:** Mirror Aztec-nr ([#2270](#2270)) ([c57f027](c57f027)) * **circuits:** Base rollup cbind msgpack ([#2263](#2263)) ([0d4c707](0d4c707)) * **circuits:** Clean up of some superfluous header includes ([#2302](#2302)) ([5e53345](5e53345)) * **circuits:** Removing assertMemberLength on Tuple objects ([#2296](#2296)) ([0247b85](0247b85)) * Consolidate mirror repos on a nightly schedule ([#1994](#1994)) ([1a586c4](1a586c4)) * **docs:** Rename to aztec.nr ([#1943](#1943)) ([a91db48](a91db48)) * Move barretenberg to top of repo. Make circuits build off barretenberg build. ([#2221](#2221)) ([404ec34](404ec34)) * Replace native token in lending contract ([#2276](#2276)) ([c46b3c8](c46b3c8)) * **subrepo:** Push aztec-nr, update default branches ([#2300](#2300)) ([80c9b77](80c9b77)) * Updated `acvm_js` ([#2272](#2272)) ([9f1a3a5](9f1a3a5)) </details> <details><summary>barretenberg.js: 0.7.1</summary> ## [0.7.1](barretenberg.js-v0.7.0...barretenberg.js-v0.7.1) (2023-09-14) ### Miscellaneous * Move barretenberg to top of repo. Make circuits build off barretenberg build. ([#2221](#2221)) ([404ec34](404ec34)) </details> <details><summary>barretenberg: 0.7.1</summary> ## [0.7.1](barretenberg-v0.7.0...barretenberg-v0.7.1) (2023-09-14) ### Miscellaneous * Move barretenberg to top of repo. Make circuits build off barretenberg build. ([#2221](#2221)) ([404ec34](404ec34)) </details> --- This PR was generated with [Release Please](https://github.com/googleapis/release-please). See [documentation](https://github.com/googleapis/release-please#release-please).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Please provide a paragraph or two giving a summary of the change, including relevant motivation and context.
Checklist:
Remove the checklist to signal you've completed it. Enable auto-merge if the PR is ready to merge.