# Library Copland.Term

This module contains the basic definitions for Copland terms, events, and annotated terms.

Require Import Omega Preamble.

# Terms and Evidence

A term is either an atomic ASP, a remote call, a sequence of terms with data a dependency, a sequence of terms with no data dependency, or parallel terms.
Plc represents a place.

Notation Plc := nat (only parsing).

An argument to a userspace or kernel measurement.

Inductive Arg: Set :=
| arg: nat Arg
| pl: Plc Arg.

Definition eq_arg_dec:
x y: Arg, {x = y} + {x y}.
Hint Resolve eq_arg_dec.

Inductive ASP: Set :=
| CPY: ASP
| KIM: (list Arg) ASP
| USM: (list Arg) ASP
| SIG: ASP
| HSH: ASP.

The method by which data is split is specified by a natural number.

Definition Split: Set := (nat × nat).

Inductive Term: Set :=
| asp: ASP Term
| att: Plc Term Term
| lseq: Term Term Term
| bseq: Split Term Term Term
| bpar: Split Term Term Term.

The structure of evidence.

Inductive Evidence: Set :=
| mt: Evidence
| sp: nat Evidence Evidence
| kk: Plc (list Arg) Evidence Evidence
| uu: Plc (list Arg) Evidence Evidence
| gg: Plc Evidence Evidence
| hh: Plc Evidence Evidence
| ss: Evidence Evidence Evidence
| pp: Evidence Evidence Evidence.

Fixpoint eval_asp t p e :=
match t with
| CPYe
| KIM Akk p A e
| USM Auu p A e
| SIGgg p e
| HSHhh p e
end.

The evidence associated with a term, a place, and some initial evidence.

Fixpoint eval t p e :=
match t with
| asp aeval_asp a p e
| att q t1eval t1 q e
| lseq t1 t2eval t2 p (eval t1 p e)
| bseq s t1 t2ss (eval t1 p (sp (fst s) e))
(eval t2 p (sp (snd s) e))
| bpar s t1 t2pp (eval t1 p (sp (fst s) e))
(eval t2 p (sp (snd s) e))
end.

# Events

There are events for each kind of action. This includes ASP actions such as measurement or data processing. It also includes control flow actions: a split occurs when a thread of control splits, and a join occurs when two threads join. Each event is distinguished using a unique natural number.
The natural number used to distinguish evidence.

Definition ev x :=
match x with
| copy i _ _i
| kmeas i _ _ _ _i
| umeas i _ _ _ _i
| sign i _ _ _i
| hash i _ _ _i
| req i _ _ _i
| rpy i _ _ _i
| split i _ _ _ _i
| join i _ _ _ _i
end.

Events are used in a manner that ensures that
e0 e1, ev e0 = ev e1e0 = e1.
See Lemma events_injective.

Definition asp_event i x p e :=
match x with
| CPYcopy i p e
| KIM Akmeas i p A e (eval_asp (KIM A) p e)
| USM Aumeas i p A e (eval_asp (USM A) p e)
| SIGsign i p e (eval_asp SIG p e)
| HSHhash i p e (eval_asp HSH p e)
end.

# Annotated Terms

Annotated terms are used to ensure that each distinct event has a distinct natural number. To do so, each term is annotated by a pair of numbers called a range. Let (i, k) be the label for term t. The labels will be chosen to have the property such that for each event in the set of events associated with term t, its number j will be in the range i j < k.
The number of events associated with a term. The branching terms add a split and a join to the events of their subterms. Similarly, the remote calls add a request and receive to the events of their subterm.

Fixpoint esize t :=
match t with
| aasp _ _ ⇒ 1
| aatt _ _ t1 ⇒ 2 + esize t1
| alseq _ t1 t2esize t1 + esize t2
| abseq _ _ t1 t2 ⇒ 2 + esize t1 + esize t2
| abpar _ _ t1 t2 ⇒ 2 + esize t1 + esize t2
end.

Definition range x :=
match x with
| aasp r _r
| aatt r _ _r
| alseq r _ _r
| abseq r _ _ _r
| abpar r _ _ _r
end.

This function annotates a term. It feeds a natural number throughout the computation so as to ensure each event has a unique natural number.

Fixpoint anno (t: Term) i: nat × AnnoTerm :=
match t with
| asp x(S i, aasp (i, S i) x)
| att p x
let (j, a) := anno x (S i) in
(S j, aatt (i, S j) p a)
| lseq x y
let (j, a) := anno x i in
let (k, b) := anno y j in
(k, alseq (i, k) a b)
| bseq s x y
let (j, a) := anno x (S i) in
let (k, b) := anno y j in
(S k, abseq (i, S k) s a b)
| bpar s x y
let (j, a) := anno x (S i) in
let (k, b) := anno y j in
(S k, abpar (i, S k) s a b)
end.

Lemma anno_range:
x i,
range (snd (anno x i)) = (i, fst (anno x i)).

Definition annotated x :=
snd (anno x 0).

This predicate determines if an annotated term is well formed, that is if its ranges correctly capture the relations between a term and its associated events.

