// r0 = l0×l0 + 19×2×(l1×l4 + l2×l3)
	r0 := uint128{"r0", GP64(), GP64()}
	mul64(r0, 1, l0, l0)
	addMul64(r0, 38, l1, l4)
	addMul64(r0, 38, l2, l3)

	// r1 = 2×l0×l1 + 19×2×l2×l4 + 19×l3×l3
	r1 := uint128{"r1", GP64(), GP64()}
	mul64(r1, 2, l0, l1)
	addMul64(r1, 38, l2, l4)
	addMul64(r1, 19, l3, l3)

	// r2 = = 2×l0×l2 + l1×l1 + 19×2×l3×l4
	r2 := uint128{"r2", GP64(), GP64()}
	mul64(r2, 2, l0, l2)
	addMul64(r2, 1, l1, l1)