From 06e22bb1af1949d5cde5432c7e5d0edd33bedde7 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 9 Jul 2024 19:32:46 +0200 Subject: [PATCH] Revert "stronger precondition for setHopfield" --- .../path/scion/info_hop_setter_lemmas.gobra | 122 +----------------- pkg/slayers/path/scion/raw.go | 27 ++-- 2 files changed, 17 insertions(+), 132 deletions(-) diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra index a56e32a3a..04aa00308 100644 --- a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra +++ b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra @@ -545,39 +545,6 @@ func MidSegEquality(raw []byte, currInfIdx int, segs io.SegLens) { } } -ghost -requires segs.Valid() -requires PktLen(segs, MetaLen) <= len(raw) -requires 0 <= currInfIdx && currInfIdx < 3 -preserves acc(sl.Bytes(raw, 0, len(raw)), R48) -preserves (currInfIdx == 0 && segs.Seg2Len > 0) || - (currInfIdx == 1 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ==> - let infoBytes := InfofieldByteSlice(raw, currInfIdx + 1) in - let hopBytes := HopfieldsByteSlice(raw, currInfIdx + 1, segs) in - acc(sl.Bytes(infoBytes, 0, path.InfoLen), R48) && - acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R48) -preserves (currInfIdx == 1 && segs.Seg2Len > 0) || - (currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ==> - let infoBytes := InfofieldByteSlice(raw, currInfIdx - 1) in - let hopBytes := HopfieldsByteSlice(raw, currInfIdx - 1, segs) in - acc(sl.Bytes(infoBytes, 0, path.InfoLen), R48) && - acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R48) -preserves (segs.Seg2Len > 0 && segs.Seg3Len > 0 && - (currInfIdx == 0 || currInfIdx == 2)) ==> - let infoBytes := InfofieldByteSlice(raw, currInfIdx + 2) in - let hopBytes := HopfieldsByteSlice(raw, currInfIdx + 2, segs) in - acc(sl.Bytes(infoBytes, 0, path.InfoLen), R48) && - acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R48) -ensures LeftSegEqualitySpec(raw, currInfIdx + 1, segs) -ensures MidSegEqualitySpec(raw, currInfIdx + 2, segs) -ensures RightSegEqualitySpec(raw, currInfIdx - 1, segs) -decreases -func AllNotCurrSegEquality(raw []byte, currInfIdx int, segs io.SegLens) { - LeftSegEquality(raw, currInfIdx + 1, segs) - MidSegEquality(raw, currInfIdx + 2, segs) - RightSegEquality(raw, currInfIdx - 1, segs) -} - // `BytesStoreCurrSeg(hopfields, currHfIdx, segLen, inf)` holds iff `hopfields` contains the // serialization of the hopfields of the current segment, which has been traversed until the // `currHfIdx`-th hop (out of `segLen` hops in total). @@ -729,91 +696,4 @@ func CombineHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) { sl.Unslice_Bytes(hopfields, 0, currHfStart, p) sl.CombineAtIndex_Bytes(hopfields, currHfStart, len(hopfields), currHfEnd, p) sl.CombineAtIndex_Bytes(hopfields, 0, len(hopfields), currHfStart, p) -} -/* -ghost -requires segs.Valid() -requires PktLen(segs, MetaLen) <= len(raw) -requires 0 <= currInfIdx && currInfIdx < 3 -requires acc(sl.Bytes(raw, 0, len(raw)), R49) -requires path.InfoFieldOffset(currInfIdx, MetaLen) + path.InfoLen <= offset -requires 0 <= currHfIdx -requires let segLen := segs.LengthOfCurrSeg(currHfIdx) in - let hfIdxSeg := currHfIdx - segs.LengthOfPrevSeg(currHfIdx) in - offset + path.HopLen * segLen <= len(raw) && - 0 <= hfIdxSeg && hfIdxSeg <= segLen -requires let infoBytes0 := InfofieldByteSlice(raw, 0) in - let hopBytes0 := HopfieldsByteSlice(raw, 0, segs) in - acc(sl.Bytes(infoBytes0, 0, path.InfoLen), R49) && - acc(sl.Bytes(hopBytes0, 0, len(hopBytes0)), R49) -requires segs.Seg2Len > 0 ==> - let infoBytes1 := InfofieldByteSlice(raw, 1) in - let hopBytes1 := HopfieldsByteSlice(raw, 1, segs) in - acc(sl.Bytes(infoBytes1, 0, path.InfoLen), R49) && - acc(sl.Bytes(hopBytes1, 0, len(hopBytes1)), R49) -requires segs.Seg3Len > 0 ==> - let infoBytes2 := InfofieldByteSlice(raw, 2) in - let hopBytes2 := HopfieldsByteSlice(raw, 2, segs) in - acc(sl.Bytes(infoBytes2, 0, path.InfoLen), R49) && - acc(sl.Bytes(hopBytes2, 0, len(hopBytes2)), R49) -decreases -pure func testTmp(raw []byte, offset int, currInfIdx int, currHfIdx int, segs io.SegLens) bool { - return let segLen := segs.LengthOfCurrSeg(currHfIdx) in - let hfIdxSeg := currHfIdx - segs.LengthOfPrevSeg(currHfIdx) in - let infoBytes0 := InfofieldByteSlice(raw, currInfIdx) in - let hopBytes0 := HopfieldsByteSlice(raw, currInfIdx, segs) in - let infoBytes1 := InfofieldByteSlice(raw, currInfIdx + 1) in - let hopBytes1 := HopfieldsByteSlice(raw, currInfIdx + 1, segs) in - let infoBytes2 := InfofieldByteSlice(raw, currInfIdx + 2) in - let hopBytes2 := HopfieldsByteSlice(raw, currInfIdx + 2, segs) in - true -}*/ -/* - CurrSegWithInfo(hopfields []byte, currHfIdx int, SegLen int, inf io.AbsInfoField) - LeftSegWithInfo( - hopfields []byte, - currInfIdx int, - segs io.SegLens, - inf option[io.AbsInfoField]) option[io.IO_seg3] - io.IO_Packet2 { - CurrSeg : CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen), - LeftSeg : LeftSeg(raw, currInfIdx + 1, segs, MetaLen), - MidSeg : MidSeg(raw, currInfIdx + 2, segs, MetaLen), - RightSeg : RightSeg(raw, currInfIdx - 1, segs, MetaLen), - } -}*/ - -/* -ghost -opaque -requires acc(sl.Bytes(raw, 0, len(raw)), R56) -requires validPktMetaHdr(raw) -preserves acc(sl.Bytes(raw, 0, len(raw)), R49) -preserves (segs.Seg2Len > 0 && segs.Seg3Len > 0 && - (currInfIdx == 2 || currInfIdx == 4)) ==> - let infoBytes := InfofieldByteSlice(raw, currInfIdx) in - let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in - acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && - acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) -ensures MidSegEqualitySpec(raw, currInfIdx, segs) -decreases -pure func absPktTmp(inf1 ) (res io.IO_pkt2) { - return let _ := reveal validPktMetaHdr(raw) in - let metaHdr := RawBytesToMetaHdr(raw) in - let currInfIdx := int(metaHdr.CurrINF) in - let currHfIdx := int(metaHdr.CurrHF) in - let seg1Len := int(metaHdr.SegLen[0]) in - let seg2Len := int(metaHdr.SegLen[1]) in - let seg3Len := int(metaHdr.SegLen[2]) in - let segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len) in - let segLen := segs.LengthOfCurrSeg(currHfIdx) in - let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in - let numINF := segs.NumInfoFields() in - let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in - io.IO_Packet2 { - CurrSeg : CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen), - LeftSeg : LeftSeg(raw, currInfIdx + 1, segs, MetaLen), - MidSeg : MidSeg(raw, currInfIdx + 2, segs, MetaLen), - RightSeg : RightSeg(raw, currInfIdx - 1, segs, MetaLen), - } -}*/ \ No newline at end of file +} \ No newline at end of file diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go index 5e2c38213..44285830e 100644 --- a/pkg/slayers/path/scion/raw.go +++ b/pkg/slayers/path/scion/raw.go @@ -536,7 +536,6 @@ func (s *Raw) GetCurrentHopField( /*@ ghost ubuf []byte @*/ ) (res path.HopField // @ requires validPktMetaHdr(ubuf) // @ requires s.GetBase(ubuf).EqAbsHeader(ubuf) // @ requires NotFullyTraversedPkt(s.absPkt(ubuf)) -// @ requires int(s.GetCurrHF(ubuf)) == idx // @ ensures acc(s.Mem(ubuf), R20) // @ ensures sl.Bytes(ubuf, 0, len(ubuf)) // @ ensures r != nil ==> r.ErrorMem() @@ -588,33 +587,39 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/) //@ inf := path.BytesToAbsInfoField(InfofieldByteSlice(ubuf, currInfIdx), 0) //@ hfIdxSeg := idx-prevSegLen //@ currHopfields := HopfieldsByteSlice(ubuf, currInfIdx, segLens) - + //@ ghost if idx == currHfIdx { //@ CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen) - //@ AllNotCurrSegEquality(ubuf, currInfIdx, segLens) - // LeftSegEquality(ubuf, currInfIdx+1, segLens) - // MidSegEquality(ubuf, currInfIdx+2, segLens) - // RightSegEquality(ubuf, currInfIdx-1, segLens) + //@ LeftSegEquality(ubuf, currInfIdx+1, segLens) + //@ MidSegEquality(ubuf, currInfIdx+2, segLens) + //@ RightSegEquality(ubuf, currInfIdx-1, segLens) //@ reveal s.absPkt(ubuf) //@ SplitHopfields(currHopfields, hfIdxSeg, segLen, R0) //@ EstablishBytesStoreCurrSeg(currHopfields, hfIdxSeg, segLen, inf) //@ SplitHopfields(currHopfields, hfIdxSeg, segLen, R0) + //@ } else { + //@ sl.SplitRange_Bytes(ubuf[offset:offset+segLen*path.HopLen], hfIdxSeg*path.HopLen, + //@ (hfIdxSeg+1)*path.HopLen, HalfPerm) + //@ } //@ sl.SplitRange_Bytes(ubuf, hopOffset, hopOffset+path.HopLen, HalfPerm) ret := tmpHopField.SerializeTo(s.Raw[hopOffset : hopOffset+path.HopLen]) //@ sl.CombineRange_Bytes(ubuf, hopOffset, hopOffset+path.HopLen, HalfPerm) //@ ValidPktMetaHdrSublice(ubuf, MetaLen) //@ assert reveal validPktMetaHdr(ubuf) - + //@ ghost if idx == currHfIdx { //@ CombineHopfields(currHopfields, hfIdxSeg, segLen, R0) //@ EstablishBytesStoreCurrSeg(currHopfields, hfIdxSeg, segLen, inf) //@ CombineHopfields(currHopfields, hfIdxSeg, segLen, R0) //@ CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen) - //@ AllNotCurrSegEquality(ubuf, currInfIdx, segLens) - // LeftSegEquality(ubuf, currInfIdx+1, segLens) - // MidSegEquality(ubuf, currInfIdx+2, segLens) - // RightSegEquality(ubuf, currInfIdx-1, segLens) + //@ LeftSegEquality(ubuf, currInfIdx+1, segLens) + //@ MidSegEquality(ubuf, currInfIdx+2, segLens) + //@ RightSegEquality(ubuf, currInfIdx-1, segLens) //@ reveal s.absPkt(ubuf) //@ assert s.absPkt(ubuf).CurrSeg.Future == //@ seq[io.IO_HF]{tmpHopField.ToIO_HF()} ++ old(s.absPkt(ubuf).CurrSeg.Future[1:]) + //@ } else { + //@ sl.CombineRange_Bytes(ubuf[offset:offset+segLen*path.HopLen], hfIdxSeg*path.HopLen, + //@ (hfIdxSeg+1)*path.HopLen, HalfPerm) + //@ } //@ CombineBytesFromInfoFields(ubuf[:hopfieldOffset], s.NumINF, segLens, R40) //@ CombineBytesFromSegments(ubuf, segLens, HalfPerm) //@ fold acc(s.Base.Mem(), R50)