It looks there is a workaround now:

func nttMul(f, g nttElement) nttElement {
	var h nttElement
	for i := 0; i < 256; i += 2 {
		a0, a1 := f[i], 
		f[i+1]
		b0, b1 := g[i], 
		g[i+1]
		_, _, _, _ = a0, a1, b0, b1
	}
	return h
}

Not benchmark it yet.

[edit] BTW, why not use slices as arguments:

func nttMul(f, g []fieldElement) nttElement {
	var h nttElement
	f, g = f[:256], g[:256]
	for i := 0; i < 256; i += 2 {
		a0, a1 := f[i], 
		f[i+1]
		b0, b1 := g[i], 
		g[i+1]
		_, _, _, _ = a0, a1, b0, b1
	}
	return h
}

That does indeed remove the bounds checks on f, but we get one on gammas[i/2], which also feels avoidable.

Slices should in theory add overhead compared to const size arrays and remove information from the type system

Yes, there are still several cases BCE fails to handle.

Now, a workaround is to double the length of gammas and only uses its elements at 2N indexes.

Now, a workaround is to double the length of gammas and only uses its elements at 2N indexes.

Interestingly, that benchmarks decidedly worse, eating between 10% and 20% of the speedup of dropping the f bounds checks. 🤷

It is possible. BCE will not always get positive effects.

Another way to remove all bound checks is declare fieldElement as [2]uint16. I'm not sure about the final effect.

The test shows that double length of gammas is the most performant: https://gotipplay.golang.org/p/VKJDqUPuhKV (maybe the implementation of fieldMul and fieldAdd will affect the results).

goos: linux
goarch: amd64
pkg: example.com
cpu: Intel(R) Core(TM) i5-4210U CPU @ 1.70GHz
Benchmark_f1-4   	 1762314	       680.7 ns/op
Benchmark_f2-4   	 3191974	       374.8 ns/op
Benchmark_f3-4   	 3488221	       343.2 ns/op
Benchmark_f4-4   	 1893159	       630.0 ns/op

Simple reproducer:

func f(a [256]byte) {
	for i := 0; i < 128; i++ {
		_ = a[2*i]
	}
}

We should be able to get rid of the bounds check. Currently I think it fails because the prove pass can't tell that the math 2*i doesn't overflow and become negative. It does seem to grok that 2*i < 256.
Should be fixable. That code is delicate though, it is not immediately obvious to me where that fix would go.