Verify the IO behavior (a.k.a., basis PR) (#248)

* manually trigger workflow * manually trigger workflow * raw byte to spec for segments and hopfields * bugfix * import fix * bugfix after gobra update * spec to pkt (currSeg) * spec to pkt (left, mid, right) * spec to pkt (termination) * code clean up * clean up * improvements * instantiate abstract functions with bodies * progress io spec * formatting * specification fixes * IO-spec to pkt rewritten * clean up * improve readability * rename of function lengthOfCurrSeg * extract asid-seqence from raw pkt * missing trigger * quick fix * Update router/dataplane_spec.gobra Co-authored-by: Dionysios Spiliopoulos <[email protected]> * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * readability improvements * further improvements * replace 4 by its constant InfoLen * readability improvement * constant for metaLen in package path * Update router/io-spec.gobra Co-authored-by: João Pereira <[email protected]> * minor improvements * move validMetaLenInPath() to test file * io-spec in Run * add body to absIO_val * fix merge mistake * fix merge mistake * fix typo * io-spec skeleton for processPkt and processSCION * import fix * Update router/io-spec.gobra * unit * well formdness * relate dataplane with dataplaneSpec * various fixes * Update verification/io/values.gobra * permission fix for dpSpecWellConfigured * permission fix in rc * fix verification error * dp.Valid() as opaque * backup * format spacing * improve perf; drop assumption * fix formatting * Update router/dataplane.go * formatting postconditions of processPkt, processSCION * fix extra permission * typo * processSCION had the same issue * ingressID is preseved intead of sInit * Revert "ingressID is preseved intead of sInit" This reverts commit 88db3fd. * Revert "processSCION had the same issue" This reverts commit 71aadfe. * Updated IO-Spec-Function to Correlate Bytes with Terms (#262) * fixes in the asid extraction functions * pre-/postconditions for process * fix formatting * fix same issue in processSCION * fix var names * precondition changes in hopfield and asidFromIfs * prostcondition fix in process and processSCION * update imports links * Apply suggestions from code review --------- Co-authored-by: Dspil <[email protected]> Co-authored-by: João Pereira <[email protected]> * made absIO_val opaque * use artificial triggers for quantifiers inside IO resources (#280) * AbsPkt improvements (#270) * absPkt opaque and other improvements * quick fixes * changed permission from R55 to R56 * added missing permission amount in ReadBatch * fixed pre/postconditions of processPkt, processSCION and process * fixed opaque format --------- Co-authored-by: João Pereira <[email protected]> * Verify send guard in Run (#263) * remove send operation * lemma for smaller buffer result in same abstract pkt * progress send guard * progress send guard * Fix incompleteness and continue with send guard (#273) * backup * backup * backup * backup * backup * drop space * pick better triggers * add necessary lemma and call to it; contains an assume false that needs to be dropped * backup * backup * add missing loop invariant about ingressID * backup * backup * fix verification error * try out a simpler trigger * widen lemma for absIO_val (#268) * widen lemma for abspkt (non termianting) * abspkt proven * renamed io-spec-lemmas * io val also proven * cleanup * merged markus' abspkt improvements * consdir lemma * proved * reinstate lemma4 * fix verification error * Simplify widen lemma from #268 (#282) * start simplifying * continue simplifying * continue simplifying stuff * continue simplifying * continue simplifying * simplify further * finish for now * Update router/io-spec.gobra --------- Co-authored-by: João Pereira <[email protected]> * Continue send (#283) * widen lemma for abspkt (non termianting) * abspkt proven * renamed io-spec-lemmas * io val also proven * cleanup * merged markus' abspkt improvements * consdir lemma * proved * reinstate lemma4 * fix verification error * Simplify widen lemma from #268 (#282) * start simplifying * continue simplifying * continue simplifying stuff * continue simplifying * continue simplifying * simplify further * finish for now * Update router/io-spec.gobra * finish send in Run * propagate changes to processSCION --------- Co-authored-by: Dspil <[email protected]> * backup * adapt to the new syntax of backend annotations * clean-up * changes according to feedback --------- Co-authored-by: João Pereira <[email protected]> Co-authored-by: Dionysios Spiliopoulos <[email protected]> Co-authored-by: Dspil <[email protected]> * IO specification skeleton in process (#284) * absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * progress in handleRouterAlerts methods * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * fix verification errors in processEgress and DoXover addressing feedback clean up --------- Co-authored-by: João Pereira <[email protected]> * Add functional spec to `InfoField.SerializeTo` (#300) * absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * backup * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * backup * backup * simplify Decoded.Reverse * progress in handleRouterAlerts methods * clean-up * add section header * drop comment * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * backup * backup * fix verification errors in processEgress and DoXover addressing feedback clean up * backup * drop one assume * readability improvements * backup * backup * simplify proof * adapt lemmas * verify spec for SerializeTo of infofield * Missing Postcondition in Process (#301) * absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * Revert "Update gobra.yml to disableNL (#289)" This reverts commit 1e60830. * progress in handleRouterAlerts methods * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * fix verification errors in processEgress and DoXover addressing feedback clean up * fix verification error * changed postcondition in process * fix verification error * fix verification error * Update gobra.yml * added postcondition to packSCMP --------- Co-authored-by: João Pereira <[email protected]> * Drop unnecessary function `hopFieldsNotConsDir` (#303) * reverse hopFieldsNotConsDir once * remove hopfieldsNotConsDir * hopFieldsConsDir => hopFields --------- Co-authored-by: João Pereira <[email protected]> * Update IO-spec to drop the `xover_core` event (#302) * progress updating the IO-spec * finish updating new IO-spec * Fix precondition of `processSCION` (#307) * start fixing pres of processSCION * backup * backup * Drop unnecessary assertions * tiny fmt * streamline msgterm assumptions (#308) * improve verification time of processPkt * IO-spec update for link check logic (#310) * io-spec update * proof of link logic * fix verification errors * drop assumption in validateSrcDstIA() * fix verification error * Update pkg/slayers/path/scion/raw.go * Pre/Post conditions of processPkt (#312) * progress with pre and post conditions for io-spec in processPkt * fix verification error * changes in process * additional temporary assumptions in process() * cleanup --------- Co-authored-by: João Pereira <[email protected]> * fmt --------- Co-authored-by: MLETHZ <[email protected]> Co-authored-by: Markus Limbeck <[email protected]> Co-authored-by: João Pereira <[email protected]>
viperproject · Apr 12, 2024 · 45d3639 · 45d3639
1 parent a8ff113
commit 45d3639
Show file tree

Hide file tree

Showing 20 changed files with 3,503 additions and 882 deletions.
diff --git a/pkg/slayers/path/hopfield_spec.gobra b/pkg/slayers/path/hopfield_spec.gobra
@@ -16,32 +16,51 @@
 
 package path
 
-ghost const MetaLen = 4
+import (
+	"verification/io"
+	"verification/utils/slices"
+	"verification/dependencies/encoding/binary"
+	. "verification/utils/definitions"
+)
 
 pred (h *HopField) Mem() {
 	acc(h) && h.ConsIngress >= 0 && h.ConsEgress >= 0
 }
 
-ghost 
+
+ghost
 decreases
-pure func InfoFieldOffset(currINF int) int {
-	return MetaLen + InfoLen * currINF
+pure func ifsToIO_ifs(ifs uint16) option[io.IO_ifs]{
+	return ifs == 0 ? none[io.IO_ifs] : some(io.IO_ifs(ifs))
 }
 
-ghost 
-requires 0 <= currINF
-requires InfoFieldOffset(currINF) < len(raw)
-requires acc(&raw[InfoFieldOffset(currINF)], _)
+ghost
+requires 0 <= start && start <= middle
+requires middle + HopLen <= end && end <= len(raw)
+requires acc(slices.AbsSlice_Bytes(raw, start, end), _)
 decreases
-pure func ConsDir(raw []byte, currINF int) bool {
-	return raw[InfoFieldOffset(currINF)] & 0x1 == 0x1
+pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) {
+	return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle + 2 + k]) in
+		let _ := Asserting(forall k int :: {&raw[middle+4:middle+6][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+6][k] == &raw[middle + 4 + k]) in
+		let _ := Asserting(forall k int :: {&raw[middle+6:middle+6+MacLen][k]} 0 <= k && k < MacLen ==> &raw[middle+6:middle+6+MacLen][k] == &raw[middle + 6 + k]) in
+		unfolding acc(slices.AbsSlice_Bytes(raw, start, end), _) in
+		let inif2 := binary.BigEndian.Uint16(raw[middle+2:middle+4]) in
+		let egif2 := binary.BigEndian.Uint16(raw[middle+4:middle+6]) in
+		let op_inif2 := ifsToIO_ifs(inif2) in
+		let op_egif2 := ifsToIO_ifs(egif2) in
+		io.IO_HF(io.IO_HF_{
+			InIF2 : op_inif2,
+			EgIF2 : op_egif2,
+			HVF : AbsMac(FromSliceToMacArray(raw[middle+6:middle+6+MacLen])),
+		})
 }
 
-ghost 
-requires 0 <= currINF
-requires InfoFieldOffset(currINF) < len(raw)
-requires acc(&raw[InfoFieldOffset(currINF)], _)
+ghost
 decreases
-pure func Peer(raw []byte, currINF int) bool {
-	return raw[InfoFieldOffset(currINF)] & 0x2 == 0x2
+pure func (h HopField) ToIO_HF() (io.IO_HF) {
+	return io.IO_HF(io.IO_HF_{
+			InIF2 : ifsToIO_ifs(h.ConsIngress),
+			EgIF2 : ifsToIO_ifs(h.ConsEgress),
+			HVF : AbsMac(h.Mac),
+		})
 }
diff --git a/pkg/slayers/path/infofield.go b/pkg/slayers/path/infofield.go
@@ -22,8 +22,10 @@ import (
 
 	"github.com/scionproto/scion/pkg/private/serrors"
 	"github.com/scionproto/scion/pkg/private/util"
+	//@ bits "github.com/scionproto/scion/verification/utils/bitwise"
 	//@ . "github.com/scionproto/scion/verification/utils/definitions"
 	//@ "github.com/scionproto/scion/verification/utils/slices"
+	//@ "verification/io"
 )
 
 // InfoLen is the size of an InfoField in bytes.
@@ -85,38 +87,59 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
 // @ preserves acc(inf, R10)
 // @ preserves slices.AbsSlice_Bytes(b, 0, InfoLen)
 // @ ensures   err == nil
+// @ ensures   inf.ToIntermediateAbsInfoField() ==
+// @ 	BytesToIntermediateAbsInfoField(b, 0, 0, InfoLen)
 // @ decreases
 func (inf *InfoField) SerializeTo(b []byte) (err error) {
 	if len(b) < InfoLen {
 		return serrors.New("buffer for InfoField too short", "expected", InfoLen,
 			"actual", len(b))
 	}
+	//@ ghost targetAbsInfo := inf.ToIntermediateAbsInfoField()
 	//@ unfold slices.AbsSlice_Bytes(b, 0, InfoLen)
 	b[0] = 0
 	if inf.ConsDir {
 		b[0] |= 0x1
 	}
+	//@ ghost tmpInfo1 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+	//@ bits.InfoFieldFirstByteSerializationLemmas()
+	//@ assert tmpInfo1.ConsDir == targetAbsInfo.ConsDir
+	//@ ghost firstByte := b[0]
 	if inf.Peer {
 		b[0] |= 0x2
 	}
+	//@ tmpInfo2 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+	//@ assert tmpInfo2.Peer == (b[0] & 0x2 == 0x2)
+	//@ assert tmpInfo2.ConsDir == (b[0] & 0x1 == 0x1)
+	//@ assert tmpInfo2.Peer == targetAbsInfo.Peer
+	//@ assert tmpInfo2.ConsDir == tmpInfo1.ConsDir
+	//@ assert tmpInfo2.ConsDir == targetAbsInfo.ConsDir
 	b[1] = 0 // reserved
 	//@ assert &b[2:4][0] == &b[2] && &b[2:4][1] == &b[3]
 	binary.BigEndian.PutUint16(b[2:4], inf.SegID)
+	//@ ghost tmpInfo3 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+	//@ assert tmpInfo3.UInfo == targetAbsInfo.UInfo
 	//@ assert &b[4:8][0] == &b[4] && &b[4:8][1] == &b[5]
 	//@ assert &b[4:8][2] == &b[6] && &b[4:8][3] == &b[7]
 	binary.BigEndian.PutUint32(b[4:8], inf.Timestamp)
+	//@ ghost tmpInfo4 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+	//@ assert tmpInfo4.AInfo == targetAbsInfo.AInfo
 	//@ fold slices.AbsSlice_Bytes(b, 0, InfoLen)
 	return nil
 }
 
 // UpdateSegID updates the SegID field by XORing the SegID field with the 2
 // first bytes of the MAC. It is the beta calculation according to
 // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation
+// @ requires hf.HVF == AbsMac(hfMac)
 // @ preserves acc(&inf.SegID)
+// @ ensures AbsUInfoFromUint16(inf.SegID) ==
+// @ 	old(io.upd_uinfo(AbsUInfoFromUint16(inf.SegID), hf))
 // @ decreases
-func (inf *InfoField) UpdateSegID(hfMac [MacLen]byte) {
+func (inf *InfoField) UpdateSegID(hfMac [MacLen]byte /* @, ghost hf io.IO_HF @ */) {
 	//@ share hfMac
 	inf.SegID = inf.SegID ^ binary.BigEndian.Uint16(hfMac[:2])
+	// @ AssumeForIO(AbsUInfoFromUint16(inf.SegID) == old(io.upd_uinfo(AbsUInfoFromUint16(inf.SegID), hf)))
 }
 
 // @ decreases

diff --git a/pkg/slayers/path/infofield_spec.gobra b/pkg/slayers/path/infofield_spec.gobra
@@ -0,0 +1,127 @@
+// Copyright 2022 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package path
+
+import (
+	"verification/io"
+	sl "verification/utils/slices"
+	"verification/dependencies/encoding/binary"
+	. "verification/utils/definitions"
+)
+
+ghost const MetaLen = 4
+
+ghost
+decreases
+pure func InfoFieldOffset(currINF, headerOffset int) int {
+	return headerOffset + MetaLen + InfoLen * currINF
+}
+
+ghost
+requires 0 <= currINF && 0 <= headerOffset
+requires InfoFieldOffset(currINF, headerOffset) < len(raw)
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56)
+decreases
+pure func ConsDir(raw []byte, currINF int, headerOffset int) bool {
+	return unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in
+		raw[InfoFieldOffset(currINF, headerOffset)] & 0x1 == 0x1
+}
+
+ghost
+requires 0 <= currINF && 0 <= headerOffset
+requires InfoFieldOffset(currINF, headerOffset) < len(raw)
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56)
+decreases
+pure func Peer(raw []byte, currINF int, headerOffset int) bool {
+	return unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in
+		raw[InfoFieldOffset(currINF, headerOffset)] & 0x2 == 0x2
+}
+
+ghost
+requires 0 <= currINF && 0 <= headerOffset
+requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56)
+decreases
+pure func Timestamp(raw []byte, currINF int, headerOffset int) io.IO_ainfo {
+	return let idx := InfoFieldOffset(currINF, headerOffset) + 4 in
+		unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in
+		let _ := Asserting(forall i int :: { &raw[idx+i] } { &raw[idx:idx+4][i] } 0 <= i && i < 4 ==>
+			&raw[idx+i] == &raw[idx:idx+4][i]) in
+		io.IO_ainfo(binary.BigEndian.Uint32(raw[idx : idx + 4]))
+}
+
+ghost
+requires 0 <= currINF && 0 <= headerOffset
+requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56)
+decreases
+pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm] {
+	return 	let idx := InfoFieldOffset(currINF, headerOffset) + 2 in
+		unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in
+		let _ := Asserting(forall k int :: {&raw[idx:idx+2][k]} 0 <= k && k < 2 ==>
+			&raw[idx:idx+4][k] == &raw[idx + k]) in
+		AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2]))
+}
+
+// This type simplifies the infoField, making it easier
+// to use than the IO_seg3 from the IO-spec.
+type IntermediateAbsInfoField adt {
+	IntermediateAbsInfoField_ {
+		AInfo io.IO_ainfo
+		UInfo set[io.IO_msgterm]
+		ConsDir bool
+		Peer bool
+	}
+}
+
+ghost
+requires 0 <= start && start <= middle
+requires middle+InfoLen <= end && end <= len(raw)
+requires acc(sl.AbsSlice_Bytes(raw, start, end), _)
+decreases
+pure func BytesToIntermediateAbsInfoField(raw [] byte, start int, middle int, end int) (IntermediateAbsInfoField) {
+	return unfolding acc(sl.AbsSlice_Bytes(raw, start, end), _) in
+		BytesToIntermediateAbsInfoFieldHelper(raw, middle, end)
+}
+
+ghost
+requires 0 <= middle
+requires middle+InfoLen <= end && end <= len(raw)
+requires forall i int :: { &raw[i] } middle <= i && i < end ==>
+	acc(&raw[i], _)
+decreases
+pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int) (IntermediateAbsInfoField) {
+	return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
+		let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
+		IntermediateAbsInfoField(IntermediateAbsInfoField_{
+			AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
+			UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
+			ConsDir : raw[middle] & 0x1 == 0x1,
+			Peer : raw[middle] & 0x2  == 0x2,
+		})
+}
+
+ghost
+decreases
+pure func (inf InfoField) ToIntermediateAbsInfoField() (IntermediateAbsInfoField) {
+	return IntermediateAbsInfoField(IntermediateAbsInfoField_{
+		AInfo : io.IO_ainfo(inf.Timestamp),
+		UInfo : AbsUInfoFromUint16(inf.SegID),
+		ConsDir : inf.ConsDir,
+		Peer : inf.Peer,
+	})
+}
diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra
@@ -0,0 +1,46 @@
+// Copyright 2020 Anapaya Systems
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package path
+
+import "verification/io"
+
+// At the moment, we assume that all cryptographic operations performed at the code level
+// imply the desired properties at the IO spec level because we cannot currently prove in
+// Gobra the correctness of these operations. Given that we do not prove any properties
+// about this function, we currently do not provide a definition for it.
+
+ghost
+decreases
+pure func AbsUInfoFromUint16(SegID uint16) set[io.IO_msgterm]
+
+ghost
+decreases
+pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm)
+
+// The following function converts a slice with at least `MacLen` elements into
+// an (exclusive) array containing the mac. Note that there are no permissions
+// involved for accessing exclusive arrays. This functions is abstract for now
+// because Gobra does not allow for array literals in pure functions, even though
+// they are no more side-effectful than creating an instance of a struct type.
+// This will soon be fixed in Gobra.
+ghost
+requires MacLen <= len(mac)
+requires forall i int :: { &mac[i] } 0 <= i && i < MacLen ==> acc(&mac[i], _)
+ensures  len(res) == MacLen
+ensures  forall i int :: { res[i] } 0 <= i && i < MacLen ==> mac[i] == res[i]
+decreases
+pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte)
diff --git a/pkg/slayers/path/scion/base.go b/pkg/slayers/path/scion/base.go
@@ -259,18 +259,7 @@ type MetaHdr struct {
 // @ preserves acc(m)
 // @ preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R50)
 // @ ensures   (len(raw) >= MetaLen) == (e == nil)
-// @ ensures   e == nil ==> (
-// @ 	MetaLen <= len(raw)              &&
-// @ 	0 <= m.CurrINF && m.CurrINF <= 3 &&
-// @ 	0 <= m.CurrHF  && m.CurrHF < 64  &&
-// @ 	m.SegsInBounds() &&
-// @ 	let lenR := len(raw) in
-// @ 	let b0 := sl.GetByte(raw, 0, lenR, 0) in
-// @ 	let b1 := sl.GetByte(raw, 0, lenR, 1) in
-// @ 	let b2 := sl.GetByte(raw, 0, lenR, 2) in
-// @ 	let b3 := sl.GetByte(raw, 0, lenR, 3) in
-// @ 	let line := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in
-// @ 	DecodedFrom(line) == *m)
+// @ ensures   e == nil ==> m.DecodeFromBytesSpec(raw)
 // @ ensures   e != nil ==> e.ErrorMem()
 // @ decreases
 func (m *MetaHdr) DecodeFromBytes(raw []byte) (e error) {
@@ -300,16 +289,11 @@ func (m *MetaHdr) DecodeFromBytes(raw []byte) (e error) {
 // @ preserves acc(m, R50)
 // @ preserves sl.AbsSlice_Bytes(b, 0, len(b))
 // @ ensures   e == nil
-// @ ensures   let lenR := len(b)           in
-// @ 	let b0 := sl.GetByte(b, 0, lenR, 0) in
-// @ 	let b1 := sl.GetByte(b, 0, lenR, 1) in
-// @ 	let b2 := sl.GetByte(b, 0, lenR, 2) in
-// @ 	let b3 := sl.GetByte(b, 0, lenR, 3) in
-// @ 	let v  := m.SerializedToLine()      in
-// @ 	binary.BigEndian.PutUint32Spec(b0, b1, b2, b3, v)
+// @ ensures   m.SerializeToSpec(b)
 // @ decreases
 func (m *MetaHdr) SerializeTo(b []byte) (e error) {
 	if len(b) < MetaLen {
+		// @ Unreachable()
 		return serrors.New("buffer for MetaHdr too short", "expected", MetaLen, "actual", len(b))
 	}
 	line := uint32(m.CurrINF)<<30 | uint32(m.CurrHF&0x3F)<<24