Skip to content

LEDGERS: Computational

This module proves that LEDGERS transition is computational.

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction
open import Ledger.Dijkstra.Specification.Abstract

module Ledger.Dijkstra.Specification.Ledgers.Properties.Computational
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Utxo txs abs
open import Ledger.Dijkstra.Specification.Ledger txs abs
open import Ledger.Dijkstra.Specification.Ledger.Properties.Computational txs abs
open import Ledger.Dijkstra.Specification.Ledgers txs abs

instance
  _ = Monad-ComputationResult

open Computational ⦃...⦄

computeLedger : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,LEDGER⦈ s')
computeLedger = computeProof {STS = _⊢_⇀⦇_,LEDGER⦈_}

completeLedger : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,LEDGER⦈ s' → (proj₁ <$> computeLedger Γ s x) ≡ success s'
completeLedger = completeness {STS = _⊢_⇀⦇_,LEDGER⦈_}

LEDGERSWithLimits-computeProof
  : (Γw : LedgersEnv) (s : LedgersWithLimitsState) (topTxs : List TopLevelTx)
  → ComputationResult String (∃[ s' ] Γw ⊢ s ⇀⦇ topTxs ,LEDGERSWithLimits⦈ s')
LEDGERSWithLimits-computeProof Γw s [] = success (s , LEDGERSWithLimits-[])
LEDGERSWithLimits-computeProof Γw s (topTx ∷ topTxs)
  with computeLedger (LedgersEnv.ledgerEnv Γw) (LedgersWithLimitsState.ledgerState s) topTx
... | failure e = failure e
... | success (ls' , step)
  with LedgersWithLimitsState.refScriptsSizeAcc s + totalRefScriptsSize (UTxOOf (LedgersWithLimitsState.ledgerState s)) topTx ≤? LedgersEnv.refScriptsSizeLimit Γw
... | no ¬p = failure "LEDGERSWithLimits: accumulated reference script size exceeds the limit"
... | yes p
  with ¿ LedgersWithLimitsState.exUnitsAcc s + totalExUnits topTx ≤ᵉᵘ LedgersEnv.exUnitsLimit Γw ¿
... | no ¬q = failure "LEDGERSWithLimits: accumulated ExUnits exceed the limit"
... | yes q
  with LEDGERSWithLimits-computeProof Γw $\begin{pmatrix} \,\htmlId{2224}{\htmlClass{Bound}{\text{ls'}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1189}{\htmlId{2230}{\htmlClass{Field}{\text{LedgersWithLimitsState.refScriptsSizeAcc}}}}\, \,\htmlId{2271}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2273}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#2180}{\htmlId{2275}{\htmlClass{Function}{\text{totalRefScriptsSize}}}}\, \,\htmlId{2295}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5921}{\htmlId{2296}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{2303}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledgers.html#1153}{\htmlId{2304}{\htmlClass{Field}{\text{LedgersWithLimitsState.ledgerState}}}}\, \,\htmlId{2339}{\htmlClass{Bound}{\text{s}}}\,\,\htmlId{2340}{\htmlClass{Symbol}{\text{))}}}\, \,\htmlId{2343}{\htmlClass{Bound}{\text{topTx}}}\, , \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1215}{\htmlId{2351}{\htmlClass{Field}{\text{LedgersWithLimitsState.exUnitsAcc}}}}\, \,\htmlId{2385}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2387}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#1978}{\htmlId{2389}{\htmlClass{Function}{\text{totalExUnits}}}}\, \,\htmlId{2402}{\htmlClass{Bound}{\text{topTx}}}\, \end{pmatrix}$ topTxs
... | failure e = failure e
... | success (s'' , rest) = success (s'' , LEDGERSWithLimits-∷ (step , p , q , rest))

LEDGERSWithLimits-completeness
  : (Γw : LedgersEnv) (s : LedgersWithLimitsState) (topTxs : List TopLevelTx) (s' : LedgersWithLimitsState)
  → Γw ⊢ s ⇀⦇ topTxs ,LEDGERSWithLimits⦈ s'
  → (proj₁ <$> LEDGERSWithLimits-computeProof Γw s topTxs) ≡ success s'
LEDGERSWithLimits-completeness Γw s [] .s LEDGERSWithLimits-[] = refl
LEDGERSWithLimits-completeness Γw s (topTx ∷ topTxs) s'' (LEDGERSWithLimits-∷ {ls' = ls'} (step , p , q , rest))
  with computeLedger (LedgersEnv.ledgerEnv Γw) (LedgersWithLimitsState.ledgerState s) topTx
     | completeLedger (LedgersEnv.ledgerEnv Γw) (LedgersWithLimitsState.ledgerState s) topTx ls' step
... | success _ | refl
  with LedgersWithLimitsState.refScriptsSizeAcc s + totalRefScriptsSize (UTxOOf (LedgersWithLimitsState.ledgerState s)) topTx ≤? LedgersEnv.refScriptsSizeLimit Γw
... | no ¬p = ⊥-elim (¬p p)
... | yes _
  with ¿ LedgersWithLimitsState.exUnitsAcc s + totalExUnits topTx ≤ᵉᵘ LedgersEnv.exUnitsLimit Γw ¿
... | no ¬q = ⊥-elim (¬q q)
... | yes _
  with LEDGERSWithLimits-computeProof Γw $\begin{pmatrix} \,\htmlId{3573}{\htmlClass{Bound}{\text{ls'}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1189}{\htmlId{3579}{\htmlClass{Field}{\text{LedgersWithLimitsState.refScriptsSizeAcc}}}}\, \,\htmlId{3620}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3622}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#2180}{\htmlId{3624}{\htmlClass{Function}{\text{totalRefScriptsSize}}}}\, \,\htmlId{3644}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5921}{\htmlId{3645}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{3652}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledgers.html#1153}{\htmlId{3653}{\htmlClass{Field}{\text{LedgersWithLimitsState.ledgerState}}}}\, \,\htmlId{3688}{\htmlClass{Bound}{\text{s}}}\,\,\htmlId{3689}{\htmlClass{Symbol}{\text{))}}}\, \,\htmlId{3692}{\htmlClass{Bound}{\text{topTx}}}\, , \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1215}{\htmlId{3700}{\htmlClass{Field}{\text{LedgersWithLimitsState.exUnitsAcc}}}}\, \,\htmlId{3734}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3736}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#1978}{\htmlId{3738}{\htmlClass{Function}{\text{totalExUnits}}}}\, \,\htmlId{3751}{\htmlClass{Bound}{\text{topTx}}}\, \end{pmatrix}$ topTxs
     | LEDGERSWithLimits-completeness Γw $\begin{pmatrix} \,\htmlId{3809}{\htmlClass{Bound}{\text{ls'}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1189}{\htmlId{3815}{\htmlClass{Field}{\text{LedgersWithLimitsState.refScriptsSizeAcc}}}}\, \,\htmlId{3856}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3858}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#2180}{\htmlId{3860}{\htmlClass{Function}{\text{totalRefScriptsSize}}}}\, \,\htmlId{3880}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5921}{\htmlId{3881}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{3888}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledgers.html#1153}{\htmlId{3889}{\htmlClass{Field}{\text{LedgersWithLimitsState.ledgerState}}}}\, \,\htmlId{3924}{\htmlClass{Bound}{\text{s}}}\,\,\htmlId{3925}{\htmlClass{Symbol}{\text{))}}}\, \,\htmlId{3928}{\htmlClass{Bound}{\text{topTx}}}\, , \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1215}{\htmlId{3936}{\htmlClass{Field}{\text{LedgersWithLimitsState.exUnitsAcc}}}}\, \,\htmlId{3970}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3972}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#1978}{\htmlId{3974}{\htmlClass{Function}{\text{totalExUnits}}}}\, \,\htmlId{3987}{\htmlClass{Bound}{\text{topTx}}}\, \end{pmatrix}$ topTxs s'' rest
... | success _ | refl = refl

instance

  Computational-LEDGERSWithLimits : Computational _⊢_⇀⦇_,LEDGERSWithLimits⦈_ String

  Computational-LEDGERSWithLimits .computeProof = LEDGERSWithLimits-computeProof
  Computational-LEDGERSWithLimits .completeness = LEDGERSWithLimits-completeness

LEDGERS-computeProof
  : (Γw : LedgersEnv) (ls : LedgerState) (topTxs : List TopLevelTx)
  → ComputationResult String (∃[ ls' ] Γw ⊢ ls ⇀⦇ topTxs ,LEDGERS⦈ ls')
LEDGERS-computeProof Γw ls topTxs
  with LEDGERSWithLimits-computeProof Γw $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.Properties.Computational.html#4518}{\htmlId{4571}{\htmlClass{Bound}{\text{ls}}}}\, \\ \,\htmlId{4576}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Script.Base.html#2360}{\htmlId{4580}{\htmlClass{Function}{\text{0ᵉᵘ}}}}\, \end{pmatrix}$ topTxs
... | failure e = failure e
... | success (s' , step) =
  success (LedgersWithLimitsState.ledgerState s' , LedgersWithLimitsState.refScriptsSizeAcc s' , LedgersWithLimitsState.exUnitsAcc s' , step)

LEDGERS-completeness
  : (Γw : LedgersEnv) (ls : LedgerState) (topTxs : List TopLevelTx) (ls' : LedgerState)
  → Γw ⊢ ls ⇀⦇ topTxs ,LEDGERS⦈ ls'
  → (proj₁ <$> LEDGERS-computeProof Γw ls topTxs) ≡ success ls'
LEDGERS-completeness Γw ls topTxs ls' (accRS , accEU , step)
  with LEDGERSWithLimits-computeProof Γw $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.Properties.Computational.html#5025}{\htmlId{5105}{\htmlClass{Bound}{\text{ls}}}}\, \\ \,\htmlId{5110}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Script.Base.html#2360}{\htmlId{5114}{\htmlClass{Function}{\text{0ᵉᵘ}}}}\, \end{pmatrix}$ topTxs
     | LEDGERSWithLimits-completeness Γw $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.Properties.Computational.html#5025}{\htmlId{5170}{\htmlClass{Bound}{\text{ls}}}}\, \\ \,\htmlId{5175}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Script.Base.html#2360}{\htmlId{5179}{\htmlClass{Function}{\text{0ᵉᵘ}}}}\, \end{pmatrix}$ topTxs $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.Properties.Computational.html#5035}{\htmlId{5194}{\htmlClass{Bound}{\text{ls'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.Properties.Computational.html#5040}{\htmlId{5200}{\htmlClass{Bound}{\text{accRS}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.Properties.Computational.html#5048}{\htmlId{5208}{\htmlClass{Bound}{\text{accEU}}}}\, \end{pmatrix}$ step
... | success _ | refl = refl

instance

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

  Computational-LEDGERS .computeProof = LEDGERS-computeProof
  Computational-LEDGERS .completeness = LEDGERS-completeness