def after_columns

stelliferous@0.0.2.0 · proofs/kernel_packing_witness.bend:60

import Base
import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Packing

60def after_columns(-depth: Nat,-input: Array<F32>,-state: Packing.RowTiles(),evidence: RowEvidence<input,depth,state>) ->
61  RowEvidence<input,depth,Packing.next_kernel_row(state)>:
62  RowEvidence{output,cursor,equation,balanced} = evidence
63  RowCursor{i,c,kr,kc,row,offset,ow,h,w,s,p,taps} = cursor
64  %Equal.sym(Packing.RowTiles(),state,restore_row(input,output,RowCursor{i,c,kr,kc,row,offset,ow,h,w,s,p,taps}),equation) : RowEvidence<input,depth,Packing.next_kernel_row(_)>
65  RowEvidence{output,RowCursor{i,c,(kr + 1 : U32),0,row,offset,ow,h,w,s,p,taps},{==},balanced}