From 2e62624135f9c663f6bf5b2a7e5d7337c0396440 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Thu, 11 Aug 2022 18:11:21 -0400 Subject: [PATCH 01/32] adding Heap Sort and Bianry Search --- examples/BinarySearch.dfy | 24 +++++++++++++++++ examples/sorting.dfy | 57 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+) create mode 100644 examples/BinarySearch.dfy create mode 100644 examples/sorting.dfy diff --git a/examples/BinarySearch.dfy b/examples/BinarySearch.dfy new file mode 100644 index 00000000..7a130fa5 --- /dev/null +++ b/examples/BinarySearch.dfy @@ -0,0 +1,24 @@ + + + +method BinarySearch(a: array, key: T,compare: (T, T) -> bool) returns (r: int) + requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i],a[j]) + ensures 0 <= r ==> r < a.Length && a[r] == key + ensures r < 0 ==> key !in a[..] +{ + var lo, hi := 0, a.Length; + while lo < hi + invariant 0 <= lo <= hi <= a.Length + invariant key !in a[..lo] && key !in a[hi..] + { + var mid := (lo + hi) / 2; + if compare(key,a[mid]) { + hi := mid; + } else if compare(a[mid],key) { + lo := mid + 1; + } else { + return mid; + } + } + return -1; +} \ No newline at end of file diff --git a/examples/sorting.dfy b/examples/sorting.dfy new file mode 100644 index 00000000..1d2545b0 --- /dev/null +++ b/examples/sorting.dfy @@ -0,0 +1,57 @@ +// Implemetation of Heap sort +include "../src/Collections/Sequences/Seq.dfy" + +method SortArray(a: array, compare: (T, T) -> bool) + requires multiset(a[..]) == multiset(old(a[..])) + modifies a + ensures forall i, j :: 0 <= i < j < a.Length ==> compare(a[i], a[j]) + { + var n := a.Length; + for i := n/2 -1 downto 0 + invariant 0 <= i <= a.Length + { + heapify(a,n,i,compare); + } + + for i:= n-1 downto 1 + invariant 0 <= i <= a.Length + { + var temp:= a[0]; + a[0]:= a[i]; + a[i]:= temp; + heapify(a,i,0,compare); + } + } + +method heapify(a: array, n:int, i:int, compare: (T, T) -> bool ) +ensures multiset(a[..]) == multiset(old(a[..])) +modifies a +{ + var largest := i; + var left := 2* i+ 1; + var right := 2* 1+ 2; + + if ((left > n) && compare(a[left], a[largest])) + { + largest := left; + } + + if (right < n && compare(a[right], a[largest])) + { + largest := right; + } + + + if (largest != i) + { + largest := i; + heapify(a,n,largest,compare); + } +} + +method Sort(s: seq, compare: (T, T) -> bool) returns (result :array) + { + var a := Seq.ToArray(s); + SortArray(a, compare); + return a; + } \ No newline at end of file From 00e866745cd02a4619619a31df52daf557eb9d14 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Tue, 16 Aug 2022 16:13:11 -0400 Subject: [PATCH 02/32] changes as suggestions --- examples/BinarySearch.dfy | 24 ---- examples/sorting.dfy | 57 --------- src/Collections/Sequences/Sorting.dfy | 171 ++++++++++++++++++++++++++ 3 files changed, 171 insertions(+), 81 deletions(-) delete mode 100644 examples/BinarySearch.dfy delete mode 100644 examples/sorting.dfy create mode 100644 src/Collections/Sequences/Sorting.dfy diff --git a/examples/BinarySearch.dfy b/examples/BinarySearch.dfy deleted file mode 100644 index 7a130fa5..00000000 --- a/examples/BinarySearch.dfy +++ /dev/null @@ -1,24 +0,0 @@ - - - -method BinarySearch(a: array, key: T,compare: (T, T) -> bool) returns (r: int) - requires forall i,j :: 0 <= i < j < a.Length ==> compare(a[i],a[j]) - ensures 0 <= r ==> r < a.Length && a[r] == key - ensures r < 0 ==> key !in a[..] -{ - var lo, hi := 0, a.Length; - while lo < hi - invariant 0 <= lo <= hi <= a.Length - invariant key !in a[..lo] && key !in a[hi..] - { - var mid := (lo + hi) / 2; - if compare(key,a[mid]) { - hi := mid; - } else if compare(a[mid],key) { - lo := mid + 1; - } else { - return mid; - } - } - return -1; -} \ No newline at end of file diff --git a/examples/sorting.dfy b/examples/sorting.dfy deleted file mode 100644 index 1d2545b0..00000000 --- a/examples/sorting.dfy +++ /dev/null @@ -1,57 +0,0 @@ -// Implemetation of Heap sort -include "../src/Collections/Sequences/Seq.dfy" - -method SortArray(a: array, compare: (T, T) -> bool) - requires multiset(a[..]) == multiset(old(a[..])) - modifies a - ensures forall i, j :: 0 <= i < j < a.Length ==> compare(a[i], a[j]) - { - var n := a.Length; - for i := n/2 -1 downto 0 - invariant 0 <= i <= a.Length - { - heapify(a,n,i,compare); - } - - for i:= n-1 downto 1 - invariant 0 <= i <= a.Length - { - var temp:= a[0]; - a[0]:= a[i]; - a[i]:= temp; - heapify(a,i,0,compare); - } - } - -method heapify(a: array, n:int, i:int, compare: (T, T) -> bool ) -ensures multiset(a[..]) == multiset(old(a[..])) -modifies a -{ - var largest := i; - var left := 2* i+ 1; - var right := 2* 1+ 2; - - if ((left > n) && compare(a[left], a[largest])) - { - largest := left; - } - - if (right < n && compare(a[right], a[largest])) - { - largest := right; - } - - - if (largest != i) - { - largest := i; - heapify(a,n,largest,compare); - } -} - -method Sort(s: seq, compare: (T, T) -> bool) returns (result :array) - { - var a := Seq.ToArray(s); - SortArray(a, compare); - return a; - } \ No newline at end of file diff --git a/src/Collections/Sequences/Sorting.dfy b/src/Collections/Sequences/Sorting.dfy new file mode 100644 index 00000000..a14b134f --- /dev/null +++ b/src/Collections/Sequences/Sorting.dfy @@ -0,0 +1,171 @@ +include "../../StandardLibrary.dfy" +include "../../UInt.dfy" +include "../Sequences/Seq.dfy" + +module sorting{ + export + reveals Reflexive, AntiSymmetric, Connected, TotalOrdering + reveals LexicographicByteSeqBelow, LexicographicByteSeqBelowAux + provides AboutLexicographicByteSeqBelow + provides MergeSortBy + provides StandardLibrary, UInt + + import StandardLibrary + import opened UInt = StandardLibrary.UInt + import Seq + +predicate Reflexive(R: (T, T) -> bool) { + forall x :: R(x, x) + } + +predicate AntiSymmetric(R: (T, T) -> bool) { + forall x, y :: R(x, y) && R(y, x) ==> x == y + } + +predicate Connected(R: (T, T) -> bool) { + forall x, y :: R(x, y) || R(y, x) + } + +predicate TotalOrdering(R: (T, T) -> bool) { + && Reflexive(R) + && AntiSymmetric(R) + && StandardLibrary.Transitive(R) + && Connected(R) + } + + /* + * Useful orderings + */ + + // reflexivelexicographical comparison of byte sequences + predicate method LexicographicByteSeqBelow(x: seq, y: seq) { + LexicographicByteSeqBelowAux(x, y, 0) + } + + predicate method LexicographicByteSeqBelowAux(x: seq, y: seq, n: nat) + requires n <= |x| && n <= |y| + decreases |x| - n + { + || n == |x| + || (n != |y| && x[n] < y[n]) + || (n != |y| && x[n] == y[n] && LexicographicByteSeqBelowAux(x, y, n + 1)) + } + + lemma AboutLexicographicByteSeqBelow() + ensures TotalOrdering(LexicographicByteSeqBelow) + { + assert Reflexive(LexicographicByteSeqBelow) by { + forall x, n | 0 <= n <= |x| { + AboutLexicographicByteSeqBelowAux_Reflexive(x, n); + } + } + assert AntiSymmetric(LexicographicByteSeqBelow) by { + forall x, y, n: nat | + n <= |x| && n <= |y| && x[..n] == y[..n] && + LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) + { + AboutLexicographicByteSeqBelowAux_AntiSymmetric(x, y, n); + } + } + assert StandardLibrary.Transitive(LexicographicByteSeqBelow) by { + forall x, y, z, n: nat | + n <= |x| && n <= |y| && n <= |z| && + LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) + { + AboutLexicographicByteSeqBelowAux_Transitive(x, y, z, n); + } + } + assert Connected(LexicographicByteSeqBelow) by { + forall x, y, n: nat | n <= |x| && n <= |y| { + AboutLexicographicByteSeqBelowAux_Connected(x, y, n); + } + } + } + + lemma AboutLexicographicByteSeqBelowAux_Reflexive(x: seq, n: nat) + requires n <= |x| + ensures LexicographicByteSeqBelowAux(x, x, n) + decreases |x| - n + { + } + + lemma AboutLexicographicByteSeqBelowAux_AntiSymmetric(x: seq, y: seq, n: nat) + requires n <= |x| && n <= |y| + requires x[..n] == y[..n] + requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) + ensures x == y + decreases |x| - n + { + } + + lemma AboutLexicographicByteSeqBelowAux_Transitive(x: seq, y: seq, z: seq, n: nat) + requires n <= |x| && n <= |y| && n <= |z| + requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) + ensures LexicographicByteSeqBelowAux(x, z, n) + decreases |x| - n + { + } + + lemma AboutLexicographicByteSeqBelowAux_Connected(x: seq, y: seq, n: nat) + requires n <= |x| && n <= |y| + ensures LexicographicByteSeqBelowAux(x, y, n) || LexicographicByteSeqBelowAux(y, x, n) + decreases |x| - n + { + } + + predicate method SortedBy(a: seq,compare: (T, T) -> bool ) { + forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]) + } + + lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> bool) + requires SortedBy(s, compare) + requires |s| == 0 || compare(x,s[0]) + {} + +function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :seq) + ensures multiset(a) == multiset(result) + { + 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, compare); + var rightSorted := MergeSortBy(right, compare); + + MergeSortedBy(leftSorted, rightSorted, compare) + } + + function method {:tailrecursion} MergeSortedBy(left: seq, right: seq, compare: (T, T) -> bool) : (result :seq) + requires SortedBy(left,compare) + requires SortedBy(right,compare) + ensures multiset(left + right) == multiset(result) + { + if |left| == 0 then + right + else if |right| == 0 then + left + else if compare(right[0],left[0]) then + LemmaNewFirstElementStillSortedBy(right[0], MergeSortedBy(left, right[1..], compare), compare); + assert right == [right[0]] + right[1..]; + + [right[0]] + MergeSortedBy(left, right[1..], compare) + + else + LemmaNewFirstElementStillSortedBy(left[0], MergeSortedBy(left[1..], right, compare), compare); + assert left == [left[0]] + left[1..]; + + [left[0]] + MergeSortedBy(left[1..], right, compare) + } + +method Sort(s: seq, compare: (T, T) -> bool) returns (result :seq) + ensures multiset(s) == multiset(result) + requires StandardLibrary.Transitive(compare) + requires Connected(compare) + { + MergeSortBy(s,compare) + } +} From fd12d32b972072b88d67d542b0ce758c962dbaa4 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Tue, 16 Aug 2022 16:14:11 -0400 Subject: [PATCH 03/32] adding dependencies --- src/StandardLibrary.dfy | 408 ++++++++++++++++++++++++++++++++++++++++ src/UInt.dfy | 329 ++++++++++++++++++++++++++++++++ 2 files changed, 737 insertions(+) create mode 100644 src/StandardLibrary.dfy create mode 100644 src/UInt.dfy diff --git a/src/StandardLibrary.dfy b/src/StandardLibrary.dfy new file mode 100644 index 00000000..22113692 --- /dev/null +++ b/src/StandardLibrary.dfy @@ -0,0 +1,408 @@ +include "../../libraries/src/Wrappers.dfy" +include "UInt.dfy" + +module StandardLibrary { + import opened Wrappers + import opened U = UInt + + lemma SeqTakeAppend(s: seq, i: int) + requires 0 <= i < |s| + ensures s[..i] + [s[i]] == s[..i + 1] + {} + + function method {:tailrecursion} Join(ss: seq>, joiner: seq): (s: seq) + requires 0 < |ss| + { + if |ss| == 1 then ss[0] else ss[0] + joiner + Join(ss[1..], joiner) + } + + function method {:tailrecursion} Split(s: seq, delim: T): (res: seq>) + ensures delim !in s ==> res == [s] + ensures s == [] ==> res == [[]] + ensures 0 < |res| + ensures forall i :: 0 <= i < |res| ==> delim !in res[i] + ensures Join(res, [delim]) == s + decreases |s| + { + var i := FindIndexMatching(s, delim, 0); + if i.Some? then [s[..i.value]] + Split(s[(i.value + 1)..], delim) else [s] + } + + lemma WillSplitOnDelim(s: seq, delim: T, prefix: seq) + requires |prefix| < |s| + requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i] + requires delim !in prefix && s[|prefix|] == delim + ensures Split(s, delim) == [prefix] + Split(s[|prefix| + 1..], delim) + { + calc { + Split(s, delim); + == + var i := FindIndexMatching(s, delim, 0); + if i.Some? then [s[..i.value]] + Split(s[i.value + 1..], delim) else [s]; + == { FindIndexMatchingLocatesElem(s, delim, 0, |prefix|); assert FindIndexMatching(s, delim, 0).Some?; } + [s[..|prefix|]] + Split(s[|prefix| + 1..], delim); + == { assert s[..|prefix|] == prefix; } + [prefix] + Split(s[|prefix| + 1..], delim); + } + } + + lemma WillNotSplitWithOutDelim(s: seq, delim: T) + requires delim !in s + ensures Split(s, delim) == [s] + { + calc { + Split(s, delim); + == + var i := FindIndexMatching(s, delim, 0); + if i.Some? then [s[..i.value]] + Split(s[i.value+1..], delim) else [s]; + == { FindIndexMatchingLocatesElem(s, delim, 0, |s|); } + [s]; + } + } + + lemma FindIndexMatchingLocatesElem(s: seq, c: T, start: nat, elemIndex: nat) + requires start <= elemIndex <= |s| + requires forall i :: start <= i < elemIndex ==> s[i] != c + requires elemIndex == |s| || s[elemIndex] == c + ensures FindIndexMatching(s, c, start) == if elemIndex == |s| then None else Some(elemIndex) + decreases elemIndex - start + {} + + function method FindIndexMatching(s: seq, c: T, i: nat): (index: Option) + requires i <= |s| + ensures index.Some? ==> i <= index.value < |s| && s[index.value] == c && c !in s[i..index.value] + ensures index.None? ==> c !in s[i..] + decreases |s| - i + { + FindIndex(s, x => x == c, i) + } + + function method {:tailrecursion} FindIndex(s: seq, f: T -> bool, i: nat): (index: Option) + requires i <= |s| + ensures index.Some? ==> i <= index.value < |s| && f(s[index.value]) && (forall j :: i <= j < index.value ==> !f(s[j])) + ensures index.None? ==> forall j :: i <= j < |s| ==> !f(s[j]) + decreases |s| - i + { + if i == |s| then None + else if f(s[i]) then Some(i) + else FindIndex(s, f, i + 1) + } + + function method {:tailrecursion} Filter(s: seq, f: T -> bool): (res: seq) + ensures forall i :: 0 <= i < |s| && f(s[i]) ==> s[i] in res + ensures forall i :: 0 <= i < |res| ==> res[i] in s && f(res[i]) + ensures |res| <= |s| + { + if |s| == 0 then [] + else if f(s[0]) then [s[0]] + Filter(s[1..], f) + else Filter(s[1..], f) + } + + lemma FilterIsDistributive(s: seq, s': seq, f: T -> bool) + ensures Filter(s + s', f) == Filter(s, f) + Filter(s', f) + { + if s == [] { + assert s + s' == s'; + } else { + var S := s + s'; + var s1 := s[1..]; + calc { + Filter(S, f); + == // def. Filter + if f(S[0]) then [S[0]] + Filter(S[1..], f) else Filter(S[1..], f); + == { assert S[0] == s[0] && S[1..] == s1 + s'; } + if f(s[0]) then [s[0]] + Filter(s1 + s', f) else Filter(s1 + s', f); + == { FilterIsDistributive(s1, s', f); } + if f(s[0]) then [s[0]] + (Filter(s1, f) + Filter(s', f)) else Filter(s1, f) + Filter(s', f); + == // associativity of + + if f(s[0]) then ([s[0]] + Filter(s1, f)) + Filter(s', f) else Filter(s1, f) + Filter(s', f); + == // distribute + over if-then-else + (if f(s[0]) then [s[0]] + Filter(s1, f) else Filter(s1, f)) + Filter(s', f); + == // def. Filter + Filter(s, f) + Filter(s', f); + } + } + } + + function method Min(a: int, b: int): int { + if a < b then a else b + } + + function method Fill(value: T, n: nat): seq + ensures |Fill(value, n)| == n + ensures forall i :: 0 <= i < n ==> Fill(value, n)[i] == value + { + seq(n, _ => value) + } + + method SeqToArray(s: seq) returns (a: array) + // "Fresh" expressions require editing memory + ensures fresh(a) + ensures a.Length == |s| + ensures forall i :: 0 <= i < |s| ==> a[i] == s[i] + { + a := new T[|s|](i requires 0 <= i < |s| => s[i]); + } + + lemma SeqPartsMakeWhole(s: seq, i: nat) + requires 0 <= i <= |s| + ensures s[..i] + s[i..] == s + {} + + /* + * Lexicographic comparison of sequences. + * + * Given two sequences `a` and `b` and a strict (that is, irreflexive) + * ordering `less` on the elements of these sequences, determine whether or not + * `a` is lexicographically "less than or equal to" `b`. + * + * `a` is lexicographically "less than or equal to" `b` holds iff + * there exists a `k` such that + * - the first `k` elements of `a` and `b` are the same + * - either: + * -- `a` has length `k` (that is, `a` is a prefix of `b`) + * -- `a[k]` is strictly less (using `less`) than `b[k]` + */ + + predicate method LexicographicLessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { + exists k :: 0 <= k <= |a| && LexicographicLessOrEqualAux(a, b, less, k) + } + + predicate method LexicographicLessOrEqualAux(a: seq, b: seq, less: (T, T) -> bool, lengthOfCommonPrefix: nat) + requires 0 <= lengthOfCommonPrefix <= |a| + { + lengthOfCommonPrefix <= |b| + && (forall i :: 0 <= i < lengthOfCommonPrefix ==> a[i] == b[i]) + && (lengthOfCommonPrefix == |a| || (lengthOfCommonPrefix < |b| && less(a[lengthOfCommonPrefix], b[lengthOfCommonPrefix]))) + } + + /* + * In order for the lexicographic ordering above to have the expected properties, the + * relation "less" must be trichotomous and transitive. + * + * For an ordering `less` to be _trichotomous_ means that for any two `x` and `y`, + * EXACTLY one of the following three conditions holds: + * - less(x, y) + * - x == y + * - less(y, x) + * Note that being trichotomous implies being irreflexive. + */ + + predicate Trichotomous(less: (T, T) -> bool) { + (forall x, y :: less(x, y) || x == y || less(y, x)) && // at least one of the three + (forall x, y :: less(x, y) && less(y, x) ==> false) && // not both of the less's + (forall x, y :: less(x, y) ==> x != y) // not a less and the equality + } + + predicate Transitive(R: (T, T) -> bool) { + forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) + } + + /* + * Here is an example relation and a lemma that says the relation is appropriate for use in + * lexicographic orderings. + */ + + lemma UInt8LessIsTrichotomousTransitive() + ensures Trichotomous(UInt8Less) + ensures Transitive(UInt8Less) + { + } + + /* + * As the following lemmas show, the lexicographic ordering is reflexive, antisymmetric, transitive, and total. + * The proofs are a bit pedantic and include steps that can be automated. + */ + + lemma LexIsReflexive(a: seq, less: (T, T) -> bool) + ensures LexicographicLessOrEqual(a, a, less) + { + assert LexicographicLessOrEqualAux(a, a, less, |a|); + } + + lemma LexIsAntisymmetric(a: seq, b: seq, less: (T, T) -> bool) + requires Trich: Trichotomous(less) + requires LexicographicLessOrEqual(a, b, less) + requires LexicographicLessOrEqual(b, a, less) + ensures a == b + { + assert LessIrreflexive: forall x,y :: less(x, y) ==> x != y by { + reveal Trich; + } + assert ASymmetric: forall x,y :: less(x, y) && less(y, x) ==> false by { + reveal Trich; + } + var k0 :| 0 <= k0 <= |a| && LexicographicLessOrEqualAux(a, b, less, k0); + var k1 :| 0 <= k1 <= |b| && LexicographicLessOrEqualAux(b, a, less, k1); + var max := if k0 < k1 then k1 else k0; + assert max <= |a| && max <= |b|; + assert SameUntilMax: forall i :: 0 <= i < max ==> a[i] == b[i]; + assert AA: k0 == |a| || (k0 < |b| && less(a[k0], b[k0])); + assert BB: k1 == |b| || (k1 < |a| && less(b[k1], a[k1])); + calc { + true; + ==> { reveal AA, BB; } + (k0 == |a| || (k0 < |b| && less(a[k0], b[k0]))) && (k1 == |b| || (k1 < |a| && less(b[k1], a[k1]))); + == // distribute && and || + (k0 == |a| && k1 == |b|) || + (k0 == |a| && k1 < |a| && less(b[k1], a[k1])) || + (k0 < |b| && less(a[k0], b[k0]) && k1 == |b|) || + (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); + == { reveal LessIrreflexive, SameUntilMax; } + (k0 == |a| && k1 == |b|) || + (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); + ==> { reveal LessIrreflexive, SameUntilMax; assert max <= k0 && max <= k1; } + (k0 == |a| && k1 == |b|) || + (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1]) && k0 == k1 == max); + == { reveal ASymmetric; } + k0 == |a| && k1 == |b|; + ==> { assert |a| == k0 <= max && |b| == k1 <= max ==> k0 == k1; } + max == |a| == |b|; + ==> { reveal SameUntilMax; } + a == b; + } + } + + lemma LexIsTransitive(a: seq, b: seq, c: seq, less: (T, T) -> bool) + requires Transitive(less) + requires LexicographicLessOrEqual(a, b, less) + requires LexicographicLessOrEqual(b, c, less) + ensures LexicographicLessOrEqual(a, c, less) + { + var k0 :| 0 <= k0 <= |a| && LexicographicLessOrEqualAux(a, b, less, k0); + var k1 :| 0 <= k1 <= |b| && LexicographicLessOrEqualAux(b, c, less, k1); + var k := if k0 < k1 then k0 else k1; + assert LexicographicLessOrEqualAux(a, c, less, k); + } + + lemma LexIsTotal(a: seq, b: seq, less: (T, T) -> bool) + requires Trich: Trichotomous(less) + ensures LexicographicLessOrEqual(a, b, less) || LexicographicLessOrEqual(b, a, less) + { + var m := 0; + while m < |a| && m < |b| && a[m] == b[m] + invariant m <= |a| && m <= |b| + invariant forall i :: 0 <= i < m ==> a[i] == b[i] + { + m := m + 1; + } + // m is the length of the common prefix of a and b + if m == |a| == |b| { + assert a == b; + LexIsReflexive(a, less); + } else if m == |a| < |b| { + assert LexicographicLessOrEqualAux(a, b, less, m); + } else if m == |b| < |a| { + assert LexicographicLessOrEqualAux(b, a, less, m); + } else { + assert m < |a| && m < |b|; + reveal Trich; + if + case less(a[m], b[m]) => + assert LexicographicLessOrEqualAux(a, b, less, m); + case less(b[m], a[m]) => + assert LexicographicLessOrEqualAux(b, a, less, m); + } + } + + /* + * SetToOrderedSequence(s, less) takes a set of T-strings and returns them as a sequence, + * ordered by the lexicographic ordering whose underlying irreflexive ordering is "less". + * The function is compilable, but will not exhibit enviable performance. + */ + + function method {:tailrecursion} SetToOrderedSequence(s: set>, less: (T, T) -> bool): (q: seq>) + requires Trichotomous(less) && Transitive(less) + ensures |s| == |q| + ensures forall i :: 0 <= i < |q| ==> q[i] in s + ensures forall k :: k in s ==> k in q + ensures forall i :: 0 < i < |q| ==> LexicographicLessOrEqual(q[i-1], q[i], less) + ensures forall i, j | 0 <= i < j < |q| :: q[i] != q[j]; + { + if s == {} then + [] + else + // In preparation for the assign-such-that statement below, we'll need to + // prove that a minimum exists and that it is unique. + // The following lemma shows existence: + ThereIsAMinimum(s, less); + // The following assertion shows uniqueness: + assert forall a, b :: IsMinimum(a, s, less) && IsMinimum(b, s, less) ==> a == b by { + // The proof of the assertion is the following forall statement. + // But why did we even bother to write the assert-by instead of + // just writing this forall statement in the first place? Because + // we are in an expression context and a forall statement cannot start + // an expression (because the "forall" makes the parser think that + // a forall expression is coming). + forall a, b | IsMinimum(a, s, less) && IsMinimum(b, s, less) { + // For the given a and b, the proof is settled by calling the following lemma: + MinimumIsUnique(a, b, s, less); + } + } + // The "a in s" in the following line follows from IsMinimum(a, s), so it + // is logically redundant. However, it is needed to convince the compiler + // that the assign-such-that statement is compilable. + var a :| a in s && IsMinimum(a, s, less); + [a] + SetToOrderedSequence(s - {a}, less) + } + + predicate method IsMinimum(a: seq, s: set>, less: (T, T) -> bool) { + a in s && + forall z :: z in s ==> LexicographicLessOrEqual(a, z, less) + } + + lemma ThereIsAMinimum(s: set>, less: (T, T) -> bool) + requires s != {} + requires Trichotomous(less) && Transitive(less) + ensures exists a :: IsMinimum(a, s, less) + { + var a := FindMinimum(s, less); + } + + lemma MinimumIsUnique(a: seq, b: seq, s: set>, less: (T, T) -> bool) + requires IsMinimum(a, s, less) && IsMinimum(b, s, less) + requires Trichotomous(less) + ensures a == b + { + LexIsAntisymmetric(a, b, less); + } + + lemma FindMinimum(s: set>, less: (T, T) -> bool) returns (a: seq) + requires s != {} + requires Trichotomous(less) && Transitive(less) + ensures IsMinimum(a, s, less) + { + a :| a in s; + if s == {a} { + LexIsReflexive(a, less); + } else { + var s' := s - {a}; + assert forall x :: x in s <==> x == a || x in s'; + var a' := FindMinimum(s', less); + if LexicographicLessOrEqual(a', a, less) { + a := a'; + } else { + assert LexicographicLessOrEqual(a, a', less) by { + LexIsTotal(a, a', less); + } + forall z | z in s + ensures LexicographicLessOrEqual(a, z, less) + { + if z == a { + LexIsReflexive(a, less); + } else { + calc { + true; + == // z in s && z != a + z in s'; + ==> // by postcondition of FindMinim(s') above + LexicographicLessOrEqual(a', z, less); + ==> { LexIsTransitive(a, a', z, less); } + LexicographicLessOrEqual(a, z, less); + } + } + } + } + } + } +} \ No newline at end of file diff --git a/src/UInt.dfy b/src/UInt.dfy new file mode 100644 index 00000000..06025a9f --- /dev/null +++ b/src/UInt.dfy @@ -0,0 +1,329 @@ +module StandardLibrary.UInt { + + // TODO: Depend on types defined in dafny-lang/libraries instead + newtype uint8 = x | 0 <= x < 0x100 + newtype uint16 = x | 0 <= x < 0x1_0000 + newtype uint32 = x | 0 <= x < 0x1_0000_0000 + newtype uint64 = x | 0 <= x < 0x1_0000_0000_0000_0000 + + newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000 + newtype int64 = x | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 + newtype posInt64 = x | 0 < x < 0x8000_0000_0000_0000 witness 1 + + const UINT16_LIMIT := 0x1_0000 + const UINT32_LIMIT := 0x1_0000_0000 + const UINT64_LIMIT := 0x1_0000_0000_0000_0000 + const INT32_MAX_LIMIT := 0x8000_0000 + const INT64_MAX_LIMIT := 0x8000_0000_0000_0000 + + predicate method UInt8Less(a: uint8, b: uint8) { a < b } + + predicate method HasUint16Len(s: seq) { + |s| < UINT16_LIMIT + } + + type seq16 = s: seq | HasUint16Len(s) + type Uint8Seq16 = seq16 + + predicate method HasUint32Len(s: seq) { + |s| < UINT32_LIMIT + } + + type seq32 = s: seq | HasUint32Len(s) + type Uint8Seq32 = seq32 + + predicate method HasUint64Len(s: seq) { + |s| < UINT64_LIMIT + } + + type seq64 = s: seq | HasUint64Len(s) + type Uint8Seq64 = seq64 + + function method UInt16ToSeq(x: uint16): (ret: seq) + ensures |ret| == 2 + ensures 0x100 * ret[0] as uint16 + ret[1] as uint16 == x + { + var b0 := (x / 0x100) as uint8; + var b1 := (x % 0x100) as uint8; + [b0, b1] + } + + function method SeqToUInt16(s: seq): (x: uint16) + requires |s| == 2 + ensures UInt16ToSeq(x) == s + ensures x >= 0 + { + var x0 := s[0] as uint16 * 0x100; + x0 + s[1] as uint16 + } + + lemma UInt16SeqSerializeDeserialize(x: uint16) + ensures SeqToUInt16(UInt16ToSeq(x)) == x + {} + + lemma UInt16SeqDeserializeSerialize(s: seq) + requires |s| == 2 + ensures UInt16ToSeq(SeqToUInt16(s)) == s + {} + + function method UInt32ToSeq(x: uint32): (ret: seq) + ensures |ret| == 4 + ensures 0x100_0000 * ret[0] as uint32 + 0x1_0000 * ret[1] as uint32 + 0x100 * ret[2] as uint32 + ret[3] as uint32 == x + { + var b0 := (x / 0x100_0000) as uint8; + var x0 := x - (b0 as uint32 * 0x100_0000); + + var b1 := (x0 / 0x1_0000) as uint8; + var x1 := x0 - (b1 as uint32 * 0x1_0000); + + var b2 := (x1 / 0x100) as uint8; + var b3 := (x1 % 0x100) as uint8; + [b0, b1, b2, b3] + } + + function method SeqToUInt32(s: seq): (x: uint32) + requires |s| == 4 + ensures UInt32ToSeq(x) == s + { + var x0 := s[0] as uint32 * 0x100_0000; + var x1 := x0 + s[1] as uint32 * 0x1_0000; + var x2 := x1 + s[2] as uint32 * 0x100; + x2 + s[3] as uint32 + } + + lemma UInt32SeqSerializeDeserialize(x: uint32) + ensures SeqToUInt32(UInt32ToSeq(x)) == x + {} + + lemma UInt32SeqDeserializeSerialize(s: seq) + requires |s| == 4 + ensures UInt32ToSeq(SeqToUInt32(s)) == s + {} + + function method UInt64ToSeq(x: uint64): (ret: seq) + ensures |ret| == 8 + ensures 0x100_0000_0000_0000 * ret[0] as uint64 + 0x1_0000_0000_0000 * ret[1] as uint64 + + 0x100_0000_0000 * ret[2] as uint64 + 0x1_0000_0000 * ret[3] as uint64 + 0x100_0000 * ret[4] as uint64 + + 0x1_0000 * ret[5] as uint64 + 0x100 * ret[6] as uint64 + ret[7] as uint64 == x + { + var b0 := (x / 0x100_0000_0000_0000) as uint8; + var x0 := x - (b0 as uint64 * 0x100_0000_0000_0000); + + var b1 := (x0 / 0x1_0000_0000_0000) as uint8; + var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); + + var b2 := (x1 / 0x100_0000_0000) as uint8; + var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); + + var b3 := (x2 / 0x1_0000_0000) as uint8; + var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); + + var b4 := (x3 / 0x100_0000) as uint8; + var x4 := x3 - (b4 as uint64 * 0x100_0000); + + var b5 := (x4 / 0x1_0000) as uint8; + var x5 := x4 - (b5 as uint64 * 0x1_0000); + + var b6 := (x5 / 0x100) as uint8; + var b7 := (x5 % 0x100) as uint8; + [b0, b1, b2, b3, b4, b5, b6, b7] + } + + function method SeqToUInt64(s: seq): (x: uint64) + requires |s| == 8 + ensures UInt64ToSeq(x) == s + { + var x0 := s[0] as uint64 * 0x100_0000_0000_0000; + var x1 := x0 + s[1] as uint64 * 0x1_0000_0000_0000; + var x2 := x1 + s[2] as uint64 * 0x100_0000_0000; + var x3 := x2 + s[3] as uint64 * 0x1_0000_0000; + var x4 := x3 + s[4] as uint64 * 0x100_0000; + var x5 := x4 + s[5] as uint64 * 0x1_0000; + var x6 := x5 + s[6] as uint64 * 0x100; + var x := x6 + s[7] as uint64; + UInt64SeqSerialize(x, s); + x + } + + lemma UInt64SeqSerialize(x: uint64, s: seq) + requires |s| == 8 + requires 0x100_0000_0000_0000 * s[0] as uint64 + + 0x1_0000_0000_0000 * s[1] as uint64 + + 0x100_0000_0000 * s[2] as uint64 + + 0x1_0000_0000 * s[3] as uint64 + + 0x100_0000 * s[4] as uint64 + + 0x1_0000 * s[5] as uint64 + + 0x100 * s[6] as uint64 + + s[7] as uint64 == x + ensures UInt64ToSeq(x) == s + { + calc { + UInt64ToSeq(x); + == + UInt64ToSeq(s[0] as uint64 * 0x100_0000_0000_0000 + + s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + == + var b0 := ((s[0] as uint64 * 0x100_0000_0000_0000 + + s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64) / 0x100_0000_0000_0000) as uint8; + assert b0 == s[0]; + var x0 := (s[0] as uint64 * 0x100_0000_0000_0000 + + s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64) - (b0 as uint64 * 0x100_0000_0000_0000); + assert x0 == (s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b1 := (x0 / 0x1_0000_0000_0000) as uint8; + assert b1 == s[1]; + var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); + assert x1 == (s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b2 := (x1 / 0x100_0000_0000) as uint8; + assert b2 == s[2]; + var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); + assert x2 == (s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b3 := (x2 / 0x1_0000_0000) as uint8; + assert b3 == s[3]; + var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); + assert x3 == (s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b4 := (x3 / 0x100_0000) as uint8; + assert b4 == s[4]; + var x4 := x3 - (b4 as uint64 * 0x100_0000); + assert x4 == (s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b5 := (x4 / 0x1_0000) as uint8; + assert b5 == s[5]; + var x5 := x4 - (b5 as uint64 * 0x1_0000); + assert x5 == (s[6] as uint64 * 0x100 + s[7] as uint64); + + var b6 := (x5 / 0x100) as uint8; + assert b6 == s[6]; + var b7 := (x5 % 0x100) as uint8; + assert b7 == s[7]; + [b0, b1, b2, b3, b4, b5, b6, b7]; + == + [s[0], s[1], s[2], s[3], s[4], s[5], s[6], s[7]]; + == + s; + } + } + + lemma UInt64SeqSerializeDeserialize(x: uint64) + ensures SeqToUInt64(UInt64ToSeq(x)) == x + {} + + lemma UInt64SeqDeserializeSerialize(s: seq) + requires |s| == 8 + ensures UInt64ToSeq(SeqToUInt64(s)) == s + {} + + function SeqToNat(s: seq): nat { + if s == [] then + 0 + else + var finalIndex := |s| - 1; + SeqToNat(s[..finalIndex]) * 0x100 + s[finalIndex] as nat + } + + // By the following lemma, prepending a 0 to a byte sequence does not change its SeqToNat value + lemma SeqToNatZeroPrefix(s: seq) + ensures SeqToNat(s) == SeqToNat([0] + s) + { + if s == [] { + } else { + var s' := [0] + s; + var sLength := |s|; + var sFinalIndex := sLength - 1; + calc { + SeqToNat(s); + == + SeqToNat(s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; + == + SeqToNat([0] + s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; + == { assert (s'[..sLength] == [0] + s[..sFinalIndex]) && s'[sLength] == s[sFinalIndex]; } + SeqToNat(s'[..sLength]) * 0x100 + s'[sLength] as nat; + == + SeqToNat(s'); + == + SeqToNat([0] + s); + } + } + } + + // By the following lemma, SeqToNat(s) == n is automatically true if the given preconditions are true + lemma SeqWithUInt32Suffix(s: seq, n: nat) + requires n < UINT32_LIMIT + requires 4 <= |s| + requires var suffixStartIndex := |s| - 4; + (s[suffixStartIndex..] == UInt32ToSeq(n as uint32)) && + (forall i :: 0 <= i < suffixStartIndex ==> s[i] == 0) + ensures SeqToNat(s) == n + { + if |s| == 4 { + calc { + SeqToNat(s); + == + SeqToNat(s[..3]) + * 0x100 + s[3] as nat; + == { assert s[..3][..2] == s[..2] && s[..3][2] == s[2]; } + (SeqToNat(s[..2]) + * 0x100 + s[2] as nat) + * 0x100 + s[3] as nat; + == { assert s[..2][..1] == s[..1] && s[..2][1] == s[1]; } + ((SeqToNat(s[..1]) + * 0x100 + s[1] as nat) + * 0x100 + s[2] as nat) + * 0x100 + s[3] as nat; + == { assert s[..1][..0] == s[..0] && s[..1][0] == s[0]; } + (((SeqToNat(s[..0]) + * 0x100 + s[0] as nat) + * 0x100 + s[1] as nat) + * 0x100 + s[2] as nat) + * 0x100 + s[3] as nat; + == + n; + } + } else { + assert s == [0] + s[1..]; + SeqToNatZeroPrefix(s[1..]); + SeqWithUInt32Suffix(s[1..], n); + } + } +} \ No newline at end of file From d8f8cee0e2eefe915e608899f07a3d009139166d Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Tue, 16 Aug 2022 16:32:39 -0400 Subject: [PATCH 04/32] adding 'RUN' line --- src/StandardLibrary.dfy | 3 +++ src/UInt.dfy | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/StandardLibrary.dfy b/src/StandardLibrary.dfy index 22113692..ff0fc57b 100644 --- a/src/StandardLibrary.dfy +++ b/src/StandardLibrary.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" + + include "../../libraries/src/Wrappers.dfy" include "UInt.dfy" diff --git a/src/UInt.dfy b/src/UInt.dfy index 06025a9f..605e9cf7 100644 --- a/src/UInt.dfy +++ b/src/UInt.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 "%s" + + module StandardLibrary.UInt { // TODO: Depend on types defined in dafny-lang/libraries instead From 57e35aec3b7143232a6d7693ee07988a03ef950d Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Tue, 16 Aug 2022 16:33:42 -0400 Subject: [PATCH 05/32] 'RUN' line --- src/Collections/Sequences/Sorting.dfy | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Collections/Sequences/Sorting.dfy b/src/Collections/Sequences/Sorting.dfy index a14b134f..2bc38461 100644 --- a/src/Collections/Sequences/Sorting.dfy +++ b/src/Collections/Sequences/Sorting.dfy @@ -1,3 +1,5 @@ +// RUN: %dafny /compile:0 "%s" + include "../../StandardLibrary.dfy" include "../../UInt.dfy" include "../Sequences/Seq.dfy" From ac104b2725731a6c124d8b13e96fe66157064667 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Wed, 17 Aug 2022 11:01:44 -0400 Subject: [PATCH 06/32] chnages as suggested for verification --- src/Collections/Sequences/Sorting.dfy | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/Collections/Sequences/Sorting.dfy b/src/Collections/Sequences/Sorting.dfy index 2bc38461..82ec91be 100644 --- a/src/Collections/Sequences/Sorting.dfy +++ b/src/Collections/Sequences/Sorting.dfy @@ -9,12 +9,12 @@ module sorting{ reveals Reflexive, AntiSymmetric, Connected, TotalOrdering reveals LexicographicByteSeqBelow, LexicographicByteSeqBelowAux provides AboutLexicographicByteSeqBelow - provides MergeSortBy + provides SortedBy, MergeSortBy, MergeSortedBy provides StandardLibrary, UInt import StandardLibrary import opened UInt = StandardLibrary.UInt - import Seq + import opened Seq predicate Reflexive(R: (T, T) -> bool) { forall x :: R(x, x) @@ -115,7 +115,8 @@ predicate TotalOrdering(R: (T, T) -> bool) { { } - predicate method SortedBy(a: seq,compare: (T, T) -> bool ) { + predicate method SortedBy(a: seq,compare: (T, T) -> bool ) + { forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]) } @@ -125,7 +126,11 @@ predicate TotalOrdering(R: (T, T) -> bool) { {} function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :seq) + requires StandardLibrary.Transitive(compare) + requires Connected(compare) ensures multiset(a) == multiset(result) + ensures SortedBy(result,compare) + { if |a| <= 1 then a @@ -144,7 +149,10 @@ function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :se function method {:tailrecursion} MergeSortedBy(left: seq, right: seq, compare: (T, T) -> bool) : (result :seq) requires SortedBy(left,compare) requires SortedBy(right,compare) + requires StandardLibrary.Transitive(compare) + requires Connected(compare) ensures multiset(left + right) == multiset(result) + ensures SortedBy(result,compare) { if |left| == 0 then right @@ -168,6 +176,6 @@ method Sort(s: seq, compare: (T, T) -> bool) returns (result :seq) requires StandardLibrary.Transitive(compare) requires Connected(compare) { - MergeSortBy(s,compare) + result := MergeSortBy(s,compare); } } From 9af98ed9301ab664a76c95e0d8a2b1325ebc3b17 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Wed, 17 Aug 2022 16:57:49 -0400 Subject: [PATCH 07/32] removing predicates and lemmas not needed,formatting. --- src/Collections/Sequences/Sorting.dfy | 30 ++++++++++++++++++--------- src/UInt.dfy | 4 ++++ 2 files changed, 24 insertions(+), 10 deletions(-) diff --git a/src/Collections/Sequences/Sorting.dfy b/src/Collections/Sequences/Sorting.dfy index 82ec91be..54af7a0a 100644 --- a/src/Collections/Sequences/Sorting.dfy +++ b/src/Collections/Sequences/Sorting.dfy @@ -1,10 +1,15 @@ // RUN: %dafny /compile:0 "%s" +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + include "../../StandardLibrary.dfy" include "../../UInt.dfy" include "../Sequences/Seq.dfy" -module sorting{ +module Sorting { export reveals Reflexive, AntiSymmetric, Connected, TotalOrdering reveals LexicographicByteSeqBelow, LexicographicByteSeqBelowAux @@ -16,19 +21,23 @@ module sorting{ import opened UInt = StandardLibrary.UInt import opened Seq -predicate Reflexive(R: (T, T) -> bool) { + predicate Reflexive(R: (T, T) -> bool) + { forall x :: R(x, x) } -predicate AntiSymmetric(R: (T, T) -> bool) { + predicate AntiSymmetric(R: (T, T) -> bool) + { forall x, y :: R(x, y) && R(y, x) ==> x == y } -predicate Connected(R: (T, T) -> bool) { + predicate Connected(R: (T, T) -> bool) + { forall x, y :: R(x, y) || R(y, x) } -predicate TotalOrdering(R: (T, T) -> bool) { + predicate TotalOrdering(R: (T, T) -> bool) + { && Reflexive(R) && AntiSymmetric(R) && StandardLibrary.Transitive(R) @@ -40,7 +49,8 @@ predicate TotalOrdering(R: (T, T) -> bool) { */ // reflexivelexicographical comparison of byte sequences - predicate method LexicographicByteSeqBelow(x: seq, y: seq) { + predicate method LexicographicByteSeqBelow(x: seq, y: seq) + { LexicographicByteSeqBelowAux(x, y, 0) } @@ -116,7 +126,7 @@ predicate TotalOrdering(R: (T, T) -> bool) { } predicate method SortedBy(a: seq,compare: (T, T) -> bool ) - { + { forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]) } @@ -125,7 +135,7 @@ predicate TotalOrdering(R: (T, T) -> bool) { requires |s| == 0 || compare(x,s[0]) {} -function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :seq) + function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :seq) requires StandardLibrary.Transitive(compare) requires Connected(compare) ensures multiset(a) == multiset(result) @@ -146,7 +156,7 @@ function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :se MergeSortedBy(leftSorted, rightSorted, compare) } - function method {:tailrecursion} MergeSortedBy(left: seq, right: seq, compare: (T, T) -> bool) : (result :seq) + function method {:tailrecursion} MergeSortedBy(left: seq, right: seq, compare: (T, T) -> bool) : (result :seq) requires SortedBy(left,compare) requires SortedBy(right,compare) requires StandardLibrary.Transitive(compare) @@ -171,7 +181,7 @@ function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :se [left[0]] + MergeSortedBy(left[1..], right, compare) } -method Sort(s: seq, compare: (T, T) -> bool) returns (result :seq) + method Sort(s: seq, compare: (T, T) -> bool) returns (result :seq) ensures multiset(s) == multiset(result) requires StandardLibrary.Transitive(compare) requires Connected(compare) diff --git a/src/UInt.dfy b/src/UInt.dfy index 605e9cf7..5f65af20 100644 --- a/src/UInt.dfy +++ b/src/UInt.dfy @@ -1,5 +1,9 @@ // RUN: %dafny /compile:0 "%s" +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ module StandardLibrary.UInt { From aab9de95f94e69473e62fee39a22f7c65d0e9d67 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Wed, 17 Aug 2022 16:59:06 -0400 Subject: [PATCH 08/32] adding copyrights info. --- src/StandardLibrary.dfy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/StandardLibrary.dfy b/src/StandardLibrary.dfy index ff0fc57b..00b7708d 100644 --- a/src/StandardLibrary.dfy +++ b/src/StandardLibrary.dfy @@ -1,5 +1,9 @@ // RUN: %dafny /compile:0 "%s" +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ include "../../libraries/src/Wrappers.dfy" include "UInt.dfy" From 513d1655473eb6ded2847acf2e8c6207b2bc2401 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Thu, 18 Aug 2022 12:13:12 -0400 Subject: [PATCH 09/32] more changes as suggested to remove unused import and formatting. --- src/UInt.dfy | 1 - 1 file changed, 1 deletion(-) diff --git a/src/UInt.dfy b/src/UInt.dfy index 5f65af20..c19594c6 100644 --- a/src/UInt.dfy +++ b/src/UInt.dfy @@ -7,7 +7,6 @@ module StandardLibrary.UInt { - // TODO: Depend on types defined in dafny-lang/libraries instead newtype uint8 = x | 0 <= x < 0x100 newtype uint16 = x | 0 <= x < 0x1_0000 newtype uint32 = x | 0 <= x < 0x1_0000_0000 From f44ea6fab748c632c85bce0c59acfc4d7759031a Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Wed, 31 Aug 2022 15:25:39 -0400 Subject: [PATCH 10/32] following suggestions --- src/Collections/Sequences/Seq.dfy | 171 ++++++++++++++++++++++- src/Collections/Sequences/Sorting.dfy | 111 +-------------- src/{StandardLibrary.dfy => Helpers.dfy} | 125 +---------------- src/Lexicographics.dfy | 95 +++++++++++++ src/UInt.dfy | 2 +- 5 files changed, 273 insertions(+), 231 deletions(-) rename src/{StandardLibrary.dfy => Helpers.dfy} (71%) create mode 100644 src/Lexicographics.dfy diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 39f5ac92..cd9ed306 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -13,13 +13,23 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "../../Wrappers.dfy" include "../../Math.dfy" +include "../../Helpers.dfy" +include "../../Lexicographics.dfy" module Seq { + export + provides SortedBy, MergeSortBy, MergeSortedWith + provides Helpers, UInt, Lexicographics, Relations - import opened Wrappers + + import opened Wrappers = Helpers.Wrappers import Math + import Helpers + import opened Comparison + import opened UInt = Helpers.UInt + import opened Lexicographics + import opened Relations = Lexicographics.Relations /********************************************************** * @@ -765,4 +775,161 @@ module Seq { } } + +/********************************************************** + * + * Splitting of Sequences + * + ***********************************************************/ + + + lemma SeqTakeAppend(s: seq, i: int) + requires 0 <= i < |s| + ensures s[..i] + [s[i]] == s[..i + 1] + {} + + function method {:tailrecursion} Join(ss: seq>, joiner: seq): (s: seq) + requires 0 < |ss| + { + if |ss| == 1 then ss[0] else ss[0] + joiner + Join(ss[1..], joiner) + } + + function method {:tailrecursion} Split(s: seq, delim: T): (res: seq>) + ensures delim !in s ==> res == [s] + ensures s == [] ==> res == [[]] + ensures 0 < |res| + ensures forall i :: 0 <= i < |res| ==> delim !in res[i] + ensures Join(res, [delim]) == s + decreases |s| + { + var i := FindIndexMatching(s, delim, 0); + if i.Some? then [s[..i.value]] + Split(s[(i.value + 1)..], delim) else [s] + } + + lemma WillSplitOnDelim(s: seq, delim: T, prefix: seq) + requires |prefix| < |s| + requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i] + requires delim !in prefix && s[|prefix|] == delim + ensures Split(s, delim) == [prefix] + Split(s[|prefix| + 1..], delim) + { + calc { + Split(s, delim); + == + var i := FindIndexMatching(s, delim, 0); + if i.Some? then [s[..i.value]] + Split(s[i.value + 1..], delim) else [s]; + == { FindIndexMatchingLocatesElem(s, delim, 0, |prefix|); assert FindIndexMatching(s, delim, 0).Some?; } + [s[..|prefix|]] + Split(s[|prefix| + 1..], delim); + == { assert s[..|prefix|] == prefix; } + [prefix] + Split(s[|prefix| + 1..], delim); + } + } + + lemma WillNotSplitWithOutDelim(s: seq, delim: T) + requires delim !in s + ensures Split(s, delim) == [s] + { + calc { + Split(s, delim); + == + var i := FindIndexMatching(s, delim, 0); + if i.Some? then [s[..i.value]] + Split(s[i.value+1..], delim) else [s]; + == { FindIndexMatchingLocatesElem(s, delim, 0, |s|); } + [s]; + } + } + + lemma FindIndexMatchingLocatesElem(s: seq, c: T, start: nat, elemIndex: nat) + requires start <= elemIndex <= |s| + requires forall i :: start <= i < elemIndex ==> s[i] != c + requires elemIndex == |s| || s[elemIndex] == c + ensures FindIndexMatching(s, c, start) == if elemIndex == |s| then None else Some(elemIndex) + decreases elemIndex - start + {} + + function method FindIndexMatching(s: seq, c: T, i: nat): (index: Option) + requires i <= |s| + ensures index.Some? ==> i <= index.value < |s| && s[index.value] == c && c !in s[i..index.value] + ensures index.None? ==> c !in s[i..] + decreases |s| - i + { + FindIndex(s, x => x == c, i) + } + + function method {:tailrecursion} FindIndex(s: seq, f: T -> bool, i: nat): (index: Option) + requires i <= |s| + ensures index.Some? ==> i <= index.value < |s| && f(s[index.value]) && (forall j :: i <= j < index.value ==> !f(s[j])) + ensures index.None? ==> forall j :: i <= j < |s| ==> !f(s[j]) + decreases |s| - i + { + if i == |s| then None + else if f(s[i]) then Some(i) + else FindIndex(s, f, i + 1) + } + + /********************************************************** + * + * Sorting of Sequences + * + ***********************************************************/ + + + predicate method SortedBy(a: seq) + { + forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]) + } + + lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> Comparison.CompResult) + requires SortedBy(s, compare) + requires |s| == 0 || compare(x,s[0]) + {} + + //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedBy` + function method MergeSortBy(a: seq, compare: (T, T) -> Comparison.CompResult): (result :seq) + requires Helpers.Transitive(compare) + requires Connected(compare) + ensures multiset(a) == multiset(result) + ensures SortedBy(result,compare) + + { + 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, compare); + var rightSorted := MergeSortBy(right, compare); + + MergeSortedBy(leftSorted, rightSorted, compare) + } + + function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, compare: (T, T) -> Comparison.CompResult) : (result :seq) + requires SortedBy(left,compare) + requires SortedBy(right,compare) + requires Helpers.Transitive(compare) + requires Connected(compare) + ensures multiset(left + right) == multiset(result) + ensures SortedBy(result,compare) + { + if |left| == 0 then + right + else if |right| == 0 then + left + else if compare(left[0],right[0]).LessThan? then + LemmaNewFirstElementStillSortedBy(left[0], MergeSortedBy(left[1..], right, compare), compare); + assert left == [left[0]] + left[1..]; + + [left[0]] + MergeSortedBy(left[1..], right, compare) + + + else + LemmaNewFirstElementStillSortedBy(right[0], MergeSortedBy(left, right[1..], compare), compare); + assert right == [right[0]] + right[1..]; + + [right[0]] + MergeSortedBy(left, right[1..], compare) + } + + } diff --git a/src/Collections/Sequences/Sorting.dfy b/src/Collections/Sequences/Sorting.dfy index 54af7a0a..68a0618b 100644 --- a/src/Collections/Sequences/Sorting.dfy +++ b/src/Collections/Sequences/Sorting.dfy @@ -8,122 +8,17 @@ include "../../StandardLibrary.dfy" include "../../UInt.dfy" include "../Sequences/Seq.dfy" +include "../../Lexicographics.dfy" module Sorting { export - reveals Reflexive, AntiSymmetric, Connected, TotalOrdering - reveals LexicographicByteSeqBelow, LexicographicByteSeqBelowAux - provides AboutLexicographicByteSeqBelow provides SortedBy, MergeSortBy, MergeSortedBy - provides StandardLibrary, UInt + provides StandardLibrary, UInt, Lexicographics import StandardLibrary import opened UInt = StandardLibrary.UInt import opened Seq - - predicate Reflexive(R: (T, T) -> bool) - { - forall x :: R(x, x) - } - - predicate AntiSymmetric(R: (T, T) -> bool) - { - forall x, y :: R(x, y) && R(y, x) ==> x == y - } - - predicate Connected(R: (T, T) -> bool) - { - forall x, y :: R(x, y) || R(y, x) - } - - predicate TotalOrdering(R: (T, T) -> bool) - { - && Reflexive(R) - && AntiSymmetric(R) - && StandardLibrary.Transitive(R) - && Connected(R) - } - - /* - * Useful orderings - */ - - // reflexivelexicographical comparison of byte sequences - predicate method LexicographicByteSeqBelow(x: seq, y: seq) - { - LexicographicByteSeqBelowAux(x, y, 0) - } - - predicate method LexicographicByteSeqBelowAux(x: seq, y: seq, n: nat) - requires n <= |x| && n <= |y| - decreases |x| - n - { - || n == |x| - || (n != |y| && x[n] < y[n]) - || (n != |y| && x[n] == y[n] && LexicographicByteSeqBelowAux(x, y, n + 1)) - } - - lemma AboutLexicographicByteSeqBelow() - ensures TotalOrdering(LexicographicByteSeqBelow) - { - assert Reflexive(LexicographicByteSeqBelow) by { - forall x, n | 0 <= n <= |x| { - AboutLexicographicByteSeqBelowAux_Reflexive(x, n); - } - } - assert AntiSymmetric(LexicographicByteSeqBelow) by { - forall x, y, n: nat | - n <= |x| && n <= |y| && x[..n] == y[..n] && - LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) - { - AboutLexicographicByteSeqBelowAux_AntiSymmetric(x, y, n); - } - } - assert StandardLibrary.Transitive(LexicographicByteSeqBelow) by { - forall x, y, z, n: nat | - n <= |x| && n <= |y| && n <= |z| && - LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) - { - AboutLexicographicByteSeqBelowAux_Transitive(x, y, z, n); - } - } - assert Connected(LexicographicByteSeqBelow) by { - forall x, y, n: nat | n <= |x| && n <= |y| { - AboutLexicographicByteSeqBelowAux_Connected(x, y, n); - } - } - } - - lemma AboutLexicographicByteSeqBelowAux_Reflexive(x: seq, n: nat) - requires n <= |x| - ensures LexicographicByteSeqBelowAux(x, x, n) - decreases |x| - n - { - } - - lemma AboutLexicographicByteSeqBelowAux_AntiSymmetric(x: seq, y: seq, n: nat) - requires n <= |x| && n <= |y| - requires x[..n] == y[..n] - requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) - ensures x == y - decreases |x| - n - { - } - - lemma AboutLexicographicByteSeqBelowAux_Transitive(x: seq, y: seq, z: seq, n: nat) - requires n <= |x| && n <= |y| && n <= |z| - requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) - ensures LexicographicByteSeqBelowAux(x, z, n) - decreases |x| - n - { - } - - lemma AboutLexicographicByteSeqBelowAux_Connected(x: seq, y: seq, n: nat) - requires n <= |x| && n <= |y| - ensures LexicographicByteSeqBelowAux(x, y, n) || LexicographicByteSeqBelowAux(y, x, n) - decreases |x| - n - { - } + import opened Lexicographics predicate method SortedBy(a: seq,compare: (T, T) -> bool ) { diff --git a/src/StandardLibrary.dfy b/src/Helpers.dfy similarity index 71% rename from src/StandardLibrary.dfy rename to src/Helpers.dfy index 00b7708d..61b434df 100644 --- a/src/StandardLibrary.dfy +++ b/src/Helpers.dfy @@ -8,129 +8,10 @@ include "../../libraries/src/Wrappers.dfy" include "UInt.dfy" -module StandardLibrary { +module Helpers { import opened Wrappers import opened U = UInt - lemma SeqTakeAppend(s: seq, i: int) - requires 0 <= i < |s| - ensures s[..i] + [s[i]] == s[..i + 1] - {} - - function method {:tailrecursion} Join(ss: seq>, joiner: seq): (s: seq) - requires 0 < |ss| - { - if |ss| == 1 then ss[0] else ss[0] + joiner + Join(ss[1..], joiner) - } - - function method {:tailrecursion} Split(s: seq, delim: T): (res: seq>) - ensures delim !in s ==> res == [s] - ensures s == [] ==> res == [[]] - ensures 0 < |res| - ensures forall i :: 0 <= i < |res| ==> delim !in res[i] - ensures Join(res, [delim]) == s - decreases |s| - { - var i := FindIndexMatching(s, delim, 0); - if i.Some? then [s[..i.value]] + Split(s[(i.value + 1)..], delim) else [s] - } - - lemma WillSplitOnDelim(s: seq, delim: T, prefix: seq) - requires |prefix| < |s| - requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i] - requires delim !in prefix && s[|prefix|] == delim - ensures Split(s, delim) == [prefix] + Split(s[|prefix| + 1..], delim) - { - calc { - Split(s, delim); - == - var i := FindIndexMatching(s, delim, 0); - if i.Some? then [s[..i.value]] + Split(s[i.value + 1..], delim) else [s]; - == { FindIndexMatchingLocatesElem(s, delim, 0, |prefix|); assert FindIndexMatching(s, delim, 0).Some?; } - [s[..|prefix|]] + Split(s[|prefix| + 1..], delim); - == { assert s[..|prefix|] == prefix; } - [prefix] + Split(s[|prefix| + 1..], delim); - } - } - - lemma WillNotSplitWithOutDelim(s: seq, delim: T) - requires delim !in s - ensures Split(s, delim) == [s] - { - calc { - Split(s, delim); - == - var i := FindIndexMatching(s, delim, 0); - if i.Some? then [s[..i.value]] + Split(s[i.value+1..], delim) else [s]; - == { FindIndexMatchingLocatesElem(s, delim, 0, |s|); } - [s]; - } - } - - lemma FindIndexMatchingLocatesElem(s: seq, c: T, start: nat, elemIndex: nat) - requires start <= elemIndex <= |s| - requires forall i :: start <= i < elemIndex ==> s[i] != c - requires elemIndex == |s| || s[elemIndex] == c - ensures FindIndexMatching(s, c, start) == if elemIndex == |s| then None else Some(elemIndex) - decreases elemIndex - start - {} - - function method FindIndexMatching(s: seq, c: T, i: nat): (index: Option) - requires i <= |s| - ensures index.Some? ==> i <= index.value < |s| && s[index.value] == c && c !in s[i..index.value] - ensures index.None? ==> c !in s[i..] - decreases |s| - i - { - FindIndex(s, x => x == c, i) - } - - function method {:tailrecursion} FindIndex(s: seq, f: T -> bool, i: nat): (index: Option) - requires i <= |s| - ensures index.Some? ==> i <= index.value < |s| && f(s[index.value]) && (forall j :: i <= j < index.value ==> !f(s[j])) - ensures index.None? ==> forall j :: i <= j < |s| ==> !f(s[j]) - decreases |s| - i - { - if i == |s| then None - else if f(s[i]) then Some(i) - else FindIndex(s, f, i + 1) - } - - function method {:tailrecursion} Filter(s: seq, f: T -> bool): (res: seq) - ensures forall i :: 0 <= i < |s| && f(s[i]) ==> s[i] in res - ensures forall i :: 0 <= i < |res| ==> res[i] in s && f(res[i]) - ensures |res| <= |s| - { - if |s| == 0 then [] - else if f(s[0]) then [s[0]] + Filter(s[1..], f) - else Filter(s[1..], f) - } - - lemma FilterIsDistributive(s: seq, s': seq, f: T -> bool) - ensures Filter(s + s', f) == Filter(s, f) + Filter(s', f) - { - if s == [] { - assert s + s' == s'; - } else { - var S := s + s'; - var s1 := s[1..]; - calc { - Filter(S, f); - == // def. Filter - if f(S[0]) then [S[0]] + Filter(S[1..], f) else Filter(S[1..], f); - == { assert S[0] == s[0] && S[1..] == s1 + s'; } - if f(s[0]) then [s[0]] + Filter(s1 + s', f) else Filter(s1 + s', f); - == { FilterIsDistributive(s1, s', f); } - if f(s[0]) then [s[0]] + (Filter(s1, f) + Filter(s', f)) else Filter(s1, f) + Filter(s', f); - == // associativity of + - if f(s[0]) then ([s[0]] + Filter(s1, f)) + Filter(s', f) else Filter(s1, f) + Filter(s', f); - == // distribute + over if-then-else - (if f(s[0]) then [s[0]] + Filter(s1, f) else Filter(s1, f)) + Filter(s', f); - == // def. Filter - Filter(s, f) + Filter(s', f); - } - } - } - function method Min(a: int, b: int): int { if a < b then a else b } @@ -412,4 +293,8 @@ module StandardLibrary { } } } +} + +module Comparison { + datatype CompResult = LessThan | Equals | GreaterThan } \ No newline at end of file diff --git a/src/Lexicographics.dfy b/src/Lexicographics.dfy new file mode 100644 index 00000000..4bbf1cea --- /dev/null +++ b/src/Lexicographics.dfy @@ -0,0 +1,95 @@ +// RUN: %dafny /compile:0 "%s" + +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +include "Relations.dfy" + +module Lexicographics { + export + reveals LexicographicByteSeqBelow, LexicographicByteSeqBelowAux + provides Helpers, UInt, Relations + + import Helpers = Relations.Helpers + import opened UInt = Helpers.UInt + import opened Relations + + // reflexivelexicographical comparison of byte sequences + predicate method LexicographicByteSeqBelow(x: seq, y: seq) + { + LexicographicByteSeqBelowAux(x, y, 0) + } + + predicate method LexicographicByteSeqBelowAux(x: seq, y: seq, n: nat) + requires n <= |x| && n <= |y| + decreases |x| - n + { + || n == |x| + || (n != |y| && x[n] < y[n]) + || (n != |y| && x[n] == y[n] && LexicographicByteSeqBelowAux(x, y, n + 1)) + } + + lemma AboutLexicographicByteSeqBelow() + ensures TotalOrdering(LexicographicByteSeqBelow) + { + assert Reflexive(LexicographicByteSeqBelow) by { + forall x, n | 0 <= n <= |x| { + AboutLexicographicByteSeqBelowAux_Reflexive(x, n); + } + } + assert AntiSymmetric(LexicographicByteSeqBelow) by { + forall x, y, n: nat | + n <= |x| && n <= |y| && x[..n] == y[..n] && + LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) + { + AboutLexicographicByteSeqBelowAux_AntiSymmetric(x, y, n); + } + } + assert Helpers.Transitive(LexicographicByteSeqBelow) by { + forall x, y, z, n: nat | + n <= |x| && n <= |y| && n <= |z| && + LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) + { + AboutLexicographicByteSeqBelowAux_Transitive(x, y, z, n); + } + } + assert Connected(LexicographicByteSeqBelow) by { + forall x, y, n: nat | n <= |x| && n <= |y| { + AboutLexicographicByteSeqBelowAux_Connected(x, y, n); + } + } + } + + lemma AboutLexicographicByteSeqBelowAux_Reflexive(x: seq, n: nat) + requires n <= |x| + ensures LexicographicByteSeqBelowAux(x, x, n) + decreases |x| - n + { + } + + lemma AboutLexicographicByteSeqBelowAux_AntiSymmetric(x: seq, y: seq, n: nat) + requires n <= |x| && n <= |y| + requires x[..n] == y[..n] + requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) + ensures x == y + decreases |x| - n + { + } + + lemma AboutLexicographicByteSeqBelowAux_Transitive(x: seq, y: seq, z: seq, n: nat) + requires n <= |x| && n <= |y| && n <= |z| + requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) + ensures LexicographicByteSeqBelowAux(x, z, n) + decreases |x| - n + { + } + + lemma AboutLexicographicByteSeqBelowAux_Connected(x: seq, y: seq, n: nat) + requires n <= |x| && n <= |y| + ensures LexicographicByteSeqBelowAux(x, y, n) || LexicographicByteSeqBelowAux(y, x, n) + decreases |x| - n + { + } +} \ No newline at end of file diff --git a/src/UInt.dfy b/src/UInt.dfy index c19594c6..74c2cc92 100644 --- a/src/UInt.dfy +++ b/src/UInt.dfy @@ -5,7 +5,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module StandardLibrary.UInt { +module Helpers.UInt { newtype uint8 = x | 0 <= x < 0x100 newtype uint16 = x | 0 <= x < 0x1_0000 From 71fe4743408fefa31ded9d472e00b84bca10bbd2 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Thu, 1 Sep 2022 11:19:35 -0400 Subject: [PATCH 11/32] changes file structure to make import and exports simple. --- src/Collections/Sequences/Seq.dfy | 35 ++-- src/Collections/Sequences/Sorting.dfy | 86 -------- src/CompariosRelations.dfy | 32 +++ src/Helpers.dfy | 287 ++------------------------ src/LexicographicHelpers.dfy | 209 +++++++++++++++++++ src/Lexicographics.dfy | 87 +++++--- src/Math.dfy | 1 - 7 files changed, 334 insertions(+), 403 deletions(-) delete mode 100644 src/Collections/Sequences/Sorting.dfy create mode 100644 src/CompariosRelations.dfy create mode 100644 src/LexicographicHelpers.dfy diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index cd9ed306..710d661e 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -14,8 +14,10 @@ *******************************************************************************/ include "../../Math.dfy" -include "../../Helpers.dfy" +include "../../LexicographicHelpers.dfy" include "../../Lexicographics.dfy" +include "../../Wrappers.dfy" +include "../../Helpers.dfy" module Seq { export @@ -23,12 +25,12 @@ module Seq { provides Helpers, UInt, Lexicographics, Relations - import opened Wrappers = Helpers.Wrappers + import opened Wrappers import Math import Helpers - import opened Comparison + import opened Helpers.Comparison import opened UInt = Helpers.UInt - import opened Lexicographics + import Lexicographics import opened Relations = Lexicographics.Relations /********************************************************** @@ -381,6 +383,15 @@ module Seq { { } + /*makes sequence of length n filled with given Value */ + function method Fill(value: T, n: nat): seq + ensures |Fill(value, n)| == n + ensures forall i :: 0 <= i < n ==> Fill(value, n)[i] == value + { + seq(n, _ => value) + } + + /********************************************************** * * Extrema in Sequences @@ -873,14 +884,14 @@ module Seq { ***********************************************************/ - predicate method SortedBy(a: seq) + predicate method SortedBy(a: seq,compare: (T, T) -> Comparison.CompResult) { - forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]) + forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]).LessThan? } lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> Comparison.CompResult) requires SortedBy(s, compare) - requires |s| == 0 || compare(x,s[0]) + requires |s| == 0 || compare(x,s[0]).LessThan? {} //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedBy` @@ -902,7 +913,7 @@ module Seq { var leftSorted := MergeSortBy(left, compare); var rightSorted := MergeSortBy(right, compare); - MergeSortedBy(leftSorted, rightSorted, compare) + MergeSortedWith(leftSorted, rightSorted, compare) } function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, compare: (T, T) -> Comparison.CompResult) : (result :seq) @@ -918,17 +929,17 @@ module Seq { else if |right| == 0 then left else if compare(left[0],right[0]).LessThan? then - LemmaNewFirstElementStillSortedBy(left[0], MergeSortedBy(left[1..], right, compare), compare); + LemmaNewFirstElementStillSortedBy(left[0], MergeSortedWith(left[1..], right, compare), compare); assert left == [left[0]] + left[1..]; - [left[0]] + MergeSortedBy(left[1..], right, compare) + [left[0]] + MergeSortedWith(left[1..], right, compare) else - LemmaNewFirstElementStillSortedBy(right[0], MergeSortedBy(left, right[1..], compare), compare); + LemmaNewFirstElementStillSortedBy(right[0], MergeSortedWith(left, right[1..], compare), compare); assert right == [right[0]] + right[1..]; - [right[0]] + MergeSortedBy(left, right[1..], compare) + [right[0]] + MergeSortedWith(left, right[1..], compare) } diff --git a/src/Collections/Sequences/Sorting.dfy b/src/Collections/Sequences/Sorting.dfy deleted file mode 100644 index 68a0618b..00000000 --- a/src/Collections/Sequences/Sorting.dfy +++ /dev/null @@ -1,86 +0,0 @@ -// RUN: %dafny /compile:0 "%s" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -include "../../StandardLibrary.dfy" -include "../../UInt.dfy" -include "../Sequences/Seq.dfy" -include "../../Lexicographics.dfy" - -module Sorting { - export - provides SortedBy, MergeSortBy, MergeSortedBy - provides StandardLibrary, UInt, Lexicographics - - import StandardLibrary - import opened UInt = StandardLibrary.UInt - import opened Seq - import opened Lexicographics - - predicate method SortedBy(a: seq,compare: (T, T) -> bool ) - { - forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]) - } - - lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> bool) - requires SortedBy(s, compare) - requires |s| == 0 || compare(x,s[0]) - {} - - function method MergeSortBy(a: seq, compare: (T, T) -> bool ): (result :seq) - requires StandardLibrary.Transitive(compare) - requires Connected(compare) - ensures multiset(a) == multiset(result) - ensures SortedBy(result,compare) - - { - 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, compare); - var rightSorted := MergeSortBy(right, compare); - - MergeSortedBy(leftSorted, rightSorted, compare) - } - - function method {:tailrecursion} MergeSortedBy(left: seq, right: seq, compare: (T, T) -> bool) : (result :seq) - requires SortedBy(left,compare) - requires SortedBy(right,compare) - requires StandardLibrary.Transitive(compare) - requires Connected(compare) - ensures multiset(left + right) == multiset(result) - ensures SortedBy(result,compare) - { - if |left| == 0 then - right - else if |right| == 0 then - left - else if compare(right[0],left[0]) then - LemmaNewFirstElementStillSortedBy(right[0], MergeSortedBy(left, right[1..], compare), compare); - assert right == [right[0]] + right[1..]; - - [right[0]] + MergeSortedBy(left, right[1..], compare) - - else - LemmaNewFirstElementStillSortedBy(left[0], MergeSortedBy(left[1..], right, compare), compare); - assert left == [left[0]] + left[1..]; - - [left[0]] + MergeSortedBy(left[1..], right, compare) - } - - method Sort(s: seq, compare: (T, T) -> bool) returns (result :seq) - ensures multiset(s) == multiset(result) - requires StandardLibrary.Transitive(compare) - requires Connected(compare) - { - result := MergeSortBy(s,compare); - } -} diff --git a/src/CompariosRelations.dfy b/src/CompariosRelations.dfy new file mode 100644 index 00000000..f4c17e79 --- /dev/null +++ b/src/CompariosRelations.dfy @@ -0,0 +1,32 @@ +include "Helpers.dfy" + +module Relations.ComparisonsRelation { + + export + reveals Reflexive, AntiSymmetric, Connected, TotalOrdering + + import opened Helpers.Comparison + + predicate Reflexive(R: (T, T) -> CompResult) + { + forall x :: R(x, x) + } + + predicate AntiSymmetric(R: (T, T) -> CompResult) + { + forall x, y :: R(x, y) && R(y, x) ==> x == y + } + + predicate Connected(R: (T, T) -> CompResult) + { + forall x, y :: R(x, y) || R(y, x) + } + + predicate TotalOrdering(R: (T, T) -> CompResult) + { + && Reflexive(R) + && AntiSymmetric(R) + && Helpers.Transitive(R) + && Connected(R) + } +} \ No newline at end of file diff --git a/src/Helpers.dfy b/src/Helpers.dfy index 61b434df..7aa6cac5 100644 --- a/src/Helpers.dfy +++ b/src/Helpers.dfy @@ -5,86 +5,19 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "../../libraries/src/Wrappers.dfy" +include "Wrappers.dfy" include "UInt.dfy" +include "Relations.dfy" module Helpers { - import opened Wrappers - import opened U = UInt - - function method Min(a: int, b: int): int { - if a < b then a else b - } - - function method Fill(value: T, n: nat): seq - ensures |Fill(value, n)| == n - ensures forall i :: 0 <= i < n ==> Fill(value, n)[i] == value - { - seq(n, _ => value) - } - - method SeqToArray(s: seq) returns (a: array) - // "Fresh" expressions require editing memory - ensures fresh(a) - ensures a.Length == |s| - ensures forall i :: 0 <= i < |s| ==> a[i] == s[i] - { - a := new T[|s|](i requires 0 <= i < |s| => s[i]); - } - - lemma SeqPartsMakeWhole(s: seq, i: nat) - requires 0 <= i <= |s| - ensures s[..i] + s[i..] == s - {} - - /* - * Lexicographic comparison of sequences. - * - * Given two sequences `a` and `b` and a strict (that is, irreflexive) - * ordering `less` on the elements of these sequences, determine whether or not - * `a` is lexicographically "less than or equal to" `b`. - * - * `a` is lexicographically "less than or equal to" `b` holds iff - * there exists a `k` such that - * - the first `k` elements of `a` and `b` are the same - * - either: - * -- `a` has length `k` (that is, `a` is a prefix of `b`) - * -- `a[k]` is strictly less (using `less`) than `b[k]` - */ + export + provides Comparison - predicate method LexicographicLessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { - exists k :: 0 <= k <= |a| && LexicographicLessOrEqualAux(a, b, less, k) - } - - predicate method LexicographicLessOrEqualAux(a: seq, b: seq, less: (T, T) -> bool, lengthOfCommonPrefix: nat) - requires 0 <= lengthOfCommonPrefix <= |a| - { - lengthOfCommonPrefix <= |b| - && (forall i :: 0 <= i < lengthOfCommonPrefix ==> a[i] == b[i]) - && (lengthOfCommonPrefix == |a| || (lengthOfCommonPrefix < |b| && less(a[lengthOfCommonPrefix], b[lengthOfCommonPrefix]))) - } - - /* - * In order for the lexicographic ordering above to have the expected properties, the - * relation "less" must be trichotomous and transitive. - * - * For an ordering `less` to be _trichotomous_ means that for any two `x` and `y`, - * EXACTLY one of the following three conditions holds: - * - less(x, y) - * - x == y - * - less(y, x) - * Note that being trichotomous implies being irreflexive. - */ - - predicate Trichotomous(less: (T, T) -> bool) { - (forall x, y :: less(x, y) || x == y || less(y, x)) && // at least one of the three - (forall x, y :: less(x, y) && less(y, x) ==> false) && // not both of the less's - (forall x, y :: less(x, y) ==> x != y) // not a less and the equality - } + import opened Comparison + import opened U = UInt + import Relations + import opened Wrappers - predicate Transitive(R: (T, T) -> bool) { - forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) - } /* * Here is an example relation and a lemma that says the relation is appropriate for use in @@ -92,209 +25,13 @@ module Helpers { */ lemma UInt8LessIsTrichotomousTransitive() - ensures Trichotomous(UInt8Less) - ensures Transitive(UInt8Less) - { - } - - /* - * As the following lemmas show, the lexicographic ordering is reflexive, antisymmetric, transitive, and total. - * The proofs are a bit pedantic and include steps that can be automated. - */ - - lemma LexIsReflexive(a: seq, less: (T, T) -> bool) - ensures LexicographicLessOrEqual(a, a, less) - { - assert LexicographicLessOrEqualAux(a, a, less, |a|); - } - - lemma LexIsAntisymmetric(a: seq, b: seq, less: (T, T) -> bool) - requires Trich: Trichotomous(less) - requires LexicographicLessOrEqual(a, b, less) - requires LexicographicLessOrEqual(b, a, less) - ensures a == b - { - assert LessIrreflexive: forall x,y :: less(x, y) ==> x != y by { - reveal Trich; - } - assert ASymmetric: forall x,y :: less(x, y) && less(y, x) ==> false by { - reveal Trich; - } - var k0 :| 0 <= k0 <= |a| && LexicographicLessOrEqualAux(a, b, less, k0); - var k1 :| 0 <= k1 <= |b| && LexicographicLessOrEqualAux(b, a, less, k1); - var max := if k0 < k1 then k1 else k0; - assert max <= |a| && max <= |b|; - assert SameUntilMax: forall i :: 0 <= i < max ==> a[i] == b[i]; - assert AA: k0 == |a| || (k0 < |b| && less(a[k0], b[k0])); - assert BB: k1 == |b| || (k1 < |a| && less(b[k1], a[k1])); - calc { - true; - ==> { reveal AA, BB; } - (k0 == |a| || (k0 < |b| && less(a[k0], b[k0]))) && (k1 == |b| || (k1 < |a| && less(b[k1], a[k1]))); - == // distribute && and || - (k0 == |a| && k1 == |b|) || - (k0 == |a| && k1 < |a| && less(b[k1], a[k1])) || - (k0 < |b| && less(a[k0], b[k0]) && k1 == |b|) || - (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); - == { reveal LessIrreflexive, SameUntilMax; } - (k0 == |a| && k1 == |b|) || - (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); - ==> { reveal LessIrreflexive, SameUntilMax; assert max <= k0 && max <= k1; } - (k0 == |a| && k1 == |b|) || - (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1]) && k0 == k1 == max); - == { reveal ASymmetric; } - k0 == |a| && k1 == |b|; - ==> { assert |a| == k0 <= max && |b| == k1 <= max ==> k0 == k1; } - max == |a| == |b|; - ==> { reveal SameUntilMax; } - a == b; - } - } - - lemma LexIsTransitive(a: seq, b: seq, c: seq, less: (T, T) -> bool) - requires Transitive(less) - requires LexicographicLessOrEqual(a, b, less) - requires LexicographicLessOrEqual(b, c, less) - ensures LexicographicLessOrEqual(a, c, less) - { - var k0 :| 0 <= k0 <= |a| && LexicographicLessOrEqualAux(a, b, less, k0); - var k1 :| 0 <= k1 <= |b| && LexicographicLessOrEqualAux(b, c, less, k1); - var k := if k0 < k1 then k0 else k1; - assert LexicographicLessOrEqualAux(a, c, less, k); - } - - lemma LexIsTotal(a: seq, b: seq, less: (T, T) -> bool) - requires Trich: Trichotomous(less) - ensures LexicographicLessOrEqual(a, b, less) || LexicographicLessOrEqual(b, a, less) - { - var m := 0; - while m < |a| && m < |b| && a[m] == b[m] - invariant m <= |a| && m <= |b| - invariant forall i :: 0 <= i < m ==> a[i] == b[i] - { - m := m + 1; - } - // m is the length of the common prefix of a and b - if m == |a| == |b| { - assert a == b; - LexIsReflexive(a, less); - } else if m == |a| < |b| { - assert LexicographicLessOrEqualAux(a, b, less, m); - } else if m == |b| < |a| { - assert LexicographicLessOrEqualAux(b, a, less, m); - } else { - assert m < |a| && m < |b|; - reveal Trich; - if - case less(a[m], b[m]) => - assert LexicographicLessOrEqualAux(a, b, less, m); - case less(b[m], a[m]) => - assert LexicographicLessOrEqualAux(b, a, less, m); - } - } - - /* - * SetToOrderedSequence(s, less) takes a set of T-strings and returns them as a sequence, - * ordered by the lexicographic ordering whose underlying irreflexive ordering is "less". - * The function is compilable, but will not exhibit enviable performance. - */ - - function method {:tailrecursion} SetToOrderedSequence(s: set>, less: (T, T) -> bool): (q: seq>) - requires Trichotomous(less) && Transitive(less) - ensures |s| == |q| - ensures forall i :: 0 <= i < |q| ==> q[i] in s - ensures forall k :: k in s ==> k in q - ensures forall i :: 0 < i < |q| ==> LexicographicLessOrEqual(q[i-1], q[i], less) - ensures forall i, j | 0 <= i < j < |q| :: q[i] != q[j]; - { - if s == {} then - [] - else - // In preparation for the assign-such-that statement below, we'll need to - // prove that a minimum exists and that it is unique. - // The following lemma shows existence: - ThereIsAMinimum(s, less); - // The following assertion shows uniqueness: - assert forall a, b :: IsMinimum(a, s, less) && IsMinimum(b, s, less) ==> a == b by { - // The proof of the assertion is the following forall statement. - // But why did we even bother to write the assert-by instead of - // just writing this forall statement in the first place? Because - // we are in an expression context and a forall statement cannot start - // an expression (because the "forall" makes the parser think that - // a forall expression is coming). - forall a, b | IsMinimum(a, s, less) && IsMinimum(b, s, less) { - // For the given a and b, the proof is settled by calling the following lemma: - MinimumIsUnique(a, b, s, less); - } - } - // The "a in s" in the following line follows from IsMinimum(a, s), so it - // is logically redundant. However, it is needed to convince the compiler - // that the assign-such-that statement is compilable. - var a :| a in s && IsMinimum(a, s, less); - [a] + SetToOrderedSequence(s - {a}, less) - } - - predicate method IsMinimum(a: seq, s: set>, less: (T, T) -> bool) { - a in s && - forall z :: z in s ==> LexicographicLessOrEqual(a, z, less) - } - - lemma ThereIsAMinimum(s: set>, less: (T, T) -> bool) - requires s != {} - requires Trichotomous(less) && Transitive(less) - ensures exists a :: IsMinimum(a, s, less) - { - var a := FindMinimum(s, less); - } - - lemma MinimumIsUnique(a: seq, b: seq, s: set>, less: (T, T) -> bool) - requires IsMinimum(a, s, less) && IsMinimum(b, s, less) - requires Trichotomous(less) - ensures a == b - { - LexIsAntisymmetric(a, b, less); - } - - lemma FindMinimum(s: set>, less: (T, T) -> bool) returns (a: seq) - requires s != {} - requires Trichotomous(less) && Transitive(less) - ensures IsMinimum(a, s, less) + ensures Relations.Trichotomous(UInt8Less) + ensures Relations.Transitive(UInt8Less) { - a :| a in s; - if s == {a} { - LexIsReflexive(a, less); - } else { - var s' := s - {a}; - assert forall x :: x in s <==> x == a || x in s'; - var a' := FindMinimum(s', less); - if LexicographicLessOrEqual(a', a, less) { - a := a'; - } else { - assert LexicographicLessOrEqual(a, a', less) by { - LexIsTotal(a, a', less); - } - forall z | z in s - ensures LexicographicLessOrEqual(a, z, less) - { - if z == a { - LexIsReflexive(a, less); - } else { - calc { - true; - == // z in s && z != a - z in s'; - ==> // by postcondition of FindMinim(s') above - LexicographicLessOrEqual(a', z, less); - ==> { LexIsTransitive(a, a', z, less); } - LexicographicLessOrEqual(a, z, less); - } - } - } - } - } } + } -module Comparison { +module Helpers.Comparison { datatype CompResult = LessThan | Equals | GreaterThan } \ No newline at end of file diff --git a/src/LexicographicHelpers.dfy b/src/LexicographicHelpers.dfy new file mode 100644 index 00000000..d9ea739c --- /dev/null +++ b/src/LexicographicHelpers.dfy @@ -0,0 +1,209 @@ +// RUN: %dafny /compile:0 "%s" + +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +include "Relations.dfy" +include "Lexicographics.dfy" + +module LexicographicHelpers{ + export + provides UInt + + import opened Relations + import opened Lexicographics + import opened Lexicographics.UInt + + lemma LexIsReflexive(a: seq, less: (T, T) -> bool) + ensures LessOrEqual(a, a, less) + { + assert LessOrEqualAux(a, a, less, |a|); + } + + lemma LexIsAntisymmetric(a: seq, b: seq, less: (T, T) -> bool) + requires Trich: Trichotomous(less) + requires LessOrEqual(a, b, less) + requires LessOrEqual(b, a, less) + ensures a == b + { + assert LessIrreflexive: forall x,y :: less(x, y) ==> x != y by { + reveal Trich; + } + assert ASymmetric: forall x,y :: less(x, y) && less(y, x) ==> false by { + reveal Trich; + } + var k0 :| 0 <= k0 <= |a| && LessOrEqualAux(a, b, less, k0); + var k1 :| 0 <= k1 <= |b| && LessOrEqualAux(b, a, less, k1); + var max := if k0 < k1 then k1 else k0; + assert max <= |a| && max <= |b|; + assert SameUntilMax: forall i :: 0 <= i < max ==> a[i] == b[i]; + assert AA: k0 == |a| || (k0 < |b| && less(a[k0], b[k0])); + assert BB: k1 == |b| || (k1 < |a| && less(b[k1], a[k1])); + calc { + true; + ==> { reveal AA, BB; } + (k0 == |a| || (k0 < |b| && less(a[k0], b[k0]))) && (k1 == |b| || (k1 < |a| && less(b[k1], a[k1]))); + == // distribute && and || + (k0 == |a| && k1 == |b|) || + (k0 == |a| && k1 < |a| && less(b[k1], a[k1])) || + (k0 < |b| && less(a[k0], b[k0]) && k1 == |b|) || + (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); + == { reveal LessIrreflexive, SameUntilMax; } + (k0 == |a| && k1 == |b|) || + (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); + ==> { reveal LessIrreflexive, SameUntilMax; assert max <= k0 && max <= k1; } + (k0 == |a| && k1 == |b|) || + (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1]) && k0 == k1 == max); + == { reveal ASymmetric; } + k0 == |a| && k1 == |b|; + ==> { assert |a| == k0 <= max && |b| == k1 <= max ==> k0 == k1; } + max == |a| == |b|; + ==> { reveal SameUntilMax; } + a == b; + } + } + + lemma LexIsTransitive(a: seq, b: seq, c: seq, less: (T, T) -> bool) + requires Transitive(less) + requires LessOrEqual(a, b, less) + requires LessOrEqual(b, c, less) + ensures LessOrEqual(a, c, less) + { + var k0 :| 0 <= k0 <= |a| && LessOrEqualAux(a, b, less, k0); + var k1 :| 0 <= k1 <= |b| && LessOrEqualAux(b, c, less, k1); + var k := if k0 < k1 then k0 else k1; + assert LessOrEqualAux(a, c, less, k); + } + + lemma LexIsTotal(a: seq, b: seq, less: (T, T) -> bool) + requires Trich: Trichotomous(less) + ensures LessOrEqual(a, b, less) || LessOrEqual(b, a, less) + { + var m := 0; + while m < |a| && m < |b| && a[m] == b[m] + invariant m <= |a| && m <= |b| + invariant forall i :: 0 <= i < m ==> a[i] == b[i] + { + m := m + 1; + } + // m is the length of the common prefix of a and b + if m == |a| == |b| { + assert a == b; + LexIsReflexive(a, less); + } else if m == |a| < |b| { + assert LessOrEqualAux(a, b, less, m); + } else if m == |b| < |a| { + assert LessOrEqualAux(b, a, less, m); + } else { + assert m < |a| && m < |b|; + reveal Trich; + if + case less(a[m], b[m]) => + assert LessOrEqualAux(a, b, less, m); + case less(b[m], a[m]) => + assert LessOrEqualAux(b, a, less, m); + } + } + /* + * SetToOrderedSequence(s, less) takes a set of T-strings and returns them as a sequence, + * ordered by the lexicographic ordering whose underlying irreflexive ordering is "less". + * The function is compilable, but will not exhibit enviable performance. + */ + + function method {:tailrecursion} SetToOrderedSequence(s: set>, less: (T, T) -> bool): (q: seq>) + requires Trichotomous(less) && Transitive(less) + ensures |s| == |q| + ensures forall i :: 0 <= i < |q| ==> q[i] in s + ensures forall k :: k in s ==> k in q + ensures forall i :: 0 < i < |q| ==> LessOrEqual(q[i-1], q[i], less) + ensures forall i, j | 0 <= i < j < |q| :: q[i] != q[j]; + { + if s == {} then + [] + else + // In preparation for the assign-such-that statement below, we'll need to + // prove that a minimum exists and that it is unique. + // The following lemma shows existence: + ThereIsAMinimum(s, less); + // The following assertion shows uniqueness: + assert forall a, b :: IsMinimum(a, s, less) && IsMinimum(b, s, less) ==> a == b by { + // The proof of the assertion is the following forall statement. + // But why did we even bother to write the assert-by instead of + // just writing this forall statement in the first place? Because + // we are in an expression context and a forall statement cannot start + // an expression (because the "forall" makes the parser think that + // a forall expression is coming). + forall a, b | IsMinimum(a, s, less) && IsMinimum(b, s, less) { + // For the given a and b, the proof is settled by calling the following lemma: + MinimumIsUnique(a, b, s, less); + } + } + // The "a in s" in the following line follows from IsMinimum(a, s), so it + // is logically redundant. However, it is needed to convince the compiler + // that the assign-such-that statement is compilable. + var a :| a in s && IsMinimum(a, s, less); + [a] + SetToOrderedSequence(s - {a}, less) + } + + predicate method IsMinimum(a: seq, s: set>, less: (T, T) -> bool) { + a in s && + forall z :: z in s ==> LessOrEqual(a, z, less) + } + + lemma ThereIsAMinimum(s: set>, less: (T, T) -> bool) + requires s != {} + requires Trichotomous(less) && Transitive(less) + ensures exists a :: IsMinimum(a, s, less) + { + var a := FindMinimum(s, less); + } + + lemma MinimumIsUnique(a: seq, b: seq, s: set>, less: (T, T) -> bool) + requires IsMinimum(a, s, less) && IsMinimum(b, s, less) + requires Trichotomous(less) + ensures a == b + { + LexIsAntisymmetric(a, b, less); + } + + lemma FindMinimum(s: set>, less: (T, T) -> bool) returns (a: seq) + requires s != {} + requires Trichotomous(less) && Transitive(less) + ensures IsMinimum(a, s, less) + { + a :| a in s; + if s == {a} { + LexIsReflexive(a, less); + } else { + var s' := s - {a}; + assert forall x :: x in s <==> x == a || x in s'; + var a' := FindMinimum(s', less); + if LessOrEqual(a', a, less) { + a := a'; + } else { + assert LessOrEqual(a, a', less) by { + LexIsTotal(a, a', less); + } + forall z | z in s + ensures LessOrEqual(a, z, less) + { + if z == a { + LexIsReflexive(a, less); + } else { + calc { + true; + == // z in s && z != a + z in s'; + ==> // by postcondition of FindMinim(s') above + LessOrEqual(a', z, less); + ==> { LexIsTransitive(a, a', z, less); } + LessOrEqual(a, z, less); + } + } + } + } + } + } +} \ No newline at end of file diff --git a/src/Lexicographics.dfy b/src/Lexicographics.dfy index 4bbf1cea..9e5e0b24 100644 --- a/src/Lexicographics.dfy +++ b/src/Lexicographics.dfy @@ -6,90 +6,119 @@ *******************************************************************************/ include "Relations.dfy" +include "UInt.dfy" module Lexicographics { export - reveals LexicographicByteSeqBelow, LexicographicByteSeqBelowAux - provides Helpers, UInt, Relations + reveals ByteSeqBelow, ByteSeqBelowAux + provides LessOrEqual, LessOrEqualAux + provides Relations, UInt - import Helpers = Relations.Helpers - import opened UInt = Helpers.UInt import opened Relations + import opened UInt = Helpers.UInt // reflexivelexicographical comparison of byte sequences - predicate method LexicographicByteSeqBelow(x: seq, y: seq) + predicate method ByteSeqBelow(x: seq, y: seq) { - LexicographicByteSeqBelowAux(x, y, 0) + ByteSeqBelowAux(x, y, 0) } - predicate method LexicographicByteSeqBelowAux(x: seq, y: seq, n: nat) + predicate method ByteSeqBelowAux(x: seq, y: seq, n: nat) requires n <= |x| && n <= |y| decreases |x| - n { || n == |x| || (n != |y| && x[n] < y[n]) - || (n != |y| && x[n] == y[n] && LexicographicByteSeqBelowAux(x, y, n + 1)) + || (n != |y| && x[n] == y[n] && ByteSeqBelowAux(x, y, n + 1)) } - lemma AboutLexicographicByteSeqBelow() - ensures TotalOrdering(LexicographicByteSeqBelow) + lemma AboutByteSeqBelow() + ensures TotalOrdering(ByteSeqBelow) { - assert Reflexive(LexicographicByteSeqBelow) by { + assert Reflexive(ByteSeqBelow) by { forall x, n | 0 <= n <= |x| { - AboutLexicographicByteSeqBelowAux_Reflexive(x, n); + AboutByteSeqBelowAux_Reflexive(x, n); } } - assert AntiSymmetric(LexicographicByteSeqBelow) by { + assert AntiSymmetric(ByteSeqBelow) by { forall x, y, n: nat | n <= |x| && n <= |y| && x[..n] == y[..n] && - LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) + ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, x, n) { - AboutLexicographicByteSeqBelowAux_AntiSymmetric(x, y, n); + AboutByteSeqBelowAux_AntiSymmetric(x, y, n); } } - assert Helpers.Transitive(LexicographicByteSeqBelow) by { + assert Relations.Transitive(ByteSeqBelow) by { forall x, y, z, n: nat | n <= |x| && n <= |y| && n <= |z| && - LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) + ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, z, n) { - AboutLexicographicByteSeqBelowAux_Transitive(x, y, z, n); + AboutByteSeqBelowAux_Transitive(x, y, z, n); } } - assert Connected(LexicographicByteSeqBelow) by { + assert Connected(ByteSeqBelow) by { forall x, y, n: nat | n <= |x| && n <= |y| { - AboutLexicographicByteSeqBelowAux_Connected(x, y, n); + AboutByteSeqBelowAux_Connected(x, y, n); } } } - lemma AboutLexicographicByteSeqBelowAux_Reflexive(x: seq, n: nat) + lemma AboutByteSeqBelowAux_Reflexive(x: seq, n: nat) requires n <= |x| - ensures LexicographicByteSeqBelowAux(x, x, n) + ensures ByteSeqBelowAux(x, x, n) decreases |x| - n { } - lemma AboutLexicographicByteSeqBelowAux_AntiSymmetric(x: seq, y: seq, n: nat) + lemma AboutByteSeqBelowAux_AntiSymmetric(x: seq, y: seq, n: nat) requires n <= |x| && n <= |y| requires x[..n] == y[..n] - requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, x, n) + requires ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, x, n) ensures x == y decreases |x| - n { } - lemma AboutLexicographicByteSeqBelowAux_Transitive(x: seq, y: seq, z: seq, n: nat) + lemma AboutByteSeqBelowAux_Transitive(x: seq, y: seq, z: seq, n: nat) requires n <= |x| && n <= |y| && n <= |z| - requires LexicographicByteSeqBelowAux(x, y, n) && LexicographicByteSeqBelowAux(y, z, n) - ensures LexicographicByteSeqBelowAux(x, z, n) + requires ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, z, n) + ensures ByteSeqBelowAux(x, z, n) decreases |x| - n { } - lemma AboutLexicographicByteSeqBelowAux_Connected(x: seq, y: seq, n: nat) + lemma AboutByteSeqBelowAux_Connected(x: seq, y: seq, n: nat) requires n <= |x| && n <= |y| - ensures LexicographicByteSeqBelowAux(x, y, n) || LexicographicByteSeqBelowAux(y, x, n) + ensures ByteSeqBelowAux(x, y, n) || ByteSeqBelowAux(y, x, n) decreases |x| - n { } + + /* + * Lexicographic comparison of sequences. + * + * Given two sequences `a` and `b` and a strict (that is, irreflexive) + * ordering `less` on the elements of these sequences, determine whether or not + * `a` is lexicographically "less than or equal to" `b`. + * + * `a` is lexicographically "less than or equal to" `b` holds iff + * there exists a `k` such that + * - the first `k` elements of `a` and `b` are the same + * - either: + * -- `a` has length `k` (that is, `a` is a prefix of `b`) + * -- `a[k]` is strictly less (using `less`) than `b[k]` + */ + + predicate method LessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { + exists k :: 0 <= k <= |a| && LessOrEqualAux(a, b, less, k) + } + + predicate method LessOrEqualAux(a: seq, b: seq, less: (T, T) -> bool, lengthOfCommonPrefix: nat) + requires 0 <= lengthOfCommonPrefix <= |a| + { + lengthOfCommonPrefix <= |b| + && (forall i :: 0 <= i < lengthOfCommonPrefix ==> a[i] == b[i]) + && (lengthOfCommonPrefix == |a| || (lengthOfCommonPrefix < |b| && less(a[lengthOfCommonPrefix], b[lengthOfCommonPrefix]))) + } + } \ No newline at end of file diff --git a/src/Math.dfy b/src/Math.dfy index b58d098b..2b7ce612 100644 --- a/src/Math.dfy +++ b/src/Math.dfy @@ -21,5 +21,4 @@ module Math { else a } - } From 41faf3791a306e5b43745642a98985a00402bd0e Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Thu, 1 Sep 2022 12:45:26 -0400 Subject: [PATCH 12/32] only verification error is compare expecting bool and not CompResult. --- src/Collections/Sequences/Seq.dfy | 14 ++++----- src/CompariosRelations.dfy | 16 ++++++++-- src/Helpers.dfy | 21 ------------- src/LexicographicHelpers.dfy | 52 +++++++++++++++++++++++++------ src/Lexicographics.dfy | 14 ++------- 5 files changed, 65 insertions(+), 52 deletions(-) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 710d661e..9d6fc1f0 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -14,24 +14,22 @@ *******************************************************************************/ include "../../Math.dfy" -include "../../LexicographicHelpers.dfy" -include "../../Lexicographics.dfy" include "../../Wrappers.dfy" include "../../Helpers.dfy" +include "../../UInt.dfy" +include "../../Relations.dfy" module Seq { export provides SortedBy, MergeSortBy, MergeSortedWith - provides Helpers, UInt, Lexicographics, Relations + provides Helpers, Relations import opened Wrappers import Math import Helpers import opened Helpers.Comparison - import opened UInt = Helpers.UInt - import Lexicographics - import opened Relations = Lexicographics.Relations + import opened Relations /********************************************************** * @@ -896,7 +894,7 @@ module Seq { //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedBy` function method MergeSortBy(a: seq, compare: (T, T) -> Comparison.CompResult): (result :seq) - requires Helpers.Transitive(compare) + requires Relations.Transitive(compare) requires Connected(compare) ensures multiset(a) == multiset(result) ensures SortedBy(result,compare) @@ -919,7 +917,7 @@ module Seq { function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, compare: (T, T) -> Comparison.CompResult) : (result :seq) requires SortedBy(left,compare) requires SortedBy(right,compare) - requires Helpers.Transitive(compare) + requires Relations.Transitive(compare) requires Connected(compare) ensures multiset(left + right) == multiset(result) ensures SortedBy(result,compare) diff --git a/src/CompariosRelations.dfy b/src/CompariosRelations.dfy index f4c17e79..f4282497 100644 --- a/src/CompariosRelations.dfy +++ b/src/CompariosRelations.dfy @@ -4,9 +4,9 @@ module Relations.ComparisonsRelation { export reveals Reflexive, AntiSymmetric, Connected, TotalOrdering - import opened Helpers.Comparison + predicate Reflexive(R: (T, T) -> CompResult) { forall x :: R(x, x) @@ -26,7 +26,19 @@ module Relations.ComparisonsRelation { { && Reflexive(R) && AntiSymmetric(R) - && Helpers.Transitive(R) + && Transitive(R) && Connected(R) } + + predicate Trichotomous(less: (T, T) -> CompResult) + { + (forall x, y :: less(x, y) || x == y || less(y, x)) && // at least one of the three + (forall x, y :: less(x, y) && less(y, x) ==> false) && // not both of the less's + (forall x, y :: less(x, y) ==> x != y) // not a less and the equality + } + + predicate Transitive(R: (T, T) -> CompResult) + { + forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) + } } \ No newline at end of file diff --git a/src/Helpers.dfy b/src/Helpers.dfy index 7aa6cac5..46c8556a 100644 --- a/src/Helpers.dfy +++ b/src/Helpers.dfy @@ -5,31 +5,10 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "Wrappers.dfy" -include "UInt.dfy" -include "Relations.dfy" - module Helpers { export provides Comparison - import opened Comparison - import opened U = UInt - import Relations - import opened Wrappers - - - /* - * Here is an example relation and a lemma that says the relation is appropriate for use in - * lexicographic orderings. - */ - - lemma UInt8LessIsTrichotomousTransitive() - ensures Relations.Trichotomous(UInt8Less) - ensures Relations.Transitive(UInt8Less) - { - } - } module Helpers.Comparison { diff --git a/src/LexicographicHelpers.dfy b/src/LexicographicHelpers.dfy index d9ea739c..6c0d0abc 100644 --- a/src/LexicographicHelpers.dfy +++ b/src/LexicographicHelpers.dfy @@ -7,27 +7,50 @@ include "Relations.dfy" include "Lexicographics.dfy" +include "UInt.dfy" module LexicographicHelpers{ export - provides UInt + provides LexIsReflexive, LexIsAntisymmetric, LexIsTransitive, LexIsTotal, UInt8LessIsTrichotomousTransitive + provides ThereIsAMinimum, MinimumIsUnique, FindMinimum + provides SetToOrderedSequence, IsMinimum + provides UInt, Relations, Lexicographics + provides LessOrEqual, LessOrEqualAux import opened Relations import opened Lexicographics + import U = UInt import opened Lexicographics.UInt + predicate method LessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { + exists k :: 0 <= k <= |a| && LessOrEqualAux(a, b, less, k) + } + + predicate method LessOrEqualAux(a: seq, b: seq, less: (T, T) -> bool, lengthOfCommonPrefix: nat) + requires 0 <= lengthOfCommonPrefix <= |a| + { + lengthOfCommonPrefix <= |b| + && (forall i :: 0 <= i < lengthOfCommonPrefix ==> a[i] == b[i]) + && (lengthOfCommonPrefix == |a| || (lengthOfCommonPrefix < |b| && less(a[lengthOfCommonPrefix], b[lengthOfCommonPrefix]))) + } + + /* + * As the following lemmas show, the lexicographic ordering is reflexive, antisymmetric, transitive, and total. + * The proofs are a bit pedantic and include steps that can be automated. + */ + lemma LexIsReflexive(a: seq, less: (T, T) -> bool) - ensures LessOrEqual(a, a, less) + ensures LessOrEqual(a, a, less) { - assert LessOrEqualAux(a, a, less, |a|); + assert LessOrEqualAux(a, a, less, |a|); } - lemma LexIsAntisymmetric(a: seq, b: seq, less: (T, T) -> bool) - requires Trich: Trichotomous(less) - requires LessOrEqual(a, b, less) - requires LessOrEqual(b, a, less) - ensures a == b - { + lemma LexIsAntisymmetric(a: seq, b: seq, less: (T, T) -> bool) + requires Trich: Trichotomous(less) + requires LessOrEqual(a, b, less) + requires LessOrEqual(b, a, less) + ensures a == b + { assert LessIrreflexive: forall x,y :: less(x, y) ==> x != y by { reveal Trich; } @@ -206,4 +229,15 @@ module LexicographicHelpers{ } } } + + /* + * Here is an example relation and a lemma that says the relation is appropriate for use in + * lexicographic orderings. + */ + + lemma UInt8LessIsTrichotomousTransitive() + ensures Relations.Trichotomous(UInt8Less) + ensures Relations.Transitive(UInt8Less) + { + } } \ No newline at end of file diff --git a/src/Lexicographics.dfy b/src/Lexicographics.dfy index 9e5e0b24..efce4320 100644 --- a/src/Lexicographics.dfy +++ b/src/Lexicographics.dfy @@ -11,12 +11,12 @@ include "UInt.dfy" module Lexicographics { export reveals ByteSeqBelow, ByteSeqBelowAux - provides LessOrEqual, LessOrEqualAux provides Relations, UInt import opened Relations import opened UInt = Helpers.UInt + // reflexivelexicographical comparison of byte sequences predicate method ByteSeqBelow(x: seq, y: seq) { @@ -109,16 +109,6 @@ module Lexicographics { * -- `a[k]` is strictly less (using `less`) than `b[k]` */ - predicate method LessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { - exists k :: 0 <= k <= |a| && LessOrEqualAux(a, b, less, k) - } - - predicate method LessOrEqualAux(a: seq, b: seq, less: (T, T) -> bool, lengthOfCommonPrefix: nat) - requires 0 <= lengthOfCommonPrefix <= |a| - { - lengthOfCommonPrefix <= |b| - && (forall i :: 0 <= i < lengthOfCommonPrefix ==> a[i] == b[i]) - && (lengthOfCommonPrefix == |a| || (lengthOfCommonPrefix < |b| && less(a[lengthOfCommonPrefix], b[lengthOfCommonPrefix]))) - } + } \ No newline at end of file From 33a43a5a6d56357a9935bb2d1ce542fa481cc173 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Thu, 8 Sep 2022 19:45:06 -0400 Subject: [PATCH 13/32] more changes , updating local changes. --- src/BoundedInts.dfy | 343 ++++++++++++++++++++++++++++++ src/Collections/Sequences/Seq.dfy | 120 +++++------ src/CompariosRelations.dfy | 44 ---- src/Helpers.dfy | 16 -- src/Lexicographics.dfy | 22 +- src/Relations/Comparison.dfy | 126 +++++++++++ src/{ => Relations}/Relations.dfy | 0 src/UInt.dfy | 335 ----------------------------- 8 files changed, 530 insertions(+), 476 deletions(-) delete mode 100644 src/CompariosRelations.dfy delete mode 100644 src/Helpers.dfy create mode 100644 src/Relations/Comparison.dfy rename src/{ => Relations}/Relations.dfy (100%) delete mode 100644 src/UInt.dfy diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy index 088fe15b..10e6afff 100644 --- a/src/BoundedInts.dfy +++ b/src/BoundedInts.dfy @@ -34,5 +34,348 @@ module BoundedInts { newtype nat16 = x: int | 0 <= x < 0x8000 newtype nat32 = x: int | 0 <= x < 0x8000_0000 newtype nat64 = x: int | 0 <= x < 0x8000_0000_0000_0000 + + newtype posInt64 = x | 0 < x < 0x8000_0000_0000_0000 witness 1 + + const UINT8_MAX: uint8 := 0xFF + const UINT16_MAX: uint16 := 0xFFFF + const UINT32_MAX: uint32 := 0xFFFF_FFFF + const UINT64_MAX: uint64 := 0xFFFF_FFFF_FFFF_FFFF + + const INT8_MIN: int8 := -0x80 + const INT8_MAX: int8 := 0x7F + const INT16_MIN: int16 := -0x8000 + const INT16_MAX: int16 := 0x7FFF + const INT32_MIN: int32 := -0x8000_0000 + const INT32_MAX: int32 := 0x7FFFFFFF + const INT64_MIN: int64 := -0x8000_0000_0000_0000 + const INT64_MAX: int64 := 0x7FFFFFFF_FFFFFFFF + + const NAT8_MAX: nat8 := 0x7F + const NAT16_MAX: nat16 := 0x7FFF + const NAT32_MAX: nat32 := 0x7FFFFFFF + const NAT64_MAX: nat64 := 0x7FFFFFFF_FFFFFFFF + + const UINT16_LIMIT := 0x1_0000 + const UINT32_LIMIT := 0x1_0000_0000 + const UINT64_LIMIT := 0x1_0000_0000_0000_0000 + const INT32_MAX_LIMIT := 0x8000_0000 + const INT64_MAX_LIMIT := 0x8000_0000_0000_0000 + + type byte = uint8 + type bytes = seq + newtype opt_byte = c: int | -1 <= c < TWO_TO_THE_8 + + predicate method UInt8Less(a: uint8, b: uint8) { a < b } + + predicate method HasUint16Len(s: seq) { + |s| < UINT16_LIMIT + } + + type seq16 = s: seq | HasUint16Len(s) + type Uint8Seq16 = seq16 + + predicate method HasUint32Len(s: seq) { + |s| < UINT32_LIMIT + } + + type seq32 = s: seq | HasUint32Len(s) + type Uint8Seq32 = seq32 + + predicate method HasUint64Len(s: seq) { + |s| < UINT64_LIMIT + } + + type seq64 = s: seq | HasUint64Len(s) + type Uint8Seq64 = seq64 + + function method UInt16ToSeq(x: uint16): (ret: seq) + ensures |ret| == 2 + ensures 0x100 * ret[0] as uint16 + ret[1] as uint16 == x + { + var b0 := (x / 0x100) as uint8; + var b1 := (x % 0x100) as uint8; + [b0, b1] + } + + function method SeqToUInt16(s: seq): (x: uint16) + requires |s| == 2 + ensures UInt16ToSeq(x) == s + ensures x >= 0 + { + var x0 := s[0] as uint16 * 0x100; + x0 + s[1] as uint16 + } + + lemma UInt16SeqSerializeDeserialize(x: uint16) + ensures SeqToUInt16(UInt16ToSeq(x)) == x + {} + + lemma UInt16SeqDeserializeSerialize(s: seq) + requires |s| == 2 + ensures UInt16ToSeq(SeqToUInt16(s)) == s + {} + + function method UInt32ToSeq(x: uint32): (ret: seq) + ensures |ret| == 4 + ensures 0x100_0000 * ret[0] as uint32 + 0x1_0000 * ret[1] as uint32 + 0x100 * ret[2] as uint32 + ret[3] as uint32 == x + { + var b0 := (x / 0x100_0000) as uint8; + var x0 := x - (b0 as uint32 * 0x100_0000); + + var b1 := (x0 / 0x1_0000) as uint8; + var x1 := x0 - (b1 as uint32 * 0x1_0000); + + var b2 := (x1 / 0x100) as uint8; + var b3 := (x1 % 0x100) as uint8; + [b0, b1, b2, b3] + } + + function method SeqToUInt32(s: seq): (x: uint32) + requires |s| == 4 + ensures UInt32ToSeq(x) == s + { + var x0 := s[0] as uint32 * 0x100_0000; + var x1 := x0 + s[1] as uint32 * 0x1_0000; + var x2 := x1 + s[2] as uint32 * 0x100; + x2 + s[3] as uint32 + } + + lemma UInt32SeqSerializeDeserialize(x: uint32) + ensures SeqToUInt32(UInt32ToSeq(x)) == x + {} + + lemma UInt32SeqDeserializeSerialize(s: seq) + requires |s| == 4 + ensures UInt32ToSeq(SeqToUInt32(s)) == s + {} + + function method UInt64ToSeq(x: uint64): (ret: seq) + ensures |ret| == 8 + ensures 0x100_0000_0000_0000 * ret[0] as uint64 + 0x1_0000_0000_0000 * ret[1] as uint64 + + 0x100_0000_0000 * ret[2] as uint64 + 0x1_0000_0000 * ret[3] as uint64 + 0x100_0000 * ret[4] as uint64 + + 0x1_0000 * ret[5] as uint64 + 0x100 * ret[6] as uint64 + ret[7] as uint64 == x + { + var b0 := (x / 0x100_0000_0000_0000) as uint8; + var x0 := x - (b0 as uint64 * 0x100_0000_0000_0000); + + var b1 := (x0 / 0x1_0000_0000_0000) as uint8; + var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); + + var b2 := (x1 / 0x100_0000_0000) as uint8; + var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); + + var b3 := (x2 / 0x1_0000_0000) as uint8; + var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); + + var b4 := (x3 / 0x100_0000) as uint8; + var x4 := x3 - (b4 as uint64 * 0x100_0000); + + var b5 := (x4 / 0x1_0000) as uint8; + var x5 := x4 - (b5 as uint64 * 0x1_0000); + + var b6 := (x5 / 0x100) as uint8; + var b7 := (x5 % 0x100) as uint8; + [b0, b1, b2, b3, b4, b5, b6, b7] + } + + function method SeqToUInt64(s: seq): (x: uint64) + requires |s| == 8 + ensures UInt64ToSeq(x) == s + { + var x0 := s[0] as uint64 * 0x100_0000_0000_0000; + var x1 := x0 + s[1] as uint64 * 0x1_0000_0000_0000; + var x2 := x1 + s[2] as uint64 * 0x100_0000_0000; + var x3 := x2 + s[3] as uint64 * 0x1_0000_0000; + var x4 := x3 + s[4] as uint64 * 0x100_0000; + var x5 := x4 + s[5] as uint64 * 0x1_0000; + var x6 := x5 + s[6] as uint64 * 0x100; + var x := x6 + s[7] as uint64; + UInt64SeqSerialize(x, s); + x + } + + lemma UInt64SeqSerialize(x: uint64, s: seq) + requires |s| == 8 + requires 0x100_0000_0000_0000 * s[0] as uint64 + + 0x1_0000_0000_0000 * s[1] as uint64 + + 0x100_0000_0000 * s[2] as uint64 + + 0x1_0000_0000 * s[3] as uint64 + + 0x100_0000 * s[4] as uint64 + + 0x1_0000 * s[5] as uint64 + + 0x100 * s[6] as uint64 + + s[7] as uint64 == x + ensures UInt64ToSeq(x) == s + { + calc { + UInt64ToSeq(x); + == + UInt64ToSeq(s[0] as uint64 * 0x100_0000_0000_0000 + + s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + == + var b0 := ((s[0] as uint64 * 0x100_0000_0000_0000 + + s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64) / 0x100_0000_0000_0000) as uint8; + assert b0 == s[0]; + var x0 := (s[0] as uint64 * 0x100_0000_0000_0000 + + s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64) - (b0 as uint64 * 0x100_0000_0000_0000); + assert x0 == (s[1] as uint64 * 0x1_0000_0000_0000 + + s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b1 := (x0 / 0x1_0000_0000_0000) as uint8; + assert b1 == s[1]; + var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); + assert x1 == (s[2] as uint64 * 0x100_0000_0000 + + s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b2 := (x1 / 0x100_0000_0000) as uint8; + assert b2 == s[2]; + var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); + assert x2 == (s[3] as uint64 * 0x1_0000_0000 + + s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b3 := (x2 / 0x1_0000_0000) as uint8; + assert b3 == s[3]; + var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); + assert x3 == (s[4] as uint64 * 0x100_0000 + + s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b4 := (x3 / 0x100_0000) as uint8; + assert b4 == s[4]; + var x4 := x3 - (b4 as uint64 * 0x100_0000); + assert x4 == (s[5] as uint64 * 0x1_0000 + + s[6] as uint64 * 0x100 + + s[7] as uint64); + + var b5 := (x4 / 0x1_0000) as uint8; + assert b5 == s[5]; + var x5 := x4 - (b5 as uint64 * 0x1_0000); + assert x5 == (s[6] as uint64 * 0x100 + s[7] as uint64); + + var b6 := (x5 / 0x100) as uint8; + assert b6 == s[6]; + var b7 := (x5 % 0x100) as uint8; + assert b7 == s[7]; + [b0, b1, b2, b3, b4, b5, b6, b7]; + == + [s[0], s[1], s[2], s[3], s[4], s[5], s[6], s[7]]; + == + s; + } + } + + lemma UInt64SeqSerializeDeserialize(x: uint64) + ensures SeqToUInt64(UInt64ToSeq(x)) == x + {} + + lemma UInt64SeqDeserializeSerialize(s: seq) + requires |s| == 8 + ensures UInt64ToSeq(SeqToUInt64(s)) == s + {} + + function SeqToNat(s: seq): nat { + if s == [] then + 0 + else + var finalIndex := |s| - 1; + SeqToNat(s[..finalIndex]) * 0x100 + s[finalIndex] as nat + } + + // By the following lemma, prepending a 0 to a byte sequence does not change its SeqToNat value + lemma SeqToNatZeroPrefix(s: seq) + ensures SeqToNat(s) == SeqToNat([0] + s) + { + if s == [] { + } else { + var s' := [0] + s; + var sLength := |s|; + var sFinalIndex := sLength - 1; + calc { + SeqToNat(s); + == + SeqToNat(s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; + == + SeqToNat([0] + s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; + == { assert (s'[..sLength] == [0] + s[..sFinalIndex]) && s'[sLength] == s[sFinalIndex]; } + SeqToNat(s'[..sLength]) * 0x100 + s'[sLength] as nat; + == + SeqToNat(s'); + == + SeqToNat([0] + s); + } + } + } + + // By the following lemma, SeqToNat(s) == n is automatically true if the given preconditions are true + lemma SeqWithUInt32Suffix(s: seq, n: nat) + requires n < UINT32_LIMIT + requires 4 <= |s| + requires var suffixStartIndex := |s| - 4; + (s[suffixStartIndex..] == UInt32ToSeq(n as uint32)) && + (forall i :: 0 <= i < suffixStartIndex ==> s[i] == 0) + ensures SeqToNat(s) == n + { + if |s| == 4 { + calc { + SeqToNat(s); + == + SeqToNat(s[..3]) + * 0x100 + s[3] as nat; + == { assert s[..3][..2] == s[..2] && s[..3][2] == s[2]; } + (SeqToNat(s[..2]) + * 0x100 + s[2] as nat) + * 0x100 + s[3] as nat; + == { assert s[..2][..1] == s[..1] && s[..2][1] == s[1]; } + ((SeqToNat(s[..1]) + * 0x100 + s[1] as nat) + * 0x100 + s[2] as nat) + * 0x100 + s[3] as nat; + == { assert s[..1][..0] == s[..0] && s[..1][0] == s[0]; } + (((SeqToNat(s[..0]) + * 0x100 + s[0] as nat) + * 0x100 + s[1] as nat) + * 0x100 + s[2] as nat) + * 0x100 + s[3] as nat; + == + n; + } + } else { + assert s == [0] + s[1..]; + SeqToNatZeroPrefix(s[1..]); + SeqWithUInt32Suffix(s[1..], n); + } + } + } diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 9d6fc1f0..4d84b253 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -15,21 +15,20 @@ include "../../Math.dfy" include "../../Wrappers.dfy" -include "../../Helpers.dfy" include "../../UInt.dfy" -include "../../Relations.dfy" +include "../../Relations/Relations.dfy" module Seq { export - provides SortedBy, MergeSortBy, MergeSortedWith - provides Helpers, Relations + // provides SortedBy, MergeSortBy, MergeSortedWith + provides Relations//, Comparison import opened Wrappers import Math - import Helpers - import opened Helpers.Comparison import opened Relations + // import opened comparison + /********************************************************** * @@ -875,70 +874,69 @@ module Seq { else FindIndex(s, f, i + 1) } - /********************************************************** - * - * Sorting of Sequences - * - ***********************************************************/ + // /********************************************************** + // * + // * Sorting of Sequences + // * + // ***********************************************************/ - predicate method SortedBy(a: seq,compare: (T, T) -> Comparison.CompResult) - { - forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]).LessThan? - } + // predicate method SortedBy(a: seq,compare: (T, T) -> CompResult) + // { + // forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]).LessThan? + // } - lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> Comparison.CompResult) - requires SortedBy(s, compare) - requires |s| == 0 || compare(x,s[0]).LessThan? - {} + // lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> CompResult) + // requires SortedBy(s, compare) + // requires |s| == 0 || compare(x,s[0]).LessThan? + // {} - //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedBy` - function method MergeSortBy(a: seq, compare: (T, T) -> Comparison.CompResult): (result :seq) - requires Relations.Transitive(compare) - requires Connected(compare) - ensures multiset(a) == multiset(result) - ensures SortedBy(result,compare) + // //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedBy` + // function method MergeSortBy(a: seq, compare: (T, T) -> CompResult): (result :seq) + // requires Total?(compare) + // requires Connected(compare) + // ensures multiset(a) == multiset(result) + // ensures SortedBy(result,compare) - { - if |a| <= 1 then - a - else - var splitIndex := |a| / 2; - var left, right := a[..splitIndex], a[splitIndex..]; + // { + // if |a| <= 1 then + // a + // else + // var splitIndex := |a| / 2; + // var left, right := a[..splitIndex], a[splitIndex..]; - assert a == left + right; + // assert a == left + right; - var leftSorted := MergeSortBy(left, compare); - var rightSorted := MergeSortBy(right, compare); + // var leftSorted := MergeSortBy(left, compare); + // var rightSorted := MergeSortBy(right, compare); - MergeSortedWith(leftSorted, rightSorted, compare) - } - - function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, compare: (T, T) -> Comparison.CompResult) : (result :seq) - requires SortedBy(left,compare) - requires SortedBy(right,compare) - requires Relations.Transitive(compare) - requires Connected(compare) - ensures multiset(left + right) == multiset(result) - ensures SortedBy(result,compare) - { - if |left| == 0 then - right - else if |right| == 0 then - left - else if compare(left[0],right[0]).LessThan? then - LemmaNewFirstElementStillSortedBy(left[0], MergeSortedWith(left[1..], right, compare), compare); - assert left == [left[0]] + left[1..]; - - [left[0]] + MergeSortedWith(left[1..], right, compare) + // MergeSortedWith(leftSorted, rightSorted, compare) + // } + + // function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, compare: (T, T) -> CompResult) : (result :seq) + // requires SortedBy(left,compare) + // requires SortedBy(right,compare) + // requires Comparison.Total?(compare) + // requires Connected(compare) + // ensures multiset(left + right) == multiset(result) + // ensures SortedBy(result,compare) + // { + // if |left| == 0 then + // right + // else if |right| == 0 then + // left + // else if compare(left[0],right[0]).LessThan? then + // LemmaNewFirstElementStillSortedBy(left[0], MergeSortedWith(left[1..], right, compare), compare); + // assert left == [left[0]] + left[1..]; + + // [left[0]] + MergeSortedWith(left[1..], right, compare) - else - LemmaNewFirstElementStillSortedBy(right[0], MergeSortedWith(left, right[1..], compare), compare); - assert right == [right[0]] + right[1..]; - - [right[0]] + MergeSortedWith(left, right[1..], compare) - } + // else + // LemmaNewFirstElementStillSortedBy(right[0], MergeSortedWith(left, right[1..], compare), compare); + // assert right == [right[0]] + right[1..]; + // [right[0]] + MergeSortedWith(left, right[1..], compare) + // } -} +} \ No newline at end of file diff --git a/src/CompariosRelations.dfy b/src/CompariosRelations.dfy deleted file mode 100644 index f4282497..00000000 --- a/src/CompariosRelations.dfy +++ /dev/null @@ -1,44 +0,0 @@ -include "Helpers.dfy" - -module Relations.ComparisonsRelation { - - export - reveals Reflexive, AntiSymmetric, Connected, TotalOrdering - import opened Helpers.Comparison - - - predicate Reflexive(R: (T, T) -> CompResult) - { - forall x :: R(x, x) - } - - predicate AntiSymmetric(R: (T, T) -> CompResult) - { - forall x, y :: R(x, y) && R(y, x) ==> x == y - } - - predicate Connected(R: (T, T) -> CompResult) - { - forall x, y :: R(x, y) || R(y, x) - } - - predicate TotalOrdering(R: (T, T) -> CompResult) - { - && Reflexive(R) - && AntiSymmetric(R) - && Transitive(R) - && Connected(R) - } - - predicate Trichotomous(less: (T, T) -> CompResult) - { - (forall x, y :: less(x, y) || x == y || less(y, x)) && // at least one of the three - (forall x, y :: less(x, y) && less(y, x) ==> false) && // not both of the less's - (forall x, y :: less(x, y) ==> x != y) // not a less and the equality - } - - predicate Transitive(R: (T, T) -> CompResult) - { - forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) - } -} \ No newline at end of file diff --git a/src/Helpers.dfy b/src/Helpers.dfy deleted file mode 100644 index 46c8556a..00000000 --- a/src/Helpers.dfy +++ /dev/null @@ -1,16 +0,0 @@ -// RUN: %dafny /compile:0 "%s" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -module Helpers { - export - provides Comparison - -} - -module Helpers.Comparison { - datatype CompResult = LessThan | Equals | GreaterThan -} \ No newline at end of file diff --git a/src/Lexicographics.dfy b/src/Lexicographics.dfy index efce4320..989b6983 100644 --- a/src/Lexicographics.dfy +++ b/src/Lexicographics.dfy @@ -5,7 +5,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "Relations.dfy" +include "Relations/Relations.dfy" include "UInt.dfy" module Lexicographics { @@ -14,7 +14,7 @@ module Lexicographics { provides Relations, UInt import opened Relations - import opened UInt = Helpers.UInt + import opened UInt // reflexivelexicographical comparison of byte sequences @@ -93,22 +93,4 @@ module Lexicographics { decreases |x| - n { } - - /* - * Lexicographic comparison of sequences. - * - * Given two sequences `a` and `b` and a strict (that is, irreflexive) - * ordering `less` on the elements of these sequences, determine whether or not - * `a` is lexicographically "less than or equal to" `b`. - * - * `a` is lexicographically "less than or equal to" `b` holds iff - * there exists a `k` such that - * - the first `k` elements of `a` and `b` are the same - * - either: - * -- `a` has length `k` (that is, `a` is a prefix of `b`) - * -- `a[k]` is strictly less (using `less`) than `b[k]` - */ - - - } \ No newline at end of file diff --git a/src/Relations/Comparison.dfy b/src/Relations/Comparison.dfy new file mode 100644 index 00000000..9e8e6097 --- /dev/null +++ b/src/Relations/Comparison.dfy @@ -0,0 +1,126 @@ +include "../Wrappers.dfy" +include "../Collections/Sequences/Seq.dfy" + +module Relations.Comparison { + export + reveals ComputeTransitivity, Comparison, CompResult, Total?, Valid?, TotalValid, UInt8LessIsTrichotomousTransitive + + provides Wrappers + + import opened Wrappers + + datatype CompResult = Lt | Eq | Gt { + function method Flip(): CompResult { + match this + case Lt => Gt + case Eq => Eq + case Gt => Lt + } + + const Le? := this != Gt + const Ge? := this != Lt + + static function method ComputeTransitivity(c0: CompResult, c1: CompResult): Option { + match (c0, c1) + case (Lt, Lt) => Some(Lt) + case (Lt, Eq) => Some(Lt) + case (Lt, Gt) => None + case (Eq, Lt) => Some(Lt) + case (Eq, Eq) => Some(Eq) + case (Eq, Gt) => Some(Gt) + case (Gt, Lt) => None + case (Gt, Eq) => Some(Gt) + case (Gt, Gt) => Some(Gt) + } + } + + datatype Comparison = Comparison(cmp: (T, T) -> CompResult) { + function method Compare(t0: T, t1: T): CompResult { + cmp(t0, t1) + } + + predicate Complete??(t0: T, t1: T) { + cmp(t0, t1) == cmp(t1, t0).Flip() + } + + predicate Antisymmetric??(t0: T, t1: T) { + cmp(t0, t1) == Eq ==> t0 == t1 + } + + predicate Transitive??(t0: T, t1: T, t2: T) { + cmp(t0, t1).Le? && cmp(t1, t2).Le? ==> cmp(t0, t2).Le? + } + + predicate Reflexive??(t0: T) { + cmp(t0, t0) == Eq + } + + lemma AlwaysReflexive(t0: T) + requires Complete??(t0, t0) + ensures Reflexive??(t0) + {} + + lemma PreciselyTransitive'(t0: T, t1: T, t2: T) + requires Complete??(t0, t1) && Complete??(t0, t2) && Complete??(t1, t2) + requires Antisymmetric??(t0, t1) && Antisymmetric??(t0, t2) && Antisymmetric??(t1, t2) + requires Transitive??(t0, t1, t2) && Transitive??(t1, t2, t0) + requires cmp(t0, t1).Le? && cmp(t1, t2).Le? + ensures CompResult.ComputeTransitivity(cmp(t0, t1), cmp(t1, t2)) == Some(cmp(t0, t2)) + {} + + lemma PreciselyTransitive(t0: T, t1: T, t2: T) + requires Reflexive??(t0) && Reflexive??(t1) && Reflexive??(t2) + requires Complete??(t0, t1) && Complete??(t0, t2) && Complete??(t1, t2) + requires Antisymmetric??(t0, t1) && Antisymmetric??(t0, t2) && Antisymmetric??(t1, t2) + requires Transitive??(t0, t1, t2) && Transitive??(t1, t2, t0) + requires Transitive??(t2, t1, t0) && Transitive??(t1, t0, t2) + ensures match CompResult.ComputeTransitivity(cmp(t0, t1), cmp(t1, t2)) + case Some(c12) => c12 == cmp(t0, t2) + case None => true + { + match (cmp(t0, t1), cmp(t1, t2)) + case (Lt, Lt) | (Lt, Eq) | (Eq, Lt) | (Eq, Eq) => + PreciselyTransitive'(t0, t1, t2); + case (Eq, Gt) | (Gt, Eq) | (Gt, Gt) => + PreciselyTransitive'(t2, t1, t0); + case (Lt, Gt) | (Gt, Lt) => + } + + predicate Complete?(ts: Seq) { + forall t0, t1 | t0 in ts && t1 in ts :: Complete??(t0, t1) + } + + predicate Antisymmetric?(ts: Seq) { + forall t0, t1 | t0 in ts && t1 in ts :: Antisymmetric??(t0, t1) + } + + predicate Transitive?(ts: Seq) { + forall t0, t1, t2 | t0 in ts && t1 in ts && t2 in ts :: Transitive??(t0, t1, t2) + } + + predicate {:opaque} Valid?(ts: Seq) { + Complete?(ts) && /* Antisymmetric?(ts) && */ Transitive?(ts) + } + + predicate {:opaque} Total?(ts: Seq) { + Complete?(ts) && Antisymmetric?(ts) && Transitive?(ts) + } + + lemma TotalValid(ts: Seq) + ensures Total?(ts) ==> Valid?(ts) + { + reveal Total?(); + reveal Valid?(); + } + } + /* + * Here is an example relation and a lemma that says the relation is appropriate for use in + * lexicographic orderings. + */ + + lemma UInt8LessIsTrichotomousTransitive() + ensures Total?(UInt8Less) + ensures Transitive(UInt8Less) + { + } +} \ No newline at end of file diff --git a/src/Relations.dfy b/src/Relations/Relations.dfy similarity index 100% rename from src/Relations.dfy rename to src/Relations/Relations.dfy diff --git a/src/UInt.dfy b/src/UInt.dfy deleted file mode 100644 index 74c2cc92..00000000 --- a/src/UInt.dfy +++ /dev/null @@ -1,335 +0,0 @@ -// RUN: %dafny /compile:0 "%s" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -module Helpers.UInt { - - newtype uint8 = x | 0 <= x < 0x100 - newtype uint16 = x | 0 <= x < 0x1_0000 - newtype uint32 = x | 0 <= x < 0x1_0000_0000 - newtype uint64 = x | 0 <= x < 0x1_0000_0000_0000_0000 - - newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000 - newtype int64 = x | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 - newtype posInt64 = x | 0 < x < 0x8000_0000_0000_0000 witness 1 - - const UINT16_LIMIT := 0x1_0000 - const UINT32_LIMIT := 0x1_0000_0000 - const UINT64_LIMIT := 0x1_0000_0000_0000_0000 - const INT32_MAX_LIMIT := 0x8000_0000 - const INT64_MAX_LIMIT := 0x8000_0000_0000_0000 - - predicate method UInt8Less(a: uint8, b: uint8) { a < b } - - predicate method HasUint16Len(s: seq) { - |s| < UINT16_LIMIT - } - - type seq16 = s: seq | HasUint16Len(s) - type Uint8Seq16 = seq16 - - predicate method HasUint32Len(s: seq) { - |s| < UINT32_LIMIT - } - - type seq32 = s: seq | HasUint32Len(s) - type Uint8Seq32 = seq32 - - predicate method HasUint64Len(s: seq) { - |s| < UINT64_LIMIT - } - - type seq64 = s: seq | HasUint64Len(s) - type Uint8Seq64 = seq64 - - function method UInt16ToSeq(x: uint16): (ret: seq) - ensures |ret| == 2 - ensures 0x100 * ret[0] as uint16 + ret[1] as uint16 == x - { - var b0 := (x / 0x100) as uint8; - var b1 := (x % 0x100) as uint8; - [b0, b1] - } - - function method SeqToUInt16(s: seq): (x: uint16) - requires |s| == 2 - ensures UInt16ToSeq(x) == s - ensures x >= 0 - { - var x0 := s[0] as uint16 * 0x100; - x0 + s[1] as uint16 - } - - lemma UInt16SeqSerializeDeserialize(x: uint16) - ensures SeqToUInt16(UInt16ToSeq(x)) == x - {} - - lemma UInt16SeqDeserializeSerialize(s: seq) - requires |s| == 2 - ensures UInt16ToSeq(SeqToUInt16(s)) == s - {} - - function method UInt32ToSeq(x: uint32): (ret: seq) - ensures |ret| == 4 - ensures 0x100_0000 * ret[0] as uint32 + 0x1_0000 * ret[1] as uint32 + 0x100 * ret[2] as uint32 + ret[3] as uint32 == x - { - var b0 := (x / 0x100_0000) as uint8; - var x0 := x - (b0 as uint32 * 0x100_0000); - - var b1 := (x0 / 0x1_0000) as uint8; - var x1 := x0 - (b1 as uint32 * 0x1_0000); - - var b2 := (x1 / 0x100) as uint8; - var b3 := (x1 % 0x100) as uint8; - [b0, b1, b2, b3] - } - - function method SeqToUInt32(s: seq): (x: uint32) - requires |s| == 4 - ensures UInt32ToSeq(x) == s - { - var x0 := s[0] as uint32 * 0x100_0000; - var x1 := x0 + s[1] as uint32 * 0x1_0000; - var x2 := x1 + s[2] as uint32 * 0x100; - x2 + s[3] as uint32 - } - - lemma UInt32SeqSerializeDeserialize(x: uint32) - ensures SeqToUInt32(UInt32ToSeq(x)) == x - {} - - lemma UInt32SeqDeserializeSerialize(s: seq) - requires |s| == 4 - ensures UInt32ToSeq(SeqToUInt32(s)) == s - {} - - function method UInt64ToSeq(x: uint64): (ret: seq) - ensures |ret| == 8 - ensures 0x100_0000_0000_0000 * ret[0] as uint64 + 0x1_0000_0000_0000 * ret[1] as uint64 + - 0x100_0000_0000 * ret[2] as uint64 + 0x1_0000_0000 * ret[3] as uint64 + 0x100_0000 * ret[4] as uint64 + - 0x1_0000 * ret[5] as uint64 + 0x100 * ret[6] as uint64 + ret[7] as uint64 == x - { - var b0 := (x / 0x100_0000_0000_0000) as uint8; - var x0 := x - (b0 as uint64 * 0x100_0000_0000_0000); - - var b1 := (x0 / 0x1_0000_0000_0000) as uint8; - var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); - - var b2 := (x1 / 0x100_0000_0000) as uint8; - var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); - - var b3 := (x2 / 0x1_0000_0000) as uint8; - var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); - - var b4 := (x3 / 0x100_0000) as uint8; - var x4 := x3 - (b4 as uint64 * 0x100_0000); - - var b5 := (x4 / 0x1_0000) as uint8; - var x5 := x4 - (b5 as uint64 * 0x1_0000); - - var b6 := (x5 / 0x100) as uint8; - var b7 := (x5 % 0x100) as uint8; - [b0, b1, b2, b3, b4, b5, b6, b7] - } - - function method SeqToUInt64(s: seq): (x: uint64) - requires |s| == 8 - ensures UInt64ToSeq(x) == s - { - var x0 := s[0] as uint64 * 0x100_0000_0000_0000; - var x1 := x0 + s[1] as uint64 * 0x1_0000_0000_0000; - var x2 := x1 + s[2] as uint64 * 0x100_0000_0000; - var x3 := x2 + s[3] as uint64 * 0x1_0000_0000; - var x4 := x3 + s[4] as uint64 * 0x100_0000; - var x5 := x4 + s[5] as uint64 * 0x1_0000; - var x6 := x5 + s[6] as uint64 * 0x100; - var x := x6 + s[7] as uint64; - UInt64SeqSerialize(x, s); - x - } - - lemma UInt64SeqSerialize(x: uint64, s: seq) - requires |s| == 8 - requires 0x100_0000_0000_0000 * s[0] as uint64 - + 0x1_0000_0000_0000 * s[1] as uint64 - + 0x100_0000_0000 * s[2] as uint64 - + 0x1_0000_0000 * s[3] as uint64 - + 0x100_0000 * s[4] as uint64 - + 0x1_0000 * s[5] as uint64 - + 0x100 * s[6] as uint64 - + s[7] as uint64 == x - ensures UInt64ToSeq(x) == s - { - calc { - UInt64ToSeq(x); - == - UInt64ToSeq(s[0] as uint64 * 0x100_0000_0000_0000 - + s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - == - var b0 := ((s[0] as uint64 * 0x100_0000_0000_0000 - + s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64) / 0x100_0000_0000_0000) as uint8; - assert b0 == s[0]; - var x0 := (s[0] as uint64 * 0x100_0000_0000_0000 - + s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64) - (b0 as uint64 * 0x100_0000_0000_0000); - assert x0 == (s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b1 := (x0 / 0x1_0000_0000_0000) as uint8; - assert b1 == s[1]; - var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); - assert x1 == (s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b2 := (x1 / 0x100_0000_0000) as uint8; - assert b2 == s[2]; - var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); - assert x2 == (s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b3 := (x2 / 0x1_0000_0000) as uint8; - assert b3 == s[3]; - var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); - assert x3 == (s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b4 := (x3 / 0x100_0000) as uint8; - assert b4 == s[4]; - var x4 := x3 - (b4 as uint64 * 0x100_0000); - assert x4 == (s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b5 := (x4 / 0x1_0000) as uint8; - assert b5 == s[5]; - var x5 := x4 - (b5 as uint64 * 0x1_0000); - assert x5 == (s[6] as uint64 * 0x100 + s[7] as uint64); - - var b6 := (x5 / 0x100) as uint8; - assert b6 == s[6]; - var b7 := (x5 % 0x100) as uint8; - assert b7 == s[7]; - [b0, b1, b2, b3, b4, b5, b6, b7]; - == - [s[0], s[1], s[2], s[3], s[4], s[5], s[6], s[7]]; - == - s; - } - } - - lemma UInt64SeqSerializeDeserialize(x: uint64) - ensures SeqToUInt64(UInt64ToSeq(x)) == x - {} - - lemma UInt64SeqDeserializeSerialize(s: seq) - requires |s| == 8 - ensures UInt64ToSeq(SeqToUInt64(s)) == s - {} - - function SeqToNat(s: seq): nat { - if s == [] then - 0 - else - var finalIndex := |s| - 1; - SeqToNat(s[..finalIndex]) * 0x100 + s[finalIndex] as nat - } - - // By the following lemma, prepending a 0 to a byte sequence does not change its SeqToNat value - lemma SeqToNatZeroPrefix(s: seq) - ensures SeqToNat(s) == SeqToNat([0] + s) - { - if s == [] { - } else { - var s' := [0] + s; - var sLength := |s|; - var sFinalIndex := sLength - 1; - calc { - SeqToNat(s); - == - SeqToNat(s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; - == - SeqToNat([0] + s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; - == { assert (s'[..sLength] == [0] + s[..sFinalIndex]) && s'[sLength] == s[sFinalIndex]; } - SeqToNat(s'[..sLength]) * 0x100 + s'[sLength] as nat; - == - SeqToNat(s'); - == - SeqToNat([0] + s); - } - } - } - - // By the following lemma, SeqToNat(s) == n is automatically true if the given preconditions are true - lemma SeqWithUInt32Suffix(s: seq, n: nat) - requires n < UINT32_LIMIT - requires 4 <= |s| - requires var suffixStartIndex := |s| - 4; - (s[suffixStartIndex..] == UInt32ToSeq(n as uint32)) && - (forall i :: 0 <= i < suffixStartIndex ==> s[i] == 0) - ensures SeqToNat(s) == n - { - if |s| == 4 { - calc { - SeqToNat(s); - == - SeqToNat(s[..3]) - * 0x100 + s[3] as nat; - == { assert s[..3][..2] == s[..2] && s[..3][2] == s[2]; } - (SeqToNat(s[..2]) - * 0x100 + s[2] as nat) - * 0x100 + s[3] as nat; - == { assert s[..2][..1] == s[..1] && s[..2][1] == s[1]; } - ((SeqToNat(s[..1]) - * 0x100 + s[1] as nat) - * 0x100 + s[2] as nat) - * 0x100 + s[3] as nat; - == { assert s[..1][..0] == s[..0] && s[..1][0] == s[0]; } - (((SeqToNat(s[..0]) - * 0x100 + s[0] as nat) - * 0x100 + s[1] as nat) - * 0x100 + s[2] as nat) - * 0x100 + s[3] as nat; - == - n; - } - } else { - assert s == [0] + s[1..]; - SeqToNatZeroPrefix(s[1..]); - SeqWithUInt32Suffix(s[1..], n); - } - } -} \ No newline at end of file From 5c8f06f4365f257691668572a95e466cec62a2f1 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Thu, 8 Sep 2022 19:50:23 -0400 Subject: [PATCH 14/32] forgot to add before. --- src/LexicographicHelpers.dfy | 43 +++++++++++++++++++----------------- src/Relations/Comparison.dfy | 1 + 2 files changed, 24 insertions(+), 20 deletions(-) diff --git a/src/LexicographicHelpers.dfy b/src/LexicographicHelpers.dfy index 6c0d0abc..8ab4c17f 100644 --- a/src/LexicographicHelpers.dfy +++ b/src/LexicographicHelpers.dfy @@ -5,22 +5,36 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "Relations.dfy" -include "Lexicographics.dfy" -include "UInt.dfy" +include "Relations/Relations.dfy" +include "Relations/Comparison.dfy" +include "BoundedInts.dfy" -module LexicographicHelpers{ +module Lexicographics.LexicographicHelpers{ export - provides LexIsReflexive, LexIsAntisymmetric, LexIsTransitive, LexIsTotal, UInt8LessIsTrichotomousTransitive + provides LexIsReflexive, LexIsAntisymmetric, LexIsTransitive, LexIsTotal provides ThereIsAMinimum, MinimumIsUnique, FindMinimum provides SetToOrderedSequence, IsMinimum - provides UInt, Relations, Lexicographics + provides BoundedInts, Relations provides LessOrEqual, LessOrEqualAux import opened Relations - import opened Lexicographics - import U = UInt - import opened Lexicographics.UInt + import opened Comparison = Relations.Comparison + import opened BoundedInts + + /* + * Lexicographic comparison of sequences. + * + * Given two sequences `a` and `b` and a strict (that is, irreflexive) + * ordering `less` on the elements of these sequences, determine whether or not + * `a` is lexicographically "less than or equal to" `b`. + * + * `a` is lexicographically "less than or equal to" `b` holds iff + * there exists a `k` such that + * - the first `k` elements of `a` and `b` are the same + * - either: + * -- `a` has length `k` (that is, `a` is a prefix of `b`) + * -- `a[k]` is strictly less (using `less`) than `b[k]` + */ predicate method LessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { exists k :: 0 <= k <= |a| && LessOrEqualAux(a, b, less, k) @@ -229,15 +243,4 @@ module LexicographicHelpers{ } } } - - /* - * Here is an example relation and a lemma that says the relation is appropriate for use in - * lexicographic orderings. - */ - - lemma UInt8LessIsTrichotomousTransitive() - ensures Relations.Trichotomous(UInt8Less) - ensures Relations.Transitive(UInt8Less) - { - } } \ No newline at end of file diff --git a/src/Relations/Comparison.dfy b/src/Relations/Comparison.dfy index 9e8e6097..c4d7f63f 100644 --- a/src/Relations/Comparison.dfy +++ b/src/Relations/Comparison.dfy @@ -8,6 +8,7 @@ module Relations.Comparison { provides Wrappers import opened Wrappers + import opened Seq datatype CompResult = Lt | Eq | Gt { function method Flip(): CompResult { From 7da871a6ce62381ee4331b14be1ec8b87c676f5a Mon Sep 17 00:00:00 2001 From: prvshah51 <89794159+prvshah51@users.noreply.github.com> Date: Mon, 12 Sep 2022 11:40:35 -0400 Subject: [PATCH 15/32] Delete Lexicographics.dfy --- src/Lexicographics.dfy | 96 ------------------------------------------ 1 file changed, 96 deletions(-) delete mode 100644 src/Lexicographics.dfy diff --git a/src/Lexicographics.dfy b/src/Lexicographics.dfy deleted file mode 100644 index 989b6983..00000000 --- a/src/Lexicographics.dfy +++ /dev/null @@ -1,96 +0,0 @@ -// RUN: %dafny /compile:0 "%s" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -include "Relations/Relations.dfy" -include "UInt.dfy" - -module Lexicographics { - export - reveals ByteSeqBelow, ByteSeqBelowAux - provides Relations, UInt - - import opened Relations - import opened UInt - - - // reflexivelexicographical comparison of byte sequences - predicate method ByteSeqBelow(x: seq, y: seq) - { - ByteSeqBelowAux(x, y, 0) - } - - predicate method ByteSeqBelowAux(x: seq, y: seq, n: nat) - requires n <= |x| && n <= |y| - decreases |x| - n - { - || n == |x| - || (n != |y| && x[n] < y[n]) - || (n != |y| && x[n] == y[n] && ByteSeqBelowAux(x, y, n + 1)) - } - - lemma AboutByteSeqBelow() - ensures TotalOrdering(ByteSeqBelow) - { - assert Reflexive(ByteSeqBelow) by { - forall x, n | 0 <= n <= |x| { - AboutByteSeqBelowAux_Reflexive(x, n); - } - } - assert AntiSymmetric(ByteSeqBelow) by { - forall x, y, n: nat | - n <= |x| && n <= |y| && x[..n] == y[..n] && - ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, x, n) - { - AboutByteSeqBelowAux_AntiSymmetric(x, y, n); - } - } - assert Relations.Transitive(ByteSeqBelow) by { - forall x, y, z, n: nat | - n <= |x| && n <= |y| && n <= |z| && - ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, z, n) - { - AboutByteSeqBelowAux_Transitive(x, y, z, n); - } - } - assert Connected(ByteSeqBelow) by { - forall x, y, n: nat | n <= |x| && n <= |y| { - AboutByteSeqBelowAux_Connected(x, y, n); - } - } - } - - lemma AboutByteSeqBelowAux_Reflexive(x: seq, n: nat) - requires n <= |x| - ensures ByteSeqBelowAux(x, x, n) - decreases |x| - n - { - } - - lemma AboutByteSeqBelowAux_AntiSymmetric(x: seq, y: seq, n: nat) - requires n <= |x| && n <= |y| - requires x[..n] == y[..n] - requires ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, x, n) - ensures x == y - decreases |x| - n - { - } - - lemma AboutByteSeqBelowAux_Transitive(x: seq, y: seq, z: seq, n: nat) - requires n <= |x| && n <= |y| && n <= |z| - requires ByteSeqBelowAux(x, y, n) && ByteSeqBelowAux(y, z, n) - ensures ByteSeqBelowAux(x, z, n) - decreases |x| - n - { - } - - lemma AboutByteSeqBelowAux_Connected(x: seq, y: seq, n: nat) - requires n <= |x| && n <= |y| - ensures ByteSeqBelowAux(x, y, n) || ByteSeqBelowAux(y, x, n) - decreases |x| - n - { - } -} \ No newline at end of file From 62b934646ce7ad818bdf7d016143612ff1b9c1da Mon Sep 17 00:00:00 2001 From: prvshah51 <89794159+prvshah51@users.noreply.github.com> Date: Mon, 12 Sep 2022 11:40:47 -0400 Subject: [PATCH 16/32] Delete LexicographicHelpers.dfy --- src/LexicographicHelpers.dfy | 246 ----------------------------------- 1 file changed, 246 deletions(-) delete mode 100644 src/LexicographicHelpers.dfy diff --git a/src/LexicographicHelpers.dfy b/src/LexicographicHelpers.dfy deleted file mode 100644 index 8ab4c17f..00000000 --- a/src/LexicographicHelpers.dfy +++ /dev/null @@ -1,246 +0,0 @@ -// RUN: %dafny /compile:0 "%s" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -include "Relations/Relations.dfy" -include "Relations/Comparison.dfy" -include "BoundedInts.dfy" - -module Lexicographics.LexicographicHelpers{ - export - provides LexIsReflexive, LexIsAntisymmetric, LexIsTransitive, LexIsTotal - provides ThereIsAMinimum, MinimumIsUnique, FindMinimum - provides SetToOrderedSequence, IsMinimum - provides BoundedInts, Relations - provides LessOrEqual, LessOrEqualAux - - import opened Relations - import opened Comparison = Relations.Comparison - import opened BoundedInts - - /* - * Lexicographic comparison of sequences. - * - * Given two sequences `a` and `b` and a strict (that is, irreflexive) - * ordering `less` on the elements of these sequences, determine whether or not - * `a` is lexicographically "less than or equal to" `b`. - * - * `a` is lexicographically "less than or equal to" `b` holds iff - * there exists a `k` such that - * - the first `k` elements of `a` and `b` are the same - * - either: - * -- `a` has length `k` (that is, `a` is a prefix of `b`) - * -- `a[k]` is strictly less (using `less`) than `b[k]` - */ - - predicate method LessOrEqual(a: seq, b: seq, less: (T, T) -> bool) { - exists k :: 0 <= k <= |a| && LessOrEqualAux(a, b, less, k) - } - - predicate method LessOrEqualAux(a: seq, b: seq, less: (T, T) -> bool, lengthOfCommonPrefix: nat) - requires 0 <= lengthOfCommonPrefix <= |a| - { - lengthOfCommonPrefix <= |b| - && (forall i :: 0 <= i < lengthOfCommonPrefix ==> a[i] == b[i]) - && (lengthOfCommonPrefix == |a| || (lengthOfCommonPrefix < |b| && less(a[lengthOfCommonPrefix], b[lengthOfCommonPrefix]))) - } - - /* - * As the following lemmas show, the lexicographic ordering is reflexive, antisymmetric, transitive, and total. - * The proofs are a bit pedantic and include steps that can be automated. - */ - - lemma LexIsReflexive(a: seq, less: (T, T) -> bool) - ensures LessOrEqual(a, a, less) - { - assert LessOrEqualAux(a, a, less, |a|); - } - - lemma LexIsAntisymmetric(a: seq, b: seq, less: (T, T) -> bool) - requires Trich: Trichotomous(less) - requires LessOrEqual(a, b, less) - requires LessOrEqual(b, a, less) - ensures a == b - { - assert LessIrreflexive: forall x,y :: less(x, y) ==> x != y by { - reveal Trich; - } - assert ASymmetric: forall x,y :: less(x, y) && less(y, x) ==> false by { - reveal Trich; - } - var k0 :| 0 <= k0 <= |a| && LessOrEqualAux(a, b, less, k0); - var k1 :| 0 <= k1 <= |b| && LessOrEqualAux(b, a, less, k1); - var max := if k0 < k1 then k1 else k0; - assert max <= |a| && max <= |b|; - assert SameUntilMax: forall i :: 0 <= i < max ==> a[i] == b[i]; - assert AA: k0 == |a| || (k0 < |b| && less(a[k0], b[k0])); - assert BB: k1 == |b| || (k1 < |a| && less(b[k1], a[k1])); - calc { - true; - ==> { reveal AA, BB; } - (k0 == |a| || (k0 < |b| && less(a[k0], b[k0]))) && (k1 == |b| || (k1 < |a| && less(b[k1], a[k1]))); - == // distribute && and || - (k0 == |a| && k1 == |b|) || - (k0 == |a| && k1 < |a| && less(b[k1], a[k1])) || - (k0 < |b| && less(a[k0], b[k0]) && k1 == |b|) || - (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); - == { reveal LessIrreflexive, SameUntilMax; } - (k0 == |a| && k1 == |b|) || - (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1])); - ==> { reveal LessIrreflexive, SameUntilMax; assert max <= k0 && max <= k1; } - (k0 == |a| && k1 == |b|) || - (k0 < |b| && less(a[k0], b[k0]) && k1 < |a| && less(b[k1], a[k1]) && k0 == k1 == max); - == { reveal ASymmetric; } - k0 == |a| && k1 == |b|; - ==> { assert |a| == k0 <= max && |b| == k1 <= max ==> k0 == k1; } - max == |a| == |b|; - ==> { reveal SameUntilMax; } - a == b; - } - } - - lemma LexIsTransitive(a: seq, b: seq, c: seq, less: (T, T) -> bool) - requires Transitive(less) - requires LessOrEqual(a, b, less) - requires LessOrEqual(b, c, less) - ensures LessOrEqual(a, c, less) - { - var k0 :| 0 <= k0 <= |a| && LessOrEqualAux(a, b, less, k0); - var k1 :| 0 <= k1 <= |b| && LessOrEqualAux(b, c, less, k1); - var k := if k0 < k1 then k0 else k1; - assert LessOrEqualAux(a, c, less, k); - } - - lemma LexIsTotal(a: seq, b: seq, less: (T, T) -> bool) - requires Trich: Trichotomous(less) - ensures LessOrEqual(a, b, less) || LessOrEqual(b, a, less) - { - var m := 0; - while m < |a| && m < |b| && a[m] == b[m] - invariant m <= |a| && m <= |b| - invariant forall i :: 0 <= i < m ==> a[i] == b[i] - { - m := m + 1; - } - // m is the length of the common prefix of a and b - if m == |a| == |b| { - assert a == b; - LexIsReflexive(a, less); - } else if m == |a| < |b| { - assert LessOrEqualAux(a, b, less, m); - } else if m == |b| < |a| { - assert LessOrEqualAux(b, a, less, m); - } else { - assert m < |a| && m < |b|; - reveal Trich; - if - case less(a[m], b[m]) => - assert LessOrEqualAux(a, b, less, m); - case less(b[m], a[m]) => - assert LessOrEqualAux(b, a, less, m); - } - } - /* - * SetToOrderedSequence(s, less) takes a set of T-strings and returns them as a sequence, - * ordered by the lexicographic ordering whose underlying irreflexive ordering is "less". - * The function is compilable, but will not exhibit enviable performance. - */ - - function method {:tailrecursion} SetToOrderedSequence(s: set>, less: (T, T) -> bool): (q: seq>) - requires Trichotomous(less) && Transitive(less) - ensures |s| == |q| - ensures forall i :: 0 <= i < |q| ==> q[i] in s - ensures forall k :: k in s ==> k in q - ensures forall i :: 0 < i < |q| ==> LessOrEqual(q[i-1], q[i], less) - ensures forall i, j | 0 <= i < j < |q| :: q[i] != q[j]; - { - if s == {} then - [] - else - // In preparation for the assign-such-that statement below, we'll need to - // prove that a minimum exists and that it is unique. - // The following lemma shows existence: - ThereIsAMinimum(s, less); - // The following assertion shows uniqueness: - assert forall a, b :: IsMinimum(a, s, less) && IsMinimum(b, s, less) ==> a == b by { - // The proof of the assertion is the following forall statement. - // But why did we even bother to write the assert-by instead of - // just writing this forall statement in the first place? Because - // we are in an expression context and a forall statement cannot start - // an expression (because the "forall" makes the parser think that - // a forall expression is coming). - forall a, b | IsMinimum(a, s, less) && IsMinimum(b, s, less) { - // For the given a and b, the proof is settled by calling the following lemma: - MinimumIsUnique(a, b, s, less); - } - } - // The "a in s" in the following line follows from IsMinimum(a, s), so it - // is logically redundant. However, it is needed to convince the compiler - // that the assign-such-that statement is compilable. - var a :| a in s && IsMinimum(a, s, less); - [a] + SetToOrderedSequence(s - {a}, less) - } - - predicate method IsMinimum(a: seq, s: set>, less: (T, T) -> bool) { - a in s && - forall z :: z in s ==> LessOrEqual(a, z, less) - } - - lemma ThereIsAMinimum(s: set>, less: (T, T) -> bool) - requires s != {} - requires Trichotomous(less) && Transitive(less) - ensures exists a :: IsMinimum(a, s, less) - { - var a := FindMinimum(s, less); - } - - lemma MinimumIsUnique(a: seq, b: seq, s: set>, less: (T, T) -> bool) - requires IsMinimum(a, s, less) && IsMinimum(b, s, less) - requires Trichotomous(less) - ensures a == b - { - LexIsAntisymmetric(a, b, less); - } - - lemma FindMinimum(s: set>, less: (T, T) -> bool) returns (a: seq) - requires s != {} - requires Trichotomous(less) && Transitive(less) - ensures IsMinimum(a, s, less) - { - a :| a in s; - if s == {a} { - LexIsReflexive(a, less); - } else { - var s' := s - {a}; - assert forall x :: x in s <==> x == a || x in s'; - var a' := FindMinimum(s', less); - if LessOrEqual(a', a, less) { - a := a'; - } else { - assert LessOrEqual(a, a', less) by { - LexIsTotal(a, a', less); - } - forall z | z in s - ensures LessOrEqual(a, z, less) - { - if z == a { - LexIsReflexive(a, less); - } else { - calc { - true; - == // z in s && z != a - z in s'; - ==> // by postcondition of FindMinim(s') above - LessOrEqual(a', z, less); - ==> { LexIsTransitive(a, a', z, less); } - LessOrEqual(a, z, less); - } - } - } - } - } - } -} \ No newline at end of file From e8e59196ae9652d372774443cc484b3d6178d5c4 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Mon, 12 Sep 2022 17:01:27 -0400 Subject: [PATCH 17/32] suggested changes , removed Lexicographics and LexicographicsHelper . --- examples/Unicode/Utf8EncodingFormExamples.dfy | 11 + src/BoundedInts.dfy | 343 ------------------ src/Collections/Sequences/Seq.dfy | 1 - 3 files changed, 11 insertions(+), 344 deletions(-) diff --git a/examples/Unicode/Utf8EncodingFormExamples.dfy b/examples/Unicode/Utf8EncodingFormExamples.dfy index f3ca0941..2de902af 100644 --- a/examples/Unicode/Utf8EncodingFormExamples.dfy +++ b/examples/Unicode/Utf8EncodingFormExamples.dfy @@ -40,4 +40,15 @@ module Utf8EncodingFormExamples { :: DecodeCodeUnitSequenceChecked(s).None? {} + /* + * Here is an example relation and a lemma that says the relation is appropriate for use in + * lexicographic orderings. + */ + + lemma UInt8LessIsTrichotomousTransitive() + ensures Total?(UInt8Less) + ensures Transitive(UInt8Less) + { + } + } diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy index 10e6afff..088fe15b 100644 --- a/src/BoundedInts.dfy +++ b/src/BoundedInts.dfy @@ -34,348 +34,5 @@ module BoundedInts { newtype nat16 = x: int | 0 <= x < 0x8000 newtype nat32 = x: int | 0 <= x < 0x8000_0000 newtype nat64 = x: int | 0 <= x < 0x8000_0000_0000_0000 - - newtype posInt64 = x | 0 < x < 0x8000_0000_0000_0000 witness 1 - - const UINT8_MAX: uint8 := 0xFF - const UINT16_MAX: uint16 := 0xFFFF - const UINT32_MAX: uint32 := 0xFFFF_FFFF - const UINT64_MAX: uint64 := 0xFFFF_FFFF_FFFF_FFFF - - const INT8_MIN: int8 := -0x80 - const INT8_MAX: int8 := 0x7F - const INT16_MIN: int16 := -0x8000 - const INT16_MAX: int16 := 0x7FFF - const INT32_MIN: int32 := -0x8000_0000 - const INT32_MAX: int32 := 0x7FFFFFFF - const INT64_MIN: int64 := -0x8000_0000_0000_0000 - const INT64_MAX: int64 := 0x7FFFFFFF_FFFFFFFF - - const NAT8_MAX: nat8 := 0x7F - const NAT16_MAX: nat16 := 0x7FFF - const NAT32_MAX: nat32 := 0x7FFFFFFF - const NAT64_MAX: nat64 := 0x7FFFFFFF_FFFFFFFF - - const UINT16_LIMIT := 0x1_0000 - const UINT32_LIMIT := 0x1_0000_0000 - const UINT64_LIMIT := 0x1_0000_0000_0000_0000 - const INT32_MAX_LIMIT := 0x8000_0000 - const INT64_MAX_LIMIT := 0x8000_0000_0000_0000 - - type byte = uint8 - type bytes = seq - newtype opt_byte = c: int | -1 <= c < TWO_TO_THE_8 - - predicate method UInt8Less(a: uint8, b: uint8) { a < b } - - predicate method HasUint16Len(s: seq) { - |s| < UINT16_LIMIT - } - - type seq16 = s: seq | HasUint16Len(s) - type Uint8Seq16 = seq16 - - predicate method HasUint32Len(s: seq) { - |s| < UINT32_LIMIT - } - - type seq32 = s: seq | HasUint32Len(s) - type Uint8Seq32 = seq32 - - predicate method HasUint64Len(s: seq) { - |s| < UINT64_LIMIT - } - - type seq64 = s: seq | HasUint64Len(s) - type Uint8Seq64 = seq64 - - function method UInt16ToSeq(x: uint16): (ret: seq) - ensures |ret| == 2 - ensures 0x100 * ret[0] as uint16 + ret[1] as uint16 == x - { - var b0 := (x / 0x100) as uint8; - var b1 := (x % 0x100) as uint8; - [b0, b1] - } - - function method SeqToUInt16(s: seq): (x: uint16) - requires |s| == 2 - ensures UInt16ToSeq(x) == s - ensures x >= 0 - { - var x0 := s[0] as uint16 * 0x100; - x0 + s[1] as uint16 - } - - lemma UInt16SeqSerializeDeserialize(x: uint16) - ensures SeqToUInt16(UInt16ToSeq(x)) == x - {} - - lemma UInt16SeqDeserializeSerialize(s: seq) - requires |s| == 2 - ensures UInt16ToSeq(SeqToUInt16(s)) == s - {} - - function method UInt32ToSeq(x: uint32): (ret: seq) - ensures |ret| == 4 - ensures 0x100_0000 * ret[0] as uint32 + 0x1_0000 * ret[1] as uint32 + 0x100 * ret[2] as uint32 + ret[3] as uint32 == x - { - var b0 := (x / 0x100_0000) as uint8; - var x0 := x - (b0 as uint32 * 0x100_0000); - - var b1 := (x0 / 0x1_0000) as uint8; - var x1 := x0 - (b1 as uint32 * 0x1_0000); - - var b2 := (x1 / 0x100) as uint8; - var b3 := (x1 % 0x100) as uint8; - [b0, b1, b2, b3] - } - - function method SeqToUInt32(s: seq): (x: uint32) - requires |s| == 4 - ensures UInt32ToSeq(x) == s - { - var x0 := s[0] as uint32 * 0x100_0000; - var x1 := x0 + s[1] as uint32 * 0x1_0000; - var x2 := x1 + s[2] as uint32 * 0x100; - x2 + s[3] as uint32 - } - - lemma UInt32SeqSerializeDeserialize(x: uint32) - ensures SeqToUInt32(UInt32ToSeq(x)) == x - {} - - lemma UInt32SeqDeserializeSerialize(s: seq) - requires |s| == 4 - ensures UInt32ToSeq(SeqToUInt32(s)) == s - {} - - function method UInt64ToSeq(x: uint64): (ret: seq) - ensures |ret| == 8 - ensures 0x100_0000_0000_0000 * ret[0] as uint64 + 0x1_0000_0000_0000 * ret[1] as uint64 + - 0x100_0000_0000 * ret[2] as uint64 + 0x1_0000_0000 * ret[3] as uint64 + 0x100_0000 * ret[4] as uint64 + - 0x1_0000 * ret[5] as uint64 + 0x100 * ret[6] as uint64 + ret[7] as uint64 == x - { - var b0 := (x / 0x100_0000_0000_0000) as uint8; - var x0 := x - (b0 as uint64 * 0x100_0000_0000_0000); - - var b1 := (x0 / 0x1_0000_0000_0000) as uint8; - var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); - - var b2 := (x1 / 0x100_0000_0000) as uint8; - var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); - - var b3 := (x2 / 0x1_0000_0000) as uint8; - var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); - - var b4 := (x3 / 0x100_0000) as uint8; - var x4 := x3 - (b4 as uint64 * 0x100_0000); - - var b5 := (x4 / 0x1_0000) as uint8; - var x5 := x4 - (b5 as uint64 * 0x1_0000); - - var b6 := (x5 / 0x100) as uint8; - var b7 := (x5 % 0x100) as uint8; - [b0, b1, b2, b3, b4, b5, b6, b7] - } - - function method SeqToUInt64(s: seq): (x: uint64) - requires |s| == 8 - ensures UInt64ToSeq(x) == s - { - var x0 := s[0] as uint64 * 0x100_0000_0000_0000; - var x1 := x0 + s[1] as uint64 * 0x1_0000_0000_0000; - var x2 := x1 + s[2] as uint64 * 0x100_0000_0000; - var x3 := x2 + s[3] as uint64 * 0x1_0000_0000; - var x4 := x3 + s[4] as uint64 * 0x100_0000; - var x5 := x4 + s[5] as uint64 * 0x1_0000; - var x6 := x5 + s[6] as uint64 * 0x100; - var x := x6 + s[7] as uint64; - UInt64SeqSerialize(x, s); - x - } - - lemma UInt64SeqSerialize(x: uint64, s: seq) - requires |s| == 8 - requires 0x100_0000_0000_0000 * s[0] as uint64 - + 0x1_0000_0000_0000 * s[1] as uint64 - + 0x100_0000_0000 * s[2] as uint64 - + 0x1_0000_0000 * s[3] as uint64 - + 0x100_0000 * s[4] as uint64 - + 0x1_0000 * s[5] as uint64 - + 0x100 * s[6] as uint64 - + s[7] as uint64 == x - ensures UInt64ToSeq(x) == s - { - calc { - UInt64ToSeq(x); - == - UInt64ToSeq(s[0] as uint64 * 0x100_0000_0000_0000 - + s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - == - var b0 := ((s[0] as uint64 * 0x100_0000_0000_0000 - + s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64) / 0x100_0000_0000_0000) as uint8; - assert b0 == s[0]; - var x0 := (s[0] as uint64 * 0x100_0000_0000_0000 - + s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64) - (b0 as uint64 * 0x100_0000_0000_0000); - assert x0 == (s[1] as uint64 * 0x1_0000_0000_0000 - + s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b1 := (x0 / 0x1_0000_0000_0000) as uint8; - assert b1 == s[1]; - var x1 := x0 - (b1 as uint64 * 0x1_0000_0000_0000); - assert x1 == (s[2] as uint64 * 0x100_0000_0000 - + s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b2 := (x1 / 0x100_0000_0000) as uint8; - assert b2 == s[2]; - var x2 := x1 - (b2 as uint64 * 0x100_0000_0000); - assert x2 == (s[3] as uint64 * 0x1_0000_0000 - + s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b3 := (x2 / 0x1_0000_0000) as uint8; - assert b3 == s[3]; - var x3 := x2 - (b3 as uint64 * 0x1_0000_0000); - assert x3 == (s[4] as uint64 * 0x100_0000 - + s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b4 := (x3 / 0x100_0000) as uint8; - assert b4 == s[4]; - var x4 := x3 - (b4 as uint64 * 0x100_0000); - assert x4 == (s[5] as uint64 * 0x1_0000 - + s[6] as uint64 * 0x100 - + s[7] as uint64); - - var b5 := (x4 / 0x1_0000) as uint8; - assert b5 == s[5]; - var x5 := x4 - (b5 as uint64 * 0x1_0000); - assert x5 == (s[6] as uint64 * 0x100 + s[7] as uint64); - - var b6 := (x5 / 0x100) as uint8; - assert b6 == s[6]; - var b7 := (x5 % 0x100) as uint8; - assert b7 == s[7]; - [b0, b1, b2, b3, b4, b5, b6, b7]; - == - [s[0], s[1], s[2], s[3], s[4], s[5], s[6], s[7]]; - == - s; - } - } - - lemma UInt64SeqSerializeDeserialize(x: uint64) - ensures SeqToUInt64(UInt64ToSeq(x)) == x - {} - - lemma UInt64SeqDeserializeSerialize(s: seq) - requires |s| == 8 - ensures UInt64ToSeq(SeqToUInt64(s)) == s - {} - - function SeqToNat(s: seq): nat { - if s == [] then - 0 - else - var finalIndex := |s| - 1; - SeqToNat(s[..finalIndex]) * 0x100 + s[finalIndex] as nat - } - - // By the following lemma, prepending a 0 to a byte sequence does not change its SeqToNat value - lemma SeqToNatZeroPrefix(s: seq) - ensures SeqToNat(s) == SeqToNat([0] + s) - { - if s == [] { - } else { - var s' := [0] + s; - var sLength := |s|; - var sFinalIndex := sLength - 1; - calc { - SeqToNat(s); - == - SeqToNat(s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; - == - SeqToNat([0] + s[..sFinalIndex]) * 0x100 + s[sFinalIndex] as nat; - == { assert (s'[..sLength] == [0] + s[..sFinalIndex]) && s'[sLength] == s[sFinalIndex]; } - SeqToNat(s'[..sLength]) * 0x100 + s'[sLength] as nat; - == - SeqToNat(s'); - == - SeqToNat([0] + s); - } - } - } - - // By the following lemma, SeqToNat(s) == n is automatically true if the given preconditions are true - lemma SeqWithUInt32Suffix(s: seq, n: nat) - requires n < UINT32_LIMIT - requires 4 <= |s| - requires var suffixStartIndex := |s| - 4; - (s[suffixStartIndex..] == UInt32ToSeq(n as uint32)) && - (forall i :: 0 <= i < suffixStartIndex ==> s[i] == 0) - ensures SeqToNat(s) == n - { - if |s| == 4 { - calc { - SeqToNat(s); - == - SeqToNat(s[..3]) - * 0x100 + s[3] as nat; - == { assert s[..3][..2] == s[..2] && s[..3][2] == s[2]; } - (SeqToNat(s[..2]) - * 0x100 + s[2] as nat) - * 0x100 + s[3] as nat; - == { assert s[..2][..1] == s[..1] && s[..2][1] == s[1]; } - ((SeqToNat(s[..1]) - * 0x100 + s[1] as nat) - * 0x100 + s[2] as nat) - * 0x100 + s[3] as nat; - == { assert s[..1][..0] == s[..0] && s[..1][0] == s[0]; } - (((SeqToNat(s[..0]) - * 0x100 + s[0] as nat) - * 0x100 + s[1] as nat) - * 0x100 + s[2] as nat) - * 0x100 + s[3] as nat; - == - n; - } - } else { - assert s == [0] + s[1..]; - SeqToNatZeroPrefix(s[1..]); - SeqWithUInt32Suffix(s[1..], n); - } - } - } diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 4d84b253..20df90df 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -15,7 +15,6 @@ include "../../Math.dfy" include "../../Wrappers.dfy" -include "../../UInt.dfy" include "../../Relations/Relations.dfy" module Seq { From bb009fb2a0f073b2dec9dfbd176118eaf79b8674 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Mon, 12 Sep 2022 17:52:10 -0400 Subject: [PATCH 18/32] removed unnecessary exports, includes from more files. --- examples/Unicode/Utf8EncodingFormExamples.dfy | 1 + src/Collections/Sequences/Seq.dfy | 75 ------------------- src/Relations/Comparison.dfy | 39 ++++------ 3 files changed, 17 insertions(+), 98 deletions(-) diff --git a/examples/Unicode/Utf8EncodingFormExamples.dfy b/examples/Unicode/Utf8EncodingFormExamples.dfy index 2de902af..bfa1c359 100644 --- a/examples/Unicode/Utf8EncodingFormExamples.dfy +++ b/examples/Unicode/Utf8EncodingFormExamples.dfy @@ -6,6 +6,7 @@ *******************************************************************************/ include "../../src/Unicode/Utf8EncodingForm.dfy" +include "../../src/Relations/Comparison.dfy" module Utf8EncodingFormExamples { import Unicode diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 20df90df..86f69711 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -15,19 +15,10 @@ include "../../Math.dfy" include "../../Wrappers.dfy" -include "../../Relations/Relations.dfy" module Seq { - export - // provides SortedBy, MergeSortBy, MergeSortedWith - provides Relations//, Comparison - - import opened Wrappers import Math - import opened Relations - // import opened comparison - /********************************************************** * @@ -872,70 +863,4 @@ module Seq { else if f(s[i]) then Some(i) else FindIndex(s, f, i + 1) } - - // /********************************************************** - // * - // * Sorting of Sequences - // * - // ***********************************************************/ - - - // predicate method SortedBy(a: seq,compare: (T, T) -> CompResult) - // { - // forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]).LessThan? - // } - - // lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> CompResult) - // requires SortedBy(s, compare) - // requires |s| == 0 || compare(x,s[0]).LessThan? - // {} - - // //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedBy` - // function method MergeSortBy(a: seq, compare: (T, T) -> CompResult): (result :seq) - // requires Total?(compare) - // requires Connected(compare) - // ensures multiset(a) == multiset(result) - // ensures SortedBy(result,compare) - - // { - // 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, compare); - // var rightSorted := MergeSortBy(right, compare); - - // MergeSortedWith(leftSorted, rightSorted, compare) - // } - - // function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, compare: (T, T) -> CompResult) : (result :seq) - // requires SortedBy(left,compare) - // requires SortedBy(right,compare) - // requires Comparison.Total?(compare) - // requires Connected(compare) - // ensures multiset(left + right) == multiset(result) - // ensures SortedBy(result,compare) - // { - // if |left| == 0 then - // right - // else if |right| == 0 then - // left - // else if compare(left[0],right[0]).LessThan? then - // LemmaNewFirstElementStillSortedBy(left[0], MergeSortedWith(left[1..], right, compare), compare); - // assert left == [left[0]] + left[1..]; - - // [left[0]] + MergeSortedWith(left[1..], right, compare) - - - // else - // LemmaNewFirstElementStillSortedBy(right[0], MergeSortedWith(left, right[1..], compare), compare); - // assert right == [right[0]] + right[1..]; - - // [right[0]] + MergeSortedWith(left, right[1..], compare) - // } - } \ No newline at end of file diff --git a/src/Relations/Comparison.dfy b/src/Relations/Comparison.dfy index c4d7f63f..c46436fd 100644 --- a/src/Relations/Comparison.dfy +++ b/src/Relations/Comparison.dfy @@ -1,14 +1,7 @@ include "../Wrappers.dfy" -include "../Collections/Sequences/Seq.dfy" module Relations.Comparison { - export - reveals ComputeTransitivity, Comparison, CompResult, Total?, Valid?, TotalValid, UInt8LessIsTrichotomousTransitive - - provides Wrappers - import opened Wrappers - import opened Seq datatype CompResult = Lt | Eq | Gt { function method Flip(): CompResult { @@ -87,41 +80,41 @@ module Relations.Comparison { case (Lt, Gt) | (Gt, Lt) => } - predicate Complete?(ts: Seq) { + predicate Complete?(ts: seq) { forall t0, t1 | t0 in ts && t1 in ts :: Complete??(t0, t1) } - predicate Antisymmetric?(ts: Seq) { + predicate Antisymmetric?(ts: seq) { forall t0, t1 | t0 in ts && t1 in ts :: Antisymmetric??(t0, t1) } - predicate Transitive?(ts: Seq) { + predicate Transitive?(ts: seq) { forall t0, t1, t2 | t0 in ts && t1 in ts && t2 in ts :: Transitive??(t0, t1, t2) } - predicate {:opaque} Valid?(ts: Seq) { + predicate {:opaque} Valid?(ts: seq) { Complete?(ts) && /* Antisymmetric?(ts) && */ Transitive?(ts) } - predicate {:opaque} Total?(ts: Seq) { + predicate {:opaque} Total?(ts: seq) { Complete?(ts) && Antisymmetric?(ts) && Transitive?(ts) } - lemma TotalValid(ts: Seq) + lemma TotalValid(ts: seq) ensures Total?(ts) ==> Valid?(ts) { reveal Total?(); reveal Valid?(); } - } - /* - * Here is an example relation and a lemma that says the relation is appropriate for use in - * lexicographic orderings. - */ - - lemma UInt8LessIsTrichotomousTransitive() - ensures Total?(UInt8Less) - ensures Transitive(UInt8Less) - { + + predicate method SortedBy(a: seq,compare: (T, T) -> CompResult) + { + forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]).Lt? + } + + lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> CompResult) + requires SortedBy(s, compare) + requires |s| == 0 || compare(x,s[0]).Lt? + {} } } \ No newline at end of file From 6d57e5522e42e8401af7a43421a1b6fb4d396cf5 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 13 Sep 2022 10:27:38 -0700 Subject: [PATCH 19/32] Remove Comparison.dfy and revert to plain relations, general cleanup --- examples/Unicode/Utf8EncodingFormExamples.dfy | 13 -- src/Relations/Comparison.dfy | 120 ------------------ 2 files changed, 133 deletions(-) delete mode 100644 src/Relations/Comparison.dfy diff --git a/examples/Unicode/Utf8EncodingFormExamples.dfy b/examples/Unicode/Utf8EncodingFormExamples.dfy index bfa1c359..46bb72e4 100644 --- a/examples/Unicode/Utf8EncodingFormExamples.dfy +++ b/examples/Unicode/Utf8EncodingFormExamples.dfy @@ -6,7 +6,6 @@ *******************************************************************************/ include "../../src/Unicode/Utf8EncodingForm.dfy" -include "../../src/Relations/Comparison.dfy" module Utf8EncodingFormExamples { import Unicode @@ -40,16 +39,4 @@ module Utf8EncodingFormExamples { ensures forall s | s in TEST_ILL_FORMED_SEQUENCES :: DecodeCodeUnitSequenceChecked(s).None? {} - - /* - * Here is an example relation and a lemma that says the relation is appropriate for use in - * lexicographic orderings. - */ - - lemma UInt8LessIsTrichotomousTransitive() - ensures Total?(UInt8Less) - ensures Transitive(UInt8Less) - { - } - } diff --git a/src/Relations/Comparison.dfy b/src/Relations/Comparison.dfy deleted file mode 100644 index c46436fd..00000000 --- a/src/Relations/Comparison.dfy +++ /dev/null @@ -1,120 +0,0 @@ -include "../Wrappers.dfy" - -module Relations.Comparison { - import opened Wrappers - - datatype CompResult = Lt | Eq | Gt { - function method Flip(): CompResult { - match this - case Lt => Gt - case Eq => Eq - case Gt => Lt - } - - const Le? := this != Gt - const Ge? := this != Lt - - static function method ComputeTransitivity(c0: CompResult, c1: CompResult): Option { - match (c0, c1) - case (Lt, Lt) => Some(Lt) - case (Lt, Eq) => Some(Lt) - case (Lt, Gt) => None - case (Eq, Lt) => Some(Lt) - case (Eq, Eq) => Some(Eq) - case (Eq, Gt) => Some(Gt) - case (Gt, Lt) => None - case (Gt, Eq) => Some(Gt) - case (Gt, Gt) => Some(Gt) - } - } - - datatype Comparison = Comparison(cmp: (T, T) -> CompResult) { - function method Compare(t0: T, t1: T): CompResult { - cmp(t0, t1) - } - - predicate Complete??(t0: T, t1: T) { - cmp(t0, t1) == cmp(t1, t0).Flip() - } - - predicate Antisymmetric??(t0: T, t1: T) { - cmp(t0, t1) == Eq ==> t0 == t1 - } - - predicate Transitive??(t0: T, t1: T, t2: T) { - cmp(t0, t1).Le? && cmp(t1, t2).Le? ==> cmp(t0, t2).Le? - } - - predicate Reflexive??(t0: T) { - cmp(t0, t0) == Eq - } - - lemma AlwaysReflexive(t0: T) - requires Complete??(t0, t0) - ensures Reflexive??(t0) - {} - - lemma PreciselyTransitive'(t0: T, t1: T, t2: T) - requires Complete??(t0, t1) && Complete??(t0, t2) && Complete??(t1, t2) - requires Antisymmetric??(t0, t1) && Antisymmetric??(t0, t2) && Antisymmetric??(t1, t2) - requires Transitive??(t0, t1, t2) && Transitive??(t1, t2, t0) - requires cmp(t0, t1).Le? && cmp(t1, t2).Le? - ensures CompResult.ComputeTransitivity(cmp(t0, t1), cmp(t1, t2)) == Some(cmp(t0, t2)) - {} - - lemma PreciselyTransitive(t0: T, t1: T, t2: T) - requires Reflexive??(t0) && Reflexive??(t1) && Reflexive??(t2) - requires Complete??(t0, t1) && Complete??(t0, t2) && Complete??(t1, t2) - requires Antisymmetric??(t0, t1) && Antisymmetric??(t0, t2) && Antisymmetric??(t1, t2) - requires Transitive??(t0, t1, t2) && Transitive??(t1, t2, t0) - requires Transitive??(t2, t1, t0) && Transitive??(t1, t0, t2) - ensures match CompResult.ComputeTransitivity(cmp(t0, t1), cmp(t1, t2)) - case Some(c12) => c12 == cmp(t0, t2) - case None => true - { - match (cmp(t0, t1), cmp(t1, t2)) - case (Lt, Lt) | (Lt, Eq) | (Eq, Lt) | (Eq, Eq) => - PreciselyTransitive'(t0, t1, t2); - case (Eq, Gt) | (Gt, Eq) | (Gt, Gt) => - PreciselyTransitive'(t2, t1, t0); - case (Lt, Gt) | (Gt, Lt) => - } - - predicate Complete?(ts: seq) { - forall t0, t1 | t0 in ts && t1 in ts :: Complete??(t0, t1) - } - - predicate Antisymmetric?(ts: seq) { - forall t0, t1 | t0 in ts && t1 in ts :: Antisymmetric??(t0, t1) - } - - predicate Transitive?(ts: seq) { - forall t0, t1, t2 | t0 in ts && t1 in ts && t2 in ts :: Transitive??(t0, t1, t2) - } - - predicate {:opaque} Valid?(ts: seq) { - Complete?(ts) && /* Antisymmetric?(ts) && */ Transitive?(ts) - } - - predicate {:opaque} Total?(ts: seq) { - Complete?(ts) && Antisymmetric?(ts) && Transitive?(ts) - } - - lemma TotalValid(ts: seq) - ensures Total?(ts) ==> Valid?(ts) - { - reveal Total?(); - reveal Valid?(); - } - - predicate method SortedBy(a: seq,compare: (T, T) -> CompResult) - { - forall i, j | 0 <= i < j < |a| :: compare(a[i],a[j]).Lt? - } - - lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, compare: (T, T) -> CompResult) - requires SortedBy(s, compare) - requires |s| == 0 || compare(x,s[0]).Lt? - {} - } -} \ No newline at end of file From 9038f2ab568ce264966369ab56c20d427a8bed93 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 13 Sep 2022 10:39:33 -0700 Subject: [PATCH 20/32] Move Relations.dfy to src (ala Functions.dfy) --- src/{Relations => }/Relations.dfy | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/{Relations => }/Relations.dfy (100%) diff --git a/src/Relations/Relations.dfy b/src/Relations.dfy similarity index 100% rename from src/Relations/Relations.dfy rename to src/Relations.dfy From a2ededeb3f74b2c0007cb23469ed942eac73ce48 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 13 Sep 2022 13:15:44 -0700 Subject: [PATCH 21/32] Making example verification cheaper, fixing Wrappers.dfy lit test --- examples/Collections/Arrays/BinarySearch.dfy.expect | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 examples/Collections/Arrays/BinarySearch.dfy.expect diff --git a/examples/Collections/Arrays/BinarySearch.dfy.expect b/examples/Collections/Arrays/BinarySearch.dfy.expect new file mode 100644 index 00000000..b48f86fa --- /dev/null +++ b/examples/Collections/Arrays/BinarySearch.dfy.expect @@ -0,0 +1,4 @@ + +Dafny program verifier finished with 2 verified, 0 errors +[-6, 0, 1, 3, 7, 7, 9] +3 From 1df340fd83dd26f9095655a5fc4ac4575a119c19 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 13 Sep 2022 14:16:38 -0700 Subject: [PATCH 22/32] Use OutputCheck instead of *.expect files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The latter doesn’t work well in CI here because the /verificationLogger options cause extra, unpredictable output lines --- examples/Collections/Arrays/BinarySearch.dfy.expect | 4 ---- 1 file changed, 4 deletions(-) delete mode 100644 examples/Collections/Arrays/BinarySearch.dfy.expect diff --git a/examples/Collections/Arrays/BinarySearch.dfy.expect b/examples/Collections/Arrays/BinarySearch.dfy.expect deleted file mode 100644 index b48f86fa..00000000 --- a/examples/Collections/Arrays/BinarySearch.dfy.expect +++ /dev/null @@ -1,4 +0,0 @@ - -Dafny program verifier finished with 2 verified, 0 errors -[-6, 0, 1, 3, 7, 7, 9] -3 From 850e3d4367a0905e52550463dce8214c6cba7de4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 13 Sep 2022 14:26:56 -0700 Subject: [PATCH 23/32] Revert remaining unneeded edits --- examples/Unicode/Utf8EncodingFormExamples.dfy | 1 + src/Collections/Sequences/Seq.dfy | 102 +----------------- src/Math.dfy | 1 + 3 files changed, 4 insertions(+), 100 deletions(-) diff --git a/examples/Unicode/Utf8EncodingFormExamples.dfy b/examples/Unicode/Utf8EncodingFormExamples.dfy index 46bb72e4..f3ca0941 100644 --- a/examples/Unicode/Utf8EncodingFormExamples.dfy +++ b/examples/Unicode/Utf8EncodingFormExamples.dfy @@ -39,4 +39,5 @@ module Utf8EncodingFormExamples { ensures forall s | s in TEST_ILL_FORMED_SEQUENCES :: DecodeCodeUnitSequenceChecked(s).None? {} + } diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 86f69711..74a8970e 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -13,10 +13,11 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "../../Math.dfy" include "../../Wrappers.dfy" +include "../../Math.dfy" module Seq { + import opened Wrappers import Math @@ -370,15 +371,6 @@ module Seq { { } - /*makes sequence of length n filled with given Value */ - function method Fill(value: T, n: nat): seq - ensures |Fill(value, n)| == n - ensures forall i :: 0 <= i < n ==> Fill(value, n)[i] == value - { - seq(n, _ => value) - } - - /********************************************************** * * Extrema in Sequences @@ -773,94 +765,4 @@ module Seq { } } - -/********************************************************** - * - * Splitting of Sequences - * - ***********************************************************/ - - - lemma SeqTakeAppend(s: seq, i: int) - requires 0 <= i < |s| - ensures s[..i] + [s[i]] == s[..i + 1] - {} - - function method {:tailrecursion} Join(ss: seq>, joiner: seq): (s: seq) - requires 0 < |ss| - { - if |ss| == 1 then ss[0] else ss[0] + joiner + Join(ss[1..], joiner) - } - - function method {:tailrecursion} Split(s: seq, delim: T): (res: seq>) - ensures delim !in s ==> res == [s] - ensures s == [] ==> res == [[]] - ensures 0 < |res| - ensures forall i :: 0 <= i < |res| ==> delim !in res[i] - ensures Join(res, [delim]) == s - decreases |s| - { - var i := FindIndexMatching(s, delim, 0); - if i.Some? then [s[..i.value]] + Split(s[(i.value + 1)..], delim) else [s] - } - - lemma WillSplitOnDelim(s: seq, delim: T, prefix: seq) - requires |prefix| < |s| - requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i] - requires delim !in prefix && s[|prefix|] == delim - ensures Split(s, delim) == [prefix] + Split(s[|prefix| + 1..], delim) - { - calc { - Split(s, delim); - == - var i := FindIndexMatching(s, delim, 0); - if i.Some? then [s[..i.value]] + Split(s[i.value + 1..], delim) else [s]; - == { FindIndexMatchingLocatesElem(s, delim, 0, |prefix|); assert FindIndexMatching(s, delim, 0).Some?; } - [s[..|prefix|]] + Split(s[|prefix| + 1..], delim); - == { assert s[..|prefix|] == prefix; } - [prefix] + Split(s[|prefix| + 1..], delim); - } - } - - lemma WillNotSplitWithOutDelim(s: seq, delim: T) - requires delim !in s - ensures Split(s, delim) == [s] - { - calc { - Split(s, delim); - == - var i := FindIndexMatching(s, delim, 0); - if i.Some? then [s[..i.value]] + Split(s[i.value+1..], delim) else [s]; - == { FindIndexMatchingLocatesElem(s, delim, 0, |s|); } - [s]; - } - } - - lemma FindIndexMatchingLocatesElem(s: seq, c: T, start: nat, elemIndex: nat) - requires start <= elemIndex <= |s| - requires forall i :: start <= i < elemIndex ==> s[i] != c - requires elemIndex == |s| || s[elemIndex] == c - ensures FindIndexMatching(s, c, start) == if elemIndex == |s| then None else Some(elemIndex) - decreases elemIndex - start - {} - - function method FindIndexMatching(s: seq, c: T, i: nat): (index: Option) - requires i <= |s| - ensures index.Some? ==> i <= index.value < |s| && s[index.value] == c && c !in s[i..index.value] - ensures index.None? ==> c !in s[i..] - decreases |s| - i - { - FindIndex(s, x => x == c, i) - } - - function method {:tailrecursion} FindIndex(s: seq, f: T -> bool, i: nat): (index: Option) - requires i <= |s| - ensures index.Some? ==> i <= index.value < |s| && f(s[index.value]) && (forall j :: i <= j < index.value ==> !f(s[j])) - ensures index.None? ==> forall j :: i <= j < |s| ==> !f(s[j]) - decreases |s| - i - { - if i == |s| then None - else if f(s[i]) then Some(i) - else FindIndex(s, f, i + 1) - } } \ No newline at end of file diff --git a/src/Math.dfy b/src/Math.dfy index 2b7ce612..b58d098b 100644 --- a/src/Math.dfy +++ b/src/Math.dfy @@ -21,4 +21,5 @@ module Math { else a } + } From 34e380a7013199e62380a235731c586cb924a8cb Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 13 Sep 2022 14:27:42 -0700 Subject: [PATCH 24/32] Newline --- src/Collections/Sequences/Seq.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 74a8970e..39f5ac92 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -765,4 +765,4 @@ module Seq { } } -} \ No newline at end of file +} From 730278a285b4c0bbbc9b048d95f7ac52e4587f8c Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 15 Sep 2022 09:52:30 -0700 Subject: [PATCH 25/32] =?UTF-8?q?Start=20to=20use=20/functionSyntax:4,=20d?= =?UTF-8?q?on=E2=80=99t=20encourage=20compiling=20SortedBy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Collections/Sequences/MergeSort.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Collections/Sequences/MergeSort.dfy b/src/Collections/Sequences/MergeSort.dfy index 3cd9a724..01dc73b3 100644 --- a/src/Collections/Sequences/MergeSort.dfy +++ b/src/Collections/Sequences/MergeSort.dfy @@ -7,12 +7,12 @@ include "../../Relations.dfy" -module Seq.MergeSort { +module {:options "/functionSyntax:4"} Seq.MergeSort { import opened Relations //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedWith` - function method MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) + function MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) requires TotalOrdering(lessThanOrEq) ensures multiset(a) == multiset(result) ensures SortedBy(result, lessThanOrEq) @@ -31,7 +31,7 @@ module Seq.MergeSort { MergeSortedWith(leftSorted, rightSorted, lessThanOrEq) } - function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) + function {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) requires SortedBy(left, lessThanOrEq) requires SortedBy(right, lessThanOrEq) requires TotalOrdering(lessThanOrEq) From f1f31ade2ab4a73451d91e0c8bf579d844993acf Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 15 Sep 2022 13:19:18 -0700 Subject: [PATCH 26/32] Revert adding /functionSyntax:4 --- src/Collections/Sequences/MergeSort.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Collections/Sequences/MergeSort.dfy b/src/Collections/Sequences/MergeSort.dfy index 01dc73b3..3cd9a724 100644 --- a/src/Collections/Sequences/MergeSort.dfy +++ b/src/Collections/Sequences/MergeSort.dfy @@ -7,12 +7,12 @@ include "../../Relations.dfy" -module {:options "/functionSyntax:4"} Seq.MergeSort { +module Seq.MergeSort { import opened Relations //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedWith` - function MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) + function method MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) requires TotalOrdering(lessThanOrEq) ensures multiset(a) == multiset(result) ensures SortedBy(result, lessThanOrEq) @@ -31,7 +31,7 @@ module {:options "/functionSyntax:4"} Seq.MergeSort { MergeSortedWith(leftSorted, rightSorted, lessThanOrEq) } - function {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) + function method {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) requires SortedBy(left, lessThanOrEq) requires SortedBy(right, lessThanOrEq) requires TotalOrdering(lessThanOrEq) From 92a19bdbfba351713d31fc3ffede97062ad95c9e Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Fri, 21 Oct 2022 16:26:07 -0400 Subject: [PATCH 27/32] Adding Quick Sort and Arrays related utilities --- src/Collections/Arrays/Arrays.dfy | 374 ++++++++++++++++++++++++++++++ src/Collections/Sets/Sets.dfy | 11 + src/Comparison.dfy | 93 ++++++++ 3 files changed, 478 insertions(+) create mode 100644 src/Collections/Arrays/Arrays.dfy create mode 100644 src/Comparison.dfy diff --git a/src/Collections/Arrays/Arrays.dfy b/src/Collections/Arrays/Arrays.dfy new file mode 100644 index 00000000..e333616b --- /dev/null +++ b/src/Collections/Arrays/Arrays.dfy @@ -0,0 +1,374 @@ +// RUN: %dafny /compile:0 "%s" + +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +include "../Sets/Sets.dfy" +include "../../Comparison.dfy" + +module Arrays{ + +import opened Sets +import opened Comparison +import opened Wrappers + + trait Sorter { + ghost const C := Comparison(Cmp) + + function method Cmp(t0: T, t1: T): Cmp + + twostate predicate Identical(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + reads arr + { + arr[lo..hi] == old(arr[lo..hi]) + } + + twostate lemma IdenticalSplit(arr: array, lo: int, mid: int, hi: int) + requires 0 <= lo <= mid <= hi <= arr.Length + requires Identical(arr, lo, hi) + ensures Identical(arr, lo, mid) + ensures Identical(arr, mid, hi) + { + assert arr[lo..mid] == arr[lo..hi][..mid-lo]; + } + + twostate lemma IdenticalShuffled(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + requires Identical(arr, lo, hi) + ensures Shuffled(arr, lo, hi) + {} + + twostate predicate SameElements(arr: array, lo: int, hi: int) + reads arr + requires 0 <= lo <= hi <= arr.Length + { + && Identical(arr, 0, lo) + && Shuffled(arr, lo, hi) + && Identical(arr, hi, arr.Length) + } + + twostate lemma SameElementsExtend(arr: array, lo: int, lo': int, hi': int, hi: int) + requires 0 <= lo <= lo' <= hi' <= hi <= arr.Length + requires SameElements(arr, lo', hi') + ensures SameElements(arr, lo, hi) + { + assert SameElements(arr, lo', hi'); + assert Identical(arr, 0, lo') && Shuffled(arr, lo', hi') && Identical(arr, hi', arr.Length); + IdenticalSplit(arr, 0, lo, lo'); IdenticalSplit(arr, hi', hi, arr.Length); + assert && Identical(arr, 0, lo) && Identical(arr, lo, lo') + && Shuffled(arr, lo', hi') + && Identical(arr, hi', hi) && Identical(arr, hi, arr.Length); + IdenticalShuffled(arr, lo, lo'); IdenticalShuffled(arr, hi', hi); + assert && Identical(arr, 0, lo) && Shuffled(arr, lo, lo') + && Shuffled(arr, lo', hi') + && Shuffled(arr, hi', hi) && Identical(arr, hi, arr.Length); + ShuffledConcat(arr, lo, lo', hi'); ShuffledConcat(arr, lo, hi', hi); + assert Identical(arr, 0, lo) && Shuffled(arr, lo, hi) && Identical(arr, hi, arr.Length); + assert SameElements(arr, lo, hi); + } + + twostate predicate Shuffled(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + reads arr + { + multiset(arr[lo..hi]) == old(multiset(arr[lo..hi])) + } + + predicate Sortable(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + reads arr + { + reveal C.Valid?(); // Leaks through + C.Valid?(Sets.OfSlice(arr, lo, hi)) + } + + twostate lemma SetOfSliceShuffled(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + requires Shuffled(arr, lo, hi) + ensures Sets.OfSlice(arr, lo, hi) == old(Sets.OfSlice(arr, lo, hi)) + { + calc { + old(Sets.OfSlice(arr, lo, hi)); + set x <- old(arr[lo..hi]); + set x <- old(multiset(arr[lo..hi])); + set x <- multiset(arr[lo..hi]); + set x <- arr[lo..hi]; + Sets.OfSlice(arr, lo, hi); + } + } + + twostate lemma SortableSameElements(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + requires old(Sortable(arr, lo, hi)) + requires SameElements(arr, lo, hi) + ensures Sortable(arr, lo, hi) + { + SetOfSliceShuffled(arr, lo, hi); + } + + twostate lemma ShuffledConcat(arr: array, lo: int, mid: int, hi: int) + requires 0 <= lo <= mid <= hi <= arr.Length + requires Shuffled(arr, lo, mid) + requires Shuffled(arr, mid, hi) + ensures Shuffled(arr, lo, hi) + { + calc { + old(multiset(arr[lo..hi])); + { assert old(arr[lo..hi] == arr[lo..mid] + arr[mid..hi]); } + old(multiset(arr[lo..mid] + arr[mid..hi])); + old(multiset(arr[lo..mid])) + old(multiset(arr[mid..hi])); + multiset(arr[lo..mid]) + multiset(arr[mid..hi]); + { assert arr[lo..hi] == arr[lo..mid] + arr[mid..hi]; } + multiset(arr[lo..hi]); + } + } + + lemma Sortable_Slice(arr: array, lo: int, hi: int, lo': int, hi': int) + requires 0 <= lo <= lo' <= hi' <= hi <= arr.Length + requires Sortable(arr, lo, hi) + ensures Sortable(arr, lo', hi') + {} + + predicate Sorted(arr: array, lo: int, hi: int) + reads arr + requires 0 <= lo <= hi <= arr.Length + { + C.Sorted(arr[lo..hi]) + } + + lemma StripedInit(sq: seq, pivot: T, lo: int, hi: int) + requires 0 <= lo <= hi <= |sq| + ensures C.Striped(sq, pivot, lo, lo, lo, hi, hi) + { + reveal C.Striped(); + } + + lemma StripedNonEmpty(sq: seq, pivot: T, lo: int, left: int, mid: int, right: int, hi: int) + requires 0 <= lo <= left <= mid <= right <= hi <= |sq| + requires C.Striped(sq, pivot, lo, left, mid, right, hi) + requires C.Valid?(Sets.OfSeq(sq[lo..hi])) + requires pivot in sq[lo..hi] + ensures left < right + { + reveal C.Valid?(); + var idx :| lo <= idx < hi && sq[idx] == pivot; + C.AlwaysReflexive(pivot); + reveal C.Striped(); + } + + twostate lemma StripedSameElements(arr: array, pivot: T, lo: int, left: int, right: int, hi: int) + requires 0 <= lo <= left <= right <= hi <= |arr[..]| + requires Shuffled(arr, lo, left) + requires Identical(arr, left, right) + requires Shuffled(arr, right, hi) + requires old(C.Striped(arr[..], pivot, lo, left, right, right, hi)) + ensures C.Striped(arr[..], pivot, lo, left, right, right, hi) + { + reveal C.Striped(); + forall i | lo <= i < left ensures Cmp(arr[..][i], pivot).Lt? { + assert arr[..][i] == arr[lo..left][i - lo]; + assert arr[..][i] in multiset(arr[lo..left]); + } + forall i | left <= i < right ensures Cmp(arr[..][i], pivot).Eq? { + assert arr[..][i] == arr[left..right][i - left]; + } + forall i | right <= i < hi ensures Cmp(arr[..][i], pivot).Gt? { + assert arr[..][i] == arr[right..hi][i - right]; + assert arr[..][i] in multiset(arr[right..hi]); + } + } + + method Swap(arr: array, ghost lo: int, i: int, j: int, ghost hi: int) + requires 0 <= lo <= i <= j < hi <= arr.Length + modifies arr + ensures SameElements(arr, lo, hi) + ensures arr[..] == old(arr[..][i := arr[j]][j := arr[i]]) + { + arr[i], arr[j] := arr[j], arr[i]; + } + + method SwapLt( + arr: array, pivot: T, + lo: int, left: int, mid: int, right: int, hi: int + ) + requires 0 <= lo <= left <= mid < right <= hi <= arr.Length + requires C.Striped(arr[..], pivot, lo, left, mid, right, hi) + requires Cmp(arr[mid], pivot).Lt? + modifies arr + ensures SameElements(arr, lo, hi) + ensures arr[..] == old(arr[..][left := arr[mid]][mid := arr[left]]) + ensures C.Striped(arr[..], pivot, lo, left + 1, mid + 1, right, hi) + { + reveal C.Striped(); + Swap(arr, lo, left, mid, hi); + } + + method SwapGt( + arr: array, pivot: T, + lo: int, left: int, mid: int, right: int, hi: int + ) + requires 0 <= lo <= left <= mid < right <= hi <= arr.Length + requires C.Striped(arr[..], pivot, lo, left, mid, right, hi) + requires Cmp(arr[mid], pivot).Gt? + modifies arr + ensures SameElements(arr, lo, hi) + ensures arr[..] == old(arr[..][mid := arr[right - 1]][right - 1 := arr[mid]]) + ensures C.Striped(arr[..], pivot, lo, left, mid, right - 1, hi) + { + reveal C.Striped(); + Swap(arr, lo, mid, right - 1, hi); + } + + lemma SortedStripedMiddle(arr: array, pivot: T, lo: int, left: int, right: int, hi: int) + requires 0 <= lo <= left < right <= hi <= arr.Length + requires Sortable(arr, lo, hi) + requires pivot in multiset(arr[lo..hi]) + requires C.Striped(arr[..], pivot, lo, left, right, right, hi) + ensures Sorted(arr, left, right) + { + reveal C.Striped(); + forall i, j | left <= i < j < right ensures Cmp(arr[i], arr[j]).Le? { + var idx :| lo <= idx < hi && arr[idx] == pivot; + assert Cmp(arr[i], pivot) == Eq; + assert C.Complete??(arr[j], pivot); + assert C.Transitive??(arr[i], pivot, arr[j]); + } + } + + lemma SortedConcat(arr: array, lo: int, mid: int, hi: int) + requires 0 <= lo <= mid <= hi <= arr.Length + requires Sorted(arr, lo, mid) + requires Sorted(arr, mid, hi) + requires forall i, j | lo <= i < mid <= j < hi :: Cmp(arr[i], arr[j]).Le? + ensures Sorted(arr, lo, hi) + { + assert arr[lo..mid] + arr[mid..hi] == arr[lo..hi]; + C.SortedConcat(arr[lo..mid], arr[mid..hi]); + } + + twostate lemma SortedIdentical(arr: array, lo: int, hi: int) + requires 0 <= lo <= hi <= arr.Length + requires old(Sorted(arr, lo, hi)) + requires Identical(arr, lo, hi) + ensures Sorted(arr, lo, hi) + { + assert arr[lo..hi] == old(arr[lo..hi]); + forall i, j | lo <= i < j < hi ensures Cmp(arr[i], arr[j]).Le? { + assert arr[i] == arr[lo..hi][i - lo]; + assert arr[j] == arr[lo..hi][j - lo]; + } + } + + lemma SortedDutchFlag(arr: array, pivot: T, lo: int, left: int, right: int, hi: int) + requires 0 <= lo <= left < right <= hi <= arr.Length + requires Sortable(arr, lo, hi) + requires pivot in multiset(arr[lo..hi]) + requires Sorted(arr, lo, left) + requires Sorted(arr, right, hi) + requires C.Striped(arr[..], pivot, lo, left, right, right, hi) + ensures Sorted(arr, lo, hi) + { + reveal C.Striped(); + forall i, j | lo <= i < left <= j < right ensures Cmp(arr[i], arr[j]).Le? { + var idx :| lo <= idx < hi && arr[idx] == pivot; + assert Cmp(arr[i], pivot).Le?; + assert Cmp(arr[j], pivot).Eq?; + assert C.Complete??(arr[j], pivot); + assert C.Transitive??(arr[i], pivot, arr[j]); + } + SortedStripedMiddle(arr, pivot, lo, left, right, hi); + SortedConcat(arr, lo, left, right); + forall i, j | lo <= i < right <= j < hi ensures Cmp(arr[i], arr[j]).Le? { + assert Cmp(arr[i], pivot).Le?; + assert Cmp(arr[j], pivot).Gt?; + assert C.Complete??(arr[i], pivot); + assert C.Complete??(arr[j], pivot); + assert C.Transitive??(arr[i], pivot, arr[j]); + } + SortedConcat(arr, lo, right, hi); + } + + method QuickSort(arr: array, lo: int := 0, hi: int := arr.Length) + requires 0 <= lo <= hi <= arr.Length + requires Sortable(arr, lo, hi) + decreases hi - lo + modifies arr + ensures Sortable(arr, lo, hi) + ensures Sorted(arr, lo, hi) + ensures SameElements(arr, lo, hi) + { + if hi - lo > 1 { + var pivot := MedianOfMedians(arr, lo, hi); + var left, right := DutchFlag(arr, pivot, lo, hi); + + label left: + SortableSameElements(arr, lo, hi); + Sortable_Slice(arr, lo, hi, lo, left); + StripedNonEmpty(arr[..], pivot, lo, left, right, right, hi); + QuickSort(arr, lo, left); + + label right: + SameElementsExtend@left(arr, lo, lo, left, hi); + SortableSameElements(arr, lo, hi); + Sortable_Slice(arr, lo, hi, right, hi); + IdenticalSplit@left(arr, left, hi, arr.Length); + IdenticalSplit@left(arr, left, right, hi); + IdenticalShuffled@left(arr, right, hi); + StripedSameElements@left(arr, pivot, lo, left, right, hi); + QuickSort(arr, right, hi); + + SameElementsExtend@right(arr, lo, right, hi, hi); + SortableSameElements(arr, lo, hi); + IdenticalSplit@right(arr, lo, left, right); + SortedIdentical@right(arr, lo, left); + StripedSameElements@right(arr, pivot, lo, left, right, hi); + SortedDutchFlag(arr, pivot, lo, left, right, hi); + } + } + + function method MedianOfMedians(arr: array, lo: int, hi: int): (t: T) + requires 0 <= lo < hi <= arr.Length + reads arr + ensures t in arr[lo..hi] + { + arr[lo] // TODO + } + + method DutchFlag(arr: array, pivot: T, lo: int, hi: int) returns (left: int, right: int) + requires 0 <= lo < hi <= arr.Length + requires pivot in multiset(arr[lo..hi]) + modifies arr + ensures SameElements(arr, lo, hi) + ensures lo <= left <= right <= hi + ensures C.Striped(arr[..], pivot, lo, left, right, right, hi) + { + left, right := lo, hi; + var mid := lo; + StripedInit(arr[..], pivot, lo, hi); + + while mid < right + invariant pivot in multiset(arr[lo..hi]) + invariant lo <= left <= mid <= right <= hi + invariant SameElements(arr, lo, hi) + invariant C.Striped(arr[..], pivot, lo, left, mid, right, hi) + { + reveal C.Striped(); + match Cmp(arr[mid], pivot) { + case Lt => + SwapLt(arr, pivot, lo, left, mid, right, hi); + left := left + 1; + mid := mid + 1; + case Gt => + SwapGt(arr, pivot, lo, left, mid, right, hi); + right := right - 1; + case Eq => + mid := mid + 1; + } + } + + } +} +} \ No newline at end of file diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index b5a29cc7..ea28f1ee 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -193,4 +193,15 @@ module Sets { LemmaSubsetSize(x, range); } + function method OfSeq(sq: seq): set { + set x <- sq + } + + function method OfSlice(arr: array, lo: int, hi: int): set + requires 0 <= lo <= hi <= arr.Length + reads arr + { + OfSeq(arr[lo..hi]) + } + } diff --git a/src/Comparison.dfy b/src/Comparison.dfy new file mode 100644 index 00000000..ce2c8225 --- /dev/null +++ b/src/Comparison.dfy @@ -0,0 +1,93 @@ +// RUN: %dafny /compile:0 "%s" + +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +include "Wrappers.dfy" +include "Relations.dfy" +module Comparison { + +import opened Wrappers +import opened Relations + + datatype Cmp = Lt | Eq | Gt { + function method Flip(): Cmp { + match this + case Lt => Gt + case Eq => Eq + case Gt => Lt + } + + const Le? := this != Gt + const Ge? := this != Lt + + static function method ComputeTransitivity(c0: Cmp, c1: Cmp): Option { + match (c0, c1) + case (Lt, Lt) => Some(Lt) + case (Lt, Eq) => Some(Lt) + case (Lt, Gt) => None + case (Eq, Lt) => Some(Lt) + case (Eq, Eq) => Some(Eq) + case (Eq, Gt) => Some(Gt) + case (Gt, Lt) => None + case (Gt, Eq) => Some(Gt) + case (Gt, Gt) => Some(Gt) + } + } + datatype Comparison = Comparison(cmp: (T, T) -> Cmp) { + function method Compare(t0: T, t1: T): Cmp { + cmp(t0, t1) + } + + predicate Complete??(t0: T, t1: T) { + cmp(t0, t1) == cmp(t1, t0).Flip() + } + + predicate Transitive??(t0: T, t1: T, t2: T) { + cmp(t0, t1).Le? && cmp(t1, t2).Le? ==> cmp(t0, t2).Le? + } + + predicate Complete?(ts: set) { + forall t0, t1 | t0 in ts && t1 in ts :: Complete??(t0, t1) + } + + predicate Transitive?(ts: set) { + forall t0, t1, t2 | t0 in ts && t1 in ts && t2 in ts :: Transitive??(t0, t1, t2) + } + + predicate {:opaque} Valid?(ts: set) { + Complete?(ts) && /* Antisymmetric?(ts) && */ Transitive?(ts) + } + + predicate Sorted(sq: seq) { + forall i, j | 0 <= i < j < |sq| :: cmp(sq[i], sq[j]).Le? + } + + predicate Reflexive??(t0: T) { + cmp(t0, t0) == Eq + } + + lemma AlwaysReflexive(t0: T) + requires Complete??(t0, t0) + ensures Reflexive??(t0) + {} + + predicate {:opaque} Striped(sq: seq, pivot: T, lo: int, left: int, mid: int, right: int, hi: int) + requires 0 <= lo <= left <= mid <= right <= hi <= |sq| + { + && (forall i | lo <= i < left :: cmp(sq[i], pivot).Lt?) + && (forall i | left <= i < mid :: cmp(sq[i], pivot).Eq?) + && (forall i | right <= i < hi :: cmp(sq[i], pivot).Gt?) + } + + lemma SortedConcat(sq0: seq, sq1: seq) + requires Sorted(sq0) + requires Sorted(sq1) + requires forall i, j | 0 <= i < |sq0| && 0 <= j < |sq1| :: cmp(sq0[i], sq1[j]).Le? + ensures Sorted(sq0 + sq1) + {} + + } + } \ No newline at end of file From bc018cbe388682a382f0bd8675f67e407d5bf9f0 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Fri, 11 Nov 2022 15:39:29 -0500 Subject: [PATCH 28/32] edit to run tests again --- src/Collections/Sets/Sets.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index ea28f1ee..e285d720 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -204,4 +204,4 @@ module Sets { OfSeq(arr[lo..hi]) } -} +} \ No newline at end of file From ae832a49ab95c5305f3445ba57e8b2ff61ff779c Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Mon, 14 Nov 2022 15:25:10 -0500 Subject: [PATCH 29/32] using different synrtax for CI --- src/Collections/Sets/Sets.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index e285d720..d0c285db 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -194,7 +194,7 @@ module Sets { } function method OfSeq(sq: seq): set { - set x <- sq + set x | x in sq } function method OfSlice(arr: array, lo: int, hi: int): set From a508b999e19cd67b7ab4de215f84f1a952c53f49 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Mon, 14 Nov 2022 16:34:46 -0500 Subject: [PATCH 30/32] for another file --- src/Collections/Arrays/Arrays.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Collections/Arrays/Arrays.dfy b/src/Collections/Arrays/Arrays.dfy index e333616b..d46ca2ac 100644 --- a/src/Collections/Arrays/Arrays.dfy +++ b/src/Collections/Arrays/Arrays.dfy @@ -92,10 +92,10 @@ import opened Wrappers { calc { old(Sets.OfSlice(arr, lo, hi)); - set x <- old(arr[lo..hi]); - set x <- old(multiset(arr[lo..hi])); - set x <- multiset(arr[lo..hi]); - set x <- arr[lo..hi]; + set x | x in old(arr[lo..hi]); + set x | x in old(multiset(arr[lo..hi])); + set x | x in multiset(arr[lo..hi]); + set x | x in arr[lo..hi]; Sets.OfSlice(arr, lo, hi); } } From 03af996c4004096e7545f08fc3100f7122a39972 Mon Sep 17 00:00:00 2001 From: Parva Shah <89794159+prvshah51@users.noreply.github.com> Date: Thu, 17 Nov 2022 17:47:00 -0500 Subject: [PATCH 31/32] Apply suggestions from review for readability Co-authored-by: Robin Salkeld --- src/Collections/Arrays/Arrays.dfy | 4 ++-- src/Collections/Sets/Sets.dfy | 2 +- src/Comparison.dfy | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Collections/Arrays/Arrays.dfy b/src/Collections/Arrays/Arrays.dfy index d46ca2ac..519bb333 100644 --- a/src/Collections/Arrays/Arrays.dfy +++ b/src/Collections/Arrays/Arrays.dfy @@ -337,7 +337,7 @@ import opened Wrappers arr[lo] // TODO } - method DutchFlag(arr: array, pivot: T, lo: int, hi: int) returns (left: int, right: int) + method DutchFlag(arr: array, pivot: T, lo: int, hi: int) returns (left: int, right: int) requires 0 <= lo < hi <= arr.Length requires pivot in multiset(arr[lo..hi]) modifies arr @@ -370,5 +370,5 @@ import opened Wrappers } } -} + } } \ No newline at end of file diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index d0c285db..3d8dc045 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -193,7 +193,7 @@ module Sets { LemmaSubsetSize(x, range); } - function method OfSeq(sq: seq): set { + function method OfSeq(sq: seq): set { set x | x in sq } diff --git a/src/Comparison.dfy b/src/Comparison.dfy index ce2c8225..9b44f8bf 100644 --- a/src/Comparison.dfy +++ b/src/Comparison.dfy @@ -9,8 +9,8 @@ include "Wrappers.dfy" include "Relations.dfy" module Comparison { -import opened Wrappers -import opened Relations + import opened Wrappers + import opened Relations datatype Cmp = Lt | Eq | Gt { function method Flip(): Cmp { From 467f5877d75ac4534e4f7b4ac01a0e8680630080 Mon Sep 17 00:00:00 2001 From: Parva Shah Date: Fri, 2 Dec 2022 16:38:20 -0500 Subject: [PATCH 32/32] improving readabilty as per suggestions --- src/Collections/Arrays/Arrays.dfy | 123 +++++++++++++++--------------- src/Comparison.dfy | 24 +++--- 2 files changed, 74 insertions(+), 73 deletions(-) diff --git a/src/Collections/Arrays/Arrays.dfy b/src/Collections/Arrays/Arrays.dfy index d46ca2ac..31861b1f 100644 --- a/src/Collections/Arrays/Arrays.dfy +++ b/src/Collections/Arrays/Arrays.dfy @@ -19,55 +19,55 @@ import opened Wrappers function method Cmp(t0: T, t1: T): Cmp - twostate predicate Identical(arr: array, lo: int, hi: int) + twostate predicate UnchangedSlice(arr: array, lo: int, hi: int) requires 0 <= lo <= hi <= arr.Length reads arr { arr[lo..hi] == old(arr[lo..hi]) } - twostate lemma IdenticalSplit(arr: array, lo: int, mid: int, hi: int) + twostate lemma UnchangedSliceSplit(arr: array, lo: int, mid: int, hi: int) requires 0 <= lo <= mid <= hi <= arr.Length - requires Identical(arr, lo, hi) - ensures Identical(arr, lo, mid) - ensures Identical(arr, mid, hi) + requires UnchangedSlice(arr, lo, hi) + ensures UnchangedSlice(arr, lo, mid) + ensures UnchangedSlice(arr, mid, hi) { assert arr[lo..mid] == arr[lo..hi][..mid-lo]; } - twostate lemma IdenticalShuffled(arr: array, lo: int, hi: int) + twostate lemma UnchangedSliceShuffled(arr: array, lo: int, hi: int) requires 0 <= lo <= hi <= arr.Length - requires Identical(arr, lo, hi) + requires UnchangedSlice(arr, lo, hi) ensures Shuffled(arr, lo, hi) {} - twostate predicate SameElements(arr: array, lo: int, hi: int) + twostate predicate UnchangedExceptSliceShuffled(arr: array, lo: int, hi: int) reads arr requires 0 <= lo <= hi <= arr.Length { - && Identical(arr, 0, lo) + && UnchangedSlice(arr, 0, lo) && Shuffled(arr, lo, hi) - && Identical(arr, hi, arr.Length) + && UnchangedSlice(arr, hi, arr.Length) } - twostate lemma SameElementsExtend(arr: array, lo: int, lo': int, hi': int, hi: int) + twostate lemma UnchangedExceptSliceShuffledExtend(arr: array, lo: int, lo': int, hi': int, hi: int) requires 0 <= lo <= lo' <= hi' <= hi <= arr.Length - requires SameElements(arr, lo', hi') - ensures SameElements(arr, lo, hi) + requires UnchangedExceptSliceShuffled(arr, lo', hi') + ensures UnchangedExceptSliceShuffled(arr, lo, hi) { - assert SameElements(arr, lo', hi'); - assert Identical(arr, 0, lo') && Shuffled(arr, lo', hi') && Identical(arr, hi', arr.Length); - IdenticalSplit(arr, 0, lo, lo'); IdenticalSplit(arr, hi', hi, arr.Length); - assert && Identical(arr, 0, lo) && Identical(arr, lo, lo') + assert UnchangedExceptSliceShuffled(arr, lo', hi'); + assert UnchangedSlice(arr, 0, lo') && Shuffled(arr, lo', hi') && UnchangedSlice(arr, hi', arr.Length); + UnchangedSliceSplit(arr, 0, lo, lo'); UnchangedSliceSplit(arr, hi', hi, arr.Length); + assert && UnchangedSlice(arr, 0, lo) && UnchangedSlice(arr, lo, lo') && Shuffled(arr, lo', hi') - && Identical(arr, hi', hi) && Identical(arr, hi, arr.Length); - IdenticalShuffled(arr, lo, lo'); IdenticalShuffled(arr, hi', hi); - assert && Identical(arr, 0, lo) && Shuffled(arr, lo, lo') + && UnchangedSlice(arr, hi', hi) && UnchangedSlice(arr, hi, arr.Length); + UnchangedSliceShuffled(arr, lo, lo'); UnchangedSliceShuffled(arr, hi', hi); + assert && UnchangedSlice(arr, 0, lo) && Shuffled(arr, lo, lo') && Shuffled(arr, lo', hi') - && Shuffled(arr, hi', hi) && Identical(arr, hi, arr.Length); + && Shuffled(arr, hi', hi) && UnchangedSlice(arr, hi, arr.Length); ShuffledConcat(arr, lo, lo', hi'); ShuffledConcat(arr, lo, hi', hi); - assert Identical(arr, 0, lo) && Shuffled(arr, lo, hi) && Identical(arr, hi, arr.Length); - assert SameElements(arr, lo, hi); + assert UnchangedSlice(arr, 0, lo) && Shuffled(arr, lo, hi) && UnchangedSlice(arr, hi, arr.Length); + assert UnchangedExceptSliceShuffled(arr, lo, hi); } twostate predicate Shuffled(arr: array, lo: int, hi: int) @@ -81,8 +81,8 @@ import opened Wrappers requires 0 <= lo <= hi <= arr.Length reads arr { - reveal C.Valid?(); // Leaks through - C.Valid?(Sets.OfSlice(arr, lo, hi)) + reveal C.Valid(); // Leaks through + C.Valid(Sets.OfSlice(arr, lo, hi)) } twostate lemma SetOfSliceShuffled(arr: array, lo: int, hi: int) @@ -100,10 +100,10 @@ import opened Wrappers } } - twostate lemma SortableSameElements(arr: array, lo: int, hi: int) + twostate lemma SortableUnchangedExceptSliceShuffled(arr: array, lo: int, hi: int) requires 0 <= lo <= hi <= arr.Length requires old(Sortable(arr, lo, hi)) - requires SameElements(arr, lo, hi) + requires UnchangedExceptSliceShuffled(arr, lo, hi) ensures Sortable(arr, lo, hi) { SetOfSliceShuffled(arr, lo, hi); @@ -126,7 +126,7 @@ import opened Wrappers } } - lemma Sortable_Slice(arr: array, lo: int, hi: int, lo': int, hi': int) + lemma SortableSubslice(arr: array, lo: int, hi: int, lo': int, hi': int) requires 0 <= lo <= lo' <= hi' <= hi <= arr.Length requires Sortable(arr, lo, hi) ensures Sortable(arr, lo', hi') @@ -149,20 +149,20 @@ import opened Wrappers lemma StripedNonEmpty(sq: seq, pivot: T, lo: int, left: int, mid: int, right: int, hi: int) requires 0 <= lo <= left <= mid <= right <= hi <= |sq| requires C.Striped(sq, pivot, lo, left, mid, right, hi) - requires C.Valid?(Sets.OfSeq(sq[lo..hi])) + requires C.Valid(Sets.OfSeq(sq[lo..hi])) requires pivot in sq[lo..hi] ensures left < right { - reveal C.Valid?(); + reveal C.Valid(); var idx :| lo <= idx < hi && sq[idx] == pivot; C.AlwaysReflexive(pivot); reveal C.Striped(); } - twostate lemma StripedSameElements(arr: array, pivot: T, lo: int, left: int, right: int, hi: int) + twostate lemma StripedUnchangedExceptSliceShuffled(arr: array, pivot: T, lo: int, left: int, right: int, hi: int) requires 0 <= lo <= left <= right <= hi <= |arr[..]| requires Shuffled(arr, lo, left) - requires Identical(arr, left, right) + requires UnchangedSlice(arr, left, right) requires Shuffled(arr, right, hi) requires old(C.Striped(arr[..], pivot, lo, left, right, right, hi)) ensures C.Striped(arr[..], pivot, lo, left, right, right, hi) @@ -184,7 +184,7 @@ import opened Wrappers method Swap(arr: array, ghost lo: int, i: int, j: int, ghost hi: int) requires 0 <= lo <= i <= j < hi <= arr.Length modifies arr - ensures SameElements(arr, lo, hi) + ensures UnchangedExceptSliceShuffled(arr, lo, hi) ensures arr[..] == old(arr[..][i := arr[j]][j := arr[i]]) { arr[i], arr[j] := arr[j], arr[i]; @@ -198,7 +198,7 @@ import opened Wrappers requires C.Striped(arr[..], pivot, lo, left, mid, right, hi) requires Cmp(arr[mid], pivot).Lt? modifies arr - ensures SameElements(arr, lo, hi) + ensures UnchangedExceptSliceShuffled(arr, lo, hi) ensures arr[..] == old(arr[..][left := arr[mid]][mid := arr[left]]) ensures C.Striped(arr[..], pivot, lo, left + 1, mid + 1, right, hi) { @@ -214,7 +214,7 @@ import opened Wrappers requires C.Striped(arr[..], pivot, lo, left, mid, right, hi) requires Cmp(arr[mid], pivot).Gt? modifies arr - ensures SameElements(arr, lo, hi) + ensures UnchangedExceptSliceShuffled(arr, lo, hi) ensures arr[..] == old(arr[..][mid := arr[right - 1]][right - 1 := arr[mid]]) ensures C.Striped(arr[..], pivot, lo, left, mid, right - 1, hi) { @@ -233,8 +233,8 @@ import opened Wrappers forall i, j | left <= i < j < right ensures Cmp(arr[i], arr[j]).Le? { var idx :| lo <= idx < hi && arr[idx] == pivot; assert Cmp(arr[i], pivot) == Eq; - assert C.Complete??(arr[j], pivot); - assert C.Transitive??(arr[i], pivot, arr[j]); + assert C.CompleteonPair(arr[j], pivot); + assert C.Transitive'(arr[i], pivot, arr[j]); } } @@ -249,10 +249,10 @@ import opened Wrappers C.SortedConcat(arr[lo..mid], arr[mid..hi]); } - twostate lemma SortedIdentical(arr: array, lo: int, hi: int) + twostate lemma SortedUnchangedSlice(arr: array, lo: int, hi: int) requires 0 <= lo <= hi <= arr.Length requires old(Sorted(arr, lo, hi)) - requires Identical(arr, lo, hi) + requires UnchangedSlice(arr, lo, hi) ensures Sorted(arr, lo, hi) { assert arr[lo..hi] == old(arr[lo..hi]); @@ -276,21 +276,22 @@ import opened Wrappers var idx :| lo <= idx < hi && arr[idx] == pivot; assert Cmp(arr[i], pivot).Le?; assert Cmp(arr[j], pivot).Eq?; - assert C.Complete??(arr[j], pivot); - assert C.Transitive??(arr[i], pivot, arr[j]); + assert C.CompleteonPair(arr[j], pivot); + assert C.Transitive'(arr[i], pivot, arr[j]); } SortedStripedMiddle(arr, pivot, lo, left, right, hi); SortedConcat(arr, lo, left, right); forall i, j | lo <= i < right <= j < hi ensures Cmp(arr[i], arr[j]).Le? { assert Cmp(arr[i], pivot).Le?; assert Cmp(arr[j], pivot).Gt?; - assert C.Complete??(arr[i], pivot); - assert C.Complete??(arr[j], pivot); - assert C.Transitive??(arr[i], pivot, arr[j]); + assert C.CompleteonPair(arr[i], pivot); + assert C.CompleteonPair(arr[j], pivot); + assert C.Transitive'(arr[i], pivot, arr[j]); } SortedConcat(arr, lo, right, hi); } + // Doesn't have the O(n log n) worst case runtime yet, need MedianofMeians algorithm implemented for that. method QuickSort(arr: array, lo: int := 0, hi: int := arr.Length) requires 0 <= lo <= hi <= arr.Length requires Sortable(arr, lo, hi) @@ -298,33 +299,33 @@ import opened Wrappers modifies arr ensures Sortable(arr, lo, hi) ensures Sorted(arr, lo, hi) - ensures SameElements(arr, lo, hi) + ensures UnchangedExceptSliceShuffled(arr, lo, hi) { if hi - lo > 1 { var pivot := MedianOfMedians(arr, lo, hi); var left, right := DutchFlag(arr, pivot, lo, hi); label left: - SortableSameElements(arr, lo, hi); - Sortable_Slice(arr, lo, hi, lo, left); + SortableUnchangedExceptSliceShuffled(arr, lo, hi); + SortableSubslice(arr, lo, hi, lo, left); StripedNonEmpty(arr[..], pivot, lo, left, right, right, hi); QuickSort(arr, lo, left); label right: - SameElementsExtend@left(arr, lo, lo, left, hi); - SortableSameElements(arr, lo, hi); - Sortable_Slice(arr, lo, hi, right, hi); - IdenticalSplit@left(arr, left, hi, arr.Length); - IdenticalSplit@left(arr, left, right, hi); - IdenticalShuffled@left(arr, right, hi); - StripedSameElements@left(arr, pivot, lo, left, right, hi); + UnchangedExceptSliceShuffledExtend@left(arr, lo, lo, left, hi); + SortableUnchangedExceptSliceShuffled(arr, lo, hi); + SortableSubslice(arr, lo, hi, right, hi); + UnchangedSliceSplit@left(arr, left, hi, arr.Length); + UnchangedSliceSplit@left(arr, left, right, hi); + UnchangedSliceShuffled@left(arr, right, hi); + StripedUnchangedExceptSliceShuffled@left(arr, pivot, lo, left, right, hi); QuickSort(arr, right, hi); - SameElementsExtend@right(arr, lo, right, hi, hi); - SortableSameElements(arr, lo, hi); - IdenticalSplit@right(arr, lo, left, right); - SortedIdentical@right(arr, lo, left); - StripedSameElements@right(arr, pivot, lo, left, right, hi); + UnchangedExceptSliceShuffledExtend@right(arr, lo, right, hi, hi); + SortableUnchangedExceptSliceShuffled(arr, lo, hi); + UnchangedSliceSplit@right(arr, lo, left, right); + SortedUnchangedSlice@right(arr, lo, left); + StripedUnchangedExceptSliceShuffled@right(arr, pivot, lo, left, right, hi); SortedDutchFlag(arr, pivot, lo, left, right, hi); } } @@ -341,7 +342,7 @@ import opened Wrappers requires 0 <= lo < hi <= arr.Length requires pivot in multiset(arr[lo..hi]) modifies arr - ensures SameElements(arr, lo, hi) + ensures UnchangedExceptSliceShuffled(arr, lo, hi) ensures lo <= left <= right <= hi ensures C.Striped(arr[..], pivot, lo, left, right, right, hi) { @@ -352,7 +353,7 @@ import opened Wrappers while mid < right invariant pivot in multiset(arr[lo..hi]) invariant lo <= left <= mid <= right <= hi - invariant SameElements(arr, lo, hi) + invariant UnchangedExceptSliceShuffled(arr, lo, hi) invariant C.Striped(arr[..], pivot, lo, left, mid, right, hi) { reveal C.Striped(); diff --git a/src/Comparison.dfy b/src/Comparison.dfy index ce2c8225..5b5e1484 100644 --- a/src/Comparison.dfy +++ b/src/Comparison.dfy @@ -41,37 +41,37 @@ import opened Relations cmp(t0, t1) } - predicate Complete??(t0: T, t1: T) { + predicate CompleteonPair(t0: T, t1: T) { cmp(t0, t1) == cmp(t1, t0).Flip() } - predicate Transitive??(t0: T, t1: T, t2: T) { + predicate Transitive'(t0: T, t1: T, t2: T) { cmp(t0, t1).Le? && cmp(t1, t2).Le? ==> cmp(t0, t2).Le? } - predicate Complete?(ts: set) { - forall t0, t1 | t0 in ts && t1 in ts :: Complete??(t0, t1) + predicate Complete(ts: set) { + forall t0, t1 | t0 in ts && t1 in ts :: CompleteonPair(t0, t1) } - predicate Transitive?(ts: set) { - forall t0, t1, t2 | t0 in ts && t1 in ts && t2 in ts :: Transitive??(t0, t1, t2) + predicate Transitive(ts: set) { + forall t0, t1, t2 | t0 in ts && t1 in ts && t2 in ts :: Transitive'(t0, t1, t2) } - predicate {:opaque} Valid?(ts: set) { - Complete?(ts) && /* Antisymmetric?(ts) && */ Transitive?(ts) + predicate {:opaque} Valid(ts: set) { + Complete(ts) && Transitive(ts) } predicate Sorted(sq: seq) { forall i, j | 0 <= i < j < |sq| :: cmp(sq[i], sq[j]).Le? } - predicate Reflexive??(t0: T) { + predicate Reflexive'(t0: T) { cmp(t0, t0) == Eq } lemma AlwaysReflexive(t0: T) - requires Complete??(t0, t0) - ensures Reflexive??(t0) + requires CompleteonPair(t0, t0) + ensures Reflexive'(t0) {} predicate {:opaque} Striped(sq: seq, pivot: T, lo: int, left: int, mid: int, right: int, hi: int) @@ -90,4 +90,4 @@ import opened Relations {} } - } \ No newline at end of file + } \ No newline at end of file