Cuda

type Device

type Launch1D

type Launch2D

type Stream

def mem_kind_device : Int

def mem_kind_host_pinned : Int

def mem_kind_managed : Int

def mem_kind_host : Int

def access_read_only : Int

def access_read_write : Int

def num_devices (_ : Unit) : {n : Int | n > 0}

def device (id : Int | id ≥ 0 && id < num_devices unit) : {d : Device | device_id d = id && max_threads_per_block d ≥ 1024 && warp_size d = 32 && max_shared_mem_per_block d ≥ 0}

def default_device (_ : Unit) : {d : Device | device_id d ≥ 0 && max_threads_per_block d ≥ 1024 && warp_size d = 32 && max_shared_mem_per_block d ≥ 0}

def default_stream (device : Device) : {stream : Stream | stream_device stream = device_id device}

def launch_1d (device : Device) (items : Int | items > 0) (threads : Int | threads > 0 && threads ≤ items && threads ≤ max_threads_per_block device && threads ≤ 1024) : { launch : Launch1D | launch_device launch = device_id device && launch_items launch = items && launch_threads launch = threads && launch_grid_size launch * launch_threads launch ≥ launch_items launch && launch_shared_bytes launch = 0 }

def launch_1d_shared (device : Device) (items : Int | items > 0) (threads : Int | threads > 0 && threads ≤ items && threads ≤ max_threads_per_block device && threads ≤ 1024) (shared : Int | shared ≥ 0 && shared ≤ max_shared_mem_per_block device) : { launch : Launch1D | launch_device launch = device_id device && launch_items launch = items && launch_threads launch = threads && launch_grid_size launch * launch_threads launch ≥ launch_items launch && launch_shared_bytes launch = shared }

def launch_1d_warped (device : Device) (items : Int | items > 0) ( threads : Int | threads > 0 && threads ≤ items && threads ≤ max_threads_per_block device && threads ≤ 1024 && (threads ≤ warp_size device || threads % warp_size device = 0) ) : { launch : Launch1D | launch_device launch = device_id device && launch_items launch = items && launch_threads launch = threads && launch_grid_size launch * launch_threads launch ≥ launch_items launch && launch_shared_bytes launch = 0 }

def launch_2d (device : Device) (width : Int | width > 0) (height : Int | height > 0) (tx : Int | tx > 0 && tx ≤ 1024) (ty : Int | ty > 0 && ty ≤ 1024 && tx * ty ≤ max_threads_per_block device && tx * ty ≤ 1024) : { launch : Launch2D | launch2d_device launch = device_id device && launch2d_width launch = width && launch2d_height launch = height && launch2d_threads_x launch = tx && launch2d_threads_y launch = ty && launch2d_grid_x launch * launch2d_threads_x launch ≥ launch2d_width launch && launch2d_grid_y launch * launch2d_threads_y launch ≥ launch2d_height launch && launch2d_shared_bytes launch = 0 }

def launch_2d_shared (device : Device) (width : Int | width > 0) (height : Int | height > 0) (tx : Int | tx > 0 && tx ≤ 1024) (ty : Int | ty > 0 && ty ≤ 1024 && tx * ty ≤ max_threads_per_block device && tx * ty ≤ 1024) (shared : Int | shared ≥ 0 && shared ≤ max_shared_mem_per_block device) : { launch : Launch2D | launch2d_device launch = device_id device && launch2d_width launch = width && launch2d_height launch = height && launch2d_threads_x launch = tx && launch2d_threads_y launch = ty && launch2d_grid_x launch * launch2d_threads_x launch ≥ launch2d_width launch && launch2d_grid_y launch * launch2d_threads_y launch ≥ launch2d_height launch && launch2d_shared_bytes launch = shared }

def upload_i32 (device : Device) (1 values : (Array Int) | Array.size values > 0) : { buffer : (ReadyBuffer Int) | buffer_device buffer = device_id device && buffer_size buffer = Array.size values && buffer_elem_size buffer = 4 && buffer_bytes buffer = buffer_size buffer * buffer_elem_size buffer && buffer_bytes buffer ≤ max_allocation device && buffer_mem_kind buffer = mem_kind_device && buffer_access buffer = access_read_write && buffer_extent_x buffer = buffer_size buffer && buffer_extent_y buffer = 1 }

