Source file elf_header.ml

(*Generated by Lem from elf_header.lem.*)
(** [elf_header] includes types, functions and other definitions for working with
  * ELF headers.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_function
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
(*import Set*)

open Lem_assert_extra

open Default_printing
open Endianness

open Elf_types_native_uint

open Byte_sequence
open Error
open Missing_pervasives
open Show

(** Special section header table indices *)

(** [shn_undef]: marks an undefined, missing or irrelevant section reference.
  * Present here instead of in elf_section_header_table.lem because a calculation
  * below requires this constant (i.e. forward reference in the ELF spec).
  *)
let shn_undef : Nat_big_num.num= ( (Nat_big_num.of_int 0))

(** [shn_xindex]: an escape value.  It indicates the actual section header index
  * is too large to fit in the containing field and is located in another
  * location (specific to the structure where it appears). Present here instead
  * of in elf_section_header_table.lem because a calculation below requires this
  * constant (i.e. forward reference in the ELF spec).
  *)
let shn_xindex : Nat_big_num.num= ( (Nat_big_num.of_int 65535)) (* 0xffff *)

(** ELF object file types.  Enumerates the ELF object file types specified in the
 *  System V ABI.  Values between [elf_ft_lo_os] and [elf_ft_hi_os] inclusive are
 *  reserved for operating system specific values typically defined in an
 *  addendum to the System V ABI for that operating system.  Values between
 *  [elf_ft_lo_proc] and [elf_ft_hi_proc] inclusive are processor specific and
 *  are typically defined in an addendum to the System V ABI for that processor
 *  series.
 *)

(** No file type *)
let elf_ft_none : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** Relocatable file *)
let elf_ft_rel : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** Executable file *)
let elf_ft_exec : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** Shared object file *)
let elf_ft_dyn : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** Core file *)
let elf_ft_core : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** Operating-system specific *)
let elf_ft_lo_os : Nat_big_num.num= ( (Nat_big_num.of_int 65024)) (* 0xfe00 *)
(** Operating-system specific *)
let elf_ft_hi_os : Nat_big_num.num= ( (Nat_big_num.of_int 65279)) (* 0xfeff *)
(** Processor specific *)
let elf_ft_lo_proc : Nat_big_num.num= ( (Nat_big_num.of_int 65280)) (* 0xff00 *)
(** Processor specific *)
let elf_ft_hi_proc : Nat_big_num.num= ( (Nat_big_num.of_int 65535)) (* 0xffff *)

(** [string_of_elf_file_type os proc m] produces a string representation of the
  * numeric encoding [m] of the ELF file type.  For values reserved for OS or
  * processor specific values, the higher-order functions [os] and [proc] are
  * used for printing, respectively.
  *)
(*val string_of_elf_file_type : (natural -> string) -> (natural -> string) -> natural -> string*)
let string_of_elf_file_type os_specific proc_specific m:string=
	 (if Nat_big_num.equal m elf_ft_none then
		"No file type"
	else if Nat_big_num.equal m elf_ft_rel then
		"REL (Relocatable file)"
	else if Nat_big_num.equal m elf_ft_exec then
		"EXEC (Executable file)"
	else if Nat_big_num.equal m elf_ft_dyn then
		"DYN (Shared object file)"
	else if Nat_big_num.equal m elf_ft_core then
		"CORE (Core file)"
	else if Nat_big_num.greater_equal m elf_ft_lo_os && Nat_big_num.less_equal m elf_ft_hi_os then
		os_specific m
	else if Nat_big_num.greater_equal m elf_ft_lo_proc && Nat_big_num.less_equal m elf_ft_hi_proc then
		proc_specific m
	else
		"Invalid file type")

(** [is_operating_specific_file_type_value] checks whether a numeric value is
  * reserved by the ABI for operating system-specific purposes.
  *)
(*val is_operating_system_specific_object_file_type_value : natural -> bool*)
let is_operating_system_specific_object_file_type_value v:bool=  (Nat_big_num.greater_equal
  v( (Nat_big_num.of_int 65024)) && Nat_big_num.less_equal v( (Nat_big_num.of_int 65279)))

(** [is_processor_specific_file_type_value] checks whether a numeric value is
  * reserved by the ABI for processor-specific purposes.
  *)
(*val is_processor_specific_object_file_type_value : natural -> bool*)
let is_processor_specific_object_file_type_value v:bool=  (Nat_big_num.greater_equal
  v( (Nat_big_num.of_int 65280)) && Nat_big_num.less_equal v( (Nat_big_num.of_int 65535)))

(** ELF machine architectures *)

