Raghav/weakest precondition#41
Conversation
…eted func/sort decls yet
…ke this a flag and don't mod array selects
|
@codex review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7dec5d4477
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| .Case<MemberReadOp>([this](MemberReadOp read) { | ||
| return builder.getConstant(read.getMemberDefOp(tables)->get(), | ||
| isWitnessOp(read)); |
There was a problem hiding this comment.
When the struct.readm source is a subcomponent value rather than the top-level %self, this returns the global member constant such as x_w/x_c and ignores the struct operand. In nested-struct/subcomponent cases that means reads from different instances, or from a subcomponent value produced by init-*, are all modeled as the same unconstrained field variable instead of read-Sub-x(subcmp), so the emitted WP can miss inequivalence involving subcomponent outputs.
Useful? React with 👍 / 👎.
* Bikeshedding * Fixed testcases * syntax error in test I guess * Adding scalar symbols for subcomponent * Basic subcomponent store works now * Slightly better subcmp read syntax * Works for calls to @Product too * Added subcomponent test * Testing aligned + unaligned --------- Co-authored-by: Raghav Malik <raghav@veridise.com>
* Single loop invariant inference done
* Loop invariants now mostly strengthening to prove postcondition, things look better
* Added circom examples
* New verification results with proper alignment
* Proper while->for conversion
* Fixing some errors as they come up
* Latest results
* Added demo script
* Latest results
* Nested loop support and symbolic store added to WP
* Added back missing slice invariant strengthening
* New results, added {signal} attribute to mux_ep
* Removed unused StrongestPostcondition
---------
Co-authored-by: Raghav Malik <raghav@veridise.com>
* README * Moved README * circom-demo -> circom-examples * Updated README --------- Co-authored-by: Raghav Malik <raghav@veridise.com>
This reverts commit 3170dd3.
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 75574f702d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
* README * Moved README * circom-demo -> circom-examples * Updated README * Updated examples path * Updated examples path * Added reference to Zequal * Update example path * Implement multidimensional array support (#53) * Implement multidimensional array support * Format --------- Co-authored-by: Raghav Malik <raghav@veridise.com> * Use z3 to run benchmarks * Fixing things pre-demo --------- Co-authored-by: Raghav Malik <raghav@veridise.com>
1 participant
No description provided.