refactor CERTS rule #922
refactor CERTS rule #922
Conversation
|
The Haskell code generated from this branch (in |
carlostome
left a comment
carlostome
left a comment
There was a problem hiding this comment.
Good work! I left some comments here and there.
| CERT-base : | ||
| data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where | ||
|
|
||
| CERT-init : |
There was a problem hiding this comment.
Maybe?
| CERT-init : | |
| CERT-pre : |
|
|
||
| data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where | ||
|
|
||
| CERT-last : |
There was a problem hiding this comment.
| CERT-last : | |
| CERT-post : |
There was a problem hiding this comment.
I'd suggest a consistent naming for the PRE-CERT and POST-CERT constructors (first-last e.g.). I did leave a suggestion.
|
|
||
| The governance state used as input to `GOVS`{.AgdaDatatype} is filtered to | ||
| remove votes from `DRep`{.AgdaInductiveConstructor}s that are no longer | ||
| remove votes from DReps that are no longer |
There was a problem hiding this comment.
I've been doing the opposite elsewhere. We should come to a consistent agreement about this.
There was a problem hiding this comment.
Yes, we should be consistent about this. It's not clear to me that AgdaInductiveConstructor (or any other special Agda highlighting class) is what we want though... which is why I proposed no formatting at all.
There was a problem hiding this comment.
After thinking about it, I suppose since DRep is a (constructor of a) GovRole, the AgdaInductiveConstructor class makes sense. Okay, let's adopt that convention (i.e., DRep{.AgdaInductiveConstructor}) throughout.
williamdemeo
force-pushed
the
726-fix-certbase
branch
from
1e23053 to
78051c0
Compare
This is a first step to refactoring the CERTS rule. Ultimately we will deprecate the "CERTBASE" rule and replace it with "preCerts" and "postCerts" functions that will run before and after the CERTS sts. Some of the things that currently happen in CERTBASE may be moved into the LEDGER rule. revert CERTS rule in conformance version
Plus, + computational proofs for new pre-cert and post-cert rules + PoV proofs for new CERTS rule + Refactor equivalence proofs for new CERTS rule. + fix some formatting in Ledger module Also, removed `AgdaInductiveConstructor` class from occurrences of "DRep" in the text; this makes it easier to be consistent throughout the document, but even if we do want to use Agda high-lighting for "DRep", it's not clear to me that `AgdaInductiveConstructor` is the right class to use.
and fix bug introduced by rebase
williamdemeo
force-pushed
the
726-fix-certbase
branch
from
78051c0 to
2ecec7b
Compare
williamdemeo
force-pushed
the
726-fix-certbase
branch
from
ed0861c to
1ae6334
Compare
2 participants
Description
The first step is to revert
CERTSto runningCERTBASElast. Ultimately we will probably deprecate the "CERTBASE" rule and replace it with "preCerts" and "postCerts" functions that will run before and after theCERTSsts. Some of the things that currently happen inCERTBASEmay be moved into the LEDGER rule.Checklist
CHANGELOG.md