(** RISC-V *)
let elf_ma_riscv : Nat_big_num.num= ( (Nat_big_num.of_int 243))
(** AMD GPU architecture *)
let elf_ma_amdgpu : Nat_big_num.num= ( (Nat_big_num.of_int 224))
(** Moxie processor family *)
let elf_ma_moxie : Nat_big_num.num= ( (Nat_big_num.of_int 223))
(** FTDI Chip FT32 high performance 32-bit RISC architecture *)
let elf_ma_ft32 : Nat_big_num.num= ( (Nat_big_num.of_int 222))
(** Controls and Data Services VISIUMcore processor *)
let elf_ma_visium : Nat_big_num.num= ( (Nat_big_num.of_int 221))
(** Zilog Z80 *)
let elf_ma_z80 : Nat_big_num.num= ( (Nat_big_num.of_int 220))
(** CSR Kalimba architecture family *)
let elf_ma_kalimba : Nat_big_num.num= ( (Nat_big_num.of_int 219))
(** Nanoradio optimised RISC *)
let elf_ma_norc : Nat_big_num.num= ( (Nat_big_num.of_int 218))
(** iCelero CoolEngine *)
let elf_ma_cool : Nat_big_num.num= ( (Nat_big_num.of_int 217))
(** Cognitive Smart Memory Processor *)
let elf_ma_coge : Nat_big_num.num= ( (Nat_big_num.of_int 216))
(** Paneve CDP architecture family *)
let elf_ma_cdp : Nat_big_num.num= ( (Nat_big_num.of_int 215))
(** KM211 KVARC processor *)
let elf_ma_kvarc : Nat_big_num.num= ( (Nat_big_num.of_int 214))
(** KM211 KMX8 8-bit processor *)
let elf_ma_kmx8 : Nat_big_num.num= ( (Nat_big_num.of_int 213))
(** KM211 KMX16 16-bit processor *)
let elf_ma_kmx16 : Nat_big_num.num= ( (Nat_big_num.of_int 212))
(** KM211 KMX32 32-bit processor *)
let elf_ma_kmx32 : Nat_big_num.num= ( (Nat_big_num.of_int 211))
(** KM211 KM32 32-bit processor *)
let elf_ma_km32 : Nat_big_num.num= ( (Nat_big_num.of_int 210))
(** Microchip 8-bit PIC(r) family *)
let elf_ma_mchp_pic : Nat_big_num.num= ( (Nat_big_num.of_int 204))
(** XMOS xCORE processor family *)
let elf_ma_xcore : Nat_big_num.num= ( (Nat_big_num.of_int 203))
(** Beyond BA2 CPU architecture *)
let elf_ma_ba2 : Nat_big_num.num= ( (Nat_big_num.of_int 202))
(** Beyond BA1 CPU architecture *)  
let elf_ma_ba1 : Nat_big_num.num= ( (Nat_big_num.of_int 201))
(** Freescale 56800EX Digital Signal Controller (DSC) *)
let elf_ma_5600ex : Nat_big_num.num= ( (Nat_big_num.of_int 200))
(** 199 Renesas 78KOR family *)
let elf_ma_78kor : Nat_big_num.num= ( (Nat_big_num.of_int 199))
(** Broadcom VideoCore V processor *)
let elf_ma_videocore5 : Nat_big_num.num= ( (Nat_big_num.of_int 198))
(** Renesas RL78 family *)
let elf_ma_rl78 : Nat_big_num.num= ( (Nat_big_num.of_int 197))
(** Open8 8-bit RISC soft processing core *)
let elf_ma_open8 : Nat_big_num.num= ( (Nat_big_num.of_int 196))
(** Synopsys ARCompact V2 *)
let elf_ma_arc_compact2 : Nat_big_num.num= ( (Nat_big_num.of_int 195))
(** KIPO_KAIST Core-A 2nd generation processor family *)
let elf_ma_corea_2nd : Nat_big_num.num= ( (Nat_big_num.of_int 194))
(** KIPO_KAIST Core-A 1st generation processor family *)
let elf_ma_corea_1st : Nat_big_num.num= ( (Nat_big_num.of_int 193))
(** CloudShield architecture family *)
let elf_ma_cloudshield : Nat_big_num.num= ( (Nat_big_num.of_int 192))
(** Infineon Technologies SLE9X core *)
let elf_ma_sle9x : Nat_big_num.num= ( (Nat_big_num.of_int 179))
(** Intel L10M *)
let elf_ma_l10m : Nat_big_num.num= ( (Nat_big_num.of_int 180))
(** Intel K10M *)
let elf_ma_k10m : Nat_big_num.num= ( (Nat_big_num.of_int 181))
(** ARM 64-bit architecture (AARCH64) *)
let elf_ma_aarch64 : Nat_big_num.num= ( (Nat_big_num.of_int 183))
(** Atmel Corporation 32-bit microprocessor family *)
let elf_ma_avr32 : Nat_big_num.num= ( (Nat_big_num.of_int 185))
(** STMicroelectronics STM8 8-bit microcontroller *)
let elf_ma_stm8 : Nat_big_num.num= ( (Nat_big_num.of_int 186))
(** Tilera TILE64 multicore architecture family *)
let elf_ma_tile64 : Nat_big_num.num= ( (Nat_big_num.of_int 187))
(** Tilera TILEPro multicore architecture family *)
let elf_ma_tilepro : Nat_big_num.num= ( (Nat_big_num.of_int 188))
(** Xilinix MicroBlaze 32-bit RISC soft processor core *)
let elf_ma_microblaze : Nat_big_num.num= ( (Nat_big_num.of_int 189))
(** NVIDIA CUDA architecture *)
let elf_ma_cuda : Nat_big_num.num= ( (Nat_big_num.of_int 190))
(** Tilera TILE-Gx multicore architecture family *)
let elf_ma_tilegx : Nat_big_num.num= ( (Nat_big_num.of_int 191))
(** Cypress M8C microprocessor *)
let elf_ma_cypress : Nat_big_num.num= ( (Nat_big_num.of_int 161))
(** Renesas R32C series microprocessors *)
let elf_ma_r32c : Nat_big_num.num= ( (Nat_big_num.of_int 162))
(** NXP Semiconductors TriMedia architecture family *)
let elf_ma_trimedia : Nat_big_num.num= ( (Nat_big_num.of_int 163))
(** QUALCOMM DSP6 processor *)
let elf_ma_qdsp6 : Nat_big_num.num= ( (Nat_big_num.of_int 164))
(** Intel 8051 and variants *)
let elf_ma_8051 : Nat_big_num.num= ( (Nat_big_num.of_int 165))
(** STMicroelectronics STxP7x family of configurable and extensible RISC processors *)
let elf_ma_stxp7x : Nat_big_num.num= ( (Nat_big_num.of_int 166))
(** Andes Technology compact code size embedded RISC processor family *)
let elf_ma_nds32 : Nat_big_num.num= ( (Nat_big_num.of_int 167))
(** Cyan Technology eCOG1X family *)
let elf_ma_ecog1x : Nat_big_num.num= ( (Nat_big_num.of_int 168))
(** Dallas Semiconductor MAXQ30 Core Micro-controllers *)
let elf_ma_maxq30 : Nat_big_num.num= ( (Nat_big_num.of_int 169))
(** New Japan Radio (NJR) 16-bit DSP Processor *)
let elf_ma_ximo16 : Nat_big_num.num= ( (Nat_big_num.of_int 170))
(** M2000 Reconfigurable RISC Microprocessor *)
let elf_ma_manik : Nat_big_num.num= ( (Nat_big_num.of_int 171))
(** Cray Inc. NV2 vector architecture *)
let elf_ma_craynv2 : Nat_big_num.num= ( (Nat_big_num.of_int 172))
(** Renesas RX family *)
let elf_ma_rx : Nat_big_num.num= ( (Nat_big_num.of_int 173))
(** Imagination Technologies META processor architecture *)
let elf_ma_metag : Nat_big_num.num= ( (Nat_big_num.of_int 174))
(** MCST Elbrus general purpose hardware architecture *)
let elf_ma_mcst_elbrus : Nat_big_num.num= ( (Nat_big_num.of_int 175))
(** Cyan Technology eCOG16 family *)
let elf_ma_ecog16 : Nat_big_num.num= ( (Nat_big_num.of_int 176))
(** National Semiconductor CompactRISC CR16 16-bit microprocessor *)
let elf_ma_cr16 : Nat_big_num.num= ( (Nat_big_num.of_int 177))
(** Freescale Extended Time Processing Unit *)
let elf_ma_etpu : Nat_big_num.num= ( (Nat_big_num.of_int 178))
(** Altium TSK3000 core *)
let elf_ma_tsk3000 : Nat_big_num.num= ( (Nat_big_num.of_int 131))
(** Freescale RS08 embedded processor *)
let elf_ma_rs08 : Nat_big_num.num= ( (Nat_big_num.of_int 132))
(** Analog Devices SHARC family of 32-bit DSP processors *)
let elf_ma_sharc : Nat_big_num.num= ( (Nat_big_num.of_int 133))
(** Cyan Technology eCOG2 microprocessor *)
let elf_ma_ecog2 : Nat_big_num.num= ( (Nat_big_num.of_int 134))
(** Sunplus S+core7 RISC processor *)
let elf_ma_ccore7 : Nat_big_num.num= ( (Nat_big_num.of_int 135))
(** New Japan Radio (NJR) 24-bit DSP Processor *)
let elf_ma_dsp24 : Nat_big_num.num= ( (Nat_big_num.of_int 136))
(** Broadcom VideoCore III processor *)
let elf_ma_videocore3 : Nat_big_num.num= ( (Nat_big_num.of_int 137))
(** RISC processor for Lattice FPGA architecture *)
let elf_ma_latticemico32 : Nat_big_num.num= ( (Nat_big_num.of_int 138))
(** Seiko Epson C17 family *)
let elf_ma_c17 : Nat_big_num.num= ( (Nat_big_num.of_int 139))
(** The Texas Instruments TMS320C6000 DSP family *)
let elf_ma_c6000 : Nat_big_num.num= ( (Nat_big_num.of_int 140))
(** The Texas Instruments TMS320C2000 DSP family *)
let elf_ma_c2000 : Nat_big_num.num= ( (Nat_big_num.of_int 141))
(** The Texas Instruments TMS320C55x DSP family *)
let elf_ma_c5500 : Nat_big_num.num= ( (Nat_big_num.of_int 142))
(** STMicroelectronics 64bit VLIW Data Signal Processor *)
let elf_ma_mmdsp_plus : Nat_big_num.num= ( (Nat_big_num.of_int 160))
(** LSI Logic 16-bit DSP Processor *)
let elf_ma_zsp : Nat_big_num.num= ( (Nat_big_num.of_int 79))
(** Donald Knuth's educational 64-bit processor *)
let elf_ma_mmix : Nat_big_num.num= ( (Nat_big_num.of_int 80))
(** Harvard University machine-independent object files *)
let elf_ma_huany : Nat_big_num.num= ( (Nat_big_num.of_int 81))
(** SiTera Prism *)
let elf_ma_prism : Nat_big_num.num= ( (Nat_big_num.of_int 82))
(** Atmel AVR 8-bit microcontroller *)
let elf_ma_avr : Nat_big_num.num= ( (Nat_big_num.of_int 83))
(** Fujitsu FR30 *)
let elf_ma_fr30 : Nat_big_num.num= ( (Nat_big_num.of_int 84))
(** Mitsubishi D10V *)
let elf_ma_d10v : Nat_big_num.num= ( (Nat_big_num.of_int 85))
(** Mitsubishi D30V *)
let elf_ma_d30v : Nat_big_num.num= ( (Nat_big_num.of_int 86))
(** NEC v850 *)
let elf_ma_v850 : Nat_big_num.num= ( (Nat_big_num.of_int 87))
(** Mitsubishi M32R *)
let elf_ma_m32r : Nat_big_num.num= ( (Nat_big_num.of_int 88))
(** Matsushita MN10300 *)
let elf_ma_mn10300 : Nat_big_num.num= ( (Nat_big_num.of_int 89))
(** Matsushita MN10200 *)
let elf_ma_mn10200 : Nat_big_num.num= ( (Nat_big_num.of_int 90))
(** picoJava *)
let elf_ma_pj : Nat_big_num.num= ( (Nat_big_num.of_int 91))
(** OpenRISC 32-bit embedded processor *)
let elf_ma_openrisc : Nat_big_num.num= ( (Nat_big_num.of_int 92))
(** ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5) *)
let elf_ma_arc_compact : Nat_big_num.num= ( (Nat_big_num.of_int 93))
(** Tensilica Xtensa Architecture *)
let elf_ma_xtensa : Nat_big_num.num= ( (Nat_big_num.of_int 94))
(** Alphamosaic VideoCore processor *)
let elf_ma_videocore : Nat_big_num.num= ( (Nat_big_num.of_int 95))
(** Thompson Multimedia General Purpose Processor *)
let elf_ma_tmm_gpp : Nat_big_num.num= ( (Nat_big_num.of_int 96))
(** National Semiconductor 32000 series *)
let elf_ma_ns32k : Nat_big_num.num= ( (Nat_big_num.of_int 97))
(** Tenor Network TPC processor *)
let elf_ma_tpc : Nat_big_num.num= ( (Nat_big_num.of_int 98))
(** Trebia SNP 1000 processor *)
let elf_ma_snp1k : Nat_big_num.num= ( (Nat_big_num.of_int 99))
(** STMicroelectronics ST200 microcontroller *)
let elf_ma_st200 : Nat_big_num.num= ( (Nat_big_num.of_int 100))
(** Ubicom IP2xxx microcontroller family *)
let elf_ma_ip2k : Nat_big_num.num= ( (Nat_big_num.of_int 101))
(** MAX Processor *)
let elf_ma_max : Nat_big_num.num= ( (Nat_big_num.of_int 102))
(** National Semiconductor CompactRISC microprocessor *)
let elf_ma_cr : Nat_big_num.num= ( (Nat_big_num.of_int 103))
(** Fujitsu F2MC16 *)
let elf_ma_f2mc16 : Nat_big_num.num= ( (Nat_big_num.of_int 104))
(** Texas Instruments embedded microcontroller msp430 *)
let elf_ma_msp430 : Nat_big_num.num= ( (Nat_big_num.of_int 105))
(** Analog Devices Blackfin (DSP) processor *)
let elf_ma_blackfin : Nat_big_num.num= ( (Nat_big_num.of_int 106))
(** S1C33 Family of Seiko Epson processors *)
let elf_ma_se_c33 : Nat_big_num.num= ( (Nat_big_num.of_int 107))
(** Sharp embedded microprocessor *)
let elf_ma_sep : Nat_big_num.num= ( (Nat_big_num.of_int 108))
(** Arca RISC Microprocessor *)
let elf_ma_arca : Nat_big_num.num= ( (Nat_big_num.of_int 109))
(** Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University *)
let elf_ma_unicore : Nat_big_num.num= ( (Nat_big_num.of_int 110))
(** eXcess: 16/32/64-bit configurable embedded CPU *)
let elf_ma_excess : Nat_big_num.num= ( (Nat_big_num.of_int 111))
(** Icera Semiconductor Inc. Deep Execution Processor *)
let elf_ma_dxp : Nat_big_num.num= ( (Nat_big_num.of_int 112))
(** Altera Nios II soft-core processor *)
let elf_ma_altera_nios2 : Nat_big_num.num= ( (Nat_big_num.of_int 113))
(** National Semiconductor CompactRISC CRX microprocessor *)
let elf_ma_crx : Nat_big_num.num= ( (Nat_big_num.of_int 114))
(** Motorola XGATE embedded processor *)
let elf_ma_xgate : Nat_big_num.num= ( (Nat_big_num.of_int 115))
(** Infineon C16x/XC16x processor *)
let elf_ma_c166 : Nat_big_num.num= ( (Nat_big_num.of_int 116))
(** Renesas M16C series microprocessors *)
let elf_ma_m16c : Nat_big_num.num= ( (Nat_big_num.of_int 117))
(** Microchip Technology dsPIC30F Digital Signal Controller *)
let elf_ma_dspic30f : Nat_big_num.num= ( (Nat_big_num.of_int 118))
(** Freescale Communication Engine RISC core *)
let elf_ma_ce : Nat_big_num.num= ( (Nat_big_num.of_int 119))
(** Renesas M32C series microprocessors *)
let elf_ma_m32c : Nat_big_num.num= ( (Nat_big_num.of_int 120))
(** No machine *)
let elf_ma_none : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** AT&T WE 32100 *)
let elf_ma_m32 : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** SPARC *)
let elf_ma_sparc : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** Intel 80386 *)
let elf_ma_386 : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** Motorola 68000 *)
let elf_ma_68k : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** Motorola 88000 *)
let elf_ma_88k : Nat_big_num.num= ( (Nat_big_num.of_int 5))
(** Intel 80860 *)
let elf_ma_860 : Nat_big_num.num= ( (Nat_big_num.of_int 7))
(** MIPS I Architecture *)
let elf_ma_mips : Nat_big_num.num= ( (Nat_big_num.of_int 8))
(** IBM System/370 Processor *)
let elf_ma_s370 : Nat_big_num.num= ( (Nat_big_num.of_int 9))
(** MIPS RS3000 Little-endian *)
let elf_ma_mips_rs3_le : Nat_big_num.num= ( (Nat_big_num.of_int 10))
(** Hewlett-Packard PA-RISC *)
let elf_ma_parisc : Nat_big_num.num= ( (Nat_big_num.of_int 15))
(** Fujitsu VPP500 *)
let elf_ma_vpp500 : Nat_big_num.num= ( (Nat_big_num.of_int 17))
(** Enhanced instruction set SPARC *)
let elf_ma_sparc32plus : Nat_big_num.num= ( (Nat_big_num.of_int 18))
(** Intel 80960 *)
let elf_ma_960 : Nat_big_num.num= ( (Nat_big_num.of_int 19))
(** PowerPC *)
let elf_ma_ppc : Nat_big_num.num= ( (Nat_big_num.of_int 20))
(** 64-bit PowerPC *)
let elf_ma_ppc64 : Nat_big_num.num= ( (Nat_big_num.of_int 21))
(** IBM System/390 Processor *)
let elf_ma_s390 : Nat_big_num.num= ( (Nat_big_num.of_int 22))
(** IBM SPU/SPC *)
let elf_ma_spu : Nat_big_num.num= ( (Nat_big_num.of_int 23))
(** NEC V800 *)
let elf_ma_v800 : Nat_big_num.num= ( (Nat_big_num.of_int 36))
(** Fujitsu FR20 *)
let elf_ma_fr20 : Nat_big_num.num= ( (Nat_big_num.of_int 37))
(** TRW RH-32 *)
let elf_ma_rh32 : Nat_big_num.num= ( (Nat_big_num.of_int 38))
(** Motorola RCE *)
let elf_ma_rce : Nat_big_num.num= ( (Nat_big_num.of_int 39))
(** ARM 32-bit architecture (AARCH32) *)
let elf_ma_arm : Nat_big_num.num= ( (Nat_big_num.of_int 40))
(** Digital Alpha *)
let elf_ma_alpha : Nat_big_num.num= ( (Nat_big_num.of_int 41))
(** Hitachi SH *)
let elf_ma_sh : Nat_big_num.num= ( (Nat_big_num.of_int 42))
(** SPARC Version 9 *)
let elf_ma_sparcv9 : Nat_big_num.num= ( (Nat_big_num.of_int 43))
(** Siemens TriCore embedded processor *)
let elf_ma_tricore : Nat_big_num.num= ( (Nat_big_num.of_int 44))
(** Argonaut RISC Core, Argonaut Technologies Inc. *)
let elf_ma_arc : Nat_big_num.num= ( (Nat_big_num.of_int 45))
(** Hitachi H8/300 *)
let elf_ma_h8_300 : Nat_big_num.num= ( (Nat_big_num.of_int 46))
(** Hitachi H8/300H *)
let elf_ma_h8_300h : Nat_big_num.num= ( (Nat_big_num.of_int 47))
(** Hitachi H8S *)
let elf_ma_h8s : Nat_big_num.num= ( (Nat_big_num.of_int 48))
(** Hitachi H8/500 *)
let elf_ma_h8_500 : Nat_big_num.num= ( (Nat_big_num.of_int 49))
(** Intel IA-64 processor architecture *)
let elf_ma_ia_64 : Nat_big_num.num= ( (Nat_big_num.of_int 50))
(** Stanford MIPS-X *)
let elf_ma_mips_x : Nat_big_num.num= ( (Nat_big_num.of_int 51))
(** Motorola ColdFire *)
let elf_ma_coldfire : Nat_big_num.num= ( (Nat_big_num.of_int 52))
(** Motorola M68HC12 *)
let elf_ma_68hc12 : Nat_big_num.num= ( (Nat_big_num.of_int 53))
(** Fujitsu MMA Multimedia Accelerator *)
let elf_ma_mma : Nat_big_num.num= ( (Nat_big_num.of_int 54))
(** Siemens PCP *)
let elf_ma_pcp : Nat_big_num.num= ( (Nat_big_num.of_int 55))
(** Sony nCPU embedded RISC processor *)
let elf_ma_ncpu : Nat_big_num.num= ( (Nat_big_num.of_int 56))
(** Denso NDR1 microprocessor *)
let elf_ma_ndr1 : Nat_big_num.num= ( (Nat_big_num.of_int 57))
(** Motorola Star*Core processor *)
let elf_ma_starcore : Nat_big_num.num= ( (Nat_big_num.of_int 58))
(** Toyota ME16 processor *)
let elf_ma_me16 : Nat_big_num.num= ( (Nat_big_num.of_int 59))
(** STMicroelectronics ST100 processor *)
let elf_ma_st100 : Nat_big_num.num= ( (Nat_big_num.of_int 60))
(** Advanced Logic Corp. TinyJ embedded processor family *)
let elf_ma_tinyj : Nat_big_num.num= ( (Nat_big_num.of_int 61))
(** AMD x86-64 architecture *)
let elf_ma_x86_64 : Nat_big_num.num= ( (Nat_big_num.of_int 62))
(** Sony DSP Processor *)
let elf_ma_pdsp : Nat_big_num.num= ( (Nat_big_num.of_int 63))
(** Digital Equipment Corp. PDP-10 *)
let elf_ma_pdp10 : Nat_big_num.num= ( (Nat_big_num.of_int 64))
(** Digital Equipment Corp. PDP-11 *)
let elf_ma_pdp11 : Nat_big_num.num= ( (Nat_big_num.of_int 65))
(** Siemens FX66 microcontroller *)
let elf_ma_fx66 : Nat_big_num.num= ( (Nat_big_num.of_int 66))
(** STMicroelectronics ST9+ 8/16 bit microcontroller *)
let elf_ma_st9plus : Nat_big_num.num= ( (Nat_big_num.of_int 67))
(** STMicroelectronics ST7 8-bit microcontroller *)
let elf_ma_st7 : Nat_big_num.num= ( (Nat_big_num.of_int 68))
(** Motorola MC68HC16 Microcontroller *)
let elf_ma_68hc16 : Nat_big_num.num= ( (Nat_big_num.of_int 69))
(** Motorola MC68HC11 Microcontroller *)
let elf_ma_68hc11 : Nat_big_num.num= ( (Nat_big_num.of_int 70))
(** Motorola MC68HC08 Microcontroller *)
let elf_ma_68hc08 : Nat_big_num.num= ( (Nat_big_num.of_int 71))
(** Motorola MC68HC05 Microcontroller *)
let elf_ma_68hc05 : Nat_big_num.num= ( (Nat_big_num.of_int 72))
(** Silicon Graphics SVx *)
let elf_ma_svx : Nat_big_num.num= ( (Nat_big_num.of_int 73))
(** STMicroelectronics ST19 8-bit microcontroller *)
let elf_ma_st19 : Nat_big_num.num= ( (Nat_big_num.of_int 74))
(** Digital VAX *)
let elf_ma_vax : Nat_big_num.num= ( (Nat_big_num.of_int 75))
(** Axis Communications 32-bit embedded processor *)
let elf_ma_cris : Nat_big_num.num= ( (Nat_big_num.of_int 76))
(** Infineon Technologies 32-bit embedded processor *)
let elf_ma_javelin : Nat_big_num.num= ( (Nat_big_num.of_int 77))
(** Element 14 64-bit DSP Processor *)
let elf_ma_firepath : Nat_big_num.num= ( (Nat_big_num.of_int 78))
(** Reserved by Intel *)
let elf_ma_intel209 : Nat_big_num.num= ( (Nat_big_num.of_int 209))
(** Reserved by Intel *)
let elf_ma_intel208 : Nat_big_num.num= ( (Nat_big_num.of_int 208))
(** Reserved by Intel *)
let elf_ma_intel207 : Nat_big_num.num= ( (Nat_big_num.of_int 207))
(** Reserved by Intel *)
let elf_ma_intel206 : Nat_big_num.num= ( (Nat_big_num.of_int 206))
(** Reserved by Intel *)
let elf_ma_intel205 : Nat_big_num.num= ( (Nat_big_num.of_int 205))
(** Reserved by Intel *)
let elf_ma_intel182 : Nat_big_num.num= ( (Nat_big_num.of_int 182))
(** Reserved by ARM *)
let elf_ma_arm184 : Nat_big_num.num= ( (Nat_big_num.of_int 184))
(** Reserved for future use *)
let elf_ma_reserved6 : Nat_big_num.num= ( (Nat_big_num.of_int 6))
(** Reserved for future use *)
let elf_ma_reserved11 : Nat_big_num.num= ( (Nat_big_num.of_int 11))
(** Reserved for future use *)
let elf_ma_reserved12 : Nat_big_num.num= ( (Nat_big_num.of_int 12))
(** Reserved for future use *)
let elf_ma_reserved13 : Nat_big_num.num= ( (Nat_big_num.of_int 13))
(** Reserved for future use *)
let elf_ma_reserved14 : Nat_big_num.num= ( (Nat_big_num.of_int 14))
(** Reserved for future use *)
let elf_ma_reserved16 : Nat_big_num.num= ( (Nat_big_num.of_int 16))
(** Reserved for future use *)
let elf_ma_reserved24 : Nat_big_num.num= ( (Nat_big_num.of_int 24))
(** Reserved for future use *)
let elf_ma_reserved25 : Nat_big_num.num= ( (Nat_big_num.of_int 25))
(** Reserved for future use *)
let elf_ma_reserved26 : Nat_big_num.num= ( (Nat_big_num.of_int 26))
(** Reserved for future use *)
let elf_ma_reserved27 : Nat_big_num.num= ( (Nat_big_num.of_int 27))
(** Reserved for future use *)
let elf_ma_reserved28 : Nat_big_num.num= ( (Nat_big_num.of_int 28))
(** Reserved for future use *)
let elf_ma_reserved29 : Nat_big_num.num= ( (Nat_big_num.of_int 29))
(** Reserved for future use *)
let elf_ma_reserved30 : Nat_big_num.num= ( (Nat_big_num.of_int 30))
(** Reserved for future use *)
let elf_ma_reserved31 : Nat_big_num.num= ( (Nat_big_num.of_int 31))
(** Reserved for future use *)
let elf_ma_reserved32 : Nat_big_num.num= ( (Nat_big_num.of_int 32))
(** Reserved for future use *)
let elf_ma_reserved33 : Nat_big_num.num= ( (Nat_big_num.of_int 33))
(** Reserved for future use *)
let elf_ma_reserved34 : Nat_big_num.num= ( (Nat_big_num.of_int 34))
(** Reserved for future use *)
let elf_ma_reserved35 : Nat_big_num.num= ( (Nat_big_num.of_int 35))
(** Reserved for future use *)
let elf_ma_reserved121 : Nat_big_num.num= ( (Nat_big_num.of_int 121))
(** Reserved for future use *)
let elf_ma_reserved122 : Nat_big_num.num= ( (Nat_big_num.of_int 122))
(** Reserved for future use *)
let elf_ma_reserved123 : Nat_big_num.num= ( (Nat_big_num.of_int 123))
(** Reserved for future use *)
let elf_ma_reserved124 : Nat_big_num.num= ( (Nat_big_num.of_int 124))
(** Reserved for future use *)
let elf_ma_reserved125 : Nat_big_num.num= ( (Nat_big_num.of_int 125))
(** Reserved for future use *)
let elf_ma_reserved126 : Nat_big_num.num= ( (Nat_big_num.of_int 126))
(** Reserved for future use *)
let elf_ma_reserved127 : Nat_big_num.num= ( (Nat_big_num.of_int 127))
(** Reserved for future use *)
let elf_ma_reserved128 : Nat_big_num.num= ( (Nat_big_num.of_int 128))
(** Reserved for future use *)
let elf_ma_reserved129 : Nat_big_num.num= ( (Nat_big_num.of_int 129))
(** Reserved for future use *)
let elf_ma_reserved130 : Nat_big_num.num= ( (Nat_big_num.of_int 130))
(** Reserved for future use *)
let elf_ma_reserved143 : Nat_big_num.num= ( (Nat_big_num.of_int 143))
(** Reserved for future use *)
let elf_ma_reserved144 : Nat_big_num.num= ( (Nat_big_num.of_int 144))
(** Reserved for future use *)
let elf_ma_reserved145 : Nat_big_num.num= ( (Nat_big_num.of_int 145))
(** Reserved for future use *)
let elf_ma_reserved146 : Nat_big_num.num= ( (Nat_big_num.of_int 146))
(** Reserved for future use *)
let elf_ma_reserved147 : Nat_big_num.num= ( (Nat_big_num.of_int 147))
(** Reserved for future use *)
let elf_ma_reserved148 : Nat_big_num.num= ( (Nat_big_num.of_int 148))
(** Reserved for future use *)
let elf_ma_reserved149 : Nat_big_num.num= ( (Nat_big_num.of_int 149))
(** Reserved for future use *)
let elf_ma_reserved150 : Nat_big_num.num= ( (Nat_big_num.of_int 150))
(** Reserved for future use *)
let elf_ma_reserved151 : Nat_big_num.num= ( (Nat_big_num.of_int 151))
(** Reserved for future use *)
let elf_ma_reserved152 : Nat_big_num.num= ( (Nat_big_num.of_int 152))
(** Reserved for future use *)
let elf_ma_reserved153 : Nat_big_num.num= ( (Nat_big_num.of_int 153))
(** Reserved for future use *)
let elf_ma_reserved154 : Nat_big_num.num= ( (Nat_big_num.of_int 154))
(** Reserved for future use *)
let elf_ma_reserved155 : Nat_big_num.num= ( (Nat_big_num.of_int 155))
(** Reserved for future use *)
let elf_ma_reserved156 : Nat_big_num.num= ( (Nat_big_num.of_int 156))
(** Reserved for future use *)
let elf_ma_reserved157 : Nat_big_num.num= ( (Nat_big_num.of_int 157))
(** Reserved for future use *)
let elf_ma_reserved158 : Nat_big_num.num= ( (Nat_big_num.of_int 158))
(** Reserved for future use *)
let elf_ma_reserved159 : Nat_big_num.num= ( (Nat_big_num.of_int 159))

