Skip to content

Commit

Permalink
add default that captures P's proof obligations
Browse files Browse the repository at this point in the history
  • Loading branch information
@FedericoAureliano
FedericoAureliano committed Nov 2, 2024
1 parent f27e546 commit 74999b4
Show file tree
Hide file tree
Showing 7 changed files with 91 additions and 29 deletions.
84 changes: 62 additions & 22 deletions Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ public void Compile(ICompilerConfiguration job)
List<string> failMessages = [];
HashSet<Invariant> succeededInv = [];
HashSet<Invariant> failedInv = [];
var missingDefault = true;

// Open database (or create if doesn't exist)
var db = new LiteDatabase(Path.Join(job.OutputDirectory.FullName, ".verifier-cache.db"));
Expand All @@ -62,7 +63,11 @@ public void Compile(ICompilerConfiguration job)

foreach (var cmd in _commands)
{
job.Output.WriteInfo($"Proof command: {cmd.Name}");
if (cmd.Name == "default")
{
missingDefault = false;
}
job.Output.WriteInfo($"Proving: {cmd.Name}");
Dictionary<string, bool> checklist = _proofCommandToFiles[cmd].ToDictionary(x => x, x => false);
Dictionary<string, Process> tasks = [];

Expand Down Expand Up @@ -93,6 +98,9 @@ public void Compile(ICompilerConfiguration job)
}
}
}

var numCompleted = checklist.Values.Sum(x => x ? 1 : 0);
Console.Write($"\r🔍 Checked {numCompleted}/{checklist.Count} goals...");

// fetch
while (checklist.ContainsValue(false))
Expand Down Expand Up @@ -150,8 +158,8 @@ public void Compile(ICompilerConfiguration job)
newTasks.ToList().ForEach(x => tasks.Add(x.Key, x.Value));
}

var numCompleted = checklist.Values.Sum(x => x ? 1 : 0);
Console.Write($"\r🔍 Verifying {numCompleted}/{checklist.Count} goals...");
numCompleted = checklist.Values.Sum(x => x ? 1 : 0);
Console.Write($"\r🔍 Checked {numCompleted}/{checklist.Count} goals...");
}

Console.WriteLine();
Expand All @@ -161,14 +169,18 @@ public void Compile(ICompilerConfiguration job)
job.Output.WriteInfo($"\n🎉 Verified {succeededInv.Count} invariants!");
foreach (var inv in succeededInv)
{
job.Output.WriteInfo($"✅ {inv.Name}");
job.Output.WriteInfo($"✅ {inv.Name.Replace("_PGROUP_", ": ")}");
}
if (!missingDefault && failMessages.Count == 0)
{
job.Output.WriteInfo($"✅ default P proof obligations");
}

MarkProvenInvariants(succeededInv);
ShowRemainings(job, failedInv);
ShowRemainings(job, failedInv, missingDefault);
if (failMessages.Count > 0)
{
job.Output.WriteInfo($"❌ Failed to verify {failMessages.Count} invariants!");
job.Output.WriteInfo($"❌ Failed to verify {failMessages.Count} properties!");
foreach (var msg in failMessages)
{
job.Output.WriteError(msg);
Expand All @@ -195,7 +207,7 @@ private void MarkProvenInvariants(HashSet<Invariant> succeededInv)
}
}

private void ShowRemainings(ICompilerConfiguration job, HashSet<Invariant> failedInv)
private void ShowRemainings(ICompilerConfiguration job, HashSet<Invariant> failedInv, bool missingDefault)
{
HashSet<Invariant> remaining = [];
foreach (var inv in _provenInvariants)
Expand All @@ -209,12 +221,17 @@ private void ShowRemainings(ICompilerConfiguration job, HashSet<Invariant> faile
}
}

