experimental: add specifications to packages pkg/addr and pkg/slayers/path, verify them in the CI with Gobra

.github/workflows/gobra.yml

@@ -1,3 +1,18 @@
+# This file sets up a workflow that runs Gobra (github.com/viperproject/gobra)
+# on selected packages of the SCION implementation. Gobra is a program verifier,
+# i.e., it checks that the implementation of each function behaves as expected.
+# The expected behaviour of each function is provided as a formal specification
+# written in comments above the function signature. When Gobra is not able to
+# prove that a function behaves according to its specification, it generates an
+# (hopefully) informative error message, which identifies the parts of the code
+# where the issues might lie.
+# For more information on Gobra and its error messages, check the following:
+# - The Gobra Book (WIP): viperproject.github.io/gobra-book/
+# - The tutorial: github.com/viperproject/gobra/blob/master/docs/tutorial.md
+# The former covers more features of Gobra and contains more up-to-date
+# information, but it is still under construction.
+
+
 name: Verify the specified codebase
 
 on:
@@ -8,32 +23,53 @@ jobs:
   setup-and-test:
     runs-on: ubuntu-latest
     env:
-      statsFile: '/gobra/stats.json'
+      imageVersion: 'v25.09'
+      module: 'github.com/scionproto/scion/'
+      includePaths: '. ./gobra/stdlib-specs'
+      continueOnError: true
     steps:
       - name: Checkout the SCION repository
         uses: actions/checkout@v2
-      - name: Set-up caching for the verification results
-        uses: actions/cache@v3
-        env:
-          cache-name: gobra-cache
+      - name: Check that the package gobra/utils is well-formed
+        uses: viperproject/[email protected]
         with:
-          path: ${{ runner.workspace }}/.gobra/cache.json
-          key: ${{ env.cache-name }}
-      - name: Verify the specified files
-        uses: viperproject/[email protected]
-        with:
-          # Prefix used to resolve SCION packages
-          module: 'github.com/scionproto/scion/'
+          packages: 'gobra/utils'
           # Gobra only verifies files annotated with the header "// +gobra"
           headerOnly: '1'
-          # Traverse the entire repository, including nested packages,
-          # in search for annotated files to verify
+          timeout: 2m
+          imageVersion: ${{ env.imageVersion }}
+          module: ${{ env.module }}
+          includePaths: ${{ env.includePaths }}
+          continue-on-error: ${{ env.continueOnError }}
+      - name: Check that specifications of third-party libraries are well-formed
+        uses: viperproject/[email protected]
+        with:
+          projectLocation: 'scion/gobra/stdlib-specs'
+          headerOnly: '1'
+          # Check all package specifications in directory stdlib-specs
           recursive: '1'
           timeout: 10m
-          caching: '1'
-          statsFile: ${{ env.statsFile }}
-      - name: Upload the verification report
-        uses: actions/upload-artifact@v4
+          imageVersion: ${{ env.imageVersion }}
+          module: ${{ env.module }}
+          includePaths: '. ../..' # relative to project location
+          continue-on-error: ${{ env.continueOnError }}
+      - name: Verify package `pkg/addr`
+        uses: viperproject/[email protected]
+        with:
+          packages: 'pkg/addr'
+          headerOnly: '1'
+          timeout: 2m
+          imageVersion: ${{ env.imageVersion }}
+          module: ${{ env.module }}
+          includePaths: ${{ env.includePaths }}
+          continue-on-error: ${{ env.continueOnError }}
+      - name: Verify package `pkg/slayers/path`
+        uses: viperproject/[email protected]
         with:
-          name: verification_stats.json
-          path: ${{ env.statsFile }}
+          packages: 'pkg/slayers/path'
+          headerOnly: '1'
+          timeout: 2m
+          imageVersion: ${{ env.imageVersion }}
+          module: ${{ env.module }}
+          includePaths: ${{ env.includePaths }}
+          continue-on-error: ${{ env.continueOnError }}

gobra/README.md

@@ -0,0 +1,22 @@
+# Gobra specs
+
+This directory contains the formal specification of a small part of the
+Go standard library (in [`./stdlib-specs`](./stdlib-specs)) required to
+verify the annotated files in the SCION codebase. In addition, we provide
+a verified Gobra package in [`./utils`](./utils) that contains useful
+definitions that are used in the verified packages of SCION.
+
+## Contributing
+
+It is expected that we will need a formal specification for more parts
+of the Go standard library as we progress in verifying more code in the
+SCION repository. To do so, one may add the type declarations and
+signatures of unspecified functions and methods (_without the bodies_),
+together with their contracts (i.e., pre- and postconditions), to the
+corresponding package specification in directory
+[`./stdlib-specs`](./stdlib-specs).
+
+Given that the specification of the standard library is not verified by
+Gobra itself, it is possible to introduce errors when writing the
+specification for these methods. Thus, any extensions to the specification
+require extreme care from the author of the extensions and from code reviewers.