(** [string_of_elf_machine_architecture m] produces a string representation of
  * the numeric encoding [m] of the ELF machine architecture.
  * TODO: finish this .
  *)
(*val string_of_elf_machine_architecture : natural -> string*)
let string_of_elf_machine_architecture m:string=
	 (if Nat_big_num.equal m elf_ma_386 then
		"Intel 80386"
  else if Nat_big_num.equal m elf_ma_ppc then
    "PowerPC"
  else if Nat_big_num.equal m elf_ma_ppc64 then
    "PowerPC64"
  else if Nat_big_num.equal m elf_ma_arm then
    "AArch"
  else if Nat_big_num.equal m elf_ma_x86_64 then
    "Advanced Micro Devices X86-64"
  else if Nat_big_num.equal m elf_ma_aarch64 then
    "AArch64"
	else
		"Other architecture")

(** ELF version numbers.  Denotes the ELF version number of an ELF file.  Current is
  * defined to have a value of 1 with the present specification.  Extensions
  * may create versions of ELF with higher version numbers.
  *)

(** Invalid version *)
let elf_ev_none : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** Current version *)
let elf_ev_current : Nat_big_num.num= ( (Nat_big_num.of_int 1))

(** [string_of_elf_version_number m] produces a string representation of the
  * numeric encoding [m] of the ELF version number.
  *)
