From 4f88e97bf73023085f7829a75c962428d9e2c107 Mon Sep 17 00:00:00 2001 From: henriman Date: Sat, 1 Feb 2025 15:27:13 +0100 Subject: [PATCH 01/12] Add minimum annotations to verify private/topology --- private/topology/linktype.go | 20 +++++++++++++++++--- verification/utils/slices/slices.gobra | 10 ++++++++++ 2 files changed, 27 insertions(+), 3 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index d8b47579f..30ac5ee32 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -44,6 +44,7 @@ const ( Peer LinkType = 4 ) +// @ requires low(l) // @ decreases func (l LinkType) String() string { if l == Unset { @@ -59,17 +60,23 @@ func (l LinkType) String() string { // LinkTypeFromString returns the numerical link type associated with a string description. If the // string is not recognized, an Unset link type is returned. The matching is case-insensitive. +// @ requires low(s) // @ decreases func LinkTypeFromString(s string) (res LinkType) { var l /*@@@*/ LinkType tmp := []byte(s) - //@ fold sl.Bytes(tmp, 0, len(tmp)) + // SIF: For now I have to make this assumption, see Gobra issue #831 + // Note that we can already infer low(len(tmp)), as the lengths are related + // in the Viper encoding, but not the contents. + //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ fold sl.LowBytes(tmp, 0, len(tmp)) if err := l.UnmarshalText(tmp); err != nil { return Unset } return l } +// @ requires low(l) // @ ensures (l == Core || l == Parent || l == Child || l == Peer) == (err == nil) // @ ensures err == nil ==> sl.Bytes(res, 0, len(res)) // @ ensures err != nil ==> err.ErrorMem() @@ -97,13 +104,20 @@ func (l LinkType) MarshalText() (res []byte, err error) { } } +// SIF: For now I assume that low(len(data)) and sl.LowBytes... suffice to infer +// that string(data) is low. See Gobra issue #832 +// @ requires low(len(data)) +// @ requires acc(sl.LowBytes(data, 0, len(data)), R15) // @ preserves acc(l) -// @ preserves acc(sl.Bytes(data, 0, len(data)), R15) +// @ ensures acc(sl.Bytes(data, 0, len(data)), R15) // @ ensures err != nil ==> err.ErrorMem() +// @ ensures low(err) // @ decreases func (l *LinkType) UnmarshalText(data []byte) (err error) { - //@ unfold acc(sl.Bytes(data, 0, len(data)), R15) + //@ unfold acc(sl.LowBytes(data, 0, len(data)), R15) //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R15) + // SIF: For now I have to make this assumption, see Gobra issue #832 + //@ assume low(string(data)) switch strings.ToLower(string(data)) { case "core": *l = Core diff --git a/verification/utils/slices/slices.gobra b/verification/utils/slices/slices.gobra index 8c7c4ac15..f89de81f5 100644 --- a/verification/utils/slices/slices.gobra +++ b/verification/utils/slices/slices.gobra @@ -32,6 +32,16 @@ pred Bytes(s []byte, start int, end int) { forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) } +// SIF: `Bytes` with the addition of asserting the elements to be low. +pred LowBytes(s []byte, start int, end int) { + // start inclusive + 0 <= start && + start <= end && + // end exclusive + end <= cap(s) && + forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) && low(s[i]) +} + pure requires acc(Bytes(s, start, end), _) requires start <= i && i < end From c8b7b5ccf2a390b0b822eeb6c667dbfa3aea9d30 Mon Sep 17 00:00:00 2001 From: henriman Date: Sat, 1 Feb 2025 16:20:08 +0100 Subject: [PATCH 02/12] Add appropriate postconditions to private/topology As for private/topology/underlay, I have added these to make the contracts more precise, as I anticipate I will need this for further verification Note that at the moment, we still need a lot of `assume` statements due to Gobra issues #831 and #832. Also, `LinkType.String` doesn't have an appropriate postcondition yet, as I couldn't assert (nor assume) low(err.Error()) for a low `err`. --- private/topology/linktype.go | 33 +++++++++++++++++++++++++-------- 1 file changed, 25 insertions(+), 8 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 30ac5ee32..0512408a4 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -45,8 +45,9 @@ const ( ) // @ requires low(l) +// SIF: I cannot assert low(res) yet bc. I can't assert (nor assume) low(err.Error()) in if-block // @ decreases -func (l LinkType) String() string { +func (l LinkType) String() (res string) { if l == Unset { return "unset" } @@ -54,13 +55,15 @@ func (l LinkType) String() string { if err != nil { return err.Error() } - //@ unfold sl.Bytes(s, 0, len(s)) + //@ unfold sl.LowBytes(s, 0, len(s)) + //@ assume low(string(s)) return string(s) } // LinkTypeFromString returns the numerical link type associated with a string description. If the // string is not recognized, an Unset link type is returned. The matching is case-insensitive. // @ requires low(s) +// @ ensures low(res) // @ decreases func LinkTypeFromString(s string) (res LinkType) { var l /*@@@*/ LinkType @@ -78,26 +81,37 @@ func LinkTypeFromString(s string) (res LinkType) { // @ requires low(l) // @ ensures (l == Core || l == Parent || l == Child || l == Peer) == (err == nil) -// @ ensures err == nil ==> sl.Bytes(res, 0, len(res)) +// @ ensures err == nil ==> sl.LowBytes(res, 0, len(res)) // @ ensures err != nil ==> err.ErrorMem() +// SIF: To make the postconditions as precise as possible, I have not put this +// assertion behind `err == nil` or `err != nil` (resp.) +// Only for LowBytes(...) I have, as that only makes sense when `res != nil`, +// and I have added `low(res)` for `err != nil` appropriately. +// @ ensures low(len(res)) && low(err) +// @ ensures err != nil ==> low(res) // @ decreases func (l LinkType) MarshalText() (res []byte, err error) { switch l { case Core: tmp := []byte("core") - //@ fold sl.Bytes(tmp, 0, len(tmp)) + // SIF: ATM we need this assumption, see Gobra issue #831 + //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ fold sl.LowBytes(tmp, 0, len(tmp)) return tmp, nil case Parent: tmp := []byte("parent") - //@ fold sl.Bytes(tmp, 0, len(tmp)) + //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ fold sl.LowBytes(tmp, 0, len(tmp)) return tmp, nil case Child: tmp := []byte("child") - //@ fold sl.Bytes(tmp, 0, len(tmp)) + //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ fold sl.LowBytes(tmp, 0, len(tmp)) return tmp, nil case Peer: tmp := []byte("peer") - //@ fold sl.Bytes(tmp, 0, len(tmp)) + //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ fold sl.LowBytes(tmp, 0, len(tmp)) return tmp, nil default: return nil, serrors.New("invalid link type") @@ -110,7 +124,10 @@ func (l LinkType) MarshalText() (res []byte, err error) { // @ requires acc(sl.LowBytes(data, 0, len(data)), R15) // @ preserves acc(l) // @ ensures acc(sl.Bytes(data, 0, len(data)), R15) -// @ ensures err != nil ==> err.ErrorMem() +// @ ensures err != nil ==> err.ErrorMem() +// SIF: As *l remains unchanged if err != nil, and we don't know if low(*l) before +// @ ensures err == nil ==> low(*l) +// SIF: We need `low(err)` regardless of `err ?= nil` as we use it in branch conditions. // @ ensures low(err) // @ decreases func (l *LinkType) UnmarshalText(data []byte) (err error) { From 9863f30e556cbd77e6287acf22a66a6b7e98c475 Mon Sep 17 00:00:00 2001 From: henriman Date: Sun, 2 Feb 2025 00:40:08 +0100 Subject: [PATCH 03/12] Add assumption due to Gobra issue #835 --- private/topology/linktype.go | 3 +++ 1 file changed, 3 insertions(+) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 0512408a4..82b777e8c 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -145,6 +145,9 @@ func (l *LinkType) UnmarshalText(data []byte) (err error) { case "peer": *l = Peer default: + // SIF: See Gobra issue #835 for why this assumption is currently necessary + //@ ghost errCtx := []interface{}{"linkType", string(data)} + //@ assume forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> acc(&errCtx[i]) && low(errCtx[i]) return serrors.New("invalid link type", "linkType", string(data)) } return nil From 82831930fed56657f5e0dca488bc8292d2f0b578 Mon Sep 17 00:00:00 2001 From: henriman Date: Fri, 14 Feb 2025 12:22:36 +0100 Subject: [PATCH 04/12] Introduce functions to express assumptions Together with the assumptions, I also moved `LowBytes` to a dedicated folder: `verification/util/sif` --- private/topology/linktype.go | 31 ++++++++++++------------ verification/utils/sif/assumptions.gobra | 11 +++++++++ verification/utils/sif/definitions.gobra | 17 +++++++++++++ verification/utils/slices/slices.gobra | 10 -------- 4 files changed, 43 insertions(+), 26 deletions(-) create mode 100644 verification/utils/sif/assumptions.gobra create mode 100644 verification/utils/sif/definitions.gobra diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 82b777e8c..b86e21140 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -23,6 +23,7 @@ import ( "github.com/scionproto/scion/pkg/private/serrors" //@ . "github.com/scionproto/scion/verification/utils/definitions" //@ sl "github.com/scionproto/scion/verification/utils/slices" + //@ "github.com/scionproto/scion/verification/utils/sif" ) // LinkType describes inter-AS links. @@ -45,7 +46,8 @@ const ( ) // @ requires low(l) -// SIF: I cannot assert low(res) yet bc. I can't assert (nor assume) low(err.Error()) in if-block +// SIF: If I wanted to assert `low(res)`, I would need to annotate `error.Error` +// in `builtin.gobra`. // @ decreases func (l LinkType) String() (res string) { if l == Unset { @@ -55,8 +57,8 @@ func (l LinkType) String() (res string) { if err != nil { return err.Error() } - //@ unfold sl.LowBytes(s, 0, len(s)) - //@ assume low(string(s)) + //@ unfold sif.LowBytes(s, 0, len(s)) + //@ sif.AssumeLowSliceToLowString(s, 1/1) return string(s) } @@ -71,8 +73,8 @@ func LinkTypeFromString(s string) (res LinkType) { // SIF: For now I have to make this assumption, see Gobra issue #831 // Note that we can already infer low(len(tmp)), as the lengths are related // in the Viper encoding, but not the contents. - //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sl.LowBytes(tmp, 0, len(tmp)) + //@ assume forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ fold sif.LowBytes(tmp, 0, len(tmp)) if err := l.UnmarshalText(tmp); err != nil { return Unset } @@ -81,7 +83,7 @@ func LinkTypeFromString(s string) (res LinkType) { // @ requires low(l) // @ ensures (l == Core || l == Parent || l == Child || l == Peer) == (err == nil) -// @ ensures err == nil ==> sl.LowBytes(res, 0, len(res)) +// @ ensures err == nil ==> sif.LowBytes(res, 0, len(res)) // @ ensures err != nil ==> err.ErrorMem() // SIF: To make the postconditions as precise as possible, I have not put this // assertion behind `err == nil` or `err != nil` (resp.) @@ -96,32 +98,30 @@ func (l LinkType) MarshalText() (res []byte, err error) { tmp := []byte("core") // SIF: ATM we need this assumption, see Gobra issue #831 //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sl.LowBytes(tmp, 0, len(tmp)) + //@ fold sif.LowBytes(tmp, 0, len(tmp)) return tmp, nil case Parent: tmp := []byte("parent") //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sl.LowBytes(tmp, 0, len(tmp)) + //@ fold sif.LowBytes(tmp, 0, len(tmp)) return tmp, nil case Child: tmp := []byte("child") //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sl.LowBytes(tmp, 0, len(tmp)) + //@ fold sif.LowBytes(tmp, 0, len(tmp)) return tmp, nil case Peer: tmp := []byte("peer") //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sl.LowBytes(tmp, 0, len(tmp)) + //@ fold sif.LowBytes(tmp, 0, len(tmp)) return tmp, nil default: return nil, serrors.New("invalid link type") } } -// SIF: For now I assume that low(len(data)) and sl.LowBytes... suffice to infer -// that string(data) is low. See Gobra issue #832 // @ requires low(len(data)) -// @ requires acc(sl.LowBytes(data, 0, len(data)), R15) +// @ requires acc(sif.LowBytes(data, 0, len(data)), R15) // @ preserves acc(l) // @ ensures acc(sl.Bytes(data, 0, len(data)), R15) // @ ensures err != nil ==> err.ErrorMem() @@ -131,10 +131,9 @@ func (l LinkType) MarshalText() (res []byte, err error) { // @ ensures low(err) // @ decreases func (l *LinkType) UnmarshalText(data []byte) (err error) { - //@ unfold acc(sl.LowBytes(data, 0, len(data)), R15) + //@ unfold acc(sif.LowBytes(data, 0, len(data)), R15) //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R15) - // SIF: For now I have to make this assumption, see Gobra issue #832 - //@ assume low(string(data)) + //@ sif.AssumeLowSliceToLowString(data, R15) switch strings.ToLower(string(data)) { case "core": *l = Core diff --git a/verification/utils/sif/assumptions.gobra b/verification/utils/sif/assumptions.gobra new file mode 100644 index 000000000..daa742bd8 --- /dev/null +++ b/verification/utils/sif/assumptions.gobra @@ -0,0 +1,11 @@ +// +gobra + +package sif + +// SIF: See Gobra issue #832 +ghost +requires p > 0 && acc(b, p) +requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) ==> low(b[i]) +ensures acc(b, p) && low(string(b)) +decreases +func AssumeLowSliceToLowString(b []byte, p perm) diff --git a/verification/utils/sif/definitions.gobra b/verification/utils/sif/definitions.gobra new file mode 100644 index 000000000..8a045118b --- /dev/null +++ b/verification/utils/sif/definitions.gobra @@ -0,0 +1,17 @@ +// +gobra + +package sif + +// SIF: `slices.Bytes` with the addition of asserting the elements to be low. +// TODO: I might want to eventually decouple this from access permissions +// and put sensitivity in a pure Boolean function +pred LowBytes(s []byte, start int, end int) { + // start inclusive + 0 <= start && + start <= end && + // end exclusive + end <= cap(s) && + // SIF: Might be useful in the future + // low(end - start) && + forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) && low(s[i]) +} \ No newline at end of file diff --git a/verification/utils/slices/slices.gobra b/verification/utils/slices/slices.gobra index f89de81f5..8c7c4ac15 100644 --- a/verification/utils/slices/slices.gobra +++ b/verification/utils/slices/slices.gobra @@ -32,16 +32,6 @@ pred Bytes(s []byte, start int, end int) { forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) } -// SIF: `Bytes` with the addition of asserting the elements to be low. -pred LowBytes(s []byte, start int, end int) { - // start inclusive - 0 <= start && - start <= end && - // end exclusive - end <= cap(s) && - forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) && low(s[i]) -} - pure requires acc(Bytes(s, start, end), _) requires start <= i && i < end From 01950a7d4661aa4243286837c01a511f8638b89e Mon Sep 17 00:00:00 2001 From: henriman Date: Thu, 13 Mar 2025 11:32:12 +0100 Subject: [PATCH 05/12] Fix typo --- pkg/slayers/scion_spec.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 1b45a2896..e45ae6064 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -441,7 +441,7 @@ pure func (s *SCION) ValidScionInitSpec(ub []byte) bool { let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in let high := s.HdrLen*LineLen in typeOf(s.Path) == (*scion.Raw) && - s.Path.(*scion.Raw).GetBase(ub[low__:high]).WeaklyValid() + s.Path.(*scion.Raw).GetBase(ub[low_:high]).WeaklyValid() } // Checks if the common path header is valid in the serialized scion packet. From 1e0500bd816959aa82570f4711e6eb48566f1999 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 14 Apr 2025 13:35:48 +0200 Subject: [PATCH 06/12] Clean up --- private/topology/linktype.go | 55 ++++++++++++------------ verification/utils/sif/assumptions.gobra | 2 +- verification/utils/sif/definitions.gobra | 17 -------- 3 files changed, 28 insertions(+), 46 deletions(-) delete mode 100644 verification/utils/sif/definitions.gobra diff --git a/private/topology/linktype.go b/private/topology/linktype.go index b86e21140..a276265e9 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -46,10 +46,8 @@ const ( ) // @ requires low(l) -// SIF: If I wanted to assert `low(res)`, I would need to annotate `error.Error` -// in `builtin.gobra`. // @ decreases -func (l LinkType) String() (res string) { +func (l LinkType) String() string { if l == Unset { return "unset" } @@ -57,8 +55,7 @@ func (l LinkType) String() (res string) { if err != nil { return err.Error() } - //@ unfold sif.LowBytes(s, 0, len(s)) - //@ sif.AssumeLowSliceToLowString(s, 1/1) + //@ unfold sl.Bytes(s, 0, len(s)) return string(s) } @@ -70,11 +67,9 @@ func (l LinkType) String() (res string) { func LinkTypeFromString(s string) (res LinkType) { var l /*@@@*/ LinkType tmp := []byte(s) - // SIF: For now I have to make this assumption, see Gobra issue #831 - // Note that we can already infer low(len(tmp)), as the lengths are related - // in the Viper encoding, but not the contents. + // TODO: Once Gobra issue #831 is resolved, remove this assumption. //@ assume forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sif.LowBytes(tmp, 0, len(tmp)) + //@ fold sl.Bytes(tmp, 0, len(tmp)) if err := l.UnmarshalText(tmp); err != nil { return Unset } @@ -83,56 +78,60 @@ func LinkTypeFromString(s string) (res LinkType) { // @ requires low(l) // @ ensures (l == Core || l == Parent || l == Child || l == Peer) == (err == nil) -// @ ensures err == nil ==> sif.LowBytes(res, 0, len(res)) +// @ ensures err == nil ==> sl.Bytes(res, 0, len(res)) +// @ ensures err == nil ==> low(len(res)) && +// @ forall i int :: { sl.GetByte(res, 0, len(res), i) } 0 <= i && i < len(res) ==> +// @ low(sl.GetByte(res, 0, len(res), i)) // @ ensures err != nil ==> err.ErrorMem() -// SIF: To make the postconditions as precise as possible, I have not put this -// assertion behind `err == nil` or `err != nil` (resp.) -// Only for LowBytes(...) I have, as that only makes sense when `res != nil`, -// and I have added `low(res)` for `err != nil` appropriately. -// @ ensures low(len(res)) && low(err) -// @ ensures err != nil ==> low(res) +// @ ensures low(err != nil) // @ decreases func (l LinkType) MarshalText() (res []byte, err error) { switch l { case Core: tmp := []byte("core") - // SIF: ATM we need this assumption, see Gobra issue #831 + // TODO: Once Gobra issue #831 is resolved, remove this assumption. //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sif.LowBytes(tmp, 0, len(tmp)) + //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil case Parent: tmp := []byte("parent") + // TODO: Once Gobra issue #831 is resolved, remove this assumption. //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sif.LowBytes(tmp, 0, len(tmp)) + //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil case Child: tmp := []byte("child") + // TODO: Once Gobra issue #831 is resolved, remove this assumption. //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sif.LowBytes(tmp, 0, len(tmp)) + //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil case Peer: tmp := []byte("peer") + // TODO: Once Gobra issue #831 is resolved, remove this assumption. //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) - //@ fold sif.LowBytes(tmp, 0, len(tmp)) + //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil default: return nil, serrors.New("invalid link type") } } -// @ requires low(len(data)) -// @ requires acc(sif.LowBytes(data, 0, len(data)), R15) +// @ requires acc(sl.Bytes(data, 0, len(data)), R15) +// @ requires low(len(data)) && +// @ forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) ==> +// @ low(sl.GetByte(data, 0, len(data), i)) // @ preserves acc(l) // @ ensures acc(sl.Bytes(data, 0, len(data)), R15) // @ ensures err != nil ==> err.ErrorMem() -// SIF: As *l remains unchanged if err != nil, and we don't know if low(*l) before // @ ensures err == nil ==> low(*l) -// SIF: We need `low(err)` regardless of `err ?= nil` as we use it in branch conditions. -// @ ensures low(err) +// @ ensures low(err != nil) // @ decreases func (l *LinkType) UnmarshalText(data []byte) (err error) { - //@ unfold acc(sif.LowBytes(data, 0, len(data)), R15) + //@ BeforeUnfold: + //@ unfold acc(sl.Bytes(data, 0, len(data)), R15) //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R15) + //@ assert forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) ==> + //@ old[BeforeUnfold](sl.GetByte(data, 0, len(data), i)) == data[i] //@ sif.AssumeLowSliceToLowString(data, R15) switch strings.ToLower(string(data)) { case "core": @@ -144,7 +143,7 @@ func (l *LinkType) UnmarshalText(data []byte) (err error) { case "peer": *l = Peer default: - // SIF: See Gobra issue #835 for why this assumption is currently necessary + // TODO: Once Gobra issue #835/#890 is resolved, remove this assumption. //@ ghost errCtx := []interface{}{"linkType", string(data)} //@ assume forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> acc(&errCtx[i]) && low(errCtx[i]) return serrors.New("invalid link type", "linkType", string(data)) diff --git a/verification/utils/sif/assumptions.gobra b/verification/utils/sif/assumptions.gobra index daa742bd8..33f20918d 100644 --- a/verification/utils/sif/assumptions.gobra +++ b/verification/utils/sif/assumptions.gobra @@ -2,7 +2,7 @@ package sif -// SIF: See Gobra issue #832 +// TODO: Once Gobra issue #832 is resolved, introduce body and prove this. ghost requires p > 0 && acc(b, p) requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) ==> low(b[i]) diff --git a/verification/utils/sif/definitions.gobra b/verification/utils/sif/definitions.gobra deleted file mode 100644 index 8a045118b..000000000 --- a/verification/utils/sif/definitions.gobra +++ /dev/null @@ -1,17 +0,0 @@ -// +gobra - -package sif - -// SIF: `slices.Bytes` with the addition of asserting the elements to be low. -// TODO: I might want to eventually decouple this from access permissions -// and put sensitivity in a pure Boolean function -pred LowBytes(s []byte, start int, end int) { - // start inclusive - 0 <= start && - start <= end && - // end exclusive - end <= cap(s) && - // SIF: Might be useful in the future - // low(end - start) && - forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) && low(s[i]) -} \ No newline at end of file From 29e7444b2908f72810d22ada938b93fbec598d7c Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 14 Apr 2025 13:44:41 +0200 Subject: [PATCH 07/12] Rename `AssumeLowSliceToLowString` to `LowSliceImpliesLowString` --- private/topology/linktype.go | 2 +- verification/utils/sif/assumptions.gobra | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index a276265e9..8c32a1a1e 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -132,7 +132,7 @@ func (l *LinkType) UnmarshalText(data []byte) (err error) { //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R15) //@ assert forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) ==> //@ old[BeforeUnfold](sl.GetByte(data, 0, len(data), i)) == data[i] - //@ sif.AssumeLowSliceToLowString(data, R15) + //@ sif.LowSliceImpliesLowString(data, R15) switch strings.ToLower(string(data)) { case "core": *l = Core diff --git a/verification/utils/sif/assumptions.gobra b/verification/utils/sif/assumptions.gobra index 33f20918d..8a612bee3 100644 --- a/verification/utils/sif/assumptions.gobra +++ b/verification/utils/sif/assumptions.gobra @@ -8,4 +8,4 @@ requires p > 0 && acc(b, p) requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) ==> low(b[i]) ensures acc(b, p) && low(string(b)) decreases -func AssumeLowSliceToLowString(b []byte, p perm) +func LowSliceImpliesLowString(b []byte, p perm) From 8f3c41c7e381bb8b844c41f8fff1359e58c461fa Mon Sep 17 00:00:00 2001 From: henriman Date: Wed, 2 Jul 2025 13:25:12 +0200 Subject: [PATCH 08/12] Remove workaround for Gobra issue #835/#890 Due to the change in the contract of serrors, the workaround is not necessary anymore --- private/topology/linktype.go | 3 --- 1 file changed, 3 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 8c32a1a1e..836d0df45 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -143,9 +143,6 @@ func (l *LinkType) UnmarshalText(data []byte) (err error) { case "peer": *l = Peer default: - // TODO: Once Gobra issue #835/#890 is resolved, remove this assumption. - //@ ghost errCtx := []interface{}{"linkType", string(data)} - //@ assume forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> acc(&errCtx[i]) && low(errCtx[i]) return serrors.New("invalid link type", "linkType", string(data)) } return nil From ceacce81d45219d2a80efe0555da527bed6818de Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 12 Aug 2025 13:57:51 +0200 Subject: [PATCH 09/12] Address PR feedback and add `&& low(i) ==>` --- private/topology/linktype.go | 31 ++++++------------------ verification/utils/sif/assumptions.gobra | 2 +- 2 files changed, 9 insertions(+), 24 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 836d0df45..81f99e6a1 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -62,13 +62,12 @@ func (l LinkType) String() string { // LinkTypeFromString returns the numerical link type associated with a string description. If the // string is not recognized, an Unset link type is returned. The matching is case-insensitive. // @ requires low(s) -// @ ensures low(res) // @ decreases func LinkTypeFromString(s string) (res LinkType) { var l /*@@@*/ LinkType tmp := []byte(s) // TODO: Once Gobra issue #831 is resolved, remove this assumption. - //@ assume forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) + //@ assume forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) && low(i) ==> low(tmp[i]) //@ fold sl.Bytes(tmp, 0, len(tmp)) if err := l.UnmarshalText(tmp); err != nil { return Unset @@ -79,36 +78,24 @@ func LinkTypeFromString(s string) (res LinkType) { // @ requires low(l) // @ ensures (l == Core || l == Parent || l == Child || l == Peer) == (err == nil) // @ ensures err == nil ==> sl.Bytes(res, 0, len(res)) -// @ ensures err == nil ==> low(len(res)) && -// @ forall i int :: { sl.GetByte(res, 0, len(res), i) } 0 <= i && i < len(res) ==> -// @ low(sl.GetByte(res, 0, len(res), i)) // @ ensures err != nil ==> err.ErrorMem() -// @ ensures low(err != nil) // @ decreases func (l LinkType) MarshalText() (res []byte, err error) { switch l { case Core: tmp := []byte("core") - // TODO: Once Gobra issue #831 is resolved, remove this assumption. - //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil case Parent: tmp := []byte("parent") - // TODO: Once Gobra issue #831 is resolved, remove this assumption. - //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil case Child: tmp := []byte("child") - // TODO: Once Gobra issue #831 is resolved, remove this assumption. - //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil case Peer: tmp := []byte("peer") - // TODO: Once Gobra issue #831 is resolved, remove this assumption. - //@ assume forall i int :: { tmp[i] } 0 <= i && i < len(tmp) ==> low(tmp[i]) //@ fold sl.Bytes(tmp, 0, len(tmp)) return tmp, nil default: @@ -118,21 +105,19 @@ func (l LinkType) MarshalText() (res []byte, err error) { // @ requires acc(sl.Bytes(data, 0, len(data)), R15) // @ requires low(len(data)) && -// @ forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) ==> -// @ low(sl.GetByte(data, 0, len(data), i)) +// @ forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) && low(i) ==> +// @ low(sl.GetByte(data, 0, len(data), i)) // @ preserves acc(l) // @ ensures acc(sl.Bytes(data, 0, len(data)), R15) // @ ensures err != nil ==> err.ErrorMem() -// @ ensures err == nil ==> low(*l) // @ ensures low(err != nil) // @ decreases func (l *LinkType) UnmarshalText(data []byte) (err error) { - //@ BeforeUnfold: - //@ unfold acc(sl.Bytes(data, 0, len(data)), R15) - //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R15) - //@ assert forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) ==> - //@ old[BeforeUnfold](sl.GetByte(data, 0, len(data), i)) == data[i] - //@ sif.LowSliceImpliesLowString(data, R15) + //@ unfold acc(sl.Bytes(data, 0, len(data)), R16) + //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R16) + //@ assert forall i int :: { &data[i] } 0 <= i && i < len(data) && low(i) ==> + //@ sl.GetByte(data, 0, len(data), i) == data[i] + //@ sif.LowSliceImpliesLowString(data, R16) switch strings.ToLower(string(data)) { case "core": *l = Core diff --git a/verification/utils/sif/assumptions.gobra b/verification/utils/sif/assumptions.gobra index 8a612bee3..2afbf9fed 100644 --- a/verification/utils/sif/assumptions.gobra +++ b/verification/utils/sif/assumptions.gobra @@ -5,7 +5,7 @@ package sif // TODO: Once Gobra issue #832 is resolved, introduce body and prove this. ghost requires p > 0 && acc(b, p) -requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) ==> low(b[i]) +requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) && low(i) ==> low(b[i]) ensures acc(b, p) && low(string(b)) decreases func LowSliceImpliesLowString(b []byte, p perm) From 0003f81cefc75a9a7c2d2e5af426b355d7e3ae94 Mon Sep 17 00:00:00 2001 From: henriman Date: Tue, 12 Aug 2025 23:05:42 +0200 Subject: [PATCH 10/12] Remove `&& low(i) ==>` from one assertion not dealing with sensitivity --- private/topology/linktype.go | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 81f99e6a1..568793f00 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -115,7 +115,7 @@ func (l LinkType) MarshalText() (res []byte, err error) { func (l *LinkType) UnmarshalText(data []byte) (err error) { //@ unfold acc(sl.Bytes(data, 0, len(data)), R16) //@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R16) - //@ assert forall i int :: { &data[i] } 0 <= i && i < len(data) && low(i) ==> + //@ assert forall i int :: { &data[i] } 0 <= i && i < len(data) ==> //@ sl.GetByte(data, 0, len(data), i) == data[i] //@ sif.LowSliceImpliesLowString(data, R16) switch strings.ToLower(string(data)) { From 27f66a534053aa14ffc391f213c5a3fbc8a85bb0 Mon Sep 17 00:00:00 2001 From: henriman Date: Mon, 18 Aug 2025 16:45:07 +0200 Subject: [PATCH 11/12] Remove assumption for Gobra issue 831 Issue 831 is fixed by PR 961 --- private/topology/linktype.go | 2 -- 1 file changed, 2 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 568793f00..5bbd0c9d0 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -66,8 +66,6 @@ func (l LinkType) String() string { func LinkTypeFromString(s string) (res LinkType) { var l /*@@@*/ LinkType tmp := []byte(s) - // TODO: Once Gobra issue #831 is resolved, remove this assumption. - //@ assume forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) && low(i) ==> low(tmp[i]) //@ fold sl.Bytes(tmp, 0, len(tmp)) if err := l.UnmarshalText(tmp); err != nil { return Unset From c72c8779212b41b69a888bb8d0af6d8c2ba19b61 Mon Sep 17 00:00:00 2001 From: henriman Date: Fri, 19 Sep 2025 10:15:39 +0200 Subject: [PATCH 12/12] Align contract clauses --- private/topology/linktype.go | 10 +++++----- verification/utils/sif/assumptions.gobra | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/private/topology/linktype.go b/private/topology/linktype.go index 5bbd0c9d0..e7cdff685 100644 --- a/private/topology/linktype.go +++ b/private/topology/linktype.go @@ -101,14 +101,14 @@ func (l LinkType) MarshalText() (res []byte, err error) { } } -// @ requires acc(sl.Bytes(data, 0, len(data)), R15) -// @ requires low(len(data)) && +// @ requires acc(sl.Bytes(data, 0, len(data)), R15) +// @ requires low(len(data)) && // @ forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) && low(i) ==> // @ low(sl.GetByte(data, 0, len(data), i)) // @ preserves acc(l) -// @ ensures acc(sl.Bytes(data, 0, len(data)), R15) -// @ ensures err != nil ==> err.ErrorMem() -// @ ensures low(err != nil) +// @ ensures acc(sl.Bytes(data, 0, len(data)), R15) +// @ ensures err != nil ==> err.ErrorMem() +// @ ensures low(err != nil) // @ decreases func (l *LinkType) UnmarshalText(data []byte) (err error) { //@ unfold acc(sl.Bytes(data, 0, len(data)), R16) diff --git a/verification/utils/sif/assumptions.gobra b/verification/utils/sif/assumptions.gobra index 2afbf9fed..c0cd79938 100644 --- a/verification/utils/sif/assumptions.gobra +++ b/verification/utils/sif/assumptions.gobra @@ -6,6 +6,6 @@ package sif ghost requires p > 0 && acc(b, p) requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) && low(i) ==> low(b[i]) -ensures acc(b, p) && low(string(b)) +ensures acc(b, p) && low(string(b)) decreases func LowSliceImpliesLowString(b []byte, p perm)