diff --git a/lib/sys/linux/cgroup.ex b/lib/sys/linux/cgroup.ex
index 1f5890c..a5b1b0a 100644
--- a/lib/sys/linux/cgroup.ex
+++ b/lib/sys/linux/cgroup.ex
@@ -12,16 +12,19 @@ defmodule Sys.Linux.Cgroup do
   @spec versions :: {:ok, MapSet.t(:cgroup | :cgroup2)} | {:error, atom()}
   def versions do
     case Mounts.list() do
-      {:ok, mounts} ->
-        versions =
-          for %{fs_type: fs} <- mounts, fs in ~w(cgroup cgroup2), into: MapSet.new() do
-            String.to_existing_atom(fs)
-          end
-
-        {:ok, versions}
+      {:ok, mounts} -> {:ok, versions_from_mounts(mounts)}
+      {:error, reason} -> {:error, reason}
+    end
+  end
 
-      {:error, reason} ->
-        {:error, reason}
+  @doc """
+  Reduce a list of mounts to the set of cgroup versions present, keyed by
+  filesystem type. Pure; `versions/0` is this applied to `/proc/mounts`.
+  """
+  @spec versions_from_mounts([Sys.Linux.Fstab.Spec.t()]) :: MapSet.t(:cgroup | :cgroup2)
+  def versions_from_mounts(mounts) do
+    for %{fs_type: fs} <- mounts, fs in ~w(cgroup cgroup2), into: MapSet.new() do
+      String.to_existing_atom(fs)
     end
   end
 end
diff --git a/lib/sys/linux/nss.ex b/lib/sys/linux/nss.ex
index 145b38d..7bfd4c3 100644
--- a/lib/sys/linux/nss.ex
+++ b/lib/sys/linux/nss.ex
@@ -27,17 +27,23 @@ defmodule Sys.Linux.Nss do
                {:getent_failed, non_neg_integer()} | :getent_unavailable | :invalid_format}
     def entries do
       with {:ok, output} <- Sys.Linux.Nss.getent(@getent_db) do
-        output
-        |> String.split("\n", trim: true)
-        |> Enum.reduce_while({:ok, []}, fn line, {:ok, acc} ->
-          case parse(line) do
-            {:ok, spec} -> {:cont, {:ok, [spec | acc]}}
-            {:error, _} = error -> {:halt, error}
-          end
-        end)
+        from_output(output)
       end
     end
 
+    @doc "Parse raw `getent passwd` output into specs, halting on the first bad line."
+    @spec from_output(binary()) :: {:ok, [Spec.t()]} | {:error, :invalid_format}
+    def from_output(output) do
+      output
+      |> String.split("\n", trim: true)
+      |> Enum.reduce_while({:ok, []}, fn line, {:ok, acc} ->
+        case parse(line) do
+          {:ok, spec} -> {:cont, {:ok, [spec | acc]}}
+          {:error, _} = error -> {:halt, error}
+        end
+      end)
+    end
+
     # passwd line: name:password:uid:gid:gecos:home_dir:shell
     @spec parse(String.t()) :: {:ok, Spec.t()} | {:error, :invalid_format}
     defp parse(line) do
@@ -83,17 +89,23 @@ defmodule Sys.Linux.Nss do
                {:getent_failed, non_neg_integer()} | :getent_unavailable | :invalid_format}
     def entries do
       with {:ok, output} <- Sys.Linux.Nss.getent(@getent_db) do
-        output
-        |> String.split("\n", trim: true)
-        |> Enum.reduce_while({:ok, []}, fn line, {:ok, acc} ->
-          case parse(line) do
-            {:ok, spec} -> {:cont, {:ok, [spec | acc]}}
-            {:error, _} = error -> {:halt, error}
-          end
-        end)
+        from_output(output)
       end
     end
 
