From ef10ea8525b04c263d82038393f0a9dcb9f1e5de Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 10 Nov 2023 13:30:40 -0800 Subject: [PATCH 1/9] =?UTF-8?q?Breaking=20spans=20by=20module=20(not=20wor?= =?UTF-8?q?king=20yet,=20tokens=20aren=E2=80=99t=20right)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../CoverageReport/CoverageReport.cs | 19 ++++++++++-- Source/DafnyDriver/CoverageReporter.cs | 30 +++++++++++++++---- 2 files changed, 40 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index 3e2bb0c5cce..f67f8f8873a 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -12,6 +12,7 @@ public class CoverageReport { private static int nextUniqueId = 0; private readonly Dictionary> labelsByFile; + private readonly Dictionary> modulesByFile; public readonly string Name; // the name to assign to this coverage report public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table. private readonly string suffix; // user-provided suffix to add to filenames that are part of this report @@ -31,6 +32,7 @@ public CoverageReport(string name, string units, string suffix, Program program) Units = units; this.suffix = suffix; labelsByFile = new(); + modulesByFile = new(); if (program != null) { RegisterFiles(program); } @@ -49,6 +51,10 @@ public void LabelCode(RangeToken span, CoverageLabel label) { public IEnumerable CoverageSpansForFile(Uri uri) { return labelsByFile.GetOrDefault(uri, () => new List()); } + + public IEnumerable ModulesInFile(Uri uri) { + return modulesByFile.GetOrDefault(uri, () => new HashSet()); + } public IEnumerable AllFiles() { return labelsByFile.Keys; @@ -65,10 +71,17 @@ public void RegisterFile(Uri uri) { } private void RegisterFiles(Node astNode) { - if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.Uri)) { - labelsByFile[astNode.StartToken.Uri] = new(); + if (astNode.StartToken.ActualFilename != null) { + var uri = astNode.StartToken.Uri; + labelsByFile.GetOrCreate(uri, () => new List()); + + if (astNode is LiteralModuleDecl moduleDecl) { + modulesByFile.GetOrCreate(uri, () => new HashSet()).Add(moduleDecl.ModuleDef); + + RegisterFiles(moduleDecl.ModuleDef); + } } - + foreach (var declaration in astNode.Children.OfType()) { RegisterFiles(declaration); } diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index f1f3671f10d..6cd5655e8c5 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -215,7 +215,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour return; } var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast().ToList(); - List header = new() { "File" }; + List header = new() { "File", "Module" }; header.AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}")); @@ -223,16 +223,34 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour List> body = new(); foreach (var sourceFile in sourceFileToCoverageReportFile.Keys) { var relativePath = Path.GetRelativePath(baseDirectory, sourceFileToCoverageReportFile[sourceFile]); + body.Add(new() { $"{relativePath}" + $"class = \"el_package\">{relativePath}", + "All modules" }); + body.Last().AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) - .Select(label => report.CoverageSpansForFile(sourceFile).Count(span => span.Label == label)).OfType()); + .Select(label => report.CoverageSpansForFile(sourceFile) + .Count(span => span.Label == label)).OfType()); + + foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) { + body.Add(new() { + $"{relativePath}", + module.FullName + }); + + body.Last().AddRange(coverageLabels + .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) + .Select(label => report.CoverageSpansForFile(sourceFile) + .Where(span => span.Span.Intersects(module.RangeToken)) + .Count(span => span.Label == label)).OfType()); + } } - List footer = new() { "Total" }; + List footer = new() { "Total", "" }; footer.AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => report.AllFiles().Select(sourceFile => @@ -243,8 +261,8 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour templateText = FileNameRegex.Replace(templateText, report.Name); templateText = TableHeaderRegex.Replace(templateText, MakeIndexFileTableRow(header)); templateText = TableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); - File.WriteAllText(Path.Combine(baseDirectory, $"index{report.UniqueSuffix}.html"), - TableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)))); + templateText = TableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); + File.WriteAllText(Path.Combine(baseDirectory, $"index{report.UniqueSuffix}.html"), templateText); } /// From 5b093f0c913c5f4ef77f0074e844fd6a691a9af0 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 10 Nov 2023 14:04:17 -0800 Subject: [PATCH 2/9] Better formatting --- Source/DafnyDriver/CoverageReporter.cs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index 6cd5655e8c5..fa0947a865d 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -237,15 +237,18 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) { body.Add(new() { - $"{relativePath}", + "", module.FullName }); - + + var moduleRange = module.RangeToken.ToDafnyRange(); body.Last().AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => report.CoverageSpansForFile(sourceFile) - .Where(span => span.Span.Intersects(module.RangeToken)) + // span.Span.Intersects(module.RangeToken) would be cleaner, + // but unfortunately coverage span tokens don't currently always + // have Token.pos set correctly. :( + .Where(span => moduleRange.Contains(span.Span.ToDafnyRange().Start)) .Count(span => span.Label == label)).OfType()); } } From 08d73c7655ccce7bb69799bacaa0d883b96c0c83 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 10 Nov 2023 15:32:18 -0800 Subject: [PATCH 3/9] Improve Base64 coverage --- Source/DafnyStandardLibraries/examples/Base64Examples.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyStandardLibraries/examples/Base64Examples.dfy b/Source/DafnyStandardLibraries/examples/Base64Examples.dfy index ebdc3874b3c..48da3ab5e00 100644 --- a/Source/DafnyStandardLibraries/examples/Base64Examples.dfy +++ b/Source/DafnyStandardLibraries/examples/Base64Examples.dfy @@ -25,8 +25,8 @@ module Base64Examples { } method {:test} TestRoundTripMedium() { - var medUints := seq(512, _ => 22); - var medBytes := seq(512, _ => 22); + var medUints := seq(512, i => (i % 256) as uint8); + var medBytes := seq(512, i => (i % 256) as bv8); CheckEncodeDecode(medUints, medBytes); } From 98349d41f6db292dc3fe1f3d2d3ef93cbceae1a7 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 13 Nov 2023 12:18:48 -0800 Subject: [PATCH 4/9] Align first two columns left --- Source/DafnyDriver/CoverageReporter.cs | 5 ++++- Source/DafnyDriver/assets/.resources/coverage.css | 11 +++++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index fa0947a865d..b16952967af 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -196,7 +196,10 @@ private void SerializeCoverageReports(List reports, string repor private string MakeIndexFileTableRow(List row) { var result = new StringBuilder("\n"); - foreach (var cell in row) { + foreach (var cell in row.Take(2)) { + result.Append($"\t{cell}\n"); + } + foreach (var cell in row.Skip(2)) { result.Append($"\t{cell}\n"); } result.Append("\n"); diff --git a/Source/DafnyDriver/assets/.resources/coverage.css b/Source/DafnyDriver/assets/.resources/coverage.css index 06ec1515b50..af92c4fc608 100644 --- a/Source/DafnyDriver/assets/.resources/coverage.css +++ b/Source/DafnyDriver/assets/.resources/coverage.css @@ -49,6 +49,11 @@ table.coverage thead td { border-bottom:#b0b0b0 1px solid; } +table.coverage thead td.name { + text-align:left; + padding-left:2px; +} + table.coverage thead td.ctr2 { text-align:right; padding-left:2px; @@ -64,6 +69,12 @@ table.coverage tbody tr:hover { background: #f0f0d0 !important; } +table.coverage tbody td.name { + text-align:left; + padding-right:14px; + padding-left:2px; +} + table.coverage tbody td.ctr2 { text-align:right; padding-right:14px; From 56cd2b4df8da330c44c8baa1aa8950acf848789d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 13 Nov 2023 14:52:18 -0800 Subject: [PATCH 5/9] Partial work to handle implicit parent modules (just capturing to come back to later) --- .../DafnyCore/AST/Modules/ModuleDefinition.cs | 2 +- .../CoverageReport/CoverageReport.cs | 17 ++--- Source/DafnyDriver/CoverageReporter.cs | 71 ++++++++++++++++--- .../coverage_report_index_template.html | 17 ++++- 4 files changed, 85 insertions(+), 22 deletions(-) diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index e5ab45f5425..f17d3e9fedd 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny; public record PrefixNameModule(IReadOnlyList Parts, LiteralModuleDecl Module); -public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable, IHasSymbolChildren { +public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable, IHasSymbolChildren { public IToken BodyStartTok = Token.NoToken; public IToken TokenWithTrailingDocString = Token.NoToken; diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index f67f8f8873a..0af99f0753e 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -13,6 +13,7 @@ public class CoverageReport { private readonly Dictionary> labelsByFile; private readonly Dictionary> modulesByFile; + public readonly string Name; // the name to assign to this coverage report public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table. private readonly string suffix; // user-provided suffix to add to filenames that are part of this report @@ -72,14 +73,14 @@ public void RegisterFile(Uri uri) { private void RegisterFiles(Node astNode) { if (astNode.StartToken.ActualFilename != null) { - var uri = astNode.StartToken.Uri; - labelsByFile.GetOrCreate(uri, () => new List()); - - if (astNode is LiteralModuleDecl moduleDecl) { - modulesByFile.GetOrCreate(uri, () => new HashSet()).Add(moduleDecl.ModuleDef); - - RegisterFiles(moduleDecl.ModuleDef); - } + labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => new List()); + } + + if (astNode is LiteralModuleDecl moduleDecl) { + // Uri may be null for implicit modules + modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => new HashSet()).Add(moduleDecl.ModuleDef); + + RegisterFiles(moduleDecl.ModuleDef); } foreach (var declaration in astNode.Children.OfType()) { diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index b16952967af..62c6cc2a3d0 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -20,9 +20,12 @@ public class CoverageReporter { private static readonly Regex UriRegexInversed = new(@"

([^\n]*)

"); private static readonly Regex IndexLinkRegex = new(@"\{\{INDEX_LINK\}\}"); private static readonly Regex LinksToOtherReportsRegex = new(@"\{\{LINKS_TO_OTHER_REPORTS\}\}"); - private static readonly Regex TableHeaderRegex = new(@"\{\{TABLE_HEADER\}\}"); - private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}"); - private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}"); + private static readonly Regex ByFileTableHeaderRegex = new(@"\{\{BY_FILE_TABLE_HEADER\}\}"); + private static readonly Regex ByFileTableFooterRegex = new(@"\{\{BY_FILE_TABLE_FOOTER\}\}"); + private static readonly Regex ByFileTableBodyRegex = new(@"\{\{BY_FILE_TABLE_BODY\}\}"); + private static readonly Regex ByModuleTableHeaderRegex = new(@"\{\{BY_MODULE_TABLE_HEADER\}\}"); + private static readonly Regex ByModuleTableFooterRegex = new(@"\{\{BY_MODULE_TABLE_FOOTER\}\}"); + private static readonly Regex ByModuleTableBodyRegex = new(@"\{\{BY_MODULE_TABLE_BODY\}\}"); private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html"); private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"([0-9]+):([0-9]+)\""); private const string CoverageReportTemplatePath = "coverage_report_template.html"; @@ -218,7 +221,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour return; } var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast().ToList(); - List header = new() { "File", "Module" }; + List header = new() { "File" }; header.AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}")); @@ -229,8 +232,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour body.Add(new() { $"{relativePath}", - "All modules" + $"class = \"el_package\">{relativePath}" }); body.Last().AddRange(coverageLabels @@ -240,7 +242,6 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) { body.Add(new() { - "", module.FullName }); @@ -255,7 +256,15 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour .Count(span => span.Label == label)).OfType()); } } + + header = new() { "Module" }; + header.AddRange(coverageLabels + .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) + .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}")); + body = new(); + PopulateByModuleTableBody(report, ) + List footer = new() { "Total", "" }; footer.AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) @@ -265,12 +274,54 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour var templateText = new StreamReader(templateStream).ReadToEnd(); templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports); templateText = FileNameRegex.Replace(templateText, report.Name); - templateText = TableHeaderRegex.Replace(templateText, MakeIndexFileTableRow(header)); - templateText = TableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); - templateText = TableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); + + templateText = ByFileTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header)); + templateText = ByFileTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); + templateText = ByFileTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); + + templateText = ByModuleTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header)); + templateText = ByModuleTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); + templateText = ByModuleTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); + File.WriteAllText(Path.Combine(baseDirectory, $"index{report.UniqueSuffix}.html"), templateText); } + private static void PopulateByModuleTableBody(CoverageReport report, ModuleDefinition module, List coverageLabels, List> body) { + body.Add(CountsForModule(report, module, coverageLabels).OfType().ToList()); + + foreach (var child in module.TopLevelDecls.OrderBy(decl => decl.Name)) { + if (child is LiteralModuleDecl moduleDecl) { + PopulateByModuleTableBody(report, moduleDecl.ModuleDef, coverageLabels, body); + } + } + } + + private static List CountsForModule(CoverageReport report, ModuleDefinition module, List coverageLabels) { + if (module.StartToken.Uri != null) { + var moduleRange = module.RangeToken.ToDafnyRange(); + return coverageLabels + .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) + .Select(label => report.CoverageSpansForFile(module.StartToken.Uri) + // span.Span.Intersects(module.RangeToken) would be cleaner, + // but unfortunately coverage span tokens don't currently always + // have Token.pos set correctly. :( + .Where(span => moduleRange.Contains(span.Span.ToDafnyRange().Start)) + .Count(span => span.Label == label)).ToList(); + } else { + var sums = new int[coverageLabels.Count]; + foreach (var child in module.TopLevelDecls) { + if (child is LiteralModuleDecl moduleDecl) { + var childModuleCounts = CountsForModule(report, moduleDecl.ModuleDef, coverageLabels); + for (var labelIndex = 0; labelIndex < coverageLabels.Count; labelIndex++) { + sums[labelIndex] += childModuleCounts[labelIndex]; + } + } + } + + return sums.ToList(); + } + } + /// /// Creates a set of links to be inserted in that point to corresponding /// report files for the same diff --git a/Source/DafnyDriver/assets/coverage_report_index_template.html b/Source/DafnyDriver/assets/coverage_report_index_template.html index bbba468d06d..0061f94dca2 100644 --- a/Source/DafnyDriver/assets/coverage_report_index_template.html +++ b/Source/DafnyDriver/assets/coverage_report_index_template.html @@ -14,13 +14,24 @@

{{FILENAME}}

