diff options
Diffstat (limited to 'common/Memtype.v')
| -rw-r--r-- | common/Memtype.v | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/common/Memtype.v b/common/Memtype.v index 59dc7a3..37ab33c 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -88,8 +88,6 @@ Module Type MEM. (** The abstract type of memory states. *) Parameter mem: Type. -Definition nullptr: block := 0. - (** * Operations on memory states *) (** [empty] is the initial memory state. *) @@ -176,11 +174,9 @@ Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), opti block. *) Parameter nextblock: mem -> block. -Axiom nextblock_pos: - forall m, nextblock m > 0. -Definition valid_block (m: mem) (b: block) := - b < nextblock m. +Definition valid_block (m: mem) (b: block) := Plt b (nextblock m). + Axiom valid_not_valid_diff: forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'. @@ -279,7 +275,7 @@ Axiom valid_pointer_implies: (** ** Properties of the initial memory state. *) -Axiom nextblock_empty: nextblock empty = 1. +Axiom nextblock_empty: nextblock empty = 1%positive. Axiom perm_empty: forall b ofs k p, ~perm empty b ofs k p. Axiom valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. @@ -607,7 +603,7 @@ Axiom alloc_result: Axiom nextblock_alloc: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - nextblock m2 = Zsucc (nextblock m1). + nextblock m2 = Psucc (nextblock m1). Axiom valid_block_alloc: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> @@ -640,7 +636,7 @@ Axiom perm_alloc_inv: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> forall b' ofs k p, perm m2 b' ofs k p -> - if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p. + if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p. (** Effect of [alloc] on access validity. *) @@ -1191,7 +1187,7 @@ Axiom drop_outside_inject: (** Memory states that inject into themselves. *) Definition flat_inj (thr: block) : meminj := - fun (b: block) => if zlt b thr then Some(b, 0) else None. + fun (b: block) => if plt b thr then Some(b, 0) else None. Parameter inject_neutral: forall (thr: block) (m: mem), Prop. @@ -1206,14 +1202,14 @@ Axiom alloc_inject_neutral: forall thr m lo hi b m', alloc m lo hi = (m', b) -> inject_neutral thr m -> - nextblock m < thr -> + Plt (nextblock m) thr -> inject_neutral thr m'. Axiom store_inject_neutral: forall chunk m b ofs v m' thr, store chunk m b ofs v = Some m' -> inject_neutral thr m -> - b < thr -> + Plt b thr -> val_inject (flat_inj thr) v v -> inject_neutral thr m'. @@ -1221,7 +1217,7 @@ Axiom drop_inject_neutral: forall m b lo hi p m' thr, drop_perm m b lo hi p = Some m' -> inject_neutral thr m -> - b < thr -> + Plt b thr -> inject_neutral thr m'. End MEM. |