1	# The compensated GELU mapper, with one scalar tail and two eight-lane stages.
2	import Base
3	import ./math_gelu_lanes.bend as Gelu
4	import ./traversal_lanes.bend as Lanes
5	import ./storage_buffer.bend as Storage
6	import ./proofs/storage_certificate.bend as Certificate
7	import ./proofs/math_gelu_lanes_certificate.bend as GeluCertificate
8	
9	def mapped(+count: Nat,+position: U32,buffer: Storage.Buffer<F32>) -> Storage.Buffer<F32>:
10	  Storage.Buffer{values,length,Certificate.Certificate{+depth,equation}} = buffer
11	  Storage.Buffer{Gelu.map_when(Lanes.covered(depth,position,count),count,position,values),length,
12	    GeluCertificate.map_when(Lanes.covered(depth,position,count),count,position,values,Certificate.Certificate{depth,equation})}