(*val string_of_elf_version_number : natural -> string*)
let string_of_elf_version_number m:string=
	 (if Nat_big_num.equal m elf_ev_none then
		"Invalid ELF version"
	else if Nat_big_num.equal m elf_ev_current then
		"1 (current)"
	else
		"Extended ELF version")

(** Check that an extended version number is correct (i.e. greater than 1). *)
let is_valid_extended_version_number (n : Nat_big_num.num):bool=  (Nat_big_num.greater n( (Nat_big_num.of_int 1)))

(** Identification indices.  The initial bytes of an ELF header (and an object
  * file) correspond to the e_ident member.
  *)

(** File identification *)
let elf_ii_mag0 : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** File identification *)
let elf_ii_mag1 : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** File identification *)
let elf_ii_mag2 : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** File identification *)
let elf_ii_mag3 : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** File class *)
let elf_ii_class : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** Data encoding *)
let elf_ii_data : Nat_big_num.num= ( (Nat_big_num.of_int 5))
(** File version *)
let elf_ii_version : Nat_big_num.num= ( (Nat_big_num.of_int 6))
(** Operating system/ABI identification *)
let elf_ii_osabi : Nat_big_num.num= ( (Nat_big_num.of_int 7))
(** ABI version *)
let elf_ii_abiversion : Nat_big_num.num= ( (Nat_big_num.of_int 8))
(** Start of padding bytes *)
let elf_ii_pad : Nat_big_num.num= ( (Nat_big_num.of_int 9))
(** Size of e*_ident[] *)
let elf_ii_nident : Nat_big_num.num= ( (Nat_big_num.of_int 16))

(** Magic number indices.  A file's first 4 bytes hold a ``magic number,''
  * identifying the file as an ELF object file.
  *)

(** Position: e*_ident[elf_ii_mag0], 0x7f magic number *)
let elf_mn_mag0 : Uint32_wrapper.uint32=  (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 127)))
(** Position: e*_ident[elf_ii_mag1], 'E' format identifier *)
let elf_mn_mag1 : Uint32_wrapper.uint32=  (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 69)))
(** Position: e*_ident[elf_ii_mag2], 'L' format identifier *)
let elf_mn_mag2 : Uint32_wrapper.uint32=  (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 76)))
(** Position: e*_ident[elf_ii_mag3], 'F' format identifier *)
let elf_mn_mag3 : Uint32_wrapper.uint32=  (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 70)))

(** ELf file classes.  The file format is designed to be portable among machines
  * of various sizes, without imposing the sizes of the largest machine on the
  * smallest. The class of the file defines the basic types used by the data
  * structures of the object file container itself.
  *)

(** Invalid class *)
let elf_class_none : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** 32 bit objects *)
let elf_class_32 : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** 64 bit objects *)
let elf_class_64 : Nat_big_num.num= ( (Nat_big_num.of_int 2))

(** [string_of_elf_file_class m] produces a string representation of the numeric
  * encoding [m] of the ELF file class.
  *)
(*val string_of_elf_file_class : natural -> string*)
let string_of_elf_file_class m:string=
	 (if Nat_big_num.equal m elf_class_none then
		"Invalid ELF file class"
	else if Nat_big_num.equal m elf_class_32 then
		"ELF32"
	else if Nat_big_num.equal m elf_class_64 then
		"ELF64"
	else
		"Invalid ELF file class")

(** ELF data encodings.  Byte e_ident[elf_ei_data] specifies the encoding of both the
  * data structures used by object file container and data contained in object
  * file sections.
  *)

(** Invalid data encoding *)
let elf_data_none : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** Two's complement values, least significant byte occupying lowest address *)
let elf_data_2lsb : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** Two's complement values, most significant byte occupying lowest address *)
let elf_data_2msb : Nat_big_num.num= ( (Nat_big_num.of_int 2))

(** [string_of_elf_data_encoding m] produces a string representation of the
  * numeric encoding [m] of the ELF data encoding.
  *)
(*val string_of_elf_data_encoding : natural -> string*)
let string_of_elf_data_encoding m:string=
	 (if Nat_big_num.equal m elf_data_none then
		"Invalid data encoding"
	else if Nat_big_num.equal m elf_data_2lsb then
		"2's complement, little endian"
	else if Nat_big_num.equal m elf_data_2msb then
		"2's complement, big endian"
	else
		"Invalid data encoding")

(** OS and ABI versions.  Byte e_ident[elf_ei_osabi] identifies the OS- or
  * ABI-specific ELF extensions used by this file. Some fields in other ELF
  * structures have flags and values that have operating system and/or ABI
  * specific meanings; the interpretation of those fields is determined by the
  * value of this byte.
  *)

(** No extensions or unspecified *)
let elf_osabi_none : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** Hewlett-Packard HP-UX *)
let elf_osabi_hpux : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** NetBSD *)
let elf_osabi_netbsd : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** GNU *)
let elf_osabi_gnu : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** Linux, historical alias for GNU *)
let elf_osabi_linux : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** Sun Solaris *)
let elf_osabi_solaris : Nat_big_num.num= ( (Nat_big_num.of_int 6))
(** AIX *)
let elf_osabi_aix : Nat_big_num.num= ( (Nat_big_num.of_int 7))
(** IRIX *)
let elf_osabi_irix : Nat_big_num.num= ( (Nat_big_num.of_int 8))
(** FreeBSD *)
let elf_osabi_freebsd : Nat_big_num.num= ( (Nat_big_num.of_int 9))
(** Compaq Tru64 Unix *)
let elf_osabi_tru64 : Nat_big_num.num= ( (Nat_big_num.of_int 10))
(** Novell Modesto *)
let elf_osabi_modesto : Nat_big_num.num= ( (Nat_big_num.of_int 11))
(** OpenBSD *)
let elf_osabi_openbsd : Nat_big_num.num= ( (Nat_big_num.of_int 12))
(** OpenVMS *)
let elf_osabi_openvms : Nat_big_num.num= ( (Nat_big_num.of_int 13))
(** Hewlett-Packard Non-stop Kernel *)
let elf_osabi_nsk : Nat_big_num.num= ( (Nat_big_num.of_int 14))
(** Amiga Research OS *)
let elf_osabi_aros : Nat_big_num.num= ( (Nat_big_num.of_int 15))
(** FenixOS highly-scalable multi-core OS *)
let elf_osabi_fenixos : Nat_big_num.num= ( (Nat_big_num.of_int 16))
(** Nuxi CloudABI *)
let elf_osabi_cloudabi : Nat_big_num.num= ( (Nat_big_num.of_int 17))
(** Stratus technologies OpenVOS *)
let elf_osabi_openvos : Nat_big_num.num= ( (Nat_big_num.of_int 18))

