open Preamble

open Exp

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open Types

open List

open Util

open FoldStuff

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

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_word_labels_code_mem :
  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector

type label_map = Nat.nat Identifiers.identifier_map

val create_label_cost_map0 :
  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
  BitVectorTrie.bitVectorTrie) Types.prod Types.sig0

val create_label_cost_map :
  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
  BitVectorTrie.bitVectorTrie) Types.prod

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

val bitvector_max_nat : Nat.nat -> Nat.nat

val code_memory_size : Nat.nat

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