AlphaGitHub
Source/Packages

Runtime.NativeDataParallel

packages/execution/src/Runtime/NativeDataParallel.alpha

1,529 lines92 declarations70.3 KiBSHA-256 a009e951c1b2
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 474–483

dpShardOffset

Full file
Where a shard's bytes lie in an owner's state: past the capture prefix, parameters (region 0) then optimizer state (region 1).
474def dpShardOffset =
475  (lambda unrestricted c : Nat .
476    (lambda unrestricted u : Nat .
477      (lambda unrestricted system : (family DataParallelSystem c u) .
478        (lambda unrestricted shard : (family NativeRegionShard) .
479          (naturalAdd
480            nativeRegionCaptureBytes
481            (naturalAdd
482              (naturalMultiply (nativeRegionOrdinal shard) (dpParameterBytes c u system))
483              (intervalBegin (nativeRegionInterval shard))))))))

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.