A received frame is consumed before its value can control local work. A
forwarder reuses that installed value, never its own selector. Each edge
advances its own invocation version, so repeats and nested choices retain
replay protection without introducing another native repeat frame.
172def nativeProtocolAnnouncements =
173 (lambda erased decision : Type 0 .
174 (lambda erased payload : Type 0 .
175 (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
176 (lambda unrestricted selector : decision .
177 (lambda unrestricted role : Nat .
178 (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
179 (lambda unrestricted label : Bytes .
180 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
181 (eliminate
182 ProtocolAnnouncements
183 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
184 (pi unrestricted tail : (family NativePhysicalCommands) .
185 (family NativePhysicalCommands)))
186 announcements
187 (branch
188 ProtocolAnnouncementsEnd
189 .
190 (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
191 (branch
192 ProtocolAnnouncementsNext
193 identity
194 value
195 rest
196 induction
197 .
198 (lambda unrestricted tail : (family NativePhysicalCommands) .
199 (let unrestricted frame =
200 (nativeProtocolDecisionFrame decision payload binding value)
201 in
202 (let unrestricted state =
203 (nativeProtocolDecisionState decision payload binding selector)
204 in
205 (nat-eliminate
206 (lambda unrestricted flag : Nat . (family NativePhysicalCommands))
207 (transfer
208 (constructor ProtocolDirection ProtocolReceive)
209 identity
210 value
211 (nativeFrameConsume
212 frame
213 (nativeMemoryStoreWord64
214 label
215 state
216 (nativeMemoryLoad (framePayloadAt frame))
217 (nativeProtocolRequireDecision
218 (nativeMemoryLoad state)
219 label
220 (nativeFrameAdvance
221 frame
222 (constructor NativeFrameTerminal NativeFrameConsumeComplete)
223 (nativeProtocolDecisionScratch decision payload binding)
224 (induction tail))))))
225 (lambda unrestricted prior : Nat .
226 (lambda unrestricted ignored : (family NativePhysicalCommands) .
227 (nativeMemoryStoreWord64
228 label
229 (framePayloadAt frame)
230 (nativeMemoryLoad state)
231 (transfer
232 (constructor ProtocolDirection ProtocolSend)
233 identity
234 value
235 (nativeFrameAdvance
236 frame
237 (constructor NativeFrameTerminal NativeFrameSendComplete)
238 (nativeProtocolDecisionScratch decision payload binding)
239 (induction tail))))))
240 (naturalEqual role (regionTransferSender identity))))))))))))))))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.