Every owner's frame occupies the first owner's storage exactly: same base,
payload extent and end, so one arena resident covers all of them.
334def nativePeerFramesShareStorage =
335 (lambda unrestricted peers : Nat .
336 (lambda unrestricted frame : (pi unrestricted owner : Nat . (family RegionFrameLayout)) .
337 (lambda unrestricted payload : Nat .
338 (let unrestricted first =
339 (frame 1)
340 in
341 (stdListFold
342 Nat
343 Nat
344 (lambda unrestricted index : Nat .
345 (lambda unrestricted rest : Nat .
346 (let unrestricted current =
347 (frame (succ index))
348 in
349 (naturalAnd
350 rest
351 (naturalAnd
352 (naturalEqual (framePayloadBytes current) payload)
353 (naturalAnd
354 (naturalEqual (frameBase current) (frameBase first))
355 (naturalEqual (frameEnd current) (frameEnd first))))))))
356 1
357 (stdListNaturalsBelow peers))))))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.