stelliferous

Search uses release 0.0.2.0 · 2,086 definitions

Releases (2)

def represent_mapIn-place transforms retain one owner and use the same generic loop lifting.
def unindexed
def model_map_step
def map_step_refines_model
def map_loop_refines_model
def model_update_stepIn-place binary updates use the current destination value in left position.
def update_step_refines_model
def update_refines_model
def indexed_fold_refines_model
def indexed_fold_change_contextOne bounded induction carries capacity, preserved sources and completed output values together.
def indexed_fold_preserves_invariant
def indexed_fold_splitSplitting a traversal preserves every state update in the same order.

def batch
def ModelState
def last_stepA loop's last step, for every state and count.
def state_afterThe whole state after count steps of the model map.
def extendedOne more step of the model map writes the position after the ones it mapped.
def continuedA batch that continues done steps of the map completes the map.
def mappedA batch from the original tree is the map of its positions.

def scratch_readbackReading the just-written scratch slot returns its cell at every slot.
def round_with
def round
type Observed
def observe
def observe_gather
def model_stored
def stored_observedOne shared scratch round; gather and scatter supply their numerical laws.

type Certificates
def completed
def map_equation
def map_in_place
def fold
def operation_sourceMetadata preparation belongs inside the erased preservation proof.
def operation_equation
def operation
def fold_operation

def map_when
def refinesThe cover test of a balanced tree gives the bounds of the refinement.
def observed
def certifiedOn any certified array the map through tiles is the ordered map.
def gathered_ownerReuse the existing gather/scatter witnesses when a cell owns certified buffers rather than passing flat certificates outside the whole traversal.
def gather
def scatter

def cellThe tile a round gathers at position.
def gathered
def writtenEight ordered writes from position.
def scattered
def cell_scattered
def roundOne round maps eight positions.
def outputThe scalar map from any position, on a packed tree.
def scalar
def few
def steppedThe position of the model map after k steps from start.
def advanced
def after_round
def round_room
def rest_room
def finish_smallThe shared induction on eight-value rounds.
def by_rounds
def rounds_propertyEvery count: whole rounds, then the last positions one by one.
def few_rounds
def more_rounds
def rounds
def mapThe whole map from any position, with a fresh scratch array.