1	# bend-osdev-acpi, aml_interp.bend: the AML interpreter (ACPI 6.5, chapter
2	# 19, ASL Reference, for what each operator does; chapter 20, AML
3	# Specification, for its encoding).
4	#
5	# The interpreter is a small-step machine over the AML bytes: a cursor (the
6	# bytes left in the term list being run), a stack of frames (the operator
7	# whose operands are being read, the If, While, method call or package
8	# being run), and the world it changes (the method's Arg and Local values,
9	# the namespace, the operation-region host, notifications and the Debug
10	# log). Each step reads one opcode, or gives one value to the frame on top.
11	# AmlM.run stops after its step bound whatever the AML does (LAWS.bend:
12	# run_steps_bound), so a method that loops for ever ends with
13	# AcpiAmlStepLimit.
14	#
15	# Operation regions are reached through the host, a template argument
16	# (aml_host.bend): ~H: Data, ~io: H -> AmlHostOp -> Result<..., AmlHostAns<H>>.
17	#
18	# Method calls take their argument count from the namespace when they are
19	# reached, which is how AML is meant to be read (a MethodInvocation is a
20	# NameString followed by as many TermArgs as the method takes, 20.2.5.4).
21	# What is not supported is listed in README.md.
22	import Base
23	import bend-osdev-word64@0.1.1.1/word64.bend as W
24	import bend-osdev-bytes@0.1.1.1/bytes.bend as B
25	import ./error.bend as E
26	import ./aml_pkglength.bend as K
27	import ./aml_name.bend as N
28	import ./aml_value.bend as V
29	import ./aml_ns.bend as S
30	import ./aml_host.bend as Hs
31	import ./aml_field.bend as F
32	
33	# Options
34	
35	type AmlOptions is Data:
36	  # the strings \_OSI answers True for; \_OS and \_REV
37	  AmlOptions{osi: List<&2, String>, os: String, rev: U32}
38	
39	# \_OSI answers True for the Windows releases firmware tests for, as
40	# operating systems commonly do, and for "Module Device" and "Processor
41	# Device"; \_OS is "Microsoft Windows NT"; \_REV is 2 (ACPI 6.5, 5.7.2)
42	def AmlOptions.default() -> AmlOptions:
43	  AmlOptions{["Windows 2000", "Windows 2001", "Windows 2001 SP1", "Windows 2001 SP2", "Windows 2001.1", "Windows 2001.1 SP1", "Windows 2006", "Windows 2006 SP1", "Windows 2006.1", "Windows 2009", "Windows 2012", "Windows 2013", "Windows 2015", "Windows 2016", "Windows 2017", "Windows 2017.2", "Windows 2018", "Windows 2018.2", "Windows 2019", "Windows 2020", "Windows 2021", "Windows 2022", "Module Device", "Processor Device", "3.0 Thermal Model", "Extended Address Space Descriptor"], "Microsoft Windows NT", 2}
44	
45	# The machine
46	
47	# the bytes left in the current term list: the list from here, and how
48	# many of its bytes belong to the list
49	type AmlCur is Data:
50	  AmlCur{code: List<&2, U32>, lim: Nat}
51	
52	# what an operand must be
53	type AmlArgK is Data:
54	  # a TermArg: a value
55	  AmlKTerm{}
56	  # a Target or SuperName: a location
57	  AmlKTarget{}
58	  # a source (Index, SizeOf, ObjectType, CreateField): its location if it
59	  # has one, its value otherwise
60	  AmlKBase{}
61	  # CondRefOf's operand: a location, or nothing if the name is undefined
62	  AmlKCond{}
63	  # a package element: a value, or a name as a reference (not run)
64	  AmlKElem{}
65	  # immediate data
66	  AmlKByte{}
67	  AmlKWord{}
68	  AmlKDWord{}
69	  # a NameString, as the path it names from the current scope
70	  AmlKName{}
71	
72	type AmlOp is Data:
73	  # an operator, by opcode (an extended opcode 0x5B xx is 256 + xx)
74	  AmlOpCode{code: U32}
75	  AmlOpCall{path: String, nargs: Nat}
76	  AmlOpOsi{}
77	
78	type AmlCtx is Data:
79	  # the scope names resolve from; Arg0-6; Local0-7; the names this method
80	  # call created (removed when it returns)
81	  AmlCtx{scope: String, args: List<&2, V.AmlValue>, locals: List<&2, V.AmlValue>, temps: List<&2, String>}
82	
83	type AmlFrame is Data:
84	  AmlFArgs{op: AmlOp, got: List<&2, V.AmlValue>, todo: List<&2, AmlArgK>}
85	  # a nested term list (Scope, Device, Else, ...): where to resume, and the
86	  # scope to restore
87	  AmlFSeq{after: AmlCur, scope: String}
88	  # an If whose predicate is being read
89	  AmlFIf{after: AmlCur}
90	  # an If whose body is running
91	  AmlFIfBody{after: AmlCur}
92	  # a While: its predicate's start, what follows it, and whether the body
93	  # is running (else the predicate is being read)
94	  AmlFWhile{start: AmlCur, after: AmlCur, body: Bool}
95	  # a method call's return point
96	  AmlFCall{ctx: AmlCtx, back: AmlCur}
97	  # a Buffer whose size is being read; the rest of its package is its
98	  # initializer
99	  AmlFBuffer{after: AmlCur}
100	  # a Package: its NumElements, the elements so far (last first)
101	  AmlFPkg{count: Nat, got: List<&2, V.AmlValue>, after: AmlCur}
102	  # a VarPackage whose count is being read
103	  AmlFVarPkg{after: AmlCur}
104	  # the bottom: the definition block, or the method evaluated
105	  AmlFTop{}
106	
107	type AmlMode is Data:
108	  # the next term of a term list, or the list's end
109	  AmlMExec{}
110	  # one operand, of this kind
111	  AmlMEval{k: AmlArgK}
112	  # a value for the frame on top
113	  AmlMGive{v: V.AmlValue}
114	  AmlMDone{v: V.AmlValue}
115	  AmlMFail{e: E.AcpiError}
116	
117	# a Notify: the object's path and the value
118	type AmlNote is Data:
119	  AmlNote{path: String, value: W.W64}
120	
121	type AmlEnv is Data:
122	  # wide: 64-bit integers; notes and debug: last first; clock: Timer, in
123	  # 100 ns units (Sleep and Stall advance it)
124	  AmlEnv{wide: Bool, opts: AmlOptions, notes: List<&2, AmlNote>, debug: List<&2, V.AmlValue>, clock: W.W64}
125	
126	type AmlWorld<-H: Data> is Data:
127	  AmlWorld{ctx: AmlCtx, ns: S.AmlNs, host: H, env: AmlEnv}
128	
129	type AmlMachine<-H: Data> is Data:
130	  AmlMachine{mode: AmlMode, cur: AmlCur, frames: List<&2, AmlFrame>, w: AmlWorld<H>}
131	
132	# a value read, and the world after reading it
133	type AmlRead<-H: Data> is Data:
134	  AmlRead{w: AmlWorld<H>, v: V.AmlValue}
135	
136	def AmlMachine.mode(-H: Data, m: AmlMachine<H>) -> AmlMode:
137	  match m:
138	    case AmlMachine{md, c, fs, w}:
139	      md
140	
141	def AmlMachine.world(-H: Data, m: AmlMachine<H>) -> AmlWorld<H>:
142	  match m:
143	    case AmlMachine{md, c, fs, w}:
144	      w
145	
146	# the machine has stopped: Done or Fail
147	def AmlMachine.halted(-H: Data, m: AmlMachine<H>) -> Bool:
148	  match m:
149	    case AmlMachine{AmlMDone{v}, c, fs, w}:
150	      True{}
151	    case AmlMachine{AmlMFail{e}, c, fs, w}:
152	      True{}
153	    case AmlMachine{md, c, fs, w}:
154	      False{}
155	
156	def in.fail(-H: Data, +e: E.AcpiError, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
157	  AmlMachine{AmlMFail{e}, c, fs, w}
158	
159	# World parts
160	
161	def AmlWorld.ctx(-H: Data, w: AmlWorld<H>) -> AmlCtx:
162	  match w:
163	    case AmlWorld{c, n, h, e}:
164	      c
165	
166	def AmlWorld.ns(-H: Data, w: AmlWorld<H>) -> S.AmlNs:
167	  match w:
168	    case AmlWorld{c, n, h, e}:
169	      n
170	
171	def AmlWorld.env(-H: Data, w: AmlWorld<H>) -> AmlEnv:
172	  match w:
173	    case AmlWorld{c, n, h, e}:
174	      e
175	
176	def AmlWorld.host(-H: Data, w: AmlWorld<H>) -> H:
177	  match w:
178	    case AmlWorld{c, n, h, e}:
179	      h
180	
181	def in.scope(-H: Data, w: AmlWorld<H>) -> String:
182	  match w:
183	    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
184	      s
185	
186	def in.wide(-H: Data, w: AmlWorld<H>) -> Bool:
187	  match w:
188	    case AmlWorld{c, n, h, AmlEnv{wd, o, nt, d, cl}}:
189	      wd
190	
191	def in.with_ns(-H: Data, w: AmlWorld<H>, n: S.AmlNs) -> AmlWorld<H>:
192	  match w:
193	    case AmlWorld{c, n0, h, e}:
194	      AmlWorld{c, n, h, e}
195	
196	def in.with_host(-H: Data, w: AmlWorld<H>, h: H) -> AmlWorld<H>:
197	  match w:
198	    case AmlWorld{c, n, h0, e}:
199	      AmlWorld{c, n, h, e}
200	
201	def in.with_ctx(-H: Data, w: AmlWorld<H>, c: AmlCtx) -> AmlWorld<H>:
202	  match w:
203	    case AmlWorld{c0, n, h, e}:
204	      AmlWorld{c, n, h, e}
205	
206	def in.with_env(-H: Data, w: AmlWorld<H>, e: AmlEnv) -> AmlWorld<H>:
207	  match w:
208	    case AmlWorld{c, n, h, e0}:
209	      AmlWorld{c, n, h, e}
210	
211	def in.with_scope(-H: Data, w: AmlWorld<H>, s: String) -> AmlWorld<H>:
212	  match w:
213	    case AmlWorld{AmlCtx{s0, a, l, t}, n, h, e}:
214	      AmlWorld{AmlCtx{s, a, l, t}, n, h, e}
215	
216	# a name created: in the namespace, and among the method call's names
217	def in.define(-H: Data, w: AmlWorld<H>, +p: String, o: S.AmlObject) -> AmlWorld<H>:
218	  match w:
219	    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
220	      AmlWorld{AmlCtx{s, a, l, Con{p, t}}, S.AmlNs.set(n, p, o), h, e}
221	
222	def in.note(-H: Data, w: AmlWorld<H>, nt: AmlNote) -> AmlWorld<H>:
223	  match w:
224	    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
225	      AmlWorld{c, n, h, AmlEnv{wd, o, Con{nt, nts}, d, cl}}
226	
227	def in.debug(-H: Data, w: AmlWorld<H>, v: V.AmlValue) -> AmlWorld<H>:
228	  match w:
229	    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
230	      AmlWorld{c, n, h, AmlEnv{wd, o, nts, Con{v, d}, cl}}
231	
232	def in.tick(-H: Data, w: AmlWorld<H>, +dt: W.W64) -> AmlWorld<H>:
233	  match w:
234	    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
235	      AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, W.W64.add(cl, dt)}}
236	
237	def in.clock(-H: Data, w: AmlWorld<H>) -> W.W64:
238	  match w:
239	    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
240	      cl
241	
242	def in.opts(-H: Data, w: AmlWorld<H>) -> AmlOptions:
243	  match w:
244	    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
245	      o
246	
247	# Decoding: reading from the cursor
248	
249	type AmlB is Data:
250	  AmlB{b: U32, cur: AmlCur}
251	
252	type AmlPkgC is Data:
253	  # the package's contents, and what follows the package
254	  AmlPkgC{body: AmlCur, after: AmlCur}
255	
256	type AmlNameC is Data:
257	  AmlNameC{name: N.AmlName, cur: AmlCur}
258	
259	def cur.byte(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlB>:
260	  match c:
261	    case AmlCur{code, lim}:
262	      match code lim:
263	        case Con{h, t} 1n+p:
264	          Done{AmlB{h, AmlCur{t, p}}}
265	        case _ _:
266	          Fail{E.AcpiAmlTruncated{}}
267	
268	def cur.at_end(c: AmlCur) -> Bool:
269	  match c:
270	    case AmlCur{code, lim}:
271	      Nat.is_eq(lim, 0n)
272	
273	# the next byte, if the list has one
274	def cur.peek(c: AmlCur) -> Maybe<&2, U32>:
275	  match c:
276	    case AmlCur{code, lim}:
277	      match lim:
278	        case 0n:
279	          None{}
280	        case 1n+p:
281	          List.head(&2, U32, code)
282	
283	def cur.skip(+n: Nat, c: AmlCur) -> AmlCur:
284	  match c:
285	    case AmlCur{code, lim}:
286	      AmlCur{B.drop(n, code), Nat.sub(lim, n)}
287	
288	def cur.take(+n: Nat, c: AmlCur) -> B.Octets:
289	  match c:
290	    case AmlCur{code, lim}:
291	      B.Octets.of_list(B.take.fast(n, code))
292	
293	def cur.len(c: AmlCur) -> Nat:
294	  match c:
295	    case AmlCur{code, lim}:
296	      lim
297	
298	def cur.pkg.k(ok: Bool, +inner: Nat, rest: List<&2, U32>, +outer: Nat) -> Result<&2, &2, E.AcpiError, AmlPkgC>:
299	  match ok:
300	    case False{}:
301	      Fail{E.AcpiAmlBadPkgLength{}}
302	    case True{}:
303	      +r = rest
304	      Done{AmlPkgC{AmlCur{r, inner}, AmlCur{B.drop(inner, r), outer}}}
305	
306	def cur.pkg.go(r: Result<&2, &2, E.AcpiError, K.AmlPkgL>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlPkgC>:
307	  match r:
308	    case Fail{e}:
309	      Fail{e}
310	    case Done{K.AmlPkgL{v, +size, rest}}:
311	      +total = U32.to_nat(v)
312	      cur.pkg.k(Bool.and(Nat.is_le(size, total), Nat.is_le(total, lim)), Nat.sub(total, size), rest, Nat.sub(lim, total))
313	
314	# a PkgLength and the package it covers (the value counts the PkgLength's
315	# own bytes); AcpiAmlBadPkgLength if it runs past the enclosing list
316	def cur.pkg(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlPkgC>:
317	  match c:
318	    case AmlCur{+code, +lim}:
319	      cur.pkg.go(K.pk.dec(code), lim)
320	
321	def cur.name.fit(ok: Bool, n: N.AmlName, rest: List<&2, U32>, left: Nat) -> Result<&2, &2, E.AcpiError, AmlNameC>:
322	  match ok:
323	    case False{}:
324	      Fail{E.AcpiAmlTruncated{}}
325	    case True{}:
326	      Done{AmlNameC{n, AmlCur{rest, left}}}
327	
328	def cur.name.k(ok: Bool, +n: N.AmlName, +size: Nat, rest: List<&2, U32>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlNameC>:
329	  match ok:
330	    case False{}:
331	      Fail{E.AcpiAmlUnsupported{"a NameString not in its shortest form"}}
332	    case True{}:
333	      cur.name.fit(Nat.is_le(size, lim), n, rest, Nat.sub(lim, size))
334	
335	def cur.name.go(r: Result<&2, &2, E.AcpiError, N.AmlNameL>, +code: List<&2, U32>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlNameC>:
336	  match r:
337	    case Fail{e}:
338	      Fail{e}
339	    case Done{N.AmlNameL{+n, rest}}:
340	      +size = N.AmlName.size(n)
341	      cur.name.k(B.list_eq.fast(B.take.fast(size, code), N.nm.enc(n)), n, size, rest, lim)
342	
343	# a NameString (in the shortest form, as compilers write it)
344	def cur.name(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlNameC>:
345	  match c:
346	    case AmlCur{+code, +lim}:
347	      cur.name.go(N.nm.dec(code), code, lim)
348	
349	def cur.fold(xs: List<&2, U32>, +sh: Nat, acc: W.W64) -> W.W64:
350	  match xs:
351	    case Nil{}:
352	      acc
353	    case Con{h, t}:
354	      cur.fold(t, Nat.add(sh, 8n), W.W64.or(acc, W.W64.shl(W.W64.from_u32(U32.and(h, 255)), sh)))
355	
356	type AmlImm is Data:
357	  AmlImm{v: W.W64, cur: AmlCur}
358	
359	def cur.imm.k(ok: Bool, +n: Nat, c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlImm>:
360	  match ok:
361	    case False{}:
362	      Fail{E.AcpiAmlTruncated{}}
363	    case True{}:
364	      match c:
365	        case AmlCur{+code, lim}:
366	          Done{AmlImm{cur.fold(B.take.fast(n, code), 0n, W.W64.zero()), AmlCur{B.drop(n, code), Nat.sub(lim, n)}}}
367	
368	# n bytes of immediate data, little-endian
369	def cur.imm(+n: Nat, +c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlImm>:
370	  cur.imm.k(Nat.is_le(n, cur.len(c)), n, c)
371	
372	# Named objects
373	
374	def in.alias.go(n: Nat, +ns: S.AmlNs, +p: String, o: Maybe<&2, S.AmlObject>) -> String:
375	  match n:
376	    case 0n:
377	      p
378	    case 1n+k:
379	      match o:
380	        case Some{S.AmlOAlias{+t}}:
381	          in.alias.go(k, ns, t, S.AmlNs.get(ns, t))
382	        case _:
383	          p
384	
385	# an alias followed to what it names (up to 8 aliases deep)
386	def in.unalias(+ns: S.AmlNs, +p: String) -> String:
387	  in.alias.go(8n, ns, p, S.AmlNs.get(ns, p))
388	
389	def in.int.of(o: Maybe<&2, S.AmlObject>) -> W.W64:
390	  match o:
391	    case Some{S.AmlOData{V.AmlInt{x}}}:
392	      x
393	    case _:
394	      W.W64.zero()
395	
396	# the Integer a Name holds (0 if there is none)
397	def in.name_int(+ns: S.AmlNs, +p: String) -> W.W64:
398	  in.int.of(S.AmlNs.get(ns, p))
399	
400	def in.up.go(n: Nat, hit: Bool, +ns: S.AmlNs, +p: String, +seg: String) -> W.W64:
401	  match n:
402	    case 0n:
403	      W.W64.zero()
404	    case 1n+k:
405	      match hit:
406	        case True{}:
407	          in.name_int(ns, S.AmlPath.child(p, seg))
408	        case False{}:
409	          +up = S.AmlPath.parent(p)
410	          in.up.go(k, S.AmlNs.has(ns, S.AmlPath.child(up, seg)), ns, up, seg)
411	
412	# the Integer seg names in p or the nearest scope enclosing it (0 if none)
413	def in.up_int(+ns: S.AmlNs, +p: String, +seg: String) -> W.W64:
414	  in.up.go(String.length(p), S.AmlNs.has(ns, S.AmlPath.child(p, seg)), ns, p, seg)
415	
416	def in.base.pick(pci: Bool, +ns: S.AmlNs, +parent: String, +off: W.W64) -> W.W64:
417	  match pci:
418	    case False{}:
419	      off
420	    case True{}:
421	      +adr = W.W64.lo(in.name_int(ns, S.AmlPath.child(parent, "_ADR")))
422	      +bus = W.W64.lo(in.up_int(ns, parent, "_BBN"))
423	      +seg = W.W64.lo(in.up_int(ns, parent, "_SEG"))
424	      W.W64.add(Hs.AmlPci.address(seg, bus, U32.shrn(adr, 16n), U32.and(adr, 65535), 0), off)
425	
426	def in.desc.go(o: Maybe<&2, S.AmlObject>, +ns: S.AmlNs, +off: Nat, +bits: Nat, +flags: U32) -> Result<&2, &2, E.AcpiError, F.AmlFieldDesc>:
427	  match o:
428	    case Some{S.AmlORegion{+sp, +roff, len, +parent}}:
429	      Done{F.AmlFieldDesc{sp, in.base.pick(U32.is_eq(sp, 2), ns, parent, roff), len, off, bits, flags}}
430	    case _:
431	      Fail{E.AcpiAmlBadType{"the region of a field is not an OperationRegion"}}
432	
433	# a field unit of a region, its region resolved
434	def in.desc(+ns: S.AmlNs, +region: String, +off: Nat, +bits: Nat, +flags: U32) -> Result<&2, &2, E.AcpiError, F.AmlFieldDesc>:
435	  in.desc.go(S.AmlNs.get(ns, in.unalias(ns, region)), ns, off, bits, flags)
436	
437	def in.fdesc(o: Maybe<&2, S.AmlObject>, +ns: S.AmlNs) -> Result<&2, &2, E.AcpiError, F.AmlFieldDesc>:
438	  match o:
439	    case Some{S.AmlOField{r, off, bits, flags}}:
440	      in.desc(ns, r, off, bits, flags)
441	    case _:
442	      Fail{E.AcpiAmlBadType{"a register of an IndexField is not a field"}}
443	
444	# Reading
445	
446	def in.nth(xs: List<&2, V.AmlValue>, i: Nat) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
447	  match xs i:
448	    case Nil{} _:
449	      Fail{E.AcpiAmlRange{}}
450	    case Con{h, t} 0n:
451	      Done{h}
452	    case Con{h, t} 1n+k:
453	      in.nth(t, k)
454	
455	def in.byte.at(m: Maybe<&2, U32>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
456	  match m:
457	    case None{}:
458	      Fail{E.AcpiAmlRange{}}
459	    case Some{b}:
460	      Done{V.AmlInt{W.W64.from_u32(b)}}
461	
462	# element i of a package, buffer or string
463	def AmlValue.element(v: V.AmlValue, +i: Nat) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
464	  match v:
465	    case V.AmlPkg{xs}:
466	      in.nth(xs, i)
467	    case V.AmlBuf{b}:
468	      in.byte.at(B.Octets.at(b, i))
469	    case V.AmlStr{s}:
470	      in.byte.at(B.Octets.at(s, i))
471	    case _:
472	      Fail{E.AcpiAmlBadType{"Index of a value that is not a package, buffer or string"}}
473	
474	def in.ctx.arg(-H: Data, w: AmlWorld<H>, i: Nat) -> V.AmlValue:
475	  match w:
476	    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
477	      Maybe.default(&2, V.AmlValue, List.get(&2, V.AmlValue, a, i), V.AmlUninit{})
478	
479	def in.ctx.local(-H: Data, w: AmlWorld<H>, i: Nat) -> V.AmlValue:
480	  match w:
481	    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
482	      Maybe.default(&2, V.AmlValue, List.get(&2, V.AmlValue, l, i), V.AmlUninit{})
483	
484	# xs with element i replaced (padded with Uninitialized up to i)
485	def in.list.set(i: Nat, xs: List<&2, V.AmlValue>, v: V.AmlValue) -> List<&2, V.AmlValue>:
486	  match i xs:
487	    case 0n Nil{}:
488	      [v]
489	    case 0n Con{h, t}:
490	      Con{v, t}
491	    case 1n+k Nil{}:
492	      Con{V.AmlUninit{}, in.list.set(k, Nil{}, v)}
493	    case 1n+k Con{h, t}:
494	      Con{h, in.list.set(k, t, v)}
495	
496	def in.set.arg(-H: Data, w: AmlWorld<H>, i: Nat, v: V.AmlValue) -> AmlWorld<H>:
497	  match w:
498	    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
499	      AmlWorld{AmlCtx{s, in.list.set(i, a, v), l, t}, n, h, e}
500	
501	def in.set.local(-H: Data, w: AmlWorld<H>, i: Nat, v: V.AmlValue) -> AmlWorld<H>:
502	  match w:
503	    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
504	      AmlWorld{AmlCtx{s, a, in.list.set(i, l, v), t}, n, h, e}
505	
506	def in.wrap(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, V.AmlValue>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
507	  match r:
508	    case Fail{e}:
509	      Fail{e}
510	    case Done{v}:
511	      Done{AmlRead{w, v}}
512	
513	def in.got.int(-H: Data, +wide: Bool, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
514	  match r:
515	    case Fail{e}:
516	      Fail{e}
517	    case Done{Hs.AmlHostAns{h, x}}:
518	      Done{AmlRead{in.with_host(H, w, h), V.AmlInt{V.AmlInt.fit(wide, x)}}}
519	
520	def in.got.buf(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, F.AmlFieldBuf<H>>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
521	  match r:
522	    case Fail{e}:
523	      Fail{e}
524	    case Done{F.AmlFieldBuf{h, o}}:
525	      Done{AmlRead{in.with_host(H, w, h), V.AmlBuf{o}}}
526	
527	def in.field.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, small: Bool, +w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
528	  match small:
529	    case True{}:
530	      match r:
531	        case Fail{e}:
532	          Fail{e}
533	        case Done{+d}:
534	          in.got.int(H, in.wide(H, w), w, F.AmlField.read_int(~H, ~io, d, AmlWorld.host(H, w)))
535	    case False{}:
536	      match r:
537	        case Fail{e}:
538	          Fail{e}
539	        case Done{+d}:
540	          in.got.buf(H, w, F.AmlField.read_buf(~H, ~io, d, AmlWorld.host(H, w)))
541	
542	def in.ixfield.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ri: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, rd: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, +f: F.AmlFieldDesc, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
543	  match ri rd:
544	    case Done{+i} Done{+d}:
545	      in.got.int(H, in.wide(H, w), w, F.AmlField.read_indexed(~H, ~io, i, d, f, AmlWorld.host(H, w)))
546	    case Fail{e} _:
547	      Fail{e}
548	    case Done{i} Fail{e}:
549	      Fail{e}
550	
551	def in.data.of(o: Maybe<&2, S.AmlObject>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
552	  match o:
553	    case Some{S.AmlOData{v}}:
554	      Done{v}
555	    case _:
556	      Fail{E.AcpiAmlBadType{"the source of a buffer field is not data"}}
557	
558	# the data a location holds, without reading hardware: a Name value, a
559	# Local, an Arg (the buffer behind a buffer field)
560	def in.read_data(-H: Data, +w: AmlWorld<H>, l: V.AmlLoc) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
561	  match l:
562	    case V.AmlLName{+p}:
563	      in.data.of(S.AmlNs.get(AmlWorld.ns(H, w), in.unalias(AmlWorld.ns(H, w), p)))
564	    case V.AmlLLocal{i}:
565	      Done{in.ctx.local(H, w, i)}
566	    case V.AmlLArg{i}:
567	      Done{in.ctx.arg(H, w, i)}
568	    case _:
569	      Fail{E.AcpiAmlUnsupported{"a buffer field of an element"}}
570	
571	def in.bf.rd.pick(-H: Data, small: Bool, +wide: Bool, +w: AmlWorld<H>, +b: B.Octets, +off: Nat, +bits: Nat) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
572	  match small:
573	    case True{}:
574	      in.wrap(H, w, Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{V.AmlInt.fit(wide, x)}, F.AmlBits.get(b, off, bits)))
575	    case False{}:
576	      Done{AmlRead{w, V.AmlBuf{F.AmlBits.get_buf(b, off, bits)}}}
577	
578	def in.bf.rd(-H: Data, +wide: Bool, +w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, V.AmlValue>, +off: Nat, +bits: Nat) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
579	  match r:
580	    case Fail{e}:
581	      Fail{e}
582	    case Done{V.AmlBuf{+b}}:
583	      in.bf.rd.pick(H, Nat.is_le(bits, 64n), wide, w, b, off, bits)
584	    case Done{v}:
585	      Fail{E.AcpiAmlBadType{"the source of a buffer field is not a buffer"}}
586	
587	def in.ix.desc(+ns: S.AmlNs, +off: Nat, +bits: Nat, +flags: U32) -> F.AmlFieldDesc:
588	  F.AmlFieldDesc{0, W.W64.zero(), W.W64.max(), off, bits, flags}
589	
590	# the value of a named object (alias followed): a field unit is read
591	# through the host
592	def in.read_obj(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +p: String, o: Maybe<&2, S.AmlObject>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
593	  match o:
594	    case None{}:
595	      Fail{E.AcpiAmlUndefined{p}}
596	    case Some{S.AmlOData{v}}:
597	      Done{AmlRead{w, v}}
598	    case Some{S.AmlOField{r, +off, +bits, +flags}}:
599	      in.field.rd(~H, ~io, Nat.is_le(bits, 64n), w, in.desc(AmlWorld.ns(H, w), r, off, bits, flags))
600	    case Some{S.AmlOIndexField{i, d, +off, +bits, +flags}}:
601	      in.ixfield.rd(~H, ~io, in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), i), AmlWorld.ns(H, w)), in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), d), AmlWorld.ns(H, w)), in.ix.desc(AmlWorld.ns(H, w), off, bits, flags), w)
602	    case Some{S.AmlOBufField{l, +off, +bits}}:
603	      in.bf.rd(H, in.wide(H, w), w, in.read_data(H, w, l), off, bits)
604	    case Some{+obj}:
605	      Done{AmlRead{w, V.AmlObj{p, S.AmlObject.type(obj)}}}
606	
607	def in.elem.rd(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, +i: Nat) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
608	  match r:
609	    case Fail{e}:
610	      Fail{e}
611	    case Done{AmlRead{w, v}}:
612	      in.wrap(H, w, AmlValue.element(v, i))
613	
614	# the value at a location
615	def in.read_loc(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, l: V.AmlLoc, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
616	  match l:
617	    case V.AmlLName{+p}:
618	      +q = in.unalias(AmlWorld.ns(H, w), p)
619	      in.read_obj(~H, ~io, w, q, S.AmlNs.get(AmlWorld.ns(H, w), q))
620	    case V.AmlLLocal{i}:
621	      Done{AmlRead{w, in.ctx.local(H, w, i)}}
622	    case V.AmlLArg{i}:
623	      Done{AmlRead{w, in.ctx.arg(H, w, i)}}
624	    case V.AmlLIndex{base, +i}:
625	      in.elem.rd(H, in.read_loc(~H, ~io, base, w), i)
626	    case V.AmlLElem{v, +i}:
627	      in.wrap(H, w, AmlValue.element(v, i))
628	    case V.AmlLDebug{}:
629	      Done{AmlRead{w, V.AmlUninit{}}}
630	    case V.AmlLNone{}:
631	      Done{AmlRead{w, V.AmlUninit{}}}
632	
633	# Writing
634	
635	def in.host.w(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
636	  match r:
637	    case Fail{e}:
638	      Fail{e}
639	    case Done{Hs.AmlHostAns{h, x}}:
640	      Done{in.with_host(H, w, h)}
641	
642	def in.field.wr.int(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +d: F.AmlFieldDesc, r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
643	  match r:
644	    case Fail{e}:
645	      Fail{e}
646	    case Done{x}:
647	      in.host.w(H, w, F.AmlField.write_int(~H, ~io, d, AmlWorld.host(H, w), x))
648	
649	def in.field.wr.buf(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +d: F.AmlFieldDesc, r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
650	  match r:
651	    case Fail{e}:
652	      Fail{e}
653	    case Done{o}:
654	      in.host.w(H, w, F.AmlField.write_buf(~H, ~io, d, AmlWorld.host(H, w), o))
655	
656	def in.field.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, small: Bool, +w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
657	  match small:
658	    case True{}:
659	      match r:
660	        case Fail{e}:
661	          Fail{e}
662	        case Done{+d}:
663	          in.field.wr.int(~H, ~io, w, d, V.AmlValue.to_int(in.wide(H, w), v))
664	    case False{}:
665	      match r:
666	        case Fail{e}:
667	          Fail{e}
668	        case Done{+d}:
669	          in.field.wr.buf(~H, ~io, w, d, V.AmlValue.to_buf(in.wide(H, w), v))
670	
671	def in.ixfield.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ri: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, rd: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, rx: Result<&2, &2, E.AcpiError, W.W64>, +f: F.AmlFieldDesc, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
672	  match ri rd rx:
673	    case Done{+i} Done{+d} Done{+x}:
674	      in.host.w(H, w, F.AmlField.write_indexed(~H, ~io, i, d, f, AmlWorld.host(H, w), x))
675	    case Fail{e} _ _:
676	      Fail{e}
677	    case Done{i} Fail{e} _:
678	      Fail{e}
679	    case Done{i} Done{d} Fail{e}:
680	      Fail{e}
681	
682	def in.fit.buf(+n: Nat, +o: B.Octets) -> B.Octets:
683	  +h = B.Octets.take(n, o)
684	  B.Octets.append(h, B.Octets.zeros(Nat.sub(n, B.Octets.len(h))))
685	
686	# the value v stored where a Name holds old: converted to old type when
687	# old is an Integer, a String or a Buffer (a Buffer keeps its length)
688	def in.convert(+wide: Bool, old: V.AmlValue, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
689	  match old:
690	    case V.AmlInt{x}:
691	      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, y => V.AmlInt{y}, V.AmlValue.to_int(wide, v))
692	    case V.AmlStr{s}:
693	      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlStr{t}, V.AmlValue.to_str(wide, v))
694	    case V.AmlBuf{+b}:
695	      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlBuf{in.fit.buf(B.Octets.len(b), t)}, V.AmlValue.to_buf(wide, v))
696	    case _:
697	      Done{v}
698	
699	def in.set.data(-H: Data, +w: AmlWorld<H>, +p: String, r: Result<&2, &2, E.AcpiError, V.AmlValue>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
700	  match r:
701	    case Fail{e}:
702	      Fail{e}
703	    case Done{v}:
704	      Done{in.with_ns(H, w, S.AmlNs.set(AmlWorld.ns(H, w), p, S.AmlOData{v}))}
705	
706	# a buffer put back where a buffer field found it
707	def in.put.data(-H: Data, +w: AmlWorld<H>, l: V.AmlLoc, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
708	  match l:
709	    case V.AmlLName{+p}:
710	      Done{in.with_ns(H, w, S.AmlNs.set(AmlWorld.ns(H, w), in.unalias(AmlWorld.ns(H, w), p), S.AmlOData{v}))}
711	    case V.AmlLLocal{i}:
712	      Done{in.set.local(H, w, i, v)}
713	    case V.AmlLArg{i}:
714	      Done{in.set.arg(H, w, i, v)}
715	    case _:
716	      Fail{E.AcpiAmlUnsupported{"a buffer field of an element"}}
717	
718	def in.bf.wr.go(-H: Data, +w: AmlWorld<H>, l: V.AmlLoc, r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
719	  match r:
720	    case Fail{e}:
721	      Fail{e}
722	    case Done{b}:
723	      in.put.data(H, w, l, V.AmlBuf{b})
724	
725	def in.bf.wr(-H: Data, +w: AmlWorld<H>, +l: V.AmlLoc, src: Result<&2, &2, E.AcpiError, V.AmlValue>, +off: Nat, +bits: Nat, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
726	  match src:
727	    case Fail{e}:
728	      Fail{e}
729	    case Done{V.AmlBuf{+b}}:
730	      in.bf.wr.go(H, w, l, Result.bind(&2, &2, E.AcpiError, W.W64, B.Octets, V.AmlValue.to_int(in.wide(H, w), v), x => F.AmlBits.set(b, off, Nat.min(bits, 64n), x)))
731	    case Done{o}:
732	      Fail{E.AcpiAmlBadType{"the source of a buffer field is not a buffer"}}
733	
734	# Store to a named object (chapter 19, Store): a Name converted to its type, a field
735	# unit written through the host, a buffer field into its buffer
736	def in.store.obj(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +p: String, o: Maybe<&2, S.AmlObject>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
737	  match o:
738	    case None{}:
739	      Fail{E.AcpiAmlUndefined{p}}
740	    case Some{S.AmlOData{old}}:
741	      in.set.data(H, w, p, in.convert(in.wide(H, w), old, v))
742	    case Some{S.AmlOField{r, +off, +bits, +flags}}:
743	      in.field.wr(~H, ~io, Nat.is_le(bits, 64n), w, in.desc(AmlWorld.ns(H, w), r, off, bits, flags), v)
744	    case Some{S.AmlOIndexField{i, d, +off, +bits, +flags}}:
745	      in.ixfield.wr(~H, ~io, in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), i), AmlWorld.ns(H, w)), in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), d), AmlWorld.ns(H, w)), V.AmlValue.to_int(in.wide(H, w), v), in.ix.desc(AmlWorld.ns(H, w), off, bits, flags), w)
746	    case Some{S.AmlOBufField{+l, +off, +bits}}:
747	      in.bf.wr(H, w, l, in.read_data(H, w, l), off, bits, v)
748	    case Some{obj}:
749	      Fail{E.AcpiAmlBadType{"Store to an object that holds no data"}}
750	
751	def in.elem.pkg(ok: Bool, xs: List<&2, V.AmlValue>, i: Nat, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
752	  match ok:
753	    case True{}:
754	      Done{V.AmlPkg{in.list.set(i, xs, v)}}
755	    case False{}:
756	      Fail{E.AcpiAmlRange{}}
757	
758	def in.elem.wrap(str: Bool, b: B.Octets) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
759	  match str:
760	    case True{}:
761	      Done{V.AmlStr{b}}
762	    case False{}:
763	      Done{V.AmlBuf{b}}
764	
765	def in.elem.bytes(ok: Bool, str: Bool, +b: B.Octets, +i: Nat, r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
766	  match ok r:
767	    case False{} _:
768	      Fail{E.AcpiAmlRange{}}
769	    case True{} Fail{e}:
770	      Fail{e}
771	    case True{} Done{x}:
772	      +nb = B.Octets.concat([B.Octets.take(i, b), B.Octets.of_list([W.W64.lo(x)]), B.Octets.drop(1n+i, b)])
773	      in.elem.wrap(str, nb)
774	
775	def in.elem.set(base: V.AmlValue, +i: Nat, +wide: Bool, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
776	  match base:
777	    case V.AmlPkg{+xs}:
778	      in.elem.pkg(Nat.is_lt(i, List.length(&2, V.AmlValue, xs)), xs, i, v)
779	    case V.AmlBuf{+b}:
780	      in.elem.bytes(Nat.is_lt(i, B.Octets.len(b)), False{}, b, i, V.AmlValue.to_int(wide, v))
781	    case V.AmlStr{+b}:
782	      in.elem.bytes(Nat.is_lt(i, B.Octets.len(b)), True{}, b, i, V.AmlValue.to_int(wide, v))
783	    case _:
784	      Fail{E.AcpiAmlBadType{"Index of a value that is not a package, buffer or string"}}
785	
786	type AmlPut<-H: Data> is Data:
787	  AmlPut{w: AmlWorld<H>, v: V.AmlValue}
788	
789	def in.put.res(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, V.AmlValue>) -> Result<&2, &2, E.AcpiError, AmlPut<H>>:
790	  match r:
791	    case Fail{e}:
792	      Fail{e}
793	    case Done{v}:
794	      Done{AmlPut{w, v}}
795	
796	def in.put.idx.go(-H: Data, r: Result<&2, &2, E.AcpiError, V.AmlValue>, +w: AmlWorld<H>, base: V.AmlLoc) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
797	  match r:
798	    case Fail{e}:
799	      Fail{e}
800	    case Done{nv}:
801	      in.put.data(H, w, base, nv)
802	
803	def in.put.idx(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, base: V.AmlLoc, +i: Nat, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
804	  match r:
805	    case Fail{e}:
806	      Fail{e}
807	    case Done{AmlRead{+w, old}}:
808	      in.put.idx.go(H, in.elem.set(old, i, in.wide(H, w), v), w, base)
809	
810	# an element of a package, buffer or string at a location replaced
811	# (Store to Index(...)); the location must be a Name, a Local or an Arg
812	def in.put.index(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +base: V.AmlLoc, +i: Nat, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
813	  in.put.idx(H, in.read_loc(~H, ~io, base, w), base, i, v)
814	
815	def in.is_writable(o: Maybe<&2, S.AmlObject>) -> Bool:
816	  match o:
817	    case Some{S.AmlOField{r, off, n, f}}:
818	      True{}
819	    case Some{S.AmlOIndexField{i, d, off, n, f}}:
820	      True{}
821	    case Some{S.AmlOBufField{l, off, n}}:
822	      True{}
823	    case _:
824	      False{}
825	
826	def in.put.name(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, fieldy: Bool, +w: AmlWorld<H>, +p: String, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
827	  match fieldy:
828	    case True{}:
829	      in.store.obj(~H, ~io, w, p, S.AmlNs.get(AmlWorld.ns(H, w), p), v)
830	    case False{}:
831	      Done{in.with_ns(H, w, S.AmlNs.set(AmlWorld.ns(H, w), p, S.AmlOData{v}))}
832	
833	# CopyObject (chapter 19), and how Index writes back: the value replaces what
834	# the location holds, without conversion (a field unit is written)
835	def in.put(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, l: V.AmlLoc, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
836	  match l:
837	    case V.AmlLName{+p}:
838	      +q = in.unalias(AmlWorld.ns(H, w), p)
839	      in.put.name(~H, ~io, in.is_writable(S.AmlNs.get(AmlWorld.ns(H, w), q)), w, q, v)
840	    case V.AmlLLocal{i}:
841	      Done{in.set.local(H, w, i, v)}
842	    case V.AmlLArg{i}:
843	      Done{in.set.arg(H, w, i, v)}
844	    case V.AmlLIndex{base, i}:
845	      in.put.index(~H, ~io, base, i, w, v)
846	    case V.AmlLElem{x, i}:
847	      Done{w}
848	    case V.AmlLDebug{}:
849	      Done{in.debug(H, w, v)}
850	    case V.AmlLNone{}:
851	      Done{w}
852	
853	# Store (chapter 19) to a location, an Arg holding a reference excepted
854	def in.store.base(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, l: V.AmlLoc, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
855	  match l:
856	    case V.AmlLName{+p}:
857	      +q = in.unalias(AmlWorld.ns(H, w), p)
858	      in.store.obj(~H, ~io, w, q, S.AmlNs.get(AmlWorld.ns(H, w), q), v)
859	    case V.AmlLLocal{i}:
860	      Done{in.set.local(H, w, i, v)}
861	    case V.AmlLArg{i}:
862	      Done{in.set.arg(H, w, i, v)}
863	    case V.AmlLIndex{base, i}:
864	      in.put.index(~H, ~io, base, i, w, v)
865	    case V.AmlLElem{x, i}:
866	      Done{w}
867	    case V.AmlLDebug{}:
868	      Done{in.debug(H, w, v)}
869	    case V.AmlLNone{}:
870	      Done{w}
871	
872	def in.store.arg(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, cur: V.AmlValue, +i: Nat, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
873	  match cur:
874	    case V.AmlRef{l2}:
875	      in.store.base(~H, ~io, l2, w, v)
876	    case _:
877	      Done{in.set.arg(H, w, i, v)}
878	
879	# Store to a location; an Arg that holds a reference is stored through
880	def in.store(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +l: V.AmlLoc, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
881	  match l:
882	    case V.AmlLArg{+i}:
883	      in.store.arg(~H, ~io, in.ctx.arg(H, w, i), i, w, v)
884	    case _:
885	      in.store.base(~H, ~io, l, w, v)
886	
887	# Machine transitions
888	
889	def in.mk(-H: Data, md: AmlMode, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
890	  AmlMachine{md, c, fs, w}
891	
892	def in.give(-H: Data, v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
893	  AmlMachine{AmlMGive{v}, c, fs, w}
894	
895	def in.no.cur() -> AmlCur:
896	  AmlCur{Nil{}, 0n}
897	
898	# a world after a change, or the failure; then v is given
899	def in.then.give(-H: Data, r: Result<&2, &2, E.AcpiError, AmlWorld<H>>, v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
900	  match r:
901	    case Fail{e}:
902	      AmlMachine{AmlMFail{e}, c, fs, w}
903	    case Done{w2}:
904	      AmlMachine{AmlMGive{v}, c, fs, w2}
905	
906	def in.read.give(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
907	  match r:
908	    case Fail{e}:
909	      AmlMachine{AmlMFail{e}, c, fs, w}
910	    case Done{AmlRead{w2, v}}:
911	      AmlMachine{AmlMGive{v}, c, fs, w2}
912	
913	def in.val.give(-H: Data, r: Result<&2, &2, E.AcpiError, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
914	  match r:
915	    case Fail{e}:
916	      AmlMachine{AmlMFail{e}, c, fs, w}
917	    case Done{v}:
918	      AmlMachine{AmlMGive{v}, c, fs, w}
919	
920	def in.loc(v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlLoc>:
921	  match v:
922	    case V.AmlRef{l}:
923	      Done{l}
924	    case V.AmlUninit{}:
925	      Done{V.AmlLNone{}}
926	    case _:
927	      Fail{E.AcpiAmlBadOperand{112}}
928	
929	def in.store.give2(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, +v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
930	  match r:
931	    case Fail{e}:
932	      AmlMachine{AmlMFail{e}, c, fs, w}
933	    case Done{l}:
934	      in.then.give(H, in.store(~H, ~io, l, w, v), v, c, fs, w)
935	
936	# the result of an operator stored in its Target, then given
937	def in.store.give(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlValue>, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
938	  match r:
939	    case Fail{e}:
940	      AmlMachine{AmlMFail{e}, c, fs, w}
941	    case Done{+v}:
942	      in.store.give2(~H, ~io, in.loc(t), v, c, fs, w)
943	
944	# Integer operators (19.6: Add, Subtract, Multiply, ShiftLeft, ShiftRight,
945	# And, NAnd, Or, NOr, XOr, Mod). Mod by zero is AcpiAmlDivZero.
946	
947	def in.mod(z: Bool, +x: W.W64, +y: W.W64) -> Result<&2, &2, E.AcpiError, W.W64>:
948	  match z:
949	    case True{}:
950	      Fail{E.AcpiAmlDivZero{}}
951	    case False{}:
952	      Done{W.W64.mod(x, y)}
953	
954	def in.shift.pick(big: Bool, left: Bool, +wide: Bool, +x: W.W64, +n: Nat) -> W.W64:
955	  match big:
956	    case True{}:
957	      W.W64.zero()
958	    case False{}:
959	      match left:
960	        case True{}:
961	          V.AmlInt.fit(wide, W.W64.shl(x, n))
962	        case False{}:
963	          W.W64.shr(x, n)
964	
965	# shifts by 64 or more give 0
966	def in.shift(left: Bool, +wide: Bool, +x: W.W64, +y: W.W64) -> W.W64:
967	  in.shift.pick(Bool.or(Bool.not(U32.is_eq(W.W64.hi(y), 0)), U32.is_le(64, W.W64.lo(y))), left, wide, x, U32.to_nat(W.W64.lo(y)))
968	
969	def in.int2(+op: Nat, +wide: Bool, +x: W.W64, +y: W.W64) -> Result<&2, &2, E.AcpiError, W.W64>:
970	  match op:
971	    case 114n:
972	      Done{V.AmlInt.fit(wide, W.W64.add(x, y))}
973	    case 116n:
974	      Done{V.AmlInt.fit(wide, W.W64.sub(x, y))}
975	    case 119n:
976	      Done{V.AmlInt.fit(wide, W.W64.mul(x, y))}
977	    case 121n:
978	      Done{in.shift(True{}, wide, x, y)}
979	    case 122n:
980	      Done{in.shift(False{}, wide, x, y)}
981	    case 123n:
982	      Done{W.W64.and(x, y)}
983	    case 124n:
984	      Done{V.AmlInt.fit(wide, W.W64.not(W.W64.and(x, y)))}
985	    case 125n:
986	      Done{W.W64.or(x, y)}
987	    case 126n:
988	      Done{V.AmlInt.fit(wide, W.W64.not(W.W64.or(x, y)))}
989	    case 127n:
990	      Done{W.W64.xor(x, y)}
991	    case 133n:
992	      in.mod(W.W64.is_zero(y), x, y)
993	    case _:
994	      Fail{E.AcpiAmlBadOpcode{U32.from_nat(op)}}
995	
996	type AmlInts is Data:
997	  AmlInts{x: W.W64, y: W.W64}
998	
999	def in.ints.go(ra: Result<&2, &2, E.AcpiError, W.W64>, rb: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, AmlInts>:
1000	  match ra rb:
1001	    case Done{x} Done{y}:
1002	      Done{AmlInts{x, y}}
1003	    case Fail{e} _:
1004	      Fail{e}
1005	    case Done{x} Fail{e}:
1006	      Fail{e}
1007	
1008	def in.ints(+wide: Bool, a: V.AmlValue, b: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlInts>:
1009	  in.ints.go(V.AmlValue.to_int(wide, a), V.AmlValue.to_int(wide, b))
1010	
1011	def in.bad(-H: Data, +code: U32, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
1012	  AmlMachine{AmlMFail{E.AcpiAmlBadOperand{code}}, c, fs, w}
1013	
1014	def in.int2.v(+op: Nat, +wide: Bool, r: Result<&2, &2, E.AcpiError, AmlInts>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1015	  match r:
1016	    case Fail{e}:
1017	      Fail{e}
1018	    case Done{AmlInts{x, y}}:
1019	      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, z => V.AmlInt{z}, in.int2(op, wide, x, y))
1020	
1021	def in.ap.int2(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1022	  match args:
1023	    case Con{a, Con{b, Con{t, Nil{}}}}:
1024	      in.store.give(~H, ~io, in.int2.v(op, in.wide(H, w), in.ints(in.wide(H, w), a, b)), t, c, fs, w)
1025	    case _:
1026	      in.bad(H, U32.from_nat(op), c, fs, w)
1027	
1028	def in.div.pick(z: Bool, +x: W.W64, +y: W.W64) -> Result<&2, &2, E.AcpiError, AmlInts>:
1029	  match z:
1030	    case True{}:
1031	      Fail{E.AcpiAmlDivZero{}}
1032	    case False{}:
1033	      Done{AmlInts{W.W64.div(x, y), W.W64.mod(x, y)}}
1034	
1035	# Divide: the remainder to its Target, the quotient to its own
1036	def in.div.v(r: Result<&2, &2, E.AcpiError, AmlInts>) -> Result<&2, &2, E.AcpiError, AmlInts>:
1037	  match r:
1038	    case Fail{e}:
1039	      Fail{e}
1040	    case Done{AmlInts{+x, +y}}:
1041	      in.div.pick(W.W64.is_zero(y), x, y)
1042	
1043	def in.div.q(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlWorld<H>>, +q: W.W64, qt: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1044	  match r:
1045	    case Fail{e}:
1046	      AmlMachine{AmlMFail{e}, c, fs, w}
1047	    case Done{+w2}:
1048	      in.store.give(~H, ~io, Done{V.AmlInt{q}}, qt, c, fs, w2)
1049	
1050	def in.div.st(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlInts>, rt: V.AmlValue, qt: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1051	  match r:
1052	    case Fail{e}:
1053	      AmlMachine{AmlMFail{e}, c, fs, w}
1054	    case Done{AmlInts{+q, rm}}:
1055	      in.div.q(~H, ~io, Result.bind(&2, &2, E.AcpiError, V.AmlLoc, AmlWorld<H>, in.loc(rt), l => in.store(~H, ~io, l, w, V.AmlInt{rm})), q, qt, c, fs, w)
1056	
1057	def in.ap.div(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1058	  match args:
1059	    case Con{a, Con{b, Con{rt, Con{qt, Nil{}}}}}:
1060	      in.div.st(~H, ~io, in.div.v(in.ints(in.wide(H, w), a, b)), rt, qt, c, fs, w)
1061	    case _:
1062	      in.bad(H, 120, c, fs, w)
1063	
1064	# Not, FindSetLeftBit, FindSetRightBit: one operand and a Target
1065	
1066	def in.fsb.first(none: Bool, +i: Nat, acc: Nat) -> Nat:
1067	  match none:
1068	    case True{}:
1069	      Nat.add(i, 1n)
1070	    case False{}:
1071	      acc
1072	
1073	def in.fsb.pick(set: Bool, left: Bool, +i: Nat, +acc: Nat) -> Nat:
1074	  match set:
1075	    case False{}:
1076	      acc
1077	    case True{}:
1078	      match left:
1079	        case True{}:
1080	          Nat.add(i, 1n)
1081	        case False{}:
1082	          in.fsb.first(Nat.is_eq(acc, 0n), i, acc)
1083	
1084	def in.fsb.go(n: Nat, +x: W.W64, +i: Nat, +left: Bool, acc: Nat) -> Nat:
1085	  match n:
1086	    case 0n:
1087	      acc
1088	    case 1n+p:
1089	      in.fsb.go(p, x, Nat.add(i, 1n), left, in.fsb.pick(W.W64.is_eq(W.W64.and(W.W64.shr(x, i), W.W64.one()), W.W64.one()), left, i, acc))
1090	
1091	def in.int1(+op: Nat, +wide: Bool, +x: W.W64) -> W.W64:
1092	  match op:
1093	    case 128n:
1094	      V.AmlInt.fit(wide, W.W64.not(x))
1095	    case 129n:
1096	      W.W64.from_nat(in.fsb.go(64n, x, 0n, True{}, 0n))
1097	    case _:
1098	      W.W64.from_nat(in.fsb.go(64n, x, 0n, False{}, 0n))
1099	
1100	def in.ap.int1(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1101	  match args:
1102	    case Con{a, Con{t, Nil{}}}:
1103	      in.store.give(~H, ~io, Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{in.int1(op, in.wide(H, w), x)}, V.AmlValue.to_int(in.wide(H, w), a)), t, c, fs, w)
1104	    case _:
1105	      in.bad(H, U32.from_nat(op), c, fs, w)
1106	
1107	# Increment, Decrement: read, change, store back
1108	
1109	def in.incdec.op(inc: Bool, +x: W.W64) -> W.W64:
1110	  match inc:
1111	    case True{}:
1112	      W.W64.add(x, W.W64.one())
1113	    case False{}:
1114	      W.W64.sub(x, W.W64.one())
1115	
1116	def in.incdec.v(-H: Data, +inc: Bool, +wide: Bool, r: Result<&2, &2, E.AcpiError, AmlRead<H>>) -> Result<&2, &2, E.AcpiError, AmlPut<H>>:
1117	  match r:
1118	    case Fail{e}:
1119	      Fail{e}
1120	    case Done{AmlRead{w2, v}}:
1121	      in.put.res(H, w2, Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{V.AmlInt.fit(wide, in.incdec.op(inc, x))}, V.AmlValue.to_int(wide, v)))
1122	
1123	def in.incdec.st(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlPut<H>>, +l: V.AmlLoc, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1124	  match r:
1125	    case Fail{e}:
1126	      AmlMachine{AmlMFail{e}, c, fs, w}
1127	    case Done{AmlPut{+w2, +v}}:
1128	      in.then.give(H, in.store(~H, ~io, l, w2, v), v, c, fs, w2)
1129	
1130	def in.incdec.loc(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +inc: Bool, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1131	  match r:
1132	    case Fail{e}:
1133	      AmlMachine{AmlMFail{e}, c, fs, w}
1134	    case Done{+l}:
1135	      in.incdec.st(~H, ~io, in.incdec.v(H, inc, in.wide(H, w), in.read_loc(~H, ~io, l, w)), l, c, fs, w)
1136	
1137	def in.ap.incdec(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +inc: Bool, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1138	  match args:
1139	    case Con{t, Nil{}}:
1140	      in.incdec.loc(~H, ~io, inc, in.loc(t), c, fs, w)
1141	    case _:
1142	      in.bad(H, 117, c, fs, w)
1143	
1144	# Logical operators (LAnd, LOr, LNot, LEqual, LGreater, LLess): Ones or 0
1145	
1146	def in.truth(+wide: Bool, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, Bool>:
1147	  Result.map(&2, &2, E.AcpiError, W.W64, Bool, x => Bool.not(W.W64.is_zero(x)), V.AmlValue.to_int(wide, v))
1148	
1149	def in.bool.v(+wide: Bool, r: Result<&2, &2, E.AcpiError, Bool>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1150	  Result.map(&2, &2, E.AcpiError, Bool, V.AmlValue, b => V.AmlInt{V.AmlInt.of_bool(wide, b)}, r)
1151	
1152	def in.logic2(ra: Result<&2, &2, E.AcpiError, Bool>, rb: Result<&2, &2, E.AcpiError, Bool>, op: Nat) -> Result<&2, &2, E.AcpiError, Bool>:
1153	  match ra rb:
1154	    case Done{x} Done{y}:
1155	      match op:
1156	        case 144n:
1157	          Done{Bool.and(x, y)}
1158	        case _:
1159	          Done{Bool.or(x, y)}
1160	    case Fail{e} _:
1161	      Fail{e}
1162	    case Done{x} Fail{e}:
1163	      Fail{e}
1164	
1165	def in.cmp.op(+op: Nat, c: Cmp) -> Bool:
1166	  match op:
1167	    case 147n:
1168	      Cmp.is_eq(c)
1169	    case 148n:
1170	      Cmp.is_gt(c)
1171	    case _:
1172	      Cmp.is_lt(c)
1173	
1174	def in.logic.pick(cmp: Bool, +op: Nat, +wide: Bool, a: V.AmlValue, +b: V.AmlValue) -> Result<&2, &2, E.AcpiError, Bool>:
1175	  match cmp:
1176	    case True{}:
1177	      Result.map(&2, &2, E.AcpiError, Cmp, Bool, x => in.cmp.op(op, x), V.AmlValue.compare(wide, a, b))
1178	    case False{}:
1179	      in.logic2(in.truth(wide, a), in.truth(wide, b), op)
1180	
1181	def in.logic.two(+op: Nat, +wide: Bool, a: V.AmlValue, +b: V.AmlValue) -> Result<&2, &2, E.AcpiError, Bool>:
1182	  in.logic.pick(Nat.is_le(147n, op), op, wide, a, b)
1183	
1184	def in.ap.logic(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1185	  match args:
1186	    case Con{a, Nil{}}:
1187	      +wide = in.wide(H, w)
1188	      in.val.give(H, in.bool.v(wide, Result.map(&2, &2, E.AcpiError, Bool, Bool, b => Bool.not(b), in.truth(wide, a))), c, fs, w)
1189	    case Con{a, Con{b, Nil{}}}:
1190	      +wide = in.wide(H, w)
1191	      in.val.give(H, in.bool.v(wide, in.logic.two(op, wide, a, b)), c, fs, w)
1192	    case _:
1193	      in.bad(H, U32.from_nat(op), c, fs, w)
1194	
1195	# Store, CopyObject, RefOf, DerefOf
1196	
1197	def in.ap.store(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1198	  match args:
1199	    case Con{v, Con{t, Nil{}}}:
1200	      in.store.give(~H, ~io, Done{v}, t, c, fs, w)
1201	    case _:
1202	      in.bad(H, 112, c, fs, w)
1203	
1204	def in.put.give(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, +v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1205	  match r:
1206	    case Fail{e}:
1207	      AmlMachine{AmlMFail{e}, c, fs, w}
1208	    case Done{l}:
1209	      in.then.give(H, in.put(~H, ~io, l, w, v), v, c, fs, w)
1210	
1211	def in.ap.copy(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1212	  match args:
1213	    case Con{+v, Con{t, Nil{}}}:
1214	      in.put.give(~H, ~io, in.loc(t), v, c, fs, w)
1215	    case _:
1216	      in.bad(H, 157, c, fs, w)
1217	
1218	def in.deref.name(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, m: Maybe<&2, String>, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
1219	  match m:
1220	    case None{}:
1221	      Fail{E.AcpiAmlUndefined{"DerefOf of a name"}}
1222	    case Some{p}:
1223	      in.read_loc(~H, ~io, V.AmlLName{p}, w)
1224	
1225	def in.deref(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, v: V.AmlValue, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
1226	  match v:
1227	    case V.AmlRef{l}:
1228	      in.read_loc(~H, ~io, l, w)
1229	    case V.AmlStr{s}:
1230	      in.deref.name(~H, ~io, S.AmlNs.resolve(AmlWorld.ns(H, w), in.scope(H, w), N.AmlName.of_text(B.Octets.to_string(s))), w)
1231	    case _:
1232	      Fail{E.AcpiAmlBadOperand{131}}
1233	
1234	def in.ap.deref(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1235	  match args:
1236	    case Con{v, Nil{}}:
1237	      in.read.give(H, in.deref(~H, ~io, v, w), c, fs, w)
1238	    case _:
1239	      in.bad(H, 131, c, fs, w)
1240	
1241	# Index (chapter 19): a reference to an element; it is also put in the Target
1242	
1243	def in.index.ref(base: V.AmlValue, +i: Nat) -> V.AmlValue:
1244	  match base:
1245	    case V.AmlRef{l}:
1246	      V.AmlRef{V.AmlLIndex{l, i}}
1247	    case _:
1248	      V.AmlRef{V.AmlLElem{base, i}}
1249	
1250	def in.size.of(v: V.AmlValue) -> Result<&2, &2, E.AcpiError, Nat>:
1251	  match v:
1252	    case V.AmlStr{s}:
1253	      Done{B.Octets.len(s)}
1254	    case V.AmlBuf{b}:
1255	      Done{B.Octets.len(b)}
1256	    case V.AmlPkg{xs}:
1257	      Done{List.length(&2, V.AmlValue, xs)}
1258	    case _:
1259	      Fail{E.AcpiAmlBadType{"SizeOf or Index of a value that is not a string, buffer or package"}}
1260	
1261	# the value a source operand stands for (read when it is a location)
1262	def in.source(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, v: V.AmlValue, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
1263	  match v:
1264	    case V.AmlRef{l}:
1265	      in.read_loc(~H, ~io, l, w)
1266	    case _:
1267	      Done{AmlRead{w, v}}
1268	
1269	def in.index.put(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ok: Bool, +ref: V.AmlValue, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1270	  match ok:
1271	    case False{}:
1272	      AmlMachine{AmlMFail{E.AcpiAmlRange{}}, c, fs, w}
1273	    case True{}:
1274	      in.put.give(~H, ~io, in.loc(t), ref, c, fs, w)
1275	
1276	def in.index.fits(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, Nat>, +base: V.AmlValue, +i: Nat, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1277	  match r:
1278	    case Fail{e}:
1279	      AmlMachine{AmlMFail{e}, c, fs, w}
1280	    case Done{n}:
1281	      in.index.put(~H, ~io, Nat.is_lt(i, n), in.index.ref(base, i), t, c, fs, w)
1282	
1283	def in.index.chk(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, +base: V.AmlValue, +i: Nat, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1284	  match r:
1285	    case Fail{e}:
1286	      AmlMachine{AmlMFail{e}, c, fs, w}
1287	    case Done{AmlRead{+w2, v}}:
1288	      in.index.fits(~H, ~io, in.size.of(v), base, i, t, c, fs, w2)
1289	
1290	def in.index.go(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ri: Result<&2, &2, E.AcpiError, W.W64>, +base: V.AmlValue, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1291	  match ri:
1292	    case Fail{e}:
1293	      AmlMachine{AmlMFail{e}, c, fs, w}
1294	    case Done{x}:
1295	      in.index.chk(~H, ~io, in.source(~H, ~io, base, w), base, W.W64.to_nat(x), t, c, fs, w)
1296	
1297	def in.small.pick(ok: Bool, x: W.W64) -> Result<&2, &2, E.AcpiError, W.W64>:
1298	  match ok:
1299	    case True{}:
1300	      Done{x}
1301	    case False{}:
1302	      Fail{E.AcpiAmlRange{}}
1303	
1304	def in.small.chk(r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, W.W64>:
1305	  match r:
1306	    case Fail{e}:
1307	      Fail{e}
1308	    case Done{+x}:
1309	      in.small.pick(U32.is_eq(W.W64.hi(x), 0), x)
1310	
1311	# an Integer operand that must be small (an index or a count: below 2^32)
1312	def in.small.int(+wide: Bool, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, W.W64>:
1313	  in.small.chk(V.AmlValue.to_int(wide, v))
1314	
1315	def in.ap.index(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1316	  match args:
1317	    case Con{+base, Con{i, Con{t, Nil{}}}}:
1318	      in.index.go(~H, ~io, in.small.int(in.wide(H, w), i), base, t, c, fs, w)
1319	    case _:
1320	      in.bad(H, 136, c, fs, w)
1321	
1322	# SizeOf, ObjectType
1323	
1324	def in.size.give(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1325	  match r:
1326	    case Fail{e}:
1327	      AmlMachine{AmlMFail{e}, c, fs, w}
1328	    case Done{AmlRead{w2, v}}:
1329	      in.val.give(H, Result.map(&2, &2, E.AcpiError, Nat, V.AmlValue, n => V.AmlInt{W.W64.from_nat(n)}, in.size.of(v)), c, fs, w2)
1330	
1331	def in.ap.size(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1332	  match args:
1333	    case Con{v, Nil{}}:
1334	      in.size.give(H, in.source(~H, ~io, v, w), c, fs, w)
1335	    case _:
1336	      in.bad(H, 135, c, fs, w)
1337	
1338	def in.otype.obj(o: Maybe<&2, S.AmlObject>) -> U32:
1339	  match o:
1340	    case Some{x}:
1341	      S.AmlObject.type(x)
1342	    case None{}:
1343	      0
1344	
1345	def in.otype(-H: Data, v: V.AmlValue, +w: AmlWorld<H>) -> U32:
1346	  match v:
1347	    case V.AmlRef{V.AmlLName{+p}}:
1348	      in.otype.obj(S.AmlNs.get(AmlWorld.ns(H, w), in.unalias(AmlWorld.ns(H, w), p)))
1349	    case V.AmlRef{V.AmlLLocal{i}}:
1350	      V.AmlValue.type(in.ctx.local(H, w, i))
1351	    case V.AmlRef{V.AmlLArg{i}}:
1352	      V.AmlValue.type(in.ctx.arg(H, w, i))
1353	    case V.AmlRef{V.AmlLDebug{}}:
1354	      16
1355	    case _:
1356	      V.AmlValue.type(v)
1357	
1358	def in.ap.otype(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1359	  match args:
1360	    case Con{v, Nil{}}:
1361	      in.give(H, V.AmlInt{W.W64.from_u32(in.otype(H, v, w))}, c, fs, w)
1362	    case _:
1363	      in.bad(H, 142, c, fs, w)
1364	
1365	def in.condref.put(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, +v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1366	  match r:
1367	    case Fail{e}:
1368	      AmlMachine{AmlMFail{e}, c, fs, w}
1369	    case Done{l}:
1370	      in.then.give(H, in.put(~H, ~io, l, w, v), V.AmlInt{V.AmlInt.ones(in.wide(H, w))}, c, fs, w)
1371	
1372	# CondRefOf (chapter 19): Ones and the reference in the Target if the object
1373	# exists, Zero otherwise
1374	def in.ap.condref(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1375	  match args:
1376	    case Con{V.AmlRef{l}, Con{t, Nil{}}}:
1377	      in.condref.put(~H, ~io, in.loc(t), V.AmlRef{l}, c, fs, w)
1378	    case Con{x, Con{t, Nil{}}}:
1379	      in.give(H, V.AmlInt{W.W64.zero()}, c, fs, w)
1380	    case _:
1381	      in.bad(H, 274, c, fs, w)
1382	
1383	# Concatenate (chapter 19): by the first operand type
1384	
1385	def in.concat(+wide: Bool, a: V.AmlValue, +b: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1386	  match a:
1387	    case V.AmlInt{x}:
1388	      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, y => V.AmlBuf{B.Octets.append(V.val.int.bytes(wide, x), V.val.int.bytes(wide, y))}, V.AmlValue.to_int(wide, b))
1389	    case V.AmlStr{s}:
1390	      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlStr{B.Octets.append(s, t)}, V.AmlValue.to_str(wide, b))
1391	    case V.AmlBuf{s}:
1392	      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlBuf{B.Octets.append(s, t)}, V.AmlValue.to_buf(wide, b))
1393	    case _:
1394	      Fail{E.AcpiAmlBadType{"Concatenate of a value that is not an integer, string or buffer"}}
1395	
1396	def in.ap.concat(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1397	  match args:
1398	    case Con{a, Con{b, Con{t, Nil{}}}}:
1399	      in.store.give(~H, ~io, in.concat(in.wide(H, w), a, b), t, c, fs, w)
1400	    case _:
1401	      in.bad(H, 115, c, fs, w)
1402	
1403	# ToInteger, ToBuffer (chapter 19)
1404	
1405	def in.to_int(+wide: Bool, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1406	  match v:
1407	    case V.AmlStr{s}:
1408	      Done{V.AmlInt{V.AmlValue.parse_int(wide, B.Octets.to_list(s))}}
1409	    case _:
1410	      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{x}, V.AmlValue.to_int(wide, v))
1411	
1412	def in.conv.v(+op: Nat, +wide: Bool, a: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1413	  match op:
1414	    case 153n:
1415	      in.to_int(wide, a)
1416	    case _:
1417	      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, b => V.AmlBuf{b}, V.AmlValue.to_buf(wide, a))
1418	
1419	def in.ap.conv(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1420	  match args:
1421	    case Con{a, Con{t, Nil{}}}:
1422	      in.store.give(~H, ~io, in.conv.v(op, in.wide(H, w), a), t, c, fs, w)
1423	    case _:
1424	      in.bad(H, U32.from_nat(op), c, fs, w)
1425	
1426	# Notify (chapter 19; 5.6.6, device object notifications): recorded, for the caller
1427	
1428	def in.notify(-H: Data, t: V.AmlValue, r: Result<&2, &2, E.AcpiError, W.W64>, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
1429	  match t r:
1430	    case V.AmlRef{V.AmlLName{p}} Done{x}:
1431	      Done{in.note(H, w, AmlNote{p, x})}
1432	    case _ Fail{e}:
1433	      Fail{e}
1434	    case _ Done{x}:
1435	      Fail{E.AcpiAmlBadOperand{134}}
1436	
1437	def in.ap.notify(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1438	  match args:
1439	    case Con{t, Con{v, Nil{}}}:
1440	      in.then.give(H, in.notify(H, t, V.AmlValue.to_int(in.wide(H, w), v), w), V.AmlUninit{}, c, fs, w)
1441	    case _:
1442	      in.bad(H, 134, c, fs, w)
1443	
1444	# Sleep and Stall advance the clock Timer reads (by 10000 and 10 units of
1445	# 100 ns per millisecond and microsecond); nothing waits
1446	
1447	def in.sleep.go(-H: Data, r: Result<&2, &2, E.AcpiError, W.W64>, +per: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1448	  match r:
1449	    case Fail{e}:
1450	      AmlMachine{AmlMFail{e}, c, fs, w}
1451	    case Done{x}:
1452	      in.give(H, V.AmlUninit{}, c, fs, in.tick(H, w, W.W64.mul(x, W.W64.from_u32(per))))
1453	
1454	def in.ap.sleep(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +per: U32, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1455	  match args:
1456	    case Con{v, Nil{}}:
1457	      in.sleep.go(H, V.AmlValue.to_int(in.wide(H, w), v), per, c, fs, w)
1458	    case _:
1459	      in.bad(H, 290, c, fs, w)
1460	
1461	# Fatal (chapter 19)
1462	def in.ap.fatal(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1463	  match args:
1464	    case Con{V.AmlInt{t}, Con{V.AmlInt{k}, Con{v, Nil{}}}}:
1465	      AmlMachine{AmlMFail{E.AcpiAmlFatal{W.W64.lo(t), W.W64.lo(k), Result.default(&2, &2, E.AcpiError, W.W64, V.AmlValue.to_int(in.wide(H, w), v), W.W64.zero())}}, c, fs, w}
1466	    case _:
1467	      in.bad(H, 306, c, fs, w)
1468	
1469	# Definitions: Name, OperationRegion, Alias, External, Mutex, Event and the
1470	# CreateField family. A name already defined is AcpiAmlDuplicate.
1471	
1472	def in.path(v: V.AmlValue) -> String:
1473	  match v:
1474	    case V.AmlRef{V.AmlLName{p}}:
1475	      p
1476	    case _:
1477	      ""
1478	
1479	def in.def.chk(-H: Data, dup: Bool, +p: String, o: S.AmlObject, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1480	  match dup:
1481	    case True{}:
1482	      AmlMachine{AmlMFail{E.AcpiAmlDuplicate{p}}, c, fs, w}
1483	    case False{}:
1484	      in.give(H, V.AmlUninit{}, c, fs, in.define(H, w, p, o))
1485	
1486	def in.def.obj(-H: Data, +p: String, o: S.AmlObject, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1487	  in.def.chk(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, o, c, fs, w)
1488	
1489	def in.ap.name(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1490	  match args:
1491	    case Con{n, Con{v, Nil{}}}:
1492	      in.def.obj(H, in.path(n), S.AmlOData{v}, c, fs, w)
1493	    case _:
1494	      in.bad(H, 8, c, fs, w)
1495	
1496	def in.region.v(ro: Result<&2, &2, E.AcpiError, W.W64>, rl: Result<&2, &2, E.AcpiError, W.W64>, +sp: U32, +scope: String) -> Result<&2, &2, E.AcpiError, S.AmlObject>:
1497	  match ro rl:
1498	    case Done{o} Done{l}:
1499	      Done{S.AmlORegion{sp, o, l, scope}}
1500	    case Fail{e} _:
1501	      Fail{e}
1502	    case Done{o} Fail{e}:
1503	      Fail{e}
1504	
1505	def in.def.res(-H: Data, +p: String, r: Result<&2, &2, E.AcpiError, S.AmlObject>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1506	  match r:
1507	    case Fail{e}:
1508	      AmlMachine{AmlMFail{e}, c, fs, w}
1509	    case Done{o}:
1510	      in.def.obj(H, p, o, c, fs, w)
1511	
1512	def in.ap.region(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1513	  match args:
1514	    case Con{n, Con{V.AmlInt{sp}, Con{o, Con{l, Nil{}}}}}:
1515	      +wide = in.wide(H, w)
1516	      in.def.res(H, in.path(n), in.region.v(V.AmlValue.to_int(wide, o), V.AmlValue.to_int(wide, l), W.W64.lo(sp), in.scope(H, w)), c, fs, w)
1517	    case _:
1518	      in.bad(H, 384, c, fs, w)
1519	
1520	def in.ap.alias(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1521	  match args:
1522	    case Con{src, Con{dst, Nil{}}}:
1523	      in.def.obj(H, in.path(dst), S.AmlOAlias{in.path(src)}, c, fs, w)
1524	    case _:
1525	      in.bad(H, 6, c, fs, w)
1526	
1527	def in.ext.pick(-H: Data, has: Bool, +p: String, +k: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1528	  match has:
1529	    case True{}:
1530	      in.give(H, V.AmlUninit{}, c, fs, w)
1531	    case False{}:
1532	      in.give(H, V.AmlUninit{}, c, fs, in.define(H, w, p, S.AmlOExternal{k}))
1533	
1534	# External declares an object defined elsewhere; it defines nothing if the
1535	# object exists
1536	def in.ap.external(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1537	  match args:
1538	    case Con{n, Con{V.AmlInt{k}, Con{a, Nil{}}}}:
1539	      +p = in.path(n)
1540	      in.ext.pick(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, W.W64.lo(k), c, fs, w)
1541	    case _:
1542	      in.bad(H, 21, c, fs, w)
1543	
1544	def in.ap.mutex(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1545	  match args:
1546	    case Con{n, Con{V.AmlInt{s}, Nil{}}}:
1547	      in.def.obj(H, in.path(n), S.AmlOMutex{W.W64.lo(s)}, c, fs, w)
1548	    case Con{n, Nil{}}:
1549	      in.def.obj(H, in.path(n), S.AmlOEvent{}, c, fs, w)
1550	    case _:
1551	      in.bad(H, 257, c, fs, w)
1552	
1553	# CreateBitField, CreateByteField, CreateWordField, CreateDWordField,
1554	# CreateQWordField, CreateField: a buffer field of a buffer Name, Local or Arg
1555	
1556	def in.cf.size(+op: Nat) -> Nat:
1557	  match op:
1558	    case 141n:
1559	      1n
1560	    case 140n:
1561	      8n
1562	    case 139n:
1563	      16n
1564	    case 138n:
1565	      32n
1566	    case _:
1567	      64n
1568	
1569	def in.cf.off(+op: Nat, +i: Nat) -> Nat:
1570	  match op:
1571	    case 141n:
1572	      i
1573	    case 275n:
1574	      i
1575	    case _:
1576	      Nat.mul(i, 8n)
1577	
1578	def in.cf.bits(+op: Nat, +n: Nat) -> Nat:
1579	  match op:
1580	    case 275n:
1581	      n
1582	    case _:
1583	      in.cf.size(op)
1584	
1585	def in.cf.mk(+op: Nat, src: V.AmlValue, ri: Result<&2, &2, E.AcpiError, W.W64>, rn: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, S.AmlObject>:
1586	  match src ri rn:
1587	    case V.AmlRef{l} Done{+i} Done{n}:
1588	      Done{S.AmlOBufField{l, in.cf.off(op, W.W64.to_nat(i)), in.cf.bits(op, W.W64.to_nat(n))}}
1589	    case _ Fail{e} _:
1590	      Fail{e}
1591	    case _ Done{i} Fail{e}:
1592	      Fail{e}
1593	    case _ Done{i} Done{n}:
1594	      Fail{E.AcpiAmlUnsupported{"a buffer field of a buffer that has no name"}}
1595	
1596	def in.ap.create(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1597	  match args:
1598	    case Con{src, Con{i, Con{n, Nil{}}}}:
1599	      +wide = in.wide(H, w)
1600	      in.def.res(H, in.path(n), in.cf.mk(op, src, in.small.int(wide, i), Done{W.W64.zero()}), c, fs, w)
1601	    case Con{src, Con{i, Con{k, Con{n, Nil{}}}}}:
1602	      +wide = in.wide(H, w)
1603	      in.def.res(H, in.path(n), in.cf.mk(op, src, in.small.int(wide, i), in.small.int(wide, k)), c, fs, w)
1604	    case _:
1605	      in.bad(H, U32.from_nat(op), c, fs, w)
1606	
1607	# \_OSI (5.7.2): Ones if the operating system supports the feature named
1608	
1609	def in.osi.has(xs: List<&2, String>, +s: String) -> Bool:
1610	  match xs:
1611	    case Nil{}:
1612	      False{}
1613	    case Con{h, t}:
1614	      Bool.or(String.eq(h, s), in.osi.has(t, s))
1615	
1616	def in.opts.osi(o: AmlOptions) -> List<&2, String>:
1617	  match o:
1618	    case AmlOptions{osi, os, rev}:
1619	      osi
1620	
1621	def in.osi.v(+wide: Bool, +osi: List<&2, String>, r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1622	  match r:
1623	    case Fail{e}:
1624	      Fail{e}
1625	    case Done{s}:
1626	      Done{V.AmlInt{V.AmlInt.of_bool(wide, in.osi.has(osi, B.Octets.to_string(s)))}}
1627	
1628	def in.ap.osi(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1629	  match args:
1630	    case Con{v, Nil{}}:
1631	      +wide = in.wide(H, w)
1632	      in.val.give(H, in.osi.v(wide, in.opts.osi(in.opts(H, w)), V.AmlValue.to_str(wide, v)), c, fs, w)
1633	    case _:
1634	      in.bad(H, 0, c, fs, w)
1635	
1636	# Method calls and returns
1637	
1638	def in.mbody(o: Maybe<&2, S.AmlObject>) -> B.Octets:
1639	  match o:
1640	    case Some{S.AmlOMethod{n, f, b}}:
1641	      b
1642	    case _:
1643	      B.Octets.empty()
1644	
1645	def in.locals() -> List<&2, V.AmlValue>:
1646	  [V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}]
1647	
1648	# the method at p called with args: its body runs in its own scope, with
1649	# fresh Locals; FCall remembers where to come back
1650	def in.call(-H: Data, +p: String, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1651	  +body = B.Octets.to_list(in.mbody(S.AmlNs.get(AmlWorld.ns(H, w), p)))
1652	  AmlMachine{AmlMExec{}, AmlCur{body, B.len.fast(body)}, Con{AmlFCall{AmlWorld.ctx(H, w), c}, fs}, in.with_ctx(H, w, AmlCtx{p, args, in.locals(), Nil{}})}
1653	
1654	def in.drop.temps(ts: List<&2, String>, ns: S.AmlNs) -> S.AmlNs:
1655	  match ts:
1656	    case Nil{}:
1657	      ns
1658	    case Con{t, rest}:
1659	      in.drop.temps(rest, S.AmlNs.remove(ns, t))
1660	
1661	def in.temps(c: AmlCtx) -> List<&2, String>:
1662	  match c:
1663	    case AmlCtx{s, a, l, t}:
1664	      t
1665	
1666	# back from a method: its names removed, the caller context restored
1667	def in.back(-H: Data, w: AmlWorld<H>, saved: AmlCtx) -> AmlWorld<H>:
1668	  match w:
1669	    case AmlWorld{c, n, h, e}:
1670	      AmlWorld{saved, in.drop.temps(in.temps(c), n), h, e}
1671	
1672	# Return: frames dropped to the method call (or the bottom)
1673	def in.unwind.ret(-H: Data, fs: List<&2, AmlFrame>, v: V.AmlValue, w: AmlWorld<H>) -> AmlMachine<H>:
1674	  match fs:
1675	    case Nil{}:
1676	      AmlMachine{AmlMDone{v}, in.no.cur(), Nil{}, w}
1677	    case Con{AmlFCall{saved, back}, rest}:
1678	      AmlMachine{AmlMGive{v}, back, rest, in.back(H, w, saved)}
1679	    case Con{AmlFTop{}, rest}:
1680	      AmlMachine{AmlMDone{v}, in.no.cur(), [AmlFTop{}], w}
1681	    case Con{f, rest}:
1682	      in.unwind.ret(H, rest, v, w)
1683	
1684	# Break: frames dropped to the While, then on after it
1685	def in.unwind.brk(-H: Data, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
1686	  match fs:
1687	    case Nil{}:
1688	      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), Nil{}, w}
1689	    case Con{AmlFWhile{s, after, b}, rest}:
1690	      AmlMachine{AmlMExec{}, after, rest, w}
1691	    case Con{AmlFCall{saved, back}, rest}:
1692	      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, back, rest, w}
1693	    case Con{AmlFTop{}, rest}:
1694	      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), rest, w}
1695	    case Con{f, rest}:
1696	      in.unwind.brk(H, rest, w)
1697	
1698	# Continue: frames dropped to the While, whose predicate is read again
1699	def in.unwind.cont(-H: Data, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
1700	  match fs:
1701	    case Nil{}:
1702	      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), Nil{}, w}
1703	    case Con{AmlFWhile{+s, after, b}, rest}:
1704	      AmlMachine{AmlMEval{AmlKTerm{}}, s, Con{AmlFWhile{s, after, False{}}, rest}, w}
1705	    case Con{AmlFCall{saved, back}, rest}:
1706	      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, back, rest, w}
1707	    case Con{AmlFTop{}, rest}:
1708	      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), rest, w}
1709	    case Con{f, rest}:
1710	      in.unwind.cont(H, rest, w)
1711	
1712	def in.ap.ret(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1713	  match args:
1714	    case Con{v, Nil{}}:
1715	      in.unwind.ret(H, fs, v, w)
1716	    case _:
1717	      in.bad(H, 164, c, fs, w)
1718	
1719	# Operators: what each opcode takes (an extended opcode 0x5B xx is 256 + xx)
1720	
1721	def in.kT() -> AmlArgK:
1722	  AmlKTerm{}
1723	
1724	def in.kG() -> AmlArgK:
1725	  AmlKTarget{}
1726	
1727	def in.kS() -> AmlArgK:
1728	  AmlKBase{}
1729	
1730	def in.kN() -> AmlArgK:
1731	  AmlKName{}
1732	
1733	def in.kY() -> AmlArgK:
1734	  AmlKByte{}
1735	
1736	def in.tt.g() -> List<&2, AmlArgK>:
1737	  [in.kT(), in.kT(), in.kG()]
1738	
1739	def in.t.g() -> List<&2, AmlArgK>:
1740	  [in.kT(), in.kG()]
1741	
1742	def in.kinds(+op: Nat) -> Maybe<&2, List<&2, AmlArgK>>:
1743	  match op:
1744	    case 6n:
1745	      Some{[in.kG(), in.kN()]}
1746	    case 8n:
1747	      Some{[in.kN(), in.kT()]}
1748	    case 21n:
1749	      Some{[in.kN(), in.kY(), in.kY()]}
1750	    case 112n:
1751	      Some{in.t.g()}
1752	    case 113n:
1753	      Some{[in.kG()]}
1754	    case 114n:
1755	      Some{in.tt.g()}
1756	    case 115n:
1757	      Some{in.tt.g()}
1758	    case 116n:
1759	      Some{in.tt.g()}
1760	    case 117n:
1761	      Some{[in.kG()]}
1762	    case 118n:
1763	      Some{[in.kG()]}
1764	    case 119n:
1765	      Some{in.tt.g()}
1766	    case 120n:
1767	      Some{[in.kT(), in.kT(), in.kG(), in.kG()]}
1768	    case 121n:
1769	      Some{in.tt.g()}
1770	    case 122n:
1771	      Some{in.tt.g()}
1772	    case 123n:
1773	      Some{in.tt.g()}
1774	    case 124n:
1775	      Some{in.tt.g()}
1776	    case 125n:
1777	      Some{in.tt.g()}
1778	    case 126n:
1779	      Some{in.tt.g()}
1780	    case 127n:
1781	      Some{in.tt.g()}
1782	    case 128n:
1783	      Some{in.t.g()}
1784	    case 129n:
1785	      Some{in.t.g()}
1786	    case 130n:
1787	      Some{in.t.g()}
1788	    case 131n:
1789	      Some{[in.kT()]}
1790	    case 133n:
1791	      Some{in.tt.g()}
1792	    case 134n:
1793	      Some{[in.kG(), in.kT()]}
1794	    case 135n:
1795	      Some{[in.kS()]}
1796	    case 136n:
1797	      Some{[in.kS(), in.kT(), in.kG()]}
1798	    case 138n:
1799	      Some{[in.kS(), in.kT(), in.kN()]}
1800	    case 139n:
1801	      Some{[in.kS(), in.kT(), in.kN()]}
1802	    case 140n:
1803	      Some{[in.kS(), in.kT(), in.kN()]}
1804	    case 141n:
1805	      Some{[in.kS(), in.kT(), in.kN()]}
1806	    case 142n:
1807	      Some{[in.kS()]}
1808	    case 143n:
1809	      Some{[in.kS(), in.kT(), in.kN()]}
1810	    case 144n:
1811	      Some{[in.kT(), in.kT()]}
1812	    case 145n:
1813	      Some{[in.kT(), in.kT()]}
1814	    case 146n:
1815	      Some{[in.kT()]}
1816	    case 147n:
1817	      Some{[in.kT(), in.kT()]}
1818	    case 148n:
1819	      Some{[in.kT(), in.kT()]}
1820	    case 149n:
1821	      Some{[in.kT(), in.kT()]}
1822	    case 150n:
1823	      Some{in.t.g()}
1824	    case 153n:
1825	      Some{in.t.g()}
1826	    case 157n:
1827	      Some{in.t.g()}
1828	    case 164n:
1829	      Some{[in.kT()]}
1830	    case 257n:
1831	      Some{[in.kN(), in.kY()]}
1832	    case 258n:
1833	      Some{[in.kN()]}
1834	    case 274n:
1835	      Some{[AmlKCond{}, in.kG()]}
1836	    case 275n:
1837	      Some{[in.kS(), in.kT(), in.kT(), in.kN()]}
1838	    case 289n:
1839	      Some{[in.kT()]}
1840	    case 290n:
1841	      Some{[in.kT()]}
1842	    case 291n:
1843	      Some{[in.kG(), AmlKWord{}]}
1844	    case 292n:
1845	      Some{[in.kG()]}
1846	    case 293n:
1847	      Some{[in.kG(), in.kT()]}
1848	    case 294n:
1849	      Some{[in.kG()]}
1850	    case 295n:
1851	      Some{[in.kG()]}
1852	    case 304n:
1853	      Some{Nil{}}
1854	    case 306n:
1855	      Some{[in.kY(), AmlKDWord{}, in.kT()]}
1856	    case 307n:
1857	      Some{Nil{}}
1858	    case 384n:
1859	      Some{[in.kN(), in.kY(), in.kT(), in.kT()]}
1860	    case _:
1861	      None{}
1862	
1863	# the operators that are statements: refused where a value is wanted
1864	def in.is_stmt(+op: Nat) -> Bool:
1865	  match op:
1866	    case 6n:
1867	      True{}
1868	    case 8n:
1869	      True{}
1870	    case 21n:
1871	      True{}
1872	    case 134n:
1873	      True{}
1874	    case 138n:
1875	      True{}
1876	    case 139n:
1877	      True{}
1878	    case 140n:
1879	      True{}
1880	    case 141n:
1881	      True{}
1882	    case 143n:
1883	      True{}
1884	    case 164n:
1885	      True{}
1886	    case 257n:
1887	      True{}
1888	    case 258n:
1889	      True{}
1890	    case 275n:
1891	      True{}
1892	    case 289n:
1893	      True{}
1894	    case 290n:
1895	      True{}
1896	    case 292n:
1897	      True{}
1898	    case 294n:
1899	      True{}
1900	    case 295n:
1901	      True{}
1902	    case 306n:
1903	      True{}
1904	    case 384n:
1905	      True{}
1906	    case _:
1907	      False{}
1908	
1909	def in.refof(args: List<&2, V.AmlValue>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1910	  match args:
1911	    case Con{t, Nil{}}:
1912	      Done{t}
1913	    case _:
1914	      Fail{E.AcpiAmlBadOperand{113}}
1915	
1916	def in.apply.code(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +code: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1917	  match code:
1918	    case 6n:
1919	      in.ap.alias(~H, ~io, args, c, fs, w)
1920	    case 8n:
1921	      in.ap.name(~H, ~io, args, c, fs, w)
1922	    case 21n:
1923	      in.ap.external(~H, ~io, args, c, fs, w)
1924	    case 112n:
1925	      in.ap.store(~H, ~io, args, c, fs, w)
1926	    case 113n:
1927	      in.val.give(H, in.refof(args), c, fs, w)
1928	    case 114n:
1929	      in.ap.int2(~H, ~io, 114n, args, c, fs, w)
1930	    case 115n:
1931	      in.ap.concat(~H, ~io, args, c, fs, w)
1932	    case 116n:
1933	      in.ap.int2(~H, ~io, 116n, args, c, fs, w)
1934	    case 117n:
1935	      in.ap.incdec(~H, ~io, True{}, args, c, fs, w)
1936	    case 118n:
1937	      in.ap.incdec(~H, ~io, False{}, args, c, fs, w)
1938	    case 119n:
1939	      in.ap.int2(~H, ~io, 119n, args, c, fs, w)
1940	    case 120n:
1941	      in.ap.div(~H, ~io, args, c, fs, w)
1942	    case 121n:
1943	      in.ap.int2(~H, ~io, 121n, args, c, fs, w)
1944	    case 122n:
1945	      in.ap.int2(~H, ~io, 122n, args, c, fs, w)
1946	    case 123n:
1947	      in.ap.int2(~H, ~io, 123n, args, c, fs, w)
1948	    case 124n:
1949	      in.ap.int2(~H, ~io, 124n, args, c, fs, w)
1950	    case 125n:
1951	      in.ap.int2(~H, ~io, 125n, args, c, fs, w)
1952	    case 126n:
1953	      in.ap.int2(~H, ~io, 126n, args, c, fs, w)
1954	    case 127n:
1955	      in.ap.int2(~H, ~io, 127n, args, c, fs, w)
1956	    case 128n:
1957	      in.ap.int1(~H, ~io, 128n, args, c, fs, w)
1958	    case 129n:
1959	      in.ap.int1(~H, ~io, 129n, args, c, fs, w)
1960	    case 130n:
1961	      in.ap.int1(~H, ~io, 130n, args, c, fs, w)
1962	    case 131n:
1963	      in.ap.deref(~H, ~io, args, c, fs, w)
1964	    case 133n:
1965	      in.ap.int2(~H, ~io, 133n, args, c, fs, w)
1966	    case 134n:
1967	      in.ap.notify(~H, ~io, args, c, fs, w)
1968	    case 135n:
1969	      in.ap.size(~H, ~io, args, c, fs, w)
1970	    case 136n:
1971	      in.ap.index(~H, ~io, args, c, fs, w)
1972	    case 138n:
1973	      in.ap.create(~H, ~io, 138n, args, c, fs, w)
1974	    case 139n:
1975	      in.ap.create(~H, ~io, 139n, args, c, fs, w)
1976	    case 140n:
1977	      in.ap.create(~H, ~io, 140n, args, c, fs, w)
1978	    case 141n:
1979	      in.ap.create(~H, ~io, 141n, args, c, fs, w)
1980	    case 142n:
1981	      in.ap.otype(~H, ~io, args, c, fs, w)
1982	    case 143n:
1983	      in.ap.create(~H, ~io, 143n, args, c, fs, w)
1984	    case 144n:
1985	      in.ap.logic(~H, ~io, 144n, args, c, fs, w)
1986	    case 145n:
1987	      in.ap.logic(~H, ~io, 145n, args, c, fs, w)
1988	    case 146n:
1989	      in.ap.logic(~H, ~io, 146n, args, c, fs, w)
1990	    case 147n:
1991	      in.ap.logic(~H, ~io, 147n, args, c, fs, w)
1992	    case 148n:
1993	      in.ap.logic(~H, ~io, 148n, args, c, fs, w)
1994	    case 149n:
1995	      in.ap.logic(~H, ~io, 149n, args, c, fs, w)
1996	    case 150n:
1997	      in.ap.conv(~H, ~io, 150n, args, c, fs, w)
1998	    case 153n:
1999	      in.ap.conv(~H, ~io, 153n, args, c, fs, w)
2000	    case 157n:
Lines 1-2000 of 2945. More: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_interp.bend&start_line=2001