open Preamble

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 Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open ExtraMonads

val reg_store :
  PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
  Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map

val reg_retrieve :
  ByteValues.beval Registers.register_env -> Registers.register ->
  ByteValues.beval Errors.res

type hw_register_env = { reg_env : ByteValues.beval
                                   BitVectorTrie.bitVectorTrie;
                         other_bit : ByteValues.bebit }

val hw_register_env_rect_Type4 :
  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
  -> hw_register_env -> 'a1

val hw_register_env_rect_Type5 :
  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
  -> hw_register_env -> 'a1

val hw_register_env_rect_Type3 :
  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
  -> hw_register_env -> 'a1

val hw_register_env_rect_Type2 :
  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
  -> hw_register_env -> 'a1

val hw_register_env_rect_Type1 :
  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
  -> hw_register_env -> 'a1

val hw_register_env_rect_Type0 :
  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
  -> hw_register_env -> 'a1

val reg_env : hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie

val other_bit : hw_register_env -> ByteValues.bebit

val hw_register_env_inv_rect_Type4 :
  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
  ByteValues.bebit -> __ -> 'a1) -> 'a1

val hw_register_env_inv_rect_Type3 :
  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
  ByteValues.bebit -> __ -> 'a1) -> 'a1

val hw_register_env_inv_rect_Type2 :
  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
  ByteValues.bebit -> __ -> 'a1) -> 'a1

val hw_register_env_inv_rect_Type1 :
  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
  ByteValues.bebit -> __ -> 'a1) -> 'a1

val hw_register_env_inv_rect_Type0 :
  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
  ByteValues.bebit -> __ -> 'a1) -> 'a1

val hw_register_env_discr : hw_register_env -> hw_register_env -> __

val hw_register_env_jmdiscr : hw_register_env -> hw_register_env -> __

val hwreg_retrieve : hw_register_env -> I8051.register -> ByteValues.beval

val hwreg_store :
  I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env

val hwreg_set_other : ByteValues.bebit -> hw_register_env -> hw_register_env

val hwreg_retrieve_sp : hw_register_env -> ByteValues.xpointer Errors.res

val hwreg_store_sp :
  hw_register_env -> ByteValues.xpointer -> hw_register_env

val init_hw_register_env : ByteValues.xpointer -> hw_register_env

type sem_graph_params = { sgp_pars : Joint.uns_params;
                          sgp_sup : (__ -> __
                                    Joint_semantics.sem_unserialized_params);
                          graph_pre_main_generator : (Joint.joint_program ->
                                                     Joint.joint_closed_internal_function) }

val sem_graph_params_rect_Type4 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_graph_params -> 'a1

val sem_graph_params_rect_Type5 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_graph_params -> 'a1

val sem_graph_params_rect_Type3 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_graph_params -> 'a1

val sem_graph_params_rect_Type2 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_graph_params -> 'a1

val sem_graph_params_rect_Type1 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_graph_params -> 'a1

val sem_graph_params_rect_Type0 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_graph_params -> 'a1

val sgp_pars : sem_graph_params -> Joint.uns_params

val sgp_sup0 :
  sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params

val graph_pre_main_generator :
  sem_graph_params -> Joint.joint_program ->
  Joint.joint_closed_internal_function

val sem_graph_params_inv_rect_Type4 :
  sem_graph_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_graph_params_inv_rect_Type3 :
  sem_graph_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_graph_params_inv_rect_Type2 :
  sem_graph_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_graph_params_inv_rect_Type1 :
  sem_graph_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_graph_params_inv_rect_Type0 :
  sem_graph_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_graph_params_jmdiscr : sem_graph_params -> sem_graph_params -> __

val sem_graph_params_to_graph_params : sem_graph_params -> Joint.graph_params

val sem_graph_params_to_sem_params :
  sem_graph_params -> Joint_semantics.sem_params

val sem_params_from_sem_graph_params__o__spp' :
  sem_graph_params -> Joint_semantics.serialized_params

val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
  sem_graph_params -> Joint.joint_closed_internal_function
  Joint_semantics.sem_unserialized_params

val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
  sem_graph_params -> Joint_semantics.sem_state_params

val sem_params_from_sem_graph_params__o__spp'__o__spp :
  sem_graph_params -> Joint.params

val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
  sem_graph_params -> Joint.stmt_params

val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
  sem_graph_params -> Joint.uns_params

val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
  sem_graph_params -> Joint.unserialized_params

type sem_lin_params = { slp_pars : Joint.uns_params;
                        slp_sup : (__ -> __
                                  Joint_semantics.sem_unserialized_params);
                        lin_pre_main_generator : (Joint.joint_program ->
                                                 Joint.joint_closed_internal_function) }

val sem_lin_params_rect_Type4 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_lin_params -> 'a1

val sem_lin_params_rect_Type5 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_lin_params -> 'a1

val sem_lin_params_rect_Type3 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_lin_params -> 'a1

val sem_lin_params_rect_Type2 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_lin_params -> 'a1

val sem_lin_params_rect_Type1 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_lin_params -> 'a1

val sem_lin_params_rect_Type0 :
  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
  sem_lin_params -> 'a1

val slp_pars : sem_lin_params -> Joint.uns_params

val slp_sup0 : sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params

val lin_pre_main_generator :
  sem_lin_params -> Joint.joint_program ->
  Joint.joint_closed_internal_function

val sem_lin_params_inv_rect_Type4 :
  sem_lin_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_lin_params_inv_rect_Type3 :
  sem_lin_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_lin_params_inv_rect_Type2 :
  sem_lin_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_lin_params_inv_rect_Type1 :
  sem_lin_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_lin_params_inv_rect_Type0 :
  sem_lin_params -> (Joint.uns_params -> (__ -> __
  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __

val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params

val sem_lin_params_to_sem_params :
  sem_lin_params -> Joint_semantics.sem_params

val sem_params_from_sem_lin_params__o__spp' :
  sem_lin_params -> Joint_semantics.serialized_params

val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
  sem_lin_params -> Joint.joint_closed_internal_function
  Joint_semantics.sem_unserialized_params

val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
  sem_lin_params -> Joint_semantics.sem_state_params

val sem_params_from_sem_lin_params__o__spp'__o__spp :
  sem_lin_params -> Joint.params

val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
  sem_lin_params -> Joint.stmt_params

val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
  sem_lin_params -> Joint.uns_params

val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
  sem_lin_params -> Joint.unserialized_params

val match_genv_t_rect_Type4 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_rect_Type5 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_rect_Type3 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_rect_Type2 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_rect_Type1 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_rect_Type0 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_inv_rect_Type4 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_inv_rect_Type3 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_inv_rect_Type2 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_inv_rect_Type1 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_inv_rect_Type0 :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val match_genv_t_discr :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> __

val match_genv_t_jmdiscr :
  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
  Globalenvs.genv_t -> __

val joint_globalenv :
  Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> Joint_semantics.genv