Merge master into the visibility-rules branch

master added lemmas and assertions that use the ghost members this branch
renamed (absPkt, validPktMetaHdr, io.upd_uinfo, path.ifsToIO_ifs, ...). The
conflicting hunks in router/dataplane.go and router/io-spec-lemmas.gobra are
resolved in favour of master's content, with this branch's renames re-applied
to it; the same renames are applied to the newly added
pkg/slayers/path/scion/lemmas.gobra.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL

Author: claude

gobra-mod.json

@@ -1,6 +1,7 @@
 {
   "default_job_cfg": {
     "module": "github.com/scionproto/scion",
+    "assert_timeout": 45000,
     "includes": ["", "verification/dependencies"],
     "only_files_with_header": true,
     "assume_injectivity_inhale": true,

pkg/slayers/path/scion/lemmas.gobra

@@ -0,0 +1,88 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+// +gobra
+
+package scion
+
+import (
+	. "verification/utils/definitions"
+	sl "verification/utils/slices"
+	"verification/io"
+)
+
+// IsXoverLemma shows that the abstract xover guard of the packet encoded in
+// `ubuf` agrees with the concrete check performed by (*Raw).IsXover, i.e., that
+// (io.Pkt).IsXover is a faithful abstraction of (Base).IsXoverSpec.
+ghost
+preserves acc(s.Mem(ubuf), R55)
+preserves acc(sl.Bytes(ubuf, 0, len(ubuf)), R56)
+preserves ValidPktMetaHdr(ubuf)
+preserves s.GetBase(ubuf).EqAbsHeader(ubuf)
+ensures   s.AbsPkt(ubuf).IsXover() == s.GetBase(ubuf).IsXoverSpec()
+decreases
+func (s *Raw) IsXoverLemma(ubuf []byte) {
+	if s.GetBase(ubuf).IsXoverSpec() {
+		s.XoverLemma(ubuf)
+	} else {
+		// The packet is not at a segment switch. Either its current hop field is
+		// not the last one of the segment being traversed, in which case the
+		// future of the current segment contains more than one hop field, or
+		// there is no segment left to switch to, in which case LeftSeg is none.
+		reveal ValidPktMetaHdr(ubuf)
+		metaHdr := RawBytesToMetaHdr(ubuf)
+		currInfIdx := int(metaHdr.CurrINF)
+		currHfIdx := int(metaHdr.CurrHF)
+		seg1Len := int(metaHdr.SegLen[0])
+		seg2Len := int(metaHdr.SegLen[1])
+		seg3Len := int(metaHdr.SegLen[2])
+		segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
+		segLen := segs.LengthOfCurrSeg(currHfIdx)
+		prevSegLen := segs.LengthOfPrevSeg(currHfIdx)
+		numINF := segs.NumInfoFields()
+		offset := HopFieldOffset(numINF, prevSegLen, MetaLen)
+		pkt := reveal s.AbsPkt(ubuf)
+		assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx - prevSegLen, segLen, MetaLen)
+		assert pkt.LeftSeg == reveal LeftSeg(ubuf, currInfIdx + 1, segs, MetaLen)
+		assert len(pkt.CurrSeg.Future) == segLen - (currHfIdx - prevSegLen)
+		assert s.GetBase(ubuf) == RawBytesToBase(ubuf)
+		assert !pkt.IsXover()
+	}
+}
+
+// LastHopNotXoverLemma shows that a packet whose current hop field is the last
+// one of its path is never at a segment switch. This is what allows the router
+// to deliver packets destined to the local AS without switching segments.
+ghost
+preserves acc(s.Mem(ubuf), R55)
+preserves s.IsLastHopSpec(ubuf)
+preserves acc(sl.Bytes(ubuf, 0, len(ubuf)), R56)
+preserves ValidPktMetaHdr(ubuf)
+preserves s.GetBase(ubuf).EqAbsHeader(ubuf)
+ensures   !s.AbsPkt(ubuf).IsXover()
+decreases
+func (s *Raw) LastHopNotXoverLemma(ubuf []byte) {
+	reveal ValidPktMetaHdr(ubuf)
+	metaHdr := RawBytesToMetaHdr(ubuf)
+	currInfIdx := int(metaHdr.CurrINF)
+	currHfIdx := int(metaHdr.CurrHF)
+	seg1Len := int(metaHdr.SegLen[0])
+	seg2Len := int(metaHdr.SegLen[1])
+	seg3Len := int(metaHdr.SegLen[2])
+	segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
+	segLen := segs.LengthOfCurrSeg(currHfIdx)
+	prevSegLen := segs.LengthOfPrevSeg(currHfIdx)
+	numINF := segs.NumInfoFields()
+	offset := HopFieldOffset(numINF, prevSegLen, MetaLen)
+	pkt := reveal s.AbsPkt(ubuf)
+	assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx - prevSegLen, segLen, MetaLen)
+	// A segment that could be switched to only exists when the current segment
+	// is not the last one, which contradicts `currHfIdx == segs.TotalHops() - 1`.
+	assert pkt.LeftSeg == reveal LeftSeg(ubuf, currInfIdx + 1, segs, MetaLen)
+	assert s.GetBase(ubuf) == RawBytesToBase(ubuf)
+	assert currHfIdx == segs.TotalHops() - 1
+	assert pkt.LeftSeg == none[io.Seg]
+}

