open Preamble

open Types

open Hints_declaration

open Core_notation

open Pts

open Logic

open Jmeq

open Russell

open Exp

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open List

open Util

open FoldStuff

open Bool

open Relations

open Nat

open BitVector

open Arithmetic

open BitVectorTrie

open String

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open CostLabel

open ASM

val inefficient_address_of_label :
  ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat

type label_map = Nat.nat Identifiers.identifier_map

val create_label_cost_map0 :
  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
  Types.prod Types.sig0

val create_label_cost_map :
  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
  Types.prod

val address_of_word_labels :
  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word

val prod_inv_rect_Type0 :
  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3

val fetch0 :
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
  BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
  Types.prod

val fetch :
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod