Skip to content
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

Jump to bottom

Drop Assumption in SetInfoField #350

Merged
merged 17 commits into from
Jun 13, 2024
Merged

Drop Assumption in SetInfoField #350

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
1b16d0c
proof setInfoField
mlimbeck Jun 4, 2024
f1b567c
fix verification errors
mlimbeck Jun 4, 2024
75a8042
fix syntax error
mlimbeck Jun 4, 2024
af94ea7
fix verification errors
mlimbeck Jun 4, 2024
e25b08c
formatting
mlimbeck Jun 11, 2024
b7aa914
simplification attempt
mlimbeck Jun 11, 2024
0290bc5
Merge branch 'master' into markus-io-spec-setInfoField-proof
mlimbeck Jun 11, 2024
84e8edc
Apply suggestions from code review
mlimbeck Jun 11, 2024
40d7e38
refactoring
mlimbeck Jun 12, 2024
70f0cfe
fix verification error
mlimbeck Jun 12, 2024
d84e9fc
fixed LeftSegEquality()
mlimbeck Jun 12, 2024
fa6ffa7
formatting
mlimbeck Jun 12, 2024
33a26b0
Apply suggestions from code review
mlimbeck Jun 12, 2024
6b8d86d
feedback
mlimbeck Jun 12, 2024
4d5eb49
Merge branch 'master' into markus-io-spec-setInfoField-proof
mlimbeck Jun 13, 2024
58e42f0
renaming AbsSlice_Bytes to Bytes
mlimbeck Jun 13, 2024
85e97e0
adding documentation
mlimbeck Jun 13, 2024
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
4 changes: 4 additions & 0 deletions pkg/slayers/path/infofield.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,8 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
//@ assert &raw[4:8][2] == &raw[6] && &raw[4:8][3] == &raw[7]
inf.Timestamp = binary.BigEndian.Uint32(raw[4:8])
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R50)
//@ assert reveal BytesToIntermediateAbsInfoField(raw, 0, 0, InfoLen) ==
//@ inf.ToIntermediateAbsInfoField()
return nil
}

Expand Down Expand Up @@ -127,6 +129,8 @@ func (inf *InfoField) SerializeTo(b []byte) (err error) {
//@ ghost tmpInfo4 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
//@ assert tmpInfo4.AInfo == targetAbsInfo.AInfo
//@ fold slices.AbsSlice_Bytes(b, 0, InfoLen)
//@ assert inf.ToIntermediateAbsInfoField() ==
//@ reveal BytesToIntermediateAbsInfoField(b, 0, 0, InfoLen)
return nil
}

Expand Down
1 change: 1 addition & 0 deletions pkg/slayers/path/infofield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ type IntermediateAbsInfoField adt {
}

