Drop two assumptions and merge validity criteria StronglyValid and …

…`FullyValid` (#366)

* backup

* backup

* fix verification error

* fix test

* fix another verification error

* fix verification error

* drop StronglyValid criteria

* cleanup

* Update gobra.yml

* Update .github/workflows/gobra.yml

* Update .github/workflows/gobra.yml

.github/workflows/gobra.yml

@@ -415,7 +415,12 @@ jobs:
           includePaths: ${{ env.includePaths }}
           assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
           checkConsistency: ${{ env.checkConsistency }}
-          chop: 10
+          # Due to a bug introduced in https://github.com/viperproject/gobra/pull/776,
+          # we must currently disable the chopper, otherwise we well-founded orders
+          # for termination checking are not available at the chopped Viper parts.
+          # We should reenable it whenever possible, as it reduces verification time in
+          # ~8 min (20%).
+          # chop: 10
           parallelizeBranches: '1'
           conditionalizePermissions: '1'
           moreJoins: 'impure'

pkg/slayers/path/scion/base_spec.gobra

@@ -57,8 +57,7 @@ decreases
 pure func (b Base) ValidCurrFieldsSpec() bool {
 	return 0 <= b.NumINF && b.NumINF <= MaxINFs &&
 		0 <= b.NumHops && b.NumHops <= MaxHops  &&
-		b.ValidCurrInfSpec()                    &&
-		b.ValidCurrHfSpec()
+		b.ValidCurrInfSpec() && b.ValidCurrHfSpec()
 }
 
 // A `Base` is weakly valid when the fields `NumINF` and `NumHops` are,
@@ -71,29 +70,29 @@ pure func (b Base) WeaklyValid() bool {
 	return 0 <= b.NumINF  && b.NumINF <= MaxINFs  &&
 		0 <= b.NumHops && b.NumHops <= MaxHops    &&
 		(0 < b.NumINF ==> 0 < b.NumHops)          &&
-		b.PathMeta.InBounds()                     &&
-		b.NumsCompatibleWithSegLen()
+		b.PathMeta.InBounds() && b.NumsCompatibleWithSegLen()
 }
 
-// A `Base` is strongly valid iff it is weakly valid and its `CurrHF`
-// and `CurrINF` are within bounds.
+// A `Base` is valid (a.k.a fully valid) iff it is weakly valid
+// and its `CurrHF` and `CurrINF` are within bounds, its `CurrHF`
+// is compatible with its `CurrINF`, and there are no singleton
+// segments. In the past, there used to be another validity
+// criteria, stronger than WeaklyValid and weaker than FullyValid.
+// This was known as StronglyValid and has been derprecated.
 ghost
 decreases
-pure func (b Base) StronglyValid() bool {
-	return b.WeaklyValid() && b.ValidCurrFieldsSpec()
+pure func (b Base) Valid() bool {
+	return b.WeaklyValid()           &&
+		b.ValidCurrFieldsSpec()      &&
+		b.CurrInfMatchesCurrHFSpec() &&
+		b.PathMeta.SegLen[0] != 1    &&
+		b.PathMeta.SegLen[1] != 1    &&
+		b.PathMeta.SegLen[2] != 1
 }
 
-// A `Base` is fully valid iff it is strongly valid and its `CurrHF` is
-// compatible with its `CurrINF`.
 ghost
 decreases
-pure func (b Base) FullyValid() bool {
-	return b.StronglyValid() && b.CurrInfMatchesCurrHF()
-}
-
-ghost
-decreases
-pure func (b Base) CurrInfMatchesCurrHF() bool {
+pure func (b Base) CurrInfMatchesCurrHFSpec() bool {
 	return b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF)
 }
 
@@ -167,7 +166,7 @@ ghost
 requires s.NumINF != 0
 requires int(s.PathMeta.CurrHF) < s.NumHops-1
 ensures  s.WeaklyValid() ==> res.WeaklyValid()
-ensures  s.StronglyValid() ==> res.StronglyValid()
+ensures  s.Valid() ==> res.Valid()
 decreases
 pure func (s Base) IncPathSpec() (res Base) {
 	return Base {
@@ -177,6 +176,12 @@ pure func (s Base) IncPathSpec() (res Base) {
 	}
 }
 
+ghost
+requires s.Valid()
+ensures  s.IsXoverSpec() ==> !s.IncPathSpec().IsXoverSpec()
+decreases
+func (s Base) NotIsXoverAfterIncPath() {}
+
 ghost
 decreases
 pure func (b Base) ReverseSpec() Base {
@@ -208,12 +213,10 @@ pure func (b Base) ReverseSegLen() [3]uint8 {
 }
 
 ghost
-requires b.StronglyValid()
-ensures  b.ReverseSpec().StronglyValid()
+requires b.Valid()
+ensures  b.ReverseSpec().Valid()
 decreases
-pure func (b Base) ReversingBaseStronglyValidSegLenHasValidSegLen() Lemma {
-	return Lemma{}
-}
+func (b Base) ReversingBaseValidSegLenHasValidSegLen() { }
 
 ghost
 requires b.Mem()
@@ -321,21 +324,6 @@ pure func (s MetaHdr) EqAbsHeader(ub []byte) bool {
 		s == DecodedFrom(binary.BigEndian.Uint32(ub[:MetaLen]))
 }
 
-ghost
-opaque
-requires MetaLen <= idx && idx <= len(ub)
-requires acc(sl.Bytes(ub, 0, len(ub)), R55)
-requires acc(sl.Bytes(ub[:idx], 0, idx), R55)
-ensures  s.EqAbsHeader(ub) == s.EqAbsHeader(ub[:idx])
-decreases
-pure func (s MetaHdr) EqAbsHeaderForSublice(ub []byte, idx int) Lemma {
-	return let _ := Asserting(ub[:MetaLen] === ub[:idx][:MetaLen]) in
-		unfolding acc(sl.Bytes(ub, 0, len(ub)), R56) in
-		unfolding acc(sl.Bytes(ub[:idx], 0, idx), R56) in
-		let _ := Asserting(s.EqAbsHeader(ub) == (s == DecodedFrom(binary.BigEndian.Uint32(ub[:MetaLen])))) in
-		Lemma{}
-}
-
 /** Lemma proven in /VerifiedSCION/verification/utils/bitwise/proofs.dfy **/
 ghost
 requires m.InBounds()

pkg/slayers/path/scion/decoded.go

@@ -213,11 +213,11 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 // @	p.Mem(ubuf)                 &&
 // @	p == s                      &&
 // @	typeOf(p) == type[*Decoded] &&
-// @	(old(s.GetBase(ubuf).StronglyValid()) ==> s.GetBase(ubuf).StronglyValid()))
+// @	(old(s.GetBase(ubuf).Valid()) ==> s.GetBase(ubuf).Valid()))
 // @ ensures  r != nil ==> r.ErrorMem() && s.Mem(ubuf)
 // @ decreases
 func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
-	//@ ghost isValid := s.GetBase(ubuf).StronglyValid()
+	//@ ghost isValid := s.GetBase(ubuf).Valid()
 	//@ ghost base := s.GetBase(ubuf)
 	//@ ghost metaHdrAferReversingSegLen := MetaHdr {
 	//@ 	CurrINF: base.PathMeta.CurrINF,
@@ -282,8 +282,8 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
 	s.PathMeta.CurrINF = uint8(s.NumINF) - s.PathMeta.CurrINF - 1
 	s.PathMeta.CurrHF = uint8(s.NumHops) - s.PathMeta.CurrHF - 1
 	//@ assert s.Base == base.ReverseSpec()
-	//@ ghost if isValid { base.ReversingBaseStronglyValidSegLenHasValidSegLen() }
-	//@ assert isValid ==> s.Base.StronglyValid()
+	//@ ghost if isValid { base.ReversingBaseValidSegLenHasValidSegLen() }
+	//@ assert isValid ==> s.Base.Valid()
 	//@ fold s.Base.Mem()
 	//@ fold s.Mem(ubuf)
 	return s, nil

pkg/slayers/path/scion/decoded_spec.gobra

@@ -113,7 +113,7 @@ requires d.Mem(ubuf)
 ensures  e == nil ==> (
 	d.Mem(ubuf) &&
 	d.LenSpec(ubuf) == old(d.LenSpec(ubuf)) &&
-	(old(d.GetBase(ubuf).StronglyValid()) ==> d.GetBase(ubuf).StronglyValid()))
+	(old(d.GetBase(ubuf).Valid()) ==> d.GetBase(ubuf).Valid()))
 ensures  e != nil ==> d.NonInitMem() && e.ErrorMem()
 decreases
 func (d *Decoded) IncPath(ghost ubuf []byte) (e error) {

pkg/slayers/path/scion/raw.go

@@ -139,17 +139,17 @@ func (s *Raw) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) {
 // @ ensures   err == nil ==> (
 // @ 	let newUb := s.RawBufferMem(ubuf) in
 // @ 	d.Mem(newUb) &&
-// @ 	(old(s.GetBase(ubuf).StronglyValid()) ==> d.GetBase(newUb).StronglyValid()))
+// @ 	(old(s.GetBase(ubuf).Valid()) ==> d.GetBase(newUb).Valid()))
 // @ ensures   err != nil ==> err.ErrorMem()
 // @ decreases
 func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) {
 	//@ unfold acc(s.Mem(ubuf), R6)
 	//@ unfold acc(s.Base.Mem(), R6)
 	//@ ghost var base Base = s.Base
 	//@ ghost var pathMeta MetaHdr = s.Base.PathMeta
-	//@ ghost validIdxs := s.GetBase(ubuf).StronglyValid()
+	//@ ghost validIdxs := s.GetBase(ubuf).Valid()
 	//@ assert validIdxs ==> s.Base.PathMeta.InBounds()
-	//@ assert validIdxs ==> base.StronglyValid()
+	//@ assert validIdxs ==> base.Valid()
 	//@ assert s.Raw[:MetaLen] === ubuf[:MetaLen]
 
 	// (VerifiedSCION) In this method, many slice operations are done in two
@@ -207,7 +207,7 @@ func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) {
 	//@ ghost if validIdxs {
 	//@ 	s.PathMeta.SerializeAndDeserializeLemma(b0, b1, b2, b3)
 	//@ 	assert pathMeta == decoded.GetMetaHdr(s.Raw)
-	//@ 	assert decoded.GetBase(s.Raw).StronglyValid()
+	//@ 	assert decoded.GetBase(s.Raw).Valid()
 	//@ }
 	//@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm)
 	//@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm)
@@ -265,17 +265,16 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
 	//@ tail := ubuf[MetaLen:]
 	//@ unfold acc(sl.Bytes(tail, 0, len(tail)), R50)
 	//@ oldHfIdxSeg := oldCurrHfIdx-oldPrevSegLen
-	//@	WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg,
-	//@ 	oldSegLen, MetaLen, MetaLen, len(ubuf))
-	//@	WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSegs, MetaLen, MetaLen, len(ubuf))
-	//@	WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSegs, MetaLen, MetaLen, len(ubuf))
-	//@	WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSegs, MetaLen, MetaLen, len(ubuf))
-	//@	LenCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
+	//@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg, oldSegLen, MetaLen, MetaLen, len(ubuf))
+	//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSegs, MetaLen, MetaLen, len(ubuf))
+	//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSegs, MetaLen, MetaLen, len(ubuf))
+	//@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSegs, MetaLen, MetaLen, len(ubuf))
+	//@ LenCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
 	//@ oldAbsPkt := reveal s.absPkt(ubuf)
 	//@ sl.SplitRange_Bytes(ubuf, 0, MetaLen, HalfPerm)
 	//@ unfold acc(s.Base.Mem(), R2)
 	err := s.PathMeta.SerializeTo(s.Raw[:MetaLen])
-	//@ assert s.Base.StronglyValid()
+	//@ assert s.Base.Valid()
 	//@ assert s.PathMeta.InBounds()
 	//@ v := s.Raw[:MetaLen]
 	//@ b0 := sl.GetByte(v, 0, MetaLen, 0)
@@ -284,7 +283,7 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
 	//@ b3 := sl.GetByte(v, 0, MetaLen, 3)
 	//@ s.PathMeta.SerializeAndDeserializeLemma(b0, b1, b2, b3)
 	//@ assert s.PathMeta.EqAbsHeader(v)
-	//@ assert RawBytesToBase(v).StronglyValid()
+	//@ assert RawBytesToBase(v).Valid()
 	//@ sl.CombineRange_Bytes(ubuf, 0, MetaLen, HalfPerm)
 	//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
 	//@ assert s.EqAbsHeader(ubuf) == s.PathMeta.EqAbsHeader(ubuf)
@@ -441,7 +440,7 @@ func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @
 	//@ ghost if idx == currInfIdx {
 	//@ 	CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
 	//@ 	LeftSegEquality(ubuf, currInfIdx+1, segLens)
-	//@  	MidSegEquality(ubuf, currInfIdx+2, segLens)
+	//@ 	MidSegEquality(ubuf, currInfIdx+2, segLens)
 	//@ 	RightSegEquality(ubuf, currInfIdx-1, segLens)
 	//@ }
 	//@ reveal s.absPkt(ubuf)
@@ -582,7 +581,7 @@ func (s *Raw) IsPenultimateHop( /*@ ghost ubuf []byte @*/ ) bool {
 
 // IsLastHop returns whether the current hop is the last hop on the path.
 // @ preserves acc(s.Mem(ubuf), R40)
-// @ ensures res == s.IsLastHopSpec(ubuf)
+// @ ensures   res == s.IsLastHopSpec(ubuf)
 // @ decreases
 func (s *Raw) IsLastHop( /*@ ghost ubuf []byte @*/ ) (res bool) {
 	//@ unfold acc(s.Mem(ubuf), R40)
@@ -591,3 +590,16 @@ func (s *Raw) IsLastHop( /*@ ghost ubuf []byte @*/ ) (res bool) {
 	//@ defer  fold acc(s.Base.Mem(), R40)
 	return int(s.PathMeta.CurrHF) == (s.NumHops - 1)
 }
+
+// CurrINFMatchesCurrHF returns whether the the path's current hopfield
+// is in the path's current segment.
+// @ preserves acc(s.Mem(ub), R40)
+// @ ensures   res == s.GetBase(ub).CurrInfMatchesCurrHFSpec()
+// @ decreases
+func (s *Raw) CurrINFMatchesCurrHF( /*@ ghost ub []byte @*/ ) (res bool) {
+	// @ unfold acc(s.Mem(ub), R40)
+	// @ defer fold acc(s.Mem(ub), R40)
+	// @ unfold acc(s.Base.Mem(), R40)
+	// @ defer fold acc(s.Base.Mem(), R40)
+	return s.PathMeta.CurrINF == s.infIndexForHF(s.PathMeta.CurrHF)
+}

pkg/slayers/path/scion/raw_spec.gobra

@@ -181,7 +181,8 @@ ghost
 requires acc(r.Mem(ub), _)
 decreases
 pure func (r *Raw) GetCurrHF(ghost ub []byte) uint8 {
-	return unfolding acc(r.Mem(ub), _) in (unfolding acc(r.Base.Mem(), _) in r.PathMeta.CurrHF)
+	return unfolding acc(r.Mem(ub), _) in
+		(unfolding acc(r.Base.Mem(), _) in r.PathMeta.CurrHF)
 }
 
 ghost
@@ -436,9 +437,8 @@ pure func validPktMetaHdr(raw []byte) bool {
 		let seg3 := int(metaHdr.SegLen[2])    in
 		let segs := io.CombineSegLens(seg1, seg2, seg3) in
 		let base := RawBytesToBase(raw)       in
-		0 < metaHdr.SegLen[0]           &&
-		base.StronglyValid()            &&
-		base.CurrInfMatchesCurrHF()		&&
+		0 < metaHdr.SegLen[0] &&
+		base.Valid()     &&
 		PktLen(segs, MetaLen) <= len(raw)
 }
 
@@ -463,7 +463,7 @@ func ValidPktMetaHdrSublice(raw []byte, idx int) {
 ghost
 requires acc(s.Mem(ub), R54)
 requires acc(sl.Bytes(ub, 0, len(ub)), R55)
-requires s.GetBase(ub).FullyValid()
+requires s.GetBase(ub).Valid()
 requires s.GetBase(ub).EqAbsHeader(ub)
 ensures  acc(sl.Bytes(ub, 0, len(ub)), R55)
 ensures  acc(s.Mem(ub), R54)

pkg/slayers/scion_spec.gobra

@@ -189,9 +189,9 @@ pure func (s *SCION) ValidPathMetaData(ghost ub []byte) bool {
 	return unfolding acc(s.Mem(ub), _) in
 		let ubPath := s.UBPath(ub) in
 		(typeOf(s.Path) == type[*scion.Raw] ==>
-			s.Path.(*scion.Raw).GetBase(ubPath).StronglyValid()) &&
+			s.Path.(*scion.Raw).GetBase(ubPath).Valid()) &&
 		(typeOf(s.Path) == type[*epic.Path] ==>
-			s.Path.(*epic.Path).GetBase(ubPath).StronglyValid())
+			s.Path.(*epic.Path).GetBase(ubPath).Valid())
 }
 
 // TODO: simplify the body of the predicate when let expressions
@@ -470,7 +470,7 @@ pure func ValidPktMetaHdr(raw []byte) bool {
 		let segs := io.CombineSegLens(seg1, seg2, seg3) in
 		let base := scion.Base{metaHdr, segs.NumInfoFields(), segs.TotalHops()} in
 		0 < metaHdr.SegLen[0] &&
-		base.FullyValid() &&
+		base.Valid() &&
 		scion.PktLen(segs, start + scion.MetaLen) <= length
 }