def upload_float64 (device : Device) (1 values : (Array Float) | Array.size values > 0) : { buffer : (ReadyBuffer Float) | buffer_device buffer = device_id device && buffer_size buffer = Array.size values && buffer_elem_size buffer = 8 && buffer_bytes buffer = buffer_size buffer * buffer_elem_size buffer && buffer_bytes buffer ≤ max_allocation device && buffer_mem_kind buffer = mem_kind_device && buffer_access buffer = access_read_write && buffer_extent_x buffer = buffer_size buffer && buffer_extent_y buffer = 1 }

def as_read_only (1 buffer : (ReadyBuffer a)) : { r : (ReadyBuffer a) | buffer_device r = buffer_device buffer && buffer_size r = buffer_size buffer && buffer_elem_size r = buffer_elem_size buffer && buffer_bytes r = buffer_bytes buffer && buffer_mem_kind r = buffer_mem_kind buffer && buffer_access r = access_read_only && buffer_extent_x r = buffer_extent_x buffer && buffer_extent_y r = buffer_extent_y buffer }

def add_i32 (launch : Launch1D) (stream : Stream | stream_device stream = launch_device launch) ( 1 left : (ReadyBuffer Int) | buffer_size left > 0 && buffer_elem_size left = 4 && buffer_device left = launch_device launch && buffer_size left = launch_items launch && buffer_mem_kind left = mem_kind_device && (buffer_access left = access_read_only || buffer_access left = access_read_write) && launch_grid_size launch * launch_threads launch ≥ buffer_size left ) ( 1 right : (ReadyBuffer Int) | buffer_size right = buffer_size left && buffer_elem_size right = buffer_elem_size left && buffer_device right = buffer_device left && buffer_mem_kind right = mem_kind_device && (buffer_access right = access_read_only || buffer_access right = access_read_write) ) : { pending : (Pending Int) | pending_device pending = launch_device launch && pending_size pending = launch_items launch && pending_stream pending = stream_id stream }

def add_float64 (launch : Launch1D) (stream : Stream | stream_device stream = launch_device launch) ( 1 left : (ReadyBuffer Float) | buffer_size left > 0 && buffer_elem_size left = 8 && buffer_device left = launch_device launch && buffer_size left = launch_items launch && buffer_mem_kind left = mem_kind_device && (buffer_access left = access_read_only || buffer_access left = access_read_write) && launch_grid_size launch * launch_threads launch ≥ buffer_size left ) ( 1 right : (ReadyBuffer Float) | buffer_size right = buffer_size left && buffer_elem_size right = buffer_elem_size left && buffer_device right = buffer_device left && buffer_mem_kind right = mem_kind_device && (buffer_access right = access_read_only || buffer_access right = access_read_write) ) : { pending : (Pending Float) | pending_device pending = launch_device launch && pending_size pending = launch_items launch && pending_stream pending = stream_id stream }

def synchronize (1 pending : (Pending a)) : { buffer : (ReadyBuffer a) | buffer_device buffer = pending_device pending && buffer_size buffer = pending_size pending && buffer_bytes buffer = buffer_size buffer * buffer_elem_size buffer && buffer_mem_kind buffer = mem_kind_device && buffer_access buffer = access_read_write && buffer_extent_x buffer = buffer_size buffer && buffer_extent_y buffer = 1 }

def synchronize_with_status (1 pending : (Pending a)) : { sb : (StatusBuffer a) | status_buffer_ok sb && status_buffer_device sb = pending_device pending && status_buffer_size sb = pending_size pending }

def unpack_status_buffer (1 sb : (StatusBuffer a) | status_buffer_ok sb) : { pair : (StatusPair a) | status_pair_ok pair && status_pair_device pair = status_buffer_device sb && status_pair_size pair = status_buffer_size sb }

def status_pair_status (1 p : (StatusPair a) | status_pair_ok p) : {s : Status | status_is_ok s}

