source: extracted/interpret.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

File size: 242.2 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Sets
6
7open Bool
8
9open Relations
10
11open Nat
12
13open Hints_declaration
14
15open Core_notation
16
17open Pts
18
19open Logic
20
21open Types
22
23open List
24
25open Listb
26
27open BitVectorTrie
28
29open String
30
31open LabelledObjects
32
33open Arithmetic
34
35open Integers
36
37open AST
38
39open CostLabel
40
41open Proper
42
43open PositiveMap
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Lists
60
61open Positive
62
63open Identifiers
64
65open Extranat
66
67open Vector
68
69open Div_and_mod
70
71open Jmeq
72
73open Russell
74
75open Util
76
77open FoldStuff
78
79open BitVector
80
81open ASM
82
83open Status
84
85open StatusProofs
86
87open Fetch
88
89open StructuredTraces
90
91open AbstractStatus
92
93(** val execute_1_preinstruction :
94    (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
95    BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
96    Status.preStatus **)
97let execute_1_preinstruction ticks cm addr_of instr s =
98  let add_ticks1 = fun s0 ->
99    Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
100  in
101  let add_ticks2 = fun s0 ->
102    Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
103  in
104  (match instr with
105   | ASM.ADD (addr1, addr2) ->
106     (fun _ ->
107       let s0 = add_ticks1 s in
108       let { Types.fst = result; Types.snd = flags } =
109         Arithmetic.add_8_with_carry
110           (Status.get_arg_8 cm s0 Bool.False
111             (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
112               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
113               Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
114               Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
115               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
116               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
117               (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
118               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
119               Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
120               (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
121               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
122               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
123               ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
124               ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
125               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
126               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
127               Vector.VEmpty)))))))))))))))))))) addr1))
128           (Status.get_arg_8 cm s0 Bool.False
129             (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
130               (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
132               ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
133               ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
134               Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
135               Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
136               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
137               ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
138               (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
139               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
140               (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
141               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
142               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
143               ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
144               Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
145               Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
146               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
147               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
148               Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False
149       in
150       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
151       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
152       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
153       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
154       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)
155   | ASM.ADDC (addr1, addr2) ->
156     (fun _ ->
157       let s0 = add_ticks1 s in
158       let old_cy_flag = Status.get_cy_flag cm s0 in
159       let { Types.fst = result; Types.snd = flags } =
160         Arithmetic.add_8_with_carry
161           (Status.get_arg_8 cm s0 Bool.False
162             (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
163               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
164               Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
165               Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
166               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
167               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
168               (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
169               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
170               Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
171               (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
172               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
173               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
174               ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
175               ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
176               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
177               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
178               Vector.VEmpty)))))))))))))))))))) addr1))
179           (Status.get_arg_8 cm s0 Bool.False
180             (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
181               (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
182               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
183               ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
184               ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
185               Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
186               Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
187               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
188               ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
189               (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
190               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
191               (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
192               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
193               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
194               ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
195               Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
196               Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
197               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
198               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
199               Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
200       in
201       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
202       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
203       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
204       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
205       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)
206   | ASM.SUBB (addr1, addr2) ->
207     (fun _ ->
208       let s0 = add_ticks1 s in
209       let old_cy_flag = Status.get_cy_flag cm s0 in
210       let { Types.fst = result; Types.snd = flags } =
211         Arithmetic.sub_8_with_carry
212           (Status.get_arg_8 cm s0 Bool.False
213             (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
214               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
215               Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
216               Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
217               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
218               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
219               (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
220               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
221               Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
222               (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
223               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
224               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
225               ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
226               ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
227               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
228               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
229               Vector.VEmpty)))))))))))))))))))) addr1))
230           (Status.get_arg_8 cm s0 Bool.False
231             (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
232               (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
233               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
234               ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
235               ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
236               Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
237               Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
238               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
239               ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
240               (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
241               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
242               (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
243               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
244               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
245               ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
246               Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
247               Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
248               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
249               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
250               Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
251       in
252       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
253       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
254       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
255       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
256       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)
257   | ASM.INC addr ->
258     (fun _ ->
259       (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
260                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
261                ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
262                ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
263                ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
264                (Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with
265        | ASM.DIRECT d ->
266          (fun _ ->
267            let s' = add_ticks1 s in
268            let result =
269              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
270                (Nat.S Nat.O))))))))
271                (Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d))
272                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
273                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
274            in
275            Status.set_arg_8 cm s' (ASM.DIRECT d) result)
276        | ASM.INDIRECT i ->
277          (fun _ ->
278            let s' = add_ticks1 s in
279            let result =
280              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
281                (Nat.S Nat.O))))))))
282                (Status.get_arg_8 cm s' Bool.True (ASM.INDIRECT i))
283                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
284                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
285            in
286            Status.set_arg_8 cm s' (ASM.INDIRECT i) result)
287        | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
288        | ASM.REGISTER r ->
289          (fun _ ->
290            let s' = add_ticks1 s in
291            let result =
292              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
293                (Nat.S Nat.O))))))))
294                (Status.get_arg_8 cm s' Bool.True (ASM.REGISTER r))
295                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
296                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
297            in
298            Status.set_arg_8 cm s' (ASM.REGISTER r) result)
299        | ASM.ACC_A ->
300          (fun _ ->
301            let s' = add_ticks1 s in
302            let result =
303              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
304                (Nat.S Nat.O))))))))
305                (Status.get_arg_8 cm s' Bool.True ASM.ACC_A)
306                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
307                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
308            in
309            Status.set_arg_8 cm s' ASM.ACC_A result)
310        | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
311        | ASM.DPTR ->
312          (fun _ ->
313            let s' = add_ticks1 s in
314            let { Types.fst = carry; Types.snd = bl } =
315              Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
316                (Nat.S (Nat.S Nat.O))))))))
317                (Status.get_8051_sfr cm s' Status.SFR_DPL)
318                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
319                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
320            in
321            let { Types.fst = carry0; Types.snd = bu } =
322              Arithmetic.full_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
323                (Nat.S (Nat.S Nat.O))))))))
324                (Status.get_8051_sfr cm s' Status.SFR_DPH)
325                (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
326                  (Nat.S (Nat.S Nat.O))))))))) carry
327            in
328            let s0 = Status.set_8051_sfr cm s' Status.SFR_DPL bl in
329            Status.set_8051_sfr cm s' Status.SFR_DPH bu)
330        | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
331        | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
332        | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
333        | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
334        | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
335        | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
336        | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
337        | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
338        | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
339        | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
340        | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
341        | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
342   | ASM.DEC addr ->
343     (fun _ ->
344       let s0 = add_ticks1 s in
345       let { Types.fst = result; Types.snd = flags } =
346         Arithmetic.sub_8_with_carry
347           (Status.get_arg_8 cm s0 Bool.True
348             (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
349               (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
350               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
351               ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons
352               ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S
353               Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
354               Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
355               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
356               ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
357               (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
358               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
359               (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
360               (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
361               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
362               ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
363               Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
364               Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
365               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
366               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
367               Vector.VEmpty)))))))))))))))))))) addr))
368           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
369             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
370       in
371       Status.set_arg_8 cm s0
372         (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
373           (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
374           Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
375           ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr,
376           (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O,
377           ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S
378           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
379           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
380           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
381           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
382           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
383           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
384           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) result)
385   | ASM.MUL (addr1, addr2) ->
386     (fun _ ->
387       let s0 = add_ticks1 s in
388       let acc_a_nat =
389         Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
390           (Nat.S (Nat.S (Nat.S Nat.O))))))))
391           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
392       in
393       let acc_b_nat =
394         Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
395           (Nat.S (Nat.S (Nat.S Nat.O))))))))
396           (Status.get_8051_sfr cm s0 Status.SFR_ACC_B)
397       in
398       let product = Nat.times acc_a_nat acc_b_nat in
399       let low =
400         Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
401           (Nat.S (Nat.S (Nat.S Nat.O))))))))
402           (Util.modulus product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
403             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
404             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
405             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
406             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
407             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
408             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
409             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
410             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
411             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
412             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
413             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
414             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
415             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
416             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
417             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
418             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
419             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
420             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
421             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
422             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
423             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
424             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
425             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
426             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
427             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
428             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
429             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
430             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
431             Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
432       in
433       let high =
434         Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
435           (Nat.S (Nat.S (Nat.S Nat.O))))))))
436           (Util.division product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
437             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
438             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
439             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
440             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
443             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
444             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
445             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
446             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
447             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
448             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
449             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
450             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
451             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
452             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
453             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
454             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
455             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
456             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
457             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
458             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
459             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
460             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
461             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
462             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
463             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
464             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
465             Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
466       in
467       let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A low in
468       Status.set_8051_sfr cm s1 Status.SFR_ACC_B high)
469   | ASM.DIV (addr1, addr2) ->
470     (fun _ ->
471       let s0 = add_ticks1 s in
472       let acc_a_nat =
473         Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
474           (Nat.S (Nat.S (Nat.S Nat.O))))))))
475           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
476       in
477       let acc_b_nat =
478         Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
479           (Nat.S (Nat.S (Nat.S Nat.O))))))))
480           (Status.get_8051_sfr cm s0 Status.SFR_ACC_B)
481       in
482       (match acc_b_nat with
483        | Nat.O -> Status.set_flags cm s0 Bool.False Types.None Bool.True
484        | Nat.S o ->
485          let q =
486            Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
487              (Nat.S (Nat.S (Nat.S Nat.O))))))))
488              (Util.division acc_a_nat (Nat.S o))
489          in
490          let r =
491            Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
492              (Nat.S (Nat.S (Nat.S Nat.O))))))))
493              (Util.modulus acc_a_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
494                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
495                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
496                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
497                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
498                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
499                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
500                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
501                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
502                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
503                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
504                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
505                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
506                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
507                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
508                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
509                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
510                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
511                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
512                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
513                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
514                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
515                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
516                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
519                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
520                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
521                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
522                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
523                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
524                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
525                (Nat.S (Nat.S (Nat.S
526                Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
527          in
528          let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A q in
529          let s2 = Status.set_8051_sfr cm s1 Status.SFR_ACC_B r in
530          Status.set_flags cm s2 Bool.False Types.None Bool.False))
531   | ASM.DA addr ->
532     (fun _ ->
533       let s0 = add_ticks1 s in
534       let { Types.fst = acc_nu; Types.snd = acc_nl } =
535         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
536           (Nat.S (Nat.S Nat.O))))
537           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
538       in
539       (match Bool.orb
540                (Util.gtb
541                  (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S
542                    Nat.O)))) acc_nl) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
543                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
544                (Status.get_ac_flag cm s0) with
545        | Bool.True ->
546          let { Types.fst = result; Types.snd = flags } =
547            Arithmetic.add_8_with_carry
548              (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
549              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
550                (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
551                (Nat.S (Nat.S (Nat.S Nat.O))))))) Bool.False
552          in
553          let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags
554          in
555          let { Types.fst = acc_nu'; Types.snd = acc_nl' } =
556            Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
557              (Nat.S (Nat.S Nat.O)))) result
558          in
559          (match Bool.orb
560                   (Util.gtb
561                     (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S
562                       Nat.O)))) acc_nu') (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
563                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) cy_flag with
564           | Bool.True ->
565             let nu =
566               Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu'
567                 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
568                   Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
569                   Nat.O)))))))
570             in
571             let new_acc =
572               Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S
573                 (Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl'
574             in
575             let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in
576             Status.set_flags cm s1 cy_flag (Types.Some
577               (Status.get_ac_flag cm s1)) (Status.get_ov_flag cm s1)
578           | Bool.False -> s0)
579        | Bool.False -> s0))
580   | ASM.JC addr ->
581     (fun _ ->
582       match Status.get_cy_flag cm s with
583       | Bool.True ->
584         let s0 = add_ticks1 s in
585         Status.set_program_counter cm s0 (addr_of addr s0)
586       | Bool.False -> let s0 = add_ticks2 s in s0)
587   | ASM.JNC addr ->
588     (fun _ ->
589       match Bool.notb (Status.get_cy_flag cm s) with
590       | Bool.True ->
591         let s0 = add_ticks1 s in
592         Status.set_program_counter cm s0 (addr_of addr s0)
593       | Bool.False -> let s0 = add_ticks2 s in s0)
594   | ASM.JB (addr1, addr2) ->
595     (fun _ ->
596       match Status.get_arg_1 cm s
597               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
598                 (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
599                 Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
600                 ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
601                 (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1)
602               Bool.False with
603       | Bool.True ->
604         let s0 = add_ticks1 s in
605         Status.set_program_counter cm s0 (addr_of addr2 s0)
606       | Bool.False -> let s0 = add_ticks2 s in s0)
607   | ASM.JNB (addr1, addr2) ->
608     (fun _ ->
609       match Bool.notb
610               (Status.get_arg_1 cm s
611                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
612                   (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
613                   Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
614                   ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
615                   ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
616                   Vector.VEmpty)))))) addr1) Bool.False) with
617       | Bool.True ->
618         let s0 = add_ticks1 s in
619         Status.set_program_counter cm s0 (addr_of addr2 s0)
620       | Bool.False -> let s0 = add_ticks2 s in s0)
621   | ASM.JBC (addr1, addr2) ->
622     (fun _ ->
623       let s0 =
624         Status.set_arg_1 cm s
625           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
626             Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))
627             (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons
628             (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) Bool.False
629       in
630       (match Status.get_arg_1 cm s0
631                (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
632                  (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
633                  Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
634                  ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
635                  (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1)
636                Bool.False with
637        | Bool.True ->
638          let s1 = add_ticks1 s0 in
639          Status.set_program_counter cm s1 (addr_of addr2 s1)
640        | Bool.False -> let s1 = add_ticks2 s0 in s1))
641   | ASM.JZ addr ->
642     (fun _ ->
643       match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
644               (Nat.S Nat.O))))))))
645               (Status.get_8051_sfr cm s Status.SFR_ACC_A)
646               (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
647                 (Nat.S (Nat.S Nat.O))))))))) with
648       | Bool.True ->
649         let s0 = add_ticks1 s in
650         Status.set_program_counter cm s0 (addr_of addr s0)
651       | Bool.False -> let s0 = add_ticks2 s in s0)
652   | ASM.JNZ addr ->
653     (fun _ ->
654       match Bool.notb
655               (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
656                 (Nat.S (Nat.S Nat.O))))))))
657                 (Status.get_8051_sfr cm s Status.SFR_ACC_A)
658                 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
659                   (Nat.S (Nat.S Nat.O)))))))))) with
660       | Bool.True ->
661         let s0 = add_ticks1 s in
662         Status.set_program_counter cm s0 (addr_of addr s0)
663       | Bool.False -> let s0 = add_ticks2 s in s0)
664   | ASM.CJNE (addr1, addr2) ->
665     (fun _ ->
666       match addr1 with
667       | Types.Inl l ->
668         let { Types.fst = addr10; Types.snd = addr2' } = l in
669         let new_cy =
670           Util.ltb
671             (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
672               (Nat.S (Nat.S (Nat.S Nat.O))))))))
673               (Status.get_arg_8 cm s Bool.False
674                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
675                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
676                   (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
677                   Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
678                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
679                   ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
680                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
681                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
682                   (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
683                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
684                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
685                   Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
686                   (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
687                   (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
688                   (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
689                   ASM.Ext_indirect, (Vector.VCons (Nat.O,
690                   ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
691                   addr10)))
692             (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
693               (Nat.S (Nat.S (Nat.S Nat.O))))))))
694               (Status.get_arg_8 cm s Bool.False
695                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
696                   Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
697                   (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
698                   ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
699                   Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
700                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
701                   ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
702                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
703                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
704                   (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
705                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
706                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
707                   Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
708                   (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
709                   (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
710                   (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
711                   ASM.Ext_indirect, (Vector.VCons (Nat.O,
712                   ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
713                   addr2')))
714         in
715         (match Bool.notb
716                  (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
717                    (Nat.S (Nat.S Nat.O))))))))
718                    (Status.get_arg_8 cm s Bool.False
719                      (ASM.subaddressing_modeel__o__mk_subaddressing_mode
720                        Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
721                        (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
722                        (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons
723                        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
724                        (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
725                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
726                        (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
727                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
728                        (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
729                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
730                        (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S
731                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
732                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
733                        ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
734                        Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
735                        Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
736                        ASM.Ext_indirect, (Vector.VCons (Nat.O,
737                        ASM.Ext_indirect_dptr,
738                        Vector.VEmpty)))))))))))))))))))) addr10))
739                    (Status.get_arg_8 cm s Bool.False
740                      (ASM.subaddressing_modeel__o__mk_subaddressing_mode
741                        (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
742                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
743                        (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
744                        (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty))))
745                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
746                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
747                        ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
748                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
749                        ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
750                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
751                        ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
752                        (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
753                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
754                        Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
755                        (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
756                        ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr,
757                        (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
758                        (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
759                        (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
760                        Vector.VEmpty)))))))))))))))))))) addr2'))) with
761          | Bool.True ->
762            let s0 = add_ticks1 s in
763            let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in
764            Status.set_flags cm s1 new_cy Types.None
765              (Status.get_ov_flag cm s1)
766          | Bool.False ->
767            let s0 = add_ticks2 s in
768            Status.set_flags cm s0 new_cy Types.None
769              (Status.get_ov_flag cm s0))
770       | Types.Inr r' ->
771         let { Types.fst = addr10; Types.snd = addr2' } = r' in
772         let new_cy =
773           Util.ltb
774             (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
775               (Nat.S (Nat.S (Nat.S Nat.O))))))))
776               (Status.get_arg_8 cm s Bool.False
777                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
778                   Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
779                   (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
780                   ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
781                   Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
782                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
783                   ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
784                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
785                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
786                   (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
787                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
788                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
789                   Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
790                   (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
791                   (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
792                   (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
793                   ASM.Ext_indirect, (Vector.VCons (Nat.O,
794                   ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
795                   addr10)))
796             (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
797               (Nat.S (Nat.S (Nat.S Nat.O))))))))
798               (Status.get_arg_8 cm s Bool.False
799                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
800                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
801                   (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Data,
802                   Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
803                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
804                   ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
805                   (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
806                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
807                   (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
808                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
809                   (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
810                   Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
811                   (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
812                   (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
813                   (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
814                   ASM.Ext_indirect, (Vector.VCons (Nat.O,
815                   ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
816                   addr2')))
817         in
818         (match Bool.notb
819                  (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
820                    (Nat.S (Nat.S Nat.O))))))))
821                    (Status.get_arg_8 cm s Bool.False
822                      (ASM.subaddressing_modeel__o__mk_subaddressing_mode
823                        (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
824                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
825                        (Vector.VCons ((Nat.S Nat.O), ASM.Registr,
826                        (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty))))
827                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
828                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
829                        ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
830                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
831                        ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
832                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
833                        ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
834                        (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
835                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
836                        Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
837                        (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
838                        ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr,
839                        (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
840                        (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
841                        (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
842                        Vector.VEmpty)))))))))))))))))))) addr10))
843                    (Status.get_arg_8 cm s Bool.False
844                      (ASM.subaddressing_modeel__o__mk_subaddressing_mode
845                        Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
846                        (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
847                        (Nat.O, ASM.Data, Vector.VEmpty)) (Vector.VCons
848                        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
849                        (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
850                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
851                        (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
852                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
853                        (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
854                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
855                        (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S
856                        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
857                        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
858                        ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
859                        Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
860                        Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
861                        ASM.Ext_indirect, (Vector.VCons (Nat.O,
862                        ASM.Ext_indirect_dptr,
863                        Vector.VEmpty)))))))))))))))))))) addr2'))) with
864          | Bool.True ->
865            let s0 = add_ticks1 s in
866            let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in
867            Status.set_flags cm s1 new_cy Types.None
868              (Status.get_ov_flag cm s1)
869          | Bool.False ->
870            let s0 = add_ticks2 s in
871            Status.set_flags cm s0 new_cy Types.None
872              (Status.get_ov_flag cm s0)))
873   | ASM.DJNZ (addr1, addr2) ->
874     (fun _ ->
875       let { Types.fst = result; Types.snd = flags } =
876         Arithmetic.sub_8_with_carry
877           (Status.get_arg_8 cm s Bool.True
878             (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
879               Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
880               (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
881               ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct,
882               Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
883               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
884               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
885               (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
886               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
887               Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
888               (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
889               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
890               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
891               ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
892               ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
893               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
894               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
895               Vector.VEmpty)))))))))))))))))))) addr1))
896           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
897             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
898       in
899       let s0 =
900         Status.set_arg_8 cm s
901           (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
902             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
903             (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O,
904             ASM.Direct, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S
905             (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
906             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
907             ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
908             Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
909             Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
910             ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
911             (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
912             Vector.VEmpty)))))))))))))) addr1) result
913       in
914       (match Bool.notb
915                (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
916                  (Nat.S (Nat.S Nat.O)))))))) result
917                  (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
918                    (Nat.S (Nat.S Nat.O)))))))))) with
919        | Bool.True ->
920          let s1 = add_ticks1 s0 in
921          Status.set_program_counter cm s1 (addr_of addr2 s1)
922        | Bool.False -> let s1 = add_ticks2 s0 in s1))
923   | ASM.ANL addr ->
924     (fun _ ->
925       let s0 = add_ticks1 s in
926       (match addr with
927        | Types.Inl l ->
928          (match l with
929           | Types.Inl l' ->
930             let { Types.fst = addr1; Types.snd = addr2 } = l' in
931             let and_val =
932               BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
933                 (Nat.S (Nat.S (Nat.S Nat.O))))))))
934                 (Status.get_arg_8 cm s0 Bool.True
935                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
936                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
937                     (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
938                     Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
939                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
940                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
941                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
942                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
943                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
944                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
945                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
946                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
947                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
948                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
949                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
950                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
951                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
952                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
953                     addr1))
954                 (Status.get_arg_8 cm s0 Bool.True
955                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
956                     (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
957                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
958                     (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
959                     ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
960                     ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
961                     (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty))))))))
962                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
963                     (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
964                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
965                     (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
966                     ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
967                     Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
968                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
969                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
970                     Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
971                     (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S
972                     (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
973                     ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons
974                     ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
975                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
976                     addr2))
977             in
978             Status.set_arg_8 cm s0
979               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
980                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
981                 (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty))
982                 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
983                 Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
984                 (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
985                 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
986                 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
987                 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
988                 (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
989                 (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
990                 Vector.VEmpty)))))))))))))) addr1) and_val
991           | Types.Inr r ->
992             let { Types.fst = addr1; Types.snd = addr2 } = r in
993             let and_val =
994               BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
995                 (Nat.S (Nat.S (Nat.S Nat.O))))))))
996                 (Status.get_arg_8 cm s0 Bool.True
997                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
998                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
999                     (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct,
1000                     Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1001                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1002                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1003                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1004                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1005                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1006                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1007                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1008                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1009                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1010                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1011                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1012                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1013                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
1014                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1015                     addr1))
1016                 (Status.get_arg_8 cm s0 Bool.True
1017                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1018                     Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1019                     (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S
1020                     Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1021                     Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1022                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1023                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1024                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1025                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1026                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1027                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1028                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1029                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1030                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1031                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1032                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1033                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1034                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
1035                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1036                     addr2))
1037             in
1038             Status.set_arg_8 cm s0
1039               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1040                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1041                 (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1042                 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1043                 Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1044                 (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
1045                 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1046                 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1047                 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1048                 (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1049                 (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1050                 Vector.VEmpty)))))))))))))) addr1) and_val)
1051        | Types.Inr r ->
1052          let { Types.fst = addr1; Types.snd = addr2 } = r in
1053          let and_val =
1054            Bool.andb (Status.get_cy_flag cm s0)
1055              (Status.get_arg_1 cm s0
1056                (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1057                  Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O),
1058                  ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1059                  Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1060                  ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1061                  (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1062                Bool.True)
1063          in
1064          Status.set_flags cm s0 and_val Types.None
1065            (Status.get_ov_flag cm s0)))
1066   | ASM.ORL addr ->
1067     (fun _ ->
1068       let s0 = add_ticks1 s in
1069       (match addr with
1070        | Types.Inl l ->
1071          (match l with
1072           | Types.Inl l' ->
1073             let { Types.fst = addr1; Types.snd = addr2 } = l' in
1074             let or_val =
1075               BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1076                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1077                 (Status.get_arg_8 cm s0 Bool.True
1078                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1079                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1080                     (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1081                     Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1082                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1083                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1084                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1085                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1086                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1087                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1088                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1089                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1090                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1091                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1092                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1093                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1094                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
1095                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1096                     addr1))
1097                 (Status.get_arg_8 cm s0 Bool.True
1098                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1099                     (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
1100                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
1101                     (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1102                     ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1103                     ASM.Data, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1104                     (Vector.VCons (Nat.O, ASM.Indirect,
1105                     Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S
1106                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1107                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1108                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1109                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1110                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1111                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1112                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1113                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1114                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1115                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1116                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1117                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1118                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
1119                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1120                     addr2))
1121             in
1122             Status.set_arg_8 cm s0
1123               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1124                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1125                 (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty))
1126                 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1127                 Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1128                 (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
1129                 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1130                 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1131                 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1132                 (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1133                 (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1134                 Vector.VEmpty)))))))))))))) addr1) or_val
1135           | Types.Inr r ->
1136             let { Types.fst = addr1; Types.snd = addr2 } = r in
1137             let or_val =
1138               BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1139                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1140                 (Status.get_arg_8 cm s0 Bool.True
1141                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1142                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1143                     (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct,
1144                     Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1145                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1146                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1147                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1148                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1149                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1150                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1151                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1152                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1153                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1154                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1155                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1156                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1157                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
1158                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1159                     addr1))
1160                 (Status.get_arg_8 cm s0 Bool.True
1161                   (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1162                     Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1163                     (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S
1164                     Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1165                     Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1166                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1167                     Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
1168                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1169                     ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1170                     (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1171                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1172                     Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1173                     (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1174                     (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1175                     ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1176                     ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1177                     ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1178                     ASM.Ext_indirect, (Vector.VCons (Nat.O,
1179                     ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1180                     addr2))
1181             in
1182             Status.set_arg_8 cm s0
1183               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1184                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1185                 (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1186                 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1187                 Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1188                 (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
1189                 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1190                 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1191                 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1192                 (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1193                 (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1194                 Vector.VEmpty)))))))))))))) addr1) or_val)
1195        | Types.Inr r ->
1196          let { Types.fst = addr1; Types.snd = addr2 } = r in
1197          let or_val =
1198            Bool.orb (Status.get_cy_flag cm s0)
1199              (Status.get_arg_1 cm s0
1200                (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1201                  Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O),
1202                  ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1203                  Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1204                  ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1205                  (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1206                Bool.True)
1207          in
1208          Status.set_flags cm s0 or_val Types.None (Status.get_ov_flag cm s0)))
1209   | ASM.XRL addr ->
1210     (fun _ ->
1211       let s0 = add_ticks1 s in
1212       (match addr with
1213        | Types.Inl l' ->
1214          let { Types.fst = addr1; Types.snd = addr2 } = l' in
1215          let xor_val =
1216            BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1217              (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1218              (Status.get_arg_8 cm s0 Bool.True
1219                (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1220                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1221                  (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1222                  Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1223                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1224                  ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1225                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1226                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1227                  (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1228                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1229                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1230                  Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1231                  (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1232                  (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1233                  Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1234                  ASM.Ext_indirect, (Vector.VCons (Nat.O,
1235                  ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1236                  addr1))
1237              (Status.get_arg_8 cm s0 Bool.True
1238                (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1239                  (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1240                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
1241                  ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data, (Vector.VCons
1242                  ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S
1243                  Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
1244                  Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1245                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1246                  ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1247                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1248                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1249                  (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1250                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1251                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1252                  Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1253                  (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1254                  (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1255                  Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1256                  ASM.Ext_indirect, (Vector.VCons (Nat.O,
1257                  ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1258                  addr2))
1259          in
1260          Status.set_arg_8 cm s0
1261            (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1262              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1263              (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1264              (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1265              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1266              ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1267              Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1268              Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1269              ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1270              (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1271              Vector.VEmpty)))))))))))))) addr1) xor_val
1272        | Types.Inr r ->
1273          let { Types.fst = addr1; Types.snd = addr2 } = r in
1274          let xor_val =
1275            BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S
1276              (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1277              (Status.get_arg_8 cm s0 Bool.True
1278                (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1279                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1280                  (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct,
1281                  Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1282                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1283                  ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1284                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1285                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1286                  (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1287                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1288                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1289                  Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1290                  (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1291                  (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1292                  Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1293                  ASM.Ext_indirect, (Vector.VCons (Nat.O,
1294                  ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1295                  addr1))
1296              (Status.get_arg_8 cm s0 Bool.True
1297                (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1298                  Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1299                  (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
1300                  ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1301                  Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1302                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1303                  ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1304                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1305                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1306                  (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1307                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1308                  (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1309                  Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1310                  (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1311                  (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1312                  Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
1313                  ASM.Ext_indirect, (Vector.VCons (Nat.O,
1314                  ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1315                  addr2))
1316          in
1317          Status.set_arg_8 cm s0
1318            (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1319              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1320              (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S
1321              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1322              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1323              ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1324              Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1325              Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1326              ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1327              (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1328              Vector.VEmpty)))))))))))))) addr1) xor_val))
1329   | ASM.CLR addr ->
1330     (fun _ ->
1331       (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
1332                ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
1333                Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr,
1334                Vector.VEmpty)))))) addr with
1335        | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1336        | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1337        | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1338        | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1339        | ASM.ACC_A ->
1340          (fun _ ->
1341            let s0 = add_ticks1 s in
1342            Status.set_arg_8 cm s0 ASM.ACC_A
1343              (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1344                (Nat.S (Nat.S Nat.O))))))))))
1345        | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1346        | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1347        | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1348        | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1349        | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1350        | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1351        | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1352        | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1353        | ASM.CARRY ->
1354          (fun _ ->
1355            let s0 = add_ticks1 s in
1356            Status.set_arg_1 cm s0 ASM.CARRY Bool.False)
1357        | ASM.BIT_ADDR b ->
1358          (fun _ ->
1359            let s0 = add_ticks1 s in
1360            Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.False)
1361        | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1362        | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1363        | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1364        | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1365   | ASM.CPL addr ->
1366     (fun _ ->
1367       (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
1368                ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
1369                Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr,
1370                Vector.VEmpty)))))) addr with
1371        | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1372        | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1373        | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1374        | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1375        | ASM.ACC_A ->
1376          (fun _ ->
1377            let s0 = add_ticks1 s in
1378            let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1379            let new_acc =
1380              BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381                (Nat.S (Nat.S Nat.O)))))))) old_acc
1382            in
1383            Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1384        | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1385        | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1386        | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1387        | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1388        | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1389        | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1390        | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1391        | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1392        | ASM.CARRY ->
1393          (fun _ ->
1394            let s0 = add_ticks1 s in
1395            let old_cy_flag = Status.get_arg_1 cm s0 ASM.CARRY Bool.True in
1396            let new_cy_flag = Bool.notb old_cy_flag in
1397            Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag)
1398        | ASM.BIT_ADDR b ->
1399          (fun _ ->
1400            let s0 = add_ticks1 s in
1401            let old_bit = Status.get_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.True
1402            in
1403            let new_bit = Bool.notb old_bit in
1404            Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) new_bit)
1405        | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1406        | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1407        | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1408        | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1409   | ASM.RL x ->
1410     (fun _ ->
1411       let s0 = add_ticks1 s in
1412       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1413       let new_acc =
1414         Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1415           (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc
1416       in
1417       Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1418   | ASM.RLC x ->
1419     (fun _ ->
1420       let s0 = add_ticks1 s in
1421       let old_cy_flag = Status.get_cy_flag cm s0 in
1422       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1423       let new_cy_flag =
1424         Vector.get_index' Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1425           (Nat.S Nat.O))))))) old_acc
1426       in
1427       let new_acc =
1428         Vector.shift_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1429           (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc old_cy_flag
1430       in
1431       let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in
1432       Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc)
1433   | ASM.RR x ->
1434     (fun _ ->
1435       let s0 = add_ticks1 s in
1436       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1437       let new_acc =
1438         Vector.rotate_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1439           (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc
1440       in
1441       Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1442   | ASM.RRC x ->
1443     (fun _ ->
1444       let s0 = add_ticks1 s in
1445       let old_cy_flag = Status.get_cy_flag cm s0 in
1446       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1447       let new_cy_flag =
1448         Vector.get_index' (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1449           Nat.O))))))) Nat.O old_acc
1450       in
1451       let new_acc =
1452         Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1453           Nat.O))))))) (Nat.S Nat.O) old_acc old_cy_flag
1454       in
1455       let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in
1456       Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc)
1457   | ASM.SWAP x ->
1458     (fun _ ->
1459       let s0 = add_ticks1 s in
1460       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1461       let { Types.fst = nu; Types.snd = nl } =
1462         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1463           (Nat.S (Nat.S Nat.O)))) old_acc
1464       in
1465       let new_acc =
1466         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1467           (Nat.S (Nat.S Nat.O)))) nl nu
1468       in
1469       Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)
1470   | ASM.MOV addr ->
1471     (fun _ ->
1472       let s0 = add_ticks1 s in
1473       (match addr with
1474        | Types.Inl l ->
1475          (match l with
1476           | Types.Inl l' ->
1477             (match l' with
1478              | Types.Inl l'' ->
1479                (match l'' with
1480                 | Types.Inl l''' ->
1481                   (match l''' with
1482                    | Types.Inl l'''' ->
1483                      let { Types.fst = addr1; Types.snd = addr2 } = l'''' in
1484                      Status.set_arg_8 cm s0
1485                        (ASM.subaddressing_modeel__o__mk_subaddressing_mode
1486                          Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1487                          Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1488                          Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1489                          (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1490                          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1491                          Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S
1492                          (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1493                          (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1494                          ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1495                          ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
1496                          ASM.Ext_indirect, (Vector.VCons (Nat.O,
1497                          ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))
1498                          addr1)
1499                        (Status.get_arg_8 cm s0 Bool.False
1500                          (ASM.subaddressing_modeel__o__mk_subaddressing_mode
1501                            (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S
1502                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1503                            Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S
1504                            (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
1505                            ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
1506                            ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons
1507                            (Nat.O, ASM.Data, Vector.VEmpty))))))))
1508                            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1509                            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1510                            ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1511                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1512                            ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1513                            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1514                            ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1515                            (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1516                            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1517                            Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S
1518                            (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data,
1519                            (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1520                            ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
1521                            Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1522                            Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1523                            ASM.Ext_indirect_dptr,
1524                            Vector.VEmpty)))))))))))))))))))) addr2))
1525                    | Types.Inr r'''' ->
1526                      let { Types.fst = addr1; Types.snd = addr2 } = r'''' in
1527                      Status.set_arg_8 cm s0
1528                        (ASM.subaddressing_modeel__o__mk_subaddressing_mode
1529                          (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1530                          (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O),
1531                          ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
1532                          Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S
1533                          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1534                          ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1535                          (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1536                          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1537                          Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S
1538                          (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons
1539                          ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1540                          ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1541                          (Nat.O, ASM.Ext_indirect_dptr,
1542                          Vector.VEmpty)))))))))))))) addr1)
1543                        (Status.get_arg_8 cm s0 Bool.False
1544                          (ASM.subaddressing_modeel__o__mk_subaddressing_mode
1545                            (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1546                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))
1547                            (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
1548                            (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1549                            (Vector.VCons (Nat.O, ASM.Data,
1550                            Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S
1551                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1552                            Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1553                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1554                            Nat.O)))))))), ASM.Indirect, (Vector.VCons
1555                            ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1556                            Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1557                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1558                            ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1559                            (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1560                            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1561                            Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1562                            (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
1563                            ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons
1564                            ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1565                            (Nat.O, ASM.Ext_indirect_dptr,
1566                            Vector.VEmpty)))))))))))))))))))) addr2)))
1567                 | Types.Inr r''' ->
1568                   let { Types.fst = addr1; Types.snd = addr2 } = r''' in
1569                   Status.set_arg_8 cm s0
1570                     (ASM.subaddressing_modeel__o__mk_subaddressing_mode
1571                       Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1572                       Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct,
1573                       Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1574                       (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1575                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1576                       Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S
1577                       (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
1578                       ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1579                       (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
1580                       (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1581                       (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1582                       Vector.VEmpty)))))))))))))) addr1)
1583                     (Status.get_arg_8 cm s0 Bool.False
1584                       (ASM.subaddressing_modeel__o__mk_subaddressing_mode
1585                         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1586                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1587                         Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1588                         (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S
1589                         (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
1590                         ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
1591                         ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O,
1592                         ASM.Data, Vector.VEmpty)))))))))) (Vector.VCons
1593                         ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1594                         (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
1595                         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596                         (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1597                         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1598                         (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1599                         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1600                         (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S
1601                         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1602                         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1603                         Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
1604                         (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S
1605                         (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1606                         Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1607                         ASM.Ext_indirect_dptr,
1608                         Vector.VEmpty)))))))))))))))))))) addr2)))
1609              | Types.Inr r'' ->
1610                let { Types.fst = addr1; Types.snd = addr2 } = r'' in
1611                Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1)
1612           | Types.Inr r ->
1613             let { Types.fst = addr1; Types.snd = addr2 } = r in
1614             Status.set_arg_1 cm s0
1615               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1616                 (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Carry,
1617                 Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr,
1618                 (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1)
1619               (Status.get_arg_1 cm s0
1620                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1621                   (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
1622                   Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1623                   ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
1624                   ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
1625                   Vector.VEmpty)))))) addr2) Bool.False))
1626        | Types.Inr r ->
1627          let { Types.fst = addr1; Types.snd = addr2 } = r in
1628          Status.set_arg_1 cm s0
1629            (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1630              Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))
1631              (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons
1632              (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1)
1633            (Status.get_arg_1 cm s0
1634              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1635                (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Carry,
1636                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1637                ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1638                (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1639              Bool.False)))
1640   | ASM.MOVX addr ->
1641     (fun _ ->
1642       let s0 = add_ticks1 s in
1643       (match addr with
1644        | Types.Inl l ->
1645          let { Types.fst = addr1; Types.snd = addr2 } = l in
1646          Status.set_arg_8 cm s0
1647            (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1648              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1649              (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1650              (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1651              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1652              ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1653              Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1654              Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1655              ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1656              (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1657              Vector.VEmpty)))))))))))))) addr1)
1658            (Status.get_arg_8 cm s0 Bool.False
1659              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1660                Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1661                (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
1662                ASM.Ext_indirect, (Vector.VCons (Nat.O,
1663                ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons
1664                ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1665                (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1666                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1667                Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S
1668                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1669                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1670                Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1671                (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S
1672                (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
1673                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
1674                ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1675                Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1676                ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1677                addr2))
1678        | Types.Inr r ->
1679          let { Types.fst = addr1; Types.snd = addr2 } = r in
1680          Status.set_arg_8 cm s0
1681            (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
1682              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1683              (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1684              (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons
1685              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1686              ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1687              Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1688              (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
1689              (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1690              Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
1691              ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1692              Vector.VEmpty)))))))))))))) addr1)
1693            (Status.get_arg_8 cm s0 Bool.False
1694              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1695                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1696                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1697                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1698                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1699                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1700                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1701                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1702                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1703                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1704                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1705                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1706                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1707                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1708                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1709                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1710                Vector.VEmpty)))))))))))))))))))) addr2))))
1711   | ASM.SETB b ->
1712     (fun _ ->
1713       let s0 = add_ticks1 s in
1714       Status.set_arg_1 cm s0
1715         (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
1716           (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Carry,
1717           (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))
1718           (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O,
1719           ASM.Carry, Vector.VEmpty)))) b) Bool.False)
1720   | ASM.PUSH addr ->
1721     (fun _ ->
1722       let s0 = add_ticks1 s in
1723       let new_sp =
1724         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1725           (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_SP)
1726           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1727             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
1728       in
1729       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1730       Status.write_at_stack_pointer cm s1
1731         (Status.get_arg_8 cm s1 Bool.False
1732           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1733             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1734             Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1735             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1736             (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1737             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1738             ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1739             (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1740             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1741             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1742             ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1743             ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1744             ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
1745             (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1746             (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1747             addr)))
1748   | ASM.POP addr ->
1749     (fun _ ->
1750       let s0 = add_ticks1 s in
1751       let contents = Status.read_at_stack_pointer cm s0 in
1752       let { Types.fst = new_sp; Types.snd = flags } =
1753         Arithmetic.sub_8_with_carry
1754           (Status.get_8051_sfr cm s0 Status.SFR_SP)
1755           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1756             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1757       in
1758       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1759       Status.set_arg_8 cm s1
1760         (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1761           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1762           (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1763           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
1764           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1765           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1766           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1767           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1768           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1769           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) contents)
1770   | ASM.XCH (addr1, addr2) ->
1771     (fun _ ->
1772       let s0 = add_ticks1 s in
1773       let old_addr =
1774         Status.get_arg_8 cm s0 Bool.False
1775           (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
1776             Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1777             (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1778             ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1779             (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty))))))
1780             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1781             (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1782             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1783             ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1784             (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1785             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1786             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1787             ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1788             ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1789             ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
1790             (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1791             (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1792             addr2)
1793       in
1794       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1795       let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A old_addr in
1796       Status.set_arg_8 cm s1
1797         (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
1798           Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1799           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons
1800           ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
1801           Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1802           (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S
1803           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1804           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1805           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1806           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1807           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1808           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) old_acc)
1809   | ASM.XCHD (addr1, addr2) ->
1810     (fun _ ->
1811       let s0 = add_ticks1 s in
1812       let { Types.fst = acc_nu; Types.snd = acc_nl } =
1813         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1814           (Nat.S (Nat.S Nat.O))))
1815           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
1816       in
1817       let { Types.fst = arg_nu; Types.snd = arg_nl } =
1818         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1819           (Nat.S (Nat.S Nat.O))))
1820           (Status.get_arg_8 cm s0 Bool.False
1821             (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1822               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1823               Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Indirect,
1824               Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1825               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
1826               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1827               (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
1828               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1829               Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1830               (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
1831               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1832               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1833               ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1834               ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1835               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1836               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1837               Vector.VEmpty)))))))))))))))))))) addr2))
1838       in
1839       let new_acc =
1840         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1841           (Nat.S (Nat.S Nat.O)))) acc_nu arg_nl
1842       in
1843       let new_arg =
1844         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1845           (Nat.S (Nat.S Nat.O)))) arg_nu acc_nl
1846       in
1847       let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in
1848       Status.set_arg_8 cm s1
1849         (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1850           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1851           (Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1852           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
1853           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1854           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1855           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1856           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1857           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1858           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) new_arg)
1859   | ASM.RET ->
1860     (fun _ ->
1861       let s0 = add_ticks1 s in
1862       let high_bits = Status.read_at_stack_pointer cm s0 in
1863       let { Types.fst = new_sp; Types.snd = flags } =
1864         Arithmetic.sub_8_with_carry
1865           (Status.get_8051_sfr cm s0 Status.SFR_SP)
1866           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1867             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1868       in
1869       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1870       let low_bits = Status.read_at_stack_pointer cm s1 in
1871       let { Types.fst = new_sp0; Types.snd = flags0 } =
1872         Arithmetic.sub_8_with_carry
1873           (Status.get_8051_sfr cm s1 Status.SFR_SP)
1874           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1875             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1876       in
1877       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
1878       let new_pc =
1879         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1880           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1881           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
1882       in
1883       Status.set_program_counter cm s2 new_pc)
1884   | ASM.RETI ->
1885     (fun _ ->
1886       let s0 = add_ticks1 s in
1887       let high_bits = Status.read_at_stack_pointer cm s0 in
1888       let { Types.fst = new_sp; Types.snd = flags } =
1889         Arithmetic.sub_8_with_carry
1890           (Status.get_8051_sfr cm s0 Status.SFR_SP)
1891           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1892             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1893       in
1894       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1895       let low_bits = Status.read_at_stack_pointer cm s1 in
1896       let { Types.fst = new_sp0; Types.snd = flags0 } =
1897         Arithmetic.sub_8_with_carry
1898           (Status.get_8051_sfr cm s1 Status.SFR_SP)
1899           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1900             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1901       in
1902       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
1903       let new_pc =
1904         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1905           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1906           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
1907       in
1908       Status.set_program_counter cm s2 new_pc)
1909   | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0)) __
1910
1911(** val execute_1_preinstruction_ok' :
1912    (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
1913    BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
1914    Status.preStatus Types.sig0 **)
1915let execute_1_preinstruction_ok' ticks cm addr_of instr s =
1916  let add_ticks1 = fun s0 ->
1917    Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
1918  in
1919  let add_ticks2 = fun s0 ->
1920    Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
1921  in
1922  (match instr with
1923   | ASM.ADD (addr1, addr2) ->
1924     (fun _ ->
1925       let s0 = add_ticks1 s in
1926       (let { Types.fst = result; Types.snd = flags } =
1927          Arithmetic.add_8_with_carry
1928            (Status.get_arg_8 cm s0 Bool.False
1929              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1930                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1931                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1932                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1933                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1934                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1935                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1936                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1937                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1938                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1939                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1940                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1941                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1942                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1943                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1944                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1945                Vector.VEmpty)))))))))))))))))))) addr1))
1946            (Status.get_arg_8 cm s0 Bool.False
1947              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1948                (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1949                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
1950                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
1951                ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
1952                Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1953                Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1954                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1955                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1956                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1957                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1958                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1959                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1960                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1961                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1962                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1963                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1964                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1965                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1966                Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False
1967        in
1968       (fun _ ->
1969       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
1970       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
1971       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
1972       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
1973       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
1974   | ASM.ADDC (addr1, addr2) ->
1975     (fun _ ->
1976       let s0 = add_ticks1 s in
1977       let old_cy_flag = Status.get_cy_flag cm s0 in
1978       (let { Types.fst = result; Types.snd = flags } =
1979          Arithmetic.add_8_with_carry
1980            (Status.get_arg_8 cm s0 Bool.False
1981              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1982                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1983                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1984                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1985                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1986                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1987                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1988                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1989                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1990                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1991                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1992                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1993                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1994                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1995                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1996                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1997                Vector.VEmpty)))))))))))))))))))) addr1))
1998            (Status.get_arg_8 cm s0 Bool.False
1999              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2000                (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2001                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2002                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2003                ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2004                Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2005                Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2006                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2007                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2008                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2009                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2010                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2011                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2012                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2013                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2014                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2015                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2016                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2017                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2018                Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
2019        in
2020       (fun _ ->
2021       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2022       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2023       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2024       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2025       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2026   | ASM.SUBB (addr1, addr2) ->
2027     (fun _ ->
2028       let s0 = add_ticks1 s in
2029       let old_cy_flag = Status.get_cy_flag cm s0 in
2030       (let { Types.fst = result; Types.snd = flags } =
2031          Arithmetic.sub_8_with_carry
2032            (Status.get_arg_8 cm s0 Bool.False
2033              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
2034                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2035                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
2036                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2037                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2038                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2039                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2040                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2041                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2042                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2043                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2044                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2045                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2046                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2047                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2048                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2049                Vector.VEmpty)))))))))))))))))))) addr1))
2050            (Status.get_arg_8 cm s0 Bool.False
2051              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2052                (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2053                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2054                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2055                ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2056                Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2057                Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2058                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2059                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2060                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2061                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2062                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2063                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2064                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2065                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2066                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2067                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2068                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2069                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2070                Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
2071        in
2072       (fun _ ->
2073       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2074       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2075       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2076       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2077       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2078   | ASM.INC addr ->
2079     (fun _ ->
2080       (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
2081                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2082                ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2083                ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2084                ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
2085                (Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with
2086        | ASM.DIRECT d ->
2087          (fun _ _ ->
2088            let s' = add_ticks1 s in
2089            let result =
2090              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2091                (Nat.S Nat.O))))))))
2092                (Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d))
2093                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
2094                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
2095            in
2096            Status.set_arg_8 cm s' (ASM.DIRECT d) result)
2097        | ASM.INDIRECT i ->
2098          (fun _ _ ->
2099            let s' = add_ticks1 s in
2100            let result =
2101              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2102                (Nat.S Nat.O))))))))
2103                (Status.get_arg_8 cm s' Bool.True (ASM.INDIRECT i))
2104                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
2105                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
2106            in
2107            Status.set_arg_8 cm s' (ASM.INDIRECT i) result)
2108        | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2109        | ASM.REGISTER r ->
2110          (fun _ _ ->
2111            let s' = add_ticks1 s in
2112            let result =
2113              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2114                (Nat.S Nat.O))))))))
2115                (Status.get_arg_8 cm s' Bool.True (ASM.REGISTER r))
2116                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
2117                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
2118            in
2119            Status.set_arg_8 cm s' (ASM.REGISTER r) result)
2120        | ASM.ACC_A ->
2121          (fun _ _ ->
2122            let s' = add_ticks1 s in
2123            let result =
2124              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2125                (Nat.S Nat.O))))))))
2126                (Status.get_arg_8 cm s' Bool.True ASM.ACC_A)
2127                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
2128                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
2129            in
2130            Status.set_arg_8 cm s' ASM.ACC_A result)
2131        | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2132        | ASM.DPTR ->
2133          (fun _ _ ->
2134            let s' = add_ticks1 s in
2135            (let { Types.fst = carry; Types.snd = bl } =
2136               Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (