checksum.bend

bend-osdev-acpi@0.1.0.0 · 39 lines · 0 definitions

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.
4import Base
5import bend-osdev-bytes@0.1.0.0/bytes.bend as B
6
7# the sum of the bytes, modulo 2^32 (tail-recursive)
8def 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
16def 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
20def 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
25def 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
29def 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)
38def AcpiChecksum.fix(+i: Nat, +o: B.Octets) -> B.Octets:
39  ck.fix.pick(Nat.is_lt(i, B.Octets.len(o)), i, o)