def status_pair_buffer (1 p : (StatusPair a) | status_pair_ok p) : { b : (ReadyBuffer a) | buffer_device b = status_pair_device p && buffer_size b = status_pair_size p && buffer_mem_kind b = mem_kind_device && buffer_access b = access_read_write && buffer_extent_x b = buffer_size b && buffer_extent_y b = 1 }

def check_ok (1 s : Status | status_is_ok s) : Unit

def discard_status (1 s : Status) : Unit

def download_i32 (1 buffer : (ReadyBuffer Int)) : { result : I32Download | i32_download_device result = buffer_device buffer && i32_download_size result = buffer_size buffer }

def download_float64 (1 buffer : (ReadyBuffer Float)) : { result : Float64Download | float64_download_device result = buffer_device buffer && float64_download_size result = buffer_size buffer }

def unpack_i32_download (1 p : I32Download) : { pair : I32DownloadPair | i32_download_pair_device pair = i32_download_device p && i32_download_pair_size pair = i32_download_size p }

def unpack_float64_download (1 p : Float64Download) : { pair : Float64DownloadPair | float64_download_pair_device pair = float64_download_device p && float64_download_pair_size pair = float64_download_size p }

def download_values_i32 (1 p : I32DownloadPair) : {xs : (Array Int) | Array.size xs = i32_download_pair_size p}

def download_buffer_i32 (1 p : I32DownloadPair) : { b : (ReadyBuffer Int) | buffer_device b = i32_download_pair_device p && buffer_size b = i32_download_pair_size p && buffer_elem_size b = 4 && buffer_bytes b = buffer_size b * buffer_elem_size b && buffer_mem_kind b = mem_kind_device && buffer_access b = access_read_write && buffer_extent_x b = buffer_size b && buffer_extent_y b = 1 }

def download_values_float64 (1 p : Float64DownloadPair) : {xs : (Array Float) | Array.size xs = float64_download_pair_size p}

def download_buffer_float64 (1 p : Float64DownloadPair) : { b : (ReadyBuffer Float) | buffer_device b = float64_download_pair_device p && buffer_size b = float64_download_pair_size p && buffer_elem_size b = 8 && buffer_bytes b = buffer_size b * buffer_elem_size b && buffer_mem_kind b = mem_kind_device && buffer_access b = access_read_write && buffer_extent_x b = buffer_size b && buffer_extent_y b = 1 }

def free (1 buffer : (ReadyBuffer a)) : Unit

def discard (1 pending : (Pending a)) : Unit

def with_i32_download (1 token : I32DownloadPair) ( 1 consume : (1 left : (Array Int) | Array.size left = i32_download_pair_size token) → ( 1 right : (ReadyBuffer Int) | buffer_device right = i32_download_pair_device token && buffer_size right = i32_download_pair_size token && buffer_elem_size right = 4 && buffer_bytes right = buffer_size right * buffer_elem_size right && buffer_mem_kind right = mem_kind_device && buffer_access right = access_read_write && buffer_extent_x right = buffer_size right && buffer_extent_y right = 1 ) → b ) : b

def with_float64_download (1 token : Float64DownloadPair) ( 1 consume : (1 left : (Array Float) | Array.size left = float64_download_pair_size token) → ( 1 right : (ReadyBuffer Float) | buffer_device right = float64_download_pair_device token && buffer_size right = float64_download_pair_size token && buffer_elem_size right = 8 && buffer_bytes right = buffer_size right * buffer_elem_size right && buffer_mem_kind right = mem_kind_device && buffer_access right = access_read_write && buffer_extent_x right = buffer_size right && buffer_extent_y right = 1 ) → b ) : b

def with_status_pair (1 token : (StatusPair a) | status_pair_ok token) ( 1 consume : (1 left : Status | status_is_ok left) → ( 1 right : (ReadyBuffer a) | buffer_device right = status_pair_device token && buffer_size right = status_pair_size token && buffer_mem_kind right = mem_kind_device && buffer_access right = access_read_write && buffer_extent_x right = buffer_size right && buffer_extent_y right = 1 ) → b ) : b