Bump to latest versions

omelkonian · Apr 19, 2023 · 7a6221a · 7a6221a
1 parent a1f55aa
commit 7a6221a
Show file tree

Hide file tree

Showing 21 changed files with 234 additions and 129 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -1,16 +1,19 @@
 name: CI
 on:
-  # schedule: [{cron: '0 0 * * *'}]
+  schedule: [{cron: '0 0 * * *'}]
   push: {branches: master}
 jobs:
   build-deploy:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2.3.1
-      - uses: omelkonian/setup-agda@v0
+      - uses: omelkonian/setup-agda@master
         with:
-          agda-version: 2.6.1
-          stdlib-version: 1.3
-          libraries: omelkonian/formal-prelude#v0.1
+          agda-version: 2.6.3
+          stdlib-version: 1.7.2
+          libraries: omelkonian/formal-prelude#3cb8424
           main: Main
           token: ${{ secrets.GITHUB_TOKEN }}
+          ribbon: true
+          rts: -K256M -H1G -M8G -A128M
+          measure-typechecking: true
diff --git a/Bisimulation/Base.agda b/Bisimulation/Base.agda
@@ -5,6 +5,7 @@ open import Prelude.General
 open import Prelude.Lists
 open import Prelude.DecEq
 open import Prelude.ToN
+open import Prelude.Membership
 
 open import UTxO.Hashing
 open import UTxO.Value
@@ -41,7 +42,7 @@ _~_ {l} _ s = (toData s) ♯ᵈ ∈ ( map (datumHash ∘ out)
 
 view-~ : ∀ {l} {s : S} {vl : ValidLedger l}
   → vl ~ s
-  → ∃[ prevTx ] ∃[ v ] (Σ[ prevOut∈ ∈ (s —→ v ∈ outputs prevTx) ]
+  → ∃ λ prevTx → ∃ λ v → Σ (s —→ v ∈ outputs prevTx) λ prevOut∈ →
       let
         oRef = (prevTx ♯ₜₓ) indexed-at toℕ (L.Any.index prevOut∈)
         out  = record { address = 𝕍; datumHash = toData s ♯ᵈ; value = v }
@@ -51,7 +52,7 @@ view-~ : ∀ {l} {s : S} {vl : ValidLedger l}
          × oRef ∈ map outRef (utxo l)
          × (getSpentOutputRef l oRef ≡ just out)
          × ((v ≥ᶜ threadₛₘ) ≡ true)
-         ))
+         )
 view-~ {l} {s} vl~s
   with ∈-map⁻ (datumHash ∘ out) vl~s
 ... | u@(record {prevTx = prevTx; out = record {value = v}}) , out∈ , refl
@@ -111,12 +112,12 @@ mkTx {l} {s} {s′} {i} {vl} {vl~s} tx≡ (r≡ , s≥ , _)
       frgT : (forge≡ tx≡ >>=ₜ λ v → ⌊ TxInfo.forge txi ≟ toValue v ⌋) ≡ true
       frgT with forge≡ tx≡
       ... | nothing = refl
-      ... | just v  rewrite ≟-refl _≟_ (toValue v) = refl
+      ... | just v  rewrite ≟-refl (toValue v) = refl
 
       rngT : (range≡ tx≡ >>=ₜ λ r → ⌊ TxInfo.range txi ≟ r ⌋) ≡ true
       rngT with range≡ tx≡
       ... | nothing = refl
-      ... | just v  rewrite ≟-refl _≟_ v = refl
+      ... | just v  rewrite ≟-refl v = refl
 
       v≡ : valueSpent txi ≡ v
       v≡ rewrite sum-single {v = InputInfo.value (mkInputInfo l i₀)}

diff --git a/Bisimulation/Completeness.agda b/Bisimulation/Completeness.agda
@@ -4,8 +4,10 @@ open import Data.List.Membership.Propositional.Properties
 open import Prelude.Init
 open import Prelude.General
 open import Prelude.Lists
+open import Prelude.Maybes
 open import Prelude.DecEq
 open import Prelude.Sets
+open import Prelude.Membership
 open import Prelude.ToN
 open import Prelude.Bifunctor
 open import Prelude.Applicative

diff --git a/Bisimulation/Soundness.agda b/Bisimulation/Soundness.agda
@@ -5,8 +5,10 @@ open import Prelude.General
 open import Prelude.Lists
 open import Prelude.DecEq
 open import Prelude.Sets
+open import Prelude.Membership
 open import Prelude.ToN
 open import Prelude.Bifunctor
+open import Prelude.Applicative
 open import Prelude.Monad
 
 open import UTxO.Hashing
