Tidy up specification document

isabelle/Core/SemanticsTypes.thy

@@ -317,12 +317,8 @@ interval within which the transaction is occurring.\<close>
 
 record Environment = timeInterval :: TimeInterval
 
-
-
-
-
-\<comment> \<open>TODO: see if we want to add data types of Semantic here (Transaction, etc) or if we want to
-move this types to Semantic\<close>
+(* TODO: see if we want to add data types of Semantic here (Transaction, etc) or if we want to
+move this types to Semantic *)
 (* Processing of time interval *)
 datatype IntervalError = InvalidInterval TimeInterval
                        | IntervalInPastError POSIXTime TimeInterval

isabelle/Doc/Specification/Core.thy

@@ -19,12 +19,25 @@ subsection \<open>Compute Transaction\label{sec:computeTransaction}\<close>
 
 text \<open>The entry point into Marlowe semantics is the function @{const computeTransaction} that
 applies input to a prior state to transition to a posterior state, perhaps reporting warnings or
-throwing an error, all in the context of an environment for the transaction.\<close>
+throwing an error, all in the context of an @{term environment} \secref{sec:state-and-env} for the transaction.\<close>
+
 text \<open>@{const computeTransaction} :: @{typeof computeTransaction}\<close>
-text \<open>FIXME: Print record: @{term [names_short, margin=40]Transaction}
+
+(* FIXME: remove duplicate definition *)
+record TransactionOutputRecord = txOutWarnings :: "TransactionWarning list"
+                                 txOutPayments :: "Payment list"
+                                 txOutState :: State
+                                 txOutContract :: Contract
+
+
+text \<open>
 @{datatype [display,names_short, margin=40]TransactionOutput}
-\<close> text \<open>FIXME: Print record: @{term [names_short, margin=40]TransactionOutputRecord}
-\<close>
+\<close> 
+
+(* FIXME: remove duplicate definition *)
+record Transaction = interval :: TimeInterval
+                     inputs :: "Input list"
+
 
 text \<open>This function adjusts the time interval for the transaction using @{const fixInterval} and
 then applies all of the transaction inputs to the contract using @{const applyAllInputs}. It
@@ -34,10 +47,15 @@ text \<open>@{code_stmts computeTransaction constant: computeTransaction (Haskel
 subsection \<open>Fix Interval\<close>
 
 text \<open>The @{const fixInterval} functions combines the minimum-time constraint of @{term State}
-with the time interval of @{term Environment} to yield a ``trimmed'' validity interval and a minimum
+with the time interval of @{term Environment} \secref{sec:state-and-env} to yield a ``trimmed'' validity interval and a minimum
 time for the new state that will result from applying the transaction. It throws an error if the
 interval is nonsensical or in the past.\<close>
-text \<open>FIXME: print type synonym: @{term [names_short, margin=40]IntervalResult}\<close>
+
+text \<open>
+@{datatype [display,names_short, margin=40]IntervalResult}
+\<close>
+
+(* FIXME: synonim are expanding *)
 text \<open>@{code_stmts fixInterval constant: fixInterval (Haskell)}\<close>
 
 subsection \<open>Apply All Inputs\label{sec:applyAllInputs}\<close>
@@ -158,13 +176,13 @@ text \<open>Division is a special case because we only evaluate to natural numbe
 
 text \<open>@{thm [display,names_short, margin=40] evalValue_DivValue}\<close>
 
-text \<open>TODO: lemmas around division? maybe extend the following to proof evalValue and not just div\<close>
+(* \<open>TODO: lemmas around division? maybe extend the following to proof evalValue and not just div\<close>*)
 text \<open>@{thm divMultiply}\<close>
 text \<open>@{thm divAbsMultiply}\<close>
-text \<open>COMMENT(BWB): I suggest that the lemmas be (i) exact multiples divide with no remainder, (ii)
+(*text \<open>COMMENT(BWB): I suggest that the lemmas be (i) exact multiples divide with no remainder, (ii)
       the remainder equals the excess above an exact multiple, and (iii) negation commutues with
       division.\<close>
-
+*)
 subsubsection \<open>Choice Value\<close>
 
 text \<open>For the \<^emph>\<open>ChoiceValue\<close> case, @{const evalValue} will look in its state if a @{typ Party} has

isabelle/Doc/Specification/Guarantees.thy

@@ -58,31 +58,30 @@ text \<open>
 
 For every Marlowe Contract there is a time after which an empty transaction can be issued that will
 close the contract and refund all the money in its accounts.
-
-FIXME: This theorem doesn't actually prove the narrative. Are we missing a theorem?
-
 \<close>
 
-text \<open>@{thm timeOutTransaction_closes_contract2}\<close>
+text \<open>@{thm [display,names_short, margin=40] timedOutTransaction_closes_contract3}\<close>
 
 section \<open>Positive Accounts\<close>
 
 text \<open>
 
 There are some values for State that are allowed by its type but make no sense, especially in the
-case of Isabelle semantics where we use lists instead of maps:
+case of Isabelle semantics where we use lists of key values to represent maps:
 \begin{enumerate}
-\item The lists represent maps, so they should have no repeated keys.
-\item We want two maps that are equal to be represented the same, so we force keys to be in ascending order.
-\item We only want to record those accounts that contain a positive amount.
+\item The lists represent maps, so they should have no repeated keys (@{term valid_map}).
+\item Two equal maps should be represented equally, so we force keys to be in ascending order  (@{term valid_map}).
+\item Only the accounts that contain a positive amount are relevant (@{term allAccountsPositiveState}).
 \end{enumerate}
-We call a value for State valid if the first two properties are true. And we say it has positive
-accounts if the third property is true.
-
 \<close>
-text \<open>FIXME: Address the review comment "Is this a note for us or the explanation to the user of what @{term playTraceAux_preserves_validAndPositive_state} proves?".\<close>
 
-text \<open>@{thm playTraceAux_preserves_validAndPositive_state}\<close>
+
+
+text \<open>@{code_stmts validAndPositive_state constant: validAndPositive_state valid_state valid_map allAccountsPositive allAccountsPositiveState (Haskell)}\<close>
+
+text \<open>If the accounts are valid and possitive, then applying an input preserves that property.\<close>
+
+text \<open>@{thm [display,names_short, margin=40] playTraceAux_preserves_validAndPositive_state}\<close>
 
 section \<open>Quiescent Result\<close>
 
@@ -112,7 +111,7 @@ section \<open>Reducing a Contract until Quiescence Is Idempotent\<close>
 text \<open>Once a contract is quiescent, further reduction will not change the contract or state,
 and it will not produce any payments or warnings.\<close>
 
-text \<open>@{thm reduceContractUntilQuiescentIdempotent}\<close>
+text \<open>@{thm [display,names_short, margin=40] reduceContractUntilQuiescentIdempotent}\<close>
 
 section \<open>Split Transactions Into Single Input Does Not Affect the Result\<close>
 

isabelle/Doc/Specification/document/root.tex

@@ -59,6 +59,7 @@
 Hernán Rajchert \and \\
 Brian Bush
 }
+\date{2 Dec 2022}
 \maketitle
 
 \tableofcontents