diff --git a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs index 02c0f897f5..2a618ea8de 100644 --- a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs +++ b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs @@ -11,7 +11,7 @@ import MAlonzo.Code.Ledger.Dijkstra.Foreign.PParams as X (LanguageCostModels(..), DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..)) import MAlonzo.Code.Ledger.Dijkstra.Foreign.Transaction as X ( TxBodyTop(..), TxTop(..), TxBodySub(..), TxSub(..) - , Tag(..), TxWitnesses(..) + , Tag(..), TxWitnesses(..), PoolVoteWitness(..) , TxId, Ix, TxIn, ExUnits, P1Script, P2Script , Script, Datum, DataHash, Value, TxOut, ScriptHash, AuxiliaryData, Withdrawals , Redeemer, RedeemerPtr diff --git a/src/Ledger/Dijkstra/Foreign/ExternalStructures.agda b/src/Ledger/Dijkstra/Foreign/ExternalStructures.agda index 6477728401..3f13ed3d16 100644 --- a/src/Ledger/Dijkstra/Foreign/ExternalStructures.agda +++ b/src/Ledger/Dijkstra/Foreign/ExternalStructures.agda @@ -73,6 +73,7 @@ instance ; cryptoStructure = it ; govParams = HsGovParams ; txidBytes = id + ; poolVoteBytes = suc -- disjoint from txidBytes in the ℕ mock ; scriptStructure = it ; adHashingScheme = isHashableSet-ℕ ; Hashable-ScriptIntegrity = record { hash = λ x → 0 } diff --git a/src/Ledger/Dijkstra/Foreign/Transaction.agda b/src/Ledger/Dijkstra/Foreign/Transaction.agda index c951548b90..225276bb86 100644 --- a/src/Ledger/Dijkstra/Foreign/Transaction.agda +++ b/src/Ledger/Dijkstra/Foreign/Transaction.agda @@ -35,6 +35,9 @@ instance HsTy-HSPlutusScript = autoHsType HSPlutusScript Conv-HSPlutusScript = autoConvert HSPlutusScript + HsTy-PoolVoteWitness = autoHsType PoolVoteWitness ⊣ withName "PoolVoteWitness" + Conv-PoolVoteWitness = autoConvert PoolVoteWitness + HsTy-TxWitnesses = autoHsType TxWitnesses ⊣ withConstructor "MkTxWitnesses" • fieldPrefix "txw" Conv-TxWitnesses = autoConvert TxWitnesses diff --git a/src/Ledger/Dijkstra/Specification/Certs.lagda.md b/src/Ledger/Dijkstra/Specification/Certs.lagda.md index d5f2e5e785..e3dae672b1 100644 --- a/src/Ledger/Dijkstra/Specification/Certs.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs.lagda.md @@ -468,6 +468,13 @@ poolVrfs ps = mapˢ (vrf ∘ params) (range ps) poolBlsKey : Pools → KeyHash → Maybe BlsKeyState poolBlsKey ps kh = lookupᵐ? ps kh >>= blsKey +-- A registered voting key is honoured until maxKeyAgeEpochs epochs after its +-- registration, judged against the epoch the key is used in. +honouredBlsKey : ℕ → Epoch → Maybe BlsKeyState → Maybe BlsVKey +honouredBlsKey maxAge e nothing = nothing +honouredBlsKey maxAge e (just k) = + if e < BlsKeyState.registered k + ℕtoEpoch maxAge then just (BlsKeyState.key k) else nothing + installBlsKey : KeyHash → BlsKeyState → Pools → Pools installBlsKey kh k = mapWithKey λ kh' s → if kh' ≡ kh then record s { blsKey = just k } else s diff --git a/src/Ledger/Dijkstra/Specification/Gov/Actions.lagda.md b/src/Ledger/Dijkstra/Specification/Gov/Actions.lagda.md index fd7e953500..b9cb40ac7e 100644 --- a/src/Ledger/Dijkstra/Specification/Gov/Actions.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Gov/Actions.lagda.md @@ -148,6 +148,10 @@ isGovVoterDRep : GovVoter → Maybe Credential isGovVoterDRep ⟦ DRep , c ⟧ᵍᵛ = just c isGovVoterDRep _ = nothing +isGovVoterSPO : GovVoter → Maybe KeyHash +isGovVoterSPO ⟦ SPO , kh ⟧ᵍᵛ = just kh +isGovVoterSPO _ = nothing + govVoterCredential : GovVoter → Credential govVoterCredential ⟦ CC , c ⟧ᵍᵛ = c govVoterCredential ⟦ DRep , c ⟧ᵍᵛ = c diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index b74e4c1551..d90d6633a1 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -45,6 +45,7 @@ record SubLedgerEnv : Type where enactState : EnactState treasury : Treasury utxo₀ : UTxO + pools₀ : Pools rewards₀ : Rewards allScripts : ℙ Script isTopLevelValid : Bool @@ -212,6 +213,7 @@ private variable isTopLevelValid : Bool allScripts : ℙ Script rewards₀ : Rewards + pools₀ : Pools ``` --> @@ -285,17 +287,17 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx SUBLEDGER-V : ∙ isTopLevelValid ≡ true - ∙ ⟦ slot , pp , treasury , utxo₀ , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁ + ∙ ⟦ slot , pp , treasury , utxo₀ , pools₀ , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁ ∙ ⟦ epoch slot , pp , allColdCreds govState₀ enactState , rewards₀ ⟧ ⊢ certState₀ ⇀⦇ stx ,SUBENTITIES⦈ certState₁ ∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁ ──────────────────────────────── - ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ + ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , pools₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ SUBLEDGER-I : ∙ isTopLevelValid ≡ false - ∙ ⟦ slot , pp , treasury , utxo₀ , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀ + ∙ ⟦ slot , pp , treasury , utxo₀ , pools₀ , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀ ──────────────────────────────── - ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ + ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , pools₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_} @@ -317,7 +319,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg legacyMode = isLegacyMode utxo₀ allScripts tx in ∙ IsValidFlagOf tx ≡ true - ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ + ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , PoolsOf certState₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ ∙ ⟦ epoch slot , pp , allColdCreds govState₁ enactState , legacyMode , rewards₀ ⟧ ⊢ certState₁ ⇀⦇ tx ,ENTITIES⦈ certState₂ ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂ ∙ ⟦ slot , pp , treasury , utxo₀ , PoolsOf certState₀ , allScripts , legacyMode ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂ @@ -338,7 +340,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg legacyMode = isLegacyMode utxo₀ allScripts tx in ∙ IsValidFlagOf tx ≡ false - ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ + ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , PoolsOf certState₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ∙ ⟦ slot , pp , treasury , utxo₀ , PoolsOf certState₀ , allScripts , legacyMode ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁ ──────────────────────────────── ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₁ , govState₀ , certState₀ ⟧ diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md index adaa4add75..09196a1aef 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md @@ -44,7 +44,7 @@ private → IsTopLevelValidFlagOf Γ ≡ false → Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s' → s' ≡ s - SUBUTXOW-noop isI (SUBUTXOW (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , SUBUTXO _)) rewrite isI = refl + SUBUTXOW-noop isI (SUBUTXOW (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , SUBUTXO _)) rewrite isI = refl -- After `rewrite isI`, `IsTopLevelValidFlagOf Γ` reduces to `false`, -- so the SUBUTXO post-state index reduces to `⟦ UTxOOf s , FeesOf s , DonationsOf s ⟧` -- which is s by eta-expansion of the UTxOState record, giving refl. @@ -111,7 +111,7 @@ instance (stx : SubLevelTx) where subUtxoΓ : SubUTxOEnv - subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , allScripts , isTopLevelValid ⟧ + subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , pools₀ , allScripts , isTopLevelValid ⟧ subentitiesΓ : SubEntitiesEnv subentitiesΓ = ⟦ epoch slot , pparams , allColdCreds govSt enactState , rewards₀ ⟧ @@ -223,7 +223,7 @@ instance legacyMode = isLegacyMode utxo₀ allScripts txTop subΓ : SubLedgerEnv - subΓ = ⟦ slot , ppolicy , pparams , enactState , treasury , utxo₀ , RewardsOf (CertStateOf s) , allScripts , IsValidFlagOf txTop ⟧ + subΓ = ⟦ slot , ppolicy , pparams , enactState , treasury , utxo₀ , PoolsOf (CertStateOf s) , RewardsOf (CertStateOf s) , allScripts , IsValidFlagOf txTop ⟧ entitiesΓ : GovState → CertState → EntitiesEnv entitiesΓ govSt certSt = ⟦ epoch slot , pparams , allColdCreds govSt enactState , legacyMode , RewardsOf certSt ⟧ diff --git a/src/Ledger/Dijkstra/Specification/Leios.lagda.md b/src/Ledger/Dijkstra/Specification/Leios.lagda.md index eba2f8d318..94871e2a2c 100644 --- a/src/Ledger/Dijkstra/Specification/Leios.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Leios.lagda.md @@ -57,21 +57,15 @@ instance --> A registered voting key is honoured until `maxKeyAgeEpochs`{.AgdaFunction} -epochs — a bound derived from the KES setup — after its registration. Expiry -is judged against the epoch the committee is -selected for, not the epoch its stake snapshot was taken in: the seat's key +epochs — a bound derived from the KES setup — after its registration +(`honouredBlsKey`{.AgdaFunction}, defined in the `Certs`{.AgdaModule} module). +Expiry is judged against the epoch the committee is selected for, not the +epoch its stake snapshot was taken in: the seat's key comes from a snapshot and may therefore have been registered several epochs ago, while the age bound is applied afresh at each epoch boundary. A committee thus has a stable set of usable keys throughout its epoch, and a key that ages out does so on a boundary rather than mid-epoch. -```agda -honouredBlsKey : ℕ → Epoch → Maybe BlsKeyState → Maybe BlsVKey -honouredBlsKey maxAge e nothing = nothing -honouredBlsKey maxAge e (just k) = - if e < BlsKeyState.registered k + ℕtoEpoch maxAge then just (BlsKeyState.key k) else nothing -``` - The committee for an epoch consists of the `leiosCommitteeSize`{.AgdaField} pools with the most active stake, ties broken by ascending pool id. Instead of sorting, a pool's seat index is *defined* as the number of pools strictly ahead diff --git a/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md b/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md index e5340c47ec..3806b102ab 100644 --- a/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md @@ -144,14 +144,23 @@ txOutToP2Script : ℙ Script → TxOut → Maybe P2Script txOutToP2Script scripts txOut = credentialToP2Script (payCred (proj₁ txOut)) scripts ``` +An SPO vote covered by a pool-vote witness needs no credential here — it is +authorized by the pool's registered voting key instead, checked in the +`Utxow`{.AgdaModule} module. All other voters contribute their credential. + ```agda +voterCredNeeded : (KeyHash ⇀ PoolVoteWitness) → GovVoter → Maybe Credential +voterCredNeeded pvs v = case isGovVoterSPO v of λ where + (just kh) → if kh ∈ dom pvs then nothing else just (KeyHashObj kh) + nothing → just (govVoterCredential v) + credsNeeded : UTxO → Tx ℓ → ℙ (ScriptPurpose × Credential) credsNeeded utxo tx = mapˢ (λ (i , o) → (⟦ Spend , i ⟧ˢᵖ , payCred (proj₁ o))) ((utxo ∣ (SpendInputsOf tx ∪ collateralInputs tx)) ˢ) ∪ mapˢ (λ a → (⟦ Reward , a ⟧ˢᵖ , CredentialOf a)) (dom ∣ WithdrawalsOf tx ∣) ∪ mapPartial (λ c → ((⟦ Cert , c ⟧ˢᵖ ,_) <$> cwitness c)) (fromList (DCertsOf tx)) ∪ mapˢ (λ x → (⟦ Mint , x ⟧ˢᵖ , ScriptObj x)) (policies (MintedValueOf tx)) - ∪ mapˢ (λ v → (⟦ Vote , v ⟧ˢᵖ , govVoterCredential v)) (fromList (map GovVoterOf (ListOfGovVotesOf tx))) + ∪ mapPartial (λ v → ((⟦ Vote , v ⟧ˢᵖ ,_) <$> voterCredNeeded (PoolVoteSigsOf tx) v)) (fromList (map GovVoterOf (ListOfGovVotesOf tx))) ∪ mapPartial (λ p → if PolicyOf p then (λ {sh} → just (⟦ Propose , p ⟧ˢᵖ , ScriptObj sh)) else nothing) (fromList (ListOfGovProposalsOf tx)) diff --git a/src/Ledger/Dijkstra/Specification/Transaction.lagda.md b/src/Ledger/Dijkstra/Specification/Transaction.lagda.md index 1404bd6c6b..2fa179315f 100644 --- a/src/Ledger/Dijkstra/Specification/Transaction.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Transaction.lagda.md @@ -136,6 +136,9 @@ record TransactionStructure : Type₁ where govParams : GovParams tokenAlgebra : TokenAlgebra txidBytes : TxId → Ser + -- Pool-vote message: the tx id under the "cardano-pool-vote" augmentation + -- context, domain-separating governance votes from Leios votes (CIP-0164). + poolVoteBytes : TxId → Ser ``` +## Pool-Vote Witnesses {#sec:pool-vote-witnesses} + +A pool-vote witness authorizes the SPO votes of the pool it is keyed by, so +each entry must name an SPO voter of the transaction and carry a signature by +the pool's honoured (registered, unexpired) voting key over +`poolVoteBytes`{.AgdaField} of the transaction id. Covered votes contribute no +cold-key credential to `credsNeeded`{.AgdaFunction} (see the +`Script.Validation`{.AgdaModule} module); requiring every entry to match a vote +is what keeps these witnesses from authorizing anything else. + +```agda +spoVoters : Tx ℓ → ℙ KeyHash +spoVoters tx = mapPartial isGovVoterSPO (fromList (map GovVoterOf (ListOfGovVotesOf tx))) + +PoolVoteAuthorized : Pools → ℕ → Epoch → Ser → KeyHash → PoolVoteWitness → Type +PoolVoteAuthorized pools maxAge e msg kh (blsW σ) = + MAny.Any (λ vk → isSignedByAggregate (vk ∷ []) msg σ) + (honouredBlsKey maxAge e (poolBlsKey pools kh)) +``` + + + ## The SUBUTXOW Transition System {#sec:the-subutxow-transition-system} 1. All needed phase-2 scripts use Plutus language V4. @@ -311,6 +344,9 @@ data _⊢_⇀⦇_,SUBUTXOW⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTx ∙ ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided (GuardsOf txSub) txVldt s ∙ ∀[ tlg ∈ TopLevelGuardsOf txSub ] TopLevelGuardWellFormed scriptsProvided tlg -- (2) ∙ vKeyHashesNeeded ⊆ vKeyHashesProvided + ∙ ∀[ (kh , w) ∈ poolVoteSigs ] + ( kh ∈ spoVoters txSub + × PoolVoteAuthorized (PoolsOf Γ) maxKeyAgeEpochs (epoch (SlotOf Γ)) (poolVoteBytes txId) kh w) ∙ scriptHashesNeeded ⊆ mapˢ hash scriptsProvided ∙ dataHashesNeededSpendInputs ⊆ dataHashesProvided ∙ dataHashesProvided ⊆ dataHashesNeededSpendInputs ∪ dataHashesOutputs ∪ dataHashesReferenceInputs @@ -423,6 +459,9 @@ attempting both. ∙ ∀[ (vk , σ) ∈ TxWitnesses.vKeySigs (Tx.txWitnesses txTop) ] isSigned vk (txidBytes (TxIdOf txTop)) σ ∙ ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided (GuardsOf txTop) txVldt s ∙ vKeyHashesNeeded ⊆ vKeyHashesProvided + ∙ ∀[ (kh , w) ∈ poolVoteSigs ] + ( kh ∈ spoVoters txTop + × PoolVoteAuthorized (PoolsOf Γ) maxKeyAgeEpochs (epoch (SlotOf Γ)) (poolVoteBytes txId) kh w) ∙ allScriptHashesNeeded - allReferenceScriptHashes ≡ᵉ allWitnessScriptHashes ∙ scriptHashesNeeded ⊆ mapˢ hash scriptsProvided ∙ dataHashesNeededSpendInputs ⊆ dataHashesProvided @@ -519,6 +558,9 @@ attempting both. ∙ ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes (TxIdOf txTop)) σ ∙ ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided (GuardsOf txTop) txVldt s ∙ vKeyHashesNeeded ⊆ vKeyHashesProvided + ∙ ∀[ (kh , w) ∈ poolVoteSigs ] + ( kh ∈ spoVoters txTop + × PoolVoteAuthorized (PoolsOf Γ) maxKeyAgeEpochs (epoch (SlotOf Γ)) (poolVoteBytes txId) kh w) ∙ allScriptHashesNeeded - allReferenceScriptHashes ≡ᵉ allWitnessScriptHashes ∙ scriptHashesNeeded ⊆ mapˢ hash scriptsProvided ∙ dataHashesNeededSpendInputs ⊆ dataHashesProvided @@ -538,8 +580,8 @@ attempting both. unquoteDecl UTXOW-normal-premises = genPremises UTXOW-normal-premises (quote UTXOW-normal) unquoteDecl UTXOW-legacy-premises = genPremises UTXOW-legacy-premises (quote UTXOW-legacy) unquoteDecl SUBUTXOW-premises = genPremises SUBUTXOW-premises (quote SUBUTXOW) -pattern UTXOW-normal-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ h = UTXOW-normal (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , h) -pattern UTXOW-legacy-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ h = UTXOW-legacy (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , h) -pattern SUBUTXOW-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ h = SUBUTXOW (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , h) +pattern UTXOW-normal-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ h = UTXOW-normal (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , h) +pattern UTXOW-legacy-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ h = UTXOW-legacy (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , h) +pattern SUBUTXOW-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ h = SUBUTXOW (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , h) ``` --> diff --git a/src/Ledger/Dijkstra/Specification/Utxow/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Utxow/Properties/Computational.lagda.md index fa7dc6be12..d1ab9e3d5b 100644 --- a/src/Ledger/Dijkstra/Specification/Utxow/Properties/Computational.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxow/Properties/Computational.lagda.md @@ -41,8 +41,8 @@ instance computeProof-aux : Dec H → ComputationResult String (∃[ s₁ ] (Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXOW⦈ s₁)) computeProof-aux (no ¬p) = failure "SUBUTXOW" - computeProof-aux (yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁)) = - map (map₂′ (λ h → SUBUTXOW {txSub = txSub} {Γ = Γ} (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , h))) + computeProof-aux (yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂)) = + map (map₂′ (λ h → SUBUTXOW {txSub = txSub} {Γ = Γ} (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , h))) (SUBUTXO.computeProof Γ s₀ txSub) computeProof : ComputationResult String (∃[ s₁ ] (Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXOW⦈ s₁)) @@ -51,9 +51,9 @@ instance completeness-aux : (d : Dec H) (s₁ : UTxOState) → Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXOW⦈ s₁ → map proj₁ (computeProof-aux d) ≡ success s₁ - completeness-aux (no ¬p) _ (SUBUTXOW-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ h) = - ⊥-elim $ ¬p (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁) - completeness-aux (yes _) _ (SUBUTXOW-⋯ _ _ _ _ _ _ _ _ _ _ _ _ h) + completeness-aux (no ¬p) _ (SUBUTXOW-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ h) = + ⊥-elim $ ¬p (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂) + completeness-aux (yes _) _ (SUBUTXOW-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ h) with SUBUTXO.computeProof Γ s₀ txSub | SUBUTXO.completeness _ _ _ _ h ... | success _ | refl = refl @@ -71,11 +71,11 @@ instance computeProof-aux : Dec H-legacy → Dec H-normal → ComputationResult String (∃[ s₁ ] (Γ ⊢ s₀ ⇀⦇ txTop ,UTXOW⦈ s₁)) - computeProof-aux (yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅)) _ = - map (map₂′ (λ h → UTXOW-legacy {txTop = txTop} {Γ = Γ} (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , h))) + computeProof-aux (yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆)) _ = + map (map₂′ (λ h → UTXOW-legacy {txTop = txTop} {Γ = Γ} (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , h))) (UTXO.computeProof Γ s₀ txTop) - computeProof-aux (no _) (yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄)) = - map (map₂′ (λ h → UTXOW-normal {txTop = txTop} {Γ = Γ} (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , h))) + computeProof-aux (no _) (yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅)) = + map (map₂′ (λ h → UTXOW-normal {txTop = txTop} {Γ = Γ} (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , h))) (UTXO.computeProof Γ s₀ txTop) computeProof-aux (no p) (no p') = failure "UTXOW" -- TODO: see https://github.com/IntersectMBO/formal-ledger-specifications/issues/1269 @@ -88,16 +88,16 @@ instance (s₁ : UTxOState) → Γ ⊢ s₀ ⇀⦇ txTop ,UTXOW⦈ s₁ → map proj₁ (computeProof-aux dLeg dNorm) ≡ success s₁ - completeness-aux (yes (q₀ , _)) _ _ (UTXOW-normal-⋯ p₀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) = + completeness-aux (yes (q₀ , _)) _ _ (UTXOW-normal-⋯ p₀ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) = case trans (sym q₀) p₀ of λ () - completeness-aux (yes _) _ _ (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) + completeness-aux (yes _) _ _ (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) with UTXO.computeProof Γ s₀ txTop | UTXO.completeness _ _ _ _ h ... | success _ | refl = refl - completeness-aux (no ¬p) _ _ (UTXOW-legacy-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ _) = + completeness-aux (no ¬p) _ _ (UTXOW-legacy-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ _) = + ⊥-elim (¬p (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆)) + completeness-aux (no _) (no ¬p) _ (UTXOW-normal-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ _) = ⊥-elim (¬p (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅)) - completeness-aux (no _) (no ¬p) _ (UTXOW-normal-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ _) = - ⊥-elim (¬p (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ )) - completeness-aux (no _) (yes _) _ (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) + completeness-aux (no _) (yes _) _ (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) with UTXO.computeProof Γ s₀ txTop | UTXO.completeness _ _ _ _ h ... | success _ | refl = refl