Cannot register and deregister (or the other way) the same stake credential in the same transaction

[WhatisRT]

This is because the deposits are updated in UTXO, so during CERT the deposits map is not being updated and only at most one of those certs will be valid.

Here are some ways of fixing this:

• [ ] ~Add a temporaryDeposits field to CertState, that is updated and properly but then discarded~
• [ ] Check the correctness of refunds in UTXO, maybe during updateCertDeposits

[TimSheard]

Consider this work around.

newtype DeltaDeposit = DeltaDeposit (Map DepositPurpose DeltaCoin) emptyDD = DeltaDepost Map.empty delta :: DeltaDeposit ->Cert -> DeltaDeposit addDD, subDD :: DeltaDeposit -> CertState -> CertState To add and subtract the changes to the CertState

In a transaction with N certs, we let deltaDD = foldl' delta emptyDD certs In the conformance test, in the CERTS rule we subtract the delta deposits (since the Agda rule didn't add them) In the UTXO rule we add the delta deposits, since the Agda rule added them but the STS rule did not.

[TimSheard]

1) Define DepositPurpose (Teodora) 2) Define DeltaDeposit (Teodora) 3) CertState -> DeltaDeposit (all the deposits) (Teodora) 3) write addDD and subDD (maybe CertState is not the right State since Proposal deposits may not be in there) (Tim) 4) Generate a ExecSpecRule Environment and ExecSpecRule State that align on deposits (Tim) 5) write code for conformance testing that uses this stuff to equate the STS State and the ExexRuleSpec state (??)

[TimSheard]

Something strange going on here. There are 4 constructors in the DELEG signal.

data ConwayDelegCert c
  = -- | Register staking credential. Deposit, when present, must match the expected deposit
    -- amount specified by `ppKeyDepositL` in the protocol parameters.
    ConwayRegCert !(StakeCredential c) !(StrictMaybe Coin)
  | -- | De-Register the staking credential. Deposit, if present, must match the amount
    -- that was left as a deposit upon stake credential registration.
    ConwayUnRegCert !(StakeCredential c) !(StrictMaybe Coin)
  | -- | Redelegate to another delegatee. Staking credential must already be registered.
    ConwayDelegCert !(StakeCredential c) !(Delegatee c)
  | -- | This is a new type of certificate, which allows to register staking credential
    -- and delegate within a single certificate. Deposit is required and must match the
    -- expected deposit amount specified by `ppKeyDepositL` in the protocol parameters.
    ConwayRegDelegCert !(StakeCredential c) !(Delegatee c) !Coin

But the spec only has 2 rules for DELEG Figure 22 page 25. why is that? Are we not showing some of the rules that already appear in earlier Eras?

[jmchapman]

@WhatisRT - William's initial version uses the first suggestion above "Add a temporaryDeposits field to CertState, that is updated and properly but then discarded".

Does this solve the problem? If so, in the interests of time would it make sense to go with this and add a possible later refactoring as a separate issue in the backlog?

[WhatisRT]

We agreed to push this back a bit. When this issue is continued it makes sense to interleave this work with #467 to some degree.

It is also probably a good idea to make an STS version of the deposit update functions. This should make the POV proof a bit easier. There are two options here:

• Either make it only a tool for the proof, basically showing that compute for this STS is extensionally equal to updateDeposits. Then the new STS wouldn't show up in any literate files and would be completely in the background.
• Actually expose the new STS. This has the benefit of not having to prove an extra equality but it means that we now have an STS that's not in the implementation. I'd only go for this option if it is sufficiently nicer.