Merge branch 'master' into 545-certs-base-case-first

IntersectMBO · Nov 20, 2024 · cbdf558 · cbdf558
2 parents 20ffac4 + bccb83b
commit cbdf558
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 37 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -17,11 +17,18 @@ jobs:
   MAlonzo:
     runs-on: ubuntu-latest
     steps:
+      - name: Check if ${{ env.MAlonzo_branch }} exists
+        uses: actions/checkout@v4
+        with:
+          ref: ${{ env.MAlonzo_branch }}
+        id: MAlonzo-exists
+        continue-on-error: true
+        if: github.ref != 'refs/heads/master'
       - uses: actions/checkout@v4
         with:
           ref: MAlonzo-code
       - name: Create branch ${{ env.MAlonzo_branch }} for generated code
-        if: github.event_name == 'pull_request' && github.event.action == 'opened'
+        if: github.ref != 'refs/heads/master' && steps.MAlonzo-exists.outcome == 'failure'
         run: |
           git checkout -b ${{ env.MAlonzo_branch }} origin/MAlonzo-code
           git push origin ${{ env.MAlonzo_branch }}

diff --git a/src/Ledger/Conway/Conformance/Utxo.agda b/src/Ledger/Conway/Conformance/Utxo.agda
@@ -29,23 +29,20 @@ open PParams
 instance
   _ = +-0-monoid
 
-certDepositUtxo : DCert → PParams → DepositPurpose ⇀ Coin
-certDepositUtxo (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵
-certDepositUtxo (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
-certDepositUtxo (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
-certDepositUtxo _                  _   = ∅
-
-updateCertDeposits  : PParams → List DCert → (DepositPurpose ⇀ Coin)
-                    → DepositPurpose ⇀ Coin
-updateCertDeposits _   []              deposits = deposits
-updateCertDeposits pp  (cert ∷ certs)  deposits
-  = (updateCertDeposits pp certs deposits ∪⁺ certDeposit cert pp) ∣ certRefund cert ᶜ
-
-updateCertDepositsUtxo  : PParams → List DCert → (DepositPurpose ⇀ Coin)
-                        → DepositPurpose ⇀ Coin
-updateCertDepositsUtxo _   []              deposits = deposits
-updateCertDepositsUtxo pp  (cert ∷ certs)  deposits
-  = updateCertDepositsUtxo pp certs deposits ∪⁺ certDepositUtxo cert pp
+updateCertDeposits  : PParams → List DCert → Deposits → Deposits
+updateCertDeposits pp [] deposits = deposits
+updateCertDeposits pp (delegate c vd khs v ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (delegate c vd khs v) pp)
+updateCertDeposits pp (regpool kh p ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∪⁺ ❴ PoolDeposit kh , pp .poolDeposit ❵)
+updateCertDeposits pp (regdrep c v a ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regdrep c v a) pp)
+updateCertDeposits pp (dereg c v ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∣ certRefund (dereg c v)ᶜ)
+updateCertDeposits pp (deregdrep c v ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∣ certRefund (deregdrep c v)ᶜ)
+updateCertDeposits pp (_ ∷ certs) deposits
+  = updateCertDeposits pp certs deposits
 
 -- -- Unchanged/defined in Utxo module:
 updateProposalDeposits : List GovProposal → TxId → Coin → Deposits → Deposits
@@ -55,7 +52,7 @@ updateProposalDeposits (_ ∷ ps)  txid  gaDep  deposits  =
   ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵
 
 updateDeposits : PParams → TxBody → Deposits → Deposits
-updateDeposits pp txb = updateCertDepositsUtxo pp txcerts
+updateDeposits pp txb = updateCertDeposits pp txcerts
                         ∘ updateProposalDeposits txprop txid (pp .govActionDeposit)
   where open TxBody txb
 

diff --git a/src/Ledger/Conway/Conformance/Utxow/Properties.agda b/src/Ledger/Conway/Conformance/Utxow/Properties.agda
@@ -16,6 +16,8 @@ open import Ledger.Conway.Conformance.Utxow txs abs
 open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Utxo.Properties txs abs
 
+open import Tactic.GenError using (genErrors)
+
 instance
   Computational-UTXOW : Computational _⊢_⇀⦇_,UTXOW⦈_ String
   Computational-UTXOW = record {Go}
@@ -24,29 +26,12 @@ instance
     open Computational Computational-UTXO
       renaming (computeProof to computeProof'; completeness to completeness')
 
-    genErr : ¬ H → String
-    genErr  ¬p = case dec-de-morgan ¬p of λ where
-      (inj₁ a) → "¬ ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ"
-      (inj₂ b) → case dec-de-morgan b of λ where
-        (inj₁ a₁) → "∀[ s ∈ scriptsP1 ] validP1Script witsKeyHashes txvldt s"
-        (inj₂ b₁) → case dec-de-morgan b₁ of λ where
-          (inj₁ a₂) → "witsVKeyNeeded utxo txb ⊆ witsKeyHashes"
-          (inj₂ b₂) → case dec-de-morgan b₂ of λ where
-            (inj₁ a₃) → "(neededHashes ＼ refScriptHashes) ≡ᵉ witsScriptHashes"
-            (inj₂ b₃) → case dec-de-morgan b₃ of λ where
-              (inj₁ a₄) → "inputHashes ⊆ txdatsHashes"
-              (inj₂ b₄) → case dec-de-morgan b₄ of λ where
-                (inj₁ a₅) → "txdatsHashes ⊆ (inputHashes ∪ allOutHashes ∪ getDataHashes (range (utxo ∣ refInputs)))"
-                (inj₂ b₅) → case dec-de-morgan b₅ of λ where
-                  (inj₁ a₆) → "languages ⊆ allowedLanguages"
-                  (inj₂ b₆) → "txADhash ≡ map hash txAD"
-
     computeProof : ComputationResult String (∃ (Γ ⊢ s ⇀⦇ tx ,UTXOW⦈_))
     computeProof =
       case H? of λ where
         (yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈)) →
           map (map₂′ (UTXOW-inductive⋯ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈)) (computeProof' Γ s tx)
-        (no ¬p) → failure $ genErr ¬p
+        (no ¬p) → failure $ genErrors ¬p
 
     completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
                         → map proj₁ computeProof ≡ success s'