Disable conditionalizePermissions (#319)

* Update gobra.yml * Update gobra.yml * fix verification error * fixed precondition of XoverEvent * enable moreJoins impure (#321) * invariant strengthening * undo change to the state consolidator --------- Co-authored-by: mlimbeck <[email protected]> Co-authored-by: Dspil <[email protected]>
viperproject · Apr 18, 2024 · 598749b · 598749b
1 parent 8d708b6
commit 598749b
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 9 deletions.
diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml
@@ -416,9 +416,8 @@ 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: '1'
+ conditionalizePermissions: '0'
+ moreJoins: 'impure'
  imageVersion: ${{ env.imageVersion }}
  mceMode: 'on'
  requireTriggers: ${{ env.requireTriggers }}

diff --git 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
 }
@@ -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]
@@ -3293,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{}) @*/
@@ -4125,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)

diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra
@@ -212,7 +212,7 @@ 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] ==> 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)))
 preserves acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>;
@@ -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)