Molly/Role.v at main · dandougherty/Molly · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
(* Time-stamp: <Wed 11/22/23 11:24 Dan Dougherty Role.v> *)

From Coq Require Export List Bool Arith.
Export ListNotations.

From RC Require Import
  CpdtTactics
  Utilities
  ListUtil
  Decidability
  Sorts
  Act
  Term
  Subterms
  (* Runtime *)
.


(** * Roles *)

(** A Role is a list of Actions (inputs, outputs, sends and receives)
    specified by Terms
*)

Definition Role :=  list (Act Term).

(** * Utilities *)

(** Extract the Terms in an action *)
Definition act_term_msg (e: Act Term): list Term :=
 match e with
     | Prm x => [x]
     | Ret x => [x]
     | Snd x1 x2 => [x1 ; x2]
     | Rcv x1 x2 => [x1 ; x2]
     end.

(** duplicates ok here *)
Fixpoint act_term_msgs (rl: Role): Terms :=
  match rl with
  | [] => []
  | a :: rest => act_term_msg a ++ act_term_msgs rest
 end.

(** Extract the Terms in a role *)
Definition terms_of_role (rl : Role): list Term :=
  nodup Term_eq_dec (act_term_msgs rl).

(** This will be the "universe" of Terms during compilation *)

Definition Subterms_of_role (rl : Role): list Term :=
  Subterms (terms_of_role rl).


(* ================================== *)

(** ** The Qt terms of a Role *)

(** need these for initialization *)

Definition quote_terms_in_role (rl: Role) : Terms :=
  filter is_quote (Subterms_of_role rl).

(* ---------------------------------------------- *)
(** ** Positive-polarity Terms *)

(** These are the elementary Terms that are constructed by the role.
    That is, if the first occurrence of an elementary term in in a
    send, it is counted here.

    We don't exclude outputs, although that would be anomalous in a
    protocol.

   Positive polarity is not the same as originating since subterms of
   keys are included in pos_pol.

    Implementation: a helper function accumulates all elementary terms
    seen so far paired with those that are first seen in a send or
    output.

    We don't bother about duplicates until later.  *)

Fixpoint pos_pol_helper (acc: Terms*Terms) (evts: list (Act Term))
  :=
  match evts with
    [] => acc

  | Rcv c t :: rest =>
      pos_pol_helper
        (Term.elems_of_terms [c;t] ++ fst acc,
          snd acc)
        rest

  | Prm t :: rest =>
      pos_pol_helper
        (Term.elems_of_terms [t] ++ fst acc,
          snd acc)
        rest

  | Snd c t :: rest =>
      pos_pol_helper
        (* all elems get added to the fst *)
        (Term.elems_of_terms (fst acc) ++ [c;t] ,
          (* add to the snd if new  *)
          ListUtil.guarded_add (fst acc) (Term.elems_of_terms [t]) (snd acc))
        rest

  | Ret t :: rest =>
      pos_pol_helper
        (* all elems get added to the fst *)
        (Term.elems_of_terms (fst acc) ++ [t] ,
          (* add to the snd if new  *)
          ListUtil.guarded_add
            (fst acc)
            (Term.elems_of_terms [t])
            (snd acc))
        rest


  end.

(** Be careful to exclude inputs.
    We remove dups here *)
Definition pos_pol_in_role (rl: Role) : Terms :=
  nodup Term_eq_dec
    (snd (pos_pol_helper
          ([], []) rl)).