(** Checks an architecture defined OSABI version is correct, i.e. in the range
  * 64 to 255 inclusive.
  *)
let is_valid_architecture_defined_osabi_version (n : Nat_big_num.num):bool=  (Nat_big_num.greater_equal
  n( (Nat_big_num.of_int 64)) && Nat_big_num.less_equal n( (Nat_big_num.of_int 255)))

(** [string_of_elf_osabi_version m] produces a string representation of the
  * numeric encoding [m] of the ELF OSABI version.
  *)
(*val string_of_elf_osabi_version : (natural -> string) -> natural -> string*)
let string_of_elf_osabi_version arch m:string=
	 (if Nat_big_num.equal m elf_osabi_none then
		"UNIX - System V"
	else if Nat_big_num.equal m elf_osabi_netbsd then
		"Hewlett-Packard HP-UX"
	else if Nat_big_num.equal m elf_osabi_netbsd then
		"NetBSD"
	else if Nat_big_num.equal m elf_osabi_gnu then
		"UNIX - GNU"
	else if Nat_big_num.equal m elf_osabi_linux then
		"Linux"
	else if Nat_big_num.equal m elf_osabi_solaris then
		"Sun Solaris"
	else if Nat_big_num.equal m elf_osabi_aix then
		"AIX"
	else if Nat_big_num.equal m elf_osabi_irix then
		"IRIX"
	else if Nat_big_num.equal m elf_osabi_freebsd then
		"FreeBSD"
	else if Nat_big_num.equal m elf_osabi_tru64 then
		"Compaq Tru64 Unix"
	else if Nat_big_num.equal m elf_osabi_modesto then
		"Novell Modesto"
	else if Nat_big_num.equal m elf_osabi_openbsd then
		"OpenBSD"
	else if Nat_big_num.equal m elf_osabi_openvms then
		"OpenVMS"
	else if Nat_big_num.equal m elf_osabi_nsk then
		"Hewlett-Packard Non-stop Kernel"
	else if Nat_big_num.equal m elf_osabi_aros then
		"Amiga Research OS"
	else if Nat_big_num.equal m elf_osabi_fenixos then
		"FenixOS highly-scalable multi-core OS"
  else if Nat_big_num.equal m elf_osabi_cloudabi then
    "Nuxi CloudABI"
  else if Nat_big_num.equal m elf_osabi_openvos then
    "Stratus technologies OpenVOS"
	else if is_valid_architecture_defined_osabi_version m then
	  arch m
	else
		"Invalid OSABI version")

(** ELF Header type *)

(** [ei_nident] is the fixed length of the identification field in the
  * [elf32_ehdr] type.
  *)
(*val ei_nident : natural*)
let ei_nident:Nat_big_num.num= ( (Nat_big_num.of_int 16))

(** [elf32_header] is the type of headers for 32-bit ELF files.
  *)
type elf32_header =
  { elf32_ident    : Uint32_wrapper.uint32 list (** Identification field *)
   ; elf32_type     : Uint32_wrapper.uint32         (** The object file type *)
   ; elf32_machine  : Uint32_wrapper.uint32         (** Required machine architecture *)
   ; elf32_version  : Uint32_wrapper.uint32         (** Object file version *)
   ; elf32_entry    : Uint32_wrapper.uint32         (** Virtual address for transfer of control *)
   ; elf32_phoff    : Uint32_wrapper.uint32          (** Program header table offset in bytes *)
   ; elf32_shoff    : Uint32_wrapper.uint32          (** Section header table offset in bytes *)
   ; elf32_flags    : Uint32_wrapper.uint32         (** Processor-specific flags *)
   ; elf32_ehsize   : Uint32_wrapper.uint32         (** ELF header size in bytes *)
   ; elf32_phentsize: Uint32_wrapper.uint32         (** Program header table entry size in bytes *)
   ; elf32_phnum    : Uint32_wrapper.uint32         (** Number of entries in program header table *)
   ; elf32_shentsize: Uint32_wrapper.uint32         (** Section header table entry size in bytes *)
   ; elf32_shnum    : Uint32_wrapper.uint32         (** Number of entries in section header table *)
   ; elf32_shstrndx : Uint32_wrapper.uint32         (** Section header table entry for section name string table *)
   }
   
(** [elf64_header] is the type of headers for 64-bit ELF files.
  *)
type elf64_header =
  { elf64_ident    : Uint32_wrapper.uint32 list (** Identification field *)
   ; elf64_type     : Uint32_wrapper.uint32         (** The object file type *)
   ; elf64_machine  : Uint32_wrapper.uint32         (** Required machine architecture *)
   ; elf64_version  : Uint32_wrapper.uint32         (** Object file version *)
   ; elf64_entry    : Uint64_wrapper.uint64         (** Virtual address for transfer of control *)
   ; elf64_phoff    : Uint64_wrapper.uint64          (** Program header table offset in bytes *)
   ; elf64_shoff    : Uint64_wrapper.uint64          (** Section header table offset in bytes *)
   ; elf64_flags    : Uint32_wrapper.uint32         (** Processor-specific flags *)
   ; elf64_ehsize   : Uint32_wrapper.uint32         (** ELF header size in bytes *)
   ; elf64_phentsize: Uint32_wrapper.uint32         (** Program header table entry size in bytes *)
   ; elf64_phnum    : Uint32_wrapper.uint32         (** Number of entries in program header table *)
   ; elf64_shentsize: Uint32_wrapper.uint32         (** Section header table entry size in bytes *)
   ; elf64_shnum    : Uint32_wrapper.uint32         (** Number of entries in section header table *)
   ; elf64_shstrndx : Uint32_wrapper.uint32         (** Section header table entry for section name string table *)
   }
   
(** [is_valid_elf32_header hdr] checks whether header [hdr] is valid, i.e. has
  * the correct magic numbers.
  * TODO: this should be expanded, presumably, or merged with some of the other
  * checks.
  *)
(*val is_valid_elf32_header : elf32_header -> bool*)
let is_valid_elf32_header hdr:bool=  (listEqualBy (=)
  (Lem_list.take 4 hdr.elf32_ident) [elf_mn_mag0; elf_mn_mag1; elf_mn_mag2; elf_mn_mag3])
  
(** [is_valid_elf64_header hdr] checks whether header [hdr] is valid, i.e. has
  * the correct magic numbers.
  * TODO: this should be expanded, presumably, or merged with some of the other
  * checks.
  *)
(*val is_valid_elf64_header : elf64_header -> bool*)
let is_valid_elf64_header hdr:bool=  (listEqualBy (=)
  (Lem_list.take 4 hdr.elf64_ident) [elf_mn_mag0; elf_mn_mag1; elf_mn_mag2; elf_mn_mag3])

(** [elf32_header_compare hdr1 hdr2] is an ordering comparison function for
  * ELF headers suitable for use in sets, finite maps and other ordered
  * data types.
  *)
(*val elf32_header_compare : elf32_header -> elf32_header -> Basic_classes.ordering*)
let elf32_header_compare h1 h2:int= 
     (pairCompare (lexicographic_compare Nat_big_num.compare) (lexicographic_compare Nat_big_num.compare) (Lem_list.map Uint32_wrapper.to_bigint h1.elf32_ident, [Uint32_wrapper.to_bigint h1.elf32_type; 
            Uint32_wrapper.to_bigint h1.elf32_machine ; Uint32_wrapper.to_bigint h1.elf32_version ; 
            Uint32_wrapper.to_bigint h1.elf32_entry ; Uint32_wrapper.to_bigint h1.elf32_phoff ; Uint32_wrapper.to_bigint h1.elf32_shoff ; 
            Uint32_wrapper.to_bigint h1.elf32_flags ; Uint32_wrapper.to_bigint h1.elf32_ehsize ; 
            Uint32_wrapper.to_bigint h1.elf32_phentsize; Uint32_wrapper.to_bigint h1.elf32_phnum ; 
            Uint32_wrapper.to_bigint h1.elf32_shentsize; Uint32_wrapper.to_bigint h1.elf32_shnum ; 
            Uint32_wrapper.to_bigint h1.elf32_shstrndx])
     (Lem_list.map Uint32_wrapper.to_bigint h2.elf32_ident, [Uint32_wrapper.to_bigint h2.elf32_type; 
            Uint32_wrapper.to_bigint h2.elf32_machine ; Uint32_wrapper.to_bigint h2.elf32_version ; 
            Uint32_wrapper.to_bigint h2.elf32_entry ; Uint32_wrapper.to_bigint h2.elf32_phoff ; Uint32_wrapper.to_bigint h2.elf32_shoff ; 
            Uint32_wrapper.to_bigint h2.elf32_flags ; Uint32_wrapper.to_bigint h2.elf32_ehsize ; 
            Uint32_wrapper.to_bigint h2.elf32_phentsize; Uint32_wrapper.to_bigint h2.elf32_phnum ; 
            Uint32_wrapper.to_bigint h2.elf32_shentsize; Uint32_wrapper.to_bigint h2.elf32_shnum ; 
            Uint32_wrapper.to_bigint h2.elf32_shstrndx]))

let instance_Basic_classes_Ord_Elf_header_elf32_header_dict:(elf32_header)ord_class= ({

  compare_method = elf32_header_compare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_header_compare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_header_compare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_header_compare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_header_compare f1 f2)(Pset.from_list compare [1; 0])))})

(** [elf64_header_compare hdr1 hdr2] is an ordering comparison function for
  * ELF headers suitable for use in sets, finite maps and other ordered
  * data types.
  *)