if (remaining.Count > 0)
if (remaining.Count > 0 || missingDefault)
{
job.Output.WriteWarning("❓ Remaining Goals:");
foreach (var inv in remaining)
{
job.Output.WriteWarning($"- {inv.Name} at {GetLocation(inv)}");
job.Output.WriteWarning($"- {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(inv)}");
}

if (missingDefault)
{
job.Output.WriteWarning($"- default P proof obligations");
}
}
}
Expand All @@ -229,7 +246,7 @@ private void ProcessFailureMessages(List<Match> collection, string[] query, stri
var line = query[int.Parse(feedback.Second.ToString()) - 1];
var step = feedback.First.ToString().Contains("[Step #0]") ? "(base case)" : "";
var matchName = Regex.Match(line, @"// Failed to verify invariant (.*) at (.*)");
var invName = matchName.Groups[1].Value;
var invName = matchName.Groups[1].Value.Replace("_PGROUP_", ": ");
failedInv.Add(invName);
failMessages.Add($"{reason} {line.Split("//").Last()} {step}");
}
Expand Down Expand Up @@ -281,7 +298,7 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
_commands = [];
_globalScope = globalScope;
BuildDependencies(globalScope);
var filename_prefix = $"{job.ProjectName}_";
var filenamePrefix = $"{job.ProjectName}_";
List<CompiledFile> files = [];
if (!globalScope.ProofCommands.Any())
{
Expand All @@ -292,15 +309,29 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
};
_commands.Add(proof);
_proofCommandToFiles.Add(proof, []);
files.AddRange(CompileToFile($"{filename_prefix}default", proof, true));
files.AddRange(CompileToFile($"{filenamePrefix}default", proof, true, true, false));
}
else
{
foreach (var proofCmd in globalScope.ProofCommands)
{
_proofCommandToFiles.Add(proofCmd, []);
files.AddRange(CompileToFile($"{filename_prefix}{proofCmd.Name}", proofCmd, true, false));
_commands.Add(proofCmd);
if (proofCmd.Goals.Count == 1 && proofCmd.Goals[0].IsDefault)
{
var proof = new ProofCommand("default", null)
{
Goals = [],
Premises = proofCmd.Premises
};
_commands.Add(proof);
_proofCommandToFiles.Add(proof, []);
files.AddRange(CompileToFile($"{filenamePrefix}default", proof, true, true, true));
}
else
{
_proofCommandToFiles.Add(proofCmd, []);
files.AddRange(CompileToFile($"{filenamePrefix}{proofCmd.Name}", proofCmd, true, false, false));
_commands.Add(proofCmd);
}
}
}

Expand All @@ -325,7 +356,7 @@ private CompiledFile GenerateCompiledFile(ProofCommand cmd, string name, Machine
return file;
}

private List<CompiledFile> CompileToFile(string name, ProofCommand cmd, bool sanityCheck, bool handlerCheck = true)
private List<CompiledFile> CompileToFile(string name, ProofCommand cmd, bool sanityCheck, bool handlerCheck, bool builtin)
{
var machines = (from m in _globalScope.AllDecls.OfType<Machine>() where !m.IsSpec select m).ToList();
var events = _globalScope.AllDecls.OfType<PEvent>().ToList();
Expand All @@ -340,7 +371,7 @@ private List<CompiledFile> CompileToFile(string name, ProofCommand cmd, bool san
{
_src = GenerateCompiledFile(cmd, name, m, s, null);
files.Add(_src);
GenerateMain(m, s, null, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck);
GenerateMain(m, s, null, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck, builtin);
}

foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent && s.HasHandler(e)))
Expand All @@ -349,7 +380,7 @@ private List<CompiledFile> CompileToFile(string name, ProofCommand cmd, bool san
{
_src = GenerateCompiledFile(cmd, name, m, s, e);
files.Add(_src);
GenerateMain(m, s, e, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck);
GenerateMain(m, s, e, cmd.Goals, cmd.Premises, sanityCheck, handlerCheck, builtin);
}
}
}
Expand Down Expand Up @@ -950,9 +981,15 @@ private void GenerateSpecHandlers(List<Machine> specs)
/********************************
* Traverse the P AST and generate the UCLID5 code using the types and helpers defined above
*******************************/
private void GenerateMain(Machine machine, State state, PEvent @event, List<Invariant> goals,
List<Invariant> requires, bool generateSanityChecks, bool handlerCheck = true)
private void
GenerateMain(Machine machine, State state, PEvent @event, List<Invariant> goals,
List<Invariant> requires, bool generateSanityChecks, bool handlerCheck, bool builtin)
{
if (builtin)
{
goals = requires;
}

EmitLine("module main {");

var machines = (from m in _globalScope.AllDecls.OfType<Machine>() where !m.IsSpec select m).ToList();
Expand Down Expand Up @@ -1062,9 +1099,12 @@ private void GenerateMain(Machine machine, State state, PEvent @event, List<Inva

EmitLine("");

foreach (var inv in requires)
if (!builtin)
{
EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};");
foreach (var inv in requires)
{
EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};");
}
}

foreach (var inv in goals)
Expand Down
2 changes: 1 addition & 1 deletion Src/PCompiler/CompilerCore/Parser/PParser.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ invariantGroupDecl : LEMMA name=iden LBRACE invariantDecl* RBRACE

proofBlockDecl : PROOF LBRACE proofBody RBRACE ;
proofBody : proofItem* ;
proofItem : PROVE (targets+=expr (COMMA targets+=expr)* | goalsAll=MUL) (USING ((premises+=expr (COMMA premises+=expr)*) | premisesAll=MUL))? (EXCEPT excludes+=expr (COMMA excludes+=expr)*)? SEMI # ProveUsingCmd ;
proofItem : PROVE (targets+=expr (COMMA targets+=expr)* | goalsAll=MUL | goalsDefault=DEFAULT) (USING ((premises+=expr (COMMA premises+=expr)*) | premisesAll=MUL))? (EXCEPT excludes+=expr (COMMA excludes+=expr)*)? SEMI # ProveUsingCmd ;

