IO specification of processPkt

pkg/slayers/path/scion/base.go

@@ -142,8 +142,8 @@ func (s *Base) IncPath() (e error) {
 // @ preserves acc(s.Mem(), definitions.ReadL19)
 // @ decreases
 func (s *Base) IsXover() bool {
-	//@ unfold acc(s.Mem(), definitions.ReadL19)
-	//@ defer fold acc(s.Mem(), definitions.ReadL19)
+	// @ unfold acc(s.Mem(), definitions.ReadL19)
+	// @ defer fold acc(s.Mem(), definitions.ReadL19)
 	return s.PathMeta.CurrHF+1 < uint8(s.NumHops) &&
 		s.PathMeta.CurrINF != s.infIndexForHF(s.PathMeta.CurrHF+1)
 }

pkg/slayers/path/scion/base_spec.gobra

@@ -63,4 +63,4 @@ decreases
 func (b *Base) DowngradePerm() {
 	unfold b.Mem()
 	fold b.NonInitMem()
-}
+}

pkg/slayers/path/scion/raw_spec.gobra

@@ -313,4 +313,4 @@ decreases
 func (s *Raw) RawBufferNonInitMem() []byte {
 	return unfolding acc(s.NonInitMem(), _) in s.Raw
 }
-/**** End of helpful pure functions ****/
+/**** End of helpful pure functions ****/

router/dataplane_spec.gobra

@@ -22,6 +22,7 @@ import (
 	sl "github.com/scionproto/scion/verification/utils/slices"
 	"github.com/scionproto/scion/pkg/scrypto"
 	"github.com/scionproto/scion/pkg/addr"
+	"github.com/scionproto/scion/verification/io"
 )
 
 // TODO: maybe change interpretation of Mutex depending on whether the
@@ -340,3 +341,30 @@ func closureSpec2(i uint16, c BatchConn)
 requires true
 func closureSpec3(c BatchConn)
 /** End of closure specs for the Run method **/
+
+/**** IO spec correlation ****/
+
+ghost
+ensures v.isIO_Internal_val1
+decreases
+pure func (p *scionPacketProcessor) IOvalue() (v io.IO_val) {
+	return IOvalue(p.rawPkt)
+}
+
+ghost
+ensures v.isIO_Internal_val1
+decreases
+pure func IOvalue(rawPkt []byte) (v io.IO_val)
+
+
+// For IO specification, there are two crossover actions:
+// 1. Core crossover where we switch from an up segment to a core segment or
+//    a core segment to a down segment
+// 2. Up2down crossover which happens when we switch immediately from an up segment
+//    to a down segment
+// The ghost variable is_up2down determines just that. If we have two segments in total
+// then the crossover must be an up2down one, otherwise a core crossover.
+// TODO: Define it. Maybe it needs not to be in base
+ghost
+decreases
+pure func (p *scionPacketProcessor) IsUp2Down() (res bool)

verification/io/io-spec.gobra

@@ -38,75 +38,191 @@ type Place int
 pred token(t Place)
 
 ghost
+decreases
 pure func undefined() IO_dp3s_state_local
 
