Definition of actions


Require Import Vbase.
Set Implicit Arguments.

Definition actid := nat.

Inductive act :=
  | Askip
  | Aload (l : nat) (v : nat)
  | Astore (l : nat) (v : nat)
  | Armw (l : nat) (v v': nat).

The function loc a returns the location accessed by action a. If a is not an access, it returns a bogus location.

Definition loc a :=
  match a with
    | Askip ⇒ 0
    | Aload l _
    | Astore l _
    | Armw l _ _l
  end.

Definition is_access a :=
  match a with
    | Aload _ _ | Astore _ _ | Armw _ _ _true
    | Askipfalse
  end.

A read is either a load or a read-modify-write action.

Definition is_read a :=
  match a with
    | Aload _ _ | Armw _ _ _true
    | _false
  end.

Definition is_readL a l :=
  match a with
    | Aload l' _
    | Armw l' _ _l' = l
    | _False
  end.

Definition is_readLV a l v :=
  match a with
    | Aload l' v'
    | Armw l' v' _l' = l v' = v
    | _False
  end.

Definition is_read_only a :=
  match a with
    | Askipfalse
    | Aload _ _true
    | Armw _ _ _false
    | Astore _ _false
  end.

A write is either a store or a read-modify-write action.

Definition is_write a :=
  match a with
    | Astore _ _ | Armw _ _ _true
    | _false
  end.

Definition is_writeL a l :=
  match a with
    | Astore l' _
    | Armw l' _ _l' = l
    | _False
  end.

Definition is_writeLV a l v :=
  match a with
    | Astore l' v'
    | Armw l' _ v'l' = l v' = v
    | _False
  end.

Definition is_write_only a :=
    match a with
    | Askipfalse
    | Aload _ _false
    | Armw _ _ _false
    | Astore _ _true
  end.

Definition is_rmw a :=
  match a with
    | Armw _ _ _true
    | _false
  end.

Lemma is_rmwE a : is_rmw a is_read a is_write a.
Proof. destruct a; ins; intuition. Qed.


Lemmas about access types


Lemma is_readLV_rmw_writeL a l v : is_readLV a l v is_rmw a is_writeL a l.
Proof. by destruct a; ins; desf. Qed.

Lemma is_readL_rmw_writeL a l : is_readL a l is_rmw a is_writeL a l.
Proof. by destruct a; ins; desf. Qed.

Lemma is_writeLV_writeL a l v : is_writeLV a l v is_writeL a l.
Proof. by destruct a; ins; desf. Qed.

Lemmas deriving is_readL.

Lemma is_writeLV_rmw_readL a l v : is_writeLV a l v is_rmw a is_readL a l.
Proof. by destruct a; ins; desf. Qed.

Lemma is_writeL_rmw_readL a l : is_writeL a l is_rmw a is_readL a l.
Proof. by destruct a; ins; desf. Qed.

Lemma is_readLV_readL a l v : is_readLV a l v is_readL a l.
Proof. by destruct a; ins; desf. Qed.

Lemmas deriving is_write.

Lemma is_rmw_write :
   a, is_rmw a is_write a.
Proof. by destruct a; ins; desf. Qed.

Lemma is_writeLV_write :
   a l v, is_writeLV a l v is_write a.
Proof. by destruct a; ins; desf. Qed.

Lemma is_writeL_write :
   a l, is_writeL a l is_write a.
Proof. by destruct a; ins; desf. Qed.

Lemmas deriving is_read.

Lemma is_rmw_read :
   a, is_rmw a is_read a.
Proof. by destruct a; ins; desf. Qed.

Lemma is_readLV_read :
   a l v, is_readLV a l v is_read a.
Proof. by destruct a; ins; desf. Qed.

Lemma is_readL_read :
   a l, is_readL a l is_read a.
Proof. by destruct a; ins; desf. Qed.

Lemma is_readL_loc x l: is_readL x l loc x = l.
Proof. by destruct x; ins; desf. Qed.

Lemma is_writeL_loc x l: is_writeL x l loc x = l.
Proof. by destruct x; ins; desf. Qed.

Lemma is_readLV_loc x l v: is_readLV x l v loc x = l.
Proof. by destruct x; ins; desf. Qed.

Lemma is_writeLV_loc x l v: is_writeLV x l v loc x = l.
Proof. by destruct x; ins; desf. Qed.

Hint Resolve
  is_writeLV_writeL is_readLV_readL
  is_writeL_write is_writeLV_write is_rmw_write
  is_readL_read is_readLV_read is_rmw_read
  is_readL_loc is_writeL_loc
  is_readLV_loc is_writeLV_loc : caccess.

Lemma is_write_access a : is_write a is_access a.
Proof. by destruct a. Qed.

Lemma is_read_access a : is_read a is_access a.
Proof. by destruct a. Qed.

Lemma is_writeL_access a l : is_writeL a l is_access a.
Proof. by destruct a. Qed.

Lemma is_readL_access a l : is_readL a l is_access a.
Proof. by destruct a. Qed.

Lemma is_readLV_access a l v : is_readLV a l v is_access a.
Proof. by destruct a. Qed.

Hint Resolve is_read_access is_readL_access is_readLV_access
             is_write_access is_writeL_access : caccess.

Lemma is_read_only_access a : is_read_only a is_access a.
Proof. by destruct a. Qed.

Lemma is_write_only_access a : is_write_only a is_access a.
Proof. by destruct a. Qed.

Lemma is_read_only_read a : is_read_only a is_read a.
Proof. by destruct a. Qed.

Lemma is_write_only_write a : is_write_only a is_write a.
Proof. by destruct a. Qed.

Hint Resolve is_read_only_read is_read_only_access
     is_write_only_write is_write_only_access : caccess.


This page has been generated by coqdoc