-Memory image of the kernel. These are the exact bytes loaded into
-memory to run the Pintos kernel. To simplify loading, it is always
-padded out with zero bytes up to an exact multiple of 4 kB in
-size.
+Memory image of the kernel, that is, the exact bytes loaded into
+memory to run the Pintos kernel. This is just @file{kernel.o} with
+debug information stripped out, which saves a lot of space, which in
+turn keeps the kernel from bumping up against a @w{512 kB} size limit
+imposed by the kernel loader's design.