open Preamble

open BitVectorTrie

open Graphs

open Order

open Registers

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Division

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open FrontEndOps

open CostLabel

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 Types

open AST

open Hints_declaration

open Core_notation

open Pts

open Logic

open RTLabs_syntax

open CostSpec

open Extra_bool

open Sets

open Listb

open Listb_extra

open CostMisc

(** val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool **)
let check_well_cost_fn f =
  Bool.andb
    (Identifiers.idmap_all PreIdentifiers.LabelTag f.RTLabs_syntax.f_graph
      (fun l s _ ->
      CostSpec.well_cost_labelled_statement f.RTLabs_syntax.f_graph s))
    (CostSpec.is_cost_label
      (Identifiers.lookup_present PreIdentifiers.LabelTag
        f.RTLabs_syntax.f_graph (Types.pi1 f.RTLabs_syntax.f_entry)))

open Deqsets_extra

(** val check_label_bounded :
    RTLabs_syntax.statement Graphs.graph -> Graphs.label -> Graphs.label
    List.list -> Identifiers.identifier_set -> Nat.nat ->
    Identifiers.identifier_set Types.option **)
let rec check_label_bounded g checking checking_tail to_check term_check =
  let stop_now = Types.Some to_check in
  (match term_check with
   | Nat.O -> (fun _ -> assert false (* absurd case *))
   | Nat.S term_check' ->
     (fun _ ->
       let st = Identifiers.lookup_present PreIdentifiers.LabelTag g checking
       in
       let succs = CostSpec.successors st in
       (match succs with
        | List.Nil -> (fun _ -> stop_now)
        | List.Cons (h, t) ->
          (match t with
           | List.Nil ->
             (fun _ ->
               let st' =
                 Identifiers.lookup_present PreIdentifiers.LabelTag g h
               in
               (match CostSpec.is_cost_label st' with
                | Bool.True -> stop_now
                | Bool.False ->
                  (match Identifiers.try_remove PreIdentifiers.LabelTag
                           to_check h with
                   | Types.None ->
                     (fun _ ->
                       match Bool.orb
                               (Deqsets.eqb
                                 (Identifiers.deq_identifier
                                   PreIdentifiers.LabelTag) (Obj.magic h)
                                 (Obj.magic checking))
                               (Listb.memb
                                 (Identifiers.deq_identifier
                                   PreIdentifiers.LabelTag) (Obj.magic h)
                                 (Obj.magic checking_tail)) with
                       | Bool.True -> Types.None
                       | Bool.False -> stop_now)
                   | Types.Some to_check' ->
                     (fun _ ->
                       check_label_bounded g h (List.Cons (checking,
                         checking_tail)) to_check'.Types.snd term_check')) __))
           | List.Cons (x, x0) -> (fun _ -> stop_now))) __)) __

(** val check_graph_bounded :
    RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set ->
    Graphs.label -> Nat.nat -> Bool.bool **)
let rec check_graph_bounded g to_check start term_check =
  (match term_check with
   | Nat.O -> (fun _ -> assert false (* absurd case *))
   | Nat.S term_check' ->
     (fun _ ->
       (match check_label_bounded g start List.Nil to_check
                (Identifiers.id_map_size PreIdentifiers.LabelTag g) with
        | Types.None -> (fun _ -> Bool.False)
        | Types.Some to_check' ->
          (fun _ ->
            (match Identifiers.choose PreIdentifiers.LabelTag to_check' with
             | Types.None -> (fun _ _ _ -> Bool.True)
             | Types.Some l_to_check'' ->
               (fun _ _ _ ->
                 check_graph_bounded g l_to_check''.Types.snd
                   l_to_check''.Types.fst.Types.fst term_check')) __ __ __))
         __)) __

(** val check_sound_cost_fn :
    RTLabs_syntax.internal_function -> Bool.bool **)
let check_sound_cost_fn fn =
  (match Identifiers.try_remove PreIdentifiers.LabelTag
           (Identifiers.id_set_of_map PreIdentifiers.LabelTag
             fn.RTLabs_syntax.f_graph) (Types.pi1 fn.RTLabs_syntax.f_entry) with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some to_check ->
     (fun _ _ _ ->
       check_graph_bounded fn.RTLabs_syntax.f_graph to_check.Types.snd
         (Types.pi1 fn.RTLabs_syntax.f_entry)
         (Identifiers.id_map_size PreIdentifiers.LabelTag
           fn.RTLabs_syntax.f_graph))) __ __ __

(** val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool **)
let check_cost_program p =
  Lists.all (fun fn ->
    match fn.Types.snd with
    | AST.Internal fn0 ->
      Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0)
    | AST.External x -> Bool.True) p.AST.prog_funct

(** val check_cost_program_prf :
    RTLabs_syntax.rTLabs_program -> __ Errors.res **)
let check_cost_program_prf p =
  (match check_cost_program p with
   | Bool.True -> (fun _ -> Errors.OK __)
   | Bool.False ->
     (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __