open Preamble

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 CostLabel

open Events

open IOMonad

open IO

open BEMem

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open BackEndOps

open Joint

open I8051bis

open ExtraGlobalenvs

type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
                     stack_sizes : (AST.ident -> Nat.nat Types.option);
                     premain : 'f;
                     pc_from_label : (Pointers.block Types.sig0 -> 'f ->
                                     Graphs.label ->
                                     ByteValues.program_counter Types.option) }

val genv_gen_rect_Type4 :
  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
  'a1 genv_gen -> 'a2

val genv_gen_rect_Type5 :
  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
  'a1 genv_gen -> 'a2

val genv_gen_rect_Type3 :
  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
  'a1 genv_gen -> 'a2

val genv_gen_rect_Type2 :
  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
  'a1 genv_gen -> 'a2

val genv_gen_rect_Type1 :
  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
  'a1 genv_gen -> 'a2

val genv_gen_rect_Type0 :
  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
  'a1 genv_gen -> 'a2

val ge :
  AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t

val stack_sizes :
  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option

val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1

val pc_from_label :
  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1 ->
  Graphs.label -> ByteValues.program_counter Types.option

val genv_gen_inv_rect_Type4 :
  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
  Types.option) -> __ -> 'a2) -> 'a2

val genv_gen_inv_rect_Type3 :
  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
  Types.option) -> __ -> 'a2) -> 'a2

val genv_gen_inv_rect_Type2 :
  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
  Types.option) -> __ -> 'a2) -> 'a2

val genv_gen_inv_rect_Type1 :
  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
  Types.option) -> __ -> 'a2) -> 'a2

val genv_gen_inv_rect_Type0 :
  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
  Types.option) -> __ -> 'a2) -> 'a2

val genv_gen_discr :
  AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __

val genv_gen_jmdiscr :
  AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __

val dpi1__o__ge__o__inject :
  AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
  Globalenvs.genv_t Types.sig0

val eject__o__ge__o__inject :
  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
  Globalenvs.genv_t Types.sig0

val ge__o__inject :
  AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
  Types.sig0

val dpi1__o__ge :
  AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
  Globalenvs.genv_t

val eject__o__ge :
  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
  Globalenvs.genv_t

val pre_main_id : AST.ident

