Transfer.Read_backEverything that reads device memory back into host storage, and NOTHING else. The module exists for its signature: copy_device_to_host is defined inside and deliberately absent from it, so the only code that can call the packed-buffer read directly is Read_back.read_back_to_host below.
That is the enforcement the previous version of this claim lacked. It said the call sites were "exhaustive BY CONSTRUCTION" while nothing constructed anything: there is no Transfer.mli, so every top-level binding in this file is exported and a fifth direct caller compiled fine. The claim happened to be true when it was written — it was re-audited, and it held — but an audited fact and an enforced one differ exactly where it matters, which is the next person to add a read-back path. Three of the four existing call sites were added or corrected in this branch precisely because they had bypassed the decision, so "someone adds a fifth and bypasses it too" is the observed failure mode, not a hypothetical one.
Now a bypass does not compile.