From 732a598665f8faa1dcc28031d3ece12744bcd53f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 17 Apr 2024 20:24:04 +0200 Subject: [PATCH 01/15] Update gobra.yml --- .github/workflows/gobra.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml index f16eae5a2..17afc680a 100644 --- a/.github/workflows/gobra.yml +++ b/.github/workflows/gobra.yml @@ -418,7 +418,7 @@ jobs: parallelizeBranches: '1' # The following flag has a significant influence on the number of branches verified. # Without it, verification would take a lot longer. - conditionalizePermissions: '1' + conditionalizePermissions: '0' imageVersion: ${{ env.imageVersion }} mceMode: 'on' requireTriggers: ${{ env.requireTriggers }} From 7a0416312df524805b1f5c9fec2012ff0cf3f9b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 17 Apr 2024 20:24:56 +0200 Subject: [PATCH 02/15] Update gobra.yml --- .github/workflows/gobra.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml index 17afc680a..53d4c6210 100644 --- a/.github/workflows/gobra.yml +++ b/.github/workflows/gobra.yml @@ -416,8 +416,6 @@ jobs: assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }} checkConsistency: ${{ env.checkConsistency }} parallelizeBranches: '1' - # The following flag has a significant influence on the number of branches verified. - # Without it, verification would take a lot longer. conditionalizePermissions: '0' imageVersion: ${{ env.imageVersion }} mceMode: 'on' From e52368507e796f4c286613789cf19f1e72cbf835 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 17 Apr 2024 22:11:23 +0200 Subject: [PATCH 03/15] fix verification error --- router/dataplane.go | 9 ++++++--- router/io-spec-abstract-transitions.gobra | 8 ++++---- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 2e69a0c3a..4c650aea9 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2678,14 +2678,14 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost dp io.DataPla var err error if p.hopField, err = p.path.GetCurrentHopField( /*@ ubPath @*/ ); err != nil { // @ ghost sl.CombineRange_Bytes(ub, startP, endP, writePerm) - // @ fold p.scionLayer.Mem(ub) + // @ fold acc(p.scionLayer.Mem(ub), 1-R55) // @ p.scionLayer.DowngradePerm(ub) // TODO parameter problem invalid path return processResult{}, err } if p.infoField, err = p.path.GetCurrentInfoField( /*@ ubPath @*/ ); err != nil { // @ ghost sl.CombineRange_Bytes(ub, startP, endP, writePerm) - // @ fold p.scionLayer.Mem(ub) + // @ fold acc(p.scionLayer.Mem(ub), 1-R55) // @ p.scionLayer.DowngradePerm(ub) // TODO parameter problem invalid path return processResult{}, err @@ -2696,6 +2696,8 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost dp io.DataPla // @ TemporaryAssumeForIO(len(get(old(absPkt(dp, ub)).LeftSeg).History) == 0) // @ TemporaryAssumeForIO(slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub)) // @ TemporaryAssumeForIO(absPkt(dp, ub) == AbsDoXover(old(absPkt(dp, ub)))) + // @ TemporaryAssumeForIO(p.EqAbsHopField(absPkt(dp, ub))) + // @ TemporaryAssumeForIO(p.EqAbsInfoField(absPkt(dp, ub))) // @ fold acc(p.scionLayer.Mem(ub), 1-R55) return processResult{}, nil } @@ -3165,7 +3167,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ newAbsPkt.isIO_val_Unsupported // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{}) // @ decreases 0 if sync.IgnoreBlockingForTermination() -// @ #backend[stateConsolidationMode(6)] +// @ #backend[moreJoins(1)] func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock *sync.Mutex, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { // @ ghost var oldPkt io.IO_pkt2 // @ ghost if(slayers.IsSupportedPkt(ub)) { @@ -3266,6 +3268,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, return r, serrors.WithCtx(err, "info", "after xover") /*@, false, absReturnErr(dp, r) @*/ } // @ assert AbsVerifyCurrentMACConstraint(nextPkt, dp) + // @ unfold acc(p.scionLayer.Mem(ub), R3) } // @ fold acc(p.scionLayer.Mem(ub), R3) // @ assert p.segmentChange ==> nextPkt.RightSeg != none[io.IO_seg2] diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index 2d36d4054..6b9d7cd36 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -212,9 +212,9 @@ requires len(get(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID).LeftSeg).Fu requires len(get(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID).LeftSeg).History) == 0 requires AbsVerifyCurrentMACConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), dp) requires AbsValidateEgressIDConstraintXover(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), dp) -requires AbsEgressInterfaceConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), egressID) -requires egressID == none[io.IO_ifs] ==> newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)) -requires egressID != none[io.IO_ifs] ==> newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))) +requires egressID != none[io.IO_ifs] ==> AbsEgressInterfaceConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), egressID) +requires (egressID == none[io.IO_ifs] ==> newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))) || + (egressID != none[io.IO_ifs] ==> newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)))) preserves acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>; ensures dp.Valid() ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) @@ -227,8 +227,8 @@ func XoverEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt reveal AbsVerifyCurrentMACConstraint(intermediatePkt1, dp) reveal AbsVerifyCurrentMACConstraint(intermediatePkt2, dp) reveal AbsValidateEgressIDConstraintXover(intermediatePkt2, dp) - reveal AbsEgressInterfaceConstraint(intermediatePkt2, egressID) if(egressID != none[io.IO_ifs]){ + reveal AbsEgressInterfaceConstraint(intermediatePkt2, egressID) reveal AbsProcessEgress(intermediatePkt2) } AtomicXover(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp) From 6382fe01a9ef3912a6002b9acbfe8d39526bfb86 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 18 Apr 2024 00:08:47 +0200 Subject: [PATCH 04/15] fixed precondition of XoverEvent --- router/dataplane.go | 1 + router/io-spec-abstract-transitions.gobra | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 4c650aea9..4ffc2d56a 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3296,6 +3296,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ p.d.getExternalMem() // @ if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) } if c, ok := p.d.external[egressID]; ok { + // @ TemporaryAssumeForIO(egressID != 0) if err := p.processEgress( /*@ ub, dp @*/ ); err != nil { // @ fold p.d.validResult(processResult{}, false) return processResult{}, err /*@, false, absReturnErr(dp, processResult{}) @*/ diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index 6b9d7cd36..fb9d60482 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -213,8 +213,8 @@ requires len(get(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID).LeftSeg).Hi requires AbsVerifyCurrentMACConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), dp) requires AbsValidateEgressIDConstraintXover(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), dp) requires egressID != none[io.IO_ifs] ==> AbsEgressInterfaceConstraint(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)), egressID) -requires (egressID == none[io.IO_ifs] ==> newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))) || - (egressID != none[io.IO_ifs] ==> newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)))) +requires egressID == none[io.IO_ifs] ==> newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)) +requires egressID != none[io.IO_ifs] ==> newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))) preserves acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>; ensures dp.Valid() ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt) From 8e6f0c6443907d5d695c54477b09e0a39f646df8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 18 Apr 2024 11:42:37 +0200 Subject: [PATCH 05/15] enable moreJoins impure (#321) --- .github/workflows/gobra.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml index 53d4c6210..137fa6572 100644 --- a/.github/workflows/gobra.yml +++ b/.github/workflows/gobra.yml @@ -417,6 +417,7 @@ jobs: checkConsistency: ${{ env.checkConsistency }} parallelizeBranches: '1' conditionalizePermissions: '0' + moreJoins: 'impure' imageVersion: ${{ env.imageVersion }} mceMode: 'on' requireTriggers: ${{ env.requireTriggers }} From 1b6397efdcc6c7b248a6d5079f28fd9352ea752b Mon Sep 17 00:00:00 2001 From: Dspil Date: Thu, 18 Apr 2024 14:25:14 +0200 Subject: [PATCH 06/15] invariant strengthening --- router/dataplane.go | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 4ffc2d56a..441624bbf 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -4129,8 +4129,7 @@ func decodeLayers(data []byte, base *slayers.SCION, // ghost clean-up: // @ ghost - // @ invariant 0 <= i0 && i0 <= len(opts) - // @ invariant -1 <= c && c <= i0 + // @ invariant -1 <= c && c < i0 // @ invariant len(processed) == len(opts) // @ invariant len(offsets) == len(opts) // @ invariant forall i int :: {&opts[i]} 0 <= i && i < len(opts) ==> acc(&opts[i], R10) From e31bcf869f6c01f48affffd2256f74e589ae6e25 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 18 Apr 2024 17:41:54 +0200 Subject: [PATCH 07/15] progress widen-lemma proof --- router/widen-lemma.gobra | 736 ++++++++------------------------------- 1 file changed, 149 insertions(+), 587 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 61580235e..0696e387c 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -21,6 +21,7 @@ import ( "verification/io" . "verification/utils/definitions" "verification/dependencies/encoding/binary" + "github.com/scionproto/scion/pkg/slayers" "github.com/scionproto/scion/pkg/slayers/path" "github.com/scionproto/scion/pkg/slayers/path/scion" ) @@ -38,19 +39,19 @@ ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R49) ensures absIO_val(dp, raw[:length], ingressID).isIO_val_Pkt2 ==> absIO_val(dp, raw[:length], ingressID) == absIO_val(dp, raw, ingressID) decreases -func absIO_valWidenLemma(dp io.DataPlaneSpec, raw []byte, ingressID uint16, length int) -/* { +func absIO_valWidenLemma(dp io.DataPlaneSpec, raw []byte, ingressID uint16, length int) { var ret1 io.IO_val var ret2 io.IO_val - if (validPktMetaHdr(raw[:length]) && absPkt(dp, raw[:length]) != none[io.IO_pkt2]) { - validPktMetaHdrWidenLemma(raw, length) - assert validPktMetaHdr(raw) + if (slayers.ValidPktMetaHdr(raw[:length]) && slayers.IsSupportedPkt(raw[:length])) { + ValidPktMetaHdrWidenLemma(raw, length) + assert slayers.ValidPktMetaHdr(raw) + IsSupportedPktWidenLemma(raw, length) + assert slayers.IsSupportedPkt(raw) absPktWidenLemma(dp, raw, length) - assert absPkt(dp, raw) != none[io.IO_pkt2] - ret1 = io.IO_val(io.IO_val_Pkt2{ifsToIO_ifs(ingressID), get(absPkt(dp, raw))}) - ret2 = io.IO_val(io.IO_val_Pkt2{ifsToIO_ifs(ingressID), get(absPkt(dp, raw[:length]))}) + ret1 = io.IO_val(io.IO_val_Pkt2{path.ifsToIO_ifs(ingressID), absPkt(dp, raw)}) + ret2 = io.IO_val(io.IO_val_Pkt2{path.ifsToIO_ifs(ingressID), absPkt(dp, raw[:length])}) assert ret1 == reveal absIO_val(dp, raw, ingressID) assert ret2 == reveal absIO_val(dp, raw[:length], ingressID) assert ret1 == ret2 @@ -65,17 +66,37 @@ ghost requires 0 <= length && length <= len(raw) requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -requires validPktMetaHdr(raw[:length]) +requires slayers.ValidPktMetaHdr(raw[:length]) ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures validPktMetaHdr(raw) +ensures slayers.ValidPktMetaHdr(raw) decreases -func validPktMetaHdrWidenLemma(raw []byte, length int) { +func ValidPktMetaHdrWidenLemma(raw []byte, length int) { unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) - reveal validPktMetaHdr(raw[:length]) - ret1 := reveal validPktMetaHdr(raw) - ret2 := reveal validPktMetaHdr(raw[:length]) + reveal slayers.ValidPktMetaHdr(raw[:length]) + ret1 := reveal slayers.ValidPktMetaHdr(raw) + ret2 := reveal slayers.ValidPktMetaHdr(raw[:length]) + assert ret1 == ret2 + fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) + fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) +} + +ghost +requires 0 <= length && length <= len(raw) +requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) +requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) +requires slayers.IsSupportedPkt(raw[:length]) +ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) +ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) +ensures slayers.IsSupportedPkt(raw) +decreases +func IsSupportedPktWidenLemma(raw []byte, length int) { + unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) + unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) + reveal slayers.IsSupportedPkt(raw[:length]) + ret1 := reveal slayers.IsSupportedPkt(raw) + ret2 := reveal slayers.IsSupportedPkt(raw[:length]) assert ret1 == ret2 fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) @@ -86,15 +107,16 @@ requires 0 <= length && length <= len(raw) requires dp.Valid() requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R50) requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R50) -requires validPktMetaHdr(raw) -requires validPktMetaHdr(raw[:length]) +requires slayers.ValidPktMetaHdr(raw) +requires slayers.ValidPktMetaHdr(raw[:length]) ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R50) ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R50) -ensures validPktMetaHdr(raw) -ensures validPktMetaHdr(raw[:length]) +ensures slayers.ValidPktMetaHdr(raw) +ensures slayers.ValidPktMetaHdr(raw[:length]) ensures absPkt(dp, raw) == absPkt(dp, raw[:length]) decreases -func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) { +func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) +/*{ // declarations var last1 io.IO_as @@ -114,8 +136,8 @@ func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) { var lm bool // abspkt step by step - _ := reveal validPktMetaHdr(raw) - _ := reveal validPktMetaHdr(raw[:length]) + _ := reveal slayers.ValidPktMetaHdr(raw) + _ := reveal slayers.ValidPktMetaHdr(raw[:length]) hdr1 := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[0:4]) hdr2 := unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][0:4]) assert unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][0:4]) == unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[:length][0:4]) @@ -260,568 +282,110 @@ func consDirWidenLemma(raw []byte, length int, currINFIdx int) { fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) } - -ghost -requires 0 <= length && length <= len(raw) -requires 1 <= numINF1 -requires 0 <= prevSegLen1 && prevSegLen1 <= currHFIdx1 -requires currHFIdx1 < segLen1 -requires hopFieldOffset(numINF1, segLen1) <= length -requires dp.Valid() -requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R52) -requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R52) -ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R52) -ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R52) -ensures asidForCurrSeg(dp, raw, numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) == - asidForCurrSeg(dp, raw[:length], numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) -decreases -func asidForCurrSegWidenLemma( - dp io.DataPlaneSpec, - raw []byte, - numINF1 int, - currHFIdx1 int, - segLen1 int, - prevSegLen1 int, - consDir1 bool, - asid1 io.IO_as, - length int) { - - var ret1 option[seq[io.IO_as]] - var ret2 option[seq[io.IO_as]] - var left1 option[seq[io.IO_as]] - var left2 option[seq[io.IO_as]] - var right1 option[seq[io.IO_as]] - var right2 option[seq[io.IO_as]] - - - if (segLen1 == 0) { - assert segLen1 == 0 - ret1 = some(seq[io.IO_as]{}) - ret2 = some(seq[io.IO_as]{}) - assert ret1 == asidForCurrSeg(dp, raw, numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret2 == asidForCurrSeg(dp, raw[:length], numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret1 == ret2 - } else { - asidsBeforeWidenLemma(dp, raw, numINF1, numINF1, currHFIdx1, currHFIdx1, prevSegLen1, prevSegLen1, consDir1, consDir1, asid1, asid1, length) - left1 = asidsBefore(dp, raw, numINF1, currHFIdx1, prevSegLen1, consDir1, asid1) - left2 = asidsBefore(dp, raw[:length], numINF1, currHFIdx1, prevSegLen1, consDir1, asid1) - assert left1 == left2 - newP := (R52 + R53)/2 - asidsAfterWidenLemma(dp, raw, numINF1, currHFIdx1, segLen1, consDir1, asid1, length, newP) - right1 = asidsAfter(dp, raw, numINF1, currHFIdx1, segLen1, consDir1, asid1) - right2 = asidsAfter(dp, raw[:length], numINF1, currHFIdx1, segLen1, consDir1, asid1) - assert right1 == right2 - if (left1 == none[seq[io.IO_as]] || right1 == none[seq[io.IO_as]]) { - assert (left2 == none[seq[io.IO_as]] || right2 == none[seq[io.IO_as]]) - ret1 = none[seq[io.IO_as]] - ret2 = none[seq[io.IO_as]] - assert ret1 == reveal asidForCurrSeg(dp, raw, numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret2 == reveal asidForCurrSeg(dp, raw[:length], numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret1 == ret2 - } else { - assert (left2 != none[seq[io.IO_as]] && right2 != none[seq[io.IO_as]]) - ret1 = some(get(left1) ++ get(right1)[1:]) - ret2 = some(get(left2) ++ get(right2)[1:]) - assert ret1 == reveal asidForCurrSeg(dp, raw, numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret2 == reveal asidForCurrSeg(dp, raw[:length], numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret1 == ret2 - } - } - assert ret1 == reveal asidForCurrSeg(dp, raw, numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret2 == reveal asidForCurrSeg(dp, raw[:length], numINF1, currHFIdx1, segLen1, prevSegLen1, consDir1, asid1) - assert ret1 == ret2 -} - -ghost -requires 1 <= numINF1 -requires 0 <= prevSegLen1 && prevSegLen1 <= currHFIdx1 -requires length <= len(raw) -requires hopFieldOffset(numINF1, currHFIdx1) + path.HopLen <= length -requires dp.Valid() -requires consDir1 == consDir2 -requires prevSegLen1 == prevSegLen2 -requires currHFIdx1 == currHFIdx2 -requires numINF1 == numINF2 -requires asid1 == asid2 -requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R53) -requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R53) -ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R53) -ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R53) -ensures forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> old(unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R53) in raw[i]) == (unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R53) in raw[i]) -ensures forall i int :: { &raw[:length][i] } 0 <= i && i < len(raw[:length]) ==> old(unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R53) in raw[:length][i]) == (unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R53) in raw[:length][i]) -ensures asidsBefore(dp, raw, numINF1, currHFIdx1, prevSegLen1, consDir1, asid1) == - asidsBefore(dp, raw[:length], numINF2, currHFIdx2, prevSegLen2, consDir2, asid2) -decreases currHFIdx1 - prevSegLen1 -func asidsBeforeWidenLemma( - dp io.DataPlaneSpec, - raw []byte, - numINF1 int, - numINF2 int, - currHFIdx1 int, - currHFIdx2 int, - prevSegLen1 int, - prevSegLen2 int, - consDir1 bool, - consDir2 bool, - asid1 io.IO_as, - asid2 io.IO_as, - length int) { - - var ret1 option[seq[io.IO_as]] - var ret2 option[seq[io.IO_as]] - var nextAsid1 option[io.IO_as] - var nextAsid2 option[io.IO_as] - var nextAsidSeq1 option[seq[io.IO_as]] - var nextAsidSeq2 option[seq[io.IO_as]] - - if (currHFIdx1 == prevSegLen1) { - assert currHFIdx2 == prevSegLen2 - ret1 = some(seq[io.IO_as]{asid1}) - ret2 = some(seq[io.IO_as]{asid2}) - assert ret1 == ret2 - } else { - assert currHFIdx2 != prevSegLen2 - nextAsid1 = asidFromIfs(dp, raw, numINF1, currHFIdx1, !consDir1, asid1) - nextAsid2 = asidFromIfs(dp, raw[:length], numINF2, currHFIdx2, !consDir2, asid2) - asidFromIfsWidenLemma(dp, raw, numINF1, numINF2, currHFIdx1, currHFIdx2, !consDir1, !consDir2, asid1, asid2, length) - assert nextAsid1 == nextAsid2 - if (nextAsid1 == none[io.IO_as]) { - assert nextAsid2 == none[io.IO_as] - ret1 = none[seq[io.IO_as]] - ret2 = none[seq[io.IO_as]] - assert ret1 == ret2 - assert ret1 == asidsBefore(dp, raw, numINF1, currHFIdx1, prevSegLen1, consDir1, asid1) - assert ret2 == asidsBefore(dp, raw[:length], numINF2, currHFIdx2, prevSegLen2, consDir2, asid2) - } else { - assert nextAsid2 != none[io.IO_as] - asidsBeforeWidenLemma(dp, raw, numINF1, numINF2, currHFIdx1-1, currHFIdx2-1, prevSegLen1, prevSegLen2, consDir1, consDir2, get(nextAsid1), get(nextAsid2), length) - nextAsidSeq1 = asidsBefore(dp, raw, numINF1, currHFIdx1-1, prevSegLen1, consDir1, get(nextAsid1)) - nextAsidSeq2 = asidsBefore(dp, raw[:length], numINF2, currHFIdx2-1, prevSegLen2, consDir2, get(nextAsid2)) - assert nextAsidSeq1 == nextAsidSeq2 - if (nextAsidSeq1 == none[seq[io.IO_as]]) { - assert nextAsidSeq2 == none[seq[io.IO_as]] - ret1 = none[seq[io.IO_as]] - ret2 = none[seq[io.IO_as]] - assert ret1 == ret2 - assert ret1 == asidsBefore(dp, raw, numINF1, currHFIdx1, prevSegLen1, consDir1, asid1) - assert ret2 == asidsBefore(dp, raw[:length], numINF2, currHFIdx2, prevSegLen2, consDir2, asid2) - } else { - ret1 = some(get(nextAsidSeq1) ++ seq[io.IO_as]{asid1}) - ret2 = some(get(nextAsidSeq2) ++ seq[io.IO_as]{asid2}) - assert ret1 == ret2 - assert ret1 == asidsBefore(dp, raw, numINF1, currHFIdx1, prevSegLen1, consDir1, asid1) - assert ret2 == asidsBefore(dp, raw[:length], numINF2, currHFIdx2, prevSegLen2, consDir2, asid2) - } - } - } -} - -ghost -requires 1 <= numINF1 -requires 0 <= currHFIdx1 -requires numINF1 == numINF2 -requires currHFIdx1 == currHFIdx2 -requires consDir1 == consDir2 -requires asid1 == asid2 -requires 0 <= length && length <= len(raw) -requires hopFieldOffset(numINF1, currHFIdx1) + path.HopLen <= length -requires dp.Valid() -requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R54) -requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R54) -ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R54) -ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R54) -ensures asidFromIfs(dp, raw, numINF1, currHFIdx1, consDir1, asid1) == - asidFromIfs(dp, raw[:length], numINF2, currHFIdx2, consDir2, asid2) -decreases -func asidFromIfsWidenLemma( - dp io.DataPlaneSpec, - raw []byte, - numINF1 int, - numINF2 int, - currHFIdx1 int, - currHFIdx2 int, - consDir1 bool, - consDir2 bool, - asid1 io.IO_as, - asid2 io.IO_as, - length int) { - var ret1 option[io.IO_as] - var ret2 option[io.IO_as] - - idx1 := hopFieldOffset(numINF1, currHFIdx1) - idx2 := hopFieldOffset(numINF2, currHFIdx1) - assert idx1 == idx2 - unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) - unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) - assert forall i int :: { &raw[idx1+2+i] } { &raw[idx1+2:idx1+4][i] } 0 <= i && i < 2 ==> - &raw[idx1+2+i] == &raw[idx1+2:idx1+4][i] - assert forall i int :: { &raw[:length][idx2+2+i] } { &raw[:length][idx2+2:idx2+4][i] } 0 <= i && i < 2 ==> - &raw[:length][idx2+2+i] == &raw[:length][idx2+2:idx2+4][i] - assert forall i int :: { &raw[idx1+4+i] } { &raw[idx1+4:idx1+6][i] } 0 <= i && i < 2 ==> - &raw[idx1+4+i] == &raw[idx1+4:idx1+6][i] - assert forall i int :: { &raw[:length][idx2+4+i] } { &raw[idx2+4:idx2+6][i] } 0 <= i && i < 2 ==> - &raw[:length][idx2+4+i] == &raw[:length][idx2+4:idx2+6][i] - ifs1 := consDir1 ? binary.BigEndian.Uint16(raw[idx1+4:idx1+6]) : binary.BigEndian.Uint16(raw[idx1+2:idx1+4]) - ifs2 := consDir2 ? binary.BigEndian.Uint16(raw[:length][idx2+4:idx2+6]) : binary.BigEndian.Uint16(raw[:length][idx2+2:idx2+4]) - assert ifs1 == ifs2 - asIfPair1 := io.AsIfsPair{asid1, io.IO_ifs(ifs1)} - asIfPair2 := io.AsIfsPair{asid2, io.IO_ifs(ifs2)} - assert asIfPair1 == asIfPair2 - if (asIfPair1 in domain(dp.GetLinks())) { - assert asIfPair2 in domain(dp.GetLinks()) - ret1 = some(dp.Lookup(asIfPair1).asid) - ret2 = some(dp.Lookup(asIfPair2).asid) - assert ret1 == ret2 - assert ret1 == asidFromIfs(dp, raw, numINF1, currHFIdx1, consDir1, asid1) - assert ret2 == asidFromIfs(dp, raw[:length], numINF2, currHFIdx2, consDir2, asid2) - } else { - assert !(asIfPair2 in domain(dp.GetLinks())) - ret1 = none[io.IO_as] - ret2 = none[io.IO_as] - assert ret1 == ret2 - assert ret1 == asidFromIfs(dp, raw, numINF1, currHFIdx1, consDir1, asid1) - assert ret2 == asidFromIfs(dp, raw[:length], numINF2, currHFIdx2, consDir2, asid2) - } - fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) - fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) - assert ret1 == ret2 - assert ret1 == asidFromIfs(dp, raw, numINF1, currHFIdx1, consDir1, asid1) - assert ret2 == asidFromIfs(dp, raw[:length], numINF2, currHFIdx2, consDir2, asid2) -} +*/ // --- The file has been simplified past this point ghost -requires R53 < p -requires 1 <= numINF -requires 0 <= currHFIdx && currHFIdx < segLen -requires length <= len(raw) -requires hopFieldOffset(numINF, segLen) <= length -requires dp.Valid() -preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), p) -preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), p) -ensures asidsAfter(dp, raw, numINF, currHFIdx, segLen, consDir, asid) == - asidsAfter(dp, raw[:length], numINF, currHFIdx, segLen, consDir, asid) -decreases segLen - currHFIdx + 1 -func asidsAfterWidenLemma(dp io.DataPlaneSpec, raw []byte, numINF int, currHFIdx int, segLen int, consDir bool, asid io.IO_as, length int, p perm) { - if currHFIdx != segLen - 1 { - nextAsid1 := asidFromIfs(dp, raw, numINF, currHFIdx, consDir, asid) - nextAsid2 := asidFromIfs(dp, raw[:length], numINF, currHFIdx, consDir, asid) - asidFromIfsWidenLemma(dp, raw, numINF, numINF, currHFIdx, currHFIdx, consDir, consDir, asid, asid, length) - assert nextAsid1 == nextAsid2 - if nextAsid1 == none[io.IO_as] { - ret := none[seq[io.IO_as]] - assert ret == asidsAfter(dp, raw, numINF, currHFIdx, segLen, consDir, asid) - assert ret == asidsAfter(dp, raw[:length], numINF, currHFIdx, segLen, consDir, asid) - } else { - newP := (p + R53)/2 - asidsAfterWidenLemma(dp, raw, numINF, currHFIdx+1, segLen, consDir, get(nextAsid1), length, newP) - nextAsidSeq1 := asidsAfter(dp, raw, numINF, currHFIdx+1, segLen, consDir, get(nextAsid1)) - nextAsidSeq2 := asidsAfter(dp, raw[:length], numINF, currHFIdx+1, segLen, consDir, get(nextAsid2)) - assert nextAsidSeq1 == nextAsidSeq2 - if nextAsidSeq1 == none[seq[io.IO_as]] { - ret := none[seq[io.IO_as]] - assert ret == asidsAfter(dp, raw, numINF, currHFIdx, segLen, consDir, asid) - assert ret == asidsAfter(dp, raw[:length], numINF, currHFIdx, segLen, consDir, asid) - } else { - ret := some(seq[io.IO_as]{asid} ++ get(nextAsidSeq1)) - assert ret == asidsAfter(dp, raw, numINF, currHFIdx, segLen, consDir, asid) - assert ret == asidsAfter(dp, raw[:length], numINF, currHFIdx, segLen, consDir, asid) - } - } - } -} - -ghost -requires dp.Valid() -requires 1 <= numINF -requires 0 < seg1Len -requires 0 <= seg2Len -requires 0 <= seg3Len -requires 0 <= length && length <= len(raw) -requires hopFieldOffset(numINF, seg1Len + seg2Len + seg3Len) <= length -requires currINFIdx <= numINF + 1 -requires 1 <= currINFIdx && currINFIdx < 4 -preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) -preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures asidsForLeftSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) == - asidsForLeftSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) -decreases -func asidsForLeftSegWidenLemma(dp io.DataPlaneSpec, raw []byte, numINF int, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, asid io.IO_as, length int) { - consDir1 := path.ConsDir(raw, currINFIdx) - consDir2 := path.ConsDir(raw[:length], currINFIdx) - consDirWidenLemma(raw, length, currINFIdx) - assert consDir1 == consDir2 - - if currINFIdx == 1 && seg2Len > 0 { - asidForCurrSegWidenLemma(dp, raw, numINF, seg1Len, seg1Len+seg2Len, seg1Len, consDir1, asid, length) - ret1 := asidForCurrSeg(dp, raw, numINF, seg1Len, seg1Len+seg2Len, seg1Len, consDir1, asid) - ret2 := asidForCurrSeg(dp, raw[:length], numINF, seg1Len, seg1Len+seg2Len, seg1Len, consDir2, asid) - assert ret1 == reveal asidsForLeftSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal asidsForLeftSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret1 == ret2 - } else if currINFIdx == 2 && seg2Len > 0 && seg3Len > 0 { - asidForCurrSegWidenLemma(dp, raw, numINF, seg1Len+seg2Len, seg1Len+seg2Len+seg3Len, seg1Len+seg2Len, consDir1, asid, length) - ret1 := asidForCurrSeg(dp, raw, numINF, seg1Len+seg2Len, seg1Len+seg2Len+seg3Len, seg1Len+seg2Len, consDir1, asid) - ret2 := asidForCurrSeg(dp, raw[:length], numINF, seg1Len+seg2Len, seg1Len+seg2Len+seg3Len, seg1Len+seg2Len, consDir2, asid) - assert ret1 == reveal asidsForLeftSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal asidsForLeftSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret1 == ret2 - } else { - ret := some(seq[io.IO_as]{}) - assert ret == reveal asidsForLeftSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret == reveal asidsForLeftSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - } -} - -ghost -requires dp.Valid() -requires 1 <= numINF -requires 0 < seg1Len -requires 0 <= seg2Len -requires 0 <= seg3Len -requires 0 <= length && length <= len(raw) -requires hopFieldOffset(numINF, seg1Len + seg2Len + seg3Len) <= length -requires currINFIdx <= numINF + 1 -requires -1 <= currINFIdx && currINFIdx < 2 -preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) -preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures asidsForRightSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) == - asidsForRightSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) -decreases -func asidsForRightSegWidenLemma(dp io.DataPlaneSpec, raw []byte, numINF int, currINFIdx int, seg1Len int, seg2Len int,seg3Len int, asid io.IO_as, length int) { - if currINFIdx == 1 && seg2Len > 0 { - consDir1 := path.ConsDir(raw, currINFIdx) - consDir2 := path.ConsDir(raw[:length], currINFIdx) - consDirWidenLemma(raw, length, currINFIdx) - assert consDir1 == consDir2 - asidForCurrSegWidenLemma(dp, raw, numINF, seg1Len+seg2Len-1, seg1Len+seg2Len, seg1Len, consDir1, asid, length) - ret1 := asidForCurrSeg(dp, raw, numINF, seg1Len+seg2Len-1, seg1Len+seg2Len, seg1Len, consDir1, asid) - ret2 := asidForCurrSeg(dp, raw[:length], numINF, seg1Len+seg2Len-1, seg1Len+seg2Len, seg1Len, consDir2, asid) - assert ret1 == reveal asidsForRightSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal asidsForRightSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret1 == ret2 - } else if currINFIdx == 0 { - consDir1 := path.ConsDir(raw, currINFIdx) - consDir2 := path.ConsDir(raw[:length], currINFIdx) - consDirWidenLemma(raw, length, currINFIdx) - assert consDir1 == consDir2 - asidForCurrSegWidenLemma(dp, raw, numINF, seg1Len-1, seg1Len, 0, consDir1, asid, length) - ret1 := asidForCurrSeg(dp, raw, numINF, seg1Len-1, seg1Len, 0, consDir1, asid) - ret2 := asidForCurrSeg(dp, raw[:length], numINF, seg1Len-1, seg1Len, 0, consDir2, asid) - assert ret1 == reveal asidsForRightSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal asidsForRightSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret1 == ret2 - } else { - ret := some(seq[io.IO_as]{}) - assert ret == reveal asidsForRightSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret == reveal asidsForRightSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - } -} - -ghost -requires dp.Valid() -requires 1 <= numINF -requires 0 < seg1Len -requires 0 <= seg2Len -requires 0 <= seg3Len -requires 0 <= length && length <= len(raw) -requires hopFieldOffset(numINF, seg1Len + seg2Len + seg3Len) <= length -requires currINFIdx <= numINF + 1 -requires 2 <= currINFIdx && currINFIdx < 5 -requires (currINFIdx == 4 && seg2Len > 0) ==> asid != none[io.IO_as] -requires (currINFIdx == 2 && seg2Len > 0 && seg3Len > 0) ==> asid != none[io.IO_as] -preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) -preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures asidsForMidSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) == - asidsForMidSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) -decreases -func asidsForMidSegWidenLemma(dp io.DataPlaneSpec, raw []byte, numINF int, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, asid option[io.IO_as], length int) { - if currINFIdx == 4 && seg2Len > 0 { - consDir1 := path.ConsDir(raw, 1) - consDir2 := path.ConsDir(raw[:length], 1) - consDirWidenLemma(raw, length, 1) - assert consDir1 == consDir2 - asidForCurrSegWidenLemma(dp, raw, numINF, seg1Len-1, seg1Len, 0, consDir1, get(asid), length) - ret1 := asidForCurrSeg(dp, raw, numINF, seg1Len-1, seg1Len, 0, consDir1, get(asid)) - ret2 := asidForCurrSeg(dp, raw[:length], numINF, seg1Len-1, seg1Len, 0, consDir2, get(asid)) - assert ret1 == reveal asidsForMidSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal asidsForMidSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret1 == ret2 - } else if currINFIdx == 2 && seg2Len > 0 && seg3Len > 0 { - consDir1 := path.ConsDir(raw, 2) - consDir2 := path.ConsDir(raw[:length], 2) - consDirWidenLemma(raw, length, 2) - assert consDir1 == consDir2 - asidForCurrSegWidenLemma(dp, raw, numINF, seg1Len+seg2Len, seg1Len+seg2Len+seg3Len, seg1Len+seg2Len, consDir1, get(asid), length) - ret1 := asidForCurrSeg(dp, raw, numINF, seg1Len + seg2Len, seg1Len + seg2Len + seg3Len, seg1Len + seg2Len, consDir1, get(asid)) - ret2 := asidForCurrSeg(dp, raw[:length], numINF, seg1Len + seg2Len, seg1Len + seg2Len + seg3Len, seg1Len + seg2Len, consDir2, get(asid)) - assert ret1 == reveal asidsForMidSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal asidsForMidSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret1 == ret2 - } else { - ret := some(seq[io.IO_as]{}) - assert ret == reveal asidsForMidSeg(dp, raw, numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret == reveal asidsForMidSeg(dp, raw[:length], numINF, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - } -} - -ghost -requires path.InfoFieldOffset(currINFIdx) + path.InfoLen <= offset -requires 0 < len(asid) -requires 0 <= length && length <= len(raw) -requires offset + path.HopLen * len(asid) <= length -requires 0 <= currHFIdx && currHFIdx <= len(asid) +requires 0 <= headerOffset +requires path.InfoFieldOffset(currINFIdx, headerOffset) + path.InfoLen <= offset +requires 0 < segLen +requires offset + path.HopLen * segLen <= length +requires length <= len(raw) +requires 0 <= currHFIdx && currHFIdx <= segLen requires 0 <= currINFIdx && currINFIdx < 3 preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures currSeg(raw, offset, currINFIdx, currHFIdx, asid) == - currSeg(raw[:length], offset, currINFIdx, currHFIdx, asid) +ensures scion.CurrSeg(raw, offset, currINFIdx, currHFIdx, segLen, headerOffset) == + scion.CurrSeg(raw[:length], offset, currINFIdx, currHFIdx, segLen, headerOffset) decreases -func currSegWidenLemma(raw []byte, offset int, currINFIdx int, currHFIdx int, asid seq[io.IO_as], length int) { +func currSegWidenLemma(raw []byte, offset int, currINFIdx int, currHFIdx int, segLen int, headerOffset int, length int) { unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R53) unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R53) - ainfo1 := path.Timestamp(raw, currINFIdx) - ainfo2 := path.Timestamp(raw[:length], currINFIdx) + ainfo1 := path.Timestamp(raw, currINFIdx, headerOffset) + ainfo2 := path.Timestamp(raw[:length], currINFIdx, headerOffset) assert ainfo1 == ainfo2 - consDir1 := path.ConsDir(raw, currINFIdx) - consDir2 := path.ConsDir(raw[:length], currINFIdx) + uinfo1 := path.AbsUinfo(raw, currINFIdx, headerOffset) + uinfo2 := path.AbsUinfo(raw[:length], currINFIdx, headerOffset) + assert uinfo1 == uinfo2 + + consDir1 := path.ConsDir(raw, currINFIdx, headerOffset) + consDir2 := path.ConsDir(raw[:length], currINFIdx, headerOffset) assert consDir1 == consDir2 - peer1 := path.Peer(raw, currINFIdx) - peer2 := path.Peer(raw[:length], currINFIdx) + peer1 := path.Peer(raw, currINFIdx, headerOffset) + peer2 := path.Peer(raw[:length], currINFIdx, headerOffset) assert peer1 == peer2 - segmentWidenLemma(raw, offset, currHFIdx, asid, ainfo1, consDir1, peer1, length) - ret1 := segment(raw, offset, currHFIdx, asid, ainfo1, consDir1, peer1) - ret2 := segment(raw[:length], offset, currHFIdx, asid, ainfo2, consDir2, peer2) - assert ret1 == reveal currSeg(raw, offset, currINFIdx, currHFIdx, asid) - assert ret2 == reveal currSeg(raw[:length], offset, currINFIdx, currHFIdx, asid) + segmentWidenLemma(raw, offset, currHFIdx, ainfo1, uinfo1, consDir1, peer1, segLen, length) + ret1 := scion.segment(raw, offset, currHFIdx, ainfo1, uinfo1, consDir1, peer1, segLen) + ret2 := scion.segment(raw[:length], offset, currHFIdx, ainfo2, uinfo2, consDir2, peer2, segLen) + assert ret1 == reveal scion.CurrSeg(raw, offset, currINFIdx, currHFIdx, segLen, headerOffset) + assert ret2 == reveal scion.CurrSeg(raw[:length], offset, currINFIdx, currHFIdx, segLen, headerOffset) assert ret1 == ret2 - fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R53) fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R53) } ghost requires 0 <= offset -requires 0 < len(asid) -requires 0 <= length && length <= len(raw) -requires offset + path.HopLen * len(asid) <= length -requires 0 <= currHFIdx && currHFIdx <= len(asid) +requires 0 < segLen +requires 0 <= currHFIdx && currHFIdx <= segLen +requires length <= len(raw) +requires offset + path.HopLen * segLen <= length requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R52) requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R52) ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R52) ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R52) -ensures segment(raw, offset, currHFIdx, asid, ainfo, consDir, peer) == segment(raw[:length], offset, currHFIdx, asid, ainfo, consDir, peer) +ensures scion.segment(raw, offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) == scion.segment(raw[:length], offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) decreases -func segmentWidenLemma(raw []byte, offset int, currHFIdx int, asid seq[io.IO_as], ainfo io.IO_ainfo, consDir bool, peer bool, length int) { +func segmentWidenLemma(raw []byte, offset int, currHFIdx int, ainfo io.IO_ainfo, uinfo set[io.IO_msgterm], consDir bool, peer bool, segLen int, length int) { newP := (R52 + R53)/2 assert R53 < newP && newP < R52 - hopFieldsConsDirWidenLemma(raw, offset, 0, set[io.IO_msgterm]{}, asid, ainfo, length, newP) - hopFieldsNotConsDirWidenLemma(raw, offset, len(asid)-1, set[io.IO_msgterm]{}, asid, ainfo, length, newP) - hopfields1 := consDir ? hopFieldsConsDir(raw, offset, 0, set[io.IO_msgterm]{}, asid, ainfo) : hopFieldsNotConsDir(raw, offset, len(asid) - 1, set[io.IO_msgterm]{}, asid, ainfo) - hopfields2 := consDir ? hopFieldsConsDir(raw[:length], offset, 0, set[io.IO_msgterm]{}, asid, ainfo) : hopFieldsNotConsDir(raw[:length], offset, len(asid) - 1, set[io.IO_msgterm]{}, asid, ainfo) + hopFieldsWidenLemma(raw, offset, 0, segLen, length, newP) + hopfields1 := scion.hopFields(raw, offset, 0, segLen) + hopfields2 := scion.hopFields(raw[:length], offset, 0, segLen) assert hopfields1 == hopfields2 - uinfo := uInfo(hopfields1, currHFIdx, consDir) - ret1 := io.IO_seg2(io.IO_seg3_{ AInfo :ainfo, UInfo : uinfo, ConsDir : consDir, Peer : peer, - Past : segPast(hopfields1, currHFIdx - 1), - Future : segFuture(hopfields1, currHFIdx), - History : segHistory(hopfields1, currHFIdx - 1), + Past : scion.segPast(hopfields1, currHFIdx - 1), + Future : scion.segFuture(hopfields1, currHFIdx), + History : scion.segHistory(hopfields1, currHFIdx - 1), }) ret2 := io.IO_seg2(io.IO_seg3_{ AInfo :ainfo, UInfo : uinfo, ConsDir : consDir, Peer : peer, - Past : segPast(hopfields2, currHFIdx - 1), - Future : segFuture(hopfields2, currHFIdx), - History : segHistory(hopfields2, currHFIdx - 1), + Past : scion.segPast(hopfields2, currHFIdx - 1), + Future : scion.segFuture(hopfields2, currHFIdx), + History : scion.segHistory(hopfields2, currHFIdx - 1), }) - assert ret1 == segment(raw, offset, currHFIdx, asid, ainfo, consDir, peer) - assert ret2 == segment(raw[:length], offset, currHFIdx, asid, ainfo, consDir, peer) + assert ret1 == scion.segment(raw, offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) + assert ret2 == scion.segment(raw[:length], offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) assert ret1 == ret2 } ghost -requires R53 < p -requires 0 <= offset -requires 0 <= currHFIdx && currHFIdx <= len(asid) -requires 0 <= length && length <= len(raw) -requires offset + path.HopLen * len(asid) <= length -preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), p) -preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), p) -ensures hopFieldsConsDir(raw, offset, currHFIdx, beta, asid, ainfo) == - hopFieldsConsDir(raw[:length], offset, currHFIdx, beta, asid, ainfo) -decreases len(asid) - currHFIdx -func hopFieldsConsDirWidenLemma(raw []byte, offset int, currHFIdx int, beta set[io.IO_msgterm], asid seq[io.IO_as], ainfo io.IO_ainfo, length int, p perm) { - if currHFIdx == len(asid) { - ret := seq[io.IO_HF]{} - assert ret == hopFieldsConsDir(raw, offset, currHFIdx, beta, asid, ainfo) - assert ret == hopFieldsConsDir(raw[:length], offset, currHFIdx, beta, asid, ainfo) - } else { - hopFieldWidenLemma(raw, offset + path.HopLen * currHFIdx, beta, asid[currHFIdx], ainfo, length) - hf1 := hopField(raw, offset + path.HopLen * currHFIdx, beta, asid[currHFIdx], ainfo) - hf2 := hopField(raw[:length], offset + path.HopLen * currHFIdx, beta, asid[currHFIdx], ainfo) - assert hf1 == hf2 - - newP := (p + R53)/2 - assert R53 < newP && newP < p - hopFieldsConsDirWidenLemma(raw, offset, currHFIdx + 1, (beta union set[io.IO_msgterm]{hf1.HVF}), asid, ainfo, length, newP) - ret1 := seq[io.IO_HF]{hf1} ++ hopFieldsConsDir(raw, offset, currHFIdx + 1, (beta union set[io.IO_msgterm]{hf1.HVF}), asid, ainfo) - ret2 := seq[io.IO_HF]{hf2} ++ hopFieldsConsDir(raw[:length], offset, currHFIdx + 1, (beta union set[io.IO_msgterm]{hf2.HVF}), asid, ainfo) - assert ret1 == hopFieldsConsDir(raw, offset, currHFIdx, beta, asid, ainfo) - assert ret2 == hopFieldsConsDir(raw[:length], offset, currHFIdx, beta, asid, ainfo) - assert ret1 == ret2 - } -} - -ghost -requires 0 <= length && length <= len(raw) -requires idx + path.HopLen <= length -requires 0 <= idx +requires 0 <= middle +requires middle + path.HopLen <= length +requires length <= len(raw) preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R54) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R54) -ensures hopField(raw, idx, beta, asid, ainfo) == hopField(raw[:length], idx, beta, asid, ainfo) +ensures path.BytesToIO_HF(raw, 0, middle, len(raw)) == path.BytesToIO_HF(raw[:length], 0, middle, length) decreases -func hopFieldWidenLemma(raw []byte, idx int, beta set[io.IO_msgterm], asid io.IO_as, ainfo io.IO_ainfo, length int) { +func BytesToIO_HFWidenLemma(raw []byte, middle int, length int) { unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) - - assert forall i int :: { &raw[idx+2+i] } { &raw[idx+2:idx+4][i] } 0 <= i && i < 2 ==> &raw[idx+2+i] == &raw[idx+2:idx+4][i] - assert forall i int :: { &raw[idx+4+i] } { &raw[idx+4:idx+6][i] } 0 <= i && i < 2 ==> &raw[idx+4+i] == &raw[idx+4:idx+6][i] - inif21 := binary.BigEndian.Uint16(raw[idx+2:idx+4]) - inif22 := binary.BigEndian.Uint16(raw[:length][idx+2:idx+4]) - assert inif21 == inif22 - - egif2 := binary.BigEndian.Uint16(raw[idx+4:idx+6]) - op_inif2 := inif21 == 0 ? none[io.IO_ifs] : some(io.IO_ifs(inif21)) - op_egif2 := egif2 == 0 ? none[io.IO_ifs] : some(io.IO_ifs(egif2)) - ts := io.IO_msgterm(io.MsgTerm_Num{ainfo}) - l := io.IO_msgterm(io.MsgTerm_L{seq[io.IO_msgterm]{ts, io.if2term(op_inif2), io.if2term(op_egif2), io.IO_msgterm(io.MsgTerm_FS{beta})}}) - hvf := io.mac(io.macKey(io.asidToKey(asid)), l) - - ret1 := io.IO_HF(io.IO_HF_{ - InIF2 : op_inif2, - EgIF2 : op_egif2, - HVF : hvf, - }) - ret2 := io.IO_HF(io.IO_HF_{ - InIF2 : op_inif2, - EgIF2 : op_egif2, - HVF : hvf, - }) - assert ret1 == hopField(raw, idx, beta, asid, ainfo) - assert ret2 == hopField(raw[:length], idx, beta, asid, ainfo) - assert ret1 == ret2 + assert path.BytesToIO_HF(raw, 0, middle, len(raw)).EgIF2 == path.BytesToIO_HF(raw[:length], 0, middle, length).EgIF2 + assert path.BytesToIO_HF(raw, 0, middle, len(raw)).InIF2 == path.BytesToIO_HF(raw[:length], 0, middle, length).InIF2 + assert path.BytesToIO_HF(raw, 0, middle, len(raw)).HVF == path.BytesToIO_HF(raw[:length], 0, middle, length).HVF fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) } @@ -829,110 +393,108 @@ func hopFieldWidenLemma(raw []byte, idx int, beta set[io.IO_msgterm], asid io.IO ghost requires R53 < p requires 0 <= offset -requires -1 <= currHFIdx && currHFIdx < len(asid) -requires 0 <= length && length <= len(raw) -requires offset + path.HopLen * currHFIdx + path.HopLen <= length +requires 0 <= currHFIdx && currHFIdx <= segLen +requires offset + path.HopLen * segLen <= length +requires length <= len(raw) preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), p) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), p) -ensures hopFieldsNotConsDir(raw, offset, currHFIdx, beta, asid, ainfo) == - hopFieldsNotConsDir(raw[:length], offset, currHFIdx, beta, asid, ainfo) -decreases currHFIdx + 1 -func hopFieldsNotConsDirWidenLemma(raw []byte, offset int, currHFIdx int, beta set[io.IO_msgterm], asid seq[io.IO_as], ainfo io.IO_ainfo, length int, p perm) { - if currHFIdx == -1 { +ensures scion.hopFields(raw, offset, currHFIdx, segLen) == + scion.hopFields(raw[:length], offset, currHFIdx, segLen) +decreases segLen - currHFIdx +func hopFieldsWidenLemma(raw []byte, offset int, currHFIdx int, segLen int, length int, p perm) { + if currHFIdx == segLen { ret := seq[io.IO_HF]{} - assert ret == hopFieldsNotConsDir(raw, offset, currHFIdx, beta, asid, ainfo) - assert ret == hopFieldsNotConsDir(raw[:length], offset, currHFIdx, beta, asid, ainfo) + assert ret == scion.hopFields(raw, offset, currHFIdx, segLen) + assert ret == scion.hopFields(raw[:length], offset, currHFIdx, segLen) } else { - hopFieldWidenLemma(raw, offset + path.HopLen * currHFIdx, beta, asid[currHFIdx], ainfo, length) - hf1 := hopField(raw, offset + path.HopLen * currHFIdx, beta, asid[currHFIdx], ainfo) - hf2 := hopField(raw[:length], offset + path.HopLen * currHFIdx, beta, asid[currHFIdx], ainfo) + BytesToIO_HFWidenLemma(raw, offset + path.HopLen * currHFIdx, length) + hf1 := path.BytesToIO_HF(raw, 0, offset + path.HopLen * currHFIdx, len(raw)) + hf2 := path.BytesToIO_HF(raw[:length], 0, offset + path.HopLen * currHFIdx, length) assert hf1 == hf2 newP := (p + R53)/2 assert R53 < newP && newP < p - hopFieldsNotConsDirWidenLemma(raw, offset, currHFIdx - 1, (beta union set[io.IO_msgterm]{hf1.HVF}), asid, ainfo, length, newP) - ret1 := hopFieldsNotConsDir(raw, offset, currHFIdx - 1, (beta union set[io.IO_msgterm]{hf1.HVF}), asid, ainfo) ++ seq[io.IO_HF]{hf1} - ret2 := hopFieldsNotConsDir(raw[:length], offset, currHFIdx - 1, (beta union set[io.IO_msgterm]{hf2.HVF}), asid, ainfo) ++ seq[io.IO_HF]{hf2} - assert ret1 == hopFieldsNotConsDir(raw, offset, currHFIdx, beta, asid, ainfo) - assert ret2 == hopFieldsNotConsDir(raw[:length], offset, currHFIdx, beta, asid, ainfo) + hopFieldsWidenLemma(raw, offset, currHFIdx - 1, segLen, length, newP) + ret1 := scion.hopFields(raw, offset, currHFIdx - 1, segLen) + ret2 := scion.hopFields(raw[:length], offset, currHFIdx - 1, segLen) + assert ret1 == scion.hopFields(raw, offset, currHFIdx, segLen) + assert ret2 == scion.hopFields(raw[:length], offset, currHFIdx, segLen) assert ret1 == ret2 } } ghost +requires 0 <= headerOffset requires 0 < seg1Len requires 0 <= seg2Len requires 0 <= seg3Len requires 0 <= length && length <= len(raw) -requires pktLen(seg1Len, seg2Len, seg3Len) <= length -requires 1 <= currINFIdx && currINFIdx < 4 -requires (currINFIdx == 1 && seg2Len > 0) ==> len(asid) == seg2Len -requires (currINFIdx == 2 && seg2Len > 0 && seg3Len > 0) ==> len(asid) == seg3Len +requires scion.pktLen(seg1Len, seg2Len, seg3Len, headerOffset) <= length +requires 1 <= currINFIdx && currINFIdx < 4 preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures leftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) == - leftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) +ensures scion.LeftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) == + scion.LeftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) decreases -func leftSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, asid seq[io.IO_as], length int) { - offset := hopFieldOffset(numInfoFields(seg1Len, seg2Len, seg3Len), 0) +func leftSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, headerOffset int, length int) { + offset := scion.HopFieldOffset(scion.NumInfoFields(seg1Len, seg2Len, seg3Len), 0, headerOffset) if currINFIdx == 1 && seg2Len > 0 { - currSegWidenLemma(raw, offset + path.HopLen * seg1Len, currINFIdx, 0, asid, length) - ret1 := some(currSeg(raw, offset + path.HopLen * seg1Len, currINFIdx, 0, asid)) - ret2 := some(currSeg(raw[:length], offset + path.HopLen * seg1Len, currINFIdx, 0, asid)) - assert ret1 == reveal leftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal leftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + currSegWidenLemma(raw, offset + path.HopLen * seg1Len, currINFIdx, 0, seg2Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset + path.HopLen * seg1Len, currINFIdx, 0, seg2Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset + path.HopLen * seg1Len, currINFIdx, 0, seg2Len, headerOffset)) + assert ret1 == reveal scion.LeftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret2 == reveal scion.LeftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 } else if currINFIdx == 2 && seg2Len > 0 && seg3Len > 0 { - currSegWidenLemma(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, asid, length) - ret1 := some(currSeg(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, asid)) - ret2 := some(currSeg(raw[:length], offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, asid)) - assert ret1 == reveal leftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal leftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + currSegWidenLemma(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, headerOffset)) + assert ret1 == reveal scion.LeftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret2 == reveal scion.LeftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 } else { ret := none[io.IO_seg3] - assert ret == reveal leftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret == reveal leftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + assert ret == reveal scion.LeftSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret == reveal scion.LeftSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) } } ghost +requires 0 <= headerOffset requires 0 < seg1Len requires 0 <= seg2Len requires 0 <= seg3Len requires 0 <= length && length <= len(raw) -requires pktLen(seg1Len, seg2Len, seg3Len) <= length +requires scion.pktLen(seg1Len, seg2Len, seg3Len, headerOffset) <= length requires -1 <= currINFIdx && currINFIdx < 2 -requires (currINFIdx == 1 && seg2Len > 0 && seg3Len > 0) ==> len(asid) == seg2Len -requires (currINFIdx == 0 && seg2Len > 0) ==> len(asid) == seg1Len preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures rightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) == - rightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) +ensures scion.RightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) == + scion.RightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) decreases -func rightSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, asid seq[io.IO_as], length int) { - offset := hopFieldOffset(numInfoFields(seg1Len, seg2Len, seg3Len), 0) +func rightSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, headerOffset int, length int) { + offset := scion.HopFieldOffset(scion.NumInfoFields(seg1Len, seg2Len, seg3Len), 0, headerOffset) if currINFIdx == 1 && seg2Len > 0 && seg3Len > 0 { - currSegWidenLemma(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len, asid, length) - ret1 := some(currSeg(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len, asid)) - ret2 := some(currSeg(raw[:length], offset + path.HopLen * seg1Len, currINFIdx, seg2Len, asid)) - assert ret1 == reveal rightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal rightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + currSegWidenLemma(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg3Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len,seg3Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg3Len, headerOffset)) + assert ret1 == reveal scion.RightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret2 == reveal scion.RightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 } else if currINFIdx == 0 && seg2Len > 0 { - currSegWidenLemma(raw, offset, currINFIdx, seg1Len, asid, length) - ret1 := some(currSeg(raw, offset, currINFIdx, seg1Len, asid)) - ret2 := some(currSeg(raw[:length], offset, currINFIdx, seg1Len, asid)) - assert ret1 == reveal rightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal rightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + currSegWidenLemma(raw, offset, currINFIdx, seg1Len, seg1Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset, currINFIdx, seg1Len, seg1Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset, currINFIdx, seg1Len, seg1Len, headerOffset)) + assert ret1 == reveal scion.RightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret2 == reveal scion.RightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 } else { ret := none[io.IO_seg3] - assert ret == reveal rightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret == reveal rightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + assert ret == reveal scion.RightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret == reveal scion.RightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) } } - +/* ghost requires 0 <= seg2Len requires 0 < seg1Len From 340397bf1d20673c63a6f80ddb9d998793e45fb5 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 18 Apr 2024 17:48:34 +0200 Subject: [PATCH 08/15] fix verification error --- router/widen-lemma.gobra | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 0696e387c..84e6b60de 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -475,9 +475,9 @@ decreases func rightSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, headerOffset int, length int) { offset := scion.HopFieldOffset(scion.NumInfoFields(seg1Len, seg2Len, seg3Len), 0, headerOffset) if currINFIdx == 1 && seg2Len > 0 && seg3Len > 0 { - currSegWidenLemma(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg3Len, headerOffset, length) - ret1 := some(scion.CurrSeg(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len,seg3Len, headerOffset)) - ret2 := some(scion.CurrSeg(raw[:length], offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg3Len, headerOffset)) + currSegWidenLemma(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg2Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg2Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset + path.HopLen * seg1Len, currINFIdx, seg2Len, seg2Len, headerOffset)) assert ret1 == reveal scion.RightSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret2 == reveal scion.RightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 From b797ea2df7386ee66962e9c9d36a0c7f9a3240a2 Mon Sep 17 00:00:00 2001 From: Dspil Date: Thu, 18 Apr 2024 19:38:58 +0200 Subject: [PATCH 09/15] proven? --- router/widen-lemma.gobra | 236 +++++++++++++-------------------------- 1 file changed, 79 insertions(+), 157 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 84e6b60de..dec4667b7 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -26,7 +26,7 @@ import ( "github.com/scionproto/scion/pkg/slayers/path/scion" ) -// Some thins in this file can be simplified. Nonetheless, the important definition here +// Some things in this file can be simplified. Nonetheless, the important definition here // is absIO_valWidenLemma. Everything else can be seen as an implementation detail. // TODO: prove Lemma ghost @@ -115,32 +115,18 @@ ensures slayers.ValidPktMetaHdr(raw) ensures slayers.ValidPktMetaHdr(raw[:length]) ensures absPkt(dp, raw) == absPkt(dp, raw[:length]) decreases -func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) -/*{ - - // declarations - var last1 io.IO_as - var last2 io.IO_as - var first1 io.IO_as - var first2 io.IO_as - var leftAsidSeq1 option[seq[io.IO_as]] - var leftAsidSeq2 option[seq[io.IO_as]] - var rightAsidSeq1 option[seq[io.IO_as]] - var rightAsidSeq2 option[seq[io.IO_as]] - var midAsidSeq1 option[seq[io.IO_as]] - var midAsidSeq2 option[seq[io.IO_as]] - var midAsid1 option[io.IO_as] - var midAsid2 option[io.IO_as] - var ret1 option[io.IO_pkt2] - var ret2 option[io.IO_pkt2] - var lm bool - - // abspkt step by step +func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) { + _ := reveal slayers.ValidPktMetaHdr(raw) _ := reveal slayers.ValidPktMetaHdr(raw[:length]) - hdr1 := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[0:4]) - hdr2 := unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][0:4]) - assert unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][0:4]) == unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[:length][0:4]) + headerOffset1 := slayers.GetAddressOffset(raw) + headerOffset2 := slayers.GetAddressOffset(raw[:length]) + + assert forall k int :: {&raw[headerOffset1:headerOffset1+scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> &raw[headerOffset1:headerOffset1+scion.MetaLen][k] == &raw[headerOffset1 + k] + assert forall k int :: {&raw[headerOffset2:headerOffset2+scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> &raw[headerOffset2:headerOffset2+scion.MetaLen][k] == &raw[headerOffset2 + k] + hdr1 := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[headerOffset1:headerOffset1+scion.MetaLen]) + hdr2 := unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][headerOffset2:headerOffset2+scion.MetaLen]) + assert unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][headerOffset2:headerOffset2+scion.MetaLen]) == unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[headerOffset1:headerOffset1+scion.MetaLen]) assert hdr1 == hdr2 metaHdr1 := scion.DecodedFrom(hdr1) @@ -167,124 +153,61 @@ func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) seg3Len2 := int(metaHdr2.SegLen[2]) assert seg3Len1 == seg3Len2 - segLen1 := lengthOfCurrSeg(currHFIdx1, seg1Len1, seg2Len1, seg3Len1) - segLen2 := lengthOfCurrSeg(currHFIdx2, seg1Len2, seg2Len2, seg3Len2) + segLen1 := scion.LengthOfCurrSeg(currHFIdx1, seg1Len1, seg2Len1, seg3Len1) + segLen2 := scion.LengthOfCurrSeg(currHFIdx2, seg1Len2, seg2Len2, seg3Len2) assert segLen1 == segLen2 - prevSegLen1 := lengthOfPrevSeg(currHFIdx1, seg1Len1, seg2Len1, seg3Len1) - prevSegLen2 := lengthOfPrevSeg(currHFIdx2, seg1Len2, seg2Len2, seg3Len2) + prevSegLen1 := scion.LengthOfPrevSeg(currHFIdx1, seg1Len1, seg2Len1, seg3Len1) + prevSegLen2 := scion.LengthOfPrevSeg(currHFIdx2, seg1Len2, seg2Len2, seg3Len2) assert prevSegLen1 == prevSegLen2 - numINF1 := numInfoFields(seg1Len1, seg2Len1, seg3Len1) - numINF2 := numInfoFields(seg1Len2, seg2Len2, seg3Len2) + numINF1 := scion.NumInfoFields(seg1Len1, seg2Len1, seg3Len1) + numINF2 := scion.NumInfoFields(seg1Len2, seg2Len2, seg3Len2) assert numINF1 == numINF2 - offset1 := hopFieldOffset(numINF1, 0) - offset2 := hopFieldOffset(numINF2, 0) + offset1 := scion.HopFieldOffset(numINF1, 0, headerOffset1) + offset2 := scion.HopFieldOffset(numINF2, 0, headerOffset2) assert offset1 == offset2 - consDir1 := path.ConsDir(raw, currINFIdx1) - consDir2 := path.ConsDir(raw[:length], currINFIdx2) - consDirWidenLemma(raw, length, currINFIdx1) - assert consDir1 == consDir2 - - asidForCurrSegWidenLemma(dp, raw, numINF1, currHFIdx1, prevSegLen1+segLen1, prevSegLen1, consDir1, dp.Asid(), length) - currAsidSeq2 := asidForCurrSeg(dp, raw, numINF1, currHFIdx1, prevSegLen1+segLen1, prevSegLen1, consDir1, dp.Asid()) - currAsidSeq1 := asidForCurrSeg(dp, raw[:length], numINF2, currHFIdx2, prevSegLen2+segLen2, prevSegLen2, consDir2, dp.Asid()) - assert currAsidSeq1 == currAsidSeq2 - - if (currAsidSeq1 == none[seq[io.IO_as]]) { - ret := none[io.IO_pkt2] - assert ret == reveal absPkt(dp, raw) - assert ret == reveal absPkt(dp, raw[:length]) - } else { - - last1 = get(currAsidSeq1)[segLen1-1] - last2 = get(currAsidSeq2)[segLen1-1] - assert last1 == last2 - - first1 = get(currAsidSeq1)[0] - first2 = get(currAsidSeq2)[0] - assert first1 == first2 - - asidsForLeftSegWidenLemma(dp, raw, numINF1, currINFIdx1+1, seg1Len1, seg2Len1, seg3Len1, last1, length) - leftAsidSeq1 = asidsForLeftSeg(dp, raw, numINF1, currINFIdx1 + 1, seg1Len1, seg2Len1, seg3Len1, last1) - leftAsidSeq2 = asidsForLeftSeg(dp, raw[:length], numINF2, currINFIdx2 + 1, seg1Len2, seg2Len2, seg3Len2, last2) - assert leftAsidSeq1 == leftAsidSeq2 - - asidsForRightSegWidenLemma(dp, raw, numINF1, currINFIdx1-1, seg1Len1, seg2Len1, seg3Len1, first1, length) - rightAsidSeq1 = asidsForRightSeg(dp, raw, numINF1, currINFIdx1 - 1, seg1Len1, seg2Len1, seg3Len1, first1) - rightAsidSeq2 = asidsForRightSeg(dp, raw[:length], numINF2, currINFIdx2 - 1, seg1Len2, seg2Len2, seg3Len2, first2) - assert rightAsidSeq1 == rightAsidSeq2 - - if (leftAsidSeq1 == none[seq[io.IO_as]] || rightAsidSeq1 == none[seq[io.IO_as]]) { - ret := none[io.IO_pkt2] - assert ret == reveal absPkt(dp, raw) - assert ret == reveal absPkt(dp, raw[:length]) - } else { - assert leftAsidSeq2 != none[seq[io.IO_as]] && rightAsidSeq2 != none[seq[io.IO_as]] - - midAsid1 = ((currINFIdx1 == 0 && seg2Len1 > 0 && seg3Len1 > 0) ? some(get(leftAsidSeq1)[len(get(leftAsidSeq1))-1]) : (currINFIdx1 == 2 && seg2Len1 > 0) ? some(get(rightAsidSeq1)[0]) : none[io.IO_as]) - midAsid2 = ((currINFIdx2 == 0 && seg2Len2 > 0 && seg3Len2 > 0) ? some(get(leftAsidSeq2)[len(get(leftAsidSeq2))-1]) : (currINFIdx2 == 2 && seg2Len2 > 0) ? some(get(rightAsidSeq2)[0]) : none[io.IO_as]) - assert midAsid1 == midAsid2 - - asidsForMidSegWidenLemma(dp, raw, numINF1, currINFIdx1+2, seg1Len1, seg2Len1, seg3Len1, midAsid1, length) - midAsidSeq1 = asidsForMidSeg(dp, raw, numINF1, currINFIdx1 + 2, seg1Len1, seg2Len1, seg3Len1, midAsid1) - midAsidSeq2 = asidsForMidSeg(dp, raw[:length], numINF2, currINFIdx2 + 2, seg1Len2, seg2Len2, seg3Len2, midAsid2) - assert midAsidSeq1 == midAsidSeq2 - if (midAsidSeq1 == none[seq[io.IO_as]]) { - ret := none[io.IO_pkt2] - assert ret == reveal absPkt(dp, raw) - assert ret == reveal absPkt(dp, raw[:length]) - } else { - currSegWidenLemma(raw, offset1+prevSegLen1, currINFIdx1, currHFIdx1-prevSegLen1, get(currAsidSeq1), length) - leftSegWidenLemma(raw, currINFIdx1 + 1, seg1Len1, seg2Len1, seg3Len1, get(leftAsidSeq1), length) - midSegWidenLemma(raw, currINFIdx1 + 2, seg1Len1, seg2Len1, seg3Len1, get(midAsidSeq1), length) - rightSegWidenLemma(raw, currINFIdx1 - 1, seg1Len1, seg2Len1, seg3Len1, get(rightAsidSeq1), length) - ret1 = some(io.IO_pkt2(io.IO_Packet2{ - CurrSeg : currSeg(raw, offset1+prevSegLen1, currINFIdx1, currHFIdx1-prevSegLen1, get(currAsidSeq1)), - LeftSeg : leftSeg(raw, currINFIdx1 + 1, seg1Len1, seg2Len1 , seg3Len1, get(leftAsidSeq1)), - MidSeg : midSeg(raw, currINFIdx1 + 2, seg1Len1, seg2Len1 , seg3Len1, get(midAsidSeq1)), - RightSeg : rightSeg(raw, currINFIdx1 - 1, seg1Len1, seg2Len1 , seg3Len1, get(rightAsidSeq1)), - })) - ret2 = some(io.IO_pkt2(io.IO_Packet2{ - CurrSeg : currSeg(raw[:length], offset2+prevSegLen2, currINFIdx2, currHFIdx2-prevSegLen2, get(currAsidSeq2)), - LeftSeg : leftSeg(raw[:length], currINFIdx2 + 1, seg1Len2, seg2Len2 , seg3Len2, get(leftAsidSeq2)), - MidSeg : midSeg(raw[:length], currINFIdx2 + 2, seg1Len2, seg2Len2 , seg3Len2, get(midAsidSeq2)), - RightSeg : rightSeg(raw[:length], currINFIdx2 - 1, seg1Len2, seg2Len2 , seg3Len2, get(rightAsidSeq2)), - })) - reveal absPkt(dp, raw) - reveal absPkt(dp, raw[:length]) - assert ret1 == absPkt(dp, raw) - assert ret2 == absPkt(dp, raw[:length]) - assert ret1 == ret2 - } - } - } -} - -ghost -requires 0 <= length && length <= len(raw) -requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) -requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) -requires 0 <= currINFIdx -requires path.InfoFieldOffset(currINFIdx) < length -ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) -ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) -ensures path.ConsDir(raw, currINFIdx) == path.ConsDir(raw[:length], currINFIdx) -decreases -func consDirWidenLemma(raw []byte, length int, currINFIdx int) { - unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) - unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) - assert &raw[path.InfoFieldOffset(currINFIdx)] == &raw[:length][path.InfoFieldOffset(currINFIdx)] - assert raw[path.InfoFieldOffset(currINFIdx)] == raw[:length][path.InfoFieldOffset(currINFIdx)] - assert (raw[path.InfoFieldOffset(currINFIdx)] & 0x1 == 0x1) == (raw[:length][path.InfoFieldOffset(currINFIdx)] & 0x1 == 0x1) - fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) - fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R56) + currSegWidenLemma(raw, offset1+prevSegLen1, currINFIdx1, currHFIdx1-prevSegLen1, segLen1, headerOffset1, length) + currSeg1 := scion.CurrSeg(raw, offset1+prevSegLen1, currINFIdx1, currHFIdx1-prevSegLen1, segLen1, headerOffset1) + currSeg2 := scion.CurrSeg(raw[:length], offset2+prevSegLen2, currINFIdx2, currHFIdx2-prevSegLen2, segLen2, headerOffset2) + assert currSeg1 == currSeg2 + + leftSegWidenLemma(raw, currINFIdx1 + 1, seg1Len1, seg2Len1 , seg3Len1, headerOffset1, length) + leftSeg1 := scion.LeftSeg(raw, currINFIdx1 + 1, seg1Len1, seg2Len1 , seg3Len1, headerOffset1) + leftSeg2 := scion.LeftSeg(raw[:length], currINFIdx2 + 1, seg1Len2, seg2Len2 , seg3Len2, headerOffset2) + assert leftSeg1 == leftSeg2 + + midSegWidenLemma(raw, currINFIdx1 + 2, seg1Len1, seg2Len1 , seg3Len1, headerOffset1, length) + midSeg1 := scion.MidSeg(raw, currINFIdx1 + 2, seg1Len1, seg2Len1 , seg3Len1, headerOffset1) + midSeg2 := scion.MidSeg(raw[:length], currINFIdx2 + 2, seg1Len2, seg2Len2 , seg3Len2, headerOffset2) + assert midSeg1 == midSeg2 + + rightSegWidenLemma(raw, currINFIdx1 - 1, seg1Len1, seg2Len1 , seg3Len1, headerOffset1, length) + rightSeg1 := scion.RightSeg(raw, currINFIdx1 - 1, seg1Len1, seg2Len1 , seg3Len1, headerOffset1) + rightSeg2 := scion.RightSeg(raw[:length], currINFIdx2 - 1, seg1Len2, seg2Len2 , seg3Len2, headerOffset2) + assert rightSeg1 == rightSeg2 + + ret1 := io.IO_pkt2(io.IO_Packet2{ + CurrSeg : currSeg1, + LeftSeg : leftSeg1, + MidSeg : midSeg1, + RightSeg : rightSeg1, + }) + ret2 := io.IO_pkt2(io.IO_Packet2{ + CurrSeg : currSeg2, + LeftSeg : leftSeg2, + MidSeg : midSeg2, + RightSeg : rightSeg2, + }) + + reveal absPkt(dp, raw) + reveal absPkt(dp, raw[:length]) + assert ret1 == absPkt(dp, raw) + assert ret2 == absPkt(dp, raw[:length]) + assert ret1 == ret2 } -*/ - -// --- The file has been simplified past this point ghost requires 0 <= headerOffset @@ -494,41 +417,40 @@ func rightSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, se assert ret == reveal scion.RightSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) } } -/* + + ghost -requires 0 <= seg2Len +requires 0 <= headerOffset requires 0 < seg1Len -requires 0 <= length && length <= len(raw) +requires 0 <= seg2Len requires 0 <= seg3Len requires 2 <= currINFIdx && currINFIdx < 5 -requires pktLen(seg1Len, seg2Len, seg3Len) <= length -requires (currINFIdx == 2 && seg2Len > 0 && seg3Len > 0) ==> len(asid) == seg3Len -requires (currINFIdx == 4 && seg2Len > 0) ==> len(asid) == seg1Len +requires 0 <= length && length <= len(raw) +requires scion.pktLen(seg1Len, seg2Len, seg3Len, headerOffset) <= length preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) -ensures midSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) == - midSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) +ensures scion.MidSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) == + scion.MidSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) decreases -func midSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, asid seq[io.IO_as], length int) { - offset := hopFieldOffset(numInfoFields(seg1Len, seg2Len, seg3Len), 0) +func midSegWidenLemma(raw []byte, currINFIdx int, seg1Len int, seg2Len int, seg3Len int, headerOffset int, length int) { + offset := scion.HopFieldOffset(scion.NumInfoFields(seg1Len, seg2Len, seg3Len), 0, headerOffset) if currINFIdx == 4 && seg2Len > 0 { - currSegWidenLemma(raw, offset, 0, seg1Len, asid, length) - ret1 := some(currSeg(raw, offset, 0, seg1Len, asid)) - ret2 := some(currSeg(raw[:length], offset, 0, seg1Len, asid)) - assert ret1 == reveal midSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal midSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + currSegWidenLemma(raw, offset, 0, seg1Len, seg1Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset, 0, seg1Len, seg1Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset, 0, seg1Len, seg1Len, headerOffset)) + assert ret1 == reveal scion.MidSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret2 == reveal scion.MidSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 } else if currINFIdx == 2 && seg2Len > 0 && seg3Len > 0 { - currSegWidenLemma(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, asid, length) - ret1 := some(currSeg(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, asid)) - ret2 := some(currSeg(raw[:length], offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, asid)) - assert ret1 == reveal midSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret2 == reveal midSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + currSegWidenLemma(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, headerOffset, length) + ret1 := some(scion.CurrSeg(raw, offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, headerOffset)) + ret2 := some(scion.CurrSeg(raw[:length], offset + path.HopLen * (seg1Len + seg2Len), currINFIdx, 0, seg3Len, headerOffset)) + assert ret1 == reveal scion.MidSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret2 == reveal scion.MidSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) assert ret1 == ret2 } else { ret := none[io.IO_seg3] - assert ret == reveal midSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, asid) - assert ret == reveal midSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, asid) + assert ret == reveal scion.MidSeg(raw, currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) + assert ret == reveal scion.MidSeg(raw[:length], currINFIdx, seg1Len, seg2Len, seg3Len, headerOffset) } } -*/ \ No newline at end of file From 9ef916f50873c188ffa4724d6d9951c0427d0b1d Mon Sep 17 00:00:00 2001 From: Dspil Date: Thu, 18 Apr 2024 20:16:52 +0200 Subject: [PATCH 10/15] fix --- router/widen-lemma.gobra | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index dec4667b7..3b88be0b1 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -337,9 +337,9 @@ func hopFieldsWidenLemma(raw []byte, offset int, currHFIdx int, segLen int, leng newP := (p + R53)/2 assert R53 < newP && newP < p - hopFieldsWidenLemma(raw, offset, currHFIdx - 1, segLen, length, newP) - ret1 := scion.hopFields(raw, offset, currHFIdx - 1, segLen) - ret2 := scion.hopFields(raw[:length], offset, currHFIdx - 1, segLen) + hopFieldsWidenLemma(raw, offset, currHFIdx + 1, segLen, length, newP) + ret1 := scion.hopFields(raw, offset, currHFIdx + 1, segLen) + ret2 := scion.hopFields(raw[:length], offset, currHFIdx + 1, segLen) assert ret1 == scion.hopFields(raw, offset, currHFIdx, segLen) assert ret2 == scion.hopFields(raw[:length], offset, currHFIdx, segLen) assert ret1 == ret2 From 2604a16cb0b6b1587939c8a5d2e36ebcc3168893 Mon Sep 17 00:00:00 2001 From: Dspil Date: Thu, 18 Apr 2024 20:39:14 +0200 Subject: [PATCH 11/15] bugfix --- router/widen-lemma.gobra | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 3b88be0b1..762f943d7 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -338,8 +338,8 @@ func hopFieldsWidenLemma(raw []byte, offset int, currHFIdx int, segLen int, leng newP := (p + R53)/2 assert R53 < newP && newP < p hopFieldsWidenLemma(raw, offset, currHFIdx + 1, segLen, length, newP) - ret1 := scion.hopFields(raw, offset, currHFIdx + 1, segLen) - ret2 := scion.hopFields(raw[:length], offset, currHFIdx + 1, segLen) + ret1 := seq[io.IO_HF]{hf1} ++ scion.hopFields(raw, offset, currHFIdx + 1, segLen) + ret2 := seq[io.IO_HF]{hf2} ++ scion.hopFields(raw[:length], offset, currHFIdx + 1, segLen) assert ret1 == scion.hopFields(raw, offset, currHFIdx, segLen) assert ret2 == scion.hopFields(raw[:length], offset, currHFIdx, segLen) assert ret1 == ret2 From 7dfe0964ddb2857a60ff0853f426e71f3d7d6a67 Mon Sep 17 00:00:00 2001 From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Date: Thu, 18 Apr 2024 20:43:05 +0200 Subject: [PATCH 12/15] Update router/widen-lemma.gobra MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- router/widen-lemma.gobra | 1 - 1 file changed, 1 deletion(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 762f943d7..12236fdeb 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -28,7 +28,6 @@ import ( // Some things in this file can be simplified. Nonetheless, the important definition here // is absIO_valWidenLemma. Everything else can be seen as an implementation detail. -// TODO: prove Lemma ghost requires 0 <= length && length <= len(raw) requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R49) From 9469646c3c42444e4ec93bf7379cf22a5213b994 Mon Sep 17 00:00:00 2001 From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Date: Thu, 18 Apr 2024 20:43:34 +0200 Subject: [PATCH 13/15] Update router/widen-lemma.gobra MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- router/widen-lemma.gobra | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 12236fdeb..babb8b2ff 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -116,8 +116,8 @@ ensures absPkt(dp, raw) == absPkt(dp, raw[:length]) decreases func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) { - _ := reveal slayers.ValidPktMetaHdr(raw) - _ := reveal slayers.ValidPktMetaHdr(raw[:length]) + reveal slayers.ValidPktMetaHdr(raw) + reveal slayers.ValidPktMetaHdr(raw[:length]) headerOffset1 := slayers.GetAddressOffset(raw) headerOffset2 := slayers.GetAddressOffset(raw[:length]) From c6721914d0139c29c76d64624177f353ba2fafa9 Mon Sep 17 00:00:00 2001 From: Dspil Date: Thu, 18 Apr 2024 20:52:18 +0200 Subject: [PATCH 14/15] joao --- router/dataplane.go | 2 +- router/widen-lemma.gobra | 20 +++++++++++++------- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index c1ea02dff..4b22afc2c 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3167,7 +3167,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost // @ newAbsPkt.isIO_val_Unsupported // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{}) // @ decreases 0 if sync.IgnoreBlockingForTermination() -// @ #backend[moreJoins(1)] +// @ #backend[stateConsolidationMode(6)] func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock *sync.Mutex, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { // @ ghost var oldPkt io.IO_pkt2 // @ ghost if(slayers.IsSupportedPkt(ub)) { diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index babb8b2ff..90acd49db 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -121,8 +121,10 @@ func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) { headerOffset1 := slayers.GetAddressOffset(raw) headerOffset2 := slayers.GetAddressOffset(raw[:length]) - assert forall k int :: {&raw[headerOffset1:headerOffset1+scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> &raw[headerOffset1:headerOffset1+scion.MetaLen][k] == &raw[headerOffset1 + k] - assert forall k int :: {&raw[headerOffset2:headerOffset2+scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==> &raw[headerOffset2:headerOffset2+scion.MetaLen][k] == &raw[headerOffset2 + k] + assert forall k int :: {&raw[k]} headerOffset1 <= k && k < headerOffset1 + scion.MetaLen ==> + &raw[headerOffset1:headerOffset1+scion.MetaLen][k-headerOffset1] == &raw[k] + assert forall k int :: {&raw[:length][k]} headerOffset2 <= k && k < headerOffset2 + scion.MetaLen ==> + &raw[headerOffset2:headerOffset2+scion.MetaLen][k-headerOffset2] == &raw[k] hdr1 := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[headerOffset1:headerOffset1+scion.MetaLen]) hdr2 := unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][headerOffset2:headerOffset2+scion.MetaLen]) assert unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][headerOffset2:headerOffset2+scion.MetaLen]) == unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[headerOffset1:headerOffset1+scion.MetaLen]) @@ -261,7 +263,8 @@ requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R52) requires acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R52) ensures acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R52) ensures acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R52) -ensures scion.segment(raw, offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) == scion.segment(raw[:length], offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) +ensures scion.segment(raw, offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) == + scion.segment(raw[:length], offset, currHFIdx, ainfo, uinfo, consDir, peer, segLen) decreases func segmentWidenLemma(raw []byte, offset int, currHFIdx int, ainfo io.IO_ainfo, uinfo set[io.IO_msgterm], consDir bool, peer bool, segLen int, length int) { newP := (R52 + R53)/2 @@ -300,14 +303,17 @@ requires middle + path.HopLen <= length requires length <= len(raw) preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R54) preserves acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R54) -ensures path.BytesToIO_HF(raw, 0, middle, len(raw)) == path.BytesToIO_HF(raw[:length], 0, middle, length) +ensures path.BytesToIO_HF(raw, 0, middle, len(raw)) == + path.BytesToIO_HF(raw[:length], 0, middle, length) decreases func BytesToIO_HFWidenLemma(raw []byte, middle int, length int) { unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) unfold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) - assert path.BytesToIO_HF(raw, 0, middle, len(raw)).EgIF2 == path.BytesToIO_HF(raw[:length], 0, middle, length).EgIF2 - assert path.BytesToIO_HF(raw, 0, middle, len(raw)).InIF2 == path.BytesToIO_HF(raw[:length], 0, middle, length).InIF2 - assert path.BytesToIO_HF(raw, 0, middle, len(raw)).HVF == path.BytesToIO_HF(raw[:length], 0, middle, length).HVF + hfBytes1 := path.BytesToIO_HF(raw, 0, middle, len(raw)) + hfBytes2 := path.BytesToIO_HF(raw[:length], 0, middle, length) + assert hfBytes1.EgIF2 == hfBytes2.EgIF2 + assert hfBytes1.InIF2 == hfBytes2.InIF2 + assert hfBytes1.HVF == hfBytes2.HVF fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R55) fold acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R55) } From 99654ec044b5e216d18e408ff091c89e7bbf7a84 Mon Sep 17 00:00:00 2001 From: Dspil Date: Thu, 18 Apr 2024 21:07:26 +0200 Subject: [PATCH 15/15] indent --- router/widen-lemma.gobra | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 90acd49db..05d87f978 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -122,9 +122,9 @@ func absPktWidenLemma(dp io.DataPlaneSpec, raw []byte, length int) { headerOffset2 := slayers.GetAddressOffset(raw[:length]) assert forall k int :: {&raw[k]} headerOffset1 <= k && k < headerOffset1 + scion.MetaLen ==> - &raw[headerOffset1:headerOffset1+scion.MetaLen][k-headerOffset1] == &raw[k] + &raw[headerOffset1:headerOffset1+scion.MetaLen][k-headerOffset1] == &raw[k] assert forall k int :: {&raw[:length][k]} headerOffset2 <= k && k < headerOffset2 + scion.MetaLen ==> - &raw[headerOffset2:headerOffset2+scion.MetaLen][k-headerOffset2] == &raw[k] + &raw[headerOffset2:headerOffset2+scion.MetaLen][k-headerOffset2] == &raw[k] hdr1 := unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[headerOffset1:headerOffset1+scion.MetaLen]) hdr2 := unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][headerOffset2:headerOffset2+scion.MetaLen]) assert unfolding acc(sl.AbsSlice_Bytes(raw[:length], 0, len(raw[:length])), R51) in binary.BigEndian.Uint32(raw[:length][headerOffset2:headerOffset2+scion.MetaLen]) == unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R51) in binary.BigEndian.Uint32(raw[headerOffset1:headerOffset1+scion.MetaLen])