Make all STSs in the Agda spec executable

[javierdiaz72]

As the first task in implementing conformance testing with respect to the formal specification, we shall focus on making all the State Transition Systems (STSs) within the formal spec executable.

[WhatisRT]

One nice thing about the Computational class is that you can't make any wrong instances. It it type checks, it's correct. That being said, you could provide more informative error messages if you do (no ¬p) → failure (genErrors ¬p) instead of (no _) → failure "My error string". genErrors will branch on all the different possibilities for ¬p and generate an error message based on their type. They are really ugly, but they tell you what went wrong (and they'll never be incorrect if you move some things around).

[javierdiaz72]

@WhatisRT: Thanks a lot for your review, I have just changed the code to use genErrors whenever possible (I got a type error when trying to use it for one of the STSs).

@IntersectMBO/ouroboros-consensus-maintainers: The PR is now ready to be merged.

[nfrisby]

1. I did not explicitly check for missing logic. But I didn't notice any glaring omissions.
2. I did not scrutinize all the chicken scratches... the conformance checking we're working towards has the wonderful benefit of bidirectionality, so I'm deferring the typo-hunting until we're guided by known disagreements.
3. We prefer rebasing PR branches onto main instead of merging main into branches. Especially since this directory is your sovereign domain, I would expect a rebase is trivial for you to execute locally. (please eliminate the merge commit f65e92a)
4. I would expect to find this kind of notation inscribed on the stone walls of an asylum cell.

module _ (M : Type↑) where
  _⁴ : ∀ {ℓ} {A B C D : Type ℓ} → (A → B → C → D → Type ℓ) → Type _
  _⁴ _~_~_~_ = ∀ {x y z w} → M (x ~ y ~ z ~ w)

_⁇⁴ = _⁇ ⁴

Just teasing :D, I'll be happy to understand it better some day (mumble mumble passing dictionaries implicitly?)

[javierdiaz72]

@nfrisby:

please eliminate the merge commit f65e92a)

Done. but now my commits show up as unverified. How can we fix this so that we can merge the PR?

[amesgen]

@nfrisby:

please eliminate the merge commit f65e92a)

Done. but now my commits show up as unverified. How can we fix this so that we can merge the PR?

Hmm, usually, rebasing should also cause the commits to be re-signed. If you don't have any other changes from this PR, I or someone else from the Consensus team can also rebase (only the committer needs to sign, not the author).

[jasagredo]

You can use this @javierdiaz72

git rebase --exec 'git commit --amend --no-edit -n -S' -i HEAD~<N>

where <N> is the number of commits to sign, in your case 4.