Skip to content

Commit

Permalink
Revert "stronger precondition for setHopfield"
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Jul 9, 2024
1 parent 580c387 commit 06e22bb
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 132 deletions.
122 changes: 1 addition & 121 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down Expand Up @@ -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),
}
}*/
}
27 changes: 16 additions & 11 deletions pkg/slayers/path/scion/raw.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 06e22bb

Please sign in to comment.