@@ -108,10 +110,10 @@ soundness {s} {i} {s′} {tx≡} {l} {vl} {- final≡ -} s→s′ vl~s sat@(rang
         thisVal≡ = cong InputInfo.validatorHash (ptx-‼ {l} {tx} {txIn} {here refl})
 
         inputs≡ : inputsAt 𝕍 txi ≡ [ ptxIn ]
-        inputs≡ = filter-singleton {P? = (𝕍 ≟_) ∘ InputInfo.validatorHash} (≟-refl _≟_ 𝕍)
+        inputs≡ = filter-singleton {P? = (𝕍 ≟_) ∘ InputInfo.validatorHash} (≟-refl 𝕍)
 
         outputs≡ : outputsAt 𝕍 txi ≡ [ txOut ]
-        outputs≡ = filter-singleton {P? = (𝕍 ≟_) ∘ address} (≟-refl _≟_ 𝕍)
+        outputs≡ = filter-singleton {P? = (𝕍 ≟_) ∘ address} (≟-refl 𝕍)
 
         getCont≡ : getContinuingOutputs ptx ≡ [ txOut ]
         getCont≡ =
@@ -127,11 +129,11 @@ soundness {s} {i} {s′} {tx≡} {l} {vl} {- final≡ -} s→s′ vl~s sat@(rang
           ∎
 
         outputsOK≡ : outputsOK ptx di ds s′ ≡ true
-        outputsOK≡ rewrite {- final≡ | -} getCont≡ | ≟-refl _≟_ (ds′ ♯ᵈ) = refl
+        outputsOK≡ rewrite {- final≡ | -} getCont≡ | ≟-refl (ds′ ♯ᵈ) = refl
 
         valueAtⁱ≡ : valueAtⁱ 𝕍 txi ≡ v
         valueAtⁱ≡ =
-          -- rewrite ≟-refl _≟_ 𝕍 | getSpent≡ = sum-single {v = v}
+          -- rewrite ≟-refl 𝕍 | getSpent≡ = sum-single {v = v}
           begin
             valueAtⁱ 𝕍 txi
           ≡⟨⟩
@@ -146,7 +148,7 @@ soundness {s} {i} {s′} {tx≡} {l} {vl} {- final≡ -} s→s′ vl~s sat@(rang
 
         valueAtᵒ≡ : valueAtᵒ 𝕍 txi ≡ forge′ +ᶜ v
         valueAtᵒ≡ =
-          -- rewrite ≟-refl _≟_ 𝕍 | getSpent≡ = sum-single {v = forge′ +ᶜ v}
+          -- rewrite ≟-refl 𝕍 | getSpent≡ = sum-single {v = forge′ +ᶜ v}
           begin
             (sumᶜ ∘ map value ∘ outputsAt 𝕍) txi
           ≡⟨ cong (sumᶜ ∘ map value) outputs≡ ⟩

diff --git a/Main.agda b/Main.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --rewriting #-}
 module Main where
 
 -- ** Basic UTxO definitions

diff --git a/README.md b/README.md
@@ -1,4 +1,4 @@
-## A formal model of the ExtendedUTxO model [![Build Status](https://travis-ci.com/omelkonian/formal-utxo.svg?branch=master)](https://travis-ci.com/omelkonian/formal-utxo)
+## A formal model of the Extended UTxO model in Agda [![CI](https://github.com/omelkonian/formal-utxo/workflows/CI/badge.svg)](https://github.com/omelkonian/formal-utxo/actions)
 
 Based on:
 > Joachim Zahnentferner, 2018, May.

diff --git a/StateMachine/Base.agda b/StateMachine/Base.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --auto-inline #-}
 {-
 A State Machine library for smart contracts, based on very similar
 library for Plutus Smart contracts
@@ -16,10 +17,15 @@ open import Data.Nat.Properties using (+-identityˡ; <⇒≢; ≤⇒pred≤)
 open import Prelude.Init
 open import Prelude.General
 open import Prelude.Lists using (enumerate)
+open import Prelude.Maybes
+open import Prelude.Nats.Postulates
 open import Prelude.Default
 open import Prelude.DecEq
 open import Prelude.Sets
+open import Prelude.Membership
+open import Prelude.Applicative
 open import Prelude.Monad
+open import Prelude.Ord
 
 open import UTxO.Hashing
 open import UTxO.Value
@@ -87,45 +93,45 @@ module CEM
   spentsOrigin txi =
     originₛₘ >>=ₜ λ o → ⌊ o ∈? map InputInfo.outputRef (TxInfo.inputInfo txi) ⌋
 
-  𝕍 : HashId
-
-  policyₛₘ : MonetaryPolicy
-  policyₛₘ pti@(record {this = c; txInfo = txi})
-    = ⌊ lookupQuantity (c , 𝕋) (TxInfo.forge txi) ≟ 1 ⌋
-    ∧ spentsOrigin txi
-    ∧ (case outputsOf (c , 𝕋) pti of λ
-        { (record {value = v; address = v♯; datumHash = d♯} ∷ [])
-          → ⌊ v♯ ≟ 𝕍 ⌋
-          ∧ (fromMaybe false $ lookupDatumPtx d♯ pti >>= fromData >>= pure ∘ initₛₘ)
-        ; _ → false })
-    where
-      𝕋 = fromMaybe c ⦇ originₛₘ ♯ₒᵣ ⦈
-
-  ℂ : CurrencySymbol
-  ℂ = policyₛₘ ♯
-
-  𝕋 : TokenName
-  𝕋 = fromMaybe ℂ ⦇ originₛₘ ♯ₒᵣ ⦈
-
-  nftₛₘ : TokenClass
-  nftₛₘ = ℂ , 𝕋
-
-  threadₛₘ : Value
-  threadₛₘ = [ ℂ , [ 𝕋 , 1 ] ]
-
-  validatorₛₘ : Validator
-  validatorₛₘ ptx di ds
-    = fromMaybe false do (s′ , tx≡) ← join ⦇ stepₛₘ (fromData ds) (fromData di) ⦈
-                         pure $ outputsOK s′
-                              ∧ verifyTxInfo (txInfo ptx) tx≡
-                              ∧ propagates threadₛₘ ptx
-    module _ where
-      outputsOK : S → Bool
-      outputsOK st = case getContinuingOutputs ptx of λ
-        { (o ∷ []) → ⌊ datumHash o ≟ toData st ♯ᵈ ⌋
-        ; _        → false }
-
-  𝕍 = validatorₛₘ ♯
+  {-# TERMINATING #-}
+  mutual
+    policyₛₘ : MonetaryPolicy
+    policyₛₘ pti@(record {thisTx = c; txInfo = txi}) =
+      let 𝕋 = fromMaybe c ⦇ originₛₘ ♯ₒᵣ ⦈ in
+        ⌊ lookupQuantity (c , 𝕋) (TxInfo.forge txi) ≟ 1 ⌋
+      ∧ spentsOrigin txi
+      ∧ (case outputsOf (c , 𝕋) pti of λ where
+          (record {value = v; address = v♯; datumHash = d♯} ∷ [])
+            → ⌊ v♯ ≟ 𝕍 ⌋
+            ∧ (fromMaybe false $ lookupDatumPtx d♯ pti >>= fromData >>= pure ∘ initₛₘ)
+          _ → false)
+
+    ℂ : CurrencySymbol
+    ℂ = policyₛₘ ♯
+
+    𝕋 : TokenName
+    𝕋 = fromMaybe ℂ ⦇ originₛₘ ♯ₒᵣ ⦈
+
+    nftₛₘ : TokenClass
+    nftₛₘ = ℂ , 𝕋
+
+    threadₛₘ : Value
+    threadₛₘ = [ ℂ , [ 𝕋 , 1 ] ]
+
+    validatorₛₘ : Validator
+    validatorₛₘ ptx di ds
+      = fromMaybe false do (s′ , tx≡) ← join ⦇ stepₛₘ (fromData ds) (fromData di) ⦈
+                           pure $ outputsOK s′
+                                ∧ verifyTxInfo (txInfo ptx) tx≡
+                                ∧ propagates threadₛₘ ptx
+      module _ where
+        outputsOK : S → Bool
+        outputsOK st = case getContinuingOutputs ptx of λ where
+          (o ∷ []) → ⌊ datumHash o ≟ toData st ♯ᵈ ⌋
+          _        → false
+
+    𝕍 : HashId
+    𝕍 = validatorₛₘ ♯
 
   -- Create a transaction input.
   infix 5 _←—_
@@ -163,14 +169,14 @@ module CEM
        = y , refl , true⇒T g≡
 
   Tpolicy⇒ : ∀ {tx l pti}
-    → this pti ≡ ℂ
+    → thisTx pti ≡ ℂ
     → txInfo pti ≡ mkTxInfo l tx
     → T (policyₛₘ pti)
     → ∃ λ v → ∃ λ s →
           (forge tx ◆ ≡ 1)
         × outputsOf nftₛₘ pti ≡ [ record {value = v; address = 𝕍; datumHash = toData s ♯ᵈ} ]
         × Init s
-  Tpolicy⇒ {tx = tx}{l}{pti@(record {this = .ℂ; txInfo = txi})} refl refl h₀
+  Tpolicy⇒ {tx = tx}{l}{pti@(record {thisTx = .ℂ; txInfo = txi})} refl refl h₀
     with forge tx ◆ ≟ 1 | h₀
   ... | no  _    | ()
   ... | yes frg≡ | h₁
@@ -218,7 +224,7 @@ module CEM
     frg◆≤1 {tx} {l} vtx = ¬>⇒≤ ¬frg◆>1
       where
         ¬frg◆>1 : ¬ (forge tx ◆ > 1)
-        ¬frg◆>1 frg◆>1 = <⇒≢ frg◆>1 (sym frg≡1)
+        ¬frg◆>1 frg◆>1 = Nat.<⇒≢ frg◆>1 (sym frg≡1)
           where
             ◆∈frg : ◆∈ forge tx
             ◆∈frg = ≤⇒pred≤ frg◆>1

diff --git a/StateMachine/Examples/DoubleSatisfactionProblem.agda b/StateMachine/Examples/DoubleSatisfactionProblem.agda
@@ -0,0 +1,38 @@
+module StateMachine.Examples.DoubleSatisfactionProblem where
+
+open import Prelude.Default
+open import UTxO.Value
+open import UTxO.Types
+open import UTxO.TxUtilities
+open import UTxO.Validity
+open import StateMachine.Base
+
+data State : Set where
+  counter : ℤ → State
+
+data Input : Set where
+  inc : Input
+
+instance
+  IsData-CS : IsData State
+  toData   ⦃ IsData-CS ⦄ (counter i) = I i
+  fromData ⦃ IsData-CS ⦄ (I i) = just (counter i)
+  fromData ⦃ IsData-CS ⦄ _     = nothing
+  from∘to  ⦃ IsData-CS ⦄ (counter i) = refl
+  from-inj ⦃ IsData-CS ⦄ (I i) (counter .i) refl = refl
+
+  IsData-CI : IsData Input
+  toData   ⦃ IsData-CI ⦄ inc = LIST []
+  fromData ⦃ IsData-CI ⦄ (LIST []) = just inc
+  fromData ⦃ IsData-CI ⦄ _         = nothing
+  from∘to  ⦃ IsData-CI ⦄ inc = refl
+  from-inj ⦃ IsData-CI ⦄ (LIST []) inc refl = refl
+
+CounterSM : StateMachine State Input
+isInitial CounterSM (counter (+ 0) ) = true
+isInitial CounterSM (counter _     ) = false
+-- isFinal   CounterSM (counter (+ 10)) = false
+-- isFinal   CounterSM _ = false
+step      CounterSM (counter i) inc =
+  just (counter (Data.Integer.suc i) , def Default-TxConstraints)
+origin    CounterSM = nothing
diff --git a/StateMachine/Examples/MultiSig.agda b/StateMachine/Examples/MultiSig.agda
@@ -1,13 +1,12 @@
-open import Data.Maybe.Properties using (just-injective)
-open import Relation.Binary.PropositionalEquality using (cong₂)
-open import Data.List.Relation.Binary.Subset.Propositional.Properties using (⊆-refl)
-
 open import Prelude.Init
 open import Prelude.Lists
 open import Prelude.DecEq
--- open import Prelude.Functor
+open import Prelude.Membership
+open import Prelude.Functor
 open import Prelude.Applicative
 open import Prelude.Default
+open import Prelude.Ord
+
 open import UTxO.Hashing
 open import UTxO.Value
 open import UTxO.Types
@@ -41,7 +40,7 @@ map-just' : {A B : Set}(ma : Maybe A)(a : A)
   → (∀{a a'} → f a ≡ f a' → a ≡ a')
   → (f <$> ma) ≡ just (f a)
   → ma ≡ just a
-map-just' (just _) a f p q = cong just (p (just-injective q))
+map-just' (just _) a f p q = cong just (p (M.just-injective q))
 
 map-nothing' : {A B : Set}(ma : Maybe A)
   → (f : A → B)
@@ -56,7 +55,7 @@ ap-map-just : {A B C : Set}(ma : Maybe A)(a : A)(mb : Maybe B)(b : B)
   → ma ≡ just a × mb ≡ just b
 ap-map-just (just _) a (just _) b f p q =
  let
-   r , r' = p (just-injective q)
+   r , r' = p (M.just-injective q)
  in
   cong just r , cong just r'
 
@@ -70,7 +69,7 @@ ap-ap-map-just : {A B C D : Set}
   → ma ≡ just a × mb ≡ just b × mc ≡ just c
 ap-ap-map-just (just _) a (just _) b (just _) c f p q =
  let
-   r , r' , r'' = p (just-injective q)
+   r , r' , r'' = p (M.just-injective q)
  in
   cong just r , cong just r' , cong just r''
 
@@ -338,7 +337,7 @@ temp : ∀ {sigs₀} →
 -- temp {sigs₀} (Collecting _ sigs) ps s′ s↝s′ = {!!}
 temp {sigs₀} (Collecting _ .sigs₀) refl .(Collecting _ sigs₀)
   base⁇
-  = ⊆-refl
+  = L.SubS.⊆-refl
 temp {sigs₀} (Collecting _ .sigs₀) refl s″
   (step⁇ {s′ = s′} {i = AddSignature sig } s↝s′ (_ , eq) p)
   with s′ | temp _ refl _ s↝s′