Skip to content

New perm syntax and changes on integers #430

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
jcp19 wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

New perm syntax and changes on integers #430

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 10 additions & 7 deletions pkg/slayers/extn.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,9 @@ type tlvOption struct {
OptAlign [2]uint8 // Xn+Y = [2]uint8{X, Y}
}

// @ preserves acc(o, R20)
// @ requires acc(o, R20)
// @ requires len(o.OptData) <= 255 // TLV option data length must fit in the uint8 OptDataLen wire field
// @ ensures acc(o, R20)
// @ ensures 0 < res
// @ ensures o.OptType == OptTypePad1 ==> res == 1
// @ ensures o.OptType != OptTypePad1 ==> 2 <= res
Expand Down Expand Up @@ -104,6 +106,7 @@ func (o *tlvOption) serializeTo(data []byte, fixLengths bool) {
// @ ensures (err == nil && res.OptType != OptTypePad1) ==> (
// @ 2 <= res.ActualLength && res.ActualLength <= len(data) && res.OptData === data[2:res.ActualLength])
// @ ensures err == nil ==> 0 < res.ActualLength
// @ ensures (err == nil && res.OptType == OptTypePad1) ==> res.ActualLength == 1
// @ ensures err != nil ==> err.ErrorMem()
// @ decreases
func decodeTLVOption(data []byte) (res *tlvOption, err error) {
Expand Down Expand Up @@ -336,7 +339,7 @@ func (h *HopByHopExtn) SerializeTo(b gopacket.SerializeBuffer,

o := make([]*tlvOption, 0, len(h.Options))
for _, v := range h.Options {
o = append( /*@ perm(0/1), @*/ o, (*tlvOption)(v))
o = append( /*@ perm(0, 1), @*/ o, (*tlvOption)(v))
}

return h.extnBase.serializeToWithTLVOptions(b, opts, o)
Expand Down Expand Up @@ -376,7 +379,7 @@ func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ invariant acc(sl.Bytes(data, 0, len(data)), R40)
// @ invariant h.BaseLayer.Contents === data[:h.ActualLen]
// @ invariant h.BaseLayer.Payload === data[h.ActualLen:]
// @ decreases h.ActualLen - offset
// @ decreases integer(h.ActualLen) - integer(offset)
for offset < h.ActualLen {
// @ sl.SplitRange_Bytes(data, offset, h.ActualLen, R40)
opt, err := decodeTLVOption(data[offset:h.ActualLen])
Expand All @@ -386,7 +389,7 @@ func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
return err
}
// @ ghost tmp := (*HopByHopOption)(opt)
h.Options = append( /*@ perm(1/2), @*/ h.Options, (*HopByHopOption)(opt))
h.Options = append( /*@ perm(1, 2), @*/ h.Options, (*HopByHopOption)(opt))
offset += opt.ActualLength
// @ assert h.Options[lenOptions] === tmp
// @ fold tmp.Mem(lenOptions)
Expand Down Expand Up @@ -508,7 +511,7 @@ func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ invariant acc(sl.Bytes(data, 0, len(data)), R40)
// @ invariant e.BaseLayer.Contents === data[:e.ActualLen]
// @ invariant e.BaseLayer.Payload === data[e.ActualLen:]
// @ decreases e.ActualLen - offset
// @ decreases integer(e.ActualLen) - integer(offset)
for offset < e.ActualLen {
// @ sl.SplitRange_Bytes(data, offset, e.ActualLen, R40)
opt, err := decodeTLVOption(data[offset:e.ActualLen])
Expand All @@ -518,7 +521,7 @@ func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
return err
}
// @ ghost tmp := (*EndToEndOption)(opt)
e.Options = append( /*@ perm(1/2), @*/ e.Options, (*EndToEndOption)(opt))
e.Options = append( /*@ perm(1, 2), @*/ e.Options, (*EndToEndOption)(opt))
offset += opt.ActualLength
// @ assert e.Options[lenOptions] === tmp
// @ fold tmp.Mem(lenOptions)
Expand Down Expand Up @@ -571,7 +574,7 @@ func (e *EndToEndExtn) SerializeTo(b gopacket.SerializeBuffer,

o := make([]*tlvOption, 0, len(e.Options))
for _, v := range e.Options {
o = append( /*@ perm(0/1), @*/ o, (*tlvOption)(v))
o = append( /*@ perm(0, 1), @*/ o, (*tlvOption)(v))
}

return e.extnBase.serializeToWithTLVOptions(b, opts, o)
Expand Down
4 changes: 2 additions & 2 deletions pkg/slayers/path/epic/epic.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,9 +312,9 @@ func (i *PktID) DecodeFromBytes(raw []byte) {
// @ decreases
func (i *PktID) SerializeTo(b []byte) {
//@ unfold sl.Bytes(b, 0, len(b))
//@ assert forall j int :: { &b[:4][j] } 0 <= 4 ==> &b[:4][j] == &b[j]
//@ assert forall j int :: { &b[:4][j] } 0 <= j && j < 4 ==> &b[:4][j] == &b[j]
binary.BigEndian.PutUint32(b[:4], i.Timestamp)
//@ assert forall j int :: { &b[4:8][j] } 0 <= 4 ==> &b[4:8][j] == &b[4 + j]
//@ assert forall j int :: { &b[4:8][j] } 0 <= j && j < 4 ==> &b[4:8][j] == &b[4 + j]
binary.BigEndian.PutUint32(b[4:8], i.Counter)
//@ fold sl.Bytes(b, 0, len(b))
}
6 changes: 3 additions & 3 deletions pkg/slayers/path/hopfield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ requires 0 <= start && start <= middle
requires middle + HopLen <= end && end <= len(raw)
requires sl.Bytes(raw, start, end)
decreases
pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.HF) {
pure func BytesToIO_HF(raw [] byte, start integer, middle integer, end integer) (io.HF) {
return let _ := sl.AssertSliceOverlap(raw, middle+2, middle+4) in
let _ := sl.AssertSliceOverlap(raw, middle+4, middle+6) in
let _ := sl.AssertSliceOverlap(raw, middle+6, middle+6+MacLen) in
Expand Down Expand Up @@ -73,7 +73,7 @@ preserves acc(sl.Bytes(raw[start:end], 0, len(raw[start:end])), R55)
ensures BytesToIO_HF(raw, 0, offset, len(raw)) ==
BytesToIO_HF(raw[start:end], 0, offset-start, end-start)
decreases
func WidenBytesHopField(raw []byte, offset int, start int, end int) {
func WidenBytesHopField(raw []byte, offset integer, start integer, end integer) {
unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
unfold acc(sl.Bytes(raw[start:end], 0, len(raw[start:end])), R56)
hfBytes1 := BytesToIO_HF(raw, 0, offset, len(raw))
Expand Down Expand Up @@ -102,7 +102,7 @@ preserves acc(sl.Bytes(raw[offset:offset+HopLen], 0, HopLen), R55)
ensures BytesToIO_HF(raw, 0, offset, len(raw)) ==
BytesToIO_HF(raw[offset:offset+HopLen], 0, 0, HopLen)
decreases
func BytesToAbsHopFieldOffsetEq(raw [] byte, offset int) {
func BytesToAbsHopFieldOffsetEq(raw [] byte, offset integer) {
WidenBytesHopField(raw, offset, offset, offset+HopLen)
}

Expand Down
18 changes: 9 additions & 9 deletions pkg/slayers/path/infofield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,16 @@ import (

ghost
decreases
pure func InfoFieldOffset(currINF, headerOffset int) int {
return headerOffset + InfoLen * currINF
pure func InfoFieldOffset(currINF int, headerOffset integer) integer {
return headerOffset + InfoLen * integer(currINF)
}

ghost
requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) < len(raw)
requires sl.Bytes(raw, 0, len(raw))
decreases
pure func ConsDir(raw []byte, currINF int, headerOffset int) bool {
pure func ConsDir(raw []byte, currINF int, headerOffset integer) bool {
return unfolding sl.Bytes(raw, 0, len(raw)) in
raw[InfoFieldOffset(currINF, headerOffset)] & 0x1 == 0x1
}
Expand All @@ -44,7 +44,7 @@ requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) < len(raw)
requires sl.Bytes(raw, 0, len(raw))
decreases
pure func Peer(raw []byte, currINF int, headerOffset int) bool {
pure func Peer(raw []byte, currINF int, headerOffset integer) bool {
return unfolding sl.Bytes(raw, 0, len(raw)) in
raw[InfoFieldOffset(currINF, headerOffset)] & 0x2 == 0x2
}
Expand All @@ -54,7 +54,7 @@ requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
requires sl.Bytes(raw, 0, len(raw))
decreases
pure func Timestamp(raw []byte, currINF int, headerOffset int) io.Ainfo {
pure func Timestamp(raw []byte, currINF int, headerOffset integer) io.Ainfo {
return let idx := InfoFieldOffset(currINF, headerOffset)+4 in
unfolding sl.Bytes(raw, 0, len(raw)) in
let _ := sl.AssertSliceOverlap(raw, idx, idx+4) in
Expand All @@ -66,7 +66,7 @@ requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
requires sl.Bytes(raw, 0, len(raw))
decreases
pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.MsgTerm] {
pure func AbsUinfo(raw []byte, currINF int, headerOffset integer) set[io.MsgTerm] {
return let idx := InfoFieldOffset(currINF, headerOffset)+2 in
unfolding sl.Bytes(raw, 0, len(raw)) in
let _ := sl.AssertSliceOverlap(raw, idx, idx+2) in
Expand All @@ -79,7 +79,7 @@ requires 0 <= middle
requires middle+InfoLen <= len(raw)
requires sl.Bytes(raw, 0, len(raw))
decreases
pure func BytesToAbsInfoField(raw [] byte, middle int) (io.AbsInfoField) {
pure func BytesToAbsInfoField(raw [] byte, middle integer) (io.AbsInfoField) {
return unfolding sl.Bytes(raw, 0, len(raw)) in
BytesToAbsInfoFieldHelper(raw, middle)
}
Expand All @@ -90,7 +90,7 @@ requires middle+InfoLen <= len(raw)
requires forall i int :: { &raw[i] } middle <= i && i < len(raw) ==>
acc(&raw[i])
decreases
pure func BytesToAbsInfoFieldHelper(raw [] byte, middle int) (io.AbsInfoField) {
pure func BytesToAbsInfoFieldHelper(raw [] byte, middle integer) (io.AbsInfoField) {
return let _ := sl.AssertSliceOverlap(raw, middle+2, middle+4) in
let _ := sl.AssertSliceOverlap(raw, middle+4, middle+8) in
io.AbsInfoField {
Expand All @@ -109,7 +109,7 @@ preserves acc(sl.Bytes(raw[middle:middle+InfoLen], 0, InfoLen), R55)
ensures BytesToAbsInfoField(raw, middle) ==
BytesToAbsInfoField(raw[middle:middle+InfoLen], 0)
decreases
func BytesToAbsInfoFieldOffsetEq(raw [] byte, middle int) {
func BytesToAbsInfoFieldOffsetEq(raw [] byte, middle integer) {
start := middle
end := middle+InfoLen
unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
Expand Down
1 change: 1 addition & 0 deletions pkg/slayers/path/scion/base.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,7 @@ func (s *Base) infIndexForHF(hf uint8) (r uint8) {
// @ pure
// @ requires s.Mem()
// @ ensures r >= MetaLen
// @ ensures r <= MetaLen + MaxINFs * path.InfoLen + MaxHops * path.HopLen
// @ decreases
func (s *Base) Len() (r int) {
return /*@ unfolding s.Mem() in @*/ MetaLen + s.NumINF*path.InfoLen + s.NumHops*path.HopLen
Expand Down
8 changes: 4 additions & 4 deletions pkg/slayers/path/scion/decoded.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,8 +155,8 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
//@ invariant b !== ubuf ==> sl.Bytes(b, 0, len(b))
//@ invariant s.LenSpec(ubuf) <= len(b)
//@ invariant 0 <= i && i <= s.getLenInfoFields(ubuf)
//@ invariant offset == MetaLen + i * path.InfoLen
//@ invariant MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + s.getLenHopFields(ubuf) * path.HopLen <= len(b)
//@ invariant integer(offset) == MetaLen + path.InfoLen * integer(i)
//@ invariant MetaLen + path.InfoLen * integer(s.getLenInfoFields(ubuf)) + path.HopLen * integer(s.getLenHopFields(ubuf)) <= len(b)
//@ decreases s.getLenInfoFields(ubuf) - i
// (VerifiedSCION) TODO: reinstate the original range clause
// for _, info := range s.InfoFields {
Expand All @@ -182,8 +182,8 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
//@ invariant b !== ubuf ==> sl.Bytes(b, 0, len(b))
//@ invariant s.LenSpec(ubuf) <= len(b)
//@ invariant 0 <= i && i <= s.getLenHopFields(ubuf)
//@ invariant offset == MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + i * path.HopLen
//@ invariant MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + s.getLenHopFields(ubuf) * path.HopLen <= len(b)
//@ invariant integer(offset) == MetaLen + path.InfoLen * integer(s.getLenInfoFields(ubuf)) + path.HopLen * integer(i)
//@ invariant MetaLen + path.InfoLen * integer(s.getLenInfoFields(ubuf)) + path.HopLen * integer(s.getLenHopFields(ubuf)) <= len(b)
//@ decreases s.getLenHopFields(ubuf)-i
// (VerifiedSCION) TODO: reinstate the original range clause
// for _, hop := range s.HopFields {
Expand Down
30 changes: 15 additions & 15 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,12 +57,12 @@ ghost
requires segs.Valid()
requires 0 <= currInfIdx
decreases
pure func HopfieldsStartIdx(currInfIdx int, segs io.SegLens) int {
pure func HopfieldsStartIdx(currInfIdx int, segs io.SegLens) integer {
return let numInf := segs.NumInfoFields() in
let infOffset := path.InfoFieldOffset(numInf, MetaLen) in
(currInfIdx == 0 || currInfIdx == 4) ? infOffset :
currInfIdx == 1 ? infOffset + segs.Seg1Len * path.HopLen :
infOffset + (segs.Seg1Len + segs.Seg2Len) * path.HopLen
currInfIdx == 1 ? infOffset + integer(segs.Seg1Len) * path.HopLen :
infOffset + (integer(segs.Seg1Len) + integer(segs.Seg2Len)) * path.HopLen
}

// HopfieldsStartIdx returns index of the last byte of the hopfields of a segment
Expand All @@ -74,12 +74,12 @@ ghost
requires segs.Valid()
requires 0 <= currInfIdx
decreases
pure func HopfieldsEndIdx(currInfIdx int, segs io.SegLens) int {
pure func HopfieldsEndIdx(currInfIdx int, segs io.SegLens) integer {
return let numInf := segs.NumInfoFields() in
let infOffset := path.InfoFieldOffset(numInf, MetaLen) in
(currInfIdx == 0 || currInfIdx == 4) ? infOffset + segs.Seg1Len * path.HopLen :
currInfIdx == 1 ? infOffset + (segs.Seg1Len + segs.Seg2Len) * path.HopLen :
infOffset + (segs.Seg1Len + segs.Seg2Len + segs.Seg3Len) * path.HopLen
(currInfIdx == 0 || currInfIdx == 4) ? infOffset + integer(segs.Seg1Len) * path.HopLen :
currInfIdx == 1 ? infOffset + (integer(segs.Seg1Len) + integer(segs.Seg2Len)) * path.HopLen :
infOffset + (integer(segs.Seg1Len) + integer(segs.Seg2Len) + integer(segs.Seg3Len)) * path.HopLen
}

// HopfieldsStartIdx returns returns the byte slice of the hopfields of a segment
Expand Down Expand Up @@ -223,7 +223,7 @@ requires 0 <= currHfIdx && currHfIdx <= SegLen
requires SegLen * path.HopLen == len(hopfields)
requires sl.Bytes(hopfields, 0, len(hopfields))
decreases
pure func CurrSegWithInfo(hopfields []byte, currHfIdx int, SegLen int, inf io.AbsInfoField) io.Seg {
pure func CurrSegWithInfo(hopfields []byte, currHfIdx integer, SegLen integer, inf io.AbsInfoField) io.Seg {
return segment(hopfields, 0, currHfIdx, inf.AInfo, inf.UInfo, inf.ConsDir, inf.Peer, SegLen)
}

Expand Down Expand Up @@ -314,7 +314,7 @@ pure func MidSegWithInfo(
ghost
requires path.InfoFieldOffset(currInfIdx, MetaLen) + path.InfoLen <= offset
requires 0 < SegLen
requires offset + path.HopLen * SegLen <= len(raw)
requires offset + path.HopLen * (SegLen) <= len(raw)
requires 0 <= currHfIdx && currHfIdx <= SegLen
requires 0 <= currInfIdx && currInfIdx < 3
preserves acc(sl.Bytes(raw, 0, len(raw)), R50)
Expand All @@ -324,7 +324,7 @@ ensures let inf := path.BytesToAbsInfoField(InfofieldByteSlice(raw, currInfIdx
CurrSegWithInfo(raw[offset:offset + SegLen * path.HopLen], currHfIdx, SegLen, inf) ==
CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen)
decreases
func CurrSegEquality(raw []byte, offset int, currInfIdx int, currHfIdx int, SegLen int) {
func CurrSegEquality(raw []byte, offset integer, currInfIdx int, currHfIdx integer, SegLen integer) {
infoBytes := InfofieldByteSlice(raw, currInfIdx)
inf := reveal path.BytesToAbsInfoField(infoBytes, 0)
infOffset := path.InfoFieldOffset(currInfIdx, MetaLen)
Expand Down Expand Up @@ -366,7 +366,7 @@ preserves acc(sl.Bytes(raw, 0, len(raw)), R50)
ensures CurrSegWithInfo(raw, currHfIdx, SegLen, inf1).UpdateCurrSeg(inf2) ==
CurrSegWithInfo(raw, currHfIdx, SegLen, inf2)
decreases
func UpdateCurrSegInfo(raw []byte, currHfIdx int, SegLen int,
func UpdateCurrSegInfo(raw []byte, currHfIdx integer, SegLen integer,
inf1 io.AbsInfoField, inf2 io.AbsInfoField) {
seg1 := reveal CurrSegWithInfo(raw, currHfIdx, SegLen, inf1)
seg2 := reveal CurrSegWithInfo(raw, currHfIdx, SegLen, inf2)
Expand Down Expand Up @@ -574,7 +574,7 @@ requires let currHfStart := currHfIdx * path.HopLen in
sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen) &&
sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen)
decreases
pure func BytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) bool {
pure func BytesStoreCurrSeg(hopfields []byte, currHfIdx integer, segLen integer, inf io.AbsInfoField) bool {
return let currseg := CurrSegWithInfo(hopfields, currHfIdx, segLen, inf) in
let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
Expand Down Expand Up @@ -605,7 +605,7 @@ preserves let currHfStart := currHfIdx * path.HopLen in
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), R49)
ensures BytesStoreCurrSeg(hopfields, currHfIdx, segLen, inf)
decreases
func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) {
func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx integer, segLen integer, inf io.AbsInfoField) {
currseg := reveal CurrSegWithInfo(hopfields, currHfIdx, segLen, inf)
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
Expand Down Expand Up @@ -633,7 +633,7 @@ ensures let currHfStart := currHfIdx * path.HopLen in
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), p) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), p)
decreases
func SplitHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
func SplitHopfields(hopfields []byte, currHfIdx integer, segLen integer, p perm) {
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
sl.SplitByIndex_Bytes(hopfields, 0, len(hopfields), currHfStart, p)
Expand All @@ -657,7 +657,7 @@ requires let currHfStart := currHfIdx * path.HopLen in
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), p)
ensures acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
decreases
func CombineHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
func CombineHopfields(hopfields []byte, currHfIdx integer, segLen integer, p perm) {
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
sl.Unslice_Bytes(hopfields, currHfEnd, len(hopfields), p)
Expand Down
Loading
Loading