Fresh: version, cursor 0 and the plan's epoch. Resume: the verified path
restore, the restored prefix, then epoch + 1 (a new membership epoch).
319def nitStart =
320 (lambda unrestricted slots : Nat .
321 (lambda unrestricted system : (family IndependentStateSystem slots) .
322 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
323 (lambda unrestricted fanout : Nat .
324 (lambda unrestricted role : Nat .
325 (lambda unrestricted resume : Nat .
326 (lambda unrestricted tail : (family NativePhysicalCommands) .
327 (let unrestricted stateAt =
328 (nitStateAt layout)
329 in
330 (nat-eliminate
331 (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
332 (nativeMemoryStoreWord64
333 b"independent-version"
334 stateAt
335 (nativeLaunchRecipeImmediate 0)
336 (nativeMemoryStoreWord64
337 b"independent-cursor"
338 (nativePointwiseAt stateAt 1)
339 (nativeLaunchRecipeImmediate 0)
340 (nativeMemoryStoreWord64
341 b"independent-epoch"
342 (nativePointwiseAt stateAt 2)
343 (nativeLaunchRecipeImmediate (nativeTreeEpoch (nitCheckpoint layout)))
344 tail)))
345 (lambda unrestricted previous : Nat .
346 (lambda unrestricted ignored : (family NativePhysicalCommands) .
347 (nativeTreeRestore
348 (nitCheckpoint layout)
349 fanout
350 (niOwners slots system)
351 role
352 (nitOwnOf slots system)
353 (nitPaths (niOwners slots system) role)
354 (lambda unrestricted shard : (family NativeRegionShard) .
355 (nitValuesAt layout))
356 (nativeMemoryCopyOperands
357 (nativeMemoryState stateAt)
358 (nativeMemoryState (nativeTreeRestoredCaptureAt (nitCheckpoint layout)))
359 nativeRegionCaptureBytes
360 nativePeerScratchSlot
361 b"independent-restore-capture"
362 (nativeLaunchRecipeAssertEqual
363 (nativeMemoryLoad stateAt)
364 (nativeMemoryLoad (nativePointwiseAt stateAt 1))
365 b"independent-input-position"
366 (nativeCheckedWordAdd
367 (nativeMemoryState (nativePointwiseAt stateAt 2))
368 (nativeMemoryLoad (nativePointwiseAt stateAt 2))
369 (nativeLaunchRecipeImmediate 1)
370 nativePeerScratchSlot
371 b"independent-epoch-overflow"
372 tail))))))
373 resume)))))))))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.