- {{TABLE_HEADER}} + {{BY_FILE_TABLE_HEADER}} - {{TABLE_FOOTER}} + {{BY_FILE_TABLE_FOOTER}} - {{TABLE_BODY}} + {{BY_FILE_TABLE_BODY}} + +
+ + + {{BY_MODULE_TABLE_HEADER}} + + + {{BY_MODULE_TABLE_FOOTER}} + + + {{BY_MODULE_TABLE_BODY}}
From e48192d330d278c8fb0a665fe58f168a10169ffc Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 13 Nov 2023 14:52:36 -0800 Subject: [PATCH 6/9] Revert "Partial work to handle implicit parent modules" This reverts commit 56cd2b4df8da330c44c8baa1aa8950acf848789d. --- .../DafnyCore/AST/Modules/ModuleDefinition.cs | 2 +- .../CoverageReport/CoverageReport.cs | 17 +++-- Source/DafnyDriver/CoverageReporter.cs | 71 +++---------------- .../coverage_report_index_template.html | 17 +---- 4 files changed, 22 insertions(+), 85 deletions(-) diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index f17d3e9fedd..e5ab45f5425 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny; public record PrefixNameModule(IReadOnlyList Parts, LiteralModuleDecl Module); -public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable, IHasSymbolChildren { +public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable, IHasSymbolChildren { public IToken BodyStartTok = Token.NoToken; public IToken TokenWithTrailingDocString = Token.NoToken; diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index 0af99f0753e..f67f8f8873a 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -13,7 +13,6 @@ public class CoverageReport { private readonly Dictionary> labelsByFile; private readonly Dictionary> modulesByFile; - public readonly string Name; // the name to assign to this coverage report public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table. private readonly string suffix; // user-provided suffix to add to filenames that are part of this report @@ -73,14 +72,14 @@ public void RegisterFile(Uri uri) { private void RegisterFiles(Node astNode) { if (astNode.StartToken.ActualFilename != null) { - labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => new List()); - } - - if (astNode is LiteralModuleDecl moduleDecl) { - // Uri may be null for implicit modules - modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => new HashSet()).Add(moduleDecl.ModuleDef); - - RegisterFiles(moduleDecl.ModuleDef); + var uri = astNode.StartToken.Uri; + labelsByFile.GetOrCreate(uri, () => new List()); + + if (astNode is LiteralModuleDecl moduleDecl) { + modulesByFile.GetOrCreate(uri, () => new HashSet()).Add(moduleDecl.ModuleDef); + + RegisterFiles(moduleDecl.ModuleDef); + } } foreach (var declaration in astNode.Children.OfType()) { diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index 62c6cc2a3d0..b16952967af 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -20,12 +20,9 @@ public class CoverageReporter { private static readonly Regex UriRegexInversed = new(@"

([^\n]*)

"); private static readonly Regex IndexLinkRegex = new(@"\{\{INDEX_LINK\}\}"); private static readonly Regex LinksToOtherReportsRegex = new(@"\{\{LINKS_TO_OTHER_REPORTS\}\}"); - private static readonly Regex ByFileTableHeaderRegex = new(@"\{\{BY_FILE_TABLE_HEADER\}\}"); - private static readonly Regex ByFileTableFooterRegex = new(@"\{\{BY_FILE_TABLE_FOOTER\}\}"); - private static readonly Regex ByFileTableBodyRegex = new(@"\{\{BY_FILE_TABLE_BODY\}\}"); - private static readonly Regex ByModuleTableHeaderRegex = new(@"\{\{BY_MODULE_TABLE_HEADER\}\}"); - private static readonly Regex ByModuleTableFooterRegex = new(@"\{\{BY_MODULE_TABLE_FOOTER\}\}"); - private static readonly Regex ByModuleTableBodyRegex = new(@"\{\{BY_MODULE_TABLE_BODY\}\}"); + private static readonly Regex TableHeaderRegex = new(@"\{\{TABLE_HEADER\}\}"); + private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}"); + private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}"); private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html"); private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"([0-9]+):([0-9]+)\""); private const string CoverageReportTemplatePath = "coverage_report_template.html"; @@ -221,7 +218,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour return; } var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast().ToList(); - List header = new() { "File" }; + List header = new() { "File", "Module" }; header.AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}")); @@ -232,7 +229,8 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour body.Add(new() { $"{relativePath}" + $"class = \"el_package\">{relativePath}", + "All modules" }); body.Last().AddRange(coverageLabels @@ -242,6 +240,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) { body.Add(new() { + "", module.FullName }); @@ -256,15 +255,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour .Count(span => span.Label == label)).OfType()); } } - - header = new() { "Module" }; - header.AddRange(coverageLabels - .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) - .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}")); - body = new(); - PopulateByModuleTableBody(report, ) - List footer = new() { "Total", "" }; footer.AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) @@ -274,54 +265,12 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour var templateText = new StreamReader(templateStream).ReadToEnd(); templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports); templateText = FileNameRegex.Replace(templateText, report.Name); - - templateText = ByFileTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header)); - templateText = ByFileTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); - templateText = ByFileTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); - - templateText = ByModuleTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header)); - templateText = ByModuleTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); - templateText = ByModuleTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); - + templateText = TableHeaderRegex.Replace(templateText, MakeIndexFileTableRow(header)); + templateText = TableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer)); + templateText = TableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow))); File.WriteAllText(Path.Combine(baseDirectory, $"index{report.UniqueSuffix}.html"), templateText); } - private static void PopulateByModuleTableBody(CoverageReport report, ModuleDefinition module, List coverageLabels, List> body) { - body.Add(CountsForModule(report, module, coverageLabels).OfType().ToList()); - - foreach (var child in module.TopLevelDecls.OrderBy(decl => decl.Name)) { - if (child is LiteralModuleDecl moduleDecl) { - PopulateByModuleTableBody(report, moduleDecl.ModuleDef, coverageLabels, body); - } - } - } - - private static List CountsForModule(CoverageReport report, ModuleDefinition module, List coverageLabels) { - if (module.StartToken.Uri != null) { - var moduleRange = module.RangeToken.ToDafnyRange(); - return coverageLabels - .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) - .Select(label => report.CoverageSpansForFile(module.StartToken.Uri) - // span.Span.Intersects(module.RangeToken) would be cleaner, - // but unfortunately coverage span tokens don't currently always - // have Token.pos set correctly. :( - .Where(span => moduleRange.Contains(span.Span.ToDafnyRange().Start)) - .Count(span => span.Label == label)).ToList(); - } else { - var sums = new int[coverageLabels.Count]; - foreach (var child in module.TopLevelDecls) { - if (child is LiteralModuleDecl moduleDecl) { - var childModuleCounts = CountsForModule(report, moduleDecl.ModuleDef, coverageLabels); - for (var labelIndex = 0; labelIndex < coverageLabels.Count; labelIndex++) { - sums[labelIndex] += childModuleCounts[labelIndex]; - } - } - } - - return sums.ToList(); - } - } - /// /// Creates a set of links to be inserted in that point to corresponding /// report files for the same diff --git a/Source/DafnyDriver/assets/coverage_report_index_template.html b/Source/DafnyDriver/assets/coverage_report_index_template.html index 0061f94dca2..bbba468d06d 100644 --- a/Source/DafnyDriver/assets/coverage_report_index_template.html +++ b/Source/DafnyDriver/assets/coverage_report_index_template.html @@ -14,24 +14,13 @@

{{FILENAME}}

