Skip to content

Commit

Permalink
simplify path/scion
Browse files Browse the repository at this point in the history
  • Loading branch information
@jcp19
jcp19 committed May 19, 2024
1 parent 6a8228a commit 06ba666
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 134 deletions.
124 changes: 8 additions & 116 deletions pkg/slayers/path/scion/base_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,152 +191,44 @@ pure func (s Base) IncPathSpec() (res Base) {
}
}

/*************** AbsBase ***************/

// There is a good deal of repition in this section of the file and the similarly
// named functions for the type `Base`. While for now this is not too big of a problem,
// we should find ways to streamline the definitions, ideally by having these defs only
// for the abstraction type only.

type AbsBase adt {
AbsBase_ {
PathMeta AbsMetaHdr
NumINF int
NumHops int
}
}

type AbsMetaHdr adt {
AbsMetaHdr_ {
// we should change the types of CurrINF and CurrHF to wider types,
// otherwise we might start getting overflow errors here when they
// are fully enabled.
CurrINF uint8
CurrHF uint8
SegLen seq[uint8]
}
}

ghost
decreases
pure func (b Base) Abs() AbsBase {
return AbsBase_{
PathMeta: b.PathMeta.Abs(),
NumINF: b.NumINF,
NumHops: b.NumHops,
}
}

ghost
decreases
pure func (b MetaHdr) Abs() AbsMetaHdr {
return AbsMetaHdr_{
CurrINF: b.CurrINF,
CurrHF: b.CurrHF,
SegLen: seq[uint8]{ b.SegLen[0], b.SegLen[1], b.SegLen[2] },
}
}

ghost
requires len(b.PathMeta.SegLen) == 3
decreases
pure func (b AbsBase) ReverseSpec() AbsBase {
return AbsBase_ {
pure func (b Base) ReverseSpec() Base {
return Base {
PathMeta: b.ReverseMetaHdrSpec(),
NumINF: b.NumINF,
NumHops: b.NumHops,
}
}

ghost
requires len(b.PathMeta.SegLen) == 3
decreases
pure func (b AbsBase) ReverseMetaHdrSpec() AbsMetaHdr {
return AbsMetaHdr_ {
pure func (b Base) ReverseMetaHdrSpec() MetaHdr {
return MetaHdr {
CurrINF: uint8(b.NumINF) - b.PathMeta.CurrINF - 1,
CurrHF: uint8(b.NumHops) - b.PathMeta.CurrHF - 1,
SegLen: b.ReverseSegLen(),
}
}

ghost
requires len(b.PathMeta.SegLen) == 3
decreases
pure func (b AbsBase) ReverseSegLen() seq[uint8] {
pure func (b Base) ReverseSegLen() [3]uint8 {
return (match b.NumINF {
case 2: seq[uint8]{ b.PathMeta.SegLen[1], b.PathMeta.SegLen[0], b.PathMeta.SegLen[2]}
case 3: seq[uint8]{ b.PathMeta.SegLen[2], b.PathMeta.SegLen[1], b.PathMeta.SegLen[0] }
case 2: [3]uint8{ b.PathMeta.SegLen[1], b.PathMeta.SegLen[0], b.PathMeta.SegLen[2] }
case 3: [3]uint8{ b.PathMeta.SegLen[2], b.PathMeta.SegLen[1], b.PathMeta.SegLen[0] }
default: b.PathMeta.SegLen
})
}

ghost
decreases
pure func (b AbsBase) ValidCurrIdxsSpec() bool {
return 0 <= b.NumINF && b.NumINF <= MaxINFs &&
len(b.PathMeta.SegLen) == 3 &&
0 <= b.NumHops && b.NumHops <= MaxHops &&
b.ValidCurrHfSpec() &&
b.ValidCurrInfSpec() &&
0 <= b.PathMeta.SegLen[0] && b.PathMeta.SegLen[0] < MaxHops &&
0 <= b.PathMeta.SegLen[1] && b.PathMeta.SegLen[1] < MaxHops &&
0 <= b.PathMeta.SegLen[2] && b.PathMeta.SegLen[2] < MaxHops &&
(b.NumINF == 1 ==> b.NumHops == int(b.PathMeta.SegLen[0])) &&
(b.NumINF == 2 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1])) &&
(b.NumINF == 3 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1] + b.PathMeta.SegLen[2])) &&
(forall i int :: { b.PathMeta.SegLen[i] } 0 <= i && i < b.NumINF ==>
b.PathMeta.SegLen[i] != 0) &&
(forall i int :: { b.PathMeta.SegLen[i] } b.NumINF <= i && i < MaxINFs ==>
b.PathMeta.SegLen[i] == 0)
}

ghost
opaque
requires b.ValidCurrIdxsSpec()
decreases
pure func (b AbsBase) CurrInfMatchesCurrHF() bool {
return b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF)
}

