def step

stelliferous@0.0.2.0 · proofs/traversal_lanes_witness.bend:110

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/traversal_cells.bend as Cells
import stelliferous@0.0.2.0/kernel_tile.bend as Tile

110def step(~Context: Data,~map: Context -> F32 -> F32,+depth: Nat,-state: Cells.State<Array<F32>,Tile.Tile8,Context>,evidence: Evidence<Context,depth,state>) ->
111  Evidence<Context,depth,Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,state)>:
112  match evidence:
113    case Evidence{values,scratch,+position,+slot,+context,equation,+values_witness,scratch_witness}:
114      %Equal.sym(Cells.State<Array<F32>,Tile.Tile8,Context>,state,Cells.State{values,scratch,position,slot,context},equation) :
115        Evidence<Context,depth,Cells.step(~Array<F32>,~Tile.Tile8,~Context,~Lanes.gather(~Context,~map),~Lanes.scatter,~8,_)>
116      stored(~Context,~map,depth,values,scratch,position,slot,context,values_witness,scratch_witness,
117        gather(~Context,~map,depth,values,position,context,values_witness))