(*val elf64_header_compare : elf64_header -> elf64_header -> Basic_classes.ordering*)
let elf64_header_compare h1 h2:int= 
     (pairCompare (lexicographic_compare Nat_big_num.compare) (lexicographic_compare Nat_big_num.compare) (Lem_list.map Uint32_wrapper.to_bigint h1.elf64_ident, [Uint32_wrapper.to_bigint h1.elf64_type; 
            Uint32_wrapper.to_bigint h1.elf64_machine ; Uint32_wrapper.to_bigint h1.elf64_version ; 
            Ml_bindings.nat_big_num_of_uint64 h1.elf64_entry ; Uint64_wrapper.to_bigint h1.elf64_phoff ; Uint64_wrapper.to_bigint h1.elf64_shoff ; 
            Uint32_wrapper.to_bigint h1.elf64_flags ; Uint32_wrapper.to_bigint h1.elf64_ehsize ; 
            Uint32_wrapper.to_bigint h1.elf64_phentsize; Uint32_wrapper.to_bigint h1.elf64_phnum ; 
            Uint32_wrapper.to_bigint h1.elf64_shentsize; Uint32_wrapper.to_bigint h1.elf64_shnum ; 
            Uint32_wrapper.to_bigint h1.elf64_shstrndx])
     (Lem_list.map Uint32_wrapper.to_bigint h2.elf64_ident, [Uint32_wrapper.to_bigint h2.elf64_type; 
            Uint32_wrapper.to_bigint h2.elf64_machine ; Uint32_wrapper.to_bigint h2.elf64_version ; 
            Ml_bindings.nat_big_num_of_uint64 h2.elf64_entry ; Uint64_wrapper.to_bigint h2.elf64_phoff ; Uint64_wrapper.to_bigint h2.elf64_shoff ; 
            Uint32_wrapper.to_bigint h2.elf64_flags ; Uint32_wrapper.to_bigint h2.elf64_ehsize ; 
            Uint32_wrapper.to_bigint h2.elf64_phentsize; Uint32_wrapper.to_bigint h2.elf64_phnum ; 
            Uint32_wrapper.to_bigint h2.elf64_shentsize; Uint32_wrapper.to_bigint h2.elf64_shnum ; 
            Uint32_wrapper.to_bigint h2.elf64_shstrndx]))

let instance_Basic_classes_Ord_Elf_header_elf64_header_dict:(elf64_header)ord_class= ({

  compare_method = elf64_header_compare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_header_compare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_header_compare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_header_compare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_header_compare f1 f2)(Pset.from_list compare [1; 0])))})

(** [is_elf32_executable_file hdr] checks whether the header [hdr] states if the
  * ELF file is of executable type.
  *)
(*val is_elf32_executable_file : elf32_header -> bool*)
let is_elf32_executable_file hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf32_type) elf_ft_exec)

(** [is_elf64_executable_file hdr] checks whether the header [hdr] states if the
  * ELF file is of executable type.
  *)
(*val is_elf64_executable_file : elf64_header -> bool*)
let is_elf64_executable_file hdr:bool=
  (* hack *)  true (*natural_of_elf64_half hdr.elf64_type = elf_ft_exec*)

(** [is_elf32_shared_object_file hdr] checks whether the header [hdr] states if the
  * ELF file is of shared object type.
  *)
(*val is_elf32_shared_object_file : elf32_header -> bool*)
let is_elf32_shared_object_file hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf32_type) elf_ft_dyn)

(** [is_elf64_shared_object_file hdr] checks whether the header [hdr] states if the
  * ELF file is of shared object type.
  *)
(*val is_elf64_shared_object_file : elf64_header -> bool*)
let is_elf64_shared_object_file hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf64_type) elf_ft_dyn)

(** [is_elf32_relocatable_file hdr] checks whether the header [hdr] states if the
  * ELF file is of relocatable type.
  *)
(*val is_elf32_relocatable_file : elf32_header -> bool*)
let is_elf32_relocatable_file hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf32_type) elf_ft_rel)

(** [is_elf64_relocatable_file hdr] checks whether the header [hdr] states if the
  * ELF file is of relocatable type.
  *)
(*val is_elf64_relocatable_file : elf64_header -> bool*)
let is_elf64_relocatable_file hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf64_type) elf_ft_rel)

(** [is_elf32_linkable_file hdr] checks whether the header [hdr] states if the
  * ELF file is of linkable (shared object or relocatable) type.
  *)
(*val is_elf32_linkable_file : elf32_header -> bool*)
let is_elf32_linkable_file hdr:bool=
   (is_elf32_shared_object_file hdr || is_elf32_relocatable_file hdr)

(** [is_elf64_linkable_file hdr] checks whether the header [hdr] states if the
  * ELF file is of linkable (shared object or relocatable) type.
  *)
(*val is_elf64_linkable_file : elf64_header -> bool*)
let is_elf64_linkable_file hdr:bool=
   (is_elf64_shared_object_file hdr || is_elf64_relocatable_file hdr)

(** [get_elf32_machine_architecture hdr] returns the ELF file's declared machine
  * architecture, extracting the information from header [hdr].
  *)
(*val get_elf32_machine_architecture : elf32_header -> natural*)
let get_elf32_machine_architecture hdr:Nat_big_num.num=
   (Uint32_wrapper.to_bigint hdr.elf32_machine)

(** [get_elf64_machine_architecture hdr] returns the ELF file's declared machine
  * architecture, extracting the information from header [hdr].
  *)
(*val get_elf64_machine_architecture : elf64_header -> natural*)
let get_elf64_machine_architecture hdr:Nat_big_num.num=
   (Uint32_wrapper.to_bigint hdr.elf64_machine)

(** [get_elf32_osabi hdr] returns the ELF file's declared OS/ABI
  * architecture, extracting the information from header [hdr].
  *)
(*val get_elf32_osabi : elf32_header -> natural*)
let get_elf32_osabi hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_osabi) with
    | Some osabi -> Uint32_wrapper.to_bigint osabi
    | None    -> failwith "get_elf32_osabi: lookup in ident failed"
  )) (* Partial: should never return Nothing *)

(** [get_elf64_osabi hdr] returns the ELF file's declared OS/ABI
  * architecture, extracting the information from header [hdr].
  *)
(*val get_elf64_osabi : elf64_header -> natural*)
let get_elf64_osabi hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_osabi) with
    | Some osabi -> Uint32_wrapper.to_bigint osabi
    | None    -> failwith "get_elf64_osabi: lookup in ident failed"
  )) (* Partial: should never return Nothing *)
  
(** [get_elf32_data_encoding hdr] returns the ELF file's declared data
  * encoding, extracting the information from header [hdr].
  *)
(*val get_elf32_data_encoding : elf32_header -> natural*)
let get_elf32_data_encoding hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_data) with
    | Some data -> Uint32_wrapper.to_bigint data
    | None    -> failwith "get_elf32_data_encoding: lookup in ident failed"
  )) (* Partial: should never return Nothing *)

(** [get_elf64_data_encoding hdr] returns the ELF file's declared data
  * encoding, extracting the information from header [hdr].
  *)
(*val get_elf64_data_encoding : elf64_header -> natural*)
let get_elf64_data_encoding hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_data) with
    | Some data -> Uint32_wrapper.to_bigint data
    | None    -> failwith "get_elf64_data_encoding: lookup in ident failed"
  )) (* Partial: should never return Nothing *)
  
(** [get_elf32_file_class hdr] returns the ELF file's declared file
  * class, extracting the information from header [hdr].
  *)
(*val get_elf32_file_class : elf32_header -> natural*)
let get_elf32_file_class hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_class) with
    | Some cls -> Uint32_wrapper.to_bigint cls
    | None    -> failwith "get_elf32_file_class: lookup in ident failed"
  )) (* Partial: should never return Nothing *)

(** [get_elf64_file_class hdr] returns the ELF file's declared file
  * class, extracting the information from header [hdr].
  *)
(*val get_elf64_file_class : elf64_header -> natural*)
let get_elf64_file_class hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_class) with
    | Some cls -> Uint32_wrapper.to_bigint cls
    | None    -> failwith "get_elf64_file_class: lookup in ident failed"
  )) (* Partial: should never return Nothing *)

(** [get_elf32_version_number hdr] returns the ELF file's declared version
  * number, extracting the information from header [hdr].
  *)
(*val get_elf32_version_number : elf32_header -> natural*)
let get_elf32_version_number hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_version) with
    | Some ver -> Uint32_wrapper.to_bigint ver
    | None    -> failwith "get_elf32_version_number: lookup in ident failed"
  )) (* Partial: should never return Nothing *)

(** [get_elf64_version_number hdr] returns the ELF file's declared version
  * number, extracting the information from header [hdr].
  *)
(*val get_elf64_version_number : elf64_header -> natural*)
let get_elf64_version_number hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_version) with
    | Some ver -> Uint32_wrapper.to_bigint ver
    | None    -> failwith "get_elf64_version_number: lookup in ident failed"
  )) (* Partial: should never return Nothing *)
  
(** [is_valid_elf32_version_number hdr] checks whether an ELF file's declared
  * version number matches the current, mandatory version number.
  * TODO: this should be merged into [is_valid_elf32_header] to create a single
  * correctness check.
  *)
(*val is_valid_elf32_version_number : elf32_header -> bool*)
let is_valid_elf32_version_numer hdr:bool=  (Nat_big_num.equal
  (get_elf32_version_number hdr) elf_ev_current)

(** [is_valid_elf64_version_number hdr] checks whether an ELF file's declared
  * version number matches the current, mandatory version number.
  * TODO: this should be merged into [is_valid_elf64_header] to create a single
  * correctness check.
  *)
(*val is_valid_elf64_version_number : elf64_header -> bool*)
let is_valid_elf64_version_numer hdr:bool=  (Nat_big_num.equal
  (get_elf64_version_number hdr) elf_ev_current)
  
(** [get_elf32_abi_version hdr] returns the ELF file's declared ABI version
  * number, extracting the information from header [hdr].
  *)
(*val get_elf32_abi_version : elf32_header -> natural*)
let get_elf32_abi_version hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf32_ident (Nat_big_num.to_int elf_ii_abiversion) with
    | Some ver -> Uint32_wrapper.to_bigint ver
    | None    -> failwith "get_elf32_abi_version: lookup in ident failed"
  )) (* Partial: should never return Nothing *)

(** [get_elf64_abi_version hdr] returns the ELF file's declared ABI version
  * number, extracting the information from header [hdr].
  *)
(*val get_elf64_abi_version : elf64_header -> natural*)
let get_elf64_abi_version hdr:Nat_big_num.num=
   ((match Lem_list.list_index hdr.elf64_ident (Nat_big_num.to_int elf_ii_abiversion) with
    | Some ver -> Uint32_wrapper.to_bigint ver
    | None    -> failwith "get_elf64_abi_version: lookup in ident failed"
  )) (* Partial: should never return Nothing *)
  
(** [deduce_endianness uc] deduces the endianness of an ELF file based on the ELF
  * header's magic number [uc].
  *)
