stelliferous
Releases (2)
Definitions (2,086)
proofs/word_encoding.bend
- law nonnegative
- def truth
- def false_true
- law finish_one
- law less_one_is_zero
- type Split
- def join
- def prepend
- def split
- law join_prepend
- law recover
- law cmp_eq
- law finish_eq_parts
- law zero_reflect
- def zero_step
- law below_one_zero
- law and_zero
- law upper_zero
proofs/word_multiplication.bend
- def truncate
- def truncate_zero
- def truncate_inc
- def truncate_encode
- def put
- def shift
- def encoded_double
- law word_roundtrip
- def double_mul
- law multiply_go
- def multiply
- def native_multiply
- def bounded_multiply
proofs/word_power_of_two.bend
- def power
- def mask
- law put_into_zero
- law shift_power
- law native_power
- law subtract_one
- law zero_subtract_zero
- law decrement_power
- law mask_preserves_bounded
- def native_word_mask
- law native_mask_preserves_bounded
- law compare_zero
- law positive_power
- law compare_equal_low_bits
- law power_monotone
- law power_value
- law pad_zero
- law pad_power
- law native_half_power
- law native_power_bound
- def native_allocatable
- def positive_double
- def nonempty_power_depthA nonempty checked owner cannot have a power-of-two capacity truncated to zero.
- def native_nonempty_depth
proofs/word_subtraction.bend
- law undo
- def subtract_add
- def add_subtract
- def encoded_subtract_add
- def restore
- def encoded_subtract
proofs/word_width.bend
- def transport
- law transport_cons
storage_allocation.bend
- def dispatch
- def allocated
- def allocate
- def storageInternal Array callers can discard the construction certificate after the same constant-depth dispatch; no traversal or clone is introduced.
- def array
storage_buffer.bend
- type Buffer
- def allocateConstruction records evidence once, without visiting the owner or carrying certificates through the elementwise loop.
- def from_list
- def write_atThe values written from the offset on; the certificate follows the storage.
- def capacity
- def bind_pair
- def bit_lengthAt most 32 word steps, independent of the allocation length.
- def allocation_depthPositive requested lengths round to the next power-of-two capacity.
- def significant_bitsShared runtime depth calculation.
- def depth_for
- def write_list
- def read_list
- def read_when
- def read_sized
- def read_or
storage_clone.bend
storage_copy.bend
- def range
tensor.bend
- type Reason
- type Problem
- type Status
- type TensorLike a PyTorch tensor's device, workers is execution context: the size of the runtime's worker pool, read once with IO.thread_count and set with with_workers.
- type PartsA nonempty sequence of tensors.
- def withinElement count of a shape that the default machine can allocate.
- def allocatable
- def count_of
- def known_count
- def count_or_zeroThe element count as a number; a shape too large to allocate counts 0.
- def view_of
- def significant_bitsBits of value, counted by tail recursion.
- def depth_forThe smallest depth whose capacity holds count elements (at least one).
- def buffer