bench/encoding/why2/caduceus/init_why.why

   1 logic eq_unit : unit, unit -> prop
   2
   3 logic neq_unit : unit, unit -> prop
   4
   5 logic eq_bool : bool, bool -> prop
   6
   7 logic neq_bool : bool, bool -> prop
   8
   9 logic lt_int : int, int -> prop
  10
  11 logic le_int : int, int -> prop
  12
  13 logic gt_int : int, int -> prop
  14
  15 logic ge_int : int, int -> prop
  16
  17 logic eq_int : int, int -> prop
  18
  19 logic neq_int : int, int -> prop
  20
  21 logic add_int : int, int -> int
  22
  23 logic sub_int : int, int -> int
  24
  25 logic mul_int : int, int -> int
  26
  27 logic div_int : int, int -> int
  28
  29 logic mod_int : int, int -> int
  30
  31 logic neg_int : int -> int
  32
  33 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
  34
  35 logic bw_compl : int -> int
  36
  37 logic bw_and : int, int -> int
  38
  39 logic bw_xor : int, int -> int
  40
  41 logic bw_or : int, int -> int
  42
  43 logic lsl : int, int -> int
  44
  45 logic lsr : int, int -> int
  46
  47 type 'z pointer
  48
  49 type 'z addr
  50
  51 type alloc_table
  52
  53 logic block_length : alloc_table, 'a1 pointer -> int
  54
  55 logic base_addr : 'a1 pointer -> 'a1 addr
  56
  57 logic offset : 'a1 pointer -> int
  58
  59 logic shift : 'a1 pointer, int -> 'a1 pointer
  60
  61 logic sub_pointer : 'a1 pointer, 'a1 pointer -> int
  62
  63 predicate lt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  64   ((base_addr(p1) = base_addr(p2)) and (offset(p1) < offset(p2)))
  65
  66 predicate le_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  67   ((base_addr(p1) = base_addr(p2)) and (offset(p1) <= offset(p2)))
  68
  69 predicate gt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  70   ((base_addr(p1) = base_addr(p2)) and (offset(p1) > offset(p2)))
  71
  72 predicate ge_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  73   ((base_addr(p1) = base_addr(p2)) and (offset(p1) >= offset(p2)))
  74
  75 predicate valid(a: alloc_table, p: 'a1 pointer) =
  76   ((0 <= offset(p)) and (offset(p) < block_length(a, p)))
  77
  78 predicate valid_index(a: alloc_table, p: 'a1 pointer, i: int) =
  79   ((0 <= (offset(p) + i)) and ((offset(p) + i) < block_length(a, p)))
  80
  81 predicate valid_range(a: alloc_table, p: 'a1 pointer, i: int, j: int) =
  82   ((0 <= (offset(p) + i)) and ((offset(p) + j) < block_length(a, p)))
  83
  84 axiom offset_shift:
  85   (forall p:'a1 pointer.
  86     (forall i:int [offset(shift(p, i))]. (offset(shift(p,
  87       i)) = (offset(p) + i))))
  88
  89 axiom shift_zero: (forall p:'a1 pointer [shift(p, 0)]. (shift(p, 0) = p))
  90
  91 axiom shift_shift:
  92   (forall p:'a1 pointer.
  93     (forall i:int.
  94       (forall j:int [shift(shift(p, i), j)]. (shift(shift(p, i),
  95         j) = shift(p, (i + j))))))
  96
  97 axiom base_addr_shift:
  98   (forall p:'a1 pointer.
  99     (forall i:int [base_addr(shift(p, i))]. (base_addr(shift(p,
 100       i)) = base_addr(p))))
 101
 102 axiom block_length_shift:
 103   (forall a:alloc_table.
 104     (forall p:'a1 pointer.
 105       (forall i:int [block_length(a, shift(p, i))]. (block_length(a, shift(p,
 106         i)) = block_length(a, p)))))
 107
 108 axiom base_addr_block_length:
 109   (forall a:alloc_table.
 110     (forall p1:'a1 pointer.
 111       (forall p2:'a1 pointer.
 112         ((base_addr(p1) = base_addr(p2)) -> (block_length(a,
 113          p1) = block_length(a, p2))))))
 114
 115 axiom pointer_pair_1:
 116   (forall p1:'a1 pointer.
 117     (forall p2:'a1 pointer.
 118       (((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))) ->
 119        (p1 = p2))))
 120
 121 axiom pointer_pair_2:
 122   (forall p1:'a1 pointer.
 123     (forall p2:'a1 pointer.
 124       ((p1 = p2) ->
 125        ((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))))))
 126
 127 axiom neq_base_addr_neq_shift:
 128   (forall p1:'a1 pointer.
 129     (forall p2:'a1 pointer.
 130       (forall i:int.
 131         (forall j:int.
 132           ((base_addr(p1) <> base_addr(p2)) -> (shift(p1, i) <> shift(p2, j)))))))
 133
 134 axiom neq_offset_neq_shift:
 135   (forall p1:'a1 pointer.
 136     (forall p2:'a1 pointer.
 137       (forall i:int.
 138         (forall j:int.
 139           (((offset(p1) + i) <> (offset(p2) + j)) -> (shift(p1,
 140            i) <> shift(p2, j)))))))
 141
 142 axiom eq_offset_eq_shift:
 143   (forall p1:'a1 pointer.
 144     (forall p2:'a1 pointer.
 145       (forall i:int.
 146         (forall j:int.
 147           ((base_addr(p1) = base_addr(p2)) ->
 148            (((offset(p1) + i) = (offset(p2) + j)) -> (shift(p1,
 149             i) = shift(p2, j))))))))
 150
 151 axiom valid_index_valid_shift:
 152   (forall a:alloc_table.
 153     (forall p:'a1 pointer.
 154       (forall i:int. (valid_index(a, p, i) -> valid(a, shift(p, i))))))
 155
 156 axiom valid_range_valid_shift:
 157   (forall a:alloc_table.
 158     (forall p:'a1 pointer.
 159       (forall i:int.
 160         (forall j:int.
 161           (forall k:int.
 162             (valid_range(a, p, i, j) ->
 163              (((i <= k) and (k <= j)) -> valid(a, shift(p, k)))))))))
 164
 165 axiom valid_range_valid:
 166   (forall a:alloc_table.
 167     (forall p:'a1 pointer.
 168       (forall i:int.
 169         (forall j:int.
 170           (valid_range(a, p, i, j) ->
 171            (((i <= 0) and (0 <= j)) -> valid(a, p)))))))
 172
 173 axiom valid_range_valid_index:
 174   (forall a:alloc_table.
 175     (forall p:'a1 pointer.
 176       (forall i:int.
 177         (forall j:int.
 178           (forall k:int.
 179             (valid_range(a, p, i, j) ->
 180              (((i <= k) and (k <= j)) -> valid_index(a, p, k))))))))
 181
 182 axiom sub_pointer_def:
 183   (forall p1:'a1 pointer.
 184     (forall p2:'a1 pointer.
 185       ((base_addr(p1) = base_addr(p2)) -> (sub_pointer(p1,
 186        p2) = (offset(p1) - offset(p2))))))
 187
 188 type ('a, 'z) memory
 189
 190 logic acc : ('a1, 'a2) memory, 'a2 pointer -> 'a1
 191
 192 logic upd : ('a1, 'a2) memory, 'a2 pointer, 'a1 -> ('a1, 'a2) memory
 193
 194 axiom acc_upd:
 195   (forall m:('a1, 'a2) memory.
 196     (forall p:'a2 pointer.
 197       (forall a:'a1 [acc(upd(m, p, a), p)]. (acc(upd(m, p, a), p) = a))))
 198
 199 axiom acc_upd_neq:
 200   (forall m:('a1, 'a2) memory.
 201     (forall p1:'a2 pointer.
 202       (forall p2:'a2 pointer.
 203         (forall a:'a1 [acc(upd(m, p1, a), p2)].
 204           ((p1 <> p2) -> (acc(upd(m, p1, a), p2) = acc(m, p2)))))))
 205
 206 axiom false_not_true: (false <> true)
 207
 208 type 'z pset
 209
 210 logic pset_empty : 'a1 pset
 211
 212 logic pset_singleton : 'a1 pointer -> 'a1 pset
 213
 214 logic pset_star : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 215
 216 logic pset_all : 'a1 pset -> 'a1 pset
 217
 218 logic pset_range : 'a1 pset, int, int -> 'a1 pset
 219
 220 logic pset_range_left : 'a1 pset, int -> 'a1 pset
 221
 222 logic pset_range_right : 'a1 pset, int -> 'a1 pset
 223
 224 logic pset_acc_all : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 225
 226 logic pset_acc_range : 'a2 pset, ('a1 pointer, 'a2) memory, int,
 227 int -> 'a1 pset
 228
 229 logic pset_acc_range_left : 'a2 pset, ('a1 pointer, 'a2) memory,
 230 int -> 'a1 pset
 231
 232 logic pset_acc_range_right : 'a2 pset, ('a1 pointer, 'a2) memory,
 233 int -> 'a1 pset
 234
 235 logic pset_union : 'a1 pset, 'a1 pset -> 'a1 pset
 236
 237 logic not_in_pset : 'a1 pointer, 'a1 pset -> prop
 238
 239 predicate not_assigns(a: alloc_table, m1: ('a1, 'a2) memory, m2: ('a1,
 240   'a2) memory, l: 'a2 pset) =
 241   (forall p:'a2 pointer.
 242     (valid(a, p) -> (not_in_pset(p, l) -> (acc(m2, p) = acc(m1, p)))))
 243
 244 axiom pset_empty_intro: (forall p:'a1 pointer. not_in_pset(p, pset_empty))
 245
 246 axiom pset_singleton_intro:
 247   (forall p1:'a1 pointer.
 248     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 249       ((p1 <> p2) -> not_in_pset(p1, pset_singleton(p2)))))
 250
 251 axiom pset_singleton_elim:
 252   (forall p1:'a1 pointer.
 253     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 254       (not_in_pset(p1, pset_singleton(p2)) -> (p1 <> p2))))
 255
 256 axiom not_not_in_singleton:
 257   (forall p:'a1 pointer. (not not_in_pset(p, pset_singleton(p))))
 258
 259 axiom pset_union_intro:
 260   (forall l1:'a1 pset.
 261     (forall l2:'a1 pset.
 262       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 263         ((not_in_pset(p, l1) and not_in_pset(p, l2)) -> not_in_pset(p,
 264          pset_union(l1, l2))))))
 265
 266 axiom pset_union_elim1:
 267   (forall l1:'a1 pset.
 268     (forall l2:'a1 pset.
 269       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 270         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l1)))))
 271
 272 axiom pset_union_elim2:
 273   (forall l1:'a1 pset.
 274     (forall l2:'a1 pset.
 275       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 276         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l2)))))
 277
 278 axiom pset_star_intro:
 279   (forall l:'a1 pset.
 280     (forall m:('a2 pointer, 'a1) memory.
 281       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 282         ((forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l))) ->
 283          not_in_pset(p, pset_star(l, m))))))
 284
 285 axiom pset_star_elim:
 286   (forall l:'a1 pset.
 287     (forall m:('a2 pointer, 'a1) memory.
 288       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 289         (not_in_pset(p, pset_star(l, m)) ->
 290          (forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l)))))))
 291
 292 axiom pset_all_intro:
 293   (forall p:'a1 pointer.
 294     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 295       ((forall p1:'a1 pointer.
 296          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))) ->
 297        not_in_pset(p, pset_all(l)))))
 298
 299 axiom pset_all_elim:
 300   (forall p:'a1 pointer.
 301     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 302       (not_in_pset(p, pset_all(l)) ->
 303        (forall p1:'a1 pointer.
 304          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))))))
 305
 306 axiom pset_range_intro:
 307   (forall p:'a1 pointer.
 308     (forall l:'a1 pset.
 309       (forall a:int.
 310         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 311           ((forall p1:'a1 pointer.
 312              (not_in_pset(p1, l) or
 313               (forall i:int.
 314                 (((a <= i) and (i <= b)) -> (p <> shift(p1, i)))))) ->
 315            not_in_pset(p, pset_range(l, a, b)))))))
 316
 317 axiom pset_range_elim:
 318   (forall p:'a1 pointer.
 319     (forall l:'a1 pset.
 320       (forall a:int.
 321         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 322           (not_in_pset(p, pset_range(l, a, b)) ->
 323            (forall p1:'a1 pointer.
 324              ((not not_in_pset(p1, l)) ->
 325               (forall i:int.
 326                 (((a <= i) and (i <= b)) -> (shift(p1, i) <> p))))))))))
 327
 328 axiom pset_range_left_intro:
 329   (forall p:'a1 pointer.
 330     (forall l:'a1 pset.
 331       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 332         ((forall p1:'a1 pointer.
 333            (not_in_pset(p1, l) or
 334             (forall i:int. ((i <= a) -> (p <> shift(p1, i)))))) ->
 335          not_in_pset(p, pset_range_left(l, a))))))
 336
 337 axiom pset_range_left_elim:
 338   (forall p:'a1 pointer.
 339     (forall l:'a1 pset.
 340       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 341         (not_in_pset(p, pset_range_left(l, a)) ->
 342          (forall p1:'a1 pointer.
 343            ((not not_in_pset(p1, l)) ->
 344             (forall i:int. ((i <= a) -> (shift(p1, i) <> p)))))))))
 345
 346 axiom pset_range_right_intro:
 347   (forall p:'a1 pointer.
 348     (forall l:'a1 pset.
 349       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 350         ((forall p1:'a1 pointer.
 351            (not_in_pset(p1, l) or
 352             (forall i:int. ((a <= i) -> (p <> shift(p1, i)))))) ->
 353          not_in_pset(p, pset_range_right(l, a))))))
 354
 355 axiom pset_range_right_elim:
 356   (forall p:'a1 pointer.
 357     (forall l:'a1 pset.
 358       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 359         (not_in_pset(p, pset_range_right(l, a)) ->
 360          (forall p1:'a1 pointer.
 361            ((not not_in_pset(p1, l)) ->
 362             (forall i:int. ((a <= i) -> (shift(p1, i) <> p)))))))))
 363
 364 axiom pset_acc_all_intro:
 365   (forall p:'a1 pointer.
 366     (forall l:'a2 pset.
 367       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 368         m))].
 369         ((forall p1:'a2 pointer.
 370            ((not not_in_pset(p1, l)) ->
 371             (forall i:int. (p <> acc(m, shift(p1, i)))))) ->
 372          not_in_pset(p, pset_acc_all(l, m))))))
 373
 374 axiom pset_acc_all_elim:
 375   (forall p:'a1 pointer.
 376     (forall l:'a2 pset.
 377       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 378         m))].
 379         (not_in_pset(p, pset_acc_all(l, m)) ->
 380          (forall p1:'a2 pointer.
 381            ((not not_in_pset(p1, l)) ->
 382             (forall i:int. (acc(m, shift(p1, i)) <> p))))))))
 383
 384 axiom pset_acc_range_intro:
 385   (forall p:'a1 pointer.
 386     (forall l:'a2 pset.
 387       (forall m:('a1 pointer, 'a2) memory.
 388         (forall a:int.
 389           (forall b:int [not_in_pset(p, pset_acc_range(l, m, a, b))].
 390             ((forall p1:'a2 pointer.
 391                ((not not_in_pset(p1, l)) ->
 392                 (forall i:int.
 393                   (((a <= i) and (i <= b)) -> (p <> acc(m, shift(p1, i))))))) ->
 394              not_in_pset(p, pset_acc_range(l, m, a, b))))))))
 395
 396 axiom pset_acc_range_elim:
 397   (forall p:'a1 pointer.
 398     (forall l:'a2 pset.
 399       (forall m:('a1 pointer, 'a2) memory.
 400         (forall a:int.
 401           (forall b:int.
 402             (not_in_pset(p, pset_acc_range(l, m, a, b)) ->
 403              (forall p1:'a2 pointer.
 404                ((not not_in_pset(p1, l)) ->
 405                 (forall i:int.
 406                   (((a <= i) and (i <= b)) -> (acc(m, shift(p1, i)) <> p)))))))))))
 407
 408 axiom pset_acc_range_left_intro:
 409   (forall p:'a1 pointer.
 410     (forall l:'a2 pset.
 411       (forall m:('a1 pointer, 'a2) memory.
 412         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 413           ((forall p1:'a2 pointer.
 414              ((not not_in_pset(p1, l)) ->
 415               (forall i:int. ((i <= a) -> (p <> acc(m, shift(p1, i))))))) ->
 416            not_in_pset(p, pset_acc_range_left(l, m, a)))))))
 417
 418 axiom pset_acc_range_left_elim:
 419   (forall p:'a1 pointer.
 420     (forall l:'a2 pset.
 421       (forall m:('a1 pointer, 'a2) memory.
 422         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 423           (not_in_pset(p, pset_acc_range_left(l, m, a)) ->
 424            (forall p1:'a2 pointer.
 425              ((not not_in_pset(p1, l)) ->
 426               (forall i:int. ((i <= a) -> (acc(m, shift(p1, i)) <> p))))))))))
 427
 428 axiom pset_acc_range_right_intro:
 429   (forall p:'a1 pointer.
 430     (forall l:'a2 pset.
 431       (forall m:('a1 pointer, 'a2) memory.
 432         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 433           ((forall p1:'a2 pointer.
 434              ((not not_in_pset(p1, l)) ->
 435               (forall i:int. ((a <= i) -> (p <> acc(m, shift(p1, i))))))) ->
 436            not_in_pset(p, pset_acc_range_right(l, m, a)))))))
 437
 438 axiom pset_acc_range_right_elim:
 439   (forall p:'a1 pointer.
 440     (forall l:'a2 pset.
 441       (forall m:('a1 pointer, 'a2) memory.
 442         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 443           (not_in_pset(p, pset_acc_range_right(l, m, a)) ->
 444            (forall p1:'a2 pointer.
 445              ((not not_in_pset(p1, l)) ->
 446               (forall i:int. ((a <= i) -> (acc(m, shift(p1, i)) <> p))))))))))
 447
 448 axiom not_assigns_trans:
 449   (forall a:alloc_table.
 450     (forall l:'a1 pset.
 451       (forall m1:('a2, 'a1) memory.
 452         (forall m2:('a2, 'a1) memory.
 453           (forall m3:('a2, 'a1) memory.
 454             (not_assigns(a, m1, m2, l) ->
 455              (not_assigns(a, m2, m3, l) -> not_assigns(a, m1, m3, l))))))))
 456
 457 axiom not_assigns_refl:
 458   (forall a:alloc_table.
 459     (forall l:'a1 pset.
 460       (forall m:('a2, 'a1) memory. not_assigns(a, m, m, l))))
 461
 462 predicate valid_acc(m1: ('a1 pointer, 'a2) memory) =
 463   (forall p:'a2 pointer.
 464     (forall a:alloc_table. (valid(a, p) -> valid(a, acc(m1, p)))))
 465
 466 predicate valid_acc_range(m1: ('a1 pointer, 'a2) memory, size: int) =
 467   (forall p:'a2 pointer.
 468     (forall a:alloc_table.
 469       (valid(a, p) -> valid_range(a, acc(m1, p), 0, (size - 1)))))
 470
 471 axiom valid_acc_range_valid:
 472   (forall m1:('a1 pointer, 'a2) memory.
 473     (forall size:int.
 474       (forall p:'a2 pointer.
 475         (forall a:alloc_table.
 476           (valid_acc_range(m1, size) -> (valid(a, p) -> valid(a, acc(m1, p))))))))
 477
 478 predicate separation1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 479   'a2) memory) =
 480   (forall p:'a2 pointer.
 481     (forall a:alloc_table.
 482       (valid(a, p) -> (base_addr(acc(m1, p)) <> base_addr(acc(m2, p))))))
 483
 484 predicate separation1_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 485   'a2) memory, size: int) =
 486   (forall p:'a2 pointer.
 487     (forall a:alloc_table.
 488       (valid(a, p) ->
 489        (forall i1:int.
 490          (forall i2:int.
 491            (((0 <= i1) and (i1 < size)) ->
 492             (((0 <= i2) and (i2 < size)) -> (base_addr(acc(m1, shift(p,
 493              i1))) <> base_addr(acc(m2, shift(p, i2)))))))))))
 494
 495 predicate separation1_range(m: ('a1 pointer, 'a2) memory, size: int) =
 496   (forall p:'a2 pointer.
 497     (forall a:alloc_table.
 498       (valid(a, p) ->
 499        (forall i1:int.
 500          (((0 <= i1) and (i1 < size)) -> (base_addr(acc(m, shift(p,
 501           i1))) <> base_addr(acc(m, p))))))))
 502
 503 predicate separation2(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 504   'a2) memory) =
 505   (forall p1:'a2 pointer.
 506     (forall p2:'a2 pointer.
 507       ((p1 <> p2) -> (base_addr(acc(m1, p1)) <> base_addr(acc(m2, p2))))))
 508
 509 predicate separation2_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 510   'a2) memory, size: int) =
 511   (forall p:'a2 pointer.
 512     (forall q:'a2 pointer.
 513       (forall a:alloc_table.
 514         (forall i:int.
 515           (((0 <= i) and (i < size)) -> (base_addr(acc(m1, shift(p,
 516            i))) <> base_addr(acc(m2, q))))))))
 517
 518 logic on_heap : alloc_table, 'a1 pointer -> prop
 519
 520 logic on_stack : alloc_table, 'a1 pointer -> prop
 521
 522 logic fresh : alloc_table, 'a1 pointer -> prop
 523
 524 axiom fresh_not_valid:
 525   (forall a:alloc_table.
 526     (forall p:'a1 pointer. (fresh(a, p) -> (not valid(a, p)))))
 527
 528 axiom fresh_not_valid_shift:
 529   (forall a:alloc_table.
 530     (forall p:'a1 pointer.
 531       (fresh(a, p) -> (forall i:int. (not valid(a, shift(p, i)))))))
 532
 533 logic alloc_extends : alloc_table, alloc_table -> prop
 534
 535 axiom alloc_extends_valid:
 536   (forall a1:alloc_table.
 537     (forall a2:alloc_table.
 538       (alloc_extends(a1, a2) ->
 539        (forall q:'a1 pointer. (valid(a1, q) -> valid(a2, q))))))
 540
 541 axiom alloc_extends_valid_index:
 542   (forall a1:alloc_table.
 543     (forall a2:alloc_table.
 544       (alloc_extends(a1, a2) ->
 545        (forall q:'a1 pointer.
 546          (forall i:int. (valid_index(a1, q, i) -> valid_index(a2, q, i)))))))
 547
 548 axiom alloc_extends_valid_range:
 549   (forall a1:alloc_table.
 550     (forall a2:alloc_table.
 551       (alloc_extends(a1, a2) ->
 552        (forall q:'a1 pointer.
 553          (forall i:int.
 554            (forall j:int.
 555              (valid_range(a1, q, i, j) -> valid_range(a2, q, i, j))))))))
 556
 557 axiom alloc_extends_refl: (forall a:alloc_table. alloc_extends(a, a))
 558
 559 axiom alloc_extends_trans:
 560   (forall a1:alloc_table.
 561     (forall a2:alloc_table.
 562       (forall a3:alloc_table [alloc_extends(a1, a2), alloc_extends(a2, a3)].
 563         (alloc_extends(a1, a2) ->
 564          (alloc_extends(a2, a3) -> alloc_extends(a1, a3))))))
 565
 566 logic free_stack : alloc_table, alloc_table, alloc_table -> prop
 567
 568 axiom free_stack_heap:
 569   (forall a1:alloc_table.
 570     (forall a2:alloc_table.
 571       (forall a3:alloc_table.
 572         (free_stack(a1, a2, a3) ->
 573          (forall p:'a1 pointer.
 574            (valid(a2, p) -> (on_heap(a2, p) -> valid(a3, p))))))))
 575
 576 axiom free_stack_stack:
 577   (forall a1:alloc_table.
 578     (forall a2:alloc_table.
 579       (forall a3:alloc_table.
 580         (free_stack(a1, a2, a3) ->
 581          (forall p:'a1 pointer.
 582            (valid(a1, p) -> (on_stack(a1, p) -> valid(a3, p))))))))
 583
 584 logic null : 'a1 pointer
 585
 586 axiom null_not_valid: (forall a:alloc_table. (not valid(a, null)))
 587
 588 type b_2_14
 589
 590 type b_2_15
 591
 592 type Z11
 593
 594 type b_2_18
 595
 596 type s_3
 597
 598 type s_4
 599
 600 type s_8
 601
 602 type SPM_16_17
 603
 604 type s_9
 605
 606 type index_1_13
 607
 608 type index_0_12
 609
 610 type u_6
 611
 612 type SPM_16
 613
 614 type t_0
 615
 616 type t_1
 617
 618 type b_2
 619
 620 type t_5
 621
 622 type t_7
 623
 624 type b_2_10
 625
 626 goal f_impl_po_1:
 627   forall alloc:alloc_table.
 628   forall b_s_9:(b_2_10 pointer, s_9) memory.
 629   forall intM_b_2_10:(int, b_2_10) memory.
 630   forall intM_t_7:(int,
 631   t_7) memory.
 632   forall s:s_9 pointer.
 633   forall t:t_7 pointer.
 634   ((("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)) and
 635     ("CADUCEUS_1":
 636     ((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 637      shift(acc(b_s_9, s), 2)) = 4)))) and
 638    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 639     (("CADUCEUS_5": valid(alloc, s)) and
 640      (("CADUCEUS_4": valid_acc(b_s_9)) and
 641       ("CADUCEUS_3": valid_acc_range(b_s_9, 3)))))) ->
 642   forall result:t_7 pointer.
 643   (result = shift(t, 1)) ->
 644   forall result0:int.
 645   (result0 = acc(intM_t_7, result)) ->
 646   valid(alloc, s)
 647
 648 goal f_impl_po_2:
 649   forall alloc:alloc_table.
 650   forall b_s_9:(b_2_10 pointer, s_9) memory.
 651   forall intM_b_2_10:(int, b_2_10) memory.
 652   forall intM_t_7:(int,
 653   t_7) memory.
 654   forall s:s_9 pointer.
 655   forall t:t_7 pointer.
 656   ((("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)) and
 657     ("CADUCEUS_1":
 658     ((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 659      shift(acc(b_s_9, s), 2)) = 4)))) and
 660    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 661     (("CADUCEUS_5": valid(alloc, s)) and
 662      (("CADUCEUS_4": valid_acc(b_s_9)) and
 663       ("CADUCEUS_3": valid_acc_range(b_s_9, 3)))))) ->
 664   forall result:t_7 pointer.
 665   (result = shift(t, 1)) ->
 666   forall result0:int.
 667   (result0 = acc(intM_t_7, result)) ->
 668   valid(alloc, s) ->
 669   forall result1:b_2_10 pointer.
 670   (result1 = acc(b_s_9, s)) ->
 671   forall result2:b_2_10 pointer.
 672   (result2 = shift(result1, 0)) ->
 673   forall result3:int.
 674   (result3 = acc(intM_b_2_10, result2)) ->
 675   valid(alloc, s) ->
 676   forall result4:b_2_10 pointer.
 677   (result4 = acc(b_s_9, s)) ->
 678   forall result5:b_2_10 pointer.
 679   (result5 = shift(result4, 2)) ->
 680   valid(alloc, result5)
 681
 682 goal f_impl_po_3:
 683   forall alloc:alloc_table.
 684   forall b_s_9:(b_2_10 pointer, s_9) memory.
 685   forall intM_b_2_10:(int, b_2_10) memory.
 686   forall intM_t_7:(int,
 687   t_7) memory.
 688   forall s:s_9 pointer.
 689   forall t:t_7 pointer.
 690   ((("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)) and
 691     ("CADUCEUS_1":
 692     ((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 693      shift(acc(b_s_9, s), 2)) = 4)))) and
 694    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 695     (("CADUCEUS_5": valid(alloc, s)) and
 696      (("CADUCEUS_4": valid_acc(b_s_9)) and
 697       ("CADUCEUS_3": valid_acc_range(b_s_9, 3)))))) ->
 698   forall result:t_7 pointer.
 699   (result = shift(t, 1)) ->
 700   forall result0:int.
 701   (result0 = acc(intM_t_7, result)) ->
 702   valid(alloc, s) ->
 703   forall result1:b_2_10 pointer.
 704   (result1 = acc(b_s_9, s)) ->
 705   forall result2:b_2_10 pointer.
 706   (result2 = shift(result1, 0)) ->
 707   forall result3:int.
 708   (result3 = acc(intM_b_2_10, result2)) ->
 709   valid(alloc, s) ->
 710   forall result4:b_2_10 pointer.
 711   (result4 = acc(b_s_9, s)) ->
 712   forall result5:b_2_10 pointer.
 713   (result5 = shift(result4, 2)) ->
 714   valid(alloc, result5) ->
 715   forall result6:int.
 716   (result6 = acc(intM_b_2_10, result5)) ->
 717   ("CADUCEUS_7": ("CADUCEUS_7": (((result0 + result3) + result6) = 7)))
 718
 719 goal f_impl_po_4:
 720   forall alloc:alloc_table.
 721   forall b_s_9:(b_2_10 pointer, s_9) memory.
 722   forall intM_b_2_10:(int, b_2_10) memory.
 723   forall intM_t_7:(int,
 724   t_7) memory.
 725   forall s:s_9 pointer.
 726   forall t:t_7 pointer.
 727   ((("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)) and
 728     ("CADUCEUS_1":
 729     ((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 730      shift(acc(b_s_9, s), 2)) = 4)))) and
 731    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 732     (("CADUCEUS_5": valid(alloc, s)) and
 733      (("CADUCEUS_4": valid_acc(b_s_9)) and
 734       ("CADUCEUS_3": valid_acc_range(b_s_9, 3)))))) ->
 735   forall result:t_7 pointer.
 736   (result = shift(t, 1)) ->
 737   forall result0:int.
 738   (result0 = acc(intM_t_7, result)) ->
 739   valid(alloc, s) ->
 740   forall result1:b_2_10 pointer.
 741   (result1 = acc(b_s_9, s)) ->
 742   forall result2:b_2_10 pointer.
 743   (result2 = shift(result1, 0)) ->
 744   forall result3:int.
 745   (result3 = acc(intM_b_2_10, result2)) ->
 746   valid(alloc, s) ->
 747   forall result4:b_2_10 pointer.
 748   (result4 = acc(b_s_9, s)) ->
 749   forall result5:b_2_10 pointer.
 750   (result5 = shift(result4, 2)) ->
 751   valid(alloc, result5) ->
 752   forall result6:int.
 753   (result6 = acc(intM_b_2_10, result5)) ->
 754   ("CADUCEUS_2": ("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)))
 755
 756 goal f_impl_po_5:
 757   forall alloc:alloc_table.
 758   forall b_s_9:(b_2_10 pointer, s_9) memory.
 759   forall intM_b_2_10:(int, b_2_10) memory.
 760   forall intM_t_7:(int,
 761   t_7) memory.
 762   forall s:s_9 pointer.
 763   forall t:t_7 pointer.
 764   ((("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)) and
 765     ("CADUCEUS_1":
 766     ((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 767      shift(acc(b_s_9, s), 2)) = 4)))) and
 768    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 769     (("CADUCEUS_5": valid(alloc, s)) and
 770      (("CADUCEUS_4": valid_acc(b_s_9)) and
 771       ("CADUCEUS_3": valid_acc_range(b_s_9, 3)))))) ->
 772   forall result:t_7 pointer.
 773   (result = shift(t, 1)) ->
 774   forall result0:int.
 775   (result0 = acc(intM_t_7, result)) ->
 776   valid(alloc, s) ->
 777   forall result1:b_2_10 pointer.
 778   (result1 = acc(b_s_9, s)) ->
 779   forall result2:b_2_10 pointer.
 780   (result2 = shift(result1, 0)) ->
 781   forall result3:int.
 782   (result3 = acc(intM_b_2_10, result2)) ->
 783   valid(alloc, s) ->
 784   forall result4:b_2_10 pointer.
 785   (result4 = acc(b_s_9, s)) ->
 786   forall result5:b_2_10 pointer.
 787   (result5 = shift(result4, 2)) ->
 788   valid(alloc, result5) ->
 789   forall result6:int.
 790   (result6 = acc(intM_b_2_10, result5)) ->
 791   ("CADUCEUS_1": (acc(intM_b_2_10, acc(b_s_9, s)) = 1))
 792
 793 goal f_impl_po_6:
 794   forall alloc:alloc_table.
 795   forall b_s_9:(b_2_10 pointer, s_9) memory.
 796   forall intM_b_2_10:(int, b_2_10) memory.
 797   forall intM_t_7:(int,
 798   t_7) memory.
 799   forall s:s_9 pointer.
 800   forall t:t_7 pointer.
 801   ((("CADUCEUS_2": (acc(intM_t_7, shift(t, 1)) = 2)) and
 802     ("CADUCEUS_1":
 803     ((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 804      shift(acc(b_s_9, s), 2)) = 4)))) and
 805    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 806     (("CADUCEUS_5": valid(alloc, s)) and
 807      (("CADUCEUS_4": valid_acc(b_s_9)) and
 808       ("CADUCEUS_3": valid_acc_range(b_s_9, 3)))))) ->
 809   forall result:t_7 pointer.
 810   (result = shift(t, 1)) ->
 811   forall result0:int.
 812   (result0 = acc(intM_t_7, result)) ->
 813   valid(alloc, s) ->
 814   forall result1:b_2_10 pointer.
 815   (result1 = acc(b_s_9, s)) ->
 816   forall result2:b_2_10 pointer.
 817   (result2 = shift(result1, 0)) ->
 818   forall result3:int.
 819   (result3 = acc(intM_b_2_10, result2)) ->
 820   valid(alloc, s) ->
 821   forall result4:b_2_10 pointer.
 822   (result4 = acc(b_s_9, s)) ->
 823   forall result5:b_2_10 pointer.
 824   (result5 = shift(result4, 2)) ->
 825   valid(alloc, result5) ->
 826   forall result6:int.
 827   (result6 = acc(intM_b_2_10, result5)) ->
 828   ("CADUCEUS_1": (acc(intM_b_2_10, shift(acc(b_s_9, s), 2)) = 4))
 829
 830 goal g_impl_po_1:
 831   forall alloc:alloc_table.
 832   forall intM_t_5:(int,
 833   'a1) memory.
 834   (2 >= 0) ->
 835   forall result:'a1 pointer.
 836   forall alloc0:alloc_table.
 837   (valid(alloc0, result) and
 838    ((offset(result) = 0) and
 839     ((block_length(alloc0, result) = 2) and
 840      (valid_range(alloc0, result, 0, (2 - 1)) and
 841       (fresh(alloc, result) and
 842        (on_stack(alloc0, result) and alloc_extends(alloc, alloc0))))))) ->
 843   forall intM_t_5_0:(int,
 844   'a1) memory.
 845   (intM_t_5_0 = upd(intM_t_5, result, 4)) ->
 846   forall result0:'a1 pointer.
 847   (result0 = shift(result, 1)) ->
 848   forall intM_t_5_1:(int,
 849   'a1) memory.
 850   (intM_t_5_1 = upd(intM_t_5_0, result0, 5)) ->
 851   forall result1:'a1 pointer.
 852   (result1 = shift(result, 0)) ->
 853   forall result2:int.
 854   (result2 = acc(intM_t_5_1, result1)) ->
 855   ("CADUCEUS_11": (result2 = 4))
 856
 857 goal h_impl_po_1:
 858   forall alloc:alloc_table.
 859   forall intM_u_6:(int,
 860   'a1) memory.
 861   (3 >= 0) ->
 862   forall result:'a1 pointer.
 863   forall alloc0:alloc_table.
 864   (valid(alloc0, result) and
 865    ((offset(result) = 0) and
 866     ((block_length(alloc0, result) = 3) and
 867      (valid_range(alloc0, result, 0, (3 - 1)) and
 868       (fresh(alloc, result) and
 869        (on_stack(alloc0, result) and alloc_extends(alloc, alloc0))))))) ->
 870   forall intM_u_6_0:(int,
 871   'a1) memory.
 872   (intM_u_6_0 = upd(intM_u_6, result, 3)) ->
 873   forall result0:'a1 pointer.
 874   (result0 = shift(result, 1)) ->
 875   forall intM_u_6_1:(int,
 876   'a1) memory.
 877   (intM_u_6_1 = upd(intM_u_6_0, result0, 4)) ->
 878   forall result1:'a1 pointer.
 879   (result1 = shift(result, 2)) ->
 880   forall intM_u_6_2:(int,
 881   'a1) memory.
 882   (intM_u_6_2 = upd(intM_u_6_1, result1, 5)) ->
 883   forall result2:'a1 pointer.
 884   (result2 = shift(result, 0)) ->
 885   forall result3:int.
 886   (result3 = acc(intM_u_6_2, result2)) ->
 887   forall result4:'a1 pointer.
 888   (result4 = shift(result, 1)) ->
 889   forall result5:int.
 890   (result5 = acc(intM_u_6_2, result4)) ->
 891   forall result6:'a1 pointer.
 892   (result6 = shift(result, 2)) ->
 893   valid(alloc0, result6)
 894
 895 goal h_impl_po_2:
 896   forall alloc:alloc_table.
 897   forall intM_u_6:(int,
 898   'a1) memory.
 899   (3 >= 0) ->
 900   forall result:'a1 pointer.
 901   forall alloc0:alloc_table.
 902   (valid(alloc0, result) and
 903    ((offset(result) = 0) and
 904     ((block_length(alloc0, result) = 3) and
 905      (valid_range(alloc0, result, 0, (3 - 1)) and
 906       (fresh(alloc, result) and
 907        (on_stack(alloc0, result) and alloc_extends(alloc, alloc0))))))) ->
 908   forall intM_u_6_0:(int,
 909   'a1) memory.
 910   (intM_u_6_0 = upd(intM_u_6, result, 3)) ->
 911   forall result0:'a1 pointer.
 912   (result0 = shift(result, 1)) ->
 913   forall intM_u_6_1:(int,
 914   'a1) memory.
 915   (intM_u_6_1 = upd(intM_u_6_0, result0, 4)) ->
 916   forall result1:'a1 pointer.
 917   (result1 = shift(result, 2)) ->
 918   forall intM_u_6_2:(int,
 919   'a1) memory.
 920   (intM_u_6_2 = upd(intM_u_6_1, result1, 5)) ->
 921   forall result2:'a1 pointer.
 922   (result2 = shift(result, 0)) ->
 923   forall result3:int.
 924   (result3 = acc(intM_u_6_2, result2)) ->
 925   forall result4:'a1 pointer.
 926   (result4 = shift(result, 1)) ->
 927   forall result5:int.
 928   (result5 = acc(intM_u_6_2, result4)) ->
 929   forall result6:'a1 pointer.
 930   (result6 = shift(result, 2)) ->
 931   valid(alloc0, result6) ->
 932   forall result7:int.
 933   (result7 = acc(intM_u_6_2, result6)) ->
 934   ("CADUCEUS_12": (((result3 + result5) + result7) = 12))
 935
 936 goal invariants_initially_established_impl_po_1:
 937   forall a_s_9:(int,
 938   s_9) memory.
 939   forall alloc:alloc_table.
 940   forall b_s_9:(b_2_10 pointer, s_9) memory.
 941   forall intM_b_2_10:(int, b_2_10) memory.
 942   forall intM_t_7:(int,
 943   t_7) memory.
 944   forall s:s_9 pointer.
 945   forall t:t_7 pointer.
 946   forall x:int.
 947   (("CADUCEUS_14":
 948    ((x = 45) and
 949     ((((acc(intM_t_7, t) = 1) and (acc(intM_t_7, shift(t, 1)) = 2)) and
 950       (acc(intM_t_7, shift(t, 2)) = 3)) and
 951      ((acc(a_s_9, s) = 1) and
 952       (((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 953         shift(acc(b_s_9, s), 1)) = 3)) and
 954        (acc(intM_b_2_10, shift(acc(b_s_9, s), 2)) = 4)))))) and
 955    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 956     (("CADUCEUS_5": valid(alloc, s)) and
 957      (("CADUCEUS_16": valid_acc(b_s_9)) and
 958       ("CADUCEUS_15": valid_acc_range(b_s_9, 3)))))) ->
 959   ("CADUCEUS_17": (acc(intM_t_7, shift(t, 1)) = 2))
 960
 961 goal invariants_initially_established_impl_po_2:
 962   forall a_s_9:(int,
 963   s_9) memory.
 964   forall alloc:alloc_table.
 965   forall b_s_9:(b_2_10 pointer, s_9) memory.
 966   forall intM_b_2_10:(int, b_2_10) memory.
 967   forall intM_t_7:(int,
 968   t_7) memory.
 969   forall s:s_9 pointer.
 970   forall t:t_7 pointer.
 971   forall x:int.
 972   (("CADUCEUS_14":
 973    ((x = 45) and
 974     ((((acc(intM_t_7, t) = 1) and (acc(intM_t_7, shift(t, 1)) = 2)) and
 975       (acc(intM_t_7, shift(t, 2)) = 3)) and
 976      ((acc(a_s_9, s) = 1) and
 977       (((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
 978         shift(acc(b_s_9, s), 1)) = 3)) and
 979        (acc(intM_b_2_10, shift(acc(b_s_9, s), 2)) = 4)))))) and
 980    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
 981     (("CADUCEUS_5": valid(alloc, s)) and
 982      (("CADUCEUS_16": valid_acc(b_s_9)) and
 983       ("CADUCEUS_15": valid_acc_range(b_s_9, 3)))))) ->
 984   ("CADUCEUS_17": (acc(intM_b_2_10, acc(b_s_9, s)) = 1))
 985
 986 goal invariants_initially_established_impl_po_3:
 987   forall a_s_9:(int,
 988   s_9) memory.
 989   forall alloc:alloc_table.
 990   forall b_s_9:(b_2_10 pointer, s_9) memory.
 991   forall intM_b_2_10:(int, b_2_10) memory.
 992   forall intM_t_7:(int,
 993   t_7) memory.
 994   forall s:s_9 pointer.
 995   forall t:t_7 pointer.
 996   forall x:int.
 997   (("CADUCEUS_14":
 998    ((x = 45) and
 999     ((((acc(intM_t_7, t) = 1) and (acc(intM_t_7, shift(t, 1)) = 2)) and
1000       (acc(intM_t_7, shift(t, 2)) = 3)) and
1001      ((acc(a_s_9, s) = 1) and
1002       (((acc(intM_b_2_10, acc(b_s_9, s)) = 1) and (acc(intM_b_2_10,
1003         shift(acc(b_s_9, s), 1)) = 3)) and
1004        (acc(intM_b_2_10, shift(acc(b_s_9, s), 2)) = 4)))))) and
1005    (("CADUCEUS_6": valid_range(alloc, t, 0, 2)) and
1006     (("CADUCEUS_5": valid(alloc, s)) and
1007      (("CADUCEUS_16": valid_acc(b_s_9)) and
1008       ("CADUCEUS_15": valid_acc_range(b_s_9, 3)))))) ->
1009   ("CADUCEUS_17": (acc(intM_b_2_10, shift(acc(b_s_9, s), 2)) = 4))
1010