source: extracted/interpret.ml @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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