Refactor #traverseProjection to include stack height parameter
#652
Conversation
- Updated the `#traverseProjection` function to accept an additional `Int` parameter representing the current height of the stack. - Adjusted all related rules to accommodate the new parameter, ensuring correct context handling during projection traversals. - Enhanced the handling of dereferencing and context management in various projection scenarios.
| ~> #writeProjection(NEW) | ||
| => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) | ||
| ... | ||
| </k> | ||
| [preserves-definedness] // valid context ensured upon context construction | ||
|
|
||
| rule <k> #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) | ||
| rule <k> #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS, _CURH) | ||
| ~> #writeMoved | ||
| => #forceSetLocal(local(I), #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL |
There was a problem hiding this comment.
I just see this outdated comment here...
| => #forceSetLocal(local(I), #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL | |
| => #forceSetLocal(local(I), #buildUpdate(Moved, CONTEXTS)) |
- Refactored the `render_rules` function to improve edge rule rendering by incorporating NDBranch logic. - Added logic to select between KCFG edges and NDBranches, ensuring proper rule application display. - Introduced a divider for better readability in the output. - Updated the handling of rules to accommodate cases where no edge is found, enhancing robustness.
- Introduced a new test file `deref_chain_calls.rs` to validate dereferencing of multiple layers of pointers to a struct. - Implemented a sample `Account` struct and functions to demonstrate dereferencing and ensure correct retrieval of balance and flags. - Added assertions to verify expected outcomes, enhancing test coverage for pointer dereferencing scenarios.
- Created a new .gitignore file in the prove-rs directory to exclude Markdown files and the proof directory from version control.
There was a problem hiding this comment.
When I checked out the branch to test it locally, I found that this file is in the way for prove_rs tests... the integration test expects all files in the directory to be rust code.
There was a problem hiding this comment.
Thank you! I'll change it.
|
The CI run times out after 6 hours (!) so there are looping proofs. |
- Added entries to the main .gitignore to exclude specific proof-related files and directories. - Removed the .gitignore file from the prove-rs directory as it is no longer needed.
|
Height is solved by |
#traverseProjectionfunction to accept an additionalIntparameter representing the current height of the stack.