based on pr #181

Author: jcp19

.gitignore

@@ -99,3 +99,7 @@ target
 *.unparsed
 *.gobrafied
 *.internal
+.devcontainer
+.metals
+.bazelbsp
+.bazel

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,24 +100,28 @@ 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)
+// @ trusted
+// @ requires as_.inRange()
+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)
+	// Format BGP ASes as_ decimal
+	if as_ <= MaxBGPAS {
+		return strconv.FormatUint(uint64(as_), 10)
 	}
-	// Format all other ASes as 'sep'-separated hex.
+	// Format all other ASes as_ 'sep'-separated hex.
 	const maxLen = len("ffff:ffff:ffff")
 	var b strings.Builder
 	b.Grow(maxLen)
@@ -114,18 +130,20 @@ func fmtAS(as AS, sep string) string {
 			b.WriteString(sep)
 		}
 		shift := uint(asPartBits * (asParts - i - 1))
-		b.WriteString(strconv.FormatUint(uint64(as>>shift)&asPartMask, asPartBase))
+		b.WriteString(strconv.FormatUint(uint64(as_>>shift)&asPartMask, asPartBase))
 	}
 	return b.String()
 }
 
-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 +157,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 +167,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("_")
 }

pkg/addr/fmt_spec.gobra

@@ -15,9 +15,6 @@
 
 // +gobra
 
-// @ initEnsures ErrBadHostAddrType.ErrorMem()
-// @ initEnsures ErrMalformedHostAddrType.ErrorMem()
-// @ initEnsures ErrUnsupportedSVCAddress.ErrorMem()
 package addr
 
 import (

pkg/addr/host.go

@@ -84,7 +84,7 @@ func (ip IP) To4(ghost wildcard bool) (res IP) {
 }
 
 pure
-preserves forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], definitions.ReadL16)
+requires forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], definitions.ReadL16)
 func isZeros(s []byte) bool
 
 // To16 converts the IP address ip to a 16-byte representation.

verification/dependencies/net/ip.gobra

@@ -9,6 +9,39 @@
 
 package strconv
 
+// import "errors" //(joao) stub errors package still not implemented
+
+// ErrRange indicates that a value is out of range for the target type.
+// var ErrRange = errors.New("value out of range") // (joao): no support for global vars and for the errors package
+
+// ErrSyntax indicates that a value does not have the right syntax for the target type.
+// var ErrSyntax = errors.New("invalid syntax") // (joao): no support for global vars and for the errors package
+
+// A NumError records a failed conversion.
+type NumError struct {
+	Func string // the failing function (ParseBool, ParseInt, ParseUint, ParseFloat, ParseComplex)
+	Num  string // the input
+	Err  error  // the reason the conversion failed (e.g. ErrRange, ErrSyntax, etc.)
+}
+
+requires p > 0
+requires acc(e, p)
+ensures acc(e, p)
+decreases _
+func (e *NumError) Error(ghost p perm) string /*{
+	return "strconv." + e.Func + ": " + "parsing " + Quote(e.Num) + ": " + e.Err.Error()
+}*/
+
+
+requires acc(e, _)
+decreases
+pure func (e *NumError) Unwrap() error { return e.Err }
+
+// const intSize = 32 << (^uint(0) >> 63)
+
+// IntSize is the size in bits of an int or uint value.
+// const IntSize = intSize
+
 // a to the power of b
 ghost
 requires exp >= 0
@@ -20,7 +53,7 @@ pure func Exp(base int, exp int) (res int) {
 // ParseUint is like ParseInt but for unsigned numbers.
 requires base == 0 || (2 <= base && base <= 36)
 requires bitSize > 0 && bitSize <= 64
-ensures retErr == nil ==> (ret >= 0 && ret < Exp(2, bitSize))
+ensures retErr == nil ==> (ret >= 0 && ret < uint64(Exp(2, bitSize)))
 ensures retErr != nil ==> retErr.ErrorMem()
 decreases _
 func ParseUint(s string, base int, bitSize int) (ret uint64, retErr error)