Add missing termination proofs

.gitignore

@@ -93,8 +93,12 @@ _build
 *.vpr
 *.internal
 *.unparsed
+gobra/tmp/*
 
 # Other
 #########################
 *.log
 *.txt
+project/
+target/
+tmp/

gobra/dependencies/kit/metrics/metrics.gobra

@@ -9,10 +9,12 @@ type Counter interface {
     requires forall i int :: 0 <= i && i < len(labelValues) ==> acc(&labelValues[i], 1/1000)
     ensures  Mem()
     ensures  forall i int :: 0 <= i && i < len(labelValues) ==> acc(&labelValues[i], 1/1000)
+    decreases
 	With(labelValues ...string) (res Counter)
 
     requires Mem()
     ensures  Mem()
+    decreases
 	Add(delta float64)
 }
 
@@ -25,14 +27,17 @@ type Gauge interface {
     requires forall i int :: 0 <= i && i < len(labelValues) ==> acc(&labelValues[i], 1/1000)
     ensures  Mem()
     ensures  forall i int :: 0 <= i && i < len(labelValues) ==> acc(&labelValues[i], 1/1000)
+    decreases
 	With(labelValues ...string) Gauge
 
     requires Mem()
     ensures  Mem()
+    decreases
 	Set(value float64)
 
     requires Mem()
     ensures  Mem()
+    decreases
 	Add(delta float64)
 }
 
@@ -47,9 +52,11 @@ type Histogram interface {
     requires forall i int :: 0 <= i && i < len(labelValues) ==> acc(&labelValues[i], 1/1000)
     ensures  Mem()
     ensures  forall i int :: 0 <= i && i < len(labelValues) ==> acc(&labelValues[i], 1/1000)
+    decreases
 	With(labelValues ...string) Histogram
 
     requires Mem()
     ensures  Mem()
+    decreases
 	Observe(value float64)
 }

gobra/dependencies/prometheus/promauto/auto.gobra

@@ -23,6 +23,7 @@ import "gobra/dependencies/prometheus/client_golang/prometheus"
 // prometheus.DefaultRegisterer. If the registration fails, NewCounter panics.
 requires opts.ConstLabels != nil ==> acc(opts.ConstLabels)
 ensures  c.Mem()
+decreases _
 func NewCounter(opts prometheus.CounterOpts) (c prometheus.Counter)
 
 
@@ -33,13 +34,15 @@ func NewCounter(opts prometheus.CounterOpts) (c prometheus.Counter)
 requires opts.ConstLabels != nil ==> acc(opts.ConstLabels)
 requires forall i int :: 0 <= i && i < len(labelNames) ==> acc(&labelNames[i])
 ensures  c.Mem()
+decreases _
 func NewCounterVec(opts prometheus.CounterOpts, labelNames []string) (c *prometheus.CounterVec)
 
 // NewGauge works like the function of the same name in the prometheus package
 // but it automatically registers the Gauge with the
 // prometheus.DefaultRegisterer. If the registration fails, NewGauge panics.
 requires opts.ConstLabels != nil ==> acc(opts.ConstLabels)
 ensures  g.Mem()
+decreases _
 func NewGauge(opts prometheus.GaugeOpts) (g prometheus.Gauge)
 
 // NewGaugeVec works like the function of the same name in the prometheus
@@ -48,4 +51,5 @@ func NewGauge(opts prometheus.GaugeOpts) (g prometheus.Gauge)
 requires opts.ConstLabels != nil ==> acc(opts.ConstLabels)
 requires forall i int :: 0 <= i && i < len(labelNames) ==> acc(&labelNames[i])
 ensures  g.Mem()
+decreases _
 func NewGaugeVec(opts prometheus.GaugeOpts, labelNames []string) (g *prometheus.GaugeVec)

gobra/lib/addr/host.gobra

@@ -475,6 +475,7 @@ func (h HostSVC) Multicast() HostSVC {
 	return h | HostSVC(SVCMcast)
 }
 
+decreases
 ensures res.Mem()
 decreases
 func (h HostSVC) Copy() (res HostAddr) {

gobra/lib/addr/isdas.gobra

@@ -51,6 +51,7 @@ const (
 type ISD uint16
 
 // ISDFromString parses an ISD from a decimal string.
+decreases
 func ISDFromString(s string) (ISD, error) {
 	isd, err := strconv.ParseUint(s, 10, ISDBits)
 	if err != nil {
@@ -65,6 +66,7 @@ func ISDFromString(s string) (ISD, error) {
 
 // ISDFromFileFmt parses an ISD from a file-format string. If prefix is true,
 // an 'ISD' prefix is expected and stripped before parsing.
+decreases
 func ISDFromFileFmt(s string, prefix bool) (ISD, error) {
 	if prefix {
 		if !strings.HasPrefix(s, ISDFmtPrefix) {
@@ -92,20 +94,23 @@ func (isd ISD) String() string {
 type AS uint64
 
 ghost
+decreases
 pure func validAS(s string) bool
 
 // ASFromString parses an AS from a decimal (in the case of the 32bit BGP AS
 // number space) or ipv6-style hex (in the case of SCION-only AS numbers)
 // string.
 ensures validAS(s) ==> err == nil
 ensures !validAS(s) ==> err != nil
+decreases
 func ASFromString(s string) (as AS, err error) {
 	return asParse(s, ":")
 }
 
 // ASFromFileFmt parses an AS from a file-format string. This is the same
 // format as ASFromString expects, with ':' replaced by '_'. If prefix is true,
 // an 'AS' prefix is expected and stripped before parsing.
+decreases
 func ASFromFileFmt(s string, prefix bool) (AS, error) {
 	if prefix {
 		if !strings.HasPrefix(s, ASFmtPrefix) {
@@ -120,6 +125,7 @@ func ASFromFileFmt(s string, prefix bool) (AS, error) {
 
 ensures validAS(s) ==> resErr == nil
 ensures !validAS(s) ==> resErr != nil
+decreases
 func asParse(s string, sep string) (resAS AS, resErr error) {
 	if strings.Index(s, sep) == -1 {
 		// Must be a BGP AS, parse as 32-bit decimal number
@@ -146,6 +152,7 @@ func asParse(s string, sep string) (resAS AS, resErr error) {
 
 	invariant 0 <= i && i <= asParts
 	invariant forall j int :: 0 <= j && j < len(parts) ==> acc(&parts[j])
+	decreases asParts - i
 	for i := 0; i < asParts; i++ {
 		// (joao) leads to error, types not comptabile with >>. Currently rewritten.
 		// as <<= asPartBits
@@ -178,6 +185,7 @@ func (as AS) FileFmt() string //{
 //	return as.fmt('_')
 //}
 
+decreases
 func (as AS) fmt(sep byte) string {
 	if !as.inRange() {
 		// (joao) fmt not currently supported
@@ -198,6 +206,7 @@ func (as AS) fmt(sep byte) string {
 	b := make([]byte, 0, maxLen)
 
 	invariant forall i int :: 0 <= i && i < len(b) ==> acc(&b[i])
+	decreases asParts - i
 	for i := 0; i < asParts; i++ {
 		if i > 0 {
 			b = append(perm(1/2), b, sep)
@@ -219,6 +228,7 @@ func (as AS) inRange() bool {
 	return as <= MaxAS
 }
 
+decreases
 func (as AS) MarshalText() ([]byte, error) {
 	if !as.inRange() {
 		// (joao) added cast to common.ErrMsg around string, otherwise leads to type error
@@ -233,6 +243,7 @@ requires forall i int :: 0 <= i && i < len(text) ==> acc(&text[i])
 ensures acc(as)
 ensures forall i int :: 0 <= i && i < len(text) ==> acc(&text[i])
 ensures !validAS(string(text)) ==> *as == old(*as)
+decreases
 func (as *AS) UnmarshalText(text []byte) error {
 	newAS, err := ASFromString(string(text))
 	if err != nil {
@@ -262,6 +273,7 @@ func IAFromRaw(b common.RawBytes) (ret IA) {
 }
 
 // IAFromString parses an IA from a string of the format 'ia-as'.
+decreases
 func IAFromString(s string) (IA, error) {
 	parts := strings.Split(s, "-")
 	if len(parts) != 2 {
@@ -281,6 +293,7 @@ func IAFromString(s string) (IA, error) {
 }
 
 // IAFromFileFmt parses an IA from a file-format
+decreases
 func IAFromFileFmt(s string, prefixes bool) (IA, error) {
 	parts := strings.Split(s, "-")
 	if len(parts) != 2 {
@@ -307,6 +320,7 @@ func (ia IA) MarshalText() ([]byte, error) {
 // UnmarshalText allows IA to be used as a map key in JSON.
 preserves acc(ia)
 preserves forall i int :: 0 <= i && i < len(text) ==> acc(&text[i], 1/1000)
+decreases
 func (ia *IA) UnmarshalText(text []byte) error {
 	if len(text) == 0 {
 		*ia = IA{}
@@ -353,6 +367,7 @@ func (ia IA) Equal(other IA) bool {
 }
 
 // IsWildcard returns whether the ia has a wildcard part (isd or as).
+decreases
 func (ia IA) IsWildcard() bool {
 	return ia.I == 0 || ia.A == 0
 }
@@ -378,6 +393,7 @@ func (ia IA) FileFmt(prefixes bool) string {
 // (joao) may be simplified, only requires acc(ia) if IAFromString leads to nil error
 requires acc(ia)
 ensures acc(ia)
+decreases
 func (ia *IA) Set(s string) error {
 	pIA, err := IAFromString(s)
 	if err != nil {
@@ -413,6 +429,7 @@ func (ia IAInt) MarshalText() (res []byte, e error) {
 
 preserves acc(ia)
 preserves forall i int :: 0 <= i && i < len(b) ==> acc(&b[i], 1/1000)
+decreases
 func (ia *IAInt) UnmarshalText(b []byte) error {
 	tIA, err := IAFromString(string(b))
 	if err != nil {

gobra/lib/common/I4.gobra

@@ -37,6 +37,7 @@ const (
 //	L4SCMP: true, L4TCP: true, L4UDP: true,
 //}
 
+decreases
 func (p L4ProtocolType) String() string {
 	switch p {
 	case L4None:

gobra/lib/common/errors.gobra

@@ -42,6 +42,7 @@ type ErrorNester interface {
 
 // GetNestedError returns the nested error, if any. Returns nil otherwise.
 // (joao) trusted function
+decreases _
 func GetNestedError(e error) error // {
 //	if n, _ := e.(ErrorNester); n != nil {
 //		return n.GetErr()
@@ -59,6 +60,7 @@ type Temporary interface {
 // IsTemporaryErr determines if e is a temporary Error. As a fall-back, if e implements ErrorNester,
 // IsTemporaryErr recurses on the nested error. Otherwise returns false.
 // (joao) trusted function
+decreases _
 func IsTemporaryErr(e error) bool // {
 //	if t, _ := e.(Temporary); t != nil {
 //		return t.Temporary()
@@ -79,6 +81,7 @@ type Timeout interface {
 // IsTimeoutErr determines if e is a temporary Error. As a fall-back, if e implements ErrorNester,
 // IsTimeoutErr recurses on the nested error. Otherwise returns false.
 // (joao) trusted function
+decreases _
 func IsTimeoutErr(e error) bool // {
 //	if t, _ := e.(Timeout); t != nil {
 //		return t.Timeout()
@@ -93,6 +96,7 @@ func IsTimeoutErr(e error) bool // {
 // used for Is checking in the calling code.
 type ErrMsg string
 
+decreases
 func (e ErrMsg) Error() string {
 	return string(e)
 }
@@ -115,6 +119,7 @@ type BasicError struct {
 // Is returns whether this error is the same error as err, or in case err is a
 // ErrMsg whether the message is equal.
 // (joao) trusted function
+decreases
 func (be BasicError) Is(err error) bool // {
 //	switch other := err.(type) {
 //	case BasicError:
@@ -127,6 +132,7 @@ func (be BasicError) Is(err error) bool // {
 //}
 
 // Unwrap returns the next error in the error chain, or nil if there is none.
+decreases
 func (be BasicError) Unwrap() error {
 	return be.GetErr()
 }
@@ -136,12 +142,14 @@ func (be BasicError) Unwrap() error {
 // information: 'msg' argument itself should be a constant string.
 // (joao) trusted function
 ensures res != nil
+decreases _
 func NewBasicError(msg ErrMsg, e error, logCtx ...interface{}) (res error) // {
 // (joao) not supported while variadic functionas are not merged in Gobra's master
 //	return BasicError{Msg: msg, logCtx: logCtx, Err: e}
 // }
 
 // (joao) trusted function
+decreases _
 func (be BasicError) TopError() string // {
 //	s := make([]string, 0, 1+(len(be.logCtx)/2))
 //	s = append(s, string(be.Msg))
@@ -152,14 +160,17 @@ func (be BasicError) TopError() string // {
 //	return strings.Join(s, " ")
 //}
 
+decreases
 func (be BasicError) Error() string {
 	return FmtError(be)
 }
 
+decreases
 func (be BasicError) GetMsg() string {
 	return string(be.Msg)
 }
 
+decreases
 func (be BasicError) GetErr() error {
 	return be.Err
 }
@@ -169,6 +180,7 @@ type MultiError []error
 
 // ToError returns the object as error interface implementation.
 // (joao) trusted function
+decreases _
 func (be MultiError) ToError() error // {
 //	if len(be) == 0 {
 //		return nil
@@ -179,13 +191,16 @@ func (be MultiError) ToError() error // {
 // multiError is the internal error interface implementation of MultiError.
 type multiError []error
 
+preserves forall i int :: 0 <= i && i < len(be) ==> acc(&be[i], 1/10)
+decreases
 func (be multiError) Error() string {
 	return FmtErrors(be)
 }
 
 // FmtError formats e for logging. It walks through all nested errors, putting each on a new line,
 // and indenting multi-line errors.
 // (joao) trusted function
+decreases _
 func FmtError(e error) string // {
 //	var s, ns []string
 //	for {
@@ -200,7 +215,7 @@ func FmtError(e error) string // {
 //}
 
 // (joao) trusted function
-func innerFmtError(e error) ([]string, error) // {
+// func innerFmtError(e error) ([]string, error) {
 //	var s []string
 //	var lines []string
 //	switch e := e.(type) {
@@ -227,6 +242,8 @@ func innerFmtError(e error) ([]string, error) // {
 
 // FmtErrors formats a slice of errors for logging.
 // (joao) trusted function
+preserves forall i int :: 0 <= i && i < len(es) ==> acc(&es[i], 1/10)
+decreases _
 func FmtErrors(es []error) string // {
 //	s := make([]string, 0, len(es))
 //	for _, e := range es {