-pred dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place)
-/*
-∀⋆ (λv. case v of
-Internal_val1 pkt recvif newpkt nextif ⇒
-if pkt ∈ ibuf s (Some recvif) ∧ (∃currseg traversedseg.
-(∃hf1 fut. dp2_enter_guard pkt currseg traversedseg asid hf1 recvif fut) ∧
-dp3s_forward (Packet2 traversedseg (LeftSeg pkt) (MidSeg pkt) (RightSeg pkt)) newpkt
-nextif)
-then ExT (λT'. ExV (λX. CBio (IN bio3s_enter) t (Internal_val1 pkt recvif newpkt nextif) X T'
-⋆ dp3s_iospec_ordered (dp3s_add_obuf s nextif newpkt) T')) else Bool True | _ ⇒ Bool True)
-*/
-
-pred dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t Place)
-/*
-∀⋆ (λv. case v of
-Internal_val1 pkt recvif newpkt nextif ⇒
-if ∃currseg. ¬ ConsDir currseg ∧ (∃nextseg. ConsDir nextseg ∧
-(∃traversedseg intermediatepkt hf1 hf2.
-xover_up2down2_link_type asid hf1 hf2 ∧
-(∃nextfut. dp3s_xover_common s pkt currseg nextseg traversedseg intermediatepkt hf1
-hf2 nextfut recvif newpkt nextif)))
-then ExT (λT'. ExV (λX. CBio (IN bio3s_xover_up2down) t (Internal_val1 pkt recvif newpkt
-nextif) X T'
-)
-⋆ dp3s_iospec_ordered (dp3s_add_obuf s nextif newpkt) T')) else Bool True
-| _ ⇒ Bool True)
-*/
-
-pred dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Place)
-/* s t ≡ ∀⋆ (λv. case v of
-Internal_val1 pkt recvif newpkt nextif ⇒
-if asid ∈ core ∧ (∃currseg nextseg.
-ConsDir nextseg = ConsDir currseg ∧ (∃traversedseg intermediatepkt hf1 hf2.
-xover_core2_link_type hf1 hf2 asid (ConsDir currseg) ∧
-(∃nextfut. dp3s_xover_common s pkt currseg nextseg traversedseg intermediatepkt hf1 hf2 nextfut recvif newpkt nextif)))
-then ExT (λT'. ExV (λX. CBio (IN bio3s_xover_core) t (Internal_val1 pkt recvif newpkt nextif) X
-T' * dp3s_iospec_ordered (dp3s_add_obuf s nextif newpkt) T')) else Bool True
-| _ ⇒ Bool True)
-*/
-
-pred dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place)
-/* s t ≡ ∀⋆ (λv. case v of
-Internal_val2 pkt newpkt nextif ⇒
-if pkt ∈ ibuf s None ∧ dp3s_forward_ext pkt newpkt nextif
-then ExT (λT'. ExV (λX. CBio (IN bio3s_exit) t (Internal_val2 pkt newpkt nextif) X T' ⋆ dp3s_iospec_ordered (dp3s_add_obuf s (Some nextif) newpkt) T'))
-else Bool True | _ ⇒ Bool True)
-*/
-
-pred CBioIO_bio3s_send(t Place)
+pred CBio_IN_bio3s_enter(t Place, v IO_val)
 
 ghost
-requires CBioIO_bio3s_send(t)
-pure func dp3s_iospec_bio3s_send_T(s IO_dp3s_state_local, t Place) Place
+requires CBio_IN_bio3s_enter(t, v)
+decreases
+pure func CBio_IN_bio3s_enter_T(s IO_dp3s_state_local, t Place, v IO_val) Place
 
