CIP-0161 | Ouroboros Phalanx minor changes + formatting

[nhenin]

This PR makes minor documentation updates to CIP‑0161 (Ouroboros Phalanx) and its related CPS‑0021 (Randomness Manipulation).
For the CPS, we fixed TOC rendering glitches caused by LaTeX notation; the CIP frontend and GitHub were not rendering them cleanly.
For the CIP, we added an Agda mechanization section and clarified how Phalanx behaves under VDF amortization attacks.

• Rendered CPS-0021: Ouroboros Randomness Manipulation
• Rendered CPD-0021: Ouroboros Randomness Generation Sub-Protocol - The coin-flipping Problem
• Rendered CIP-0161 Ouroboros Phalanx - Breaking Grinding Incentives

[rrtoledo]

LGTM

[rphair]

Thanks again @nhenin @rrtoledo for your impressively specialised and detailed work, with further appreciation for the maintenance of this quantity of material. All these initial review questions & more can be discussed in person when this update is introduced for Triage at the meeting next week (https://hackmd.io/@cip-editors/126) where you & all your team are welcome as always to attend.

As you say the changes to CIP are mostly formatting but may also have some conceptual differences in the sections not mentioned: so it should get a double-check review from Consensus reviewers. All the changes look good to me personally: though for instance I can't confirm subtle differences like "effectiveness" vs. "security" of the protocol.

To rephrase & maybe add a bit to your list of significant changes above, I'd like to highlight this new material for review:

• (small) CIP new section 5.1 (renumbering all sections below it: ugh) Phalanx Initialization
• (medium) CIP new section 7 Formal specification in Agda
• (potentially BIG in implications) CIP adding new Phalanx protocol parameters

@Ryun1 @perturbing we should find appropriate reviewers to tag for the new protocol parameters in particular... and clarify some standard method for accepting these requests (to also apply to the concurrent #1129 - cc @Cerkoryn).

After we agree upon all structural formalities, we'll tag anyone who reviewed the original Phalanx CIP & CPS submissions plus one or two reviewers from Consensus (cc @ch1bo):

• As decided here, we wouldn't wait for these indefinitely, but should give them enough time to express a constructive interest.
• This should include a reasonable time period for re-review of altered details & new sections: especially for thresholds for fallback to Praos (even if redundant with the recently merged Leios CIP).

Regarding the special characters, with thanks for cleaning those up:

• A lot of the corrected lines with maths text are correcting the English text white space & grammar rather than the maths... but please @nhenin @rrtoledo feel free to call attention to any changes that technical reviewers might miss in that mixture.
• Apologies on behalf of the editors for not noticing any inconsistencies that may have been caused by the non-Roman characters: we'll keep an eye out for similar problems in the future especially in links & section headings, and on the derived web site(s).

---

One thing that we can't submit as a correction since it's not in your change scope: please update your Solution-To: section of the CIP front matter so it's consistent with this repository change in the works (cc @Ryun1 who's coordinating these changes):

• #1125

I believe it will be sufficient to change the CIP front matter to contain:

Solution-To:
  - CPS-0017: https://github.com/cardano-foundation/CIPs/tree/master/CPS-0017
  - CPS-0021: https://github.com/cardano-foundation/CIPs/blob/master/CPS-0021
Discussions:
  - https://github.com/cardano-foundation/CIPs/pull/1065
  - https://github.com/cardano-foundation/CIPs/pull/1131

(@nhenin the CPS will be edited as necessary in #1128 if you continue not to change that README in this branch)

---

Finally @nhenin @rrtoledo please I hope review & correction can continue on this branch without a further force-push: though again we'll trust your judgement about substantial changes & maintenance perhaps being more important to do properly than in a manner that preserves the review & collective editing history. 🙏

[nhenin]

Hi @rphair, I will attend the meeting tonight to present this update. Most of your feedback has been incorporated into my commit, and the points that were not added are explained in the corresponding comments below.

[rphair]

Since #1131 (comment) is again resolved — after needing to look at a possible alternative solution for the numbered headers — editors agreed at the meeting today that the updates look complete and understandable: so marking Confirmed.

Before merge we'd just like to wait for @perturbing to go over it while wearing the "academic" hat, and hopefully getting a corroborative review from @ch1bo or any of the Consensus experts as suggested in #1131 (review).

[rphair]

p.s. for @perturbing and other pending reviewers about issues beyond the Consensus behaviour: even if choosing not to wait indefinitely for a Consensus approval of these updates, before moving on to Last Check (as mentioned already in #1131 (review)) we need to at least record some recommendations here about the implication of adding 2 new protocol parameters (cc @katomm @thenic95).