RATIFY Conformance test failure on CI

[lehins]

This failure appeared on #5161 PR

           rsDelay = (Impl: False) (Agda: True)}

  To rerun use: --match "/Conway/Conformance/Ticks transition graph/RATIFY/" --seed 1076768625

Randomized with seed 1076768625

Finished in 1372.5483 seconds
267 examples, 1 failure, 127 pending

[Soupstraw]

Here's what I found out after digging around a bit:

• The failure happened because a change to the constitution was passed in the spec, but not in the implementation
• The constitutional committee is inactive because the number of active members is below the threshold (8 active, 78 required)
• The thresholds for accepting a change to the constitution was set to zero for both the DReps and CCs, SPOs don't need to vote
• The proposal had no valid votes

[lehins]

Yes, according to many discussions I had with @WhatisRT and others we wanted to allow ratification of proposals without committee only when there is an empty committee with threshold set to 0 and ppCommitteeMinSizeL is also set to zero:

cardano-ledger/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Internal.hs

Lines 474 to 492 in 5d37e3a

	threshold =
	case committeeThreshold <$> committee of
	-- when we are not in a bootstrap phase,
	-- if the committee size is smaller than the minimum given in PParams,
	-- we treat it as if we had no committee
	SJust t
	| hardforkConwayBootstrapPhase (pp ^. ppProtocolVersionL)
	|| activeCommitteeSize >= minSize ->
	VotingThreshold t
	_ -> NoVotingThreshold
	minSize = pp ^. ppCommitteeMinSizeL
	isActive coldKey validUntil =
	case Map.lookup coldKey hotKeys of
	Just (CommitteeMemberResigned _) -> False
	Just _ -> currentEpoch <= validUntil
	Nothing -> False
	activeCommitteeSize =
	fromIntegral . Map.size . Map.filterWithKey isActive $
	foldMap' committeeMembers committee

[WhatisRT]

Here's the line in the spec that I'd expect to reject a proposal with a too small CC: https://github.com/IntersectMBO/formal-ledger-specifications/blob/b022bf45ed09b124bb271c4d6626fa0105b0b40b/src/Ledger/Conway/Ratify.lagda#L434

I think it would be nice to have a decent pipeline to turn test failures into a Haskell module that can be compiled against the spec, which would make this much easier to investigate. Maybe you can do something like show (toSpecType testCase) and we can put the result of that into a relatively generic file?

[Soupstraw]

I'll try to implement an ImpTest that exemplifies this bug, the original test case was huge and a pain to work with.

[Soupstraw]

I might still be missing some detail, I tried writing a minimal ImpTest to reproduce the issue, but it's passing conformance
#5184

[Soupstraw]

Here's the original test failure:
test.txt

[Soupstraw]

I created a branch called jj/conformance-failure at the commit where the failure happens.

This runs the test:
cabal test cardano-ledger-conformance --test-options='--match "/Conway/Conformance/Ticks transition graph/RATIFY/" --seed 1076768625'

[Soupstraw]

Ok, I realize why my hand-written test did not reproduce the error. The reason is that we don't currently run conformance on the epoch boundary, but that's where the RATIFY rule gets run.