From a92cab6448b25c2238007bbe6d9baad2a37d483f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 18 Nov 2024 12:30:31 +0100 Subject: [PATCH 1/4] Finished SubsequenceView --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 202 +++++++++++++----- .../DafnyRuntimeDafny/src/dfyconfig.toml | 2 + 2 files changed, 154 insertions(+), 50 deletions(-) create mode 100644 Source/DafnyRuntime/DafnyRuntimeDafny/src/dfyconfig.toml diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index 75d93f5348a..b030283a500 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -389,34 +389,34 @@ abstract module {:options "/functionSyntax:4"} Dafny { // Total class instances in the tree. // Used in decreases clauses. - ghost const NodeCount: nat + ghost var Repr: set ghost predicate Valid() - decreases NodeCount, 0 - ensures Valid() ==> 0 < NodeCount + reads this, Repr + decreases |Repr|, 0 + ensures Valid() ==> 0 < |Repr| function Cardinality(): size_t requires Valid() - decreases NodeCount, 1 + reads this, Repr + decreases |Repr|, 1 ghost function Value(): seq + reads this, Repr requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() method Select(index: size_t) returns (ret: T) + decreases |Repr| requires Valid() requires index < Cardinality() ensures ret == Value()[index] - { - var a := ToArray(); - return a.Select(index); - } method Drop(lo: size_t) returns (ret: Sequence) requires Valid() requires lo <= Cardinality() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures ret.Valid() ensures ret.Value() == Value()[lo..] { @@ -426,7 +426,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { method Take(hi: size_t) returns (ret: Sequence) requires Valid() requires hi <= Cardinality() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures ret.Valid() ensures ret.Value() == Value()[..hi] { @@ -436,21 +436,16 @@ abstract module {:options "/functionSyntax:4"} Dafny { method Subsequence(lo: size_t, hi: size_t) returns (ret: Sequence) requires Valid() requires lo <= hi <= Cardinality() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures ret.Valid() ensures ret.Value() == Value()[lo..hi] { - // Probably not worth pushing this into a ToArray(lo, hi) overload - // to optimize further, because one x[lo..hi] call is very likely - // to be followed by several others anyway. - var a := ToArray(); - var subarray := a.Subarray(lo, hi); - ret := new ArraySequence(subarray); + ret := new SubsequenceView(this, lo, hi); } method ToArray() returns (ret: ImmutableArray) requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures Valid() ensures ret.Valid() ensures ret.Length() == Cardinality() @@ -613,15 +608,106 @@ abstract module {:options "/functionSyntax:4"} Dafny { } } + class SubsequenceView extends Sequence { + var origin: Sequence + var lo: size_t + var hi: size_t + + constructor(origin: Sequence, lo: size_t, hi: size_t) + { + this.origin := origin; + this.lo := lo; + this.hi := hi; + } + + ghost function Value(): seq + reads this, Repr + requires Valid() + decreases |Repr|, 2 + ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() + { + var r := origin.Value()[lo..hi]; + assert |r| == hi - lo; + assert |r| as size_t == hi - lo; + assert |r| as size_t == Cardinality(); // Why do I need these steps? Seems too simple + r + } + + ghost predicate Valid() + reads this, Repr + decreases |Repr|, 0 + ensures Valid() ==> 0 < |Repr| + { + origin in Repr && + origin.Repr < Repr && + |origin.Repr| < |Repr| && // why is this not implied by the previous line? + hi >= lo && + origin.Valid() && hi <= origin.Cardinality() + } + + method Select(index: size_t) returns (ret: T) + decreases |Repr| + requires Valid() + requires index < Cardinality() + ensures ret == Value()[index] + { + ret := origin.Select(index + lo); + } + + function Cardinality(): size_t + requires Valid() + reads this, Repr + decreases |Repr|, 1 + { + hi - lo + } + + method ToArray() returns (ret: ImmutableArray) + requires Valid() + decreases |Repr|, 2 + ensures Valid() + ensures ret.Valid() + ensures ret.Length() == Cardinality() + ensures ret.values == Value() + { + var size := Cardinality(); + var builder := NativeArray.Make(size); + var i := 0; + while(i != size) + invariant builder.Valid() + invariant builder.Length() == size + invariant i <= size + invariant i <= builder.Length() + invariant fresh(builder.Repr) + invariant forall j: size_t :: j < i ==> builder.values[j].Set? + && builder.values[j].value == Value()[j] + { + var value := Select(i); + builder.Update(i, value); + i := i + 1; + } + + // for i: size_t := 0 to Cardinality() + // invariant builder.Valid() + // invariant i < Cardinality() && i < builder.Length() + // invariant fresh(builder.Repr) + // { + // var value := Select(i); + // builder.Update(i, value); + // } + ret := builder.Freeze(size); + } + } + class ArraySequence extends Sequence { const values: ImmutableArray ghost predicate Valid() - decreases NodeCount, 0 - ensures Valid() ==> 0 < NodeCount + decreases |Repr|, 0 + ensures Valid() ==> 0 < |Repr| { && values.Valid() - && NodeCount == 1 + && |Repr| == 1 } constructor(value: ImmutableArray, isString: bool := false) @@ -631,19 +717,24 @@ abstract module {:options "/functionSyntax:4"} Dafny { { this.values := value; this.isString := isString; - this.NodeCount := 1; + this.Repr := {this}; + } + + method Select(index: size_t) returns (ret: T) + { + } function Cardinality(): size_t requires Valid() - decreases NodeCount, 1 + decreases |Repr|, 1 { values.Length() } ghost function Value(): seq requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() { values.values @@ -651,7 +742,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { method ToArray() returns (ret: ImmutableArray) requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures ret.Valid() ensures ret.Length() == Cardinality() ensures ret.values == Value() @@ -666,10 +757,10 @@ abstract module {:options "/functionSyntax:4"} Dafny { const length: size_t ghost predicate Valid() - decreases NodeCount, 0 - ensures Valid() ==> 0 < NodeCount + decreases |Repr|, 0 + ensures Valid() ==> 0 < |Repr| { - && NodeCount == 1 + left.NodeCount + right.NodeCount + && Repr == {this} + left.Repr + right.Repr && left.Valid() && right.Valid() && left.Cardinality() as int + right.Cardinality() as int < SIZE_T_LIMIT as int @@ -687,19 +778,24 @@ abstract module {:options "/functionSyntax:4"} Dafny { this.right := right; this.length := left.Cardinality() + right.Cardinality(); this.isString := left.isString || right.isString; - this.NodeCount := 1 + left.NodeCount + right.NodeCount; + this.Repr := {this} + left.Repr + right.Repr; } + method Select(index: size_t) returns (ret: T) + { + + } + function Cardinality(): size_t requires Valid() - decreases NodeCount, 1 + decreases |Repr|, 1 { length } ghost function Value(): seq requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() { var ret := left.Value() + right.Value(); @@ -709,7 +805,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { method ToArray() returns (ret: ImmutableArray) requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures ret.Valid() ensures ret.Length() == Cardinality() ensures ret.values == Value() @@ -727,7 +823,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires builder.Valid() requires SizeAdditionInRange(builder.size, e.Cardinality()) modifies builder.Repr - decreases e.NodeCount + decreases |e.Repr| ensures builder.ValidAndDisjoint() ensures e.Valid() ensures builder.Value() == old(builder.Value()) + e.Value() @@ -754,7 +850,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires forall expr <- stack.Value() :: expr.Valid() requires builder.size as int + e.Cardinality() as int + CardinalitySum(stack.Value()) < SIZE_T_LIMIT modifies builder.Repr, stack.Repr - decreases e.NodeCount + NodeCountSum(stack.Value()) + decreases |e.Repr| + NodeCountSum(stack.Value()) ensures builder.Valid() ensures stack.Valid() ensures builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())) @@ -808,7 +904,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { 0 else var last := |s| - 1; - NodeCountSum(s[..last]) + s[last].NodeCount + NodeCountSum(s[..last]) + |s[last].Repr| } ghost function CardinalitySum(s: seq>): nat @@ -827,50 +923,56 @@ abstract module {:options "/functionSyntax:4"} Dafny { const length: size_t ghost predicate Valid() - decreases NodeCount, 0 - ensures Valid() ==> 0 < NodeCount + decreases |Repr|, 0 + ensures Valid() ==> 0 < |Repr| { - && 0 < NodeCount + && 0 < |Repr| && |value| < SIZE_T_LIMIT && length == |value| as size_t && box.Valid() && box.inv == (s: Sequence) => - && s.NodeCount < NodeCount + && |s.Repr| < |Repr| && s.Valid() && s.Value() == value } constructor(wrapped: Sequence) requires wrapped.Valid() - requires 1 <= wrapped.NodeCount + requires 1 <= |wrapped.Repr| ensures Valid() ensures Value() == wrapped.Value() { + this.box := box; + this.length := wrapped.Cardinality(); + this.value := value; + new; var value := wrapped.Value(); - var nodeCount := 1 + wrapped.NodeCount; + var tRepr := {this} + wrapped.Repr; var inv := (s: Sequence) => - && s.NodeCount < nodeCount + && |s.Repr| < |Repr| && s.Valid() && s.Value() == value; var box := AtomicBox.Make(inv, wrapped); - this.box := box; - this.length := wrapped.Cardinality(); this.isString := wrapped.isString; - this.value := value; - this.NodeCount := nodeCount; + this.Repr := tRepr; + } + + method Select(index: size_t) returns (ret: T) + { + } function Cardinality(): size_t requires Valid() - decreases NodeCount, 1 + decreases |Repr|, 1 { length } ghost function Value(): seq requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() { assert |value| as size_t == Cardinality(); @@ -879,7 +981,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { method ToArray() returns (ret: ImmutableArray) requires Valid() - decreases NodeCount, 2 + decreases |Repr|, 2 ensures ret.Valid() ensures ret.Length() == Cardinality() ensures ret.values == Value() diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dfyconfig.toml b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dfyconfig.toml new file mode 100644 index 00000000000..3008b21a509 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dfyconfig.toml @@ -0,0 +1,2 @@ +[options] +general-traits="legacy" \ No newline at end of file From 32043b4fd3ae754ada9d0970120e86fc70375f5a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 18 Nov 2024 16:11:24 +0100 Subject: [PATCH 2/4] Select implementations for Array and Concat sequence --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 120 +++++++++++++----- 1 file changed, 85 insertions(+), 35 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index b030283a500..d38722460c7 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -451,6 +451,48 @@ abstract module {:options "/functionSyntax:4"} Dafny { ensures ret.Length() == Cardinality() ensures ret.values == Value() + method ToArrayDefault() returns (ret: ImmutableArray) + requires Valid() + decreases |Repr|, 2 + ensures Valid() + ensures ret.Valid() + ensures ret.Length() == Cardinality() + ensures ret.values == Value() + { + var builder := new Vector(Cardinality()); + var stack := new Vector>(TEN_SIZE); + AppendOptimized(builder, this, stack); + ret := builder.Freeze(); + + // var size := Cardinality(); + // var builder := NativeArray.Make(size); + // var i := 0; + // while(i != size) + // invariant builder.Valid() + // invariant builder.Length() == size + // invariant i <= size + // invariant i <= builder.Length() + // invariant fresh(builder.Repr) + // invariant forall j: size_t :: j < i ==> + // builder.values[j].Set? + // && builder.values[j].value == Value()[j] + // { + // var value := Select(i); + // builder.Update(i, value); + // i := i + 1; + // } + + // for i: size_t := 0 to Cardinality() + // invariant builder.Valid() + // invariant i < Cardinality() && i < builder.Length() + // invariant fresh(builder.Repr) + // { + // var value := Select(i); + // builder.Update(i, value); + // } + // ret := builder.Freeze(size); + } + // We specifically DON'T yet implement a ToString() method because that // doesn't help much in practice. Most runtimes implement the conversion between // various Dafny types and their native string type, which we don't yet model here. @@ -573,7 +615,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { ensures ret.Valid() ensures ret.Value() == s.Value()[..i] + [t] + s.Value()[(i + 1)..] { - var a := s.ToArray(); + var a := s.ToArray(); // TODO Should remove var newValue := NativeArray.Copy(a); newValue.Update(i, t); var newValueFrozen := newValue.Freeze(newValue.Length()); @@ -604,7 +646,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { } var c := new ConcatSequence(left', right'); - ret := new LazySequence(c); + ret := new LazySequence(c); // TODO Why this wrapper? Ins't ConcatSequence already lazy? } } @@ -670,32 +712,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { ensures ret.Length() == Cardinality() ensures ret.values == Value() { - var size := Cardinality(); - var builder := NativeArray.Make(size); - var i := 0; - while(i != size) - invariant builder.Valid() - invariant builder.Length() == size - invariant i <= size - invariant i <= builder.Length() - invariant fresh(builder.Repr) - invariant forall j: size_t :: j < i ==> builder.values[j].Set? - && builder.values[j].value == Value()[j] - { - var value := Select(i); - builder.Update(i, value); - i := i + 1; - } - - // for i: size_t := 0 to Cardinality() - // invariant builder.Valid() - // invariant i < Cardinality() && i < builder.Length() - // invariant fresh(builder.Repr) - // { - // var value := Select(i); - // builder.Update(i, value); - // } - ret := builder.Freeze(size); + ret := ToArrayDefault(); } } @@ -703,6 +720,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { const values: ImmutableArray ghost predicate Valid() + reads this, Repr decreases |Repr|, 0 ensures Valid() ==> 0 < |Repr| { @@ -721,11 +739,16 @@ abstract module {:options "/functionSyntax:4"} Dafny { } method Select(index: size_t) returns (ret: T) + decreases |Repr| + requires Valid() + requires index < Cardinality() + ensures ret == Value()[index] { - + ret := values.Select(index); } function Cardinality(): size_t + reads this, Repr requires Valid() decreases |Repr|, 1 { @@ -733,6 +756,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { } ghost function Value(): seq + reads this, Repr requires Valid() decreases |Repr|, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() @@ -753,16 +777,24 @@ abstract module {:options "/functionSyntax:4"} Dafny { class ConcatSequence extends Sequence { const left: Sequence + const leftSize: size_t const right: Sequence const length: size_t ghost predicate Valid() + reads this, Repr decreases |Repr|, 0 ensures Valid() ==> 0 < |Repr| { - && Repr == {this} + left.Repr + right.Repr + && {this, left, right} <= Repr + && left.Repr !! right.Repr + && this !in left.Repr + && this !in right.Repr + && left.Repr < Repr && |left.Repr| < |Repr| // Do not undertand why second part is needed + && right.Repr < Repr && |right.Repr| < |Repr| // Do not undertand why second part is needed && left.Valid() && right.Valid() + && leftSize == left.Cardinality() && left.Cardinality() as int + right.Cardinality() as int < SIZE_T_LIMIT as int && length == left.Cardinality() + right.Cardinality() } @@ -770,23 +802,38 @@ abstract module {:options "/functionSyntax:4"} Dafny { constructor(left: Sequence, right: Sequence) requires left.Valid() requires right.Valid() + requires left in left.Repr + requires right in right.Repr + requires left.Repr !! right.Repr requires left.Cardinality() as int + right.Cardinality() as int < SIZE_T_LIMIT as int ensures Valid() ensures Value() == left.Value() + right.Value() { this.left := left; this.right := right; + this.leftSize := left.Cardinality(); this.length := left.Cardinality() + right.Cardinality(); this.isString := left.isString || right.isString; this.Repr := {this} + left.Repr + right.Repr; + new; + assert |this.Repr| == |left.Repr| + |right.Repr| + 1; } method Select(index: size_t) returns (ret: T) + decreases |Repr| + requires Valid() + requires index < Cardinality() + ensures ret == Value()[index] { - + if (index < left.Cardinality()) { + ret := left.Select(index); + } else { + ret := right.Select(index - leftSize); + } } function Cardinality(): size_t + reads this, Repr requires Valid() decreases |Repr|, 1 { @@ -794,6 +841,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { } ghost function Value(): seq + reads this, Repr requires Valid() decreases |Repr|, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() @@ -806,14 +854,12 @@ abstract module {:options "/functionSyntax:4"} Dafny { method ToArray() returns (ret: ImmutableArray) requires Valid() decreases |Repr|, 2 + ensures Valid() ensures ret.Valid() ensures ret.Length() == Cardinality() ensures ret.values == Value() { - var builder := new Vector(length); - var stack := new Vector>(TEN_SIZE); - AppendOptimized(builder, this, stack); - ret := builder.Freeze(); + ret := ToArrayDefault(); } } @@ -959,6 +1005,10 @@ abstract module {:options "/functionSyntax:4"} Dafny { } method Select(index: size_t) returns (ret: T) + decreases |Repr| + requires Valid() + requires index < Cardinality() + ensures ret == Value()[index] { } From 310bd15bb996bbdbfe4ddcd2bd12f3f6e11cc96c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 18 Nov 2024 16:12:29 +0100 Subject: [PATCH 3/4] Remove unused code --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 28 ------------------- 1 file changed, 28 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index d38722460c7..dd1cd579d7a 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -463,34 +463,6 @@ abstract module {:options "/functionSyntax:4"} Dafny { var stack := new Vector>(TEN_SIZE); AppendOptimized(builder, this, stack); ret := builder.Freeze(); - - // var size := Cardinality(); - // var builder := NativeArray.Make(size); - // var i := 0; - // while(i != size) - // invariant builder.Valid() - // invariant builder.Length() == size - // invariant i <= size - // invariant i <= builder.Length() - // invariant fresh(builder.Repr) - // invariant forall j: size_t :: j < i ==> - // builder.values[j].Set? - // && builder.values[j].value == Value()[j] - // { - // var value := Select(i); - // builder.Update(i, value); - // i := i + 1; - // } - - // for i: size_t := 0 to Cardinality() - // invariant builder.Valid() - // invariant i < Cardinality() && i < builder.Length() - // invariant fresh(builder.Repr) - // { - // var value := Select(i); - // builder.Update(i, value); - // } - // ret := builder.Freeze(size); } // We specifically DON'T yet implement a ToString() method because that From 0c4250e4b1c772078a9493425405a15eed2d1733 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 18 Nov 2024 16:53:04 +0100 Subject: [PATCH 4/4] Work on LazySequenceCopy --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 52 ++++++++++++------- 1 file changed, 34 insertions(+), 18 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index dd1cd579d7a..3521aa2accf 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -606,19 +606,19 @@ abstract module {:options "/functionSyntax:4"} Dafny { // Optimize away redundant lazy wrappers // (which will happen a lot with chained concatenations) var left' := left; - if (left is LazySequence) { - var lazyLeft := left as LazySequence; + if (left is LazySequenceCopy) { + var lazyLeft := left as LazySequenceCopy; left' := lazyLeft.box.Get(); } var right' := right; - if (right is LazySequence) { - var lazyRight := right as LazySequence; + if (right is LazySequenceCopy) { + var lazyRight := right as LazySequenceCopy; right' := lazyRight.box.Get(); } var c := new ConcatSequence(left', right'); - ret := new LazySequence(c); // TODO Why this wrapper? Ins't ConcatSequence already lazy? + ret := new LazySequenceCopy(c); } } @@ -850,8 +850,8 @@ abstract module {:options "/functionSyntax:4"} Dafny { var concat := e as ConcatSequence; AppendRecursive(builder, concat.left); AppendRecursive(builder, concat.right); - } else if e is LazySequence { - var lazy := e as LazySequence; + } else if e is LazySequenceCopy { + var lazy := e as LazySequenceCopy; var boxed := lazy.box.Get(); AppendRecursive(builder, boxed); } else { @@ -882,8 +882,9 @@ abstract module {:options "/functionSyntax:4"} Dafny { label L1: AppendOptimized(builder, concat.left, stack); assert builder.Value() == old@L1(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old@L1(stack.Value())); - } else if e is LazySequence { - var lazy := e as LazySequence; + } else if e is LazySequenceCopy { + // TODO should this trigger materializing the lazy sequence? After all it's reading all its elements + var lazy := e as LazySequenceCopy; var boxed := lazy.box.Get(); AppendOptimized(builder, boxed, stack); assert builder.Value() == old(builder.Value()) + boxed.Value() + ConcatValueOnStack(old(stack.Value())); @@ -935,12 +936,13 @@ abstract module {:options "/functionSyntax:4"} Dafny { CardinalitySum(s[..last]) + s[last].Cardinality() as nat } - class LazySequence extends Sequence { + class LazySequenceCopy extends Sequence { ghost const value: seq const box: AtomicBox> const length: size_t ghost predicate Valid() + reads this, Repr decreases |Repr|, 0 ensures Valid() ==> 0 < |Repr| { @@ -963,11 +965,12 @@ abstract module {:options "/functionSyntax:4"} Dafny { this.box := box; this.length := wrapped.Cardinality(); this.value := value; - new; + var value := wrapped.Value(); + new; var tRepr := {this} + wrapped.Repr; - var inv := (s: Sequence) => - && |s.Repr| < |Repr| + var inv := (s: Sequence) reads s, s.Repr, this, Repr => + // && |s.Repr| < |Repr| && s.Valid() && s.Value() == value; var box := AtomicBox.Make(inv, wrapped); @@ -982,7 +985,16 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires index < Cardinality() ensures ret == Value()[index] { - + // TODO we could count how often Select is called, and only copy the array of .Select is called 1/10th of the total size. + var expr := box.Get(); + if (expr is ArraySequence) { + ret := (expr as ArraySequence).Select(index); + } else { + var valuesArray := expr.ToArray(); + var arraySeq := new ArraySequence(valuesArray); + box.Put(arraySeq); + ret := arraySeq.Select(index); + } } function Cardinality(): size_t @@ -1009,10 +1021,14 @@ abstract module {:options "/functionSyntax:4"} Dafny { ensures ret.values == Value() { var expr := box.Get(); - ret := expr.ToArray(); - - var arraySeq := new ArraySequence(ret); - box.Put(arraySeq); + if (expr is ArraySequence) { + ret := (expr as ArraySequence).values; + } else { + var valuesArray := expr.ToArray(); + var arraySeq := new ArraySequence(valuesArray); + box.Put(arraySeq); + ret := valuesArray; + } } }