open Preamble open Status open BitVectorTrie open String open Integers open AST open LabelledObjects open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Lists open Positive open Identifiers open CostLabel open ASM open Exp open Setoids open Monad open Option open Extranat open Vector open FoldStuff open BitVector open Arithmetic open Fetch open Assembly open Div_and_mod open Jmeq open Russell open Util open Bool open Relations open Nat open List open Hints_declaration open Core_notation open Pts open Logic open Types open Extralib open PolicyFront open PolicyStep val jump_expansion_internal : ASM.labelled_instruction List.list Types.sig0 -> Nat.nat -> (Bool.bool, PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 val measure_int : ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat -> Nat.nat val je_fixpoint : ASM.labelled_instruction List.list Types.sig0 -> PolicyFront.ppc_pc_map Types.option Types.sig0 val jump_expansion' : ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word, BitVector.word -> Bool.bool) Types.prod Types.sig0 Types.option