[Feature] prove * using * command for incremental proof construction
#783
Conversation
This file contains hidden or 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
ankushdesai
approved these changes
Oct 7, 2024
| invariant a6: coordinator() is Committed ==> (forall (p: Participant) :: p in participants() ==> preference(p) == YES); | ||
| } | ||
|
|
||
| Proof { |
There was a problem hiding this comment.
@shazqadeer You will love this as well.
|
I added an |
FedericoAureliano
approved these changes
Oct 10, 2024
| USING : 'using'; | ||
| LEMMA : 'Lemma'; | ||
| THEOREM : 'Theorem'; | ||
| EXCEPT : 'except'; |
There was a problem hiding this comment.
Do you have an example that uses the "except" keyword? I'm not totally sure I understand what it does. Is it just like commenting an invariant out?
There was a problem hiding this comment.
Yes, essentially it is excluding invariants from goals and premises.
For example, if you write prove X using * and you do not want to put Y in the *, then you can write prove X using * except Y.
Also, if you write prove * and do not want to include Y in *, you can write prove * except Y.
There was a problem hiding this comment.
Oh cool, looks good to me!
dd47b1e
into
p-org:experimental/pverifier
0 of 7 checks passed
FedericoAureliano
pushed a commit
that referenced
this pull request
Nov 28, 2024
#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
ankushdesai
added a commit
that referenced
this pull request
Dec 10, 2024
* Prototype Support For Verification (#762) * 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]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#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 * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]>
FedericoAureliano
added a commit
that referenced
this pull request
Jul 22, 2025
* Prototype Support For Verification (#762) * 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]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#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 * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]>
ankushdesai
added a commit
that referenced
this pull request
Jul 30, 2025
* Start to move PVerifier so that its ready to be merged into P3.0 (#805) * Prototype Support For Verification (#762) * 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]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#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 * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> * bugfix: do not check default constraints at the same time as user constraints. Also hash filenames to make them shorter. * reorganize files before creating new documentation that is consistent with the rest of P * first draft of pverifier docs * cleanup pverifier documentation * fix link * prove-using should use assumes and not form cycles * [feature] Checking individual proof blocks via `-pb` (#848) * [add] running individual proof blocks via `-pb` * save * fixes * [fix] duplicated call stmts of spec procedures (#851) * set sanity check (#852) * Correct and complete PVerifier installation instructions on Amazon Linux 2. (#864) Co-authored-by: Mark Tuttle <[email protected]> * [fix] Postpone type checking of invariants, axioms, init-conditions and pure functions (#865) * save fixes * retrigger checks * fill in proof block at the end of scope construction * save fixes (#866) * [tweak] error reporting for loop invariants (#867) * add loop invariant failing report * use a set to maintain error messages * [fix] catching assertion failures (#868) * add loop invariant failing report * use a set to maintain error messages * add error reporting for assertions * [fix] Use local variables for assume statements (#870) * [fix] pre/post condition type checking (#872) * correct link to 2PC (#878) link to 2PC for PVerifier was not correct. * small updates to announcement * Start to move PVerifier so that its ready to be merged into P3.0 (#805) * Prototype Support For Verification (#762) * 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]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#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 * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> * bugfix: do not check default constraints at the same time as user constraints. Also hash filenames to make them shorter. * reorganize files before creating new documentation that is consistent with the rest of P * first draft of pverifier docs * cleanup pverifier documentation * fix link * prove-using should use assumes and not form cycles * [feature] Checking individual proof blocks via `-pb` (#848) * [add] running individual proof blocks via `-pb` * save * fixes * [fix] duplicated call stmts of spec procedures (#851) * set sanity check (#852) * Correct and complete PVerifier installation instructions on Amazon Linux 2. (#864) Co-authored-by: Mark Tuttle <[email protected]> * [fix] Postpone type checking of invariants, axioms, init-conditions and pure functions (#865) * save fixes * retrigger checks * fill in proof block at the end of scope construction * save fixes (#866) * [tweak] error reporting for loop invariants (#867) * add loop invariant failing report * use a set to maintain error messages * [fix] catching assertion failures (#868) * add loop invariant failing report * use a set to maintain error messages * add error reporting for assertions * [fix] Use local variables for assume statements (#870) * [fix] pre/post condition type checking (#872) * correct link to 2PC (#878) link to 2PC for PVerifier was not correct. * small updates to announcement * fix bad merge: accidently kept both instead of the correct one for compiler config * add some more examples * save * remove the inflight axiom * remove the other * move verification examples to the correct folder * add ASSUME and PURE tokens to P Verifier syntax check; remove duplicates from merge * Remove the incomplete parser support for assume and assert annotations over events and machines * merge "major/P3.0" --------- Co-authored-by: Ankush Desai <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> Co-authored-by: AngAng <[email protected]> Co-authored-by: Mark Tuttle <[email protected]> Co-authored-by: Mark Tuttle <[email protected]> Co-authored-by: Muqsit Azeem <[email protected]> Co-authored-by: Christine Zhou <[email protected]>
ankushdesai
added a commit
that referenced
this pull request
Aug 13, 2025
* Renamed the folders and targets; (#806) * Fix PChecker .dll file not found (#829) Co-authored-by: Christine Zhou <[email protected]> * fix typo in a workflow file - macosci.yml * Update build system and Java compiler, remove dependency JARs * Removed all the PRuntimes that are not supported any more * Merging PEx into the Major release P 3.0 branch. (#860) * Removed the C backend completely in the P 2.1 * Upgraded P to use .Net 8.0 * Updated the actions to .Net 8.0 * [PSym] Upgrade to .NET 8.0 * [PCover] Adds temporary CLI mode to trigger new explicit engine * [PCover] Adds initial version of cleaned up PCover backend TODO: Implement basic new runtime interface to pass code compilation post generation * [PCover] Minor * [PCover IR] Cleans up logic relating to event handlers Removes using PMachineValue for now * [CLI] Adds new pcover cli (hidden) * [PCover IR] Cleanup IR for sending event, machine creation, etc. * [PCover runtime] Adds basic runtime setup files * [PCover] Adds placeholder for CLI config * [PCover] Adds main and trace loggers using Log4J * [PCover] Adds event buffer represented as fifo queue with sender semantics * [PCover] Adds event handler placeholders * [PCover] Adds event/message placeholders * [PCover] Adds basic code for machine/state/test driver * [PCover] Adds basic code for scheduler * [PCover] Adds global data structures and program interface * [PCover] Adds utils * [PCover IR] Minor renaming * [PCover] Adds PValues for P data types * [PCover] Renaming and minor corrections Renames Machine/Monitor/Program to PMachine/PMonitor/PModel Corrects PBool value * [PCover] Minor update to javadocs * [PCover] Reformating * [PCover IR+RT] Rename Message to PMessage * [CLI] Minor correction * [PExplicit] Renames new PCover to PExplicit * [PExplicit] Minor correction to CLI * [PExplicit RT] Rename repeat to current, backtrack to unexplored choices * [PExplicit RT] Adds CLI options and config * [PExplicit RT] Adds new exceptions when a bug is found * [PExplicit RT] Adds timeout/memout monitors * [Pexplicit RT] Adds utils for timed call, random number generator, and in-line asserts * [Pexplicit RT] Adds more logging functions * [PExplicit RT] Updates machine and message queues to check if machine can run and if a message is a create machine event * [PExplicit RT] Add function to check if an event is a create machine event * [PExplicit RT] Improve choices and schedule fields * [PExplicit RT] Implements main PExplicit fentry point, runtime executor service, making timed call Deletes DeferQueue. Instead the plan is to handle defers as in C# runtime. Updates global fields * [PExplicit RT] Updates loggers Adds new log functions to the main logger, adds a scratch logger for intermediate printing * [PExplicit RT] Implements and cleans up certain PMachine/State functions * [PExplicit RT] Adds initial version of scheduler Work in progress: finish pending TODOs and JavaDoc comments * [PExplicit RT] Implements basic machine/scheduler/FIFO functions TODOs: receives, defers, etc. * [PExplicit RT] Adds initial support for stateless dfs-style backtracking Adds tracking all machine instances in global context * [PExplicit IR] Removes StringVS TODO: support formatted arguments in PString in RT * [PExplicit RT] Corrects basic dfs-search Corrects adding new machines to global and schedule context Adds basic functions for PMessage Corrects scheduler DFS-style search working on pingPong * [PExplicit RT] Improves how peeking into a machine's FIFO queue works * [PExplicit] Support formatted PString, initial support for defers and receives Adds support for formatted string Adds continuations to runtime and cleans up IR with a simplified interface Adds partial support for defers and receives TODO: finish defer and receive handling * [PExplicit RT] Adds support for defers and blocking receive Adds tracking deferred events via a defer queue Adds PContinuation to track all continuations Adds blocking on a continuation, and unblocking when handling one of the corresponding case event Corrects peeking logic in sender queue Renames FifoQueue to SenderQueue * [PExplicit] Adds support for receives, loops, and named tuple constructor Cleans up support for receives. Adds support for receives within while loop Simplifies IR for loops Updates PValue for PCollection types Corrects constructor for PNamedTuple * [PExplicit] Implements operations for primitive PValue types Minor renaming * [PExplicit] Adds running mvn test and github ci action * [PExplicit RT] Implement raising an event * Disable GitHub CI actions temporarily to only run PExplicit CI * [PExplicit] Several minor updates Support goto event handlers with transition functions Correct PTuple constructor Correct status and result when a bug is bound Cleanup return in functions in IR. Start adding pending/unsupported tests in PExplicit test runner * [PExplicit] Support announce, correct named tuple set ffield, support != operation * [PExplicit] Several corrections Implement raise event, updates logging, updates PCollection to be an interface, updates exclude list for regression runs Adds enforcing max step bound * [PExplicit] Correct raise event with payload * [PExplicit] Correct PString constructor * [PExplicit IR] Exit current flow context if raise or goto statements are present * Update gitignore * [PExplicit] Several corrections Changes PCollection types to not take parameters (so that collections over any type can be allowed) Corrects choosing from a PCollection Corrects IR to track whether function exited or not Avoid printing redundant code if receive cases already exited * [PExplicit] Support enum references with values specified Support enum to int Update excluded regressions list * [PExplicit IR] Correct dynamic type casting in IR * Suppress github ci failures due to not running them on current branch * [PExplicit] Cleaned up type casting in IR Added type casting regressions Corrected PTuple set field * [PExplicit] Support continue statement Remove unreachable code after receive case block * [PExplicit] Several small upgrades Support blocking receives during state transitions and exit functions Support getting values of a PMap Add logging for entering and exiting a state * [PExplicit] Several corrections and minor lang feature support Corrects type casting from any when a function returns a value Adds catching null pointer and stack overflow exceptions as a bug Implement get or default from a PMap Comments out liveness test regressions for now (added TODO) Cleans up PMachineValue constructor * [PExplicit] Refactoring and cleanup * Undo temporary changes to GitHub CI * [PExplicit] Update pom, minor refactoring * [PExplicit] Update to java 17 * [PExplicit] Minor: report class cast exception as a bug * [PExplicit] Convert run status to enum * [PExplicit] Clean up control flow relating to pending state transition (exit/new-state-entry) Renames blockedEntryState to blockedNewStateEntry * [PExplicit] Update comments * Added support for generating a warning when spec handles an event but does not add it in its observes list (#716) * Create custom converter for JSON serialization in .NET8 (#717) * Create custom converter for JSON serialization in .NET8 * Add check for different dictionary type for null replacement --------- Co-authored-by: Eric Hua <[email protected]> * [PExplicit] Support deadlock and liveness checking Adds deadlock checking Adds basic liveness checking, based on whether a monitor is in a hot state at the end of a schedule Updates logger to resemble like in C# * [PExplicit] Minor * [PExplicit] Adds buggy trace replayer and basic .schedule writer * [PExplicit] Correct issues when replaying buggy trace Corrected catching null/class-cast errors when replaying Corrected how a machine resets (to reset variables relating to blocking receives) Corrected how current choice is fetched when replaying * [PExplicit] Adds TextWriter to write trace in txt format Updates logging * [PExplicit] Correct halt event name * [PExplicit] Adds state caching Adds state caching to avoid revisiting same state more than once State caching mode can be: none, fingerprint (i.e., use hash codes), or exact (use exact values). Fingerprinting is the default. Updates logging and stats to track and report distinct states Minor cleanup to IR * [PExplicit] Minor refactoring * [PExplicit] Correct cycle error in replayer, enforce cycle detection only when --fail-on-maxsteps enabled * [PExplicit] Correct local var names in IR * [PExplicit] Correct replayer, add initial version of stateful backtracking * [PExplicit] Correct backtracking * [PExplicit] Refactor and enable stateful backtracking * [PExplicit] Minor improvement to stateful backtracking * [PExplicit] Reformat code * [PExplicit] More reformatting * [PExplicit] Minor corrections Correct comparing machines (including monitors) Correct printing step state * [PExplicit] Correct PMachine/PMonitor hashCode and compateTo functions * [PExplicit] Uniquify instanceId for PMachine as well as PMonitor * [PExplicit] Improve state caching Adds storing hashcode and string representation during PValue initialization Adds new state caching modes using hash functions from guava library New state caching modes include: hashcode (java built in, 32-bit), siphash24 (64-bit), murmur3_128 (128-bit, default), sha256 (256-bit), or exact (using exact string representation) * [PExplicit] Add non-chronological search Adds non-chronological search that implements search beyond DFS. New search modes include random, astar Each run is executed over search tasks, with each task tracking the set of unexplored choices it is assigned to explore Each search task can create new children sub-tasks * [Pexplicit] Minor * [PExplicit] Minor refactoring * [PExplicit] Refactoring and cleanup * Limit number of choices in choose expression to at most 10000 (#725) * Limit number of choices in a choose(.) to atmost 10,000 Adds throwing a compile-time or runtime error if the number of choices in a choose(.) is greater than 10000. Updates GitHub docs to reflect this change. * Adds regression tests for choose exceeding 10000 choices * [PSym] Throw error if number of choices are greater than 10000 * Make PEvents and PTypes serializable in java (#726) * [PExplicit IR] Minor correction * [PExplicit] Update usage via P CLI * [PExplicit] Several corrections to choice tracking Change choice in a schedule to be either ScheduleChoice or DataChoice Step state does not track step/choice number, only tracks current machines and machine states (in stateful backtracking) Correct SearchTask to store full list of prefix/suffix choices. Suffix choices contain list of unexplored choices assigned to this task. Update how liveness/deadlock checking is asserted and replayed. * [PExplicit] Minor refactoring * [PExplicit] Refactoring and setting defaults * [PExplicit] Correct counting unexplored choices * [PExplicit] Minor changes to logging and asserts * [PExplicit] Throw error if number of choices in choose(.) exceeds 10K * [PExplicit] Correct stateful backtracking with complex data choices * [PEx] Minor update * [PEx] Support Java foreign functions * [PEx] Minor corrections to IR * [PEx] Minor: correct an assertion * [PEx] Make receive inside while as not implemented for now Update enum logging and stats reporting PMap: throw error if adding already existing key * [PEx] Experimenting with while and receive in IR * [PEx] Correct corner cases with while, receive, and after statements * [Tst] Add unit test to check interaction between while, receive w/ case payload, and after statements after receive and while * Removed the C backend completely in the P 2.1 * [PCover] Adds temporary CLI mode to trigger new explicit engine * [CLI] Adds new pcover cli (hidden) * [PExplicit] Renames new PCover to PExplicit * Correct sync with mainline * [PEx] Revamps tracking unexplored choices, changes schedule choice (#745) * [PEx] Change schedule choice from PMachine to PMachineId * [PEx] Major revamping of Choice: 1/n Old schedule/data choice changed to schedule/data SearchUnit Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue<?> TODO: clean up Schedule with new class structure * Revert "[PEx] Major revamping of Choice: 1/n" This reverts commit 53c5d15. * [PEx] Separates unexplored choices from schedule * [PEx] Cleanup and minor corrections to recent changes to SearchTask * [PEx] Minor correction * [PEx] Corrections to new backtracking logic * [PEx] Adds modes for stateful backtracking Adds CLI option --stateful-backtrack none|intra-task|all to limit stateful backtracking to OFF|within-a-task|ON * [PEx] Add support to serialize and deserialize search tasks in/from file * [PEx] Updates mvn test config * [PEx] Minor correction Fix issue relating to intra-task stateful backtracking with dynamic machine creation * [PEx IR] Minor correction * [PEx] Several improvements to IR Revamps IR to store continuation variables within PContinuation class Adds function to get the default value from a PValue object Removes generating get/set/reset functions for PMachine variables. Instead, using reflection in PEx RT. Minor refactoring * [PEx IR] Minor cleanup * [PEx] Cleanup disk tasks on exit, change defaults Cleanup tasks/ directory on exiting Change default for schedules-per-task to 500 Change report wait time to 10 sec. * [PEx] Minor: create .schedule only if bug is found * [PEx] Adds writing buggy trace in file Adds serializing buggy trace in file Minor renaming * [PEx] Adds option --replay <.schedule file> to replay a buggy trace * [PEx] Minor * [PEx] Fix serialization issues found by P regression tests * [PEx] Minor cleanup * [PEx] Improve cleanup of disk tasks on exit * [PEx] Minor correction Update liveness check, minor renaming * [PEx] Add first version of RL-based choice selection * [PEx] Correct timelines tracking and RL-based choice selection * [PEx] Update timelines, corrects CI * [PEx] Renaming and refactoring Renames PExplicit -> PEx, GlobalFunctions -> PExForeignCode, mode explicit -> pex Refactors PEx IR generator * [CLI] Update PEx CLI options Makes --mode option visible. * [CLI] Cleanup PEx CLI options * [CI] Correct PEx CI * [PEx] Add support for refinement interfaces * [Tutorial] Adds updates for running with PEx Adds changes/hints to enable running with PEx 1_ClientServer: limits number of withdraw requests to at most 5, adds 2 hints to limit data non-determinism 2_TwoPhaseCommit: adds hint to create random transaction without foreign code and with less data non-determinism 3_EspressoMachine: no change * [PEx] Minor: update pom.xml * [PEx] Implements multi-threaded PEx version (#768) * [PEx] Move globals to PExGlobal, adds --nproc CLI option Moves state cache, timelines, num tasks data structures to PEx global class Adds CLI option --nproc to provide number of threads * [PEx] Adds dedicated logger for each thread Moves global results reporting to global class * [PEx] parallel: adds todos, cleans up global class * [PEx] parallel: fix IR, move scheduler specific fields from globals * [PEx] parallel: update IR so that main machine and monitors are created by PEx runtime * [PEx] parallel: make search statistics thread safe * [PEx] parallel: completes first version Several updates: support multi-thread executor, result tracking, exceptions tracking, compiling results, terminating threads, resolving data conflicts, implements lock/release for shared constructs * [PEx] parallel: minor change * [PEx] parallel: update GitHub CI to run with 3 threads * [PEx] parallel: minor corrections Make global machine/monitor instance ids thread safe Add hash/name to PContinuation object for thread-safe state caching * [PEx] Adds tracking and limiting number of choices per choose(.) statement Adds tracking number of calls and total choices generated in a schedule corresponding to each choose(.) statement in the model. Adds option --max-choices-per-call and --max-choices-total to limit max number of choices in a schedule corresponding to a choose(.) statement (default is 10,000 for per choose.) call and no limit on total choices, as in C# backend). Else, a TooManyChoicesException is triggered as a bug. * [PEx] bump version, change cli defaults Change max choices per choose statement to 10 per call and 100 per schedule by default Minor renaming * [PEx] code cleanup and refactoring * [PEx] minor logging changes, [Tst] Change choose(100) to choose(10) * [PEx] Minor logging changes * [PEx] Changes return codes 0: ok, 2: bug, 3: bug (too_many_choices), 4: timeout, 5: memout, 6: error * [PEx] Correct return codes, [Tst] Limit choose choices * [Tutorial] Update hints for PEx [PEx] minor change * [PEx] Minor updates and cleanup (#775) * [PEx] Several updates to logging, PEx config Changes default max choices limit to 20 per call and 250 per schedule (to account for open-source protocols with monolithic transition relation modeled as single action) Adds logging support to print choose(.) location info for easy debugging TooManyChoicesException via replayer log Minor correction * [PEx] Refactoring and formatting changes * [PEx] Update cli default Change each task to 2K schedules by default * [PEx] Minor correction Make sure continuation with loop does not declare local var twice * [PEx] Correct repeated local var declaration in IR * [PEx] Correct code too large error due to receive-inside-loop inlining * [PEx] Adds PLoopObject to track receive-loop variables * [PEx] Minor: correct defaults in help menu * modified cache@v2 to cache@v4 * Rename PEvent to Event, Handle PrimitiveType.Null in GetDefaultValue * [PEx] Correct functions containing non-tail ending goto/raise (#835) * [PEx] Correct inlining for functions returning a value (#840) * [PEx] Correct functions containing goto/raise Changes PEx IR to support functions that contain non-tail ending goto/raise Enables supporting needed function inlining in spec machines Bumps PEx runtime revision to 0.3.0 * [PEx] Remove wrongly-added files * [PEx IR] Correct function inlining for non-null returning functions Add guard conditions to disable function body statement if already returned Throw exception if inlining is unsupported * removed CSharp, Java modes in CompilerOutput , removed global.json * Minor changes to make customer model to compile (#842) * [PEx] Disable support for receive statement inside loop (#843) Throw compile-time exception for receive statement inside loop with appropriate message Adds try/catch to gracefully report not-supported errors during compiling for PEx PEX RT: exclude tests with receive inside loop * Dev/remove libhandler (#847) * Update build system and Java compiler, remove dependency JARs (#849) * Update build system and Java compiler, remove dependency JARs * Update CheckerCore logging and state machine components * [PEx] Correct inlining functions with non-null return without assignment (#850) * [PEx] Correct inlining functions with non-null return without assignment, support test driver name same as test machine name [PEx IR] Adds support for inlining functions that return non-null but are not assigned to a variable during function call [PEx IR+RT] Prefixes test driver names with test_ to support test name same as test main machine name [Tst] Adds unit test with test case name same as main machine name * [PEx IR] Correct IR for functions returning null * [Tst] Update new unit test to align with hardcoded test name in C# unit test runner * [Tst] Dropping unit test since C# test runner uses hardcoded test name and main machine * [PEx IR] Minor correction when pritning source location in exception * Moved PEx outside the PRuntimes * Update pex.yml * Update build scripts and test executor; add build documentation * Fix Java version to 17 and correct P build directory path * Pex param test (#855) * Add global constant varaibles; TODO backend * Updated BuildGlobalScope * add global variable * fix global variable types * Allow multiple tests * Add int list literal syntax * add parametric test * Quick-fix * fix bad quick-fix * add rich syntax * Small merge error * Param (#833) * update assumption * fix: add deps back * refactor: constant -> param * fix * clean the code * unify normal/param/assume tests * clean the code * rename * merging safety test parser rules * clean the code * Update github CI action v2 to v3 * iUpdate github CI action v2 to v3 on ubuntu * rename variable "param" into "parameter" to avoid keyword conflicts * T-wise combinatorial test (#837) * add twise * clean the code * Solved Concerns from Lewis: + new allow twise number be 1 + unify twise number valid condition + add unit test * add new test case * unit test for ParamAssignment.IterateAssignments * merge * fix duplicate declears bug --------- Co-authored-by: Ankush Desai <[email protected]> * PR #860 Fixes: Removed Coverage and Verification modes, fixed code quality issues, added comments for placeholders, and added missing newlines at the end of files --------- Co-authored-by: Aman Goel <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: mchadalavada <[email protected]> Co-authored-by: Aishwarya Jagarapu <[email protected]> Co-authored-by: aishu-j <[email protected]> Co-authored-by: ChristineZh0u <[email protected]> Co-authored-by: Zhe Zhou <[email protected]> * Updating PEx maven publish Github action (#874) Co-authored-by: Christine Zhou <[email protected]> * Dev p3.0/param testcases (#879) * Add global constant varaibles; TODO backend * Updated BuildGlobalScope * add global variable * fix global variable types * Allow multiple tests * Add int list literal syntax * add parametric test * Quick-fix * fix bad quick-fix * add rich syntax * Small merge error * Param (#833) * update assumption * fix: add deps back * refactor: constant -> param * fix * clean the code * unify normal/param/assume tests * clean the code * rename * merging safety test parser rules * clean the code * Update github CI action v2 to v3 * iUpdate github CI action v2 to v3 on ubuntu * rename variable "param" into "parameter" to avoid keyword conflicts * T-wise combinatorial test (#837) * add twise * clean the code * T-wise combinatorial (Solved Concerns from Lewis) (#838) * Solved Concerns from Lewis: + new allow twise number be 1 + unify twise number valid condition + add unit test * add new test case * unit test for ParamAssignment.IterateAssignments * Dev/remove libhandler (#847) * Update build system and Java compiler, remove dependency JARs (#849) * Update build system and Java compiler, remove dependency JARs * Update CheckerCore logging and state machine components * Modified regression tests to run in process, added test cases for parametric test (#875) Co-authored-by: Christine Zhou <[email protected]> * Fix pex regression test * remove unnecessary line * Addressing PR comments --------- Co-authored-by: zhezhouzz <[email protected]> Co-authored-by: zhezhouzz <[email protected]> Co-authored-by: Ankush Desai <[email protected]> Co-authored-by: Christine Zhou <[email protected]> * P Verifier (#887) * Start to move PVerifier so that its ready to be merged into P3.0 (#805) * Prototype Support For Verification (#762) * 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]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#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 * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> * bugfix: do not check default constraints at the same time as user constraints. Also hash filenames to make them shorter. * reorganize files before creating new documentation that is consistent with the rest of P * first draft of pverifier docs * cleanup pverifier documentation * fix link * prove-using should use assumes and not form cycles * [feature] Checking individual proof blocks via `-pb` (#848) * [add] running individual proof blocks via `-pb` * save * fixes * [fix] duplicated call stmts of spec procedures (#851) * set sanity check (#852) * Correct and complete PVerifier installation instructions on Amazon Linux 2. (#864) Co-authored-by: Mark Tuttle <[email protected]> * [fix] Postpone type checking of invariants, axioms, init-conditions and pure functions (#865) * save fixes * retrigger checks * fill in proof block at the end of scope construction * save fixes (#866) * [tweak] error reporting for loop invariants (#867) * add loop invariant failing report * use a set to maintain error messages * [fix] catching assertion failures (#868) * add loop invariant failing report * use a set to maintain error messages * add error reporting for assertions * [fix] Use local variables for assume statements (#870) * [fix] pre/post condition type checking (#872) * correct link to 2PC (#878) link to 2PC for PVerifier was not correct. * small updates to announcement * Start to move PVerifier so that its ready to be merged into P3.0 (#805) * Prototype Support For Verification (#762) * 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]> * add install instructions for amazon linux * [Feature] `prove * using *` command for incremental proof construction (#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 * add support for foreign functions with contracts and update one tutorial to include an example * allow duplicate invariant names in different groups using group name as prefix * add caching using liteDB and md5 hash of uclid files * fix bug in caching by simplifying process checklist * fix bug in global procedures: always prepend self reference * add default that captures P's proof obligations * fix bug in file names * cleanup example for tutorial * add 2pc verification tutorial * pverifier backend and reorganize verification tutorials * init keyword -> init-condition keyword * add error message when trying to use pverifier syntax for other backends * move install instructions to docs and update link in 2pc verification tutorial. * rename uclid5 backend to pverifier * remove unnecessary imports * add iff symbol --------- Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> * bugfix: do not check default constraints at the same time as user constraints. Also hash filenames to make them shorter. * reorganize files before creating new documentation that is consistent with the rest of P * first draft of pverifier docs * cleanup pverifier documentation * fix link * prove-using should use assumes and not form cycles * [feature] Checking individual proof blocks via `-pb` (#848) * [add] running individual proof blocks via `-pb` * save * fixes * [fix] duplicated call stmts of spec procedures (#851) * set sanity check (#852) * Correct and complete PVerifier installation instructions on Amazon Linux 2. (#864) Co-authored-by: Mark Tuttle <[email protected]> * [fix] Postpone type checking of invariants, axioms, init-conditions and pure functions (#865) * save fixes * retrigger checks * fill in proof block at the end of scope construction * save fixes (#866) * [tweak] error reporting for loop invariants (#867) * add loop invariant failing report * use a set to maintain error messages * [fix] catching assertion failures (#868) * add loop invariant failing report * use a set to maintain error messages * add error reporting for assertions * [fix] Use local variables for assume statements (#870) * [fix] pre/post condition type checking (#872) * correct link to 2PC (#878) link to 2PC for PVerifier was not correct. * small updates to announcement * fix bad merge: accidently kept both instead of the correct one for compiler config * add some more examples * save * remove the inflight axiom * remove the other * move verification examples to the correct folder * add ASSUME and PURE tokens to P Verifier syntax check; remove duplicates from merge * Remove the incomplete parser support for assume and assert annotations over events and machines * merge "major/P3.0" --------- Co-authored-by: Ankush Desai <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> Co-authored-by: AngAng <[email protected]> Co-authored-by: Mark Tuttle <[email protected]> Co-authored-by: Mark Tuttle <[email protected]> Co-authored-by: Muqsit Azeem <[email protected]> Co-authored-by: Christine Zhou <[email protected]> * add two more examples * Add param tests in tutorials (#889) * Add param tests to tutorials, modified wiki * Add param test for two phase commit example * Add new feature were running p check -tc testName runs all tests with the testName as prefix * Minor fixes to tutorial docs * fix logic error --------- Co-authored-by: Christine Zhou <[email protected]> * [add] Paxos and Raft for P Tutorials (#890) * [add] Paxos and Raft in P tutorial * save tweaks * Add documentation for PEx (#893) * Dev p3.0/pex doc (#900) * Add documentation for PEx * Addressing comments --------- Co-authored-by: Christine Zhou <[email protected]> * Dev p3.0/pex doc (#902) * Add documentation for PEx * Addressing comments * Remove unecesarry files --------- Co-authored-by: Christine Zhou <[email protected]> --------- Co-authored-by: ChristineZh0u <[email protected]> Co-authored-by: Christine Zhou <[email protected]> Co-authored-by: Aishwarya Jagarapu <[email protected]> Co-authored-by: Aman Goel <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: mchadalavada <[email protected]> Co-authored-by: aishu-j <[email protected]> Co-authored-by: Zhe Zhou <[email protected]> Co-authored-by: zhezhouzz <[email protected]> Co-authored-by: Federico Mora Rocha <[email protected]> Co-authored-by: AD1024 <[email protected]> Co-authored-by: Mike He <[email protected]> Co-authored-by: AngAng <[email protected]> Co-authored-by: Mark Tuttle <[email protected]> Co-authored-by: Mark Tuttle <[email protected]> Co-authored-by: Muqsit Azeem <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
New features:
prove X using Y, which is equivalent torequires X, Y; ensures X; You can writeprove X using *which will put all invariants other than X to therequires. Similarly, you can writeprove *;which is equivalent to proving all invariants in one shot.verify()calls in Uclid5 are parallelized now; by default, it uses half the host machine's cores. You can specify the number of cores to use by passing-j <num cores>in the command line argument.LemmaandTheoremblock for bundling invariant declarations, which can be referred to in theprove X using YcommandsPlease see the example here
Other features:
provecommand in the example, you will get results look like this: