Forge and search that earns its proof

Hand-optimized kernels are usually folklore with a benchmark attached. Forge treats performance as a search problem that still has to pass verification...