PLT-3505 small fixes to the isabelle specification

CHANGELOG.md

@@ -0,0 +1,24 @@
+# Changelog
+
+# XXX 2023 - Marlowe specification version 3, (RC2 or final?)
+
+## Specification
+- [PLT-4195](https://github.com/input-output-hk/marlowe/pull/161) - Change MoneyPreservation for AssetPreservation
+- [PLT-3505](https://github.com/input-output-hk/marlowe/pull/168) - Several small fixes to the specification from the audit report
+- [SCP-4869](https://github.com/input-output-hk/marlowe/pull/164) - Add lemma for DivValue rounding to zero
+- [SCP-4908](https://github.com/input-output-hk/marlowe/pull/163) - Add Escrow to the contract examples
+
+## Test Spec
+- [SCP-4860](https://github.com/input-output-hk/marlowe/pull/158) - Make tests reproducible
+- [SCP-4698](https://github.com/input-output-hk/marlowe/pull/154) - Implement roundtrip test for all serialized types
+- [SCP-4901](https://github.com/input-output-hk/marlowe/pull/160) - Add tests to EvalValue
+- [PLT-4250](https://github.com/input-output-hk/marlowe/pull/170) - Add tests to EvalObservation
+- [PLT-3313](https://github.com/input-output-hk/marlowe/pull/167) - Add Semiarbitrary instances and property based tests for some of Isabelle theorems
+
+## General
+- [SCP-4748](https://github.com/input-output-hk/marlowe/pull/155) - Fixed cabal packages.
+- [SCP-4848](https://github.com/input-output-hk/marlowe/pull/156) - Fix problem with `edit-marlowe-proofs` command.
+- [PR 175](https://github.com/input-output-hk/marlowe/pull/175) - Add version bounds to all libraries
+
+# Dec 2022 - Marlowe specification version 3, RC1
+Version `v3-rc1` was tagged on commit `c8c67ad6892ec68842461d2e66b02ca87f93f70c` on 19 Dec 2022 and submitted to the auditors. This marks the begining of the changelog.

isabelle/Core/OptBoundTimeInterval.thy

@@ -34,12 +34,12 @@ fun bToSet :: "OptBoundTimeInterval => POSIXTime set" where
  | "bToSet (Bounded l, Bounded r) = {l..r}"
 
 
-section "Interval intesection"
+section "Interval intersection"
 
 text
 \<open>
 The interval intersection is achieved by calculating the maximum lower bound and the minimum
-higher bound, favouring Bounded to Unbounded endpoits.
+higher bound, favouring Bounded to Unbounded endpoints.
 \<close>
 fun maxLow :: "BEndpoint \<Rightarrow> BEndpoint \<Rightarrow> BEndpoint" where
   "maxLow Unbounded y = y"

isabelle/Core/PositiveAccounts.thy

@@ -9,16 +9,14 @@ fun positiveMoneyInAccountOrNoAccount :: "AccountId \<Rightarrow> Token \<Righta
    | Some x \<Rightarrow> x > 0)"
 
 lemma addMoneyToAccountPositve_match :
- "\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok accs \<Longrightarrow>
-    money > 0 \<Longrightarrow>
+ "money > 0 \<Longrightarrow>
     newBalance > 0 \<Longrightarrow>
     positiveMoneyInAccountOrNoAccount y tok2 (MList.insert (y, tok2) newBalance accs)"
   apply simp
   by (simp add: MList.insert_lookup_Some)
 
 lemma addMoneyToAccountPositive_noMatch :
  "\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok accs \<Longrightarrow>
-    money > 0 \<Longrightarrow>
     (accId, tok) \<noteq> (y, tok2) \<Longrightarrow>
     newBalance > 0 \<Longrightarrow>
     positiveMoneyInAccountOrNoAccount y tok2 (MList.insert (accId, tok2) newBalance accs)"
@@ -63,14 +61,6 @@ lemma positiveMoneyInAccountOrNoAccount_sublist_gtZero_different :
   apply (simp only:positiveMoneyInAccountOrNoAccount.simps findWithDefault.simps)
   by (metis MList.delete.simps(2) MList.different_delete_lookup)
 
-lemma positiveMoneyInAccountOrNoAccount_sublist_gtZero :
-    "valid_map ((accIdTok, money) # rest) \<Longrightarrow>
-     money > 0 \<Longrightarrow>
-    (\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok ((accIdTok, money) # rest)) \<Longrightarrow> positiveMoneyInAccountOrNoAccount y tok2 rest"
-  apply (cases "accIdTok = (y, tok2)")
-  using positiveMoneyInAccountOrNoAccount_valid_zero apply auto[1]
-  using positiveMoneyInAccountOrNoAccount_sublist_gtZero_different by blast
-
 lemma positiveMoneyInAccountOrNoAccount_gtZero_preservation :
   "valid_map ((accIdTok, money) # rest) \<Longrightarrow>
    (\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok ((accIdTok, money) # rest)) \<Longrightarrow> positiveMoneyInAccountOrNoAccount y tok2 rest"
@@ -366,20 +356,11 @@ lemma positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive :
   apply simp
   using positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive_aux2 by auto
 
-theorem accountsArePositive :
-  "valid_state state \<Longrightarrow> (\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok (accounts state)) \<Longrightarrow>
-  computeTransaction txIn state cont = TransactionOutput txOut \<Longrightarrow>
-  positiveMoneyInAccountOrNoAccount y tok2 (accounts (txOutState txOut))"
-  using computeTransaction_gtZero by blast
-
 theorem accountsArePositive2 :
     "valid_state state \<Longrightarrow> allAccountsPositiveState state
     \<Longrightarrow> computeTransaction txIn state cont = TransactionOutput txOut
-    \<Longrightarrow> allAccountsPositiveState (txOutState txOut)"
-  by (meson accountsArePositive allAccountsPositiveImpliesPositiveMoneyInAccountOrNoAccount allAccountsPositiveState.elims(2) allAccountsPositiveState.elims(3) computeTransaction_preserves_valid_state positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive valid_state.elims(2))
-
-lemma valid_state_valid_accounts : "valid_state state \<Longrightarrow> valid_map (accounts state)"
-  by simp
+    \<Longrightarrow> allAccountsPositiveState (txOutState txOut)"  
+  by (meson computeTransaction_gtZero allAccountsPositiveImpliesPositiveMoneyInAccountOrNoAccount allAccountsPositiveState.elims(2) allAccountsPositiveState.elims(3) computeTransaction_preserves_valid_state positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive valid_state.elims(2))
 
 theorem accountsArePositive2_trace :
     "valid_state (txOutState txIn) \<Longrightarrow> allAccountsPositiveState (txOutState txIn)

isabelle/Core/QuiescentResult.thy

@@ -2,9 +2,6 @@ theory QuiescentResult
 imports Semantics PositiveAccounts
 begin
 
-lemma reduceOne_onlyIfNonEmptyState : "refundOne acc = Some c \<Longrightarrow> acc \<noteq> []"
-  by auto
-
 lemma reduceContractStepPayIsQuiescent :
       "(let moneyToPay = evalValue env sta x23
         in if moneyToPay \<le> 0 then Reduced (ReduceNonPositivePay x21 x22 tok moneyToPay) ReduceNoPayment sta x24
@@ -13,8 +10,7 @@ lemma reduceContractStepPayIsQuiescent :
                     warning = if paidMoney < moneyToPay then ReducePartialPay x21 x22 tok paidMoney moneyToPay else ReduceNoWarning;
                     (payment, finalAccs) = giveMoney x21 x22 tok paidMoney newAccs
                 in Reduced warning payment (sta\<lparr>accounts := finalAccs\<rparr>) x24) =
-       NotReduced \<Longrightarrow>
-       cont = Pay x21 x22 tok x23 x24 \<Longrightarrow> False"
+       NotReduced \<Longrightarrow> False"
   apply (cases "evalValue env sta x23 \<le> 0")
   apply simp
   apply (cases "min (moneyInAccount x21 tok (accounts sta)) (evalValue env sta x23) < (evalValue env sta x23)")
@@ -150,7 +146,8 @@ lemma reductionLoop_reduce_monotonic : "reductionLoop True env sta cont wa ef =
     by simp
   done
 
-lemma reduceContractUntilQuiescent_ifDifferentReduced : "reduceContractUntilQuiescent si sta cont = ContractQuiescent reduce wa ef sta newCont \<Longrightarrow> cont \<noteq> newCont \<Longrightarrow> reduce"
+text "If we reduce the contract and the continuation has changed, then the reduced flag should be true"
+theorem reduceContractUntilQuiescent_ifDifferentReduced : "reduceContractUntilQuiescent si sta cont = ContractQuiescent reduce wa ef sta newCont \<Longrightarrow> cont \<noteq> newCont \<Longrightarrow> reduce"
   apply (simp only:reduceContractUntilQuiescent.simps)
   apply (simp only:reductionLoop.simps)
   apply (cases "reduceContractStep si sta cont")

isabelle/Core/Semantics.thy

@@ -510,7 +510,7 @@ fun applyCases :: "Environment \<Rightarrow> State \<Rightarrow> Input \<Rightar
         \<and> amount = evalValue env state val)
    then let warning = if amount > 0
                       then ApplyNoWarning
-                      else ApplyNonPositiveDeposit party1 accId2 tok2 amount in
+                      else ApplyNonPositiveDeposit party2 accId2 tok2 amount in
         let newState = state \<lparr> accounts := addMoneyToAccount accId1 tok1 amount (accounts state) \<rparr> in
         Applied warning newState cont
    else applyCases env state (IDeposit accId1 party1 tok1 amount) rest)" |
@@ -580,8 +580,8 @@ fun applyAllLoop :: "bool \<Rightarrow> Environment \<Rightarrow> State \<Righta
                                  (payments @ pays) curState cont
         | Cons input rest \<Rightarrow>
            (case applyInput env curState input cont of
-              Applied applyWarn newState cont \<Rightarrow>
-                  applyAllLoop True env newState cont rest
+              Applied applyWarn newState appliedCont \<Rightarrow>
+                  applyAllLoop True env newState appliedCont rest
                                (warnings @ (convertReduceWarnings reduceWarns)
                                          @ (convertApplyWarning applyWarn))
                                (payments @ pays)
@@ -721,34 +721,80 @@ and maxTimeCase :: "Case \<Rightarrow> int" where
 
 subsection "calculateNonAmbiguousInterval"
 
+text "Helper functions for \<^emph>\<open>calculateNonAmbiguousInterval\<close>"
 fun gtIfNone :: "int option \<Rightarrow> int \<Rightarrow> bool" where
 "gtIfNone None _ = True" |
 "gtIfNone (Some x) y = (x > y)"
 
 fun geIfNone :: "int option \<Rightarrow> int \<Rightarrow> bool" where
 "geIfNone None _ = True" |
-"geIfNone (Some x) y = (x \<ge> y)"
+"geIfNone (Some x) y = (x \<ge> y) "
 
 fun subIfSome :: "int option \<Rightarrow> int \<Rightarrow> int option" where
 "subIfSome None _ = None" |
 "subIfSome (Some x) y = Some (x - y)"
 
 
+text \<open>
+A TimeInterval (startTime, endTime) can be ambiguous wrt a When's timeout if startTime < timeout \<le> endTime
+
+\<close>
+
+text \<open>The \<^emph>\<open>calculateNonAmbiguousInterval\<close> function can help a user to calculate a TimeInterval that
+won't be ambiguous for the next \<^emph>\<open>n\<close> inputs of a contract.\<close>
+
+text \<open>The only Contract constructor that can yield a \<^term>\<open>TEAmbiguousTimeIntervalError\<close> is the \<^term>\<open>When\<close> case. 
+Computing a transaction of a contract that starts in a non quiescent state (\<^term>\<open>Let\<close>, \<^term>\<open>Pay\<close>, \<^term>\<open>If\<close>, \<^term>\<open>Assert\<close>) 
+can end in a \<^term>\<open>TEAmbiguousTimeIntervalError\<close> iff there is a \<^term>\<open>When\<close> case that makes it ambiguous.
+\<close>
+
+text \<open>A TimeInterval expressed as the tuple \<^term>\<open>(startTime \<times> endTime)\<close> can be ambiguous wrt a \<^term>\<open>When\<close>'s timeout
+iff \<^emph>\<open>startTime < timeout \<le> endTime\<close>
+\<close>
+
+text
+\<open> It parameters of \<^emph>\<open>calculateNonAmbiguousInterval\<close> are:
+\<^item> An optional number of Inputs to check. The number of inputs corresponds to the number of "When". 
+If None is passed, it means that we should check for transactions of any number of inputs.
+\<^item> A lower bound (normally the current time).
+\<^item> The Contract to check.
+
+The function returns an Optionally Bound Time Interval, as defined in the \<^emph>\<open>OptBoundTimeInterval.thy\<close> theory.
+In the \<^emph>\<open>TimeRange.thy\<close> theory we prove that computing a transaction with these bounds doesn't end with an ambiguous error. 
+\<close>
+\<comment> \<open>TODO: The intersectInterval can produce an invalid time interval, which would mean that not suitable TimeInterval was found\<close>
 fun calculateNonAmbiguousInterval :: "int option \<Rightarrow> POSIXTime \<Rightarrow> Contract \<Rightarrow> OptBoundTimeInterval"
-where
+  where
+\<comment> \<open>A Close contract can't be ambiguous, so an Unbounded interval is returned \<close>
 "calculateNonAmbiguousInterval _ _ Close = (Unbounded, Unbounded)" |
+\<comment> \<open>A Pay contract isn't ambiguous by itself, so we calculate for the continuation\<close>
 "calculateNonAmbiguousInterval n t (Pay _ _ _ _ c) = calculateNonAmbiguousInterval n t c" |
-"calculateNonAmbiguousInterval n t (If _ ct cf) = intersectInterval (calculateNonAmbiguousInterval n t ct)
+\<comment> \<open>If we branch, we intersect the result of both possibilites. \<close>
+\<comment> \<open>TODO: Note that not knowing which branch can be selected beforehand means that we return a smaller TimeInterval than
+possible. Maybe we could improve this by using the actual Input instead of the number of inputs\<close>
+"calculateNonAmbiguousInterval n t (If _ ct cf) = intersectInterval 
+                                                           (calculateNonAmbiguousInterval n t ct)
                                                            (calculateNonAmbiguousInterval n t cf)" |
-"calculateNonAmbiguousInterval n t (When Nil timeout tcont) =
+\<comment> \<open>We treat the When contract in two parts. The base case (when no actions are available) and a recursive
+case, when we have a particular action \<close>
+"calculateNonAmbiguousInterval n t (When [] timeout tcont) =
   (if t < timeout
+  \<comment> \<open>If the When's timeout is in the future, we can generate a non-ambiguous time interval
+      by restricting the endTime to be strictly lower than the timeout\<close>
    then (Unbounded, Bounded (timeout - 1))
+  \<comment> \<open>If the timeout is in the past, we need to restrict the startTime to be larger or equal than
+     the timeout\<close>
    else intersectInterval (Bounded timeout, Unbounded) (calculateNonAmbiguousInterval n t tcont))" |
-"calculateNonAmbiguousInterval n t (When (Cons (Case _ cont ) tail) timeout tcont) =
+
+"calculateNonAmbiguousInterval n t (When (Case _ cont  # restCases) timeout tcont) =  
   (if gtIfNone n 0
+\<comment> \<open>If n is none (check all) or n > 0 we recursively calculate the intersection for all the continuations\<close>
    then intersectInterval (calculateNonAmbiguousInterval (subIfSome n 1) t cont)
-                         (calculateNonAmbiguousInterval n t (When tail timeout tcont))
-   else calculateNonAmbiguousInterval n t (When tail timeout tcont))" |
+                         (calculateNonAmbiguousInterval n t (When restCases timeout tcont))
+\<comment> \<open>If n \<le> 0 we don't calculate for the current case and we iterate until we reach the base case\<close>  
+\<comment> \<open>TODO: we should be able to change restCases for [] to check the base case directly\<close>
+   else calculateNonAmbiguousInterval n t (When restCases timeout tcont))" |
+\<comment> \<open>A Let or Assert contracts aren't ambiguous by themselves, so we calculate for the continuation\<close>
 "calculateNonAmbiguousInterval n t (Let _ _ c) = calculateNonAmbiguousInterval n t c" |
 "calculateNonAmbiguousInterval n t (Assert _ c) = calculateNonAmbiguousInterval n t c"