Every participant mentioned in either conditional body must know the
decision, including forwarding-only roles of a nested choice. No guessing
or implicit merging of unrelated branch schedules is permitted.
96def globalProtocolCovered =
97 (lambda erased operation : Type 0 .
98 (lambda erased payload : Type 0 .
99 (lambda erased decision : Type 0 .
100 (lambda unrestricted known : (pi unrestricted role : Nat . Nat) .
101 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
102 (eliminate
103 GlobalProtocol
104 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
105 Nat)
106 program
107 (branch GlobalProtocolEnd . 1)
108 (branch
109 GlobalProtocolLocal
110 role
111 value
112 rest
113 induction
114 .
115 (naturalAnd (known role) induction))
116 (branch
117 GlobalProtocolTransfer
118 identity
119 value
120 rest
121 induction
122 .
123 (naturalAnd
124 (known (regionTransferSender identity))
125 (naturalAnd (known (regionTransferReceiver identity)) (naturalAnd induction 1))))
126 (branch
127 GlobalProtocolRepeat
128 count
129 body
130 rest
131 bodyCheck
132 restCheck
133 .
134 (naturalAnd bodyCheck restCheck))
135 (branch
136 GlobalProtocolChoice
137 identity
138 selector
139 announcements
140 zeroBody
141 oneBody
142 rest
143 zeroCheck
144 oneCheck
145 restCheck
146 .
147 (naturalAnd
148 (known (regionTransferSender identity))
149 (naturalAnd
150 (eliminate
151 ProtocolAnnouncements
152 (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
153 announcements
154 (branch ProtocolAnnouncementsEnd . 1)
155 (branch
156 ProtocolAnnouncementsNext
157 edge
158 value
159 tail
160 induction
161 .
162 (naturalAnd
163 (known (regionTransferSender edge))
164 (naturalAnd
165 (known (regionTransferReceiver edge))
166 (naturalAnd induction 1)))))
167 (naturalAnd zeroCheck (naturalAnd oneCheck (naturalAnd restCheck 1))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.