diff --git a/examples/Enumerators/Datatypes.dfy b/examples/Enumerators/Datatypes.dfy new file mode 100644 index 00000000..58636d4f --- /dev/null +++ b/examples/Enumerators/Datatypes.dfy @@ -0,0 +1,80 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "Enumerators.dfy" + +// An example of an enumerator that traverses the sub-values in +// an algebraic datatype value. +module DatatypeEnumerator { + + import opened Enumerators + + datatype Tree = Node(left: Tree, value: T, right: Tree) | Nil + + datatype TreeTraversal = InorderTraversal(Tree) /* | PreorderTraversal(Tree) | PostorderTraversal(Tree) */ { + method Enumerator() returns (e: Enumerator) + ensures e.Valid() + ensures fresh(e.Repr) + ensures e.enumerated == [] + { + match this + case InorderTraversal(tree) => { + e := InorderEnumerator(tree); + } + } + } + + method InorderEnumerator(tree: Tree) returns (e: Enumerator) + ensures e.Valid() + ensures fresh(e.Repr) + ensures e.enumerated == [] + { + match tree + case Nil => { + e := new SeqEnumerator([]); + } + case Node(left, value, right) => { + // TODO: How to make this lazy? + var thisValueEnum := new SeqEnumerator([value]); + var leftEnum := InorderEnumerator(left); + var rightEnum := InorderEnumerator(right); + var tmp := new ConcatEnumerator(leftEnum, thisValueEnum); + e := new ConcatEnumerator(tmp, rightEnum); + } + } + + method Main() { + var tree := Node( + Node( + Nil, + 1, + Node(Nil, 2, Nil) + ), + 3, + Node( + Node(Nil, 4, Nil), + 5, + Nil + ) + ); + + var traversal := InorderTraversal(tree); + var e := traversal.Enumerator(); + while true + invariant e.Valid() && fresh(e.Repr) + decreases e.Decreases() + { + var x := e.Next(); + if x.None? { break; } + + print x.value; + } + + // With foreach loop support, the above could just be: + // + // foreach x in InorderTraversal(tree) { + // print x; + // } + + } +} \ No newline at end of file diff --git a/examples/Enumerators/Datatypes.dfy.expect b/examples/Enumerators/Datatypes.dfy.expect new file mode 100644 index 00000000..eef2943b --- /dev/null +++ b/examples/Enumerators/Datatypes.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 5 verified, 0 errors +12345 \ No newline at end of file diff --git a/examples/Enumerators/Enumerators.dfy b/examples/Enumerators/Enumerators.dfy new file mode 100644 index 00000000..9a65915d --- /dev/null +++ b/examples/Enumerators/Enumerators.dfy @@ -0,0 +1,225 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../../src/Enumerators/Enumerators.dfy" + +module Demo { + + import opened Enumerators + import opened Wrappers + + // Note the common template for using a while loop on + // an arbitrary Enumerator. This will likely be what we + // propose that a "foreach" loop in Dafny will desugar to. + + method Example1() { + var numbers := [1, 2, 3, 4, 5]; + + var e: Enumerator := new SeqEnumerator(numbers); + while true + invariant e.Valid() && fresh(e.Repr) + decreases e.Decreases() + { + var element := e.Next(); + if element.None? { break; } + + print element.value, "\n"; + } + } + + method Example2() { + var first := [1, 2, 3, 4, 5]; + var second := [6, 7, 8]; + var e1 := new SeqEnumerator(first); + var e2 := new SeqEnumerator(second); + var e: Enumerator := new ConcatEnumerator(e1, e2); + + while true + invariant e.Valid() && fresh(e.Repr) + decreases e.Decreases() + { + var element := e.Next(); + if element.None? { break; } + + print element.value, "\n"; + } + } + + method PrintWithCommas() { + var first := [1, 2, 3, 4, 5]; + var e: Enumerator := new SeqEnumerator(first); + + for index := 0 to * + invariant e.Valid() && fresh(e.Repr) + decreases e.Decreases() + { + var element := e.Next(); + if element.None? { break; } + + if index > 0 { + print ", "; + } + print element; + } + print "\n"; + } + + method MappingExample() { + var first := [1, 2, 3, 4, 5]; + var e1 := new SeqEnumerator(first); + var e: Enumerator := new MappingEnumerator(x => x + 2, e1); + + var result: seq := []; + while true + invariant e.Valid() && fresh(e.Repr) + decreases e.Decreases() + { + var element := e.Next(); + if element.None? { break; } + + result := result + [element.value]; + } + assert e.enumerated == Seq.Map(x => x + 2, first); + } + + // Some examples showing the equivalence between enumerator + // operations and sequence operations. + + method RoundTrip(s: seq) returns (result: seq) + ensures result == s + { + var e: Enumerator := new SeqEnumerator(s); + result := CollectToSeq(e); + } + + // method ToArray(s: seq) returns (result: array) + // ensures result[..] == s + // { + // var e: Enumerator := new SeqEnumerator(s); + // assert Sized(e, |s|); + // result := CollectToArray(e, |s|); + // } + + method AddTwoToEach(s: seq) returns (result: seq) + ensures result == Seq.Map(x => x + 2, s) + { + var e := new SeqEnumerator(s); + var mapped := new MappingEnumerator(x => x + 2, e); + result := CollectToSeq(mapped); + } + + method SetToSeq(s: set) returns (result: seq) + ensures multiset(result) == multiset(s) + { + var e := new SetEnumerator(s); + result := CollectToSeq(e); + } + + method SeqEnumerator(s: seq) returns (r: Enumerator) + ensures r.Valid() && fresh(r.Repr) + // ensures Sized(r, |s|) + { + r := new SeqEnumerator(s); + } + + // method SizedExample() + // { + // var e: Enumerator := SeqEnumerator([1,2,3,4,5]); + // assert Sized(e, 5); + // var one := e.Next(); + // assert Sized(e, 5); + // } + + + method Filter(s: seq, p: T -> bool) returns (result: seq) + ensures result == Seq.Filter(p, s) + { + var e := new SeqEnumerator(s); + var filtered: FilteredEnumerator := new FilteredEnumerator(e, p); + result := CollectToSeq(filtered); + assert e.enumerated == s; + } + + method Concatenate(first: seq, second: seq) returns (result: seq) + ensures result == first + second + { + var e1 := new SeqEnumerator(first); + var e2 := new SeqEnumerator(second); + var concatenated: ConcatEnumerator := new ConcatEnumerator(e1, e2); + result := CollectToSeq(concatenated); + assert concatenated.Valid(); + } + + // method ConcatenateToArray(first: seq, second: seq) returns (result: array) + // ensures result[..] == first + second + // { + // var e1 := new SeqEnumerator(first); + // var e2 := new SeqEnumerator(second); + // var concatenated: ConcatEnumerator := new ConcatEnumerator(e1, e2); + // concatenated.CountOfResult(|first|, |second|); + // result := CollectToArray(concatenated, |first| + |second|); + // assert concatenated.Valid(); + // } + + class Cell { + constructor() {} + } + + // An enumerator that produces newly allocated objects. + // Test case for framing. + class CellEnumerator extends Enumerator { + var remaining: nat + predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + remaining + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + if remaining > 0 { + var cell := new Cell(); + element := Some(cell); + remaining := remaining - 1; + } else { + element := None; + } + Enumerated(element); + } + } + + method EnumerateForever() decreases * { + var allNats := new NatEnumerator(); + while true + invariant allNats.Valid() && fresh(allNats.Repr) + decreases * + { + var next := allNats.Next(); + print next; + } + } +} \ No newline at end of file diff --git a/examples/Enumerators/Enumerators.dfy.expect b/examples/Enumerators/Enumerators.dfy.expect new file mode 100644 index 00000000..ccc01c35 --- /dev/null +++ b/examples/Enumerators/Enumerators.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 11 verified, 0 errors diff --git a/examples/Enumerators/IteratorAdaptor.dfy b/examples/Enumerators/IteratorAdaptor.dfy new file mode 100644 index 00000000..b4fb0aaa --- /dev/null +++ b/examples/Enumerators/IteratorAdaptor.dfy @@ -0,0 +1,112 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../../src/Enumerators/Enumerators.dfy" +include "../../src/Wrappers.dfy" + +// Dafny iterators do not share any common supertype, so there isn't +// currently any way to write a single adaptor from an arbitrary +// iterator to the Enumerator trait. However, this example should +// serve as a template for adapting any specific iterator. +// +// In practice, a loop that uses a specific iterator type will need to +// declare a "decreases" termination metric, and hence the iterator +// in question will need at least one "yield ensures" clause to +// support such a metric. The same is true for adapting a specific iterator +// to the Enumerator trait in order to implement the Decreases() function. +module IteratorAdaptorExample { + + import opened Enumerators + import opened Wrappers + + iterator RangeIterator(start: int, end: int) yields (element: int) + requires start <= end + // These are necessary in order to prove termination via Decreases() + yield ensures |elements| <= end - start + ensures |elements| == end - start + // These are necessary to prove the Repr <= old(Repr) post-condition + // of Next(). Iterators that instantiate and "hand off" objects + // will need weaker post-conditions. + yield ensures _new == {} + ensures _new == {} + { + for i := start to end + invariant i - start == |elements| + invariant _new == {} + { + yield i; + } + } + + class RangeEnumerator extends Enumerator { + + const iter: RangeIterator + var iterDone: bool + var remaining: nat + + constructor(start: int, end: int) + requires start <= end + ensures Valid() + ensures fresh(Repr) + { + iter := new RangeIterator(start, end); + remaining := end - start; + iterDone := false; + enumerated := []; + Repr := {this, iter}; + } + + predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && iter in Repr + && iter._modifies == iter._reads == iter._new == {} + && (!iterDone ==> iter.Valid()) + && (iterDone ==> remaining == 0) + && remaining == (iter.end - iter.start) - |iter.elements| + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + if iterDone { + element := None; + } else { + var more := iter.MoveNext(); + if more { + element := Some(iter.element); + remaining := remaining - 1; + } else { + iterDone := true; + element := None; + } + } + + Enumerated(element); + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + remaining + } + } +} \ No newline at end of file diff --git a/examples/Enumerators/IteratorAdaptor.dfy.expect b/examples/Enumerators/IteratorAdaptor.dfy.expect new file mode 100644 index 00000000..e5f9ee5a --- /dev/null +++ b/examples/Enumerators/IteratorAdaptor.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 12 verified, 0 errors diff --git a/examples/Enumerators/JavaStyle.dfy b/examples/Enumerators/JavaStyle.dfy new file mode 100644 index 00000000..cc2022cd --- /dev/null +++ b/examples/Enumerators/JavaStyle.dfy @@ -0,0 +1,160 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../../src/Frames.dfy" +include "../../src/Wrappers.dfy" +include "Enumerators.dfy" + +// There are lots of ways to define an Iterator/Enumerator +// concept, and there is precious little alignment on the exact +// APIs that various programming languages have chosen. :) +// This is an example of how to adapt another flavour of enumerator +// (Java's in this case) to Dafny's. +module JavaStyleExample { + + import opened Frames + import opened Wrappers + import opened Enumerators + + // Roughly aligns with Java's Iterator interface. + trait JavaStyleIterator extends Validatable { + + method HasNext() returns (result: bool) + requires Valid() + ensures !result <==> Decreases() == 0 + + method Next() returns (res: T) + requires Valid() + requires Decreases() > 0 + modifies Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures Decreases() < old(Decreases()) + + function Decreases(): nat + reads Repr + requires Valid() + } + + // Adapts from a Java Iterator to an Enumerator. + class JavaStyleIteratorEnumerator extends Enumerator { + + const iter: JavaStyleIterator + + constructor(iter: JavaStyleIterator) + requires iter.Valid() + modifies iter.Repr + ensures Valid() + ensures iter.Repr <= old(iter.Repr) + ensures Repr == {this} + iter.Repr + { + this.iter := iter; + Repr := {this} + iter.Repr; + } + + predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(iter) + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + var hasNext := iter.HasNext(); + if hasNext { + var value := iter.Next(); + element := Some(value); + } else { + element := None; + } + Enumerated(element); + } + + function Decreases(): nat + reads Repr + requires Valid() + decreases Repr, 1 + { + iter.Decreases() + } + } + + class SeqJavaStyleIterator extends JavaStyleIterator { + + var s: seq + + constructor(s: seq) + ensures Valid() + ensures fresh(Repr) + { + this.s := s; + Repr := {this}; + } + + predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + } + + method HasNext() returns (result: bool) + requires Valid() + ensures !result <==> Decreases() == 0 + { + return |s| > 0; + } + + method Next() returns (res: T) + requires Valid() + requires Decreases() > 0 + modifies Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures Decreases() < old(Decreases()) + { + res := s[0]; + s := s[1..]; + } + + function Decreases(): nat + reads Repr + requires Valid() + { + |s| + } + } + + method Main() { + var iter := new SeqJavaStyleIterator([1,2,3,4,5]); + + var enum: Enumerator := new JavaStyleIteratorEnumerator(iter); + while true + invariant enum.Valid() && fresh(enum.Repr) + decreases enum.Decreases() + { + var element := enum.Next(); + if element.None? { break; } + + print element.value, "\n"; + } + } +} \ No newline at end of file diff --git a/examples/Enumerators/JavaStyle.dfy.expect b/examples/Enumerators/JavaStyle.dfy.expect new file mode 100644 index 00000000..b15bb607 --- /dev/null +++ b/examples/Enumerators/JavaStyle.dfy.expect @@ -0,0 +1,7 @@ + +Dafny program verifier finished with 22 verified, 0 errors +1 +2 +3 +4 +5 diff --git a/src/Actions/Actions.dfy b/src/Actions/Actions.dfy new file mode 100644 index 00000000..44b2047f --- /dev/null +++ b/src/Actions/Actions.dfy @@ -0,0 +1,263 @@ + +include "../Wrappers.dfy" +include "../Frames.dfy" +include "../Math.dfy" +include "../Collections/Sequences/Seq.dfy" + +include "GenericAction.dfy" + +module {:options "--function-syntax:4"} Actions { + + import opened Wrappers + import opened Frames + import opened Seq + import opened Math + import opened GenericActions + import opened Termination + + // TODO: NOT a fully general-purpose handle on any arbitrary Dafny method, + // because gaps in Dafny expressiveness make that impossible for now + // (e.g. field references in framing clauses aren't expressions, + // decreases metrics aren't directly expressible in user code) + // Consider naming this something more specific, related to the assumptions: + // 1. Validatable (and doesn't modify anything not in Repr) + // 2. Behavior specified only by referring to consumed and produced. + trait {:termination false} Action extends GenericAction, Validatable { + + ghost var history: seq<(T', R')> + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> CanProduce(history) + decreases height, 0 + + // KEY DESIGN POINT: these predicates specifically avoid reading the current + // state of the action. + // That's so extrisnic properties of an action do NOT depend on their current state. + // This is key to ensure that you can prove properties of a given action that + // will continue to hold as the Dafny heap changes. + // This approach works because Dafny understands that for a given object, + // the implementation of CanConsume/CanProduce cannot change over time. + // + // The downside is that these are then forced to use quantifiers + // to talk about all possible states of an action. + + // TODO: Necessary but not sufficient that: + // CanConsume(history, nextIn) ==> exists nextOut :: CanProduce(history + [(nextIn, nextOut)]) + // Does that need to be explicitly part of the spec? + ghost predicate CanConsume(history: seq<(T, R)>, next: T) + requires Valid() + requires CanProduce(history) + reads Repr + decreases height + + ghost predicate CanProduce(history: seq<(T, R)>) + decreases height + + ghost predicate Requires(t: T) + reads Reads(t) + { + && Valid() + && CanConsume(history, t) + } + ghost function Reads(t: T): set + reads this + ensures this in Reads(t) + { + {this} + Repr + } + ghost function Modifies(t: T): set + reads Reads(t) + { + Repr + } + ghost function Decreases(t: T): TerminationMetric + reads Reads(t) + { + NatTerminationMetric(height) + } + twostate predicate Ensures(t: T, new r: R) + reads Reads(t) + { + && Valid() + && history == old(history) + [(t, r)] + && fresh(Repr - old(Repr)) + } + + // Helpers + + ghost method Update(t: T, r: R) + reads `history + modifies `history + ensures history == old(history) + [(t, r)] + { + history := history + [(t, r)]; + } + + ghost function Consumed(): seq + reads this + { + Inputs(history) + } + + ghost function Produced(): seq + reads this + { + Outputs(history) + } + } + + // Common action invariants + + function Inputs(history: seq<(T, R)>): seq { + Seq.Map((e: (T, R)) => e.0, history) + } + + function Outputs(history: seq<(T, R)>): seq { + Seq.Map((e: (T, R)) => e.1, history) + } + + ghost predicate OnlyProduces(i: Action, history: seq<(T, R)>, c: R) + { + i.CanProduce(history) <==> forall e <- history :: e.1 == c + } + + ghost predicate CanConsumeAll(a: Action, input: seq) { + forall i | 0 < i < |input| :: + var consumed := input[..(i - 1)]; + var next := input[i]; + forall history | a.CanProduce(history) && Inputs(history) == consumed :: a.CanConsume(history, next) + } + + ghost predicate Terminated(s: seq, c: T, n: nat) { + forall i | 0 <= i < |s| :: n <= i <==> s[i] == c + } + + lemma TerminatedUndistributes(left: seq, right: seq, c: T, n: nat) + requires Terminated(left + right, c, n) + ensures Terminated(left, c, n) + ensures Terminated(right, c, Math.Max(0, n - |left|)) + { + assert forall i | 0 <= i < |left| :: left[i] == (left + right)[i]; + assert forall i | 0 <= i < |right| :: right[i] == (left + right)[i + |left|]; + } + + // TODO: generalize to "EventuallyProducesSequence"? + ghost predicate ProducesTerminatedBy(i: Action, c: R, limit: nat) { + forall history: seq<(T, R)> | i.CanProduce(history) + :: exists n: nat | n <= limit :: Terminated(Outputs(history), c, n) + } + + // Class of actions whose precondition doesn't depend on history (probably needs a better name) + ghost predicate ContextFree(a: Action, p: T -> bool) { + forall history, next | a.CanProduce(history) + :: a.CanConsume(history, next) <==> p(next) + } + + // Aggregators + + type IAggregator = Action + type Aggregator = a: Action | exists limit :: ProducesTerminatedBy(a, false, limit) witness * + + // TODO: Refactor to use DynamicArray + class ArrayAggregator extends Action { + + var storage: array + var index: nat + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(history) + decreases height, 0 + { + && this in Repr + && storage in Repr + && 0 < storage.Length + && 0 <= index <= storage.Length + && Consumed() == storage[..index] + } + + constructor() + ensures Valid() + ensures fresh(Repr - {this}) + ensures history == [] + { + index := 0; + storage := new T[10]; + + history := []; + Repr := {this, storage}; + } + + ghost predicate CanConsume(history: seq<(T, ())>, next: T) + decreases height + { + true + } + ghost predicate CanProduce(history: seq<(T, ())>) + decreases height + { + true + } + + method Invoke(t: T) returns (r: ()) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + if index == storage.Length { + var newStorage := new T[storage.Length * 2]; + forall i | 0 <= i < index { + newStorage[i] := storage[i]; + } + storage := newStorage; + + Repr := {this, storage}; + } + storage[index] := t; + index := index + 1; + + r := (); + Update(t, r); + assert Valid(); + } + + function Values(): seq + requires Valid() + reads Repr + ensures Values() == Consumed() + { + storage[..index] + } + } + + method AggregatorExample() { + var a := new ArrayAggregator(); + var _ := a.Invoke(1); + var _ := a.Invoke(2); + var _ := a.Invoke(3); + var _ := a.Invoke(4); + var _ := a.Invoke(5); + assert a.Values() == [1, 2, 3, 4, 5]; + } + + // Other primitives/examples todo: + // * Promise-like single-use Action to capture a value for reading later + // * Eliminate all the (!new) restrictions - look into "older" parameters? + // * How to state the invariant that a constructor as an action creates a new object every time? + // * Lemma that takes produced as input, instead of forall produced? + // * Enumerable ==> defines e.Enumerator() + // * BUT can have infinite containers, probably need IEnumerable as well? (different T for the Action) + // * Expressing that an Action "Eventually produces something" (look at how VMC models this for randomness) + // * IsEnumerator(a) == "a eventually produces None" && "a then only produces None" + // * Build on that to make CrossProduct(enumerable1, enumerable2) + // * Example of adapting an iterator + // * Example of enumerating all possible values of a type (for test generation) + // * Needs to handle infinite types too, hence needs the "eventually produces something" concept + +} \ No newline at end of file diff --git a/src/Actions/Combinators.dfy b/src/Actions/Combinators.dfy new file mode 100644 index 00000000..61610b69 --- /dev/null +++ b/src/Actions/Combinators.dfy @@ -0,0 +1,64 @@ +include "Actions.dfy" +include "Enumerators.dfy" + +module ActionCombinators { + + import opened Actions + import opened Wrappers + import opened Enumerators + + // Wrapping a side-effect free function as an action + method Function(f: T --> R) + returns (a: Action) + ensures fresh(a.Repr) + ensures forall history: seq<(T, R)> | a.CanProduce(history), e <- history :: + f.requires(e.0) && e.1 == f(e.0) + + // Producing an enumerator for a given sequence. + // Explicitly specified to enumerate that sequence. + method EnumeratorOfSeq(s: seq) + returns (e: Enumerator) + ensures EnumeratesSeq(e, s) + ensures e.history == [] + + // a.k.a. Chain(first, second) + // + // To map a function f over the values of an action a: + // Compose(Function(f), a) + // + // Or over an enumerator e: + // var maybeF := (maybeT: Option) => match maybeT { + // case Some(t) => Some(f(t)) + // case None => None + // }; + // Compose(Function(maybeF), e) + // + // To map an Action a over a sequence s: + // Collect(Compose(a, EnumeratorOfSeq(s))) + method Compose(second: Action, first: Action) + returns (composed: Action) + requires second.Repr !! first.Repr + + // Produces Seq.Filter(what a produces, p) + // a has to be an Enumerator rather than just an Action + // to ensure Invoke() eventually terminates + method Filter(e: Enumerator, p: T -> bool) + returns (filtered: Enumerator) + + // Produces Seq.Flatten(Actions.Map(inner, (what outer produces))) + // inner needs to be an action rather than just a function + // since enumerators are usually objects that need allocation. + method Nested(outer: Enumerator, inner: Action>) + returns (nested: Enumerator) + + method ForEach(source: Enumerator, sink: Aggregator) + // Ensures that source is exhausted + // and that sink.Consumed() == Enumerated(source.Produced()) + + method Collect(source: Enumerator) + returns (s: seq) + // Ensures that source is exhausted + // and that s == Enumerated(source.Produced()) + // Likely implemented by creating an ArrayAggregator sink + // and calling ForEach(source, sink) +} \ No newline at end of file diff --git a/src/Actions/ComposedAction.dfy b/src/Actions/ComposedAction.dfy new file mode 100644 index 00000000..e523bdab --- /dev/null +++ b/src/Actions/ComposedAction.dfy @@ -0,0 +1,114 @@ +include "Actions.dfy" +include "Enumerators.dfy" +include "FunctionAction.dfy" + +module Composed { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + import opened Functions + + class Compose extends Action { + + const first: Action + const second: Action + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> CanProduce(history) + decreases height, 0 + { + && this in Repr + && ValidComponent(first) + && ValidComponent(second) + && first.Repr !! second.Repr + && CanProduce(history) + && Consumed() == first.Consumed() + && first.Produced() == second.Consumed() + && Produced() == second.Produced() + } + + constructor(second: Action, first: Action) + requires first.Valid() + requires second.Valid() + requires first.Repr !! second.Repr + requires first.history == [] + requires second.history == [] + ensures Valid() + ensures history == [] + { + this.first := first; + this.second := second; + + history := []; + Repr := {this} + first.Repr + second.Repr; + height := first.height + second.height + 1; + } + + ghost predicate CanConsume(history: seq<(T, R)>, next: T) + requires CanProduce(history) + decreases height + { + forall piped: seq | CanPipe(history, piped) :: + && var firstHistory := Seq.Zip(Inputs(history), piped); + && var secondHistory := Seq.Zip(piped, Outputs(history)); + && first.CanConsume(firstHistory, next) + && forall pipedNext: V | first.CanProduce(firstHistory + [(next, pipedNext)]) :: + && second.CanConsume(secondHistory, pipedNext) + + // Note that you can't compose any arbitrary first with a second: + // if you need to read first.produced to know if you can consume another input, + // that won't work here because this outer CanConsume predicate doesn't take that as input. + // (...unless there's a way of inferring what was produced from second.produced) + } + + ghost predicate CanProduce(history: seq<(T, R)>) + decreases height + { + exists piped: seq :: CanPipe(history, piped) + } + + ghost predicate CanPipe(history: seq<(T, R)>, piped: seq) + decreases height, 0 + { + && |piped| == |history| + && first.CanProduce(Seq.Zip(Inputs(history), piped)) + && second.CanProduce(Seq.Zip(piped, Outputs(history))) + } + + method Invoke(t: T) returns (r: R) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert first.Valid(); + var v := first.Invoke(t); + r := second.Invoke(v); + + Update(t, r); + Repr := {this} + first.Repr + second.Repr; + } + } + + method Example() { + var e: SeqEnumerator := new SeqEnumerator([1, 2, 3, 4, 5]); + SeqEnumeratorIsEnumerator(e); + var f := (x: Option) => match x { + case Some(v) => Some(v + v) + case None => None + }; + var doubler := new FunctionAction(f); + var mapped: Compose<(), Option, Option> := new Compose(doubler, e); + + // TODO: Need some lemmas + var x := mapped.Invoke(()); + assert mapped.Produced() == [Some(2)]; + assert [x] == [Some(2)]; + assert x == Some(2); + } +} \ No newline at end of file diff --git a/src/Actions/ConstructorAction.dfy b/src/Actions/ConstructorAction.dfy new file mode 100644 index 00000000..455ab3f8 --- /dev/null +++ b/src/Actions/ConstructorAction.dfy @@ -0,0 +1,86 @@ + +include "Enumerators.dfy" + +module ConstructorExample { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + + class C { + var x: nat + + constructor(x: nat) + reads {} + ensures this.x == x + { + this.x := x; + } + } + + class MakeCAction extends Action { + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(history) + decreases height, 0 + { + && this in Repr + && CanProduce(history) + && (forall e <- history :: e.1 in Repr) + } + + constructor() + ensures Valid() + ensures fresh(Repr) + ensures history == [] + { + history := []; + Repr := {this}; + } + + ghost predicate CanConsume(history: seq<(nat, C)>, next: nat) + requires CanProduce(history) + decreases height + { + true + } + ghost predicate CanProduce(history: seq<(nat, C)>) + reads this, Repr + decreases height + { + forall e <- history :: e.1.x == e.0 + } + + method Invoke(t: nat) returns (r: C) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert Valid(); + r := new C(t); + + Update(t, r); + } + } + + lemma MakeCActionMakesCs(a: MakeCAction) + ensures forall history | a.CanProduce(history) :: + forall e: (nat, C) <- history :: fresh(e.1) + + // method Example() { + // var doubler := new FunctionAction(v => v + v); + + // assert doubler.history == []; + + // var x := doubler.Invoke(2); + // assert doubler.Produced() == [x]; + // assert [x] == [4]; + // assert x == 4; + // } +} \ No newline at end of file diff --git a/src/Actions/ConstructorGenericAction.dfy b/src/Actions/ConstructorGenericAction.dfy new file mode 100644 index 00000000..2dfaf16f --- /dev/null +++ b/src/Actions/ConstructorGenericAction.dfy @@ -0,0 +1,87 @@ + +include "Enumerators.dfy" + +module GenericConstructorExample { + + import opened GenericActions + import opened Enumerators + import opened Wrappers + import opened Seq + import opened Termination + + class C { + var x: nat + + constructor(x: nat) + reads {} + ensures this.x == x + { + this.x := x; + } + } + + class MakeCAction extends GenericAction { + + constructor() + { + } + + ghost predicate Requires(t: nat) + reads Reads(t) + { + true + } + ghost function Reads(t: nat): set + reads this + ensures this in Reads(t) + { + {this} + } + ghost function Modifies(t: nat): set + reads Reads(t) + { + {} + } + ghost function Decreases(t: nat): TerminationMetric + reads Reads(t) + { + NatTerminationMetric(0) + } + twostate predicate Ensures(t: nat, new r: C) + reads Reads(t) + { + true + } + + method Invoke(t: nat) returns (r: C) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + r := new C(t); + + assert IsFresh(r); + } + + twostate predicate IsFresh(new r: C) { + fresh(r) + } + } + + // lemma MakeCActionMakesCs(a: MakeCAction) + // ensures forall history | a.CanProduce(history) :: + // forall e: (nat, C) <- history :: fresh(e.1) + + // method Example() { + // var doubler := new FunctionAction(v => v + v); + + // assert doubler.history == []; + + // var x := doubler.Invoke(2); + // assert doubler.Produced() == [x]; + // assert [x] == [4]; + // assert x == 4; + // } +} \ No newline at end of file diff --git a/src/Actions/DecreasesClauses.dfy b/src/Actions/DecreasesClauses.dfy new file mode 100644 index 00000000..d939e494 --- /dev/null +++ b/src/Actions/DecreasesClauses.dfy @@ -0,0 +1,103 @@ + +module Termination { + + datatype ClauseTail = More(next: TerminationMetric) | Top + + datatype TerminationMetric = TerminationMetric(first: TMValue, rest: ClauseTail) { + predicate DecreasesTo(other: TerminationMetric) { + if first == other.first then + match (rest, other.rest) { + case (_, Top) => false + case (Top, More(_)) => true + case (More(next), More(otherNext)) => next.DecreasesTo(otherNext) + } + else + first.DecreasesTo(other.first) + } + + ghost function {:axiom} Ordinal(): ORDINAL + } + + // Convenience constructors + function TerminationMetric1(value1: TMValue): TerminationMetric { + TerminationMetric(value1, Top) + } + function TerminationMetric2(value1: TMValue, value2: TMValue): TerminationMetric { + TerminationMetric(value1, More(TerminationMetric(value2, Top))) + } + function NatTerminationMetric(m: nat): TerminationMetric { + TerminationMetric1(TMNat(m)) + } + + // Heterogeneous encoding of the essential features of individual + // decreases clause list elements. + datatype TMValue = + | TMNat(natValue: nat) + | TMChar(charValue: nat) + | TMSeq(seqValue: seq) + | TMDatatype(children: seq) + // TODO: All other supported kinds of Dafny values + { + predicate DecreasesTo(other: TMValue) { + match (this, other) { + // Simple well-ordered types + case (TMNat(left), TMNat(right)) => left > right + case (TMChar(left), TMChar(right)) => left > right + // TODO: etc. + // Other is a strict subsequence of this + case (TMSeq(left), TMSeq(right)) => + || (exists i | 0 <= i < |left| :: left[..i] == right) + || (exists i | 0 < i <= |left| :: left[i..] == right) + || (exists i, j | 0 <= i < j <= |left| :: left[..i] + left[j..] == right) + // This is a sequence and other is a datatype and structurally included + // (treating a sequence as a datatype with N children) + case (TMSeq(leftSeq), TMDatatype(_)) => + || other in leftSeq + // Structural inclusion inside a datatype + // TODO: Does other have to be a datatype too? + case (TMDatatype(leftChildren), _) => + || other in leftChildren + + // TODO: other cases + case _ => false + } + } + } + + // TODO: prove DecreasesTo is a well-founded ordering + // (useful exercise and helps catch typos inconsistent with Dafny's ordering) + + // Assume a mapping exists from the DecreasesTo ordering onto the ordinals. + // This always exists, but is complicated to define concretely + // and technically has to be defined for a whole program. + // It's sound to just assume it exists to convince Dafny that + // `decreases terminationMetric.Ordinal()` is valid. + lemma {:axiom} OrdinalOrdered(left: TerminationMetric, right: TerminationMetric) + requires left.DecreasesTo(right) + ensures left.Ordinal() > right.Ordinal() +} + +module Example { + + datatype Tree = Node(children: seq>) | Nil + + function Count(t: Tree): nat { + match t + case Node(children) => + // assert t decreases to children; + CountSum(children) + case Nil => + 0 + } + + function CountSum(children: seq>): nat { + if |children| == 0 then + 0 + else + // assert children decreases to children[0]; + var firstCount := Count(children[0]); + // assert children decreases to children[1..]; + var restCount := CountSum(children[1..]); + firstCount + restCount + } +} \ No newline at end of file diff --git a/src/Actions/Enumerators.dfy b/src/Actions/Enumerators.dfy new file mode 100644 index 00000000..2c6ab808 --- /dev/null +++ b/src/Actions/Enumerators.dfy @@ -0,0 +1,399 @@ + +include "Actions.dfy" + +module {:options "--function-syntax:4"} Enumerators { + + import opened Actions + import opened Wrappers + import opened Seq + import opened Math + + function Enumerated(produced: seq>): seq { + if |produced| == 0 || produced[0].None? then + [] + else + [produced[0].value] + Enumerated(produced[1..]) + } + + // TODO: Feels like there should be a cleaner expression of this + ghost predicate EnumeratesSeq(a: Action<(), Option>, s: seq) { + forall history | a.CanProduce(history) :: + var produced := Outputs(history); + var enumerated := Enumerated(produced); + && enumerated <= s + && (|enumerated| < |produced| ==> enumerated == s) + } + + lemma TerminatedDefinesEnumerated(s: seq>, n: nat) + requires Terminated(s, None, n) + ensures + && var length := Math.Min(|s|, n); + && Enumerated(s) == seq(length, i requires 0 <= i < length => s[i].value) + { + if n == 0 || |s| == 0 { + } else { + if s[0] == None { + } else { + assert 1 <= |Enumerated(s)|; + TerminatedDefinesEnumerated(s[1..], n - 1); + } + } + } + + lemma TerminatedDistributesOverConcat(left: seq, right: seq, c: T, n: nat) + requires Terminated(left, c, |left|) + requires Terminated(right, c, n) + ensures Terminated(left + right, c, |left| + n) + {} + + lemma EnumeratedDistributesOverConcat(left: seq>, right: seq>, n: nat) + requires Terminated(left, None, n) + ensures + if n < |left| then + Enumerated(left + right) == Enumerated(left) + else + Enumerated(left + right) == Enumerated(left) + Enumerated(right) + decreases |left| + |right| + { + if |left| == 0 { + assert left + right == right; + } else if |right| == 0 { + assert left + right == left; + } else { + if n < |left| { + if n == 0 { + + } else { + assert Terminated(left[1..], None, n - 1); + EnumeratedDistributesOverConcat(left[1..], right, n - 1); + assert left == [left[0]] + left[1..]; + EnumeratedDistributesOverConcat([left[0]], left[1..], 1); + assert ([left[0]] + left[1..]) + right == [left[0]] + (left[1..] + right); + } + } else { + assert Terminated(left[1..], None, |left[1..]|); + EnumeratedDistributesOverConcat(left[1..], right, n); + assert left == [left[0]] + left[1..]; + EnumeratedDistributesOverConcat([left[0]], left[1..], 1); + assert ([left[0]] + left[1..]) + right == [left[0]] + (left[1..] + right); + } + } + } + + lemma EnumeratedDistributesOverConcat2(left: seq>, right: seq>, n: nat) + requires Terminated(left + right, None, n) + ensures Enumerated(left + right) == Enumerated(left) + Enumerated(right) + { + TerminatedUndistributes(left, right, None, n); + TerminatedDefinesEnumerated(left + right, n); + EnumeratedDistributesOverConcat(left, right, n); + } + + + ghost function ProducedForEnumerator(s: seq, n: nat): seq> { + var before := Math.Min(|s|, n); + var after := Math.Max(|s|, n); + Seq.Map(x => Some(x), s[..before]) + Seq.Repeat(None, after - before) + } + + ghost predicate EnumerationBoundedBy(e: Action<(), Option>, limit: nat) { + forall history: seq<((), Option)> | e.CanProduce(history) :: + exists n: nat | n <= limit :: Terminated(Outputs(history), None, n) + } + + ghost predicate ConsumesAnything(a: Action<(), Option>) { + forall history, next | a.CanProduce(history) :: a.CanConsume(history, next) + } + + ghost predicate IsEnumerator(a: Action<(), Option>) { + && ConsumesAnything(a) + && exists limit :: EnumerationBoundedBy(a, limit) + } + + ghost function EnumerationBound(a: Action<(), Option>): (limit: nat) + requires IsEnumerator(a) + ensures EnumerationBoundedBy(a, limit) + { + var limit: nat :| EnumerationBoundedBy(a, limit); + limit + } + + ghost function EnumerationTerminationMetric(a: Action<(), Option>): nat + requires a.Valid() + reads a.Repr + requires IsEnumerator(a) + { + var limit := EnumerationBound(a); + var n: nat :| n <= limit && Terminated(Outputs(a.history), None, n); + TerminatedDefinesEnumerated(a.Produced(), n); + limit - |Enumerated(a.Produced())| + } + + twostate lemma ProducingSomeImpliesTerminated(a: Action<(), Option>, nextProduced: Option) + requires old(a.Valid()) + requires old(a.CanProduce(a.history)) + requires a.Valid() + requires a.CanProduce(a.history) + requires IsEnumerator(a) + requires a.Produced() == old(a.Produced()) + [nextProduced] + requires nextProduced.Some? + ensures Terminated(a.Produced(), None, |a.Produced()|) + { + var before := old(a.Produced()); + var n: nat :| n <= |before| && Terminated(before, None, n); + var m: nat :| Terminated(a.Produced(), None, m); + if n < |before| { + assert before[|before| - 1] == None; + assert a.Produced()[|a.Produced()| - 1] != None; + assert |a.Produced()| <= m; + assert a.Produced()[|before| - 1] != None; + assert false; + } + assert |before| <= n; + } + + twostate lemma EnumerationTerminationMetricDecreased(a: Action<(), Option>, nextProduced: Option) + requires old(a.Valid()) + requires a.Valid() + requires IsEnumerator(a) + requires a.Produced() == old(a.Produced()) + [nextProduced] + requires nextProduced.Some? + ensures EnumerationTerminationMetric(a) < old(EnumerationTerminationMetric(a)) + { + var before := old(a.Produced()); + var n: nat :| n <= |before| && Terminated(before, None, n); + var m: nat :| Terminated(a.Produced(), None, m); + if n < |before| { + assert before[|before| - 1] == None; + assert a.Produced()[|a.Produced()| - 1] != None; + assert |a.Produced()| <= m; + assert a.Produced()[|before| - 1] != None; + assert false; + } + assert |before| <= n; + + TerminatedDefinesEnumerated(before, n); + assert |Enumerated(before)| <= n; + TerminatedDistributesOverConcat(before, [nextProduced], None, 1); + assert Terminated(a.Produced(), None, |a.Produced()|); + TerminatedDefinesEnumerated(a.Produced(), |a.Produced()|); + } + + // Potentially infinite enumerator + type IEnumerator = Action<(), T> + + type Enumerator = e: IEnumerator> | IsEnumerator(e) witness * + + class SeqEnumerator extends Action<(), Option> { + + const elements: seq + // TODO: size_t? It's a hell of a lot easier to prove correct + // if this can increase unbounded to stay at |consumed|, + // but it's not ghost so we care about bounding it. + var index: nat + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(history) + decreases height, 0 + { + && this in Repr + && index == |history| + && CanProduce(history) + } + + constructor(s: seq) + ensures Valid() + ensures fresh(Repr - {this}) + ensures history == [] + ensures elements == s + { + elements := s; + index := 0; + + history := []; + Repr := {this}; + } + + ghost predicate CanConsume(history: seq<((), Option)>, next: ()) + decreases height + { + true + } + ghost predicate CanProduce(history: seq<((), Option)>) + decreases height + { + var index := |history|; + var values := Math.Min(index, |elements|); + var nones := index - values; + Outputs(history) == Seq.Map(x => Some(x), elements[..values]) + Seq.Repeat(None, nones) + } + + method Invoke(t: ()) returns (r: Option) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert Valid(); + if index < |elements| { + r := Some(elements[index]); + } else { + r := None; + } + + index := index + 1; + Update((), r); + assert this in Repr; + assert index == |history|; + // TODO: Need some resuable lemmas relating Inputs() and Outputs()? + assert CanProduce(history); + } + } + + lemma SeqEnumeratorIsEnumerator(e: SeqEnumerator) + ensures IsEnumerator(e) + { + forall history | e.CanProduce(history) + ensures Terminated(Outputs(history), None, |e.elements|) + { + } + assert EnumerationBoundedBy(e, |e.elements|); + } + + class SeqIEnumerator extends Action<(), T> { + + const elements: seq + var index: nat + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(history) + decreases height, 0 + { + && this in Repr + && 0 <= index <= |elements| + && |history| == index + && Produced() == elements[0..index] + } + + constructor(s: seq) + ensures Valid() + ensures fresh(Repr - {this}) + ensures history == [] + ensures elements == s + { + elements := s; + index := 0; + + history := []; + Repr := {this}; + } + + ghost predicate CanConsume(history: seq<((), T)>, next: ()) + decreases height + { + |history| + 1 <= |elements| + } + ghost predicate CanProduce(history: seq<((), T)>) + decreases height + { + |history| <= |elements| && Outputs(history) == elements[..|history|] + } + + method Invoke(t: ()) returns (r: T) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert Valid(); + r := elements[index]; + index := index + 1; + + Update((), r); + } + } + + // Note that this means "possibly infinite" as opposed to "definitely infinite", + // but if a value is finite its enumerator has to communicate + trait IEnumerable { + method IEnumerator() returns (e: IEnumerator) + } + + trait Enumerable extends IEnumerable> { + method Enumerator() returns (e: Enumerator) + } + + // method ForEach(source: Enumerator, sink: Aggregator) + // requires source.Valid() + // requires sink.Valid() + // requires forall produced + // | source.CanProduce(Seq.Repeat((), |produced|), produced) + // :: sink.CanConsume(produced, Seq.Repeat((), |produced|)) + // requires source.Repr !! sink.Repr + // modifies source.Repr, sink.Repr + // { + // while true + // invariant source.Valid() + // invariant fresh(source.Repr - old(source.Repr)) + // invariant sink.Valid() + // invariant fresh(sink.Repr - old(sink.Repr)) + // invariant source.Repr !! sink.Repr + // modifies source.Repr, sink.Repr + // decreases EnumerationTerminationMetric(source) + // { + // label beforeLoop: + // var next: Option := source.Invoke(()); + // if next.None? { break; } + // EnumerationTerminationMetricDecreased@beforeLoop(source, next); + + // var _ := sink.Invoke(next.value); + // } + // } + + // Examples + + method EnumeratorExample() { + var e2: SeqEnumerator := new SeqEnumerator([1, 2, 3, 4, 5]); + SeqEnumeratorIsEnumerator(e2); + + // Could be `while next :- e2.Invoke(())` instead :) + while true + invariant e2.Valid() + invariant fresh(e2.Repr) + decreases EnumerationTerminationMetric(e2) + { + label beforeLoop: + var next: Option := e2.Invoke(()); + if next.None? { break; } + EnumerationTerminationMetricDecreased@beforeLoop(e2, next); + + print next.value; + } + } + + method IEnumeratorExample() { + var e: Action<(), int> := new SeqIEnumerator([1, 2, 3, 4, 5]); + var x := e.Invoke(()); + assert e.Produced() == [1]; + x := e.Invoke(()); + assert e.Produced() == [1, 2]; + x := e.Invoke(()); + assert e.Produced() == [1, 2, 3]; + x := e.Invoke(()); + assert e.Produced() == [1, 2, 3, 4]; + x := e.Invoke(()); + assert e.Produced() == [1, 2, 3, 4, 5]; + } + + method Main() { + EnumeratorExample(); + } +} \ No newline at end of file diff --git a/src/Actions/FilteredEnumerator.dfy b/src/Actions/FilteredEnumerator.dfy new file mode 100644 index 00000000..420c7930 --- /dev/null +++ b/src/Actions/FilteredEnumerator.dfy @@ -0,0 +1,127 @@ + +include "Enumerators.dfy" + +module Filtered { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + + class Filter extends Action<(), Option> { + + const wrapped: Action<(), Option> + + // TODO: Can we support --> or ~>? + const filter: T -> bool + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(consumed, produced) + decreases height, 0 + { + && this in Repr + && ValidComponent(wrapped) + && IsEnumerator(wrapped) + && CanProduce(consumed, produced) + && Enumerated(produced) == Seq.Filter(filter, Enumerated(wrapped.produced)) + } + + constructor(filter: T -> bool, wrapped: Action<(), Option>) + requires wrapped.Valid() + requires IsEnumerator(wrapped) + requires wrapped.consumed == [] && wrapped.produced == [] + ensures Valid() + { + this.filter := filter; + this.wrapped := wrapped; + + consumed := []; + produced := []; + Repr := {this} + wrapped.Repr; + height := wrapped.height + 1; + } + + ghost predicate CanConsume(consumed: seq<()>, produced: seq>, next: ()) + decreases height + { + true + } + ghost predicate CanProduce(consumed: seq<()>, produced: seq>) + ensures CanProduce(consumed, produced) ==> |consumed| == |produced| + decreases height + { + && |consumed| == |produced| + && exists producedByWrapped: seq> :: ValidWrappedProduced(produced, producedByWrapped) + } + + ghost predicate ValidWrappedProduced(produced: seq>, producedByWrapped: seq>) { + && wrapped.CanProduce(Seq.Repeat((), |producedByWrapped|), producedByWrapped) + && Enumerated(produced) == Seq.Filter(filter, Enumerated(producedByWrapped)) + } + + method {:vcs_split_on_every_assert} Invoke(t: ()) returns (r: Option) + requires Valid() + requires CanConsume(consumed, produced, t) + modifies Repr + decreases height + ensures Valid() + ensures fresh(Repr - old(Repr)) + ensures consumed == old(consumed) + [t] + ensures produced == old(produced) + [r] + { + while true + invariant wrapped.Valid() + invariant fresh(wrapped.Repr - old(wrapped.Repr)) + invariant ValidWrappedProduced(produced, wrapped.produced) + invariant produced == old(produced) + invariant consumed == old(consumed) + invariant Enumerated(produced) == Seq.Filter(filter, Enumerated(wrapped.produced)) + decreases EnumerationTerminationMetric(wrapped) + { + assert IsEnumerator(wrapped); + assert ConsumesAnything(wrapped); + assert wrapped.Valid(); + assert wrapped.CanProduce(wrapped.consumed, wrapped.produced); + label before: + r := wrapped.Invoke(()); + + Repr := {this} + wrapped.Repr; + + if r.None? || filter(r.value) { + break; + } + EnumerationTerminationMetricDecreased@before(wrapped, r); + + // var wrappedEnumeratedBefore := Enumerated(old@before(wrapped.produced)); + // assert wrapped.produced == old@before(wrapped.produced) + [r]; + + // ProducingSomeImpliesTerminated@before(wrapped, r); + // TerminatedBoundsEnumerated(wrapped.produced, |wrapped.produced|); + // // TerminatedDistributesOverConcat(old@before(wrapped.produced), [r], None, 1); + // assert |Enumerated(wrapped.produced)| == |wrapped.produced|; + // assert wrapped.produced == old@before(wrapped.produced) + [r]; + // EnumeratedDistributesOverConcat(old@before(wrapped.produced), [r], 1); + // assert Enumerated(wrapped.produced) == Enumerated(old@before(wrapped.produced)) + [r.value]; + + // assert Enumerated(old(produced)) == Seq.Filter(filter, Enumerated(old(wrapped.produced))); + // calc { + // Seq.Filter(filter, Enumerated(wrapped.produced)); + // Seq.Filter(filter, Enumerated(old(wrapped.produced) + [r])); + // Seq.Filter(filter, Enumerated(old(wrapped.produced)) + Enumerated([r])); + // Seq.Filter(filter, Enumerated(old(wrapped.produced)) + [r.value]); + // { LemmaFilterDistributesOverConcat(filter, wrappedEnumeratedBefore, [r.value]); } + // Seq.Filter(filter, Enumerated(old(wrapped.produced))) + Seq.Filter(filter, [r.value]); + // Seq.Filter(filter, Enumerated(old(wrapped.produced))); + // } + // assert Enumerated(produced) == Seq.Filter(filter, Enumerated(wrapped.produced)); + } + + assert r.Some? ==> filter(r.value); + assert wrapped.CanProduce(wrapped.consumed, wrapped.produced); + Update(t, r); + } + } +} \ No newline at end of file diff --git a/src/Actions/FunctionAction.dfy b/src/Actions/FunctionAction.dfy new file mode 100644 index 00000000..7d003e71 --- /dev/null +++ b/src/Actions/FunctionAction.dfy @@ -0,0 +1,76 @@ + +include "Enumerators.dfy" + +module Functions { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + + class FunctionAction extends Action { + + // TODO: Can we support ~>? + const f: T --> R + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(history) + decreases height, 0 + { + && this in Repr + && CanProduce(history) + && Produced() == Seq.Map(f, Consumed()) + } + + constructor(f: T -> R) + ensures Valid() + ensures this.f == f + ensures fresh(Repr) + ensures history == [] + { + this.f := f; + + history := []; + Repr := {this}; + } + + ghost predicate CanConsume(history: seq<(T, R)>, next: T) + requires CanProduce(history) + decreases height + { + f.requires(next) + } + ghost predicate CanProduce(history: seq<(T, R)>) + decreases height + { + forall e <- history :: f.requires(e.0) && e.1 == f(e.0) + } + + method Invoke(t: T) returns (r: R) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert Valid(); + r := f(t); + + Update(t, r); + } + } + + method Example() { + var doubler := new FunctionAction(v => v + v); + + assert doubler.history == []; + + var x := doubler.Invoke(2); + assert doubler.Produced() == [x]; + assert [x] == [4]; + assert x == 4; + } +} \ No newline at end of file diff --git a/src/Actions/GenericAction.dfy b/src/Actions/GenericAction.dfy new file mode 100644 index 00000000..ee45578e --- /dev/null +++ b/src/Actions/GenericAction.dfy @@ -0,0 +1,40 @@ + +include "../Wrappers.dfy" +include "../Frames.dfy" +include "../Math.dfy" +include "../Collections/Sequences/Seq.dfy" + +include "DecreasesClauses.dfy" + +module GenericActions { + + import opened Termination + + trait {:termination false} GenericAction { + + // Specification predicates + + ghost predicate Requires(t: T) + reads Reads(t) + ghost function Reads(t: T): set + // requires Requires(t) + reads this + ensures this in Reads(t) + ghost function Modifies(t: T): set + reads Reads(t) + ghost function Decreases(t: T): TerminationMetric + reads Reads(t) + twostate predicate Ensures(t: T, new r: R) + reads Reads(t) + + // Actual action implementation + + method Invoke(t: T) returns (r: R) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + } + +} \ No newline at end of file diff --git a/src/Actions/IteratorAction.dfy b/src/Actions/IteratorAction.dfy new file mode 100644 index 00000000..9fc9e59a --- /dev/null +++ b/src/Actions/IteratorAction.dfy @@ -0,0 +1,114 @@ +include "Enumerators.dfy" + +module IteratorActionExample { + + import opened Actions + import opened Enumerators + import opened Wrappers + + iterator Iter(s: set) yields (x: T) + yield ensures x in s && x !in xs[..|xs|-1] + ensures s == set z | z in xs + { + var r := s; + while (r != {}) + invariant r !! set z | z in xs + invariant s == r + set z | z in xs + { + var y :| y in r; + assert y !in xs; + r, x := r - {y}, y; + assert y !in xs; + yield; + assert y == xs[|xs|-1]; // a lemma to help prove loop invariant + } + } + + class IterAction extends Action<(), Option> { + + const i: Iter + var more: bool + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> CanProduce(history) + decreases height, 0 + { + && this in Repr + && i in Repr + && i._new <= Repr + && i._reads <= Repr + && i._modifies <= Repr + && this !in i._reads + && this !in i._new + && (more ==> i.Valid()) + && CanProduce(history) + } + + constructor(i: Iter) + requires i.Valid() + requires i.xs == [] + ensures Valid() + { + this.i := i; + this.more := true; + + history := []; + Repr := {this, i} + i._modifies + i._reads + i._new; + new; + assert (set x | x in Enumerated(Outputs(history))) == {}; + } + + ghost predicate CanConsume(history: seq<((), Option)>, next: ()) + requires CanProduce(history) + decreases height + { + true + } + + ghost predicate CanProduce(history: seq<((), Option)>) + decreases height + { + && var enumeratedSet := (set x | x in Enumerated(Outputs(history))); + && enumeratedSet <= i.s + } + + method Invoke(t: ()) returns (r: Option) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert Valid(); + assert this !in i._reads; + if more { + r := Some(i.x); + assert this !in i._reads; + + var more := i.MoveNext(); + assert this !in i._reads; + assert more ==> i.Valid(); + assert this !in i._new; + } else { + assert this !in i._new; + r := None; + assert this !in i._new; + } + assert this !in i._new; + assert more ==> i.Valid(); + + Update(t, r); + Repr := {this, i} + i._reads + i._new + i._modifies; + + assert this in Repr; + assert i in Repr; + assert i._reads <= Repr; + assert i._new <= Repr; + assert more ==> i.Valid(); + // assert CanProduce(consumed, produced); + } + } + +} \ No newline at end of file diff --git a/src/Actions/MappingEnumerator.dfy b/src/Actions/MappingEnumerator.dfy new file mode 100644 index 00000000..3a43c5c1 --- /dev/null +++ b/src/Actions/MappingEnumerator.dfy @@ -0,0 +1,129 @@ + +include "Enumerators.dfy" + +module Mapped { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + + // TODO: should be unnecessary with FunctionAction, ComposedAction, and the right lemmas + class Map extends Action { + + const wrapped: Action + ghost const wrappedCanConsume: (seq, seq, T) --> bool + ghost const wrappedCanProduce: (seq, seq) -> bool + + // TODO: Can we support --> or ~>? + const f: R -> R' + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(consumed, produced) + decreases height, 0 + { + && this in Repr + && ValidComponent(wrapped) + && CanProduce(consumed, produced) + && consumed == wrapped.consumed + && produced == Seq.Map(f, wrapped.produced) + && wrappedCanConsume == wrapped.CanConsume + && wrappedCanProduce == wrapped.CanProduce + } + + constructor(f: R -> R', wrapped: Action) + requires wrapped.Valid() + requires wrapped.consumed == [] && wrapped.produced == [] + ensures Valid() + ensures fresh(Repr - (wrapped.Repr)) + ensures this.wrapped == wrapped + ensures this.f == f + { + this.f := f; + this.wrapped := wrapped; + + consumed := []; + produced := []; + Repr := {this} + wrapped.Repr; + height := wrapped.height + 1; + wrappedCanConsume := wrapped.CanConsume; + wrappedCanProduce := wrapped.CanProduce; + new; + assert ValidWrappedProduced(consumed, produced, wrapped.produced); + } + + ghost predicate CanConsume(consumed: seq, produced: seq, next: T) + requires CanProduce(consumed, produced) + decreases height + { + forall producedByWrapped: seq | ValidWrappedProduced(consumed, produced, producedByWrapped) :: + assert wrapped.CanProduce(consumed, producedByWrapped); + wrapped.CanConsume(consumed, producedByWrapped, next) + } + ghost predicate CanProduce(consumed: seq, produced: seq) + decreases height + { + exists producedByWrapped: seq :: ValidWrappedProduced(consumed, produced, producedByWrapped) + } + + ghost predicate ValidWrappedProduced(consumed: seq, produced: seq, producedByWrapped: seq) { + && wrappedCanProduce(consumed, producedByWrapped) + && produced == Seq.Map(f, producedByWrapped) + } + + method Invoke(t: T) returns (r: R') + requires Valid() + requires CanConsume(consumed, produced, t) + modifies Repr + decreases height + ensures Valid() + ensures fresh(Repr - old(Repr)) + ensures consumed == old(consumed) + [t] + ensures produced == old(produced) + [r] + { + assert wrapped.Valid(); + var x := wrapped.Invoke(t); + r := f(x); + + Repr := {this} + wrapped.Repr; + Update(t, r); + + Seq.LemmaMapDistributesOverConcat(f, old(wrapped.produced), [x]); + assert ValidWrappedProduced(consumed, produced, wrapped.produced); + } + } + + // lemma EnumeratornessCommutes(mapped: Map<(), Option, Option>) + // requires mapped.Valid() + // requires IsEnumerator(mapped.wrapped) + // ensures IsEnumerator(mapped) + // { + // var limit := EnumerationBound(mapped.wrapped); + // forall consumed, produced | mapped.CanProduce(consumed, produced) + // ensures exists n: nat | n <= limit :: Terminated(produced, None, n) + // { + // var producedByWrapped :| mapped.ValidWrappedProduced(consumed, produced, producedByWrapped); + // var n :| n <= limit && Terminated(producedByWrapped, None, n); + // assert Terminated(produced, None, n); + // } + // assert EnumerationBoundedBy(mapped, limit); + // } + + method Example() { + var e: SeqEnumerator := new SeqEnumerator([1, 2, 3, 4, 5]); + SeqEnumeratorIsEnumerator(e); + var f := (x: Option) => match x { + case Some(v) => Some(v + v) + case None => None + }; + var mapped: Map<(), Option, Option> := new Map(f, e); + + var x := mapped.Invoke(()); + assert mapped.produced == [Some(2)]; + assert [x] == [Some(2)]; + assert x == Some(2); + } +} \ No newline at end of file diff --git a/src/Actions/NestedEnumerator.dfy b/src/Actions/NestedEnumerator.dfy new file mode 100644 index 00000000..43ccb1a2 --- /dev/null +++ b/src/Actions/NestedEnumerator.dfy @@ -0,0 +1,135 @@ + +include "Enumerators.dfy" + +module Nested { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + + // The equivalent of SelectMany from LINQ + class Nested extends Action<(), Option> { + + const first: Action<(), V> + const secondConstr: Action>> + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(consumed, produced) + decreases height, 0 + { + && this in Repr + && ValidComponent(first) + && ValidComponent(secondConstr) + && first.Repr !! secondConstr.Repr + && IsEnumerator(wrapped) + && CanProduce(consumed, produced) + && Enumerated(produced) == Seq.Filter(filter, Enumerated(wrapped.produced)) + } + + constructor(filter: T -> bool, wrapped: Action<(), Option>) + requires wrapped.Valid() + requires IsEnumerator(wrapped) + requires wrapped.consumed == [] && wrapped.produced == [] + ensures Valid() + { + this.filter := filter; + this.wrapped := wrapped; + + consumed := []; + produced := []; + Repr := {this} + wrapped.Repr; + height := wrapped.height + 1; + } + + ghost predicate CanConsume(consumed: seq<()>, produced: seq>, next: ()) + decreases height + { + true + } + ghost predicate CanProduce(consumed: seq<()>, produced: seq>) + ensures CanProduce(consumed, produced) ==> |consumed| == |produced| + decreases height + { + && |consumed| == |produced| + && exists producedByWrapped: seq> :: ValidWrappedProduced(produced, producedByWrapped) + } + + ghost predicate ValidWrappedProduced(produced: seq>, producedByWrapped: seq>) { + && wrapped.CanProduce(Seq.Repeat((), |producedByWrapped|), producedByWrapped) + && Enumerated(produced) == Seq.Filter(filter, Enumerated(producedByWrapped)) + } + + // + method {:vcs_split_on_every_assert} Invoke(t: ()) returns (r: Option) + requires Valid() + requires CanConsume(consumed, produced, t) + modifies Repr + decreases height + ensures Valid() + ensures fresh(Repr - old(Repr)) + ensures consumed == old(consumed) + [t] + ensures produced == old(produced) + [r] + { + // while true: + // if + + while true + invariant wrapped.Valid() + invariant fresh(wrapped.Repr - old(wrapped.Repr)) + invariant ValidWrappedProduced(produced, wrapped.produced) + invariant produced == old(produced) + invariant consumed == old(consumed) + invariant Enumerated(produced) == Seq.Filter(filter, Enumerated(wrapped.produced)) + decreases EnumerationTerminationMetric(wrapped) + { + assert IsEnumerator(wrapped); + assert ConsumesAnything(wrapped); + assert wrapped.Valid(); + assert wrapped.CanProduce(wrapped.consumed, wrapped.produced); + label before: + r := wrapped.Invoke(()); + + Repr := {this} + wrapped.Repr; + + if r.None? || filter(r.value) { + break; + } + EnumerationTerminationMetricDecreased@before(wrapped, r); + + // var wrappedEnumeratedBefore := Enumerated(old@before(wrapped.produced)); + // assert wrapped.produced == old@before(wrapped.produced) + [r]; + + // ProducingSomeImpliesTerminated@before(wrapped, r); + // TerminatedBoundsEnumerated(wrapped.produced, |wrapped.produced|); + // // TerminatedDistributesOverConcat(old@before(wrapped.produced), [r], None, 1); + // assert |Enumerated(wrapped.produced)| == |wrapped.produced|; + // assert wrapped.produced == old@before(wrapped.produced) + [r]; + // EnumeratedDistributesOverConcat(old@before(wrapped.produced), [r], 1); + // assert Enumerated(wrapped.produced) == Enumerated(old@before(wrapped.produced)) + [r.value]; + + // assert Enumerated(old(produced)) == Seq.Filter(filter, Enumerated(old(wrapped.produced))); + // calc { + // Seq.Filter(filter, Enumerated(wrapped.produced)); + // Seq.Filter(filter, Enumerated(old(wrapped.produced) + [r])); + // Seq.Filter(filter, Enumerated(old(wrapped.produced)) + Enumerated([r])); + // Seq.Filter(filter, Enumerated(old(wrapped.produced)) + [r.value]); + // { LemmaFilterDistributesOverConcat(filter, wrappedEnumeratedBefore, [r.value]); } + // Seq.Filter(filter, Enumerated(old(wrapped.produced))) + Seq.Filter(filter, [r.value]); + // Seq.Filter(filter, Enumerated(old(wrapped.produced))); + // } + // assert Enumerated(produced) == Seq.Filter(filter, Enumerated(wrapped.produced)); + } + + assert r.Some? ==> filter(r.value); + assert wrapped.CanProduce(wrapped.consumed, wrapped.produced); + Update(t, r); + } + } + + // TODO: Lemma that if first is an enumerator (which requires V == Option for some V') + // then Nested(first, secondConstr) is too +} \ No newline at end of file diff --git a/src/Actions/NoOpEnumerator.dfy b/src/Actions/NoOpEnumerator.dfy new file mode 100644 index 00000000..fe418fd5 --- /dev/null +++ b/src/Actions/NoOpEnumerator.dfy @@ -0,0 +1,92 @@ +include "Enumerators.dfy" + +module NoOp { + + import opened Actions + import opened Enumerators + import opened Wrappers + import opened Seq + + // Useful test case to ensure it's possible to compose Actions in general: + // if you can't simply wrap an Action and implement the same specification, + // there's no hope of changing behavior or composing Actions. :) + class NoOp extends Action { + + const wrapped: Action + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + ensures Valid() ==> + && CanProduce(history) + decreases height, 0 + { + && this in Repr + && ValidComponent(wrapped) + && CanProduce(history) + && history == wrapped.history + } + + constructor(wrapped: Action) + requires wrapped.Valid() + requires wrapped.history == [] + ensures Valid() + { + this.wrapped := wrapped; + + history := []; + Repr := {this} + wrapped.Repr; + height := wrapped.height + 1; + new; + } + + ghost predicate CanConsume(history: seq<(T, R)>, next: T) + requires CanProduce(history) + decreases height + { + wrapped.CanConsume(history, next) + } + + ghost predicate CanProduce(history: seq<(T, R)>) + decreases height + { + wrapped.CanProduce(history) + } + + method Invoke(t: T) returns (r: R) + requires Requires(t) + reads Reads(t) + modifies Modifies(t) + decreases Decreases(t).Ordinal() + ensures Ensures(t, r) + { + assert CanConsume(history, t); + r := wrapped.Invoke(t); + + Repr := {this} + wrapped.Repr; + Update(t, r); + assert Valid(); + } + } + + lemma EnumeratornessCommutes(noop: NoOp<(), Option>) + requires noop.Valid() + requires IsEnumerator(noop.wrapped) + ensures IsEnumerator(noop) + { + // TODO: working around the fact that triggers don't automatically apply + // because noop has the type NoOp as opposed to Action. + // Not sure if there's a more reusable workaround to the problem (which is going to recur frequently in this library) + var noopAsAction: Action<(), Option> := noop; + + forall history, next | noop.CanProduce(history) ensures noopAsAction.CanConsume(history, next) { + assert noop.CanConsume(history, next); + } + + var limit := EnumerationBound(noop.wrapped); + forall history | noopAsAction.CanProduce(history) ensures exists n: nat | n <= limit :: Terminated(Outputs(history), None, n) { + assert noop.CanProduce(history); + } + assert EnumerationBoundedBy(noop, limit); + } +} \ No newline at end of file diff --git a/src/Actions/ObjectQuantification.dfy b/src/Actions/ObjectQuantification.dfy new file mode 100644 index 00000000..b3de1fa0 --- /dev/null +++ b/src/Actions/ObjectQuantification.dfy @@ -0,0 +1,9 @@ +module Testing { + + trait SimpleAction { + method Invoke() returns (t: T) + } + + method + +} \ No newline at end of file diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index 44c7264e..85d18ddd 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -100,6 +100,13 @@ module {:options "-functionSyntax:4"} Maps { map y | y in m.Values :: var x :| x in m.Keys && m[x] == y; x } + function {:opaque} BetterInvert(m: map): map + requires Injective(m) + { + reveal Injective(); + map k | k in m :: m[k] := k + } + /* Inverted maps are injective. */ lemma LemmaInvertIsInjective(m: map) ensures Injective(Invert(m)) diff --git a/src/Collections/Sequences/MergeSort.dfy b/src/Collections/Sequences/MergeSort.dfy index 42be3a36..f4121e5f 100644 --- a/src/Collections/Sequences/MergeSort.dfy +++ b/src/Collections/Sequences/MergeSort.dfy @@ -12,7 +12,7 @@ module {:options "-functionSyntax:4"} Seq.MergeSort { import opened Relations //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedWith` - function MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) + function MergeSortBy(a: seq, lessThanOrEq: (T, T) -> bool): (result :seq) requires TotalOrdering(lessThanOrEq) ensures multiset(a) == multiset(result) ensures SortedBy(result, lessThanOrEq) @@ -31,7 +31,7 @@ module {:options "-functionSyntax:4"} Seq.MergeSort { MergeSortedWith(leftSorted, rightSorted, lessThanOrEq) } - function {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) + function {:tailrecursion} MergeSortedWith(left: seq, right: seq, lessThanOrEq: (T, T) -> bool) : (result :seq) requires SortedBy(left, lessThanOrEq) requires SortedBy(right, lessThanOrEq) requires TotalOrdering(lessThanOrEq) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 815970b9..df3a4414 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -728,7 +728,7 @@ module {:options "-functionSyntax:4"} Seq { } /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */ - lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, + lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, stp: (B, A, B) -> bool, f: (B, A) -> B, b: B, @@ -786,7 +786,7 @@ module {:options "-functionSyntax:4"} Seq { } /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */ - lemma LemmaInvFoldRight(inv: (seq, B) -> bool, + lemma LemmaInvFoldRight(inv: (seq, B) -> bool, stp: (A, B, B) -> bool, f: (A, B) -> B, b: B, @@ -833,7 +833,7 @@ module {:options "-functionSyntax:4"} Seq { } /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */ - lemma SortedUnique(xs: seq, ys: seq, R: (T, T) -> bool) + lemma SortedUnique(xs: seq, ys: seq, R: (T, T) -> bool) requires SortedBy(xs, R) requires SortedBy(ys, R) requires TotalOrdering(R) @@ -853,7 +853,7 @@ module {:options "-functionSyntax:4"} Seq { } /* Converts a set to a sequence that is ordered w.r.t. a given total order. */ - function SetToSortedSeq(s: set, R: (T, T) -> bool): (xs: seq) + function SetToSortedSeq(s: set, R: (T, T) -> bool): (xs: seq) requires TotalOrdering(R) ensures multiset(s) == multiset(xs) ensures SortedBy(xs, R) diff --git a/src/Enumerators/EnumeratorFns.dfy b/src/Enumerators/EnumeratorFns.dfy new file mode 100644 index 00000000..f7d5df2b --- /dev/null +++ b/src/Enumerators/EnumeratorFns.dfy @@ -0,0 +1,71 @@ + + +datatype Option<+T> = Some(value: T) | None + +function SeqEnumeratorFn(s: seq): Option<(seq, T)> { + if |s| == 0 then + None + else + Some((s[1..], s[0])) +} + +function SetEnumeratorFn(s: set): Option<(set, T)> { + if |s| == 0 then + None + else + var t :| t in s; + Some((s - {t}, t)) +} + +type EnumeratorFn = S -> Option<(S, T)> +datatype Enumerator_ = Enumerator(state: S, fn: EnumeratorFn, ghost decreasesFn: S -> nat) { + ghost predicate Valid() { + Decreases(fn, decreasesFn) + } +} +ghost predicate Decreases(fn: EnumeratorFn, decreasesFn: S -> nat) { + forall s: S :: match fn(s) + case Some((s', _)) => decreasesFn(s') < decreasesFn(s) + case None => true +} + +type Enumerator = e: Enumerator_ | e.Valid() witness * + +function {:tailrecursion} Enumerate(e: Enumerator): seq + decreases e.decreasesFn(e.state) +{ + match e.fn(e.state) + case Some((s, t)) => [t] + Enumerate(Enumerator(s, e.fn, e.decreasesFn)) + case None => [] +} + +function ConcatEnumeratorFn(first: EnumeratorFn, second: EnumeratorFn): EnumeratorFn<(A, B), T> { + x => + var (a, b) := x; + match first(a) + case Some((a', t)) => Some(((a', b), t)) + case None => + match second(b) + case Some((b', t)) => Some(((a, b'), t)) + case None => None +} + +function ConcatDecreasesFn(first: A -> nat, second: B -> nat): ((A, B)) -> nat { + x => + var (a, b) := x; + var result: nat := first(a) + second(b); + result +} + +function ConcatEnumerator(first: Enumerator, second: Enumerator): Enumerator<(A, B), T> { + var result := Enumerator((first.state, second.state), + ConcatEnumeratorFn(first.fn, second.fn), + ConcatDecreasesFn(first.decreasesFn, second.decreasesFn)); + result +} + +lemma ConcatEnumeratesConcat(first: Enumerator, second: Enumerator) + ensures Enumerate(ConcatEnumerator(first, second)) == Enumerate(first) + Enumerate(second) +{ + +} \ No newline at end of file diff --git a/src/Enumerators/Enumerators.dfy b/src/Enumerators/Enumerators.dfy new file mode 100644 index 00000000..0edea5f7 --- /dev/null +++ b/src/Enumerators/Enumerators.dfy @@ -0,0 +1,908 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "../Frames.dfy" +include "../Wrappers.dfy" +include "../Math.dfy" +include "../Collections/Sequences/Seq.dfy" + +module Enumerators { + + import opened Frames + import opened Wrappers + import opened Seq + import opened Math + + // A trait for any value that produces a potentially infinite sequence of values. + trait {:termination false} IEnumerator extends Validatable { + + // The Valid() predicate from the Validatable trait can be thought of + // as the "enumeration invariant", which in turn becomes + // the loop invariant in a while loop that uses an enumerator. + + // All values produced by the Next() method in the order they + // were produced. + // TODO: Is this actually useful? + ghost var ienumerated: seq + + method Next() returns (element: T) + requires Valid() + modifies Repr + decreases Repr + ensures ValidAndDisjoint() + ensures ienumerated == old(ienumerated) + [element] + } + + class NatEnumerator extends IEnumerator { + + var next: nat + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && next == |ienumerated| + && ienumerated == seq(|ienumerated|, i => i) + } + + constructor() + ensures Valid() + ensures fresh(Repr) + { + next := 0; + Repr := {this}; + ienumerated := []; + } + + method Next() returns (element: nat) + requires Valid() + modifies Repr + decreases Repr + ensures ValidAndDisjoint() + ensures ienumerated == old(ienumerated) + [element] + { + element := next; + next := next + 1; + + ienumerated := ienumerated + [element]; + } + } + + // A trait for any value that produces a finite sequence of values. + trait {:termination false} Enumerator extends IEnumerator> { + + ghost var enumerated: seq + + ghost method Enumerated(element: Option) + modifies this`ienumerated, this`enumerated + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> enumerated == old(enumerated) + [element.value] + ensures element.None? ==> unchanged(`enumerated) + { + ienumerated := ienumerated + [element]; + if element.Some? { + enumerated := enumerated + [element.value]; + } + } + + // The termination measure for the enumerator. Must decrease on every + // call to Next() that doesn't return None. + // + // Would be better as an arbitrary termination clause somehow instead, + // but we don't have language-level access to the built-in well-founded + // ordering. See https://github.com/dafny-lang/dafny/issues/762. + // TODO: Rename since this isn't 1:1 with decreases clauses, possibly "Remaining" + function Decreases(): nat + reads Repr + decreases Repr, 1 + requires Valid() + + // TODO: Done() alias for Decreases() == 0? + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + // This is more restrictive than the usual post-condition of + // Validatable.ValidAndDisjoint(), because if we allow the Repr + // of an enumerator to grow, even if fresh, it becomes much more + // difficult to prove termination of a wrapper enumerator like + // FilteredEnumerator below which needs to make a recursive call to + // Next() inside a loop. + ensures Repr <= old(Repr) + // TODO: Package up the rest in a twostate predicate? + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + } + + /********************************************************** + * + * Specializations + * + ***********************************************************/ + + // TODO: These aren't actually what we need. They only assert + // a property about the current state of an enumerator, but we need + // to assert this property holds for the enumerator in the future + // as well, as long as it stays Valid(). + // + // An alternate that works is to make these traits with body-less + // lemmas that must be proven by subclasses. That will cause an explosion + // of concrete types, though, because (for example) the ConcatEnumerator + // can't dynamically decide to extend SizedEnumerator whenever + // its two children do, so it forces a separate SizedConcatEnumerator + // (which can't even share implementation by extending SizedEnumerator) + + // TODO: Don't use "Size", implies sizeof() semantics + ghost predicate Sized(e: Enumerator, count: nat) + reads e.Repr + requires e.Valid() + { + e.Decreases() == 0 ==> |e.enumerated| == count + } + + ghost predicate EnumeratesMultiset(e: Enumerator, enumerated: multiset) + reads e.Repr + requires e.Valid() + { + e.Decreases() == 0 ==> multiset(e.enumerated) == enumerated + } + + ghost predicate EnumeratesSet(e: Enumerator, enumerated: set) + reads e.Repr + requires e.Valid() + { + e.Decreases() == 0 ==> multiset(e.enumerated) == multiset(enumerated) + } + + ghost predicate EnumeratesSeq(e: Enumerator, enumerated: seq) + reads e.Repr + requires e.Valid() + { + e.Decreases() == 0 ==> e.enumerated == enumerated + } + + /********************************************************** + * + * Concrete implementations + * + ***********************************************************/ + + // TODO: Some of these should be IEnumerator adaptors instead, + // possibly with an Enumerator subclass specialization. + + class SeqEnumerator extends Enumerator { + + const elements: seq + var index: nat + + constructor(s: seq) + ensures Valid() + ensures fresh(Repr - {this}) + ensures enumerated == [] + ensures elements == s + { + elements := s; + index := 0; + + enumerated := []; + Repr := {this}; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && 0 <= index <= |elements| + && enumerated == elements[0..index] + } + + function Decreases(): nat + reads Repr + requires Valid() + decreases Repr, 1 + { + |elements| - index + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + if index < |elements| { + element := Some(elements[index]); + index := index + 1; + } else { + element := None; + } + Enumerated(element); + } + } + + // This encapsulates the canonical method for enumerating + // the values in a set by using :| and set subtraction. + // Enumerating a set this way will generally take quadratic time, however, + // given each set subtraction will normally require making a new copy of + // the set at runtime. + // + // The good news is that if the Enumerator concept, or a generalized + // type characteristic it satisfies, is added to Dafny itself, then + // the various runtimes can provide a much more efficient implementation + // of EnumeratorOfSet based on iteration features in the underlying set + // implementation. + class SetEnumerator extends Enumerator { + ghost const original: set + var remaining: set + + constructor(s: set) + ensures Valid() + ensures fresh(Repr) + ensures enumerated == [] + ensures original == s + { + this.original := s; + this.remaining := s; + + enumerated := []; + Repr := {this}; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && multiset(enumerated) + multiset(remaining) == multiset(original) + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + |remaining| + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + if |remaining| > 0 { + var t :| t in remaining; + element := Some(t); + remaining := remaining - {t}; + } else { + element := None; + } + Enumerated(element); + } + } + + /********************************************************** + * + * Higher-order operations + * + ***********************************************************/ + + // TODO: Great case study for maintaining known properties through this transformation. + class MappingEnumerator extends Enumerator { + const wrapped: Enumerator + const f: T -> R + + constructor(f: T -> R, wrapped: Enumerator) + requires wrapped.Valid() + requires wrapped.enumerated == [] + ensures Valid() + ensures fresh(Repr - wrapped.Repr) + ensures enumerated == [] + ensures this.wrapped == wrapped + ensures this.f == f + { + this.wrapped := wrapped; + this.f := f; + Repr := {this} + wrapped.Repr; + enumerated := []; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(wrapped) + && enumerated == Seq.Map(f, wrapped.enumerated) + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + var optT := wrapped.Next(); + match optT + case Some(t) => { + element := Some(f(t)); + Enumerated(element); + } + case None => { + element := None; + Enumerated(element); + } + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + wrapped.Decreases() + } + } + + lemma MappingEnumeratorPreservesLength(e: MappingEnumerator, count: nat) + requires e.Valid() + requires Sized(e.wrapped, count) + ensures Sized(e, count) + {} + + // TODO: Generalize to a FlattenEnumerator that wraps an Enumerator> instead? + class ConcatEnumerator extends Enumerator { + + const first: Enumerator + var firstDone: bool + const second: Enumerator + + constructor(first: Enumerator, second: Enumerator) + requires first.Valid() && first.enumerated == [] + requires second.Valid() && second.enumerated == [] + requires first.Repr !! second.Repr + ensures Valid() + ensures fresh(Repr - first.Repr - second.Repr) + ensures this.first == first + ensures this.second == second + { + this.first := first; + this.firstDone := false; + this.second := second; + + enumerated := first.enumerated + second.enumerated; + Repr := {this} + first.Repr + second.Repr; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(first) + && ValidComponent(second) + && first.Repr !! second.Repr + && (firstDone ==> first.Decreases() == 0) + && (!firstDone ==> second.enumerated == []) + && enumerated == first.enumerated + second.enumerated + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + element := None; + if !firstDone { + element := first.Next(); + } + if element.None? { + firstDone := true; + element := second.Next(); + } + + Repr := {this} + first.Repr + second.Repr; + Enumerated(element); + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + first.Decreases() + second.Decreases() + } + + lemma CountOfResult(firstCount: nat, secondCount: nat) + requires Valid() + requires Sized(first, firstCount) + requires Sized(second, secondCount) + ensures Sized(this, firstCount + secondCount) + {} + } + + // This is a tricky one to make fully general: + // + // * The most general is of type (IEnumerator, IEnumerator) -> IEnumerator<(A, B)> + // * If either argument is finte, the result is too + // * If both arguments are sized, the result is too + // + // ...and if the class forgets any useful such properties, + // additional code can't add them later since the methods are opaque :( + // + // May also want an Enumerator2 variation, to avoid the + // pair overhead for common cases like `foreach x, index in` + class ZipEnumerator extends Enumerator<(A, B)> { + + const first: Enumerator + const second: Enumerator + + constructor(first: Enumerator, second: Enumerator, size: nat) + requires first.Valid() && first.enumerated == [] + requires second.Valid() && second.enumerated == [] + requires first.Repr !! second.Repr + ensures Valid() + ensures fresh(Repr - first.Repr - second.Repr) + ensures this.first == first + ensures this.second == second + { + this.first := first; + this.second := second; + + enumerated := []; + Repr := {this} + first.Repr + second.Repr; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(first) + && ValidComponent(second) + && first.Repr !! second.Repr + // TODO: See top-level comment + // && |enumerated| == |first.enumerated| == |second.enumerated| + // && enumerated == Seq.Zip(first.enumerated, second.enumerated) + } + + method Next() returns (element: Option<(A, B)>) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + var left := first.Next(); + var right := second.Next(); + if left.Some? && right.Some? { + element := Some((left.value, right.value)); + } else { + element := None; + } + + Repr := {this} + first.Repr + second.Repr; + Enumerated(element); + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + Math.Min(first.Decreases(), second.Decreases()) + } + } + + class WithIndexEnumerator extends Enumerator<(T, nat)> { + + const wrapped: Enumerator + var nextIndex: nat + + constructor(wrapped: Enumerator) + requires wrapped.Valid() + requires wrapped.enumerated == [] + ensures Valid() + ensures fresh(Repr - wrapped.Repr) + ensures enumerated == [] + ensures this.wrapped == wrapped + { + this.wrapped := wrapped; + this.nextIndex := 0; + + Repr := {this} + wrapped.Repr; + enumerated := []; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(wrapped) + // TODO: Similar challenge to ZipEnumerator although hopefully not as hard + // && enumerated == Seq.Zip(wrapped.enumerated, seq(|wrapped.enumerated|, i => i)) + } + + method Next() returns (element: Option<(T, nat)>) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + var t := wrapped.Next(); + if t.Some? { + element := Some((t.value, nextIndex)); + nextIndex := nextIndex + 1; + } else { + element := None; + } + Enumerated(element); + + // reveal Seq.Zip(); + // assert enumerated == Seq.Zip(wrapped.enumerated, seq(|wrapped.enumerated|, i => i)); + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + wrapped.Decreases() + } + } + + class FilteredEnumerator extends Enumerator { + const wrapped: Enumerator + const filter: T -> bool + + constructor(wrapped: Enumerator, filter: T -> bool) + requires wrapped.Valid() + requires wrapped.enumerated == [] + ensures Valid() + ensures fresh(Repr - old(wrapped.Repr)) + ensures enumerated == [] + ensures this.wrapped == wrapped + ensures this.filter == filter + { + this.wrapped := wrapped; + this.filter := filter; + Repr := {this} + wrapped.Repr; + enumerated := []; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(wrapped) + && enumerated == Seq.Filter(filter, wrapped.enumerated) + } + + method Next() returns (element: Option) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + element := None; + var more := true; + while more + invariant Valid() + invariant wrapped.Repr < old(Repr) + invariant Repr == old(Repr) + invariant element.Some? ==> Decreases() < old(Decreases()) + invariant !more && element.None? ==> Decreases() == 0 + invariant !more && element.None? ==> enumerated == old(enumerated) + invariant unchanged(`ienumerated) + invariant enumerated == Seq.Filter(filter, wrapped.enumerated) + decreases wrapped.Decreases(), more + { + var wrappedEnumeratedBefore := wrapped.enumerated; + // This is where it is very difficult to prove termination if we + // allow wrapped.Repr to potentially grow, because the assertion + // we must satisfy for the recursive call to be allowed is actually + // wrapped.Repr < old(Repr). That means updating Repr after this call + // wouldn't help. + var element := wrapped.Next(); + if element.None? { + assert Decreases() == 0; + more := false; + // break; + } else { + reveal Seq.Filter(); + LemmaFilterDistributesOverConcat(filter, wrappedEnumeratedBefore, [element.value]); + + if filter(element.value) { + enumerated := enumerated + [element.value]; + more := false; + // break; + } else { + } + } + } + ienumerated := ienumerated + [element]; + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + wrapped.Decreases() + } + } + + // This would allow a foreach loop to bind the values enumerated so far: + // + // foreach (x, xs) in WithEnumerated(collection) { ... } + // + // I like this better than the magical definitions iterators provide, + // since this way you're not culture-specific. :) + class WithEnumeratedEnumerator extends Enumerator<(T, ghost seq)> { + const wrapped: Enumerator + + constructor(wrapped: Enumerator) + requires wrapped.Valid() + requires wrapped.enumerated == [] + ensures Valid() + ensures fresh(Repr - wrapped.Repr) + ensures enumerated == [] + ensures this.wrapped == wrapped + { + this.wrapped := wrapped; + Repr := {this} + wrapped.Repr; + enumerated := []; + } + + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + decreases Repr, 0 + { + && this in Repr + && ValidComponent(wrapped) + } + + method Next() returns (element: Option<(T, ghost seq)>) + requires Valid() + modifies Repr + decreases Repr + ensures Valid() + ensures Repr <= old(Repr) + ensures ienumerated == old(ienumerated) + [element] + ensures element.Some? ==> ( + && Decreases() < old(Decreases()) + && enumerated == old(enumerated) + [element.value] + ) + ensures element.None? ==> ( + && Decreases() == 0 + && enumerated == old(enumerated) + ) + { + var optT := wrapped.Next(); + match optT + case Some(t) => { + element := Some((t, ghost wrapped.enumerated)); + Enumerated(element); + } + case None => { + element := None; + Enumerated(element); + } + } + + function Decreases(): nat + reads this, Repr + requires Valid() + decreases Repr, 1 + { + wrapped.Decreases() + } + } + + method Fold(f: (A, T) -> A, init: A, e: Enumerator) returns (result: A) + requires e.Valid() + requires e.enumerated == [] + modifies e.Repr + ensures e.Valid() + ensures e.Decreases() == 0 + ensures result == Seq.FoldLeft(f, init, e.enumerated) + { + reveal Seq.FoldLeft(); + result := init; + while true + invariant e.Valid() && e.Repr <= old(e.Repr) + decreases e.Decreases() + + invariant result == Seq.FoldLeft(f, init, e.enumerated) + { + // TODO: Will the foreach loop sugar support this? + // May at least need to use old@