feat: StandardLibrary for Go

Author: Shubham Chaturvedi

.github/workflows/library_go_tests.yml

@@ -0,0 +1,87 @@
+# This workflow performs tests in Go.
+name: Library Go tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  testGo:
+    strategy:
+      fail-fast: false
+      matrix:
+        library:
+          [
+            StandardLibrary,
+          ]
+        go-version: ["1.23"]
+        os: [
+          # TODO fix Dafny-generated tests on Windows;
+          # the sys.path workaround for generated Dafny doesn't work on Windows.
+          # Note: only tests use the sys.path workaround, not source code.
+          # Windows source code is tested downstream (ex. ESDK-Go CI).
+          # windows-latest,
+          ubuntu-latest,
+          macos-12,
+        ]
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: GoTests
+
+      - uses: actions/checkout@v4
+      # The specification submodule is private so we don't have access, but we don't need
+      # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
+      - run: git submodule update --init libraries
+      - run: git submodule update --init smithy-dafny
+
+      # TODO: This is still in nighlty
+      - name: Setup Dafny
+        uses: dafny-lang/setup-dafny-action@v1.7.0
+        with:
+          dafny-version: "nightly-latest"
+
+      - name: Setup Go ${{ matrix.go-version }} for running tests
+        uses: actions/setup-go@v2
+        with:
+          go-version: ${{ matrix.go-version }}
+
+      - name: Install Go imports
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
+      - name: Build ${{ matrix.library }} implementation
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_go CORES=$CORES
+
+      - name: Test ${{ matrix.library }}
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          make test_go

StandardLibrary/Makefile

@@ -17,8 +17,9 @@ transpile_implementation: STD_LIBRARY=
 transpile_test: STD_LIBRARY=
 transpile_dependencies: STD_LIBRARY=
 
-# Python
+GO_MODULE_NAME="github.com/dafny-lang/DafnyStandardLibGo"
 
+# Python
 PYTHON_MODULE_NAME=smithy_dafny_standard_library
 
 RUST_OTHER_FILES := \

StandardLibrary/runtimes/go/ImplementationFromDafny-go/ConcurrentCall/externs.go

@@ -0,0 +1,18 @@
+package ConcurrentCall
+
+import "sync"
+
+func ConcurrentCall(calle Callee, serialIters uint32, concurrentIters uint32) {
+	var wg sync.WaitGroup
+	for i := uint32(0); i < concurrentIters; i++ {
+		wg.Add(1)
+		concurrentPos := i
+		go func() {
+			defer wg.Done()
+			for j := uint32(0); j < serialIters; j++ {
+				calle.Call(j, concurrentPos)
+			}
+		}()
+		wg.Wait()
+	}
+}

StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries/externs.go

