Start to move PVerifier so that its ready to be merged into P3.0 #805

ankushdesai · 2024-12-03T20:48:11Z

No description provided.

* 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

…as prefix

… tutorial.

ankushdesai · 2024-12-03T20:50:04Z

Src/PCompiler/CompilerCore/Backend/TargetLanguage.cs

@@ -17,6 +18,7 @@ static TargetLanguage()
            RegisterCodeGenerator(CompilerOutput.Java, new JavaCompiler());
            RegisterCodeGenerator(CompilerOutput.Symbolic, new SymbolicCodeGenerator());
            RegisterCodeGenerator(CompilerOutput.Stately, new StatelyCodeGenerator());
+            RegisterCodeGenerator(CompilerOutput.Uclid5, new Uclid5CodeGenerator());


Lets rename this to PVerifier instead of UCLID5

ankushdesai · 2024-12-03T20:50:54Z

Src/PCompiler/CompilerCore/Backend/Uclid5/CompilationContext.cs

@@ -0,0 +1,11 @@
+namespace Plang.Compiler.Backend.Uclid5;


Can we please rename the entire folder Backend/Uclid5 to Backend/PVerifier

ankushdesai · 2024-12-03T20:52:43Z

Src/PCompiler/CompilerCore/Compiler.cs

@@ -67,7 +78,10 @@ public int Compile(ICompilerConfiguration job)
                var compiledFiles = job.Backend.GenerateCode(job, scope);
                foreach (var file in compiledFiles)
                {
-                    job.Output.WriteInfo($"Generated {file.FileName}.");
+                    if (entry != CompilerOutput.Uclid5)


Why are we not printing the generated files?

We generate many files, so instead of printing them all, we aggregate them.

For example for the 2pc tutorial, instead of printing out 88 file names, we would print:

Code generation for Uclid5... Generated 22 files for TwoPhaseCommitVerification_system_config Generated 22 files for TwoPhaseCommitVerification_kondo_using_system_config Generated 22 files for TwoPhaseCommitVerification_safety_using_kondo Generated 22 files for TwoPhaseCommitVerification_default Compiling generated code... Proving: system_config 🔍 Checked 22/22 goals... Proving: kondo using system_config 🔍 Checked 22/22 goals... Proving: safety using kondo 🔍 Checked 22/22 goals... Proving: default using system_config 🔍 Checked 22/22 goals...

ankushdesai · 2024-12-03T20:53:28Z

Src/PCompiler/CompilerCore/Compiler.cs

@@ -107,6 +121,40 @@ private static PParser.ProgramContext Parse(ICompilerConfiguration job, FileInfo
            var fileStream = new AntlrInputStream(fileText);
            var lexer = new PLexer(fileStream);
            var tokens = new CommonTokenStream(lexer);
+
+            if (!job.OutputLanguages.Contains(CompilerOutput.Uclid5))


ankushdesai · 2024-12-03T21:01:01Z

Src/PCompiler/CompilerCore/Parser/PLexer.g4

@@ -109,6 +129,7 @@ NONDET     : '$'  ;
 LNOT   : '!' ;
 LAND   : '&&' ;
 LOR    : '||' ;
+LTHEN  : '==>';


Do you think we can add <==> for IFF or add IFF as a keyword.

ankushdesai · 2024-12-03T21:02:48Z

Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs

@@ -70,7 +75,15 @@ public void AddLocalVariable(Variable local)
        {
            localVariables.Add(local);
        }
-
+        public void AddRequire(IPExpr expr)


I remember there were no issues with pure functions where a pure function must not refer to a machine field. Can we add a static check for this?

ankushdesai · 2024-12-03T21:04:09Z

Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/TestExpr.cs

+using Plang.Compiler.TypeChecker.AST.Declarations;
+using Plang.Compiler.TypeChecker.Types;
+
+namespace Plang.Compiler.TypeChecker.AST.Expressions


Can you remind me what is this for?

Why has this changed?

This is for algebraic data types. It is for testing what constructor was used to build a given ADT expression.

The PVerifier encoding uses ADTs for messages and machines. So, for example, if we have two different kinds of machines, A and B, then we would get an ADT like:

datatype machine := A | B;

Later, if we have some variable, x, of type machine, we can use test expressions to ask, e.g., "Is x an A machine?"

Thanks! Can we rename this to TestADTExpr to make this clearer? Thanks!

FedericoAureliano and others added 16 commits November 27, 2024 16:34

add install instructions for amazon linux

f28f1ce

add support for foreign functions with contracts and update one tutor…

8d40993

…ial to include an example

allow duplicate invariant names in different groups using group name …

21ea906

…as prefix

add caching using liteDB and md5 hash of uclid files

4f68d8c

fix bug in caching by simplifying process checklist

97b0570

fix bug in global procedures: always prepend self reference

479ed18

add default that captures P's proof obligations

d62226d

fix bug in file names

92a01ed

cleanup example for tutorial

45f5269

add 2pc verification tutorial

be3227b

pverifier backend and reorganize verification tutorials

80eed8b

init keyword -> init-condition keyword

c12d6a7

add error message when trying to use pverifier syntax for other backends

c26fc9b

move install instructions to docs and update link in 2pc verification…

446859b

… tutorial.

ankushdesai requested a review from FedericoAureliano December 3, 2024 20:48

ankushdesai commented Dec 3, 2024

View reviewed changes

FedericoAureliano added 3 commits December 5, 2024 10:26

rename uclid5 backend to pverifier

d01c547

remove unnecessary imports

0a92d4c

add iff symbol

07f2a06

ankushdesai merged commit 98c6ddf into dev_p3.0/pverifier Dec 10, 2024
8 checks passed

ankushdesai deleted the experimental/pverifier branch December 10, 2024 10:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Start to move PVerifier so that its ready to be merged into P3.0 #805

Start to move PVerifier so that its ready to be merged into P3.0 #805

ankushdesai commented Dec 3, 2024

ankushdesai Dec 3, 2024

ankushdesai Dec 3, 2024

ankushdesai Dec 3, 2024

FedericoAureliano Dec 5, 2024

ankushdesai Dec 3, 2024

ankushdesai Dec 3, 2024

ankushdesai Dec 3, 2024

ankushdesai Dec 3, 2024

ankushdesai Dec 3, 2024

FedericoAureliano Dec 5, 2024

ankushdesai Dec 10, 2024

Start to move PVerifier so that its ready to be merged into P3.0 #805

Start to move PVerifier so that its ready to be merged into P3.0 #805

Conversation

ankushdesai commented Dec 3, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment