open Preamble

open BitVectorTrie

open String

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Identifiers

open CostLabel

open ASM

open Types

open Hints_declaration

open Core_notation

open Pts

open Logic

open Jmeq

open Russell

open Status

open StatusProofs

open Fetch

open Hide

open Division

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open IOMonad

open IO

open Sets

open Listb

open StructuredTraces

open AbstractStatus

val execute_1_preinstruction :
  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
  Status.preStatus

val execute_1_preinstruction_ok' :
  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
  Status.preStatus Types.sig0

val compute_target_of_unconditional_jump :
  BitVector.word -> ASM.instruction -> BitVector.word

val is_unconditional_jump : ASM.instruction -> Bool.bool

val program_counter_after_other :
  BitVector.word -> ASM.instruction -> BitVector.word

val addr_of_relative :
  'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word

val execute_1_0 :
  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
  Status.status Types.sig0

val current_instruction_cost :
  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat

val execute_1' :
  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
  Status.status Types.sig0

val execute_1 :
  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
  Status.status

val execute_1_pseudo_instruction0 :
  (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
  (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) ->
  Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
  Status.pseudoStatus

val execute_1_pseudo_instruction :
  ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat)
  Types.prod) -> (ASM.identifier -> BitVector.word) -> (ASM.identifier ->
  BitVector.word) -> Status.pseudoStatus -> Status.pseudoStatus

val execute :
  Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
  Status.status