Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Cannot register and deregister same stake credential #547

Merged
merged 19 commits into from
Oct 18, 2024
Merged

Cannot register and deregister same stake credential #547

merged 19 commits into from
Oct 18, 2024
+553 −442

Conversation

williamdemeo
Copy link
Contributor

Description

This addresses issue #512

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • Code is formatted according to CONTRIBUTING.md
  • Self-reviewed the diff

@williamdemeo williamdemeo linked an issue Aug 16, 2024 that may be closed by this pull request
Cannot register and deregister (or the other way) the same stake credential in the same transaction #512
Closed
2 tasks
@williamdemeo williamdemeo marked this pull request as draft August 16, 2024 19:58
@williamdemeo williamdemeo force-pushed the 512-cannot-register-and-deregister-stake-credential branch from e5935a3 to af99909 Compare October 9, 2024 13:14
@williamdemeo williamdemeo marked this pull request as ready for review October 10, 2024 06:22
WhatisRT
WhatisRT requested changes Oct 10, 2024
View reviewed changes
Copy link
Collaborator

@WhatisRT WhatisRT left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think all the changes in Ledger.Certs and Ledger.Epoch are just reverting formatting/cleanup that I've done over a month ago. Can you revert those two files?

Also, note that Ledger.Utxo is a literate file, so please make sure it looks good in the PDF. In particular, the decision procedure should be hidden, and ValidCertDeposits might be better explained in prose than shown in a figure.

Otherwise, I think this looks pretty good!

WhatisRT
WhatisRT reviewed Oct 10, 2024
View reviewed changes
Copy link
Collaborator

@WhatisRT WhatisRT left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, sorry, I spoke too soon. I wrote

Check the correctness of refunds in UTXO

in the issue, but what I meant was to check it there instead of in CERTS. So it's also necessary to remove those checks from CERTS, because that's what actually prevents us from registering and deregistering in the same transaction. I think the best way to do that is to remove deposits from CertEnv and all the other environments in the file and then follow all the errors.

Note that this also means that ValidCertDeposits needs to be slightly adjusted, so that all the removed checks are done there. In particular, it also needs to check deposit amounts, so it needs to have a Deposits argument rather than ℙ DepositPurpose. I don't think it should affect much though.

@williamdemeo
Copy link
Contributor Author

I think all the changes in Ledger.Certs and Ledger.Epoch are just reverting formatting/cleanup that I've done over a month ago. Can you revert those two files?

I made (most of) those changes to try to ensure that the vertical vector formatting doesn't get confused by the line breaks. (The insertion of the module with no parameters was a mistake.) In any case, I'll revert the changes and check if the pdf looks okay. But I may need to reformat the vectors as long single lines so they look okay in the pdf.

@williamdemeo
Copy link
Contributor Author

Ah, sorry, I spoke too soon. I wrote

Check the correctness of refunds in UTXO

in the issue, but what I meant was to check it there instead of in CERTS. So it's also necessary to remove those checks from CERTS, because that's what actually prevents us from registering and deregistering in the same transaction. I think the best way to do that is to remove deposits from CertEnv and all the other environments in the file and then follow all the errors.

Note that this also means that ValidCertDeposits needs to be slightly adjusted, so that all the removed checks are done there. In particular, it also needs to check deposit amounts, so it needs to have a Deposits argument rather than ℙ DepositPurpose. I don't think it should affect much though.

@UlfNorell do you have time to work on these changes? I'd like to get back to finishing the Ledger pov PR and work on issue #578?

Btw, I merged your branch into the one on which this PR is based and fill the remaining holes and rewrote some of the proofs, so it now type-checks and passes the CI. I suppose you will want to make a new branch off this one like you did last time (assuming you have time to work on this). Thanks!!

@UlfNorell
Copy link
Collaborator

@williamdemeo I'll try to make some progress today. If it's ok with you I'll just push to this branch. Last time was a major change to the way things were done, but now it's just continuing work on the PR.

@williamdemeo
Copy link
Contributor Author

williamdemeo commented Oct 11, 2024 via email

@WhatisRT
Copy link
Collaborator

But I may need to reformat the vectors as long single lines so they look okay in the pdf.

Did something change that affects the vectors? I remember being able to strategically insert newlines in certain places without them affecting how the PDF renders. Also, if I look at CERTBASE and certState' in EPOCH, they look fine in the PDF right now, I don't see what needs to be fixed.

@williamdemeo
Copy link
Contributor Author

But I may need to reformat the vectors as long single lines so they look okay in the pdf.

Did something change that affects the vectors? I remember being able to strategically insert newlines in certain places without them affecting how the PDF renders. Also, if I look at CERTBASE and certState' in EPOCH, they look fine in the PDF right now, I don't see what needs to be fixed.

Ah, sorry, I didn't realize the script output could be manipulated by strategically inserting newlines. I guess nothing needs to be fixed then. 👍🏼

@williamdemeo
Copy link
Contributor Author

@UlfNorell I just merged the latest master, so I suggest a git pull before doing more work on this.

@UlfNorell
Move dereg checks from CERT rules to UTXOS
8b77b71 
Note: this also changes the check for `deregdrep c d` to
        (DRepDeposit c , d) ∈ deps
      from
        (CredentialDeposit c , d) ∈ deps
UlfNorell
UlfNorell reviewed Oct 11, 2024
View reviewed changes
src/Ledger/Certs.lagda
⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys ⟧ᵛ

GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (CredentialDeposit c , d) ∈ deps
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this have been (DRepDeposit c , d) ∈ deps? That's what I put in ValidCertDeposits.

@UlfNorell
Copy link
Collaborator

I think I managed moving the checks from CERT to ValidCertDeposits. There were just one small question about whether the check in GOVCERT-deregdrep was wrong before.

@williamdemeo
Copy link
Contributor Author

I just requested a review from @WhatisRT, but I still need to check the pdf. I will do that today.

@williamdemeo
Merge branch 'master' into 512-cannot-register-and-deregister-stake-c…
472e46f 
…redential
@williamdemeo
add missing functionality
b60144a
@williamdemeo
fix pdf
37ca31f 
+ show `ValidCertDeposits` type declaration but hide definition
+ hide `ValidCertDeposits?`  decision procedure
+ add explanation of `ValidCertDeposits` to prose
@williamdemeo
Copy link
Contributor Author

@WhatisRT I finished fixing the pdf. I think this PR is good to go now.

WhatisRT
WhatisRT approved these changes Oct 16, 2024
View reviewed changes
Copy link
Collaborator

@WhatisRT WhatisRT left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just some minor stuff, otherwise LGTM

src/Ledger/Utxo.lagda Outdated Show resolved Hide resolved
src/Ledger/Utxo.lagda Outdated Show resolved Hide resolved
src/Ledger/Utxo.lagda Outdated Show resolved Hide resolved
src/Ledger/Utxo.lagda Outdated Show resolved Hide resolved
@williamdemeo williamdemeo merged commit eed1ca0 into master Oct 18, 2024
8 checks passed
@williamdemeo williamdemeo deleted the 512-cannot-register-and-deregister-stake-credential branch October 18, 2024 02:22
github-actions bot added a commit that referenced this pull request Oct 18, 2024
@github-actions
Generate code for GH-547
af9a54a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@UlfNorell UlfNorell UlfNorell left review comments

@WhatisRT WhatisRT WhatisRT approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Cannot register and deregister (or the other way) the same stake credential in the same transaction
3 participants
@williamdemeo @UlfNorell @WhatisRT