backup

viperproject · Jul 24, 2024 · 82b08bc · 82b08bc
1 parent d61970f
commit 82b08bc
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 16 deletions.
diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra
@@ -205,6 +205,7 @@ func ExternalEnterOrExitEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], ne
 	reveal AbsValidateEgressIDConstraint(nextPkt, (ingressID != none[io.IO_ifs]), dp)
 	reveal AbsProcessEgress(nextPkt)
 	if(ingressID == none[io.IO_ifs]){
+		// assert false
 		AtomicExit(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
 	} else {
 		AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)

diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra
@@ -60,8 +60,8 @@ ensures   len(res) != 0 ==> res === ub[start:end]
 decreases
 func (p Payload) Payload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
 	res = []byte(p)
-    assert unfolding acc(p.Mem(ub), R20) in true
-    return res, 0, len(p)
+	assert unfolding acc(p.Mem(ub), R20) in true
+	return res, 0, len(p)
 }
 
 requires b != nil && b.Mem()

diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
@@ -21,16 +21,16 @@ package io
 //     to the interface y of AS a2.
 type DataPlaneSpec adt {
 	DataPlaneSpec_{
-		linkTypes		dict[IO_ifs]IO_Link
-		neighborIAs		dict[IO_ifs]IO_as
-		localIA			IO_as
-		links			dict[AsIfsPair]AsIfsPair
+		linkTypes   dict[IO_ifs]IO_Link
+		neighborIAs dict[IO_ifs]IO_as
+		localIA     IO_as
+		links       dict[AsIfsPair]AsIfsPair
 	}
 }
 
 type AsIfsPair struct {
-	asid	IO_as
-	ifs		IO_ifs
+	asid IO_as
+	ifs  IO_ifs
 }
 
 ghost

diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -33,20 +33,43 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm {
 
 ghost
 decreases
-opaque
 pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool {
 	return let inif := hf.InIF2 in
 		let egif := hf.EgIF2 in
 		let x := hf.HVF in
-		let l := IO_msgterm(MsgTerm_L{
-			seq[IO_msgterm]{
-				IO_msgterm(MsgTerm_Num{ts}),
-				if2term(inif),
-				if2term(egif),
-				IO_msgterm(MsgTerm_FS{uinfo})}}) in
-		x == mac(macKey(asidToKey(dp.Asid())), l)
+		let next := dp.nextMsgtermSpec(inif, egif, ts, uinfo) in
+		x == next
+}
+
+ghost
+//opaque
+decreases
+pure func (dp DataPlaneSpec) nextMsgtermSpec(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm {
+	// return let l := MsgTerm_L {
+	// 	seq[IO_msgterm]{
+	// 		MsgTerm_Num{ts},
+	// 		if2term(inif),
+	// 		if2term(egif),
+	// 		MsgTerm_FS{uinfo}},
+	// } in mac(macKey(asidToKey(dp.Asid())), l)
+	return let l := plaintextToMac(inif, egif, ts, uinfo) in
+		mac(macKey(asidToKey(dp.Asid())), l)
+}
+
+ghost
+opaque
+decreases
+pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm {
+	return MsgTerm_L {
+		seq[IO_msgterm]{
+			MsgTerm_Num{ts},
+			if2term(inif),
+			if2term(egif),
+			MsgTerm_FS{uinfo}},
+	}
 }
 
+
 ghost
 decreases
 pure func macKey(key IO_key) IO_msgterm {