PVerifier Backend #803
Closed
PVerifier Backend #803
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
* Initial commit for UCLID5 backend. Mostly type definitions for now. * Start encoding of handlers and statements. Need to encode expressions. * small update to assignment handling and generate comments to see what is missing * add next block * support more statements and expressions * refactor before adding helper functions to shorten explicit strings * use more macros so that updates are consistent. Also, use local variables in procedures and then bundle up the new machine using these local variables at the end of the procedure. * WIP: UCLID reserved words, like input, need to be taken care of when printing. * switch from enums for state to datatypes * fix bug in skipping handlers; use .States consistently. WIP: need to support map types correctly * Update UCLID5 backend: avoid keywords through prefix scheme * add support for maps * Functions are procedures; implement call site; need to generate procedure code. * add support for helper function bodies as UCLID procedures. Always call a procedure with an argument representing the calling machine. * add simple chain replication and update compiler to handle it * add helper for setting field defaults for maps and sets; init fields to defaults * fix bug in precodnition for event handlers * add happy path chain replication * add ucl files * checkpoint chain replication * add support for foreach statements, default expressions, etc, before moving to new encoding * add goto types * add label type * gotos should carry target. Need to redo procedures and next block to handle labels. * WIP: rewrite UCLID5 backend to use labels and not have implicit ignores. Need to add handlers back in. * Finish foundation of new encoding * inline deref function * WIP: add support for spec machines. Now constructing listener map, need to use map on sends. * add spec procedure calls after evry send * WIP: add invariant to parser * add support for invariants at the P level * add support for quantifier expressions * add support for quantifying over machines * fix bugs in permission type quantification * add support for pure, a keyword for specification functions. Need to fix TestExpr * add enough proof syntax to prove that clients in chain rep don't receive unexpected events * add 9, fix compiler bug for empty events, start proof * add axiom keyword * add support for testing state * incorrect proof. Need to find contradiction * make sure to verify all procedurs * add support for quantifying over and selecting from specific event kinds * add partial 2pc proof. Need to add syntax for talking about state delay * add compiler pass to uclid backend * add difference constraints * full 2pc proof * deal with final proof obligation of 2pc * add simple chain replication verification, add spec machine field access, change flying to inflight * add unique identifier to actions and automatically prove that it is actually unique * add sent keyword * remove stale examples. Will add back later when updated. * rename tutorial * add support for limited map nesting; start adding multi round 2pc * start adding support for choose (placeholder); add support for assume * update 2pc rounds with assumption; add ring leader election that needs a bit more time to solve than the default * add limited support for choose expressions * add support for pure functions with bodies * better verification feedback for users * add timeout for UCLID5 backend * allow for specific events in diff loop invaraints * start generalizing 2pc with rounds * finish 2pc rounds; fix bug with negative timeout value * reorganize verification tutorial * add feedback for failing to prove assertions and update 2pc kv example to show it off * add kv version of 2pc that has a consistency monitor * make users init fields to default values * fix bug when spec machine handlers don't take arguments * add support for return statements (although we are not actually exiting the procedure on them) * fix bug in global procedure bindings; inline procedures unless they do not have a body. * handle empty payloads for spec handlers * add parens around state check to avoid binding issues; update 2pc-key-value example to generate random values too * [fix] canonicalize container type before checking for codegen * add 'handles-all' flag that can be turned off to avoid checking that all events are handled * add support for iterating over maps with the keys expression * more missing parens * add check-only argument and change no-event-handler-checks to a flag * fix bugs in new command line options * no need to run any handlers in next block. Fix condition for check only flag. * don't forget to check the base case! * relax type checking on pure functions * do not init local variables to default values * add missing local variable declarations for global procedures --------- Co-authored-by: AD1024 <[email protected]> Co-authored-by: Ankush Desai <[email protected]>
#783) * [add] prove using command * [add] invariant ref * [save] generating queries for proof commands * [save] finish commands * save parallization * save * save * save * save * [save] more tweaks * remove some commented code * [fix] separate sanity check and event handler checks * [add] `except` keyword * remove some commented code * [fix] generate local state for spec machines
…ial to include an example
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.
Add support for formal verification of P programs using UCLID5 as a backend. We introduce new keywords for verification but disallow their use in all other backends.
See
Docs/docs/advanced/install-verification-backend.mdfor instructions on how to install the verification dependencies. SeeDocs/docs/tutorial/advanced/twophasecommitverification.mdfor a tutorial on how to use the verification backend once installed.