Many file formats use checksums of one sort or another. Therefore you may want to write such a checksum or verify a checksum in a constrained field. See Field Constraints.
Some formats use simple additive checksums. Another common checksum
is the Cyclic Redundancy Checksum (CRC). The standard function
crc32 calculates the 32 bit CRC defined by ISO-3309.
fun crc32 = (byte[] buf) uint<32>: { ... }
This function returns the 32 bit CRC for the data contained in the array buf.