1	# bend-osdev-acpi, slit.bend: the System Locality Distance Information
2	# Table, "SLIT" (ACPI 6.5, section 5.2.17): after the header, the number of
3	# system localities N (8 bytes, offset 36), then the N x N matrix of
4	# relative distances, one byte each, row by row, from offset 44. Entry
5	# (i, i) is 10 (a locality's distance to itself); 0xFF means unreachable.
6	import Base
7	import bend-osdev-word64@0.1.0.0/word64.bend as W
8	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
9	import ./error.bend as E
10	import ./header.bend as H
11	import ./fields.bend as F
12	
13	type AcpiSlit is Data:
14	  AcpiSlit{header: H.AcpiHeader, count: Nat, matrix: B.Octets}
15	
16	def AcpiSlit.count(s: AcpiSlit) -> Nat:
17	  match s:
18	    case AcpiSlit{h, n, m}:
19	      n
20	
21	def slit.mk(ok: Bool, +h: H.AcpiHeader, +n: Nat, +body: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
22	  match ok:
23	    case False{}:
24	      Fail{E.AcpiBadSize{B.Octets.len(body)}}
25	    case True{}:
26	      Done{AcpiSlit{h, n, B.Octets.slice(8n, Nat.mul(n, n), body)}}
27	
28	def slit.body(ok: Bool, +h: H.AcpiHeader, +body: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
29	  match ok:
30	    case False{}:
31	      Fail{E.AcpiTooShort{44n, Nat.add(36n, B.Octets.len(body))}}
32	    case True{}:
33	      +big = F.AcpiF.u64(body, 0n)
34	      +n = U32.to_nat(W.W64.lo(big))
35	      slit.mk(Bool.and(U32.is_eq(W.W64.hi(big), 0), Bool.and(U32.is_lt(W.W64.lo(big), 65536), Nat.is_le(Nat.add(8n, Nat.mul(n, n)), B.Octets.len(body)))), h, n, body)
36	
37	# a checked table as an SLIT: the N x N matrix must fit in the body
38	# (AcpiBadSize otherwise; N is limited to 65535)
39	def AcpiSlit.of_sdt(t: H.AcpiSdt) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
40	  match t:
41	    case H.AcpiSdt{h, +body}:
42	      slit.body(Nat.is_le(8n, B.Octets.len(body)), h, body)
43	
44	def slit.parse(r: Result<&2, &2, E.AcpiError, H.AcpiSdt>) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
45	  match r:
46	    case Fail{e}:
47	      Fail{e}
48	    case Done{t}:
49	      AcpiSlit.of_sdt(t)
50	
51	def AcpiSlit.parse(+o: B.Octets) -> Result<&2, &2, E.AcpiError, AcpiSlit>:
52	  slit.parse(H.AcpiSdt.parse_sig(B.Octets.of_string("SLIT"), o))
53	
54	def slit.at(ok: Bool, +n: Nat, +m: B.Octets, +i: Nat, j: Nat) -> Maybe<&2, U32>:
55	  match ok:
56	    case False{}:
57	      None{}
58	    case True{}:
59	      B.Octets.at(m, Nat.add(Nat.mul(i, n), j))
60	
61	# the distance from locality i to locality j, if both are below N
62	def AcpiSlit.distance(s: AcpiSlit, +i: Nat, +j: Nat) -> Maybe<&2, U32>:
63	  match s:
64	    case AcpiSlit{h, +n, m}:
65	      slit.at(Bool.and(Nat.is_lt(i, n), Nat.is_lt(j, n)), n, m, i, j)
66	
67	# the table, from N and the matrix (fitted to N x N bytes)
68	def AcpiSlit.build(s: AcpiSlit) -> B.Octets:
69	  match s:
70	    case AcpiSlit{H.AcpiHeader{sg, l, r, c, o, t, orv, ci, cr}, +n, m}:
71	      H.AcpiSdt.build(H.AcpiHeader{B.Octets.of_string("SLIT"), l, r, c, o, t, orv, ci, cr}, B.Octets.append(B.Octets.le64(W.W64.from_nat(n)), F.AcpiF.fit(Nat.mul(n, n), m)))