source: extracted/interpret.ml @ 2908

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

Bug fixed by hand, they will be fixed automatically by the new extraction.

File size: 245.5 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 Jmeq
48
49open Russell
50
51open Util
52
53open List
54
55open Lists
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Positive
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open Identifiers
76
77open CostLabel
78
79open ASM
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 s0 = Status.set_8051_sfr cm s' Status.SFR_DPL bl in
351            Status.set_8051_sfr cm s0 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 (Status.get_arg_16 cm s0 addr2) addr1)
1634           | Types.Inr r ->
1635             let { Types.fst = addr1; Types.snd = addr2 } = r in
1636             Status.set_arg_1 cm s0
1637               (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1638                 (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Carry,
1639                 Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr,
1640                 (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1)
1641               (Status.get_arg_1 cm s0
1642                 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1643                   (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr,
1644                   Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1645                   ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
1646                   ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
1647                   Vector.VEmpty)))))) addr2) Bool.False))
1648        | Types.Inr r ->
1649          let { Types.fst = addr1; Types.snd = addr2 } = r in
1650          Status.set_arg_1 cm s0
1651            (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1652              Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))
1653              (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons
1654              (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1)
1655            (Status.get_arg_1 cm s0
1656              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1657                (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Carry,
1658                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1659                ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr,
1660                (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2)
1661              Bool.False)))
1662   | ASM.MOVX addr ->
1663     (fun _ ->
1664       let s0 = add_ticks1 s in
1665       (match addr with
1666        | Types.Inl l ->
1667          let { Types.fst = addr1; Types.snd = addr2 } = l in
1668          Status.set_arg_8 cm s0
1669            (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1670              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1671              (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1672              (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct,
1673              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1674              ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1675              Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1676              Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1677              ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1678              (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1679              Vector.VEmpty)))))))))))))) addr1)
1680            (Status.get_arg_8 cm s0 Bool.False
1681              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
1682                Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1683                (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O),
1684                ASM.Ext_indirect, (Vector.VCons (Nat.O,
1685                ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons
1686                ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1687                (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1688                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1689                Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S
1690                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr,
1691                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1692                Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1693                (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S
1694                (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons
1695                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons
1696                ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S
1697                Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1698                ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1699                addr2))
1700        | Types.Inr r ->
1701          let { Types.fst = addr1; Types.snd = addr2 } = r in
1702          Status.set_arg_8 cm s0
1703            (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
1704              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1705              (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1706              (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons
1707              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1708              ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1709              Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1710              (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
1711              (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1712              Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
1713              ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1714              Vector.VEmpty)))))))))))))) addr1)
1715            (Status.get_arg_8 cm s0 Bool.False
1716              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1717                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1718                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1719                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1720                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1721                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1722                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1723                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1724                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1725                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1726                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1727                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1728                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1729                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1730                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1731                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1732                Vector.VEmpty)))))))))))))))))))) addr2))))
1733   | ASM.SETB b ->
1734     (fun _ ->
1735       let s0 = add_ticks1 s in
1736       Status.set_arg_1 cm s0
1737         (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O)
1738           (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Carry,
1739           (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))
1740           (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O,
1741           ASM.Carry, Vector.VEmpty)))) b) Bool.False)
1742   | ASM.PUSH addr ->
1743     (fun _ ->
1744       let s0 = add_ticks1 s in
1745       let new_sp =
1746         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1747           (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_SP)
1748           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1749             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
1750       in
1751       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1752       Status.write_at_stack_pointer cm s1
1753         (Status.get_arg_8 cm s1 Bool.False
1754           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1755             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1756             Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))
1757             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1758             (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1759             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1760             ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1761             (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1762             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1763             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1764             ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1765             ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1766             ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
1767             (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1768             (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1769             addr)))
1770   | ASM.POP addr ->
1771     (fun _ ->
1772       let s0 = add_ticks1 s in
1773       let contents = Status.read_at_stack_pointer cm s0 in
1774       let { Types.fst = new_sp; Types.snd = flags } =
1775         Arithmetic.sub_8_with_carry
1776           (Status.get_8051_sfr cm s0 Status.SFR_SP)
1777           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1778             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1779       in
1780       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1781       Status.set_arg_8 cm s1
1782         (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1783           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1784           (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1785           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
1786           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1787           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1788           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1789           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1790           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1791           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) contents)
1792   | ASM.XCH (addr1, addr2) ->
1793     (fun _ ->
1794       let s0 = add_ticks1 s in
1795       let old_addr =
1796         Status.get_arg_8 cm s0 Bool.False
1797           (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
1798             Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1799             (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1800             ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
1801             (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty))))))
1802             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1803             (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
1804             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
1805             ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1806             (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1807             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1808             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1809             ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1810             ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1811             ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
1812             (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
1813             (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
1814             addr2)
1815       in
1816       let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in
1817       let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A old_addr in
1818       Status.set_arg_8 cm s1
1819         (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
1820           Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
1821           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons
1822           ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
1823           Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1824           (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S
1825           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1826           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1827           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1828           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1829           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1830           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) old_acc)
1831   | ASM.XCHD (addr1, addr2) ->
1832     (fun _ ->
1833       let s0 = add_ticks1 s in
1834       let { Types.fst = acc_nu; Types.snd = acc_nl } =
1835         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1836           (Nat.S (Nat.S Nat.O))))
1837           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
1838       in
1839       let { Types.fst = arg_nu; Types.snd = arg_nl } =
1840         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1841           (Nat.S (Nat.S Nat.O))))
1842           (Status.get_arg_8 cm s0 Bool.False
1843             (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1844               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1845               Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Indirect,
1846               Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1847               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct,
1848               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1849               (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
1850               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1851               Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1852               (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons
1853               ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b,
1854               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1855               ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1856               ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1857               ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1858               (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1859               Vector.VEmpty)))))))))))))))))))) addr2))
1860       in
1861       let new_acc =
1862         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1863           (Nat.S (Nat.S Nat.O)))) acc_nu arg_nl
1864       in
1865       let new_arg =
1866         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
1867           (Nat.S (Nat.S Nat.O)))) arg_nu acc_nl
1868       in
1869       let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in
1870       Status.set_arg_8 cm s1
1871         (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
1872           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons
1873           (Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S
1874           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons
1875           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
1876           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr,
1877           (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
1878           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons
1879           ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1880           ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) new_arg)
1881   | ASM.RET ->
1882     (fun _ ->
1883       let s0 = add_ticks1 s in
1884       let high_bits = Status.read_at_stack_pointer cm s0 in
1885       let { Types.fst = new_sp; Types.snd = flags } =
1886         Arithmetic.sub_8_with_carry
1887           (Status.get_8051_sfr cm s0 Status.SFR_SP)
1888           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1889             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1890       in
1891       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1892       let low_bits = Status.read_at_stack_pointer cm s1 in
1893       let { Types.fst = new_sp0; Types.snd = flags0 } =
1894         Arithmetic.sub_8_with_carry
1895           (Status.get_8051_sfr cm s1 Status.SFR_SP)
1896           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1897             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1898       in
1899       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
1900       let new_pc =
1901         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1902           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1903           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
1904       in
1905       Status.set_program_counter cm s2 new_pc)
1906   | ASM.RETI ->
1907     (fun _ ->
1908       let s0 = add_ticks1 s in
1909       let high_bits = Status.read_at_stack_pointer cm s0 in
1910       let { Types.fst = new_sp; Types.snd = flags } =
1911         Arithmetic.sub_8_with_carry
1912           (Status.get_8051_sfr cm s0 Status.SFR_SP)
1913           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1914             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1915       in
1916       let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in
1917       let low_bits = Status.read_at_stack_pointer cm s1 in
1918       let { Types.fst = new_sp0; Types.snd = flags0 } =
1919         Arithmetic.sub_8_with_carry
1920           (Status.get_8051_sfr cm s1 Status.SFR_SP)
1921           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1922             (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False
1923       in
1924       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
1925       let new_pc =
1926         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1927           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1928           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
1929       in
1930       Status.set_program_counter cm s2 new_pc)
1931   | ASM.NOP -> (fun _ -> let s0 = add_ticks1 s in s0)
1932   | ASM.JMP x ->
1933     (fun _ ->
1934       let s0 = add_ticks1 s in
1935       let dptr =
1936         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1937           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1938           (Nat.S (Nat.S Nat.O))))))))
1939           (Status.get_8051_sfr cm s0 Status.SFR_DPH)
1940           (Status.get_8051_sfr cm s0 Status.SFR_DPL)
1941       in
1942       let big_acc =
1943         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1944           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1945           (Nat.S (Nat.S Nat.O))))))))
1946           (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1947             (Nat.S Nat.O)))))))))
1948           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
1949       in
1950       let jmp_addr =
1951         Arithmetic.add
1952           (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1953             Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1954             (Nat.S Nat.O))))))))) big_acc dptr
1955       in
1956       let new_pc =
1957         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1958           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1959           Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
1960       in
1961       Status.set_program_counter cm s0 new_pc)) __
1962
1963(** val execute_1_preinstruction_ok' :
1964    (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
1965    BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
1966    Status.preStatus Types.sig0 **)
1967let execute_1_preinstruction_ok' ticks cm addr_of instr s =
1968  let add_ticks1 = fun s0 ->
1969    Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
1970  in
1971  let add_ticks2 = fun s0 ->
1972    Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
1973  in
1974  (match instr with
1975   | ASM.ADD (addr1, addr2) ->
1976     (fun _ ->
1977       let s0 = add_ticks1 s in
1978       (let { Types.fst = result; Types.snd = flags } =
1979          Arithmetic.add_8_with_carry
1980            (Status.get_arg_8 cm s0 Bool.False
1981              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
1982                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1983                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
1984                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1985                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
1986                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1987                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
1988                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1989                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
1990                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
1991                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1992                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1993                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1994                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1995                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
1996                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
1997                Vector.VEmpty)))))))))))))))))))) addr1))
1998            (Status.get_arg_8 cm s0 Bool.False
1999              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2000                (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2001                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2002                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2003                ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2004                Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2005                Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2006                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2007                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2008                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2009                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2010                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2011                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2012                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2013                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2014                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2015                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2016                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2017                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2018                Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False
2019        in
2020       (fun _ ->
2021       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2022       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2023       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2024       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2025       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2026   | ASM.ADDC (addr1, addr2) ->
2027     (fun _ ->
2028       let s0 = add_ticks1 s in
2029       let old_cy_flag = Status.get_cy_flag cm s0 in
2030       (let { Types.fst = result; Types.snd = flags } =
2031          Arithmetic.add_8_with_carry
2032            (Status.get_arg_8 cm s0 Bool.False
2033              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
2034                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2035                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
2036                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2037                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2038                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2039                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2040                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2041                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2042                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2043                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2044                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2045                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2046                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2047                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2048                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2049                Vector.VEmpty)))))))))))))))))))) addr1))
2050            (Status.get_arg_8 cm s0 Bool.False
2051              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2052                (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2053                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2054                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2055                ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2056                Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2057                Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2058                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2059                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2060                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2061                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2062                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2063                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2064                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2065                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2066                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2067                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2068                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2069                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2070                Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
2071        in
2072       (fun _ ->
2073       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2074       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2075       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2076       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2077       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2078   | ASM.SUBB (addr1, addr2) ->
2079     (fun _ ->
2080       let s0 = add_ticks1 s in
2081       let old_cy_flag = Status.get_cy_flag cm s0 in
2082       (let { Types.fst = result; Types.snd = flags } =
2083          Arithmetic.sub_8_with_carry
2084            (Status.get_arg_8 cm s0 Bool.False
2085              (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
2086                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2087                (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a,
2088                Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2089                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2090                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2091                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2092                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2093                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2094                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2095                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2096                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2097                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2098                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2099                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2100                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2101                Vector.VEmpty)))))))))))))))))))) addr1))
2102            (Status.get_arg_8 cm s0 Bool.False
2103              (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S
2104                (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2105                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons
2106                ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons
2107                ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
2108                Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
2109                Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
2110                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
2111                ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2112                (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect,
2113                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2114                (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
2115                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
2116                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2117                ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2118                Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2119                Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2120                ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect,
2121                (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
2122                Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag
2123        in
2124       (fun _ ->
2125       let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in
2126       let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in
2127       let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in
2128       let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in
2129       Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __)
2130   | ASM.INC addr ->
2131     (fun _ ->
2132       (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
2133                (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2134                ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2135                ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2136                ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect,
2137                (Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with
2138        | ASM.DIRECT d ->
2139          (fun _ _ ->
2140            let s' = add_ticks1 s in
2141            let result =
2142              Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2143                (Nat.S Nat.O))))))))
2144                (Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d))
2145                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
2146                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
2147            in
2148            Status.set_arg_8 cm s' (ASM.DIRECT d) result)
2149        | ASM.INDIRECT i ->
2150          (