Conformance failure: Spec reports that pool is not registered for voting

[aniketd]

Two tests fail with:

(Agda: Left `Dec\xa;(isRegistered (.proj₁ Γ)\xa; (.Ledger.GovernanceActions.GovVote.voter sig))\xa;`)

In these tests, both CCs and an SPO submit their votes, but failure only occurs for the SPO vote submission.

To rerun use:

1. --match "/proposals of same priority are enacted in order of submission/"
2. --match "/only the first action of a transaction gets enacted/"

[WhatisRT]

I think this is most likely either a translation bug or a bug in isRegistered (though that looks fine to me right now). It's probably not a bug with registering the pool, since that certificate is actually implemented (only retiring is broken).

[aniketd]

Noted @WhatisRT, thanks! I have added the investigation label.

[Soupstraw]

This is a bug in genErrors. I tried to normalize the hole here:

        computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
            (yes p , yes p') → case Any↔ .from p of λ where
              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
            (yes _ , no ¬p) → failure (genErrors ¬p)
            (no ¬p , _)     → failure ( {!genErrors ¬p !})

and this is what I got

"Dec\n(isRegistered (.proj₁ Γ)\n (.Ledger.GovernanceActions.GovVote.voter sig))"

As you can see, it gives a nonsensical error, it should be something like lookupActionId pparams (proj₁ voter) gid s instead. I think the problem is that lookupActionId is a proof of existence, and genErrors sees the sigma type and tries to recurse into that thinking it's a conjunction instead of printing out the ∃[_]_ term.

[WhatisRT]

It turns out that this is unrelated to the existential after all. Here's a minimized reproducer:

open import Prelude

test : String
test = case (0 ≟ 1) ,′ (1 ≟ 1) of λ where
    (yes p , _) → ""
    (no ¬p , _) → {!genErrors ¬p!}

Normalizing the hole gives "Dec (1 ≡ 1)" instead of "Dec (0 ≡ 1)" as expected. Currently looking at the code to see where the de-bruijn mistake is.

[WhatisRT]

Ah, the documentation I wrote helpfully immediately reveals the bug:

-- genError: returns the type of the most recently bound variable as a string

So genErrors does all the work of properly going into branches etc., but then the generated error message is just from the most recently bound variable. This makes sense, because if you make a branch, you always want to print the variable just introduced. But if you don't make a branch the most recent might not be the one you actually want to print.

So I suppose we could either do some annoying restructuring, or we add a simple wrapper that always generates a case x of λ x → before doing anything 😂