Update proven security to include IOP terms

[Al-Kindi-0]

The way we compute the proven security in get_proven_security takes into account only the FRI soundness error part $\epsilon_{FRI}$. It would be great to include the terms coming from the protocol pre-FRI.
I believe the update expression should be like:

$$ L^{+}\cdot\left(\frac{1}{|\mathbb{F}|} + \frac{d\cdot(k^+ - 1) + (k-1)}{|\mathbb{F}| - |D\cup H|}\right) + \epsilon_{FRI} $$

where:

1. $H$ is the trace domain of size $k$
2. $D$ is the LDE domain of size $n$
3. $k^+ := k + 2$
4. $L^+ := \frac{m+0.5}{\sqrt{\rho^+}}$ where $m\geq 3$ is the Johnson proximity parameter which for simiplicity can be taken to be equal to $3$ and $\rho^+ := \frac{k^+}{n}$
5. $\mathbb{F}$ is the extension field.
6. $\epsilon_{FRI}$ is the soundness error bound for FRI run with proximity parameter $\theta^+ := 1 - \alpha^+ := 1 - (1 + \frac{1}{2m})\cdot \sqrt{\rho^+}$
7. $d$ is the number of constraint composition column polynomials.

[pdg744]

Not sure I'm reading this right; it looks like you're saying $d$ is the number of constraints? Or maybe constraint composition column polynomials is the number of segment polynomials?

Ulrich defines $d$ as the maximum degree of the constraints, but I think the expression in the error bound is actually the number of segment polynomials.

[irakliyk]

Closed by #215.