@@ -0,0 +1,145 @@
+package DafnyLibraries
+
+import (
+	sync "sync"
+
+	_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+	Std_Wrappers "github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+)
+
+// Definition of class MutableMap
+type MutableMap struct {
+	Internal sync.Map
+}
+
+func New_MutableMap_() *MutableMap {
+	return &MutableMap{}
+}
+
+type CompanionStruct_MutableMap_ struct {
+}
+
+var Companion_MutableMap_ = CompanionStruct_MutableMap_{}
+
+func (_this *MutableMap) Equals(other *MutableMap) bool {
+	return _this == other
+}
+
+func (_this *MutableMap) EqualsGeneric(x interface{}) bool {
+	other, ok := x.(*MutableMap)
+	return ok && _this.Equals(other)
+}
+
+func (*MutableMap) String() string {
+	return "ExternConcurrent.MutableMap"
+}
+
+func Type_MutableMap_(Type_K_ _dafny.TypeDescriptor, Type_V_ _dafny.TypeDescriptor) _dafny.TypeDescriptor {
+	return type_MutableMap_{Type_K_, Type_V_}
+}
+
+type type_MutableMap_ struct {
+	Type_K_ _dafny.TypeDescriptor
+	Type_V_ _dafny.TypeDescriptor
+}
+
+func (_this type_MutableMap_) Default() interface{} {
+	return (*MutableMap)(nil)
+}
+
+func (_this type_MutableMap_) String() string {
+	return "ExternConcurrent.MutableMap"
+}
+func (_this *MutableMap) ParentTraits_() []*_dafny.TraitID {
+	return [](*_dafny.TraitID){}
+}
+
+var _ _dafny.TraitOffspring = &MutableMap{}
+
+func (_this *MutableMap) Ctor__() {
+	{
+	}
+}
+func (_this *MutableMap) Keys() _dafny.Set {
+	{
+		keys := make([]interface{}, 0)
+
+		_this.Internal.Range(func(key, value interface{}) bool {
+			keys = append(keys, key)
+			return true
+		})
+
+		return _dafny.SetOf(keys[:]...)
+	}
+}
+func (_this *MutableMap) HasKey(k interface{}) bool {
+	{
+		_, ok := _this.Internal.Load(k)
+		return ok
+	}
+}
+func (_this *MutableMap) Values() _dafny.Set {
+	{
+		values := make([]interface{}, 0)
+
+		_this.Internal.Range(func(key, value interface{}) bool {
+			values = append(values, value)
+			return true
+		})
+
+		return _dafny.SetOf(values[:]...)
+	}
+}
+func (_this *MutableMap) Items() _dafny.Set {
+	{
+		items := make([]interface{}, 0)
+
+		_this.Internal.Range(func(key, value interface{}) bool {
+			items = append(items, _dafny.TupleOf(key, value))
+			return true
+		})
+
+		return _dafny.SetOf(items[:]...)
+	}
+}
+func (_this *MutableMap) Select(k interface{}) interface{} {
+	r := _this.Get(k)
+	if r.IsFailure() {
+		panic("ff")
+	}
+	return r.Dtor_value()
+}
+func (_this *MutableMap) Get(k interface{}) Std_Wrappers.Option {
+	{
+		value, ok := _this.Internal.Load(k)
+		if ok {
+			return Std_Wrappers.Companion_Option_.Create_Some_(value)
+		} else {
+			return Std_Wrappers.Companion_Option_.Create_None_()
+		}
+	}
+}
+func (_this *MutableMap) Put(k interface{}, v interface{}) {
+	{
+		_this.Internal.Store(k, v)
+	}
+}
+func (_this *MutableMap) Remove(k interface{}) {
+	{
+		_this.Internal.Delete(k)
+	}
+}
+func (_this *MutableMap) Size() _dafny.Int {
+	{
+		var c _dafny.Int = _dafny.Zero
+
+		_this.Internal.Range(func(key, value interface{}) bool {
+			c = c.Plus(_dafny.One)
+			return true
+		})
+
+		return c
+	}
+}
+
+// End of class MutableMap

StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go

@@ -0,0 +1,35 @@
+package FileIO
+
+import (
+	"io/ioutil"
+	os "os"
+	"path/filepath"
+
+	_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+)
+
+func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
+	p := _dafny.SequenceVerbatimString(path, false)
+	dat, err := ioutil.ReadFile(p)
+	if err != nil {
+		errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
+		return true, _dafny.EmptySeq, errAsSequence
+	}
+	datAsSequence := _dafny.SeqOfBytes(dat)
+	return false, datAsSequence, _dafny.EmptySeq
+}
+
+func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
+	p := _dafny.SequenceVerbatimString(path, false)
+
+	// Create directories
+	os.MkdirAll(filepath.Dir(p), os.ModePerm)
+
+	bytesArray := _dafny.ToByteArray(bytes)
+	err := ioutil.WriteFile(p, bytesArray, 0644)
+	if err != nil {
+		errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
+		return true, errAsSequence
+	}
+	return false, _dafny.EmptySeq
+}

StandardLibrary/runtimes/go/ImplementationFromDafny-go/SortedSets/externs.go

@@ -0,0 +1,58 @@
+package SortedSets
+
+import (
+	"sort"
+
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+)
+
+func SetToOrderedSequence(set dafny.Set, fn func(interface{}, interface{}) bool) dafny.Sequence {
+	var arr []interface{}
+	for i := set.Iterator(); ; {
+		val, ok := i()
+		if ok {
+			arr = append(arr, val)
+		} else {
+			sort.Slice(arr, func(i, j int) bool {
+				a := arr[i].(dafny.Sequence)
+				b := arr[j].(dafny.Sequence)
+				for ii, jj := dafny.Iterate(a), dafny.Iterate(b); ; {
+					v1, ok1 := ii()
+					v2, ok2 := jj()
+					if ok1 && ok2 {
+						if fn(v1, v2) {
+							return true
+						}
+						if fn(v2, v1) {
+							return false
+						}
+					} else if ok1 {
+						return false
+					} else if ok2 {
+						return true
+					} else {
+						return false
+					}
+				}
+			})
+			return dafny.SeqOf(arr...)
+		}
+	}
+}
+
+func SetToOrderedSequence2(set dafny.Set, fn func(interface{}, interface{}) bool) dafny.Sequence {
+	return SetToOrderedSequence(set, fn)
+}
+
+func SetToSequence(set dafny.Set) dafny.Sequence {
+	var arr []interface{}
+	for i := set.Iterator(); ; {
+		val, ok := i()
+		if ok {
+			arr = append(arr, val)
+		} else {
+			return dafny.SeqOf(arr...)
+		}
+	}
+
+}

StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go

@@ -0,0 +1,20 @@
+package _Time
+
+import (
+	"time"
+
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+)
+
+func CurrentRelativeTime() int64 {
+	return int64(time.Now().Second())
+}
+
+func GetCurrentTimeStamp() Wrappers.Result {
+	return Wrappers.Companion_Result_.Create_Success_(dafny.SeqOfChars([]dafny.Char(time.Now().Format("2006-01-02T15:04:05.000000Z"))...))
+}
+
+func CurrentRelativeTimeMilli() int64 {
+	return time.Now().UnixMilli()
+}