val fetch_function :
  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
  (AST.ident, 'a1 AST.fundef) Types.prod Errors.res

val fetch_internal_function :
  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
  (AST.ident, 'a1) Types.prod Errors.res

val code_block_of_block :
  Pointers.block -> Pointers.block Types.sig0 Types.option

val block_of_funct_id :
  'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
  Types.sig0 Errors.res

val gen_pc_from_label :
  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
  ByteValues.program_counter Errors.res

type genv = Joint.joint_closed_internal_function genv_gen

type sem_state_params = { empty_framesT : __;
                          empty_regsT : (ByteValues.xpointer -> __);
                          load_sp : (__ -> ByteValues.xpointer Errors.res);
                          save_sp : (__ -> ByteValues.xpointer -> __) }

val sem_state_params_rect_Type4 :
  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  'a1) -> sem_state_params -> 'a1

val sem_state_params_rect_Type5 :
  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  'a1) -> sem_state_params -> 'a1

val sem_state_params_rect_Type3 :
  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  'a1) -> sem_state_params -> 'a1

val sem_state_params_rect_Type2 :
  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  'a1) -> sem_state_params -> 'a1

val sem_state_params_rect_Type1 :
  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  'a1) -> sem_state_params -> 'a1

val sem_state_params_rect_Type0 :
  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  'a1) -> sem_state_params -> 'a1

type framesT 

val empty_framesT : sem_state_params -> __

type regsT 

val empty_regsT : sem_state_params -> ByteValues.xpointer -> __

val load_sp : sem_state_params -> __ -> ByteValues.xpointer Errors.res

val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __

val sem_state_params_inv_rect_Type4 :
  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  __ -> 'a1) -> 'a1

val sem_state_params_inv_rect_Type3 :
  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  __ -> 'a1) -> 'a1

val sem_state_params_inv_rect_Type2 :
  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  __ -> 'a1) -> 'a1

val sem_state_params_inv_rect_Type1 :
  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  __ -> 'a1) -> 'a1

val sem_state_params_inv_rect_Type0 :
  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
  __ -> 'a1) -> 'a1

val sem_state_params_jmdiscr : sem_state_params -> sem_state_params -> __

type internal_stack =
| Empty_is
| One_is of ByteValues.beval
| Both_is of ByteValues.beval * ByteValues.beval

val internal_stack_rect_Type4 :
  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
  -> 'a1) -> internal_stack -> 'a1

val internal_stack_rect_Type5 :
  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
  -> 'a1) -> internal_stack -> 'a1

val internal_stack_rect_Type3 :
  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
  -> 'a1) -> internal_stack -> 'a1

val internal_stack_rect_Type2 :
  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
  -> 'a1) -> internal_stack -> 'a1

val internal_stack_rect_Type1 :
  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
  -> 'a1) -> internal_stack -> 'a1

val internal_stack_rect_Type0 :
  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
  -> 'a1) -> internal_stack -> 'a1

val internal_stack_inv_rect_Type4 :
  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1

val internal_stack_inv_rect_Type3 :
  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1

val internal_stack_inv_rect_Type2 :
  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1

val internal_stack_inv_rect_Type1 :
  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1

val internal_stack_inv_rect_Type0 :
  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1

val internal_stack_discr : internal_stack -> internal_stack -> __

val internal_stack_jmdiscr : internal_stack -> internal_stack -> __

val is_push : internal_stack -> ByteValues.beval -> internal_stack Errors.res

val is_pop :
  internal_stack -> (ByteValues.beval, internal_stack) Types.prod Errors.res

type state = { st_frms : __ Types.option; istack : internal_stack;
               carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
               stack_usage : Nat.nat }

val state_rect_Type4 :
  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1

val state_rect_Type5 :
  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1

val state_rect_Type3 :
  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1

val state_rect_Type2 :
  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1

val state_rect_Type1 :
  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1

val state_rect_Type0 :
  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1

val st_frms : sem_state_params -> state -> __ Types.option

val istack : sem_state_params -> state -> internal_stack

val carry : sem_state_params -> state -> ByteValues.bebit

val regs : sem_state_params -> state -> __

val m : sem_state_params -> state -> BEMem.bemem

val stack_usage : sem_state_params -> state -> Nat.nat

val state_inv_rect_Type4 :
  sem_state_params -> state -> (__ Types.option -> internal_stack ->
  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1

val state_inv_rect_Type3 :
  sem_state_params -> state -> (__ Types.option -> internal_stack ->
  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1

val state_inv_rect_Type2 :
  sem_state_params -> state -> (__ Types.option -> internal_stack ->
  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1

val state_inv_rect_Type1 :
  sem_state_params -> state -> (__ Types.option -> internal_stack ->
  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1

val state_inv_rect_Type0 :
  sem_state_params -> state -> (__ Types.option -> internal_stack ->
  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1

val state_jmdiscr : sem_state_params -> state -> state -> __

val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res

type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
                  last_pop : ByteValues.program_counter }

val state_pc_rect_Type4 :
  sem_state_params -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1

val state_pc_rect_Type5 :
  sem_state_params -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1

val state_pc_rect_Type3 :
  sem_state_params -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1

val state_pc_rect_Type2 :
  sem_state_params -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1

val state_pc_rect_Type1 :
  sem_state_params -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1

val state_pc_rect_Type0 :
  sem_state_params -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1

val st_no_pc : sem_state_params -> state_pc -> state

val pc : sem_state_params -> state_pc -> ByteValues.program_counter

val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter

val state_pc_inv_rect_Type4 :
  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> __ -> 'a1) -> 'a1

val state_pc_inv_rect_Type3 :
  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> __ -> 'a1) -> 'a1

val state_pc_inv_rect_Type2 :
  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> __ -> 'a1) -> 'a1

val state_pc_inv_rect_Type1 :
  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> __ -> 'a1) -> 'a1

val state_pc_inv_rect_Type0 :
  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
  ByteValues.program_counter -> __ -> 'a1) -> 'a1

val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __

val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __

val dpi1__o__st_no_pc__o__inject :
  sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0

val eject__o__st_no_pc__o__inject :
  sem_state_params -> state_pc Types.sig0 -> state Types.sig0

val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0

val dpi1__o__st_no_pc :
  sem_state_params -> (state_pc, 'a1) Types.dPair -> state

val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state

val init_pc : ByteValues.program_counter

val null_pc : Positive.pos -> ByteValues.program_counter

val set_m : sem_state_params -> BEMem.bemem -> state -> state

val set_regs : sem_state_params -> __ -> state -> state

val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state

val set_carry : sem_state_params -> ByteValues.bebit -> state -> state

val set_istack : sem_state_params -> internal_stack -> state -> state

val set_pc :
  sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc

val set_no_pc : sem_state_params -> state -> state_pc -> state_pc

val set_last_pop :
  sem_state_params -> state -> ByteValues.program_counter -> state_pc

val set_frms : sem_state_params -> __ -> state -> state

type call_kind =
| PTR
| ID

val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1

val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1

val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1

val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1

val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1

val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1

val call_kind_inv_rect_Type4 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val call_kind_inv_rect_Type3 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val call_kind_inv_rect_Type2 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val call_kind_inv_rect_Type1 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val call_kind_inv_rect_Type0 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val call_kind_discr : call_kind -> call_kind -> __

val call_kind_jmdiscr : call_kind -> call_kind -> __

val kind_of_call :
  Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum ->
  call_kind

type 'f sem_unserialized_params = { st_pars : sem_state_params;
                                    acca_store_ : (__ -> ByteValues.beval ->
                                                  __ -> __ Errors.res);
                                    acca_retrieve_ : (__ -> __ ->
                                                     ByteValues.beval
                                                     Errors.res);
                                    acca_arg_retrieve_ : (__ -> __ ->
                                                         ByteValues.beval
                                                         Errors.res);
                                    accb_store_ : (__ -> ByteValues.beval ->
                                                  __ -> __ Errors.res);
                                    accb_retrieve_ : (__ -> __ ->
                                                     ByteValues.beval
                                                     Errors.res);
                                    accb_arg_retrieve_ : (__ -> __ ->
                                                         ByteValues.beval
                                                         Errors.res);
                                    dpl_store_ : (__ -> ByteValues.beval ->
                                                 __ -> __ Errors.res);
                                    dpl_retrieve_ : (__ -> __ ->
                                                    ByteValues.beval
                                                    Errors.res);
                                    dpl_arg_retrieve_ : (__ -> __ ->
                                                        ByteValues.beval
                                                        Errors.res);
                                    dph_store_ : (__ -> ByteValues.beval ->
                                                 __ -> __ Errors.res);
                                    dph_retrieve_ : (__ -> __ ->
                                                    ByteValues.beval
                                                    Errors.res);
                                    dph_arg_retrieve_ : (__ -> __ ->
                                                        ByteValues.beval
                                                        Errors.res);
                                    snd_arg_retrieve_ : (__ -> __ ->
                                                        ByteValues.beval
                                                        Errors.res);
                                    pair_reg_move_ : (__ -> __ -> __
                                                     Errors.res);
                                    save_frame : (call_kind -> __ -> state_pc
                                                 -> state Errors.res);
                                    setup_call : (Nat.nat -> __ -> __ ->
                                                 state -> state Errors.res);
                                    fetch_external_args : (AST.external_function
                                                          -> state -> __ ->
                                                          Values.val0
                                                          List.list
                                                          Errors.res);
                                    set_result : (Values.val0 List.list -> __
                                                 -> state -> state
                                                 Errors.res);
                                    call_args_for_main : __;
                                    call_dest_for_main : __;
                                    read_result : (AST.ident List.list -> 'f
                                                  AST.fundef
                                                  Globalenvs.genv_t -> __ ->
                                                  state -> ByteValues.beval
                                                  List.list Errors.res);
                                    eval_ext_seq : (AST.ident List.list -> 'f
                                                   genv_gen -> __ ->
                                                   AST.ident -> state ->
                                                   state Errors.res);
                                    pop_frame : (AST.ident List.list -> 'f
                                                genv_gen -> AST.ident -> __
                                                -> state -> (state,
                                                ByteValues.program_counter)
                                                Types.prod Errors.res) }

val sem_unserialized_params_rect_Type4 :
  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
  sem_unserialized_params -> 'a2

val sem_unserialized_params_rect_Type5 :
  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
  sem_unserialized_params -> 'a2

val sem_unserialized_params_rect_Type3 :
  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
  sem_unserialized_params -> 'a2

val sem_unserialized_params_rect_Type2 :
  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
  sem_unserialized_params -> 'a2

val sem_unserialized_params_rect_Type1 :
  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
  sem_unserialized_params -> 'a2

val sem_unserialized_params_rect_Type0 :
  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
  sem_unserialized_params -> 'a2

val st_pars :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  sem_state_params

val acca_store_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> __ -> __ Errors.res

val acca_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val acca_arg_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val accb_store_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> __ -> __ Errors.res

val accb_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val accb_arg_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val dpl_store_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> __ -> __ Errors.res

val dpl_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val dpl_arg_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val dph_store_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> __ -> __ Errors.res

val dph_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val dph_arg_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val snd_arg_retrieve_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
  ByteValues.beval Errors.res

val pair_reg_move_ :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> __
  Errors.res

val save_frame :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind -> __
  -> state_pc -> state Errors.res

val setup_call :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
  -> __ -> state -> state Errors.res

val fetch_external_args :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  AST.external_function -> state -> __ -> Values.val0 List.list Errors.res

val set_result :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
  List.list -> __ -> state -> state Errors.res

val call_args_for_main :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __

val call_dest_for_main :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __

val read_result :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
  List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
  ByteValues.beval List.list Errors.res

val eval_ext_seq :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
  List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res

val pop_frame :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res

val sem_unserialized_params_inv_rect_Type4 :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2

val sem_unserialized_params_inv_rect_Type3 :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2

val sem_unserialized_params_inv_rect_Type2 :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2

val sem_unserialized_params_inv_rect_Type1 :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2

val sem_unserialized_params_inv_rect_Type0 :
  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2

val sem_unserialized_params_jmdiscr :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
  sem_unserialized_params -> __

val helper_def_retrieve :
  (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ -> 'a1
  -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
  sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res

val helper_def_store :
  (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
  ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
  'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
  Errors.res

val acca_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val acca_store :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> state -> state Errors.res

val acca_arg_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val accb_store :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> state -> state Errors.res

val accb_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val accb_arg_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val dpl_store :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> state -> state Errors.res

val dpl_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val dpl_arg_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val dph_store :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
  ByteValues.beval -> state -> state Errors.res

val dph_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val dph_arg_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val snd_arg_retrieve :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  ByteValues.beval Errors.res

val pair_reg_move :
  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
  __

val push : sem_state_params -> state -> ByteValues.beval -> state Errors.res

val pop :
  sem_state_params -> state -> (ByteValues.beval, state) Types.prod
  Errors.res

val push_ra :
  sem_state_params -> state -> ByteValues.program_counter -> state Errors.res

val pop_ra :
  sem_state_params -> state -> (state, ByteValues.program_counter) Types.prod
  Errors.res

type serialized_params = { spp : Joint.params;
                           msu_pars : Joint.joint_closed_internal_function
                                      sem_unserialized_params;
                           offset_of_point : (__ -> Positive.pos);
                           point_of_offset : (Positive.pos -> __) }

val serialized_params_rect_Type4 :
  (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> 'a1) -> serialized_params -> 'a1

val serialized_params_rect_Type5 :
  (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> 'a1) -> serialized_params -> 'a1

val serialized_params_rect_Type3 :
  (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> 'a1) -> serialized_params -> 'a1

val serialized_params_rect_Type2 :
  (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> 'a1) -> serialized_params -> 'a1

val serialized_params_rect_Type1 :
  (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> 'a1) -> serialized_params -> 'a1

val serialized_params_rect_Type0 :
  (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> 'a1) -> serialized_params -> 'a1

val spp : serialized_params -> Joint.params

val msu_pars :
  serialized_params -> Joint.joint_closed_internal_function
  sem_unserialized_params

val offset_of_point : serialized_params -> __ -> Positive.pos

val point_of_offset : serialized_params -> Positive.pos -> __

val serialized_params_inv_rect_Type4 :
  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> __ -> 'a1) -> 'a1

val serialized_params_inv_rect_Type3 :
  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> __ -> 'a1) -> 'a1

val serialized_params_inv_rect_Type2 :
  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> __ -> 'a1) -> 'a1

val serialized_params_inv_rect_Type1 :
  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> __ -> 'a1) -> 'a1

val serialized_params_inv_rect_Type0 :
  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
  __ -> __ -> __ -> 'a1) -> 'a1

val serialized_params_jmdiscr : serialized_params -> serialized_params -> __

val spp__o__stmt_pars : serialized_params -> Joint.stmt_params

val spp__o__stmt_pars__o__uns_pars : serialized_params -> Joint.uns_params

val spp__o__stmt_pars__o__uns_pars__o__u_pars :
  serialized_params -> Joint.unserialized_params

val msu_pars__o__st_pars : serialized_params -> sem_state_params

type sem_params = { spp' : serialized_params;
                    pre_main_generator : (Joint.joint_program ->
                                         Joint.joint_closed_internal_function) }

val sem_params_rect_Type4 :
  (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1

val sem_params_rect_Type5 :
  (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1

val sem_params_rect_Type3 :
  (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1

val sem_params_rect_Type2 :
  (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1

val sem_params_rect_Type1 :
  (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1

val sem_params_rect_Type0 :
  (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1

val spp' : sem_params -> serialized_params

val pre_main_generator :
  sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function

val sem_params_inv_rect_Type4 :
  sem_params -> (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_params_inv_rect_Type3 :
  sem_params -> (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_params_inv_rect_Type2 :
  sem_params -> (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_params_inv_rect_Type1 :
  sem_params -> (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_params_inv_rect_Type0 :
  sem_params -> (serialized_params -> (Joint.joint_program ->
  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1

val sem_params_jmdiscr : sem_params -> sem_params -> __

val spp'__o__msu_pars :
  sem_params -> Joint.joint_closed_internal_function sem_unserialized_params

val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params

val spp'__o__spp : sem_params -> Joint.params

val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params

val spp'__o__spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params

val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
  sem_params -> Joint.unserialized_params

val pc_of_point :
  sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter

val point_of_pc : sem_params -> ByteValues.program_counter -> __

val fetch_statement :
  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
  ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
  Joint.joint_statement) Types.prod Errors.res

val pc_of_label :
  sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
  Graphs.label -> ByteValues.program_counter Errors.res

val succ_pc :
  sem_params -> ByteValues.program_counter -> __ ->
  ByteValues.program_counter

val goto :
  sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
  state_pc Errors.res

val next : sem_params -> __ -> state_pc -> state_pc

val next_of_call_pc :
  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
  __ Errors.res

val eval_seq_no_pc :
  sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
  -> state -> state Errors.res

val block_of_call :
  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
  (__, __) Types.prod) Types.sum -> state -> __

val eval_external_call :
  sem_params -> AST.external_function -> __ -> __ -> state -> __

val increment_stack_usage : sem_state_params -> Nat.nat -> state -> state

val decrement_stack_usage : sem_state_params -> Nat.nat -> state -> state

val eval_internal_call :
  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
  Joint.joint_internal_function -> __ -> state -> __

val is_inl : ('a1, 'a2) Types.sum -> Bool.bool

val eval_call :
  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
  (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __

val eval_statement_no_pc :
  sem_params -> AST.ident List.list -> genv -> AST.ident ->
  Joint.joint_statement -> state -> state Errors.res

val eval_return :
  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
  __ -> state -> __

val eval_tailcall :
  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
  (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __ ->
  state_pc -> __

val eval_statement_advance :
  sem_params -> AST.ident List.list -> genv -> AST.ident ->
  Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
  -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO

val eval_state :
  sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
  IO.io_in, state_pc) IOMonad.iO