pkg/slayers/path/scion/raw_spec.gobra

@@ -451,6 +451,11 @@ func ValidPktMetaHdrSublice(raw []byte, idx int) {
 	unfold acc(sl.Bytes(raw[:idx], 0, idx), R56)
 	assert forall i int :: { &raw[:MetaLen][i] } 0 <= i && i < MetaLen ==>
 		&raw[:MetaLen][i] == &raw[:idx][:MetaLen][i]
+	// Sharing the locations is not enough: the two calls of RawBytesToMetaHdr
+	// read the meta header through different sl.Bytes predicates, so their
+	// snapshots must be related on those bytes as well.
+	assert forall i int :: { &raw[:MetaLen][i] } 0 <= i && i < MetaLen ==>
+		raw[:MetaLen][i] == raw[:idx][:MetaLen][i]
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	fold acc(sl.Bytes(raw[:idx], 0, idx), R56)
 }

pkg/slayers/scion_spec.gobra

@@ -441,10 +441,10 @@ ensures  acc(sl.Bytes(ub, 0, length), R55)
 ensures  s.ValidHeaderOffset(ub, len(ub))
 decreases
 func (s *SCION) ValidHeaderOffsetFromSubSliceLemma(ub []byte, length int) {
-	reveal s.ValidHeaderOffset(ub, len(ub))
+	reveal s.ValidHeaderOffset(ub, length)
 	unfold acc(sl.Bytes(ub, 0, len(ub)), R56)
 	unfold acc(sl.Bytes(ub, 0, length), R56)
-	assert reveal s.ValidHeaderOffset(ub, length)
+	assert reveal s.ValidHeaderOffset(ub, len(ub))
 	fold acc(sl.Bytes(ub, 0, len(ub)), R56)
 	fold acc(sl.Bytes(ub, 0, length), R56)
 }
@@ -551,7 +551,11 @@ pure func IsSupportedPkt(raw []byte) bool {
 	return CmnHdrLen <= len(raw) &&
 		let pathType := path.Type(GetPathType(raw))     in
 		let nextHdr  := L4ProtocolType(GetNextHdr(raw)) in
-		pathType == scion.PathType &&
+		// EPIC packets are forwarded by the same code that forwards SCION packets,
+		// operating on the SCION path that the EPIC metadata prefixes. Their
+		// abstraction is the abstraction of that underlying SCION path, so they
+		// are subject to the same IO-spec obligations.
+		(pathType == scion.PathType || pathType == epic.PathType) &&
 		nextHdr != L4SCMP
 }
 
@@ -562,7 +566,7 @@ pure func IsSupportedRawPkt(raw seq[byte]) bool {
 	return CmnHdrLen <= len(raw) &&
 		let pathType := path.Type(raw[8])     in
 		let nextHdr  := L4ProtocolType(raw[4]) in
-		pathType == scion.PathType &&
+		(pathType == scion.PathType || pathType == epic.PathType) &&
 		nextHdr != L4SCMP
 }
 
@@ -575,6 +579,12 @@ decreases
 func IsSupportedPktSubslice(raw []byte, idx int) {
 	unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	unfold acc(sl.Bytes(raw[:idx], 0, idx), R56)
+	// The two calls of IsSupportedPkt read the next header and the path type
+	// through different sl.Bytes predicates. Reading both locations through
+	// both slices while the predicates are unfolded is what makes their
+	// snapshots agree on them.
+	assert raw[:idx][4] == raw[4]
+	assert raw[:idx][8] == raw[8]
 	reveal IsSupportedPkt(raw)
 	reveal IsSupportedPkt(raw[:idx])
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
@@ -590,6 +600,9 @@ decreases
 func GetPathTypeSubslice(raw []byte, idx int) {
 	unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	unfold acc(sl.Bytes(raw[:idx], 0, idx), R56)
+	// Relates the two sl.Bytes snapshots on the byte holding the path type,
+	// which is the only one the two calls of GetPathType read.
+	assert raw[:idx][8] == raw[8]
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	fold acc(sl.Bytes(raw[:idx], 0, idx), R56)
 }