open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open BitVectorTrie

open String

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Lists

open Positive

open Identifiers

open CostLabel

open ASM

open Exp

open Setoids

open Monad

open Option

open Extranat

open Vector

open FoldStuff

open BitVector

open Arithmetic

open Fetch

open Status

type jump_length =
| Short_jump
| Absolute_jump
| Long_jump

val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1

val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1

val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1

val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1

val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1

val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1

val jump_length_inv_rect_Type4 :
  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val jump_length_inv_rect_Type3 :
  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val jump_length_inv_rect_Type2 :
  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val jump_length_inv_rect_Type1 :
  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val jump_length_inv_rect_Type0 :
  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val jump_length_discr : jump_length -> jump_length -> __

val jump_length_jmdiscr : jump_length -> jump_length -> __

val short_jump_cond :
  BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
  Types.prod

val absolute_jump_cond :
  BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
  Types.prod

val assembly_preinstruction :
  ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
  Vector.vector List.list

val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list

val expand_relative_jump_internal :
  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
  (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
  (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
  ASM.instruction List.list

val expand_relative_jump :
  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
  (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
  ASM.preinstruction -> ASM.instruction List.list

val is_code : AST.region -> Bool.bool

val expand_pseudo_instruction :
  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
  (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
  ASM.instruction List.list

val assembly_1_pseudoinstruction :
  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
  (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
  (Nat.nat, Bool.bool Vector.vector List.list) Types.prod

val instruction_size :
  (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
  BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
  (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
  -> Nat.nat

val assembly :
  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
  (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0

val ticks_of_instruction : ASM.instruction -> Nat.nat

val ticks_of0 :
  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
  BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod

val ticks_of :
  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
  BitVector.word -> (Nat.nat, Nat.nat) Types.prod