Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 6 additions & 2 deletions .github/workflows/library_interop_keyring_test_vectors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,9 @@ jobs:

- name: Install LibCurl
if: matrix.os == 'ubuntu-22.04' && matrix.language == 'c'
run: sudo apt-get install libcurl4-openssl-dev
run: |
sudo apt-get update
sudo apt-get install -y libcurl4-openssl-dev

- name: Checkout C-ESDK
if: matrix.language == 'c'
Expand Down Expand Up @@ -338,7 +340,9 @@ jobs:

- name: Install LibCurl
if: matrix.os == 'ubuntu-22.04' && matrix.decrypting_language == 'c'
run: sudo apt-get install libcurl4-openssl-dev
run: |
sudo apt-get update
sudo apt-get install -y libcurl4-openssl-dev

- name: Checkout C-ESDK
if: matrix.decrypting_language == 'c'
Expand Down
2 changes: 2 additions & 0 deletions TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,5 @@ require (
github.com/google/uuid v1.6.0 // indirect
github.com/jmespath/go-jmespath v0.4.0 // indirect
)

replace github.com/dafny-lang/DafnyRuntimeGo/v4 => ../../../../esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4
2 changes: 0 additions & 2 deletions TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,6 @@ github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 h1:pqEJQtlKWvnv3B6VRt60ZmsHy3So
github.com/aws/aws-sdk-go-v2/service/sts v1.33.8/go.mod h1:f6vjfZER1M17Fokn0IzssOTMT2N8ZSq+7jnNF0tArvw=
github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro=
github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg=
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1 h1:tTQ9M9HCUaf2SXqutj2vmMqJKJpefWMSqx1niqTqi8M=
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto=
github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8=
github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0=
Expand Down
2 changes: 2 additions & 0 deletions TestVectors/runtimes/go/TestsFromDafny-go/go.mod
Original file line number Diff line number Diff line change
Expand Up @@ -47,3 +47,5 @@ require (
github.com/google/uuid v1.6.0 // indirect
github.com/jmespath/go-jmespath v0.4.0 // indirect
)

replace github.com/dafny-lang/DafnyRuntimeGo/v4 => ../../../../esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4
2 changes: 0 additions & 2 deletions TestVectors/runtimes/go/TestsFromDafny-go/go.sum
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,6 @@ github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 h1:pqEJQtlKWvnv3B6VRt60ZmsHy3So
github.com/aws/aws-sdk-go-v2/service/sts v1.33.8/go.mod h1:f6vjfZER1M17Fokn0IzssOTMT2N8ZSq+7jnNF0tArvw=
github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro=
github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg=
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1 h1:tTQ9M9HCUaf2SXqutj2vmMqJKJpefWMSqx1niqTqi8M=
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto=
github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8=
github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0=
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
# If you prefer the allow list template instead of the deny list, see community template:
# https://github.com/github/gitignore/blob/main/community/Golang/Go.AllowList.gitignore
#
# Binaries for programs and plugins
*.exe
*.exe~
*.dll
*.so
*.dylib

# Test binary, built with `go test -c`
*.test

# Output of the go coverage tool, specifically when used with LiteIDE
*.out

# Dependency directories (remove the comment below to include it)
# vendor/

# Go workspace file
go.work
go.work.sum
21 changes: 21 additions & 0 deletions esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
MIT License

Copyright (c) 2024 Dafny

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
# DafnyRuntimeGo

The Go version of the Dafny runtime library
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module github.com/dafny-lang/DafnyRuntimeGo

go 1.21
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
// Package _System
// Dafny module _System compiled into Go

package _System

import (
os "os"

_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
)

var _ = os.Args
var _ _dafny.Dummy__

type Dummy__ struct{}

// Definition of class Nat
type Nat struct {
}

func New_Nat_() *Nat {
_this := Nat{}

return &_this
}

type CompanionStruct_Nat_ struct {
}

var Companion_Nat_ = CompanionStruct_Nat_{}

func (*Nat) String() string {
return "_System.Nat"
}

// End of class Nat

func Type_Nat_() _dafny.TypeDescriptor {
return type_Nat_{}
}

type type_Nat_ struct {
}

func (_this type_Nat_) Default() interface{} {
return _dafny.Zero
}

func (_this type_Nat_) String() string {
return "_System.Nat"
}
func (_this *CompanionStruct_Nat_) Is_(__source _dafny.Int) bool {
var _0_x _dafny.Int = (__source)
_ = _0_x
return (_0_x).Sign() != -1
}
Loading
Loading