open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

type move_dst =
| PSD of Registers.register
| HDW of I8051.register

val move_dst_rect_Type4 :
  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1

val move_dst_rect_Type5 :
  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1

val move_dst_rect_Type3 :
  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1

val move_dst_rect_Type2 :
  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1

val move_dst_rect_Type1 :
  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1

val move_dst_rect_Type0 :
  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1

val move_dst_inv_rect_Type4 :
  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
  'a1) -> 'a1

val move_dst_inv_rect_Type3 :
  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
  'a1) -> 'a1

val move_dst_inv_rect_Type2 :
  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
  'a1) -> 'a1

val move_dst_inv_rect_Type1 :
  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
  'a1) -> 'a1

val move_dst_inv_rect_Type0 :
  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
  'a1) -> 'a1

val move_dst_discr : move_dst -> move_dst -> __

val move_dst_jmdiscr : move_dst -> move_dst -> __

type move_src = move_dst Joint.argument

val move_src_from_dst : move_dst -> move_src

val dpi1__o__move_dst_to_src__o__inject :
  (move_dst, 'a1) Types.dPair -> move_src Types.sig0

val eject__o__move_dst_to_src__o__inject :
  move_dst Types.sig0 -> move_src Types.sig0

val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0

val dpi1__o__move_dst_to_src : (move_dst, 'a1) Types.dPair -> move_src

val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src

val psd_argument_move_src : Joint.psd_argument -> move_src

val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
  BitVector.byte -> move_src Types.sig0

val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0

val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0

val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0

val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
  BitVector.byte Types.sig0 -> move_src Types.sig0

val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
  BitVector.byte Types.sig0 -> move_src Types.sig0

val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
  Registers.register Types.sig0 -> move_src Types.sig0

val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
  Registers.register -> move_src Types.sig0

val dpi1__o__psd_argument_to_move_src__o__inject :
  (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0

val eject__o__psd_argument_to_move_src__o__inject :
  Joint.psd_argument Types.sig0 -> move_src Types.sig0

val psd_argument_to_move_src__o__inject :
  Joint.psd_argument -> move_src Types.sig0

val byte_to_psd_argument__o__psd_argument_to_move_src :
  BitVector.byte -> move_src

val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
  (BitVector.byte, 'a1) Types.dPair -> move_src

val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
  (BitVector.byte, 'a1) Types.dPair -> move_src

val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
  (Registers.register, 'a1) Types.dPair -> move_src

val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
  BitVector.byte Types.sig0 -> move_src

val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
  BitVector.byte Types.sig0 -> move_src

val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
  Registers.register Types.sig0 -> move_src

val reg_to_psd_argument__o__psd_argument_to_move_src :
  Registers.register -> move_src

val dpi1__o__psd_argument_to_move_src :
  (Joint.psd_argument, 'a1) Types.dPair -> move_src

val eject__o__psd_argument_to_move_src :
  Joint.psd_argument Types.sig0 -> move_src

type ertl_seq =
| Ertl_new_frame
| Ertl_del_frame
| Ertl_frame_size of Registers.register

val ertl_seq_rect_Type4 :
  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1

val ertl_seq_rect_Type5 :
  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1

val ertl_seq_rect_Type3 :
  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1

val ertl_seq_rect_Type2 :
  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1

val ertl_seq_rect_Type1 :
  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1

val ertl_seq_rect_Type0 :
  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1

val ertl_seq_inv_rect_Type4 :
  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
  -> 'a1

val ertl_seq_inv_rect_Type3 :
  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
  -> 'a1

val ertl_seq_inv_rect_Type2 :
  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
  -> 'a1

val ertl_seq_inv_rect_Type1 :
  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
  -> 'a1

val ertl_seq_inv_rect_Type0 :
  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
  -> 'a1

val ertl_seq_discr : ertl_seq -> ertl_seq -> __

val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __

val eRTL_uns : Joint.unserialized_params

val regs_from_move_dst : move_dst -> Registers.register List.list

val regs_from_move_src : move_src -> Registers.register List.list

val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list

val eRTL_functs : Joint.get_pseudo_reg_functs

val eRTL : Joint.graph_params

type ertl_program = Joint.joint_program

val dpi1__o__reg_to_ertl_snd_argument__o__inject :
  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0

val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0

val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
  (Registers.register, 'a1) Types.dPair -> move_src

val eject__o__reg_to_ertl_snd_argument__o__inject :
  Registers.register Types.sig0 -> Joint.psd_argument Types.sig0

val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
  Registers.register Types.sig0 -> move_src Types.sig0

val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
  Registers.register Types.sig0 -> move_src

val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
  Registers.register -> move_src

val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
  Registers.register -> move_src Types.sig0

val reg_to_ertl_snd_argument__o__inject :
  Registers.register -> Joint.psd_argument Types.sig0

val dpi1__o__reg_to_ertl_snd_argument :
  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument

val eject__o__reg_to_ertl_snd_argument :
  Registers.register Types.sig0 -> Joint.psd_argument

val dpi1__o__byte_to_ertl_snd_argument__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0

val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0

val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
  (BitVector.byte, 'a1) Types.dPair -> move_src

val eject__o__byte_to_ertl_snd_argument__o__inject :
  BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0

val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
  BitVector.byte Types.sig0 -> move_src Types.sig0

val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
  BitVector.byte Types.sig0 -> move_src

val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
  BitVector.byte -> move_src

val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
  BitVector.byte -> move_src Types.sig0

val byte_to_ertl_snd_argument__o__inject :
  BitVector.byte -> Joint.psd_argument Types.sig0

val dpi1__o__byte_to_ertl_snd_argument :
  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument

val eject__o__byte_to_ertl_snd_argument :
  BitVector.byte Types.sig0 -> Joint.psd_argument

val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq

val dpi1__o__ertl_seq_to_joint_seq__o__inject :
  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0

val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0

val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step

val eject__o__ertl_seq_to_joint_seq__o__inject :
  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0

val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0

val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step

val ertl_seq_to_joint_seq__o__seq_to_step :
  AST.ident List.list -> __ -> Joint.joint_step

val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
  AST.ident List.list -> __ -> Joint.joint_step Types.sig0

val ertl_seq_to_joint_seq__o__inject :
  AST.ident List.list -> __ -> Joint.joint_seq Types.sig0

val dpi1__o__ertl_seq_to_joint_seq :
  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq

val eject__o__ertl_seq_to_joint_seq :
  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq

val eRTL_premain : ertl_program -> Joint.joint_closed_internal_function