Merge pull request #12 from henriman/sif-pkg-slayers-path-onehop

Verify `pkg/slayers/path/onehop`

Author: henriman

pkg/slayers/path/empty/empty_spec.gobra

@@ -58,4 +58,5 @@ Path implements path.Path
 // Definitions to allow *Path to be treated as a path.Path
 pred (e *Path) Mem(buf []byte) { acc(e) && len(buf) == 0 }
 pred (e *Path) NonInitMem() { true }
+
 (*Path) implements path.Path

pkg/slayers/path/hopfield.go

@@ -110,15 +110,15 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
 // SerializeTo writes the fields into the provided buffer. The buffer must be of length >=
 // path.HopLen.
 // @ requires  len(b) >= HopLen
-// @ requires  acc(h.Mem(), R10)
-// @ requires  low(h.GetEgressRouterAlert()) && low(h.GetIngressRouterAlert())
+// @ requires  acc(h.Mem(), R10) && h.IsLow()
 // @ preserves sl.Bytes(b, 0, HopLen)
 // @ ensures   acc(h.Mem(), R10)
 // @ ensures   err == nil
 // @ ensures   BytesToIO_HF(b, 0, 0, HopLen) ==
 // @ 	unfolding acc(h.Mem(), R10) in h.Abs()
 // @ decreases
 func (h *HopField) SerializeTo(b []byte) (err error) {
+	//@ h.RevealIsLow(R10)
 	if len(b) < HopLen {
 		return serrors.New("buffer for HopField too short", "expected", MacLen, "actual", len(b))
 	}

pkg/slayers/path/hopfield_spec.gobra

@@ -27,6 +27,37 @@ pred (h *HopField) Mem() {
 	acc(h) && h.ConsIngress >= 0 && h.ConsEgress >= 0
 }
 
+ghost
+requires h.Mem()
+decreases
+pure func (h *HopField) GetEgressRouterAlert() bool {
+	return unfolding h.Mem() in h.EgressRouterAlert
+}
+
+ghost
+requires h.Mem()
+decreases
+pure func (h *HopField) GetIngressRouterAlert() bool {
+	return unfolding h.Mem() in h.IngressRouterAlert
+}
+
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires h.Mem()
+decreases
+pure func (h *HopField) IsLow() bool
+
+// "Reveal the body" of `h.IsLow` (necessary bc. we can't implement `h.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires acc(h.Mem(), p) && h.IsLow()
+ensures  acc(h.Mem(), p)
+ensures  low(h.GetEgressRouterAlert()) && low(h.GetIngressRouterAlert())
+decreases
+func (h *HopField) RevealIsLow(p perm)
 
 ghost
 decreases
@@ -115,17 +146,3 @@ pure func (h HopField) Abs() (io.HF) {
 		HVF: AbsMac(h.Mac),
 	}
 }
-
-ghost
-requires h.Mem()
-decreases
-pure func (h *HopField) GetEgressRouterAlert() bool {
-	return unfolding h.Mem() in h.EgressRouterAlert
-}
-
-ghost
-requires h.Mem()
-decreases
-pure func (h *HopField) GetIngressRouterAlert() bool {
-	return unfolding h.Mem() in h.IngressRouterAlert
-}

pkg/slayers/path/onehop/onehop.go

@@ -64,6 +64,7 @@ type Path struct {
 }
 
 // @ requires  o.NonInitMem()
+// @ requires  low(len(data))
 // @ preserves acc(sl.Bytes(data, 0, len(data)), R42)
 // @ ensures   (len(data) >= PathLen) == (r == nil)
 // @ ensures   r == nil ==> o.Mem(data)
@@ -98,20 +99,25 @@ func (o *Path) DecodeFromBytes(data []byte) (r error) {
 	return r
 }
 
