1	import Base
2	
3	# Accepts an interval whose endpoint does not exceed its address-space limit.
4	def range_valid(limit: Nat, offset: Nat, max: Nat) -> Bool:
5	  Nat.is_le(offset, Nat.sub(limit, max))