Merge branch 'master' into temp

pkg/addr/fmt.go

@@ -12,6 +12,8 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+// +gobra
+
 package addr
 
 import (
@@ -24,6 +26,8 @@ import (
 
 // ParseFormattedIA parses an IA that was formatted with the FormatIA function.
 // The same options must be provided to successfully parse.
+// @ trusted
+// @ requires false
 func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) {
 	parts := strings.Split(ia, "-")
 	if len(parts) != 2 {
@@ -33,15 +37,17 @@ func ParseFormattedIA(ia string, opts ...FormatOption) (IA, error) {
 	if err != nil {
 		return 0, serrors.WrapStr("parsing ISD part", err, "value", ia)
 	}
-	as, err := ParseFormattedAS(parts[1], opts...)
+	as_, err := ParseFormattedAS(parts[1], opts...)
 	if err != nil {
 		return 0, serrors.WrapStr("parsing AS part", err, "value", ia)
 	}
-	return MustIAFrom(isd, as), nil
+	return MustIAFrom(isd, as_), nil
 }
 
 // ParseFormattedISD parses an ISD number that was formatted with the FormatISD
 // function. The same options must be provided to successfully parse.
+// @ trusted
+// @ requires false
 func ParseFormattedISD(isd string, opts ...FormatOption) (ISD, error) {
 	o := applyFormatOptions(opts)
 	if o.defaultPrefix {
@@ -56,29 +62,35 @@ func ParseFormattedISD(isd string, opts ...FormatOption) (ISD, error) {
 
 // ParseFormattedAS parses an AS number that was formatted with the FormatAS
 // function. The same options must be provided to successfully parse.
-func ParseFormattedAS(as string, opts ...FormatOption) (AS, error) {
+// @ trusted
+// @ requires false
+func ParseFormattedAS(as_ string, opts ...FormatOption) (AS, error) {
 	o := applyFormatOptions(opts)
 	if o.defaultPrefix {
-		trimmed := strings.TrimPrefix(as, "AS")
-		if trimmed == as {
-			return 0, serrors.New("prefix is missing", "prefix", "AS", "value", as)
+		trimmed := strings.TrimPrefix(as_, "AS")
+		if trimmed == as_ {
+			return 0, serrors.New("prefix is missing", "prefix", "AS", "value", as_)
 		}
-		as = trimmed
+		as_ = trimmed
 	}
-	return parseAS(as, o.separator)
+	return parseAS(as_, o.separator)
 }
 
 // FormatIA formats the ISD-AS.
+// @ trusted
+// @ requires false
 func FormatIA(ia IA, opts ...FormatOption) string {
 	o := applyFormatOptions(opts)
-	as := fmtAS(ia.AS(), o.separator)
+	as_ := fmtAS(ia.AS(), o.separator)
 	if o.defaultPrefix {
-		return fmt.Sprintf("ISD%d-AS%s", ia.ISD(), as)
+		return fmt.Sprintf("ISD%d-AS%s", ia.ISD(), as_)
 	}
-	return fmt.Sprintf("%d-%s", ia.ISD(), as)
+	return fmt.Sprintf("%d-%s", ia.ISD(), as_)
 }
 
 // FormatISD formats the ISD number.
+// @ trusted
+// @ requires false
 func FormatISD(isd ISD, opts ...FormatOption) string {
 	o := applyFormatOptions(opts)
 	if o.defaultPrefix {
@@ -88,44 +100,63 @@ func FormatISD(isd ISD, opts ...FormatOption) string {
 }
 
 // FormatAS formats the AS number.
-func FormatAS(as AS, opts ...FormatOption) string {
+// @ trusted
+// @ requires false
+func FormatAS(as_ AS, opts ...FormatOption) string {
 	o := applyFormatOptions(opts)
-	s := fmtAS(as, o.separator)
+	s := fmtAS(as_, o.separator)
 	if o.defaultPrefix {
 		return "AS" + s
 	}
 	return s
 }
 
-func fmtAS(as AS, sep string) string {
-	if !as.inRange() {
-		return fmt.Sprintf("%d [Illegal AS: larger than %d]", as, MaxAS)
+// @ requires as_.inRange()
+// @ decreases
+func fmtAS(as_ AS, sep string) string {
+	if !as_.inRange() {
+		return fmt.Sprintf("%d [Illegal AS: larger than %d]", as_, MaxAS)
 	}
 	// Format BGP ASes as decimal
-	if as <= MaxBGPAS {
-		return strconv.FormatUint(uint64(as), 10)
+	if as_ <= MaxBGPAS {
+		// (VerifiedSCION) the following property is guaranteed by the type system,
+		// but Gobra cannot infer it yet
+		// @ assume 0 <= as_
+		return strconv.FormatUint(uint64(as_), 10)
 	}
 	// Format all other ASes as 'sep'-separated hex.
-	const maxLen = len("ffff:ffff:ffff")
-	var b strings.Builder
+	// (VerifiedSCION) revert this change when Gobra is fixed.
+	// const maxLen = len("ffff:ffff:ffff")
+	var maxLen = len("ffff:ffff:ffff")
+	var b /*@@@*/ strings.Builder
+	// @ b.ZeroBuilderIsReadyToUse()
 	b.Grow(maxLen)
+	// @ invariant b.Mem()
+	// @ decreases asParts - i
 	for i := 0; i < asParts; i++ {
 		if i > 0 {
 			b.WriteString(sep)
 		}
 		shift := uint(asPartBits * (asParts - i - 1))
-		b.WriteString(strconv.FormatUint(uint64(as>>shift)&asPartMask, asPartBase))
+		// (VerifiedSCION) the following property is guaranteed by the type system,
+		// but Gobra cannot infer it yet
+		// @ assume 0 <= uint64(as_>>shift)&asPartMask
+		b.WriteString(strconv.FormatUint(uint64(as_>>shift)&asPartMask, asPartBase))
 	}
 	return b.String()
 }
 
-type FormatOption func(*formatOptions)
+// (VerifiedSCION) revert this change when Gobra is fixed.
+// type FormatOption func(*formatOptions)
+type FormatOption = func(*formatOptions)
 
 type formatOptions struct {
 	defaultPrefix bool
 	separator     string
 }
 
+// @ trusted
+// @ requires false
 func applyFormatOptions(opts []FormatOption) formatOptions {
 	o := formatOptions{
 		defaultPrefix: false,
@@ -139,6 +170,8 @@ func applyFormatOptions(opts []FormatOption) formatOptions {
 
 // WithDefaultPrefix enables the default prefix which depends on the type. For
 // the AS number, the prefix is 'AS'. For the ISD number, the prefix is 'ISD'.
+// @ trusted
+// @ requires false
 func WithDefaultPrefix() FormatOption {
 	return func(o *formatOptions) {
 		o.defaultPrefix = true
@@ -147,13 +180,17 @@ func WithDefaultPrefix() FormatOption {
 
 // WithSeparator sets the separator to use for formatting AS numbers. In case of
 // the empty string, the ':' is used.
+// @ trusted
+// @ requires false
 func WithSeparator(separator string) FormatOption {
 	return func(o *formatOptions) {
 		o.separator = separator
 	}
 }
 
 // WithFileSeparator returns an option that sets the separator to underscore.
+// @ trusted
+// @ requires false
 func WithFileSeparator() FormatOption {
 	return WithSeparator("_")
 }

verification/dependencies/strings/builder.gobra

@@ -0,0 +1,42 @@
+// Copyright 2009 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in https://golang.org/LICENSE
+
+// Signatures for the public declarations in file
+// https://github.com/golang/go/blob/master/src/strings/strings.go
+
+// +gobra
+
+package strings
+
+// A Builder is used to efficiently build a string using Write methods.
+// It minimizes memory copying. The zero value is ready to use.
+// Do not copy a non-zero Builder.
+type Builder struct {
+	addr *Builder // of receiver, to detect copies by value
+	buf  []byte
+}
+
+pred (b *Builder) Mem()
+
+// String returns the accumulated string.
+preserves b.Mem()
+decreases _
+func (b *Builder) String() string
+
+requires  0 <= n
+preserves b.Mem()
+decreases _
+func (b *Builder) Grow(n int)
+
+preserves b.Mem()
+ensures   err == nil
+decreases _
+func (b *Builder) WriteString(s string) (n int, err error)
+
+ghost
+requires acc(b)
+requires *b === Builder{}
+ensures  b.Mem()
+decreases _
+func (b *Builder) ZeroBuilderIsReadyToUse()

verification/utils/bitwise/bitwise-eqs.gobra

@@ -69,6 +69,7 @@ ensures 3 & 2 == 2
 decreases
 pure func InfoFieldFirstByteSerializationLemmas() bool
 
+ghost
 ensures csum > 0xffff ==>
 	let newCsum := (csum >> 16) + (csum & 0xffff) in
 	newCsum < csum