- {{BY_FILE_TABLE_HEADER}} + {{TABLE_HEADER}} - {{BY_FILE_TABLE_FOOTER}} + {{TABLE_FOOTER}} - {{BY_FILE_TABLE_BODY}} - -
- - - {{BY_MODULE_TABLE_HEADER}} - - - {{BY_MODULE_TABLE_FOOTER}} - - - {{BY_MODULE_TABLE_BODY}} + {{TABLE_BODY}}
From d0613f58444a41ac8f857da698d98f98a8fbddc2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 13 Nov 2023 15:05:00 -0800 Subject: [PATCH 7/9] Whitespace --- Source/DafnyCore/CoverageReport/CoverageReport.cs | 8 ++++---- Source/DafnyDriver/CoverageReporter.cs | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index f67f8f8873a..ac88e4ce270 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -51,7 +51,7 @@ public void LabelCode(RangeToken span, CoverageLabel label) { public IEnumerable CoverageSpansForFile(Uri uri) { return labelsByFile.GetOrDefault(uri, () => new List()); } - + public IEnumerable ModulesInFile(Uri uri) { return modulesByFile.GetOrDefault(uri, () => new HashSet()); } @@ -74,14 +74,14 @@ private void RegisterFiles(Node astNode) { if (astNode.StartToken.ActualFilename != null) { var uri = astNode.StartToken.Uri; labelsByFile.GetOrCreate(uri, () => new List()); - + if (astNode is LiteralModuleDecl moduleDecl) { modulesByFile.GetOrCreate(uri, () => new HashSet()).Add(moduleDecl.ModuleDef); - + RegisterFiles(moduleDecl.ModuleDef); } } - + foreach (var declaration in astNode.Children.OfType()) { RegisterFiles(declaration); } diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index b16952967af..7f176264c4a 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -232,12 +232,12 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour $"class = \"el_package\">{relativePath}", "All modules" }); - + body.Last().AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => report.CoverageSpansForFile(sourceFile) .Count(span => span.Label == label)).OfType()); - + foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) { body.Add(new() { "", @@ -248,9 +248,9 @@ private void CreateIndexFile(CoverageReport report, Dictionary sour body.Last().AddRange(coverageLabels .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable) .Select(label => report.CoverageSpansForFile(sourceFile) - // span.Span.Intersects(module.RangeToken) would be cleaner, - // but unfortunately coverage span tokens don't currently always - // have Token.pos set correctly. :( + // span.Span.Intersects(module.RangeToken) would be cleaner, + // but unfortunately coverage span tokens don't currently always + // have Token.pos set correctly. :( .Where(span => moduleRange.Contains(span.Span.ToDafnyRange().Start)) .Count(span => span.Label == label)).OfType()); } From 9bdbd49d101054106e5f52d98110f2d05f294784 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 13 Nov 2023 15:21:11 -0800 Subject: [PATCH 8/9] feat: import Collections library (#4756) Imports the Collections libraries from `dafny-lang/libraries`, as a new `DafnyStdLibs` library. --- Source/DafnyStandardLibraries/README.md | 3 +- .../DafnyStandardLibraries-arithmetic.doo | Bin 13690 -> 13690 bytes .../binaries/DafnyStandardLibraries.doo | Bin 9759 -> 16613 bytes .../src/DafnyStdLibs/Collections/Arrays.dfy | 41 + .../DafnyStdLibs/Collections/Collections.dfy | 13 + .../DafnyStdLibs/Collections/Collections.md | 27 + .../src/DafnyStdLibs/Collections/Imaps.dfy | 109 ++ .../src/DafnyStdLibs/Collections/Isets.dfy | 51 + .../src/DafnyStdLibs/Collections/Maps.dfy | 130 +++ .../src/DafnyStdLibs/Collections/Seqs.dfy | 952 ++++++++++++++++++ .../src/DafnyStdLibs/Collections/Sets.dfy | 320 ++++++ .../src/DafnyStdLibs/Math.dfy | 44 + .../src/DafnyStdLibs/Math.md | 7 + .../src/DafnyStdLibs/Wrappers.dfy | 4 +- 14 files changed, 1698 insertions(+), 3 deletions(-) create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Arrays.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.md create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Imaps.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Isets.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Maps.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Seqs.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Sets.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.dfy create mode 100644 Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.md diff --git a/Source/DafnyStandardLibraries/README.md b/Source/DafnyStandardLibraries/README.md index 66821390321..557dc9f03ca 100644 --- a/Source/DafnyStandardLibraries/README.md +++ b/Source/DafnyStandardLibraries/README.md @@ -2,7 +2,7 @@ This project contains the source for the standard libraries that are packaged together with the Dafny distribution. -The libraries in this directory are available automatically +The libraries in this directory are available automatically when you provide the `--standard-libraries` option. No need to `include` any files! For example: @@ -42,6 +42,7 @@ The sections below describe how to use each library: - [DafnyStdLibs.Wrappers](src/DafnyStdLibs/Wrappers) -- simple datatypes to support common patterns, such as optional values or the result of operations that can fail - [DafnyStdLibs.Relations](src/DafnyStdLibs/Relations) -- properties of relations - [DafnyStdLibs.Functions](src/DafnyStdLibs/Functions) -- properties of functions +- [DafnyStdLibs.Collections](src/DafnyStdLibs/Collections) -- properties of the built-in collection types (seq, set, iset, map, imap, array) - DafnyStdLibs.DynamicArray -- an array that can grow and shrink - [DafnyStdLibs.Base64](src/DafnyStdLibs/Base64) -- base-64 encoding and decoding diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo index 751e58a33381ba5583c3c82b4eaa82bbd6037e34..56b0d250b4eb7aff55bc8b862c915ac9f926afca 100644 GIT binary patch delta 45 ucmeyB^(%`vz?+#xgn@y9gW+~|?nK@T%s^`60|gThJ(=0m0!-VP+5iA+T@V2P delta 45 tcmeyB^(%`vz?+#xgn@y9gTdG%XCm(fW+1ikfr1H$p3H1&0jBLtZ2&MW4AB4p diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index 66542eda88d397a323493fdc26a967033c8fed9e..ccd7d02381c01b0bb101e9ac1910317d2ef14c76 100644 GIT binary patch delta 16455 zcmV(`K-0gUOyz+A4Nyx11QY-O00;ojYi*GY(0|WsZC9HJ&G=_O0078;0RRU8003}u zZ)b90ZS8$&a~rp^=y(5$@u|9(WK1jEw97gr$M(6d7sn}C$yrpY+#xx##^$1MC>_$4 z?r(o+tPP-n8In?#`(9OINdutKJG!xc`)x8zFDJ{Sx7FQhZMB|!`)vaM&#$syu4mJa zvww8_v=w%6v132ovUHYweUc=jY&=er@8Mro>HTG^K0HYB$-KeJ zl4O?sdXvwxA{i!6UnDL5Et?cK@TrwB#D9|);xmA{f8xP=x%`lgE-Ql^Dv<2}$PeRm zG-7b;4XfSdbjH3XizaLR^b0OZ(Fjy4kV`gbv|*J4p);M)!NasfgcAhkxZF zW|iJw{wteJ-xlz1eM||4aVr@+qW+I$9OKiQo5?U8XADVT7wZN1#UL|*R22OJzz>se zk~$YkBYDO?{YNqkbl75joJ^MUt9=j(@x(9j@H~UG(`-8g(mzvEa)9u@0_hmlEog>n1{A^`mfRlD- z4~7G$r_XG=mnp~&DVKx-?L2OKyii4!!zZrJi6?e?*^tk_IO2EHK z@B112EdP+O-}6aQfT_z5iH*zWhJ%apQOVoMFk75Wd956jgZv2>`gFk-b$B zX~EZn+d=V5am}3WFVo2{j5o98FKJO^v-v%ih2+%go(H$KWZU4w)HZpr zmc}@~4sgmh^f6(*3?SqVMh*+h&~>G$2CNOi*n`@J!0f?p6JYDL4UUVl?a9r28kkjp zP=-{cMMRYrqWgtWB?V5ZYI2v%XE(}|M^(0JKZ)iIVIqqL$qCQ>hZ!+oC_AG7u%@!} zS75~O;sbM7QGWrhA($A&TzcIgrwx9@7U(T z9V@$op1Yc&TSi8|l^ncC>h(o(e4Mm*8p(eqo$YNt6f+oyrd}J>+Y49g@M;UH{Jh_4 zGC1u2&P9kSM$g$4NCT=gA&N3irai9TEgYiii}Tin=zq7QFrjUZGGN@uZ#1J z{^%q$ioFIM)4SrSDMr$e8twXEQ^R(%28IbZ1q!-EG%H-m8Xgpy2L?CO(DYCU+zJ;r z2Zs>O5k2Ip8&XE@Fhc6si>M>lvz@L93QZ?{Di3tyRB z3+NFRpxZl0g=}Fx++9U@l?|rD?B!@W`0OA~d+9hOgzq+{>C+WL>h;7!%5tw|?CsJ> z^&F%$dq|{&lm#jTm#Vrq+|;5gAXZ$*mMMnRK!5%K+ySQGkRVYO_GO{#v0dF3T@hla zuGF}(#l8on+taB-Tj?CS!!{eXkZ6u1a68QgH?tzY%|=V#i26}|QS*AdWS9+R84J~T zk!BE!>LrI;c=qD_Lh##6Q&?<1-`eV3!14}(;(2dt>w+tK(qAUyY<@KzqOpzPb~BoP zpMOn0&aZ&U(EGOx&u^0Mp;HNpC)vLtb~?w+E?`Cu)*O()atX_P`2=5ZGeYhdaS80- zSNVt~J9>7Sv1r1;<>_S3zFHi`MJ=5f3GTWL8F|p~6Z@q{H~s|wV0^u5qVW6^<1fIX zc%Mt&o1mIAhEHG~$}gNTpV*hK`oc9HB!3GfwxIK5Yl}61mN0p%>I#nwsLtE5VcIQZ zP1>kJo2t-36*{_t%n1cCT+_HsV^rv>J;@lT%4)H{oO-%z1_=7^^6I>QRdbMz2AX%S z)?;P_lwb9%ndQMyLORouMR7ke zdUd_gt4EGrwy3qk?*3+@7pl-j6}s+N)K?>c9E32gbk(lpT%Qjz-SXkBS310fxfQSv z)iWBK92knIAOuB<2ZGQAYIrN6!MV!JcmyXZGJ*6yKsiKp#Qw5 zSm_Uh56w%z2a2hJXNFyI2~^@}m0%*uaWY;mB}9qi#fw;oOI0&nmB%T@XP6EuC$J@b zhm4HuS}5TLy_KnLn8ZGqJp{P)iqfJpiL{Xnp zgcrm67Dd8G`l3QGrN$_@dz$Kz(Dd&)Rd|Govf`Wi-!}ka#(%Dz@h1)C*CND zkn?WASWwbH7zUXIP`Q@E@rUXBM<3aeTuYbqA@x-AfOZ1rXn!M-$r?7XvZrs0HXy?F z@EmmPxtQOF0~4&ULly>eGz=T@(nrcPzPY^27XShGK+FcZS}Qe4@B3oTeh_f>1G|Y; zrh08(*pz7=LhB9wFXXunzu}++<*Cg>+06i42=H%|<=jqC55Z;mosy0P#XA11p6r z+UOYEg!oa;o3P&LpsJ@W?Ux?-sz}|%tt3XMjByy{Sg;qJZ3-hAX+|JWHvXBO`sA!4 zPUh&4&e45$Qe(w{sZPgXo{7}GNXeb@2mz`dCc%()>3^xkhmxqsGO|*n*H!lWSO?{? zuiI}a7=jO*dk7Uk62OfX9af9cDxw_5IW%oSfpG~TFbp@-eOFFYqwXb;QhPWSj(rp7 zFirI67`W(BZEsUYFP+${#RE;Mq#Z2jm=b$Jgcry$RMjZX#rh));6llR5F$-SN$zPH zk@GtpH-GT(<3aEjLw8%!xlI>iQqv)|?SJaPr$;F-IaectB?_Zh;74Ct(dR7AZsD?wFYID4ARb*ot7(2ZfJHHrJs+gkQW8y65PUij;;{zUH zU45;G6<_Ch5sfDEJQ~=limh$L8ml}FcSb2s-J|6lUamGT@g8fuOUlhfhSLI%wKcD_ z7JtrkBfPB^$NKtyPj|4HbEudSgt5URL=YBnU=z8NV2yTZjgGq$3J|IZjA~JoBExRQ zWVONx1xJ+83I0$-=)iDe&d@O>GG5F*yIV0vjMz#Zbp=LC99JOBYBMDcros`fZL0T9 z2iOcYw(w!C8U$z1i-lgO)C<2*nK!awm470`Fb}XlYHG_2op~;#!w;9YOUi}AH@ZM@ z&Obw4*e-~w&@QV$IG_rtZztpt9xnCu_{UPL_KuU`c2tJDa?(pvP?Gd^0xnKQFzqLv z6YCI8Y~7@{1~G!y(*=*ZJW9WNpD*ZmfKeJwM+%V>1s!Zf+UwJa0Rt=*?+y- zl}xURgu{EwcLth;^VvtwS|f{tu`{CU3ZR0rRhTPi;faDj^Av&O)>dR@J!}>_-HPZt znQqa*R&o?XViLikTF~Jdj+>b1@>Tsz#gHuA|9NmwSSPy_d<3n2#I%M+-8Zl(8WESU z#=2WDHmNj}J22c}A(*XD1N|!5N`LDCvXj;(sfkwOU@{V6%BGs{bReAZ#`gUG(-1lh zaYX$HxyA~qMAkMlt%aIO5GKHPk${;fNO+UTC42GDKk$k>aW#I5!KpA=n@Wc5DI~NWMCej z&EO=LsVJ_a#VUdY_A;7P!Jo^F4l8(!6D(oeSels4bpg$QM>%wf;`X^<9%Jbh$vf2G zhuFp1 zq{!bQ5ATyf`+`bHQzzrdQPXPF@6(EYKVTbB)<^8NSsLkS0VzSi&?@ptM z&(>NeO-N{=vlRL8CDozB5)}~clp`FP>(~V0!1Qwf;lNFeKYy1kO=!!u93(R8=ph?# zqi)|=y93mE-~l=1V^%~1Q+=_(2P&dtG;+g6n>n-&bv_8UXnJck=duhR{w>;Y*w;L8 z;Nz(x;X?=cj(1qXMZ2Ts$txh-F$lL^ggYEzgsL|~{qkpHzw4X_F-pTH;V9Ws^Y%Xn zCd>gH&i1OYb5&@ND zh_=vPFVex>y1c>?%u&+wcL~PEYLeMOLD}cBN(99(?|;zQE0z#;&;8evp(r<&7;yBm zcMj4SS*Rs02AEcb5MrGuVx6@RqqaIC#A5a-MIF*NXNxdbfWxG2i4k4lhz?zfITTg# zX}BU>a8_M;E1om;Ha82*qy7T#VGf+~Ee%1`ck5OB0_R*mqYtWE*Nk{4 zXK_b&tbeDwSXUH8ob4*kMPcv_C{)5;id%1`?n7|6OwlJtybexe%@uI5+e>|VZbDSt zSzVSjR`17dYSfmdi6rEHlfkf}HkXGe*=sQVqP`<;mHch=Ya&gQxw8)UieuR6%W7=Lo)jg)$z3`cDCqbonMaG`jYe$M`W zH63L~XU8h-K09tEIW-?>-F~icgem`A+(MPB>$#tJuZyDDHi6&k@%4Ne+nXU*1+2d6 zWkF>ymNgu7=KY-W&&~xIW`Zt!_k|tNRt3q|-w9WGc~azD?uW_OWz3?hJtdmLYlB@7*+~)*^bbjZI ztAWXgX!aM*IHQ>*HePD#l=Asu>OEk@MO*=h0hX-@F{VTtOu*9WvT6P+Hf{vHPD~^G zth{RW9`H?J^$E{D`MJD~Y-pm$xmqNl4W^pckx+R~=h}T_FPZ`bR;wVC3CZpn9MhP00^YG+K#j$PG>?NQXf0PjGx73XC_!eu%TCrRu%~*A2ZS|;!4yA&- zA*&0y=o=0+B3S$mp|8Mp zbx*d|vRUaNUqvPT3~9j6lst;%?;1d=Y<6L|k6oD^b=E9#V0q+`5l4qbHo!fw5c9~m zchoct;bv32=BnzXkS5a$v(OTwI4U7P~RmS4DGTY*?-p$sw1^M_8}1@ zS2%6teE9zR8`arBb{5N8C}c|C1F3{h3EfqM;_euxmRL1#bA&s#L*5+juDnOyIY0X_ z`VovgE9!>1g~9b|;<$0e{sS7ZYQR}lgCy3(mPi3R})Fuqv6DN-Wmc80MVlwMf)8+`vg4%=b@lx>N?^D&n3%r=uX@ z^u}Mxz!e*)iv)1}a9>3H8HDcbpmNVp|MYe;-z(r2v7&w>n16ngvrqgW^(=Uxawhi9 z-`JbE<)r{QTnb=bs=X2S0L{*GJ~?~?Khq*%P_?A^Q@1yvr*3cfQ@5yH@CGYJ#o1Jl zQC&zE`Ip@@d_o7FcU?B1A3Ye0)7+ji=YyBpW7wpQYE=*{twO z_@3Ep$bXRFh1miMQQ&9f59eW;34h_;x;EFkYSU8crV|f0ofM&oiEknvX+AK@=Gkn*xL|SQ8(w9;yv_tW5-`o3 zCyejo>F{QhC9l%U$@0T|_+&uMe%G|`>`@i=40_vS4{hAV?hXm0y`$^wY;Si-I2}yN z?(S}fCa8<})$Z-~_PRSgvd=E!TxY+xzq8xfCn5HbfLi$P^fyRH50?e-4Mz;*}8e7Du^wcC5$-cGBxv)}2qcf0MKz1=QDv%S5y*K0GZ zX}w_TV&vXyb@n>l9R{Jb-`(r&FnA1m27h$7$3X7vb=vJ7&7uzCQMz(^}%@FYr+5B{T^fOUa!^K-EVi>Ov>H;0E4&N zMk(41>)k!prnA4_>um4ug6wx0B|Qe7NsD#CSk(hrZNuLTt9?ckQ_Sx6PP^A*(tly3 zvF=&F-EGD_MrW(Nx671mugzG|>h_p9?6+Fo_TKhhdylELQ06vGFTaJywV%ve?bL+X~tti&D z9T-06o?BjlVq@2(#pmL4+v-W4S}d8Q)l|)GR8iBmon{pkt?e|csApXl$*O9$8ye}q zn~p{q&qIr?li4g?iUEI|&99~`(#j|4Z22KeXM-y^>7O1XDOBQT{Xb{RgMZ|#$wKpj zh2nMg+gT%d&hpObbkxwn=lo_iDfleR`)lath@tI<>mRaTw?44gg~eOTdV0RKb`-|Tn&Zl@7flm7$rhgOJo|Pp}^GU+7wUUO>w3%Fqdl0}Sx0<>K5$^u`DrZ6% zO!!w2g++(5d$jC2+Fjzl~s&iKL0^iwt#b2yoU-hJ zNi<^}wwRM7IK37o zrsseDmd%g;(Me#xVmUHHOapBF!06!Ev z#C5N_@2>}9HtL?yKYyOyX8$K!76D|KjpqfR%4es>HC$}lnVdgeFzC!KKYq-ZR@E3{ z_b{O<5og-E;JUit7stxa@DQ7*3t9@qlmV9Q5a=3$hr6*LjcZ##D(^-7_FPnv3}%$E zhIbUUtRsn7MTSO&8)YP?1xcnpZgLrXUEI?guQ@EQNuJjbXMe@p@&Naei3p8KEDJik}pRuv`))6NC;ywM01YT7+H;b&zSDf z)y|R}e6=$Lq<>U3ewu&_t3sGqu?cC$%r)C*itI8+F|!>|O)lmj!K?@Y%iabiU`g?C z3_~I}40=2H1VhAaMls2|eVau?wym=+o5G%L>4E*~*DVu+x%#{2%a<$bQ{x@tf_*!= z&1R&^Hsl}wY$pFWwk>waEOyCz-ufA$E$&qLjsMAk@_)HXm$mUM50k|cYc}|M_*WqC zwkTyFS}svl>!NXeOg*`%>NsaFL<@6NAS_ZIjvoD^{*(pmjS51|ErI42*fMj^GR2p2 zEZ$8g)A@9g4|MM=SAaRu`37o5YY|ejBd&LzS{;#U6-66%llZ8^LRdPR^Tg-T$lzVb zbgCLXfq!7LN?gbszlaNwZp-n2C0+|Tc0%5@)W17fkR(4tq(d5=EIHNu*9G@f;;Us7 zoW$i5bOBq?sw zZ2KRXJ7dQEV|B(k)Gtg_fwGv*t>ooY|1 zdX@(m^A&KeF*Q(`nqglJ<)#bu7NuN%rr5{`5p_&7UMYoLN7E|juMe8OIyu$voxFz7 z`Gcme>@ev^eM@LI}TV#rlH-& zGwvLocv}E*WoJjC^iMC0e-co{?-epPBA5I#=HggG{Y?BfOvL|ydHC;|hW~l9@c-RO z_=oIQJJx@b&kB)$>pRYwEuGn3?QT)}pN;<>fu0Y`p<038I0cK%AFSTi^kbgq8q9%(_`9MAhYVWOW5{T`di zGSqtuHtM?}t?Uin5Ec75`G=*B3CP7_(FYzCbePvqwc3 zn-BbaR2&-t%js0X7ajAD&v_kW3wXxtdX&#kJZWD~3+iD4_8FwTa1$7ykd?vB4D5II zn_M;z>e*}ddp4Pam;5lw2cEDOMa}$?a)-&^-sV38$nl*3Df}bQ>~pRtTz_@7h1mMb z@Jy4ft)y=Uh0ydlK!KJum(1F^ESJ>5pBDiVIbH8BN%D%eBqdY76dm=YqlX8Vwu0{? z%GxwtqDqHX>Bx%DSsPbU3<@JVYhRqR%J5r95hLFcgpd4JR$_&bvo^$$7=+o}J>xGK z&e{ejD(jkdZU=TGI_roibbr>Bhf#Mp~f9LEyP;OfllWV9eMbO*XD(S z9KD5F?%O$=p2%%F*v*>VIA|Y_Ge^SyxvHo3N4-Pl#S7n9=)+PA`38I{5oX-V4fj)E zAdAM5Gd>JmBz5w*6bEuF+L}O*oD=(yQNz_-3|H!C)*KSyGm~ypj({(MFn2UazUWI3oLw$bZ!}z}D*nL3AB=xr)gSk29}J1U-Htp` z;kV;AJg~-Zi&jI?TOGPlCgtuO|R3aN^aw5z|D&c-^wD-kKVI^fnr zr)j1 zA*hb3eG#f=;7hGxF_x=s!LEf$aS#>lnpsoaIw~kn!1yWO7ZCP(p0Sh~%F}J)P$_QW z{;CWVCZi#_6|Y2$>2@|o{_*K`sXUz;#^=I9h;iEr-xmdOQ zqx1n``EX-no_}B4+fb^4G+Q(D z@nJ^~D-U+P#JZt#MfD0M?v8TlI#2V7-3T2bEHejl4}yg1*0ariEyyu}MdK}U#&(!3 z-d`S_)nB}5*yH*w3sqrdfqYT#Hu2XE@t`3>4#xdkN`EDssOJ+JHer;>#Y!a~-JS{% zW+9sgX8;&4X3MD>vxW^;Bx$S5i7Q4?Y^_DsmaFFxeoTpj1eyhx$yDy~2kh7%YLh== z%oOeLzvY_=Dse@@vUwvE|JJPK5;lSu1#A0tv*I7-DBm8?^7aNmq%`Ggq87g}j}JK) zYM2ci7=QaD2zUk$v+~|GHX)&aCjXIC6xx5nfn88Z^#r8HSyke)7SUR_=P*k&7d8CD zX|DkhVB3S}ZpI_jzEonZ*<=)vKWX23|#)3-`^a4QH08tS(Sdo@ajH$;8Oua8ce$xEXeb@;Qv z^#lGqf#o3f^QB8SZworT)e_2LKC~-q4+7$-5rP(;2dvxen@+2SzfutjgzD$4^?$j) zc^4dcomq3gA@(Q%csnO##W)S#YB4~4>q}hk{^d#F1kD1!RO|FoEVkoTq}Guo;D z83kdYj|SW-|Jj0}3hWHRo?_%lt{i{NHPA>lZ96^^`)4fiyi4a-TcWRXuo?MlTRko0 zO{t|UjuJ~I7H^ELsLfXdljKaiZz!TyxetV~LK0tE$6YZY%!%(LJI9Sx(tj(2!1sL^ zNf`LK8=*o4e=fLPGFiu2sd`Ct59j#WZi2IN;$i76(@}bwPaa=Sc^?gMM2?=yg5N|> zd0#?L^GRG!^T}iADeqP42xEmLzO+tNJ(cYO3hDs%6_izYOa--A8dOmCpxv*o8*L_+ zv+0#;a^jMaG!4l)`J1c(Rc zAgd7NpeRQiG&@a4>3p6|aMC5x2WR8uFdNLWw2;Bv8exu@Z+@ma)PKIomg(1n+d=V5 z0lVpbnNEIz1Znw;phfOYknR0V2@-ANzZ4yoU`_XCQ>FRVKnUV}1jO1CcHzo5s2v2< zn=-I;DgRD9EX*38siQkE9;c-;(bmObtX^C18#KPlG%(l52V~;n6cU}ytV4pjKow^} z(p5%cBH(d!((cb&n}1io6K=qr*O%YRDBY$oa}z7SeHFGp43w}r_-b}C8QQH+X4z{tj@_oCY(nW> z$ma!AE9U1`SAj4iLIy^wOLY#=n{WtisDMGJruuF+5>!B227iNgdQU=Fb@u{A++qcl z5<6@EmVL-4A4i$oM=m~+ek>1er_RY0Enh46!*F+e?#1%e)^d}z@2VVCZ{aSF1ltz4 z@3VI|Ba+fj6s6%={5xm9Pwd(QBKZn_Iag%(nS8@5SGB_cMIJ*wxtpnc9B>1Hk6Ahe ztSaQ!>GjcBGk-Zfu3y4N=l?lQPSvSpHHSarPYQ@Hr-8dA=rt05Iu&0dVdn76RT4Q| zC1F6>_ek&tzSz9`CU`yn&WSrgNae{&Q9VqHE(d^@hMrYJne$7L`18$lOdj>iX5xm} zwB-Jt&#z9!gAX9XX7U<|QGDkgLlQkTk42mwL&cDA*MFDgy227D>gOoLim?31Hz=58 zLbIbGgsAMrKx0iXEJudoW2q$71^t0J{VPUaa_~G+(iLy0&(nMaUoGiji60uc00DFY z+IY#9-b*6p*REgXa1BBKW}X%AnR`%iZP>IU`@kQ_sBLJU>?J*Svy=>hEoi)&J5ws{ z!^D*OQ-8zQ53!RRO2XS+SIr4c*x+FFJLQ8C3ppLx@H~l&Tv>gamrLk9kt+AfTP=B2-s^<7FLcG=-cS<^DjJyaYfS zeSc*F!iUx|h6+DqXsDE`*`O^>)qD_}Q@P$kJjbqYH&^E2EjWg)$~E6g)E$=A4@ou> zDU=I00@#6jPa+s-`@6Ja7FZoyg>7~NmP~+YHsk?;EI9z%tX9T4{y(BIL<$|9Lr@CZ|yG9P5 zvE=*Gw$3lAcn-ZEF}ASn`v5fYpLi_R^fF2$F|O^FPZR;L)BNKVcEe|i{f_sQE`NFL zapY3%gwUO$5m|tDH%1Tx32#_7l3)^69!U^t+^!{RYA8X)4k@}SsS={vqeO5Ou`=GQ zL==JcRRLhG{hnSrAjs9+w6uBiqt?E=vZEFviF<0;HLE;z%72Nx6gz1NPYt_o`@X04j6g83l3i}@s~wfnZudhr zhf^WHez?vCFt<^tt4U(}#PunF!aEdzy)Z}m>wP@gw=eW74&~sF@v6%!QnlX5i)2(C z8*g)w%qHkB_>~XmXoJp(jc=+GD3gqpFD9`t2SR$hYlcJM;{M7PH(w7G9#d?c5-#9LNBP4ZuFqW6BC($8j@XRXwmSfIzJp~59m zXg`JJmIm45ZvR8)y0pqUhGH(=4FLVBIpCZz;-3sR}!^--bBhQxsYHWn}RgQ!d(xQb+hrLY#G8 zT{W?@0R&b)?Wf!lJl1x0l}_HzUjIrdKy(7$e}qqg3a~7-Stfu7*ncJpZ4B+{@03r! zTidi#YCPmKd;GK|uo#-bJ9l~%Y9=#?51uwr*WEvP}u3UT>uM`#s=&zYxp zD7aOi>M1_~l*+mDz<=eD?^ygkz8M2Lp6ND|F+YB1f)kC+m`6L#o#IPz1Kd)S8H`Th zD(NK^HVXsOIH*K`z=R5r06X_KAaT8^ICmUzDw^>6DWj5sZ=lujiJ-%(GvRgM{ua>0 ziDrZw|JlLg;$DxbV;zfE-)9Q+t>Q;DGUb;#X=P9tcYpb1>j}QQmtXB)JGAR9 z_=VnHy#*O(iHmr$fAgz$#W2(5t zfSVKXxzq1g&x3zGfXxK6Y;ZFx*x&cA8vyE6NG(X`zTklzy~dVsV}Y8K^V)Fq!2b3@ z2ND46PjK;m^nZB5EAmf%O=xdb#9eW;`9unDtyf`X+fuzY?J3VMqd$te(VM=7o6V zNOmA1xP}wdf}-g2Y7iuP;jPv$Z&Emd1`?q&~MQ!TNp#}RSXBmPz#v{xCFC5T% z0)ZKS7T%xP=g8P-2Il+<%}Jr4*rAbdl}681#Idsu=3k4)gPbQM)l-N|`TIZZ*CffY z>mi?yj6g1bEz$>oUqh5H9$K#-@_`i@IC=tXDfchaH^<1c-grLNAN`CZ%t|uN(;#v!{4 z8pkqh9823Wj2u=p4(df%Qf$aP{@;5KHh(DjGV`+DiS;E_!NSl>cOe7wd^BHOQfKV$ zBBhQSUlwK2J*BqLP?BrHC9caeN|hy`8Kui+No@vL&d`Qdx1!CQ`eMd7G7I0dU8T=r z)jkWm&r)M!f!Jv}`Iy!1=XdzMWkQ(5JuCeAoj#@9-i;_ims2(8-52Vdn>g2rrGNYI z?vCTX)Hjrq@S139NUnaPNfgLXo+0wsA8oliqKp^+%4XA-)0@e#KB>Tr38-yr1!m|4 zfJqrM%v`mmqt#3%)O0+@7Z$i=4sXzPUsftVDIjjHL6_KYZ)jv#stj^E!j>Cf!2ufN znx2#k$m9@bZQjHSZ*=c|UBDs9%ztFCrgzhb7kowOk1{L3j@Lk55YK=#MX6aHM4bK` z)5>{P%-@dTRg&Uey2!`rD7peNP8a@a435PL1(dI8q%c?REqaK4>L`On2Ap83KV9N1amN6QN0oKN*0R<&Z>01GD{_e264`jjeodWg0;(X zjdE393oR(rW}8aOb2f%Qrn7k-#!*@;$AbM+w!R}hJ`n8zo>l80}nk__wn z3etF!Pljlzw!}e_>(|`8H-B5f_5@>OShJR~t4L~<04j5SYd$pXT<9xthb!60g0Doju{B|-YpyTz& zYyl-w6JRrRkzm-o;CeQ_&4*0%2x`-+ww2GbvHNY1UZ;b6zH~mHX4f<4)6eNBAO6+( zSg?T9`E)XOKKyv&e<`krPjA>j?0%kJ6JK9*EeFmFMl5Ky3Xe{XrKX8_ett_o5Uw`6 zJ7qwru)b*@<{Xc;rhfx%{N%U(qL^iW9j0^rG$#X(;G2ab!94j2hnlIGU*)jXk0F3k zfrNkH1|`Y?{Jl9&0Dq#VJrznUd4Ti@9XnvyLn5Io*d?+$%zJX~;MWl0ZzzGTU>_Z; ze<5vz{}?cxpU-Xv^XV+nB5iscgwZ9K?VLtL+}8kDQOI{3Dr4tH4CvBgE}NwE8G-p zTgqm)*-$cgm|dnfqd9-Wh2nCElmBg8HK7OrX0E}ewZx%lv^>spqbYdoXEyd7vO!f{ zaatT4(EyLF`p>cQ;nO6z(y;+5Yno|Ir}I}r7(bY=b$?XDdq$4MI#x%9R@1{N8=pth zK^@DvnS`M_<|qcddYM}2?_9#i+C3U|5kvDTmM4Y`mv=!`((m`s4jbyJzsuDQ?opEi zk$S|#h)wx${`0vxk?$C#4T7>r6=lSnbCl5@cU(ueI@j0qcgeE{mhGC;cakr)5y3i0gGl?cIjnG^DkE~GKO!r!R+yhI+n2IgBI zZGUd71wS5NtK&#A?-0}(*XTs-3KQ{#T4WB))95)K4%@$5KyF2{_C%F$atmy5vbQk_ zVpN-UGg)-d2GGm;LOdqKe(BhE2Q2uTNsG>tz)scgrsMI=Jmq+wDZGC|cea@+$e#if z!1hmv2-vvkTyeLANw^BMNoa;L4vW*KK!1>goD{`$kXwW}_`7qYsK;jVr5Xue+;0o` zR*fuH6XsGK;w}YPNus1z0u5>+93$Wzm;;~r#NYfNOciZ7II{N}c!wwZin|zY*8$A@ z5Y++4Ks<@lXI0F#F9ue+SRKc{i(^W`t%@UHAfA^B;CRw6Bq$m;YZ!d)F))ouO@B`W zlm6p0yBuW;OMPduLFu7Pyo+2l0!<2=%iG!Pf%@(xh0mR3=VG#hhK4I%wTRn=mz3qQwyFc zd*Ur{Vk9h8-53P~jYhy9Atw_yuzzR6%|*hGGA%7pI8wU1tEkBz=CkSK<7oMS*sY7o z*({wD`Fu@JVn*K;jOt4x$iy#UJn=&4DyW|N3Zu{pD6}dztnte{30mqH5_&$EuT2N3 z`VTTmYlD&|n(@ z0%UQV1hb*Agocl@Vu%P;z80?+27Zj)YS&5`yG6YqyG8M8?3Rsqj1{CoRto!6belw! z0{ikHYY-#vM3L{*P*{nlk$)Ejz8PhOOD`s}oVxoWfWDLZqN@gU6TK%kcmsyQU-e({ zE)3bsj?ZWe&J}2WMTQB>0tuDc`(mfUKV&Q#dVO3UOee!!I7}hIY&M(D4wBdS_KWv7 z^TBk?ye)rU^OOm z{4kwlOjkazPV2W~>hnyUU&V$65Mfo=p7w&)f91csGrT{}rq}65)>bw=`sujN2$g;R zq=F?aCj$w?CPB+XrvUEE1p{>0VAPW=KAgX0^Y=3~KMG_kcxF4;d~n4#F~|>mW0qi* zwJYlumjm8)t5|kHB7bo<)v~T5g*erZ^SnM@4=42)%xxo%oD!^7779nHmJX8U>v|}H z>XsuH!wimmzWEMfk$*GW)9S@En>m^{-!UBDd}rY%D%Jrx1<^GR$@*uf&E(l@FcHm3 zVIHR}7qPhp+^B3a^6N@gQ=e&#_{qGsgw);w>h#2k-HI>~*?-fiXHW9sqxDScRD&$h z4awoc624VMGkgWh654>=&S@n@C6VFkTQtg15=tDmqx#CmL*nGx4~>wpp=$PXir)TO z!Gt`ZN_|=A@EV~1okM>OAmLL3_r&Y0FBko_8YjfgCcuXkhFpM>jj(@Uvo!fN?Y)|@ z6I$VzxNU}-L4P65XZp@P$BG8P>2+0q=J9tGy;suK_+Uj_2PG->Qml+3R2x4u`yWF4 z&!lo|@Y(?Mb~+Jun9;tfF@zW*!B%C9q{dhR|53mK+`x`tR|;Q`)DVRi@2TL`@?qB6 zy+85?j8qNR+Ei=OR%>e-Yi*^W84t^@$(Dow#K0_)ixK||P)h*<6ay3h000O8&ueXy Xs3kb#M>`c@@_SV+ws;5N(Etnpr@0fb delta 9547 zcmV-RCA8Y*fdQXP4Nyx11QY-O00;muNNkY}(0?#UY*#5MC0?N<003*~000L7003}u zZ)b90ZS6g2Z`(%N-~B6?0=t$H#Sy8~N4&`4>;`C?AaT>(HH@qdI%cB76)9Irod5pL zeLgcBN^-Xgyg(b#Cnn`Eema;;5Zqc_ z8+SEdpy$!5fkuBjDi+zNPw66BVQAl@qa#G>$y4;_32Of9U(r9O=*iQkr?iKUg?H%y zqx*YNTOA?F2a`s$roR}>tPsq#{%DQS9Ow*Ug!p+J4RQiT;QhX>ihr7q%TJTH5Cl^9XUp zajhJ<5Sn*`*{4*<4%7}I-p~%QZhs7&;@p)*EhhmMwVb?15*`(k_1k%#71^z%f3483 z5Q}ICg`mfkteUJ$VVpvEX#JS1u2-TXKn*;jm{8^sQN7(?N zz7c(O;Hs_BKVR!aqXaej%ZKA-mLow8ml(;j@wf_}M;e|-!rp2aDS1C>o)kbp|ksMpy~^kM^UxJNEk% z^80>s9}8)O|JgsJkDe)y{(ns$4U|V;_jMsjw6F8t^Q=&jE3E7E>BfQpM{&}}sRfS| zR4>w7lxg&#^<$165Wz3Ao56UTj%k0aHe^frQIwP4q&V*KI}~-=Bz__zAkSFz{et5x zc@UxBvssj5S7#3*ot7_kgBBj6qSv!=x;meeUKutH^k@Aj(q+Thw|_-b!hRHGS5bzk z@3wHYHDlxnZbFgV zh36_F@3u762uD}DB!5~L)8|#CkB~~*Tq8vJgfD%(9u17~j}^rO0Mw3B_gY8A3celP zj`ENB4GOv+=d+JUHjDMgL7u0J;=8H~CaLO?M;)!{wocO4NT|$?a%J`tV00=*K+E5l zuqeZ&v{C@yZBy71j%hF3f)nNw?N7IdHr0)B8*rPAtzfYVM1Kwpj%hV8{MC;&i!ovy zrYYMp#<=a$L6Dh@3=x)*Yig4xtS!OlNo`ADda~OF*k)s$d6A8Mwk+n3RRvtifTpza zn9_=(UrAHq;FzgKcTure@<{GA*-$)@kPYA>t2!tNEBw0!F+wC8SpbVBIQVlgG`-ls z3{eEYl?($}%zxz9EJB`tNZRM~_vvqV9x}X5+PDN+qy?&T)89^pxBXLH3U{dO4r6W! zj&2bf!)A2!G^*8B(dlUvck9t#qomUzsTjdHmi=O-U*Fv=A>CF``^B)?Kyc9i$)$@c z#LxL0vxd16jBw5fn|fZqTNzB%Ru|1niZ^LTCntodJAeE*)*koq)73>H9vTxGE?!BF z#Li_Zn-y&^i#B7h?4gHQ2}2f~lmyX2hvlYbr3`W*14)}4C^6)ew%nx6put76#}0|< zx{Q$o43{~!J?2R4tlN@>p~D{I#M3cRI(9w%TEcSe4vOib|65M;|AFFiCZDTS$pbdC{7;g~e z@`cT4Hx1!sI+~Bu=ac#9i$ORXrTv@$v0J*P&6kU)vzbMd7GBH5+k%N|8$=25fJ9L( zQ&Ipag@!kEsK%E=t!f`#rz)hn5)W`VP&qgTSbt=VL)K_UY}2+WDnJe4My(Fk#J5wv zEt@*ljn3fP?XzwV@y?MbZST_2a*=1Z>11s?(a>uzd|i*UjMLE~MWq^P5&}Y1J(F-# zUA?%tr1F-_6q=YX4i4Iv`1KAz;zj%5;F1`6G+am1w78y+mE4ACTTY4})7huu8Vea? ze}97Ld>FNkjZV0Emi~@wrweu1C0>!k?;I3`Wek>l@)W=I>b8ue3AVC!s;ZND1UAp zGU6}PJwl<=7r#7knbF?i+g>3Af2i4r%w5Bf+yzPY5k$~M zt6J_FVk2+inC{A5gqy(ZH4M&PHh<}X*{fBWy@qi1YV+*X+EMm`r0>aIEh~Gq!R)20 zS_JIYAC|q84lSia%gjYXo(WhIQfY;|wwUCGB+0bO(_6bVy}703@DGkz$xQ|f&Xf}Z zXT<^m*aDQ^a&LOGK(XlPDU^q<^aGH^lAHAVkP&d|bV6szZ3rhfhwFPqK!0^pT>>?y zG+AoPrOWAz9FrU*QX4dRAeKxlMX=~WX9avPwb>JDhQdf~&iMHq5~ZC8cP&dB10+-` zGbt{=27)9SQcQRy4%W-1jBs^4ed;T5p>7gYd7UC-hC~oNfi1!9axxG#HNq{hm6>fY zI%mxj#xLLrW-JHDpnU)YLw`HIJJyNZiy*tG(rp}&HPUKacRzP+ALL#k0nb~@gZaFa z5kM905V9kqtXPAW;C4;mK-ARRx4>2{(0I@}{XdLfz!%Jw0)PzK2SAWJ+|QiWy;{tt z_;qYf)-bqLew1qm! zsrG(7zsN4#F99%1j2HTbFq{ATP)&9Lw*(XnhqPfWA6%-OX7GG9CcO0A~Tv zT#M8A^SpR#6I(LZ5-meK_2lb-`UK3dMqnl@#e~`(yv}1x2!FA|3v6SL>H0oCFo7Bq zu+ce3Q(-Hzw26{~mseNW3PVsa0IPwf)iO&G`@T@HA31{kNFSoLajfyB-bp^kvfh8X zk5^22$>P~@`Ca!GAzagq60N~$CtEM?C>jY_+tIo!GYw#k##D&E*mrYC_YZEsp(9{f zj99r~6Z(U~q<>>+1q@7qOuF3~7Nb~g5lC%$80#!9K%`Ndft5n0V?+%uOMI{7Wm#_^ z2#vI*c;UnsqIHwDk{ThHVmHaYV$ZwU&oM^wPMCJ$7JFdrpzPdNx&-$~5E!>$K$ycnC? zk}h<}ZTlk2Ut1JsQvXo`+-u8sF^UX^H<32$Ng*i_;&DC7HZ?*2bXSyEQhSjmQy?=)h zY=0LV0;dFSYSawjgasVfR6>fgM_k$?F?T{?g7zsz`(BbfX*Y1P8gN3vP^EW)-&GMB zFwC0MbxaAY7cM1VJ6*vJOB1 z3YhvPu86R^sjnqJG{uU$#tb*%Gu+CPUYLWDNpIo^ajb%g_pBh606}ciNpI7f4bcRQKhHg`6+4UDzO1l-frM3jP{lmeupj5Nhv?Mf!oMBL@Q7CRlo+<)`g zd!My>UJm-sh;FKY0AmYSD`=_<1^>%S1V&h^D9oDMEyQ%oWAET}3kFsxPyiDX4;5iW zhv_)x#6+}LjWdBInH&FwGbwB`yQFf&R(+4t8klt3!MtR6Lc#{`-JG>aP%1ZIn8ku~ zwgM&kDzla54rV9KZKfu|jGdDakAG0MwR{5s4aQsh^Z!pn;Ax1V>U)@LRG3PX-C|m8 ziyq{LSJ`YZAzFN23>F2ynn0X0gzibLIp4qIt74t47Y7FhHoBdxrtLK|x{y6*cXwJ) zg8J0mo1Uqqei%%$YCA}`+Bxdo7nxnLrTA!lmCvR6)Dg5QmYtUV=f> z(_fq2b3t|z-oI{YfMyVt4!h&>JmIG(*|xC+kHLSRMlp9cOV-uF#u99kf_(s!`=AoK z+{V;Y88Dqt)mD}LIA!iBRDb;~%oUYhTPdBvQ33=f;Je~rmYijBVy~$nsVgt501@b~ z(X`1W98pYc?|kG#nA-*kp?M=L$uPwbjJ#P{TjyF4h*Yn)RLO0;Uwe ztzC>Th@GG2<5rEKXDW4Q@+!OZ!s!HCGll~_> zeKlC=XPo4*(-;n(!-MzB(J0OHzlm^34AShY)E;a=P0xOHvmkjj$R-GJ?T7R06cK^? zB2ZD5N7KRNYQC7J<9{E(voOy;@R9D*We;Fxq>$%p+2SQkRKdTOEyLuE@Y}LS<%V_km_O26V#Py=Hlz8_g z)vm)50R$)I1iRKcwjtQD{OlmuaZ}@mvR4zrv$X)JIJNhXjeoUKcPPEx0IGf9K?%yI zs0jwfaiPKocT|qiunikA3TO#*K1dzWu-?^Nur~GZZyw{rzVZVHHl4f@J~oI?tiuu} z*$H1K4oWv8+@ zW;{Zo}8lHz|voUR#o`2{F^b9)zX=E1Y6&C^wn}Un5 z#7kJR5n<3)M};t-e==3O?9JFBObp;Ss%dIeu5eTiUD7oa-tmFEBfj7)+;{`enOd8h zDdpaHq3&UJoboL#L3lp4xZG*f@zYu%8F6sN^)uq2x^~Tob#hikbcZnA`A|U+)!8nW zoEHY!fPVr_*h^_^S3>WCLv*Skps>o`rtzI3EK2(}5%oE7S z_id74pf#75DCI#B>b<4yCz|cUsH)k%1I7lnpX|u?6WjKaVB1f&wEaZ2{lsJY$>z47 zY;XI%Bui|+YLdk{?2lKy%1yQTooNH^thwH-o(u&~Vktib`iKDG`x)n-jSDj5 z0-gKr3%#NZEqp~OqFgY?i8@wE8M3z{HUYpJA?*NACQ-HYn4HjdX?9UOE(7&tMU12$Q1_ACIaJz zgH!&I5AoD__m0&KzJ*6K0k4M#P9uCTS>3m0Io`wod#7ybXjkJ(0nyEK>4Bk|3YR3n zw^NjE+HrX6CQEtVYnc&Zy(F2zyo@I(v7-Cb#*xSD);; zyr^torogpYMMGOGHE*J!@;RO9_ny6Yj7_dpXUYlEY7(f`WJ|4v%~FB0+8(U}VSgLX z0Le&Iq%}|ZT`9c(Y?QB&Lu=ts*|Af-_ z%Mg;F_O&V)Q~7Q-kC+fNI+rCoSN=mAdl3W@>zV+m)LC;OrSV>M=g$ip(dCH9LDNHbRpFt+zQz{7Vl6=8 zu*Sv(PDK^5F?r=!V99+Z(tve{;4;R@w9ewjwMwYH)Gn)H$gY27Rv`PAU4L-A{VsF& z;!0p{t2%peSjL~F#QGyGqrARVEn}lvF32*fuB=tBdf-yZxf?QE$tAZfYr?EFR|vdF z*<2^N?|L{O#<{9AdG*Dgx*iTY8+>2F+etkfJL+M`LjL6SFt{35UQ@-PHI=J4s9xum zR?J%!!aL)=w5;Dz0sLQ4R(}FX{uJXHJ_N?%HC^+>kSYqQcrzMM<=Go+3< zQ}R(Pd)I(s%5oQm`LQdxqfT2TcDx?BXTp`kB3sbzcoB2Yv?rU;e$O<4r|8@?>E2_# z+;H!}*=k>b^Oe1K3+mACN-o?b5_Ijd0L3?Snj^G5c9#T#Z#Z@0Y=8Ln_cy}D03!3v zS|DOdzXuXTPYK^4N-=i~L$6o`aCwB=w?keY?hf7~Z=9dqjeR&P&p_Ldw=kGdjUG1+ z#P6_(ss(4L1u?3D%Of`90<<^lytCfVeK1>c!R+V}GZ%o05c5sk<{Jl_Z&G5ur6(!= zC(PHpLg1dv*YV=WiNyvR!;BNX8jGTbSvc{7`SuA;lS^k^1>6&8AaXJeZ~TQEoQnavNI>oH#s$=$ zPUzMSD)S8WFRy1sKgYL-<+UXh`Z7b0$U*9b^FZZ-?ww!in}504r2rYe6hMBdc1iC6 zT3lpgad?S;4)O>=6`CTSx?Q?Hb-N^=x>d$GZ?HmKoX;ss=ArO~#vI7aFoc_-&drcf zMd0fElzh5Z8);kyp=d?$vvf0{cGDC}U1KTe5-a|CFKQ#onQy9FIonv0I{-E58iSVm zT!zOwE6N~>&VT9JY9}3)@qJxFQ5iu17sLHh*7wy>o=XQTUl9R&&z!!Q8gT)p4qbA^ z3B`Bcmz;PH7RcaYD2dXt%^fIeWaD-M**ojORN+nlgpb?Y)VgOLeQO+_5GY9gbnfVP zd;!IC3dBxAxB5c6G+0Op{B*}Y@r>Kt2Cd}>0QNGsJb!3k2hI&rlkO5c%)+`tQV=BS zgp;_WkqyN>#|B`vUfQ-=stGp1O3CXAA%O^%VyF=1M_XLsL_?PE%WbhR5|6!>#a|Vg z9n~R-WLY=gcf4ydDny~zj|~=)ZrQeQX{fFn{DCf*5L!MRNi*C!)CxHMb@3F4W!; z?JW>|PmWLeP=~%GuLEL;RTRB02qf-`KHW~I1;R;GR(ic&0yET7<3!PUuNk-F zxZi4bo9*sl(u#YnxZCfw5SekO-*3l=YS=E2xk$aYn@K-ubrFQ-VXNQnB6x^;1hm&i zAiMn}j@z(^5=BOF+(E)=_7NSJjQFtAPJdb*#7w`_Z1xdZhs|EU(@MIBhX@CfdAo`K zZymOgX#4GEvv(M`Vx;BPp+mr(SQJTx7471hg#_cxJ4q^?VM|fKuBt67uGw%10vGrplie{^g+~Kg1GitVpNkv(eyY zFv^Ox@%UYOvoIc!^73!S!#w+%8jqe8#)G#@`$>KcJbE?At)BB6;OQBeY=2i;+ zyJ(8hL>EW8E{;`Mh?S;iMU52y^pcLFsFtE>bvi4KqGwX;{L&6GOMf^aw3%%omLjFV zkYE83-Y*E~OHC+5jmmRI`7|xA=i>-@r$Trm+6~z#9A;M;dQJn$e+Y3t4MOG+J&xv+ zF|`brnc)ujce7oX8}2~fk(T5$CbA6fR^OFOiSEP<)Vg=aT;YIzx$6 z06f+DKUR$oX=R20W&`8^YNt~Pl=YPFc?{$)sWN_+PismK>kUwLr6ZEON(}E%exA%n zHC4}z$PLwSN1E_zWo9AocJddUfQ+7^M!hhRNJOLZ`VNtVHYoIix(ogzOogg#D@Z{_W2m}_aoRx&cu8=hU(^&p2{N;g{#2HR z3hv9O_Az?$F#34gj2=G0Z=Y4U)-|beurKB}YrKc222oS5UUdTbOPi$B@#}r8Z+k zW`?Hh1?+gFiO<$fh!wt+GeEfaiBi&9$mj$xh^yHtl2M7mp z?0=osu78fAe@2fVpGN;OUXL;cR(ONU)d7E8Tk&pqI)|U5pL@o4KUQ%gS|!TIKdx%4 zn7k%Lza(Vif#7`=nVzri)^$BI^DcfglqOuH}TAGZnGl0KSIPBn@)`G+1O&%Zg;ph;#49Yz|vyh zJ%1E5yv_}I`H7KfL4pti=*B7yo^0E*Zm(5|&`fn}5)^1K0d}mN%}|O+$J?u9g)d)R zYpO7`baxkM$?uEBeD-Ow-XV3Hl5)Nn%<`<*Fp|hPUcsrp)}2E9>ZWsE3?^?D;}ma6 zsY2>I+h90Z4uj^+QZ#m(r9sUcT}sbJ#ec?pfTq6#PAYKlc9HH_0}x?O?DU+)A3#Bg zR9ys~q59-@FiB^lloty-BC?`ton=G*V>-wS9ET@qp1)ZjiU$*uq6UiMs28f68c|MP zznv?e6(f!G%Xf?fQC8fc|4D<42MV4V8R;!+@}IIL36-d-RDa1^ z39xks1FYH4!rxIbTBHF|{=_=EnBeUj$$BN>`@}t1g^8Q?bBdcbR}(iIL~1N253G|r zrp^~Aay?&{aF=+y zMP8iI#lH7NHkqho&RDw?CjEqfhktxy62+mZ95*89#uc)Lgh~OGevTi1XSiuz9j;|3 z6~11d!4zC@(Bx_dS(Z5_RD2f&=_OXpeoj#}baq-B&1d6`2285Kbg`H(j-oSiwuKxJ zIEvmZi_v_VvhxCG`o|9i1a%ed?I6$hDKGlQ{rwt2AT){>Fvxb3H#a1ZKYuzujh;q7 z&u1yJmG=l~?UpX0o%0I?RL9~+0rUkFJo<0scXO@q?P7j2_=Lu?fhWJ5))1o%_b6)3WW3bw0N`ND{Yu<4v!C=4vNt=c^%Fkj0Sni zM1?9oS@7Me?U?SG*33|VM1P#mg|2IgL9mC&Y0geJqls@+zpeX;z(klm@P7zV@uzo|Kgokf z8@SXv0kXt4n1pjp`C1nt@Cu$qtw9Mp?}7{!B!-x8UN0w!8nNGxYL%S_q{;Ljm>}vy zVgAF6>>W0;3NB;;<>re@hcgWQR|5SEgT#;ODkjorbG?YCVUnPGWH3Fb(G>!?Zm9ob zF*BFn(BH$H9k2?+#ea1-6asQtKC*WbIVw5;;ny_%g(crAcF(mf=ur)A6Ox$LOR18E z5SBlL_;+Fb=ghbTc;NtIV-_ttWVR1=2A4n>*if-BZlouWA31)NGtw*AO6BVbPf_Y? zV5oT2Vwm<8*v|Y8C*|o{xavOh)%^{fb-z+-R@1WSvLz(|kQJEeFi31yDJdmhp(FqRYv=%zwLmHcnI!-K008DNBkuqJ diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Arrays.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Arrays.dfy new file mode 100644 index 00000000000..a1b8e4613c5 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Arrays.dfy @@ -0,0 +1,41 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module defines useful properties and functions relating to the built-in `array` type. + */ +module DafnyStdLibs.Collections.Arrays { + + import opened Wrappers + import opened Relations + import opened Seq + + method BinarySearch(a: array, key: T, less: (T, T) -> bool) returns (r: Option) + requires Seq.SortedBy(a[..], (x, y) => less(x, y) || x == y) + requires StrictTotalOrdering(less) + ensures r.Some? ==> r.value < a.Length && a[r.value] == key + ensures r.None? ==> key !in a[..] + { + var lo, hi : nat := 0, a.Length; + while lo < hi + invariant 0 <= lo <= hi <= a.Length + invariant key !in a[..lo] && key !in a[hi..] + invariant a[..] == old(a[..]) + { + var mid := (lo + hi) / 2; + + if less(key, a[mid]) { + hi := mid; + } else if less(a[mid], key) { + lo:= mid + 1; + } else { + return Some(mid); + } + } + + return None; + } + +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.dfy new file mode 100644 index 00000000000..07230ef9037 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.dfy @@ -0,0 +1,13 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module contains submodules each defining useful properties and functions + relating to the built-in collection types. + */ +module DafnyStdLibs.Collections { + // This module currently contains no definitions, + // but is defined so that the module comment appears in generated documentation. +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.md b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.md new file mode 100644 index 00000000000..484a5efb7d6 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.md @@ -0,0 +1,27 @@ +## The `Collections` module + +This module includes a variety of submodules that define properties of +various collections: + +- Sets: functions and lemmas expressing properties of Dafny's `set` type, such as properties of subsets, unions, and intersections, filtering of sets using predicates, mapping sets to other sets using functions + +- Isets: function and lemmas to manipulate `iset`s + +- Seqs: functions and lemmas expressing properties of Dafny's `seq` type, +such as properties of subsequences, filtering of sequences, +finding elements (i.e., index-of, last-index-of), +inserting or removing elements, +reversing, repeating or combining (zipping or flattening) sequences, +sorting, and +conversion to sets. + +- Maps: functions and lemmas to manipulate `map`s + +- Imaps: functions and lemmas to manipulate `imap`s + +- Arrays: manipulations of arrays + + diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Imaps.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Imaps.dfy new file mode 100644 index 00000000000..069465c1962 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Imaps.dfy @@ -0,0 +1,109 @@ +/******************************************************************************* + * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module defines useful properties and functions relating to the built-in `imap` type. + */ +module DafnyStdLibs.Collections.Imaps { + + import opened Wrappers + + function Get(m: imap, x: X): Option + { + if x in m then Some(m[x]) else None + } + + /* Remove all key-value pairs corresponding to the iset of keys provided. */ + ghost function {:opaque} RemoveKeys(m: imap, xs: iset): (m': imap) + ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x] + ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs + ensures m'.Keys == m.Keys - xs + { + imap x | x in m && x !in xs :: m[x] + } + + /* Remove a key-value pair. Returns unmodified imap if key is not found. */ + ghost function {:opaque} RemoveKey(m: imap, x: X): (m': imap) + ensures m' == RemoveKeys(m, iset{x}) + ensures forall x' {:trigger m'[x']} :: x' in m' ==> m'[x'] == m[x'] + { + imap i | i in m && i != x :: m[i] + } + + /* Keep all key-value pairs corresponding to the iset of keys provided. */ + ghost function {:opaque} Restrict(m: imap, xs: iset): (m': imap) + ensures m' == RemoveKeys(m, m.Keys - xs) + { + imap x | x in xs && x in m :: m[x] + } + + /* True iff x maps to the same value or does not exist in m and m'. */ + ghost predicate EqualOnKey(m: imap, m': imap, x: X) + { + (x !in m && x !in m') || (x in m && x in m' && m[x] == m'[x]) + } + + /* True iff m is a subset of m'. */ + ghost predicate IsSubset(m: imap, m': imap) + { + && m.Keys <= m'.Keys + && forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x) + } + + /* Union of two imaps. Does not require disjoint domains; on the intersection, + values from the second imap are chosen. */ + ghost function {:opaque} Union(m: imap, m': imap): (r: imap) + ensures r.Keys == m.Keys + m'.Keys + ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] + ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x] + { + m + m' + } + + /* True iff an imap is injective. */ + ghost predicate {:opaque} Injective(m: imap) + { + forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] + } + + /* Swaps imap keys and values. Values are not required to be unique; no + promises on which key is chosen on the intersection. */ + ghost function {:opaque} Invert(m: imap): imap + { + imap y | y in m.Values :: var x :| x in m.Keys && m[x] == y; x + } + + /* Inverted maps are injective. */ + lemma LemmaInvertIsInjective(m: imap) + ensures Injective(Invert(m)) + { + reveal Injective(); + reveal Invert(); + } + + /* True iff an imap contains all valid keys. */ + ghost predicate {:opaque} Total(m: imap) + { + forall i {:trigger m[i]}{:trigger i in m} :: i in m + } + + /* True iff an imap is monotonic. */ + ghost predicate {:opaque} Monotonic(m: imap) + { + forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && x <= x' ==> m[x] <= m[x'] + } + + /* True iff an imap is monotonic. Only considers keys greater than or + equal to start. */ + ghost predicate {:opaque} MonotonicFrom(m: imap, start: int) + { + forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] + } + +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Isets.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Isets.dfy new file mode 100644 index 00000000000..108a1a8e03a --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Isets.dfy @@ -0,0 +1,51 @@ +/******************************************************************************* + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module defines useful properties and functions relating to the built-in `iset` type. + */ +module DafnyStdLibs.Collections.Isets { + + import opened Functions + import opened Relations + + /* If all elements in iset x are in iset y, x is a subset of y. */ + lemma LemmaSubset(x: iset, y: iset) + requires forall e {:trigger e in y} :: e in x ==> e in y + ensures x <= y + { + } + + /* Map an injective function to each element of an iset. */ + ghost function {:opaque} Map(xs: iset, f: X-->Y): (ys: iset) + reads f.reads + requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires Injective(f) + ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys + { + var ys := iset x | x in xs :: f(x); + ys + } + + /* Construct an iset using elements of another set for which a function + returns true. */ + ghost function {:opaque} Filter(xs: iset, f: X~>bool): (ys: iset) + reads set x, o | x in xs && o in f.reads(x) :: o + requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x) + ensures forall y {:trigger f(y)}{:trigger y in xs} :: y in ys <==> y in xs && f(y) + { + var ys := iset x | x in xs && f(x); + ys + } + +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Maps.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Maps.dfy new file mode 100644 index 00000000000..311b826b736 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Maps.dfy @@ -0,0 +1,130 @@ +/******************************************************************************* + * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module defines useful properties and functions relating to the built-in `map` type. + */ +module DafnyStdLibs.Collections.Maps { + + import opened Wrappers + + function Get(m: map, x: X): Option + { + if x in m then Some(m[x]) else None + } + + function {:opaque} ToImap(m: map): (m': imap) + ensures forall x {:trigger m'[x]} :: x in m ==> x in m' && m'[x] == m[x] + ensures forall x {:trigger x in m'} :: x in m' ==> x in m + { + imap x | x in m :: m[x] + } + + /* Remove all key-value pairs corresponding to the set of keys provided. */ + function {:opaque} RemoveKeys(m: map, xs: set): (m': map) + ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x] + ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs + ensures m'.Keys == m.Keys - xs + { + m - xs + } + + /* Remove a key-value pair. Returns unmodified map if key is not found. */ + function {:opaque} Remove(m: map, x: X): (m': map) + ensures m' == RemoveKeys(m, {x}) + ensures |m'.Keys| <= |m.Keys| + ensures x in m ==> |m'| == |m| - 1 + ensures x !in m ==> |m'| == |m| + { + var m' := map x' | x' in m && x' != x :: m[x']; + assert m'.Keys == m.Keys - {x}; + m' + } + + /* Keep all key-value pairs corresponding to the set of keys provided. */ + function {:opaque} Restrict(m: map, xs: set): (m': map) + ensures m' == RemoveKeys(m, m.Keys - xs) + { + map x | x in xs && x in m :: m[x] + } + + /* True iff x maps to the same value or does not exist in m and m'. */ + ghost predicate EqualOnKey(m: map, m': map, x: X) + { + (x !in m && x !in m') || (x in m && x in m' && m[x] == m'[x]) + } + + /* True iff m is a subset of m'. */ + ghost predicate IsSubset(m: map, m': map) + { + && m.Keys <= m'.Keys + && forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x) + } + + /* Union of two maps. Does not require disjoint domains; on the intersection, + values from the second map are chosen. */ + function {:opaque} Union(m: map, m': map): (r: map) + ensures r.Keys == m.Keys + m'.Keys + ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] + ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x] + { + m + m' + } + + /* The size of the disjoint union is equal to the sum of individual map + sizes. */ + lemma LemmaDisjointUnionSize(m: map, m': map) + requires m.Keys !! m'.Keys + ensures |Union(m, m')| == |m| + |m'| + { + var u := Union(m, m'); + assert |u.Keys| == |m.Keys| + |m'.Keys|; + } + + /* True iff a map is injective. */ + ghost predicate {:opaque} Injective(m: map) + { + forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] + } + + /* Swaps map keys and values. Values are not required to be unique; no + promises on which key is chosen on the intersection. */ + ghost function {:opaque} Invert(m: map): map + { + map y | y in m.Values :: var x :| x in m.Keys && m[x] == y; x + } + + /* Inverted maps are injective. */ + lemma LemmaInvertIsInjective(m: map) + ensures Injective(Invert(m)) + { + reveal Injective(); + reveal Invert(); + } + + /* True iff a map contains all valid keys. */ + ghost predicate {:opaque} Total(m: map) + { + forall i {:trigger m[i]}{:trigger i in m} :: i in m + } + + /* True iff a map is monotonic. */ + ghost predicate {:opaque} Monotonic(m: map) + { + forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && x <= x' ==> m[x] <= m[x'] + } + + /* True iff a map is monotonic. Only considers keys greater than or + equal to start. */ + ghost predicate {:opaque} MonotonicFrom(m: map, start: int) + { + forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] + } + +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Seqs.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Seqs.dfy new file mode 100644 index 00000000000..1328113ece5 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Seqs.dfy @@ -0,0 +1,952 @@ +/******************************************************************************* + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module defines useful properties and functions relating to the built-in `seq` type. + */ +module DafnyStdLibs.Collections.Seq { + + import opened Wrappers + import opened Relations + import Math + + /********************************************************** + * + * Manipulating the End of a Sequence + * + ***********************************************************/ + + /* Returns the first element of a non-empty sequence. */ + function First(xs: seq): T + requires |xs| > 0 + { + xs[0] + } + + /* Returns the subsequence of a non-empty sequence obtained by + dropping the first element. */ + function DropFirst(xs: seq): seq + requires |xs| > 0 + { + xs[1..] + } + + /* Returns the last element of a non-empty sequence. */ + function Last(xs: seq): T + requires |xs| > 0 + { + xs[|xs|-1] + } + + /* Returns the subsequence of a non-empty sequence obtained by + dropping the last element. */ + function DropLast(xs: seq): seq + requires |xs| > 0 + { + xs[..|xs|-1] + } + + /* The concatenation of two subsequences of a non-empty sequence, the first obtained + from dropping the last element, the second consisting only of the last + element, is the original sequence. */ + lemma LemmaLast(xs: seq) + requires |xs| > 0 + ensures DropLast(xs) + [Last(xs)] == xs + { + } + + /* The last element of two concatenated sequences, the second one being non-empty, will be the + last element of the latter sequence. */ + lemma LemmaAppendLast(xs: seq, ys: seq) + requires 0 < |ys| + ensures Last(xs + ys) == Last(ys) + { + } + + /* The concatenation of sequences is associative. */ + lemma LemmaConcatIsAssociative(xs: seq, ys: seq, zs: seq) + ensures xs + (ys + zs) == (xs + ys) + zs + { + } + + /********************************************************** + * + * Manipulating the Content of a Sequence + * + ***********************************************************/ + + /* Is true if the sequence xs is a prefix of the sequence ys. */ + ghost predicate IsPrefix(xs: seq, ys: seq) + ensures IsPrefix(xs, ys) ==> (|xs| <= |ys| && xs == ys[..|xs|]) + { + xs <= ys + } + + /* Is true if the sequence xs is a suffix of the sequence ys. */ + ghost predicate IsSuffix(xs: seq, ys: seq) + { + && |xs| <= |ys| + && xs == ys[|ys|-|xs|..] + } + + /* A sequence that is sliced at the pos-th element, concatenated + with that same sequence sliced from the pos-th element, is equal to the + original unsliced sequence. */ + lemma LemmaSplitAt(xs: seq, pos: nat) + requires pos < |xs| + ensures xs[..pos] + xs[pos..] == xs + { + } + + /* Any element in a slice is included in the original sequence. */ + lemma LemmaElementFromSlice(xs: seq, xs': seq, a: int, b: int, pos: nat) + requires 0 <= a <= pos < b <= |xs| + requires xs' == xs[a..b] + ensures pos - a < |xs'| + ensures xs'[pos-a] == xs[pos] + { + } + + /* A slice (from s2..e2) of a slice (from s1..e1) of a sequence is equal to just a + slice (s1+s2..s1+e2) of the original sequence. */ + lemma LemmaSliceOfSlice(xs: seq, s1: int, e1: int, s2: int, e2: int) + requires 0 <= s1 <= e1 <= |xs| + requires 0 <= s2 <= e2 <= e1 - s1 + ensures xs[s1..e1][s2..e2] == xs[s1+s2..s1+e2] + { + var r1 := xs[s1..e1]; + var r2 := r1[s2..e2]; + var r3 := xs[s1+s2..s1+e2]; + assert |r2| == |r3|; + forall i {:trigger r2[i], r3[i]}| 0 <= i < |r2| ensures r2[i] == r3[i] + { + } + } + + /* Converts a sequence to an array. */ + method ToArray(xs: seq) returns (a: array) + ensures fresh(a) + ensures a.Length == |xs| + ensures forall i :: 0 <= i < |xs| ==> a[i] == xs[i] + { + a := new T[|xs|](i requires 0 <= i < |xs| => xs[i]); + } + + /* Converts a sequence to a set. */ + function {:opaque} ToSet(xs: seq): set + { + set x: T | x in xs + } + + /* The cardinality of a set of elements is always less than or + equal to that of the full sequence of elements. */ + lemma LemmaCardinalityOfSet(xs: seq) + ensures |ToSet(xs)| <= |xs| + { + reveal ToSet(); + if |xs| == 0 { + } else { + assert ToSet(xs) == ToSet(DropLast(xs)) + {Last(xs)}; + LemmaCardinalityOfSet(DropLast(xs)); + } + } + + /* A sequence is of length 0 if and only if its conversion to + a set results in the empty set. */ + lemma LemmaCardinalityOfEmptySetIs0(xs: seq) + ensures |ToSet(xs)| == 0 <==> |xs| == 0 + { + reveal ToSet(); + if |xs| != 0 { + assert xs[0] in ToSet(xs); + } + } + + /* Is true if there are no duplicate values in the sequence. */ + ghost predicate {:opaque} HasNoDuplicates(xs: seq) + { + (forall i, j {:trigger xs[i], xs[j]}:: 0 <= i < |xs| && 0 <= j < |xs| && i != j ==> xs[i] != xs[j]) + } + + /* If sequences xs and ys don't have duplicates and there are no + elements in common between them, then the concatenated sequence xs + ys + will not contain duplicates either. */ + lemma {:timeLimitMultiplier 3} LemmaNoDuplicatesInConcat(xs: seq, ys: seq) + requires HasNoDuplicates(xs) + requires HasNoDuplicates(ys) + requires multiset(xs) !! multiset(ys) + ensures HasNoDuplicates(xs+ys) + { + reveal HasNoDuplicates(); + var zs := xs + ys; + if |zs| > 1 { + assert forall i {:trigger zs[i]} :: 0 <= i < |xs| ==> + zs[i] in multiset(xs); + assert forall j {:trigger zs[j]} :: |xs| <= j < |zs| ==> + zs[j] in multiset(ys); + assert forall i, j {:trigger zs[i], zs[j]} :: i != j && 0 <= i < |xs| && |xs| <= j < |zs| ==> + zs[i] != zs[j]; + } + } + + /* A sequence with no duplicates converts to a set of the same + cardinality. */ + lemma LemmaCardinalityOfSetNoDuplicates(xs: seq) + requires HasNoDuplicates(xs) + ensures |ToSet(xs)| == |xs| + { + reveal HasNoDuplicates(); + reveal ToSet(); + if |xs| == 0 { + } else { + LemmaCardinalityOfSetNoDuplicates(DropLast(xs)); + assert ToSet(xs) == ToSet(DropLast(xs)) + {Last(xs)}; + } + } + + /* A sequence with cardinality equal to its set has no duplicates. */ + lemma LemmaNoDuplicatesCardinalityOfSet(xs: seq) + requires |ToSet(xs)| == |xs| + ensures HasNoDuplicates(xs) + { + reveal HasNoDuplicates(); + reveal ToSet(); + if |xs| == 0 { + } else { + assert xs == [First(xs)] + DropFirst(xs); + assert ToSet(xs) == {First(xs)} + ToSet(DropFirst(xs)); + if First(xs) in DropFirst(xs) { + // If there is a duplicate, then we show that |ToSet(s)| == |s| cannot hold. + assert ToSet(xs) == ToSet(DropFirst(xs)); + LemmaCardinalityOfSet(DropFirst(xs)); + } else { + assert |ToSet(xs)| == 1 + |ToSet(DropFirst(xs))|; + LemmaNoDuplicatesCardinalityOfSet(DropFirst(xs)); + } + } + } + + /* Given a sequence with no duplicates, each element occurs only + once in its conversion to a multiset. */ + lemma LemmaMultisetHasNoDuplicates(xs: seq) + requires HasNoDuplicates(xs) + ensures forall x {:trigger multiset(xs)[x]} | x in multiset(xs):: multiset(xs)[x] == 1 + { + if |xs| == 0 { + } else { + assert xs == DropLast(xs) + [Last(xs)]; + assert Last(xs) !in DropLast(xs) by { + reveal HasNoDuplicates(); + } + assert HasNoDuplicates(DropLast(xs)) by { + reveal HasNoDuplicates(); + } + LemmaMultisetHasNoDuplicates(DropLast(xs)); + } + } + + /* For an element that occurs at least once in a sequence, the index of its + first occurrence is returned. */ + function {:opaque} IndexOf(xs: seq, v: T): (i: nat) + requires v in xs + ensures i < |xs| && xs[i] == v + ensures forall j {:trigger xs[j]} :: 0 <= j < i ==> xs[j] != v + { + if xs[0] == v then 0 else 1 + IndexOf(xs[1..], v) + } + + /* Returns Some(i), if an element occurs at least once in a sequence, and i is + the index of its first occurrence. Otherwise the return is None. */ + function {:opaque} IndexOfOption(xs: seq, v: T): (o: Option) + ensures if o.Some? then o.value < |xs| && xs[o.value] == v && + forall j {:trigger xs[j]} :: 0 <= j < o.value ==> xs[j] != v + else v !in xs + { + if |xs| == 0 then None() + else + if xs[0] == v then Some(0) + else + var o' := IndexOfOption(xs[1..], v); + if o'.Some? then Some(o'.value + 1) else None() + } + + /* For an element that occurs at least once in a sequence, the index of its + last occurrence is returned. */ + function {:opaque} LastIndexOf(xs: seq, v: T): (i: nat) + requires v in xs + ensures i < |xs| && xs[i] == v + ensures forall j {:trigger xs[j]} :: i < j < |xs| ==> xs[j] != v + { + if xs[|xs|-1] == v then |xs| - 1 else LastIndexOf(xs[..|xs|-1], v) + } + + /* Returns Some(i), if an element occurs at least once in a sequence, and i is + the index of its last occurrence. Otherwise the return is None. */ + function {:opaque} LastIndexOfOption(xs: seq, v: T): (o: Option) + ensures if o.Some? then o.value < |xs| && xs[o.value] == v && + forall j {:trigger xs[j]} :: o.value < j < |xs| ==> xs[j] != v + else v !in xs + { + if |xs| == 0 then None() + else if xs[|xs|-1] == v then Some(|xs| - 1) else LastIndexOfOption(xs[..|xs|-1], v) + } + + /* Returns a sequence without the element at a given position. */ + function {:opaque} Remove(xs: seq, pos: nat): (ys: seq) + requires pos < |xs| + ensures |ys| == |xs| - 1 + ensures forall i {:trigger ys[i], xs[i]} | 0 <= i < pos :: ys[i] == xs[i] + ensures forall i {:trigger ys[i]} | pos <= i < |xs| - 1 :: ys[i] == xs[i+1] + { + xs[..pos] + xs[pos+1..] + } + + /* If a given element occurs at least once in a sequence, the sequence without + its first occurrence is returned. Otherwise the same sequence is returned. */ + function {:opaque} RemoveValue(xs: seq, v: T): (ys: seq) + ensures v !in xs ==> xs == ys + ensures v in xs ==> |multiset(ys)| == |multiset(xs)| - 1 + ensures v in xs ==> multiset(ys)[v] == multiset(xs)[v] - 1 + ensures HasNoDuplicates(xs) ==> HasNoDuplicates(ys) && ToSet(ys) == ToSet(xs) - {v} + { + reveal HasNoDuplicates(); + reveal ToSet(); + if v !in xs then xs + else + var i := IndexOf(xs, v); + assert xs == xs[..i] + [v] + xs[i+1..]; + xs[..i] + xs[i+1..] + } + + /* Inserts an element at a given position and returns the resulting (longer) sequence. */ + function {:opaque} Insert(xs: seq, a: T, pos: nat): seq + requires pos <= |xs| + ensures |Insert(xs, a, pos)| == |xs| + 1 + ensures forall i {:trigger Insert(xs, a, pos)[i], xs[i]} :: 0 <= i < pos ==> Insert(xs, a, pos)[i] == xs[i] + ensures forall i {:trigger xs[i]} :: pos <= i < |xs| ==> Insert(xs, a, pos)[i+1] == xs[i] + ensures Insert(xs, a, pos)[pos] == a + ensures multiset(Insert(xs, a, pos)) == multiset(xs) + multiset{a} + { + assert xs == xs[..pos] + xs[pos..]; + xs[..pos] + [a] + xs[pos..] + } + + /* Returns the sequence that is in reverse order to a given sequence. */ + function {:opaque} Reverse(xs: seq): (ys: seq) + ensures |ys| == |xs| + ensures forall i {:trigger ys[i]}{:trigger xs[|xs| - i - 1]} :: 0 <= i < |xs| ==> ys[i] == xs[|xs| - i - 1] + { + if xs == [] then [] else [xs[|xs|-1]] + Reverse(xs[0 .. |xs|-1]) + } + + /* Returns a constant sequence of a given length. */ + function {:opaque} Repeat(v: T, length: nat): (xs: seq) + ensures |xs| == length + ensures forall i: nat {:trigger xs[i]} | i < |xs| :: xs[i] == v + { + if length == 0 then + [] + else + [v] + Repeat(v, length - 1) + } + + /* Unzips a sequence that contains pairs into two separate sequences. */ + function {:opaque} Unzip(xs: seq<(A, B)>): (seq, seq) + ensures |Unzip(xs).0| == |Unzip(xs).1| == |xs| + ensures forall i {:trigger Unzip(xs).0[i]} {:trigger Unzip(xs).1[i]} + :: 0 <= i < |xs| ==> (Unzip(xs).0[i], Unzip(xs).1[i]) == xs[i] + { + if |xs| == 0 then ([], []) + else + var (a, b):= Unzip(DropLast(xs)); + (a + [Last(xs).0], b + [Last(xs).1]) + } + + /* Zips two sequences of equal length into one sequence that consists of pairs. */ + function {:opaque} Zip(xs: seq, ys: seq): seq<(A, B)> + requires |xs| == |ys| + ensures |Zip(xs, ys)| == |xs| + ensures forall i {:trigger Zip(xs, ys)[i]}:: 0 <= i < |Zip(xs, ys)| ==> Zip(xs, ys)[i] == (xs[i], ys[i]) + ensures Unzip(Zip(xs, ys)).0 == xs + ensures Unzip(Zip(xs, ys)).1 == ys + { + if |xs| == 0 then [] + else Zip(DropLast(xs), DropLast(ys)) + [(Last(xs), Last(ys))] + } + + /* Unzipping and zipping a sequence results in the original sequence */ + lemma LemmaZipOfUnzip(xs: seq<(A,B)>) + ensures Zip(Unzip(xs).0, Unzip(xs).1) == xs + { + } + + /********************************************************** + * + * Extrema in Sequences + * + ***********************************************************/ + + /* Returns the maximum integer value in a non-empty sequence of integers. */ + function {:opaque} Max(xs: seq): int + requires 0 < |xs| + ensures forall k {:trigger k in xs} :: k in xs ==> Max(xs) >= k + ensures Max(xs) in xs + { + assert xs == [xs[0]] + xs[1..]; + if |xs| == 1 then xs[0] else Math.Max(xs[0], Max(xs[1..])) + } + + /* The maximum of the concatenation of two non-empty sequences is greater than or + equal to the maxima of its two non-empty subsequences. */ + lemma LemmaMaxOfConcat(xs: seq, ys: seq) + requires 0 < |xs| && 0 < |ys| + ensures Max(xs+ys) >= Max(xs) + ensures Max(xs+ys) >= Max(ys) + ensures forall i {:trigger i in [Max(xs + ys)]} :: i in xs + ys ==> Max(xs + ys) >= i + { + reveal Max(); + if |xs| == 1 { + } else { + assert xs[1..] + ys == (xs + ys)[1..]; + LemmaMaxOfConcat(xs[1..], ys); + } + } + + /* Returns the minimum integer value in a non-empty sequence of integers. */ + function {:opaque} Min(xs: seq): int + requires 0 < |xs| + ensures forall k {:trigger k in xs} :: k in xs ==> Min(xs) <= k + ensures Min(xs) in xs + { + assert xs == [xs[0]] + xs[1..]; + if |xs| == 1 then xs[0] else Math.Min(xs[0], Min(xs[1..])) + } + + /* The minimum of the concatenation of two non-empty sequences is + less than or equal to the minima of its two non-empty subsequences. */ + lemma LemmaMinOfConcat(xs: seq, ys: seq) + requires 0 < |xs| && 0 < |ys| + ensures Min(xs+ys) <= Min(xs) + ensures Min(xs+ys) <= Min(ys) + ensures forall i {:trigger i in xs + ys} :: i in xs + ys ==> Min(xs + ys) <= i + { + reveal Min(); + if |xs| == 1 { + } else { + assert xs[1..] + ys == (xs + ys)[1..]; + LemmaMinOfConcat(xs[1..], ys); + } + } + + /* The maximum element in a non-empty sequence is greater than or equal to + the maxima of its non-empty subsequences. */ + lemma LemmaSubseqMax(xs: seq, from: nat, to: nat) + requires from < to <= |xs| + ensures Max(xs[from..to]) <= Max(xs) + { + var subseq := xs[from..to]; + var subseqMax := Max(subseq); + assert forall x | x in subseq :: x in xs[from..]; + assert subseqMax in subseq; + assert subseqMax in xs; + } + + /* The minimum element of a non-empty sequence is less than or equal + to the minima of its non-empty subsequences. */ + lemma LemmaSubseqMin(xs: seq, from: nat, to: nat) + requires from < to <= |xs| + ensures Min(xs[from..to]) >= Min(xs) + { + var subseq := xs[from..to]; + var subseqMin := Min(subseq); + assert forall x | x in subseq :: x in xs[from..]; + assert subseqMin in subseq; + assert subseqMin in xs; + } + + /********************************************************** + * + * Sequences of Sequences + * + ***********************************************************/ + + /* Flattens a sequence of sequences into a single sequence by concatenating + subsequences, starting from the first element. */ + function Flatten(xs: seq>): seq + decreases |xs| + { + if |xs| == 0 then [] + else xs[0] + Flatten(xs[1..]) + } + + /* Flattening sequences of sequences is distributive over concatenation. That is, concatenating + the flattening of two sequences of sequences is the same as flattening the + concatenation of two sequences of sequences. */ + lemma {:vcs_split_on_every_assert} LemmaFlattenConcat(xs: seq>, ys: seq>) + ensures Flatten(xs + ys) == Flatten(xs) + Flatten(ys) + { + if |xs| == 0 { + assert xs + ys == ys; + } else { + calc == { + Flatten(xs + ys); + { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } + xs[0] + Flatten(xs[1..] + ys); + xs[0] + Flatten(xs[1..]) + Flatten(ys); + Flatten(xs) + Flatten(ys); + } + } + } + + /* Flattens a sequence of sequences into a single sequence by concatenating + subsequences in reverse order, i.e. starting from the last element. */ + function FlattenReverse(xs: seq>): seq + decreases |xs| + { + if |xs| == 0 then [] + else FlattenReverse(DropLast(xs)) + Last(xs) + } + + /* Flattening sequences of sequences in reverse order is distributive over concatentation. + That is, concatenating the flattening of two sequences of sequences in reverse + order is the same as flattening the concatenation of two sequences of sequences + in reverse order. */ + lemma LemmaFlattenReverseConcat(xs: seq>, ys: seq>) + ensures FlattenReverse(xs + ys) == FlattenReverse(xs) + FlattenReverse(ys) + { + if |ys| == 0 { + assert FlattenReverse(ys) == []; + assert xs + ys == xs; + } else { + calc == { + FlattenReverse(xs + ys); + { assert Last(xs + ys) == Last(ys); assert DropLast(xs + ys) == xs + DropLast(ys); } + FlattenReverse(xs + DropLast(ys)) + Last(ys); + FlattenReverse(xs) + FlattenReverse(DropLast(ys)) + Last(ys); + FlattenReverse(xs) + FlattenReverse(ys); + } + } + } + + /* Flattening sequences of sequences in order (starting from the beginning) + and in reverse order (starting from the end) results in the same sequence. */ + lemma LemmaFlattenAndFlattenReverseAreEquivalent(xs: seq>) + ensures Flatten(xs) == FlattenReverse(xs) + { + if |xs| == 0 { + } else { + calc == { + FlattenReverse(xs); + FlattenReverse(DropLast(xs)) + Last(xs); + { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(xs)); } + Flatten(DropLast(xs)) + Last(xs); + Flatten(DropLast(xs)) + Flatten([Last(xs)]); + { LemmaFlattenConcat(DropLast(xs), [Last(xs)]); + assert xs == DropLast(xs) + [Last(xs)]; } + Flatten(xs); + } + } + } + + /* The length of a flattened sequence of sequences xs is greater than or + equal to any of the lengths of the elements of xs. */ + lemma LemmaFlattenLengthGeSingleElementLength(xs: seq>, i: int) + requires 0 <= i < |xs| + ensures |FlattenReverse(xs)| >= |xs[i]| + { + if i < |xs| - 1 { + LemmaFlattenLengthGeSingleElementLength(xs[..|xs|-1], i); + } + } + + /* The length of a flattened sequence of sequences xs is less than or equal + to the length of xs multiplied by a number not smaller than the length of the + longest sequence in xs. */ + lemma LemmaFlattenLengthLeMul(xs: seq>, j: int) + requires forall i {:trigger xs[i]} | 0 <= i < |xs| :: |xs[i]| <= j + ensures |FlattenReverse(xs)| <= |xs| * j + { + if |xs| == 0 { + } else { + LemmaFlattenLengthLeMul(xs[..|xs|-1], j); + assert |FlattenReverse(xs[..|xs|-1])| <= (|xs|-1) * j; + } + } + + + /********************************************************** + * + * Higher-Order Sequence Functions + * + ***********************************************************/ + + /* Returns the sequence one obtains by applying a function to every element + of a sequence. */ + function {:opaque} Map(f: (T ~> R), xs: seq): (result: seq) + requires forall i {:trigger xs[i]} :: 0 <= i < |xs| ==> f.requires(xs[i]) + ensures |result| == |xs| + ensures forall i {:trigger result[i]}:: 0 <= i < |xs| ==> result[i] == f(xs[i]) + reads set i, o {:trigger o in f.reads(xs[i])} | 0 <= i < |xs| && o in f.reads(xs[i]):: o + { + if |xs| == 0 then [] + else [f(xs[0])] + Map(f, xs[1..]) + } + + /* Applies a function to every element of a sequence, returning a Result value (which is a + failure-compatible type). Returns either a failure, or, if successful at every element, + the transformed sequence. */ + function {:opaque} MapWithResult(f: (T ~> Result), xs: seq): (result: Result, E>) + requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) + ensures result.Success? ==> + && |result.value| == |xs| + && (forall i :: 0 <= i < |xs| ==> + && f(xs[i]).Success? + && result.value[i] == f(xs[i]).value) + reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o + { + if |xs| == 0 then Success([]) + else + var head :- f(xs[0]); + var tail :- MapWithResult(f, xs[1..]); + Success([head] + tail) + } + + /* Applying a function to a sequence is distributive over concatenation. That is, concatenating + two sequences and then applying Map is the same as applying Map to each sequence separately, + and then concatenating the two resulting sequences. */ + lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) + requires forall i {:trigger xs[i]}:: 0 <= i < |xs| ==> f.requires(xs[i]) + requires forall j {:trigger ys[j]}:: 0 <= j < |ys| ==> f.requires(ys[j]) + ensures Map(f, xs + ys) == Map(f, xs) + Map(f, ys) + { + reveal Map(); + if |xs| == 0 { + assert xs + ys == ys; + } else { + calc { + Map(f, xs + ys); + { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } + Map(f, [xs[0]]) + Map(f, xs[1..] + ys); + Map(f, [xs[0]]) + Map(f, xs[1..]) + Map(f, ys); + {assert [(xs + ys)[0]] + xs[1..] + ys == xs + ys;} + Map(f, xs) + Map(f, ys); + } + } + } + + /* Returns the subsequence consisting of those elements of a sequence that satisfy a given + predicate. */ + function {:opaque} Filter(f: (T ~> bool), xs: seq): (result: seq) + requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) + ensures |result| <= |xs| + ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i]) + reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o + { + if |xs| == 0 then [] + else (if f(xs[0]) then [xs[0]] else []) + Filter(f, xs[1..]) + } + + /* Filtering a sequence is distributive over concatenation. That is, concatenating two sequences + and then using "Filter" is the same as using "Filter" on each sequence separately, and then + concatenating the two resulting sequences. */ + lemma {:opaque} {:vcs_split_on_every_assert} + LemmaFilterDistributesOverConcat(f: (T ~> bool), xs: seq, ys: seq) + requires forall i {:trigger xs[i]}:: 0 <= i < |xs| ==> f.requires(xs[i]) + requires forall j {:trigger ys[j]}:: 0 <= j < |ys| ==> f.requires(ys[j]) + ensures Filter(f, xs + ys) == Filter(f, xs) + Filter(f, ys) + { + reveal Filter(); + if |xs| == 0 { + assert xs + ys == ys; + } else { + calc { + Filter(f, xs + ys); + { assert {:split_here} (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } + Filter(f, [xs[0]]) + Filter(f, xs[1..] + ys); + Filter(f, [xs[0]]) + (Filter(f, xs[1..]) + Filter(f, ys)); + { assert {:split_here} [(xs + ys)[0]] + (xs[1..] + ys) == xs + ys; } + Filter(f, xs) + Filter(f, ys); + } + } + } + + /* Folds a sequence xs from the left (the beginning), by repeatedly acting on the accumulator + init via the function f. */ + function {:opaque} FoldLeft(f: (A, T) -> A, init: A, xs: seq): A + { + if |xs| == 0 then init + else FoldLeft(f, f(init, xs[0]), xs[1..]) + } + + /* Folding to the left is distributive over concatenation. That is, concatenating two + sequences and then folding them to the left, is the same as folding to the left the + first sequence and using the result to fold to the left the second sequence. */ + lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, xs: seq, ys: seq) + ensures FoldLeft(f, init, xs + ys) == FoldLeft(f, FoldLeft(f, init, xs), ys) + { + reveal FoldLeft(); + if |xs| == 0 { + assert xs + ys == ys; + } else { + assert |xs| >= 1; + assert ([xs[0]] + xs[1..] + ys)[0] == xs[0]; + calc { + FoldLeft(f, FoldLeft(f, init, xs), ys); + FoldLeft(f, FoldLeft(f, f(init, xs[0]), xs[1..]), ys); + { LemmaFoldLeftDistributesOverConcat(f, f(init, xs[0]), xs[1..], ys); } + FoldLeft(f, f(init, xs[0]), xs[1..] + ys); + { assert (xs + ys)[0] == xs[0]; + assert (xs + ys)[1..] == xs[1..] + ys; } + FoldLeft(f, init, xs + ys); + } + } + } + + /* Is true, if inv is an invariant under stp, which is a relational + version of the function f passed to fold. */ + ghost predicate InvFoldLeft(inv: (B, seq) -> bool, + stp: (B, A, B) -> bool) + { + forall x: A, xs: seq, b: B, b': B :: + inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs) + } + + /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */ + lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, + stp: (B, A, B) -> bool, + f: (B, A) -> B, + b: B, + xs: seq) + requires InvFoldLeft(inv, stp) + requires forall b, a :: stp(b, a, f(b, a)) + requires inv(b, xs) + ensures inv(FoldLeft(f, b, xs), []) + { + reveal FoldLeft(); + if xs == [] { + } else { + assert [xs[0]] + xs[1..] == xs; + LemmaInvFoldLeft(inv, stp, f, f(b, xs[0]), xs[1..]); + } + } + + /* Folds a sequence xs from the right (the end), by acting on the accumulator init via the + function f. */ + function {:opaque} FoldRight(f: (T, A) -> A, xs: seq, init: A): A + { + if |xs| == 0 then init + else f(xs[0], FoldRight(f, xs[1..], init)) + } + + /* Folding to the right is (contravariantly) distributive over concatenation. That is, concatenating + two sequences and then folding them to the right, is the same as folding to the right + the second sequence and using the result to fold to the right the first sequence. */ + lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, xs: seq, ys: seq) + ensures FoldRight(f, xs + ys, init) == FoldRight(f, xs, FoldRight(f, ys, init)) + { + reveal FoldRight(); + if |xs| == 0 { + assert xs + ys == ys; + } else { + calc { + FoldRight(f, xs, FoldRight(f, ys, init)); + f(xs[0], FoldRight(f, xs[1..], FoldRight(f, ys, init))); + f(xs[0], FoldRight(f, xs[1..] + ys, init)); + { assert (xs + ys)[0] == xs[0]; + assert (xs +ys)[1..] == xs[1..] + ys; } + FoldRight(f, xs + ys, init); + } + } + } + + /* Is true, if inv is an invariant under stp, which is a relational version + of the function f passed to fold. */ + ghost predicate InvFoldRight(inv: (seq, B) -> bool, + stp: (A, B, B) -> bool) + { + forall x: A, xs: seq, b: B, b': B :: + inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b') + } + + /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */ + lemma LemmaInvFoldRight(inv: (seq, B) -> bool, + stp: (A, B, B) -> bool, + f: (A, B) -> B, + b: B, + xs: seq) + requires InvFoldRight(inv, stp) + requires forall a, b :: stp(a, b, f(a, b)) + requires inv([], b) + ensures inv(xs, FoldRight(f, xs, b)) + { + reveal FoldRight(); + if xs == [] { + } else { + assert [xs[0]] + xs[1..] == xs; + } + } + + + /********************************************************** + * + * Sets to Ordered Sequences + * + ***********************************************************/ + + /* Converts a set to a sequence (ghost). */ + ghost function SetToSeqSpec(s: set): (xs: seq) + ensures multiset(s) == multiset(xs) + { + if s == {} then [] else var x :| x in s; [x] + SetToSeqSpec(s - {x}) + } + + /* Converts a set to a sequence (compiled). */ + method SetToSeq(s: set) returns (xs: seq) + ensures multiset(s) == multiset(xs) + { + xs := []; + var left: set := s; + while left != {} + invariant multiset(left) + multiset(xs) == multiset(s) + { + var x :| x in left; + left := left - {x}; + xs := xs + [x]; + } + } + + /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */ + lemma SortedUnique(xs: seq, ys: seq, R: (T, T) -> bool) + requires SortedBy(xs, R) + requires SortedBy(ys, R) + requires TotalOrdering(R) + requires multiset(xs) == multiset(ys) + ensures xs == ys + { + if xs == [] { + assert multiset(xs) == multiset{}; + assert multiset(ys) == multiset{}; + assert ys == []; + } else { + assert xs == [xs[0]] + xs[1..]; + assert ys == [ys[0]] + ys[1..]; + assert multiset(xs[1..]) == multiset(xs) - multiset{xs[0]}; + assert multiset(ys[1..]) == multiset(ys) - multiset{ys[0]}; + assert multiset(xs[1..]) == multiset(ys[1..]); + SortedUnique(xs[1..], ys[1..], R); + } + } + + /* Converts a set to a sequence that is ordered w.r.t. a given total order (ghost). */ + ghost function SetToSortedSeqSpec(s: set, R: (T, T) -> bool): (xs: seq) + requires TotalOrdering(R) + ensures multiset(s) == multiset(xs) + ensures SortedBy(xs, R) + { + MergeSortBy(SetToSeqSpec(s), R) + } + + /* Converts a set to a sequence that is ordered w.r.t. a given total order (compiled). */ + method SetToSortedSeq(s: set, R: (T, T) -> bool) returns (xs: seq) + requires TotalOrdering(R) + ensures multiset(s) == multiset(xs) + ensures SortedBy(xs, R) + { + xs := SetToSeq(s); + xs := MergeSortBy(xs, R); + SortedUnique(xs, SetToSortedSeqSpec(s, R), R); + } + + + /**************************** + ** Sorting sequences + ***************************** */ + + //Splits a sequence in two, sorts the two subsequences (recursively), and merges the two sorted sequences using `MergeSortedWith` + function MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) + requires TotalOrdering(lessThanOrEq) + ensures multiset(a) == multiset(result) + ensures SortedBy(result, lessThanOrEq) + { + if |a| <= 1 then + a + else + var splitIndex := |a| / 2; + var left, right := a[..splitIndex], a[splitIndex..]; + + assert a == left + right; + + var leftSorted := MergeSortBy(left, lessThanOrEq); + var rightSorted := MergeSortBy(right, lessThanOrEq); + + MergeSortedWith(leftSorted, rightSorted, lessThanOrEq) + } + + ghost predicate SortedBy(a: seq, lessThan: (T, T) -> bool) { + forall i, j | 0 <= i < j < |a| :: lessThan(a[i], a[j]) + } + + /* An element in an ordered set is called minimal, if it is less than every element of the set. */ + ghost predicate IsMinimum(R: (T, T) -> bool, m: T, s: set) { + m in s && forall y: T | y in s :: R(m, y) + } + + /* Any totally ordered set contains a unique minimal element. */ + lemma LemmaUniqueMinimum(R: (T, T) -> bool, s: set) returns (m: T) + requires |s| > 0 && TotalOrdering(R) + ensures IsMinimum(R, m, s) && (forall n: T | IsMinimum(R, n, s) :: m == n) + { + var x :| x in s; + if s == {x} { + m := x; + } else { + var m' := LemmaUniqueMinimum(R, s - {x}); + if + case R(m', x) => m := m'; + case R(x, m') => m := x; + } + } + + lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, lessThan: (T, T) -> bool) + requires SortedBy(s, lessThan) + requires |s| == 0 || lessThan(x, s[0]) + requires TotalOrdering(lessThan) + ensures SortedBy([x] + s, lessThan) + {} + + + // Helper function for MergeSortBy + function {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) + requires SortedBy(left, lessThanOrEq) + requires SortedBy(right, lessThanOrEq) + requires TotalOrdering(lessThanOrEq) + ensures multiset(left + right) == multiset(result) + ensures SortedBy(result, lessThanOrEq) + { + if |left| == 0 then + right + else if |right| == 0 then + left + else if lessThanOrEq(left[0], right[0]) then + LemmaNewFirstElementStillSortedBy(left[0], MergeSortedWith(left[1..], right, lessThanOrEq), lessThanOrEq); + assert left == [left[0]] + left[1..]; + + [left[0]] + MergeSortedWith(left[1..], right, lessThanOrEq) + + else + LemmaNewFirstElementStillSortedBy(right[0], MergeSortedWith(left, right[1..], lessThanOrEq), lessThanOrEq); + assert right == [right[0]] + right[1..]; + + [right[0]] + MergeSortedWith(left, right[1..], lessThanOrEq) + } +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Sets.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Sets.dfy new file mode 100644 index 00000000000..d4ad1a54de7 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Sets.dfy @@ -0,0 +1,320 @@ +/******************************************************************************* + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + This module defines useful properties and functions relating to the built-in `set` type. + */ +module DafnyStdLibs.Collections.Sets { + + import opened Functions + import opened Relations + + /* If all elements in set x are in set y, x is a subset of y. */ + lemma LemmaSubset(x: set, y: set) + requires forall e {:trigger e in y} :: e in x ==> e in y + ensures x <= y + { + } + + /* If x is a subset of y, then the size of x is less than or equal to the + size of y. */ + lemma LemmaSubsetSize(x: set, y: set) + ensures x < y ==> |x| < |y| + ensures x <= y ==> |x| <= |y| + { + if x != {} { + var e :| e in x; + LemmaSubsetSize(x - {e}, y - {e}); + } + } + + /* If x is a subset of y and the size of x is equal to the size of y, x is + equal to y. */ + lemma LemmaSubsetEquality(x: set, y: set) + requires x <= y + requires |x| == |y| + ensures x == y + decreases x, y + { + if x == {} { + } else { + var e :| e in x; + LemmaSubsetEquality(x - {e}, y - {e}); + } + } + + /* A singleton set has a size of 1. */ + lemma LemmaSingletonSize(x: set, e: T) + requires x == {e} + ensures |x| == 1 + { + } + + /* Elements in a singleton set are equal to each other. */ + lemma LemmaSingletonEquality(x: set, a: T, b: T) + requires |x| == 1 + requires a in x + requires b in x + ensures a == b + { + if a != b { + assert {a} < x; + LemmaSubsetSize({a}, x); + assert false; + } + } + + /* A singleton set has at least one element and any two elements are equal. */ + ghost predicate IsSingleton(s: set) { + && (exists x :: x in s) + && (forall x, y | x in s && y in s :: x == y) + } + + /* A set has exactly one element, if and only if, it has at least one element and any two elements are equal. */ + lemma LemmaIsSingleton(s: set) + ensures |s| == 1 <==> IsSingleton(s) + { + if |s| == 1 { + forall x, y | x in s && y in s ensures x == y { + LemmaSingletonEquality(s, x, y); + } + } + if IsSingleton(s) { + var x :| x in s; + assert s == {x}; + assert |s| == 1; + } + } + + /* Non-deterministically extracts an element from a set that contains at least one element. */ + ghost function ExtractFromNonEmptySet(s: set): (x: T) + requires |s| != 0 + ensures x in s + { + var x :| x in s; + x + } + + /* Deterministically extracts the unique element from a singleton set. In contrast to + `ExtractFromNonEmptySet`, this implementation compiles, as the uniqueness of the element + being picked can be proven. */ + function ExtractFromSingleton(s: set): (x: T) + requires |s| == 1 + ensures s == {x} + { + LemmaIsSingleton(s); + var x :| x in s; + x + } + + /* If an injective function is applied to each element of a set to construct + another set, the two sets have the same size. */ + lemma LemmaMapSize(xs: set, ys: set, f: X-->Y) + requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires Injective(f) + requires forall x {:trigger f(x)} :: x in xs <==> f(x) in ys + requires forall y {:trigger y in ys} :: y in ys ==> exists x :: x in xs && y == f(x) + ensures |xs| == |ys| + { + if xs != {} { + var x :| x in xs; + var xs' := xs - {x}; + var ys' := ys - {f(x)}; + LemmaMapSize(xs', ys', f); + } + } + + /* Map an injective function to each element of a set. */ + function {:opaque} Map(xs: set, f: X-->Y): (ys: set) + reads f.reads + requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires Injective(f) + ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys + ensures |xs| == |ys| + { + var ys := set x | x in xs :: f(x); + LemmaMapSize(xs, ys, f); + ys + } + + /* If a set ys is constructed using elements of another set xs for which a + function returns true, the size of ys is less than or equal to the size of + xs. */ + lemma LemmaFilterSize(xs: set, ys: set, f: X~>bool) + requires forall x {:trigger f.requires(x)}{:trigger x in xs} :: x in xs ==> f.requires(x) + requires forall y {:trigger f(y)}{:trigger y in xs} :: y in ys ==> y in xs && f(y) + ensures |ys| <= |xs| + decreases xs, ys + { + if ys != {} { + var y :| y in ys; + var xs' := xs - {y}; + var ys' := ys - {y}; + LemmaFilterSize(xs', ys', f); + } + } + + /* Construct a set using elements of another set for which a function returns + true. */ + function {:opaque} Filter(xs: set, f: X~>bool): (ys: set) + reads set x, o | x in xs && o in f.reads(x) :: o + requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x) + ensures forall y {:trigger f(y)}{:trigger y in xs} :: y in ys <==> y in xs && f(y) + ensures |ys| <= |xs| + { + var ys := set x | x in xs && f(x); + LemmaFilterSize(xs, ys, f); + ys + } + + /* The size of a union of two sets is greater than or equal to the size of + either individual set. */ + lemma LemmaUnionSize(xs: set, ys: set) + ensures |xs + ys| >= |xs| + ensures |xs + ys| >= |ys| + { + if ys == {} { + } else { + var y :| y in ys; + if y in xs { + var xr := xs - {y}; + var yr := ys - {y}; + assert xr + yr == xs + ys - {y}; + LemmaUnionSize(xr, yr); + } else { + var yr := ys - {y}; + assert xs + yr == xs + ys - {y}; + LemmaUnionSize(xs, yr); + } + } + } + + /* Construct a set with all integers in the range [a, b). */ + function {:opaque} SetRange(a: int, b: int): (s: set) + requires a <= b + ensures forall i {:trigger i in s} :: a <= i < b <==> i in s + ensures |s| == b - a + decreases b - a + { + if a == b then {} else {a} + SetRange(a + 1, b) + } + + /* Construct a set with all integers in the range [0, n). */ + function {:opaque} SetRangeZeroBound(n: int): (s: set) + requires n >= 0 + ensures forall i {:trigger i in s} :: 0 <= i < n <==> i in s + ensures |s| == n + { + SetRange(0, n) + } + + /* If a set solely contains integers in the range [a, b), then its size is + bounded by b - a. */ + lemma LemmaBoundedSetSize(x: set, a: int, b: int) + requires forall i {:trigger i in x} :: i in x ==> a <= i < b + requires a <= b + ensures |x| <= b - a + { + var range := SetRange(a, b); + forall e {:trigger e in range}{:trigger e in x} | e in x + ensures e in range + { + } + assert x <= range; + LemmaSubsetSize(x, range); + } + + /** In a set, a greatest element is necessarily maximal. */ + lemma LemmaGreatestImpliesMaximal(R: (T, T) -> bool, max: T, s: set) + requires IsGreatest(R, max, s) + ensures IsMaximal(R, max, s) + { + } + + /** In a set, a least element is necessarily minimal. */ + lemma LemmaLeastImpliesMinimal(R: (T, T) -> bool, min: T, s: set) + requires IsLeast(R, min, s) + ensures IsMinimal(R, min, s) + { + } + + /** In a totally-ordered set, an element is maximal if and only if it is a greatest element. */ + lemma LemmaMaximalEquivalentGreatest(R: (T, T) -> bool, max: T, s: set) + requires TotalOrdering(R) + ensures IsGreatest(R, max, s) <==> IsMaximal(R, max, s) + { + } + + /** In a totally-ordered set, an element is minimal if and only if it is a least element. */ + lemma LemmaMinimalEquivalentLeast(R: (T, T) -> bool, min: T, s: set) + requires TotalOrdering(R) + ensures IsLeast(R, min, s) <==> IsMinimal(R, min, s) + { + } + + /** In a partially-ordered set, there exists at most one least element. */ + lemma LemmaLeastIsUnique(R: (T, T) -> bool, s: set) + requires PartialOrdering(R) + ensures forall min, min' | IsLeast(R, min, s) && IsLeast(R, min', s) :: min == min' + {} + + /** In a partially-ordered set, there exists at most one greatest element. */ + lemma LemmaGreatestIsUnique(R: (T, T) -> bool, s: set) + requires PartialOrdering(R) + ensures forall max, max' | IsGreatest(R, max, s) && IsGreatest(R, max', s) :: max == max' + {} + + /** In a totally-ordered set, there exists at most one minimal element. */ + lemma LemmaMinimalIsUnique(R: (T, T) -> bool, s: set) + requires TotalOrdering(R) + ensures forall min, min' | IsMinimal(R, min, s) && IsMinimal(R, min', s) :: min == min' + {} + + /** In a totally-ordered set, there exists at most one maximal element. */ + lemma LemmaMaximalIsUnique(R: (T, T) -> bool, s: set) + requires TotalOrdering(R) + ensures forall max, max' | IsMaximal(R, max, s) && IsMaximal(R, max', s) :: max == max' + {} + + /** Any totally-ordered set contains a unique minimal (equivalently, least) element. */ + lemma LemmaFindUniqueMinimal(R: (T, T) -> bool, s: set) returns (min: T) + requires |s| > 0 && TotalOrdering(R) + ensures IsMinimal(R, min, s) && (forall min': T | IsMinimal(R, min', s) :: min == min') + { + var x :| x in s; + if s == {x} { + min := x; + } else { + var min' := LemmaFindUniqueMinimal(R, s - {x}); + if + case R(min', x) => min := min'; + case R(x, min') => min := x; + } + } + + /** Any totally ordered set contains a unique maximal (equivalently, greatest) element. */ + lemma LemmaFindUniqueMaximal(R: (T, T) -> bool, s: set) returns (max: T) + requires |s| > 0 && TotalOrdering(R) + ensures IsMaximal(R, max, s) && (forall max': T | IsMaximal(R, max', s) :: max == max') + { + var x :| x in s; + if s == {x} { + max := x; + } else { + var max' := LemmaFindUniqueMaximal(R, s - {x}); + if + case R(max', x) => max := x; + case R(x, max') => max := max'; + } + } +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.dfy new file mode 100644 index 00000000000..f9f4d7e98e9 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.dfy @@ -0,0 +1,44 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** Defines various integer-math functions */ +module DafnyStdLibs.Math { + + /** Minimum of two integers */ + function Min(a: int, b: int): int + { + if a < b + then a + else b + } + + /** Minimum of three integers */ + function Min3(a: int, b: int, c: int): int + { + Min(a, Min(b, c)) + } + + /** Maximum of two integers */ + function Max(a: int, b: int): int + { + if a < b + then b + else a + } + + /** Maximum of three integers */ + function Max3(a: int, b: int, c: int): int + { + Max(a, Max(b, c)) + } + + /** Integer absolute value */ + function Abs(a: int): int + { + if a < 0 + then -a + else a + } +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.md b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.md new file mode 100644 index 00000000000..460142a3f2c --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Math.md @@ -0,0 +1,7 @@ +## The `Math` module + +The `Math` module defines integer-related math functions (e.g. Min, Max, Abs). + +- Integer-related functions over collections of integers (e.g. minimum of a sequence) are +available in the `Collections` module. diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Wrappers.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Wrappers.dfy index d37f1f5a6a4..30da42efb59 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/Wrappers.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/Wrappers.dfy @@ -1,6 +1,6 @@ /******************************************************************************* * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT + * SPDX-License-Identifier: MIT *******************************************************************************/ /** This module provides various kinds of failure-compatible datatypes, including Option. @@ -202,4 +202,4 @@ module DafnyStdLibs.Wrappers { { if condition then Pass' else Fail'(error) } -} \ No newline at end of file +} From 73c278a3d8dc651b90572ddea6bf74745a8299ba Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 13 Nov 2023 15:44:00 -0800 Subject: [PATCH 9/9] Still recursively register modules with no file attached --- Source/DafnyCore/CoverageReport/CoverageReport.cs | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index ac88e4ce270..84ba454e708 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -72,14 +72,15 @@ public void RegisterFile(Uri uri) { private void RegisterFiles(Node astNode) { if (astNode.StartToken.ActualFilename != null) { - var uri = astNode.StartToken.Uri; - labelsByFile.GetOrCreate(uri, () => new List()); - - if (astNode is LiteralModuleDecl moduleDecl) { - modulesByFile.GetOrCreate(uri, () => new HashSet()).Add(moduleDecl.ModuleDef); - - RegisterFiles(moduleDecl.ModuleDef); + labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => new List()); + } + + if (astNode is LiteralModuleDecl moduleDecl) { + if (astNode.StartToken.ActualFilename != null) { + modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => new HashSet()).Add(moduleDecl.ModuleDef); } + + RegisterFiles(moduleDecl.ModuleDef); } foreach (var declaration in astNode.Children.OfType()) {