extracted/measurable.mli

   1 open Preamble
   2
   3 open IO
   4
   5 open CostLabel
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open Lists
  12
  13 open Identifiers
  14
  15 open AST
  16
  17 open Division
  18
  19 open Z
  20
  21 open BitVectorZ
  22
  23 open Pointers
  24
  25 open Coqlib
  26
  27 open Values
  28
  29 open Events
  30
  31 open Exp
  32
  33 open Arithmetic
  34
  35 open Vector
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Extranat
  42
  43 open Integers
  44
  45 open Proper
  46
  47 open ErrorMessages
  48
  49 open Option
  50
  51 open Setoids
  52
  53 open Monad
  54
  55 open Positive
  56
  57 open PreIdentifiers
  58
  59 open Errors
  60
  61 open IOMonad
  62
  63 open Div_and_mod
  64
  65 open Jmeq
  66
  67 open Russell
  68
  69 open Util
  70
  71 open Bool
  72
  73 open Relations
  74
  75 open Nat
  76
  77 open List
  78
  79 open Hints_declaration
  80
  81 open Core_notation
  82
  83 open Pts
  84
  85 open Logic
  86
  87 open Types
  88
  89 open Extralib
  90
  91 open SmallstepExec
  92
  93 open Executions
  94
  95 open Hide
  96
  97 open Sets
  98
  99 open Listb
 100
 101 open StructuredTraces
 102
 103 open Stacksize
 104
 105 type classified_system = { cs_exec : (IO.io_out, IO.io_in)
 106                                      SmallstepExec.fullexec; cs_global :
 107                            __; cs_labelled : (__ -> Bool.bool);
 108                            cs_classify : (__ ->
 109                                          StructuredTraces.status_class);
 110                            cs_callee : (__ -> __ -> AST.ident) }
 111
 112 val classified_system_rect_Type4 :
 113   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
 114   (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
 115   classified_system -> 'a1
 116
 117 val classified_system_rect_Type5 :
 118   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
 119   (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
 120   classified_system -> 'a1
 121
 122 val classified_system_rect_Type3 :
 123   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
 124   (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
 125   classified_system -> 'a1
 126
 127 val classified_system_rect_Type2 :
 128   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
 129   (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
 130   classified_system -> 'a1
 131
 132 val classified_system_rect_Type1 :
 133   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
 134   (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
 135   classified_system -> 'a1
 136
 137 val classified_system_rect_Type0 :
 138   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
 139   (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
 140   classified_system -> 'a1
 141
 142 val cs_exec :
 143   classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
 144
 145 val cs_global : classified_system -> __
 146
 147 val cs_labelled : classified_system -> __ -> Bool.bool
 148
 149 val cs_classify : classified_system -> __ -> StructuredTraces.status_class
 150
 151 val cs_callee0 : classified_system -> __ -> AST.ident
 152
 153 val classified_system_inv_rect_Type4 :
 154   classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
 155   (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
 156   AST.ident) -> __ -> 'a1) -> 'a1
 157
 158 val classified_system_inv_rect_Type3 :
 159   classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
 160   (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
 161   AST.ident) -> __ -> 'a1) -> 'a1
 162
 163 val classified_system_inv_rect_Type2 :
 164   classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
 165   (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
 166   AST.ident) -> __ -> 'a1) -> 'a1
 167
 168 val classified_system_inv_rect_Type1 :
 169   classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
 170   (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
 171   AST.ident) -> __ -> 'a1) -> 'a1
 172
 173 val classified_system_inv_rect_Type0 :
 174   classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
 175   (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
 176   AST.ident) -> __ -> 'a1) -> 'a1
 177
 178 val cs_exec__o__es1 :
 179   classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
 180
 181 type cs_state = __
 182
 183 val intensional_event_of_event :
 184   Events.event -> StructuredTraces.intensional_event List.list
 185
 186 val intensional_events_of_events :
 187   Events.trace -> StructuredTraces.intensional_event List.list
 188
 189 val intensional_state_change :
 190   classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
 191   StructuredTraces.intensional_event List.list) Types.prod
 192
 193 val intensional_trace_of_trace :
 194   classified_system -> AST.ident List.list -> (cs_state, Events.trace)
 195   Types.prod List.list -> (AST.ident List.list,
 196   StructuredTraces.intensional_event List.list) Types.prod
 197
 198 val normal_state : classified_system -> cs_state -> Bool.bool
 199
 200 val measure_stack :
 201   (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
 202   StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info
 203
 204 val will_return_aux :
 205   classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
 206   List.list -> Bool.bool
 207
 208 val will_return' :
 209   classified_system -> (cs_state, Events.trace) Types.prod List.list ->
 210   Bool.bool
 211
 212 type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
 213                                          SmallstepExec.fullexec;
 214                               pcs_labelled : (__ -> __ -> Bool.bool);
 215                               pcs_classify : (__ -> __ ->
 216                                              StructuredTraces.status_class);
 217                               pcs_callee : (__ -> __ -> __ -> AST.ident) }
 218
 219 val preclassified_system_rect_Type4 :
 220   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
 221   (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
 222   AST.ident) -> 'a1) -> preclassified_system -> 'a1
 223
 224 val preclassified_system_rect_Type5 :
 225   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
 226   (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
 227   AST.ident) -> 'a1) -> preclassified_system -> 'a1
 228
 229 val preclassified_system_rect_Type3 :
 230   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
 231   (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
 232   AST.ident) -> 'a1) -> preclassified_system -> 'a1
 233
 234 val preclassified_system_rect_Type2 :
 235   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
 236   (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
 237   AST.ident) -> 'a1) -> preclassified_system -> 'a1
 238
 239 val preclassified_system_rect_Type1 :
 240   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
 241   (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
 242   AST.ident) -> 'a1) -> preclassified_system -> 'a1
 243
 244 val preclassified_system_rect_Type0 :
 245   ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
 246   (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
 247   AST.ident) -> 'a1) -> preclassified_system -> 'a1
 248
 249 val pcs_exec :
 250   preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
 251
 252 val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool
 253
 254 val pcs_classify :
 255   preclassified_system -> __ -> __ -> StructuredTraces.status_class
 256
 257 val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident
 258
 259 val preclassified_system_inv_rect_Type4 :
 260   preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
 261   (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
 262   (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
 263
 264 val preclassified_system_inv_rect_Type3 :
 265   preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
 266   (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
 267   (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
 268
 269 val preclassified_system_inv_rect_Type2 :
 270   preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
 271   (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
 272   (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
 273
 274 val preclassified_system_inv_rect_Type1 :
 275   preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
 276   (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
 277   (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
 278
 279 val preclassified_system_inv_rect_Type0 :
 280   preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
 281   (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
 282   (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
 283
 284 val pcs_exec__o__es1 :
 285   preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
 286
 287 val pcs_to_cs : preclassified_system -> __ -> classified_system
 288
 289 val observables :
 290   preclassified_system -> __ -> Nat.nat -> Nat.nat ->
 291   (StructuredTraces.intensional_event List.list,
 292   StructuredTraces.intensional_event List.list) Types.prod Errors.res
 293
 294 val observe_all_in_measurable :
 295   Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
 296   Types.unit0) -> AST.ident List.list -> __ ->
 297   (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
 298   Types.prod
 299