Adding DataPlaneSpec to the IO-spec

verification/io/dataplane_abstract.gobra

@@ -0,0 +1,54 @@
+// 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_{
+		//external          seq[IO_ifs]
+		linkTypes		dict[IO_ifs]IO_Link
+		neighborIAs     dict[IO_ifs]IO_as
+		internal        IO_ifs //TODO: propably not needed, = 0
+		localIA         IO_as
+		topology 		TopologySpec
+	}
+}
+
+type TopologySpec adt {
+	TopologySpec_{
+		core_as_set     set[IO_as]
+		links	 		dict[IO_as](dict[IO_ifs]IO_as)
+	}
+}
+
+ghost
+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)
+pure func (dp DataPlaneSpec) getNeighborIA(ifs IO_ifs) IO_as {
+	return dp.neighborIAs[ifs]
+}
+
+ghost
+pure func (dp DataPlaneSpec) getLocalIA() IO_as {
+	return dp.localIA
+}