From aed044ead4142fb86f6bb93969d4a7dd63fd1f5e Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Thu, 2 Sep 2021 10:35:35 -0700 Subject: [PATCH 01/36] Add NatSeq and Io libraries --- README.md | 2 + examples/Io/IoExample.dfy | 64 ++ examples/Io/IoExample.dfy.expect | 2 + examples/NatSeq/NatSeqExample.dfy | 38 ++ examples/NatSeq/NatSeqExample.dfy.expect | 2 + src/Collections/Sequences/NatSeq.dfy | 595 ++++++++++++++++++ src/Collections/Sequences/NatSeq.dfy.expect | 2 + .../Sequences/NatSeqConversions.dfy | 300 +++++++++ .../Sequences/NatSeqConversions.dfy.expect | 2 + src/Io/Io.dfy | 128 ++++ src/Io/Io.dfy.expect | 2 + src/Io/IoNative.cs | 113 ++++ src/NativeTypes.dfy | 39 ++ src/NativeTypes.dfy.expect | 2 + 14 files changed, 1291 insertions(+) create mode 100644 examples/Io/IoExample.dfy create mode 100644 examples/Io/IoExample.dfy.expect create mode 100644 examples/NatSeq/NatSeqExample.dfy create mode 100644 examples/NatSeq/NatSeqExample.dfy.expect create mode 100644 src/Collections/Sequences/NatSeq.dfy create mode 100644 src/Collections/Sequences/NatSeq.dfy.expect create mode 100644 src/Collections/Sequences/NatSeqConversions.dfy create mode 100644 src/Collections/Sequences/NatSeqConversions.dfy.expect create mode 100644 src/Io/Io.dfy create mode 100644 src/Io/Io.dfy.expect create mode 100644 src/Io/IoNative.cs create mode 100644 src/NativeTypes.dfy create mode 100644 src/NativeTypes.dfy.expect diff --git a/README.md b/README.md index 98bcaba7..fef7bac5 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,8 @@ Much of this code came from or was inspired by code from the following projects: * [Ironclad Apps](https://github.com/microsoft/Ironclad/tree/main/ironclad-apps) * [IronFleet](https://github.com/microsoft/Ironclad/tree/main/ironfleet) +* [James Wilcox's Notes](https://github.com/wilcoxjay/notes) * [Vale](https://github.com/project-everest/vale/tree/legacy_dafny) * [Verified BetrFS](https://github.com/vmware-labs/verified-betrfs) +* [Verifying OpenTitan](https://github.com/secure-foundations/veri-titan) diff --git a/examples/Io/IoExample.dfy b/examples/Io/IoExample.dfy new file mode 100644 index 00000000..69172a8a --- /dev/null +++ b/examples/Io/IoExample.dfy @@ -0,0 +1,64 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../../src/Io/Io.dfy" +include "../../src/NativeTypes.dfy" + +module IoExample { + + import opened Io + import opened NativeTypes + + /* Useful to convert Dafny strings into arrays of characters. */ + method ArrayFromSeq(s: seq) returns (a: array) + ensures a[..] == s + { + a := new A[|s|] ( i requires 0 <= i < |s| => s[i] ); + } + + method {:main} Main(ghost env: HostEnvironment) + requires env.ok.ok() + modifies env.ok + { + var fname := ArrayFromSeq("foo.txt"); + var f: FileStream; + var ok: bool; + + var numArgs := HostConstants.NumCommandLineArgs(env); + if numArgs < 1 { + print "Error: invalid number of command line arguments\n"; + return; + } + print "# command line args: "; + print numArgs; + print "\n"; + + var arg0 := HostConstants.GetCommandLineArg(0, env); + print "command: " + arg0[..] + "\n"; + + var fileExists := FileStream.FileExists(fname, env); + if fileExists { + print fname[..] + " exists!\n"; + + var ok, len := FileStream.FileLength(fname, env); + if !ok { print "Error: invalid file length\n"; return; } + print fname[..] + " length: "; + print len; + print "\n"; + } + + ok, f := FileStream.Open(fname, env); + if !ok { print "Error: open failed\n"; return; } + + /* This is "hello world!" in ascii. */ + var data: array := ArrayFromSeq([104, 101, 108, 108, 111, 32, 119, 111, 114, 108, 100, 33, 10]); + + ok := f.Write(0, data, 0, data.Length as int32); + if !ok { print "Error: write failed\n"; return; } + + ok := f.Close(); + + print "done!\n"; + } + +} diff --git a/examples/Io/IoExample.dfy.expect b/examples/Io/IoExample.dfy.expect new file mode 100644 index 00000000..ba00363f --- /dev/null +++ b/examples/Io/IoExample.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors diff --git a/examples/NatSeq/NatSeqExample.dfy b/examples/NatSeq/NatSeqExample.dfy new file mode 100644 index 00000000..9b742b81 --- /dev/null +++ b/examples/NatSeq/NatSeqExample.dfy @@ -0,0 +1,38 @@ +// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../../src/Collections/Sequences/NatSeqConversions.dfy" + +module NatSeqExample { + + import opened Uint8_32 + + method Main() { + var n := 49602234234; + + // Convert n to uint8 and uint32 sequences + var smallSeq, largeSeq := Small.FromNat(n), Large.FromNat(n); + + Small.LemmaNatSeqNat(n); + Large.LemmaNatSeqNat(n); + assert Small.ToNat(smallSeq) == Large.ToNat(largeSeq) == n; + + // Extend smallSeq + smallSeq := Small.SeqExtendMultiple(smallSeq, E()); + assert Small.ToNat(smallSeq) == n; + + // Convert between smallSeqExtended and largeSeq + LemmaToSmall(largeSeq); + LemmaToLarge(smallSeq); + assert Small.ToNat(ToSmall(largeSeq)) == n; + assert Large.ToNat(ToLarge(smallSeq)) == n; + assert |ToSmall(largeSeq)| == |largeSeq| * E(); + assert |ToLarge(smallSeq)| == |smallSeq| / E(); + + LemmaSmallLargeSmall(smallSeq); + LemmaLargeSmallLarge(largeSeq); + assert ToSmall(ToLarge(smallSeq)) == smallSeq; + assert ToLarge(ToSmall(largeSeq)) == largeSeq; + } + +} diff --git a/examples/NatSeq/NatSeqExample.dfy.expect b/examples/NatSeq/NatSeqExample.dfy.expect new file mode 100644 index 00000000..823a60a1 --- /dev/null +++ b/examples/NatSeq/NatSeqExample.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 1 verified, 0 errors diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/NatSeq.dfy new file mode 100644 index 00000000..359267df --- /dev/null +++ b/src/Collections/Sequences/NatSeq.dfy @@ -0,0 +1,595 @@ +// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +/* The first element of a sequence is the least significant word; the last +element is the most significant word. */ + +include "../../NonlinearArithmetic/DivMod.dfy" +include "../../NonlinearArithmetic/Mul.dfy" +include "../../NonlinearArithmetic/Power.dfy" +include "Seq.dfy" + +abstract module NatSeq { + + import opened DivMod + import opened Mul + import opened Power + import opened Seq + + /* Upper bound of a word */ + function method BOUND(): nat + ensures BOUND() > 1 + + type uint = i: int | 0 <= i < BOUND() + + ////////////////////////////////////////////////////////////////////////////// + // + // ToNat definition and lemmas + // + ////////////////////////////////////////////////////////////////////////////// + + /* Converts a sequence to a nat beginning from the least significant word. */ + function method {:opaque} ToNat(xs: seq): nat + { + if |xs| == 0 then 0 + else + LemmaMulNonnegativeAuto(); + ToNat(DropFirst(xs)) * BOUND() + First(xs) + } + + /* Converts a sequence to a nat beginning from the most significant word. */ + function method {:opaque} ToNatRev(xs: seq): nat + { + if |xs| == 0 then 0 + else + LemmaPowPositiveAuto(); + LemmaMulNonnegativeAuto(); + ToNatRev(DropLast(xs)) + Last(xs) * Pow(BOUND(), |xs| - 1) + } + + /* Given the same sequence, ToNat and ToNatRev return the same nat. */ + lemma LemmaToNatEqToNatRev(xs: seq) + ensures ToNat(xs) == ToNatRev(xs) + { + reveal ToNat(); + reveal ToNatRev(); + if xs == [] { + } else { + if DropLast(xs) == [] { + calc { + ToNatRev(xs); + Last(xs) * Pow(BOUND(), |xs| - 1); + { LemmaPow0Auto(); } + ToNat(xs); + } + } else { + calc { + ToNatRev(xs); + ToNatRev(DropLast(xs)) + Last(xs) * Pow(BOUND(), |xs| - 1); + { LemmaToNatEqToNatRev(DropLast(xs)); } + ToNat(DropLast(xs)) + Last(xs) * Pow(BOUND(), |xs| - 1); + ToNat(DropFirst(DropLast(xs))) * BOUND() + First(xs) + Last(xs) + * Pow(BOUND(), |xs| - 1); + { LemmaToNatEqToNatRev(DropFirst(DropLast(xs))); } + ToNatRev(DropFirst(DropLast(xs))) * BOUND() + First(xs) + Last(xs) + * Pow(BOUND(), |xs| - 1); + { + assert DropFirst(DropLast(xs)) == DropLast(DropFirst(xs)); + reveal Pow(); + LemmaMulProperties(); + } + ToNatRev(DropLast(DropFirst(xs))) * BOUND() + First(xs) + Last(xs) + * Pow(BOUND(), |xs| - 2) * BOUND(); + { LemmaMulIsDistributiveAddOtherWayAuto(); } + ToNatRev(DropFirst(xs)) * BOUND() + First(xs); + { LemmaToNatEqToNatRev(DropFirst(xs)); } + ToNat(xs); + } + } + } + } + + lemma LemmaToNatEqToNatRevAuto() + ensures forall xs: seq {:trigger ToNatRev(xs)}{:trigger ToNat(xs)} + :: ToNat(xs) == ToNatRev(xs) + { + reveal ToNat(); + reveal ToNatRev(); + forall xs: seq {:trigger ToNatRev(xs)}{:trigger ToNat(xs)} + ensures ToNat(xs) == ToNatRev(xs) + { + LemmaToNatEqToNatRev(xs); + } + } + + /* The nat representation of a sequence of length 1 is its first (and only) + word. */ + lemma LemmaSeqLen1(xs: seq) + requires |xs| == 1 + ensures ToNat(xs) == First(xs) + { + reveal ToNat(); + } + + /* The nat representation of a sequence of length 2 is sum of its first + word and the product of its second word and BOUND(). */ + lemma LemmaSeqLen2(xs: seq) + requires |xs| == 2 + ensures ToNat(xs) == First(xs) + xs[1] * BOUND() + { + reveal ToNat(); + LemmaSeqLen1(DropLast(xs)); + } + + /* Appending a zero does not change the nat representation of the sequence. */ + lemma LemmaSeqAppendZero(xs: seq) + ensures ToNat(xs + [0]) == ToNat(xs) + { + reveal ToNatRev(); + LemmaToNatEqToNatRevAuto(); + calc == { + ToNat(xs + [0]); + ToNatRev(xs + [0]); + ToNatRev(xs) + 0 * Pow(BOUND(), |xs|); + { LemmaMulBasicsAuto(); } + ToNatRev(xs); + ToNat(xs); + } + } + + /* The nat representation of a sequence is bounded by BOUND() to the power of + the sequence length. */ + lemma LemmaSeqNatBound(xs: seq) + ensures ToNat(xs) < Pow(BOUND(), |xs|) + { + reveal Pow(); + if |xs| == 0 { + reveal ToNat(); + } else { + var len' := |xs| - 1; + var pow := Pow(BOUND(), len'); + calc { + ToNat(xs); + { LemmaToNatEqToNatRev(xs); } + ToNatRev(xs); + { reveal ToNatRev(); } + ToNatRev(DropLast(xs)) + Last(xs) * pow; + < { + LemmaToNatEqToNatRev(DropLast(xs)); + LemmaSeqNatBound(DropLast(xs)); + } + pow + Last(xs) * pow; + <= { + LemmaPowPositiveAuto(); + LemmaMulInequalityAuto(); + } + pow + (BOUND() - 1) * pow; + { LemmaMulIsDistributiveAuto(); } + Pow(BOUND(), len' + 1); + } + } + } + + /* The nat representation of a sequence can be calculated using the nat + representation of its prefix. */ + lemma LemmaSeqPrefix(xs: seq, i: nat) + requires 0 <= i <= |xs| + ensures ToNat(xs[..i]) + ToNat(xs[i..]) * Pow(BOUND(), i) == ToNat(xs) + { + reveal ToNat(); + reveal Pow(); + if i == 1 { + assert ToNat(xs[..1]) == First(xs); + } else if i > 1 { + calc { + ToNat(xs[..i]) + ToNat(xs[i..]) * Pow(BOUND(), i); + ToNat(DropFirst(xs[..i])) * BOUND() + First(xs) + ToNat(xs[i..]) * Pow(BOUND(), i); + { + assert DropFirst(xs[..i]) == DropFirst(xs)[..i-1]; + LemmaMulProperties(); + } + ToNat(DropFirst(xs)[..i-1]) * BOUND() + First(xs) + (ToNat(xs[i..]) * Pow(BOUND(), i - 1)) * BOUND(); + { LemmaMulIsDistributiveAddOtherWayAuto(); } + (ToNat(DropFirst(xs)[..i-1]) + ToNat(DropFirst(xs)[i-1..]) * Pow(BOUND(), i - 1)) * BOUND() + First(xs); + { LemmaSeqPrefix(DropFirst(xs), i - 1); } + ToNat(xs); + } + } + } + + /* If there is an inequality between the most significant words of two + sequences, then there is an inequality between the nat representations of + those sequences. Helper lemma for LemmaSeqNeq. */ + lemma LemmaSeqMswInequality(xs: seq, ys: seq) + requires |xs| == |ys| > 0 + requires Last(xs) < Last(ys) + ensures ToNat(xs) < ToNat(ys) + { + reveal ToNatRev(); + LemmaToNatEqToNatRevAuto(); + var len' := |xs| - 1; + calc { + ToNat(xs); + ToNatRev(xs); + < { LemmaSeqNatBound(DropLast(xs)); } + Pow(BOUND(), len') + Last(xs) * Pow(BOUND(), len'); + == { LemmaMulIsDistributiveAuto(); } + (1 + Last(xs)) * Pow(BOUND(), len'); + <= { LemmaPowPositiveAuto(); LemmaMulInequalityAuto(); } + ToNatRev(ys); + ToNat(ys); + } + } + + /* Two sequences do not have the same nat representations if their prefixes + do not have the same nat representations. Helper lemma for LemmaSeqNeq. */ + lemma LemmaSeqPrefixNeq(xs: seq, ys: seq, i: nat) + requires 0 <= i <= |xs| == |ys| + requires ToNat(xs[..i]) != ToNat(ys[..i]) + ensures ToNat(xs) != ToNat(ys) + decreases |xs| - i + { + if i == |xs| { + assert xs[..i] == xs; + assert ys[..i] == ys; + } else { + if xs[i] == ys[i] { + reveal ToNatRev(); + assert DropLast(xs[..i+1]) == xs[..i]; + assert DropLast(ys[..i+1]) == ys[..i]; + + LemmaToNatEqToNatRevAuto(); + assert ToNat(xs[..i+1]) == ToNatRev(xs[..i+1]); + } else { + if xs[i] < ys[i] { LemmaSeqMswInequality(xs[..i+1], ys[..i+1]); } + else { LemmaSeqMswInequality(ys[..i+1], xs[..i+1]); } + } + LemmaSeqPrefixNeq(xs, ys, i + 1); + } + } + + /* If two sequences of the same length are not equal, their nat + representations are not equal. */ + lemma LemmaSeqNeq(xs: seq, ys: seq) + requires |xs| == |ys| + requires xs != ys + ensures ToNat(xs) != ToNat(ys) + { + ghost var i: nat, n: nat := 0, |xs|; + + while i < n + invariant 0 <= i < n + invariant xs[..i] == ys[..i] + { + if xs[i] != ys[i] { + break; + } + i := i + 1; + } + assert ToNatRev(xs[..i]) == ToNatRev(ys[..i]); + + reveal ToNatRev(); + assert xs[..i+1][..i] == xs[..i]; + assert ys[..i+1][..i] == ys[..i]; + LemmaPowPositiveAuto(); + LemmaMulStrictInequalityAuto(); + assert ToNatRev(xs[..i+1]) != ToNatRev(ys[..i+1]); + LemmaToNatEqToNatRevAuto(); + + LemmaSeqPrefixNeq(xs, ys, i+1); + } + + /* If the nat representations of two sequences of the same length are equal + to each other, the sequences are the same. */ + lemma LemmaSeqEq(xs: seq, ys: seq) + requires |xs| == |ys| + requires ToNat(xs) == ToNat(ys) + ensures xs == ys + { + calc ==> { + xs != ys; + { LemmaSeqNeq(xs, ys); } + ToNat(xs) != ToNat(ys); + false; + } + } + + /* The nat representation of a sequence and its least significant word are + congruent. */ + lemma LemmaSeqLswModEquivalence(xs: seq) + requires |xs| >= 1; + ensures IsModEquivalent(ToNat(xs), First(xs), BOUND()); + { + if |xs| == 1 { + LemmaSeqLen1(xs); + LemmaModEquivalenceAuto(); + } else { + assert IsModEquivalent(ToNat(xs), First(xs), BOUND()) by { + reveal ToNat(); + calc ==> { + true; + { LemmaModEquivalenceAuto(); } + IsModEquivalent(ToNat(xs), ToNat(DropFirst(xs)) * BOUND() + First(xs), BOUND()); + { LemmaModMultiplesBasicAuto(); } + IsModEquivalent(ToNat(xs), First(xs), BOUND()); + } + } + } + } + + ////////////////////////////////////////////////////////////////////////////// + // + // FromNat definition and lemmas + // + ////////////////////////////////////////////////////////////////////////////// + + /* Converts a nat to a sequence. */ + function method {:opaque} FromNat(n: nat): (xs: seq) + { + if n == 0 then [] + else + LemmaDivBasicsAuto(); + LemmaDivDecreasesAuto(); + [n % BOUND()] + FromNat(n / BOUND()) + } + + /* Ensures length of the sequence generated by FromNat is less than len. + Helper lemma for FromNatWithLen. */ + lemma LemmaFromNatLen(n: nat, len: nat) + requires Pow(BOUND(), len) > n + ensures |FromNat(n)| <= len + decreases n + { + reveal FromNat(); + if n == 0 { + } else { + calc { + |FromNat(n)|; + == { LemmaDivBasicsAuto(); } + 1 + |FromNat(n / BOUND())|; + <= { + LemmaMultiplyDivideLtAuto(); + LemmaDivDecreasesAuto(); + reveal Pow(); + LemmaFromNatLen(n / BOUND(), len - 1); + } + len; + } + } + } + + /* If we start with a nat, convert it to a sequence, and convert it back, we + get the same nat we started with. */ + lemma LemmaNatSeqNat(n: nat) + ensures ToNat(FromNat(n)) == n + decreases n + { + reveal ToNat(); + reveal FromNat(); + if n == 0 { + } else { + calc { + ToNat(FromNat(n)); + { LemmaDivBasicsAuto(); } + ToNat([n % BOUND()] + FromNat(n / BOUND())); + n % BOUND() + ToNat(FromNat(n / BOUND())) * BOUND(); + { + LemmaDivDecreasesAuto(); + LemmaNatSeqNat(n / BOUND()); + } + n % BOUND() + n / BOUND() * BOUND(); + { LemmaFundamentalDivMod(n, BOUND()); } + n; + } + } + } + + /* Extends a sequence to a specified length. */ + function method {:opaque} SeqExtend(xs: seq, n: nat): (ys: seq) + requires |xs| <= n + ensures |ys| == n + ensures ToNat(ys) == ToNat(xs) + decreases n - |xs| + { + if |xs| >= n then xs else LemmaSeqAppendZero(xs); SeqExtend(xs + [0], n) + } + + /* Extends a sequence to a length that is a multiple of n. */ + function method {:opaque} SeqExtendMultiple(xs: seq, n: nat): (ys: seq) + requires n > 0 + ensures |ys| % n == 0 + ensures ToNat(ys) == ToNat(xs) + { + var newLen := |xs| + n - (|xs| % n); + LemmaSubModNoopRight(|xs| + n, |xs|, n); + LemmaModBasicsAuto(); + assert newLen % n == 0; + + LemmaSeqNatBound(xs); + LemmaPowIncreasesAuto(); + SeqExtend(xs, newLen) + } + + /* Converts a nat to a sequence of a specified length. */ + function method {:opaque} FromNatWithLen(n: nat, len: nat): (xs: seq) + requires Pow(BOUND(), len) > n + ensures |xs| == len + ensures ToNat(xs) == n + { + LemmaFromNatLen(n, len); + LemmaNatSeqNat(n); + SeqExtend(FromNat(n), len) + } + + /* If the nat representation of a sequence is zero, then the sequence is a + sequence of zeros. */ + lemma LemmaSeqZero(xs: seq) + requires ToNat(xs) == 0 + ensures forall i {:trigger xs[i]} :: 0 <= i < |xs| ==> xs[i] == 0 + { + reveal ToNat(); + if |xs| == 0 { + } else { + LemmaMulNonnegativeAuto(); + assert First(xs) == 0; + + LemmaMulNonzeroAuto(); + LemmaSeqZero(DropFirst(xs)); + } + } + + /* Generates a sequence of zeros of a specified length. */ + function method {:opaque} SeqZero(len: nat): (xs: seq) + ensures |xs| == len + ensures forall i {:trigger xs[i]} :: 0 <= i < |xs| ==> xs[i] == 0 + ensures ToNat(xs) == 0 + { + LemmaPowPositive(BOUND(), len); + var xs := FromNatWithLen(0, len); + LemmaSeqZero(xs); + xs + } + + /* If we start with a sequence, convert it to a nat, and convert it back to a + sequence with the same length as the original sequence, we get the same + sequence we started with. */ + lemma LemmaSeqNatSeq(xs: seq) + ensures Pow(BOUND(), |xs|) > ToNat(xs) + ensures FromNatWithLen(ToNat(xs), |xs|) == xs + { + reveal FromNat(); + reveal ToNat(); + LemmaSeqNatBound(xs); + if |xs| > 0 { + calc { + FromNatWithLen(ToNat(xs), |xs|) != xs; + { LemmaSeqNeq(FromNatWithLen(ToNat(xs), |xs|), xs); } + ToNat(FromNatWithLen(ToNat(xs), |xs|)) != ToNat(xs); + ToNat(xs) != ToNat(xs); + false; + } + } + } + + ////////////////////////////////////////////////////////////////////////////// + // + // Addition and subtraction + // + ////////////////////////////////////////////////////////////////////////////// + + /* Adds two sequences. */ + function method {:opaque} SeqAdd(xs: seq, ys: seq): (seq, nat) + requires |xs| == |ys| + ensures var (zs, cout) := SeqAdd(xs, ys); + |zs| == |xs| && 0 <= cout <= 1 + decreases xs + { + if |xs| == 0 then ([], 0) + else + var (zs', cin) := SeqAdd(DropLast(xs), DropLast(ys)); + var sum: int := Last(xs) + Last(ys) + cin; + var (sum_out, cout) := if sum < BOUND() then (sum, 0) + else (sum - BOUND(), 1); + (zs' + [sum_out], cout) + } + + /* SeqAdd returns the same value as converting the sequences to nats, then + adding them. */ + lemma LemmaSeqAdd(xs: seq, ys: seq, zs: seq, cout: nat) + requires |xs| == |ys| + requires SeqAdd(xs, ys) == (zs, cout) + ensures ToNat(xs) + ToNat(ys) == ToNat(zs) + cout * Pow(BOUND(), |xs|) + { + reveal SeqAdd(); + if |xs| == 0 { + reveal ToNat(); + } else { + var pow := Pow(BOUND(), |xs| - 1); + var (zs', cin) := SeqAdd(DropLast(xs), DropLast(ys)); + var sum: int := Last(xs) + Last(ys) + cin; + var z := if sum < BOUND() then sum else sum - BOUND(); + assert sum == z + cout * BOUND(); + + reveal ToNatRev(); + LemmaToNatEqToNatRevAuto(); + calc { + ToNat(zs); + ToNatRev(zs); + ToNatRev(zs') + z * pow; + { LemmaSeqAdd(DropLast(xs), DropLast(ys), zs', cin); } + ToNatRev(DropLast(xs)) + ToNatRev(DropLast(ys)) - cin * pow + z * pow; + { + LemmaMulEqualityAuto(); + assert sum * pow == (z + cout * BOUND()) * pow; + LemmaMulIsDistributiveAuto(); + } + ToNatRev(xs) + ToNatRev(ys) - cout * BOUND() * pow; + { + LemmaMulIsAssociative(cout, BOUND(), pow); + reveal Pow(); + } + ToNatRev(xs) + ToNatRev(ys) - cout * Pow(BOUND(), |xs|); + ToNat(xs) + ToNat(ys) - cout * Pow(BOUND(), |xs|); + } + } + } + + /* Subtracts two sequences. */ + function method {:opaque} SeqSub(xs: seq, ys: seq): (seq, nat) + requires |xs| == |ys| + ensures var (zs, cout) := SeqSub(xs, ys); + |zs| == |xs| && 0 <= cout <= 1 + decreases xs + { + if |xs| == 0 then ([], 0) + else + var (zs, cin) := SeqSub(DropLast(xs), DropLast(ys)); + var (diff_out, cout) := if Last(xs) >= Last(ys) + cin + then (Last(xs) - Last(ys) - cin, 0) + else (BOUND() + Last(xs) - Last(ys) - cin, 1); + (zs + [diff_out], cout) + } + + /* SeqSub returns the same value as converting the sequences to nats, then + subtracting them. */ + lemma LemmaSeqSub(xs: seq, ys: seq, zs: seq, cout: nat) + requires |xs| == |ys| + requires SeqSub(xs, ys) == (zs, cout) + ensures ToNat(xs) - ToNat(ys) + cout * Pow(BOUND(), |xs|) == ToNat(zs) + { + reveal SeqSub(); + if |xs| == 0 { + reveal ToNat(); + } else { + var pow := Pow(BOUND(), |xs| - 1); + var (zs', cin) := SeqSub(DropLast(xs), DropLast(ys)); + var z := if Last(xs) >= Last(ys) + cin + then Last(xs) - Last(ys) - cin + else BOUND() + Last(xs) - Last(ys) - cin; + assert cout * BOUND() + Last(xs) - cin - Last(ys) == z; + + reveal ToNatRev(); + LemmaToNatEqToNatRevAuto(); + calc { + ToNat(zs); + ToNatRev(zs); + ToNatRev(zs') + z * pow; + { LemmaSeqSub(DropLast(xs), DropLast(ys), zs', cin); } + ToNatRev(DropLast(xs)) - ToNatRev(DropLast(ys)) + cin * pow + z * pow; + { + LemmaMulEqualityAuto(); + assert pow * (cout * BOUND() + Last(xs) - cin - Last(ys)) == pow * z; + LemmaMulIsDistributiveAuto(); + } + ToNatRev(xs) - ToNatRev(ys) + cout * BOUND() * pow; + { + LemmaMulIsAssociative(cout, BOUND(), pow); + reveal Pow(); + } + ToNatRev(xs) - ToNatRev(ys) + cout * Pow(BOUND(), |xs|); + ToNat(xs) - ToNat(ys) + cout * Pow(BOUND(), |xs|); + } + } + } + +} diff --git a/src/Collections/Sequences/NatSeq.dfy.expect b/src/Collections/Sequences/NatSeq.dfy.expect new file mode 100644 index 00000000..bba7f9e6 --- /dev/null +++ b/src/Collections/Sequences/NatSeq.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 41 verified, 0 errors diff --git a/src/Collections/Sequences/NatSeqConversions.dfy b/src/Collections/Sequences/NatSeqConversions.dfy new file mode 100644 index 00000000..c8036867 --- /dev/null +++ b/src/Collections/Sequences/NatSeqConversions.dfy @@ -0,0 +1,300 @@ +// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../../NonlinearArithmetic/DivMod.dfy" +include "../../NonlinearArithmetic/Mul.dfy" +include "../../NonlinearArithmetic/Power.dfy" +include "Seq.dfy" +include "NatSeq.dfy" + +/* Sequence with smaller bound. */ +abstract module SmallSeq refines NatSeq { + + function method BITS(): nat + ensures BITS() > 1 + + function method BOUND(): nat + { + LemmaPowPositive(2, BITS() - 1); + LemmaPowStrictlyIncreases(2, BITS() - 1, BITS()); + Pow(2, BITS()) + } + +} + +/* Sequence with larger bound. */ +abstract module LargeSeq refines NatSeq { + + import Small : SmallSeq + + function method BITS(): nat + ensures BITS() > Small.BITS() && BITS() % Small.BITS() == 0 + + function method BOUND(): nat + { + LemmaPowPositive(2, BITS() - 1); + LemmaPowStrictlyIncreases(2, BITS() - 1, BITS()); + Pow(2, BITS()) + } + +} + +abstract module NatSeqConversions { + + import opened DivMod + import opened Mul + import opened Power + import opened Seq + + import opened Large : LargeSeq + + /* Small.BOUND() to the power of E is Large.BOUND(). */ + function method E(): (E: nat) + ensures Pow(Small.BOUND(), E) == Large.BOUND() + ensures E > 0 + { + LemmaDivBasicsAuto(); + LemmaPowMultipliesAuto(); + LemmaFundamentalDivMod(Large.BITS(), Small.BITS()); + Large.BITS() / Small.BITS() + } + + /* Converts a sequence from Large.BOUND() to Small.BOUND(). */ + function method {:opaque} ToSmall(xs: seq): (ys: seq) + ensures |ys| == |xs| * E() + { + if |xs| == 0 then [] + else + LemmaMulIsDistributiveAddOtherWay(E(), 1, |xs| - 1); + Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs)) + } + + /* Converts a sequence from Small.BOUND() to Large.BOUND(). */ + function method {:opaque} ToLarge(xs: seq): (ys: seq) + requires |xs| % E() == 0 + ensures |ys| == |xs| / E() + { + if |xs| == 0 then LemmaDivBasicsAuto(); [] + else + LemmaModIsZero(|xs|, E()); + assert |xs| >= E(); + + Small.LemmaSeqNatBound(xs[..E()]); + LemmaModSubMultiplesVanishAuto(); + LemmaDivMinusOne(|xs|, E()); + [Small.ToNat(xs[..E()]) as Large.uint] + ToLarge(xs[E()..]) + } + + /* Sequence conversion from Large.BOUND() to Small.BOUND() does not + change its nat representation. */ + lemma LemmaToSmall(xs: seq) + ensures Small.ToNat(ToSmall(xs)) == Large.ToNat(xs) + { + reveal Small.ToNat(); + reveal Large.ToNat(); + reveal ToSmall(); + if |xs| == 0 { + } else { + calc { + Small.ToNat(ToSmall(xs)); + Small.ToNat(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); + { + Small.LemmaSeqPrefix(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs)), E()); + LemmaToSmall(DropFirst(xs)); + } + First(xs) + Large.ToNat(DropFirst(xs)) * Pow(Small.BOUND(), E()); + { assert Pow(Small.BOUND(), E()) == Large.BOUND(); } + Large.ToNat(xs); + } + } + } + + /* Sequence conversion from Small.BOUND() to Large.BOUND() does not + change its nat representation. */ + lemma LemmaToLarge(xs: seq) + requires |xs| % E() == 0 + ensures Large.ToNat(ToLarge(xs)) == Small.ToNat(xs) + { + reveal Large.ToNat(); + reveal Small.ToNat(); + reveal ToLarge(); + if |xs| == 0 { + } else { + calc { + Large.ToNat(ToLarge(xs)); + { + LemmaModIsZero(|xs|, E()); + LemmaModSubMultiplesVanishAuto(); + Small.LemmaSeqNatBound(xs[..E()]); + } + Large.ToNat([Small.ToNat(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); + { LemmaToLarge(xs[E()..]); } + Small.ToNat(xs[..E()]) + Small.ToNat(xs[E()..]) * Pow(Small.BOUND(), E()); + { Small.LemmaSeqPrefix(xs, E()); } + Small.ToNat(xs); + } + } + } + + /* ToSmall is injective. */ + lemma LemmaToSmallIsInjective(xs: seq, ys: seq) + requires ToSmall(xs) == ToSmall(ys) + requires |xs| == |ys| + ensures xs == ys + { + LemmaToSmall(xs); + LemmaToSmall(ys); + assert Large.ToNat(xs) == Large.ToNat(ys); + Large.LemmaSeqEq(xs, ys); + } + + /* ToLarge is injective. */ + lemma LemmaToLargeIsInjective(xs: seq, ys: seq) + requires |xs| % E() == |ys| % E() == 0 + requires ToLarge(xs) == ToLarge(ys) + requires |xs| == |ys| + ensures xs == ys + { + LemmaToLarge(xs); + LemmaToLarge(ys); + assert Small.ToNat(xs) == Small.ToNat(ys); + Small.LemmaSeqEq(xs, ys); + } + + /* If we start with a Small sequence, convert it to a Large sequence, + and convert it back, we get the same sequence we started with. */ + lemma LemmaSmallLargeSmall(xs: seq) + requires |xs| % E() == 0 + ensures ToSmall(ToLarge(xs)) == xs + { + reveal ToSmall(); + reveal ToLarge(); + if |xs| == 0 { + } else { + calc { + ToSmall(ToLarge(xs)); + { + LemmaModIsZero(|xs|, E()); + Small.LemmaSeqNatBound(xs[..E()]); + LemmaModSubMultiplesVanishAuto(); + } + ToSmall([Small.ToNat(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); + Small.FromNatWithLen(Small.ToNat(xs[..E()]), E()) + ToSmall(ToLarge(xs[E()..])); + { + Small.LemmaSeqNatSeq(xs[..E()]); + LemmaSmallLargeSmall(xs[E()..]); + } + xs; + } + } + } + + /* If we start with a Large sequence, convert it to a Sequence sequence, + and convert it back, we get the same sequence we started with. */ + lemma LemmaLargeSmallLarge(xs: seq) + ensures |ToSmall(xs)| % E() == 0 + ensures ToLarge(ToSmall(xs)) == xs + { + reveal ToSmall(); + reveal ToLarge(); + LemmaModMultiplesBasicAuto(); + if |xs| == 0 { + } else { + calc { + ToLarge(ToSmall(xs)); + ToLarge(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); + [Small.ToNat(Small.FromNatWithLen(First(xs), E())) as Large.uint] + ToLarge(ToSmall(DropFirst(xs))); + [First(xs)] + ToLarge(ToSmall(DropFirst(xs))); + { LemmaLargeSmallLarge(DropFirst(xs)); } + [First(xs)] + DropFirst(xs); + xs; + } + } + } + +} + +/* Conversions between sequences of uint8 and uint16. */ +module Uint8_16 refines NatSeqConversions { + + module Uint8Seq refines SmallSeq { + function method BITS(): nat { 8 } + } + + module Uint16Seq refines LargeSeq { + import Small = Uint8Seq + function method BITS(): nat { 16 } + } + + import opened Large = Uint16Seq + import Small = Large.Small + +} + +/* Conversions between sequences of uint8 and uint32. */ +module Uint8_32 refines NatSeqConversions { + + module Uint8Seq refines SmallSeq { + function method BITS(): nat { 8 } + } + + module Uint32Seq refines LargeSeq { + import Small = Uint8Seq + function method BITS(): nat { 32 } + } + + import opened Large = Uint32Seq + import Small = Large.Small + +} + +/* Conversions between sequences of uint8 and uint64. */ +module Uint8_64 refines NatSeqConversions { + + module Uint8Seq refines SmallSeq { + function method BITS(): nat { 8 } + } + + module Uint64Seq refines LargeSeq { + import Small = Uint8Seq + function method BITS(): nat { 64 } + } + + import opened Large = Uint64Seq + import Small = Large.Small + +} + +/* Conversions between sequences of uint16 and uint32. */ +module Uint16_32 refines NatSeqConversions { + + module Uint16Seq refines SmallSeq { + function method BITS(): nat { 16 } + } + + module Uint32Seq refines LargeSeq { + import Small = Uint16Seq + function method BITS(): nat { 32 } + } + + import opened Large = Uint32Seq + import Small = Large.Small + +} + +/* Conversions between sequences of uint32 and uint64. */ +module Uint32_64 refines NatSeqConversions { + + module Uint32Seq refines SmallSeq { + function method BITS(): nat { 32 } + } + + module Uint64Seq refines LargeSeq { + import Small = Uint32Seq + function method BITS(): nat { 64 } + } + + import opened Large = Uint64Seq + import Small = Large.Small + +} diff --git a/src/Collections/Sequences/NatSeqConversions.dfy.expect b/src/Collections/Sequences/NatSeqConversions.dfy.expect new file mode 100644 index 00000000..856160c0 --- /dev/null +++ b/src/Collections/Sequences/NatSeqConversions.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 456 verified, 0 errors diff --git a/src/Io/Io.dfy b/src/Io/Io.dfy new file mode 100644 index 00000000..2aa259df --- /dev/null +++ b/src/Io/Io.dfy @@ -0,0 +1,128 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../NativeTypes.dfy" + +module {:extern "IoNative"} Io { + + import opened NativeTypes + + ////////////////////////////////////////////////////////////////////////////// + // Per-host constants + ////////////////////////////////////////////////////////////////////////////// + + class HostConstants + { + constructor {:extern} () requires false + + /* Result of C# System.Environment.GetCommandLineArgs(); argument 0 is name + of executable. */ + function {:extern} CommandLineArgs(): seq reads this + + static method {:extern} NumCommandLineArgs(ghost env: HostEnvironment) returns (n: uint32) + ensures n as int == |env.constants.CommandLineArgs()| + + static method {:extern} GetCommandLineArg(i: uint64, ghost env: HostEnvironment) returns (arg: array) + requires 0 <= i as int < |env.constants.CommandLineArgs()| + ensures arg[..] == env.constants.CommandLineArgs()[i] + } + + ////////////////////////////////////////////////////////////////////////////// + // Failure + ////////////////////////////////////////////////////////////////////////////// + + class OkState + { + constructor {:extern} () requires false + function {:extern} ok(): bool reads this + } + + ////////////////////////////////////////////////////////////////////////////// + // File System + ////////////////////////////////////////////////////////////////////////////// + + class FileSystemState + { + constructor {:extern} () requires false + + /* File system maps file names to their contents. */ + function {:extern} state(): map> + reads this + } + + class HostEnvironment + { + ghost var constants: HostConstants + ghost var ok: OkState + ghost var files: FileSystemState + } + + class FileStream + { + ghost var env: HostEnvironment + function {:extern} Name(): string reads this + function {:extern} IsOpen(): bool reads this + constructor {:extern} () requires false + + static method {:extern} FileExists(name: array, ghost env: HostEnvironment) returns (result: bool) + requires env.ok.ok() + ensures result <==> old(name[..]) in env.files.state() + + static method {:extern} FileLength(name: array, ghost env: HostEnvironment) returns (success: bool, len: int32) + requires env.ok.ok() + requires name[..] in env.files.state() + modifies env.ok + ensures env.ok.ok() == success + ensures success ==> len as int == |env.files.state()[name[..]]| + + static method {:extern} Open(name: array, ghost env: HostEnvironment) + returns (ok: bool, f: FileStream) + requires env.ok.ok() + modifies env.ok + ensures env.ok.ok() == ok + ensures ok ==> fresh(f) && f.env == env && f.IsOpen() && f.Name() == name[..] + + method {:extern} Close() returns (ok: bool) + requires env.ok.ok() + requires IsOpen() + modifies this + modifies env.ok + ensures env == old(env) + ensures env.ok.ok() == ok + + method {:extern} Read(fileOffset: nat32, buffer: array, start: int32, end: int32) returns (ok: bool) + requires env.ok.ok() + requires IsOpen() + requires 0 <= start as int <= end as int <= buffer.Length + modifies this + modifies env.ok + modifies buffer + ensures env == old(env) + ensures env.ok.ok() == ok + ensures Name() == old(Name()) + ensures forall i:int :: 0 <= i < buffer.Length && !(start as int <= i < end as int) ==> buffer[i] == old(buffer[i]) + ensures ok ==> IsOpen() + + method {:extern} Write(fileOffset: nat32, buffer: array, start: int32, end: int32) returns (ok: bool) + requires env.ok.ok() + requires IsOpen() + requires 0 <= start as int <= end as int <= buffer.Length + modifies this + modifies env.ok + ensures env == old(env) + ensures env.ok.ok() == ok + ensures Name() == old(Name()) + ensures ok ==> IsOpen() + + method {:extern} Flush() returns (ok: bool) + requires env.ok.ok() + requires IsOpen() + modifies this + modifies env.ok + ensures env == old(env) + ensures env.ok.ok() == ok + ensures Name() == old(Name()) + ensures ok ==> IsOpen() + } + +} diff --git a/src/Io/Io.dfy.expect b/src/Io/Io.dfy.expect new file mode 100644 index 00000000..0825601c --- /dev/null +++ b/src/Io/Io.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 9 verified, 0 errors diff --git a/src/Io/IoNative.cs b/src/Io/IoNative.cs new file mode 100644 index 00000000..0167b318 --- /dev/null +++ b/src/Io/IoNative.cs @@ -0,0 +1,113 @@ +using System; +using FStream = System.IO.FileStream; + +namespace @IoNative { + +public partial class HostConstants +{ + public static uint NumCommandLineArgs() + { + return (uint)System.Environment.GetCommandLineArgs().Length; + } + + public static char[] GetCommandLineArg(ulong i) + { + return System.Environment.GetCommandLineArgs()[i].ToCharArray(); + } +} + +public partial class FileStream +{ + internal FStream fstream; + internal FileStream(FStream fstream) { this.fstream = fstream; } + + public static bool FileExists(char[] name) + { + return System.IO.File.Exists(new string(name)); + } + + public static void FileLength(char[] name, out bool success, out int len) + { + len = -1; + try { + System.IO.FileInfo fi = new System.IO.FileInfo(new string(name)); + if (fi.Length < System.Int32.MaxValue) { // We only support small files + len = (int)fi.Length; + success = true; + } + else { + success = false; + } + + } + catch (Exception e) { + System.Console.Error.WriteLine(e); + success = false; + } + } + + public static void Open(char[] name, out bool ok, out FileStream f) + { + try { + f = new FileStream(new FStream(new string(name), System.IO.FileMode.OpenOrCreate, System.IO.FileAccess.ReadWrite)); + ok = true; + } + catch (Exception e) { + System.Console.Error.WriteLine(e); + f = null; + ok = false; + } + } + + public bool Close() + { + try { + fstream.Close(); + return true; + } + catch (Exception e) { + System.Console.Error.WriteLine(e); + return false; + } + } + + public bool Read(int fileOffset, byte[] buffer, int start, int end) + { + try { + fstream.Seek(fileOffset, System.IO.SeekOrigin.Begin); + fstream.Read(buffer, start, end - start); + return true; + } + catch (Exception e) { + System.Console.Error.WriteLine(e); + return false; + } + } + + public bool Write(int fileOffset, byte[] buffer, int start, int end) + { + try { + fstream.Seek(fileOffset, System.IO.SeekOrigin.Begin); + fstream.Write(buffer, start, end - start); + return true; + } + catch (Exception e) { + System.Console.Error.WriteLine(e); + return false; + } + } + + public bool Flush() + { + try { + fstream.Flush(); + return true; + } + catch (Exception e) { + System.Console.Error.WriteLine(e); + return false; + } + } +} + +} diff --git a/src/NativeTypes.dfy b/src/NativeTypes.dfy new file mode 100644 index 00000000..660f42ce --- /dev/null +++ b/src/NativeTypes.dfy @@ -0,0 +1,39 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module NativeTypes { + const BASE_0: int := 1 + + const BASE_1: int := 2 + const BASE_2: int := 4 + const BASE_4: int := 16 + const BASE_5: int := 32 + const BASE_8: int := 0x1_00 + const BASE_16: int := 0x1_0000 + const BASE_24: int := 0x1_000000 + const BASE_32: int := 0x1_00000000 + const BASE_40: int := 0x1_00000000_00 + const BASE_48: int := 0x1_00000000_0000 + const BASE_56: int := 0x1_00000000_000000 + const BASE_64: int := 0x1_00000000_00000000 + const BASE_128: int := 0x1_00000000_00000000_00000000_00000000 + const BASE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000 + const BASE_512: int := + 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; + + newtype {:nativeType "byte"} uint8 = x:int | 0 <= x < 0x1_00 + newtype {:nativeType "ushort"} uint16 = x: int | 0 <= x < 0x1_0000 + newtype {:nativeType "uint"} uint32 = x: int | 0 <= x < 0x1_00000000 + newtype {:nativeType "ulong"} uint64 = x: int | 0 <= x < 0x1_00000000_00000000 + + newtype {:nativeType "sbyte"} int8 = x: int | -0x80 <= x < 0x80 + newtype {:nativeType "short"} int16 = x: int | -0x8000 <= x < 0x8000 + newtype {:nativeType "int"} int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 + newtype {:nativeType "long"} int64 = x: int | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 + + newtype {:nativeType "sbyte"} nat8 = x: int | 0 <= x < 0x80 + newtype {:nativeType "short"} nat16 = x: int | 0 <= x < 0x8000 + newtype {:nativeType "int"} nat32 = x: int | 0 <= x < 0x8000_0000 + newtype {:nativeType "long"} nat64 = x: int | 0 <= x < 0x8000_0000_0000_0000 + +} diff --git a/src/NativeTypes.dfy.expect b/src/NativeTypes.dfy.expect new file mode 100644 index 00000000..e5f9ee5a --- /dev/null +++ b/src/NativeTypes.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 12 verified, 0 errors From 59bb5ad226c6cf8c77ac8b580814c89d0bac1103 Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Fri, 3 Sep 2021 12:29:34 -0700 Subject: [PATCH 02/36] Style changes --- src/Collections/Sequences/NatSeq.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/NatSeq.dfy index 359267df..bd21825e 100644 --- a/src/Collections/Sequences/NatSeq.dfy +++ b/src/Collections/Sequences/NatSeq.dfy @@ -18,7 +18,7 @@ abstract module NatSeq { /* Upper bound of a word */ function method BOUND(): nat - ensures BOUND() > 1 + ensures BOUND() > 1 type uint = i: int | 0 <= i < BOUND() From 7f246e010943b792e53b5f4de56aa88de2589de8 Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Fri, 3 Sep 2021 12:35:09 -0700 Subject: [PATCH 03/36] Remove explicit triggers --- src/Collections/Sequences/NatSeq.dfy | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/NatSeq.dfy index bd21825e..3001d224 100644 --- a/src/Collections/Sequences/NatSeq.dfy +++ b/src/Collections/Sequences/NatSeq.dfy @@ -90,12 +90,11 @@ abstract module NatSeq { } lemma LemmaToNatEqToNatRevAuto() - ensures forall xs: seq {:trigger ToNatRev(xs)}{:trigger ToNat(xs)} - :: ToNat(xs) == ToNatRev(xs) + ensures forall xs: seq :: ToNat(xs) == ToNatRev(xs) { reveal ToNat(); reveal ToNatRev(); - forall xs: seq {:trigger ToNatRev(xs)}{:trigger ToNat(xs)} + forall xs: seq ensures ToNat(xs) == ToNatRev(xs) { LemmaToNatEqToNatRev(xs); @@ -425,7 +424,7 @@ abstract module NatSeq { sequence of zeros. */ lemma LemmaSeqZero(xs: seq) requires ToNat(xs) == 0 - ensures forall i {:trigger xs[i]} :: 0 <= i < |xs| ==> xs[i] == 0 + ensures forall i :: 0 <= i < |xs| ==> xs[i] == 0 { reveal ToNat(); if |xs| == 0 { @@ -441,7 +440,7 @@ abstract module NatSeq { /* Generates a sequence of zeros of a specified length. */ function method {:opaque} SeqZero(len: nat): (xs: seq) ensures |xs| == len - ensures forall i {:trigger xs[i]} :: 0 <= i < |xs| ==> xs[i] == 0 + ensures forall i :: 0 <= i < |xs| ==> xs[i] == 0 ensures ToNat(xs) == 0 { LemmaPowPositive(BOUND(), len); From 8781a8d81ce13be85288c2b9b2e35cb8b3f795aa Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Fri, 3 Sep 2021 13:37:10 -0700 Subject: [PATCH 04/36] Add copyright headers --- examples/Io/IoExample.dfy | 8 ++++++++ examples/NatSeq/NatSeqExample.dfy | 8 ++++++++ src/Collections/Sequences/NatSeq.dfy | 8 ++++++++ src/Collections/Sequences/NatSeqConversions.dfy | 8 ++++++++ src/Io/Io.dfy | 8 ++++++++ src/Io/IoNative.cs | 8 ++++++++ 6 files changed, 48 insertions(+) diff --git a/examples/Io/IoExample.dfy b/examples/Io/IoExample.dfy index 69172a8a..78c76695 100644 --- a/examples/Io/IoExample.dfy +++ b/examples/Io/IoExample.dfy @@ -1,6 +1,14 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" +/******************************************************************************* +* Original: Copyright (c) Microsoft Corporation +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + include "../../src/Io/Io.dfy" include "../../src/NativeTypes.dfy" diff --git a/examples/NatSeq/NatSeqExample.dfy b/examples/NatSeq/NatSeqExample.dfy index 9b742b81..2203b5d8 100644 --- a/examples/NatSeq/NatSeqExample.dfy +++ b/examples/NatSeq/NatSeqExample.dfy @@ -1,6 +1,14 @@ // RUN: %dafny /compile:0 /noNLarith "%s" > "%t" // RUN: %diff "%s.expect" "%t" +/******************************************************************************* +* Original: Copyright (c) Microsoft Corporation +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + include "../../src/Collections/Sequences/NatSeqConversions.dfy" module NatSeqExample { diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/NatSeq.dfy index 3001d224..da3a367d 100644 --- a/src/Collections/Sequences/NatSeq.dfy +++ b/src/Collections/Sequences/NatSeq.dfy @@ -1,6 +1,14 @@ // RUN: %dafny /compile:0 /noNLarith "%s" > "%t" // RUN: %diff "%s.expect" "%t" +/******************************************************************************* +* Original: Copyright (c) Microsoft Corporation +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + /* The first element of a sequence is the least significant word; the last element is the most significant word. */ diff --git a/src/Collections/Sequences/NatSeqConversions.dfy b/src/Collections/Sequences/NatSeqConversions.dfy index c8036867..3ea425e5 100644 --- a/src/Collections/Sequences/NatSeqConversions.dfy +++ b/src/Collections/Sequences/NatSeqConversions.dfy @@ -1,6 +1,14 @@ // RUN: %dafny /compile:0 /noNLarith "%s" > "%t" // RUN: %diff "%s.expect" "%t" +/******************************************************************************* +* Original: Copyright (c) Microsoft Corporation +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + include "../../NonlinearArithmetic/DivMod.dfy" include "../../NonlinearArithmetic/Mul.dfy" include "../../NonlinearArithmetic/Power.dfy" diff --git a/src/Io/Io.dfy b/src/Io/Io.dfy index 2aa259df..998418ef 100644 --- a/src/Io/Io.dfy +++ b/src/Io/Io.dfy @@ -1,6 +1,14 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" +/******************************************************************************* +* Original: Copyright (c) Microsoft Corporation +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + include "../NativeTypes.dfy" module {:extern "IoNative"} Io { diff --git a/src/Io/IoNative.cs b/src/Io/IoNative.cs index 0167b318..85d13588 100644 --- a/src/Io/IoNative.cs +++ b/src/Io/IoNative.cs @@ -1,3 +1,11 @@ +/******************************************************************************* +* Original: Copyright (c) Microsoft Corporation +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + using System; using FStream = System.IO.FileStream; From c6c0764cc1c261aa69a675db54dd327a1156dfe3 Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Fri, 3 Sep 2021 13:53:53 -0700 Subject: [PATCH 05/36] Update LICENSE --- LICENSE | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/LICENSE b/LICENSE index a58bea61..1825a1a4 100644 --- a/LICENSE +++ b/LICENSE @@ -26,6 +26,7 @@ This project also includes code from projects shown in README.md, which were lic 1) BSD-2 License: https://github.com/vmware-labs/verified-betrfs/blob/master/LICENSE.txt 2) Apache License (Version 2.0): https://github.com/project-everest/vale/blob/legacy_dafny/LICENSE 3) MIT License: https://github.com/microsoft/Ironclad/blob/main/ironfleet/LICENSE +4) MIT License: https://github.com/secure-foundations/veri-titan/blob/master/LICENSE 1) Copyright 2021 VMware, Inc. @@ -245,3 +246,26 @@ Permission is hereby granted, free of charge, to any person obtaining a copy of The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +4) +MIT License + +Copyright (c) 2020 Secure Foundations Lab + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. From 13cf6c27ea24253391439d6db21a4aceacdf92eb Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Fri, 3 Sep 2021 13:57:58 -0700 Subject: [PATCH 06/36] Fix copyright headers --- examples/Io/IoExample.dfy | 5 +---- examples/NatSeq/NatSeqExample.dfy | 5 +---- src/Collections/Sequences/NatSeq.dfy | 2 +- src/Collections/Sequences/NatSeqConversions.dfy | 5 +---- src/Io/Io.dfy | 5 +---- src/Io/IoNative.cs | 5 +---- 6 files changed, 6 insertions(+), 21 deletions(-) diff --git a/examples/Io/IoExample.dfy b/examples/Io/IoExample.dfy index 78c76695..4b3363db 100644 --- a/examples/Io/IoExample.dfy +++ b/examples/Io/IoExample.dfy @@ -2,10 +2,7 @@ // RUN: %diff "%s.expect" "%t" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ diff --git a/examples/NatSeq/NatSeqExample.dfy b/examples/NatSeq/NatSeqExample.dfy index 2203b5d8..c4cad96b 100644 --- a/examples/NatSeq/NatSeqExample.dfy +++ b/examples/NatSeq/NatSeqExample.dfy @@ -2,10 +2,7 @@ // RUN: %diff "%s.expect" "%t" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/NatSeq.dfy index da3a367d..bfe71a03 100644 --- a/src/Collections/Sequences/NatSeq.dfy +++ b/src/Collections/Sequences/NatSeq.dfy @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation +* Original: Copyright (c) 2020 Secure Foundations Lab * SPDX-License-Identifier: MIT * * Modifications and Extensions: Copyright by the contributors to the Dafny Project diff --git a/src/Collections/Sequences/NatSeqConversions.dfy b/src/Collections/Sequences/NatSeqConversions.dfy index 3ea425e5..fe530cfd 100644 --- a/src/Collections/Sequences/NatSeqConversions.dfy +++ b/src/Collections/Sequences/NatSeqConversions.dfy @@ -2,10 +2,7 @@ // RUN: %diff "%s.expect" "%t" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ diff --git a/src/Io/Io.dfy b/src/Io/Io.dfy index 998418ef..87d665a7 100644 --- a/src/Io/Io.dfy +++ b/src/Io/Io.dfy @@ -2,10 +2,7 @@ // RUN: %diff "%s.expect" "%t" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ diff --git a/src/Io/IoNative.cs b/src/Io/IoNative.cs index 85d13588..a3114f36 100644 --- a/src/Io/IoNative.cs +++ b/src/Io/IoNative.cs @@ -1,8 +1,5 @@ /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ From 790677523e7e96e7a3eee890ebe683ee5d49e35b Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Mon, 6 Sep 2021 22:43:08 -0700 Subject: [PATCH 07/36] Remove Io --- README.md | 1 - examples/Io/IoExample.dfy | 69 ---------------- examples/Io/IoExample.dfy.expect | 2 - src/Io/Io.dfy | 133 ------------------------------- src/Io/Io.dfy.expect | 2 - src/Io/IoNative.cs | 118 --------------------------- 6 files changed, 325 deletions(-) delete mode 100644 examples/Io/IoExample.dfy delete mode 100644 examples/Io/IoExample.dfy.expect delete mode 100644 src/Io/Io.dfy delete mode 100644 src/Io/Io.dfy.expect delete mode 100644 src/Io/IoNative.cs diff --git a/README.md b/README.md index fef7bac5..c8fb5426 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,6 @@ Much of this code came from or was inspired by code from the following projects: * [Ironclad Apps](https://github.com/microsoft/Ironclad/tree/main/ironclad-apps) * [IronFleet](https://github.com/microsoft/Ironclad/tree/main/ironfleet) -* [James Wilcox's Notes](https://github.com/wilcoxjay/notes) * [Vale](https://github.com/project-everest/vale/tree/legacy_dafny) * [Verified BetrFS](https://github.com/vmware-labs/verified-betrfs) * [Verifying OpenTitan](https://github.com/secure-foundations/veri-titan) diff --git a/examples/Io/IoExample.dfy b/examples/Io/IoExample.dfy deleted file mode 100644 index 4b3363db..00000000 --- a/examples/Io/IoExample.dfy +++ /dev/null @@ -1,69 +0,0 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -include "../../src/Io/Io.dfy" -include "../../src/NativeTypes.dfy" - -module IoExample { - - import opened Io - import opened NativeTypes - - /* Useful to convert Dafny strings into arrays of characters. */ - method ArrayFromSeq(s: seq) returns (a: array) - ensures a[..] == s - { - a := new A[|s|] ( i requires 0 <= i < |s| => s[i] ); - } - - method {:main} Main(ghost env: HostEnvironment) - requires env.ok.ok() - modifies env.ok - { - var fname := ArrayFromSeq("foo.txt"); - var f: FileStream; - var ok: bool; - - var numArgs := HostConstants.NumCommandLineArgs(env); - if numArgs < 1 { - print "Error: invalid number of command line arguments\n"; - return; - } - print "# command line args: "; - print numArgs; - print "\n"; - - var arg0 := HostConstants.GetCommandLineArg(0, env); - print "command: " + arg0[..] + "\n"; - - var fileExists := FileStream.FileExists(fname, env); - if fileExists { - print fname[..] + " exists!\n"; - - var ok, len := FileStream.FileLength(fname, env); - if !ok { print "Error: invalid file length\n"; return; } - print fname[..] + " length: "; - print len; - print "\n"; - } - - ok, f := FileStream.Open(fname, env); - if !ok { print "Error: open failed\n"; return; } - - /* This is "hello world!" in ascii. */ - var data: array := ArrayFromSeq([104, 101, 108, 108, 111, 32, 119, 111, 114, 108, 100, 33, 10]); - - ok := f.Write(0, data, 0, data.Length as int32); - if !ok { print "Error: write failed\n"; return; } - - ok := f.Close(); - - print "done!\n"; - } - -} diff --git a/examples/Io/IoExample.dfy.expect b/examples/Io/IoExample.dfy.expect deleted file mode 100644 index ba00363f..00000000 --- a/examples/Io/IoExample.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 4 verified, 0 errors diff --git a/src/Io/Io.dfy b/src/Io/Io.dfy deleted file mode 100644 index 87d665a7..00000000 --- a/src/Io/Io.dfy +++ /dev/null @@ -1,133 +0,0 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -include "../NativeTypes.dfy" - -module {:extern "IoNative"} Io { - - import opened NativeTypes - - ////////////////////////////////////////////////////////////////////////////// - // Per-host constants - ////////////////////////////////////////////////////////////////////////////// - - class HostConstants - { - constructor {:extern} () requires false - - /* Result of C# System.Environment.GetCommandLineArgs(); argument 0 is name - of executable. */ - function {:extern} CommandLineArgs(): seq reads this - - static method {:extern} NumCommandLineArgs(ghost env: HostEnvironment) returns (n: uint32) - ensures n as int == |env.constants.CommandLineArgs()| - - static method {:extern} GetCommandLineArg(i: uint64, ghost env: HostEnvironment) returns (arg: array) - requires 0 <= i as int < |env.constants.CommandLineArgs()| - ensures arg[..] == env.constants.CommandLineArgs()[i] - } - - ////////////////////////////////////////////////////////////////////////////// - // Failure - ////////////////////////////////////////////////////////////////////////////// - - class OkState - { - constructor {:extern} () requires false - function {:extern} ok(): bool reads this - } - - ////////////////////////////////////////////////////////////////////////////// - // File System - ////////////////////////////////////////////////////////////////////////////// - - class FileSystemState - { - constructor {:extern} () requires false - - /* File system maps file names to their contents. */ - function {:extern} state(): map> - reads this - } - - class HostEnvironment - { - ghost var constants: HostConstants - ghost var ok: OkState - ghost var files: FileSystemState - } - - class FileStream - { - ghost var env: HostEnvironment - function {:extern} Name(): string reads this - function {:extern} IsOpen(): bool reads this - constructor {:extern} () requires false - - static method {:extern} FileExists(name: array, ghost env: HostEnvironment) returns (result: bool) - requires env.ok.ok() - ensures result <==> old(name[..]) in env.files.state() - - static method {:extern} FileLength(name: array, ghost env: HostEnvironment) returns (success: bool, len: int32) - requires env.ok.ok() - requires name[..] in env.files.state() - modifies env.ok - ensures env.ok.ok() == success - ensures success ==> len as int == |env.files.state()[name[..]]| - - static method {:extern} Open(name: array, ghost env: HostEnvironment) - returns (ok: bool, f: FileStream) - requires env.ok.ok() - modifies env.ok - ensures env.ok.ok() == ok - ensures ok ==> fresh(f) && f.env == env && f.IsOpen() && f.Name() == name[..] - - method {:extern} Close() returns (ok: bool) - requires env.ok.ok() - requires IsOpen() - modifies this - modifies env.ok - ensures env == old(env) - ensures env.ok.ok() == ok - - method {:extern} Read(fileOffset: nat32, buffer: array, start: int32, end: int32) returns (ok: bool) - requires env.ok.ok() - requires IsOpen() - requires 0 <= start as int <= end as int <= buffer.Length - modifies this - modifies env.ok - modifies buffer - ensures env == old(env) - ensures env.ok.ok() == ok - ensures Name() == old(Name()) - ensures forall i:int :: 0 <= i < buffer.Length && !(start as int <= i < end as int) ==> buffer[i] == old(buffer[i]) - ensures ok ==> IsOpen() - - method {:extern} Write(fileOffset: nat32, buffer: array, start: int32, end: int32) returns (ok: bool) - requires env.ok.ok() - requires IsOpen() - requires 0 <= start as int <= end as int <= buffer.Length - modifies this - modifies env.ok - ensures env == old(env) - ensures env.ok.ok() == ok - ensures Name() == old(Name()) - ensures ok ==> IsOpen() - - method {:extern} Flush() returns (ok: bool) - requires env.ok.ok() - requires IsOpen() - modifies this - modifies env.ok - ensures env == old(env) - ensures env.ok.ok() == ok - ensures Name() == old(Name()) - ensures ok ==> IsOpen() - } - -} diff --git a/src/Io/Io.dfy.expect b/src/Io/Io.dfy.expect deleted file mode 100644 index 0825601c..00000000 --- a/src/Io/Io.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 9 verified, 0 errors diff --git a/src/Io/IoNative.cs b/src/Io/IoNative.cs deleted file mode 100644 index a3114f36..00000000 --- a/src/Io/IoNative.cs +++ /dev/null @@ -1,118 +0,0 @@ -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -using System; -using FStream = System.IO.FileStream; - -namespace @IoNative { - -public partial class HostConstants -{ - public static uint NumCommandLineArgs() - { - return (uint)System.Environment.GetCommandLineArgs().Length; - } - - public static char[] GetCommandLineArg(ulong i) - { - return System.Environment.GetCommandLineArgs()[i].ToCharArray(); - } -} - -public partial class FileStream -{ - internal FStream fstream; - internal FileStream(FStream fstream) { this.fstream = fstream; } - - public static bool FileExists(char[] name) - { - return System.IO.File.Exists(new string(name)); - } - - public static void FileLength(char[] name, out bool success, out int len) - { - len = -1; - try { - System.IO.FileInfo fi = new System.IO.FileInfo(new string(name)); - if (fi.Length < System.Int32.MaxValue) { // We only support small files - len = (int)fi.Length; - success = true; - } - else { - success = false; - } - - } - catch (Exception e) { - System.Console.Error.WriteLine(e); - success = false; - } - } - - public static void Open(char[] name, out bool ok, out FileStream f) - { - try { - f = new FileStream(new FStream(new string(name), System.IO.FileMode.OpenOrCreate, System.IO.FileAccess.ReadWrite)); - ok = true; - } - catch (Exception e) { - System.Console.Error.WriteLine(e); - f = null; - ok = false; - } - } - - public bool Close() - { - try { - fstream.Close(); - return true; - } - catch (Exception e) { - System.Console.Error.WriteLine(e); - return false; - } - } - - public bool Read(int fileOffset, byte[] buffer, int start, int end) - { - try { - fstream.Seek(fileOffset, System.IO.SeekOrigin.Begin); - fstream.Read(buffer, start, end - start); - return true; - } - catch (Exception e) { - System.Console.Error.WriteLine(e); - return false; - } - } - - public bool Write(int fileOffset, byte[] buffer, int start, int end) - { - try { - fstream.Seek(fileOffset, System.IO.SeekOrigin.Begin); - fstream.Write(buffer, start, end - start); - return true; - } - catch (Exception e) { - System.Console.Error.WriteLine(e); - return false; - } - } - - public bool Flush() - { - try { - fstream.Flush(); - return true; - } - catch (Exception e) { - System.Console.Error.WriteLine(e); - return false; - } - } -} - -} From 2c3bd36690a074a9564d96ce6899f8806c857989 Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Tue, 7 Sep 2021 16:41:23 -0700 Subject: [PATCH 08/36] Change expect file --- src/Collections/Sequences/NatSeqConversions.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Collections/Sequences/NatSeqConversions.dfy.expect b/src/Collections/Sequences/NatSeqConversions.dfy.expect index 856160c0..c62d0a44 100644 --- a/src/Collections/Sequences/NatSeqConversions.dfy.expect +++ b/src/Collections/Sequences/NatSeqConversions.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 456 verified, 0 errors +Dafny program verifier finished with 526 verified, 0 errors From 30a8c34f11b0e00180812cd00b7d1e89dad9034c Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Thu, 9 Sep 2021 12:09:10 -0700 Subject: [PATCH 09/36] Remove {:nativeType} attributes --- src/NativeTypes.dfy | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/NativeTypes.dfy b/src/NativeTypes.dfy index 660f42ce..71ecd7e9 100644 --- a/src/NativeTypes.dfy +++ b/src/NativeTypes.dfy @@ -21,19 +21,19 @@ module NativeTypes { const BASE_512: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; - newtype {:nativeType "byte"} uint8 = x:int | 0 <= x < 0x1_00 - newtype {:nativeType "ushort"} uint16 = x: int | 0 <= x < 0x1_0000 - newtype {:nativeType "uint"} uint32 = x: int | 0 <= x < 0x1_00000000 - newtype {:nativeType "ulong"} uint64 = x: int | 0 <= x < 0x1_00000000_00000000 + newtype uint8 = x:int | 0 <= x < 0x1_00 + newtype uint16 = x: int | 0 <= x < 0x1_0000 + newtype uint32 = x: int | 0 <= x < 0x1_00000000 + newtype uint64 = x: int | 0 <= x < 0x1_00000000_00000000 - newtype {:nativeType "sbyte"} int8 = x: int | -0x80 <= x < 0x80 - newtype {:nativeType "short"} int16 = x: int | -0x8000 <= x < 0x8000 - newtype {:nativeType "int"} int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 - newtype {:nativeType "long"} int64 = x: int | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 + newtype int8 = x: int | -0x80 <= x < 0x80 + newtype int16 = x: int | -0x8000 <= x < 0x8000 + newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 + newtype int64 = x: int | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 - newtype {:nativeType "sbyte"} nat8 = x: int | 0 <= x < 0x80 - newtype {:nativeType "short"} nat16 = x: int | 0 <= x < 0x8000 - newtype {:nativeType "int"} nat32 = x: int | 0 <= x < 0x8000_0000 - newtype {:nativeType "long"} nat64 = x: int | 0 <= x < 0x8000_0000_0000_0000 + newtype nat8 = x: int | 0 <= x < 0x80 + 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 } From d6a2aaf323b4ccde0773fe0590676eb33c0e2cda Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Mon, 13 Sep 2021 08:58:51 -0700 Subject: [PATCH 10/36] Name changes --- examples/NatSeq/NatSeqExample.dfy | 12 +- src/BoundedInts.dfy | 39 ++ ...ypes.dfy.expect => BoundedInts.dfy.expect} | 0 src/Collections/Sequences/NatSeq.dfy | 344 +++++++++--------- .../Sequences/NatSeqConversions.dfy | 62 ++-- src/NativeTypes.dfy | 39 -- 6 files changed, 252 insertions(+), 244 deletions(-) create mode 100644 src/BoundedInts.dfy rename src/{NativeTypes.dfy.expect => BoundedInts.dfy.expect} (100%) delete mode 100644 src/NativeTypes.dfy diff --git a/examples/NatSeq/NatSeqExample.dfy b/examples/NatSeq/NatSeqExample.dfy index c4cad96b..e10b3c45 100644 --- a/examples/NatSeq/NatSeqExample.dfy +++ b/examples/NatSeq/NatSeqExample.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" +// RUN: %dafny /compile:3 /noNLarith "%s" > "%t" // RUN: %diff "%s.expect" "%t" /******************************************************************************* @@ -17,20 +17,22 @@ module NatSeqExample { // Convert n to uint8 and uint32 sequences var smallSeq, largeSeq := Small.FromNat(n), Large.FromNat(n); + expect smallSeq == [122, 7, 134, 140, 11]; + expect largeSeq == [2357593978, 11]; Small.LemmaNatSeqNat(n); Large.LemmaNatSeqNat(n); - assert Small.ToNat(smallSeq) == Large.ToNat(largeSeq) == n; + assert Small.ToNatRight(smallSeq) == Large.ToNatRight(largeSeq) == n; // Extend smallSeq smallSeq := Small.SeqExtendMultiple(smallSeq, E()); - assert Small.ToNat(smallSeq) == n; + assert Small.ToNatRight(smallSeq) == n; // Convert between smallSeqExtended and largeSeq LemmaToSmall(largeSeq); LemmaToLarge(smallSeq); - assert Small.ToNat(ToSmall(largeSeq)) == n; - assert Large.ToNat(ToLarge(smallSeq)) == n; + assert Small.ToNatRight(ToSmall(largeSeq)) == n; + assert Large.ToNatRight(ToLarge(smallSeq)) == n; assert |ToSmall(largeSeq)| == |largeSeq| * E(); assert |ToLarge(smallSeq)| == |smallSeq| / E(); diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy new file mode 100644 index 00000000..9fb9857b --- /dev/null +++ b/src/BoundedInts.dfy @@ -0,0 +1,39 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module BoundedInts { + const TWO_TO_THE_0: int := 1 + + const TWO_TO_THE_1: int := 2 + const TWO_TO_THE_2: int := 4 + const TWO_TO_THE_4: int := 16 + const TWO_TO_THE_5: int := 32 + const TWO_TO_THE_8: int := 0x100 + const TWO_TO_THE_16: int := 0x10000 + const TWO_TO_THE_24: int := 0x1000000 + const TWO_TO_THE_32: int := 0x1_00000000 + const TWO_TO_THE_40: int := 0x100_00000000 + const TWO_TO_THE_48: int := 0x10000_00000000 + const TWO_TO_THE_56: int := 0x1000000_00000000 + const TWO_TO_THE_64: int := 0x1_00000000_00000000 + const TWO_TO_THE_128: int := 0x1_00000000_00000000_00000000_00000000 + const TWO_TO_THE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000 + const TWO_TO_THE_512: int := + 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; + + newtype uint8 = x: int | 0 <= x < TWO_TO_THE_8 + newtype uint16 = x: int | 0 <= x < TWO_TO_THE_16 + newtype uint32 = x: int | 0 <= x < TWO_TO_THE_32 + newtype uint64 = x: int | 0 <= x < TWO_TO_THE_64 + + newtype int8 = x: int | -0x80 <= x < 0x80 + newtype int16 = x: int | -0x8000 <= x < 0x8000 + newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 + newtype int64 = x: int | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 + + newtype nat8 = x: int | 0 <= x < 0x80 + 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 + +} diff --git a/src/NativeTypes.dfy.expect b/src/BoundedInts.dfy.expect similarity index 100% rename from src/NativeTypes.dfy.expect rename to src/BoundedInts.dfy.expect diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/NatSeq.dfy index bfe71a03..5e08bdd7 100644 --- a/src/Collections/Sequences/NatSeq.dfy +++ b/src/Collections/Sequences/NatSeq.dfy @@ -9,8 +9,9 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -/* The first element of a sequence is the least significant word; the last -element is the most significant word. */ +/* Little endian interpretation of a sequence of numbers with a given base. The +first element of a sequence is the least significant position; the last +element is the most significant position. */ include "../../NonlinearArithmetic/DivMod.dfy" include "../../NonlinearArithmetic/Mul.dfy" @@ -24,11 +25,10 @@ abstract module NatSeq { import opened Power import opened Seq - /* Upper bound of a word */ - function method BOUND(): nat - ensures BOUND() > 1 + function method BASE(): nat + ensures BASE() > 1 - type uint = i: int | 0 <= i < BOUND() + type uint = i: int | 0 <= i < BASE() ////////////////////////////////////////////////////////////////////////////// // @@ -36,133 +36,139 @@ abstract module NatSeq { // ////////////////////////////////////////////////////////////////////////////// - /* Converts a sequence to a nat beginning from the least significant word. */ - function method {:opaque} ToNat(xs: seq): nat + /* Converts a sequence to a nat beginning with the least significant position. */ + function method {:opaque} ToNatRight(xs: seq): nat { if |xs| == 0 then 0 else LemmaMulNonnegativeAuto(); - ToNat(DropFirst(xs)) * BOUND() + First(xs) + ToNatRight(DropFirst(xs)) * BASE() + First(xs) } - /* Converts a sequence to a nat beginning from the most significant word. */ - function method {:opaque} ToNatRev(xs: seq): nat + /* Converts a sequence to a nat beginning with the most significant position. */ + function method {:opaque} ToNatLeft(xs: seq): nat { if |xs| == 0 then 0 else LemmaPowPositiveAuto(); LemmaMulNonnegativeAuto(); - ToNatRev(DropLast(xs)) + Last(xs) * Pow(BOUND(), |xs| - 1) + ToNatLeft(DropLast(xs)) + Last(xs) * Pow(BASE(), |xs| - 1) } - /* Given the same sequence, ToNat and ToNatRev return the same nat. */ - lemma LemmaToNatEqToNatRev(xs: seq) - ensures ToNat(xs) == ToNatRev(xs) + /* Given the same sequence, ToNatRight and ToNatLeft return the same nat. */ + lemma LemmaToNatLeftEqToNatRight(xs: seq) + ensures ToNatRight(xs) == ToNatLeft(xs) { - reveal ToNat(); - reveal ToNatRev(); + reveal ToNatRight(); + reveal ToNatLeft(); if xs == [] { } else { if DropLast(xs) == [] { calc { - ToNatRev(xs); - Last(xs) * Pow(BOUND(), |xs| - 1); - { LemmaPow0Auto(); } - ToNat(xs); + ToNatLeft(xs); + Last(xs) * Pow(BASE(), |xs| - 1); + { + LemmaPow0Auto(); + LemmaMulBasicsAuto(); + } + Last(xs); + First(xs); + { assert ToNatRight(DropFirst(xs)) == 0; } + ToNatRight(xs); } } else { calc { - ToNatRev(xs); - ToNatRev(DropLast(xs)) + Last(xs) * Pow(BOUND(), |xs| - 1); - { LemmaToNatEqToNatRev(DropLast(xs)); } - ToNat(DropLast(xs)) + Last(xs) * Pow(BOUND(), |xs| - 1); - ToNat(DropFirst(DropLast(xs))) * BOUND() + First(xs) + Last(xs) - * Pow(BOUND(), |xs| - 1); - { LemmaToNatEqToNatRev(DropFirst(DropLast(xs))); } - ToNatRev(DropFirst(DropLast(xs))) * BOUND() + First(xs) + Last(xs) - * Pow(BOUND(), |xs| - 1); + ToNatLeft(xs); + ToNatLeft(DropLast(xs)) + Last(xs) * Pow(BASE(), |xs| - 1); + { LemmaToNatLeftEqToNatRight(DropLast(xs)); } + ToNatRight(DropLast(xs)) + Last(xs) * Pow(BASE(), |xs| - 1); + ToNatRight(DropFirst(DropLast(xs))) * BASE() + First(xs) + Last(xs) + * Pow(BASE(), |xs| - 1); + { LemmaToNatLeftEqToNatRight(DropFirst(DropLast(xs))); } + ToNatLeft(DropFirst(DropLast(xs))) * BASE() + First(xs) + Last(xs) + * Pow(BASE(), |xs| - 1); { assert DropFirst(DropLast(xs)) == DropLast(DropFirst(xs)); reveal Pow(); LemmaMulProperties(); } - ToNatRev(DropLast(DropFirst(xs))) * BOUND() + First(xs) + Last(xs) - * Pow(BOUND(), |xs| - 2) * BOUND(); + ToNatLeft(DropLast(DropFirst(xs))) * BASE() + First(xs) + Last(xs) + * Pow(BASE(), |xs| - 2) * BASE(); { LemmaMulIsDistributiveAddOtherWayAuto(); } - ToNatRev(DropFirst(xs)) * BOUND() + First(xs); - { LemmaToNatEqToNatRev(DropFirst(xs)); } - ToNat(xs); + ToNatLeft(DropFirst(xs)) * BASE() + First(xs); + { LemmaToNatLeftEqToNatRight(DropFirst(xs)); } + ToNatRight(xs); } } } } - lemma LemmaToNatEqToNatRevAuto() - ensures forall xs: seq :: ToNat(xs) == ToNatRev(xs) + lemma LemmaToNatLeftEqToNatRightAuto() + ensures forall xs: seq :: ToNatRight(xs) == ToNatLeft(xs) { - reveal ToNat(); - reveal ToNatRev(); + reveal ToNatRight(); + reveal ToNatLeft(); forall xs: seq - ensures ToNat(xs) == ToNatRev(xs) + ensures ToNatRight(xs) == ToNatLeft(xs) { - LemmaToNatEqToNatRev(xs); + LemmaToNatLeftEqToNatRight(xs); } } /* The nat representation of a sequence of length 1 is its first (and only) - word. */ + position. */ lemma LemmaSeqLen1(xs: seq) requires |xs| == 1 - ensures ToNat(xs) == First(xs) + ensures ToNatRight(xs) == First(xs) { - reveal ToNat(); + reveal ToNatRight(); } /* The nat representation of a sequence of length 2 is sum of its first - word and the product of its second word and BOUND(). */ + position and the product of its second position and BASE(). */ lemma LemmaSeqLen2(xs: seq) requires |xs| == 2 - ensures ToNat(xs) == First(xs) + xs[1] * BOUND() + ensures ToNatRight(xs) == First(xs) + xs[1] * BASE() { - reveal ToNat(); + reveal ToNatRight(); LemmaSeqLen1(DropLast(xs)); } /* Appending a zero does not change the nat representation of the sequence. */ lemma LemmaSeqAppendZero(xs: seq) - ensures ToNat(xs + [0]) == ToNat(xs) + ensures ToNatRight(xs + [0]) == ToNatRight(xs) { - reveal ToNatRev(); - LemmaToNatEqToNatRevAuto(); - calc == { - ToNat(xs + [0]); - ToNatRev(xs + [0]); - ToNatRev(xs) + 0 * Pow(BOUND(), |xs|); + reveal ToNatLeft(); + LemmaToNatLeftEqToNatRightAuto(); + calc { + ToNatRight(xs + [0]); + ToNatLeft(xs + [0]); + ToNatLeft(xs) + 0 * Pow(BASE(), |xs|); { LemmaMulBasicsAuto(); } - ToNatRev(xs); - ToNat(xs); + ToNatLeft(xs); + ToNatRight(xs); } } - /* The nat representation of a sequence is bounded by BOUND() to the power of + /* The nat representation of a sequence is bounded by BASE() to the power of the sequence length. */ lemma LemmaSeqNatBound(xs: seq) - ensures ToNat(xs) < Pow(BOUND(), |xs|) + ensures ToNatRight(xs) < Pow(BASE(), |xs|) { reveal Pow(); if |xs| == 0 { - reveal ToNat(); + reveal ToNatRight(); } else { var len' := |xs| - 1; - var pow := Pow(BOUND(), len'); + var pow := Pow(BASE(), len'); calc { - ToNat(xs); - { LemmaToNatEqToNatRev(xs); } - ToNatRev(xs); - { reveal ToNatRev(); } - ToNatRev(DropLast(xs)) + Last(xs) * pow; + ToNatRight(xs); + { LemmaToNatLeftEqToNatRight(xs); } + ToNatLeft(xs); + { reveal ToNatLeft(); } + ToNatLeft(DropLast(xs)) + Last(xs) * pow; < { - LemmaToNatEqToNatRev(DropLast(xs)); + LemmaToNatLeftEqToNatRight(DropLast(xs)); LemmaSeqNatBound(DropLast(xs)); } pow + Last(xs) * pow; @@ -170,9 +176,9 @@ abstract module NatSeq { LemmaPowPositiveAuto(); LemmaMulInequalityAuto(); } - pow + (BOUND() - 1) * pow; + pow + (BASE() - 1) * pow; { LemmaMulIsDistributiveAuto(); } - Pow(BOUND(), len' + 1); + Pow(BASE(), len' + 1); } } } @@ -181,50 +187,50 @@ abstract module NatSeq { representation of its prefix. */ lemma LemmaSeqPrefix(xs: seq, i: nat) requires 0 <= i <= |xs| - ensures ToNat(xs[..i]) + ToNat(xs[i..]) * Pow(BOUND(), i) == ToNat(xs) + ensures ToNatRight(xs[..i]) + ToNatRight(xs[i..]) * Pow(BASE(), i) == ToNatRight(xs) { - reveal ToNat(); + reveal ToNatRight(); reveal Pow(); if i == 1 { - assert ToNat(xs[..1]) == First(xs); + assert ToNatRight(xs[..1]) == First(xs); } else if i > 1 { calc { - ToNat(xs[..i]) + ToNat(xs[i..]) * Pow(BOUND(), i); - ToNat(DropFirst(xs[..i])) * BOUND() + First(xs) + ToNat(xs[i..]) * Pow(BOUND(), i); + ToNatRight(xs[..i]) + ToNatRight(xs[i..]) * Pow(BASE(), i); + ToNatRight(DropFirst(xs[..i])) * BASE() + First(xs) + ToNatRight(xs[i..]) * Pow(BASE(), i); { assert DropFirst(xs[..i]) == DropFirst(xs)[..i-1]; LemmaMulProperties(); } - ToNat(DropFirst(xs)[..i-1]) * BOUND() + First(xs) + (ToNat(xs[i..]) * Pow(BOUND(), i - 1)) * BOUND(); + ToNatRight(DropFirst(xs)[..i-1]) * BASE() + First(xs) + (ToNatRight(xs[i..]) * Pow(BASE(), i - 1)) * BASE(); { LemmaMulIsDistributiveAddOtherWayAuto(); } - (ToNat(DropFirst(xs)[..i-1]) + ToNat(DropFirst(xs)[i-1..]) * Pow(BOUND(), i - 1)) * BOUND() + First(xs); + (ToNatRight(DropFirst(xs)[..i-1]) + ToNatRight(DropFirst(xs)[i-1..]) * Pow(BASE(), i - 1)) * BASE() + First(xs); { LemmaSeqPrefix(DropFirst(xs), i - 1); } - ToNat(xs); + ToNatRight(xs); } } } - /* If there is an inequality between the most significant words of two + /* If there is an inequality between the most significant positions of two sequences, then there is an inequality between the nat representations of those sequences. Helper lemma for LemmaSeqNeq. */ lemma LemmaSeqMswInequality(xs: seq, ys: seq) requires |xs| == |ys| > 0 requires Last(xs) < Last(ys) - ensures ToNat(xs) < ToNat(ys) + ensures ToNatRight(xs) < ToNatRight(ys) { - reveal ToNatRev(); - LemmaToNatEqToNatRevAuto(); + reveal ToNatLeft(); + LemmaToNatLeftEqToNatRightAuto(); var len' := |xs| - 1; calc { - ToNat(xs); - ToNatRev(xs); + ToNatRight(xs); + ToNatLeft(xs); < { LemmaSeqNatBound(DropLast(xs)); } - Pow(BOUND(), len') + Last(xs) * Pow(BOUND(), len'); + Pow(BASE(), len') + Last(xs) * Pow(BASE(), len'); == { LemmaMulIsDistributiveAuto(); } - (1 + Last(xs)) * Pow(BOUND(), len'); + (1 + Last(xs)) * Pow(BASE(), len'); <= { LemmaPowPositiveAuto(); LemmaMulInequalityAuto(); } - ToNatRev(ys); - ToNat(ys); + ToNatLeft(ys); + ToNatRight(ys); } } @@ -232,8 +238,8 @@ abstract module NatSeq { do not have the same nat representations. Helper lemma for LemmaSeqNeq. */ lemma LemmaSeqPrefixNeq(xs: seq, ys: seq, i: nat) requires 0 <= i <= |xs| == |ys| - requires ToNat(xs[..i]) != ToNat(ys[..i]) - ensures ToNat(xs) != ToNat(ys) + requires ToNatRight(xs[..i]) != ToNatRight(ys[..i]) + ensures ToNatRight(xs) != ToNatRight(ys) decreases |xs| - i { if i == |xs| { @@ -241,15 +247,16 @@ abstract module NatSeq { assert ys[..i] == ys; } else { if xs[i] == ys[i] { - reveal ToNatRev(); + reveal ToNatLeft(); assert DropLast(xs[..i+1]) == xs[..i]; assert DropLast(ys[..i+1]) == ys[..i]; - LemmaToNatEqToNatRevAuto(); - assert ToNat(xs[..i+1]) == ToNatRev(xs[..i+1]); + LemmaToNatLeftEqToNatRightAuto(); + assert ToNatRight(xs[..i+1]) == ToNatLeft(xs[..i+1]); + } else if xs[i] < ys[i] { + LemmaSeqMswInequality(xs[..i+1], ys[..i+1]); } else { - if xs[i] < ys[i] { LemmaSeqMswInequality(xs[..i+1], ys[..i+1]); } - else { LemmaSeqMswInequality(ys[..i+1], xs[..i+1]); } + LemmaSeqMswInequality(ys[..i+1], xs[..i+1]); } LemmaSeqPrefixNeq(xs, ys, i + 1); } @@ -260,7 +267,7 @@ abstract module NatSeq { lemma LemmaSeqNeq(xs: seq, ys: seq) requires |xs| == |ys| requires xs != ys - ensures ToNat(xs) != ToNat(ys) + ensures ToNatRight(xs) != ToNatRight(ys) { ghost var i: nat, n: nat := 0, |xs|; @@ -273,15 +280,15 @@ abstract module NatSeq { } i := i + 1; } - assert ToNatRev(xs[..i]) == ToNatRev(ys[..i]); + assert ToNatLeft(xs[..i]) == ToNatLeft(ys[..i]); - reveal ToNatRev(); + reveal ToNatLeft(); assert xs[..i+1][..i] == xs[..i]; assert ys[..i+1][..i] == ys[..i]; LemmaPowPositiveAuto(); LemmaMulStrictInequalityAuto(); - assert ToNatRev(xs[..i+1]) != ToNatRev(ys[..i+1]); - LemmaToNatEqToNatRevAuto(); + assert ToNatLeft(xs[..i+1]) != ToNatLeft(ys[..i+1]); + LemmaToNatLeftEqToNatRightAuto(); LemmaSeqPrefixNeq(xs, ys, i+1); } @@ -290,35 +297,35 @@ abstract module NatSeq { to each other, the sequences are the same. */ lemma LemmaSeqEq(xs: seq, ys: seq) requires |xs| == |ys| - requires ToNat(xs) == ToNat(ys) + requires ToNatRight(xs) == ToNatRight(ys) ensures xs == ys { calc ==> { xs != ys; { LemmaSeqNeq(xs, ys); } - ToNat(xs) != ToNat(ys); + ToNatRight(xs) != ToNatRight(ys); false; } } - /* The nat representation of a sequence and its least significant word are + /* The nat representation of a sequence and its least significant position are congruent. */ lemma LemmaSeqLswModEquivalence(xs: seq) requires |xs| >= 1; - ensures IsModEquivalent(ToNat(xs), First(xs), BOUND()); + ensures IsModEquivalent(ToNatRight(xs), First(xs), BASE()); { if |xs| == 1 { LemmaSeqLen1(xs); LemmaModEquivalenceAuto(); } else { - assert IsModEquivalent(ToNat(xs), First(xs), BOUND()) by { - reveal ToNat(); + assert IsModEquivalent(ToNatRight(xs), First(xs), BASE()) by { + reveal ToNatRight(); calc ==> { true; { LemmaModEquivalenceAuto(); } - IsModEquivalent(ToNat(xs), ToNat(DropFirst(xs)) * BOUND() + First(xs), BOUND()); + IsModEquivalent(ToNatRight(xs), ToNatRight(DropFirst(xs)) * BASE() + First(xs), BASE()); { LemmaModMultiplesBasicAuto(); } - IsModEquivalent(ToNat(xs), First(xs), BOUND()); + IsModEquivalent(ToNatRight(xs), First(xs), BASE()); } } } @@ -337,15 +344,14 @@ abstract module NatSeq { else LemmaDivBasicsAuto(); LemmaDivDecreasesAuto(); - [n % BOUND()] + FromNat(n / BOUND()) + [n % BASE()] + FromNat(n / BASE()) } /* Ensures length of the sequence generated by FromNat is less than len. Helper lemma for FromNatWithLen. */ lemma LemmaFromNatLen(n: nat, len: nat) - requires Pow(BOUND(), len) > n + requires Pow(BASE(), len) > n ensures |FromNat(n)| <= len - decreases n { reveal FromNat(); if n == 0 { @@ -353,12 +359,12 @@ abstract module NatSeq { calc { |FromNat(n)|; == { LemmaDivBasicsAuto(); } - 1 + |FromNat(n / BOUND())|; + 1 + |FromNat(n / BASE())|; <= { LemmaMultiplyDivideLtAuto(); LemmaDivDecreasesAuto(); reveal Pow(); - LemmaFromNatLen(n / BOUND(), len - 1); + LemmaFromNatLen(n / BASE(), len - 1); } len; } @@ -368,24 +374,24 @@ abstract module NatSeq { /* If we start with a nat, convert it to a sequence, and convert it back, we get the same nat we started with. */ lemma LemmaNatSeqNat(n: nat) - ensures ToNat(FromNat(n)) == n + ensures ToNatRight(FromNat(n)) == n decreases n { - reveal ToNat(); + reveal ToNatRight(); reveal FromNat(); if n == 0 { } else { calc { - ToNat(FromNat(n)); + ToNatRight(FromNat(n)); { LemmaDivBasicsAuto(); } - ToNat([n % BOUND()] + FromNat(n / BOUND())); - n % BOUND() + ToNat(FromNat(n / BOUND())) * BOUND(); + ToNatRight([n % BASE()] + FromNat(n / BASE())); + n % BASE() + ToNatRight(FromNat(n / BASE())) * BASE(); { LemmaDivDecreasesAuto(); - LemmaNatSeqNat(n / BOUND()); + LemmaNatSeqNat(n / BASE()); } - n % BOUND() + n / BOUND() * BOUND(); - { LemmaFundamentalDivMod(n, BOUND()); } + n % BASE() + n / BASE() * BASE(); + { LemmaFundamentalDivMod(n, BASE()); } n; } } @@ -395,7 +401,7 @@ abstract module NatSeq { function method {:opaque} SeqExtend(xs: seq, n: nat): (ys: seq) requires |xs| <= n ensures |ys| == n - ensures ToNat(ys) == ToNat(xs) + ensures ToNatRight(ys) == ToNatRight(xs) decreases n - |xs| { if |xs| >= n then xs else LemmaSeqAppendZero(xs); SeqExtend(xs + [0], n) @@ -405,7 +411,7 @@ abstract module NatSeq { function method {:opaque} SeqExtendMultiple(xs: seq, n: nat): (ys: seq) requires n > 0 ensures |ys| % n == 0 - ensures ToNat(ys) == ToNat(xs) + ensures ToNatRight(ys) == ToNatRight(xs) { var newLen := |xs| + n - (|xs| % n); LemmaSubModNoopRight(|xs| + n, |xs|, n); @@ -419,9 +425,9 @@ abstract module NatSeq { /* Converts a nat to a sequence of a specified length. */ function method {:opaque} FromNatWithLen(n: nat, len: nat): (xs: seq) - requires Pow(BOUND(), len) > n + requires Pow(BASE(), len) > n ensures |xs| == len - ensures ToNat(xs) == n + ensures ToNatRight(xs) == n { LemmaFromNatLen(n, len); LemmaNatSeqNat(n); @@ -431,10 +437,10 @@ abstract module NatSeq { /* If the nat representation of a sequence is zero, then the sequence is a sequence of zeros. */ lemma LemmaSeqZero(xs: seq) - requires ToNat(xs) == 0 + requires ToNatRight(xs) == 0 ensures forall i :: 0 <= i < |xs| ==> xs[i] == 0 { - reveal ToNat(); + reveal ToNatRight(); if |xs| == 0 { } else { LemmaMulNonnegativeAuto(); @@ -449,9 +455,9 @@ abstract module NatSeq { function method {:opaque} SeqZero(len: nat): (xs: seq) ensures |xs| == len ensures forall i :: 0 <= i < |xs| ==> xs[i] == 0 - ensures ToNat(xs) == 0 + ensures ToNatRight(xs) == 0 { - LemmaPowPositive(BOUND(), len); + LemmaPowPositive(BASE(), len); var xs := FromNatWithLen(0, len); LemmaSeqZero(xs); xs @@ -461,18 +467,18 @@ abstract module NatSeq { sequence with the same length as the original sequence, we get the same sequence we started with. */ lemma LemmaSeqNatSeq(xs: seq) - ensures Pow(BOUND(), |xs|) > ToNat(xs) - ensures FromNatWithLen(ToNat(xs), |xs|) == xs + ensures Pow(BASE(), |xs|) > ToNatRight(xs) + ensures FromNatWithLen(ToNatRight(xs), |xs|) == xs { reveal FromNat(); - reveal ToNat(); + reveal ToNatRight(); LemmaSeqNatBound(xs); if |xs| > 0 { calc { - FromNatWithLen(ToNat(xs), |xs|) != xs; - { LemmaSeqNeq(FromNatWithLen(ToNat(xs), |xs|), xs); } - ToNat(FromNatWithLen(ToNat(xs), |xs|)) != ToNat(xs); - ToNat(xs) != ToNat(xs); + FromNatWithLen(ToNatRight(xs), |xs|) != xs; + { LemmaSeqNeq(FromNatWithLen(ToNatRight(xs), |xs|), xs); } + ToNatRight(FromNatWithLen(ToNatRight(xs), |xs|)) != ToNatRight(xs); + ToNatRight(xs) != ToNatRight(xs); false; } } @@ -495,8 +501,8 @@ abstract module NatSeq { else var (zs', cin) := SeqAdd(DropLast(xs), DropLast(ys)); var sum: int := Last(xs) + Last(ys) + cin; - var (sum_out, cout) := if sum < BOUND() then (sum, 0) - else (sum - BOUND(), 1); + var (sum_out, cout) := if sum < BASE() then (sum, 0) + else (sum - BASE(), 1); (zs' + [sum_out], cout) } @@ -505,38 +511,38 @@ abstract module NatSeq { lemma LemmaSeqAdd(xs: seq, ys: seq, zs: seq, cout: nat) requires |xs| == |ys| requires SeqAdd(xs, ys) == (zs, cout) - ensures ToNat(xs) + ToNat(ys) == ToNat(zs) + cout * Pow(BOUND(), |xs|) + ensures ToNatRight(xs) + ToNatRight(ys) == ToNatRight(zs) + cout * Pow(BASE(), |xs|) { reveal SeqAdd(); if |xs| == 0 { - reveal ToNat(); + reveal ToNatRight(); } else { - var pow := Pow(BOUND(), |xs| - 1); + var pow := Pow(BASE(), |xs| - 1); var (zs', cin) := SeqAdd(DropLast(xs), DropLast(ys)); var sum: int := Last(xs) + Last(ys) + cin; - var z := if sum < BOUND() then sum else sum - BOUND(); - assert sum == z + cout * BOUND(); + var z := if sum < BASE() then sum else sum - BASE(); + assert sum == z + cout * BASE(); - reveal ToNatRev(); - LemmaToNatEqToNatRevAuto(); + reveal ToNatLeft(); + LemmaToNatLeftEqToNatRightAuto(); calc { - ToNat(zs); - ToNatRev(zs); - ToNatRev(zs') + z * pow; + ToNatRight(zs); + ToNatLeft(zs); + ToNatLeft(zs') + z * pow; { LemmaSeqAdd(DropLast(xs), DropLast(ys), zs', cin); } - ToNatRev(DropLast(xs)) + ToNatRev(DropLast(ys)) - cin * pow + z * pow; + ToNatLeft(DropLast(xs)) + ToNatLeft(DropLast(ys)) - cin * pow + z * pow; { LemmaMulEqualityAuto(); - assert sum * pow == (z + cout * BOUND()) * pow; + assert sum * pow == (z + cout * BASE()) * pow; LemmaMulIsDistributiveAuto(); } - ToNatRev(xs) + ToNatRev(ys) - cout * BOUND() * pow; + ToNatLeft(xs) + ToNatLeft(ys) - cout * BASE() * pow; { - LemmaMulIsAssociative(cout, BOUND(), pow); + LemmaMulIsAssociative(cout, BASE(), pow); reveal Pow(); } - ToNatRev(xs) + ToNatRev(ys) - cout * Pow(BOUND(), |xs|); - ToNat(xs) + ToNat(ys) - cout * Pow(BOUND(), |xs|); + ToNatLeft(xs) + ToNatLeft(ys) - cout * Pow(BASE(), |xs|); + ToNatRight(xs) + ToNatRight(ys) - cout * Pow(BASE(), |xs|); } } } @@ -553,7 +559,7 @@ abstract module NatSeq { var (zs, cin) := SeqSub(DropLast(xs), DropLast(ys)); var (diff_out, cout) := if Last(xs) >= Last(ys) + cin then (Last(xs) - Last(ys) - cin, 0) - else (BOUND() + Last(xs) - Last(ys) - cin, 1); + else (BASE() + Last(xs) - Last(ys) - cin, 1); (zs + [diff_out], cout) } @@ -562,39 +568,39 @@ abstract module NatSeq { lemma LemmaSeqSub(xs: seq, ys: seq, zs: seq, cout: nat) requires |xs| == |ys| requires SeqSub(xs, ys) == (zs, cout) - ensures ToNat(xs) - ToNat(ys) + cout * Pow(BOUND(), |xs|) == ToNat(zs) + ensures ToNatRight(xs) - ToNatRight(ys) + cout * Pow(BASE(), |xs|) == ToNatRight(zs) { reveal SeqSub(); if |xs| == 0 { - reveal ToNat(); + reveal ToNatRight(); } else { - var pow := Pow(BOUND(), |xs| - 1); + var pow := Pow(BASE(), |xs| - 1); var (zs', cin) := SeqSub(DropLast(xs), DropLast(ys)); var z := if Last(xs) >= Last(ys) + cin then Last(xs) - Last(ys) - cin - else BOUND() + Last(xs) - Last(ys) - cin; - assert cout * BOUND() + Last(xs) - cin - Last(ys) == z; + else BASE() + Last(xs) - Last(ys) - cin; + assert cout * BASE() + Last(xs) - cin - Last(ys) == z; - reveal ToNatRev(); - LemmaToNatEqToNatRevAuto(); + reveal ToNatLeft(); + LemmaToNatLeftEqToNatRightAuto(); calc { - ToNat(zs); - ToNatRev(zs); - ToNatRev(zs') + z * pow; + ToNatRight(zs); + ToNatLeft(zs); + ToNatLeft(zs') + z * pow; { LemmaSeqSub(DropLast(xs), DropLast(ys), zs', cin); } - ToNatRev(DropLast(xs)) - ToNatRev(DropLast(ys)) + cin * pow + z * pow; + ToNatLeft(DropLast(xs)) - ToNatLeft(DropLast(ys)) + cin * pow + z * pow; { LemmaMulEqualityAuto(); - assert pow * (cout * BOUND() + Last(xs) - cin - Last(ys)) == pow * z; + assert pow * (cout * BASE() + Last(xs) - cin - Last(ys)) == pow * z; LemmaMulIsDistributiveAuto(); } - ToNatRev(xs) - ToNatRev(ys) + cout * BOUND() * pow; + ToNatLeft(xs) - ToNatLeft(ys) + cout * BASE() * pow; { - LemmaMulIsAssociative(cout, BOUND(), pow); + LemmaMulIsAssociative(cout, BASE(), pow); reveal Pow(); } - ToNatRev(xs) - ToNatRev(ys) + cout * Pow(BOUND(), |xs|); - ToNat(xs) - ToNat(ys) + cout * Pow(BOUND(), |xs|); + ToNatLeft(xs) - ToNatLeft(ys) + cout * Pow(BASE(), |xs|); + ToNatRight(xs) - ToNatRight(ys) + cout * Pow(BASE(), |xs|); } } } diff --git a/src/Collections/Sequences/NatSeqConversions.dfy b/src/Collections/Sequences/NatSeqConversions.dfy index fe530cfd..2a406efc 100644 --- a/src/Collections/Sequences/NatSeqConversions.dfy +++ b/src/Collections/Sequences/NatSeqConversions.dfy @@ -12,13 +12,13 @@ include "../../NonlinearArithmetic/Power.dfy" include "Seq.dfy" include "NatSeq.dfy" -/* Sequence with smaller bound. */ +/* Sequence with smaller base. */ abstract module SmallSeq refines NatSeq { function method BITS(): nat ensures BITS() > 1 - function method BOUND(): nat + function method BASE(): nat { LemmaPowPositive(2, BITS() - 1); LemmaPowStrictlyIncreases(2, BITS() - 1, BITS()); @@ -27,7 +27,7 @@ abstract module SmallSeq refines NatSeq { } -/* Sequence with larger bound. */ +/* Sequence with larger base. */ abstract module LargeSeq refines NatSeq { import Small : SmallSeq @@ -35,7 +35,7 @@ abstract module LargeSeq refines NatSeq { function method BITS(): nat ensures BITS() > Small.BITS() && BITS() % Small.BITS() == 0 - function method BOUND(): nat + function method BASE(): nat { LemmaPowPositive(2, BITS() - 1); LemmaPowStrictlyIncreases(2, BITS() - 1, BITS()); @@ -53,9 +53,9 @@ abstract module NatSeqConversions { import opened Large : LargeSeq - /* Small.BOUND() to the power of E is Large.BOUND(). */ + /* Small.BASE() to the power of E is Large.BASE(). */ function method E(): (E: nat) - ensures Pow(Small.BOUND(), E) == Large.BOUND() + ensures Pow(Small.BASE(), E) == Large.BASE() ensures E > 0 { LemmaDivBasicsAuto(); @@ -64,7 +64,7 @@ abstract module NatSeqConversions { Large.BITS() / Small.BITS() } - /* Converts a sequence from Large.BOUND() to Small.BOUND(). */ + /* Converts a sequence from Large.BASE() to Small.BASE(). */ function method {:opaque} ToSmall(xs: seq): (ys: seq) ensures |ys| == |xs| * E() { @@ -74,7 +74,7 @@ abstract module NatSeqConversions { Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs)) } - /* Converts a sequence from Small.BOUND() to Large.BOUND(). */ + /* Converts a sequence from Small.BASE() to Large.BASE(). */ function method {:opaque} ToLarge(xs: seq): (ys: seq) requires |xs| % E() == 0 ensures |ys| == |xs| / E() @@ -87,56 +87,56 @@ abstract module NatSeqConversions { Small.LemmaSeqNatBound(xs[..E()]); LemmaModSubMultiplesVanishAuto(); LemmaDivMinusOne(|xs|, E()); - [Small.ToNat(xs[..E()]) as Large.uint] + ToLarge(xs[E()..]) + [Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..]) } - /* Sequence conversion from Large.BOUND() to Small.BOUND() does not + /* Sequence conversion from Large.BASE() to Small.BASE() does not change its nat representation. */ lemma LemmaToSmall(xs: seq) - ensures Small.ToNat(ToSmall(xs)) == Large.ToNat(xs) + ensures Small.ToNatRight(ToSmall(xs)) == Large.ToNatRight(xs) { - reveal Small.ToNat(); - reveal Large.ToNat(); + reveal Small.ToNatRight(); + reveal Large.ToNatRight(); reveal ToSmall(); if |xs| == 0 { } else { calc { - Small.ToNat(ToSmall(xs)); - Small.ToNat(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); + Small.ToNatRight(ToSmall(xs)); + Small.ToNatRight(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); { Small.LemmaSeqPrefix(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs)), E()); LemmaToSmall(DropFirst(xs)); } - First(xs) + Large.ToNat(DropFirst(xs)) * Pow(Small.BOUND(), E()); - { assert Pow(Small.BOUND(), E()) == Large.BOUND(); } - Large.ToNat(xs); + First(xs) + Large.ToNatRight(DropFirst(xs)) * Pow(Small.BASE(), E()); + { assert Pow(Small.BASE(), E()) == Large.BASE(); } + Large.ToNatRight(xs); } } } - /* Sequence conversion from Small.BOUND() to Large.BOUND() does not + /* Sequence conversion from Small.BASE() to Large.BASE() does not change its nat representation. */ lemma LemmaToLarge(xs: seq) requires |xs| % E() == 0 - ensures Large.ToNat(ToLarge(xs)) == Small.ToNat(xs) + ensures Large.ToNatRight(ToLarge(xs)) == Small.ToNatRight(xs) { - reveal Large.ToNat(); - reveal Small.ToNat(); + reveal Large.ToNatRight(); + reveal Small.ToNatRight(); reveal ToLarge(); if |xs| == 0 { } else { calc { - Large.ToNat(ToLarge(xs)); + Large.ToNatRight(ToLarge(xs)); { LemmaModIsZero(|xs|, E()); LemmaModSubMultiplesVanishAuto(); Small.LemmaSeqNatBound(xs[..E()]); } - Large.ToNat([Small.ToNat(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); + Large.ToNatRight([Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); { LemmaToLarge(xs[E()..]); } - Small.ToNat(xs[..E()]) + Small.ToNat(xs[E()..]) * Pow(Small.BOUND(), E()); + Small.ToNatRight(xs[..E()]) + Small.ToNatRight(xs[E()..]) * Pow(Small.BASE(), E()); { Small.LemmaSeqPrefix(xs, E()); } - Small.ToNat(xs); + Small.ToNatRight(xs); } } } @@ -149,7 +149,7 @@ abstract module NatSeqConversions { { LemmaToSmall(xs); LemmaToSmall(ys); - assert Large.ToNat(xs) == Large.ToNat(ys); + assert Large.ToNatRight(xs) == Large.ToNatRight(ys); Large.LemmaSeqEq(xs, ys); } @@ -162,7 +162,7 @@ abstract module NatSeqConversions { { LemmaToLarge(xs); LemmaToLarge(ys); - assert Small.ToNat(xs) == Small.ToNat(ys); + assert Small.ToNatRight(xs) == Small.ToNatRight(ys); Small.LemmaSeqEq(xs, ys); } @@ -183,8 +183,8 @@ abstract module NatSeqConversions { Small.LemmaSeqNatBound(xs[..E()]); LemmaModSubMultiplesVanishAuto(); } - ToSmall([Small.ToNat(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); - Small.FromNatWithLen(Small.ToNat(xs[..E()]), E()) + ToSmall(ToLarge(xs[E()..])); + ToSmall([Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); + Small.FromNatWithLen(Small.ToNatRight(xs[..E()]), E()) + ToSmall(ToLarge(xs[E()..])); { Small.LemmaSeqNatSeq(xs[..E()]); LemmaSmallLargeSmall(xs[E()..]); @@ -208,7 +208,7 @@ abstract module NatSeqConversions { calc { ToLarge(ToSmall(xs)); ToLarge(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); - [Small.ToNat(Small.FromNatWithLen(First(xs), E())) as Large.uint] + ToLarge(ToSmall(DropFirst(xs))); + [Small.ToNatRight(Small.FromNatWithLen(First(xs), E())) as Large.uint] + ToLarge(ToSmall(DropFirst(xs))); [First(xs)] + ToLarge(ToSmall(DropFirst(xs))); { LemmaLargeSmallLarge(DropFirst(xs)); } [First(xs)] + DropFirst(xs); diff --git a/src/NativeTypes.dfy b/src/NativeTypes.dfy deleted file mode 100644 index 71ecd7e9..00000000 --- a/src/NativeTypes.dfy +++ /dev/null @@ -1,39 +0,0 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -module NativeTypes { - const BASE_0: int := 1 - - const BASE_1: int := 2 - const BASE_2: int := 4 - const BASE_4: int := 16 - const BASE_5: int := 32 - const BASE_8: int := 0x1_00 - const BASE_16: int := 0x1_0000 - const BASE_24: int := 0x1_000000 - const BASE_32: int := 0x1_00000000 - const BASE_40: int := 0x1_00000000_00 - const BASE_48: int := 0x1_00000000_0000 - const BASE_56: int := 0x1_00000000_000000 - const BASE_64: int := 0x1_00000000_00000000 - const BASE_128: int := 0x1_00000000_00000000_00000000_00000000 - const BASE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000 - const BASE_512: int := - 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; - - newtype uint8 = x:int | 0 <= x < 0x1_00 - newtype uint16 = x: int | 0 <= x < 0x1_0000 - newtype uint32 = x: int | 0 <= x < 0x1_00000000 - newtype uint64 = x: int | 0 <= x < 0x1_00000000_00000000 - - newtype int8 = x: int | -0x80 <= x < 0x80 - newtype int16 = x: int | -0x8000 <= x < 0x8000 - newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 - newtype int64 = x: int | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 - - newtype nat8 = x: int | 0 <= x < 0x80 - 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 - -} From 6013e6e9e7f058fd7df59643f8b5094a52e231a8 Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Mon, 13 Sep 2021 09:01:02 -0700 Subject: [PATCH 11/36] Add example with custom small and large widths --- examples/NatSeq/NatSeqCustomExample.dfy | 42 +++++++++++++++++++ .../NatSeq/NatSeqCustomExample.dfy.expect | 2 + 2 files changed, 44 insertions(+) create mode 100644 examples/NatSeq/NatSeqCustomExample.dfy create mode 100644 examples/NatSeq/NatSeqCustomExample.dfy.expect diff --git a/examples/NatSeq/NatSeqCustomExample.dfy b/examples/NatSeq/NatSeqCustomExample.dfy new file mode 100644 index 00000000..866af936 --- /dev/null +++ b/examples/NatSeq/NatSeqCustomExample.dfy @@ -0,0 +1,42 @@ +// RUN: %dafny /compile:3 /noNLarith "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +include "../../src/Collections/Sequences/NatSeqConversions.dfy" + +module Uint3_6 refines NatSeqConversions { + + module Uint3Seq refines SmallSeq { + function method BITS(): nat { 3 } + } + module Uint6Seq refines LargeSeq { + import Small = Uint3Seq + function method BITS(): nat { 6 } + } + import opened Large = Uint6Seq + import Small = Large.Small + +} + +module NatSeqExample { + + import opened Uint3_6 + + method Main() { + var n := 165; + + // Convert n to uint3 and uint6 sequences + var smallSeq, largeSeq := Small.FromNat(n), Large.FromNat(n); + expect smallSeq == [5, 4, 2]; + expect largeSeq == [37, 2]; + + Small.LemmaNatSeqNat(n); + Large.LemmaNatSeqNat(n); + assert Small.ToNatRight(smallSeq) == Large.ToNatRight(largeSeq) == n; + } + +} diff --git a/examples/NatSeq/NatSeqCustomExample.dfy.expect b/examples/NatSeq/NatSeqCustomExample.dfy.expect new file mode 100644 index 00000000..19c94d8b --- /dev/null +++ b/examples/NatSeq/NatSeqCustomExample.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 64 verified, 0 errors From 0c527a289198b25309ff643d2ff051126ded918f Mon Sep 17 00:00:00 2001 From: sarahc7 Date: Mon, 13 Sep 2021 09:19:26 -0700 Subject: [PATCH 12/36] More name changes --- .../LittleEndianNatCustomExample.dfy} | 6 +++--- .../LittleEndianNatCustomExample.dfy.expect | 2 ++ .../LittleEndianNatExample.dfy} | 4 ++-- .../LittleEndianNatExample.dfy.expect} | 0 examples/NatSeq/NatSeqCustomExample.dfy.expect | 2 -- .../{NatSeq.dfy => LittleEndianNat.dfy} | 2 +- ...q.dfy.expect => LittleEndianNat.dfy.expect} | 0 ...ions.dfy => LittleEndianNatConversions.dfy} | 18 +++++++++--------- ...t => LittleEndianNatConversions.dfy.expect} | 0 9 files changed, 17 insertions(+), 17 deletions(-) rename examples/{NatSeq/NatSeqCustomExample.dfy => LittleEndianNat/LittleEndianNatCustomExample.dfy} (85%) create mode 100644 examples/LittleEndianNat/LittleEndianNatCustomExample.dfy.expect rename examples/{NatSeq/NatSeqExample.dfy => LittleEndianNat/LittleEndianNatExample.dfy} (92%) rename examples/{NatSeq/NatSeqExample.dfy.expect => LittleEndianNat/LittleEndianNatExample.dfy.expect} (100%) delete mode 100644 examples/NatSeq/NatSeqCustomExample.dfy.expect rename src/Collections/Sequences/{NatSeq.dfy => LittleEndianNat.dfy} (99%) rename src/Collections/Sequences/{NatSeq.dfy.expect => LittleEndianNat.dfy.expect} (100%) rename src/Collections/Sequences/{NatSeqConversions.dfy => LittleEndianNatConversions.dfy} (94%) rename src/Collections/Sequences/{NatSeqConversions.dfy.expect => LittleEndianNatConversions.dfy.expect} (100%) diff --git a/examples/NatSeq/NatSeqCustomExample.dfy b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy similarity index 85% rename from examples/NatSeq/NatSeqCustomExample.dfy rename to examples/LittleEndianNat/LittleEndianNatCustomExample.dfy index 866af936..2c497afe 100644 --- a/examples/NatSeq/NatSeqCustomExample.dfy +++ b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy @@ -6,9 +6,9 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "../../src/Collections/Sequences/NatSeqConversions.dfy" +include "../../src/Collections/Sequences/LittleEndianNatConversions.dfy" -module Uint3_6 refines NatSeqConversions { +module Uint3_6 refines LittleEndianNatConversions { module Uint3Seq refines SmallSeq { function method BITS(): nat { 3 } @@ -22,7 +22,7 @@ module Uint3_6 refines NatSeqConversions { } -module NatSeqExample { +module LittleEndianNatCustomExample { import opened Uint3_6 diff --git a/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy.expect b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy.expect new file mode 100644 index 00000000..a4d7ffed --- /dev/null +++ b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 76 verified, 0 errors diff --git a/examples/NatSeq/NatSeqExample.dfy b/examples/LittleEndianNat/LittleEndianNatExample.dfy similarity index 92% rename from examples/NatSeq/NatSeqExample.dfy rename to examples/LittleEndianNat/LittleEndianNatExample.dfy index e10b3c45..8c121002 100644 --- a/examples/NatSeq/NatSeqExample.dfy +++ b/examples/LittleEndianNat/LittleEndianNatExample.dfy @@ -6,9 +6,9 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -include "../../src/Collections/Sequences/NatSeqConversions.dfy" +include "../../src/Collections/Sequences/LittleEndianNatConversions.dfy" -module NatSeqExample { +module LittleEndianNatExample { import opened Uint8_32 diff --git a/examples/NatSeq/NatSeqExample.dfy.expect b/examples/LittleEndianNat/LittleEndianNatExample.dfy.expect similarity index 100% rename from examples/NatSeq/NatSeqExample.dfy.expect rename to examples/LittleEndianNat/LittleEndianNatExample.dfy.expect diff --git a/examples/NatSeq/NatSeqCustomExample.dfy.expect b/examples/NatSeq/NatSeqCustomExample.dfy.expect deleted file mode 100644 index 19c94d8b..00000000 --- a/examples/NatSeq/NatSeqCustomExample.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 64 verified, 0 errors diff --git a/src/Collections/Sequences/NatSeq.dfy b/src/Collections/Sequences/LittleEndianNat.dfy similarity index 99% rename from src/Collections/Sequences/NatSeq.dfy rename to src/Collections/Sequences/LittleEndianNat.dfy index 5e08bdd7..bd792672 100644 --- a/src/Collections/Sequences/NatSeq.dfy +++ b/src/Collections/Sequences/LittleEndianNat.dfy @@ -18,7 +18,7 @@ include "../../NonlinearArithmetic/Mul.dfy" include "../../NonlinearArithmetic/Power.dfy" include "Seq.dfy" -abstract module NatSeq { +abstract module LittleEndianNat { import opened DivMod import opened Mul diff --git a/src/Collections/Sequences/NatSeq.dfy.expect b/src/Collections/Sequences/LittleEndianNat.dfy.expect similarity index 100% rename from src/Collections/Sequences/NatSeq.dfy.expect rename to src/Collections/Sequences/LittleEndianNat.dfy.expect diff --git a/src/Collections/Sequences/NatSeqConversions.dfy b/src/Collections/Sequences/LittleEndianNatConversions.dfy similarity index 94% rename from src/Collections/Sequences/NatSeqConversions.dfy rename to src/Collections/Sequences/LittleEndianNatConversions.dfy index 2a406efc..db97cc84 100644 --- a/src/Collections/Sequences/NatSeqConversions.dfy +++ b/src/Collections/Sequences/LittleEndianNatConversions.dfy @@ -10,10 +10,10 @@ include "../../NonlinearArithmetic/DivMod.dfy" include "../../NonlinearArithmetic/Mul.dfy" include "../../NonlinearArithmetic/Power.dfy" include "Seq.dfy" -include "NatSeq.dfy" +include "LittleEndianNat.dfy" /* Sequence with smaller base. */ -abstract module SmallSeq refines NatSeq { +abstract module SmallSeq refines LittleEndianNat { function method BITS(): nat ensures BITS() > 1 @@ -28,7 +28,7 @@ abstract module SmallSeq refines NatSeq { } /* Sequence with larger base. */ -abstract module LargeSeq refines NatSeq { +abstract module LargeSeq refines LittleEndianNat { import Small : SmallSeq @@ -44,7 +44,7 @@ abstract module LargeSeq refines NatSeq { } -abstract module NatSeqConversions { +abstract module LittleEndianNatConversions { import opened DivMod import opened Mul @@ -220,7 +220,7 @@ abstract module NatSeqConversions { } /* Conversions between sequences of uint8 and uint16. */ -module Uint8_16 refines NatSeqConversions { +module Uint8_16 refines LittleEndianNatConversions { module Uint8Seq refines SmallSeq { function method BITS(): nat { 8 } @@ -237,7 +237,7 @@ module Uint8_16 refines NatSeqConversions { } /* Conversions between sequences of uint8 and uint32. */ -module Uint8_32 refines NatSeqConversions { +module Uint8_32 refines LittleEndianNatConversions { module Uint8Seq refines SmallSeq { function method BITS(): nat { 8 } @@ -254,7 +254,7 @@ module Uint8_32 refines NatSeqConversions { } /* Conversions between sequences of uint8 and uint64. */ -module Uint8_64 refines NatSeqConversions { +module Uint8_64 refines LittleEndianNatConversions { module Uint8Seq refines SmallSeq { function method BITS(): nat { 8 } @@ -271,7 +271,7 @@ module Uint8_64 refines NatSeqConversions { } /* Conversions between sequences of uint16 and uint32. */ -module Uint16_32 refines NatSeqConversions { +module Uint16_32 refines LittleEndianNatConversions { module Uint16Seq refines SmallSeq { function method BITS(): nat { 16 } @@ -288,7 +288,7 @@ module Uint16_32 refines NatSeqConversions { } /* Conversions between sequences of uint32 and uint64. */ -module Uint32_64 refines NatSeqConversions { +module Uint32_64 refines LittleEndianNatConversions { module Uint32Seq refines SmallSeq { function method BITS(): nat { 32 } diff --git a/src/Collections/Sequences/NatSeqConversions.dfy.expect b/src/Collections/Sequences/LittleEndianNatConversions.dfy.expect similarity index 100% rename from src/Collections/Sequences/NatSeqConversions.dfy.expect rename to src/Collections/Sequences/LittleEndianNatConversions.dfy.expect From 0d0649e6e6b748547b44bfa87de3309c150e5daf Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Nov 2021 18:45:49 -0700 Subject: [PATCH 13/36] Pick up Dafny 3.3, add verification results report --- .github/workflows/tests.yml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index ee85741f..6e728fda 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -12,12 +12,14 @@ jobs: - name: Install Dafny uses: tchajed/setup-dafny-action@v1 with: - dafny-version: "3.2.0" + dafny-version: "3.3.0" - - uses: actions/setup-python@v1 + - name: Verify Dafny Code + run: dafny /verificationLogger:trx **/*.dfy - - name: Install lit - run: pip install lit OutputCheck - - - name: Verify/Test Dafny code - run: lit --time-tests -v . + - name: Publish Verification Results + uses: dorny/test-reporter@v1 + with: + name: Verification Results + path: '**/*.trx' + reporter: dotnet-trx From 6c5d6ecbe0659f1ba62e4aa5cbc987080e6849bc Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Nov 2021 18:49:25 -0700 Subject: [PATCH 14/36] See if using an environment allows CI to post results from a fork --- .github/workflows/tests.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 6e728fda..b5b1227a 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -6,6 +6,7 @@ on: ["pull_request", "push"] jobs: verification: runs-on: ubuntu-latest + environment: continuous-integration steps: - uses: actions/checkout@v2 From 03d2c9e6c02218f01165cfc21212444d089c4c91 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Nov 2021 18:55:04 -0700 Subject: [PATCH 15/36] No luck, try documented workaround --- .github/workflows/test-report.yml | 16 ++++++++++++++++ .github/workflows/tests.yml | 10 ++++------ 2 files changed, 20 insertions(+), 6 deletions(-) create mode 100644 .github/workflows/test-report.yml diff --git a/.github/workflows/test-report.yml b/.github/workflows/test-report.yml new file mode 100644 index 00000000..66909938 --- /dev/null +++ b/.github/workflows/test-report.yml @@ -0,0 +1,16 @@ +name: 'Test Report' +on: + workflow_run: + workflows: ['CI'] # runs after CI workflow + types: + - completed +jobs: + report: + runs-on: ubuntu-latest + steps: + - uses: dorny/test-reporter@v1 + with: + artifact: verification-results + name: Verification Tests + path: '*.trx' + reporter: dotnet-trx \ No newline at end of file diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index b5b1227a..1e66ddb0 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -6,7 +6,6 @@ on: ["pull_request", "push"] jobs: verification: runs-on: ubuntu-latest - environment: continuous-integration steps: - uses: actions/checkout@v2 @@ -18,9 +17,8 @@ jobs: - name: Verify Dafny Code run: dafny /verificationLogger:trx **/*.dfy - - name: Publish Verification Results - uses: dorny/test-reporter@v1 + - uses: actions/upload-artifact@v2 # upload test results + if: success() || failure() # run this step even if previous step failed with: - name: Verification Results - path: '**/*.trx' - reporter: dotnet-trx + name: verification-results + path: 'TestResults/*.trx' From 0d19733102cc036ffdd9fad9219311c30e81e227 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Nov 2021 20:58:51 -0700 Subject: [PATCH 16/36] Dummy verification-breaking change --- src/Wrappers.dfy | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy index 8e2e6d8d..7e9189b1 100644 --- a/src/Wrappers.dfy +++ b/src/Wrappers.dfy @@ -90,4 +90,10 @@ module Wrappers { { if condition then Pass else Fail(error) } + + // Dummy verification-breaking change + function Foo(): int { + assert false; + 42 + } } From 6460f3da18a3cd8a1511e18ac4afbfe33a2b5982 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Nov 2021 22:17:02 -0700 Subject: [PATCH 17/36] Fix wrong workflow symbol --- .github/workflows/test-report.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-report.yml b/.github/workflows/test-report.yml index 66909938..df5b8f68 100644 --- a/.github/workflows/test-report.yml +++ b/.github/workflows/test-report.yml @@ -1,7 +1,7 @@ name: 'Test Report' on: workflow_run: - workflows: ['CI'] # runs after CI workflow + workflows: ['tests'] # runs after CI workflow types: - completed jobs: From 0f2e4951efa97d5e725fd03c9642ae3478cb6cde Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Nov 2021 22:19:10 -0700 Subject: [PATCH 18/36] Revert "Dummy verification-breaking change" This reverts commit 0d19733102cc036ffdd9fad9219311c30e81e227. --- src/Wrappers.dfy | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy index 7e9189b1..8e2e6d8d 100644 --- a/src/Wrappers.dfy +++ b/src/Wrappers.dfy @@ -90,10 +90,4 @@ module Wrappers { { if condition then Pass else Fail(error) } - - // Dummy verification-breaking change - function Foo(): int { - assert false; - 42 - } } From b52462d020c25d629ef9e74b57443169875a2974 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 9 Feb 2022 11:57:46 -0800 Subject: [PATCH 19/36] Move to Dafny 3.4 and add CSV verification output --- .github/workflows/tests.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 1e66ddb0..0cc2a284 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -12,10 +12,10 @@ jobs: - name: Install Dafny uses: tchajed/setup-dafny-action@v1 with: - dafny-version: "3.3.0" + dafny-version: "3.4.0" - name: Verify Dafny Code - run: dafny /verificationLogger:trx **/*.dfy + run: dafny /verificationLogger:trx /verificationLogger:csv **/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 045408ad5c26044a82865a85a3ec72d879b31154 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Mar 2022 09:37:16 -0800 Subject: [PATCH 20/36] Fix bad quotes --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 0b39c7bb..504fbdaa 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -19,7 +19,7 @@ jobs: dafny-version: "3.4.2" - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv '**/*.dfy' + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv **/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 3be0e51e5aef4869cc341862f59d3d85b70d6521 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Mar 2022 09:42:49 -0800 Subject: [PATCH 21/36] Trying to fix ** globbing --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 504fbdaa..6cda2937 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -19,7 +19,7 @@ jobs: dafny-version: "3.4.2" - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv **/*.dfy + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/**/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From f675930fb64cc7dffe2326f6d787de8bf004bdeb Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Mar 2022 09:51:24 -0800 Subject: [PATCH 22/36] Avoid NonLinearArithmetic for now --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 6cda2937..ed0d8839 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -19,7 +19,7 @@ jobs: dafny-version: "3.4.2" - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/**/*.dfy + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/**/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 9bc2e6dc09052380f599e62795ab83438de6d8ba Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Mar 2022 11:05:18 -0800 Subject: [PATCH 23/36] Ah Sequences is hiding some /noNLArith flags as well --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index ed0d8839..ecb93ea0 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -19,7 +19,7 @@ jobs: dafny-version: "3.4.2" - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/**/*.dfy + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Sets/**/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From aa1927eb7b70185daa7beab74139e002e0df924d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Mar 2022 11:09:29 -0800 Subject: [PATCH 24/36] Typo --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index ecb93ea0..55e08702 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -19,7 +19,7 @@ jobs: dafny-version: "3.4.2" - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Sets/**/*.dfy + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/Sets/**/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 12426a069df50da839972a501d0c54e4e65b4e27 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 2 Mar 2022 11:42:17 -0800 Subject: [PATCH 25/36] Sigh --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 55e08702..0a2c3241 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -19,7 +19,7 @@ jobs: dafny-version: "3.4.2" - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/Sets/**/*.dfy + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/Sets/*.dfy - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 548a9dfc1dbb56b77d26ff779aa653ef5615b108 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 9 Mar 2022 15:57:09 -0800 Subject: [PATCH 26/36] Add Dafny verification report --- .github/workflows/tests.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 0a2c3241..a71dea3c 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -18,9 +18,16 @@ jobs: with: dafny-version: "3.4.2" + - name: Install Dafny report generator + run: dotnet tool install --global dafny-reportgenerator + - name: Verify Dafny Code run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/Sets/*.dfy + - name: Generate Report + # TODO: temporary intentional failure to verify it stops the build + run: dafny-reportgenerator summarize-csv-results --max-resource-count 5 TestResults/*.csv + - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed with: From 717d820b6f944f3697904f05dc427e79e8266d0f Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 9 Mar 2022 16:33:18 -0800 Subject: [PATCH 27/36] Trying to get globbing to work --- .github/workflows/tests.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index a71dea3c..69cfa385 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -22,11 +22,10 @@ jobs: run: dotnet tool install --global dafny-reportgenerator - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/Collections/Sets/*.dfy + run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/NonlinearArithmetic/**/*.dfy - name: Generate Report - # TODO: temporary intentional failure to verify it stops the build - run: dafny-reportgenerator summarize-csv-results --max-resource-count 5 TestResults/*.csv + run: dafny-reportgenerator summarize-csv-results --max-resource-count 1000000 TestResults/*.csv - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From f6ad1641d0b404ba752888ec5b10b0046a23788c Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 9 Mar 2022 16:34:52 -0800 Subject: [PATCH 28/36] Missing flag --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 69cfa385..1cde826a 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -22,7 +22,7 @@ jobs: run: dotnet tool install --global dafny-reportgenerator - name: Verify Dafny Code - run: dafny /compile:0 /trace /verificationLogger:trx /verificationLogger:csv src/NonlinearArithmetic/**/*.dfy + run: dafny /compile:0 /trace /noNLarith /verificationLogger:trx /verificationLogger:csv src/NonlinearArithmetic/**/*.dfy - name: Generate Report run: dafny-reportgenerator summarize-csv-results --max-resource-count 1000000 TestResults/*.csv From 5fc4b193949545023d4d634d005be76bc7f57432 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 9 Mar 2022 21:02:07 -0800 Subject: [PATCH 29/36] Remove dafny option that overrides dafny exit code MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This way there’s no need to explicitly check the output for errors, so we can nuke all the .expect files --- .gitignore | 1 + examples/LittleEndianNat/LittleEndianNatCustomExample.dfy | 3 +-- examples/LittleEndianNat/LittleEndianNatExample.dfy | 3 +-- examples/Wrappers.dfy | 3 +-- lit.site.cfg | 3 --- src/BoundedInts.dfy | 3 +-- src/BoundedInts.dfy.expect | 2 -- src/Collections/Maps/Imaps.dfy | 3 +-- src/Collections/Maps/Imaps.dfy.expect | 2 -- src/Collections/Maps/Maps.dfy | 3 +-- src/Collections/Maps/Maps.dfy.expect | 2 -- src/Collections/Sequences/LittleEndianNat.dfy | 3 +-- src/Collections/Sequences/LittleEndianNat.dfy.expect | 2 -- src/Collections/Sequences/LittleEndianNatConversions.dfy | 3 +-- .../Sequences/LittleEndianNatConversions.dfy.expect | 2 -- src/Collections/Sequences/Seq.dfy | 3 +-- src/Collections/Sequences/Seq.dfy.expect | 2 -- src/Collections/Sets/Isets.dfy | 3 +-- src/Collections/Sets/Isets.dfy.expect | 2 -- src/Collections/Sets/Sets.dfy | 3 +-- src/Collections/Sets/Sets.dfy.expect | 2 -- src/Functions.dfy | 3 +-- src/Functions.dfy.expect | 2 -- src/Math.dfy | 3 +-- src/Math.dfy.expect | 2 -- src/NonlinearArithmetic/DivMod.dfy | 3 +-- src/NonlinearArithmetic/DivMod.dfy.expect | 6 ------ src/NonlinearArithmetic/Internals/DivInternals.dfy | 3 +-- src/NonlinearArithmetic/Internals/DivInternals.dfy.expect | 2 -- src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy | 3 +-- .../Internals/DivInternalsNonlinear.dfy.expect | 2 -- src/NonlinearArithmetic/Internals/GeneralInternals.dfy | 3 +-- .../Internals/GeneralInternals.dfy.expect | 2 -- src/NonlinearArithmetic/Internals/ModInternals.dfy | 3 +-- src/NonlinearArithmetic/Internals/ModInternals.dfy.expect | 2 -- src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy | 3 +-- .../Internals/ModInternalsNonlinear.dfy.expect | 2 -- src/NonlinearArithmetic/Internals/MulInternals.dfy | 3 +-- src/NonlinearArithmetic/Internals/MulInternals.dfy.expect | 2 -- src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy | 3 +-- .../Internals/MulInternalsNonlinear.dfy.expect | 2 -- src/NonlinearArithmetic/Mul.dfy | 3 +-- src/NonlinearArithmetic/Mul.dfy.expect | 2 -- src/NonlinearArithmetic/Power.dfy | 3 +-- src/NonlinearArithmetic/Power.dfy.expect | 2 -- src/NonlinearArithmetic/Power2.dfy | 3 +-- src/NonlinearArithmetic/Power2.dfy.expect | 2 -- src/Wrappers.dfy | 3 +-- src/Wrappers.dfy.expect | 2 -- 49 files changed, 26 insertions(+), 101 deletions(-) delete mode 100644 src/BoundedInts.dfy.expect delete mode 100644 src/Collections/Maps/Imaps.dfy.expect delete mode 100644 src/Collections/Maps/Maps.dfy.expect delete mode 100644 src/Collections/Sequences/LittleEndianNat.dfy.expect delete mode 100644 src/Collections/Sequences/LittleEndianNatConversions.dfy.expect delete mode 100644 src/Collections/Sequences/Seq.dfy.expect delete mode 100644 src/Collections/Sets/Isets.dfy.expect delete mode 100644 src/Collections/Sets/Sets.dfy.expect delete mode 100644 src/Functions.dfy.expect delete mode 100644 src/Math.dfy.expect delete mode 100644 src/NonlinearArithmetic/DivMod.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/DivInternals.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/GeneralInternals.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/ModInternals.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/MulInternals.dfy.expect delete mode 100644 src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy.expect delete mode 100644 src/NonlinearArithmetic/Mul.dfy.expect delete mode 100644 src/NonlinearArithmetic/Power.dfy.expect delete mode 100644 src/NonlinearArithmetic/Power2.dfy.expect delete mode 100644 src/Wrappers.dfy.expect diff --git a/.gitignore b/.gitignore index 806a7c87..05c99deb 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ **/Output/ +**/TestResults/ diff --git a/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy index 2c497afe..c60e7020 100644 --- a/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy +++ b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:3 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:3 /noNLarith "%s" /******************************************************************************* * Copyright by the contributors to the Dafny Project diff --git a/examples/LittleEndianNat/LittleEndianNatExample.dfy b/examples/LittleEndianNat/LittleEndianNatExample.dfy index 8c121002..232bda48 100644 --- a/examples/LittleEndianNat/LittleEndianNatExample.dfy +++ b/examples/LittleEndianNat/LittleEndianNatExample.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:3 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:3 /noNLarith "%s" /******************************************************************************* * Copyright by the contributors to the Dafny Project diff --git a/examples/Wrappers.dfy b/examples/Wrappers.dfy index ab705374..a2fc75cf 100644 --- a/examples/Wrappers.dfy +++ b/examples/Wrappers.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:3 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:3 "%s" include "../src/Wrappers.dfy" diff --git a/lit.site.cfg b/lit.site.cfg index ae8d2d7c..01e92337 100644 --- a/lit.site.cfg +++ b/lit.site.cfg @@ -120,9 +120,6 @@ dafnyExecutable += ' -useBaseNameForFileName' dafnyExecutable += ' -timeLimit:30' -# The following option adjusts the exit codes of the Dafny executable -dafnyExecutable += ' -countVerificationErrors:0' - # We do not want output such as "Compiled program written to Foo.cs" # from the compilers, since that changes with the target language dafnyExecutable += ' -compileVerbose:0' diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy index 9fb9857b..088fe15b 100644 --- a/src/BoundedInts.dfy +++ b/src/BoundedInts.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" module BoundedInts { const TWO_TO_THE_0: int := 1 diff --git a/src/BoundedInts.dfy.expect b/src/BoundedInts.dfy.expect deleted file mode 100644 index e5f9ee5a..00000000 --- a/src/BoundedInts.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 12 verified, 0 errors diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy index 72720fa1..7494ef0e 100644 --- a/src/Collections/Maps/Imaps.dfy +++ b/src/Collections/Maps/Imaps.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, diff --git a/src/Collections/Maps/Imaps.dfy.expect b/src/Collections/Maps/Imaps.dfy.expect deleted file mode 100644 index e5f9ee5a..00000000 --- a/src/Collections/Maps/Imaps.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 12 verified, 0 errors diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index b06e65cd..c152d02e 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, diff --git a/src/Collections/Maps/Maps.dfy.expect b/src/Collections/Maps/Maps.dfy.expect deleted file mode 100644 index 66ffe366..00000000 --- a/src/Collections/Maps/Maps.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 14 verified, 0 errors diff --git a/src/Collections/Sequences/LittleEndianNat.dfy b/src/Collections/Sequences/LittleEndianNat.dfy index 15377247..1383cce7 100644 --- a/src/Collections/Sequences/LittleEndianNat.dfy +++ b/src/Collections/Sequences/LittleEndianNat.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) 2020 Secure Foundations Lab diff --git a/src/Collections/Sequences/LittleEndianNat.dfy.expect b/src/Collections/Sequences/LittleEndianNat.dfy.expect deleted file mode 100644 index bba7f9e6..00000000 --- a/src/Collections/Sequences/LittleEndianNat.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 41 verified, 0 errors diff --git a/src/Collections/Sequences/LittleEndianNatConversions.dfy b/src/Collections/Sequences/LittleEndianNatConversions.dfy index db97cc84..1796ff67 100644 --- a/src/Collections/Sequences/LittleEndianNatConversions.dfy +++ b/src/Collections/Sequences/LittleEndianNatConversions.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Copyright by the contributors to the Dafny Project diff --git a/src/Collections/Sequences/LittleEndianNatConversions.dfy.expect b/src/Collections/Sequences/LittleEndianNatConversions.dfy.expect deleted file mode 100644 index c62d0a44..00000000 --- a/src/Collections/Sequences/LittleEndianNatConversions.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 526 verified, 0 errors diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 060168dd..39f5ac92 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original Copyright under the following: diff --git a/src/Collections/Sequences/Seq.dfy.expect b/src/Collections/Sequences/Seq.dfy.expect deleted file mode 100644 index 808136c6..00000000 --- a/src/Collections/Sequences/Seq.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 71 verified, 0 errors diff --git a/src/Collections/Sets/Isets.dfy b/src/Collections/Sets/Isets.dfy index c3a9fce4..5652d575 100644 --- a/src/Collections/Sets/Isets.dfy +++ b/src/Collections/Sets/Isets.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original Copyright under the following: diff --git a/src/Collections/Sets/Isets.dfy.expect b/src/Collections/Sets/Isets.dfy.expect deleted file mode 100644 index 00a51f82..00000000 --- a/src/Collections/Sets/Isets.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 3 verified, 0 errors diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index ae4058d6..b5a29cc7 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original Copyright under the following: diff --git a/src/Collections/Sets/Sets.dfy.expect b/src/Collections/Sets/Sets.dfy.expect deleted file mode 100644 index 4b0fec56..00000000 --- a/src/Collections/Sets/Sets.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 15 verified, 0 errors diff --git a/src/Functions.dfy b/src/Functions.dfy index 64739653..78928b83 100644 --- a/src/Functions.dfy +++ b/src/Functions.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original Copyright under the following: diff --git a/src/Functions.dfy.expect b/src/Functions.dfy.expect deleted file mode 100644 index 823a60a1..00000000 --- a/src/Functions.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 1 verified, 0 errors diff --git a/src/Math.dfy b/src/Math.dfy index 7af7124a..b58d098b 100644 --- a/src/Math.dfy +++ b/src/Math.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Copyright by the contributors to the Dafny Project diff --git a/src/Math.dfy.expect b/src/Math.dfy.expect deleted file mode 100644 index 012f5b99..00000000 --- a/src/Math.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 0 verified, 0 errors diff --git a/src/NonlinearArithmetic/DivMod.dfy b/src/NonlinearArithmetic/DivMod.dfy index 2ac45237..5567ef8c 100644 --- a/src/NonlinearArithmetic/DivMod.dfy +++ b/src/NonlinearArithmetic/DivMod.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/DivMod.dfy.expect b/src/NonlinearArithmetic/DivMod.dfy.expect deleted file mode 100644 index 452a80c9..00000000 --- a/src/NonlinearArithmetic/DivMod.dfy.expect +++ /dev/null @@ -1,6 +0,0 @@ -DivMod.dfy(1484,4): Warning: For expression "d * k > 0": - /!\ No trigger covering all quantified variables found. In sub-expression at DivMod.dfy(1485,20) -DivMod.dfy(1518,4): Warning: For expression "0 < a * b": - /!\ No trigger covering all quantified variables found. In sub-expression at DivMod.dfy(1519,16) - -Dafny program verifier finished with 239 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/DivInternals.dfy b/src/NonlinearArithmetic/Internals/DivInternals.dfy index 0843953a..99ef30f6 100644 --- a/src/NonlinearArithmetic/Internals/DivInternals.dfy +++ b/src/NonlinearArithmetic/Internals/DivInternals.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/DivInternals.dfy.expect b/src/NonlinearArithmetic/Internals/DivInternals.dfy.expect deleted file mode 100644 index ccc01c35..00000000 --- a/src/NonlinearArithmetic/Internals/DivInternals.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 11 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy index cdbb51b1..a3dbe371 100644 --- a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy +++ b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy.expect b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy.expect deleted file mode 100644 index ee799665..00000000 --- a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 8 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy index f3f664cd..a54fde89 100644 --- a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy +++ b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy.expect b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy.expect deleted file mode 100644 index 823a60a1..00000000 --- a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 1 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy index b31ce9c6..3d244ec9 100644 --- a/src/NonlinearArithmetic/Internals/ModInternals.dfy +++ b/src/NonlinearArithmetic/Internals/ModInternals.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy.expect b/src/NonlinearArithmetic/Internals/ModInternals.dfy.expect deleted file mode 100644 index 66ffe366..00000000 --- a/src/NonlinearArithmetic/Internals/ModInternals.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 14 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy index b4f83af2..8f5d3672 100644 --- a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy +++ b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy.expect b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy.expect deleted file mode 100644 index 1981561c..00000000 --- a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 10 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/MulInternals.dfy b/src/NonlinearArithmetic/Internals/MulInternals.dfy index 100cda2a..cbde1ae6 100644 --- a/src/NonlinearArithmetic/Internals/MulInternals.dfy +++ b/src/NonlinearArithmetic/Internals/MulInternals.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/MulInternals.dfy.expect b/src/NonlinearArithmetic/Internals/MulInternals.dfy.expect deleted file mode 100644 index 0825601c..00000000 --- a/src/NonlinearArithmetic/Internals/MulInternals.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 9 verified, 0 errors diff --git a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy index 9d2cd154..7304a299 100644 --- a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy +++ b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy.expect b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy.expect deleted file mode 100644 index 83193971..00000000 --- a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 6 verified, 0 errors diff --git a/src/NonlinearArithmetic/Mul.dfy b/src/NonlinearArithmetic/Mul.dfy index dea53c59..1cf34eef 100644 --- a/src/NonlinearArithmetic/Mul.dfy +++ b/src/NonlinearArithmetic/Mul.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Mul.dfy.expect b/src/NonlinearArithmetic/Mul.dfy.expect deleted file mode 100644 index 723e6aee..00000000 --- a/src/NonlinearArithmetic/Mul.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 54 verified, 0 errors diff --git a/src/NonlinearArithmetic/Power.dfy b/src/NonlinearArithmetic/Power.dfy index d5d0d01c..5d86e94c 100644 --- a/src/NonlinearArithmetic/Power.dfy +++ b/src/NonlinearArithmetic/Power.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Power.dfy.expect b/src/NonlinearArithmetic/Power.dfy.expect deleted file mode 100644 index dae7b996..00000000 --- a/src/NonlinearArithmetic/Power.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 59 verified, 0 errors diff --git a/src/NonlinearArithmetic/Power2.dfy b/src/NonlinearArithmetic/Power2.dfy index 969fefc3..f03527bf 100644 --- a/src/NonlinearArithmetic/Power2.dfy +++ b/src/NonlinearArithmetic/Power2.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 /noNLarith "%s" /******************************************************************************* * Original: Copyright (c) Microsoft Corporation diff --git a/src/NonlinearArithmetic/Power2.dfy.expect b/src/NonlinearArithmetic/Power2.dfy.expect deleted file mode 100644 index 0825601c..00000000 --- a/src/NonlinearArithmetic/Power2.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 9 verified, 0 errors diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy index 0f992587..ddb9b7f3 100644 --- a/src/Wrappers.dfy +++ b/src/Wrappers.dfy @@ -1,5 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %dafny /compile:0 "%s" /******************************************************************************* * Copyright by the contributors to the Dafny Project diff --git a/src/Wrappers.dfy.expect b/src/Wrappers.dfy.expect deleted file mode 100644 index ba00363f..00000000 --- a/src/Wrappers.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 4 verified, 0 errors From 94f9189929088159ae1bd052eb92468170629970 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 10 Mar 2022 09:50:38 -0800 Subject: [PATCH 30/36] Fix jobs (hopefully) --- .github/workflows/tests.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 1cde826a..4bfb12ce 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -22,10 +22,10 @@ jobs: run: dotnet tool install --global dafny-reportgenerator - name: Verify Dafny Code - run: dafny /compile:0 /trace /noNLarith /verificationLogger:trx /verificationLogger:csv src/NonlinearArithmetic/**/*.dfy + run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . - name: Generate Report - run: dafny-reportgenerator summarize-csv-results --max-resource-count 1000000 TestResults/*.csv + run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 27c350c64d7b16e99f36ae471e6feef024352bfb Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 10 Mar 2022 09:58:29 -0800 Subject: [PATCH 31/36] Put lit back --- .github/workflows/tests.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 4bfb12ce..dcb22750 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -21,6 +21,9 @@ jobs: - name: Install Dafny report generator run: dotnet tool install --global dafny-reportgenerator + - name: Install lit + run: pip install lit OutputCheck + - name: Verify Dafny Code run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . From ab26e78a3a1f690aebf8e228f868c5c604f14a80 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 10 Mar 2022 11:19:28 -0800 Subject: [PATCH 32/36] Set bound of 1 second --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index dcb22750..4363de4f 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -28,7 +28,7 @@ jobs: run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . - name: Generate Report - run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results + run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results --max-duration-seconds 1 - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From 519f1c9cee4c31afa054ba8f9e009ff071847cca Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 10 Mar 2022 11:26:11 -0800 Subject: [PATCH 33/36] Too aggressive, fall back to 10 seconds for now --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 4363de4f..e519f637 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -28,7 +28,7 @@ jobs: run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . - name: Generate Report - run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results --max-duration-seconds 1 + run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results --max-duration-seconds 10 - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed From a4107008bfb8642358ec8f38c602b10ddb37c98d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 10 Mar 2022 14:03:39 -0800 Subject: [PATCH 34/36] Fix upload path pattern, fail if nothing matches --- .github/workflows/tests.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index e519f637..9da73d16 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -34,4 +34,5 @@ jobs: if: success() || failure() # run this step even if previous step failed with: name: verification-results - path: 'TestResults/*.trx' + path: '**/TestResults/*.trx' + if-no-files-found: error From feedfa8c65a98674cd37ed4d1d61232cd597ceb3 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 11 Mar 2022 08:49:20 -0800 Subject: [PATCH 35/36] Naming improvement --- .../workflows/{test-report.yml => generate-test-report.yml} | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename .github/workflows/{test-report.yml => generate-test-report.yml} (82%) diff --git a/.github/workflows/test-report.yml b/.github/workflows/generate-test-report.yml similarity index 82% rename from .github/workflows/test-report.yml rename to .github/workflows/generate-test-report.yml index df5b8f68..f8f96683 100644 --- a/.github/workflows/test-report.yml +++ b/.github/workflows/generate-test-report.yml @@ -1,4 +1,4 @@ -name: 'Test Report' +name: 'Generate Test Report' on: workflow_run: workflows: ['tests'] # runs after CI workflow @@ -11,6 +11,6 @@ jobs: - uses: dorny/test-reporter@v1 with: artifact: verification-results - name: Verification Tests + name: Verification Results path: '*.trx' reporter: dotnet-trx \ No newline at end of file From 48340eb9280a76ea3c74e40a824fa7701c3f78b5 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 11 Mar 2022 08:51:24 -0800 Subject: [PATCH 36/36] Update .github/workflows/tests.yml MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Clément Pit-Claudel --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 9da73d16..48147878 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -28,7 +28,7 @@ jobs: run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . - name: Generate Report - run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results --max-duration-seconds 10 + run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10 - uses: actions/upload-artifact@v2 # upload test results if: success() || failure() # run this step even if previous step failed