-
Notifications
You must be signed in to change notification settings - Fork 158
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.
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
Alonzo audit #2448
Alonzo audit #2448
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
looks good to me!
\nextdef | ||
& \fun{feesOK} \in \PParams \to \Tx \to \UTxO \to \Bool \\ | ||
& \fun{feesOK}~\var{pp}~tx~utxo~= \\ | ||
&~~ \minfee{pp}~{tx} \leq \txfee{txb} \wedge (\fun{txrdmrs}~tx \neq \Nothing \Rightarrow \\ | ||
&~~~~~~((\forall (a, \wcard, \_) \in \fun{range}~(\fun{collateral}~{txb} \restrictdom \var{utxo}), \fun{paymentHK}~a \in \AddrVKey) \\ | ||
&~~~~~~((\forall (a, \wcard, \_) \in \fun{range}~(\fun{collateral}~{txb} \restrictdom \var{utxo}), a \in \AddrVKey) \\ | ||
&~~~~~~\wedge~ \fun{adaOnly}~\var{balance} \\ | ||
&~~~~~~\wedge~ \var{balance}~*~100 \geq \txfee~{txb} * (\fun{collateralPercent}~pp))) \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
i think this has a couple extra brackets? I'm having a hard time tracking them here hehe
&~~~~~~\wedge~ \fun{adaOnly}~\var{balance} \\ | ||
&~~~~~~\wedge~ \var{balance}~*~100 \geq \txfee~{txb} * (\fun{collateralPercent}~pp))) \\ | ||
&~~~~~~\wedge~ \fun{collateral}~{tx}~ \neq~\{\} \\ | ||
&~~~~~~\wedge~ \fun{collateral}~{tx}~ \neq~\{\}) \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
i think this closes the line 21 first bracket?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, I think the parentheses are fine
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ok
@@ -659,7 +663,7 @@ \subsection{The UTXOS transition system} | |||
\var{txb}\leteq\txbody{tx} & | |||
\fun{ininterval}~\var{slot}~(\fun{txvldt}~{tx}) & | |||
\hldiff{\var{(\wcard, i_f)}\leteq\fun{txvldt}~{tx}} \\~\\ | |||
\hldiff{\fun{txrdmrs}~\var{tx}\neq \Nothing ~\Rightarrow~ \fun{epochInfoSlotToUTCTime}~\mathsf{epochInfo}~\mathsf{systemTime}~i_f \neq \Nothing} \\ | |||
\hldiff{\Nothing \notin \{\fun{txrdmrs}~\var{tx}, i_f\} ~\Rightarrow~ \fun{epochInfoSlotToUTCTime}~\mathsf{epochInfo}~\mathsf{systemTime}~i_f \neq \Nothing} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
\notin?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a compact way of saying that both of those aren't Nothing. So this modifies the line to only check the conversion if i_f
isn't nothing as well
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
right, didnt notice it was \notin ... a set
two tiny things (which maybe Im just confused about, looks really good otherwise) |
Lots of small changes/additions pointed out by different audits