(*val deduce_endianness : list unsigned_char -> endianness*)
let deduce_endianness id2:endianness=
   ((match Lem_list.list_index id2 5 with
    | None -> failwith "deduce_endianness: read of magic number has failed"
    | Some v  ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint v) elf_data_2lsb then
        Little
      else if Nat_big_num.equal (Uint32_wrapper.to_bigint v) elf_data_2msb then
        Big
      else
        failwith "deduce_endianness: value is not valid"
  ))

(** [get_elf32_header_endianness hdr] returns the endianness of the ELF file
  * as declared in its header, [hdr].
  *)
(*val get_elf32_header_endianness : elf32_header -> endianness*)
let get_elf32_header_endianness hdr:endianness=
   (deduce_endianness (hdr.elf32_ident))

(** [get_elf64_header_endianness hdr] returns the endianness of the ELF file
  * as declared in its header, [hdr].
  *)
(*val get_elf64_header_endianness : elf64_header -> endianness*)
let get_elf64_header_endianness hdr:endianness=
   (deduce_endianness (hdr.elf64_ident))
  
(** [has_elf32_header_associated_entry_point hdr] checks whether the header
  * [hdr] declares an entry point for the program.
  *)
(*val has_elf32_header_associated_entry_point : elf32_header -> bool*)
let has_elf32_header_associated_entry_point hdr:bool=  (not (Nat_big_num.equal (Uint32_wrapper.to_bigint hdr.elf32_entry)( (Nat_big_num.of_int 0))))

(** [has_elf64_header_associated_entry_point hdr] checks whether the header
  * [hdr] declares an entry point for the program.
  *)
(*val has_elf64_header_associated_entry_point : elf64_header -> bool*)
let has_elf64_header_associated_entry_point hdr:bool=  (not (Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_entry)( (Nat_big_num.of_int 0))))
  
(** [has_elf32_header_string_table hdr] checks whether the header
  * [hdr] declares whether the program has a string table or not.
  *)
(*val has_elf32_header_string_table : elf32_header -> bool*)
let has_elf32_header_string_table hdr:bool=  (not (Nat_big_num.equal (Uint32_wrapper.to_bigint hdr.elf32_shstrndx) shn_undef))
  
(** [has_elf64_header_string_table hdr] checks whether the header
  * [hdr] declares whether the program has a string table or not.
  *)
(*val has_elf64_header_string_table : elf64_header -> bool*)
let has_elf64_header_string_table hdr:bool=  (not (Nat_big_num.equal (Uint32_wrapper.to_bigint hdr.elf64_shstrndx) shn_undef))
  
(** [is_elf32_header_section_size_in_section_header_table hdr] checks whether the header
  * [hdr] declares whether the section size is too large to fit in the header
  * field and is instead stored in the section header table.
  *)
(*val is_elf32_header_section_size_in_section_header_table : elf32_header -> bool*)
let is_elf32_header_section_size_in_section_header_table hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf32_shnum)( (Nat_big_num.of_int 0)))
  
(** [is_elf64_header_section_size_in_section_header_table hdr] checks whether the header
  * [hdr] declares whether the section size is too large to fit in the header
  * field and is instead stored in the section header table.
  *)
(*val is_elf64_header_section_size_in_section_header_table : elf64_header -> bool*)
let is_elf64_header_section_size_in_section_header_table hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf64_shnum)( (Nat_big_num.of_int 0)))
  
(** [is_elf32_header_string_table_index_in_link hdr] checks whether the header
  * [hdr] declares whether the string table index is too large to fit in the
  * header's field and is instead stored in the link field of an entry in the
  * section header table.
  *)
(*val is_elf32_header_string_table_index_in_link : elf32_header -> bool*)
let is_elf32_header_string_table_index_in_link hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf32_shstrndx) shn_xindex)
  
(** [is_elf64_header_string_table_index_in_link hdr] checks whether the header
  * [hdr] declares whether the string table index is too large to fit in the
  * header's field and is instead stored in the link field of an entry in the
  * section header table.
  *)
(*val is_elf64_header_string_table_index_in_link : elf64_header -> bool*)
let is_elf64_header_string_table_index_in_link hdr:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint hdr.elf64_shstrndx) shn_xindex)

(** The [hdr_print_bundle] type is used to tidy up other type signatures.  Some of the
  * top-level string_of_ functions require six or more functions passed to them,
  * which quickly gets out of hand.  This type is used to reduce that complexity.
  * The first component of the type is an OS specific print function, the second is
  * a processor specific print function.
  *)
type hdr_print_bundle = (Nat_big_num.num -> string) * (Nat_big_num.num -> string)

(** [string_of_elf32_header hdr_bdl hdr] returns a string-based representation
  * of header [hdr] using the ABI-specific print bundle [hdr_bdl].
  *)
(*val string_of_elf32_header : hdr_print_bundle -> elf32_header -> string*)
let string_of_elf32_header (os, proc) hdr:string=
	 (unlines [
	  ("\t" ^ ("Magic number: " ^ string_of_list 
  instance_Show_Show_Elf_types_native_uint_unsigned_char_dict hdr.elf32_ident))
  ; ("\t" ^ ("Endianness: " ^ string_of_endianness (deduce_endianness hdr.elf32_ident)))
	; ("\t" ^ ("Type: " ^ string_of_elf_file_type os proc (Uint32_wrapper.to_bigint hdr.elf32_type)))
  ; ("\t" ^ ("Version: " ^ string_of_elf_version_number (Uint32_wrapper.to_bigint hdr.elf32_version)))
	; ("\t" ^ ("Machine: " ^ string_of_elf_machine_architecture (Uint32_wrapper.to_bigint hdr.elf32_machine)))
  ; ("\t" ^ ("Entry point: " ^ Uint32_wrapper.to_string hdr.elf32_entry))
  ; ("\t" ^ ("Flags: " ^ Uint32_wrapper.to_string hdr.elf32_flags))
  ; ("\t" ^ ("Entries in program header table: " ^ Uint32_wrapper.to_string hdr.elf32_phnum))
  ; ("\t" ^ ("Entries in section header table: " ^ Uint32_wrapper.to_string hdr.elf32_shnum))
	])

(** [string_of_elf64_header hdr_bdl hdr] returns a string-based representation
  * of header [hdr] using the ABI-specific print bundle [hdr_bdl].
  *)
(*val string_of_elf64_header : hdr_print_bundle -> elf64_header -> string*)
let string_of_elf64_header (os, proc) hdr:string=
   (unlines [
    ("\t" ^ ("Magic number: " ^ string_of_list 
  instance_Show_Show_Elf_types_native_uint_unsigned_char_dict hdr.elf64_ident))
  ; ("\t" ^ ("Endianness: " ^ string_of_endianness (deduce_endianness hdr.elf64_ident)))
  ; ("\t" ^ ("Type: " ^ string_of_elf_file_type os proc (Uint32_wrapper.to_bigint hdr.elf64_type)))
  ; ("\t" ^ ("Version: " ^ string_of_elf_version_number (Uint32_wrapper.to_bigint hdr.elf64_version)))
  ; ("\t" ^ ("Machine: " ^ string_of_elf_machine_architecture (Uint32_wrapper.to_bigint hdr.elf64_machine)))
  ; ("\t" ^ ("Entry point: " ^ Uint64_wrapper.to_string hdr.elf64_entry))
  ; ("\t" ^ ("Flags: " ^ Uint32_wrapper.to_string hdr.elf64_flags))
  ; ("\t" ^ ("Entries in program header table: " ^ Uint32_wrapper.to_string hdr.elf64_phnum))
  ; ("\t" ^ ("Entries in section header table: " ^ Uint32_wrapper.to_string hdr.elf64_shnum))
  ])

(** The following are thin wrappers around the pretty-printing functions above
  * using a default print bundle for the header.
  *)
  
(*val string_of_elf32_header_default : elf32_header -> string*)
let string_of_elf32_header_default:elf32_header ->string=
	 (string_of_elf32_header
    (default_os_specific_print,
      default_proc_specific_print))

(*val string_of_elf64_header_default : elf64_header -> string*)
let string_of_elf64_header_default:elf64_header ->string=
   (string_of_elf64_header
    (default_os_specific_print,
      default_proc_specific_print))
	
let instance_Show_Show_Elf_header_elf32_header_dict:(elf32_header)show_class= ({

  show_method = string_of_elf32_header_default})

let instance_Show_Show_Elf_header_elf64_header_dict:(elf64_header)show_class= ({

  show_method = string_of_elf64_header_default})

(** [read_elf_ident bs0] reads the initial bytes of an ELF file from byte sequence
  * [bs0], returning the remainder of the byte sequence too.
  * Fails if transcription fails.
  *)
(*val read_elf_ident : byte_sequence -> error (list unsigned_char * byte_sequence)*)
let read_elf_ident bs:((Uint32_wrapper.uint32)list*Byte_sequence_wrapper.byte_sequence)error= 
 (repeatM' ei_nident bs (read_unsigned_char default_endianness))

(** [bytes_of_elf32_header hdr] blits an ELF header [hdr] to a byte sequence,
  * ready for transcription to a binary file.
  *)
(*val bytes_of_elf32_header : elf32_header -> byte_sequence*)
let bytes_of_elf32_header hdr:Byte_sequence_wrapper.byte_sequence=
   (let endian = (deduce_endianness hdr.elf32_ident) in
    Byte_sequence.from_byte_lists [
      Lem_list.map (fun u->Char.chr (Uint32_wrapper.to_int u)) hdr.elf32_ident
    ; bytes_of_elf32_half endian hdr.elf32_type
    ; bytes_of_elf32_half endian hdr.elf32_machine
    ; bytes_of_elf32_word endian hdr.elf32_version
    ; bytes_of_elf32_addr endian hdr.elf32_entry
    ; bytes_of_elf32_off  endian hdr.elf32_phoff
    ; bytes_of_elf32_off  endian hdr.elf32_shoff
    ; bytes_of_elf32_word endian hdr.elf32_flags
    ; bytes_of_elf32_half endian hdr.elf32_ehsize
    ; bytes_of_elf32_half endian hdr.elf32_phentsize
    ; bytes_of_elf32_half endian hdr.elf32_phnum
    ; bytes_of_elf32_half endian hdr.elf32_shentsize
    ; bytes_of_elf32_half endian hdr.elf32_shnum
    ; bytes_of_elf32_half endian hdr.elf32_shstrndx
    ])
    
(** [bytes_of_elf64_header hdr] blits an ELF header [hdr] to a byte sequence,
  * ready for transcription to a binary file.
  *)
(*val bytes_of_elf64_header : elf64_header -> byte_sequence*)
let bytes_of_elf64_header hdr:Byte_sequence_wrapper.byte_sequence=
   (let endian = (deduce_endianness hdr.elf64_ident) in
    Byte_sequence.from_byte_lists [
      Lem_list.map (fun u->Char.chr (Uint32_wrapper.to_int u)) hdr.elf64_ident
    ; bytes_of_elf64_half endian hdr.elf64_type
    ; bytes_of_elf64_half endian hdr.elf64_machine
    ; bytes_of_elf64_word endian hdr.elf64_version
    ; bytes_of_elf64_addr endian hdr.elf64_entry
    ; bytes_of_elf64_off  endian hdr.elf64_phoff
    ; bytes_of_elf64_off  endian hdr.elf64_shoff
    ; bytes_of_elf64_word endian hdr.elf64_flags
    ; bytes_of_elf64_half endian hdr.elf64_ehsize
    ; bytes_of_elf64_half endian hdr.elf64_phentsize
    ; bytes_of_elf64_half endian hdr.elf64_phnum
    ; bytes_of_elf64_half endian hdr.elf64_shentsize
    ; bytes_of_elf64_half endian hdr.elf64_shnum
    ; bytes_of_elf64_half endian hdr.elf64_shstrndx
    ])
    
(*val is_elf32_header_padding_correct : elf32_header -> bool*)
let is_elf32_header_padding_correct ehdr:bool=   ((Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 9) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 10) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 11) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 12) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 13) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) && ((Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 14) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) && (Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 15) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))))))))))

