From 0f4646b9c7cbba9b2924cb2eee2d610c972c6582 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 17 Jun 2024 15:53:04 +0200 Subject: [PATCH] fmt --- .../path/scion/info_hop_setter_lemmas.gobra | 38 +++++++++---------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra index 769ee9df3..09e421953 100644 --- a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra +++ b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra @@ -249,10 +249,10 @@ pure func LeftSegWithInfo( segs io.SegLens, inf option[io.AbsInfoField]) option[io.IO_seg3] { return (currInfIdx == 1 && segs.Seg2Len > 0) ? - some(CurrSegWithInfo(hopfields, 0, segs.Seg2Len, get(inf))) : - (currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ? - some(CurrSegWithInfo(hopfields, 0, segs.Seg3Len, get(inf))) : - none[io.IO_seg3] + some(CurrSegWithInfo(hopfields, 0, segs.Seg2Len, get(inf))) : + (currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ? + some(CurrSegWithInfo(hopfields, 0, segs.Seg3Len, get(inf))) : + none[io.IO_seg3] } // RightSegWithInfo returns the abstract representation of the previous segment of a packet. @@ -276,10 +276,10 @@ pure func RightSegWithInfo( segs io.SegLens, inf option[io.AbsInfoField]) option[io.IO_seg3] { return (currInfIdx == 1 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ? - some(CurrSegWithInfo(hopfields, segs.Seg2Len, segs.Seg2Len, get(inf))) : - (currInfIdx == 0 && segs.Seg2Len > 0) ? - some(CurrSegWithInfo(hopfields, segs.Seg1Len, segs.Seg1Len, get(inf))) : - none[io.IO_seg3] + some(CurrSegWithInfo(hopfields, segs.Seg2Len, segs.Seg2Len, get(inf))) : + (currInfIdx == 0 && segs.Seg2Len > 0) ? + some(CurrSegWithInfo(hopfields, segs.Seg1Len, segs.Seg1Len, get(inf))) : + none[io.IO_seg3] } // MidSegWithInfo returns the abstract representation of the last or first segment of a packet. @@ -303,10 +303,10 @@ pure func MidSegWithInfo( segs io.SegLens, inf option[io.AbsInfoField]) option[io.IO_seg3] { return (currInfIdx == 4 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ? - some(CurrSegWithInfo(hopfields, segs.Seg1Len, segs.Seg1Len, get(inf))) : - (currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ? - some(CurrSegWithInfo(hopfields, 0, segs.Seg3Len, get(inf))) : - none[io.IO_seg3] + some(CurrSegWithInfo(hopfields, segs.Seg1Len, segs.Seg1Len, get(inf))) : + (currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ? + some(CurrSegWithInfo(hopfields, 0, segs.Seg3Len, get(inf))) : + none[io.IO_seg3] } // CurrSegEquality ensures that the two definitions of abstract segments, CurrSegWithInfo(..) @@ -496,13 +496,13 @@ decreases pure func MidSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool { return (segs.Seg2Len > 0 && segs.Seg3Len > 0 && (currInfIdx == 2 || currInfIdx == 4)) ? - let infoBytes := InfofieldByteSlice(raw, currInfIdx) in - let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in - let inf := some(path.BytesToAbsInfoField(infoBytes, 0)) in - MidSeg(raw, currInfIdx, segs, MetaLen) == - MidSegWithInfo(hopBytes, currInfIdx, segs, inf) : - MidSeg(raw, currInfIdx, segs, MetaLen) == - MidSegWithInfo(nil, currInfIdx, segs, none[io.AbsInfoField]) + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in + let inf := some(path.BytesToAbsInfoField(infoBytes, 0)) in + MidSeg(raw, currInfIdx, segs, MetaLen) == + MidSegWithInfo(hopBytes, currInfIdx, segs, inf) : + MidSeg(raw, currInfIdx, segs, MetaLen) == + MidSegWithInfo(nil, currInfIdx, segs, none[io.AbsInfoField]) } // MidSegEquality ensures that the two definitions of abstract segments, MidSegWithInfo(..)