diff --git a/pkg/addr/fmt.go b/pkg/addr/fmt.go
index f534b82ea..0e29f2f1d 100644
--- a/pkg/addr/fmt.go
+++ b/pkg/addr/fmt.go
@@ -119,9 +119,6 @@ func fmtAS(as_ AS, sep string) string {
 	}
 	// Format BGP ASes as decimal
 	if as_ <= MaxBGPAS {
-		// (VerifiedSCION) the following property is guaranteed by the type system,
-		// but Gobra cannot infer it yet
-		// @ assume 0 <= as_
 		return strconv.FormatUint(uint64(as_), 10)
 	}
 	// Format all other ASes as 'sep'-separated hex.
@@ -131,6 +128,7 @@ func fmtAS(as_ AS, sep string) string {
 	var b /*@@@*/ strings.Builder
 	// @ b.ZeroBuilderIsReadyToUse()
 	b.Grow(maxLen)
+	// @ invariant 0 <= i && i <= asParts
 	// @ invariant b.Mem()
 	// @ decreases asParts - i
 	for i := 0; i < asParts; i++ {
@@ -138,9 +136,6 @@ func fmtAS(as_ AS, sep string) string {
 			b.WriteString(sep)
 		}
 		shift := uint(asPartBits * (asParts - i - 1))
-		// (VerifiedSCION) the following property is guaranteed by the type system,
-		// but Gobra cannot infer it yet
-		// @ assume 0 <= uint64(as_>>shift)&asPartMask
 		b.WriteString(strconv.FormatUint(uint64(as_>>shift)&asPartMask, asPartBase))
 	}
 	return b.String()
diff --git a/pkg/addr/host.go b/pkg/addr/host.go
index ce971e76c..4afb36c57 100644
--- a/pkg/addr/host.go
+++ b/pkg/addr/host.go
@@ -34,6 +34,7 @@ import (
 	"strings"
 
 	"github.com/scionproto/scion/pkg/private/serrors"
+	//@ "math"
 	//@ . "github.com/scionproto/scion/verification/utils/definitions"
 	//@ sl "github.com/scionproto/scion/verification/utils/slices"
 )
@@ -358,7 +359,10 @@ func (h HostSVC) Pack() (res []byte) {
 	return out
 }
 
-// @ requires pad >= 0
+// (VerifiedSCION) the upper bound on 'pad' is needed under the sound bounded-integer
+// semantics: without it, 'HostLenSVC + pad' may overflow and the length passed to 'make'
+// is then not known to be non-negative.
+// @ requires 0 <= pad && pad <= math.MaxInt64 - HostLenSVC
 // @ ensures acc(res)
 // @ decreases
 func (h HostSVC) PackWithPad(pad int) (res []byte) {
diff --git a/pkg/addr/isdas.go b/pkg/addr/isdas.go
index ee5f5e296..0103348fe 100644
--- a/pkg/addr/isdas.go
+++ b/pkg/addr/isdas.go
@@ -127,7 +127,7 @@ func asParseBGP(s string) (retAs AS, retErr error) {
 	// @ strconv.Exp2to10(30)
 	// @ strconv.Exp2to10(20)
 	// @ strconv.Exp2to10(10)
-	// @ assert _as < uint64(strconv.Exp(2, BGPASBits))
+	// @ assert integer(_as) < strconv.Exp(2, BGPASBits)
 	return AS(_as), nil
 }
 
diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
index 886d6c3d2..29e4c9c83 100644
--- a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
+++ b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
@@ -102,7 +102,7 @@ pure func HopfieldsByteSlice(raw []byte, currInfIdx int, segs io.SegLens) ([]byt
 
 // SliceBytesIntoSegments splits the raw bytes of a packet into its hopfield segments
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires acc(sl.Bytes(raw, 0, len(raw)), p)
@@ -126,7 +126,7 @@ func SliceBytesIntoSegments(raw []byte, segs io.SegLens, p perm) {
 
 // CombineBytesFromSegments combines the three hopfield segments of a packet into a single slice of bytes.
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires PktLen(segs, MetaLen) <= len(raw)
 requires acc(sl.Bytes(raw[:HopfieldsStartIdx(0, segs)], 0, HopfieldsStartIdx(0, segs)), p)
@@ -150,7 +150,7 @@ func CombineBytesFromSegments(raw []byte, segs io.SegLens, p perm) {
 
 // SliceBytesIntoInfoFields splits the raw bytes of a packet into its infofields
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires MetaLen + numInf * path.InfoLen <= len(raw)
 requires numInf == segs.NumInfoFields()
@@ -182,7 +182,7 @@ func SliceBytesIntoInfoFields(raw []byte, numInf int, segs io.SegLens, p perm) {
 
 // CombineBytesFromInfoFields combines the infofields of a packet into a single slice of bytes.
 ghost
-requires 0 < p
+requires noPerm < p
 requires segs.Valid()
 requires MetaLen + numInf * path.InfoLen <= len(raw)
 requires numInf == segs.NumInfoFields()
@@ -623,7 +623,7 @@ func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf
 // to the subslice containing all past hopfields, to the sublice containing the current hopfield,
 // and to another containing all future hopfields.
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= currHfIdx && currHfIdx < segLen
 requires segLen * path.HopLen == len(hopfields)
 requires acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
@@ -647,7 +647,7 @@ func SplitHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
 // current hopfield, and future hopfields of a segment into a single permission to the slice
 // containing all hopfields of that segment.
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= currHfIdx && currHfIdx < segLen
 requires segLen * path.HopLen == len(hopfields)
 requires let currHfStart := currHfIdx * path.HopLen in
diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra
index 3bcf6a96f..6182f2abe 100644
--- a/pkg/slayers/scion_spec.gobra
+++ b/pkg/slayers/scion_spec.gobra
@@ -332,7 +332,7 @@ pure func (s *SCION) PathScionEndIdx(ub []byte) int {
 }
 
 ghost
-requires  0 < p
+requires  noPerm < p
 preserves acc(s.Mem(ub), p)
 ensures   let start := s.PathStartIdx(ub) in
 	let end := s.PathEndIdx(ub) in
diff --git a/router/dataplane.go b/router/dataplane.go
index 7803ba3c7..918692f4b 100644
--- a/router/dataplane.go
+++ b/router/dataplane.go
@@ -325,9 +325,9 @@ func (d *DataPlane) SetKey(key []byte) (res error) {
 	// @ unfold MutexInvariant{d}()
 	// @ assert !d.IsRunning()
 	// @ d.isRunningEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ d.keyIsSetEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ unfold macFactoryInv(d.macFactory, d.key)
 	// @ defer fold MutexInvariant{d}()
 	// @ defer fold d.Mem()
@@ -387,9 +387,9 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error {
 	// @ unfold MutexInvariant{d}()
 	// @ assert !d.IsRunning()
 	// @ d.isRunningEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ d.internalIsSetEq()
-	// @ unfold acc(d.Mem(), 1/2)
+	// @ unfold acc(d.Mem(), perm(1, 2))
 	// @ unfold internalInv(d.internal)
 	// @ unfold internalIPInv(d.internalIP)
 	if d.running {
@@ -438,16 +438,16 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error {
 		// @ Unreachable()
 		return emptyValue
 	}
-	// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), 1/2) }
+	// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), perm(1, 2)) }
 	if _, existsB := d.external[ifID]; existsB {
 		// @ establishAlreadySet()
-		// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), 1/2) }
+		// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), perm(1, 2)) }
 		// @ fold externalInv(d.external)
 		// @ fold d.Mem()
 		// @ fold MutexInvariant{d}()
 		return serrors.WithCtx(alreadySet, "ifID", ifID)
 	}
-	// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), 1/2) }
+	// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), perm(1, 2)) }
 	if d.external == nil {
 		d.external = make(map[uint16]BatchConn)
 		// @ fold accBatchConn(d.external)
diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra
index f6e3288f3..9bcd12be6 100644
--- a/router/dataplane_spec.gobra
+++ b/router/dataplane_spec.gobra
@@ -35,9 +35,9 @@ import (
 	sl "github.com/scionproto/scion/verification/utils/slices"
 )
 
-ghost const MutexPerm perm = 1/4
-ghost const OutMutexPerm perm = 3/4
-ghost const runningPerm perm = 1/2
+ghost const MutexPerm perm = perm(1, 4)
+ghost const OutMutexPerm perm = perm(3, 4)
+ghost const runningPerm perm = perm(1, 2)
 
 pred MutexInvariant(d *DataPlane) {
 	acc(&d.running, runningPerm) &&
@@ -67,7 +67,7 @@ pred (d *DataPlane) Mem() {
 	acc(&d.macFactory)                        &&
 	acc(&d.bfdSessions)                       &&
 	acc(&d.localIA)                           &&
-	acc(&d.running, 1/2)                      &&
+	acc(&d.running, perm(1, 2))                      &&
 	acc(&d.Metrics)                           &&
 	acc(&d.forwardingMetrics)                 &&
 	acc(&d.key)                               &&
diff --git a/verification/dependencies/crypto/cipher/cipher.gobra b/verification/dependencies/crypto/cipher/cipher.gobra
index 43d4d6656..34fb6022a 100644
--- a/verification/dependencies/crypto/cipher/cipher.gobra
+++ b/verification/dependencies/crypto/cipher/cipher.gobra
@@ -94,7 +94,7 @@ type BlockMode interface {
 	// maintains state and does not reset at each CryptBlocks call.
 	requires  len(src) <= len(dst)
 	preserves Mem()
-	preserves acc(sl.Bytes(dst, 0, len(dst)), 1 - R10)
+	preserves acc(sl.Bytes(dst, 0, len(dst)), writePerm - R10)
 	preserves dst !== src ==> acc(sl.Bytes(dst, 0, len(dst)), R10)
 	preserves acc(sl.Bytes(src, 0, len(src)), R10)
 	ensures   BlockSize() == old(BlockSize())
diff --git a/verification/dependencies/github.com/google/gopacket/flows.gobra b/verification/dependencies/github.com/google/gopacket/flows.gobra
index 585b46cdb..7558379a7 100644
--- a/verification/dependencies/github.com/google/gopacket/flows.gobra
+++ b/verification/dependencies/github.com/google/gopacket/flows.gobra
@@ -29,13 +29,13 @@ type Flow struct {
 	src, dst   [MaxEndpointSize]byte
 }
 
-preserves acc(sl.Bytes(src, 0, len(src)), 1/10000) && acc(sl.Bytes(dst, 0, len(dst)), 1/10000)
+preserves acc(sl.Bytes(src, 0, len(src)), perm(1, 10000)) && acc(sl.Bytes(dst, 0, len(dst)), perm(1, 10000))
 requires len(src) <= MaxEndpointSize && len(dst) <= MaxEndpointSize
 ensures f.slen == len(src)
 ensures f.dlen == len(dst)
-ensures unfolding acc(sl.Bytes(src, 0, len(src)), 1/10000) in
+ensures unfolding acc(sl.Bytes(src, 0, len(src)), perm(1, 10000)) in
 	forall i int :: { &src[i] } 0 <= i && i < len(src) ==> f.src[i] == src[i]
-ensures unfolding acc(sl.Bytes(dst, 0, len(dst)), 1/10000) in
+ensures unfolding acc(sl.Bytes(dst, 0, len(dst)), perm(1, 10000)) in
 	forall i int :: { &dst[i] } 0 <= i && i < len(dst) ==> f.dst[i] == dst[i]
 ensures f.typ == t
 decreases
diff --git a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra
index 14214df43..9e117539f 100644
--- a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra
+++ b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra
@@ -135,7 +135,7 @@ pred (b *BFDAuthHeader) Mem() {
 	acc(b) && sl.Bytes(b.Data, 0, len(b.Data))
 }
 
-preserves acc(h, 1/10000)
+preserves acc(h, perm(1, 10000))
 decreases
 func (h *BFDAuthHeader) Length() int {
 	switch h.AuthType {
@@ -176,7 +176,7 @@ pred (b *BFD) NonInitMem() {
 
 pred (b *BFD) Mem(ub []byte)
 
-preserves acc(d, 1/10000)
+preserves acc(d, perm(1, 10000))
 decreases
 func (d *BFD) Length() int
 
diff --git a/verification/dependencies/github.com/google/gopacket/layers/tcpip.gobra b/verification/dependencies/github.com/google/gopacket/layers/tcpip.gobra
index 4706f04c5..11216f3d3 100644
--- a/verification/dependencies/github.com/google/gopacket/layers/tcpip.gobra
+++ b/verification/dependencies/github.com/google/gopacket/layers/tcpip.gobra
@@ -18,7 +18,7 @@ type tcpipchecksum struct {
 type tcpipPseudoHeader interface {
 	pred Mem()
 
-	preserves acc(Mem(), 1/10000)
+	preserves acc(Mem(), perm(1, 10000))
 	decreases
 	pseudoheaderChecksum() (uint32, error)
 }
diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra
index 339466fb6..c2c678d7d 100644
--- a/verification/dependencies/hash/hash.gobra
+++ b/verification/dependencies/hash/hash.gobra
@@ -35,7 +35,7 @@ type Hash interface {
 	// io.Writer // (gobra) Fix: this was changed to be able to re-specify method Write with a stronger spec
 
 	preserves Mem() 
-	preserves acc(p, 1/1000)
+	preserves acc(p, perm(1, 1000))
 	ensures   0 <= n && n <= len(p)
 	// the last conjunct comes from the spec of io.Writer
 	ensures   err == nil && n == len(p)
@@ -45,7 +45,7 @@ type Hash interface {
 
 	// Sum appends the current hash to b and returns the resulting slice.
 	// It does not change the underlying hash state.
-	preserves acc(Mem(), 1/1000)
+	preserves acc(Mem(), perm(1, 1000))
 	requires acc(b)
 	ensures  acc(res) && len(res) == len(b) + Size()
 	decreases
diff --git a/verification/dependencies/io/io.gobra b/verification/dependencies/io/io.gobra
index 3970ba8cb..a838deb48 100644
--- a/verification/dependencies/io/io.gobra
+++ b/verification/dependencies/io/io.gobra
@@ -72,7 +72,7 @@ type Writer interface {
 	pred Mem()
 
 	preserves Mem() 
-	preserves acc(p, 1/1000)
+	preserves acc(p, perm(1, 1000))
 	ensures 0 <= n && n <= len(p)
 	ensures (n < len(p)) == (err != nil)
 	Write(p []byte) (n int, err error)
diff --git a/verification/dependencies/math/const.gobra b/verification/dependencies/math/const.gobra
new file mode 100644
index 000000000..92f758829
--- /dev/null
+++ b/verification/dependencies/math/const.gobra
@@ -0,0 +1,32 @@
+// Copyright 2009 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in the LICENSE file.
+
+// Signatures for the public declarations in file
+// https://github.com/golang/go/blob/master/src/math/const.go
+
+// +gobra
+
+package math
+
+// Integer limit values.
+//
+// (VerifiedSCION) the architecture-dependent limits `MaxInt`, `MinInt`, and
+// `MaxUint` are deliberately not provided: their values depend on the width of
+// the platform `int`/`uint`, which Gobra does not fix, so a proof relying on
+// them would be unsound for some target. Use the limits of a concrete sized
+// type instead.
+const (
+	MaxInt8   = 1<<7 - 1  // 127
+	MinInt8   = -1 << 7   // -128
+	MaxInt16  = 1<<15 - 1 // 32767
+	MinInt16  = -1 << 15  // -32768
+	MaxInt32  = 1<<31 - 1 // 2147483647
+	MinInt32  = -1 << 31  // -2147483648
+	MaxInt64  = 1<<63 - 1 // 9223372036854775807
+	MinInt64  = -1 << 63  // -9223372036854775808
+	MaxUint8  = 1<<8 - 1  // 255
+	MaxUint16 = 1<<16 - 1 // 65535
+	MaxUint32 = 1<<32 - 1 // 4294967295
+	MaxUint64 = 1<<64 - 1 // 18446744073709551615
+)
diff --git a/verification/dependencies/net/iprawsock.gobra b/verification/dependencies/net/iprawsock.gobra
index 20d001a40..62014ea89 100644
--- a/verification/dependencies/net/iprawsock.gobra
+++ b/verification/dependencies/net/iprawsock.gobra
@@ -35,5 +35,5 @@ pred (a *IPAddr) Mem() {
 ensures res == "ip"
 func (a *IPAddr) Network() (res string) { return "ip" }
 
-preserves a != nil ==> acc(a.Mem(), 1/1000)
+preserves a != nil ==> acc(a.Mem(), perm(1, 1000))
 func (a *IPAddr) String() string
diff --git a/verification/dependencies/net/net.gobra b/verification/dependencies/net/net.gobra
index 9b3003c20..8c250ce16 100644
--- a/verification/dependencies/net/net.gobra
+++ b/verification/dependencies/net/net.gobra
@@ -20,12 +20,12 @@ import (
 type Addr interface {
 	pred Mem()
 
-	requires acc(Mem(), 1/1000)
-	ensures acc(Mem(), 1/1000)
+	requires acc(Mem(), perm(1, 1000))
+	ensures acc(Mem(), perm(1, 1000))
 	Network() string
 
-	requires acc(Mem(), 1/1000)
-	ensures acc(Mem(), 1/1000)
+	requires acc(Mem(), perm(1, 1000))
+	ensures acc(Mem(), perm(1, 1000))
 	String() string
 }
 
diff --git a/verification/dependencies/net/udpsock.gobra b/verification/dependencies/net/udpsock.gobra
index d1a9f2b71..321cfa475 100644
--- a/verification/dependencies/net/udpsock.gobra
+++ b/verification/dependencies/net/udpsock.gobra
@@ -73,10 +73,10 @@ ensures   err != nil ==> err.ErrorMem()
 func (c *UDPConn) ReadFrom(b []byte) (n int, addr Addr, err error)
 
 // WriteToUDP acts like WriteTo but takes a UDPAddr.
-requires acc(c.Mem(), _) && acc(addr.Mem(), 1/1000)
-requires forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], 1/1000)
-ensures c.Mem() && acc(addr.Mem(), 1/1000)
-ensures forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], 1/1000)
+requires acc(c.Mem(), _) && acc(addr.Mem(), perm(1, 1000))
+requires forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], perm(1, 1000))
+ensures c.Mem() && acc(addr.Mem(), perm(1, 1000))
+ensures forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], perm(1, 1000))
 func (c *UDPConn) WriteToUDP(b []byte, addr *UDPAddr) (int, error)
 
 // WriteTo implements the PacketConn WriteTo method.
diff --git a/verification/dependencies/strconv/atoi.gobra b/verification/dependencies/strconv/atoi.gobra
index e50a2b4ce..ba02639c0 100644
--- a/verification/dependencies/strconv/atoi.gobra
+++ b/verification/dependencies/strconv/atoi.gobra
@@ -10,10 +10,14 @@
 package strconv
 
 // a to the power of b
+// (VerifiedSCION) 'base', 'exp', and the result are mathematical integers: under the sound
+// bounded-integer semantics, typing them as 'int' would make the repeated multiplication
+// overflow-prone and thus opaque, and 'Exp(2, 64)' (a legal argument of 'ParseUint') is not
+// even representable as an 'int'.
 ghost
 requires exp >= 0
 decreases exp
-pure func Exp(base int, exp int) (res int) {
+pure func Exp(base integer, exp integer) (res integer) {
 	return exp == 0 ? 1 : (base * Exp(base, exp - 1))
 }
 
@@ -22,7 +26,7 @@ ghost
 requires exp >= 10
 ensures  Exp(2, exp) == 1024 * Exp(2, exp - 10)
 decreases
-func Exp2to10(exp int) {
+func Exp2to10(exp integer) {
 	assert Exp(2, exp) == 2 * Exp(2, exp - 1)
 	assert Exp(2, exp) == 4 * Exp(2, exp - 2)
 	assert Exp(2, exp) == 8 * Exp(2, exp - 3)
@@ -37,7 +41,7 @@ func Exp2to10(exp int) {
 // ParseUint is like ParseInt but for unsigned numbers.
 requires base == 0 || (2 <= base && base <= 36)
 requires bitSize > 0 && bitSize <= 64
-ensures retErr == nil ==> (ret >= 0 && ret < uint64(Exp(2, bitSize)))
+ensures retErr == nil ==> integer(ret) < Exp(2, integer(bitSize))
 ensures retErr != nil ==> retErr.ErrorMem()
 decreases _
 func ParseUint(s string, base int, bitSize int) (ret uint64, retErr error)
diff --git a/verification/dependencies/time/time.gobra b/verification/dependencies/time/time.gobra
index 141537282..24bfa1df8 100644
--- a/verification/dependencies/time/time.gobra
+++ b/verification/dependencies/time/time.gobra
@@ -259,7 +259,7 @@ func (t Time) MarshalBinary() ([]byte, error)
 
 // UnmarshalBinary implements the encoding.BinaryUnmarshaler interface.
 requires acc(t)
-requires p > 0
+requires noPerm < p
 requires forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
 ensures acc(t)
 ensures forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
@@ -273,7 +273,7 @@ func (t Time) GobEncode() (res []byte, error)
 
 // GobDecode implements the gob.GobDecoder interface.
 requires acc(t)
-requires p > 0
+requires noPerm < p
 requires forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
 ensures acc(t)
 ensures forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
@@ -287,7 +287,7 @@ func (t Time) MarshalJSON() (res []byte, error)
 
 // UnmarshalJSON implements the json.Unmarshaler interface.
 requires acc(t)
-requires p > 0
+requires noPerm < p
 requires forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
 ensures acc(t)
 ensures forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
@@ -301,7 +301,7 @@ func (t Time) MarshalText() (res []byte, error)
 
 // UnmarshalText implements the encoding.TextUnmarshaler interface.
 requires acc(t)
-requires p > 0
+requires noPerm < p
 requires forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
 ensures acc(t)
 ensures forall i int :: { &data[i] } 0 <= i && i < len(data) ==> acc(&data[i], p)
@@ -315,7 +315,7 @@ func Unix(sec int64, nsec int64) Time
 
 // Date returns the Time corresponding to yyyy-mm-dd hh:mm:ss + nsec nanoseconds
 // in the appropriate zone for that time in the given location.
-requires p > 0
+requires noPerm < p
 requires acc(loc, p)
 ensures acc(loc, p)
 decreases
diff --git a/verification/utils/bitwise/bitwise-eqs.gobra b/verification/utils/bitwise/bitwise-eqs.gobra
index 0e399685e..9c2bc7a58 100644
--- a/verification/utils/bitwise/bitwise-eqs.gobra
+++ b/verification/utils/bitwise/bitwise-eqs.gobra
@@ -21,7 +21,10 @@
 package bitwise
 
 ghost
-ensures 0 <= b && b < 256
+// (VerifiedSCION) stated over the mathematical integers: under the sound bounded-integer
+// semantics '256' is not a valid 'byte' constant, so 'b < 256' no longer type-checks.
+// The property itself now holds by typing, so callers need this lemma only to name it.
+ensures 0 <= integer(b) && integer(b) < 256
 decreases
 func ByteValue(b byte)
 
diff --git a/verification/utils/definitions/definitions.gobra b/verification/utils/definitions/definitions.gobra
index 3b458ff59..7e3497293 100644
--- a/verification/utils/definitions/definitions.gobra
+++ b/verification/utils/definitions/definitions.gobra
@@ -16,9 +16,9 @@
 
 package definitions
 
-const HalfPerm perm = 1/2
+const HalfPerm perm = perm(1, 2)
 const (
-	R00 perm = 1/(2 << iota)
+	R00 perm = perm(1, 2 << iota)
 	R0
 	R1
 	R2
diff --git a/verification/utils/monoset/monoset.gobra b/verification/utils/monoset/monoset.gobra
index d84b09a10..74069363c 100644
--- a/verification/utils/monoset/monoset.gobra
+++ b/verification/utils/monoset/monoset.gobra
@@ -29,7 +29,7 @@ type BoundedMonotonicSet struct {
 pred (b BoundedMonotonicSet) Inv() {
 	(b.Start <= b.End) &&
 	(forall i int64 :: b.Start <= i && i <= b.End ==>
-		(i elem domain(b.valuesMap) && acc(b.valuesMap[i], 1/2))) &&
+		(i elem domain(b.valuesMap) && acc(b.valuesMap[i], perm(1, 2)))) &&
 	// injectivity requirement
 	(forall j1, j2 int64 :: b.Start <= j1 && j1 <= b.End && b.Start <= j2 && j2 <= b.End && j1 != j2 ==>
 		b.valuesMap[j1] != b.valuesMap[j2])
@@ -83,13 +83,13 @@ func (b BoundedMonotonicSet) PromoteContains(i int64) {
 pred (b BoundedMonotonicSet) DoesNotContain(i int64) {
 	b.Start <= i && i <= b.End &&
 	i elem domain(b.valuesMap) &&
-	acc(b.valuesMap[i], 1/2) &&
+	acc(b.valuesMap[i], perm(1, 2)) &&
 	!(*b.valuesMap[i])
 }
 
 ghost
-preserves acc(b.Inv(), 1/4)
-preserves acc(b.DoesNotContain(i), 1/4)
+preserves acc(b.Inv(), perm(1, 4))
+preserves acc(b.DoesNotContain(i), perm(1, 4))
 ensures   b.Start <= i && i <= b.End
 ensures   !b.FContains(i)
 decreases
@@ -100,7 +100,7 @@ func (b BoundedMonotonicSet) DoesNotContainImpliesNotFContains(i int64) {
 }
 
 ghost
-preserves acc(b.Inv(), 1/4)
+preserves acc(b.Inv(), perm(1, 4))
 preserves b.Contains(i)
 ensures   b.Start <= i && i <= b.End
 ensures   b.FContains(i)
@@ -156,7 +156,7 @@ func Alloc(start, end int64) (res BoundedMonotonicSet) {
 	invariant forall j int64 :: {b.valuesMap[j]} {*b.valuesMap[j]} i <= j && j <= end ==>
 		acc(b.valuesMap[j]) && !(*b.valuesMap[j])
 	invariant forall j int64 :: start <= j && j < i ==>
-		acc(b.valuesMap[j], 1/2)
+		acc(b.valuesMap[j], perm(1, 2))
 	invariant forall j int64 :: start <= j && j < i ==>
 		b.DoesNotContain(j)
 	invariant forall j int64 :: start <= j && j < i ==>
@@ -193,7 +193,7 @@ pure func (b BoundedMonotonicSet) toSetAux(start int64) set[int64] {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires acc(b.Inv(), p)
 requires b.Contains(v)
 ensures  acc(b.Inv(), p)
@@ -243,7 +243,7 @@ func (b BoundedMonotonicSet) ContainsImpliesAbstractContains(v int64, p perm) {
 }
 
 ghost
-requires  0 < p
+requires  noPerm < p
 preserves acc(b.Inv(), p)
 preserves b.DoesNotContain(v)
 ensures   !(v elem b.ToSet())
diff --git a/verification/utils/slices/slices.gobra b/verification/utils/slices/slices.gobra
index f8c21ed66..27d764497 100644
--- a/verification/utils/slices/slices.gobra
+++ b/verification/utils/slices/slices.gobra
@@ -40,7 +40,7 @@ pure func GetByte(s []byte, start int, end int, i int) byte {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires acc(Bytes(s, start, end), p)
 requires start <= idx && idx <= end
 ensures  acc(Bytes(s, start, idx), p)
@@ -53,7 +53,7 @@ func SplitByIndex_Bytes(s []byte, start int, end int, idx int, p perm) {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires acc(Bytes(s, start, idx), p)
 requires acc(Bytes(s, idx,   end), p)
 ensures  acc(Bytes(s, start, end), p)
@@ -65,7 +65,7 @@ func CombineAtIndex_Bytes(s []byte, start int, end int, idx int, p perm) {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires acc(Bytes(s, start, end), p)
 // the following precondition convinces Gobra that
 // the slice operation is well-formed
@@ -79,7 +79,7 @@ func Reslice_Bytes(s []byte, start int, end int, p perm) {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= start && start <= end && end <= cap(s)
 requires acc(Bytes(s[start:end], 0, len(s[start:end])), p)
 ensures  acc(Bytes(s, start, end), p)
@@ -105,7 +105,7 @@ func Unslice_Bytes(s []byte, start int, end int, p perm) {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= start && start <= end && end <= len(s)
 requires acc(Bytes(s, 0, len(s)), p)
 ensures  acc(Bytes(s[start:end], 0, end-start), p)
@@ -119,7 +119,7 @@ func SplitRange_Bytes(s []byte, start int, end int, p perm) {
 }
 
 ghost
-requires 0 < p
+requires noPerm < p
 requires 0 <= start && start <= end && end <= len(s)
 requires acc(Bytes(s[start:end], 0, end-start), p)
 requires acc(Bytes(s, 0, start), p)
@@ -159,7 +159,7 @@ func PermsImplyIneqWithWildcard(s1 []byte, s2 []byte) {
 }
 
 ghost
-requires  0 < p
+requires  noPerm < p
 requires  len(s1) > 0 || len(s2) > 0
 preserves Bytes(s1, 0, len(s1))
 preserves acc(Bytes(s2, 0, len(s2)), p)