ghost
decreases
pure func (b AbsBase) ValidCurrInfSpec() bool {
return 0 <= b.PathMeta.CurrINF && b.PathMeta.CurrINF < b.NumINF
}

ghost
decreases
pure func (b AbsBase) ValidCurrHfSpec() bool {
return 0 <= b.PathMeta.CurrHF && b.PathMeta.CurrHF < b.NumHops
}

ghost
requires len(s.PathMeta.SegLen) == 3
ensures 0 <= r && r < 3
decreases
pure func (s AbsBase) InfForHfSpec(hf uint8) (r uint8) {
return hf < s.PathMeta.SegLen[0] ?
0 :
(hf < s.PathMeta.SegLen[0] + s.PathMeta.SegLen[1] ? 1 : 2)
}

ghost
requires b.ValidCurrIdxsSpec()
ensures b.ReverseSpec().ValidCurrIdxsSpec()
decreases
pure func (b AbsBase) ReversingValidBaseIsValidBase() Lemma {
return Lemma{}
}

ghost
ensures b.ValidCurrIdxsSpec() == b.Abs().ValidCurrIdxsSpec()
decreases
pure func (b Base) ValidBaseHasValidAbs() Lemma {
pure func (b Base) ReversingValidBaseIsValidBase() Lemma {
return Lemma{}
}

/*************** End of AbsBase ***************/

ghost
requires b.Mem()
ensures b.NonInitMem()
Expand Down
33 changes: 15 additions & 18 deletions pkg/slayers/path/scion/decoded.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,20 +218,17 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
// @ decreases
func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
//@ ghost isValid := s.ValidCurrIdxs(ubuf)
/*@
ghost base := s.GetBase(ubuf)
ghost absBase := base.Abs()
ghost absMetaHdrAferReversingSegLen := AbsMetaHdr_ {
CurrINF: absBase.PathMeta.CurrINF,
CurrHF: absBase.PathMeta.CurrHF,
SegLen: absBase.ReverseSegLen(),
}
ghost absBaseAfterReversingSegLen := AbsBase_ {
PathMeta: absMetaHdrAferReversingSegLen,
NumINF: absBase.NumINF,
NumHops: absBase.NumHops,
}
@*/
//@ ghost base := s.GetBase(ubuf)
//@ ghost metaHdrAferReversingSegLen := MetaHdr {
//@ CurrINF: base.PathMeta.CurrINF,
//@ CurrHF: base.PathMeta.CurrHF,
//@ SegLen: base.ReverseSegLen(),
//@ }
//@ ghost baseAfterReversingSegLen := Base {
//@ PathMeta: metaHdrAferReversingSegLen,
//@ NumINF: base.NumINF,
//@ NumHops: base.NumHops,
//@ }
//@ unfold s.Mem(ubuf)
//@ unfold s.Base.Mem()
if s.NumINF == 0 {
Expand Down Expand Up @@ -265,7 +262,7 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
//@ invariant s.Mem(ubuf)
//@ invariant 0 <= i && i <= s.GetNumHops(ubuf)
//@ invariant -1 <= j && j < s.GetNumHops(ubuf)
//@ invariant s.GetBase(ubuf).Abs() == absBaseAfterReversingSegLen
//@ invariant s.GetBase(ubuf) == baseAfterReversingSegLen
//@ decreases j-i
for i, j := 0, ( /*@ unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in @*/ s.NumHops - 1 /*@ ) @*/); i < j; i, j = i+1, j-1 {
//@ unfold s.Mem(ubuf)
Expand All @@ -284,9 +281,9 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) {
//@ unfold s.Base.Mem()
s.PathMeta.CurrINF = uint8(s.NumINF) - s.PathMeta.CurrINF - 1
s.PathMeta.CurrHF = uint8(s.NumHops) - s.PathMeta.CurrHF - 1
//@ assert s.Base.Abs() == absBase.ReverseSpec()
//@ ghost if isValid { absBase.ReversingValidBaseIsValidBase() }
//@ assert isValid ==> s.Base.Abs().ValidCurrIdxsSpec()
//@ assert s.Base == base.ReverseSpec()
//@ ghost if isValid { base.ReversingValidBaseIsValidBase() }
//@ assert isValid ==> s.Base.ValidCurrIdxsSpec()
//@ fold s.Base.Mem()
//@ fold s.Mem(ubuf)
return s, nil
Expand Down

0 comments on commit 06ba666

Please sign in to comment.