+
+// This corresponds to the condition of the if statement in the io-spec case for enter
+ghost
+decreases
+pure func dp3s_iospec_bio3s_enter_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+	return some(v.IO_Internal_val1_2) in domain(s.ibuf) ==>
+		(let ibuf_set := s.ibuf[some(v.IO_Internal_val1_2)] in (v.IO_Internal_val1_1 in ibuf_set)) &&
+		(exists currseg IO_seg3, traversedseg IO_seg3 ::
+		(exists hf1 IO_HF, fut seq[IO_HF] ::
+			dp2_enter_guard(
+				v.IO_Internal_val1_1,
+				currseg,
+				traversedseg,
+				asid(),
+				hf1,
+				v.IO_Internal_val1_2,
+				fut) &&
+				dp3s_forward(
+					IO_pkt2(
+						IO_Packet2{
+							traversedseg,
+							v.IO_Internal_val1_1.LeftSeg,
+							v.IO_Internal_val1_1.MidSeg,
+							v.IO_Internal_val1_1.RightSeg}),
+					v.IO_Internal_val1_3,
+					v.IO_Internal_val1_4)))
+}
+
+pred dp3s_iospec_bio3s_enter(s IO_dp3s_state_local, t Place) {
+	forall v IO_val ::
+	(v.isIO_Internal_val1 ==>
+		(dp3s_iospec_bio3s_enter_guard(s, t, v) ==>
+			(CBio_IN_bio3s_enter(t, v) &&
+				dp3s_iospec_ordered(
+					dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3),
+					CBio_IN_bio3s_enter_T(s, t, v)))))
+}
+
+pred CBio_IN_bio3s_xover_up2down(t Place, v IO_val)
+
+ghost
+requires CBio_IN_bio3s_xover_up2down(t, v)
+pure func dp3s_iospec_bio3s_xover_up2down_T(s IO_dp3s_state_local, t Place, v IO_val) Place
+
+
+// This corresponds to the condition of the if statement in the io-spec case for xover_up2down
+ghost
+decreases
+pure func dp3s_iospec_bio3s_xover_up2down_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+	return (exists currseg IO_seg3 :: !currseg.ConsDir &&
+		(exists nextseg IO_seg3 :: nextseg.ConsDir &&
+			(exists traversedseg IO_seg3, intermediatepkt IO_pkt3, hf1 IO_HF, hf2 IO_HF ::
+			xover_up2down2_link_type(asid(), hf1, hf2) &&
+				(exists nextfut seq[IO_HF] ::
+				dp3s_xover_common(
+					s,
+					v.IO_Internal_val1_1,
+					currseg,
+					nextseg,
+					traversedseg,
+					intermediatepkt,
+					hf1,
+					hf2,
+					nextfut,
+					v.IO_Internal_val1_2,
+					v.IO_Internal_val1_3,
+					v.IO_Internal_val1_4,)))))
+}
+
+pred dp3s_iospec_bio3s_xover_up2down(s IO_dp3s_state_local, t Place) {
+	forall v IO_val ::
+	(v.isIO_Internal_val1 ==>
+		(dp3s_iospec_bio3s_xover_up2down_guard(s, t, v) ==>
+			(CBio_IN_bio3s_xover_up2down(t, v) &&
+				dp3s_iospec_ordered(
+					dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3),
+					dp3s_iospec_bio3s_xover_up2down_T(s, t, v)))))
+}
+
+pred CBio_IN_bio3s_xover_core(t Place, v IO_val)
+
+ghost
+requires CBio_IN_bio3s_xover_core(t, v)
+pure func dp3s_iospec_bio3s_xover_core_T(s IO_dp3s_state_local, t Place, v IO_val) Place
+
+// This corresponds to the condition of the if statement in the io-spec case for xover_core
+ghost
+decreases
+pure func dp3s_iospec_bio3s_xover_core_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+	return (asid() in core_as_set() &&
+		(exists currseg IO_seg3, nextseg IO_seg3 ::
+		currseg.ConsDir == nextseg.ConsDir &&
+			(exists traversedseg IO_seg3, intermediatepkt IO_pkt3, hf1 IO_HF, hf2 IO_HF ::
+			xover_core2_link_type(hf1, hf2, asid(), currseg.ConsDir) &&
+				(exists nextfut seq[IO_HF] ::
+				dp3s_xover_common(
+					s,
+					v.IO_Internal_val1_1,
+					currseg,
+					nextseg,
+					traversedseg,
+					intermediatepkt,
+					hf1,
+					hf2,
+					nextfut,
+					v.IO_Internal_val1_2,
+					v.IO_Internal_val1_3,
+					v.IO_Internal_val1_4)))))
+}
+
+pred dp3s_iospec_bio3s_xover_core(s IO_dp3s_state_local, t Place) {
+	forall v IO_val ::
+	(v.isIO_Internal_val1 ==>
+		(dp3s_iospec_bio3s_xover_core_guard(s, t, v) ==>
+			(CBio_IN_bio3s_xover_core(t, v) &&
+				dp3s_iospec_ordered(
+					dp3s_add_obuf(s, v.IO_Internal_val1_4, v.IO_Internal_val1_3),
+					dp3s_iospec_bio3s_xover_core_T(s, t, v)))))
+}
+
+
+pred CBio_IN_bio3s_exit(t Place, v IO_val)
+
+ghost
+requires CBio_IN_bio3s_exit(t, v)
+pure func dp3s_iospec_bio3s_exit_T(s IO_dp3s_state_local, t Place, v IO_val) Place
+
+// This corresponds to the condition of the if statement in the io-spec case for exit
+ghost
+decreases
+pure func dp3s_iospec_bio3s_exit_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+	return none[IO_ifs] in domain(s.ibuf) ==>
+		(let ibuf_set := s.ibuf[none[IO_ifs]] in (v.IO_Internal_val2_1 in ibuf_set))
+}
+
+pred dp3s_iospec_bio3s_exit(s IO_dp3s_state_local, t Place) {
+	forall v IO_val ::
+	(v.isIO_Internal_val2 ==>
+		(dp3s_iospec_bio3s_exit_guard(s, t, v) ==>
+				(CBio_IN_bio3s_exit(t, v) &&
+					dp3s_iospec_ordered(
+						dp3s_add_obuf(s, some(v.IO_Internal_val2_3), v.IO_Internal_val2_2),
+						dp3s_iospec_bio3s_exit_T(s, t, v)))))
+}
+
+
+pred CBioIO_bio3s_send(t Place, v IO_val)
+
+ghost
+requires CBioIO_bio3s_send(t, v)
+pure func dp3s_iospec_bio3s_send_T(s IO_dp3s_state_local, t Place, v IO_val) Place
+
+// This corresponds to the condition of the if statement in the io-spec case for send
 ghost
