Skip to content

feat: Stop boxing byte/char/CodePoint sequences in Go #6353

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 14 commits into from
Sep 5, 2025
Merged

feat: Stop boxing byte/char/CodePoint sequences in Go #6353

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
99d7e5b
feat: Stop boxing byte sequences in Go
fabiomadge Aug 31, 2025
5670e52
review
fabiomadge Sep 3, 2025
79e645d
Merge branch 'master' into feat_go_optimized_byte_sequences
fabiomadge Sep 3, 2025
ed00827
Squashed commit of the following:
robin-aws Sep 4, 2025
a10a40e
Merge branch 'master' into feat_go_optimized_byte_sequences
robin-aws Sep 4, 2025
ec60bcf
Fix for loops
robin-aws Sep 4, 2025
81e9376
Merge branch 'feat_go_optimized_byte_sequences' of github.com:fabioma…
robin-aws Sep 4, 2025
5a42090
cleanup
robin-aws Sep 4, 2025
3b1e5a3
More cleanup
robin-aws Sep 4, 2025
f3c9137
Optimize ArrayRangeToSeq too
robin-aws Sep 4, 2025
362ea79
Fix ToByteArray
robin-aws Sep 4, 2025
5583957
Uncomment test
robin-aws Sep 4, 2025
7b97964
Change SeqFromArray back to not copy, address TODOs
robin-aws Sep 5, 2025
d5e7ee2
Typo
robin-aws Sep 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
134 changes: 104 additions & 30 deletions Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,15 +82,34 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc
return true
}

