652 remove superscripts from rec constr #655
Conversation
carlostome
force-pushed
the
652-remove-superscripts-from-rec-constr
branch
from
c56a925 to
b08b87f
Compare
|
This is currently blocked by #653 |
carlostome
force-pushed
the
652-remove-superscripts-from-rec-constr
branch
from
675be19 to
ef77a0e
Compare
carlostome
force-pushed
the
652-remove-superscripts-from-rec-constr
branch
from
8c1cc29 to
f5a6fb8
Compare
carlostome
force-pushed
the
652-remove-superscripts-from-rec-constr
branch
from
e9c13f9 to
8b8148e
Compare
This comment was marked as outdated.
This comment was marked as outdated.
|
We need to decide what the name for |
| field | ||
| Δt Δr Δf : ℤ | ||
| rs : Credential ⇀ Coin | ||
| \end{code} | ||
| \begin{code}[hide] | ||
| -- more convient here than doing checks | ||
| {zeroSum} : Δt + Δr + Δf + ℤ.+ ∑[ x ← rs ] x ≡ ℤ.0ℤ |
There was a problem hiding this comment.
I'm not sure why this {zeroSum} line was included in the first place, so I'm not sure why it can be removed. 😅
There was a problem hiding this comment.
I'm not sure either why the field is there. Nothing seems to break if I simply remove it.
@WhatisRT, do you know the purpose of this field?
There was a problem hiding this comment.
It's going to be relevant for the preservation of ada proof. RewardUpdate is constructed at some point during the epoch and then applied (see applyRUpd) at the epoch boundary (this is something we could potentially change in the future, because IIRC this is purely done for performance reasons, but that's another topic). When we apply the RewardUpdate the amount of ada in the system changes by this sum, which is why we need it to be zero. So I think there are only two options to deal with this:
- weaken the statement to something like 'ada is preserved if the
RewardUpdatewas correctly constructed', or - just do it correct-by-construction as is done here.
We usually don't do correct-by-construction in our data for various reasons (e.g. it makes translation for conformance tests more difficult), but here it seemed like a good choice because it disturbs very little and we actually get a stronger property in the end.
There was a problem hiding this comment.
I'd suggest for now removing this (having a hidden field complicates things in using the uniform constructor approach), and when (and if) needed it we put it back.
| b c : Bool | ||
|
|
||
| instance | ||
| unquoteDecl To-R'' = derive-To ⦃ defaultTCOptions ⦄ ((quote R'' , To-R'') ∷ []) |
There was a problem hiding this comment.
I'm still trying to understand how the metaprogramming logic works, so I won't comment on this part of the PR.
| @@ -148,7 +149,7 @@ instance | |||
| ledger' : Γ C.⊢ (getCertDeps* cdeposits ⊢conv s) ⇀⦇ tx ,LEDGER⦈ C.⟦ utxoStC' , govSt' , certStateC' ⟧ˡ | |||
| ledger' = C.LEDGER-V⋯ refl utxow' certs' gov' | |||
| utxoEq : utxoStC' ≡ utxoSt' | |||
| utxoEq = cong (λ • → L.⟦ _ , _ , • , _ ⟧ᵘ) | |||
| utxoEq = cong (λ • → ⟦ _ , _ , • , _ ⟧) | |||
There was a problem hiding this comment.
I'm surprised you can remove both the superscript and the L. here. 🤔 I suppose I should try to understand the metaprogramming you did to see why this works.
There was a problem hiding this comment.
This is about an instance of To for RewardsUpdate being in scope.
There was a problem hiding this comment.
I really like this, but it's a shame that we're losing some of the patterns here. I think some of them should be resurrected. Here's the most obvious place where things got worse. Before:
After:
Obviously this has other issues as well, but in the before it's really easy to see what changed and maybe more crucially what didn't change (and that e.g. the reserves and treasury didn't get swapped), and in the after this is completely gone (and just adding the vertical vectors back in isn't going to fix it). There are a few other places such as UTXOW.
It's a shame that it's not quite as powerful as Lean's ⟨ ⟩ which also functions as a pattern on the LHS, but there probably isn't much we can do about that. I think in the above cases, it would be good to keep the patterns around just to render those more nicely.
Maybe it could be a future AIM project to get such record patterns that can be used for matching as well?
|
The before/after differences are due to a bug in the |
|
If #666 is fixed then it still doesn't resolve the problem. In the before picture, the LHS provides quite a lot of information visually, just by being able to line up matching entries on the RHS. This gets lost completely if the LHS is just |
Checklist
CHANGELOG.md