-requires CBioIO_bio3s_send(t)
-pure func dp3s_iospec_bio3s_send_R(s IO_dp3s_state_local, t Place) IO_val
+decreases
+pure func dp3s_iospec_bio3s_send_guard(s IO_dp3s_state_local, t Place, v IO_val) bool {
+	return v.IO_val_Pkt2_1 in domain(s.obuf) ==>
+		(let obuf_set := s.obuf[v.IO_val_Pkt2_1] in (v.IO_val_Pkt2_2 in obuf_set))
+}
 
 // TODO: annotate WriteBatch, skipped for now
-pred dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place)
-/* ≡ ∀⋆ (λv. case v of
-Pkt2 recvif pkt ⇒
-if pkt ∈ obuf s recvif
-then ExT (λT'. ExV (λX. CBio (IO bio3s_send) t (Pkt2 recvif pkt) X T'
-⋆ dp3s_iospec_ordered s T')) else Bool True | Unsupported recvif pkt ⇒
-ExT (λT'. ExV (λX. CBio (IO bio3s_send) t (Unsupported recvif pkt) X T' ⋆ dp3s_iospec_ordered s T')) | _ ⇒ Bool True)
-*/
+pred dp3s_iospec_bio3s_send(s IO_dp3s_state_local, t Place) {
+	forall v IO_val ::
+	(v.isIO_val_Pkt2 ==> 
+		(dp3s_iospec_bio3s_send_guard(s, t, v) ==>
+			CBioIO_bio3s_send(t, v) &&
+				dp3s_iospec_ordered(
+					s,
+					dp3s_iospec_bio3s_send_T(s, t, v)))) &&
+		(v.isIO_val_Unsupported ==>
+			CBioIO_bio3s_send(t, v) &&
+				dp3s_iospec_ordered(
+					s,
+					dp3s_iospec_bio3s_send_T(s, t, v)))
+}
 
 pred CBioIO_bio3s_recv(t Place)
 
@@ -158,4 +274,5 @@ pred dp3s_iospec_skip(s IO_dp3s_state_local, t Place) {
 
 pred dp3s_iospec_stop(s IO_dp3s_state_local, t Place) {
 	true
-}
+}
+

verification/io/router.gobra

@@ -20,6 +20,10 @@ package io
 
 // TODO: make individual_router an interface type with the following methods
 
+ghost
+decreases
+pure func core_as_set() set[IO_as]
+
 ghost
 decreases
 pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool
@@ -105,4 +109,4 @@ pure func dp3s_xover_common(
 			(let lookupRes := s.ibuf[some(recvif)] in (m in lookupRes)) &&
 			dp2_xover_common_guard(m, currseg, nextseg, traversedseg, intermediatepkt, hf1, hf2, nextfut, asid(), recvif) &&
 			dp3s_forward(intermediatepkt, newpkt, nextif)
-}
+}