open Preamble open BitVectorTrie open String open Exp open Arithmetic open Vector open FoldStuff open BitVector open Extranat open Integers open AST open LabelledObjects open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Extralib open Setoids open Monad open Option open Div_and_mod open Util open List open Lists open Bool open Relations open Nat open Positive open Identifiers open CostLabel open ASM open Types open Hints_declaration open Core_notation open Pts open Logic open Jmeq open Russell open Status open StatusProofs open Fetch open Hide open Division open Z open BitVectorZ open Pointers open Coqlib open Values open Events open IOMonad open IO open Sets open Listb open StructuredTraces open AbstractStatus (** val execute_1_preinstruction : (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus -> BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2 Status.preStatus **) let execute_1_preinstruction ticks cm addr_of instr s = let add_ticks1 = fun s0 -> Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) in let add_ticks2 = fun s0 -> Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock) in (match instr with | ASM.ADD (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let { Types.fst = result; Types.snd = flags } = Arithmetic.add_8_with_carry (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False in let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag) | ASM.ADDC (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in let { Types.fst = result; Types.snd = flags } = Arithmetic.add_8_with_carry (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag in let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag) | ASM.SUBB (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag in let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag) | ASM.INC addr -> (fun _ -> (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with | ASM.DIRECT d -> (fun _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' (ASM.DIRECT d) result) | ASM.INDIRECT i -> (fun _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True (ASM.INDIRECT i)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' (ASM.INDIRECT i) result) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True (ASM.REGISTER r)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' (ASM.REGISTER r) result) | ASM.ACC_A -> (fun _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True ASM.ACC_A) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' ASM.ACC_A result) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> let s' = add_ticks1 s in let { Types.fst = carry; Types.snd = bl } = Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s' Status.SFR_DPL) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let { Types.fst = carry0; Types.snd = bu } = Arithmetic.full_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s' Status.SFR_DPH) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) carry in let s'' = Status.set_8051_sfr cm s' Status.SFR_DPL bl in Status.set_8051_sfr cm s'' Status.SFR_DPH bu) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.DEC addr -> (fun _ -> let s0 = add_ticks1 s in let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) result) | ASM.MUL (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let acc_a_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in let acc_b_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_B) in let product = Nat.times acc_a_nat acc_b_nat in let low = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.modulus product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in let high = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.division product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A low in Status.set_8051_sfr cm s1 Status.SFR_ACC_B high) | ASM.DIV (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let acc_a_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in let acc_b_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_B) in (match acc_b_nat with | Nat.O -> Status.set_flags cm s0 Bool.False Types.None Bool.True | Nat.S o -> let q = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.division acc_a_nat (Nat.S o)) in let r = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.modulus acc_a_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A q in let s2 = Status.set_8051_sfr cm s1 Status.SFR_ACC_B r in Status.set_flags cm s2 Bool.False Types.None Bool.False)) | ASM.DA addr -> (fun _ -> let s0 = add_ticks1 s in let { Types.fst = acc_nu; Types.snd = acc_nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in (match Bool.orb (Util.gtb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nl) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) (Status.get_ac_flag cm s0) with | Bool.True -> let { Types.fst = result; Types.snd = flags } = Arithmetic.add_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) Bool.False in let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let { Types.fst = acc_nu'; Types.snd = acc_nl' } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) result in (match Bool.orb (Util.gtb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu') (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) cy_flag with | Bool.True -> let nu = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu' (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) in let new_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl' in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in Status.set_flags cm s1 cy_flag (Types.Some (Status.get_ac_flag cm s1)) (Status.get_ov_flag cm s1) | Bool.False -> s0) | Bool.False -> s0)) | ASM.JC addr -> (fun _ -> match Status.get_cy_flag cm s with | Bool.True -> let s0 = add_ticks1 s in Status.set_program_counter cm s0 (addr_of addr s0) | Bool.False -> let s0 = add_ticks2 s in s0) | ASM.JNC addr -> (fun _ -> match Bool.notb (Status.get_cy_flag cm s) with | Bool.True -> let s0 = add_ticks1 s in Status.set_program_counter cm s0 (addr_of addr s0) | Bool.False -> let s0 = add_ticks2 s in s0) | ASM.JB (addr1, addr2) -> (fun _ -> match Status.get_arg_1 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1) Bool.False with | Bool.True -> let s0 = add_ticks1 s in Status.set_program_counter cm s0 (addr_of addr2 s0) | Bool.False -> let s0 = add_ticks2 s in s0) | ASM.JNB (addr1, addr2) -> (fun _ -> match Bool.notb (Status.get_arg_1 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1) Bool.False) with | Bool.True -> let s0 = add_ticks1 s in Status.set_program_counter cm s0 (addr_of addr2 s0) | Bool.False -> let s0 = add_ticks2 s in s0) | ASM.JBC (addr1, addr2) -> (fun _ -> let s0 = Status.set_arg_1 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) Bool.False in (match Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1) Bool.False with | Bool.True -> let s1 = add_ticks1 s0 in Status.set_program_counter cm s1 (addr_of addr2 s1) | Bool.False -> let s1 = add_ticks2 s0 in s1)) | ASM.JZ addr -> (fun _ -> match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s Status.SFR_ACC_A) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) with | Bool.True -> let s0 = add_ticks1 s in Status.set_program_counter cm s0 (addr_of addr s0) | Bool.False -> let s0 = add_ticks2 s in s0) | ASM.JNZ addr -> (fun _ -> match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s Status.SFR_ACC_A) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) with | Bool.True -> let s0 = add_ticks1 s in Status.set_program_counter cm s0 (addr_of addr s0) | Bool.False -> let s0 = add_ticks2 s in s0) | ASM.CJNE (addr1, addr2) -> (fun _ -> match addr1 with | Types.Inl l -> let { Types.fst = addr10; Types.snd = addr2' } = l in let new_cy = Util.ltb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10))) (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) in (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10)) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) with | Bool.True -> let s0 = add_ticks1 s in let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in Status.set_flags cm s1 new_cy Types.None (Status.get_ov_flag cm s1) | Bool.False -> let s0 = add_ticks2 s in Status.set_flags cm s0 new_cy Types.None (Status.get_ov_flag cm s0)) | Types.Inr r' -> let { Types.fst = addr10; Types.snd = addr2' } = r' in let new_cy = Util.ltb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10))) (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) in (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10)) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) with | Bool.True -> let s0 = add_ticks1 s in let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in Status.set_flags cm s1 new_cy Types.None (Status.get_ov_flag cm s1) | Bool.False -> let s0 = add_ticks2 s in Status.set_flags cm s0 new_cy Types.None (Status.get_ov_flag cm s0))) | ASM.DJNZ (addr1, addr2) -> (fun _ -> let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_arg_8 cm s Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in let s0 = Status.set_arg_8 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) result in (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) result (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) with | Bool.True -> let s1 = add_ticks1 s0 in Status.set_program_counter cm s1 (addr_of addr2 s1) | Bool.False -> let s1 = add_ticks2 s0 in s1)) | ASM.ANL addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> (match l with | Types.Inl l' -> let { Types.fst = addr1; Types.snd = addr2 } = l' in let and_val = BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) and_val | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let and_val = BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) and_val) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let and_val = Bool.andb (Status.get_cy_flag cm s0) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.True) in Status.set_flags cm s0 and_val Types.None (Status.get_ov_flag cm s0))) | ASM.ORL addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> (match l with | Types.Inl l' -> let { Types.fst = addr1; Types.snd = addr2 } = l' in let or_val = BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Data, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) or_val | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let or_val = BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) or_val) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let or_val = Bool.orb (Status.get_cy_flag cm s0) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.True) in Status.set_flags cm s0 or_val Types.None (Status.get_ov_flag cm s0))) | ASM.XRL addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l' -> let { Types.fst = addr1; Types.snd = addr2 } = l' in let xor_val = BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) xor_val | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let xor_val = BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) xor_val)) | ASM.CLR addr -> (fun _ -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> let s0 = add_ticks1 s in Status.set_arg_8 cm s0 ASM.ACC_A (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> let s0 = add_ticks1 s in Status.set_arg_1 cm s0 ASM.CARRY Bool.False) | ASM.BIT_ADDR b -> (fun _ -> let s0 = add_ticks1 s in Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.False) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.CPL addr -> (fun _ -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_acc = BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) old_acc in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_arg_1 cm s0 ASM.CARRY Bool.True in let new_cy_flag = Bool.notb old_cy_flag in Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag) | ASM.BIT_ADDR b -> (fun _ -> let s0 = add_ticks1 s in let old_bit = Status.get_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.True in let new_bit = Bool.notb old_bit in Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) new_bit) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.RL x -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_acc = Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.RLC x -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) old_acc in let new_acc = Vector.shift_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc old_cy_flag in let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc) | ASM.RR x -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_acc = Vector.rotate_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.RRC x -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_cy_flag = Vector.get_index' (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) Nat.O old_acc in let new_acc = Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) (Nat.S Nat.O) old_acc old_cy_flag in let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc) | ASM.SWAP x -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let { Types.fst = nu; Types.snd = nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) old_acc in let new_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) nl nu in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.MOV addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> (match l with | Types.Inl l' -> (match l' with | Types.Inl l'' -> (match l'' with | Types.Inl l''' -> (match l''' with | Types.Inl l'''' -> let { Types.fst = addr1; Types.snd = addr2 } = l'''' in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) | Types.Inr r'''' -> let { Types.fst = addr1; Types.snd = addr2 } = r'''' in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2))) | Types.Inr r''' -> let { Types.fst = addr1; Types.snd = addr2 } = r''' in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2))) | Types.Inr r'' -> let { Types.fst = addr1; Types.snd = addr2 } = r'' in Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)))) addr2)) addr1) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in Status.set_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.False)) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in Status.set_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.False))) | ASM.MOVX addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> let { Types.fst = addr1; Types.snd = addr2 } = l in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)))) | ASM.SETB b -> (fun _ -> let s0 = add_ticks1 s in Status.set_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) b) Bool.False) | ASM.PUSH addr -> (fun _ -> let s0 = add_ticks1 s in let new_sp = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in Status.write_at_stack_pointer cm s1 (Status.get_arg_8 cm s1 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr))) | ASM.POP addr -> (fun _ -> let s0 = add_ticks1 s in let contents = Status.read_at_stack_pointer cm s0 in let { Types.fst = new_sp; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) contents) | ASM.XCH (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let old_addr = Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2) in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A old_addr in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) old_acc) | ASM.XCHD (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let { Types.fst = acc_nu; Types.snd = acc_nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in let { Types.fst = arg_nu; Types.snd = arg_nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in let new_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu arg_nl in let new_arg = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) arg_nu acc_nl in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) new_arg) | ASM.RET -> (fun _ -> let s0 = add_ticks1 s in let high_bits = Status.read_at_stack_pointer cm s0 in let { Types.fst = new_sp; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in let low_bits = Status.read_at_stack_pointer cm s1 in let { Types.fst = new_sp0; Types.snd = flags0 } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in let new_pc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits in Status.set_program_counter cm s2 new_pc) | ASM.RETI -> (fun _ -> let s0 = add_ticks1 s in let high_bits = Status.read_at_stack_pointer cm s0 in let { Types.fst = new_sp; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in let low_bits = Status.read_at_stack_pointer cm s1 in let { Types.fst = new_sp0; Types.snd = flags0 } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in let new_pc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits in Status.set_program_counter cm s2 new_pc) | ASM.NOP -> (fun _ -> let s0 = add_ticks1 s in s0) | ASM.JMP acc_dptr -> (fun _ -> let s0 = add_ticks1 s in let jmp_addr = Status.get_arg_16 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr) in Status.set_program_counter cm s0 jmp_addr)) __ (** val execute_1_preinstruction_ok' : (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus -> BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2 Status.preStatus Types.sig0 **) let execute_1_preinstruction_ok' ticks cm addr_of instr s = let add_ticks1 = fun s0 -> Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) in let add_ticks2 = fun s0 -> Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock) in (match instr with | ASM.ADD (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in (let { Types.fst = result; Types.snd = flags } = Arithmetic.add_8_with_carry (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) Bool.False in (fun _ -> let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __) | ASM.ADDC (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in (let { Types.fst = result; Types.snd = flags } = Arithmetic.add_8_with_carry (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag in (fun _ -> let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __) | ASM.SUBB (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in (let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) old_cy_flag in (fun _ -> let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in let ac_flag = Vector.get_index' (Nat.S Nat.O) (Nat.S Nat.O) flags in let ov_flag = Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags in let s1 = Status.set_arg_8 cm s0 ASM.ACC_A result in Status.set_flags cm s1 cy_flag (Types.Some ac_flag) ov_flag)) __) | ASM.INC addr -> (fun _ -> (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with | ASM.DIRECT d -> (fun _ _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True (ASM.DIRECT d)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' (ASM.DIRECT d) result) | ASM.INDIRECT i -> (fun _ _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True (ASM.INDIRECT i)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' (ASM.INDIRECT i) result) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True (ASM.REGISTER r)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' (ASM.REGISTER r) result) | ASM.ACC_A -> (fun _ _ -> let s' = add_ticks1 s in let result = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s' Bool.True ASM.ACC_A) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in Status.set_arg_8 cm s' ASM.ACC_A result) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ _ -> let s' = add_ticks1 s in (let { Types.fst = carry; Types.snd = bl } = Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s' Status.SFR_DPL) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in (fun _ -> (let { Types.fst = carry0; Types.snd = bu } = Arithmetic.full_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s' Status.SFR_DPH) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) carry in (fun _ -> let s1 = Status.set_8051_sfr cm s' Status.SFR_DPL bl in Status.set_8051_sfr cm s1 Status.SFR_DPH bu)) __)) __) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ __) | ASM.DEC addr -> (fun _ -> let s0 = add_ticks1 s in (let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) result)) __) | ASM.MUL (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let acc_a_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in let acc_b_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_B) in let product = Nat.times acc_a_nat acc_b_nat in let low = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.modulus product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in let high = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.division product (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A low in Status.set_8051_sfr cm s1 Status.SFR_ACC_B high) | ASM.DIV (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let acc_a_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in let acc_b_nat = Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_B) in (match acc_b_nat with | Nat.O -> (fun _ -> Status.set_flags cm s0 Bool.False Types.None Bool.True) | Nat.S o -> (fun _ -> let q = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.division acc_a_nat (Nat.S o)) in let r = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Util.modulus acc_a_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A q in let s2 = Status.set_8051_sfr cm s1 Status.SFR_ACC_B r in Status.set_flags cm s2 Bool.False Types.None Bool.False)) __) | ASM.DA addr -> (fun _ -> let s0 = add_ticks1 s in (let { Types.fst = acc_nu; Types.snd = acc_nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in (fun _ -> (match Bool.orb (Util.gtb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nl) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) (Status.get_ac_flag cm s0) with | Bool.True -> (fun _ -> (let { Types.fst = result; Types.snd = flags } = Arithmetic.add_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) Bool.False in (fun _ -> let cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags in (let { Types.fst = acc_nu'; Types.snd = acc_nl' } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) result in (fun _ -> (match Bool.orb (Util.gtb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu') (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) cy_flag with | Bool.True -> (fun _ -> let nu = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu' (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) in let new_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl' in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in Status.set_flags cm s1 cy_flag (Types.Some (Status.get_ac_flag cm s1)) (Status.get_ov_flag cm s1)) | Bool.False -> (fun _ -> s0)) __)) __)) __) | Bool.False -> (fun _ -> s0)) __)) __) | ASM.JC addr -> (fun _ -> (match Status.get_cy_flag cm s with | Bool.True -> (fun _ -> let s1 = add_ticks1 s in Status.set_program_counter cm s1 (addr_of addr s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s in s1)) __) | ASM.JNC addr -> (fun _ -> (match Bool.notb (Status.get_cy_flag cm s) with | Bool.True -> (fun _ -> let s1 = add_ticks1 s in Status.set_program_counter cm s1 (addr_of addr s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s in s1)) __) | ASM.JB (addr1, addr2) -> (fun _ -> (match Status.get_arg_1 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1) Bool.False with | Bool.True -> (fun _ -> let s1 = add_ticks1 s in Status.set_program_counter cm s1 (addr_of addr2 s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s in s1)) __) | ASM.JNB (addr1, addr2) -> (fun _ -> (match Bool.notb (Status.get_arg_1 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1) Bool.False) with | Bool.True -> (fun _ -> let s1 = add_ticks1 s in Status.set_program_counter cm s1 (addr_of addr2 s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s in s1)) __) | ASM.JBC (addr1, addr2) -> (fun _ -> let s0 = Status.set_arg_1 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) Bool.False in (match Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr1) Bool.False with | Bool.True -> (fun _ -> let s1 = add_ticks1 s0 in Status.set_program_counter cm s1 (addr_of addr2 s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s0 in s1)) __) | ASM.JZ addr -> (fun _ -> (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s Status.SFR_ACC_A) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) with | Bool.True -> (fun _ -> let s1 = add_ticks1 s in Status.set_program_counter cm s1 (addr_of addr s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s in s1)) __) | ASM.JNZ addr -> (fun _ -> (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s Status.SFR_ACC_A) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) with | Bool.True -> (fun _ -> let s1 = add_ticks1 s in Status.set_program_counter cm s1 (addr_of addr s1)) | Bool.False -> (fun _ -> let s1 = add_ticks2 s in s1)) __) | ASM.CJNE (addr1, addr2) -> (fun _ -> match addr1 with | Types.Inl l -> let { Types.fst = addr10; Types.snd = addr2' } = l in let new_cy = Util.ltb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10))) (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) in (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10)) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) with | Bool.True -> let s0 = add_ticks1 s in let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in Status.set_flags cm s1 new_cy Types.None (Status.get_ov_flag cm s1) | Bool.False -> let s0 = add_ticks2 s in Status.set_flags cm s0 new_cy Types.None (Status.get_ov_flag cm s0)) | Types.Inr r' -> let { Types.fst = addr10; Types.snd = addr2' } = r' in let new_cy = Util.ltb (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10))) (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) in (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr10)) (Status.get_arg_8 cm s Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2'))) with | Bool.True -> let s0 = add_ticks1 s in let s1 = Status.set_program_counter cm s0 (addr_of addr2 s0) in Status.set_flags cm s1 new_cy Types.None (Status.get_ov_flag cm s1) | Bool.False -> let s0 = add_ticks2 s in Status.set_flags cm s0 new_cy Types.None (Status.get_ov_flag cm s0))) | ASM.DJNZ (addr1, addr2) -> (fun _ -> (let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_arg_8 cm s Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> let s1 = Status.set_arg_8 cm s (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) result in (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) result (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) with | Bool.True -> (fun _ -> let s2 = add_ticks1 s1 in Status.set_program_counter cm s2 (addr_of addr2 s2)) | Bool.False -> (fun _ -> let s2 = add_ticks2 s1 in s2)) __)) __) | ASM.ANL addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> (match l with | Types.Inl l' -> let { Types.fst = addr1; Types.snd = addr2 } = l' in let and_val = BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) and_val | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let and_val = BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) and_val) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let and_val = Bool.andb (Status.get_cy_flag cm s0) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.True) in Status.set_flags cm s0 and_val Types.None (Status.get_ov_flag cm s0))) | ASM.ORL addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> (match l with | Types.Inl l' -> let { Types.fst = addr1; Types.snd = addr2 } = l' in let or_val = BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Data, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) or_val | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let or_val = BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) or_val) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let or_val = Bool.orb (Status.get_cy_flag cm s0) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.True) in Status.set_flags cm s0 or_val Types.None (Status.get_ov_flag cm s0))) | ASM.XRL addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l' -> let { Types.fst = addr1; Types.snd = addr2 } = l' in let xor_val = BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) xor_val | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in let xor_val = BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr1)) (Status.get_arg_8 cm s0 Bool.True (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) xor_val)) | ASM.CLR addr -> (fun _ -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ _ -> let s0 = add_ticks1 s in Status.set_arg_8 cm s0 ASM.ACC_A (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ _ -> let s0 = add_ticks1 s in Status.set_arg_1 cm s0 ASM.CARRY Bool.False) | ASM.BIT_ADDR b -> (fun _ _ -> let s0 = add_ticks1 s in Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.False) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ __) | ASM.CPL addr -> (fun _ -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_acc = BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) old_acc in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_arg_1 cm s0 ASM.CARRY Bool.True in let new_cy_flag = Bool.notb old_cy_flag in Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag) | ASM.BIT_ADDR b -> (fun _ _ -> let s0 = add_ticks1 s in let old_bit = Status.get_arg_1 cm s0 (ASM.BIT_ADDR b) Bool.True in let new_bit = Bool.notb old_bit in Status.set_arg_1 cm s0 (ASM.BIT_ADDR b) new_bit) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ __) | ASM.RL x -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_acc = Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.RLC x -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_cy_flag = Vector.get_index' Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) old_acc in let new_acc = Vector.shift_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc old_cy_flag in let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc) | ASM.RR x -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_acc = Vector.rotate_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O) old_acc in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc) | ASM.RRC x -> (fun _ -> let s0 = add_ticks1 s in let old_cy_flag = Status.get_cy_flag cm s0 in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let new_cy_flag = Vector.get_index' (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) Nat.O old_acc in let new_acc = Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) (Nat.S Nat.O) old_acc old_cy_flag in let s1 = Status.set_arg_1 cm s0 ASM.CARRY new_cy_flag in Status.set_8051_sfr cm s1 Status.SFR_ACC_A new_acc) | ASM.SWAP x -> (fun _ -> let s0 = add_ticks1 s in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in (let { Types.fst = nu; Types.snd = nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) old_acc in (fun _ -> let new_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) nl nu in Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc)) __) | ASM.MOV addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> (match l with | Types.Inl l' -> (match l' with | Types.Inl l'' -> (match l'' with | Types.Inl l''' -> (match l''' with | Types.Inl l'''' -> let { Types.fst = addr1; Types.snd = addr2 } = l'''' in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) | Types.Inr r'''' -> let { Types.fst = addr1; Types.snd = addr2 } = r'''' in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2))) | Types.Inr r''' -> let { Types.fst = addr1; Types.snd = addr2 } = r''' in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2))) | Types.Inr r'' -> let { Types.fst = addr1; Types.snd = addr2 } = r'' in Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)))) addr2)) addr1) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in Status.set_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.False)) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in Status.set_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) addr1) (Status.get_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S Nat.O)) (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O), ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))))) addr2) Bool.False))) | ASM.MOVX addr -> (fun _ -> let s0 = add_ticks1 s in (match addr with | Types.Inl l -> let { Types.fst = addr1; Types.snd = addr2 } = l in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) | Types.Inr r -> let { Types.fst = addr1; Types.snd = addr2 } = r in Status.set_arg_8 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr1) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Acc_a, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)))) | ASM.SETB b -> (fun _ -> let s0 = add_ticks1 s in Status.set_arg_1 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S Nat.O) (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) b) Bool.False) | ASM.PUSH addr -> (fun _ -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr with | ASM.DIRECT d -> (fun _ _ -> let s0 = add_ticks1 s in let new_sp = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in Status.write_at_stack_pointer cm s1 (Status.get_arg_8 cm s1 Bool.False (ASM.DIRECT d))) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ __) | ASM.POP addr -> (fun _ -> let s0 = add_ticks1 s in let contents = Status.read_at_stack_pointer cm s0 in (let { Types.fst = new_sp; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr) contents)) __) | ASM.XCH (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in let old_addr = Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2) in let old_acc = Status.get_8051_sfr cm s0 Status.SFR_ACC_A in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A old_addr in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) old_acc) | ASM.XCHD (addr1, addr2) -> (fun _ -> let s0 = add_ticks1 s in (let { Types.fst = acc_nu; Types.snd = acc_nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) in (fun _ -> (let { Types.fst = arg_nu; Types.snd = arg_nl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Status.get_arg_8 cm s0 Bool.False (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))))))))) addr2)) in (fun _ -> let new_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) acc_nu arg_nl in let new_arg = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) arg_nu acc_nl in let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) addr2) new_arg)) __)) __) | ASM.RET -> (fun _ -> let s0 = add_ticks1 s in let high_bits = Status.read_at_stack_pointer cm s0 in (let { Types.fst = new_sp; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in let low_bits = Status.read_at_stack_pointer cm s1 in (let { Types.fst = new_sp0; Types.snd = flags0 } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in let new_pc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits in Status.set_program_counter cm s2 new_pc)) __)) __) | ASM.RETI -> (fun _ -> let s0 = add_ticks1 s in let high_bits = Status.read_at_stack_pointer cm s0 in (let { Types.fst = new_sp; Types.snd = flags } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s0 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> let s1 = Status.set_8051_sfr cm s0 Status.SFR_SP new_sp in let low_bits = Status.read_at_stack_pointer cm s1 in (let { Types.fst = new_sp0; Types.snd = flags0 } = Arithmetic.sub_8_with_carry (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) Bool.False in (fun _ -> let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in let new_pc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits in Status.set_program_counter cm s2 new_pc)) __)) __) | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0) | ASM.JMP acc_dptr -> (fun _ -> let s0 = add_ticks1 s in let jmp_addr = Status.get_arg_16 cm s0 (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr) in Status.set_program_counter cm s0 jmp_addr)) __ (** val compute_target_of_unconditional_jump : BitVector.word -> ASM.instruction -> BitVector.word **) let compute_target_of_unconditional_jump program_counter = function | ASM.ACALL x -> BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) | ASM.LCALL x -> BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) | ASM.AJMP addr -> Types.pi1 ((match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 a -> (fun _ -> (let { Types.fst = pc_bu; Types.snd = pc_bl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) program_counter in (fun _ -> let new_addr = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) pc_bu a in new_addr)) __) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.LJMP addr -> Types.pi1 ((match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 a -> (fun _ -> a)) __) | ASM.SJMP addr -> Types.pi1 ((match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE r -> (fun _ -> Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter (Arithmetic.sign_extension r)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.MOVC (x, x0) -> BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) | ASM.RealInstruction x -> BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (** val is_unconditional_jump : ASM.instruction -> Bool.bool **) let is_unconditional_jump = function | ASM.ACALL x -> Bool.False | ASM.LCALL x -> Bool.False | ASM.AJMP x -> Bool.True | ASM.LJMP x -> Bool.True | ASM.SJMP x -> Bool.True | ASM.MOVC (x, x0) -> Bool.False | ASM.RealInstruction x -> Bool.False (** val program_counter_after_other : BitVector.word -> ASM.instruction -> BitVector.word **) let program_counter_after_other program_counter instruction = match is_unconditional_jump instruction with | Bool.True -> compute_target_of_unconditional_jump program_counter instruction | Bool.False -> program_counter (** val addr_of_relative : 'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word **) let addr_of_relative cm x s = (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative, Vector.VEmpty)) x with | ASM.DIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE r -> (fun _ -> Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) s.Status.program_counter (Arithmetic.sign_extension r)) | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *))) __ (** val execute_1_0 : BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod -> Status.status Types.sig0 **) let execute_1_0 cm s0 instr_pc_ticks = (let { Types.fst = instr_pc; Types.snd = ticks } = instr_pc_ticks in (fun _ -> (let { Types.fst = instr; Types.snd = pc } = { Types.fst = instr_pc.Types.fst; Types.snd = instr_pc.Types.snd } in (fun _ -> let s = Status.set_program_counter cm s0 pc in (match instr with | ASM.ACALL addr -> (fun _ -> let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 a -> (fun _ -> let new_sp = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp in let { Types.fst = pc_bu; Types.snd = pc_bl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) s2.Status.program_counter in let s3 = Status.write_at_stack_pointer cm s2 pc_bl in let new_sp0 = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s3 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s4 = Status.set_8051_sfr cm s3 Status.SFR_SP new_sp0 in let s5 = Status.write_at_stack_pointer cm s4 pc_bu in let { Types.fst = fiv; Types.snd = thr' } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) pc_bu in let new_addr = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) fiv a in Status.set_program_counter cm s5 new_addr) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.LCALL addr -> (fun _ -> let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 a -> (fun _ -> let new_sp = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp in let { Types.fst = pc_bu; Types.snd = pc_bl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) s2.Status.program_counter in let s3 = Status.write_at_stack_pointer cm s2 pc_bl in let new_sp0 = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s3 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s4 = Status.set_8051_sfr cm s3 Status.SFR_SP new_sp0 in let s5 = Status.write_at_stack_pointer cm s4 pc_bu in Status.set_program_counter cm s5 a)) __) | ASM.AJMP addr -> (fun _ -> let new_pc = compute_target_of_unconditional_jump s.Status.program_counter instr in let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in Status.set_program_counter cm s1 new_pc) | ASM.LJMP addr -> (fun _ -> let new_pc = compute_target_of_unconditional_jump s.Status.program_counter instr in let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in Status.set_program_counter cm s1 new_pc) | ASM.SJMP addr -> (fun _ -> let new_pc = compute_target_of_unconditional_jump s.Status.program_counter instr in let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in Status.set_program_counter cm s1 new_pc) | ASM.MOVC (addr1, addr2) -> (fun _ -> let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_dptr, (Vector.VCons (Nat.O, ASM.Acc_pc, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> let big_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Status.get_8051_sfr cm s1 Status.SFR_ACC_A) in let dptr = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s1 Status.SFR_DPH) (Status.get_8051_sfr cm s1 Status.SFR_DPL) in let new_addr = Arithmetic.add (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) dptr big_acc in let result = BitVectorTrie.lookup (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) new_addr cm (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) in Status.set_8051_sfr cm s1 Status.SFR_ACC_A result) | ASM.ACC_PC -> (fun _ -> let big_acc = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Status.get_8051_sfr cm s1 Status.SFR_ACC_A) in let new_addr = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) s1.Status.program_counter big_acc in let result = BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) new_addr cm (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) in Status.set_8051_sfr cm s1 Status.SFR_ACC_A result) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.RealInstruction instr' -> (fun _ -> execute_1_preinstruction { Types.fst = ticks; Types.snd = ticks } cm (addr_of_relative cm) instr' s)) __)) __)) __ (** val current_instruction_cost : BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat **) let current_instruction_cost cm s = (Fetch.fetch cm s.Status.program_counter).Types.snd (** val execute_1' : BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Status.status Types.sig0 **) let execute_1' cm s = let instr_pc_ticks = Fetch.fetch cm s.Status.program_counter in Types.pi1 (execute_1_0 cm s instr_pc_ticks) (** val execute_1 : BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Status.status **) let execute_1 cm s = Types.pi1 (execute_1' cm s) (** val execute_1_pseudo_instruction0 : (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) -> Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word -> Status.pseudoStatus **) let execute_1_pseudo_instruction0 ticks cm addr_of_label addr_of_symbol s instr pc = let s0 = Status.set_program_counter cm s pc in let s1 = match instr with | ASM.Instruction instr0 -> execute_1_preinstruction ticks cm (fun x y -> addr_of_label x) instr0 s0 | ASM.Comment cmt -> Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) | ASM.Cost cst -> s0 | ASM.Jmp jmp -> let s1 = Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) in Status.set_program_counter cm s1 (addr_of_label jmp) | ASM.Jnz (acc, dst1, dst2) -> (match Bool.notb (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s0 Status.SFR_ACC_A) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) with | Bool.True -> let s1 = Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) in Status.set_program_counter cm s1 (addr_of_label dst1) | Bool.False -> let s1 = Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock) in Status.set_program_counter cm s1 (addr_of_label dst2)) | ASM.Call call -> let s1 = Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) in let a = addr_of_label call in let new_sp = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s1 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp in let { Types.fst = pc_bu; Types.snd = pc_bl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) s2.Status.program_counter in let s3 = Status.write_at_stack_pointer cm s2 pc_bl in let new_sp0 = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Status.get_8051_sfr cm s3 Status.SFR_SP) (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)) in let s4 = Status.set_8051_sfr cm s3 Status.SFR_SP new_sp0 in let s5 = Status.write_at_stack_pointer cm s4 pc_bu in Status.set_program_counter cm s5 a | ASM.Mov (dst, ident, off) -> let s1 = Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock) in let v = (Arithmetic.add_16_with_carry (addr_of_symbol ident) off Bool.False).Types.fst in (match dst with | Types.Inl dptr -> Status.set_arg_16 cm s1 v dptr | Types.Inr pr -> let v' = match pr.Types.snd with | ASM.HIGH -> (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) v).Types.fst | ASM.LOW -> (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) v).Types.snd in Status.set_arg_8 cm s1 (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))))))))))))) pr.Types.fst) v') in s1 (** val execute_1_pseudo_instruction : ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat) Types.prod) -> (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) -> Status.pseudoStatus -> Status.pseudoStatus **) let execute_1_pseudo_instruction cm ticks_of addr_of_label addr_of_symbol s = let { Types.fst = instr; Types.snd = pc } = ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter in let ticks = ticks_of s.Status.program_counter __ in execute_1_pseudo_instruction0 ticks cm addr_of_label addr_of_symbol s instr pc (** val execute : Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Status.status **) let rec execute n cm s = match n with | Nat.O -> s | Nat.S o -> execute o cm (execute_1 cm s)