typeDefDecl : TYPE name=iden SEMI # ForeignTypeDef
| TYPE name=iden ASSIGN type SEMI # PTypeDef
Expand Down
10 changes: 10 additions & 0 deletions Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Invariant.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,24 @@ public class Invariant : IPDecl
public Invariant(string name, IPExpr body, ParserRuleContext sourceNode)
{
Debug.Assert(sourceNode is PParser.InvariantDeclContext);
IsDefault = false;
Name = name;
Body = body;
SourceLocation = sourceNode;
}

public Invariant(ParserRuleContext sourceNode)
{
SourceLocation = sourceNode;
IsDefault = true;
Name = "defualt";
}

public IPExpr Body { get; set; }

public string Name { get; set; }

public bool IsDefault { get; }
public ParserRuleContext SourceLocation { get; }
}
}
4 changes: 2 additions & 2 deletions Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ public static void PopulateStubs(
public override object VisitInvariantDecl(PParser.InvariantDeclContext context)
{
var group = context.Parent as PParser.InvariantGroupDeclContext;
var name = group != null ? $"{group.name.GetText()}_{context.name.GetText()}": context.name.GetText();
var name = group != null ? $"{group.name.GetText()}_PGROUP_{context.name.GetText()}": context.name.GetText();
var decl = CurrentScope.Put(name, context);
nodesToDeclarations.Put(context, decl);
return null;
Expand All @@ -60,7 +60,7 @@ public override object VisitInvariantGroupDecl(PParser.InvariantGroupDeclContext

public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
{
var name = $"proof_cmd_{CurrentScope.ProofCommands.Count()}";
var name = string.Join(", ", context._targets.Select(t => t.GetText()));
var decl = CurrentScope.Put(name, context);
nodesToDeclarations.Put(context, decl);
return null;
Expand Down
10 changes: 9 additions & 1 deletion Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -732,14 +732,20 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
{
premises = CurrentScope.AllDecls.OfType<Invariant>().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList();
}
if (context.goalsAll == null)

if (context.goalsAll == null && context.goalsDefault == null)
{
goals = context._targets.Select(exprVisitor.Visit).ToList();
}
else if (context.goalsDefault != null)
{
goals = [new InvariantRefExpr(new Invariant(context), context)];
}
else
{
goals = CurrentScope.AllDecls.OfType<Invariant>().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList();
}

if (premises.Count == context._premises.Count)
{
proofCmd.Premises = premises.Zip(context._premises, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
Expand All @@ -748,6 +754,7 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
{
proofCmd.Premises = premises.SelectMany(x => ToInvariant(x, context)).ToList();
}

if (goals.Count == context._targets.Count)
{
proofCmd.Goals = goals.Zip(context._targets, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
Expand All @@ -756,6 +763,7 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
{
proofCmd.Goals = goals.SelectMany(x => ToInvariant(x, context)).ToList();
}

proofCmd.Excepts = excepts.Zip(context._excludes, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
// exclude things appear in `goals` from `premises`
proofCmd.Premises = proofCmd.Premises.Except(proofCmd.Goals).Except(proofCmd.Excepts).ToList();
Expand Down
3 changes: 3 additions & 0 deletions Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,9 @@ pure preference(m: machine, triple: krvTriple) : tVote;

pure subset(small: set[rvPair], large: set[rvPair]) : bool = forall (rv: rvPair) :: rv in small ==> rv in large;

// lets assume that there is at least one participant
axiom exists (x: machine) :: x in participants();

// assumptions about how the system is setup and the pure functions above
init coordinator() is Coordinator;
init forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2;
Expand Down
7 changes: 4 additions & 3 deletions Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ Lemma no_unexpected_messages {
invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2) == YES);

// supporting invariants, based on the Kondo paper
Lemma kondo_invs {
Lemma kondo {
invariant a1: forall (e: eVoteResp) :: inflight e ==> e.source in participants();
invariant a2: forall (e: eVoteResp) :: inflight e ==> e.vote == preference(e.source);
invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted;
Expand All @@ -118,7 +118,8 @@ Lemma kondo_invs {
}

Proof {
prove safety using kondo_invs;
prove safety using kondo;
prove no_unexpected_messages, system_config;
prove kondo_invs using no_unexpected_messages, system_config;
prove kondo using no_unexpected_messages, system_config;
prove default using no_unexpected_messages, system_config;
}

0 comments on commit 74999b4

Please sign in to comment.