Skip to content

Commit

Permalink
Empty </: Path
Browse files Browse the repository at this point in the history
  • Loading branch information
@jcp19
jcp19 committed Oct 21, 2023
1 parent da2b9f4 commit 08b48c8
Show file tree
Hide file tree
Showing 9 changed files with 96 additions and 116 deletions.
15 changes: 8 additions & 7 deletions pkg/slayers/path/empty/empty.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ func RegisterPath() {
//@ ensures p != nil
//@ decreases
func /*@ newPath @*/ () (p path.Path) {
emptyTmp := Path{}
emptyTmp := &Path{}
//@ fold emptyTmp.NonInitMem()
return emptyTmp
},
Expand All @@ -57,6 +57,7 @@ func RegisterPath() {
// bytes on the wire and is used for AS internal communication.
type Path struct{}

// @ requires o.NonInitMem()
// @ ensures len(r) == 0 ==> (
// @ e == nil &&
// @ o.Mem() &&
Expand All @@ -66,38 +67,38 @@ type Path struct{}
// @ e.ErrorMem() &&
// @ o.NonInitMem())
// @ decreases
func (o Path) DecodeFromBytes(r []byte) (e error) {
func (o *Path) DecodeFromBytes(r []byte) (e error) {
if len(r) != 0 {
//@ fold o.NonInitMem()
return serrors.New("decoding an empty path", "len", len(r))
}
//@ unfold o.NonInitMem()
//@ fold o.Mem()
return nil
}

// @ ensures e == nil
// @ decreases
func (o Path) SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error) {
func (o *Path) SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error) {
return nil
}

// @ ensures p == o
// @ ensures e == nil
// @ decreases
func (o Path) Reverse( /*@ ghost ub []byte @*/ ) (p path.Path, e error) {
func (o *Path) Reverse( /*@ ghost ub []byte @*/ ) (p path.Path, e error) {
return o, nil
}

// @ pure
// @ ensures 0 <= r
// @ decreases
func (o Path) Len( /*@ ghost ub []byte @*/ ) (r int) {
func (o *Path) Len( /*@ ghost ub []byte @*/ ) (r int) {
return PathLen
}

// @ pure
// @ ensures r == PathType
// @ decreases
func (o Path) Type( /*@ ghost ub []byte @*/ ) (r path.Type) {
func (o *Path) Type( /*@ ghost ub []byte @*/ ) (r path.Type) {
return PathType
}
19 changes: 0 additions & 19 deletions pkg/slayers/path/empty/empty_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,25 +21,6 @@ import (
"github.com/scionproto/scion/verification/utils/slices"
)

Path implements path.Path

pred (e Path) Mem() { true }
pred (e Path) NonInitMem() { true }

ghost
decreases
pure func (e Path) Valid(ghost ub []byte) bool {
return len(ub) == 0
}

ghost
ensures e.NonInitMem()
decreases
func (e Path) DowngradePerm(buf []byte) {
unfold e.Mem()
fold e.NonInitMem()
}

// Definitions to allow *Path to be treated as a path.Path
(*Path) implements path.Path

Expand Down
4 changes: 2 additions & 2 deletions pkg/slayers/path/empty/empty_spec_test.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,11 @@
package empty

func FoldNonInitMem_test() {
e := Path{}
e@ := Path{}
fold e.NonInitMem()
}

func FoldMem_test() {
e := Path{}
e@ := Path{}
fold e.Mem()
}
1 change: 1 addition & 0 deletions pkg/slayers/path/hopfield.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ type HopField struct {
// @ requires len(raw) >= HopLen
// @ preserves acc(h)
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R45)
// @ ensures h.Valid()
// @ ensures err == nil
// @ decreases
func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
Expand Down
1 change: 1 addition & 0 deletions pkg/slayers/path/scion/base_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ import (
sl "github.com/scionproto/scion/verification/utils/slices"
)

// TODO: drop
pred (b *Base) NonInitMem() {
acc(b)
}
Expand Down
59 changes: 28 additions & 31 deletions pkg/slayers/path/scion/decoded.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,8 +56,8 @@ type Decoded struct {
// @ let b3 := sl.GetByte(data, 0, lenD, 3) in
// @ let line := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in
// @ let metaHdr := DecodedFrom(line) in
// @ metaHdr == s.GetMetaHdr(data) &&
// @ s.InfsMatchHfs(data))
// @ metaHdr == s.GetMetaHdr() &&
// @ s.InfsMatchHfs())
// @ ensures r != nil ==> (r.ErrorMem() && s.NonInitMem())
// @ decreases
func (s *Decoded) DecodeFromBytes(data []byte) (r error) {
Expand Down Expand Up @@ -106,8 +106,8 @@ func (s *Decoded) DecodeFromBytes(data []byte) (r error) {
//@ invariant acc(s.Base.Mem(), R1)
//@ invariant len(s.HopFields) == s.Base.GetNumHops()
//@ invariant 0 <= i && i <= s.Base.GetNumHops()
//@ invariant forall j int :: { &s.HopFields[j] } i <= j && j < s.Base.GetNumHops() ==> acc(&s.HopFields[j])
//@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < i ==> s.HopFields[j].Mem()
//@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < s.Base.GetNumHops() ==> acc(&s.HopFields[j])
//@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < i ==> s.HopFields[j].Valid()
//@ invariant len(data) >= MetaLen + s.Base.GetNumINF() * path.InfoLen + s.Base.GetNumHops() * path.HopLen
//@ invariant offset == MetaLen + s.Base.GetNumINF() * path.InfoLen + i * path.HopLen
//@ invariant acc(sl.AbsSlice_Bytes(data, 0, offset), R41)
Expand Down Expand Up @@ -155,7 +155,7 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
//@ fold acc(s.Base.Mem(), R1)
//@ sl.Unslice_Bytes(b, 0, MetaLen, writePerm)
//@ sl.CombineAtIndex_Bytes(b, 0, len(b), MetaLen, writePerm)
//@ fold acc(s.Mem(ubuf), R1)
//@ fold acc(s.Mem(), R1)
offset := MetaLen

//@ invariant acc(s.Mem(), R1) && s.Valid(ubuf)
Expand All @@ -182,10 +182,10 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
//@ sl.Unslice_Bytes(b, offset, offset + path.InfoLen, writePerm)
//@ sl.CombineAtIndex_Bytes(b, offset, len(b), offset + path.InfoLen, writePerm)
//@ sl.CombineAtIndex_Bytes(b, 0, len(b), offset, writePerm)
//@ fold acc(s.Mem(ubuf), R1)
//@ fold acc(s.Mem(), R1)
offset += path.InfoLen
}
//@ invariant acc(s.Mem(ubuf), R1)
//@ invariant acc(s.Mem(), R1) && s.Valid(ubuf)
//@ invariant sl.AbsSlice_Bytes(ubuf, 0, len(ubuf))
//@ invariant b !== ubuf ==> sl.AbsSlice_Bytes(b, 0, len(b))
//@ invariant s.Len(ubuf) <= len(b)
Expand Down Expand Up @@ -215,44 +215,45 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
}

// Reverse reverses a SCION path.
// @ requires s.Mem(ubuf)
// @ requires s.Mem() && s.Valid(ubuf)
// @ ensures r == nil ==> (
// @ p != nil &&
// @ p.Mem(ubuf) &&
// @ p.Mem() &&
// @ p.Valid(ubuf) &&
// @ p == s &&
// @ typeOf(p) == type[*Decoded] &&
// @ (old(s.ValidCurrIdxs(ubuf)) ==> s.ValidCurrIdxs(ubuf)))
// @ ensures r != nil ==> r.ErrorMem() && s.Mem(ubuf)
// @ (old(s.ValidCurrIdxs()) ==> s.ValidCurrIdxs()))
// @ ensures r != nil ==> r.ErrorMem() && s.Mem()
// @ decreases
func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
//@ ghost isValid := s.ValidCurrIdxs(ubuf)
//@ unfold s.Mem(ubuf)
//@ ghost isValid := s.ValidCurrIdxs()
//@ unfold s.Mem()
//@ unfold s.Base.Mem()
if s.NumINF == 0 {
//@ fold s.Base.Mem()
//@ fold s.Mem()
return nil, serrors.New("empty decoded path is invalid and cannot be reversed")
}
//@ fold s.Base.Mem()
//@ fold s.Mem(ubuf)
//@ ghost base := s.GetBase(ubuf)
//@ fold s.Mem()
//@ ghost base := s.GetBase()

// Reverse order of InfoFields and SegLens
//@ invariant s.Mem(ubuf)
//@ invariant isValid ==> s.ValidCurrIdxs(ubuf)
//@ invariant 0 <= i && i < s.GetNumINF(ubuf)
//@ invariant 0 <= j && j < s.GetNumINF(ubuf)
//@ invariant s.Mem() && s.Valid(ubuf)
//@ invariant isValid ==> s.ValidCurrIdxs()
//@ invariant 0 <= i && i < s.GetNumINF()
//@ invariant 0 <= j && j < s.GetNumINF()
//@ decreases j-i
for i, j := 0, ( /*@ unfolding s.Mem() in (unfolding s.Base.Mem() in @*/ s.NumINF - 1 /*@) @*/); i < j; i, j = i+1, j-1 {
//@ unfold s.Mem()
s.InfoFields[i], s.InfoFields[j] = s.InfoFields[j], s.InfoFields[i]
//@ unfold s.Base.Mem()
s.PathMeta.SegLen[i], s.PathMeta.SegLen[j] = s.PathMeta.SegLen[j], s.PathMeta.SegLen[i]
//@ fold s.Base.Mem()
//@ fold s.Mem(ubuf)
//@ fold s.Mem()
}
//@ preserves s.Mem(ubuf)
//@ preserves isValid ==> s.ValidCurrIdxs(ubuf)
//@ preserves s.Mem() && s.Valid(ubuf)
//@ preserves isValid ==> s.ValidCurrIdxs()
//@ decreases
//@ outline(
//@ unfold s.Mem()
Expand All @@ -273,25 +274,21 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {

// Reverse order of hop fields
//@ invariant s.Mem() && s.Valid(ubuf)
//@ invariant 0 <= i && i <= s.GetNumHops(ubuf)
//@ invariant -1 <= j && j < s.GetNumHops(ubuf)
//@ invariant isValid ==> s.ValidCurrIdxs(ubuf)
//@ invariant 0 <= i && i <= s.GetNumHops()
//@ invariant -1 <= j && j < s.GetNumHops()
//@ invariant isValid ==> s.ValidCurrIdxs()
//@ decreases j-i
for i, j := 0, ( /*@ unfolding s.Mem() in (unfolding s.Base.Mem() in @*/ s.NumHops - 1 /*@ ) @*/); i < j; i, j = i+1, j-1 {
//@ unfold s.Mem()
//@ assert &s.HopFields[i] != &s.HopFields[j]
//@ unfold s.HopFields[i].Mem()
//@ unfold s.HopFields[j].Mem()
//@ assert acc(&s.HopFields[i]) && acc(&s.HopFields[j])
s.HopFields[i], s.HopFields[j] = s.HopFields[j], s.HopFields[i]
//@ assert acc(&s.HopFields[i]) && acc(&s.HopFields[j])
//@ fold s.HopFields[i].Mem()
//@ fold s.HopFields[j].Mem()
//@ fold s.Mem()
}
// Update CurrINF and CurrHF and SegLens
//@ preserves s.Mem(ubuf)
//@ preserves isValid ==> s.ValidCurrIdxs(ubuf)
//@ preserves s.Mem() && s.Valid(ubuf)
//@ preserves isValid ==> s.ValidCurrIdxs()
//@ decreases
//@ outline(
//@ unfold s.Mem()
Expand Down
Loading

0 comments on commit 08b48c8

Please sign in to comment.