l := left.ToArray().(GoNativeArray).contents
r := right.ToArray().(GoNativeArray).contents
if IsEqualityComparable(l[0]) {
return slices.Equal(l[:index], r[:index])
} else {
for i := uint32(0); i < index; i++ {
if !AreEqual(l[i], r[i]) {
return false
leftArr, rightArr := left.ToArray(), right.ToArray()

// Fast path for ByteNativeArray
if l, ok := leftArr.(ByteNativeArray); ok {
if r, ok := rightArr.(ByteNativeArray); ok {
return slices.Equal(l.contents[:index], r.contents[:index])
}
}

// Fast path for GoNativeArray (preserve original optimization)
if l, ok := leftArr.(GoNativeArray); ok {
if r, ok := rightArr.(GoNativeArray); ok {
if IsEqualityComparable(l.contents[0]) {
return slices.Equal(l.contents[:index], r.contents[:index])
}
for i := uint32(0); i < index; i++ {
if !AreEqual(l.contents[i], r.contents[i]) {
return false
}
}
return true
}
}

// Generic fallback
for i := uint32(0); i < index; i++ {
if !AreEqual(leftArr.Select(i), rightArr.Select(i)) {
return false
}
}
return true
Expand Down Expand Up @@ -531,24 +550,28 @@ var EmptySeq = SeqOf()
// for the compiler to coerce the init function to a
// func (uint32) interface{}.
func SeqCreate(n uint32, init func(Int) interface{}) Sequence {
if seq, ok := tryByteSeqInit(n, init); ok {
return seq
}
return Companion_Sequence_.Create(n, func(index uint32) interface{} {
return init(IntOfUint32(index))
})
}

func SeqFromArray(contents []interface{}, isString bool) Sequence {
arr := GoNativeArray{
contents: contents,
if seq, ok := tryByteSeq(contents); ok && !isString {
return seq
}
result := New_ArraySequence_()
result.Ctor__(arr, isString)
result.Ctor__(GoNativeArray{contents: contents}, isString)
return result
}

// SeqOf returns a sequence containing the given values.
func SeqOf(values ...interface{}) Sequence {
// Making a defensive copy here because variadic functions can get hinky
// if someone says SeqOf(slice...) and then mutates slice.
if seq, ok := tryByteSeq(values); ok {
return seq
}
arr := make([]interface{}, len(values))
copy(arr, values)
return SeqFromArray(arr, false)
Expand All @@ -564,11 +587,7 @@ func SeqOfChars(values ...Char) Sequence {
}

func SeqOfBytes(values []byte) Sequence {
arr := make([]interface{}, len(values))
for i, v := range values {
arr[i] = v
}
return SeqFromArray(arr, false)
return newByteSeq(values)
}

// SeqOfString converts the given string into a sequence of characters.
Expand Down Expand Up @@ -734,18 +753,73 @@ func (seq *LazySequence) ToByteArray() []byte {
}

func ToByteArray(x Sequence) []byte {
nativeArray := x.ToArray().(GoNativeArray)
arr := make([]byte, len(nativeArray.contents))
for i, v := range nativeArray.contents {
arr[i] = v.(byte)
if arr, ok := x.ToArray().(ByteNativeArray); ok {
return arr.contents
}
return arr
arr := x.ToArray()
result := make([]byte, arr.Length())
for i := uint32(0); i < arr.Length(); i++ {
result[i] = arr.Select(i).(byte)
}
return result
}

/******************************************************************************
* Arrays
******************************************************************************/

// ByteNativeArray - optimized for uint8 sequences
type ByteNativeArray struct{ contents []byte }

func (a ByteNativeArray) Length() uint32 { return uint32(len(a.contents)) }
func (a ByteNativeArray) Select(i uint32) interface{} { return a.contents[i] }
func (a ByteNativeArray) Update(i uint32, t interface{}) { a.contents[i] = t.(uint8) }
func (a ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) {
for j := uint32(0); j < other.Length(); j++ {
a.contents[i+j] = other.Select(j).(uint8)
}
}
func (a ByteNativeArray) Freeze(size uint32) ImmutableArray { return a.Subarray(0, size) }
func (a ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray {
return ByteNativeArray{contents: a.contents[lo:hi]}
}
func (a ByteNativeArray) String() string { return "ByteNativeArray" }

// Helper to create byte sequences
func newByteSeq(data []byte) Sequence {
result := New_ArraySequence_()
result.Ctor__(ByteNativeArray{contents: data}, false)
return result
}

// Helper to try creating optimized uint8 sequence from slice
func tryByteSeq(contents []interface{}) (Sequence, bool) {
if len(contents) > 0 {
if _, ok := contents[0].(uint8); ok {
data := make([]byte, len(contents))
for i, v := range contents {
data[i] = v.(uint8)
}
return newByteSeq(data), true
}
}
return nil, false
}

// Helper to try creating optimized uint8 sequence from init function
func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) {
if n > 0 {
if _, ok := init(Zero).(uint8); ok {
data := make([]byte, n)
for i := uint32(0); i < n; i++ {
data[i] = init(IntOfUint32(i)).(uint8)
}
return newByteSeq(data), true
}
}
return nil, false
}

// A GoNativeArray is a single dimensional Go slice,
// wrapped up for the benefit of dafnyRuntime.dfy.
// We should refactor to wrap an Array interface as defined below
Expand All @@ -772,12 +846,11 @@ func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32
}

func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray {
otherArray := other.(GoNativeArray)
contents := make([]interface{}, otherArray.Length())
copy(contents, otherArray.contents)
return GoNativeArray{
contents: contents,
contents := make([]interface{}, other.Length())
for i := uint32(0); i < other.Length(); i++ {
contents[i] = other.Select(i)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we'd better implement this using copy as in the original, just with two different versions. Otherwise the loop will be a performance regression over the original.

}
return GoNativeArray{contents: contents}
}

func (array GoNativeArray) Length() uint32 {
Expand All @@ -793,8 +866,9 @@ func (array GoNativeArray) Update(i uint32, t interface{}) {
}

func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) {
otherArray := other.(GoNativeArray)
copy(array.contents[i:(i+otherArray.Length())], otherArray.contents)
for j := uint32(0); j < other.Length(); j++ {
array.contents[i+j] = other.Select(j)
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same as above.

}

func (array GoNativeArray) Freeze(size uint32) ImmutableArray {
Expand Down
134 changes: 104 additions & 30 deletions Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,15 +82,34 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc
return true
}

l := left.ToArray().(GoNativeArray).contents
r := right.ToArray().(GoNativeArray).contents
if IsEqualityComparable(l[0]) {
return slices.Equal(l[:index], r[:index])
} else {
for i := uint32(0); i < index; i++ {
if !AreEqual(l[i], r[i]) {
return false
leftArr, rightArr := left.ToArray(), right.ToArray()

// Fast path for ByteNativeArray
if l, ok := leftArr.(ByteNativeArray); ok {
if r, ok := rightArr.(ByteNativeArray); ok {
return slices.Equal(l.contents[:index], r.contents[:index])
}
}

// Fast path for GoNativeArray (preserve original optimization)
if l, ok := leftArr.(GoNativeArray); ok {
if r, ok := rightArr.(GoNativeArray); ok {
if IsEqualityComparable(l.contents[0]) {
return slices.Equal(l.contents[:index], r.contents[:index])
}
for i := uint32(0); i < index; i++ {
if !AreEqual(l.contents[i], r.contents[i]) {
return false
}
}
return true
}
}

// Generic fallback
for i := uint32(0); i < index; i++ {
if !AreEqual(leftArr.Select(i), rightArr.Select(i)) {
return false
}
}
return true
Expand Down Expand Up @@ -531,24 +550,28 @@ var EmptySeq = SeqOf()
// for the compiler to coerce the init function to a
// func (uint32) interface{}.
func SeqCreate(n uint32, init func(Int) interface{}) Sequence {
if seq, ok := tryByteSeqInit(n, init); ok {
return seq
}
return Companion_Sequence_.Create(n, func(index uint32) interface{} {
return init(IntOfUint32(index))
})
}

func SeqFromArray(contents []interface{}, isString bool) Sequence {
arr := GoNativeArray{
contents: contents,
if seq, ok := tryByteSeq(contents); ok && !isString {
return seq
}
result := New_ArraySequence_()
result.Ctor__(arr, isString)
result.Ctor__(GoNativeArray{contents: contents}, isString)
return result
}

// SeqOf returns a sequence containing the given values.
func SeqOf(values ...interface{}) Sequence {
// Making a defensive copy here because variadic functions can get hinky
// if someone says SeqOf(slice...) and then mutates slice.
if seq, ok := tryByteSeq(values); ok {
return seq
}
arr := make([]interface{}, len(values))
copy(arr, values)
return SeqFromArray(arr, false)
Expand All @@ -564,11 +587,7 @@ func SeqOfChars(values ...Char) Sequence {
}

func SeqOfBytes(values []byte) Sequence {
arr := make([]interface{}, len(values))
for i, v := range values {
arr[i] = v
}
return SeqFromArray(arr, false)
return newByteSeq(values)
}

// SeqOfString converts the given string into a sequence of characters.
Expand Down Expand Up @@ -734,18 +753,73 @@ func (seq *LazySequence) ToByteArray() []byte {
}

func ToByteArray(x Sequence) []byte {
nativeArray := x.ToArray().(GoNativeArray)
arr := make([]byte, len(nativeArray.contents))
for i, v := range nativeArray.contents {
arr[i] = v.(byte)
if arr, ok := x.ToArray().(ByteNativeArray); ok {
return arr.contents
}
return arr
arr := x.ToArray()
result := make([]byte, arr.Length())
for i := uint32(0); i < arr.Length(); i++ {
result[i] = arr.Select(i).(byte)
}
return result
}

/******************************************************************************
* Arrays
******************************************************************************/

// ByteNativeArray - optimized for uint8 sequences
type ByteNativeArray struct{ contents []byte }

func (a ByteNativeArray) Length() uint32 { return uint32(len(a.contents)) }
func (a ByteNativeArray) Select(i uint32) interface{} { return a.contents[i] }
func (a ByteNativeArray) Update(i uint32, t interface{}) { a.contents[i] = t.(uint8) }
func (a ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) {
for j := uint32(0); j < other.Length(); j++ {
a.contents[i+j] = other.Select(j).(uint8)
}
}
func (a ByteNativeArray) Freeze(size uint32) ImmutableArray { return a.Subarray(0, size) }
func (a ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray {
return ByteNativeArray{contents: a.contents[lo:hi]}
}
func (a ByteNativeArray) String() string { return "ByteNativeArray" }

// Helper to create byte sequences
func newByteSeq(data []byte) Sequence {
result := New_ArraySequence_()
result.Ctor__(ByteNativeArray{contents: data}, false)
return result
}

// Helper to try creating optimized uint8 sequence from slice
func tryByteSeq(contents []interface{}) (Sequence, bool) {
if len(contents) > 0 {
if _, ok := contents[0].(uint8); ok {
data := make([]byte, len(contents))
for i, v := range contents {
data[i] = v.(uint8)
}
return newByteSeq(data), true
}
}
return nil, false
}

// Helper to try creating optimized uint8 sequence from init function
func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) {
if n > 0 {
if _, ok := init(Zero).(uint8); ok {
data := make([]byte, n)
for i := uint32(0); i < n; i++ {
data[i] = init(IntOfUint32(i)).(uint8)
}
return newByteSeq(data), true
}
}
return nil, false
}

// A GoNativeArray is a single dimensional Go slice,
// wrapped up for the benefit of dafnyRuntime.dfy.
// We should refactor to wrap an Array interface as defined below
Expand All @@ -772,12 +846,11 @@ func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32
}

func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray {
otherArray := other.(GoNativeArray)
contents := make([]interface{}, otherArray.Length())
copy(contents, otherArray.contents)
return GoNativeArray{
contents: contents,
contents := make([]interface{}, other.Length())
for i := uint32(0); i < other.Length(); i++ {
contents[i] = other.Select(i)
}
return GoNativeArray{contents: contents}
}

func (array GoNativeArray) Length() uint32 {
Expand All @@ -793,8 +866,9 @@ func (array GoNativeArray) Update(i uint32, t interface{}) {
}

func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) {
otherArray := other.(GoNativeArray)
copy(array.contents[i:(i+otherArray.Length())], otherArray.contents)
for j := uint32(0); j < other.Length(); j++ {
array.contents[i+j] = other.Select(j)
}
}

func (array GoNativeArray) Freeze(size uint32) ImmutableArray {
Expand Down
Loading