Final computational instances #240
Conversation
|
Thank you! Maybe we can have a quick look at it in the meeting soon? One thing I can point out right now is that CI is failing since |
UlfNorell
force-pushed
the
final-computational-instances
branch
from
232ce06 to
523fb93
Compare
There was a problem hiding this comment.
I've found just a few things, mostly relating to the PDF. However, I believe @omelkonian will complain about long lines.
There was a problem hiding this comment.
LGTM overall, but the RATIFY proof could use some love.
Here's an alternative approach that tackles the issue at its root, namely making the initial definitions of accepted/expired/... properly abstract, which leads to a much cleaner proof that the RATIFY relation is computational.
The downside of course is that the decision procedures have to be put in the same file (i.e. Ledger.Ratify.lagda), breaking modularity a bit, however that can be tackled in Agda-2.6.4 using opaque. Since @UlfNorell's next step is to bump the Agda version, it might seem reasonable to revisit this PR immediately after that so that we can have the best of both worlds.
PS: The branch above also contains some minor cleanups on the other files (Chain/NewPP) and a handful of constructor patterns to make life easier when working on RATIFY:
pattern RATIFY-Continue₁ x y = RATIFY-Continue (inj₁ (x , y))
pattern RATIFY-Continue₂ x y = RATIFY-Continue (inj₂ (x , y))
pattern RATIFY-Continue₂₁ x y = RATIFY-Continue₂ x (inj₁ y)
pattern RATIFY-Continue₂₂ x y = RATIFY-Continue₂ x (inj₂ y)Feel free to cherry-pick regardless of how we handle the abstraction issue above.
Alternatively, if we want this PR merged ASAP, we can create a new issue from the above discussion, and clean up the current approach as I demonstrate here: apart from overall styling fixes (e.g. for smaller lines), it avoids repetition by formulating what we are abstracting over explicitly and bundling all (abstracted) arguments in a tuple.
UlfNorell
force-pushed
the
final-computational-instances
branch
from
e65bce5 to
2d801bc
Compare
Update Computational record in Introduction Remove unnecessary abstracts Decidable comparison of rationals Computational instance for RATIFY and fix minor bug in rule Computational instance for NEWEPOCH Computational for NEWPP and fix NEWPP-Reject rule Computational instance for CHAIN and fix rule import NewPP.Properties in Everything.agda Go back to the old Computational in the Introduction Remove minimumAVS check from Ratify.accepted Remove spurious blank line Abstract definitions for cleaner Ratify.Properties (#247) Co-authored-by: Orestis Melkonian <[email protected]>
UlfNorell
force-pushed
the
final-computational-instances
branch
from
2d801bc to
22a5d18
Compare
|
@WhatisRT it's now ready to approve and merge. |
Fixes #147
This adds Computational instances for the remaining rules.
Also fixes some minor issues in a few of the rules (
RATIFY',NEWPPandCHAIN)