open Preamble
+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+
open Exp
open Setoids
open Div_and_mod
-open Jmeq
-
-open Russell
-
-open Types
-
open List
open Util
open Bool
-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-
open Relations
open Nat
open ASM
-val inefficient_address_of_word_labels_code_mem :
- ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
+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, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
+ 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, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod
+ 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 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