KernelPackingWitness.tile: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend as KernelPackingWitness Lines 186-201 of stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&start_line=186&end_line=201 import Base import stelliferous@0.0.2.0/traversal_loop.bend as Loop import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Packing import stelliferous@0.0.2.0/kernel_tile.bend as Tile import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness import stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend as PackingReadWitness def tile(+depth: Nat,within: Bool,wraps: Bool,-input: Array,-output: Array,+i: U32,+position: U32,+h: U32,+w: U32,+k: U32,+s: U32,+p: U32,+ow: U32, +channels: Nat,+taps: Nat,+inner: Nat,+input_evidence: PackingReadWitness.family(input),balanced: Witness.Witness(Tile.Tile8,depth,output)) -> TileEvidence: match within wraps: case True{} wraps: +cursor = {RowCursor{i,0,0,0,(position / ow : U32),(position % ow : U32),ow,h,w,s,p,taps} : RowCursor} after_row_tile(depth,input,position,k,channels,inner,Loop.run(~Packing.RowTiles(),~Packing.channel_step(~Packing.block),channels,restore_row(input,output,cursor)), channel_loop(~Packing.block,~PackingReadWitness.row_block,depth,channels,input,restore_row(input,output,cursor),input_evidence,RowEvidence{output,cursor,{==},balanced})) case False{} True{}: +cursor = {RowCursor{i,0,0,0,(position / ow : U32),(position % ow : U32),ow,h,w,s,p,taps} : RowCursor} after_row_tile(depth,input,position,k,channels,inner,Loop.run(~Packing.RowTiles(),~Packing.channel_step(~Packing.wrap_block),channels,restore_row(input,output,cursor)), channel_loop(~Packing.wrap_block,~PackingReadWitness.wrap_block,depth,channels,input,restore_row(input,output,cursor),input_evidence,RowEvidence{output,cursor,{==},balanced})) case False{} False{}: +cursor = {CrossingCursor{i,0,position,h,w,k,s,p,ow} : CrossingCursor} after_crossing(depth,input,channels,taps,inner,Loop.run(~Packing.Crossings(),~Packing.crossing_step,inner,restore_crossing(input,output,cursor)), crossing_loop(depth,inner,input,restore_crossing(input,output,cursor),input_evidence,CrossingEvidence{output,cursor,{==},balanced})) Uses (31): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=Crossings https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=RowTiles https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=block https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=channel_step https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=crossing_step https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=tile https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_spatial_packing.bend&name=wrap_block https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8 https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend&name=family https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend&name=row_block https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend&name=wrap_block https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=CrossingCursor https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=CrossingEvidence https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=RowCursor https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=RowEvidence https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=TileEvidence https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=after_crossing https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=after_row_tile https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=channel_loop https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=crossing_loop https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=restore_crossing https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend&name=restore_row https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_loop.bend&name=run