lib/systems/parse: make isCompatible description clearer and more useful

Stating that CPUs and the isCompatible relation forms a category (or
preorder) is correct but overtly technical.  We can state it more
clearly for readers unfamiliar with mathematics while retaining some
keywords to be useful to technical readers.

1 files changed, 14 insertions, 9 deletions

diff --git a/lib/systems/parse.nix b/lib/systems/parse.nix
index a06ac0d11f7..accaeb652d0 100644
--- a/lib/systems/parse.nix
+++ b/lib/systems/parse.nix
@@ -121,15 +121,20 @@ rec {
     js       = { bits = 32; significantByte = littleEndian; family = "js"; };
   };
 
-  # Determine where two CPUs are compatible with each other. That is,
-  # can we run code built for system b on system a? For that to
-  # happen, then the set of all possible possible programs that system
-  # b accepts must be a subset of the set of all programs that system
-  # a accepts. This compatibility relation forms a category where each
-  # CPU is an object and each arrow from a to b represents
-  # compatibility. CPUs with multiple modes of Endianness are
-  # isomorphic while all CPUs are endomorphic because any program
-  # built for a CPU can run on that CPU.
+  # Determine when two CPUs are compatible with each other. That is,
+  # can code built for system B run on system A? For that to happen,
+  # the programs that system B accepts must be a subset of the
+  # programs that system A accepts.
+  #
+  # We have the following properties of the compatibility relation,
+  # which must be preserved when adding compatibility information for
+  # additional CPUs.
+  # - (reflexivity)
+  #   Every CPU is compatible with itself.
+  # - (transitivity)
+  #   If A is compatible with B and B is compatible with C then A is compatible with C.
+  # - (compatible under multiple endianness)
+  #   CPUs with multiple modes of endianness are pairwise compatible.
   isCompatible = a: b: with cpuTypes; lib.any lib.id [
     # x86
     (b == i386 && isCompatible a i486)