replace 4 by its constant InfoLen

mlimbeck · Nov 22, 2023 · e923c40 · e923c40
1 parent 24d19e1
commit e923c40
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/router/io-spec.gobra b/router/io-spec.gobra
@@ -372,7 +372,7 @@ pure func segment(raw []byte,
 }
 
 ghost
-requires 4 + 8 * currINFIdx + 8 <= offset
+requires infoFieldOffset(currINFIdx) + path.InfoLen <= offset
 requires 0 < len(asid)
 requires offset + path.HopLen * len(asid) <= len(raw)
 requires 0 <= currHFIdx && currHFIdx <= len(asid)