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
  | CPY ⇒ e
  | KIM A ⇒ kk p A e
  | USM A ⇒ uu p A e
  | SIG ⇒ gg p e
  | HSH ⇒ hh p e
  end.

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

Fixpoint eval t p e :=
  match t with
  | asp a ⇒ eval_asp a p e
  | att q t1 ⇒ eval t1 q e
  | lseq t1 t2 ⇒ eval t2 p (eval t1 p e)
  | bseq s t1 t2 ⇒ ss (eval t1 p (sp (fst s) e))
                       (eval t2 p (sp (snd s) e))
  | bpar s t1 t2 ⇒ pp (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.

Inductive Ev: Set :=
| copy: nat → Plc → Evidence → Ev
| kmeas: nat → Plc → (list Arg) → Evidence → Evidence → Ev
| umeas: nat → Plc → (list Arg) → Evidence → Evidence → Ev
| sign: nat → Plc → Evidence → Evidence → Ev
| hash: nat → Plc → Evidence → Evidence → Ev
| req: nat → Plc → Plc → Evidence → Ev
| rpy: nat → Plc → Plc → Evidence → Ev
| split: nat → Plc → Evidence → Evidence → Evidence → Ev
| join: nat → Plc → Evidence → Evidence → Evidence → Ev.

Definition eq_ev_dec:
  ∀ x y: Ev, {x = y} + {x ≠ y}.
Hint Resolve eq_ev_dec.

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 e1 → e0 = e1.
See Lemma events_injective.

Definition asp_event i x p e :=
  match x with
  | CPY ⇒ copy i p e
  | KIM A ⇒ kmeas i p A e (eval_asp (KIM A) p e)
  | USM A ⇒ umeas i p A e (eval_asp (USM A) p e)
  | SIG ⇒ sign i p e (eval_asp SIG p e)
  | HSH ⇒ hash 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.

Definition Range: Set := nat × nat.


Inductive AnnoTerm: Set :=
| aasp: Range → ASP → AnnoTerm
| aatt: Range → Plc → AnnoTerm → AnnoTerm
| alseq: Range → AnnoTerm → AnnoTerm → AnnoTerm
| abseq: Range → Split → AnnoTerm → AnnoTerm → AnnoTerm
| abpar: Range → Split → AnnoTerm → AnnoTerm → AnnoTerm.

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 t2 ⇒ esize 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 _ x ⇒ eval (asp x) p e
  | aatt _ q x ⇒ aeval x q e
  | alseq _ t1 t2 ⇒ aeval t2 p (aeval t1 p e)
  | abseq _ s t1 t2 ⇒ ss (aeval t1 p ((sp (fst s)) e))
                          (aeval t2 p ((sp (snd s)) e))
  | abpar _ s t1 t2 ⇒ pp (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.