1	# bend-osdev-acpi, checksum.bend: the ACPI checksum (ACPI 6.5, section
2	# 5.2.6, and 5.2.5.3 for the RSDP). A table is valid when all its bytes,
3	# its checksum byte included, sum to zero modulo 256.
4	import Base
5	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
6	
7	# the sum of the bytes, modulo 2^32 (tail-recursive)
8	def ck.sum.go(xs: List<&2, U32>, acc: U32) -> U32:
9	  match xs:
10	    case Nil{}:
11	      acc
12	    case Con{h, t}:
13	      ck.sum.go(t, U32.add(acc, U32.and(255, h)))
14	
15	# the sum of the bytes, modulo 256
16	def AcpiChecksum.sum(o: B.Octets) -> U32:
17	  U32.and(255, ck.sum.go(B.Octets.to_list(o), 0))
18	
19	# the bytes sum to zero modulo 256
20	def AcpiChecksum.ok(o: B.Octets) -> Bool:
21	  U32.is_eq(AcpiChecksum.sum(o), 0)
22	
23	# the byte that, put at offset i of o (whose byte there is ignored), makes
24	# o sum to zero modulo 256
25	def AcpiChecksum.byte_for(+i: Nat, +o: B.Octets) -> U32:
26	  +without = U32.and(255, U32.sub(AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))
27	  U32.and(255, U32.sub(256, without))
28	
29	def ck.fix.pick(fits: Bool, +i: Nat, +o: B.Octets) -> B.Octets:
30	  match fits:
31	    case True{}:
32	      B.Octets.concat([B.Octets.take(i, o), B.Octets.of_list([AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)])
33	    case False{}:
34	      o
35	
36	# o with its byte at offset i replaced by the checksum byte (o unchanged if
37	# it has no byte i)
38	def AcpiChecksum.fix(+i: Nat, +o: B.Octets) -> B.Octets:
39	  ck.fix.pick(Nat.is_lt(i, B.Octets.len(o)), i, o)