-// @ preserves acc(o.Mem(ubuf), R1)
+// @ requires  low(len(b))
+// @ requires  acc(o.Mem(ubuf), R1) && o.IsLow(ubuf)
 // @ preserves acc(sl.Bytes(ubuf, 0, len(ubuf)), R1)
 // @ preserves sl.Bytes(b, 0, len(b))
+// @ ensures   acc(o.Mem(ubuf), R1)
 // @ ensures   (len(b) >= PathLen) == (err == nil)
 // @ ensures   err != nil ==> err.ErrorMem()
 // @ ensures   err == nil ==> o.LenSpec(ubuf) <= len(b)
 // @ decreases
 func (o *Path) SerializeTo(b []byte /*@, ubuf []byte @*/) (err error) {
+	//@ o.RevealIsLow(ubuf, R1)
 	if len(b) < PathLen {
 		return serrors.New("buffer too short for OneHop path", "expected", int(PathLen), "actual",
 			int(len(b)))
 	}
 	offset := 0
 	//@ unfold acc(o.Mem(ubuf), R1)
+	//@ o.FirstHop.RevealIsLow(R2)
+	//@ o.SecondHop.RevealIsLow(R2)
 	//@ sl.SplitRange_Bytes(b, 0, offset+path.InfoLen, writePerm)
 	if err := o.Info.SerializeTo(b[:offset+path.InfoLen]); err != nil {
 		//@ sl.CombineRange_Bytes(b, 0, offset+path.InfoLen, writePerm)
@@ -135,10 +141,13 @@ func (o *Path) SerializeTo(b []byte /*@, ubuf []byte @*/) (err error) {
 
 // ToSCIONDecoded converts the one hop path in to a normal SCION path in the
 // decoded format.
-// @ preserves o.Mem(ubuf)
+// @ requires  o.Mem(ubuf)
+// @ requires  low(o.GetSecondHopConsIngress(ubuf))
 // @ preserves sl.Bytes(ubuf, 0, len(ubuf))
+// @ ensures   o.Mem(ubuf)
 // @ ensures   err == nil ==> (sd != nil && sd.Mem(ubuf))
 // @ ensures   err != nil ==> err.ErrorMem()
+// @ ensures   low(err != nil)
 // @ decreases
 func (o *Path) ToSCIONDecoded( /*@ ghost ubuf []byte @*/ ) (sd *scion.Decoded, err error) {
 	//@ unfold acc(o.Mem(ubuf), R1)
@@ -198,14 +207,15 @@ func (o *Path) ToSCIONDecoded( /*@ ghost ubuf []byte @*/ ) (sd *scion.Decoded, e
 }
 
 // Reverse a OneHop path that returns a reversed SCION path.
-// @ requires o.Mem(ubuf)
+// @ requires  o.Mem(ubuf) && o.IsLow(ubuf)
 // @ preserves sl.Bytes(ubuf, 0, len(ubuf))
-// @ ensures err == nil ==> p != nil
-// @ ensures err == nil ==> p.Mem(ubuf)
-// @ ensures err == nil ==> typeOf(p) == type[*scion.Decoded]
-// @ ensures err != nil ==> err.ErrorMem()
+// @ ensures   err == nil ==> p != nil
+// @ ensures   err == nil ==> p.Mem(ubuf)
+// @ ensures   err == nil ==> typeOf(p) == type[*scion.Decoded]
+// @ ensures   err != nil ==> err.ErrorMem()
 // @ decreases
 func (o *Path) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) {
+	//@ o.RevealIsLow(ubuf, writePerm)
 	sp, err := o.ToSCIONDecoded( /*@ ubuf @*/ )
 	if err != nil {
 		return nil, serrors.WrapStr("converting to scion path", err)

pkg/slayers/path/onehop/onehop_spec.gobra

@@ -32,6 +32,55 @@ pred (o *Path) Mem(ubuf []byte) {
 	PathLen <= len(ubuf)
 }
 
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) GetSecondHopConsIngress(ghost ub []byte) uint16 {
+	return unfolding o.Mem(ub) in 
+		unfolding o.SecondHop.Mem() in o.SecondHop.ConsIngress
+}
+
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) GetInfo(ghost ub []byte) path.InfoField {
+	return unfolding o.Mem(ub) in o.Info
+}
+
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) FirstHopIsLow(ghost ub []byte) bool {
+	return unfolding o.Mem(ub) in o.FirstHop.IsLow()
+}
+
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) SecondHopIsLow(ghost ub []byte) bool {
+	return unfolding o.Mem(ub) in o.SecondHop.IsLow()
+}
+
+// TODO: Once Gobra issue #846 is resolved, implement `IsLow`.
+ghost
+trusted
+requires o.Mem(ub)
+decreases
+pure func (o *Path) IsLow(ub []byte) bool
+
+// "Reveal the body" of `o.IsLow` (necessary bc. we can't implement `o.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires acc(o.Mem(ub), p) && o.IsLow(ub)
+ensures  acc(o.Mem(ub), p)
+ensures  low(o.GetSecondHopConsIngress(ub)) &&
+	low(o.GetInfo(ub).ConsDir) && low(o.GetInfo(ub).Peer) &&
+	o.FirstHopIsLow(ub) && o.SecondHopIsLow(ub)
+decreases
+func (o *Path) RevealIsLow(ub []byte, p perm)
+
 ghost
 requires p.Mem(buf)
 ensures  p.NonInitMem()
@@ -64,4 +113,4 @@ pure func (p *Path) LenSpec(ghost ub []byte) int {
 	return PathLen
 }
 
-(*Path) implements path.Path
+(*Path) implements path.Path

pkg/slayers/path/path.go

@@ -113,7 +113,7 @@ type Path interface {
 	//@ IsValidResultOfDecoding(b []byte) bool
 	// Reverse reverses a path such that it can be used in the reversed direction.
 	// XXX(shitz): This method should possibly be moved to a higher-level path manipulation package.
-	//@ requires  Mem(ub)
+	//@ requires  Mem(ub) && IsLow(ub)
 	//@ preserves sl.Bytes(ub, 0, len(ub))
 	//@ ensures   e == nil ==> p != nil
 	//@ ensures   e == nil ==> p.Mem(ub)

pkg/slayers/path/scion/decoded_spec.gobra

@@ -47,12 +47,12 @@ pred (d *Decoded) Mem(ubuf []byte) {
 	(forall i int :: { &d.HopFields[i] } 0 <= i && i < len(d.HopFields) ==> d.HopFields[i].Mem())
 }
 
-// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
 ghost
-trusted
 requires d.Mem(ub)
 decreases
-pure func (d *Decoded) IsLow(ub []byte) bool
+pure func (d *Decoded) IsLow(ub []byte) bool {
+	return true
+}
 
 /**** End of Predicates ****/
 
@@ -119,6 +119,7 @@ ensures  e == nil ==> (
 	d.LenSpec(ubuf) == old(d.LenSpec(ubuf)) &&
 	(old(d.GetBase(ubuf).Valid()) ==> d.GetBase(ubuf).Valid()))
 ensures  e != nil ==> d.NonInitMem() && e.ErrorMem()
+ensures  low(e != nil)
 decreases
 func (d *Decoded) IncPath(ghost ubuf []byte) (e error) {
 	unfold d.Mem(ubuf)

pkg/slayers/path/scion/raw_spec.gobra

@@ -38,12 +38,13 @@ pred (s *Raw) Mem(buf []byte) {
 	len(s.Raw) == s.Base.Len()
 }
 
-// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
 ghost
-trusted
 requires s.Mem(ub)
 decreases
-pure func (s *Raw) IsLow(ub []byte) bool
+pure func (s *Raw) IsLow(ub []byte) bool {
+	return true
+}
+
 /**** End of Predicates ****/
 
 (*Raw) implements path.Path