From b34f54610c97d74fa0dc1d8eeee620dd1328eb3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 8 Jan 2025 21:47:48 +0100 Subject: [PATCH] backup --- .../path/scion/info_hop_setter_lemmas.gobra | 7 +++-- pkg/slayers/path/scion/raw_spec.gobra | 26 ++++++++++++------- pkg/slayers/path/scion/widen-lemma.gobra | 5 ++++ 3 files changed, 24 insertions(+), 14 deletions(-) diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra index 0e0daf889..2c6f7cea2 100644 --- 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 index 09303ba4d..856ebd813 100644 --- 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 index 2c706646d..69294dc0f 100644 --- 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)