1module Runtime.RegionFrame
2
3import Runtime.RegionTransfer
4import Learning.Transition
5import Representation.Partition
6import Data.Bytes
7import Data.SHA256
8import Data.SHA256Digest
9import Model.Parameter
10import Model.Word64
11import Std.Foundation
12import Std.List
13import Std.Natural
14
15family RegionFrameFailure : Type 0
16constructor RegionFrameBounds
17constructor RegionFrameWrongHeader
18constructor RegionFrameWrongExtent
19constructor RegionFrameWrongDigest
20constructor RegionFrameHashUnavailable
21constructor RegionFrameWrongPhase
22
23end-family
24
25-- A scheduled receive already knows every identity and extent. It must compare
26-- this canonical header before receiving the body into its admitted staging
27-- region. No length, address, allocation or route is taken from peer bytes.
28-- Version 1: magic/version, payload extent, four length-prefixed identities,
29-- epoch, state version, operation, sender, receiver, interval begin/end. Words
30-- are unsigned little-endian 64-bit. The trailer hashes header AND payload.
31-- SHA-256 detects corruption; it does not authenticate an untrusted peer.
32def regionFrameMagic =
33 (bytes-append b"ALPXFER" (bytes 1))
34
35def regionFrameWordLimit : Nat =
36 18446744073709551615
37
38def regionFrameDigestBytes : Nat =
39 32
40
41def regionFrameWord =
42 (lambda unrestricted n : Nat . (dataBytesWord64LE (modelWord64FromNaturalTruncated n)))
43
44def regionFrameSuccess =
45 (lambda unrestricted value : Bytes .
46 (constructor StdResult StdSuccess (family RegionFrameFailure) Bytes value))
47
48def regionFrameFailure =
49 (lambda unrestricted code : (family RegionFrameFailure) .
50 (constructor StdResult StdFailure (family RegionFrameFailure) Bytes code))
51
52-- Delaying the continuation makes bounds checks precede copying and hashing
53-- in a strict native realization, as well as in the lazy checker.
54def regionFrameRequire =
55 (lambda unrestricted flag : Nat .
56 (lambda unrestricted code : (family RegionFrameFailure) .
57 (lambda unrestricted next : (pi unrestricted unit : Nat . (family StdResult (family RegionFrameFailure) Bytes)) .
58 (nat-eliminate
59 (lambda unrestricted n : Nat . (family StdResult (family RegionFrameFailure) Bytes))
60 (regionFrameFailure code)
61 (lambda unrestricted p : Nat .
62 (lambda unrestricted ignored : (family StdResult (family RegionFrameFailure) Bytes) .
63 (next 0)))
64 flag))))
65
66def regionFrameThen =
67 (lambda unrestricted result : (family StdResult (family RegionFrameFailure) Bytes) .
68 (lambda unrestricted next : (pi unrestricted value : Bytes . (family StdResult (family RegionFrameFailure) Bytes)) .
69 (eliminate
70 StdResult
71 (lambda unrestricted current : (family StdResult (family RegionFrameFailure) Bytes) .
72 (family StdResult (family RegionFrameFailure) Bytes))
73 result
74 (branch StdFailure code . (regionFrameFailure code))
75 (branch StdSuccess value . (next value)))))
76
77-- Check by subtraction before concatenation. In particular no sum of lengths
78-- may wrap and turn an oversized header into a seemingly small allocation.
79def regionFrameJoinWithin =
80 (lambda unrestricted chunks : (family StdList Bytes) .
81 (eliminate
82 StdList
83 (lambda unrestricted current : (family StdList Bytes) .
84 (pi unrestricted budget : Nat . (family StdResult (family RegionFrameFailure) Bytes)))
85 chunks
86 (branch StdListEmpty . (lambda unrestricted budget : Nat . (regionFrameSuccess b"")))
87 (branch
88 StdListCons
89 head
90 tail
91 induction
92 .
93 (lambda unrestricted budget : Nat .
94 (regionFrameRequire
95 (naturalLessOrEqual (bytes-length head) budget)
96 (constructor RegionFrameFailure RegionFrameBounds)
97 (lambda unrestricted delayed : Nat .
98 (regionFrameThen
99 (induction (naturalSaturatingSubtract budget (bytes-length head)))
100 (lambda unrestricted rest : Bytes . (regionFrameSuccess (bytes-append head rest))))))))))
101
102def regionFrameChunk =
103 (lambda unrestricted value : Bytes .
104 (lambda unrestricted tail : (family StdList Bytes) .
105 (constructor StdList StdListCons Bytes value tail)))
106
107def regionFrameName =
108 (lambda unrestricted value : Bytes .
109 (lambda unrestricted tail : (family StdList Bytes) .
110 (regionFrameChunk (regionFrameWord (bytes-length value)) (regionFrameChunk value tail))))
111
112def regionFrameNumber =
113 (lambda unrestricted value : Nat .
114 (lambda unrestricted tail : (family StdList Bytes) .
115 (regionFrameChunk (regionFrameWord value) tail)))
116
117-- The fixed route suffix is shared by encoding and offset derivation. Runtime
118-- round patching therefore follows this schema, not copied byte constants.
119def regionFrameRoute =
120 (lambda unrestricted operation : Nat .
121 (lambda unrestricted sender : Nat .
122 (lambda unrestricted receiver : Nat .
123 (lambda unrestricted begin : Nat .
124 (lambda unrestricted end : Nat .
125 (bytes-append
126 (regionFrameWord operation)
127 (bytes-append
128 (regionFrameWord sender)
129 (bytes-append
130 (regionFrameWord receiver)
131 (bytes-append (regionFrameWord begin) (regionFrameWord end))))))))))
132
133def regionFrameVersionFromEnd =
134 (bytes-length (bytes-append (regionFrameWord 0) (regionFrameRoute 0 0 0 0 0)))
135
136def regionFrameEpochFromEnd =
137 (naturalAdd (bytes-length (regionFrameWord 0)) regionFrameVersionFromEnd)
138
139def regionFrameHeader =
140 (lambda unrestricted identity : (family RegionTransferIdentity) .
141 (lambda unrestricted payloadBytes : Nat .
142 (lambda unrestricted headerBudget : Nat .
143 (eliminate
144 RegionTransferIdentity
145 (lambda unrestricted current : (family RegionTransferIdentity) .
146 (family StdResult (family RegionFrameFailure) Bytes))
147 identity
148 (branch
149 RegionTransferIdentityOf
150 composition
151 run
152 region
153 representation
154 round
155 operation
156 sender
157 receiver
158 interval
159 .
160 (eliminate
161 LearningRound
162 (lambda unrestricted current : (family LearningRound) .
163 (family StdResult (family RegionFrameFailure) Bytes))
164 round
165 (branch
166 LearningRoundOf
167 epoch
168 version
169 .
170 (regionFrameRequire
171 (naturalAnd
172 (naturalLessOrEqual headerBudget regionFrameWordLimit)
173 (naturalAnd
174 (naturalLessOrEqual payloadBytes regionFrameWordLimit)
175 (naturalAnd
176 (naturalLessOrEqual epoch regionFrameWordLimit)
177 (naturalAnd
178 (naturalLessOrEqual version regionFrameWordLimit)
179 (naturalAnd
180 (naturalLessOrEqual operation regionFrameWordLimit)
181 (naturalAnd
182 (naturalLessOrEqual sender regionFrameWordLimit)
183 (naturalAnd
184 (naturalLessOrEqual receiver regionFrameWordLimit)
185 (naturalAnd
186 (naturalLessOrEqual (intervalEnd interval) regionFrameWordLimit)
187 (naturalLessOrEqual
188 (intervalBegin interval)
189 (intervalEnd interval))))))))))
190 (constructor RegionFrameFailure RegionFrameBounds)
191 (lambda unrestricted delayed : Nat .
192 (regionFrameJoinWithin
193 (regionFrameChunk
194 regionFrameMagic
195 (regionFrameNumber
196 payloadBytes
197 (regionFrameName
198 composition
199 (regionFrameName
200 run
201 (regionFrameName
202 region
203 (regionFrameName
204 representation
205 (regionFrameNumber
206 epoch
207 (regionFrameNumber
208 version
209 (regionFrameChunk
210 (regionFrameRoute
211 operation
212 sender
213 receiver
214 (intervalBegin interval)
215 (intervalEnd interval))
216 (constructor StdList StdListEmpty Bytes))))))))))
217 headerBudget))))))))))
218
219def regionFrameHash =
220 (lambda unrestricted bytes : Bytes .
221 (eliminate
222 SHA256Result
223 (lambda unrestricted current : (family SHA256Result) .
224 (family StdResult (family RegionFrameFailure) Bytes))
225 (sha256Bytes bytes)
226 (branch SHA256Succeeded digest . (regionFrameSuccess (sha256DigestToBytes digest)))
227 (branch
228 SHA256Failed
229 code
230 .
231 (regionFrameFailure (constructor RegionFrameFailure RegionFrameHashUnavailable)))))
232
233def encodeRegionFrame =
234 (lambda unrestricted identity : (family RegionTransferIdentity) .
235 (lambda unrestricted headerBudget : Nat .
236 (lambda unrestricted payloadBudget : Nat .
237 (lambda unrestricted payload : Bytes .
238 (regionFrameRequire
239 (naturalLessOrEqual (bytes-length payload) payloadBudget)
240 (constructor RegionFrameFailure RegionFrameBounds)
241 (lambda unrestricted delayed : Nat .
242 (regionFrameThen
243 (regionFrameHeader identity (bytes-length payload) headerBudget)
244 (lambda unrestricted header : Bytes .
245 (regionFrameRequire
246 (naturalAnd
247 (naturalLessOrEqual
248 (bytes-length header)
249 (naturalSaturatingSubtract regionFrameWordLimit regionFrameDigestBytes))
250 (naturalLessOrEqual
251 (bytes-length payload)
252 (naturalSaturatingSubtract
253 (naturalSaturatingSubtract regionFrameWordLimit regionFrameDigestBytes)
254 (bytes-length header))))
255 (constructor RegionFrameFailure RegionFrameBounds)
256 (lambda unrestricted delayed : Nat .
257 (let unrestricted content =
258 (bytes-append header payload)
259 in
260 (regionFrameThen
261 (regionFrameHash content)
262 (lambda unrestricted digest : Bytes .
263 (regionFrameSuccess (bytes-append content digest)))))))))))))))
264
265-- This decoder is for a bounded scheduled frame, not a discovery protocol.
266-- It rejects trailing bytes as well as truncation and binds the digest to the
267-- complete scope. Native framing reads the expected header and body extents
268-- separately; this pure boundary validates the completed immutable bytes.
269def decodeRegionFrame =
270 (lambda unrestricted identity : (family RegionTransferIdentity) .
271 (lambda unrestricted expectedBytes : Nat .
272 (lambda unrestricted headerBudget : Nat .
273 (lambda unrestricted frame : Bytes .
274 (regionFrameThen
275 (regionFrameHeader identity expectedBytes headerBudget)
276 (lambda unrestricted header : Bytes .
277 (regionFrameRequire
278 (naturalAnd
279 (naturalLessOrEqual regionFrameDigestBytes (bytes-length frame))
280 (naturalAnd
281 (naturalLessOrEqual
282 (bytes-length header)
283 (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes))
284 (naturalEqual
285 expectedBytes
286 (naturalSaturatingSubtract
287 (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes)
288 (bytes-length header)))))
289 (constructor RegionFrameFailure RegionFrameWrongExtent)
290 (lambda unrestricted delayed : Nat .
291 (regionFrameRequire
292 (bytes-equal header (dataBytesTakeValidated (bytes-length header) frame))
293 (constructor RegionFrameFailure RegionFrameWrongHeader)
294 (lambda unrestricted delayed : Nat .
295 (let unrestricted contentBytes =
296 (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes)
297 in
298 (regionFrameThen
299 (regionFrameHash (dataBytesTakeValidated contentBytes frame))
300 (lambda unrestricted digest : Bytes .
301 (regionFrameRequire
302 (bytes-equal digest (dataBytesDropValidated contentBytes frame))
303 (constructor RegionFrameFailure RegionFrameWrongDigest)
304 (lambda unrestricted delayed : Nat .
305 (regionFrameSuccess
306 (dataBytesTakeValidated
307 expectedBytes
308 (dataBytesDropValidated (bytes-length header) frame))))))))))))))))))
309
310def receiveRegionFrame =
311 (lambda unrestricted identity : (family RegionTransferIdentity) .
312 (lambda unrestricted expectedBytes : Nat .
313 (lambda unrestricted headerBudget : Nat .
314 (lambda unrestricted phase : (family TransferPhase) .
315 (lambda unrestricted frame : Bytes .
316 (regionFrameRequire
317 (naturalEqual (transferPhaseCode phase) 2)
318 (constructor RegionFrameFailure RegionFrameWrongPhase)
319 (lambda unrestricted delayed : Nat .
320 (decodeRegionFrame identity expectedBytes headerBudget frame))))))))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.