def finish

stelliferous@0.0.2.0 · proofs/traversal_lanes_witness.bend:119

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
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

119def finish(~Context: Data,~map: Context -> F32 -> F32,+depth: Nat,count: Nat,-state: Cells.State<Array<F32>,Tile.Tile8,Context>,evidence: Evidence<Context,depth,state>) ->
120  Witness.Witness(F32,depth,Lanes.finish(~Context,~map,count,state)):
121  match evidence:
122    case Evidence{values,scratch,position,slot,context,equation,values_witness,scratch_witness}:
123      %Equal.sym(Cells.State<Array<F32>,Tile.Tile8,Context>,state,Cells.State{values,scratch,position,slot,context},equation) :
124        Witness.Witness(F32,depth,Lanes.finish(~Context,~map,count,_))
125      TraversalWitness.map_in_place(~F32,~Context,~map,depth,count,position,context,values,values_witness)