make hf_valid opaque

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)

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()

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

verification/io/other_defs.gobra

@@ -200,6 +200,7 @@ type IO_dp2_state adt {
 }
 
 ghost
+opaque
 decreases
 pure func (m IO_msgterm) extract_asid() IO_as {
 	return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_

verification/io/router.gobra

@@ -27,47 +27,72 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm {
 		case none[IO_ifs]:
 			MsgTerm_Empty{}
 		default:
-			IO_msgterm(MsgTerm_AS{IO_as(get(ifs))})
+			MsgTerm_AS{IO_as(get(ifs))}
 	}
 }
 
 ghost
 decreases
 pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool {
+	return hf_valid_impl(dp.Asid(), ts, uinfo, hf)
+}
+
+ghost
+decreases
+pure func hf_valid_impl(asid IO_as, 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 hvf := hf.HVF in
+		let next := nextMsgtermSpec(asid, inif, egif, ts, uinfo) in
+		hvf == next
+}
+
+ghost
+opaque
+ensures result.extract_asid() == asid
+decreases
+pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) (result IO_msgterm) {
+	return let l := plaintextToMac(inif, egif, ts, uinfo) in
+		let res := mac(macKey(asidToKey(asid)), l) in
+		let _ := reveal res.extract_asid() in
+		res
+}
+
+ghost
+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 {
-	return IO_msgterm(MsgTerm_Key{key})
+	return MsgTerm_Key{key}
 }
 
 ghost
 decreases
 pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm {
-	return IO_msgterm( MsgTerm_Hash {
-		MsgTerm_Hash_ : IO_msgterm( MsgTerm_MPair{
-			MsgTerm_MPair_1 : fst,
-			MsgTerm_MPair_2 : snd,
-		}),
-	})
+	return MsgTerm_Hash {
+		MsgTerm_Hash_: MsgTerm_MPair {
+			MsgTerm_MPair_1: fst,
+			MsgTerm_MPair_2: snd,
+		},
+	}
 }
 
 // helper function, not defined in IO spec
 ghost
 decreases
-pure func asidToKey(asid IO_as) IO_key{
-	return IO_key(Key_macK{asid})
+pure func asidToKey(asid IO_as) IO_key {
+	return Key_macK{asid}
 }
 
 ghost