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 StructuredTraces

type evaluation_params = { globals : AST.ident List.list;
                           ev_genv : Joint_semantics.genv }

val evaluation_params_rect_Type4 :
  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
  -> 'a1) -> evaluation_params -> 'a1

val evaluation_params_rect_Type5 :
  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
  -> 'a1) -> evaluation_params -> 'a1

val evaluation_params_rect_Type3 :
  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
  -> 'a1) -> evaluation_params -> 'a1

val evaluation_params_rect_Type2 :
  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
  -> 'a1) -> evaluation_params -> 'a1

val evaluation_params_rect_Type1 :
  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
  -> 'a1) -> evaluation_params -> 'a1

val evaluation_params_rect_Type0 :
  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
  -> 'a1) -> evaluation_params -> 'a1

val globals :
  Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list

val ev_genv :
  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv

val evaluation_params_inv_rect_Type4 :
  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
  Joint_semantics.genv -> __ -> 'a1) -> 'a1

val evaluation_params_inv_rect_Type3 :
  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
  Joint_semantics.genv -> __ -> 'a1) -> 'a1

val evaluation_params_inv_rect_Type2 :
  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
  Joint_semantics.genv -> __ -> 'a1) -> 'a1

val evaluation_params_inv_rect_Type1 :
  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
  Joint_semantics.genv -> __ -> 'a1) -> 'a1

val evaluation_params_inv_rect_Type0 :
  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
  Joint_semantics.genv -> __ -> 'a1) -> 'a1

val evaluation_params_discr :
  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __

val evaluation_params_jmdiscr :
  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __

val dpi1__o__ev_genv__o__inject :
  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
  Joint_semantics.genv Types.sig0

val dpi1__o__ev_genv__o__ge__o__inject :
  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
  Types.sig0

val dpi1__o__ev_genv__o__ge :
  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t

val eject__o__ev_genv__o__inject :
  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
  Joint_semantics.genv Types.sig0

val eject__o__ev_genv__o__ge__o__inject :
  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
  Types.sig0

val eject__o__ev_genv__o__ge :
  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t

val ev_genv__o__ge :
  Joint_semantics.sem_params -> evaluation_params ->
  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t

val ev_genv__o__ge__o__inject :
  Joint_semantics.sem_params -> evaluation_params ->
  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
  Types.sig0

val ev_genv__o__inject :
  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
  Types.sig0

val dpi1__o__ev_genv :
  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
  Joint_semantics.genv

val eject__o__ev_genv :
  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
  Joint_semantics.genv

type prog_params = { prog_spars : Joint_semantics.sem_params;
                     prog : Joint.joint_program;
                     stack_sizes : (AST.ident -> Nat.nat Types.option) }

val prog_params_rect_Type4 :
  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> 'a1) -> prog_params -> 'a1

val prog_params_rect_Type5 :
  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> 'a1) -> prog_params -> 'a1

val prog_params_rect_Type3 :
  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> 'a1) -> prog_params -> 'a1

val prog_params_rect_Type2 :
  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> 'a1) -> prog_params -> 'a1

val prog_params_rect_Type1 :
  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> 'a1) -> prog_params -> 'a1

val prog_params_rect_Type0 :
  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> 'a1) -> prog_params -> 'a1

val prog_spars : prog_params -> Joint_semantics.sem_params

val prog : prog_params -> Joint.joint_program

val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option

val prog_params_inv_rect_Type4 :
  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1

val prog_params_inv_rect_Type3 :
  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1

val prog_params_inv_rect_Type2 :
  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1

val prog_params_inv_rect_Type1 :
  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1

val prog_params_inv_rect_Type0 :
  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1

val prog_params_jmdiscr : prog_params -> prog_params -> __

val prog_spars__o__spp' : prog_params -> Joint_semantics.serialized_params

val prog_spars__o__spp'__o__msu_pars :
  prog_params -> Joint.joint_closed_internal_function
  Joint_semantics.sem_unserialized_params

val prog_spars__o__spp'__o__msu_pars__o__st_pars :
  prog_params -> Joint_semantics.sem_state_params

val prog_spars__o__spp'__o__spp : prog_params -> Joint.params

val prog_spars__o__spp'__o__spp__o__stmt_pars :
  prog_params -> Joint.stmt_params

val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
  prog_params -> Joint.uns_params

val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
  prog_params -> Joint.unserialized_params

val joint_make_global : prog_params -> evaluation_params

val joint_make_global__o__ev_genv : prog_params -> Joint_semantics.genv

val joint_make_global__o__ev_genv__o__ge :
  prog_params -> Joint.joint_closed_internal_function AST.fundef
  Globalenvs.genv_t

val joint_make_global__o__ev_genv__o__ge__o__inject :
  prog_params -> Joint.joint_closed_internal_function AST.fundef
  Globalenvs.genv_t Types.sig0

val joint_make_global__o__ev_genv__o__inject :
  prog_params -> Joint_semantics.genv Types.sig0

val joint_make_global__o__inject :
  prog_params -> evaluation_params Types.sig0

val make_initial_state : prog_params -> Joint_semantics.state_pc Errors.res

val joint_classify_step :
  Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
  StructuredTraces.status_class

val joint_classify_final :
  Joint.unserialized_params -> Joint.joint_fin_step ->
  StructuredTraces.status_class

val joint_classify :
  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
  -> StructuredTraces.status_class

val joint_call_ident :
  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
  -> AST.ident

val joint_tailcall_ident :
  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
  -> AST.ident

val pcDeq : Deqsets.deqSet

val cost_label_of_stmt :
  Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
  CostLabel.costlabel Types.option

val joint_label_of_pc :
  Joint_semantics.sem_params -> evaluation_params ->
  ByteValues.program_counter -> CostLabel.costlabel Types.option

val exit_pc' : ByteValues.program_counter

val joint_final :
  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
  -> Integers.int Types.option

val joint_abstract_status : prog_params -> StructuredTraces.abstract_status

val joint_status :
  Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
  Types.option) -> StructuredTraces.abstract_status