ghost
opaque
requires 0 <= start && start <= middle
requires middle+InfoLen <= end && end <= len(raw)
requires acc(sl.AbsSlice_Bytes(raw, start, end), _)
Expand Down
83 changes: 49 additions & 34 deletions pkg/slayers/path/scion/raw.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ oldSeg3Len := int(s.PathMeta.SegLen[2])
//@ oldSegLen := LengthOfCurrSeg(oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ oldPrevSegLen := LengthOfPrevSeg(oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ oldOffset := HopFieldOffset(s.Base.NumINF, 0, 0)
//@ oldOffset := HopFieldOffset(s.Base.NumINF, oldPrevSegLen, 0)
//@ fold acc(s.Base.Mem(), R56)
if err := s.Base.IncPath(); err != nil {
//@ fold s.NonInitMem()
Expand All @@ -264,14 +264,13 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ sl.Reslice_Bytes(ubuf, MetaLen, len(ubuf), HalfPerm)
//@ tail := ubuf[MetaLen:]
//@ unfold acc(sl.AbsSlice_Bytes(tail, 0, len(tail)), R50)
//@ oldoffsetWithHops := oldOffset + path.HopLen * oldPrevSegLen
//@ oldHfIdxSeg := oldCurrHfIdx-oldPrevSegLen
//@ WidenCurrSeg(ubuf, oldoffsetWithHops + MetaLen, oldCurrInfIdx, oldHfIdxSeg,
//@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg,
//@ oldSegLen, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ LenCurrSeg(tail, oldoffsetWithHops, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
//@ LenCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
//@ oldAbsPkt := reveal s.absPkt(ubuf)
//@ sl.SplitRange_Bytes(ubuf, 0, MetaLen, HalfPerm)
//@ unfold acc(s.Base.Mem(), R2)
Expand All @@ -295,8 +294,8 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ assert currHfIdx == oldCurrHfIdx + 1

//@ ghost if(currInfIdx == oldCurrInfIdx) {
//@ IncCurrSeg(tail, oldoffsetWithHops, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
//@ WidenCurrSeg(ubuf, oldoffsetWithHops + MetaLen, oldCurrInfIdx, oldHfIdxSeg + 1,
//@ IncCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
//@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg + 1,
//@ oldSegLen, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
Expand All @@ -305,7 +304,7 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ } else {
//@ segLen := LengthOfCurrSeg(currHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ prevSegLen := LengthOfPrevSeg(currHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ offsetWithHops := oldOffset + path.HopLen * prevSegLen + MetaLen
//@ offsetWithHops := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
//@ hfIdxSeg := currHfIdx-prevSegLen
//@ XoverSegNotNone(tail, oldCurrInfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ XoverCurrSeg(tail, oldCurrInfIdx + 1, oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
Expand Down Expand Up @@ -355,8 +354,10 @@ func (s *Raw) GetInfoField(idx int /*@, ghost ubuf []byte @*/) (ifield path.Info
//@ sl.CombineRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, R21)
//@ unfold acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R56)
//@ unfold acc(sl.AbsSlice_Bytes(ubuf[infOffset : infOffset+path.InfoLen], 0, path.InfoLen), R56)
//@ assert reveal path.BytesToIntermediateAbsInfoField(ubuf, 0, infOffset, len(ubuf)) ==
//@ reveal path.BytesToIntermediateAbsInfoField(ubuf[infOffset : infOffset+path.InfoLen], 0, 0, path.InfoLen)
//@ assert info.ToIntermediateAbsInfoField() ==
//@ path.BytesToIntermediateAbsInfoField(ubuf, 0, infOffset, len(ubuf))
//@ reveal path.BytesToIntermediateAbsInfoField(ubuf, 0, infOffset, len(ubuf))
//@ fold acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R56)
//@ fold acc(sl.AbsSlice_Bytes(ubuf[infOffset : infOffset+path.InfoLen], 0, path.InfoLen), R56)
//@ sl.CombineRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, R21)
Expand Down Expand Up @@ -397,54 +398,68 @@ func (s *Raw) GetCurrentInfoField( /*@ ghost ubuf []byte @*/ ) (res path.InfoFie
// @ ensures sl.AbsSlice_Bytes(ubuf, 0, len(ubuf))
// @ ensures r != nil ==> r.ErrorMem()
// posts for IO:
// @ ensures r == nil && idx == int(old(s.GetCurrINF(ubuf))) ==>
// @ ensures r == nil ==>
// @ validPktMetaHdr(ubuf) && s.EqAbsHeader(ubuf)
// @ ensures r == nil && idx == int(old(s.GetCurrINF(ubuf))) ==>
// @ let oldPkt := old(s.absPkt(ubuf)) in
// @ let newPkt := AbsSetInfoField(oldPkt, info.ToIntermediateAbsInfoField()) in
// @ s.absPkt(ubuf) == newPkt
// @ decreases
// @ #backend[exhaleMode(1)]
func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @*/) (r error) {
//@ share info
//@ ghost oldCurrINF := int(old(s.GetCurrINF(ubuf)))
//@ reveal validPktMetaHdr(ubuf)
//@ unfold acc(s.Mem(ubuf), R50)
//@ unfold acc(s.Base.Mem(), R50)
//@ currInfIdx := int(s.PathMeta.CurrINF)
//@ currHfIdx := int(s.PathMeta.CurrHF)
//@ seg1Len := int(s.PathMeta.SegLen[0])
//@ seg2Len := int(s.PathMeta.SegLen[1])
//@ seg3Len := int(s.PathMeta.SegLen[2])
//@ segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len)
//@ prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len)
//@ offset := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
//@ hopfieldOffset := MetaLen + s.NumINF*path.InfoLen
if idx >= s.NumINF {
err := serrors.New("InfoField index out of bounds", "max", s.NumINF-1, "actual", idx)
//@ fold acc(s.Base.Mem(), R50)
//@ fold acc(s.Mem(ubuf), R50)
return err
}
infOffset := MetaLen + idx*path.InfoLen
//@ assert idx == oldCurrINF ==> reveal validPktMetaHdr(ubuf)
//@ assert idx == oldCurrINF ==> s.EqAbsHeader(ubuf)

//@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm)
//@ ValidPktMetaHdrSublice(ubuf, len(s.Raw))
//@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm)
//@ assert idx == oldCurrINF ==> RawBytesToBase(ubuf[:len(s.Raw)]).ValidCurrIdxsSpec()

//@ assert sl.AbsSlice_Bytes(s.Raw, 0, len(s.Raw))
//@ sl.SplitRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm)
//@ assert acc(sl.AbsSlice_Bytes(s.Raw, 0, infOffset), HalfPerm)
//@ sl.Reslice_Bytes(s.Raw, 0, infOffset, HalfPerm/2)
//@ ValidPktMetaHdrSublice(s.Raw, infOffset)
//@ sl.SplitRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm)
//@ assert idx == oldCurrINF ==> RawBytesToBase(s.Raw[:infOffset]).ValidCurrIdxsSpec()
//@ SliceBytesbyInfoFields(ubuf, MetaLen, s.NumINF, HalfPerm)
//@ SliceBytesbySegments(ubuf[hopfieldOffset:], 0, seg1Len, seg2Len, seg3Len, HalfPerm)

//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
//@ oldInfo := path.BytesToIntermediateAbsInfoField(ubuf[infOffset : infOffset+path.InfoLen], 0, 0, path.InfoLen)
//@ newInfo := info.ToIntermediateAbsInfoField()
//@ hfIdxSeg := currHfIdx-prevSegLen
//@ hopfields := ubuf[offset:offset + segLen*path.HopLen]
//@ ghost if(idx == currInfIdx) {
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
//@ CurrSegEqLemma(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
//@ LeftSegEqLemma(ubuf, currInfIdx+1, seg1Len, seg2Len, seg3Len)
//@ MidSegEqLemma(ubuf, currInfIdx+2, seg1Len, seg2Len, seg3Len)
//@ RightSegEqLemma(ubuf, currInfIdx-1, seg1Len, seg2Len, seg3Len)
//@ }
//@ reveal s.absPkt(ubuf)
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
//@ sl.SplitRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, HalfPerm)
ret := info.SerializeTo(s.Raw[infOffset : infOffset+path.InfoLen])
//@ sl.CombineRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm)
//@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm)
//@ ValidPktMetaHdrSublice(ubuf, infOffset)

//@ sl.Unslice_Bytes(s.Raw, 0, infOffset, HalfPerm/2)
//@ sl.CombineRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm)
//@ assert idx == oldCurrINF ==> RawBytesToBase(ubuf).ValidCurrIdxsSpec()
//@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm)
//@ sl.CombineRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, HalfPerm)
//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
//@ assert reveal validPktMetaHdr(ubuf)
//@ ghost if(idx == currInfIdx) {
//@ CurrSegEqLemma(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
//@ CurrSegEqLemma2(hopfields, hfIdxSeg, segLen, oldInfo, newInfo)
//@ LeftSegEqLemma(ubuf, currInfIdx+1, seg1Len, seg2Len, seg3Len)
//@ MidSegEqLemma(ubuf, currInfIdx+2, seg1Len, seg2Len, seg3Len)
//@ RightSegEqLemma(ubuf, currInfIdx-1, seg1Len, seg2Len, seg3Len)
//@ reveal s.absPkt(ubuf)
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
//@ }
//@ CombineBytesbySegments(ubuf[hopfieldOffset:], 0, seg1Len, seg2Len, seg3Len, HalfPerm)
//@ CombineBytesbyInfoFields(ubuf, MetaLen, s.NumINF, HalfPerm)
//@ fold acc(s.Base.Mem(), R50)
//@ fold acc(s.Mem(ubuf), R50)
//@ assert idx == oldCurrINF ==> reveal validPktMetaHdr(ubuf)
//@ TemporaryAssumeForIO(idx == oldCurrINF ==> s.absPkt(ubuf) == AbsSetInfoField(old(s.absPkt(ubuf)), info.ToIntermediateAbsInfoField()))
return ret
}

Expand Down
Loading
Loading