Ledger: Computational

This module proves that the LEDGER transition system is computational.

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Transaction
open import Ledger.Conway.Specification.Abstract
import Ledger.Conway.Specification.Certs

module Ledger.Conway.Specification.Ledger.Properties.Computational
  (txs : _) (open TransactionStructure txs) (open Ledger.Conway.Specification.Certs govStructure)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Prelude
open import Ledger.Conway.Specification.Certs.Properties.Computational govStructure
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Conway.Specification.Gov.Properties.Computational txs
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Conway.Specification.Utxo txs abs
open import Ledger.Conway.Specification.Utxow txs abs
open import Ledger.Conway.Specification.Utxow.Properties.Computational txs abs

open import Data.Bool.Properties using (¬-not)

instance
  _ = Monad-ComputationResult

  Computational-LEDGER : Computational _⊢_⇀⦇_,LEDGER⦈_ String
  Computational-LEDGER = record {go}
    where
    open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete)
    computeUtxow = comp {STS = _⊢_⇀⦇_,UTXOW⦈_}
    computeCerts = comp {STS = _⊢_⇀⦇_,CERTS⦈_}
    computeGov   = comp {STS = _⊢_⇀⦇_,GOVS⦈_}

    module go
      (Γ : LEnv)   (let open LEnv Γ)
      (s : LState) (let open LState s)
      (tx : Tx)    (let open Tx tx renaming (body to txb); open TxBody txb)
      where
      utxoΓ = UTxOEnv ∋ record { LEnv Γ }
      certΓ = CertEnv ∋ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#903}{\htmlId{1838}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1055}{\htmlId{1844}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1113}{\htmlId{1851}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5051}{\htmlId{1861}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#4876}{\htmlId{1874}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\htmlId{1890}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$
      govΓ : CertState → GovEnv
      govΓ = λ certState → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Transaction.html#4768}{\htmlId{1955}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#903}{\htmlId{1962}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1055}{\htmlId{1968}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1113}{\htmlId{1975}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1078}{\htmlId{1985}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1139}{\htmlId{1995}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.Computational.html#1941}{\htmlId{2008}{\htmlClass{Bound}{\text{certState}}}}\, \\ \,\htmlId{2020}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$

      computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s')
      computeProof = case isValid ≟ true of λ where
        (yes p) → do
          (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
          (certSt' , certStep) ← computeCerts certΓ certState txCerts
          (govSt'  , govStep)  ← computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt) (txgov txb)
          success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
        (no ¬p) → do
          (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
          success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep)

      completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s'
      completeness ledgerSt (LEDGER-V⋯ v utxoStep certStep govStep)
        with isValid ≟ true
      ... | no ¬v = contradiction v ¬v
      ... | yes refl
        with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
      ... | success (utxoSt' , _) | refl
        with computeCerts certΓ certState txCerts | complete _ _ _ _ certStep
      ... | success (certSt' , _) | refl
        with computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep
      ... | success (govSt' , _) | refl = refl
      completeness ledgerSt (LEDGER-I⋯ i utxoStep)
        with isValid ≟ true
      ... | yes refl = case i of λ ()
      ... | no ¬v
        with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
      ... | success (utxoSt' , _) | refl = refl

Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String
Computational-LEDGERS = it