gobra/stdlib-specs/encoding/encoding_spec.gobra

@@ -0,0 +1,26 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package encoding
+
+type TextUnmarshaler interface {
+	pred Mem()
+
+	preserves Mem() && acc(text)
+	ensures   err != nil ==> err.ErrorMem()
+	decreases
+	UnmarshalText(text []byte) (err error)
+}

gobra/stdlib-specs/flag/flag_spec.gobra

@@ -0,0 +1,28 @@
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package flag
+
+type Value interface {
+	pred Mem()
+
+	preserves Mem()
+	decreases
+	String() string
+
+	preserves Mem()
+	ensures   err != nil ==> err.ErrorMem()
+	decreases
+	Set(string) (err error)
+}

gobra/stdlib-specs/fmt/fmt_spec.gobra

@@ -0,0 +1,32 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package fmt
+
+import "github.com/scionproto/scion/gobra/utils/"
+
+preserves forall i int :: { &v[i] } 0 <= i && i < len(v) ==>
+	acc(&v[i], utils.ReadPerm)
+decreases
+func Sprintf(format string, v ...interface{}) string
+
+type Stringer interface {
+	pred Mem()
+
+	preserves Mem()
+	decreases
+	String() string
+}

gobra/stdlib-specs/hash/hash_spec.gobra

@@ -0,0 +1,55 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package hash
+
+import "github.com/scionproto/scion/gobra/utils/"
+
+type Hash interface {
+	pred Mem()
+
+	// Implementations of Hash must also implement io.Writer.
+	preserves Mem() 
+	preserves acc(p, utils.ReadPerm)
+	ensures   0 <= n && n <= len(p)
+	// The documentation of this interface states that the Write
+	// method in implementations of Hash may never fail.
+	// (https://pkg.go.dev/hash#Hash)
+	ensures   err == nil && n == len(p)
+	ensures   Size() == old(Size()) + len(p)
+	decreases
+	Write(p []byte) (n int, err error)
+
+	preserves acc(Mem(), utils.ReadPerm)
+	requires acc(b)
+	ensures  acc(res) && len(res) == len(b) + Size()
+	decreases
+	Sum(b []byte) (res []byte)
+
+	preserves Mem()
+	decreases
+	Reset()
+
+	requires Mem()
+	ensures  0 <= res
+	decreases
+	pure Size() (res int)
+
+	requires Mem()
+	ensures  0 <= res
+	decreases
+	pure BlockSize() (res int)
+}

gobra/stdlib-specs/net/ip.gobra

@@ -0,0 +1,30 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package net
+
+// IP address lengths (bytes).
+const (
+	IPv4len = 4
+	IPv6len = 16
+)
+
+type IP []byte
+
+pred (ip IP) Mem() {
+	(len(ip) == IPv4len || len(ip) == IPv6len) &&
+	forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i])
+}

gobra/stdlib-specs/net/iprawsock.gobra

@@ -0,0 +1,21 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package net
+
+ensures err != nil ==> err.ErrorMem()
+decreases
+func SplitHostPort(hostport string) (host string, port string, err error)

gobra/stdlib-specs/net/netip/netip_spec.gobra

@@ -0,0 +1,62 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package netip
+
+import "github.com/scionproto/scion/gobra/utils/"
+
+type Addr struct {
+	privateField utils.PrivateField
+}
+
+type AddrPort struct {
+	privateField utils.PrivateField
+}
+
+decreases
+func (ip Addr) String() string
+
+ensures err != nil ==> err.ErrorMem()
+decreases
+func ParseAddr(s string) (addr Addr, err error)
+
+decreases
+func AddrFrom4(addr [4]byte) Addr
+
+decreases
+func AddrFrom16(addr [16]byte) Addr
+
+decreases
+func (ip Addr) Unmap() Addr
+
+decreases
+func (ip Addr) IsValid() (res bool)
+
+decreases
+func (ip Addr) Is4() bool
+
+decreases
+func (ip Addr) Is6() bool
+
+ensures acc(b)
+decreases
+func (ip Addr) AsSlice() (b []byte)
+
+decreases
+func (p AddrPort) IsValid() (res bool)
+
+decreases
+func (p AddrPort) Addr() Addr