From a68a3e791c310e1fc809df3834507c412b248064 Mon Sep 17 00:00:00 2001
From: mlimbeck <mlimbeck@student.ethz.ch>
Date: Wed, 22 Nov 2023 21:29:31 +0100
Subject: [PATCH] move validMetaLenInPath() to test file

---
 pkg/slayers/path/scion/base_spec.gobra      |  7 -------
 pkg/slayers/path/scion/base_spec_test.gobra | 11 +++++++++++
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra
index b933026cb..b12aec326 100644
--- a/pkg/slayers/path/scion/base_spec.gobra
+++ b/pkg/slayers/path/scion/base_spec.gobra
@@ -45,13 +45,6 @@ pred (b *Base) Mem() {
 	(0 < b.NumINF ==> 0 < b.NumHops)
 }
 
-ghost 
-ensures res
-decreases
-pure func validMetaLenInPath() (res bool) {
-	return MetaLen == path.MetaLen
-}
-
 ghost
 decreases
 pure func (b Base) ValidCurrInfSpec() bool {
diff --git a/pkg/slayers/path/scion/base_spec_test.gobra b/pkg/slayers/path/scion/base_spec_test.gobra
index d48116d9b..5d07d6a53 100644
--- a/pkg/slayers/path/scion/base_spec_test.gobra
+++ b/pkg/slayers/path/scion/base_spec_test.gobra
@@ -16,7 +16,18 @@
 
 package scion
 
+import (
+	"github.com/scionproto/scion/pkg/slayers/path"
+)
+
 func canAllocateBase() {
 	b := &Base{}
 	fold b.Mem()
+}
+
+ghost 
+ensures res
+decreases
+pure func validMetaLenInPath() (res bool) {
+	return MetaLen == path.MetaLen
 }
\ No newline at end of file