Inductive well_formed: AnnoTerm Prop :=
| wf_asp: r x,
snd r = S (fst r)
well_formed (aasp r x)
| wf_att: r p x,
well_formed x
S (fst r) = fst (range x)
snd r = S (snd (range x))
well_formed (aatt r p x)
| wf_lseq: r x y,
well_formed x well_formed y
fst r = fst (range x)
snd (range x) = fst (range y)
snd r = snd (range y)
well_formed (alseq r x y)
| wf_bseq: r s x y,
well_formed x well_formed y
S (fst r) = fst (range x)
snd (range x) = fst (range y)
snd r = S (snd (range y))
well_formed (abseq r s x y)
| wf_bpar: r s x y,
well_formed x well_formed y
S (fst r) = fst (range x)
snd (range x) = fst (range y)
snd r = S (snd (range y))
well_formed (abpar r s x y).
Hint Constructors well_formed.

Lemma well_formed_range:
t,
well_formed t
snd (range t) = fst (range t) + esize t.

Lemma anno_well_formed:
t i,
well_formed (snd (anno t i)).

Eval for annotated terms.

Fixpoint aeval t p e :=
match t with
| aasp _ xeval (asp x) p e
| aatt _ q xaeval x q e
| alseq _ t1 t2aeval t2 p (aeval t1 p e)
| abseq _ s t1 t2ss (aeval t1 p ((sp (fst s)) e))
(aeval t2 p ((sp (snd s)) e))
| abpar _ s t1 t2pp (aeval t1 p ((sp (fst s)) e))
(aeval t2 p ((sp (snd s)) e))
end.

Lemma eval_aeval:
t p e i,
eval t p e = aeval (snd (anno t i)) p e.

This predicate specifies when a term, a place, and some initial evidence is related to an event. In other words, it specifies the set of events associated with a term, a place, and some initial evidence.

Inductive events: AnnoTerm Plc Evidence Ev Prop :=
| evtscpy:
r i p e,
fst r = i
events (aasp r CPY) p e (copy i p e)
| evtskim:
i r a p e e',
fst r = i
kk p a e = e'
events (aasp r (KIM a)) p e (kmeas i p a e e')
| evtsusm:
i r a p e e',
fst r = i
uu p a e = e'
events (aasp r (USM a)) p e (umeas i p a e e')
| evtssig:
r i p e e',
fst r = i
gg p e = e'
events (aasp r SIG) p e (sign i p e e')
| evtshsh:
r i p e e',
fst r = i
hh p e = e'
events (aasp r HSH) p e (hash i p e e')

| evtsattreq:
r p q t e i,
fst r = i
events (aatt r q t) p e (req i p q e)
| evtsatt:
r p q t e ev,
events t q e ev
events (aatt r q t) p e ev
| evtsattrpy:
r p q t e e' i,
snd r = S i
aeval t q e = e'
events (aatt r q t) p e (rpy i p q e')

| evtslseql:
r t1 t2 p e ev,
events t1 p e ev
events (alseq r t1 t2) p e ev
| evtslseqr:
r t1 t2 p e ev,
events t2 p (aeval t1 p e) ev
events (alseq r t1 t2) p e ev

| evtsbseqsplit:
r i s t1 t2 p e,
fst r = i
events (abseq r s t1 t2) p e
(split i p e (sp (fst s) e) (sp (snd s) e))
| evtsbseql:
r s t1 t2 p e ev,
events t1 p (sp (fst s) e) ev
events (abseq r s t1 t2) p e ev
| evtsbseqr:
r s t1 t2 p e ev,
events t2 p (sp (snd s) e) ev
events (abseq r s t1 t2) p e ev
| evtsbseqjoin:
r i s t1 t2 p e e1 e2,
snd r = S i
aeval t1 p (sp (fst s) e) = e1
aeval t2 p (sp (snd s) e) = e2
events (abseq r s t1 t2) p e
(join i p e1 e2 (ss e1 e2))

| evtsbparsplit:
r i s t1 t2 p e,
fst r = i
events (abpar r s t1 t2) p e
(split i p e (sp (fst s) e) (sp (snd s) e))
| evtsbparl:
r s t1 t2 p e ev,
events t1 p (sp (fst s) e) ev
events (abpar r s t1 t2) p e ev
| evtsbparr:
r s t1 t2 p e ev,
events t2 p (sp (snd s) e) ev
events (abpar r s t1 t2) p e ev
| evtsbparjoin:
r i s t1 t2 p e e1 e2,
snd r = S i
aeval t1 p (sp (fst s) e) = e1
aeval t2 p (sp (snd s) e) = e2
events (abpar r s t1 t2) p e
(join i p e1 e2 (pp e1 e2)).
Hint Constructors events.

Lemma events_range:
t p e v,
well_formed t
events t p e v
fst (range t) ev v < snd (range t).

Lemma at_range:
x r i,
S (fst r) = fst x
snd r = S (snd x)
fst r i < snd r
i = fst r
fst x i < snd x
i = snd x.

Lemma lin_range:
x y i,
snd x = fst y
fst x i < snd y
fst x i < snd x
fst y i < snd y.

Lemma bra_range:
x y r i,
S (fst r) = fst x
snd x = fst y
snd r = S (snd y)
fst r i < snd r
i = fst r
fst x i < snd x
fst y i < snd y
i = snd y.

Properties of events.

Lemma events_range_event:
t p e i,
well_formed t
fst (range t) i < snd (range t)
v, events t p e v ev v = i.

Ltac events_event_range :=
repeat match goal with
| [ H: events _ _ _ _ |- _ ] ⇒
apply events_range in H; auto
end; omega.

Lemma events_injective:
t p e v1 v2,
well_formed t
events t p e v1
events t p e v2
ev v1 = ev v2
v1 = v2.