Cuda
Types
linear type ReadyBuffer a
linear type Float64Download
linear type StatusBuffer a
Functions
def mem_kind_device : Int
def mem_kind_host_pinned : Int
def mem_kind_managed : 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 (p : StatusPair a | status_pair_ok p) : {s : Status | status_is_ok s}
def status_pair_buffer (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 (p : I32DownloadPair) : {xs : Array Int | Array.size xs = i32_download_pair_size p}
def download_buffer_i32 (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 (p : Float64DownloadPair) : {xs : Array Float | Array.size xs = float64_download_pair_size p}
def download_buffer_float64 (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
Uninterpreted
Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.
def device_id : (d : Device) → Int
def num_devices : (_ : Unit) → Int
def max_threads_per_block : (d : Device) → Int
def max_allocation : (d : Device) → Int
def warp_size : (d : Device) → Int
def max_shared_mem_per_block : (d : Device) → Int
def launch_device : (launch : Launch1D) → Int
def launch_items : (launch : Launch1D) → Int
def launch_threads : (launch : Launch1D) → Int
def launch_grid_size : (launch : Launch1D) → Int
def launch_shared_bytes : (launch : Launch1D) → Int
def launch2d_device : (launch : Launch2D) → Int
def launch2d_width : (launch : Launch2D) → Int
def launch2d_height : (launch : Launch2D) → Int
def launch2d_threads_x : (launch : Launch2D) → Int
def launch2d_threads_y : (launch : Launch2D) → Int
def launch2d_grid_x : (launch : Launch2D) → Int
def launch2d_grid_y : (launch : Launch2D) → Int
def launch2d_shared_bytes : (launch : Launch2D) → Int
def stream_device : (stream : Stream) → Int
def stream_id : (stream : Stream) → Int
def pending_stream : (pending : Pending a) → Int
def buffer_device : (buffer : ReadyBuffer a) → Int
def buffer_size : (buffer : ReadyBuffer a) → Int
def buffer_elem_size : (buffer : ReadyBuffer a) → Int
def buffer_bytes : (buffer : ReadyBuffer a) → Int
def buffer_mem_kind : (buffer : ReadyBuffer a) → Int
def buffer_access : (buffer : ReadyBuffer a) → Int
def buffer_extent_x : (buffer : ReadyBuffer a) → Int
def buffer_extent_y : (buffer : ReadyBuffer a) → Int
def pending_device : (pending : Pending a) → Int
def pending_size : (pending : Pending a) → Int
def i32_download_device : (p : I32Download) → Int
def i32_download_size : (p : I32Download) → Int
def i32_download_pair_device : (p : I32DownloadPair) → Int
def i32_download_pair_size : (p : I32DownloadPair) → Int
def float64_download_device : (p : Float64Download) → Int
def float64_download_size : (p : Float64Download) → Int
def float64_download_pair_device : (p : Float64DownloadPair) → Int
def float64_download_pair_size : (p : Float64DownloadPair) → Int
def status_is_ok : (s : Status) → Bool
def status_code : (s : Status) → Int
def status_buffer_ok : (sb : StatusBuffer a) → Bool
def status_buffer_device : (sb : StatusBuffer a) → Int
def status_buffer_size : (sb : StatusBuffer a) → Int
def status_pair_ok : (p : StatusPair a) → Bool
def status_pair_device : (p : StatusPair a) → Int
def status_pair_size : (p : StatusPair a) → Int