1	# bend-osdev-acpi, aml_field.bend: reading and writing field units (ACPI
2	# 6.5, chapter 19, Field; and section 5.5.2.4, Access to Operation
3	# Regions) and buffer fields (chapter 19, CreateBitField and the others).
4	#
5	# A field unit is bits [bit_off, bit_off + bits) of its region, read and
6	# written in units of its access width (FieldFlags bits 0-3: ByteAcc 1
7	# byte, WordAcc 2, DWordAcc 4, QWordAcc 8; AnyAcc and BufferAcc are read a
8	# byte at a time). A unit the field covers only in part is written by its
9	# update rule (bits 5-6: Preserve reads the unit first, WriteAsOnes and
10	# WriteAsZeros fill the other bits). A unit outside the region is refused
11	# (AcpiAmlRange). Fields up to 64 bits are Integers; wider fields, and wider
12	# buffer fields, are Buffers.
13	import Base
14	import bend-osdev-word64@0.1.1.1/word64.bend as W
15	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
16	import ./error.bend as E
17	import ./aml_host.bend as Hs
18	
19	# a field unit, with its region resolved
20	type AmlFieldDesc is Data:
21	  AmlFieldDesc{space: U32, base: W.W64, rlen: W.W64, bit_off: Nat, bits: Nat, flags: U32}
22	
23	def fld.width.go(a: Nat) -> Nat:
24	  match a:
25	    case 2n:
26	      2n
27	    case 3n:
28	      4n
29	    case 4n:
30	      8n
31	    case _:
32	      1n
33	
34	# the access width in bytes, from the field flags
35	def AmlField.unit(+flags: U32) -> Nat:
36	  fld.width.go(U32.to_nat(U32.and(flags, 15)))
37	
38	def AmlField.update_rule(+flags: U32) -> U32:
39	  U32.and(U32.shrn(flags, 5n), 3)
40	
41	def fld.mask.pick(all: Bool, +n: Nat) -> W.W64:
42	  match all:
43	    case True{}:
44	      W.W64.max()
45	    case False{}:
46	      W.W64.sub(W.W64.shl(W.W64.one(), n), W.W64.one())
47	
48	# n low bits set
49	def fld.mask(+n: Nat) -> W.W64:
50	  fld.mask.pick(Nat.is_le(64n, n), n)
51	
52	def fld.min(+a: Nat, +b: Nat) -> Nat:
53	  Nat.min(a, b)
54	
55	def fld.max(+a: Nat, +b: Nat) -> Nat:
56	  Nat.max(a, b)
57	
58	# one unit: its address, and the part of the field it holds
59	type AmlUnit is Data:
60	  # addr: the unit's address; s: the field's first bit in it; n: how many
61	  # field bits it holds; d: where they go in the field's value
62	  AmlUnit{addr: W.W64, s: Nat, n: Nat, d: Nat, fits: Bool}
63	
64	def fld.unit(+f: AmlFieldDesc, +k: Nat) -> AmlUnit:
65	  match f:
66	    case AmlFieldDesc{sp, +base, +rlen, +off, +bits, +flags}:
67	      +w = AmlField.unit(flags)
68	      +ubits = Nat.mul(w, 8n)
69	      +start = Nat.mul(k, ubits)
70	      +lo = fld.max(off, start)
71	      +hi = fld.min(Nat.add(off, bits), Nat.add(start, ubits))
72	      AmlUnit{W.W64.add(base, W.W64.from_nat(Nat.mul(k, w))), Nat.sub(lo, start), Nat.sub(hi, lo), Nat.sub(lo, off), W.W64.is_le(W.W64.from_nat(Nat.mul(Nat.add(k, 1n), w)), rlen)}
73	
74	def fld.first(+f: AmlFieldDesc) -> Nat:
75	  match f:
76	    case AmlFieldDesc{sp, base, rlen, +off, bits, +flags}:
77	      Nat.div(off, Nat.mul(AmlField.unit(flags), 8n))
78	
79	def fld.count(+f: AmlFieldDesc) -> Nat:
80	  match f:
81	    case AmlFieldDesc{sp, base, rlen, +off, +bits, +flags}:
82	      +ub = Nat.mul(AmlField.unit(flags), 8n)
83	      Nat.sub(Nat.add(Nat.div(Nat.sub(Nat.add(off, bits), 1n), ub), 1n), Nat.div(off, ub))
84	
85	def fld.space(f: AmlFieldDesc) -> U32:
86	  match f:
87	    case AmlFieldDesc{sp, base, rlen, off, bits, flags}:
88	      sp
89	
90	def fld.flags(f: AmlFieldDesc) -> U32:
91	  match f:
92	    case AmlFieldDesc{sp, base, rlen, off, bits, flags}:
93	      flags
94	
95	def fld.bits(f: AmlFieldDesc) -> Nat:
96	  match f:
97	    case AmlFieldDesc{sp, base, rlen, off, bits, flags}:
98	      bits
99	
100	def fld.access(+f: AmlFieldDesc, +addr: W.W64) -> Hs.AmlAccess:
101	  Hs.AmlAccess{fld.space(f), addr, Nat.mul(AmlField.unit(fld.flags(f)), 8n)}
102	
103	def AmlUnit.addr(u: AmlUnit) -> W.W64:
104	  match u:
105	    case AmlUnit{a, s, n, d, ok}:
106	      a
107	
108	def AmlUnit.fits(u: AmlUnit) -> Bool:
109	  match u:
110	    case AmlUnit{a, s, n, d, ok}:
111	      ok
112	
113	# the unit's own bits that belong to the field
114	def AmlUnit.hole(u: AmlUnit) -> W.W64:
115	  match u:
116	    case AmlUnit{a, +s, +n, d, ok}:
117	      W.W64.shl(fld.mask(n), s)
118	
119	# the field bits a unit holds, from the unit's value v, in place in the
120	# field's value
121	def AmlUnit.take(u: AmlUnit, +v: W.W64) -> W.W64:
122	  match u:
123	    case AmlUnit{a, +s, +n, +d, ok}:
124	      W.W64.shl(W.W64.and(W.W64.shr(v, s), fld.mask(n)), d)
125	
126	# the unit's share of the field's value x, in place in the unit
127	def AmlUnit.put(u: AmlUnit, +x: W.W64) -> W.W64:
128	  match u:
129	    case AmlUnit{a, +s, +n, +d, ok}:
130	      W.W64.shl(W.W64.and(W.W64.shr(x, d), fld.mask(n)), s)
131	
132	# the unit is the field's alone (no other bits to keep)
133	def AmlUnit.whole(u: AmlUnit, +w: Nat) -> Bool:
134	  match u:
135	    case AmlUnit{a, s, +n, d, ok}:
136	      Nat.is_eq(n, Nat.mul(w, 8n))
137	
138	def fld.rd.unit(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, fits: Bool, h: H, +a: Hs.AmlAccess) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
139	  match fits:
140	    case True{}:
141	      io(h, Hs.AmlHRead{a})
142	    case False{}:
143	      Fail{E.AcpiAmlRange{}}
144	
145	def fld.rd.next(-H: Data, +u: AmlUnit, +acc: W.W64, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
146	  match r:
147	    case Fail{e}:
148	      Fail{e}
149	    case Done{Hs.AmlHostAns{h2, +v}}:
150	      Done{Hs.AmlHostAns{h2, W.W64.or(acc, AmlUnit.take(u, v))}}
151	
152	# units k .. k + n - 1, read and joined into the value in r
153	def fld.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +f: AmlFieldDesc, +k: Nat, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
154	  match n:
155	    case 0n:
156	      r
157	    case 1n+p:
158	      match r:
159	        case Fail{e}:
160	          Fail{e}
161	        case Done{Hs.AmlHostAns{h, acc}}:
162	          +u = fld.unit(f, k)
163	          fld.rd(~H, ~io, p, f, 1n+k, fld.rd.next(H, u, acc, fld.rd.unit(~H, ~io, AmlUnit.fits(u), h, fld.access(f, AmlUnit.addr(u)))))
164	
165	# the value of a field unit of at most 64 bits
166	def AmlField.read_int(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +f: AmlFieldDesc, h: H) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
167	  fld.rd(~H, ~io, fld.count(f), f, fld.first(f), Done{Hs.AmlHostAns{h, W.W64.zero()}})
168	
169	# Writing
170	
171	# the unit's bits that are not the field's, by the update rule: read
172	# (Preserve), all ones, all zeros
173	def fld.keep(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, whole: Bool, rule: Nat, h: H, +a: Hs.AmlAccess) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
174	  match whole:
175	    case True{}:
176	      Done{Hs.AmlHostAns{h, W.W64.zero()}}
177	    case False{}:
178	      match rule:
179	        case 1n:
180	          Done{Hs.AmlHostAns{h, W.W64.max()}}
181	        case 2n:
182	          Done{Hs.AmlHostAns{h, W.W64.zero()}}
183	        case _:
184	          io(h, Hs.AmlHRead{a})
185	
186	def fld.wr.unit(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +u: AmlUnit, +a: Hs.AmlAccess, +x: W.W64) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
187	  match r:
188	    case Fail{e}:
189	      Fail{e}
190	    case Done{Hs.AmlHostAns{h, +old}}:
191	      io(h, Hs.AmlHWrite{a, W.W64.or(W.W64.and(old, W.W64.not(AmlUnit.hole(u))), AmlUnit.put(u, x))})
192	
193	def fld.wr.fits(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, fits: Bool, h: H, +f: AmlFieldDesc, +u: AmlUnit, +x: W.W64) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
194	  match fits:
195	    case False{}:
196	      Fail{E.AcpiAmlRange{}}
197	    case True{}:
198	      +a = fld.access(f, AmlUnit.addr(u))
199	      +flags = fld.flags(f)
200	      fld.wr.unit(~H, ~io, fld.keep(~H, ~io, AmlUnit.whole(u, AmlField.unit(flags)), U32.to_nat(AmlField.update_rule(flags)), h, a), u, a, x)
201	
202	# units k .. k + n - 1 written with their share of x
203	def fld.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +f: AmlFieldDesc, +k: Nat, +x: W.W64, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
204	  match n:
205	    case 0n:
206	      r
207	    case 1n+p:
208	      match r:
209	        case Fail{e}:
210	          Fail{e}
211	        case Done{Hs.AmlHostAns{h, v}}:
212	          +u = fld.unit(f, k)
213	          fld.wr(~H, ~io, p, f, 1n+k, x, fld.wr.fits(~H, ~io, AmlUnit.fits(u), h, f, u, x))
214	
215	# a field unit of at most 64 bits set to x (its low bits)
216	def AmlField.write_int(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +f: AmlFieldDesc, h: H, +x: W.W64) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
217	  fld.wr(~H, ~io, fld.count(f), f, fld.first(f), x, Done{Hs.AmlHostAns{h, W.W64.zero()}})
218	
219	# Wider fields: a byte at a time, as a Buffer
220	
221	def fld.byte(+f: AmlFieldDesc, +j: Nat) -> AmlFieldDesc:
222	  match f:
223	    case AmlFieldDesc{sp, base, rlen, +off, +bits, flags}:
224	      AmlFieldDesc{sp, base, rlen, Nat.add(off, Nat.mul(j, 8n)), Nat.min(8n, Nat.sub(bits, Nat.mul(j, 8n))), flags}
225	
226	type AmlFieldBuf<-H: Data> is Data:
227	  AmlFieldBuf{host: H, value: B.Octets}
228	
229	def fld.rev(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
230	  match xs:
231	    case Nil{}:
232	      acc
233	    case Con{x, t}:
234	      fld.rev(t, Con{x, acc})
235	
236	# bytes j .. j + n of the field; r: the read of byte j - 1
237	def fld.bytes.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +f: AmlFieldDesc, +j: Nat, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, acc: List<&2, U32>) -> Result<&2, &2, E.AcpiError, AmlFieldBuf<H>>:
238	  match n:
239	    case 0n:
240	      match r:
241	        case Fail{e}:
242	          Fail{e}
243	        case Done{Hs.AmlHostAns{h, v}}:
244	          Done{AmlFieldBuf{h, B.Octets.of_list(fld.rev(Con{W.W64.lo(v), acc}, Nil{}))}}
245	    case 1n+p:
246	      match r:
247	        case Fail{e}:
248	          Fail{e}
249	        case Done{Hs.AmlHostAns{h, v}}:
250	          fld.bytes.rd(~H, ~io, p, f, 1n+j, AmlField.read_int(~H, ~io, fld.byte(f, j), h), Con{W.W64.lo(v), acc})
251	
252	def fld.nbytes(+f: AmlFieldDesc) -> Nat:
253	  Nat.div(Nat.add(fld.bits(f), 7n), 8n)
254	
255	# a field unit of any width, as a Buffer of its bytes
256	def AmlField.read_buf(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +f: AmlFieldDesc, h: H) -> Result<&2, &2, E.AcpiError, AmlFieldBuf<H>>:
257	  fld.bytes.rd(~H, ~io, Nat.sub(fld.nbytes(f), 1n), f, 1n, AmlField.read_int(~H, ~io, fld.byte(f, 0n), h), Nil{})
258	
259	def fld.bytes.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +f: AmlFieldDesc, +j: Nat, +o: B.Octets, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
260	  match n:
261	    case 0n:
262	      r
263	    case 1n+p:
264	      match r:
265	        case Fail{e}:
266	          Fail{e}
267	        case Done{Hs.AmlHostAns{h, v}}:
268	          fld.bytes.wr(~H, ~io, p, f, 1n+j, o, AmlField.write_int(~H, ~io, fld.byte(f, j), h, W.W64.from_u32(Maybe.default(&2, U32, B.Octets.at(o, j), 0))))
269	
270	# a field unit of any width set from the bytes of o (zeros past its end)
271	def AmlField.write_buf(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +f: AmlFieldDesc, h: H, +o: B.Octets) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
272	  fld.bytes.wr(~H, ~io, fld.nbytes(f), f, 0n, o, Done{Hs.AmlHostAns{h, W.W64.zero()}})
273	
274	# Buffer fields: bits of a buffer
275	
276	def fld.bit(+o: B.Octets, +i: Nat) -> W.W64:
277	  W.W64.and(W.W64.shr(W.W64.from_u32(Maybe.default(&2, U32, B.Octets.at(o, Nat.div(i, 8n)), 0)), Nat.mod(i, 8n)), W.W64.one())
278	
279	def fld.bits.get(n: Nat, +o: B.Octets, +i: Nat, +k: Nat, acc: W.W64) -> W.W64:
280	  match n:
281	    case 0n:
282	      acc
283	    case 1n+p:
284	      fld.bits.get(p, o, Nat.add(i, 1n), Nat.add(k, 1n), W.W64.or(acc, W.W64.shl(fld.bit(o, i), k)))
285	
286	def fld.bits.pick(ok: Bool, r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, W.W64>:
287	  match ok:
288	    case True{}:
289	      r
290	    case False{}:
291	      Fail{E.AcpiAmlRange{}}
292	
293	# bits [off, off + n) of o (n at most 64), as an integer; AcpiAmlRange if
294	# they run past o
295	def AmlBits.get(+o: B.Octets, +off: Nat, +n: Nat) -> Result<&2, &2, E.AcpiError, W.W64>:
296	  fld.bits.pick(Nat.is_le(Nat.add(off, n), Nat.mul(B.Octets.len(o), 8n)), Done{fld.bits.get(n, o, off, 0n, W.W64.zero())})
297	
298	def fld.bits.one(on: Bool, +old: U32, +bit: U32) -> U32:
299	  match on:
300	    case True{}:
301	      U32.or(old, bit)
302	    case False{}:
303	      U32.and(old, U32.not(bit))
304	
305	def fld.bits.set(n: Nat, xs: List<&2, U32>, +i: Nat, +k: Nat, +v: W.W64) -> List<&2, U32>:
306	  match n:
307	    case 0n:
308	      xs
309	    case 1n+p:
310	      +ys = xs
311	      +j = Nat.div(i, 8n)
312	      +bit = U32.shln(1, Nat.mod(i, 8n))
313	      +old = Maybe.default(&2, U32, B.at(ys, j), 0)
314	      +on = W.W64.is_eq(W.W64.and(W.W64.shr(v, k), W.W64.one()), W.W64.one())
315	      fld.bits.set(p, List.set(&2, U32, ys, j, fld.bits.one(on, old, bit)), Nat.add(i, 1n), Nat.add(k, 1n), v)
316	
317	def fld.bufs.pick(ok: Bool, +o: B.Octets, +off: Nat, n: Nat, +v: W.W64) -> Result<&2, &2, E.AcpiError, B.Octets>:
318	  match ok:
319	    case True{}:
320	      Done{B.Octets.of_list(fld.bits.set(n, B.Octets.to_list(o), off, 0n, v))}
321	    case False{}:
322	      Fail{E.AcpiAmlRange{}}
323	
324	# o with bits [off, off + n) set from the low n bits of v (n at most 64)
325	def AmlBits.set(+o: B.Octets, +off: Nat, +n: Nat, +v: W.W64) -> Result<&2, &2, E.AcpiError, B.Octets>:
326	  fld.bufs.pick(Nat.is_le(Nat.add(off, n), Nat.mul(B.Octets.len(o), 8n)), o, off, n, v)
327	
328	def fld.bitsb.get(n: Nat, +o: B.Octets, +i: Nat, acc: List<&2, U32>) -> List<&2, U32>:
329	  match n:
330	    case 0n:
331	      fld.rev(acc, Nil{})
332	    case 1n+p:
333	      fld.bitsb.get(p, o, Nat.add(i, 8n), Con{W.W64.lo(fld.bits.get(8n, o, i, 0n, W.W64.zero())), acc})
334	
335	# bits [off, off + n) of o as a Buffer of ceil(n / 8) bytes (the last byte's
336	# high bits are the bits that follow the field; callers mask them)
337	def AmlBits.get_buf(+o: B.Octets, +off: Nat, +n: Nat) -> B.Octets:
338	  B.Octets.of_list(fld.bitsb.get(Nat.div(Nat.add(n, 7n), 8n), o, off, Nil{}))
339	
340	# IndexField (chapter 19): the field's bits are reached a unit at a time by
341	# writing the unit's byte offset to the index field, then reading or
342	# writing the data field. f: the field (base 0; rlen its reach). A write
343	# puts the field's share of each unit in the data field; the other bits of
344	# the unit are written as zeros (the update rule is not applied through
345	# the data register).
346	
347	def fld.ix.rd.k(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +dat: AmlFieldDesc, +u: AmlUnit, +acc: W.W64, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
348	  match r:
349	    case Fail{e}:
350	      Fail{e}
351	    case Done{Hs.AmlHostAns{h, v}}:
352	      fld.rd.next(H, u, acc, AmlField.read_int(~H, ~io, dat, h))
353	
354	def fld.ix.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +idx: AmlFieldDesc, +dat: AmlFieldDesc, +f: AmlFieldDesc, +k: Nat, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
355	  match n:
356	    case 0n:
357	      r
358	    case 1n+p:
359	      match r:
360	        case Fail{e}:
361	          Fail{e}
362	        case Done{Hs.AmlHostAns{h, acc}}:
363	          +u = fld.unit(f, k)
364	          fld.ix.rd(~H, ~io, p, idx, dat, f, 1n+k, fld.ix.rd.k(~H, ~io, dat, u, acc, AmlField.write_int(~H, ~io, idx, h, AmlUnit.addr(u))))
365	
366	def AmlField.read_indexed(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +idx: AmlFieldDesc, +dat: AmlFieldDesc, +f: AmlFieldDesc, h: H) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
367	  fld.ix.rd(~H, ~io, fld.count(f), idx, dat, f, fld.first(f), Done{Hs.AmlHostAns{h, W.W64.zero()}})
368	
369	def fld.ix.data(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +dat: AmlFieldDesc, +u: AmlUnit, +x: W.W64, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
370	  match r:
371	    case Fail{e}:
372	      Fail{e}
373	    case Done{Hs.AmlHostAns{h, v}}:
374	      AmlField.write_int(~H, ~io, dat, h, AmlUnit.put(u, x))
375	
376	def fld.ix.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +idx: AmlFieldDesc, +dat: AmlFieldDesc, +f: AmlFieldDesc, +k: Nat, +x: W.W64, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
377	  match n:
378	    case 0n:
379	      r
380	    case 1n+p:
381	      match r:
382	        case Fail{e}:
383	          Fail{e}
384	        case Done{Hs.AmlHostAns{h, v}}:
385	          +u = fld.unit(f, k)
386	          fld.ix.wr(~H, ~io, p, idx, dat, f, 1n+k, x, fld.ix.data(~H, ~io, dat, u, x, AmlField.write_int(~H, ~io, idx, h, AmlUnit.addr(u))))
387	
388	def AmlField.write_indexed(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +idx: AmlFieldDesc, +dat: AmlFieldDesc, +f: AmlFieldDesc, h: H, +x: W.W64) -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>:
389	  fld.ix.wr(~H, ~io, fld.count(f), idx, dat, f, fld.first(f), x, Done{Hs.AmlHostAns{h, W.W64.zero()}})