(* This file was originally generated by why.
It can be modified; only the generated parts will be overwritten. *)
theory caduceus_why = Main:
typedecl addr;
typedecl pointer;
typedecl alloc_table;
typedecl 'a memory;
typedecl assign_loc;
(*Why logic*) consts bw_compl :: "[int] => int";
(*Why logic*) consts bw_and :: "[int, int] => int";
(*Why logic*) consts bw_xor :: "[int, int] => int";
(*Why logic*) consts bw_or :: "[int, int] => int";
(*Why logic*) consts lsl :: "[int, int] => int";
(*Why logic*) consts lsr :: "[int, int] => int";
(*Why*) consts null :: "pointer";
(*Why logic*) consts block_length :: "[alloc_table, pointer] => int";
(*Why logic*) consts base_addr :: "[pointer] => addr";
(*Why logic*) consts offset :: "[pointer] => int";
(*Why logic*) consts shift :: "[pointer, int] => pointer";
(*Why logic*) consts sub_pointer :: "[pointer, pointer] => int";
(*Why predicate*) constdefs lt_pointer :: "[pointer, pointer] => bool"
"lt_pointer p1
p2 == (((base_addr p1) = (base_addr p2)) & ((offset p1) < (offset p2)))";
(*Why predicate*) constdefs le_pointer :: "[pointer, pointer] => bool"
"le_pointer p1
p2 == (((base_addr p1) = (base_addr p2)) & ((offset p1) <= (offset p2)))";
(*Why predicate*) constdefs gt_pointer :: "[pointer, pointer] => bool"
"gt_pointer p1
p2 == (((base_addr p1) = (base_addr p2)) & ((offset p2) < (offset p1)))";
(*Why predicate*) constdefs ge_pointer :: "[pointer, pointer] => bool"
"ge_pointer p1
p2 == (((base_addr p1) = (base_addr p2)) & ((offset p2) <= (offset p1)))";
(*Why predicate*) constdefs valid :: "[alloc_table, pointer] => bool"
"valid a p == ((0 <= (offset p)) & ((offset p) < (block_length a p)))";
(*Why predicate*) constdefs valid_index :: "[alloc_table, pointer,
int] => bool"
"valid_index a p
i == ((0 <= ((offset p) + i)) & (((offset p) + i) < (block_length a p)))";
(*Why predicate*) constdefs valid_range :: "[alloc_table, pointer, int,
int] => bool"
"valid_range a p i
j == ((0 <= ((offset p) + i)) &
((i <= j) & (((offset p) + j) < (block_length a p))))";
(*Why axiom*) axioms offset_shift: "((!p::pointer.
((!i::int.
((offset (shift p i)) =
((offset p) + i))))))";
(*Why axiom*) axioms shift_zero: "((!p::pointer. ((shift p 0) = p)))";
(*Why axiom*) axioms shift_shift: "((!p::pointer.
((!i::int.
((!j::int.
((shift (shift p i) j) =
(shift p (i + j)))))))))";
(*Why axiom*) axioms base_addr_shift: "((!p::pointer.
((!i::int.
((base_addr (shift p i)) =
(base_addr p))))))";
(*Why axiom*) axioms block_length_shift: "((!a::alloc_table.
((!p::pointer.
((!i::int.
((block_length a (shift p i)) =
(block_length a p))))))))";
(*Why axiom*) axioms base_addr_block_length: "((!a::alloc_table.
((!p1::pointer.
((!p2::pointer.
(((base_addr p1) =
(base_addr p2)) -->
((block_length a p1) =
(block_length a p2)))))))))";
(*Why axiom*) axioms pointer_pair_1: "((!p1::pointer.
((!p2::pointer.
((((base_addr p1) = (base_addr p2)) &
((offset p1) = (offset p2))) -->
(p1 = p2))))))";
(*Why axiom*) axioms pointer_pair_2: "((!p1::pointer.
((!p2::pointer.
((p1 = p2) -->
(((base_addr p1) = (base_addr p2)) &
((offset p1) = (offset p2))))))))";
(*Why axiom*) axioms neq_base_addr_neq_shift: "((!p1::pointer.
((!p2::pointer.
((!i::int.
((!j::int.
(~((base_addr p1) =
(base_addr p2)) -->
~((shift p1 i) =
(shift p2 j)))))))))))";
(*Why axiom*) axioms neq_offset_neq_shift: "((!p1::pointer.
((!p2::pointer.
((!i::int.
((!j::int.
(~(((offset p1) + i) =
((offset p2) + j)) -->
~((shift p1 i) =
(shift p2 j)))))))))))";
(*Why axiom*) axioms eq_offset_eq_shift: "((!p1::pointer.
((!p2::pointer.
((!i::int.
((!j::int.
(((base_addr p1) =
(base_addr p2)) -->
((((offset p1) + i) =
((offset p2) + j)) -->
((shift p1 i) = (shift p2 j))))))))))))";
(*Why axiom*) axioms valid_index_valid_shift: "((!a::alloc_table.
((!p::pointer.
((!i::int.
((valid_index a p i) -->
(valid a (shift p i)))))))))";
(*Why axiom*) axioms valid_range_valid_shift: "((!a::alloc_table.
((!p::pointer.
((!i::int.
((!j::int.
((!k::int.
((valid_range a p i j) -->
(((i <= k) & (k <= j)) -->
(valid a (shift p k))))))))))))))";
(*Why axiom*) axioms valid_range_valid: "((!a::alloc_table.
((!p::pointer.
((!i::int.
((!j::int.
((valid_range a p i j) -->
(((i <= 0) & (0 <= j)) -->
(valid a p)))))))))))";
(*Why axiom*) axioms valid_range_valid_index: "((!a::alloc_table.
((!p::pointer.
((!i::int.
((!j::int.
((!k::int.
((valid_range a p i j) -->
(((i <= k) & (k <= j)) -->
(valid_index a p k)))))))))))))";
(*Why axiom*) axioms sub_pointer_def: "((!p1::pointer.
((!p2::pointer.
(((base_addr p1) = (base_addr p2)) -->
((sub_pointer p1 p2) =
((offset p1) - (offset p2))))))))";
(*Why logic*) consts acc :: "[('a43 memory), pointer] => 'a43";
(*Why logic*) consts upd :: "[('a44 memory), pointer, 'a44] => ('a44 memory)";
(*Why axiom*) axioms acc_upd: "((!m::('a45 memory).
((!p::pointer.
((!a::'a45. ((acc (upd m p a) p) = a)))))))";
(*Why axiom*) axioms acc_upd_eq: "((!m::('a46 memory).
((!p1::pointer.
((!p2::pointer.
((!a::'a46.
((p1 = p2) -->
((acc (upd m p1 a) p2) = a))))))))))";
(*Why axiom*) axioms acc_upd_neq: "((!m::('a47 memory).
((!p1::pointer.
((!p2::pointer.
((!a::'a47.
(~(p1 = p2) -->
((acc (upd m p1 a) p2) = (acc m p2)))))))))))";
(*Why axiom*) axioms false_not_true: "~(F = T)";
typedecl pset;
(*Why logic*) consts pset_empty :: "pset";
(*Why logic*) consts pset_singleton :: "[pointer] => pset";
(*Why logic*) consts pset_star :: "[pset, (pointer memory)] => pset";
(*Why logic*) consts pset_all :: "[pset] => pset";
(*Why logic*) consts pset_range :: "[pset, int, int] => pset";
(*Why logic*) consts pset_range_left :: "[pset, int] => pset";
(*Why logic*) consts pset_range_right :: "[pset, int] => pset";
(*Why logic*) consts pset_acc_all :: "[pset, (pointer memory)] => pset";
(*Why logic*) consts pset_acc_range ::
"[pset, (pointer memory), int, int] => pset";
(*Why logic*) consts pset_acc_range_left ::
"[pset, (pointer memory), int] => pset";
(*Why logic*) consts pset_acc_range_right ::
"[pset, (pointer memory), int] => pset";
(*Why logic*) consts pset_union :: "[pset, pset] => pset";
(*Why logic*) consts not_in_pset :: "[pointer, pset] => bool";
(*Why predicate*) constdefs not_assigns :: "[alloc_table, ('a48 memory),
('a48 memory), pset] => bool"
"not_assigns a m1 m2
l == ((!p::pointer.
((valid a p) --> ((not_in_pset p l) --> ((acc m2 p) = (acc m1 p))))))";
(*Why axiom*) axioms pset_empty_intro: "((!p::pointer.
(not_in_pset p pset_empty)))";
(*Why axiom*) axioms pset_singleton_intro: "((!p1::pointer.
((!p2::pointer.
(~(p1 = p2) -->
(not_in_pset p1
(pset_singleton p2)))))))";
(*Why axiom*) axioms pset_singleton_elim: "((!p1::pointer.
((!p2::pointer.
((not_in_pset p1
(pset_singleton p2)) -->
~(p1 = p2))))))";
(*Why axiom*) axioms not_not_in_singleton: "((!p::pointer.
~((not_in_pset p
(pset_singleton p)))))";
(*Why axiom*) axioms pset_union_intro: "((!l1::pset.
((!l2::pset.
((!p::pointer.
(((not_in_pset p l1) &
(not_in_pset p l2)) -->
(not_in_pset p
(pset_union l1 l2)))))))))";
(*Why axiom*) axioms pset_union_elim1: "((!l1::pset.
((!l2::pset.
((!p::pointer.
((not_in_pset p
(pset_union l1 l2)) -->
(not_in_pset p l1))))))))";
(*Why axiom*) axioms pset_union_elim2: "((!l1::pset.
((!l2::pset.
((!p::pointer.
((not_in_pset p
(pset_union l1 l2)) -->
(not_in_pset p l2))))))))";
(*Why axiom*) axioms pset_star_intro: "((!l::pset.
((!m::(pointer memory).
((!p::pointer.
(((!p1::pointer.
((p = (acc m p1)) -->
(not_in_pset p1 l)))) -->
(not_in_pset p (pset_star l m)))))))))";
(*Why axiom*) axioms pset_star_elim: "((!l::pset.
((!m::(pointer memory).
((!p::pointer.
((not_in_pset p (pset_star l m)) -->
((!p1::pointer.
((p = (acc m p1)) -->
(not_in_pset p1 l)))))))))))";
(*Why axiom*) axioms pset_all_intro: "((!p::pointer.
((!l::pset.
(((!p1::pointer.
(~((not_in_pset p1 l)) -->
~((base_addr p) = (base_addr p1))))) -->
(not_in_pset p (pset_all l)))))))";
(*Why axiom*) axioms pset_all_elim: "((!p::pointer.
((!l::pset.
((not_in_pset p (pset_all l)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
~((base_addr p) = (base_addr p1))))))))))";
(*Why axiom*) axioms pset_range_intro: "((!p::pointer.
((!l::pset.
((!a::int.
((!b::int.
(((!p1::pointer.
((not_in_pset p1 l) |
((!i::int.
(((a <= i) & (i <= b)) -->
~(p = (shift p1 i)))))))) -->
(not_in_pset p
(pset_range l a b)))))))))))";
(*Why axiom*) axioms pset_range_elim: "((!p::pointer.
((!l::pset.
((!a::int.
((!b::int.
((not_in_pset p
(pset_range l a b)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
(((a <= i) & (i <= b)) -->
~((shift p1 i) = p))))))))))))))))";
(*Why axiom*) axioms pset_range_left_intro: "((!p::pointer.
((!l::pset.
((!a::int.
(((!p1::pointer.
((not_in_pset p1 l) |
((!i::int.
((i <= a) -->
~(p = (shift p1 i)))))))) -->
(not_in_pset p
(pset_range_left l a)))))))))";
(*Why axiom*) axioms pset_range_left_elim: "((!p::pointer.
((!l::pset.
((!a::int.
((not_in_pset p
(pset_range_left l a)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
((i <= a) -->
~((shift p1 i) = p))))))))))))))";
(*Why axiom*) axioms pset_range_right_intro: "((!p::pointer.
((!l::pset.
((!a::int.
(((!p1::pointer.
((not_in_pset p1 l) |
((!i::int.
((a <= i) -->
~(p = (shift p1 i)))))))) -->
(not_in_pset p
(pset_range_right l a)))))))))";
(*Why axiom*) axioms pset_range_right_elim: "((!p::pointer.
((!l::pset.
((!a::int.
((not_in_pset p
(pset_range_right l a)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
((a <= i) -->
~((shift p1 i) = p))))))))))))))";
(*Why axiom*) axioms pset_acc_all_intro: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
(((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
~(p = (acc m (shift p1 i)))))))) -->
(not_in_pset p
(pset_acc_all l m)))))))))";
(*Why axiom*) axioms pset_acc_all_elim: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((not_in_pset p
(pset_acc_all l m)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
~((acc m (shift p1 i)) = p)))))))))))))";
(*Why axiom*) axioms pset_acc_range_intro: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((!a::int.
((!b::int.
(((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
(((a <= i) & (i <= b)) -->
~(p =
(acc m (shift p1 i))))))))) -->
(not_in_pset p
(pset_acc_range l m a b)))))))))))))";
(*Why axiom*) axioms pset_acc_range_elim: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((!a::int.
((!b::int.
((not_in_pset p
(pset_acc_range l m a b)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
(((a <= i) & (i <= b)) -->
~((acc m (shift p1 i)) =
p))))))))))))))))))";
(*Why axiom*) axioms pset_acc_range_left_intro: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((!a::int.
(((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
((i <= a) -->
~(p =
(acc m
(shift p1 i))))))))) -->
(not_in_pset p
(pset_acc_range_left l
m a)))))))))))";
(*Why axiom*) axioms pset_acc_range_left_elim: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((!a::int.
((not_in_pset p
(pset_acc_range_left l m
a)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
((i <= a) -->
~((acc m
(shift p1 i)) =
p))))))))))))))))";
(*Why axiom*) axioms pset_acc_range_right_intro: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((!a::int.
(((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
((a <= i) -->
~(p =
(acc m
(shift p1 i))))))))) -->
(not_in_pset p
(pset_acc_range_right
l m a)))))))))))";
(*Why axiom*) axioms pset_acc_range_right_elim: "((!p::pointer.
((!l::pset.
((!m::(pointer memory).
((!a::int.
((not_in_pset p
(pset_acc_range_right l
m a)) -->
((!p1::pointer.
(~((not_in_pset p1 l)) -->
((!i::int.
((a <= i) -->
~((acc m
(shift p1 i)) =
p))))))))))))))))";
(*Why axiom*) axioms not_assigns_trans: "((!a::alloc_table.
((!l::pset.
((!m1::('a49 memory).
((!m2::('a49 memory).
((!m3::('a49 memory).
((not_assigns a m1 m2 l) -->
((not_assigns a m2 m3 l) -->
(not_assigns a m1 m3 l)))))))))))))";
(*Why axiom*) axioms not_assigns_refl: "((!a::alloc_table.
((!l::pset.
((!m::('a50 memory).
(not_assigns a m m l)))))))";
(*Why predicate*) constdefs valid1 :: "[(pointer memory)] => bool"
"valid1 m1 == ((!p::pointer.
((!a::alloc_table.
((valid a p) --> (valid a (acc m1 p)))))))";
(*Why predicate*) constdefs valid1_range :: "[(pointer memory), int] => bool"
"valid1_range m1
xsize == ((!p::pointer.
((!a::alloc_table.
((valid a p) --> (valid_range a (acc m1 p) 0 (xsize - 1)))))))";
(*Why predicate*) constdefs separation1 :: "[(pointer memory),
(pointer memory)] => bool"
"separation1 m1
m2 == ((!p::pointer.
((!a::alloc_table.
((valid a p) --> ~((base_addr (acc m1 p)) = (base_addr (acc m2 p))))))))";
(*Why predicate*) constdefs separation1_range1 :: "[(pointer memory),
(pointer memory),
int] => bool"
"separation1_range1 m1 m2
xsize == ((!p::pointer.
((!a::alloc_table.
((valid a p) -->
((!i::int.
(((0 <= i) & (i < xsize)) -->
~((base_addr (acc m1 (shift p i))) = (base_addr (acc m2 p)))))))))))";
(*Why predicate*) constdefs separation1_range :: "[(pointer memory),
int] => bool"
"separation1_range m
xsize == ((!p::pointer.
((!a::alloc_table.
((valid a p) -->
((!i1::int.
((!i2::int.
(((0 <= i1) & (i1 < xsize)) -->
(((0 <= i2) & (i2 < xsize)) -->
(~(i1 = i2) -->
~((base_addr (acc m (shift p i1))) =
(base_addr (acc m (shift p i2))))))))))))))))";
(*Why predicate*) constdefs separation2 :: "[(pointer memory),
(pointer memory)] => bool"
"separation2 m1
m2 == ((!p1::pointer.
((!p2::pointer.
((!a::alloc_table.
(~(p1 = p2) -->
~((base_addr (acc m1 p1)) = (base_addr (acc m2 p2))))))))))";
(*Why predicate*) constdefs separation2_range1 :: "[(pointer memory),
(pointer memory),
int] => bool"
"separation2_range1 m1 m2
xsize == ((!p::pointer.
((!q::pointer.
((!a::alloc_table.
((!i::int.
(((0 <= i) & (i < xsize)) -->
~((base_addr (acc m1 (shift p i))) = (base_addr (acc m2 q))))))))))))";
(*Why logic*) consts on_heap :: "[alloc_table, pointer] => bool";
(*Why logic*) consts on_stack :: "[alloc_table, pointer] => bool";
(*Why logic*) consts fresh :: "[alloc_table, pointer] => bool";
(*Why axiom*) axioms fresh_not_valid: "((!a::alloc_table.
((!p::pointer.
((fresh a p) -->
((!i::int.
~((valid a (shift p i))))))))))";
(*Why logic*) consts alloc_stack ::
"[pointer, alloc_table, alloc_table] => bool";
(*Why axiom*) axioms alloc_stack_p: "((!p::pointer.
((!a1::alloc_table.
((!a2::alloc_table.
((alloc_stack p a1 a2) -->
(valid a2 p))))))))";
(*Why axiom*) axioms alloc_stack_valid: "((!p::pointer.
((!a1::alloc_table.
((!a2::alloc_table.
((alloc_stack p a1 a2) -->
((!q::pointer.
((valid a1 q) --> (valid a2 q)))))))))))";
(*Why axiom*) axioms alloc_stack_valid_range: "((!p::pointer.
((!a1::alloc_table.
((!a2::alloc_table.
((alloc_stack p a1 a2) -->
((!q::pointer.
((!i::int.
((!j::int.
((valid_range a1 q i j) -->
(valid_range a2 q i j)))))))))))))))";
(*Why logic*) consts free_heap ::
"[pointer, alloc_table, alloc_table] => bool";
(*Why logic*) consts free_stack ::
"[alloc_table, alloc_table, alloc_table] => bool";
(*Why axiom*) axioms free_stack_heap: "((!a1::alloc_table.
((!a2::alloc_table.
((!a3::alloc_table.
((free_stack a1 a2 a3) -->
((!p::pointer.
((valid a2 p) -->
((on_heap a2 p) --> (valid a3 p))))))))))))";
(*Why axiom*) axioms free_stack_stack: "((!a1::alloc_table.
((!a2::alloc_table.
((!a3::alloc_table.
((free_stack a1 a2 a3) -->
((!p::pointer.
((valid a1 p) -->
((on_stack a1 p) -->
(valid a3 p))))))))))))";
end
