open Preamble 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 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 Interpret (** val aSMRegisterRets : ASM.subaddressing_mode List.list **) let aSMRegisterRets = List.Cons ((ASM.DIRECT (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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), (List.Cons ((ASM.DIRECT (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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))))), (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))))))), List.Nil))))))) (** val as_result_of_finaladdr : 'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int Types.option **) let as_result_of_finaladdr cm st finaladdr = match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) st.Status.program_counter finaladdr with | Bool.True -> let vals = List.map (fun h -> Status.get_arg_8 cm st 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.Registr, 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)))))))))))))))))))) h)) aSMRegisterRets in let dummy = BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) in let first_byte = fun l -> match l with | List.Nil -> { Types.fst = dummy; Types.snd = List.Nil } | List.Cons (hd, tl) -> { Types.fst = hd; Types.snd = tl } in let { Types.fst = b1; Types.snd = tl1 } = first_byte vals in let { Types.fst = b2; Types.snd = tl2 } = first_byte tl1 in let { Types.fst = b3; Types.snd = tl3 } = first_byte tl2 in let { Types.fst = b4; Types.snd = tl4 } = first_byte tl3 in Types.Some (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (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)))))))))) b4 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (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))))))))) b3 (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)))))))) b2 b1))) | Bool.False -> Types.None (** val oC_as_call_ident : ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status Types.sig0 -> AST.ident **) let oC_as_call_ident prog cm s0 = let pc = (Types.pi1 (Interpret.execute_1' cm (Types.pi1 s0))).Status.program_counter in (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) pc prog.ASM.symboltable with | Types.None -> assert false (* absurd case *) | Types.Some id -> id) (** val oC_abstract_status : ASM.labelled_object_code -> StructuredTraces.abstract_status **) let oC_abstract_status prog = { StructuredTraces.as_pc = AbstractStatus.word_deqset; StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog.ASM.cm)); StructuredTraces.as_classify = (Obj.magic (AbstractStatus.oC_classify prog.ASM.cm)); StructuredTraces.as_label_of_pc = (fun pc -> BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels); StructuredTraces.as_result = (fun st -> as_result_of_finaladdr prog.ASM.cm (Obj.magic st) prog.ASM.final_pc); StructuredTraces.as_call_ident = (Obj.magic (oC_as_call_ident prog prog.ASM.cm)); StructuredTraces.as_tailcall_ident = (fun clearme -> let st = clearme in (match AbstractStatus.current_instruction prog.ASM.cm (Obj.magic st) with | ASM.ACALL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __) | ASM.LCALL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __) | ASM.AJMP x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.LJMP x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.SJMP x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.MOVC (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.RealInstruction clearme0 -> (match clearme0 with | ASM.ADD (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.ADDC (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.SUBB (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.INC x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.DEC x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.MUL (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.DIV (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.DA x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.JC x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.JNC x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.JB (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.JNB (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.JBC (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.JZ x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.JNZ x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.CJNE (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.DJNZ (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __) | ASM.ANL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.ORL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.XRL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.CLR x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.CPL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.RL x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.RLC x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.RR x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.RRC x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.SWAP x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.MOV x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.MOVX x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.SETB x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.PUSH x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.POP x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.XCH (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.XCHD (x, y) -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.RET -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __) | ASM.RETI -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __) | ASM.NOP -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __) | ASM.JMP x -> (fun _ -> Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) } (** val trace_any_label_length : ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret -> Status.status -> Status.status -> StructuredTraces.trace_any_label -> Nat.nat **) let trace_any_label_length prog trace_ends_flag start_status final_status the_trace = StructuredTraces.as_trace_any_label_length' (oC_abstract_status prog) trace_ends_flag (Obj.magic start_status) (Obj.magic final_status) the_trace (** val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list **) let rec all_program_counter_list = function | Nat.O -> List.Nil | Nat.S n' -> List.Cons ((Arithmetic.bitvector_of_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.O)))))))))))))))) n'), (all_program_counter_list n')) (** val compute_paid_trace_any_label : ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret -> Status.status -> Status.status -> StructuredTraces.trace_any_label -> Nat.nat **) let rec compute_paid_trace_any_label prog trace_ends_flag start_status final_status = function | StructuredTraces.Tal_base_not_return (the_status, x) -> Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status) | StructuredTraces.Tal_base_return (the_status, x) -> Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status) | StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) -> Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call) | StructuredTraces.Tal_base_tailcall (pre_fun_call, start_fun_call, final, x1) -> Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call) | StructuredTraces.Tal_step_call (end_flag, pre_fun_call, start_fun_call, after_fun_call, final, call_trace, final_trace) -> let current_instruction_cost = Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call) in let final_trace_cost = compute_paid_trace_any_label prog end_flag (Obj.magic after_fun_call) (Obj.magic final) final_trace in Nat.plus current_instruction_cost final_trace_cost | StructuredTraces.Tal_step_default (end_flag, status_pre, status_init, status_end, tail_trace) -> let current_instruction_cost = Interpret.current_instruction_cost prog.ASM.cm (Obj.magic status_pre) in let tail_trace_cost = compute_paid_trace_any_label prog end_flag (Obj.magic status_init) (Obj.magic status_end) tail_trace in Nat.plus current_instruction_cost tail_trace_cost (** val compute_paid_trace_label_label : ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret -> Status.status -> Status.status -> StructuredTraces.trace_label_label -> Nat.nat **) let compute_paid_trace_label_label prog trace_ends_flag start_status final_status = function | StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) -> compute_paid_trace_any_label prog ends_flag (Obj.magic initial) (Obj.magic final) given_trace (** val block_cost' : ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool -> Nat.nat Types.sig0 **) let rec block_cost' prog program_counter' program_size first_time_around = (match program_size with | Nat.O -> (fun _ -> Nat.O) | Nat.S program_size' -> (fun _ -> (let { Types.fst = eta302; Types.snd = ticks } = Fetch.fetch prog.ASM.cm program_counter' in let { Types.fst = instruction; Types.snd = program_counter'' } = eta302 in (fun _ -> let to_continue = match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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' prog.ASM.costlabels with | Types.None -> Bool.True | Types.Some x -> first_time_around in let x = (match to_continue with | Bool.True -> (fun _ -> Types.pi1 ((match instruction with | ASM.ACALL addr -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.LCALL addr -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.AJMP addr -> (fun _ -> let jump_target = Interpret.compute_target_of_unconditional_jump program_counter'' instruction in Nat.plus ticks (Types.pi1 (block_cost' prog jump_target program_size' Bool.False))) | ASM.LJMP addr -> (fun _ -> let jump_target = Interpret.compute_target_of_unconditional_jump program_counter'' instruction in Nat.plus ticks (Types.pi1 (block_cost' prog jump_target program_size' Bool.False))) | ASM.SJMP addr -> (fun _ -> let jump_target = Interpret.compute_target_of_unconditional_jump program_counter'' instruction in Nat.plus ticks (Types.pi1 (block_cost' prog jump_target program_size' Bool.False))) | ASM.MOVC (src, trgt) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.RealInstruction real_instruction -> (fun _ -> (match real_instruction with | ASM.ADD (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.ADDC (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.SUBB (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.INC x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.DEC x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.MUL (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.DIV (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.DA x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.JC relative -> (fun _ -> ticks) | ASM.JNC relative -> (fun _ -> ticks) | ASM.JB (bit_addr, relative) -> (fun _ -> ticks) | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks) | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks) | ASM.JZ relative -> (fun _ -> ticks) | ASM.JNZ relative -> (fun _ -> ticks) | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks) | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks) | ASM.ANL x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.ORL x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.XRL x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.CLR x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.CPL x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.RL x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.RLC x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.RR x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.RRC x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.SWAP x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.MOV x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.MOVX x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.SETB x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.PUSH x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.POP x -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.XCH (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.XCHD (x, x0) -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.RET -> (fun _ -> ticks) | ASM.RETI -> (fun _ -> ticks) | ASM.NOP -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False))) | ASM.JMP addr -> (fun _ -> Nat.plus ticks (Types.pi1 (block_cost' prog program_counter'' program_size' Bool.False)))) __)) __)) | Bool.False -> (fun _ -> Nat.O)) __ in x)) __)) __ (** val block_cost : ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **) let block_cost prog program_counter = let cost_of_block = block_cost' prog program_counter (Exp.exp (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.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) Bool.True in cost_of_block