Adding DataPlaneSpec to the IO-spec (#230)

* making IO-spec dependend on abstract dataplane * renaming Abs_Dataplane to DataPlaneSpec * removing local state from IO-spec next place functions * rewriting IO-spec with match clause * comment out unnecessary functions * cosmetic changes * documentation for DataPlaneSpec and Valid function * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * cosmetic changes * fix comment * cosmetic changes * guards require correct type --------- Co-authored-by: João Pereira <[email protected]>
viperproject · Oct 18, 2023 · 10676f7 · 10676f7
1 parent 5d9c8d8
commit 10676f7
Show file tree

Hide file tree

Showing 7 changed files with 301 additions and 321 deletions.
diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
@@ -0,0 +1,72 @@
+// 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 io
+
+type DataPlaneSpec adt {
+	DataPlaneSpec_{
+		linkTypes		dict[IO_ifs]IO_Link
+		neighborIAs		dict[IO_ifs]IO_as
+		localIA			IO_as
+		topology 		TopologySpec
+	}
+}
+
+// TopologySpec provides information about the entire network topology. 
+// coreAS: IDs of the core Autonomous Systems
+// links: representation of the network topology as a graph.
+//		links[a1][1] == a2 means that AS a1 has an edge to AS a2 via interface 1.
+type TopologySpec adt {
+	TopologySpec_{
+		coreAS		set[IO_as]
+		links	 		dict[IO_as](dict[IO_ifs]IO_as)
+	}
+}
+
+ghost
+decreases
+pure func (dp DataPlaneSpec) Valid() bool{
+	return domain(dp.linkTypes) == domain(dp.neighborIAs) && 
+		dp.localIA in domain(dp.topology.links) &&
+		dp.neighborIAs == dp.topology.links[dp.localIA] &&
+		(forall core IO_as :: {core in dp.topology.coreAS} core in dp.topology.coreAS ==> core in domain(dp.topology.links))
+}
+
+ghost
+decreases
+requires ifs in domain(dp.linkTypes)
+pure func (dp DataPlaneSpec) GetLinkType(ifs IO_ifs) IO_Link {
+	return dp.linkTypes[ifs]
+}
+
+ghost
+requires ifs in domain(dp.neighborIAs)
+decreases
+pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as {
+	return dp.neighborIAs[ifs]
+}
+
+ghost
+decreases
+pure func (dp DataPlaneSpec) GetLocalIA() IO_as {
+	return dp.localIA
+}
+
+ghost
+decreases
+pure func (dp DataPlaneSpec) GetCoreAS() set[IO_as] {
+	return dp.topology.coreAS
+}