81 (** val inefficient_address_of_label :
82 ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **)
83 let inefficient_address_of_label instr_list id =
84 LabelledObjects.index_of
85 (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id)
88 type label_map = Nat.nat Identifiers.identifier_map
90 (** val create_label_cost_map0 :
91 ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
92 Types.prod Types.sig0 **)
93 let create_label_cost_map0 program =
95 (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
96 (let { Types.fst = eta19; Types.snd = ppc } =
97 Types.pi1 labels_costs_ppc
100 (let { Types.fst = labels; Types.snd = costs } = eta19 in
102 (let { Types.fst = label; Types.snd = instr } = x in
106 | Types.None -> labels
107 | Types.Some l -> Identifiers.add PreIdentifiers.ASMTag labels l ppc
111 | ASM.Instruction x0 -> costs
112 | ASM.Comment x0 -> costs
114 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
115 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
116 (Nat.S Nat.O))))))))))))))))
117 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
118 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
119 (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) cost costs
120 | ASM.Jmp x0 -> costs
121 | ASM.Jnz (x0, x1, x2) -> costs
122 | ASM.Call x0 -> costs
123 | ASM.Mov (x0, x1, x2) -> costs
125 { Types.fst = { Types.fst = labels1; Types.snd = costs1 }; Types.snd =
126 (Nat.S ppc) })) __)) __)) __) { Types.fst = { Types.fst =
127 (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
128 (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
129 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130 Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
132 (** val create_label_cost_map :
133 ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
135 let create_label_cost_map program =
136 Types.pi1 (create_label_cost_map0 program)
138 (** val address_of_word_labels :
139 ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
140 let address_of_word_labels program id =
141 let labels = (create_label_cost_map program).Types.fst in
142 let address_of_label = fun l ->
143 Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O
145 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
146 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
147 Nat.O)))))))))))))))) (address_of_label id)
149 (** val prod_inv_rect_Type0 :
150 ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
151 let prod_inv_rect_Type0 clearme =
152 let { Types.fst = fst; Types.snd = snd } = clearme in
153 (fun auto -> auto fst snd __)
156 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
157 BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
159 let fetch0 pmem pc v =
160 let { Types.fst = b; Types.snd = v0 } =
161 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
166 let { Types.fst = b0; Types.snd = v1 } =
167 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0
171 let { Types.fst = b1; Types.snd = v2 } =
172 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
176 let { Types.fst = b2; Types.snd = v3 } =
177 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
181 let { Types.fst = b3; Types.snd = v4 } =
182 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
186 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
187 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
188 { Types.fst = (ASM.REGISTER v4); Types.snd =
189 ASM.ACC_A }))))))); Types.snd = pc }; Types.snd = (Nat.S
192 let { Types.fst = b4; Types.snd = v5 } =
193 Vector.head (Nat.S (Nat.S Nat.O)) v4
197 let { Types.fst = b5; Types.snd = v6 } =
198 Vector.head (Nat.S Nat.O) v5
202 { Types.fst = { Types.fst = (ASM.RealInstruction
203 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
204 (Types.Inr { Types.fst = (ASM.INDIRECT
205 (Vector.from_singl v6)); Types.snd =
206 ASM.ACC_A }))))))); Types.snd = pc }; Types.snd =
209 let { Types.fst = b6; Types.snd = v7 } =
214 prod_inv_rect_Type0 (ASM.next pmem pc)
215 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
216 (ASM.RealInstruction (ASM.MOV (Types.Inl
217 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
218 (ASM.DIRECT b10); Types.snd = ASM.ACC_A }))))));
219 Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
221 { Types.fst = { Types.fst = (ASM.RealInstruction
222 (ASM.CPL ASM.ACC_A)); Types.snd = pc };
223 Types.snd = (Nat.S Nat.O) }))
225 let { Types.fst = b5; Types.snd = v6 } =
226 Vector.head (Nat.S Nat.O) v5
230 { Types.fst = { Types.fst = (ASM.RealInstruction
231 (ASM.MOVX (Types.Inr { Types.fst = (ASM.EXT_INDIRECT
232 (Vector.from_singl v6)); Types.snd = ASM.ACC_A })));
233 Types.snd = pc }; Types.snd = (Nat.S (Nat.S
236 let { Types.fst = b6; Types.snd = v7 } =
241 prod_inv_rect_Type0 (ASM.next pmem pc)
242 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
243 (ASM.ACALL (ASM.ADDR11
244 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
245 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
246 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
247 ((Nat.S (Nat.S Nat.O)), Bool.True,
248 (Vector.VCons ((Nat.S Nat.O), Bool.True,
249 (Vector.VCons (Nat.O, Bool.True,
250 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
251 Types.snd = (Nat.S (Nat.S Nat.O)) })
253 { Types.fst = { Types.fst = (ASM.RealInstruction
254 (ASM.MOVX (Types.Inr { Types.fst =
255 ASM.EXT_INDIRECT_DPTR; Types.snd =
256 ASM.ACC_A }))); Types.snd = pc }; Types.snd =
257 (Nat.S (Nat.S Nat.O)) }))))
259 let { Types.fst = b3; Types.snd = v4 } =
260 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
264 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
265 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl
266 { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
267 v4) }))))))); Types.snd = pc }; Types.snd = (Nat.S
270 let { Types.fst = b4; Types.snd = v5 } =
271 Vector.head (Nat.S (Nat.S Nat.O)) v4
275 let { Types.fst = b5; Types.snd = v6 } =
276 Vector.head (Nat.S Nat.O) v5
280 { Types.fst = { Types.fst = (ASM.RealInstruction
281 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
282 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
283 (ASM.INDIRECT (Vector.from_singl v6)) })))))));
284 Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
286 let { Types.fst = b6; Types.snd = v7 } =
291 prod_inv_rect_Type0 (ASM.next pmem pc)
292 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
293 (ASM.RealInstruction (ASM.MOV (Types.Inl
294 (Types.Inl (Types.Inl (Types.Inl (Types.Inl
295 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT
296 b10) }))))))); Types.snd = pc0 }; Types.snd =
299 { Types.fst = { Types.fst = (ASM.RealInstruction
300 (ASM.CLR ASM.ACC_A)); Types.snd = pc };
301 Types.snd = (Nat.S Nat.O) }))
303 let { Types.fst = b5; Types.snd = v6 } =
304 Vector.head (Nat.S Nat.O) v5
308 { Types.fst = { Types.fst = (ASM.RealInstruction
309 (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A;
310 Types.snd = (ASM.EXT_INDIRECT
311 (Vector.from_singl v6)) }))); Types.snd = pc };
312 Types.snd = (Nat.S (Nat.S Nat.O)) }
314 let { Types.fst = b6; Types.snd = v7 } =
319 prod_inv_rect_Type0 (ASM.next pmem pc)
320 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
321 (ASM.AJMP (ASM.ADDR11
322 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
323 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
324 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
325 ((Nat.S (Nat.S Nat.O)), Bool.True,
326 (Vector.VCons ((Nat.S Nat.O), Bool.True,
327 (Vector.VCons (Nat.O, Bool.True,
328 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
329 Types.snd = (Nat.S (Nat.S Nat.O)) })
331 { Types.fst = { Types.fst = (ASM.RealInstruction
332 (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A;
333 Types.snd = ASM.EXT_INDIRECT_DPTR })));
334 Types.snd = pc }; Types.snd = (Nat.S (Nat.S
337 let { Types.fst = b2; Types.snd = v3 } =
338 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
342 let { Types.fst = b3; Types.snd = v4 } =
343 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
347 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
348 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ
349 ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd =
350 pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })
352 let { Types.fst = b4; Types.snd = v5 } =
353 Vector.head (Nat.S (Nat.S Nat.O)) v4
357 let { Types.fst = b5; Types.snd = v6 } =
358 Vector.head (Nat.S Nat.O) v5
362 { Types.fst = { Types.fst = (ASM.RealInstruction
363 (ASM.XCHD (ASM.ACC_A, (ASM.INDIRECT
364 (Vector.from_singl v6))))); Types.snd = pc };
365 Types.snd = (Nat.S Nat.O) }
367 let { Types.fst = b6; Types.snd = v7 } =
372 prod_inv_rect_Type0 (ASM.next pmem pc)
374 prod_inv_rect_Type0 (ASM.next pmem pc0)
375 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
376 (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT
377 b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
378 Types.snd = (Nat.S (Nat.S Nat.O)) }))
380 { Types.fst = { Types.fst = (ASM.RealInstruction
381 (ASM.DA ASM.ACC_A)); Types.snd = pc };
382 Types.snd = (Nat.S Nat.O) }))
384 let { Types.fst = b5; Types.snd = v6 } =
385 Vector.head (Nat.S Nat.O) v5
389 let { Types.fst = b6; Types.snd = v7 } =
394 { Types.fst = { Types.fst = (ASM.RealInstruction
395 (ASM.SETB ASM.CARRY)); Types.snd = pc };
396 Types.snd = (Nat.S Nat.O) }
398 prod_inv_rect_Type0 (ASM.next pmem pc)
399 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
400 (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR
401 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
404 let { Types.fst = b6; Types.snd = v7 } =
409 prod_inv_rect_Type0 (ASM.next pmem pc)
410 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
411 (ASM.ACALL (ASM.ADDR11
412 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
413 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
414 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
415 ((Nat.S (Nat.S Nat.O)), Bool.True,
416 (Vector.VCons ((Nat.S Nat.O), Bool.True,
417 (Vector.VCons (Nat.O, Bool.False,
418 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
419 Types.snd = (Nat.S (Nat.S Nat.O)) })
421 prod_inv_rect_Type0 (ASM.next pmem pc)
422 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
423 (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10)));
424 Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S
427 let { Types.fst = b3; Types.snd = v4 } =
428 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
432 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCH
433 (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
434 Types.snd = (Nat.S Nat.O) }
436 let { Types.fst = b4; Types.snd = v5 } =
437 Vector.head (Nat.S (Nat.S Nat.O)) v4
441 let { Types.fst = b5; Types.snd = v6 } =
442 Vector.head (Nat.S Nat.O) v5
446 { Types.fst = { Types.fst = (ASM.RealInstruction
447 (ASM.XCH (ASM.ACC_A, (ASM.INDIRECT
448 (Vector.from_singl v6))))); Types.snd = pc };
449 Types.snd = (Nat.S Nat.O) }
451 let { Types.fst = b6; Types.snd = v7 } =
456 prod_inv_rect_Type0 (ASM.next pmem pc)
457 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
458 (ASM.RealInstruction (ASM.XCH (ASM.ACC_A,
459 (ASM.DIRECT b10)))); Types.snd = pc0 };
460 Types.snd = (Nat.S Nat.O) })
462 { Types.fst = { Types.fst = (ASM.RealInstruction
463 (ASM.SWAP ASM.ACC_A)); Types.snd = pc };
464 Types.snd = (Nat.S Nat.O) }))
466 let { Types.fst = b5; Types.snd = v6 } =
467 Vector.head (Nat.S Nat.O) v5
471 let { Types.fst = b6; Types.snd = v7 } =
476 { Types.fst = { Types.fst = (ASM.RealInstruction
477 (ASM.CLR ASM.CARRY)); Types.snd = pc };
478 Types.snd = (Nat.S Nat.O) }
480 prod_inv_rect_Type0 (ASM.next pmem pc)
481 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
482 (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR
483 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
486 let { Types.fst = b6; Types.snd = v7 } =
491 prod_inv_rect_Type0 (ASM.next pmem pc)
492 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
493 (ASM.AJMP (ASM.ADDR11
494 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
495 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
496 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
497 ((Nat.S (Nat.S Nat.O)), Bool.True,
498 (Vector.VCons ((Nat.S Nat.O), Bool.True,
499 (Vector.VCons (Nat.O, Bool.False,
500 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
501 Types.snd = (Nat.S (Nat.S Nat.O)) })
503 prod_inv_rect_Type0 (ASM.next pmem pc)
504 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
505 (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT
506 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
507 (Nat.S Nat.O)) })))))))
509 let { Types.fst = b1; Types.snd = v2 } =
510 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
514 let { Types.fst = b2; Types.snd = v3 } =
515 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
519 let { Types.fst = b3; Types.snd = v4 } =
520 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
524 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
525 prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ ->
526 { Types.fst = { Types.fst = (ASM.RealInstruction
527 (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4);
528 Types.snd = (ASM.DATA b10) }), (ASM.RELATIVE b20))));
529 Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
531 let { Types.fst = b4; Types.snd = v5 } =
532 Vector.head (Nat.S (Nat.S Nat.O)) v4
536 let { Types.fst = b5; Types.snd = v6 } =
537 Vector.head (Nat.S Nat.O) v5
541 prod_inv_rect_Type0 (ASM.next pmem pc)
543 prod_inv_rect_Type0 (ASM.next pmem pc0)
544 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
545 (ASM.RealInstruction (ASM.CJNE ((Types.Inr
546 { Types.fst = (ASM.INDIRECT
547 (Vector.from_singl v6)); Types.snd = (ASM.DATA
548 b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 };
549 Types.snd = (Nat.S (Nat.S Nat.O)) }))
551 let { Types.fst = b6; Types.snd = v7 } =
556 prod_inv_rect_Type0 (ASM.next pmem pc)
558 prod_inv_rect_Type0 (ASM.next pmem pc0)
559 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
560 (ASM.RealInstruction (ASM.CJNE ((Types.Inl
561 { Types.fst = ASM.ACC_A; Types.snd =
562 (ASM.DIRECT b10) }), (ASM.RELATIVE b20))));
563 Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
566 prod_inv_rect_Type0 (ASM.next pmem pc)
568 prod_inv_rect_Type0 (ASM.next pmem pc0)
569 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
570 (ASM.RealInstruction (ASM.CJNE ((Types.Inl
571 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
572 b10) }), (ASM.RELATIVE b20)))); Types.snd =
573 pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))
575 let { Types.fst = b5; Types.snd = v6 } =
576 Vector.head (Nat.S Nat.O) v5
580 let { Types.fst = b6; Types.snd = v7 } =
585 { Types.fst = { Types.fst = (ASM.RealInstruction
586 (ASM.CPL ASM.CARRY)); Types.snd = pc };
587 Types.snd = (Nat.S Nat.O) }
589 prod_inv_rect_Type0 (ASM.next pmem pc)
590 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
591 (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR
592 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
595 let { Types.fst = b6; Types.snd = v7 } =
600 prod_inv_rect_Type0 (ASM.next pmem pc)
601 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
602 (ASM.ACALL (ASM.ADDR11
603 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
604 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
605 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
606 ((Nat.S (Nat.S Nat.O)), Bool.True,
607 (Vector.VCons ((Nat.S Nat.O), Bool.False,
608 (Vector.VCons (Nat.O, Bool.True,
609 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
610 Types.snd = (Nat.S (Nat.S Nat.O)) })
612 prod_inv_rect_Type0 (ASM.next pmem pc)
613 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
614 (ASM.RealInstruction (ASM.ANL (Types.Inr
615 { Types.fst = ASM.CARRY; Types.snd =
616 (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 };
617 Types.snd = (Nat.S (Nat.S Nat.O)) })))))
619 let { Types.fst = b3; Types.snd = v4 } =
620 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
624 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
625 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
626 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
627 { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DIRECT
628 b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
631 let { Types.fst = b4; Types.snd = v5 } =
632 Vector.head (Nat.S (Nat.S Nat.O)) v4
636 let { Types.fst = b5; Types.snd = v6 } =
637 Vector.head (Nat.S Nat.O) v5
641 prod_inv_rect_Type0 (ASM.next pmem pc)
642 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
643 (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
644 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
645 (ASM.INDIRECT (Vector.from_singl v6)); Types.snd =
646 (ASM.DIRECT b10) }))))))); Types.snd = pc0 };
647 Types.snd = (Nat.S (Nat.S Nat.O)) })
649 { Types.fst = { Types.fst = (ASM.RealInstruction
650 (ASM.MUL (ASM.ACC_A, ASM.ACC_B))); Types.snd = pc };
651 Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
653 let { Types.fst = b5; Types.snd = v6 } =
654 Vector.head (Nat.S Nat.O) v5
658 let { Types.fst = b6; Types.snd = v7 } =
663 { Types.fst = { Types.fst = (ASM.RealInstruction
664 (ASM.INC ASM.DPTR)); Types.snd = pc };
665 Types.snd = (Nat.S (Nat.S Nat.O)) }
667 prod_inv_rect_Type0 (ASM.next pmem pc)
668 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
669 (ASM.RealInstruction (ASM.MOV (Types.Inl
670 (Types.Inr { Types.fst = ASM.CARRY; Types.snd =
671 (ASM.BIT_ADDR b10) })))); Types.snd = pc0 };
672 Types.snd = (Nat.S Nat.O) }))
674 let { Types.fst = b6; Types.snd = v7 } =
679 prod_inv_rect_Type0 (ASM.next pmem pc)
680 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
681 (ASM.AJMP (ASM.ADDR11
682 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
683 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
684 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
685 ((Nat.S (Nat.S Nat.O)), Bool.True,
686 (Vector.VCons ((Nat.S Nat.O), Bool.False,
687 (Vector.VCons (Nat.O, Bool.True,
688 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
689 Types.snd = (Nat.S (Nat.S Nat.O)) })
691 prod_inv_rect_Type0 (ASM.next pmem pc)
692 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
693 (ASM.RealInstruction (ASM.ORL (Types.Inr
694 { Types.fst = ASM.CARRY; Types.snd =
695 (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 };
696 Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
698 let { Types.fst = b2; Types.snd = v3 } =
699 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
703 let { Types.fst = b3; Types.snd = v4 } =
704 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
708 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB
709 (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
710 Types.snd = (Nat.S Nat.O) }
712 let { Types.fst = b4; Types.snd = v5 } =
713 Vector.head (Nat.S (Nat.S Nat.O)) v4
717 let { Types.fst = b5; Types.snd = v6 } =
718 Vector.head (Nat.S Nat.O) v5
722 { Types.fst = { Types.fst = (ASM.RealInstruction
723 (ASM.SUBB (ASM.ACC_A, (ASM.INDIRECT
724 (Vector.from_singl v6))))); Types.snd = pc };
725 Types.snd = (Nat.S Nat.O) }
727 let { Types.fst = b6; Types.snd = v7 } =
732 prod_inv_rect_Type0 (ASM.next pmem pc)
733 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
734 (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
735 (ASM.DIRECT b10)))); Types.snd = pc0 };
736 Types.snd = (Nat.S Nat.O) })
738 prod_inv_rect_Type0 (ASM.next pmem pc)
739 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
740 (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
741 (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
744 let { Types.fst = b5; Types.snd = v6 } =
745 Vector.head (Nat.S Nat.O) v5
749 let { Types.fst = b6; Types.snd = v7 } =
754 { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A,
755 ASM.ACC_DPTR)); Types.snd = pc }; Types.snd =
756 (Nat.S (Nat.S Nat.O)) }
758 prod_inv_rect_Type0 (ASM.next pmem pc)
759 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
760 (ASM.RealInstruction (ASM.MOV (Types.Inr
761 { Types.fst = (ASM.BIT_ADDR b10); Types.snd =
762 ASM.CARRY }))); Types.snd = pc0 }; Types.snd =
763 (Nat.S (Nat.S Nat.O)) }))
765 let { Types.fst = b6; Types.snd = v7 } =
770 prod_inv_rect_Type0 (ASM.next pmem pc)
771 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
772 (ASM.ACALL (ASM.ADDR11
773 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
774 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
775 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
776 ((Nat.S (Nat.S Nat.O)), Bool.True,
777 (Vector.VCons ((Nat.S Nat.O), Bool.False,
778 (Vector.VCons (Nat.O, Bool.False,
779 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
780 Types.snd = (Nat.S (Nat.S Nat.O)) })
782 prod_inv_rect_Type0 (ASM.next pmem pc)
784 prod_inv_rect_Type0 (ASM.next pmem pc0)
785 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
786 (ASM.RealInstruction (ASM.MOV (Types.Inl
787 (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
788 Types.snd = (ASM.DATA16
789 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
790 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
791 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
792 (Nat.S (Nat.S Nat.O)))))))) b10 b20)) })))));
793 Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
796 let { Types.fst = b3; Types.snd = v4 } =
797 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
801 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
802 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
803 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
804 (ASM.DIRECT b10); Types.snd = (ASM.REGISTER v4) }))))));
805 Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })
807 let { Types.fst = b4; Types.snd = v5 } =
808 Vector.head (Nat.S (Nat.S Nat.O)) v4
812 let { Types.fst = b5; Types.snd = v6 } =
813 Vector.head (Nat.S Nat.O) v5
817 prod_inv_rect_Type0 (ASM.next pmem pc)
818 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
819 (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
820 (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT
821 b10); Types.snd = (ASM.INDIRECT
822 (Vector.from_singl v6)) })))))); Types.snd = pc0 };
823 Types.snd = (Nat.S (Nat.S Nat.O)) })
825 let { Types.fst = b6; Types.snd = v7 } =
830 prod_inv_rect_Type0 (ASM.next pmem pc)
832 prod_inv_rect_Type0 (ASM.next pmem pc0)
833 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
834 (ASM.RealInstruction (ASM.MOV (Types.Inl
835 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
836 (ASM.DIRECT b10); Types.snd = (ASM.DIRECT
837 b20) })))))); Types.snd = pc1 }; Types.snd =
838 (Nat.S (Nat.S Nat.O)) }))
840 { Types.fst = { Types.fst = (ASM.RealInstruction
841 (ASM.DIV (ASM.ACC_A, ASM.ACC_B))); Types.snd =
842 pc }; Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S
845 let { Types.fst = b5; Types.snd = v6 } =
846 Vector.head (Nat.S Nat.O) v5
850 let { Types.fst = b6; Types.snd = v7 } =
855 { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A,
856 ASM.ACC_PC)); Types.snd = pc }; Types.snd =
857 (Nat.S (Nat.S Nat.O)) }
859 prod_inv_rect_Type0 (ASM.next pmem pc)
860 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
861 (ASM.RealInstruction (ASM.ANL (Types.Inr
862 { Types.fst = ASM.CARRY; Types.snd =
863 (ASM.BIT_ADDR b10) }))); Types.snd = pc0 };
864 Types.snd = (Nat.S (Nat.S Nat.O)) }))
866 let { Types.fst = b6; Types.snd = v7 } =
871 prod_inv_rect_Type0 (ASM.next pmem pc)
872 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
873 (ASM.AJMP (ASM.ADDR11
874 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
875 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
876 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
877 ((Nat.S (Nat.S Nat.O)), Bool.True,
878 (Vector.VCons ((Nat.S Nat.O), Bool.False,
879 (Vector.VCons (Nat.O, Bool.False,
880 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
881 Types.snd = (Nat.S (Nat.S Nat.O)) })
883 prod_inv_rect_Type0 (ASM.next pmem pc)
884 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
885 (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 };
886 Types.snd = (Nat.S (Nat.S Nat.O)) }))))))))
888 let { Types.fst = b0; Types.snd = v1 } =
889 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0
893 let { Types.fst = b1; Types.snd = v2 } =
894 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
898 let { Types.fst = b2; Types.snd = v3 } =
899 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
903 let { Types.fst = b3; Types.snd = v4 } =
904 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
908 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
909 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
910 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
911 { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DATA
912 b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
915 let { Types.fst = b4; Types.snd = v5 } =
916 Vector.head (Nat.S (Nat.S Nat.O)) v4
920 let { Types.fst = b5; Types.snd = v6 } =
921 Vector.head (Nat.S Nat.O) v5
925 prod_inv_rect_Type0 (ASM.next pmem pc)
926 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
927 (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
928 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
929 (ASM.INDIRECT (Vector.from_singl v6)); Types.snd =
930 (ASM.DATA b10) }))))))); Types.snd = pc0 };
931 Types.snd = (Nat.S Nat.O) })
933 let { Types.fst = b6; Types.snd = v7 } =
938 prod_inv_rect_Type0 (ASM.next pmem pc)
940 prod_inv_rect_Type0 (ASM.next pmem pc0)
941 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
942 (ASM.RealInstruction (ASM.MOV (Types.Inl
943 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
944 (ASM.DIRECT b10); Types.snd = (ASM.DATA
945 b20) })))))); Types.snd = pc1 }; Types.snd =
946 (Nat.S (Nat.S (Nat.S Nat.O))) }))
948 prod_inv_rect_Type0 (ASM.next pmem pc)
949 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
950 (ASM.RealInstruction (ASM.MOV (Types.Inl
951 (Types.Inl (Types.Inl (Types.Inl (Types.Inl
952 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
953 b10) }))))))); Types.snd = pc0 }; Types.snd =
956 let { Types.fst = b5; Types.snd = v6 } =
957 Vector.head (Nat.S Nat.O) v5
961 let { Types.fst = b6; Types.snd = v7 } =
966 { Types.fst = { Types.fst = (ASM.RealInstruction
967 (ASM.JMP ASM.ACC_DPTR)); Types.snd = pc };
968 Types.snd = (Nat.S (Nat.S Nat.O)) }
970 prod_inv_rect_Type0 (ASM.next pmem pc)
971 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
972 (ASM.RealInstruction (ASM.ORL (Types.Inr
973 { Types.fst = ASM.CARRY; Types.snd =
974 (ASM.BIT_ADDR b10) }))); Types.snd = pc0 };
975 Types.snd = (Nat.S (Nat.S Nat.O)) }))
977 let { Types.fst = b6; Types.snd = v7 } =
982 prod_inv_rect_Type0 (ASM.next pmem pc)
983 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
984 (ASM.ACALL (ASM.ADDR11
985 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
986 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
987 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
988 ((Nat.S (Nat.S Nat.O)), Bool.False,
989 (Vector.VCons ((Nat.S Nat.O), Bool.True,
990 (Vector.VCons (Nat.O, Bool.True,
991 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
992 Types.snd = (Nat.S (Nat.S Nat.O)) })
994 prod_inv_rect_Type0 (ASM.next pmem pc)
995 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
996 (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
997 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
998 (Nat.S Nat.O)) })))))
1000 let { Types.fst = b3; Types.snd = v4 } =
1001 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1005 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL
1006 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1007 (ASM.REGISTER v4) }))); Types.snd = pc }; Types.snd =
1010 let { Types.fst = b4; Types.snd = v5 } =
1011 Vector.head (Nat.S (Nat.S Nat.O)) v4
1015 let { Types.fst = b5; Types.snd = v6 } =
1016 Vector.head (Nat.S Nat.O) v5
1020 { Types.fst = { Types.fst = (ASM.RealInstruction
1021 (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A;
1022 Types.snd = (ASM.INDIRECT
1023 (Vector.from_singl v6)) }))); Types.snd = pc };
1024 Types.snd = (Nat.S Nat.O) }
1026 let { Types.fst = b6; Types.snd = v7 } =
1027 Vector.head Nat.O v6
1031 prod_inv_rect_Type0 (ASM.next pmem pc)
1032 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1033 (ASM.RealInstruction (ASM.XRL (Types.Inl
1034 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT
1035 b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S
1038 prod_inv_rect_Type0 (ASM.next pmem pc)
1039 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1040 (ASM.RealInstruction (ASM.XRL (Types.Inl
1041 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
1042 b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S
1045 let { Types.fst = b5; Types.snd = v6 } =
1046 Vector.head (Nat.S Nat.O) v5
1050 let { Types.fst = b6; Types.snd = v7 } =
1051 Vector.head Nat.O v6
1055 prod_inv_rect_Type0 (ASM.next pmem pc)
1057 prod_inv_rect_Type0 (ASM.next pmem pc0)
1058 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1059 (ASM.RealInstruction (ASM.XRL (Types.Inr
1060 { Types.fst = (ASM.DIRECT b10); Types.snd =
1061 (ASM.DATA b20) }))); Types.snd = pc1 };
1062 Types.snd = (Nat.S (Nat.S Nat.O)) }))
1064 prod_inv_rect_Type0 (ASM.next pmem pc)
1065 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1066 (ASM.RealInstruction (ASM.XRL (Types.Inr
1067 { Types.fst = (ASM.DIRECT b10); Types.snd =
1068 ASM.ACC_A }))); Types.snd = pc0 }; Types.snd =
1071 let { Types.fst = b6; Types.snd = v7 } =
1072 Vector.head Nat.O v6
1076 prod_inv_rect_Type0 (ASM.next pmem pc)
1077 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1078 (ASM.AJMP (ASM.ADDR11
1079 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1080 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1081 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1082 ((Nat.S (Nat.S Nat.O)), Bool.False,
1083 (Vector.VCons ((Nat.S Nat.O), Bool.True,
1084 (Vector.VCons (Nat.O, Bool.True,
1085 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1086 Types.snd = (Nat.S (Nat.S Nat.O)) })
1088 prod_inv_rect_Type0 (ASM.next pmem pc)
1089 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1090 (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE
1091 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1092 (Nat.S Nat.O)) }))))))
1094 let { Types.fst = b2; Types.snd = v3 } =
1095 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1099 let { Types.fst = b3; Types.snd = v4 } =
1100 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1104 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL
1105 (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1106 (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd =
1109 let { Types.fst = b4; Types.snd = v5 } =
1110 Vector.head (Nat.S (Nat.S Nat.O)) v4
1114 let { Types.fst = b5; Types.snd = v6 } =
1115 Vector.head (Nat.S Nat.O) v5
1119 { Types.fst = { Types.fst = (ASM.RealInstruction
1120 (ASM.ANL (Types.Inl (Types.Inl { Types.fst =
1121 ASM.ACC_A; Types.snd = (ASM.INDIRECT
1122 (Vector.from_singl v6)) })))); Types.snd = pc };
1123 Types.snd = (Nat.S Nat.O) }
1125 let { Types.fst = b6; Types.snd = v7 } =
1126 Vector.head Nat.O v6
1130 prod_inv_rect_Type0 (ASM.next pmem pc)
1131 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1132 (ASM.RealInstruction (ASM.ANL (Types.Inl
1133 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1134 (ASM.DIRECT b10) })))); Types.snd = pc0 };
1135 Types.snd = (Nat.S Nat.O) })
1137 prod_inv_rect_Type0 (ASM.next pmem pc)
1138 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1139 (ASM.RealInstruction (ASM.ANL (Types.Inl
1140 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1141 (ASM.DATA b10) })))); Types.snd = pc0 };
1142 Types.snd = (Nat.S Nat.O) })))
1144 let { Types.fst = b5; Types.snd = v6 } =
1145 Vector.head (Nat.S Nat.O) v5
1149 let { Types.fst = b6; Types.snd = v7 } =
1150 Vector.head Nat.O v6
1154 prod_inv_rect_Type0 (ASM.next pmem pc)
1156 prod_inv_rect_Type0 (ASM.next pmem pc0)
1157 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1158 (ASM.RealInstruction (ASM.ANL (Types.Inl
1159 (Types.Inr { Types.fst = (ASM.DIRECT b10);
1160 Types.snd = (ASM.DATA b20) })))); Types.snd =
1161 pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
1163 prod_inv_rect_Type0 (ASM.next pmem pc)
1164 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1165 (ASM.RealInstruction (ASM.ANL (Types.Inl
1166 (Types.Inr { Types.fst = (ASM.DIRECT b10);
1167 Types.snd = ASM.ACC_A })))); Types.snd = pc0 };
1168 Types.snd = (Nat.S Nat.O) }))
1170 let { Types.fst = b6; Types.snd = v7 } =
1171 Vector.head Nat.O v6
1175 prod_inv_rect_Type0 (ASM.next pmem pc)
1176 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1177 (ASM.ACALL (ASM.ADDR11
1178 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1179 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1180 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1181 ((Nat.S (Nat.S Nat.O)), Bool.False,
1182 (Vector.VCons ((Nat.S Nat.O), Bool.True,
1183 (Vector.VCons (Nat.O, Bool.False,
1184 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1185 Types.snd = (Nat.S (Nat.S Nat.O)) })
1187 prod_inv_rect_Type0 (ASM.next pmem pc)
1188 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1189 (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE
1190 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1191 (Nat.S Nat.O)) })))))
1193 let { Types.fst = b3; Types.snd = v4 } =
1194 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1198 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL
1199 (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1200 (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd =
1203 let { Types.fst = b4; Types.snd = v5 } =
1204 Vector.head (Nat.S (Nat.S Nat.O)) v4
1208 let { Types.fst = b5; Types.snd = v6 } =
1209 Vector.head (Nat.S Nat.O) v5
1213 { Types.fst = { Types.fst = (ASM.RealInstruction
1214 (ASM.ORL (Types.Inl (Types.Inl { Types.fst =
1215 ASM.ACC_A; Types.snd = (ASM.INDIRECT
1216 (Vector.from_singl v6)) })))); Types.snd = pc };
1217 Types.snd = (Nat.S Nat.O) }
1219 let { Types.fst = b6; Types.snd = v7 } =
1220 Vector.head Nat.O v6
1224 prod_inv_rect_Type0 (ASM.next pmem pc)
1225 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1226 (ASM.RealInstruction (ASM.ORL (Types.Inl
1227 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1228 (ASM.DIRECT b10) })))); Types.snd = pc0 };
1229 Types.snd = (Nat.S Nat.O) })
1231 prod_inv_rect_Type0 (ASM.next pmem pc)
1232 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1233 (ASM.RealInstruction (ASM.ORL (Types.Inl
1234 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1235 (ASM.DATA b10) })))); Types.snd = pc0 };
1236 Types.snd = (Nat.S Nat.O) })))
1238 let { Types.fst = b5; Types.snd = v6 } =
1239 Vector.head (Nat.S Nat.O) v5
1243 let { Types.fst = b6; Types.snd = v7 } =
1244 Vector.head Nat.O v6
1248 prod_inv_rect_Type0 (ASM.next pmem pc)
1250 prod_inv_rect_Type0 (ASM.next pmem pc0)
1251 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1252 (ASM.RealInstruction (ASM.ORL (Types.Inl
1253 (Types.Inr { Types.fst = (ASM.DIRECT b10);
1254 Types.snd = (ASM.DATA b20) })))); Types.snd =
1255 pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
1257 prod_inv_rect_Type0 (ASM.next pmem pc)
1258 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1259 (ASM.RealInstruction (ASM.ORL (Types.Inl
1260 (Types.Inr { Types.fst = (ASM.DIRECT b10);
1261 Types.snd = ASM.ACC_A })))); Types.snd = pc0 };
1262 Types.snd = (Nat.S Nat.O) }))
1264 let { Types.fst = b6; Types.snd = v7 } =
1265 Vector.head Nat.O v6
1269 prod_inv_rect_Type0 (ASM.next pmem pc)
1270 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1271 (ASM.AJMP (ASM.ADDR11
1272 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1273 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1274 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1275 ((Nat.S (Nat.S Nat.O)), Bool.False,
1276 (Vector.VCons ((Nat.S Nat.O), Bool.True,
1277 (Vector.VCons (Nat.O, Bool.False,
1278 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1279 Types.snd = (Nat.S (Nat.S Nat.O)) })
1281 prod_inv_rect_Type0 (ASM.next pmem pc)
1282 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1283 (ASM.RealInstruction (ASM.JC (ASM.RELATIVE
1284 b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1285 (Nat.S Nat.O)) })))))))
1287 let { Types.fst = b1; Types.snd = v2 } =
1288 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
1292 let { Types.fst = b2; Types.snd = v3 } =
1293 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1297 let { Types.fst = b3; Types.snd = v4 } =
1298 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1302 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC
1303 (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
1304 Types.snd = (Nat.S Nat.O) }
1306 let { Types.fst = b4; Types.snd = v5 } =
1307 Vector.head (Nat.S (Nat.S Nat.O)) v4
1311 let { Types.fst = b5; Types.snd = v6 } =
1312 Vector.head (Nat.S Nat.O) v5
1316 { Types.fst = { Types.fst = (ASM.RealInstruction
1317 (ASM.ADDC (ASM.ACC_A, (ASM.INDIRECT
1318 (Vector.from_singl v6))))); Types.snd = pc };
1319 Types.snd = (Nat.S Nat.O) }
1321 let { Types.fst = b6; Types.snd = v7 } =
1322 Vector.head Nat.O v6
1326 prod_inv_rect_Type0 (ASM.next pmem pc)
1327 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1328 (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
1329 (ASM.DIRECT b10)))); Types.snd = pc0 };
1330 Types.snd = (Nat.S Nat.O) })
1332 prod_inv_rect_Type0 (ASM.next pmem pc)
1333 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1334 (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
1335 (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
1338 let { Types.fst = b5; Types.snd = v6 } =
1339 Vector.head (Nat.S Nat.O) v5
1343 let { Types.fst = b6; Types.snd = v7 } =
1344 Vector.head Nat.O v6
1348 { Types.fst = { Types.fst = (ASM.RealInstruction
1349 (ASM.RLC ASM.ACC_A)); Types.snd = pc };
1350 Types.snd = (Nat.S Nat.O) }
1352 { Types.fst = { Types.fst = (ASM.RealInstruction
1353 ASM.RETI); Types.snd = pc }; Types.snd = (Nat.S
1356 let { Types.fst = b6; Types.snd = v7 } =
1357 Vector.head Nat.O v6
1361 prod_inv_rect_Type0 (ASM.next pmem pc)
1362 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1363 (ASM.ACALL (ASM.ADDR11
1364 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1365 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1366 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1367 ((Nat.S (Nat.S Nat.O)), Bool.False,
1368 (Vector.VCons ((Nat.S Nat.O), Bool.False,
1369 (Vector.VCons (Nat.O, Bool.True,
1370 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1371 Types.snd = (Nat.S (Nat.S Nat.O)) })
1373 prod_inv_rect_Type0 (ASM.next pmem pc)
1375 prod_inv_rect_Type0 (ASM.next pmem pc0)
1376 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1377 (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR
1378 b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1379 Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
1381 let { Types.fst = b3; Types.snd = v4 } =
1382 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1386 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD
1387 (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
1388 Types.snd = (Nat.S Nat.O) }
1390 let { Types.fst = b4; Types.snd = v5 } =
1391 Vector.head (Nat.S (Nat.S Nat.O)) v4
1395 let { Types.fst = b5; Types.snd = v6 } =
1396 Vector.head (Nat.S Nat.O) v5
1400 { Types.fst = { Types.fst = (ASM.RealInstruction
1401 (ASM.ADD (ASM.ACC_A, (ASM.INDIRECT
1402 (Vector.from_singl v6))))); Types.snd = pc };
1403 Types.snd = (Nat.S Nat.O) }
1405 let { Types.fst = b6; Types.snd = v7 } =
1406 Vector.head Nat.O v6
1410 prod_inv_rect_Type0 (ASM.next pmem pc)
1411 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1412 (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
1413 (ASM.DIRECT b10)))); Types.snd = pc0 };
1414 Types.snd = (Nat.S Nat.O) })
1416 prod_inv_rect_Type0 (ASM.next pmem pc)
1417 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1418 (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
1419 (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
1422 let { Types.fst = b5; Types.snd = v6 } =
1423 Vector.head (Nat.S Nat.O) v5
1427 let { Types.fst = b6; Types.snd = v7 } =
1428 Vector.head Nat.O v6
1432 { Types.fst = { Types.fst = (ASM.RealInstruction
1433 (ASM.RL ASM.ACC_A)); Types.snd = pc };
1434 Types.snd = (Nat.S Nat.O) }
1436 { Types.fst = { Types.fst = (ASM.RealInstruction
1437 ASM.RET); Types.snd = pc }; Types.snd = (Nat.S
1440 let { Types.fst = b6; Types.snd = v7 } =
1441 Vector.head Nat.O v6
1445 prod_inv_rect_Type0 (ASM.next pmem pc)
1446 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1447 (ASM.AJMP (ASM.ADDR11
1448 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1449 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1450 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1451 ((Nat.S (Nat.S Nat.O)), Bool.False,
1452 (Vector.VCons ((Nat.S Nat.O), Bool.False,
1453 (Vector.VCons (Nat.O, Bool.True,
1454 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1455 Types.snd = (Nat.S (Nat.S Nat.O)) })
1457 prod_inv_rect_Type0 (ASM.next pmem pc)
1459 prod_inv_rect_Type0 (ASM.next pmem pc0)
1460 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1461 (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR
1462 b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1463 Types.snd = (Nat.S (Nat.S Nat.O)) })))))))
1465 let { Types.fst = b2; Types.snd = v3 } =
1466 Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1470 let { Types.fst = b3; Types.snd = v4 } =
1471 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1475 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC
1476 (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S
1479 let { Types.fst = b4; Types.snd = v5 } =
1480 Vector.head (Nat.S (Nat.S Nat.O)) v4
1484 let { Types.fst = b5; Types.snd = v6 } =
1485 Vector.head (Nat.S Nat.O) v5
1489 { Types.fst = { Types.fst = (ASM.RealInstruction
1490 (ASM.DEC (ASM.INDIRECT (Vector.from_singl v6))));
1491 Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
1493 let { Types.fst = b6; Types.snd = v7 } =
1494 Vector.head Nat.O v6
1498 prod_inv_rect_Type0 (ASM.next pmem pc)
1499 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1500 (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10)));
1501 Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
1503 { Types.fst = { Types.fst = (ASM.RealInstruction
1504 (ASM.DEC ASM.ACC_A)); Types.snd = pc };
1505 Types.snd = (Nat.S Nat.O) }))
1507 let { Types.fst = b5; Types.snd = v6 } =
1508 Vector.head (Nat.S Nat.O) v5
1512 let { Types.fst = b6; Types.snd = v7 } =
1513 Vector.head Nat.O v6
1517 { Types.fst = { Types.fst = (ASM.RealInstruction
1518 (ASM.RRC ASM.ACC_A)); Types.snd = pc };
1519 Types.snd = (Nat.S Nat.O) }
1521 prod_inv_rect_Type0 (ASM.next pmem pc)
1523 prod_inv_rect_Type0 (ASM.next pmem pc0)
1524 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1525 (ASM.LCALL (ASM.ADDR16
1526 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
1527 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1528 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1529 (Nat.S (Nat.S Nat.O)))))))) b10 b20)));
1530 Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
1533 let { Types.fst = b6; Types.snd = v7 } =
1534 Vector.head Nat.O v6
1538 prod_inv_rect_Type0 (ASM.next pmem pc)
1539 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1540 (ASM.ACALL (ASM.ADDR11
1541 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1542 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1543 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1544 ((Nat.S (Nat.S Nat.O)), Bool.False,
1545 (Vector.VCons ((Nat.S Nat.O), Bool.False,
1546 (Vector.VCons (Nat.O, Bool.False,
1547 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1548 Types.snd = (Nat.S (Nat.S Nat.O)) })
1550 prod_inv_rect_Type0 (ASM.next pmem pc)
1552 prod_inv_rect_Type0 (ASM.next pmem pc0)
1553 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1554 (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR
1555 b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1556 Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
1558 let { Types.fst = b3; Types.snd = v4 } =
1559 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1563 { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC
1564 (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S
1567 let { Types.fst = b4; Types.snd = v5 } =
1568 Vector.head (Nat.S (Nat.S Nat.O)) v4
1572 let { Types.fst = b5; Types.snd = v6 } =
1573 Vector.head (Nat.S Nat.O) v5
1577 { Types.fst = { Types.fst = (ASM.RealInstruction
1578 (ASM.INC (ASM.INDIRECT (Vector.from_singl v6))));
1579 Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
1581 let { Types.fst = b6; Types.snd = v7 } =
1582 Vector.head Nat.O v6
1586 prod_inv_rect_Type0 (ASM.next pmem pc)
1587 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1588 (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10)));
1589 Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
1591 { Types.fst = { Types.fst = (ASM.RealInstruction
1592 (ASM.INC ASM.ACC_A)); Types.snd = pc };
1593 Types.snd = (Nat.S Nat.O) }))
1595 let { Types.fst = b5; Types.snd = v6 } =
1596 Vector.head (Nat.S Nat.O) v5
1600 let { Types.fst = b6; Types.snd = v7 } =
1601 Vector.head Nat.O v6
1605 { Types.fst = { Types.fst = (ASM.RealInstruction
1606 (ASM.RR ASM.ACC_A)); Types.snd = pc };
1607 Types.snd = (Nat.S Nat.O) }
1609 prod_inv_rect_Type0 (ASM.next pmem pc)
1611 prod_inv_rect_Type0 (ASM.next pmem pc0)
1612 (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1613 (ASM.LJMP (ASM.ADDR16
1614 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
1615 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1616 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1617 (Nat.S (Nat.S Nat.O)))))))) b10 b20)));
1618 Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
1621 let { Types.fst = b6; Types.snd = v7 } =
1622 Vector.head Nat.O v6
1626 prod_inv_rect_Type0 (ASM.next pmem pc)
1627 (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1628 (ASM.AJMP (ASM.ADDR11
1629 (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1630 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1631 (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1632 ((Nat.S (Nat.S Nat.O)), Bool.False,
1633 (Vector.VCons ((Nat.S Nat.O), Bool.False,
1634 (Vector.VCons (Nat.O, Bool.False,
1635 Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1636 Types.snd = (Nat.S (Nat.S Nat.O)) })
1638 { Types.fst = { Types.fst = (ASM.RealInstruction
1639 ASM.NOP); Types.snd = pc }; Types.snd = (Nat.S
1643 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
1644 ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **)
1646 let { Types.fst = word; Types.snd = byte } = ASM.next pmem pc in
1647 fetch0 pmem word byte