+    @doc "Parse raw `getent group` output into specs, halting on the first bad line."
+    @spec from_output(binary()) :: {:ok, [Spec.t()]} | {:error, :invalid_format}
+    def from_output(output) do
+      output
+      |> String.split("\n", trim: true)
+      |> Enum.reduce_while({:ok, []}, fn line, {:ok, acc} ->
+        case parse(line) do
+          {:ok, spec} -> {:cont, {:ok, [spec | acc]}}
+          {:error, _} = error -> {:halt, error}
+        end
+      end)
+    end
+
     # group line: name:password:gid:member1,member2,...
     @spec parse(String.t()) :: {:ok, Spec.t()} | {:error, :invalid_format}
     defp parse(line) do
diff --git a/test/hyper/node/budget/hard_state_properties_test.exs b/test/hyper/node/budget/hard_state_properties_test.exs
new file mode 100644
index 0000000..1ebf0b6
--- /dev/null
+++ b/test/hyper/node/budget/hard_state_properties_test.exs
@@ -0,0 +1,67 @@
+defmodule Hyper.Node.Budget.HardStatePropertiesTest do
+  @moduledoc """
+  Algebraic laws of the pure `Hyper.Node.Budget.Hard.State` accumulator: `cut`
+  is the inverse of `bump` on every spec, bumps accumulate additively (so the
+  running total is order-independent), and `track`/`untrack` round-trip a
+  reservation by reference. The example tests spot-check single values; these
+  pin the laws across the domain.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Hyper.Node.Budget.Hard.State
+  alias Hyper.Vm.Instance.Spec
+  alias Unit.{Bandwidth, Information}
+
+  # Only `mem`/`disk` matter to bump/cut; the other fields are along for the ride.
+  defp spec do
+    gen all(mem_mib <- integer(0..1_000_000), disk_mib <- integer(0..1_000_000)) do
+      %Spec{
+        vcpus: 1,
+        mem: Information.mib(mem_mib),
+        disk: Information.mib(disk_mib),
+        disk_bw: Bandwidth.zero(),
+        net_bw: Bandwidth.zero()
+      }
+    end
+  end
+
+  property "cut undoes bump for any spec" do
+    check all(s <- spec()) do
+      state = State.zero() |> State.bump(s) |> State.cut(s)
+      assert state.mem_allocated == Information.zero()
+      assert state.disk_allocated == Information.zero()
+    end
+  end
+
+  property "the running total is the sum of bumped specs (hence order-independent)" do
+    check all(specs <- list_of(spec(), max_length: 20)) do
+      state = Enum.reduce(specs, State.zero(), fn s, acc -> State.bump(acc, s) end)
+
+      total_mem = specs |> Enum.map(&Information.as_bytes(&1.mem)) |> Enum.sum()
+      total_disk = specs |> Enum.map(&Information.as_bytes(&1.disk)) |> Enum.sum()
+
+      assert Information.as_bytes(state.mem_allocated) == total_mem
+      assert Information.as_bytes(state.disk_allocated) == total_disk
+    end
+  end
+
+  property "untrack returns exactly the spec track stored, leaving the rest unchanged" do
+    check all(s <- spec()) do
+      base = State.zero()
+      ref = make_ref()
+      tracked = State.track(base, ref, s)
+      assert {^s, rest} = State.untrack(tracked, ref)
+      assert rest.reservations == base.reservations
+    end
+  end
+
+  property "untrack of a ref that was never tracked yields nil and an unchanged state" do
+    check all(s <- spec()) do
+      ref = make_ref()
+      other = make_ref()
+      state = State.track(State.zero(), ref, s)
+      assert {nil, ^state} = State.untrack(state, other)
+    end
+  end
+end
diff --git a/test/hyper/node/budget/node_state_properties_test.exs b/test/hyper/node/budget/node_state_properties_test.exs
new file mode 100644
index 0000000..daab200
--- /dev/null
+++ b/test/hyper/node/budget/node_state_properties_test.exs
@@ -0,0 +1,89 @@
+defmodule Hyper.Node.Budget.NodeStatePropertiesTest do
+  @moduledoc """
+  Monotonicity laws of the pure `NodeState.fits?/2` predicate, complementing the
+  exact-`<=`-boundary example tests. A spec strictly within every ceiling always
+  fits, exceeding free memory always fails, and a spec that fits a node still
+  fits a node with strictly more headroom.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+  use Unit.Operators
+
+  alias Hyper.Node.Budget.NodeState
+  alias Hyper.Vm.Instance.Spec
+  alias Unit.{Bandwidth, Information}
+
+  # A node, idle on every soft metric with `cpu_max_load` at 1.0, so the only
+  # binding limits are the generated hard headrooms and cpu capacity.
+  defp state do
+    gen all(
+          mem_gib <- integer(1..64),
+          disk_gib <- integer(1..1000),
+          cpu_cap <- integer(1..128)
+        ) do
+      %NodeState{
+        node: :n@h,
+        mem_free: Information.gib(mem_gib),
+        disk_free: Information.gib(disk_gib),
+        cpu_load: 0.0,
+        cpu_capacity: cpu_cap,
+        cpu_max_load: 1.0,
+        disk_bw_load: Bandwidth.zero(),
+        disk_bw_ceiling: Bandwidth.gibps(10),
+        net_bw_load: Bandwidth.zero(),
+        net_bw_ceiling: Bandwidth.gibps(10),
+        layers: []
+      }
+    end
+  end
+
+  # A spec whose demand sits within every ceiling of `st`.
+  defp fitting_spec(st) do
+    gen all(
+          mem_gib <- integer(0..Information.as_gib(st.mem_free)),
+          disk_gib <- integer(0..Information.as_gib(st.disk_free)),
+          vcpus <- integer(0..st.cpu_capacity)
+        ) do
+      %Spec{
+        vcpus: vcpus,
+        mem: Information.gib(mem_gib),
+        disk: Information.gib(disk_gib),
+        disk_bw: Bandwidth.zero(),
+        net_bw: Bandwidth.zero()
+      }
+    end
+  end
+
+  property "a spec within every ceiling always fits" do
+    check all(st <- state(), spec <- fitting_spec(st)) do
+      assert NodeState.fits?(st, spec)
+    end
+  end
+
+  property "exceeding free memory always fails" do
+    check all(st <- state(), over <- integer(1..1000)) do
+      spec = %Spec{
+        vcpus: 0,
+        mem: st.mem_free + Information.gib(over),
+        disk: Information.zero(),
+        disk_bw: Bandwidth.zero(),
+        net_bw: Bandwidth.zero()
+      }
+
+      refute NodeState.fits?(st, spec)
+    end
+  end
+
+  property "a fitting spec still fits when the node gains headroom" do
+    check all(st <- state(), spec <- fitting_spec(st), extra <- integer(0..100)) do
+      roomier = %{
+        st
+        | mem_free: st.mem_free + Information.gib(extra),
+          disk_free: st.disk_free + Information.gib(extra)
+      }
+
+      # Precondition the law on the spec actually fitting `st`.
+      if NodeState.fits?(st, spec), do: assert(NodeState.fits?(roomier, spec))
+    end
+  end
+end
diff --git a/test/hyper/node/budget/node_state_test.exs b/test/hyper/node/budget/node_state_test.exs
new file mode 100644
index 0000000..8798a96
--- /dev/null
+++ b/test/hyper/node/budget/node_state_test.exs
@@ -0,0 +1,81 @@
+defmodule Hyper.Node.Budget.NodeStateTest do
+  use ExUnit.Case, async: true
+
+  alias Hyper.Node.Budget.NodeState
+  alias Hyper.Vm.Instance.Spec
+  alias Unit.{Bandwidth, Information}
+
+  # A node with generous headroom, idle on every metric. Override per case.
+  defp roomy_state(overrides \\ %{}) do
+    struct!(
+      %NodeState{
+        node: :node@host,
+        mem_free: Information.gib(8),
+        disk_free: Information.gib(100),
+        cpu_load: 0.0,
+        cpu_capacity: 8,
+        cpu_max_load: 0.8,
+        disk_bw_load: Bandwidth.zero(),
+        disk_bw_ceiling: Bandwidth.gibps(1),
+        net_bw_load: Bandwidth.zero(),
+        net_bw_ceiling: Bandwidth.gibps(1),
+        layers: []
+      },
+      overrides
+    )
+  end
+
+  defp spec(overrides \\ %{}) do
+    struct!(
+      %Spec{
+        vcpus: 1,
+        mem: Information.gib(1),
+        disk: Information.gib(10),
+        disk_bw: Bandwidth.mibps(10),
+        net_bw: Bandwidth.mibps(10)
+      },
+      overrides
+    )
+  end
+
+  test "a spec that fits every metric is admitted" do
+    assert NodeState.fits?(roomy_state(), spec())
+  end
+
+  test "memory demand over free headroom is rejected" do
+    state = roomy_state(%{mem_free: Information.gib(1)})
+    refute NodeState.fits?(state, spec(%{mem: Information.gib(2)}))
+  end
+
+  test "memory demand exactly at free headroom still fits (<= boundary)" do
+    state = roomy_state(%{mem_free: Information.gib(2)})
+    assert NodeState.fits?(state, spec(%{mem: Information.gib(2)}))
+  end
+
+  test "disk demand over free headroom is rejected" do
+    state = roomy_state(%{disk_free: Information.gib(5)})
+    refute NodeState.fits?(state, spec(%{disk: Information.gib(6)}))
+  end
+
+  test "cpu demand that crosses the load ceiling is rejected" do
+    # load 0.5 + 3 vcpus / 8 cores = 0.875 > cpu_max_load 0.8
+    state = roomy_state(%{cpu_load: 0.5})
+    refute NodeState.fits?(state, spec(%{vcpus: 3}))
+  end
+
+  test "cpu demand exactly at the load ceiling still fits" do
+    # load 0.0 + 8 vcpus / 8 cores = 1.0 <= cpu_max_load 1.0
+    state = roomy_state(%{cpu_max_load: 1.0})
+    assert NodeState.fits?(state, spec(%{vcpus: 8}))
+  end
+
+  test "disk bandwidth over its ceiling is rejected" do
+    state = roomy_state(%{disk_bw_ceiling: Bandwidth.mibps(5)})
+    refute NodeState.fits?(state, spec(%{disk_bw: Bandwidth.mibps(6)}))
+  end
+
+  test "net bandwidth over its ceiling is rejected" do
+    state = roomy_state(%{net_bw_ceiling: Bandwidth.mibps(5)})
+    refute NodeState.fits?(state, spec(%{net_bw: Bandwidth.mibps(6)}))
+  end
+end
diff --git a/test/sys/linux/cgroup_properties_test.exs b/test/sys/linux/cgroup_properties_test.exs
new file mode 100644
index 0000000..ee769b6
--- /dev/null
+++ b/test/sys/linux/cgroup_properties_test.exs
@@ -0,0 +1,64 @@
+defmodule Sys.Linux.CgroupPropertiesTest do
+  @moduledoc """
+  `Cgroup.versions_from_mounts/1` reduces a mount list to the set of cgroup
+  versions present, keyed by `fs_type`. The result is exactly the cgroup
+  fs_types that appear: it ignores every other filesystem, is insensitive to
+  order and duplication, and never contains a version that was not mounted.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Cgroup
+  alias Sys.Linux.Fstab.Spec
+
+  @cgroup_fs ~w(cgroup cgroup2)
+  # Filesystem types that must never contribute to the result.
+  @other_fs ~w(ext4 xfs btrfs proc sysfs tmpfs overlay)
+
+  defp mount(fs_type) do
+    %Spec{device: "none", mount_point: "/x", fs_type: fs_type, mount_opts: "rw"}
+  end
+
+  defp fs_type, do: member_of(@cgroup_fs ++ @other_fs)
+
+  property "the result is exactly the set of cgroup fs_types present" do
+    check all(types <- list_of(fs_type(), max_length: 20)) do
+      mounts = Enum.map(types, &mount/1)
+
+      expected =
+        types
+        |> Enum.filter(&(&1 in @cgroup_fs))
+        |> Enum.map(&String.to_existing_atom/1)
+        |> MapSet.new()
+
+      assert Cgroup.versions_from_mounts(mounts) == expected
+    end
+  end
+
+  property "non-cgroup mounts never change the result" do
+    check all(
+            types <- list_of(member_of(@cgroup_fs), max_length: 10),
+            noise <- list_of(member_of(@other_fs), max_length: 10)
+          ) do
+      base = Enum.map(types, &mount/1)
+      with_noise = Enum.map(types ++ noise, &mount/1)
+      assert Cgroup.versions_from_mounts(base) == Cgroup.versions_from_mounts(with_noise)
+    end
+  end
+
+  property "order and duplication do not affect the result" do
+    check all(types <- list_of(fs_type(), max_length: 20)) do
+      mounts = Enum.map(types, &mount/1)
+      result = Cgroup.versions_from_mounts(mounts)
+      assert Cgroup.versions_from_mounts(Enum.reverse(mounts)) == result
+      assert Cgroup.versions_from_mounts(mounts ++ mounts) == result
+    end
+  end
+
+  property "the result is always a subset of {:cgroup, :cgroup2}" do
+    check all(types <- list_of(fs_type(), max_length: 20)) do
+      result = Cgroup.versions_from_mounts(Enum.map(types, &mount/1))
+      assert MapSet.subset?(result, MapSet.new([:cgroup, :cgroup2]))
+    end
+  end
+end
diff --git a/test/sys/linux/nss_properties_test.exs b/test/sys/linux/nss_properties_test.exs
new file mode 100644
index 0000000..27dc236
--- /dev/null
+++ b/test/sys/linux/nss_properties_test.exs
@@ -0,0 +1,115 @@
+defmodule Sys.Linux.NssPropertiesTest do
+  @moduledoc """
+  Round-trip and rejection laws of the pure `Nss.Passwd.from_output/1` and
+  `Nss.Group.from_output/1` parsers. A well-formed line reconstructs its fields
+  exactly; a line with the wrong field count or a non-integer id is rejected.
+  Mirrors `Sys.Linux.SubidPropertiesTest`.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Nss.{Group, Passwd}
+
+  # A field with neither colon (field separator) nor newline (line separator);
+  # `/` and `.` are allowed so home/shell look like real paths.
+  defp field, do: string([?a..?z, ?A..?Z, ?0..?9, ?_, ?/, ?., ?-], max_length: 12)
+
+  defp nonempty,
+    do: string([?a..?z, ?A..?Z, ?0..?9, ?_, ?/, ?., ?-], min_length: 1, max_length: 12)
+
+  defp id, do: integer(0..4_000_000_000)
+  # Letters only, so it can never be parsed as a bare integer (malformed id case).
+  defp alpha, do: string([?a..?z, ?A..?Z], min_length: 1, max_length: 8)
+
+  describe "Passwd.from_output/1" do
+    property "round-trips a well-formed passwd line into its seven fields" do
+      check all(
+              name <- nonempty(),
+              pw <- field(),
+              uid <- id(),
+              gid <- id(),
+              gecos <- field(),
+              home <- field(),
+              shell <- field()
+            ) do
+        line = Enum.join([name, pw, uid, gid, gecos, home, shell], ":")
+        assert {:ok, [e]} = Passwd.from_output(line <> "\n")
+        assert e.name == name
+        assert e.password == pw
+        assert e.uid == uid
+        assert e.gid == gid
+        assert e.gecos == gecos
+        assert e.home_dir == home
+        assert e.shell == shell
+      end
+    end
+
+    property "parses N well-formed lines into N entries" do
+      record =
+        gen all(name <- nonempty(), uid <- id(), gid <- id(), home <- field(), shell <- field()) do
+          Enum.join([name, "x", uid, gid, "", home, shell], ":")
+        end
+
+      check all(lines <- list_of(record, min_length: 1, max_length: 10)) do
+        assert {:ok, entries} = Passwd.from_output(Enum.join(lines, "\n") <> "\n")
+        assert length(entries) == length(lines)
+      end
+    end
+
+    property "a non-integer uid is rejected" do
+      check all(name <- nonempty(), junk <- alpha(), gid <- id()) do
+        line = Enum.join([name, "x", junk, gid, "", "/h", "/sh"], ":")
+        assert Passwd.from_output(line <> "\n") == {:error, :invalid_format}
+      end
+    end
+
+    property "a line without exactly seven colon-fields is rejected" do
+      check all(
+              fields <- list_of(nonempty(), min_length: 1, max_length: 10),
+              length(fields) != 7
+            ) do
+        assert Passwd.from_output(Enum.join(fields, ":") <> "\n") == {:error, :invalid_format}
+      end
+    end
+
+    test "empty output yields an empty list" do
+      assert Passwd.from_output("") == {:ok, []}
+    end
+  end
+
+  describe "Group.from_output/1" do
+    property "round-trips name/gid and splits the member list" do
+      check all(
+              name <- nonempty(),
+              pw <- field(),
+              gid <- id(),
+              members <- list_of(nonempty(), max_length: 6)
+            ) do
+        line = Enum.join([name, pw, gid, Enum.join(members, ",")], ":")
+        assert {:ok, [grp]} = Group.from_output(line <> "\n")
+        assert grp.name == name
+        assert grp.gid == gid
+        assert grp.members == members
+      end
+    end
+
+    property "a non-integer gid is rejected" do
+      check all(name <- nonempty(), junk <- alpha(), members <- field()) do
+        line = Enum.join([name, "x", junk, members], ":")
+        assert Group.from_output(line <> "\n") == {:error, :invalid_format}
+      end
+    end
+
+    property "fewer than four colon-fields is rejected" do
+      check all(fields <- list_of(nonempty(), min_length: 1, max_length: 3)) do
+        # `parse` splits with `parts: 4`; fewer than four fields can never match
+        # the four-element destructure.
+        assert Group.from_output(Enum.join(fields, ":") <> "\n") == {:error, :invalid_format}
+      end
+    end
+
+    test "empty output yields an empty list" do
+      assert Group.from_output("") == {:ok, []}
+    end
+  end
+end
diff --git a/test/unit/scaling_properties_test.exs b/test/unit/scaling_properties_test.exs
new file mode 100644
index 0000000..bf39c83
--- /dev/null
+++ b/test/unit/scaling_properties_test.exs
@@ -0,0 +1,119 @@
+defmodule Unit.ScalingPropertiesTest do
+  @moduledoc """
+  Laws of the binary-prefix constructors and the read-back accessors, which
+  `Unit.QuantityPropertiesTest` does not touch (it only exercises the canonical
+  bytes / bytes-per-sec / nanosecond constructors through the `Quantity`
+  protocol). Every prefix constructor is exact multiplication by a power of 1024
+  (1000 for time), and every `as_*` accessor is truncating integer division that
+  cancels its own constructor exactly.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Unit.{Bandwidth, Information, Time}
+
+  @kib 1024
+  @mib 1024 * @kib
+  @gib 1024 * @mib
+  @tib 1024 * @gib
+
+  @us 1_000
+  @ms 1_000_000
+  @s 1_000_000_000
+
+  # Bounded for legible shrink output; Elixir integers are bignums, so the bound
+  # is for readability, not to dodge overflow. Signed, to exercise the
+  # toward-zero behaviour of the truncating accessors.
+  defp scalar, do: integer(-1_000_000..1_000_000)
+  defp nonneg, do: integer(0..1_000_000)
+
+  # --- Information -----------------------------------------------------------
+
+  property "Information prefix constructors scale by powers of 1024" do
+    check all(v <- scalar()) do
+      assert Information.as_bytes(Information.bytes(v)) == v
+      assert Information.as_bytes(Information.kib(v)) == v * @kib
+      assert Information.as_bytes(Information.mib(v)) == v * @mib
+      assert Information.as_bytes(Information.gib(v)) == v * @gib
+      assert Information.as_bytes(Information.tib(v)) == v * @tib
+    end
+  end
+
+  property "each Information prefix is 1024x the one below it" do
+    check all(v <- scalar()) do
+      assert Information.kib(v * 1024) == Information.mib(v)
+      assert Information.mib(v * 1024) == Information.gib(v)
+      assert Information.gib(v * 1024) == Information.tib(v)
+    end
+  end
+
+  property "as_mib / as_gib cancel their own constructor exactly" do
+    check all(v <- scalar()) do
+      assert Information.as_mib(Information.mib(v)) == v
+      assert Information.as_gib(Information.gib(v)) == v
+    end
+  end
+
+  property "as_mib is truncating division: exact quotient with a bounded remainder" do
+    check all(b <- nonneg()) do
+      q = Information.as_mib(Information.bytes(b))
+      assert q == div(b, @mib)
+      assert q * @mib <= b and b < (q + 1) * @mib
+    end
+  end
+
+  # --- Bandwidth -------------------------------------------------------------
+
+  property "Bandwidth prefix constructors scale by powers of 1024" do
+    check all(v <- scalar()) do
+      assert Bandwidth.as_bytes_per_sec(Bandwidth.bps(v)) == v
+      assert Bandwidth.as_bytes_per_sec(Bandwidth.kibps(v)) == v * @kib
+      assert Bandwidth.as_bytes_per_sec(Bandwidth.mibps(v)) == v * @mib
+      assert Bandwidth.as_bytes_per_sec(Bandwidth.gibps(v)) == v * @gib
+      assert Bandwidth.as_bytes_per_sec(Bandwidth.tibps(v)) == v * @tib
+    end
+  end
+
+  property "each Bandwidth prefix is 1024x the one below it" do
+    check all(v <- scalar()) do
+      assert Bandwidth.kibps(v * 1024) == Bandwidth.mibps(v)
+      assert Bandwidth.mibps(v * 1024) == Bandwidth.gibps(v)
+      assert Bandwidth.gibps(v * 1024) == Bandwidth.tibps(v)
+    end
+  end
+
+  # --- Time ------------------------------------------------------------------
+
+  property "Time constructors scale to nanoseconds by powers of 1000" do
+    check all(v <- scalar()) do
+      assert Time.as_ns(Time.ns(v)) == v
+      assert Time.as_ns(Time.us(v)) == v * @us
+      assert Time.as_ns(Time.ms(v)) == v * @ms
+      assert Time.as_ns(Time.s(v)) == v * @s
+    end
+  end
+
+  property "each Time unit is 1000x the one below it" do
+    check all(v <- scalar()) do
+      assert Time.ns(v * 1000) == Time.us(v)
+      assert Time.us(v * 1000) == Time.ms(v)
+      assert Time.ms(v * 1000) == Time.s(v)
+    end
+  end
+
+  property "as_us / as_ms / as_s cancel their own constructor exactly" do
+    check all(v <- scalar()) do
+      assert Time.as_us(Time.us(v)) == v
+      assert Time.as_ms(Time.ms(v)) == v
+      assert Time.as_s(Time.s(v)) == v
+    end
+  end
+
+  property "as_us is truncating division: exact quotient with a bounded remainder" do
+    check all(ns <- nonneg()) do
+      q = Time.as_us(Time.ns(ns))
+      assert q == div(ns, @us)
+      assert q * @us <= ns and ns < (q + 1) * @us
+    end
+  end
+end