From 9d219102eccbf72a7cb64f59fb87f4213f64f307 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 13 Feb 2023 12:33:43 -0800 Subject: [PATCH 01/11] Maps: add MapKeys --- src/Collections/Maps/Maps.dfy | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index f666d8c4..0d9cc5e8 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -1,18 +1,22 @@ // RUN: %dafny /compile:0 "%s" /******************************************************************************* -* Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, +* Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, * ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* +* SPDX-License-Identifier: BSD-2-Clause +* * Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT +* SPDX-License-Identifier: MIT *******************************************************************************/ include "../../Wrappers.dfy" +include "../../Functions.dfy" +include "../Sets/Sets.dfy" module {:options "-functionSyntax:4"} Maps { import opened Wrappers + import Functions + import Sets function Get(m: map, x: X): Option { @@ -127,4 +131,16 @@ module {:options "-functionSyntax:4"} Maps { forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] } + /* Map an injective function over the keys of a map, retaining the values. */ + function {:opaque} MapKeys(m: map, f: X --> X'): (m': map) + reads f.reads + requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires Functions.Injective(f) + ensures |m'| == |m| + ensures m'.Values == m.Values + { + var m' := map k <- m :: f(k) := m[k]; + Sets.LemmaMapSize(m.Keys, m'.Keys, f); + m' + } } From 9f1df7144c00e99efb637092e8f1949a067ce3b0 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 13 Feb 2023 13:44:33 -0800 Subject: [PATCH 02/11] fix formatting --- src/Collections/Maps/Maps.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index 0d9cc5e8..caa087c7 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -138,7 +138,7 @@ module {:options "-functionSyntax:4"} Maps { requires Functions.Injective(f) ensures |m'| == |m| ensures m'.Values == m.Values - { + { var m' := map k <- m :: f(k) := m[k]; Sets.LemmaMapSize(m.Keys, m'.Keys, f); m' From 433ad7d448eb9acafd2881b13bd12435de0ab3bb Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 15 Feb 2023 10:37:04 -0800 Subject: [PATCH 03/11] Update src/Collections/Maps/Maps.dfy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- src/Collections/Maps/Maps.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index caa087c7..80004c9e 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -131,7 +131,7 @@ module {:options "-functionSyntax:4"} Maps { forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] } - /* Map an injective function over the keys of a map, retaining the values. */ + /* Maps an injective function over the keys of a map, retaining the values. */ function {:opaque} MapKeys(m: map, f: X --> X'): (m': map) reads f.reads requires forall x {:trigger f.requires(x)} :: f.requires(x) From 2c30705863f65451e18b188008c3719eea2dee18 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 20 Feb 2023 14:32:42 -0800 Subject: [PATCH 04/11] add postcondition m'[f(x)] == m[x] --- src/Collections/Maps/Maps.dfy | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index 80004c9e..56074775 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -138,6 +138,7 @@ module {:options "-functionSyntax:4"} Maps { requires Functions.Injective(f) ensures |m'| == |m| ensures m'.Values == m.Values + ensures forall x | x in m :: f(x) in m' && (m'[f(x)] == m[x]) { var m' := map k <- m :: f(k) := m[k]; Sets.LemmaMapSize(m.Keys, m'.Keys, f); From 5fbb83e2bdd6cbadbf0e80b5ec06dcf5af25b7d6 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 12:43:50 -0700 Subject: [PATCH 05/11] add some other useful Map functions/lemmas --- src/Collections/Maps/Maps.dfy | 55 +++++++++++++++++++++++++++++++++-- 1 file changed, 52 insertions(+), 3 deletions(-) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index 0f1c8a78..d832ab0b 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -1,12 +1,12 @@ // RUN: %verify "%s" /******************************************************************************* - * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, * ETH Zurich, and University of Washington - * SPDX-License-Identifier: BSD-2-Clause + * SPDX-License-Identifier: BSD-2-Clause * * Modifications and Extensions: Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT + * SPDX-License-Identifier: MIT ******************************************************************************/ include "../../Wrappers.dfy" @@ -97,6 +97,39 @@ module {:options "-functionSyntax:4"} Maps { forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] } + ghost predicate {:opaque} Contains(big: map, small: map) + { + && small.Keys <= big.Keys + && forall x <- small :: small[x] == big[x] + } + + lemma LemmaContainsPreservesInjectivity(big: map, small: map) + requires Contains(big, small) + requires Injective(big) + ensures Injective(small) + { + reveal Contains(); + reveal Injective(); + } + + lemma LemmaInjectiveImpliesUniqueValues(m: map) + requires Injective(m) + ensures |m.Keys| == |m.Values| + { + if |m| > 0 { + var x: X :| x in m; + var y := m[x]; + var m' := Remove(m, x); + reveal Contains(); + assert Contains(m, m'); + + reveal Injective(); + assert m'.Values == m.Values - {y}; + LemmaContainsPreservesInjectivity(m, m'); + LemmaInjectiveImpliesUniqueValues(m'); + } + } + /* 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 @@ -144,4 +177,20 @@ module {:options "-functionSyntax:4"} Maps { Sets.LemmaMapSize(m.Keys, m'.Keys, f); m' } + + /* Maps a function over the values of a map, retaining the keys. */ + function {:opaque} MapValues(m: map, f: Y --> Y'): (m': map) + reads f.reads + requires forall y {:trigger f.requires(y)} :: f.requires(y) + ensures |m'| == |m| + ensures m'.Keys == m.Keys + ensures forall x | x in m :: m'[x] == f(m[x]) + { + var m' := map x <- m :: x := f(m[x]); + assert |m'| == |m| by { + assert m'.Keys == m.Keys; + assert |m'.Keys| == |m.Keys|; + } + m' + } } From 88caf978b809400f94130aff9e24cb3bc4bdbb1d Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 12:50:23 -0700 Subject: [PATCH 06/11] add simple examples --- examples/Collections/Maps/MapsExamples.dfy | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 examples/Collections/Maps/MapsExamples.dfy diff --git a/examples/Collections/Maps/MapsExamples.dfy b/examples/Collections/Maps/MapsExamples.dfy new file mode 100644 index 00000000..bf9f60bc --- /dev/null +++ b/examples/Collections/Maps/MapsExamples.dfy @@ -0,0 +1,17 @@ +include "../../../src/Functions.dfy" +include "../../../src/Collections/Maps/Maps.dfy" + +module {:options "--function-syntax:4"} MapsExamples { + import Functions + import Maps + + function ByteKeyMapToIntKeys(m: map): (m': map) + { + Maps.MapKeys(m, b => b as int) + } + + function ByteValueMapToIntValues(m: map): (m': map) + { + Maps.MapValues(m, b => b as int) + } +} From c3df03648cfecea2a160f5ea15ef0cbe2043da71 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 13:01:27 -0700 Subject: [PATCH 07/11] add RUN line to MapsExamples --- examples/Collections/Maps/MapsExamples.dfy | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/examples/Collections/Maps/MapsExamples.dfy b/examples/Collections/Maps/MapsExamples.dfy index bf9f60bc..60b336ad 100644 --- a/examples/Collections/Maps/MapsExamples.dfy +++ b/examples/Collections/Maps/MapsExamples.dfy @@ -1,3 +1,10 @@ +// RUN: %verify "%s" + +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + include "../../../src/Functions.dfy" include "../../../src/Collections/Maps/Maps.dfy" From 808dc384a74a16a9ea6e042175afd4b1c95382d2 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 13:01:48 -0700 Subject: [PATCH 08/11] MapsExamples.dfy -> Maps.dfy --- examples/Collections/Maps/{MapsExamples.dfy => Maps.dfy} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename examples/Collections/Maps/{MapsExamples.dfy => Maps.dfy} (100%) diff --git a/examples/Collections/Maps/MapsExamples.dfy b/examples/Collections/Maps/Maps.dfy similarity index 100% rename from examples/Collections/Maps/MapsExamples.dfy rename to examples/Collections/Maps/Maps.dfy From bd6f8029f0172ccba91ba4cc948194963d32b9f9 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 14:12:24 -0700 Subject: [PATCH 09/11] use IsSubset instead of Contains --- src/Collections/Maps/Maps.dfy | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index d832ab0b..c221f60c 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -68,7 +68,7 @@ module {:options "-functionSyntax:4"} Maps { 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) + && forall x <- m :: m[x] == m'[x] } /* Union of two maps. Does not require disjoint domains; on the intersection, @@ -97,18 +97,11 @@ module {:options "-functionSyntax:4"} Maps { forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] } - ghost predicate {:opaque} Contains(big: map, small: map) - { - && small.Keys <= big.Keys - && forall x <- small :: small[x] == big[x] - } - - lemma LemmaContainsPreservesInjectivity(big: map, small: map) - requires Contains(big, small) + lemma LemmaSubsetIsInjective(small: map, big: map) + requires IsSubset(small, big) requires Injective(big) ensures Injective(small) { - reveal Contains(); reveal Injective(); } @@ -117,15 +110,15 @@ module {:options "-functionSyntax:4"} Maps { ensures |m.Keys| == |m.Values| { if |m| > 0 { + reveal Injective(); + var x: X :| x in m; var y := m[x]; var m' := Remove(m, x); - reveal Contains(); - assert Contains(m, m'); + assert IsSubset(m', m); - reveal Injective(); assert m'.Values == m.Values - {y}; - LemmaContainsPreservesInjectivity(m, m'); + LemmaSubsetIsInjective(m', m); LemmaInjectiveImpliesUniqueValues(m'); } } From 24f3936b7339b95644d2df88db6af23cbe8357cb Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 14:16:24 -0700 Subject: [PATCH 10/11] put f params first in Map* functions --- src/Collections/Maps/Maps.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index c221f60c..430b8ace 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -158,7 +158,7 @@ module {:options "-functionSyntax:4"} Maps { } /* Maps an injective function over the keys of a map, retaining the values. */ - function {:opaque} MapKeys(m: map, f: X --> X'): (m': map) + function {:opaque} MapKeys(f: X --> X', m: map): (m': map) reads f.reads requires forall x {:trigger f.requires(x)} :: f.requires(x) requires Functions.Injective(f) @@ -172,7 +172,7 @@ module {:options "-functionSyntax:4"} Maps { } /* Maps a function over the values of a map, retaining the keys. */ - function {:opaque} MapValues(m: map, f: Y --> Y'): (m': map) + function {:opaque} MapValues(f: Y --> Y', m: map): (m': map) reads f.reads requires forall y {:trigger f.requires(y)} :: f.requires(y) ensures |m'| == |m| From 30c9116eb81c9f9eefac2b7075a2608691f3f4d0 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 19 Apr 2023 14:20:50 -0700 Subject: [PATCH 11/11] fix examples --- examples/Collections/Maps/Maps.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/Collections/Maps/Maps.dfy b/examples/Collections/Maps/Maps.dfy index 60b336ad..5cac2446 100644 --- a/examples/Collections/Maps/Maps.dfy +++ b/examples/Collections/Maps/Maps.dfy @@ -14,11 +14,11 @@ module {:options "--function-syntax:4"} MapsExamples { function ByteKeyMapToIntKeys(m: map): (m': map) { - Maps.MapKeys(m, b => b as int) + Maps.MapKeys(b => b as int, m) } function ByteValueMapToIntValues(m: map): (m': map) { - Maps.MapValues(m, b => b as int) + Maps.MapValues(b => b as int, m) } }