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

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),
+		})
 }

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

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,
+	})
+}

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)

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