Formal spec update #2353

polinavino · 2021-06-24T04:33:13Z

Comments that have come up over the last couple of weeks (including Sebastian's)
First attempt at "script evaluation is deterministic" property
JIRA ticket CAD-3056

Not in here (coming up in next PR):

some renaming
txInfo
Datums only for inputs or outputs check

alonzo/formal-spec/properties.tex

WhatisRT · 2021-06-24T10:54:10Z

alonzo/formal-spec/properties.tex

+\begin{property}[Script interpreter arguments are fixed (deterministic script evaluation)]
+  \label{prop:fixed-inputs}
+
+For this property to hold, we make an important assumption about the Plutus script


This paragraph is vacuously true because we're talking about mathematical functions instead of program code

True, I will leave it in as a note and make the function vs code distinction

alonzo/formal-spec/properties.tex

WhatisRT · 2021-06-24T10:58:44Z

alonzo/formal-spec/properties.tex

+    e\vdash s\trans{ledger}{tx}s', \\
+    e'\vdash u\trans{ledger}{tx'}u', \\
+    \txbody{tx} = \txbody{tx'}, \\
+    (\fun{languages}~(\fun{txwits}~{tx}))~\restrictdom~\fun{costmdls}~(\field_{pp}(s))~=~(\fun{languages}~(\fun{txwits}~{tx'}))~\restrictdom\fun{costmdls}~(\field_{pp}(s')), \\


This should not be a precondition, but a conclusion from the wppHash

yeah! I forgot to remove this after i figure that too

WhatisRT · 2021-06-24T11:12:56Z

alonzo/formal-spec/properties.tex

+      in order to proceed to phase-2, wherein $\fun{evalScripts}$ is run
+    \end{itemize}
+
+    \item The second argument is a list. We will show that it must be the same list for the $e, s, tx, s'$


This proof seems to be mostly a repetition of the properties already discussed in the main text. I think this should be more formal instead. Also, I don't think it's necessary to remind the reader about what a function does here. They probably need to refer to its definition anyway if they don't remember.

JaredCorduan · 2021-07-06T14:24:58Z

alonzo/formal-spec/utxo.tex

-    & \fun{isNonNativeScriptAddress} \in \Tx \to \Addr \to \Bool \\
-    & \fun{isNonNativeScriptAddress}~tx~a = \\
+    & \fun{isTwoPhaseScriptAddress} \in \Tx \to \Addr \to \Bool \\
+    & \fun{isTwoPhaseScriptAddress}~tx~a = \\


this is certainly an improvement, I appreciate it, now the code and the spec agree. unfortunately 😬 we may have to change it again, just a heads up, sorry

WhatisRT

Looks good in general, but I found some small issues and typos

WhatisRT · 2021-07-06T13:58:28Z

alonzo/formal-spec/properties.tex


 \begin{lemma}
  For all environments $e$, transactions $tx$ and states $s, s'$ such that
  \begin{equation*}
-    e\vdash s\trans{ledger}{tx}s',
+    e\vdash s\trans{ledger}{tx}s'~\wedge~\fun{collateralPercent}~(\field_{pp}~(s))~\geq~100


This seems a bit awkward, why not use the φ function from above and multiply minfee below with collateralPercent instead of requiring this condition?

i think the usefulness of this lemma comes from the idea that we want to establish some conditions under which we can guarantee that the transaction pays the minfee

I'm not sure we care about the minfee specifically, only that it pays a fee if we want it to. But the statement using φ is more general, and so this can be a corollary

i'll try this

If the collateralPercent is smaller than 100, we dont have anything to bound the fee with. I dont think it is useful to say anything along the lines of "depending on collateralPercent, and assuming one of the fee params is > 0,
0 < totalCollateralBalance < minfee <= txfee OR
0 < minfee < totalCollateralBalance .... etc. and consider every other case, then for fee params = 0 case too

I think this property is clear and useful for testing as is

WhatisRT · 2021-07-06T14:21:26Z

alonzo/formal-spec/properties.tex

+
+  The following holds :
+
+  \[\forall ~tp,~tp~\in~\fun{collectTwoPhaseScriptInputs} ~\field_{pp}(s)~\var{tx}~ \Utxo(s)\]


I think using actual equality would be cleaner here

that's true

oh, hm - never mind. The return type of collectTwoPhaseScriptInputs is a list, and that the order of this list does not matter for evalScripts is discussed in the corollary that follows

Right, I forgot that it's a list. Don't we have a toSet function that we already use? Then we could say that they are equal as sets. The issue I'm having with introducing a name here is that it sort of suggests that that element could be used elsewhere.

oh yeah, toSet would make sense

WhatisRT · 2021-07-06T14:25:27Z

alonzo/formal-spec/properties.tex

+
+    The $\fun{collectTwoPhaseScriptInputs}$
+    function (see \ref{fig:functions:script2})
+    makes a list where each entry contains a Plutus script


'constructs' is probably nicer than 'makes'

alonzo/formal-spec/properties.tex

WhatisRT · 2021-07-06T14:35:02Z

alonzo/formal-spec/properties.tex

+\end{corollary}
+
+\begin{proof}
+  Let us consider the use of arguments of $\fun{evalScripts}$ (see Figure \ref{fig:functions:script2}).


Shouldn't the proof just be a reference to the previous lemma?

evalScripts now gets an additional tx argument and runs all the native scripts, so I had to discuss that in this proof. It worked out that way because of how the code ended up and there wasnt a clearly better way to do it.

Oh, I missed that. But I don't think the way it's written right now works: the list passed to evalScripts only contains 2 phase scripts (that's even in the type). I'm very confused by this change...

It is weird for sure - I changed the type to be Script instead of just phase-1 scripts to match the code. In the code, the filtering is done at the collectTwoPhaseScriptInputs stage, so the (s, _, _, _) option with s being a phase-1 script never actually gets included in sLst (even though the evaluation for them is defined correctly in evalScripts).

The reason for all this craziness is that scripts are of just one type, Script (with two constructors), so the type-level distinction is not possible. So, each function has to behave correctly on both kinds of scripts even if we know some are filtered out.

alonzo/formal-spec/properties.tex

alonzo/formal-spec/utxo.tex

WhatisRT · 2021-07-08T12:10:05Z

alonzo/formal-spec/properties.tex

    and the argumets passed to the interpreter for its evaluation.

    To show that $\fun{collectTwoPhaseScriptInputs}$ returns a list containing
    the same elements for both $tx$ and $tx'$,
    we observe that
    the set of elements from which this list is produced via $\fun{toList}$
    is generated using the following functions, as well as set comprehension
-    and list operations. We observe that these functions are deterministic
+    and list operations (which are known to be deterministic).


I don't think we should be talking about functions being deterministic. We're doing a mathematical model, so there's no such thing as a non-deterministic function.

WhatisRT · 2021-07-08T12:10:30Z

alonzo/formal-spec/properties.tex

-      a given transaction), and the script purpose from the script hash and purpose pair.
-
+      \item $\fun{valContext}$ and $\fun{txInfo}$ :
+      The $\fun{valContext}$ function is assumed deterministic.


Same as above

WhatisRT · 2021-07-19T12:43:56Z

alonzo/formal-spec/utxo.tex

@@ -348,7 +348,7 @@ \subsection{Plutus Script Validation}
  inputs. Specifically, each tuple in the list contains :

  \begin{itemize}
-  \item the script;
+  \item the script, only if it is a non-native one;


2-phase instead?

i used phase-2 and phase-1, it seemed nicer to me (eg. this script is run in phase 2, so it's a phase-2 script). But I can change.

WhatisRT

Sorry for holding this up for this long, but I think we can merge it now!

polinavino requested a review from WhatisRT as a code owner June 24, 2021 04:33

polinavino requested a review from JaredCorduan June 24, 2021 04:33

WhatisRT reviewed Jun 24, 2021

View reviewed changes

polinavino changed the title ~~Formal spec update~~ [WIP] - Formal spec update Jun 24, 2021

polinavino force-pushed the polina/formal-fix branch from 6f0c252 to bed4a46 Compare July 5, 2021 23:42

polinavino changed the title ~~[WIP] - Formal spec update~~ Formal spec update Jul 5, 2021

polinavino requested a review from WhatisRT July 6, 2021 13:24

JaredCorduan reviewed Jul 6, 2021

View reviewed changes

WhatisRT reviewed Jul 6, 2021

View reviewed changes

polinavino requested a review from WhatisRT July 7, 2021 18:40

WhatisRT reviewed Jul 8, 2021

View reviewed changes

polinavino requested a review from WhatisRT July 18, 2021 21:31

WhatisRT reviewed Jul 19, 2021

View reviewed changes

WhatisRT approved these changes Jul 20, 2021

View reviewed changes

temp

3d78630

polinavino force-pushed the polina/formal-fix branch from b162d1a to 3d78630 Compare July 20, 2021 15:46

polinavino merged commit 0143575 into master Jul 20, 2021

iohk-bors bot deleted the polina/formal-fix branch July 20, 2021 16:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Formal spec update #2353

Formal spec update #2353

polinavino commented Jun 24, 2021 •

edited

Loading

WhatisRT Jun 24, 2021

polinavino Jun 24, 2021

WhatisRT Jun 24, 2021

polinavino Jun 24, 2021

WhatisRT Jun 24, 2021

JaredCorduan Jul 6, 2021

WhatisRT left a comment

WhatisRT Jul 6, 2021

polinavino Jul 6, 2021

WhatisRT Jul 8, 2021

polinavino Jul 8, 2021

polinavino Jul 18, 2021

WhatisRT Jul 6, 2021

polinavino Jul 6, 2021

polinavino Jul 6, 2021

WhatisRT Jul 8, 2021

polinavino Jul 8, 2021

WhatisRT Jul 6, 2021

WhatisRT Jul 6, 2021

polinavino Jul 6, 2021

WhatisRT Jul 8, 2021

polinavino Jul 16, 2021

WhatisRT Jul 8, 2021

polinavino Jul 8, 2021

WhatisRT Jul 8, 2021

WhatisRT Jul 19, 2021

polinavino Jul 19, 2021

WhatisRT left a comment


		The following holds :

		\[\forall ~tp,~tp~\in~\fun{collectTwoPhaseScriptInputs} ~\field_{pp}(s)~\var{tx}~ \Utxo(s)\]

Formal spec update #2353

Formal spec update #2353

Conversation

polinavino commented Jun 24, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

WhatisRT left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

WhatisRT left a comment

Choose a reason for hiding this comment

polinavino commented Jun 24, 2021 •

edited

Loading