1module Compiler.Planning.RegionFrame
2
3import Runtime.RegionTransfer
4import Runtime.RegionFrame
5import Runtime.WordDigest
6import Runtime.ArenaCertificate
7import Data.SHA256
8import Data.SHA256Padding
9import Model.Parameter
10import Model.Word64
11import Std.Foundation
12import Std.Natural
13
14-- One content region is reused for SHA padding AFTER the trailer has been
15-- received separately. Padding can never overwrite the transmitted digest.
16family RegionFrameLayout : Type 0
17constructor RegionFrameLayoutOf
18field unrestricted frameLayoutHeader : Bytes
19field unrestricted frameLayoutPayloadBytes : Nat
20field unrestricted frameLayoutBase : Nat
21field unrestricted frameLayoutPadding : Bytes
22
23end-family
24
25family RegionFrameLayoutFailure : Type 0
26constructor RegionFrameLayoutHeaderRejected
27constructor RegionFrameLayoutPaddingRejected
28constructor RegionFrameLayoutBoundsRejected
29
30end-family
31
32def frameHeader =
33 (lambda unrestricted layout : (family RegionFrameLayout) .
34 (eliminate
35 RegionFrameLayout
36 (lambda unrestricted current : (family RegionFrameLayout) . Bytes)
37 layout
38 (branch RegionFrameLayoutOf header payload base padding . header)))
39
40def framePayloadBytes =
41 (lambda unrestricted layout : (family RegionFrameLayout) .
42 (eliminate
43 RegionFrameLayout
44 (lambda unrestricted current : (family RegionFrameLayout) . Nat)
45 layout
46 (branch RegionFrameLayoutOf header payload base padding . payload)))
47
48def frameBase =
49 (lambda unrestricted layout : (family RegionFrameLayout) .
50 (eliminate
51 RegionFrameLayout
52 (lambda unrestricted current : (family RegionFrameLayout) . Nat)
53 layout
54 (branch RegionFrameLayoutOf header payload base padding . base)))
55
56def framePadding =
57 (lambda unrestricted layout : (family RegionFrameLayout) .
58 (eliminate
59 RegionFrameLayout
60 (lambda unrestricted current : (family RegionFrameLayout) . Bytes)
61 layout
62 (branch RegionFrameLayoutOf header payload base padding . padding)))
63
64def frameAlign =
65 (lambda unrestricted extent : Nat .
66 (naturalMultiply
67 digestWorkAlignment
68 (naturalDivideUnchecked
69 (naturalAdd extent (naturalSaturatingSubtract digestWorkAlignment 1))
70 digestWorkAlignment)))
71
72def frameContentBytes =
73 (lambda unrestricted layout : (family RegionFrameLayout) .
74 (naturalAdd (bytes-length (frameHeader layout)) (framePayloadBytes layout)))
75
76def framePaddedBytes =
77 (lambda unrestricted layout : (family RegionFrameLayout) .
78 (naturalAdd (frameContentBytes layout) (bytes-length (framePadding layout))))
79
80def frameBlockCount =
81 (lambda unrestricted layout : (family RegionFrameLayout) .
82 (naturalDivideUnchecked (framePaddedBytes layout) digestBlockBytes))
83
84def frameExpectedRelative =
85 (lambda unrestricted layout : (family RegionFrameLayout) . (framePaddedBytes layout))
86
87def frameReceivedRelative =
88 (lambda unrestricted layout : (family RegionFrameLayout) .
89 (naturalAdd (frameExpectedRelative layout) (bytes-length (frameHeader layout))))
90
91def frameComputedRelative =
92 (lambda unrestricted layout : (family RegionFrameLayout) .
93 (naturalAdd (frameReceivedRelative layout) regionFrameDigestBytes))
94
95def frameWorkRelative =
96 (lambda unrestricted layout : (family RegionFrameLayout) .
97 (frameAlign (naturalAdd (frameComputedRelative layout) regionFrameDigestBytes)))
98
99def framePhaseRelative =
100 (lambda unrestricted layout : (family RegionFrameLayout) .
101 (naturalAdd (frameWorkRelative layout) digestWorkBytes))
102
103def frameStorageBytes =
104 (lambda unrestricted layout : (family RegionFrameLayout) .
105 (naturalAdd (framePhaseRelative layout) digestAddressBytes))
106
107def frameHeaderAt =
108 (lambda unrestricted layout : (family RegionFrameLayout) . (frameBase layout))
109
110def framePayloadAt =
111 (lambda unrestricted layout : (family RegionFrameLayout) .
112 (naturalAdd (frameBase layout) (bytes-length (frameHeader layout))))
113
114def framePaddingAt =
115 (lambda unrestricted layout : (family RegionFrameLayout) .
116 (naturalAdd (frameBase layout) (frameContentBytes layout)))
117
118def frameExpectedAt =
119 (lambda unrestricted layout : (family RegionFrameLayout) .
120 (naturalAdd (frameBase layout) (frameExpectedRelative layout)))
121
122-- These are offsets in a locally constructed, admitted canonical header.
123-- Peer-provided lengths never participate in their derivation.
124def frameExpectedVersionAt =
125 (lambda unrestricted layout : (family RegionFrameLayout) .
126 (naturalAdd
127 (frameExpectedAt layout)
128 (naturalSaturatingSubtract (bytes-length (frameHeader layout)) regionFrameVersionFromEnd)))
129
130def frameExpectedEpochAt =
131 (lambda unrestricted layout : (family RegionFrameLayout) .
132 (naturalAdd
133 (frameExpectedAt layout)
134 (naturalSaturatingSubtract (bytes-length (frameHeader layout)) regionFrameEpochFromEnd)))
135
136def frameReceivedAt =
137 (lambda unrestricted layout : (family RegionFrameLayout) .
138 (naturalAdd (frameBase layout) (frameReceivedRelative layout)))
139
140def frameComputedAt =
141 (lambda unrestricted layout : (family RegionFrameLayout) .
142 (naturalAdd (frameBase layout) (frameComputedRelative layout)))
143
144def frameWorkAt =
145 (lambda unrestricted layout : (family RegionFrameLayout) .
146 (naturalAdd (frameBase layout) (frameWorkRelative layout)))
147
148def framePhaseAt =
149 (lambda unrestricted layout : (family RegionFrameLayout) .
150 (naturalAdd (frameBase layout) (framePhaseRelative layout)))
151
152def frameEnd =
153 (lambda unrestricted layout : (family RegionFrameLayout) .
154 (naturalAdd (frameBase layout) (frameStorageBytes layout)))
155
156def frameLayoutResidents =
157 (lambda unrestricted layout : (family RegionFrameLayout) .
158 (constructor
159 ArenaResidents
160 ArenaResidentsNext
161 (constructor
162 ArenaResident
163 ArenaResidentValue
164 b"frame-content-and-padding"
165 (frameHeaderAt layout)
166 (framePaddedBytes layout)
167 1)
168 (constructor
169 ArenaResidents
170 ArenaResidentsNext
171 (constructor
172 ArenaResident
173 ArenaResidentValue
174 b"frame-expected-header"
175 (frameExpectedAt layout)
176 (bytes-length (frameHeader layout))
177 1)
178 (constructor
179 ArenaResidents
180 ArenaResidentsNext
181 (constructor
182 ArenaResident
183 ArenaResidentValue
184 b"frame-received-digest"
185 (frameReceivedAt layout)
186 regionFrameDigestBytes
187 1)
188 (constructor
189 ArenaResidents
190 ArenaResidentsNext
191 (constructor
192 ArenaResident
193 ArenaResidentValue
194 b"frame-computed-digest"
195 (frameComputedAt layout)
196 regionFrameDigestBytes
197 1)
198 (constructor
199 ArenaResidents
200 ArenaResidentsNext
201 (constructor
202 ArenaResident
203 ArenaResidentValue
204 b"frame-hash-work"
205 (frameWorkAt layout)
206 digestWorkBytes
207 digestWorkAlignment)
208 (constructor
209 ArenaResidents
210 ArenaResidentsNext
211 (constructor
212 ArenaResident
213 ArenaResidentValue
214 b"frame-phase"
215 (framePhaseAt layout)
216 digestAddressBytes
217 digestAddressBytes)
218 (constructor ArenaResidents ArenaResidentsEnd))))))))
219
220-- Admission compares a derived extent with available capacity; the executable
221-- allocates exactly frameEnd. Base alignment makes the shared relative layout
222-- independent of an earlier role's placement. Subtraction avoids base overflow.
223def frameLayoutFits =
224 (lambda unrestricted available : Nat .
225 (lambda unrestricted layout : (family RegionFrameLayout) .
226 (naturalAnd
227 (naturalLessOrEqual available regionFrameWordLimit)
228 (naturalAnd
229 (naturalIsZero (naturalModuloUnchecked (frameBase layout) digestWorkAlignment))
230 (naturalAnd
231 (naturalLessOrEqual (frameBase layout) available)
232 (naturalLessOrEqual
233 (frameStorageBytes layout)
234 (naturalSaturatingSubtract available (frameBase layout))))))))
235
236def planRegionFrameLayout =
237 (lambda unrestricted identity : (family RegionTransferIdentity) .
238 (lambda unrestricted payloadBytes : Nat .
239 (lambda unrestricted headerBudget : Nat .
240 (lambda unrestricted base : Nat .
241 (lambda unrestricted available : Nat .
242 (eliminate
243 StdResult
244 (lambda unrestricted current : (family StdResult (family RegionFrameFailure) Bytes) .
245 (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)))
246 (regionFrameHeader identity payloadBytes headerBudget)
247 (branch
248 StdFailure
249 code
250 .
251 (constructor
252 StdResult
253 StdFailure
254 (family RegionFrameLayoutFailure)
255 (family RegionFrameLayout)
256 (constructor RegionFrameLayoutFailure RegionFrameLayoutHeaderRejected)))
257 (branch
258 StdSuccess
259 header
260 .
261 (nat-eliminate
262 (lambda unrestricted valid : Nat .
263 (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)))
264 (constructor
265 StdResult
266 StdFailure
267 (family RegionFrameLayoutFailure)
268 (family RegionFrameLayout)
269 (constructor RegionFrameLayoutFailure RegionFrameLayoutBoundsRejected))
270 (lambda unrestricted previous : Nat .
271 (lambda unrestricted ignored : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
272 (eliminate
273 StdResult
274 (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
275 (family
276 StdResult
277 (family RegionFrameLayoutFailure)
278 (family RegionFrameLayout)))
279 (sha256PaddingSuffix (naturalAdd (bytes-length header) payloadBytes))
280 (branch
281 StdFailure
282 code
283 .
284 (constructor
285 StdResult
286 StdFailure
287 (family RegionFrameLayoutFailure)
288 (family RegionFrameLayout)
289 (constructor RegionFrameLayoutFailure RegionFrameLayoutPaddingRejected)))
290 (branch
291 StdSuccess
292 padding
293 .
294 (let unrestricted layout : (family RegionFrameLayout) =
295 (constructor
296 RegionFrameLayout
297 RegionFrameLayoutOf
298 header
299 payloadBytes
300 base
301 padding)
302 in
303 (nat-eliminate
304 (lambda unrestricted fits : Nat .
305 (family
306 StdResult
307 (family RegionFrameLayoutFailure)
308 (family RegionFrameLayout)))
309 (constructor
310 StdResult
311 StdFailure
312 (family RegionFrameLayoutFailure)
313 (family RegionFrameLayout)
314 (constructor
315 RegionFrameLayoutFailure
316 RegionFrameLayoutBoundsRejected))
317 (lambda unrestricted previous : Nat .
318 (lambda unrestricted ignored : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
319 (constructor
320 StdResult
321 StdSuccess
322 (family RegionFrameLayoutFailure)
323 (family RegionFrameLayout)
324 layout)))
325 (frameLayoutFits available layout)))))))
326 (naturalAnd
327 (naturalLessOrEqual
328 (bytes-length header)
329 (modelWord64Natural sha256MaximumInputBytes))
330 (naturalLessOrEqual
331 payloadBytes
332 (naturalSaturatingSubtract
333 (modelWord64Natural sha256MaximumInputBytes)
334 (bytes-length header))))))))))))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.