From 2f6ef128005fb33af464759052dfa6b54128de99 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 9 Sep 2025 13:32:09 -0700 Subject: [PATCH 1/6] First cut --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 48 ++++++++++++++++- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 51 ++++++++++++++++--- 2 files changed, 89 insertions(+), 10 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index 209e5d0e08f..1f5e9900d1c 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -159,6 +159,11 @@ abstract module {:options "/functionSyntax:4"} Dafny { ensures fresh(ret.Repr) ensures ret.Length() == length + static method {:axiom} {:extern} MakeWithPrototype(length: size_t, prototype: ImmutableArray) returns (ret: NativeArray) + ensures ret.Valid() + ensures fresh(ret.Repr) + ensures ret.Length() == length + static method {:axiom} {:extern} MakeWithInit(length: size_t, initFn: size_t -> T) returns (ret: NativeArray) ensures ret.Valid() ensures fresh(ret.Repr) @@ -240,6 +245,17 @@ abstract module {:options "/functionSyntax:4"} Dafny { Repr := {this} + storage.Repr; } + constructor WithPrototype(length: size_t, prototype: ImmutableArray) + ensures Valid() + ensures Value() == [] + ensures fresh(Repr) + { + var storage := NativeArray.MakeWithPrototype(length, prototype); + this.storage := storage; + size := 0; + Repr := {this} + storage.Repr; + } + ghost function Value(): seq requires Valid() reads this, Repr @@ -297,8 +313,8 @@ abstract module {:options "/functionSyntax:4"} Dafny { newCapacity := Max(newCapacity, storage.Length() * TWO_SIZE); } - var newStorage := NativeArray.Make(newCapacity); var values := storage.Freeze(size); + var newStorage := NativeArray.MakeWithPrototype(newCapacity, values); newStorage.UpdateSubarray(0, values); storage := newStorage; @@ -599,11 +615,23 @@ abstract module {:options "/functionSyntax:4"} Dafny { var c := new ConcatSequence(left', right'); ret := new LazySequence(c); } + + // TODO: clean up + method PrototypeArray() returns (ret: ImmutableArray) + requires Valid() + decreases NodeCount, 1 } class ArraySequence extends Sequence { const values: ImmutableArray + method PrototypeArray() returns (ret: ImmutableArray) + requires Valid() + decreases NodeCount, 1 + { + return values; + } + ghost predicate Valid() decreases NodeCount, 0 ensures Valid() ==> 0 < NodeCount @@ -653,6 +681,13 @@ abstract module {:options "/functionSyntax:4"} Dafny { const right: Sequence const length: size_t + method PrototypeArray() returns (ret: ImmutableArray) + requires Valid() + decreases NodeCount, 1 + { + ret := left.PrototypeArray(); + } + ghost predicate Valid() decreases NodeCount, 0 ensures Valid() ==> 0 < NodeCount @@ -702,7 +737,8 @@ abstract module {:options "/functionSyntax:4"} Dafny { ensures ret.Length() == Cardinality() ensures ret.values == Value() { - var builder := new Vector(length); + var prototype := PrototypeArray(); + var builder := new Vector.WithPrototype(length, prototype); var stack := new Vector>(TEN_SIZE); AppendOptimized(builder, this, stack); ret := builder.Freeze(); @@ -814,6 +850,14 @@ abstract module {:options "/functionSyntax:4"} Dafny { const box: AtomicBox> const length: size_t + method PrototypeArray() returns (ret: ImmutableArray) + requires Valid() + decreases NodeCount, 1 + { + var expr : Sequence := box.Get(); + ret := expr.PrototypeArray(); + } + ghost predicate Valid() decreases NodeCount, 0 ensures Valid() ==> 0 < NodeCount diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index 465992abc4d..1076046a6d9 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -742,11 +742,8 @@ type GoNativeArray struct { underlying Array } -func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { - underlying := &arrayStruct{ - contents: make([]interface{}, length), - dims: []int{int(length)}, - } +func (CompanionStruct_NativeArray_) Make(length uint32, prototype NativeArray) NativeArray { + underlying := prototype.(GoNativeArray).underlying.arrayNewOfSameType(int(length)) return GoNativeArray{underlying: underlying} } @@ -806,6 +803,7 @@ type Array interface { anySlice(lo, hi Int) []interface{} arrayCopy() Array arrayEqualUpTo(other Array, index int) bool + arrayNewOfSameType(length int) Array // specializations ArrayGet1Byte(index int) byte ArraySet1Byte(value byte, index int) @@ -953,6 +951,7 @@ func NewArrayFromExample(example interface{}, init interface{}, dims ...Int) Arr arr[i] = init } } + return &arrayStruct{ contents: arr, dims: intDims, @@ -1007,7 +1006,7 @@ func newArrayWithValues(values ...interface{}) Array { } } -// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. +// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. // It is currently only used internally, by CompanionStruct_NativeArray_.MakeWithInit. // It could potentially be used in the translation of Dafny array instantiations with initializing lambdas, // but that is currently rewritten by the single-pass compiler instead. @@ -1119,7 +1118,7 @@ func (_this arrayStruct) arrayCopy() Array { copy(newDims, _this.dims) return &arrayStruct{ contents: newContents, - dims: newDims, + dims: newDims, } } @@ -1129,6 +1128,15 @@ func (_this arrayStruct) arrayEqualUpTo(other Array, index int) bool { return defaultArrayEqualUpTo(_this, other, uint32(index)) } +func (_this arrayStruct) arrayNewOfSameType(length int) Array { + conents := make([]interface{}, length) + dims := []int{length} + return &arrayStruct{ + contents: conents, + dims: dims, + } +} + func (_this arrayStruct) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1244,6 +1252,15 @@ func (_this arrayForByte) arrayEqualUpTo(other Array, index int) bool { } } +func (_this arrayForByte) arrayNewOfSameType(length int) Array { + conents := make([]byte, length) + dims := []int{length} + return &arrayForByte{ + contents: conents, + dims: dims, + } +} + func (_this arrayForByte) ArrayGet1Byte(index int) byte { return _this.contents[index] } @@ -1361,6 +1378,15 @@ func (_this arrayForChar) arrayEqualUpTo(other Array, index int) bool { } } +func (_this arrayForChar) arrayNewOfSameType(length int) Array { + conents := make([]Char, length) + dims := []int{length} + return &arrayForChar{ + contents: conents, + dims: dims, + } +} + func (_this arrayForChar) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1464,7 +1490,7 @@ func (_this arrayForCodePoint) arrayCopy() Array { return &arrayForCodePoint{ contents: newContents, // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: _this.dims, } } @@ -1477,6 +1503,15 @@ func (_this arrayForCodePoint) arrayEqualUpTo(other Array, index int) bool { } } +func (_this arrayForCodePoint) arrayNewOfSameType(length int) Array { + conents := make([]CodePoint, length) + dims := []int{length} + return &arrayForCodePoint{ + contents: conents, + dims: dims, + } +} + func (_this arrayForCodePoint) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } From c690e808f8cfd9e94f618579265fa1bb72275903 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 9 Sep 2025 13:36:05 -0700 Subject: [PATCH 2/6] Fix --- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 10 +- .../dafny/dafnyFromDafny.go | 110 +++++++++++++----- 2 files changed, 92 insertions(+), 28 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index 1076046a6d9..a85cf1a33a3 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -742,7 +742,15 @@ type GoNativeArray struct { underlying Array } -func (CompanionStruct_NativeArray_) Make(length uint32, prototype NativeArray) NativeArray { +func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { + underlying := &arrayStruct{ + contents: make([]interface{}, length), + dims: []int{int(length)}, + } + return GoNativeArray{underlying: underlying} +} + +func (CompanionStruct_NativeArray_) MakeWithPrototype(length uint32, prototype ImmutableArray) NativeArray { underlying := prototype.(GoNativeArray).underlying.arrayNewOfSameType(int(length)) return GoNativeArray{underlying: underlying} } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go index a64613285ae..4ff58266d9e 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go @@ -88,7 +88,7 @@ TAIL_CALL_START: _ = _0_concat _0_concat = e.(*ConcatSequence) if !(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE())) { - panic("dafnyRuntime.dfy(754,6): " + (SeqOfString("expectation violation")).String()) + panic("dafnyRuntime.dfy(790,6): " + (SeqOfString("expectation violation")).String()) } (stack).AddLast((_0_concat).Right()) var _in0 *Vector = builder @@ -150,7 +150,7 @@ TAIL_CALL_START: } } else { if !(false) { - panic("dafnyRuntime.dfy(777,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) + panic("dafnyRuntime.dfy(813,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) } } } @@ -192,6 +192,7 @@ type Sequence interface { ToArray() ImmutableArray Elements() Sequence UniqueElements() Set + PrototypeArray() ImmutableArray } func (_static *CompanionStruct_Sequence_) SetString(_this Sequence) Sequence { @@ -386,7 +387,7 @@ func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Seque var ret Sequence = (Sequence)(nil) _ = ret if !(Companion_Default___.SizeAdditionInRange((left).Cardinality(), (right).Cardinality())) { - panic("dafnyRuntime.dfy(582,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) + panic("dafnyRuntime.dfy(598,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) } var _0_left_k Sequence _ = _0_left_k @@ -759,6 +760,18 @@ func (_this *Vector) Ctor__(length uint32) { (_this).Size = uint32(0) } } +func (_this *Vector) WithPrototype(length uint32, prototype ImmutableArray) { + { + var _0_storage NativeArray + _ = _0_storage + var _out0 NativeArray + _ = _out0 + _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithPrototype(length, prototype)) + _0_storage = Companion_NativeArray_.CastTo_(_out0) + (_this).Storage = _0_storage + (_this).Size = uint32(0) + } +} func (_this *Vector) Select(index uint32) interface{} { { return (_this.Storage).Select(index) @@ -796,20 +809,20 @@ func (_this *Vector) EnsureCapacity(newMinCapacity uint32) { if ((_this.Storage).Length()) <= ((Companion_Default___.SIZE__T__MAX()) / (Companion_Default___.TWO__SIZE())) { _0_newCapacity = (_this).Max(_0_newCapacity, ((_this.Storage).Length())*(Companion_Default___.TWO__SIZE())) } - var _1_newStorage NativeArray - _ = _1_newStorage - var _out0 NativeArray + var _1_values ImmutableArray + _ = _1_values + var _out0 ImmutableArray _ = _out0 - _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Make(_0_newCapacity)) - _1_newStorage = Companion_NativeArray_.CastTo_(_out0) - var _2_values ImmutableArray - _ = _2_values - var _out1 ImmutableArray + _out0 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) + _1_values = Companion_ImmutableArray_.CastTo_(_out0) + var _2_newStorage NativeArray + _ = _2_newStorage + var _out1 NativeArray _ = _out1 - _out1 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) - _2_values = Companion_ImmutableArray_.CastTo_(_out1) - (_1_newStorage).UpdateSubarray(uint32(0), _2_values) - (_this).Storage = _1_newStorage + _out1 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithPrototype(_0_newCapacity, _1_values)) + _2_newStorage = Companion_NativeArray_.CastTo_(_out1) + (_2_newStorage).UpdateSubarray(uint32(0), _1_values) + (_this).Storage = _2_newStorage } } func (_this *Vector) RemoveLast() interface{} { @@ -947,6 +960,15 @@ func (_this *ArraySequence) Take(hi uint32) Sequence { _out1 = Companion_Sequence_.Take(_this, hi) return _out1 } +func (_this *ArraySequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + ret = (_this).Values() + return ret + return ret + } +} func (_this *ArraySequence) Ctor__(value ImmutableArray, isString bool) { { (_this)._values = value @@ -1059,6 +1081,17 @@ func (_this *ConcatSequence) Take(hi uint32) Sequence { _out2 = Companion_Sequence_.Take(_this, hi) return _out2 } +func (_this *ConcatSequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_(((_this).Left()).PrototypeArray()) + ret = Companion_ImmutableArray_.CastTo_(_out0) + return ret + } +} func (_this *ConcatSequence) Ctor__(left Sequence, right Sequence) { { (_this)._left = left @@ -1076,23 +1109,29 @@ func (_this *ConcatSequence) ToArray() ImmutableArray { { var ret ImmutableArray = (ImmutableArray)(nil) _ = ret - var _0_builder *Vector - _ = _0_builder + var _0_prototype ImmutableArray + _ = _0_prototype + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_((_this).PrototypeArray()) + _0_prototype = Companion_ImmutableArray_.CastTo_(_out0) + var _1_builder *Vector + _ = _1_builder var _nw0 *Vector = New_Vector_() _ = _nw0 - _nw0.Ctor__((_this).Length()) - _0_builder = _nw0 - var _1_stack *Vector - _ = _1_stack + _nw0.WithPrototype((_this).Length(), _0_prototype) + _1_builder = _nw0 + var _2_stack *Vector + _ = _2_stack var _nw1 *Vector = New_Vector_() _ = _nw1 _nw1.Ctor__(Companion_Default___.TEN__SIZE()) - _1_stack = _nw1 - Companion_Default___.AppendOptimized(_0_builder, _this, _1_stack) - var _out0 ImmutableArray - _ = _out0 - _out0 = Companion_ImmutableArray_.CastTo_((_0_builder).Freeze()) - ret = Companion_ImmutableArray_.CastTo_(_out0) + _2_stack = _nw1 + Companion_Default___.AppendOptimized(_1_builder, _this, _2_stack) + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_1_builder).Freeze()) + ret = Companion_ImmutableArray_.CastTo_(_out1) return ret } } @@ -1196,6 +1235,23 @@ func (_this *LazySequence) Take(hi uint32) Sequence { _out3 = Companion_Sequence_.Take(_this, hi) return _out3 } +func (_this *LazySequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _0_expr Sequence + _ = _0_expr + var _out0 interface{} + _ = _out0 + _out0 = ((_this).Box()).Get() + _0_expr = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_0_expr).PrototypeArray()) + ret = Companion_ImmutableArray_.CastTo_(_out1) + return ret + } +} func (_this *LazySequence) Ctor__(wrapped Sequence) { { var _0_box AtomicBox From 93c4e4341340a0a0410be93f7f9d0ba4fd87af6a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 10 Sep 2025 07:42:52 -0700 Subject: [PATCH 3/6] Apply to old runtime as well --- .../DafnyRuntimeGo/dafny/dafny.go | 49 +++++++- .../DafnyRuntimeGo/dafny/dafnyFromDafny.go | 110 +++++++++++++----- 2 files changed, 129 insertions(+), 30 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index 465992abc4d..a85cf1a33a3 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -750,6 +750,11 @@ func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { return GoNativeArray{underlying: underlying} } +func (CompanionStruct_NativeArray_) MakeWithPrototype(length uint32, prototype ImmutableArray) NativeArray { + underlying := prototype.(GoNativeArray).underlying.arrayNewOfSameType(int(length)) + return GoNativeArray{underlying: underlying} +} + func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) NativeArray { underlying := newArrayWithInitFn(init, int(length)) return GoNativeArray{underlying: underlying} @@ -806,6 +811,7 @@ type Array interface { anySlice(lo, hi Int) []interface{} arrayCopy() Array arrayEqualUpTo(other Array, index int) bool + arrayNewOfSameType(length int) Array // specializations ArrayGet1Byte(index int) byte ArraySet1Byte(value byte, index int) @@ -953,6 +959,7 @@ func NewArrayFromExample(example interface{}, init interface{}, dims ...Int) Arr arr[i] = init } } + return &arrayStruct{ contents: arr, dims: intDims, @@ -1007,7 +1014,7 @@ func newArrayWithValues(values ...interface{}) Array { } } -// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. +// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. // It is currently only used internally, by CompanionStruct_NativeArray_.MakeWithInit. // It could potentially be used in the translation of Dafny array instantiations with initializing lambdas, // but that is currently rewritten by the single-pass compiler instead. @@ -1119,7 +1126,7 @@ func (_this arrayStruct) arrayCopy() Array { copy(newDims, _this.dims) return &arrayStruct{ contents: newContents, - dims: newDims, + dims: newDims, } } @@ -1129,6 +1136,15 @@ func (_this arrayStruct) arrayEqualUpTo(other Array, index int) bool { return defaultArrayEqualUpTo(_this, other, uint32(index)) } +func (_this arrayStruct) arrayNewOfSameType(length int) Array { + conents := make([]interface{}, length) + dims := []int{length} + return &arrayStruct{ + contents: conents, + dims: dims, + } +} + func (_this arrayStruct) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1244,6 +1260,15 @@ func (_this arrayForByte) arrayEqualUpTo(other Array, index int) bool { } } +func (_this arrayForByte) arrayNewOfSameType(length int) Array { + conents := make([]byte, length) + dims := []int{length} + return &arrayForByte{ + contents: conents, + dims: dims, + } +} + func (_this arrayForByte) ArrayGet1Byte(index int) byte { return _this.contents[index] } @@ -1361,6 +1386,15 @@ func (_this arrayForChar) arrayEqualUpTo(other Array, index int) bool { } } +func (_this arrayForChar) arrayNewOfSameType(length int) Array { + conents := make([]Char, length) + dims := []int{length} + return &arrayForChar{ + contents: conents, + dims: dims, + } +} + func (_this arrayForChar) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1464,7 +1498,7 @@ func (_this arrayForCodePoint) arrayCopy() Array { return &arrayForCodePoint{ contents: newContents, // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: _this.dims, } } @@ -1477,6 +1511,15 @@ func (_this arrayForCodePoint) arrayEqualUpTo(other Array, index int) bool { } } +func (_this arrayForCodePoint) arrayNewOfSameType(length int) Array { + conents := make([]CodePoint, length) + dims := []int{length} + return &arrayForCodePoint{ + contents: conents, + dims: dims, + } +} + func (_this arrayForCodePoint) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go index a64613285ae..4ff58266d9e 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go @@ -88,7 +88,7 @@ TAIL_CALL_START: _ = _0_concat _0_concat = e.(*ConcatSequence) if !(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE())) { - panic("dafnyRuntime.dfy(754,6): " + (SeqOfString("expectation violation")).String()) + panic("dafnyRuntime.dfy(790,6): " + (SeqOfString("expectation violation")).String()) } (stack).AddLast((_0_concat).Right()) var _in0 *Vector = builder @@ -150,7 +150,7 @@ TAIL_CALL_START: } } else { if !(false) { - panic("dafnyRuntime.dfy(777,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) + panic("dafnyRuntime.dfy(813,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) } } } @@ -192,6 +192,7 @@ type Sequence interface { ToArray() ImmutableArray Elements() Sequence UniqueElements() Set + PrototypeArray() ImmutableArray } func (_static *CompanionStruct_Sequence_) SetString(_this Sequence) Sequence { @@ -386,7 +387,7 @@ func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Seque var ret Sequence = (Sequence)(nil) _ = ret if !(Companion_Default___.SizeAdditionInRange((left).Cardinality(), (right).Cardinality())) { - panic("dafnyRuntime.dfy(582,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) + panic("dafnyRuntime.dfy(598,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) } var _0_left_k Sequence _ = _0_left_k @@ -759,6 +760,18 @@ func (_this *Vector) Ctor__(length uint32) { (_this).Size = uint32(0) } } +func (_this *Vector) WithPrototype(length uint32, prototype ImmutableArray) { + { + var _0_storage NativeArray + _ = _0_storage + var _out0 NativeArray + _ = _out0 + _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithPrototype(length, prototype)) + _0_storage = Companion_NativeArray_.CastTo_(_out0) + (_this).Storage = _0_storage + (_this).Size = uint32(0) + } +} func (_this *Vector) Select(index uint32) interface{} { { return (_this.Storage).Select(index) @@ -796,20 +809,20 @@ func (_this *Vector) EnsureCapacity(newMinCapacity uint32) { if ((_this.Storage).Length()) <= ((Companion_Default___.SIZE__T__MAX()) / (Companion_Default___.TWO__SIZE())) { _0_newCapacity = (_this).Max(_0_newCapacity, ((_this.Storage).Length())*(Companion_Default___.TWO__SIZE())) } - var _1_newStorage NativeArray - _ = _1_newStorage - var _out0 NativeArray + var _1_values ImmutableArray + _ = _1_values + var _out0 ImmutableArray _ = _out0 - _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Make(_0_newCapacity)) - _1_newStorage = Companion_NativeArray_.CastTo_(_out0) - var _2_values ImmutableArray - _ = _2_values - var _out1 ImmutableArray + _out0 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) + _1_values = Companion_ImmutableArray_.CastTo_(_out0) + var _2_newStorage NativeArray + _ = _2_newStorage + var _out1 NativeArray _ = _out1 - _out1 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) - _2_values = Companion_ImmutableArray_.CastTo_(_out1) - (_1_newStorage).UpdateSubarray(uint32(0), _2_values) - (_this).Storage = _1_newStorage + _out1 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithPrototype(_0_newCapacity, _1_values)) + _2_newStorage = Companion_NativeArray_.CastTo_(_out1) + (_2_newStorage).UpdateSubarray(uint32(0), _1_values) + (_this).Storage = _2_newStorage } } func (_this *Vector) RemoveLast() interface{} { @@ -947,6 +960,15 @@ func (_this *ArraySequence) Take(hi uint32) Sequence { _out1 = Companion_Sequence_.Take(_this, hi) return _out1 } +func (_this *ArraySequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + ret = (_this).Values() + return ret + return ret + } +} func (_this *ArraySequence) Ctor__(value ImmutableArray, isString bool) { { (_this)._values = value @@ -1059,6 +1081,17 @@ func (_this *ConcatSequence) Take(hi uint32) Sequence { _out2 = Companion_Sequence_.Take(_this, hi) return _out2 } +func (_this *ConcatSequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_(((_this).Left()).PrototypeArray()) + ret = Companion_ImmutableArray_.CastTo_(_out0) + return ret + } +} func (_this *ConcatSequence) Ctor__(left Sequence, right Sequence) { { (_this)._left = left @@ -1076,23 +1109,29 @@ func (_this *ConcatSequence) ToArray() ImmutableArray { { var ret ImmutableArray = (ImmutableArray)(nil) _ = ret - var _0_builder *Vector - _ = _0_builder + var _0_prototype ImmutableArray + _ = _0_prototype + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_((_this).PrototypeArray()) + _0_prototype = Companion_ImmutableArray_.CastTo_(_out0) + var _1_builder *Vector + _ = _1_builder var _nw0 *Vector = New_Vector_() _ = _nw0 - _nw0.Ctor__((_this).Length()) - _0_builder = _nw0 - var _1_stack *Vector - _ = _1_stack + _nw0.WithPrototype((_this).Length(), _0_prototype) + _1_builder = _nw0 + var _2_stack *Vector + _ = _2_stack var _nw1 *Vector = New_Vector_() _ = _nw1 _nw1.Ctor__(Companion_Default___.TEN__SIZE()) - _1_stack = _nw1 - Companion_Default___.AppendOptimized(_0_builder, _this, _1_stack) - var _out0 ImmutableArray - _ = _out0 - _out0 = Companion_ImmutableArray_.CastTo_((_0_builder).Freeze()) - ret = Companion_ImmutableArray_.CastTo_(_out0) + _2_stack = _nw1 + Companion_Default___.AppendOptimized(_1_builder, _this, _2_stack) + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_1_builder).Freeze()) + ret = Companion_ImmutableArray_.CastTo_(_out1) return ret } } @@ -1196,6 +1235,23 @@ func (_this *LazySequence) Take(hi uint32) Sequence { _out3 = Companion_Sequence_.Take(_this, hi) return _out3 } +func (_this *LazySequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _0_expr Sequence + _ = _0_expr + var _out0 interface{} + _ = _out0 + _out0 = ((_this).Box()).Get() + _0_expr = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_0_expr).PrototypeArray()) + ret = Companion_ImmutableArray_.CastTo_(_out1) + return ret + } +} func (_this *LazySequence) Ctor__(wrapped Sequence) { { var _0_box AtomicBox From 48709560dee52b51866298a7ea6baa90229c3989 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 10 Sep 2025 09:31:25 -0700 Subject: [PATCH 4/6] Formatting --- Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index 1f5e9900d1c..a70d7f87f03 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -625,7 +625,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { class ArraySequence extends Sequence { const values: ImmutableArray - method PrototypeArray() returns (ret: ImmutableArray) + method PrototypeArray() returns (ret: ImmutableArray) requires Valid() decreases NodeCount, 1 { @@ -681,7 +681,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { const right: Sequence const length: size_t - method PrototypeArray() returns (ret: ImmutableArray) + method PrototypeArray() returns (ret: ImmutableArray) requires Valid() decreases NodeCount, 1 { From 95ba91e72226c5c591a6f3572f7fa3d3a0ee6a15 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 10 Sep 2025 10:49:46 -0700 Subject: [PATCH 5/6] Comments --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 25 +++++++++++++++---- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index a70d7f87f03..279c8ff7c0b 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -245,6 +245,9 @@ abstract module {:options "/functionSyntax:4"} Dafny { Repr := {this} + storage.Repr; } + // Note it is important to use this constructor + // if T may be compiled to a primitive type we want to avoid boxing, + // such as bytes or characters! constructor WithPrototype(length: size_t, prototype: ImmutableArray) ensures Valid() ensures Value() == [] @@ -420,6 +423,21 @@ abstract module {:options "/functionSyntax:4"} Dafny { decreases NodeCount, 2 ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality() + // Returns an array of the same element type as this sequence. + // Used to ensure when we create more arrays of T elements + // that we optimize for common types like bytes and characters, + // even though in several Dafny backends we don't have enough type information + // at runtime from Dafny itself. + // TypeDescriptors would be the more general solution, + // but they are not present where we need them + // in most backends. + // + // Note this is very similar to the DafnySequence.newCopier(int length) + // method in the Java runtime. + method PrototypeArray() returns (ret: ImmutableArray) + requires Valid() + decreases NodeCount, 1 + method Select(index: size_t) returns (ret: T) requires Valid() requires index < Cardinality() @@ -615,11 +633,6 @@ abstract module {:options "/functionSyntax:4"} Dafny { var c := new ConcatSequence(left', right'); ret := new LazySequence(c); } - - // TODO: clean up - method PrototypeArray() returns (ret: ImmutableArray) - requires Valid() - decreases NodeCount, 1 } class ArraySequence extends Sequence { @@ -685,6 +698,8 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires Valid() decreases NodeCount, 1 { + // This is arbitrary but should work well for the majority of cases, + // and is consistent with how the Java runtime currently handles the same problem. ret := left.PrototypeArray(); } From eb34ef2ee83b5ccc41a5f179afdd72e9b54864e6 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 10 Sep 2025 12:08:48 -0700 Subject: [PATCH 6/6] make update-from-dafny --- .../DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go | 8 ++++---- .../DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go index 4ff58266d9e..463fb517b45 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafnyFromDafny.go @@ -88,7 +88,7 @@ TAIL_CALL_START: _ = _0_concat _0_concat = e.(*ConcatSequence) if !(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE())) { - panic("dafnyRuntime.dfy(790,6): " + (SeqOfString("expectation violation")).String()) + panic("dafnyRuntime.dfy(805,6): " + (SeqOfString("expectation violation")).String()) } (stack).AddLast((_0_concat).Right()) var _in0 *Vector = builder @@ -150,7 +150,7 @@ TAIL_CALL_START: } } else { if !(false) { - panic("dafnyRuntime.dfy(813,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) + panic("dafnyRuntime.dfy(828,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) } } } @@ -185,6 +185,7 @@ type Sequence interface { IsString() bool IsString_set_(value bool) Cardinality() uint32 + PrototypeArray() ImmutableArray Select(index uint32) interface{} Drop(lo uint32) Sequence Take(hi uint32) Sequence @@ -192,7 +193,6 @@ type Sequence interface { ToArray() ImmutableArray Elements() Sequence UniqueElements() Set - PrototypeArray() ImmutableArray } func (_static *CompanionStruct_Sequence_) SetString(_this Sequence) Sequence { @@ -387,7 +387,7 @@ func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Seque var ret Sequence = (Sequence)(nil) _ = ret if !(Companion_Default___.SizeAdditionInRange((left).Cardinality(), (right).Cardinality())) { - panic("dafnyRuntime.dfy(598,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) + panic("dafnyRuntime.dfy(616,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) } var _0_left_k Sequence _ = _0_left_k diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go index 4ff58266d9e..463fb517b45 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go @@ -88,7 +88,7 @@ TAIL_CALL_START: _ = _0_concat _0_concat = e.(*ConcatSequence) if !(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE())) { - panic("dafnyRuntime.dfy(790,6): " + (SeqOfString("expectation violation")).String()) + panic("dafnyRuntime.dfy(805,6): " + (SeqOfString("expectation violation")).String()) } (stack).AddLast((_0_concat).Right()) var _in0 *Vector = builder @@ -150,7 +150,7 @@ TAIL_CALL_START: } } else { if !(false) { - panic("dafnyRuntime.dfy(813,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) + panic("dafnyRuntime.dfy(828,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) } } } @@ -185,6 +185,7 @@ type Sequence interface { IsString() bool IsString_set_(value bool) Cardinality() uint32 + PrototypeArray() ImmutableArray Select(index uint32) interface{} Drop(lo uint32) Sequence Take(hi uint32) Sequence @@ -192,7 +193,6 @@ type Sequence interface { ToArray() ImmutableArray Elements() Sequence UniqueElements() Set - PrototypeArray() ImmutableArray } func (_static *CompanionStruct_Sequence_) SetString(_this Sequence) Sequence { @@ -387,7 +387,7 @@ func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Seque var ret Sequence = (Sequence)(nil) _ = ret if !(Companion_Default___.SizeAdditionInRange((left).Cardinality(), (right).Cardinality())) { - panic("dafnyRuntime.dfy(598,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) + panic("dafnyRuntime.dfy(616,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) } var _0_left_k Sequence _ = _0_left_k