open Preamble

open ExtraMonads

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open ExtraGlobalenvs

open I8051bis

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open BackEndOps

open Joint

open BEMem

open CostLabel

open Events

open IOMonad

open IO

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

open Globalenvs

open Joint_semantics

open SemanticsUtils

open RTL

type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
                stackp : ByteValues.xpointer }

val reg_sp_rect_Type4 :
  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
  -> reg_sp -> 'a1

val reg_sp_rect_Type5 :
  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
  -> reg_sp -> 'a1

val reg_sp_rect_Type3 :
  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
  -> reg_sp -> 'a1

val reg_sp_rect_Type2 :
  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
  -> reg_sp -> 'a1

val reg_sp_rect_Type1 :
  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
  -> reg_sp -> 'a1

val reg_sp_rect_Type0 :
  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
  -> reg_sp -> 'a1

val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map

val stackp : reg_sp -> ByteValues.xpointer

val reg_sp_inv_rect_Type4 :
  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
  ByteValues.xpointer -> __ -> 'a1) -> 'a1

val reg_sp_inv_rect_Type3 :
  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
  ByteValues.xpointer -> __ -> 'a1) -> 'a1

val reg_sp_inv_rect_Type2 :
  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
  ByteValues.xpointer -> __ -> 'a1) -> 'a1

val reg_sp_inv_rect_Type1 :
  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
  ByteValues.xpointer -> __ -> 'a1) -> 'a1

val reg_sp_inv_rect_Type0 :
  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
  ByteValues.xpointer -> __ -> 'a1) -> 'a1

val reg_sp_discr : reg_sp -> reg_sp -> __

val reg_sp_jmdiscr : reg_sp -> reg_sp -> __

val dpi1__o__reg_sp_env__o__inject :
  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
  Types.sig0

val eject__o__reg_sp_env__o__inject :
  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0

val reg_sp_env__o__inject :
  reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0

val dpi1__o__reg_sp_env :
  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map

val eject__o__reg_sp_env :
  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map

val reg_sp_store :
  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp

val reg_sp_retrieve :
  reg_sp -> Registers.register -> ByteValues.beval Errors.res

val reg_sp_empty : ByteValues.xpointer -> reg_sp

type frame = { fr_ret_regs : Registers.register List.list;
               fr_pc : ByteValues.program_counter;
               fr_carry : ByteValues.bebit; fr_regs : reg_sp }

val frame_rect_Type4 :
  (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1

val frame_rect_Type5 :
  (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1

val frame_rect_Type3 :
  (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1

val frame_rect_Type2 :
  (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1

val frame_rect_Type1 :
  (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1

val frame_rect_Type0 :
  (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1

val fr_ret_regs : frame -> Registers.register List.list

val fr_pc : frame -> ByteValues.program_counter

val fr_carry : frame -> ByteValues.bebit

val fr_regs : frame -> reg_sp

val frame_inv_rect_Type4 :
  frame -> (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type3 :
  frame -> (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type2 :
  frame -> (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type1 :
  frame -> (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type0 :
  frame -> (Registers.register List.list -> ByteValues.program_counter ->
  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1

val frame_discr : frame -> frame -> __

val frame_jmdiscr : frame -> frame -> __

val rTL_state_params : Joint_semantics.sem_state_params

type rTL_state = Joint_semantics.state

val rtl_arg_retrieve :
  reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res

val rtl_fetch_ra :
  rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod Errors.res

val rtl_init_local : Registers.register -> reg_sp -> reg_sp

val rtl_setup_call_separate :
  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
  rTL_state -> rTL_state Errors.res

val rtl_setup_call_separate_overflow :
  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
  rTL_state -> rTL_state Errors.res

val rtl_setup_call_unique :
  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
  rTL_state -> rTL_state Errors.res

type rTL_state_pc = Joint_semantics.state_pc

val rtl_save_frame : Registers.register List.list -> rTL_state_pc -> __

val rtl_fetch_external_args :
  AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
  Values.val0 List.list Errors.res

val rtl_set_result :
  Values.val0 List.list -> Registers.register List.list -> rTL_state ->
  rTL_state Errors.res

val rtl_reg_store :
  PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
  Joint_semantics.state

val rtl_reg_retrieve :
  Joint_semantics.state -> Registers.register -> ByteValues.beval Errors.res

val rtl_read_result :
  Registers.register List.list -> rTL_state -> ByteValues.beval List.list
  Errors.res

val rtl_pop_frame_separate :
  Registers.register List.list -> rTL_state -> (rTL_state,
  ByteValues.program_counter) Types.prod Errors.res

val rtl_pop_frame_unique :
  Registers.register List.list -> rTL_state -> (rTL_state,
  ByteValues.program_counter) Types.prod Errors.res

val block_of_register_pair :
  Registers.register -> Registers.register -> rTL_state -> Pointers.block
  Errors.res

val eval_rtl_seq :
  RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res

val reg_res_store :
  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
  Errors.res

val rTL_semantics_separate : SemanticsUtils.sem_graph_params

val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params

val rTL_semantics_unique : SemanticsUtils.sem_graph_params