source: extracted/interpret.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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