From e93d4804f9d99150079728572c00a518af20a7c5 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 30 Jul 2015 12:04:16 -0700 Subject: Implement a Dafny server. The Dafny server is a command line utility that allows non-.Net editors to take advantage of Dafny's caching facilities, as used by the Dafny extension for Visual Studio. The server is essentially a REPL, which produces output in the same format as the Dafny CLI; clients thus do not need to understand the internals of Dafny's caching. A typical editing session proceeds as follows: * When a new Dafny file is opened, the editor starts a new instance of the Dafny server. The cache is blank at that point. * The editor sends a copy of the buffer for initial verification. This takes some time, after which the server returns a list of errors. * The user makes modifications; the editor periodically sends a new copy of the buffer's contents to the Dafny server, which quickly returns an updated list of errors. The client-server protocol is sequential, uses JSON, and works over ASCII pipes by base64-encoding queries. It defines one type of query, and two types of responses: Queries are of the following form: verify [[DAFNY-CLIENT: EOM]] Responses are of the following form: [SUCCESS] [[DAFNY-SERVER: EOM]] or [FAILURE] [[DAFNY-SERVER: EOM]] The JSON payload is an array with 4 fields: * args: An array of Dafny arguments, as passed to the Dafny CLI * source: A Dafny program, or the path to a Dafny source file. * sourceIsFile: A boolean indicating whether the 'source' argument is a Dafny program or the path to one. * filename: The name of the original source file, to be used in error messages For small files, embedding the Dafny source directly into a message is convenient; for larger files, however, it is generally better for performance to write the source snapshot to a separate file, and to pass that to Dafny by setting the 'sourceIsFile' flag to true. --- Source/DafnyServer/Server.cs | 269 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 269 insertions(+) create mode 100644 Source/DafnyServer/Server.cs (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs new file mode 100644 index 00000000..36c28627 --- /dev/null +++ b/Source/DafnyServer/Server.cs @@ -0,0 +1,269 @@ +using System; +using System.IO; +using System.Text; +using System.Collections.Generic; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; + +using Dafny = Microsoft.Dafny; +using Bpl = Microsoft.Boogie; +using Microsoft.Boogie; + +namespace Microsoft.Dafny { + class Interaction { + internal static string SUCCESS = "SUCCESS"; + internal static string FAILURE = "FAILURE"; + internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]"; + internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]"; + + internal static void EOM(string header, string msg) { + var trailer = (msg == null) ? "" : "\n"; + Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG); + Console.Out.Flush(); + } + + internal static void EOM(string header, Exception ex, string subHeader="") { + var aggregate = ex as AggregateException; + subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " "; + + if (aggregate == null) { + EOM(header, subHeader + ex.Message); + } else { + EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); + } + } + } + + // FIXME: This should not be duplicated here + class DafnyConsolePrinter : ConsolePrinter { + public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { + // Dafny has 0-indexed columns, but Boogie counts from 1 + var realigned_tok = new Token(tok.line, tok.col - 1); + realigned_tok.kind = tok.kind; + realigned_tok.pos = tok.pos; + realigned_tok.val = tok.val; + realigned_tok.filename = tok.filename; + base.ReportBplError(realigned_tok, message, error, tw, category); + + if (tok is Dafny.NestedToken) { + var nt = (Dafny.NestedToken)tok; + ReportBplError(nt.Inner, "Related location", false, tw); + } + } + } + + [Serializable] + class VerificationTask { + [DataMember] + string[] args = null; + + [DataMember] + string filename = null; + + [DataMember] + string source = null; + + [DataMember] + bool sourceIsFile = false; + + string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } + + internal static VerificationTask ReadTask(string b64_repr) { + try { + var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); + using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { + DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); + return (VerificationTask)serializer.ReadObject(ms); + } + } catch (Exception ex) { + throw new ServerException("Deserialization failed: {0}.", ex.Message); + } + } + + internal static void SelfTest() { + var task = new VerificationTask() { + filename = "", + sourceIsFile = false, + args = new string[] { }, + source = "method selftest() { assert true; }" + }; + try { + task.Run(); + Interaction.EOM(Interaction.SUCCESS, null); + } catch (Exception ex) { + Interaction.EOM(Interaction.FAILURE, ex); + } + } + + internal void Run() { + Server.ApplyArgs(args); + new DafnyHelper(filename, ProgramSource).Verify(); + } + } + + class ServerException : Exception { + internal ServerException(string message) : base(message) { } + internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } + } + + class Server { + private bool running; + + static void Main(string[] args) { + Server server = new Server(); + if (args.Length > 0) { + if (args[0] == "selftest") { + VerificationTask.SelfTest(); + } else { + Console.WriteLine("Not sure what to do with '{0}'", String.Join(" ", args)); + } + } else { + server.Loop(); + } + } + + public Server() { + this.running = true; + Console.CancelKeyPress += this.CancelKeyPress; + ExecutionEngine.printer = new DafnyConsolePrinter(); + } + + internal static void ApplyArgs(string[] args) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + if (CommandLineOptions.Clo.Parse(args)) { + // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME + // Dafny.DafnyOptions.O.ModelViewFile = "-"; + Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.VerifySnapshots = 2; + } else { + throw new ServerException("Invalid command line options"); + } + } + + void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { + e.Cancel = true; + // FIXME TerminateProver and RunningProverFromCommandLine + // Cancel the current verification? TerminateProver() ? Or kill entirely? + } + + static bool EndOfPayload(out string line) { + line = Console.ReadLine(); + return line == null || line == Interaction.CLIENT_EOM_TAG; + } + + static string ReadPayload() { + StringBuilder buffer = new StringBuilder(); + string line = null; + while (!EndOfPayload(out line)) { + buffer.Append(line); + } + return buffer.ToString(); + } + + void Loop() { + for (int cycle = 0; running; cycle++) { + var line = Console.ReadLine() ?? "quit"; + var command = line.Split(); + Respond(command); + } + } + + void Respond(string[] command) { + try { + if (command.Length == 0) { + throw new ServerException("Empty command"); + } + + var verb = command[0]; + if (verb == "verify") { + checkArgs(command, 0); + var payload = ReadPayload(); + VerificationTask.ReadTask(payload).Run(); + } else if (verb == "quit") { + checkArgs(command, 0); + Exit(); + } else { + throw new ServerException("Unknown verb '{0}'", verb); + } + + Interaction.EOM(Interaction.SUCCESS, "Verification completed successfully!"); + } catch (ServerException ex) { + Interaction.EOM(Interaction.FAILURE, ex); + } catch (Exception ex) { + Interaction.EOM(Interaction.FAILURE, ex, "[FATAL]"); + running = false; + } + } + + void checkArgs(string[] command, int expectedLength) { + if (command.Length - 1 != expectedLength) { + throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength); + } + } + + void Exit() { + this.running = false; + } + } + + class DafnyHelper { + private string fname; + private string source; + + private Dafny.Errors errors; + private Dafny.Program dafnyProgram; + private Bpl.Program boogieProgram; + + public DafnyHelper(string fname, string source) { + this.fname = fname; + this.source = source; + this.errors = new Dafny.Errors(); + } + + public bool Verify() { + return Parse() && Resolve() && Translate() && Boogie(); + } + + private bool Parse() { + Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); + Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); + var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && + Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); + if (success) { + dafnyProgram = new Dafny.Program(fname, module, builtIns); + } + return success; + } + + private bool Resolve() { + var resolver = new Dafny.Resolver(dafnyProgram); + resolver.ResolveProgram(dafnyProgram); + return resolver.ErrorCount == 0; + } + + private bool Translate() { + var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix + boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? + return true; + } + + // FIXME var boogieFilename = Path.Combine(Path.GetTempPath(), Path.ChangeExtension(Path.GetFileName(fname), "bpl")); + private bool Boogie() { + if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { + ExecutionEngine.EliminateDeadVariables(boogieProgram); + ExecutionEngine.CollectModSets(boogieProgram); + ExecutionEngine.CoalesceBlocks(boogieProgram); + ExecutionEngine.Inline(boogieProgram); + + switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), null, null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for programId and error delegate + case PipelineOutcome.Done: + case PipelineOutcome.VerificationCompleted: + return true; + } + } + + return false; + } + } +} \ No newline at end of file -- cgit v1.2.3 From 48fed349a2fc592e7f015ecaa6cf98582446278f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 30 Jul 2015 17:43:13 -0700 Subject: Fix an issue where the server would reverify the same file multiple times. The confusing part here is that if one passes null as the ProgramId for two consecutive calls to Boogie, then Boogie will return the same results twice, regardless of what the second program was. --- Source/DafnyServer/Server.cs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 36c28627..660188ba 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -114,6 +114,9 @@ namespace Microsoft.Dafny { if (args.Length > 0) { if (args[0] == "selftest") { VerificationTask.SelfTest(); + } else if (File.Exists(args[0])) { + Console.SetIn(new StreamReader(args[0])); + server.Loop(); } else { Console.WriteLine("Not sure what to do with '{0}'", String.Join(" ", args)); } @@ -248,15 +251,14 @@ namespace Microsoft.Dafny { return true; } - // FIXME var boogieFilename = Path.Combine(Path.GetTempPath(), Path.ChangeExtension(Path.GetFileName(fname), "bpl")); private bool Boogie() { - if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { + if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? ExecutionEngine.EliminateDeadVariables(boogieProgram); ExecutionEngine.CollectModSets(boogieProgram); ExecutionEngine.CoalesceBlocks(boogieProgram); ExecutionEngine.Inline(boogieProgram); - switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), null, null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for programId and error delegate + switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate case PipelineOutcome.Done: case PipelineOutcome.VerificationCompleted: return true; -- cgit v1.2.3 From 990966db7dcea00045c5c104ded084348e8f7dde Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 14:26:53 -0700 Subject: Split the server source into multiple files --- Source/DafnyServer/DafnyHelper.cs | 87 ++++++++++++++ Source/DafnyServer/DafnyServer.csproj | 7 +- Source/DafnyServer/Server.cs | 202 +++------------------------------ Source/DafnyServer/Utilities.cs | 60 ++++++++++ Source/DafnyServer/VerificationTask.cs | 59 ++++++++++ 5 files changed, 227 insertions(+), 188 deletions(-) create mode 100644 Source/DafnyServer/DafnyHelper.cs create mode 100644 Source/DafnyServer/Utilities.cs create mode 100644 Source/DafnyServer/VerificationTask.cs (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs new file mode 100644 index 00000000..10d98677 --- /dev/null +++ b/Source/DafnyServer/DafnyHelper.cs @@ -0,0 +1,87 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; +using Bpl = Microsoft.Boogie; + +namespace Microsoft.Dafny { + // FIXME: This should not be duplicated here + class DafnyConsolePrinter : ConsolePrinter { + public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { + // Dafny has 0-indexed columns, but Boogie counts from 1 + var realigned_tok = new Token(tok.line, tok.col - 1); + realigned_tok.kind = tok.kind; + realigned_tok.pos = tok.pos; + realigned_tok.val = tok.val; + realigned_tok.filename = tok.filename; + base.ReportBplError(realigned_tok, message, error, tw, category); + + if (tok is Dafny.NestedToken) { + var nt = (Dafny.NestedToken)tok; + ReportBplError(nt.Inner, "Related location", false, tw); + } + } + } + + class DafnyHelper { + private string fname; + private string source; + + private Dafny.Errors errors; + private Dafny.Program dafnyProgram; + private Bpl.Program boogieProgram; + + public DafnyHelper(string fname, string source) { + this.fname = fname; + this.source = source; + this.errors = new Dafny.Errors(); + } + + public bool Verify() { + return Parse() && Resolve() && Translate() && Boogie(); + } + + private bool Parse() { + Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); + Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); + var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && + Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); + if (success) { + dafnyProgram = new Dafny.Program(fname, module, builtIns); + } + return success; + } + + private bool Resolve() { + var resolver = new Dafny.Resolver(dafnyProgram); + resolver.ResolveProgram(dafnyProgram); + return resolver.ErrorCount == 0; + } + + private bool Translate() { + var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix + boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? + return true; + } + + private bool Boogie() { + if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? + ExecutionEngine.EliminateDeadVariables(boogieProgram); + ExecutionEngine.CollectModSets(boogieProgram); + ExecutionEngine.CoalesceBlocks(boogieProgram); + ExecutionEngine.Inline(boogieProgram); + + switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate + case PipelineOutcome.Done: + case PipelineOutcome.VerificationCompleted: + return true; + } + } + + return false; + } + } +} diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 0aac88b2..3da33f16 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -1,4 +1,4 @@ - + @@ -55,6 +55,9 @@ + + + @@ -72,4 +75,4 @@ --> - + \ No newline at end of file diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 660188ba..c6f619d3 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -10,116 +10,21 @@ using Bpl = Microsoft.Boogie; using Microsoft.Boogie; namespace Microsoft.Dafny { - class Interaction { - internal static string SUCCESS = "SUCCESS"; - internal static string FAILURE = "FAILURE"; - internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]"; - internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]"; - - internal static void EOM(string header, string msg) { - var trailer = (msg == null) ? "" : "\n"; - Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG); - Console.Out.Flush(); - } - - internal static void EOM(string header, Exception ex, string subHeader="") { - var aggregate = ex as AggregateException; - subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " "; - - if (aggregate == null) { - EOM(header, subHeader + ex.Message); - } else { - EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); - } - } - } - - // FIXME: This should not be duplicated here - class DafnyConsolePrinter : ConsolePrinter { - public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { - // Dafny has 0-indexed columns, but Boogie counts from 1 - var realigned_tok = new Token(tok.line, tok.col - 1); - realigned_tok.kind = tok.kind; - realigned_tok.pos = tok.pos; - realigned_tok.val = tok.val; - realigned_tok.filename = tok.filename; - base.ReportBplError(realigned_tok, message, error, tw, category); - - if (tok is Dafny.NestedToken) { - var nt = (Dafny.NestedToken)tok; - ReportBplError(nt.Inner, "Related location", false, tw); - } - } - } - - [Serializable] - class VerificationTask { - [DataMember] - string[] args = null; - - [DataMember] - string filename = null; - - [DataMember] - string source = null; - - [DataMember] - bool sourceIsFile = false; - - string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } - - internal static VerificationTask ReadTask(string b64_repr) { - try { - var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); - using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { - DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); - return (VerificationTask)serializer.ReadObject(ms); - } - } catch (Exception ex) { - throw new ServerException("Deserialization failed: {0}.", ex.Message); - } - } - - internal static void SelfTest() { - var task = new VerificationTask() { - filename = "", - sourceIsFile = false, - args = new string[] { }, - source = "method selftest() { assert true; }" - }; - try { - task.Run(); - Interaction.EOM(Interaction.SUCCESS, null); - } catch (Exception ex) { - Interaction.EOM(Interaction.FAILURE, ex); - } - } - - internal void Run() { - Server.ApplyArgs(args); - new DafnyHelper(filename, ProgramSource).Verify(); - } - } - - class ServerException : Exception { - internal ServerException(string message) : base(message) { } - internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } - } - class Server { private bool running; static void Main(string[] args) { Server server = new Server(); - if (args.Length > 0) { - if (args[0] == "selftest") { - VerificationTask.SelfTest(); - } else if (File.Exists(args[0])) { - Console.SetIn(new StreamReader(args[0])); - server.Loop(); - } else { - Console.WriteLine("Not sure what to do with '{0}'", String.Join(" ", args)); - } + + var hasArg = args.Length > 0; + var arg = hasArg ? args[0] : null; + + if (hasArg && args[0] == "selftest") { + VerificationTask.SelfTest(); + } else if (hasArg && File.Exists(arg)) { + Console.WriteLine("# Reading from {0}", arg); + Console.SetIn(new StreamReader(arg)); + server.Loop(); } else { server.Loop(); } @@ -131,19 +36,6 @@ namespace Microsoft.Dafny { ExecutionEngine.printer = new DafnyConsolePrinter(); } - internal static void ApplyArgs(string[] args) { - Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); - if (CommandLineOptions.Clo.Parse(args)) { - // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME - // Dafny.DafnyOptions.O.ModelViewFile = "-"; - Dafny.DafnyOptions.O.ProverKillTime = 10; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); - Dafny.DafnyOptions.O.VerifySnapshots = 2; - } else { - throw new ServerException("Invalid command line options"); - } - } - void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine @@ -167,8 +59,10 @@ namespace Microsoft.Dafny { void Loop() { for (int cycle = 0; running; cycle++) { var line = Console.ReadLine() ?? "quit"; - var command = line.Split(); - Respond(command); + if (line != String.Empty && !line.StartsWith("#")) { + var command = line.Split(); + Respond(command); + } } } @@ -180,11 +74,11 @@ namespace Microsoft.Dafny { var verb = command[0]; if (verb == "verify") { - checkArgs(command, 0); + ServerUtils.checkArgs(command, 0); var payload = ReadPayload(); VerificationTask.ReadTask(payload).Run(); } else if (verb == "quit") { - checkArgs(command, 0); + ServerUtils.checkArgs(command, 0); Exit(); } else { throw new ServerException("Unknown verb '{0}'", verb); @@ -199,73 +93,9 @@ namespace Microsoft.Dafny { } } - void checkArgs(string[] command, int expectedLength) { - if (command.Length - 1 != expectedLength) { - throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength); - } - } - void Exit() { this.running = false; } } - class DafnyHelper { - private string fname; - private string source; - - private Dafny.Errors errors; - private Dafny.Program dafnyProgram; - private Bpl.Program boogieProgram; - - public DafnyHelper(string fname, string source) { - this.fname = fname; - this.source = source; - this.errors = new Dafny.Errors(); - } - - public bool Verify() { - return Parse() && Resolve() && Translate() && Boogie(); - } - - private bool Parse() { - Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); - Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); - var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && - Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); - if (success) { - dafnyProgram = new Dafny.Program(fname, module, builtIns); - } - return success; - } - - private bool Resolve() { - var resolver = new Dafny.Resolver(dafnyProgram); - resolver.ResolveProgram(dafnyProgram); - return resolver.ErrorCount == 0; - } - - private bool Translate() { - var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix - boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? - return true; - } - - private bool Boogie() { - if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? - ExecutionEngine.EliminateDeadVariables(boogieProgram); - ExecutionEngine.CollectModSets(boogieProgram); - ExecutionEngine.CoalesceBlocks(boogieProgram); - ExecutionEngine.Inline(boogieProgram); - - switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate - case PipelineOutcome.Done: - case PipelineOutcome.VerificationCompleted: - return true; - } - } - - return false; - } - } } \ No newline at end of file diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs new file mode 100644 index 00000000..8fb03b05 --- /dev/null +++ b/Source/DafnyServer/Utilities.cs @@ -0,0 +1,60 @@ +using System; +using System.IO; +using System.Text; +using System.Collections.Generic; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using Microsoft.Boogie; + +namespace Microsoft.Dafny { + class Interaction { + internal static string SUCCESS = "SUCCESS"; + internal static string FAILURE = "FAILURE"; + internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]"; + internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]"; + + internal static void EOM(string header, string msg) { + var trailer = (msg == null) ? "" : "\n"; + Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG); + Console.Out.Flush(); + } + + internal static void EOM(string header, Exception ex, string subHeader = "") { + var aggregate = ex as AggregateException; + subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " "; + + if (aggregate == null) { + EOM(header, subHeader + ex.Message); + } else { + EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); + } + } + } + + class ServerException : Exception { + internal ServerException(string message) : base(message) { } + internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } + } + + class ServerUtils { + internal static void checkArgs(string[] command, int expectedLength) { + if (command.Length - 1 != expectedLength) { + throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength); + } + } + + internal static void ApplyArgs(string[] args) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + + if (CommandLineOptions.Clo.Parse(args)) { + // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME + // Dafny.DafnyOptions.O.ModelViewFile = "-"; + Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.VerifySnapshots = 2; + } else { + throw new ServerException("Invalid command line options"); + } + } + } +} diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs new file mode 100644 index 00000000..a00688b1 --- /dev/null +++ b/Source/DafnyServer/VerificationTask.cs @@ -0,0 +1,59 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using System.Text; +using System.Threading.Tasks; + +namespace Microsoft.Dafny { + [Serializable] + class VerificationTask { + [DataMember] + string[] args = null; + + [DataMember] + string filename = null; + + [DataMember] + string source = null; + + [DataMember] + bool sourceIsFile = false; + + string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } + + internal static VerificationTask ReadTask(string b64_repr) { + try { + var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); + using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { + DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); + return (VerificationTask)serializer.ReadObject(ms); + } + } catch (Exception ex) { + throw new ServerException("Deserialization failed: {0}.", ex.Message); + } + } + + internal static void SelfTest() { + var task = new VerificationTask() { + filename = "", + sourceIsFile = false, + args = new string[] { }, + source = "method selftest() { assert true; }" + }; + try { + task.Run(); + Interaction.EOM(Interaction.SUCCESS, null); + } catch (Exception ex) { + Interaction.EOM(Interaction.FAILURE, ex); + } + } + + internal void Run() { + ServerUtils.ApplyArgs(args); + new DafnyHelper(filename, ProgramSource).Verify(); + } + } +} -- cgit v1.2.3 From 65334f8f33c92a1e37376d6484d60ee45b55ca1d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 15:11:03 -0700 Subject: Add tests for the server --- Source/DafnyServer/Server.cs | 2 +- Test/lit.site.cfg | 8 + Test/runTests.py | 89 ++-- Test/server/simple-session.transcript | 637 +++++++++++++++++++++++++++ Test/server/simple-session.transcript.expect | 299 +++++++++++++ 5 files changed, 1000 insertions(+), 35 deletions(-) create mode 100644 Test/server/simple-session.transcript create mode 100644 Test/server/simple-session.transcript.expect (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index c6f619d3..74cdd8c2 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -22,7 +22,7 @@ namespace Microsoft.Dafny { if (hasArg && args[0] == "selftest") { VerificationTask.SelfTest(); } else if (hasArg && File.Exists(arg)) { - Console.WriteLine("# Reading from {0}", arg); + Console.WriteLine("# Reading from {0}", Path.GetFileName(arg)); Console.SetIn(new StreamReader(arg)); server.Loop(); } else { diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index a960bdbc..c5718f86 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -79,14 +79,21 @@ lit_config.note('Repository root is {}'.format(repositoryRoot)) binaryDir = os.path.join( repositoryRoot, 'Binaries') dafnyExecutable = os.path.join( binaryDir, 'Dafny.exe') +serverExecutable = os.path.join( binaryDir, 'DafnyServer.exe') if not os.path.exists(dafnyExecutable): lit_config.fatal('Could not find Dafny.exe at {}'.format(dafnyExecutable)) +if not os.path.exists(serverExecutable): + lit_config.warning('Could not find DafnyServer.exe at {}'.format(serverExecutable)) +else: + config.suffixes.append('.transcript') + dafnyExecutable = quotePath(dafnyExecutable) if os.name == 'posix': dafnyExecutable = 'mono ' + dafnyExecutable + serverExecutable = 'mono ' + serverExecutable if lit.util.which('mono') == None: lit_config.fatal('Cannot find mono. Make sure it is your PATH') @@ -105,6 +112,7 @@ if len(dafnyParams) > 0: lit_config.note('Using Dafny: {}\n'.format(dafnyExecutable)) config.substitutions.append( ('%dafny', dafnyExecutable) ) +config.substitutions.append( ('%server', serverExecutable) ) # Sanity check: Check solver executable is available # FIXME: Should this check be removed entirely? diff --git a/Test/runTests.py b/Test/runTests.py index fc9c20e7..ebdb0655 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -38,6 +38,7 @@ class Defaults: DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:300"] + EXTENSIONS = [".dfy", ".transcript"] class Colors: RED = '\033[91m' @@ -103,7 +104,6 @@ class Test: def __init__(self, name, source_path, cmds, timeout, compiler_id = 0): self.name = name - self.dfy = None if self.name is None else (self.name + ".dfy") self.source_path = Test.uncygdrive(source_path) self.expect_path = Test.source_to_expect_path(self.source_path) self.source_directory, self.fname = os.path.split(self.source_path) @@ -182,7 +182,7 @@ class Test: debug(Debug.REPORT, "{} of {}".format(len(tests), len(results)), headers=status) if status != TestStatus.PASSED: for test in tests: - debug(Debug.REPORT, "* " + test.dfy, headers=status, silentheaders=True) + debug(Debug.REPORT, "* " + test.name, headers=status, silentheaders=True) debug(Debug.REPORT) @@ -190,14 +190,14 @@ class Test: if failing: with open("failing.lst", mode='w') as writer: for t in failing: - writer.write("{}\t{}\n".format(t.name, t.source_path)) + writer.write("{}\n".format(t.name)) debug(Debug.REPORT, "Some tests failed: use [runTests.py failing.lst] to rerun the failing tests") debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs)) def run(self): - debug(Debug.DEBUG, "Starting {}".format(self.dfy)) + debug(Debug.DEBUG, "Starting {}".format(self.name)) os.makedirs(self.temp_directory, exist_ok=True) # os.chdir(self.source_directory) @@ -227,7 +227,7 @@ class Test: stdout, stderr = stdout.strip(), stderr.strip() if stdout != b"" or stderr != b"": - debug(Debug.TRACE, "Writing the output of {} to {}".format(self.dfy, self.temp_output_path)) + debug(Debug.TRACE, "Writing the output of {} to {}".format(self.name, self.temp_output_path)) with open(self.temp_output_path, mode='ab') as writer: writer.write(stdout + stderr) if stderr != b"": @@ -249,7 +249,7 @@ class Test: fstring = "[{:5.2f}s] {} ({}{})" progress = "{}/{}".format(tid, len(alltests)) - message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), + message = fstring.format(self.duration, wrap_color(self.name, Colors.BRIGHT), wrap_color(progress, Colors.BRIGHT), running) debug(Debug.INFO, message, headers=self.status) @@ -275,7 +275,7 @@ def setup_parser(): parser = argparse.ArgumentParser(description='Run the Dafny test suite.') parser.add_argument('path', type=str, action='store', nargs='+', - help='Input files or folders. Folders are searched for .dfy files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') + help='Input files or folders. Folders are searched for test files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') parser.add_argument('--compiler', type=str, action='append', default=None, help='Dafny executable. Default: {}'.format(Defaults.DAFNY_BIN)) @@ -293,11 +293,14 @@ def setup_parser(): help='Excluded directories. {} are automatically added.'.format(Defaults.ALWAYS_EXCLUDED)) parser.add_argument('--verbosity', action='store', type=int, default=1, - help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info.') + help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info; 3: Trace.') parser.add_argument('-v', action='store_const', default=1, dest="verbosity", const=2, help='Short for --verbosity 2.') + parser.add_argument('-vv', action='store_const', default=1, dest="verbosity", const=3, + help='Short for --verbosity 3.') + parser.add_argument('--report', '-r', action='store', type=str, default=None, help='Give an explicit name to the report file. Defaults to the current date and time.') @@ -339,7 +342,7 @@ def run_one_internal(test, test_id, args, running): # ignore further work once you receive a kill signal KILLED = True except Exception as e: - debug(Debug.ERROR, "[{}] {}".format(test.dfy, e)) + debug(Debug.ERROR, "[{}] {}".format(test.name, e)) test.status = TestStatus.UNKNOWN finally: running.remove(test_id) @@ -349,53 +352,71 @@ def run_one_internal(test, test_id, args, running): def run_one(args): return run_one_internal(*args) -def read_one_test(name, fname, compiler_cmds, timeout): +def get_server_path(compiler): + REGEXP = r"\bDafny.exe\b.*" + if re.search(REGEXP, compiler): + return re.sub(REGEXP, "DafnyServer.exe", compiler) + else: + return None + +def substitute_binaries(cmd, compiler): + cmd = cmd.replace("%dafny", compiler) + cmd = cmd.replace("%server", get_server_path(compiler)) + return cmd + +def read_one_test(fname, compiler_cmds, timeout): for cid, compiler_cmd in enumerate(compiler_cmds): source_path = os.path.realpath(fname) with open(source_path, mode='r') as reader: cmds = [] for line in reader: line = line.strip() - match = re.match("^// *RUN: *(?!%diff)([^ ].*)$", line) + match = re.match("^[/# ]*RUN: *(?!%diff)([^ ].*)$", line) if match: - cmds.append(match.groups()[0].replace("%dafny", compiler_cmd)) + debug(Debug.TRACE, "Found RUN spec: {}".format(line)) + cmds.append(substitute_binaries(match.groups()[0], compiler_cmd)) else: break if cmds: - yield Test(name, source_path, cmds, timeout, cid) + yield Test(fname, source_path, cmds, timeout, cid) else: - debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) + debug(Debug.WARNING, "Test file {} has no RUN specification".format(fname)) -def find_one(name, fname, compiler_cmds, timeout, allow_lst=False): - name, ext = os.path.splitext(fname) - if ext == ".dfy": +def find_one(fname, compiler_cmds, timeout): + _, ext = os.path.splitext(fname) + if ext in Defaults.EXTENSIONS: if os.path.exists(fname): debug(Debug.TRACE, "Found test file: {}".format(fname)) - yield from read_one_test(name, fname, compiler_cmds, timeout) + yield from read_one_test(fname, compiler_cmds, timeout) else: debug(Debug.ERROR, "Test file {} not found".format(fname)) - elif ext == ".lst" and allow_lst: #lst files are only read if explicitly listed on the CLI - debug(Debug.INFO, "Loading tests from {}".format(fname)) - with open(fname) as reader: - for line in reader: - _name, _path = line.strip().split() - yield from find_one(_name, _path, compiler_cmds, timeout) else: debug(Debug.TRACE, "Ignoring {}".format(fname)) -def find_tests(paths, compiler_cmds, excluded, timeout): +def expand_lsts(paths): for path in paths: + _, ext = os.path.splitext(path) + if ext == ".lst": #lst files are only read if explicitly listed on the CLI + debug(Debug.INFO, "Loading tests from {}".format(path)) + with open(path) as reader: + for line in reader: + _path = line.strip() + yield _path + else: + yield path + +def find_tests(paths, compiler_cmds, excluded, timeout): + for path in expand_lsts(paths): if os.path.isdir(path): debug(Debug.TRACE, "Searching for tests in {}".format(path)) for base, dirnames, fnames in os.walk(path): dirnames[:] = [d for d in dirnames if d not in excluded] for fname in fnames: - yield from find_one(fname, os.path.join(base, fname), compiler_cmds, timeout) + yield from find_one(os.path.join(base, fname), compiler_cmds, timeout) else: - yield from find_one(path, path, compiler_cmds, timeout, True) - + yield from find_one(path, compiler_cmds, timeout) def run_tests(args): if args.compiler is None: @@ -404,12 +425,15 @@ def run_tests(args): args.base_flags = Defaults.FLAGS for compiler in args.compiler: + server = get_server_path(compiler) if not os.path.exists(compiler): debug(Debug.ERROR, "Compiler not found: {}".format(compiler)) return + if not os.path.exists(server): + debug(Debug.WARNING, "Server not found") tests = list(find_tests(args.path, [compiler + ' ' + " ".join(args.base_flags + args.flags) - for compiler in args.compiler], + for compiler in args.compiler], args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) @@ -447,10 +471,7 @@ def run_tests(args): def diff(paths, accept, difftool): - for path in paths: - if not path.endswith(".dfy"): - path += ".dfy" - + for path in expand_lsts(paths): if not os.path.exists(path): debug(Debug.ERROR, "Not found: {}".format(path)) else: @@ -470,7 +491,7 @@ def compare_results(globs, time_all): from glob import glob paths = [path for g in globs for path in glob(g)] reports = {path: Test.load_report(path) for path in paths} - resultsets = {path: {test.dfy: (test.status, test.duration) for test in report} + resultsets = {path: {test.name: (test.status, test.duration) for test in report} for path, report in reports.items()} all_tests = set(name for resultset in resultsets.values() for name in resultset.keys()) diff --git a/Test/server/simple-session.transcript b/Test/server/simple-session.transcript new file mode 100644 index 00000000..26539267 --- /dev/null +++ b/Test/server/simple-session.transcript @@ -0,0 +1,637 @@ +# RUN: %server "%s" > "%t" +# RUN: %diff "%s.expect" "%t" +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG4gfVxuIiwi +c291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG4iLCJzb3VyY2VJc0ZpbGUiOmZh +bHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7Iiwic291 +cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gICIs +InNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG59Iiwi +c291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG5cbn0i +LCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHhc +bn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +clxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFs +c2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg +e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp +bGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg +e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp +bGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIs +InNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj +ZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj +ZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4J2ludCwgeCcgKiB4JyA+IDA7XG59Iiwic291cmNlSXNG +aWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50LCB4JyAqIHgnID4gMDtcbn0iLCJzb3VyY2VJ +c0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6ICwgeCcgKiB4JyA+IDA7XG59Iiwic291 +cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPiAwO1xufSIsInNvdXJj +ZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbn0iLCJzb3Vy +Y2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgXG59Iiwi +c291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzXG59 +Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIs +InNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNl +fQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTScodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0 +ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9y +YWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5z +dGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAx +O1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4 +JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0 +KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAz +O1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAq +IHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnID49IDA7XG4gIGFzc2Vy +dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnICAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDwgMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy +dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIFxuICBh +c3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu +ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy +XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu +ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect new file mode 100644 index 00000000..89c3351d --- /dev/null +++ b/Test/server/simple-session.transcript.expect @@ -0,0 +1,299 @@ +# Reading from simple-session.transcript +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,13): Error: rbrace expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(6,2): Error: rbrace expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,0): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,0): Error: ident expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(6,2): Error: EOF expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(6,2): Error: EOF expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(11,0): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(11,0): Error: semi expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(11,0): Error: invalid UnaryExpression +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,25): Error: openparen expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,25): Error: openparen expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,26): Error: invalid QSep +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,28): Error: invalid QSep +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,27): Error: invalid UnaryExpression +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(12,0): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +transcript(33,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,14): Error: Duplicate member name: M +transcript(33,14): Error: Duplicate member name: M +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(38,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(38,38): Error: semi expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(38,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,2): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,2): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,2): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,9): Error: invalid AssertStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,9): Error: invalid AssertStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,9): Error: unresolved identifier: fal +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] -- cgit v1.2.3 From 4b3fc0e7413424e27131dd8dd919423711f097ad Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 08:46:35 -0700 Subject: Use a nice warning symbol in some warning messages This is useful because trigger-related messages can contain quite a bit of information, especially if they include info about multiple split quantifiers. --- Source/Dafny/DafnyOptions.cs | 1 + Source/Dafny/Triggers/QuantifiersCollection.cs | 58 +++++++++++++++----------- Source/DafnyServer/Server.cs | 4 +- Source/DafnyServer/Utilities.cs | 5 ++- 4 files changed, 40 insertions(+), 28 deletions(-) (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 66cf639f..245632ad 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -40,6 +40,7 @@ namespace Microsoft.Dafny Bpl.CommandLineOptions.Install(options); } + public bool UnicodeOutput = false; public bool DisallowSoundnessCheating = false; public bool Dafnycc = false; public int Induction = 3; diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 828e0e18..cbc212d2 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -132,55 +132,63 @@ namespace Microsoft.Dafny.Triggers { //FIXME } - private void CommitOne(QuantifierWithTriggers q, object conjunctId) { + private void CommitOne(QuantifierWithTriggers q, bool addHeader) { var errorLevel = ErrorLevel.Info; var msg = new StringBuilder(); - var indent = conjunctId != null ? " " : " "; - var header = conjunctId != null ? String.Format(" For conjunct {0}:{1}", conjunctId, Environment.NewLine) : ""; + var indent = addHeader ? " " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: no_trigger is passed down to Boogie - msg.Append(indent).AppendLine("Not generating triggers for this quantifier."); + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie + msg.AppendFormat(" Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); + // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) + // FIXME typeQuantifier? } else { - foreach (var candidate in q.Candidates) { - q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); + if (addHeader) { + msg.AppendFormat(" For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } - if (q.Candidates.Any()) { - msg.Append(indent).AppendLine("Selected triggers:"); - foreach (var mc in q.Candidates) { - msg.Append(indent).Append(" ").AppendLine(mc.ToString()); - } + foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger + q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); } - if (q.RejectedCandidates.Any()) { - msg.Append(indent).AppendLine("Rejected triggers:"); - foreach (var mc in q.RejectedCandidates) { - msg.Append(indent).Append(" ").AppendLine(mc.ToString()); - } - } + AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent); + AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); #if QUANTIFIER_WARNINGS + string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension if (!q.CandidateTerms.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("No terms found to trigger on."); + msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on."); } else if (!q.Candidates.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("No trigger covering all quantified variables found."); - } else if (!q.CouldSuppressLoops) { + msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found."); + } else if (!q.CouldSuppressLoops && !q.AllowsLoops) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("Suppressing loops would leave this quantifier without triggers."); + msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); } #endif } - + if (msg.Length > 0) { - reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, header + msg.ToString()); + reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray())); + } + } + + private static void AddTriggersToMessage(string header, List triggers, StringBuilder msg, string indent, bool newlines = false) { + if (triggers.Any()) { + msg.Append(indent).Append(header); + if (triggers.Count == 1) { + msg.Append(" "); + } else if (triggers.Count > 1) { + msg.AppendLine().Append(indent).Append(" "); + } + var separator = newlines && triggers.Count > 1 ? Environment.NewLine + indent + " " : ", "; + msg.AppendLine(String.Join(separator, triggers)); } } internal void CommitTriggers() { foreach (var q in quantifiers) { - CommitOne(q, quantifiers.Count > 1 ? q.quantifier : null); + CommitOne(q, quantifiers.Count > 1); } } } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 74cdd8c2..bdfd66b4 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -33,11 +33,13 @@ namespace Microsoft.Dafny { public Server() { this.running = true; Console.CancelKeyPress += this.CancelKeyPress; + Console.InputEncoding = System.Text.Encoding.UTF8; + Console.OutputEncoding = System.Text.Encoding.UTF8; ExecutionEngine.printer = new DafnyConsolePrinter(); } void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { - e.Cancel = true; + // e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine // Cancel the current verification? TerminateProver() ? Or kill entirely? } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 8fb03b05..4b06e9f5 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,14 @@ namespace Microsoft.Dafny { internal static void ApplyArgs(string[] args) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + Dafny.DafnyOptions.O.ProverKillTime = 10; if (CommandLineOptions.Clo.Parse(args)) { // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME // Dafny.DafnyOptions.O.ModelViewFile = "-"; - Dafny.DafnyOptions.O.ProverKillTime = 10; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.UnicodeOutput = true; Dafny.DafnyOptions.O.VerifySnapshots = 2; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); } else { throw new ServerException("Invalid command line options"); } -- cgit v1.2.3 From a019d797bd42866242e48ef00850f74e3bdc9241 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 16:41:10 -0700 Subject: Server: disable tracing when running tests, and fix an encoding issue. z3 doesn't support byte-order marks; thus using the default UTF8Encoding object (to allow printing nice warning signs) causes issues, as it sends a BOM before anything else. --- Source/DafnyServer/Server.cs | 24 ++++++++++++++++-------- Source/DafnyServer/Utilities.cs | 3 ++- Source/DafnyServer/VerificationTask.cs | 6 +++--- 3 files changed, 21 insertions(+), 12 deletions(-) (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index bdfd66b4..0a9ce599 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -11,6 +11,7 @@ using Microsoft.Boogie; namespace Microsoft.Dafny { class Server { + private bool trace; private bool running; static void Main(string[] args) { @@ -23,33 +24,40 @@ namespace Microsoft.Dafny { VerificationTask.SelfTest(); } else if (hasArg && File.Exists(arg)) { Console.WriteLine("# Reading from {0}", Path.GetFileName(arg)); - Console.SetIn(new StreamReader(arg)); + Console.SetIn(new StreamReader(arg, Encoding.UTF8)); + server.trace = false; server.Loop(); } else { server.Loop(); } } + private void SetupConsole() { + var utf8 = new UTF8Encoding(false, true); + Console.OutputEncoding = utf8; + Console.OutputEncoding = utf8; + Console.CancelKeyPress += CancelKeyPress; + } + public Server() { + this.trace = true; this.running = true; - Console.CancelKeyPress += this.CancelKeyPress; - Console.InputEncoding = System.Text.Encoding.UTF8; - Console.OutputEncoding = System.Text.Encoding.UTF8; ExecutionEngine.printer = new DafnyConsolePrinter(); + SetupConsole(); } void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { // e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine - // Cancel the current verification? TerminateProver() ? Or kill entirely? + // Cancel the current verification? TerminateProver()? Or kill entirely? } - static bool EndOfPayload(out string line) { + bool EndOfPayload(out string line) { line = Console.ReadLine(); return line == null || line == Interaction.CLIENT_EOM_TAG; } - static string ReadPayload() { + string ReadPayload() { StringBuilder buffer = new StringBuilder(); string line = null; while (!EndOfPayload(out line)) { @@ -78,7 +86,7 @@ namespace Microsoft.Dafny { if (verb == "verify") { ServerUtils.checkArgs(command, 0); var payload = ReadPayload(); - VerificationTask.ReadTask(payload).Run(); + VerificationTask.ReadTask(payload).Run(trace); } else if (verb == "quit") { ServerUtils.checkArgs(command, 0); Exit(); diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 4b06e9f5..96254a3d 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,7 +43,7 @@ namespace Microsoft.Dafny { } } - internal static void ApplyArgs(string[] args) { + internal static void ApplyArgs(string[] args, bool trace) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); Dafny.DafnyOptions.O.ProverKillTime = 10; @@ -53,6 +53,7 @@ namespace Microsoft.Dafny { Dafny.DafnyOptions.O.UnicodeOutput = true; Dafny.DafnyOptions.O.VerifySnapshots = 2; Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.Clo.Trace = trace; } else { throw new ServerException("Invalid command line options"); } diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index a00688b1..dbafc781 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -44,15 +44,15 @@ namespace Microsoft.Dafny { source = "method selftest() { assert true; }" }; try { - task.Run(); + task.Run(false); Interaction.EOM(Interaction.SUCCESS, null); } catch (Exception ex) { Interaction.EOM(Interaction.FAILURE, ex); } } - internal void Run() { - ServerUtils.ApplyArgs(args); + internal void Run(bool trace = true) { + ServerUtils.ApplyArgs(args, trace); new DafnyHelper(filename, ProgramSource).Verify(); } } -- cgit v1.2.3 From 43cbd76e07262d05434e36dff99f8d10eb59a773 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 16:15:26 -0700 Subject: Use /tracePO instead of /trace in the server This removes the need for special treatment of test input (/trace includes timings in the output, which are not suitable for tests. /tracePO does not) --- Source/DafnyServer/Server.cs | 5 +- Source/DafnyServer/Utilities.cs | 12 +- Source/DafnyServer/VerificationTask.cs | 6 +- Test/server/minimal.transcript | 8 + Test/server/minimal.transcript.expect | 14 + Test/server/simple-session.transcript.expect | 694 ++++++++++++++++++++++++++- 6 files changed, 705 insertions(+), 34 deletions(-) create mode 100644 Test/server/minimal.transcript create mode 100644 Test/server/minimal.transcript.expect (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 0a9ce599..e524a9a3 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -11,7 +11,6 @@ using Microsoft.Boogie; namespace Microsoft.Dafny { class Server { - private bool trace; private bool running; static void Main(string[] args) { @@ -25,7 +24,6 @@ namespace Microsoft.Dafny { } else if (hasArg && File.Exists(arg)) { Console.WriteLine("# Reading from {0}", Path.GetFileName(arg)); Console.SetIn(new StreamReader(arg, Encoding.UTF8)); - server.trace = false; server.Loop(); } else { server.Loop(); @@ -40,7 +38,6 @@ namespace Microsoft.Dafny { } public Server() { - this.trace = true; this.running = true; ExecutionEngine.printer = new DafnyConsolePrinter(); SetupConsole(); @@ -86,7 +83,7 @@ namespace Microsoft.Dafny { if (verb == "verify") { ServerUtils.checkArgs(command, 0); var payload = ReadPayload(); - VerificationTask.ReadTask(payload).Run(trace); + VerificationTask.ReadTask(payload).Run(); } else if (verb == "quit") { ServerUtils.checkArgs(command, 0); Exit(); diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 3bc334b3..d6654ac1 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,18 +43,18 @@ namespace Microsoft.Dafny { } } - internal static void ApplyArgs(string[] args, bool trace) { + internal static void ApplyArgs(string[] args) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); Dafny.DafnyOptions.O.ProverKillTime = 10; if (CommandLineOptions.Clo.Parse(args)) { // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME // Dafny.DafnyOptions.O.ModelViewFile = "-"; - DafnyOptions.O.PrintTooltips = true; - DafnyOptions.O.UnicodeOutput = true; - DafnyOptions.O.VerifySnapshots = 2; - DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); - DafnyOptions.O.Trace = trace; + DafnyOptions.O.VerifySnapshots = 2; // Use caching + DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME + DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout + DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs + DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification } else { throw new ServerException("Invalid command line options"); } diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index dbafc781..a00688b1 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -44,15 +44,15 @@ namespace Microsoft.Dafny { source = "method selftest() { assert true; }" }; try { - task.Run(false); + task.Run(); Interaction.EOM(Interaction.SUCCESS, null); } catch (Exception ex) { Interaction.EOM(Interaction.FAILURE, ex); } } - internal void Run(bool trace = true) { - ServerUtils.ApplyArgs(args, trace); + internal void Run() { + ServerUtils.ApplyArgs(args); new DafnyHelper(filename, ProgramSource).Verify(); } } diff --git a/Test/server/minimal.transcript b/Test/server/minimal.transcript new file mode 100644 index 00000000..9625fb00 --- /dev/null +++ b/Test/server/minimal.transcript @@ -0,0 +1,8 @@ +# RUN: %server "%s" > "%t" +# RUN: %diff "%s.expect" "%t" +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] diff --git a/Test/server/minimal.transcript.expect b/Test/server/minimal.transcript.expect new file mode 100644 index 00000000..bf3f9dfb --- /dev/null +++ b/Test/server/minimal.transcript.expect @@ -0,0 +1,14 @@ +# Reading from minimal.transcript + +Verifying CheckWellformed$$_module.__default.A ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... + [2 proof obligations] error +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect index 89c3351d..91429d8e 100644 --- a/Test/server/simple-session.transcript.expect +++ b/Test/server/simple-session.transcript.expect @@ -1,24 +1,60 @@ # Reading from simple-session.transcript + +Verifying CheckWellformed$$_module.__default.A ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... + [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... + [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,13): Error: rbrace expected @@ -27,22 +63,114 @@ Verification completed successfully! transcript(6,2): Error: rbrace expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [0 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [0 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,0): Error: ident expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [1 proof obligation] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment @@ -51,21 +179,113 @@ Verification completed successfully! transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [2 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [2 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [2 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [3 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [3 proof obligations] verified +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [3 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here @@ -77,6 +297,20 @@ transcript(6,2): Error: EOF expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [3 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here @@ -112,15 +346,59 @@ transcript(10,27): Error: invalid UnaryExpression Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [1 proof obligation] error transcript(10,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here @@ -128,9 +406,39 @@ transcript(12,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here @@ -190,18 +498,130 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... + [5 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M2... + [5 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... + [2 proof obligations] error transcript(38,9): Error: assertion violation Execution trace: (0,0): anon0 @@ -218,6 +638,44 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... + [2 proof obligations] error transcript(38,9): Error: assertion violation Execution trace: (0,0): anon0 @@ -227,12 +685,90 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... + [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M2... + [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here @@ -260,6 +796,44 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here @@ -287,12 +861,90 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here + +Verifying CheckWellformed$$_module.__default.A ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.A ... +Retrieving cached verification result for implementation Impl$$_module.__default.A... + [0 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M_k ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M_k ... +Retrieving cached verification result for implementation Impl$$_module.__default.M_k... + [1 proof obligation] verified + +Verifying CheckWellformed$$_module.__default.M0 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M0 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M0... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M1 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M1 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M1... + [5 proof obligations] verified + +Verifying CheckWellformed$$_module.__default.M2 ... +Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2... + [0 proof obligations] verified + +Verifying Impl$$_module.__default.M2 ... +Retrieving cached verification result for implementation Impl$$_module.__default.M2... + [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verification completed successfully! -- cgit v1.2.3 From e676ad0877d31cb73a1a6bb5aae677ac64593fd6 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 19:58:46 -0700 Subject: Cleanup a number of FIXMEs that I had left in the code --- Source/Dafny/DafnyAst.cs | 12 ++++++------ Source/Dafny/Resolver.cs | 6 +++--- Source/Dafny/Triggers/QuantifiersCollection.cs | 8 ++------ Source/Dafny/Triggers/TriggersCollector.cs | 6 ++++-- Source/DafnyServer/DafnyHelper.cs | 2 +- Source/DafnyServer/Server.cs | 9 +-------- Source/DafnyServer/Utilities.cs | 6 ++---- 7 files changed, 19 insertions(+), 30 deletions(-) (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 14a354c4..06f6d856 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7769,7 +7769,7 @@ namespace Microsoft.Dafny { } else if (decl is Method) { Visit((Method)decl); } - //FIXME More? + //TODO More? } public void Visit(Method method) { Visit(method.Ens); @@ -7777,7 +7777,7 @@ namespace Microsoft.Dafny { Visit(method.Mod.Expressions); Visit(method.Decreases.Expressions); if (method.Body != null) { Visit(method.Body); } - //FIXME More? + //TODO More? } public void Visit(Function function) { Visit(function.Ens); @@ -7785,7 +7785,7 @@ namespace Microsoft.Dafny { Visit(function.Reads); Visit(function.Decreases.Expressions); if (function.Body != null) { Visit(function.Body); } - //FIXME More? + //TODO More? } protected virtual void VisitOneExpr(Expression expr) { Contract.Requires(expr != null); @@ -7842,7 +7842,7 @@ namespace Microsoft.Dafny { } else if (decl is Method) { Visit((Method)decl, st); } - //FIXME More? + //TODO More? } public void Visit(Method method, State st) { Visit(method.Ens, st); @@ -7850,7 +7850,7 @@ namespace Microsoft.Dafny { Visit(method.Mod.Expressions, st); Visit(method.Decreases.Expressions, st); if (method.Body != null) { Visit(method.Body, st); } - //FIXME More? + //TODO More? } public void Visit(Function function, State st) { Visit(function.Ens, st); @@ -7858,7 +7858,7 @@ namespace Microsoft.Dafny { Visit(function.Reads, st); Visit(function.Decreases.Expressions, st); if (function.Body != null) { Visit(function.Body, st); } - //FIXME More? + //TODO More? } /// /// Visit one expression proper. This method is invoked before it is invoked on the diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2f2b5a54..e5fe7cf8 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -199,7 +199,7 @@ namespace Microsoft.Dafny public void ResolveProgram(Program prog) { Contract.Requires(prog != null); - var origErrorCount = reporter.Count(ErrorLevel.Error); //FIXME (Clement): This is used further below, but not in the >0 comparisons in the next few lines. Is that right? + var origErrorCount = reporter.Count(ErrorLevel.Error); //TODO: This is used further below, but not in the >0 comparisons in the next few lines. Is that right? var bindings = new ModuleBindings(null); var b = BindModuleNames(prog.DefaultModuleDef, bindings); bindings.BindName("_module", prog.DefaultModule, b); @@ -8301,7 +8301,7 @@ namespace Microsoft.Dafny receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass, true); } else { if (!scope.AllowInstance) { - reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context"); //FIXME: Rephrase this + reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context"); //TODO: Rephrase this // nevertheless, set "receiver" to a value so we can continue resolution } receiver = new ImplicitThisExpr(expr.tok); @@ -8604,7 +8604,7 @@ namespace Microsoft.Dafny Dictionary members; if (classMembers.TryGetValue(cd, out members) && members.TryGetValue(expr.SuffixName, out member)) { if (!member.IsStatic) { - reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName); //FIXME Unify with similar error message + reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName); //TODO Unify with similar error messages // nevertheless, continue creating an expression that approximates a correct one } var receiver = new StaticReceiverExpr(expr.tok, (UserDefinedType)ty.NormalizeExpand(), (ClassDecl)member.EnclosingClass, false); diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index bfa90d81..8e4c3261 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -7,8 +7,6 @@ using System.Text; using Microsoft.Boogie; using System.Diagnostics.Contracts; -//FIXME: When scoring, do not consider old(x) to be higher than x. - namespace Microsoft.Dafny.Triggers { class QuantifierWithTriggers { internal QuantifierExpr quantifier; @@ -149,16 +147,14 @@ namespace Microsoft.Dafny.Triggers { var msg = new StringBuilder(); var indent = addHeader ? " " : ""; - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop, split and autotriggers attributes are passed down to Boogie + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); - // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) - // FIXME typeQuantifier? } else { if (addHeader) { msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } - foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger + foreach (var candidate in q.Candidates) { q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 3b2853ed..30f7b9e8 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -249,10 +249,12 @@ namespace Microsoft.Dafny.Triggers { return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); } - // FIXME document that this will contain duplicates + /// + /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms. + /// internal List CollectTriggers(QuantifierExpr quantifier) { Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier - // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions + // NOTE: We could check for existing trigger attributes and return that instead return Annotate(quantifier).PrivateTerms; } diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 952f71c5..3204fdb3 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -74,7 +74,7 @@ namespace Microsoft.Dafny { ExecutionEngine.CoalesceBlocks(boogieProgram); ExecutionEngine.Inline(boogieProgram); - //FIXME Could capture errors instead of printing them (pass a delegate instead of null) + //NOTE: We could capture errors instead of printing them (pass a delegate instead of null) switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { case PipelineOutcome.Done: case PipelineOutcome.VerificationCompleted: diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index e524a9a3..77840007 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -32,9 +32,8 @@ namespace Microsoft.Dafny { private void SetupConsole() { var utf8 = new UTF8Encoding(false, true); + Console.InputEncoding = utf8; Console.OutputEncoding = utf8; - Console.OutputEncoding = utf8; - Console.CancelKeyPress += CancelKeyPress; } public Server() { @@ -43,12 +42,6 @@ namespace Microsoft.Dafny { SetupConsole(); } - void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { - // e.Cancel = true; - // FIXME TerminateProver and RunningProverFromCommandLine - // Cancel the current verification? TerminateProver()? Or kill entirely? - } - bool EndOfPayload(out string line) { line = Console.ReadLine(); return line == null || line == Interaction.CLIENT_EOM_TAG; diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index d6654ac1..59b3abb9 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,11 @@ namespace Microsoft.Dafny { internal static void ApplyArgs(string[] args) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); - Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { - // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME - // Dafny.DafnyOptions.O.ModelViewFile = "-"; DafnyOptions.O.VerifySnapshots = 2; // Use caching - DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME + DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification -- cgit v1.2.3 From 8695668ca1121dde6a91f7a0c00ef0b065104c40 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 09:40:58 -0700 Subject: Give up on trying to set the console's input encoding to UTF8 Fortunately, the server spec already assumes an ASCII input channel. --- Source/DafnyServer/Server.cs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'Source/DafnyServer/Server.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 77840007..8c94ad5b 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -31,9 +31,8 @@ namespace Microsoft.Dafny { } private void SetupConsole() { - var utf8 = new UTF8Encoding(false, true); - Console.InputEncoding = utf8; - Console.OutputEncoding = utf8; + // Setting InputEncoding to UTF8 causes z3 to choke. + Console.OutputEncoding = new UTF8Encoding(false, true); } public Server() { -- cgit v1.2.3