extracted/aSMCosts.ml

   1 open Preamble
   2
   3 open Fetch
   4
   5 open Hide
   6
   7 open Division
   8
   9 open Z
  10
  11 open BitVectorZ
  12
  13 open Pointers
  14
  15 open Coqlib
  16
  17 open Values
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Sets
  26
  27 open Listb
  28
  29 open StructuredTraces
  30
  31 open AbstractStatus
  32
  33 open BitVectorTrie
  34
  35 open String
  36
  37 open Exp
  38
  39 open Arithmetic
  40
  41 open Vector
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Extranat
  48
  49 open Integers
  50
  51 open AST
  52
  53 open LabelledObjects
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Option
  74
  75 open Div_and_mod
  76
  77 open Util
  78
  79 open List
  80
  81 open Lists
  82
  83 open Bool
  84
  85 open Relations
  86
  87 open Nat
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open ASM
  96
  97 open Types
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Jmeq
 108
 109 open Russell
 110
 111 open Status
 112
 113 open StatusProofs
 114
 115 open Interpret
 116
 117 (** val aSMRegisterRets : ASM.subaddressing_mode List.list **)
 118 let aSMRegisterRets =
 119   List.Cons ((ASM.DIRECT
 120     (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 121       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 122       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 123       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 124       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 125       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 126       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 127       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 128       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 129       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 130       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 131       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 132       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 133       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 134       (Nat.S (Nat.S (Nat.S (Nat.S
 135       Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
 136     (List.Cons ((ASM.DIRECT
 137     (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 138       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 139       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 140       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 141       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 142       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 143       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 144       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 145       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 146       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 147       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 148       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 149       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 150       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 151       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 152       Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
 153     (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 154     Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
 155     (Nat.O, Bool.False, Vector.VEmpty))))))), (List.Cons ((ASM.REGISTER
 156     (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
 157     Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 158     Vector.VEmpty))))))), List.Nil)))))))
 159
 160 (** val as_result_of_finaladdr :
 161     'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int
 162     Types.option **)
 163 let as_result_of_finaladdr cm st finaladdr =
 164   match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 165           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 166           Nat.O)))))))))))))))) st.Status.program_counter finaladdr with
 167   | Bool.True ->
 168     let vals =
 169       List.map (fun h ->
 170         Status.get_arg_8 cm st Bool.False
 171           (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
 172             Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 173             (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 174             ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct,
 175             (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty))))))
 176             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 177             (Nat.S (Nat.S Nat.O))))))))), ASM.Direct, (Vector.VCons ((Nat.S
 178             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))),
 179             ASM.Indirect, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 180             (Nat.S (Nat.S Nat.O))))))), ASM.Registr, (Vector.VCons ((Nat.S
 181             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), ASM.Acc_a,
 182             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
 183             ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
 184             ASM.Data, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 185             ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_pc,
 186             (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
 187             (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))))))))
 188             h)) aSMRegisterRets
 189     in
 190     let dummy =
 191       BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 192         Nat.O))))))))
 193     in
 194     let first_byte = fun l ->
 195       match l with
 196       | List.Nil -> { Types.fst = dummy; Types.snd = List.Nil }
 197       | List.Cons (hd, tl) -> { Types.fst = hd; Types.snd = tl }
 198     in
 199     let { Types.fst = b1; Types.snd = tl1 } = first_byte vals in
 200     let { Types.fst = b2; Types.snd = tl2 } = first_byte tl1 in
 201     let { Types.fst = b3; Types.snd = tl3 } = first_byte tl2 in
 202     let { Types.fst = b4; Types.snd = tl4 } = first_byte tl3 in
 203     Types.Some
 204     (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 205       Nat.O))))))))
 206       (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 207         Nat.O))))))))
 208         (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 209           Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 210           (Nat.S Nat.O)))))))))) b4
 211       (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 212         Nat.O))))))))
 213         (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 214           Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 215           (Nat.S Nat.O))))))))) b3
 216         (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 217           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 218           (Nat.S (Nat.S Nat.O)))))))) b2 b1)))
 219   | Bool.False -> Types.None
 220
 221 (** val oC_as_call_ident :
 222     ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
 223     Status.status Types.sig0 -> AST.ident **)
 224 let oC_as_call_ident prog cm s0 =
 225   let pc =
 226     (Types.pi1 (Interpret.execute_1' cm (Types.pi1 s0))).Status.program_counter
 227   in
 228   (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 229            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 230            (Nat.S Nat.O)))))))))))))))) pc prog.ASM.symboltable with
 231    | Types.None -> assert false (* absurd case *)
 232    | Types.Some id -> id)
 233
 234 (** val oC_abstract_status :
 235     ASM.labelled_object_code -> StructuredTraces.abstract_status **)
 236 let oC_abstract_status prog =
 237   { StructuredTraces.as_pc = AbstractStatus.word_deqset;
 238     StructuredTraces.as_pc_of =
 239     (Obj.magic (Status.program_counter prog.ASM.cm));
 240     StructuredTraces.as_classify =
 241     (Obj.magic (AbstractStatus.oC_classify prog.ASM.cm));
 242     StructuredTraces.as_label_of_pc = (fun pc ->
 243     BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 244       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 245       Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
 246     StructuredTraces.as_result = (fun st ->
 247     as_result_of_finaladdr prog.ASM.cm (Obj.magic st) prog.ASM.final_pc);
 248     StructuredTraces.as_call_ident =
 249     (Obj.magic (oC_as_call_ident prog prog.ASM.cm));
 250     StructuredTraces.as_tailcall_ident = (fun clearme ->
 251     let st = clearme in
 252     (match AbstractStatus.current_instruction prog.ASM.cm (Obj.magic st) with
 253      | ASM.ACALL x ->
 254        (fun _ ->
 255          Obj.magic StructuredTraces.status_class_discr
 256            StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
 257      | ASM.LCALL x ->
 258        (fun _ ->
 259          Obj.magic StructuredTraces.status_class_discr
 260            StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
 261      | ASM.AJMP x ->
 262        (fun _ ->
 263          Obj.magic StructuredTraces.status_class_discr
 264            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 265      | ASM.LJMP x ->
 266        (fun _ ->
 267          Obj.magic StructuredTraces.status_class_discr
 268            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 269      | ASM.SJMP x ->
 270        (fun _ ->
 271          Obj.magic StructuredTraces.status_class_discr
 272            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 273      | ASM.MOVC (x, y) ->
 274        (fun _ ->
 275          Obj.magic StructuredTraces.status_class_discr
 276            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 277      | ASM.RealInstruction clearme0 ->
 278        (match clearme0 with
 279         | ASM.ADD (x, y) ->
 280           (fun _ ->
 281             Obj.magic StructuredTraces.status_class_discr
 282               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 283         | ASM.ADDC (x, y) ->
 284           (fun _ ->
 285             Obj.magic StructuredTraces.status_class_discr
 286               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 287         | ASM.SUBB (x, y) ->
 288           (fun _ ->
 289             Obj.magic StructuredTraces.status_class_discr
 290               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 291         | ASM.INC x ->
 292           (fun _ ->
 293             Obj.magic StructuredTraces.status_class_discr
 294               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 295         | ASM.DEC x ->
 296           (fun _ ->
 297             Obj.magic StructuredTraces.status_class_discr
 298               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 299         | ASM.MUL (x, y) ->
 300           (fun _ ->
 301             Obj.magic StructuredTraces.status_class_discr
 302               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 303         | ASM.DIV (x, y) ->
 304           (fun _ ->
 305             Obj.magic StructuredTraces.status_class_discr
 306               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 307         | ASM.DA x ->
 308           (fun _ ->
 309             Obj.magic StructuredTraces.status_class_discr
 310               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 311         | ASM.JC x ->
 312           (fun _ ->
 313             Obj.magic StructuredTraces.status_class_discr
 314               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 315         | ASM.JNC x ->
 316           (fun _ ->
 317             Obj.magic StructuredTraces.status_class_discr
 318               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 319         | ASM.JB (x, y) ->
 320           (fun _ ->
 321             Obj.magic StructuredTraces.status_class_discr
 322               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 323         | ASM.JNB (x, y) ->
 324           (fun _ ->
 325             Obj.magic StructuredTraces.status_class_discr
 326               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 327         | ASM.JBC (x, y) ->
 328           (fun _ ->
 329             Obj.magic StructuredTraces.status_class_discr
 330               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 331         | ASM.JZ x ->
 332           (fun _ ->
 333             Obj.magic StructuredTraces.status_class_discr
 334               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 335         | ASM.JNZ x ->
 336           (fun _ ->
 337             Obj.magic StructuredTraces.status_class_discr
 338               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 339         | ASM.CJNE (x, y) ->
 340           (fun _ ->
 341             Obj.magic StructuredTraces.status_class_discr
 342               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 343         | ASM.DJNZ (x, y) ->
 344           (fun _ ->
 345             Obj.magic StructuredTraces.status_class_discr
 346               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 347         | ASM.ANL x ->
 348           (fun _ ->
 349             Obj.magic StructuredTraces.status_class_discr
 350               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 351         | ASM.ORL x ->
 352           (fun _ ->
 353             Obj.magic StructuredTraces.status_class_discr
 354               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 355         | ASM.XRL x ->
 356           (fun _ ->
 357             Obj.magic StructuredTraces.status_class_discr
 358               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 359         | ASM.CLR x ->
 360           (fun _ ->
 361             Obj.magic StructuredTraces.status_class_discr
 362               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 363         | ASM.CPL x ->
 364           (fun _ ->
 365             Obj.magic StructuredTraces.status_class_discr
 366               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 367         | ASM.RL x ->
 368           (fun _ ->
 369             Obj.magic StructuredTraces.status_class_discr
 370               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 371         | ASM.RLC x ->
 372           (fun _ ->
 373             Obj.magic StructuredTraces.status_class_discr
 374               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 375         | ASM.RR x ->
 376           (fun _ ->
 377             Obj.magic StructuredTraces.status_class_discr
 378               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 379         | ASM.RRC x ->
 380           (fun _ ->
 381             Obj.magic StructuredTraces.status_class_discr
 382               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 383         | ASM.SWAP x ->
 384           (fun _ ->
 385             Obj.magic StructuredTraces.status_class_discr
 386               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 387         | ASM.MOV x ->
 388           (fun _ ->
 389             Obj.magic StructuredTraces.status_class_discr
 390               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 391         | ASM.MOVX x ->
 392           (fun _ ->
 393             Obj.magic StructuredTraces.status_class_discr
 394               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 395         | ASM.SETB x ->
 396           (fun _ ->
 397             Obj.magic StructuredTraces.status_class_discr
 398               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 399         | ASM.PUSH x ->
 400           (fun _ ->
 401             Obj.magic StructuredTraces.status_class_discr
 402               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 403         | ASM.POP x ->
 404           (fun _ ->
 405             Obj.magic StructuredTraces.status_class_discr
 406               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 407         | ASM.XCH (x, y) ->
 408           (fun _ ->
 409             Obj.magic StructuredTraces.status_class_discr
 410               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 411         | ASM.XCHD (x, y) ->
 412           (fun _ ->
 413             Obj.magic StructuredTraces.status_class_discr
 414               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 415         | ASM.RET ->
 416           (fun _ ->
 417             Obj.magic StructuredTraces.status_class_discr
 418               StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
 419         | ASM.RETI ->
 420           (fun _ ->
 421             Obj.magic StructuredTraces.status_class_discr
 422               StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
 423         | ASM.NOP ->
 424           (fun _ ->
 425             Obj.magic StructuredTraces.status_class_discr
 426               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 427         | ASM.JMP x ->
 428           (fun _ ->
 429             Obj.magic StructuredTraces.status_class_discr
 430               StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
 431
 432 (** val trace_any_label_length :
 433     ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
 434     Status.status -> Status.status -> StructuredTraces.trace_any_label ->
 435     Nat.nat **)
 436 let trace_any_label_length prog trace_ends_flag start_status final_status the_trace =
 437   StructuredTraces.as_trace_any_label_length' (oC_abstract_status prog)
 438     trace_ends_flag (Obj.magic start_status) (Obj.magic final_status)
 439     the_trace
 440
 441 (** val all_program_counter_list :
 442     Nat.nat -> BitVector.bitVector List.list **)
 443 let rec all_program_counter_list = function
 444 | Nat.O -> List.Nil
 445 | Nat.S n' ->
 446   List.Cons
 447     ((Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 448        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 449        Nat.O)))))))))))))))) n'), (all_program_counter_list n'))
 450
 451 (** val compute_paid_trace_any_label :
 452     ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
 453     Status.status -> Status.status -> StructuredTraces.trace_any_label ->
 454     Nat.nat **)
 455 let rec compute_paid_trace_any_label prog trace_ends_flag start_status final_status = function
 456 | StructuredTraces.Tal_base_not_return (the_status, x) ->
 457   Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status)
 458 | StructuredTraces.Tal_base_return (the_status, x) ->
 459   Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status)
 460 | StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
 461   Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
 462 | StructuredTraces.Tal_base_tailcall
 463     (pre_fun_call, start_fun_call, final, x1) ->
 464   Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
 465 | StructuredTraces.Tal_step_call
 466     (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
 467      call_trace, final_trace) ->
 468   let current_instruction_cost =
 469     Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
 470   in
 471   let final_trace_cost =
 472     compute_paid_trace_any_label prog end_flag (Obj.magic after_fun_call)
 473       (Obj.magic final) final_trace
 474   in
 475   Nat.plus current_instruction_cost final_trace_cost
 476 | StructuredTraces.Tal_step_default
 477     (end_flag, status_pre, status_init, status_end, tail_trace) ->
 478   let current_instruction_cost =
 479     Interpret.current_instruction_cost prog.ASM.cm (Obj.magic status_pre)
 480   in
 481   let tail_trace_cost =
 482     compute_paid_trace_any_label prog end_flag (Obj.magic status_init)
 483       (Obj.magic status_end) tail_trace
 484   in
 485   Nat.plus current_instruction_cost tail_trace_cost
 486
 487 (** val compute_paid_trace_label_label :
 488     ASM.labelled_object_code -> StructuredTraces.trace_ends_with_ret ->
 489     Status.status -> Status.status -> StructuredTraces.trace_label_label ->
 490     Nat.nat **)
 491 let compute_paid_trace_label_label prog trace_ends_flag start_status final_status = function
 492 | StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
 493   compute_paid_trace_any_label prog ends_flag (Obj.magic initial)
 494     (Obj.magic final) given_trace
 495
 496 (** val block_cost' :
 497     ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Bool.bool ->
 498     Nat.nat Types.sig0 **)
 499 let rec block_cost' prog program_counter' program_size first_time_around =
 500   (match program_size with
 501    | Nat.O -> (fun _ -> Nat.O)
 502    | Nat.S program_size' ->
 503      (fun _ ->
 504        (let { Types.fst = eta302; Types.snd = ticks } =
 505           Fetch.fetch prog.ASM.cm program_counter'
 506         in
 507        let { Types.fst = instruction; Types.snd = program_counter'' } =
 508          eta302
 509        in
 510        (fun _ ->
 511        let to_continue =
 512          match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 513                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 514                  (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter'
 515                  prog.ASM.costlabels with
 516          | Types.None -> Bool.True
 517          | Types.Some x -> first_time_around
 518        in
 519        let x =
 520          (match to_continue with
 521           | Bool.True ->
 522             (fun _ ->
 523               Types.pi1
 524                 ((match instruction with
 525                   | ASM.ACALL addr ->
 526                     (fun _ ->
 527                       Nat.plus ticks
 528                         (Types.pi1
 529                           (block_cost' prog program_counter'' program_size'
 530                             Bool.False)))
 531                   | ASM.LCALL addr ->
 532                     (fun _ ->
 533                       Nat.plus ticks
 534                         (Types.pi1
 535                           (block_cost' prog program_counter'' program_size'
 536                             Bool.False)))
 537                   | ASM.AJMP addr ->
 538                     (fun _ ->
 539                       let jump_target =
 540                         Interpret.compute_target_of_unconditional_jump
 541                           program_counter'' instruction
 542                       in
 543                       Nat.plus ticks
 544                         (Types.pi1
 545                           (block_cost' prog jump_target program_size'
 546                             Bool.False)))
 547                   | ASM.LJMP addr ->
 548                     (fun _ ->
 549                       let jump_target =
 550                         Interpret.compute_target_of_unconditional_jump
 551                           program_counter'' instruction
 552                       in
 553                       Nat.plus ticks
 554                         (Types.pi1
 555                           (block_cost' prog jump_target program_size'
 556                             Bool.False)))
 557                   | ASM.SJMP addr ->
 558                     (fun _ ->
 559                       let jump_target =
 560                         Interpret.compute_target_of_unconditional_jump
 561                           program_counter'' instruction
 562                       in
 563                       Nat.plus ticks
 564                         (Types.pi1
 565                           (block_cost' prog jump_target program_size'
 566                             Bool.False)))
 567                   | ASM.MOVC (src, trgt) ->
 568                     (fun _ ->
 569                       Nat.plus ticks
 570                         (Types.pi1
 571                           (block_cost' prog program_counter'' program_size'
 572                             Bool.False)))
 573                   | ASM.RealInstruction real_instruction ->
 574                     (fun _ ->
 575                       (match real_instruction with
 576                        | ASM.ADD (x, x0) ->
 577                          (fun _ ->
 578                            Nat.plus ticks
 579                              (Types.pi1
 580                                (block_cost' prog program_counter''
 581                                  program_size' Bool.False)))
 582                        | ASM.ADDC (x, x0) ->
 583                          (fun _ ->
 584                            Nat.plus ticks
 585                              (Types.pi1
 586                                (block_cost' prog program_counter''
 587                                  program_size' Bool.False)))
 588                        | ASM.SUBB (x, x0) ->
 589                          (fun _ ->
 590                            Nat.plus ticks
 591                              (Types.pi1
 592                                (block_cost' prog program_counter''
 593                                  program_size' Bool.False)))
 594                        | ASM.INC x ->
 595                          (fun _ ->
 596                            Nat.plus ticks
 597                              (Types.pi1
 598                                (block_cost' prog program_counter''
 599                                  program_size' Bool.False)))
 600                        | ASM.DEC x ->
 601                          (fun _ ->
 602                            Nat.plus ticks
 603                              (Types.pi1
 604                                (block_cost' prog program_counter''
 605                                  program_size' Bool.False)))
 606                        | ASM.MUL (x, x0) ->
 607                          (fun _ ->
 608                            Nat.plus ticks
 609                              (Types.pi1
 610                                (block_cost' prog program_counter''
 611                                  program_size' Bool.False)))
 612                        | ASM.DIV (x, x0) ->
 613                          (fun _ ->
 614                            Nat.plus ticks
 615                              (Types.pi1
 616                                (block_cost' prog program_counter''
 617                                  program_size' Bool.False)))
 618                        | ASM.DA x ->
 619                          (fun _ ->
 620                            Nat.plus ticks
 621                              (Types.pi1
 622                                (block_cost' prog program_counter''
 623                                  program_size' Bool.False)))
 624                        | ASM.JC relative -> (fun _ -> ticks)
 625                        | ASM.JNC relative -> (fun _ -> ticks)
 626                        | ASM.JB (bit_addr, relative) -> (fun _ -> ticks)
 627                        | ASM.JNB (bit_addr, relative) -> (fun _ -> ticks)
 628                        | ASM.JBC (bit_addr, relative) -> (fun _ -> ticks)
 629                        | ASM.JZ relative -> (fun _ -> ticks)
 630                        | ASM.JNZ relative -> (fun _ -> ticks)
 631                        | ASM.CJNE (src_trgt, relative) -> (fun _ -> ticks)
 632                        | ASM.DJNZ (src_trgt, relative) -> (fun _ -> ticks)
 633                        | ASM.ANL x ->
 634                          (fun _ ->
 635                            Nat.plus ticks
 636                              (Types.pi1
 637                                (block_cost' prog program_counter''
 638                                  program_size' Bool.False)))
 639                        | ASM.ORL x ->
 640                          (fun _ ->
 641                            Nat.plus ticks
 642                              (Types.pi1
 643                                (block_cost' prog program_counter''
 644                                  program_size' Bool.False)))
 645                        | ASM.XRL x ->
 646                          (fun _ ->
 647                            Nat.plus ticks
 648                              (Types.pi1
 649                                (block_cost' prog program_counter''
 650                                  program_size' Bool.False)))
 651                        | ASM.CLR x ->
 652                          (fun _ ->
 653                            Nat.plus ticks
 654                              (Types.pi1
 655                                (block_cost' prog program_counter''
 656                                  program_size' Bool.False)))
 657                        | ASM.CPL x ->
 658                          (fun _ ->
 659                            Nat.plus ticks
 660                              (Types.pi1
 661                                (block_cost' prog program_counter''
 662                                  program_size' Bool.False)))
 663                        | ASM.RL x ->
 664                          (fun _ ->
 665                            Nat.plus ticks
 666                              (Types.pi1
 667                                (block_cost' prog program_counter''
 668                                  program_size' Bool.False)))
 669                        | ASM.RLC x ->
 670                          (fun _ ->
 671                            Nat.plus ticks
 672                              (Types.pi1
 673                                (block_cost' prog program_counter''
 674                                  program_size' Bool.False)))
 675                        | ASM.RR x ->
 676                          (fun _ ->
 677                            Nat.plus ticks
 678                              (Types.pi1
 679                                (block_cost' prog program_counter''
 680                                  program_size' Bool.False)))
 681                        | ASM.RRC x ->
 682                          (fun _ ->
 683                            Nat.plus ticks
 684                              (Types.pi1
 685                                (block_cost' prog program_counter''
 686                                  program_size' Bool.False)))
 687                        | ASM.SWAP x ->
 688                          (fun _ ->
 689                            Nat.plus ticks
 690                              (Types.pi1
 691                                (block_cost' prog program_counter''
 692                                  program_size' Bool.False)))
 693                        | ASM.MOV x ->
 694                          (fun _ ->
 695                            Nat.plus ticks
 696                              (Types.pi1
 697                                (block_cost' prog program_counter''
 698                                  program_size' Bool.False)))
 699                        | ASM.MOVX x ->
 700                          (fun _ ->
 701                            Nat.plus ticks
 702                              (Types.pi1
 703                                (block_cost' prog program_counter''
 704                                  program_size' Bool.False)))
 705                        | ASM.SETB x ->
 706                          (fun _ ->
 707                            Nat.plus ticks
 708                              (Types.pi1
 709                                (block_cost' prog program_counter''
 710                                  program_size' Bool.False)))
 711                        | ASM.PUSH x ->
 712                          (fun _ ->
 713                            Nat.plus ticks
 714                              (Types.pi1
 715                                (block_cost' prog program_counter''
 716                                  program_size' Bool.False)))
 717                        | ASM.POP x ->
 718                          (fun _ ->
 719                            Nat.plus ticks
 720                              (Types.pi1
 721                                (block_cost' prog program_counter''
 722                                  program_size' Bool.False)))
 723                        | ASM.XCH (x, x0) ->
 724                          (fun _ ->
 725                            Nat.plus ticks
 726                              (Types.pi1
 727                                (block_cost' prog program_counter''
 728                                  program_size' Bool.False)))
 729                        | ASM.XCHD (x, x0) ->
 730                          (fun _ ->
 731                            Nat.plus ticks
 732                              (Types.pi1
 733                                (block_cost' prog program_counter''
 734                                  program_size' Bool.False)))
 735                        | ASM.RET -> (fun _ -> ticks)
 736                        | ASM.RETI -> (fun _ -> ticks)
 737                        | ASM.NOP ->
 738                          (fun _ ->
 739                            Nat.plus ticks
 740                              (Types.pi1
 741                                (block_cost' prog program_counter''
 742                                  program_size' Bool.False)))
 743                        | ASM.JMP addr ->
 744                          (fun _ ->
 745                            Nat.plus ticks
 746                              (Types.pi1
 747                                (block_cost' prog program_counter''
 748                                  program_size' Bool.False)))) __)) __))
 749           | Bool.False -> (fun _ -> Nat.O)) __
 750        in
 751        x)) __)) __
 752
 753 (** val block_cost :
 754     ASM.labelled_object_code -> BitVector.word -> Nat.nat Types.sig0 **)
 755 let block_cost prog program_counter =
 756   let cost_of_block =
 757     block_cost' prog program_counter
 758       (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 759         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 760         (Nat.S Nat.O))))))))))))))))) Bool.True
 761   in
 762   cost_of_block
 763