open Preamble

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

open Label

open Sets

open Listb

open Star

open Frontend_misc

open CexecInd

open Casts

open ClassifyOp

open Smallstep

open Extra_bool

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Globalenvs

open Csem

open SmallstepExec

open Division

open Z

open BitVectorZ

open Pointers

open Values

open Events

open IOMonad

open IO

open Cexec

open TypeComparison

open SimplifyCasts

open MemProperties

open MemoryInjections

open Fresh

open SwitchRemoval

open FrontEndOps

open Cminor_syntax

open ToCminor

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

open ToRTLabs

open Deqsets_extra

open CostMisc

open Listb_extra

open CostSpec

open CostCheck

open CostInj

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open String

open LabelledObjects

open I8051

open BackEndOps

open Joint

open RTL

open RTLabsToRTL

open ERTL

open RegisterSet

open RTLToERTL

open Fixpoints

open Set_adt

open Liveness

open Interference

open Joint_LTL_LIN

open LTL

open ERTLToLTL

open LIN

open Linearise

open LTLToLIN

open ASM

open BitVectorTrieSet

open LINToASM

type pass =
| Clight_pass
| Clight_switch_removed_pass
| Clight_label_pass
| Clight_simplified_pass
| Cminor_pass
| Rtlabs_pass
| Rtl_separate_pass
| Rtl_uniq_pass
| Ertl_pass
| Ltl_pass
| Lin_pass
| Assembly_pass
| Object_code_pass

val pass_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> pass -> 'a1

val pass_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> pass -> 'a1

val pass_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> pass -> 'a1

val pass_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> pass -> 'a1

val pass_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> pass -> 'a1

val pass_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> pass -> 'a1

val pass_inv_rect_Type4 :
  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val pass_inv_rect_Type3 :
  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val pass_inv_rect_Type2 :
  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val pass_inv_rect_Type1 :
  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val pass_inv_rect_Type0 :
  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val pass_discr : pass -> pass -> __

val pass_jmdiscr : pass -> pass -> __

type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod

type syntax_of_pass = __

type observe_pass = pass -> syntax_of_pass -> Types.unit0

val front_end :
  observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
  Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
  Types.prod Errors.res

open Uses

val compute_fixpoint : Fixpoints.fixpoint_computer

val colour_graph : Interference.coloured_graph_computer

open AssocList

val lookup_stack_cost :
  Joint.params -> Joint.joint_program -> PreIdentifiers.identifier -> Nat.nat
  Types.option

val back_end :
  observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
  (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res

open Status

open Fetch

open Assembly

open PolicyFront

open PolicyStep

open Policy

val assembler :
  observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
  Errors.res

open StructuredTraces

open AbstractStatus

open StatusProofs

open Interpret

open ASMCosts

val lift_out_of_sigma :
  'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 -> 'a2

val lift_cost_map_back_to_front :
  ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
  Label.clight_cost_map

open UtilBranch

open ASMCostsSplit

type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
                         c_stack_cost : Joint.stack_cost_model;
                         c_max_stack : Nat.nat;
                         c_init_costlabel : CostLabel.costlabel;
                         c_labelled_clight : Csyntax.clight_program;
                         c_clight_cost_map : Label.clight_cost_map }

val compiler_output_rect_Type4 :
  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
  'a1) -> compiler_output -> 'a1

val compiler_output_rect_Type5 :
  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
  'a1) -> compiler_output -> 'a1

val compiler_output_rect_Type3 :
  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
  'a1) -> compiler_output -> 'a1

val compiler_output_rect_Type2 :
  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
  'a1) -> compiler_output -> 'a1

val compiler_output_rect_Type1 :
  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
  'a1) -> compiler_output -> 'a1

val compiler_output_rect_Type0 :
  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
  'a1) -> compiler_output -> 'a1

val c_labelled_object_code : compiler_output -> ASM.labelled_object_code

val c_stack_cost : compiler_output -> Joint.stack_cost_model

val c_max_stack : compiler_output -> Nat.nat

val c_init_costlabel : compiler_output -> CostLabel.costlabel

val c_labelled_clight : compiler_output -> Csyntax.clight_program

val c_clight_cost_map : compiler_output -> Label.clight_cost_map

val compiler_output_inv_rect_Type4 :
  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
  Label.clight_cost_map -> __ -> 'a1) -> 'a1

val compiler_output_inv_rect_Type3 :
  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
  Label.clight_cost_map -> __ -> 'a1) -> 'a1

val compiler_output_inv_rect_Type2 :
  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
  Label.clight_cost_map -> __ -> 'a1) -> 'a1

val compiler_output_inv_rect_Type1 :
  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
  Label.clight_cost_map -> __ -> 'a1) -> 'a1

val compiler_output_inv_rect_Type0 :
  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
  Label.clight_cost_map -> __ -> 'a1) -> 'a1

val compiler_output_jmdiscr : compiler_output -> compiler_output -> __

val compile :
  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res