Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

some trigger updates #25

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

some trigger updates #25

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7fe04f3
removed some tiggers that repeats dafny, added some comments for dafn…
yizhou7 Oct 10, 2021
85e585f
address some comments from @parno
yizhou7 Oct 14, 2021
16c9e3d
refomat some code, add some explainations on triggers
yizhou7 Oct 14, 2021
b7ae16c
Update STYLE.md
yizhou7 Oct 14, 2021
6937071
remove trigger from pre-condition
yizhou7 Nov 6, 2021
064984b
update Reverse post condition trigger
yizhou7 Nov 6, 2021
381bc75
rename Union operations
yizhou7 Nov 6, 2021
9198630
remove manual trigger for Injective/Monotonic/MonotonicFrom
yizhou7 Nov 8, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion src/Collections/Maps/Imaps.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,9 @@ module Imaps {

/* Remove all key-value pairs corresponding to the iset of keys provided. */
function {:opaque} RemoveKeys<X, Y>(m: imap<X, Y>, xs: iset<X>): (m': imap<X, Y>)
/* Dafny selected triggers: {m[x]}, {m'[x]}, {x in m'}, {x in xs}, {x in m} */
ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x]
/* Dafny selected triggers: {x in xs}, {x in m}, {x in m'} */
ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs
ensures m'.Keys == m.Keys - xs
{
Expand All @@ -32,6 +34,7 @@ module Imaps {
/* Remove a key-value pair. Returns unmodified imap if key is not found. */
function {:opaque} RemoveKey<X, Y>(m: imap<X, Y>, x: X): (m': imap<X, Y>)
ensures m' == RemoveKeys(m, iset{x})
/* Dafny selected triggers: {m[x']}, {m'[x']}, {x' in m'} */
ensures forall x' {:trigger m'[x']} :: x' in m' ==> m'[x'] == m[x']
{
imap i | i in m && i != x :: m[i]
Expand All @@ -54,14 +57,16 @@ module Imaps {
predicate IsSubset<X, Y>(m: imap<X, Y>, m': imap<X, Y>)
{
&& m.Keys <= m'.Keys
&& forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x)
&& forall x :: 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. */
function {:opaque} Union<X, Y>(m: imap<X, Y>, m': imap<X, Y>): (r: imap<X, Y>)
ensures r.Keys == m.Keys + m'.Keys
/* Dafny selected triggers: {m'[x]}, {r[x]}, {x in m'} */
ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x]
/* Dafny selected triggers: {m[x]}, {r[x]}, {x in m'}, {x in m} */
ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x]
{
m + m'
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
Expand All @@ -70,6 +75,7 @@ module Imaps {
/* True iff an imap is injective. */
predicate {:opaque} Injective<X, Y>(m: imap<X, Y>)
{
/* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */
forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x']
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
}

Expand All @@ -91,19 +97,22 @@ module Imaps {
/* True iff an imap contains all valid keys. */
predicate {:opaque} Total<X(!new), Y>(m: imap<X, Y>)
{
/* Dafny selected triggers: {i in m} */
forall i {:trigger m[i]}{:trigger i in m} :: i in m
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
}

/* True iff an imap is monotonic. */
predicate {:opaque} Monotonic(m: imap<int, int>)
{
/* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */
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. */
predicate {:opaque} MonotonicFrom(m: imap<int, int>, start: int)
{
/* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */
forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x']
}

Expand Down
12 changes: 11 additions & 1 deletion src/Collections/Maps/Maps.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,19 @@ module Maps {
}

function method {:opaque} ToImap<X, Y>(m: map<X, Y>): (m': imap<X, Y>)
/* Dafny selected triggers: {m[x]}, {m'[x]}, {x in m'}, {x in m} */
ensures forall x {:trigger m'[x]} :: x in m ==> x in m' && m'[x] == m[x]
/* Dafny selected triggers: {x in m}, {x in m'} */
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 method {:opaque} RemoveKeys<X, Y>(m: map<X, Y>, xs: set<X>): (m': map<X, Y>)
/* Dafny selected triggers: {m[x]}, {m'[x]}, {x in m'}, {x in xs}, {x in m} */
ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x]
/* Dafny selected triggers: {x in xs}, {x in m}, {x in m'} */
ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs
Comment on lines +36 to 37
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The trigger in the other direction (that is, x in m) seems equally useful to me. Is there a reason not to include it?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the ensures is an implication, we might only want the x in m'? My limited understanding is that we are ensuring the properties of m', rather than the original m. So might not be necessary to invoke this fact every time we see the original map.

ensures m'.Keys == m.Keys - xs
{
Expand Down Expand Up @@ -65,14 +69,16 @@ module Maps {
predicate IsSubset<X, Y>(m: map<X, Y>, m': map<X, Y>)
{
&& m.Keys <= m'.Keys
&& forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x)
&& forall x :: 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 method {:opaque} Union<X, Y>(m: map<X, Y>, m': map<X, Y>): (r: map<X, Y>)
ensures r.Keys == m.Keys + m'.Keys
/* Dafny selected triggers: {m'[x]}, {r[x]}, {x in m'} */
ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x]
/* Dafny selected triggers: {m[x]}, {r[x]}, {x in m'}, {x in m} */
ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x]
{
m + m'
Expand All @@ -91,6 +97,7 @@ module Maps {
/* True iff a map is injective. */
predicate {:opaque} Injective<X, Y>(m: map<X, Y>)
{
/* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */
forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x']
}

Expand All @@ -112,19 +119,22 @@ module Maps {
/* True iff a map contains all valid keys. */
predicate {:opaque} Total<X(!new), Y>(m: map<X, Y>)
{
/* Dafny selected triggers: {i in m} */
forall i {:trigger m[i]}{:trigger i in m} :: i in m
}

/* True iff a map is monotonic. */
predicate {:opaque} Monotonic(m: map<int, int>)
{
/* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */
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. */
predicate {:opaque} MonotonicFrom(m: map<int, int>, start: int)
{
/* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */
forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x']
}

Expand Down
54 changes: 30 additions & 24 deletions src/Collections/Sequences/Seq.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ module Seq {
var r2 := r1[s2..e2];
var r3 := s[s1+s2..s1+e2];
assert |r2| == |r3|;
forall i {:trigger r2[i], r3[i]}| 0 <= i < |r2| ensures r2[i] == r3[i];
forall i | 0 <= i < |r2| ensures r2[i] == r3[i];
{
}
}
Expand Down Expand Up @@ -166,7 +166,7 @@ module Seq {
/* is true if there are no duplicate values in the sequence */
predicate {:opaque} HasNoDuplicates<T>(s: seq<T>)
{
(forall i, j {:trigger s[i], s[j]}:: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j])
(forall i, j :: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j])
}

/* if sequence a and b don't have duplicates and there are no elements in
Expand All @@ -181,7 +181,7 @@ module Seq {
reveal HasNoDuplicates();
var c := a + b;
if |c| > 1 {
assert forall i, j {:trigger c[i], c[j]}:: i != j && 0 <= i < |a| && |a| <= j < |c| ==>
assert forall i, j :: i != j && 0 <= i < |a| && |a| <= j < |c| ==>
c[i] in multiset(a) && c[j] in multiset(b) && c[i] != c[j];
}
}
Expand All @@ -203,7 +203,7 @@ module Seq {
/* proves that there are no duplicate values in the multiset version of the sequence */
lemma LemmaMultisetHasNoDuplicates<T>(s: seq<T>)
requires HasNoDuplicates(s)
ensures forall x {:trigger multiset(s)[x]} | x in multiset(s):: multiset(s)[x] == 1
ensures forall x | x in multiset(s):: multiset(s)[x] == 1
{
if |s| == 0 {
} else {
Expand All @@ -222,7 +222,7 @@ module Seq {
function method {:opaque} IndexOf<T(==)>(s: seq<T>, v: T): (i: nat)
requires v in s
ensures i < |s| && s[i] == v
ensures forall j {:trigger s[j]} :: 0 <= j < i ==> s[j] != v
ensures forall j :: 0 <= j < i ==> s[j] != v
{
if s[0] == v then 0 else 1 + IndexOf(s[1..], v)
}
Expand All @@ -231,7 +231,7 @@ module Seq {
found */
function method {:opaque} IndexOfOption<T(==)>(s: seq<T>, v: T): (o: Option<nat>)
ensures if o.Some? then o.value < |s| && s[o.value] == v &&
forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v
forall j :: 0 <= j < o.value ==> s[j] != v
else v !in s
{
if |s| == 0 then None()
Expand All @@ -246,7 +246,7 @@ module Seq {
function method {:opaque} LastIndexOf<T(==)>(s: seq<T>, v: T): (i: nat)
requires v in s
ensures i < |s| && s[i] == v
ensures forall j {:trigger s[j]} :: i < j < |s| ==> s[j] != v
ensures forall j :: i < j < |s| ==> s[j] != v
{
if s[|s|-1] == v then |s| - 1 else LastIndexOf(s[..|s|-1], v)
}
Expand All @@ -255,7 +255,7 @@ module Seq {
found */
function method {:opaque} LastIndexOfOption<T(==)>(s: seq<T>, v: T): (o: Option<nat>)
ensures if o.Some? then o.value < |s| && s[o.value] == v &&
forall j {:trigger s[j]} :: o.value < j < |s| ==> s[j] != v
forall j :: o.value < j < |s| ==> s[j] != v
else v !in s
{
if |s| == 0 then None()
Expand All @@ -266,8 +266,8 @@ module Seq {
function method {:opaque} Remove<T>(s: seq<T>, pos: nat): (s': seq<T>)
requires pos < |s|
ensures |s'| == |s| - 1
ensures forall i {:trigger s'[i], s[i]} | 0 <= i < pos :: s'[i] == s[i]
ensures forall i {:trigger s'[i]} | pos <= i < |s| - 1 :: s'[i] == s[i+1]
ensures forall i | 0 <= i < pos :: s'[i] == s[i]
ensures forall i| pos <= i < |s| - 1 :: s'[i] == s[i+1]
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
{
s[..pos] + s[pos+1..]
}
Expand All @@ -292,8 +292,8 @@ module Seq {
function method {:opaque} Insert<T>(s: seq<T>, a: T, pos: nat): seq<T>
requires pos <= |s|
ensures |Insert(s, a, pos)| == |s| + 1
ensures forall i {:trigger Insert(s, a, pos)[i], s[i]} :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i]
ensures forall i {:trigger s[i]} :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i]
ensures forall i :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i]
ensures forall i :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i]
ensures Insert(s, a, pos)[pos] == a
ensures multiset(Insert(s, a, pos)) == multiset(s) + multiset{a}
{
Expand All @@ -303,14 +303,15 @@ module Seq {

function method {:opaque} Reverse<T>(s: seq<T>): (s': seq<T>)
ensures |s'| == |s|
/* Dafny selected triggers: {s'[i]} */
ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1]
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
{
if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1])
}

function method {:opaque} Repeat<T>(v: T, length: nat): (s: seq<T>)
ensures |s| == length
ensures forall i: nat {:trigger s[i]} | i < |s| :: s[i] == v
ensures forall i: nat | i < |s| :: s[i] == v
{
if length == 0 then
[]
Expand All @@ -321,6 +322,7 @@ module Seq {
/* unzips a sequence that contains ordered pairs into 2 seperate sequences */
function method {:opaque} Unzip<A,B>(s: seq<(A, B)>): (seq<A>, seq<B>)
ensures |Unzip(s).0| == |Unzip(s).1| == |s|
/* Dafny selected triggers: {s[i]}, {Unzip(s).1[i]}, {Unzip(s).0[i]} */
ensures forall i {:trigger Unzip(s).0[i]} {:trigger Unzip(s).1[i]}
:: 0 <= i < |s| ==> (Unzip(s).0[i], Unzip(s).1[i]) == s[i]
{
Expand All @@ -335,6 +337,7 @@ module Seq {
function method {:opaque} Zip<A,B>(a: seq<A>, b: seq<B>): seq<(A, B)>
requires |a| == |b|
ensures |Zip(a, b)| == |a|
/* Dafny selected triggers: {b[i]}, {a[i]}, {Zip(a, b)[i]} */
ensures forall i {:trigger Zip(a, b)[i]}:: 0 <= i < |Zip(a, b)| ==> Zip(a, b)[i] == (a[i], b[i])
ensures Unzip(Zip(a, b)).0 == a
ensures Unzip(Zip(a, b)).1 == b
Expand All @@ -358,7 +361,7 @@ module Seq {
/* finds the maximum integer value in the sequence */
function method {:opaque} Max(s: seq<int>): int
requires 0 < |s|
ensures forall k {:trigger k in s} :: k in s ==> Max(s) >= k
ensures forall k :: k in s ==> Max(s) >= k
ensures Max(s) in s
{
assert s == [s[0]] + s[1..];
Expand All @@ -371,6 +374,7 @@ module Seq {
requires 0 < |a| && 0 < |b|
ensures Max(a+b) >= Max(a)
ensures Max(a+b) >= Max(b)
/* Dafny selected trigger: {i in a + b} */
ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
{
reveal Max();
Expand All @@ -384,7 +388,7 @@ module Seq {
/* finds the minimum integer value in the sequence */
function method {:opaque} Min(s: seq<int>): int
requires 0 < |s|
ensures forall k {:trigger k in s} :: k in s ==> Min(s) <= k
ensures forall k :: k in s ==> Min(s) <= k
ensures Min(s) in s
{
assert s == [s[0]] + s[1..];
Expand All @@ -397,7 +401,8 @@ module Seq {
requires 0 < |a| && 0 < |b|
ensures Min(a+b) <= Min(a)
ensures Min(a+b) <= Min(b)
ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i
/* Dafny selected trigger: {i in a + b} */
ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
{
reveal Min();
if |a| == 1 {
Expand Down Expand Up @@ -531,7 +536,7 @@ module Seq {
than the length of the original sequence of sequences multiplied by the length of
the longest sequence */
lemma LemmaFlattenLengthLeMul<T>(s: seq<seq<T>>, j: int)
requires forall i {:trigger s[i]} | 0 <= i < |s| :: |s[i]| <= j
requires forall i | 0 <= i < |s| :: |s[i]| <= j
ensures |FlattenReverse(s)| <= |s| * j
{
if |s| == 0 {
Expand All @@ -549,10 +554,11 @@ module Seq {

/* applies a transformation function on the sequence */
function method {:opaque} Map<T,R>(f: (T ~> R), s: seq<T>): (result: seq<R>)
requires forall i {:trigger s[i]} :: 0 <= i < |s| ==> f.requires(s[i])
requires forall i :: 0 <= i < |s| ==> f.requires(s[i])
ensures |result| == |s|
/* Dafny selected triggers: {s[i]}, {result[i]} */
ensures forall i {:trigger result[i]}:: 0 <= i < |s| ==> result[i] == f(s[i]);
reads set i, o {:trigger o in f.reads(s[i])} | 0 <= i < |s| && o in f.reads(s[i]):: o
reads set i, o | 0 <= i < |s| && o in f.reads(s[i]):: o
{
if |s| == 0 then []
else [f(s[0])] + Map(f, s[1..])
Expand All @@ -562,8 +568,8 @@ module Seq {
Map on each sequence seperately and then concatenating the two resulting
sequences */
lemma {:opaque} LemmaMapDistributesOverConcat<T,R>(f: (T ~> R), a: seq<T>, b: seq<T>)
requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i])
requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j])
requires forall i :: 0 <= i < |a| ==> f.requires(a[i])
requires forall j :: 0 <= j < |b| ==> f.requires(b[j])
ensures Map(f, a + b) == Map(f, a) + Map(f, b)
{
reveal Map();
Expand All @@ -585,7 +591,7 @@ module Seq {
function method {:opaque} Filter<T>(f: (T ~> bool), s: seq<T>): (result: seq<T>)
requires forall i :: 0 <= i < |s| ==> f.requires(s[i])
ensures |result| <= |s|
ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i])
ensures forall i: nat :: i < |result| && f.requires(result[i]) ==> f(result[i])
reads f.reads
{
if |s| == 0 then []
Expand All @@ -595,8 +601,8 @@ module Seq {
/* concatenating two sequences and then using "filter" is the same as using "filter" on each sequences
seperately and then concatenating their resulting sequences */
lemma {:opaque} LemmaFilterDistributesOverConcat<T>(f: (T ~> bool), a: seq<T>, b: seq<T>)
requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i])
requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j])
requires forall i :: 0 <= i < |a| ==> f.requires(a[i])
requires forall j :: 0 <= j < |b| ==> f.requires(b[j])
ensures Filter(f, a + b) == Filter(f, a) + Filter(f, b)
{
reveal Filter();
Expand Down
9 changes: 6 additions & 3 deletions src/Collections/Sets/Isets.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ module Isets {

/* If all elements in iset x are in iset y, x is a subset of y. */
lemma LemmaSubset<T>(x: iset<T>, y: iset<T>)
/* Dafny selected triggers: {e in y}, {e in x} */
requires forall e {:trigger e in y} :: e in x ==> e in y
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
ensures x <= y
{
Expand All @@ -30,9 +31,10 @@ module Isets {
/* Map an injective function to each element of an iset. */
function {:opaque} Map<X(!new), Y>(xs: iset<X>, f: X-->Y): (ys: iset<Y>)
reads f.reads
requires forall x {:trigger f.requires(x)} :: f.requires(x)
requires forall x :: f.requires(x)
requires Injective(f)
ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys
/* Dafny selected triggers: {f(x)}, {x in xs} */
ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys
{
var ys := iset x | x in xs :: f(x);
ys
Expand All @@ -42,7 +44,8 @@ module Isets {
returns true. */
function {:opaque} Filter<X(!new)>(xs: iset<X>, f: X~>bool): (ys: iset<X>)
reads f.reads
requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x)
requires forall x :: x in xs ==> f.requires(x)
/* Dafny selected triggers: {f(y)}, {y in xs}, {y in ys} */
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);
Expand Down
Loading