(*val is_magic_number_correct : list unsigned_char -> bool*)
let is_magic_number_correct ident:bool=  ((Lem.option_equal (=)
  (Lem_list.list_index ident 0) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 127))))) && ((Lem.option_equal (=)
  (Lem_list.list_index ident 1) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 69)))))  && ((Lem.option_equal (=)
  (Lem_list.list_index ident 2) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 76)))))  && (Lem.option_equal (=)
  (Lem_list.list_index ident 3) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 70))))))))

(** [read_elf32_header bs0] reads an ELF header from the byte sequence [bs0].
  * Fails if transcription fails.
  *)
(*val read_elf32_header : byte_sequence -> error (elf32_header * byte_sequence)*)
let read_elf32_header bs:(elf32_header*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf_ident bs) (fun (ident, bs) ->
	if not (is_magic_number_correct ident) then
	  fail "read_elf32_header: magic number incorrect"
	else
    let endian = (deduce_endianness ident) in bind (read_elf32_half endian bs) (fun (typ, bs) -> bind (read_elf32_half endian bs) (fun (machine, bs) -> bind (read_elf32_word endian bs) (fun (version, bs) -> bind (read_elf32_addr endian bs) (fun (entry, bs) -> bind (read_elf32_off  endian bs) (fun (phoff, bs) -> bind (read_elf32_off  endian bs) (fun (shoff, bs) -> bind (read_elf32_word endian bs) (fun (flags, bs) -> bind (read_elf32_half endian bs) (fun (ehsize, bs) -> bind (read_elf32_half endian bs) (fun (phentsize, bs) -> bind (read_elf32_half endian bs) (fun (phnum, bs) -> bind (read_elf32_half endian bs) (fun (shentsize, bs) -> bind (read_elf32_half endian bs) (fun (shnum, bs) -> bind (read_elf32_half endian bs) (fun (shstrndx, bs) ->
    (match Lem_list.list_index ident 4 with
      | None -> fail "read_elf32_header: transcription of ELF identifier failed"
      | Some c  ->
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) elf_class_32 then
		      return ({ elf32_ident = ident; elf32_type  = typ;
                      elf32_machine = machine; elf32_version = version;
                      elf32_entry = entry; elf32_phoff = phoff;
                      elf32_shoff = shoff; elf32_flags = flags;
                      elf32_ehsize = ehsize; elf32_phentsize = phentsize;
                      elf32_phnum = phnum; elf32_shentsize = shentsize;
                      elf32_shnum = shnum; elf32_shstrndx = shstrndx }, bs)
        else
          fail "read_elf32_header: not a 32-bit ELF file"
    ))))))))))))))))

(** [read_elf64_header bs0] reads an ELF header from the byte sequence [bs0].
  * Fails if transcription fails.
  *)
(*val read_elf64_header : byte_sequence -> error (elf64_header * byte_sequence)*)
let read_elf64_header bs:(elf64_header*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf_ident bs) (fun (ident, bs) ->
  if not (is_magic_number_correct ident) then
    fail "read_elf64_header: magic number incorrect"
  else
    let endian = (deduce_endianness ident) in bind (read_elf64_half endian bs) (fun (typ, bs) -> bind (read_elf64_half endian bs) (fun (machine, bs) -> bind (read_elf64_word endian bs) (fun (version, bs) -> bind (read_elf64_addr endian bs) (fun (entry, bs) -> bind (read_elf64_off  endian bs) (fun (phoff, bs) -> bind (read_elf64_off  endian bs) (fun (shoff, bs) -> bind (read_elf64_word endian bs) (fun (flags, bs) -> bind (read_elf64_half endian bs) (fun (ehsize, bs) -> bind (read_elf64_half endian bs) (fun (phentsize, bs) -> bind (read_elf64_half endian bs) (fun (phnum, bs) -> bind (read_elf64_half endian bs) (fun (shentsize, bs) -> bind (read_elf64_half endian bs) (fun (shnum, bs) -> bind (read_elf64_half endian bs) (fun (shstrndx, bs) ->
    (match Lem_list.list_index ident 4 with
      | None -> fail "read_elf64_header: transcription of ELF identifier failed"
      | Some c  ->
        if Nat_big_num.equal (Uint32_wrapper.to_bigint c) elf_class_64 then
          return ({ elf64_ident = ident; elf64_type  = typ;
                     elf64_machine = machine; elf64_version = version;
                     elf64_entry = entry; elf64_phoff = phoff;
                     elf64_shoff = shoff; elf64_flags = flags;
                     elf64_ehsize = ehsize; elf64_phentsize = phentsize;
                     elf64_phnum = phnum; elf64_shentsize = shentsize;
                     elf64_shnum = shnum; elf64_shstrndx = shstrndx }, bs)
        else
          fail "read_elf64_header: not a 64-bit ELF file"
    ))))))))))))))))

(** [is_elf32_header_class_correct hdr] checks whether the declared file class
  * is correct.
  *)
(*val is_elf32_header_class_correct : elf32_header -> bool*)
let is_elf32_header_class_correct ehdr:bool=  (Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 4) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 1)))))
  
(** [is_elf64_header_class_correct hdr] checks whether the declared file class
  * is correct.
  *)
(*val is_elf64_header_class_correct : elf64_header -> bool*)
let is_elf64_header_class_correct ehdr:bool=  (Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf64_ident 4) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 1)))))

(** [is_elf32_header_version_correct hdr] checks whether the declared file version
  * is correct.
  *)
(*val is_elf32_header_version_correct : elf32_header -> bool*)
let is_elf32_header_version_correct ehdr:bool=  (Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf32_ident 6) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 1)))))
  
(** [is_elf64_header_version_correct hdr] checks whether the declared file version
  * is correct.
  *)
(*val is_elf64_header_version_correct : elf64_header -> bool*)
let is_elf64_header_version_correct ehdr:bool=  (Lem.option_equal (=)
  (Lem_list.list_index ehdr.elf64_ident 6) (Some (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 1)))))

(** [is_elf32_header_valid] checks whether an [elf32_header] value is a valid 32-bit
  * ELF file header (i.e. [elf32_ident] is [ei_nident] entries long, and other
  * constraints on headers).
  *)
(*val is_elf32_header_valid : elf32_header -> bool*)
let is_elf32_header_valid ehdr:bool=  (Nat_big_num.equal
  (Nat_big_num.of_int (List.length ehdr.elf32_ident)) ei_nident &&
  (is_magic_number_correct ehdr.elf32_ident &&
  (is_elf32_header_padding_correct ehdr &&
  (is_elf32_header_class_correct ehdr &&
  is_elf32_header_version_correct ehdr))))

(** [get_elf32_header_program_table_size] calculates the size of the program table
  * (entry size x number of entries) based on data in the ELF header.
  *)
(*val get_elf32_header_program_table_size : elf32_header -> natural*)
let get_elf32_header_program_table_size ehdr:Nat_big_num.num=
   (let phentsize = (Uint32_wrapper.to_bigint ehdr.elf32_phentsize) in
  let phnum     = (Uint32_wrapper.to_bigint ehdr.elf32_phnum) in Nat_big_num.mul
    phentsize phnum)

(** [get_elf64_header_program_table_size] calculates the size of the program table
  * (entry size x number of entries) based on data in the ELF header.
  *)
(*val get_elf64_header_program_table_size : elf64_header -> natural*)
let get_elf64_header_program_table_size ehdr:Nat_big_num.num=
   (let phentsize = (Uint32_wrapper.to_bigint ehdr.elf64_phentsize) in
  let phnum     = (Uint32_wrapper.to_bigint ehdr.elf64_phnum) in Nat_big_num.mul
    phentsize phnum)

(** [is_elf32_header_section_table_present] calculates whether a section table
  * is present in the ELF file or not.
  *)
(*val is_elf32_header_section_table_present : elf32_header -> bool*)
let is_elf32_header_section_table_present ehdr:bool=
   (not ( Nat_big_num.equal(Uint32_wrapper.to_bigint ehdr.elf32_shoff)( (Nat_big_num.of_int 0))))

(** [is_elf64_header_section_table_present] calculates whether a section table
  * is present in the ELF file or not.
  *)
(*val is_elf64_header_section_table_present : elf64_header -> bool*)
let is_elf64_header_section_table_present ehdr:bool=
   (not ( Nat_big_num.equal(Uint64_wrapper.to_bigint ehdr.elf64_shoff)( (Nat_big_num.of_int 0))))

(** [get_elf32_header_section_table_size] calculates the size of the section table
  * (entry size x number of entries) based on data in the ELF header.
  *)
(*val get_elf32_header_section_table_size : elf32_header -> natural*)
let get_elf32_header_section_table_size ehdr:Nat_big_num.num=
   (let shentsize = (Uint32_wrapper.to_bigint ehdr.elf32_shentsize) in
  let shnum     = (Uint32_wrapper.to_bigint ehdr.elf32_shnum) in Nat_big_num.mul
    shentsize shnum)

(** [get_elf64_header_section_table_size] calculates the size of the section table
  * (entry size x number of entries) based on data in the ELF header.
  *)
(*val get_elf64_header_section_table_size : elf64_header -> natural*)
let get_elf64_header_section_table_size ehdr:Nat_big_num.num=
   (let shentsize = (Uint32_wrapper.to_bigint ehdr.elf64_shentsize) in
  let shnum     = (Uint32_wrapper.to_bigint ehdr.elf64_shnum) in Nat_big_num.mul
    shentsize shnum)