source: driver/extracted/interpret.ml @ 3106

Last change on this file since 3106 was 3080, checked in by sacerdot, 7 years ago

New extraction.

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