backup

viperproject · Jan 8, 2025 · b34f546 · b34f546
1 parent 11eada7
commit b34f546
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 14 deletions.
diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
@@ -320,7 +320,7 @@ requires  0 <= currInfIdx && currInfIdx < 3
 preserves acc(sl.Bytes(raw, 0, len(raw)), R50)
 preserves acc(sl.Bytes(raw[offset:offset + SegLen * path.HopLen], 0, SegLen * path.HopLen), R50)
 preserves acc(sl.Bytes(InfofieldByteSlice(raw, currInfIdx), 0, path.InfoLen), R50)
-ensures let inf := path.BytesToAbsInfoField(InfofieldByteSlice(raw, currInfIdx), 0) in
+ensures   let inf := path.BytesToAbsInfoField(InfofieldByteSlice(raw, currInfIdx), 0) in
 	CurrSegWithInfo(raw[offset:offset + SegLen * path.HopLen], currHfIdx, SegLen, inf) ==
 	CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen)
 decreases
@@ -331,9 +331,8 @@ func CurrSegEquality(raw []byte, offset int, currInfIdx int, currHfIdx int, SegL
 	unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	unfold acc(sl.Bytes(infoBytes, 0, path.InfoLen), R56)
 	path.BytesToAbsInfoFieldOffsetEq(raw, infOffset)
-	// TODO: drop reveal
-	assert /*reveal*/ path.BytesToAbsInfoField(raw, infOffset) ==
-		/*reveal*/ path.BytesToAbsInfoField(infoBytes, 0)
+	assert path.BytesToAbsInfoField(raw, infOffset) ==
+		path.BytesToAbsInfoField(infoBytes, 0)
 	reveal CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen)
 	reveal CurrSegWithInfo(raw[offset:offset + SegLen * path.HopLen], currHfIdx, SegLen, inf)
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)

diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
@@ -372,6 +372,7 @@ opaque
 requires sl.Bytes(raw, 0, len(raw))
 requires validPktMetaHdr(raw)
 decreases
+// TODO: rename this to View()
 pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
 	return let _ := reveal validPktMetaHdr(raw) in
 		let metaHdr := RawBytesToMetaHdr(raw)  in
@@ -386,10 +387,10 @@ pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
 		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),
+			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),
 		}
 }
 
@@ -675,7 +676,7 @@ ensures   s.EqAbsInfoField(s.absPkt(ubuf), info.ToAbsInfoField())
 ensures   s.EqAbsHopField(s.absPkt(ubuf), hop.ToIO_HF())
 decreases
 func (s *Raw) DecodingLemma(ubuf []byte, info path.InfoField, hop path.HopField) {
-	reveal validPktMetaHdr(ubuf)
+	assert reveal validPktMetaHdr(ubuf)
 	metaHdr := RawBytesToMetaHdr(ubuf)
 	currInfIdx := int(metaHdr.CurrINF)
 	currHfIdx := int(metaHdr.CurrHF)
@@ -688,13 +689,18 @@ func (s *Raw) DecodingLemma(ubuf []byte, info path.InfoField, hop path.HopField)
 	numINF := segs.NumInfoFields()
 	offset := HopFieldOffset(numINF, prevSegLen, MetaLen)
 	hfIdxSeg := currHfIdx - prevSegLen
-	reveal s.CorrectlyDecodedInf(ubuf, info)
-	reveal s.CorrectlyDecodedHf(ubuf, hop)
-	reveal s.absPkt(ubuf)
+	assert reveal s.CorrectlyDecodedInf(ubuf, info)
+	assert reveal s.CorrectlyDecodedHf(ubuf, hop)
+
 	reveal CurrSeg(ubuf, offset, currInfIdx, hfIdxSeg, segLen, MetaLen)
 	HopsFromPrefixOfRawMatchPrefixOfHops(ubuf, offset, 0, segLen, hfIdxSeg)
-	assert reveal s.EqAbsInfoField(s.absPkt(ubuf), info.ToAbsInfoField())
-	assert reveal s.EqAbsHopField(s.absPkt(ubuf), hop.ToIO_HF())
+
+	pktView := reveal s.absPkt(ubuf)
+	infoView := info.ToAbsInfoField()
+
+	assert pktView.CurrSeg.Peer == infoView.Peer
+	assert reveal s.EqAbsInfoField(pktView, infoView)
+	assert reveal s.EqAbsHopField(pktView, hop.ToIO_HF())
 }
 
 ghost

diff --git a/pkg/slayers/path/scion/widen-lemma.gobra b/pkg/slayers/path/scion/widen-lemma.gobra
@@ -50,10 +50,15 @@ func WidenCurrSeg(raw []byte,
 
 	ainfo1 := path.Timestamp(raw, currInfIdx, headerOffset)
 	ainfo2 := path.Timestamp(raw[start:length], currInfIdx, headerOffset-start)
+	sl.AssertSliceOverlap(raw, start, length)
+	idxTimestamp := path.InfoFieldOffset(currInfIdx, headerOffset-start)+4
+	sl.AssertSliceOverlap(raw[start:length], idxTimestamp, idxTimestamp+4)
 	assert ainfo1 == ainfo2
 
 	uinfo1 := path.AbsUinfo(raw, currInfIdx, headerOffset)
 	uinfo2 := path.AbsUinfo(raw[start:length], currInfIdx, headerOffset-start)
+	idxUinfo := path.InfoFieldOffset(currInfIdx, headerOffset-start)+2
+	sl.AssertSliceOverlap(raw[start:length], idxUinfo, idxUinfo+2)
 	assert uinfo1 == uinfo2
 
 	consDir1 := path.ConsDir(raw, currInfIdx, headerOffset)