From 84bfdbeb4f1d7cd717e162090a576f37e6e35971 Mon Sep 17 00:00:00 2001 From: Polina Vinogradova Date: Mon, 15 Apr 2024 20:36:22 -0400 Subject: [PATCH] compiling Chain, working on lin-tests --- src/Ledger/Chain.lagda | 1 + src/Ledger/LinTest.lagda | 267 +++++++++++++++++++++++++++++++++++++++ src/Ledger/Utxo.lagda | 2 +- src/Ledger/Zone.lagda | 31 +++-- 4 files changed, 284 insertions(+), 17 deletions(-) create mode 100644 src/Ledger/LinTest.lagda diff --git a/src/Ledger/Chain.lagda b/src/Ledger/Chain.lagda index 0899a1fef..3e88c1f74 100644 --- a/src/Ledger/Chain.lagda +++ b/src/Ledger/Chain.lagda @@ -19,6 +19,7 @@ open import Ledger.Ledger txs abs open import Ledger.Ratify txs open import Ledger.Utxo txs abs open import Ledger.Epoch txs abs +open import Ledger.Zone txs abs \end{code} \begin{figure*}[h] diff --git a/src/Ledger/LinTest.lagda b/src/Ledger/LinTest.lagda new file mode 100644 index 000000000..b9a2d1bd2 --- /dev/null +++ b/src/Ledger/LinTest.lagda @@ -0,0 +1,267 @@ +\section{Transaction Linearelisability Test} + +\begin{code}[hide] +{-# OPTIONS --safe #-} + +open import Ledger.Transaction +open import Ledger.PParams +open import Ledger.Prelude +open import Ledger.Abstract +open import Ledger.Transaction using (TransactionStructure) + +module Ledger.LinTest + (txs : _) (open TransactionStructure txs) + (abs : AbstractFunctions txs) (open AbstractFunctions abs) + where + +open import Ledger.Zone txs abs + +open Tx +\end{code} + +Topological sort/cycle detection tests. + +\begin{figure*}[h] +\begin{code} + +txBody : TxBody +txBody = record { + txins : ℙ TxIn + txouts : Ix ⇀ TxOut + txfee = 0 + mint = ∅ + txvldt = (nothing , nothing) + txcerts = [] + txwdrls = ∅ + txvote = [] + txprop = [] + txdonation = 0 + txup = nothing + txADhash = nothing + netwrk = nothing + txsize = 0 + txid : TxId + collateral : ℙ TxIn + reqSigHash : ℙ KeyHash + scriptIntHash = nothing + fulfills : ℙ Fulfill + requests : Ix ⇀ Request + requiredTxs = ∅ + } + +txWits : TxWitnesses +txWits = record { + vkSigs = ∅ + scripts = ∅ + txdats = ∅ + txrdmrs = ∅ + } + + +tx : Tx +tx = record { body = txBody; wits = txWits; isValid = true; txAD = nothing } + + + + + + + +-- get a set of TxIds containing all IDs of transaction in given list tb +getIDs : List Tx → ℙ TxId +getIDs tb = foldr (λ { tx ls → ls ∪ (singleton (tx .Tx.body .TxBody.txid)) }) ∅ tb + +-- make edges for a given transaction +mkEdges : Tx → List Tx → List (Tx × Tx) +mkEdges _ [] = [] +mkEdges tx (h ∷ tb) with ( ( tx .Tx.body .TxBody.txid ) ∈? (fromList (map proj₁ (setToList (h .Tx.body .TxBody.txins)))) ) +... | yes p = (tx , h) ∷ mkEdges tx tb +... | no ¬p = mkEdges tx tb + +-- make FR edges for a given transaction +mkFREdges : Tx → List Tx → List (Tx × Tx) +mkFREdges _ [] = [] +mkFREdges tx (h ∷ tb) with ( ( tx .Tx.body .TxBody.txid ) ∈? (fromList (map proj₁ (setToList (h .Tx.body .TxBody.fulfills)))) ) +... | yes p = (h , tx) ∷ mkFREdges tx tb +... | no ¬p = mkFREdges tx tb + +-- make all edges for all transactions +mkAllEdges : List Tx → List Tx → List (Tx × Tx) +mkAllEdges [] ls = [] +mkAllEdges (h ∷ tb) ls = mkEdges h ls ++ mkFREdges h ls ++ mkAllEdges tb ls + +-- for a given tx, and set of edges, +-- returns a list of transactions ls such that for each e in ls is such that e -> tx is a dependency +-- i.e. returns all ends of incoming edges +hasIncEdges : Tx → List (Tx × Tx) → List Tx +hasIncEdges tx [] = [] +hasIncEdges tx ((e , tx') ∷ edges) with (tx .Tx.body .TxBody.txid ≡ᵇ tx' .Tx.body .TxBody.txid) +... | true = e ∷ (hasIncEdges tx edges) +... | false = (hasIncEdges tx edges) + +-- filters a list of transactions such that only ones with no incoming edges remain +nodesWithNoIncomingEdge : List Tx → List (Tx × Tx) → List Tx +nodesWithNoIncomingEdge [] edges = [] +nodesWithNoIncomingEdge (tx ∷ txs) edges with (hasIncEdges tx edges) +... | e ∷ dges = nodesWithNoIncomingEdge txs edges +... | [] = tx ∷ nodesWithNoIncomingEdge txs edges + +-- remove the first instance of a transaction in a list +removeTx : Tx → List Tx → List Tx +removeTx tx [] = [] +removeTx tx (n ∷ ne) with (tx .Tx.body .TxBody.txid ≡ᵇ n .Tx.body .TxBody.txid) +... | true = ne +... | false = [ n ] ++ (removeTx tx ne) + +-- remove a transaction from a list if it has no incoming edges +ifNoEdgeRemove : Tx → List (Tx × Tx) → List Tx → List Tx +ifNoEdgeRemove tx edges s with (hasIncEdges tx edges) +... | [] = removeTx tx s +... | e ∷ dges = s + +-- given tx1, for all tx such that (tx1 , tx) in edges, +-- remove (tx1 , tx) from the graph +-- if tx has no other incoming edges then +-- insert tx into S +updateRES : Tx → List (Tx × Tx) → List Tx → ((List (Tx × Tx)) × (List Tx)) +updateRES tx1 [] s = ([] , s) +updateRES tx1 ((tx , tx') ∷ em) s with (tx .Tx.body .TxBody.txid ≡ᵇ tx1 .Tx.body .TxBody.txid) +... | true = (proj₁ (updateRES tx1 em (ifNoEdgeRemove tx em s)) , (ifNoEdgeRemove tx em s)) +... | false = ((tx , tx') ∷ proj₁ (updateRES tx1 em s) , s) + +-- topologically sorts a tx list +-- arguments : tracking edges for agda termination check, remaining edges, remaining txs with no incoming edge (S), current sorted list (L) +-- returns nothing if there are remaining edges the graph, but S is empty +topSortTxs : List (Tx × Tx) → List (Tx × Tx) → List Tx → List Tx → Maybe (List Tx) +topSortTxs e [] s srtd = just srtd +topSortTxs [] (r ∷ em) s srtd = nothing +topSortTxs e (r ∷ em) [] srtd = nothing +topSortTxs ((tx1 , tx2) ∷ dges) (r ∷ em) (tx ∷ rls) srtd = + topSortTxs dges (proj₁ updRES) (proj₂ updRES) (srtd ++ [ tx1 ]) + where updRES = updateRES tx1 (r ∷ em) (removeTx tx1 (tx ∷ rls)) + +-- TOP SORT original +-- L ← Empty list that will contain the sorted elements +-- S ← Set of all nodes with no incoming edge +-- +-- while S is not empty do +-- remove a node n from S +-- add n to L +-- for each node m with an edge e from n to m do +-- remove edge e from the graph +-- if m has no other incoming edges then +-- insert m into S +-- +-- if graph has edges then +-- return error (graph has at least one cycle) +-- else +-- return L (a topologically sorted order) + +-- TOP SORT implemented +-- L ← Empty list that will contain the sorted elements +-- S ← Set of all nodes with no incoming edge +-- -- +-- for each (tx1 , tx2) in edges do +-- remove tx1 from S +-- add tx1 to L +-- for all tx such that (tx1 , tx) in edges, +-- remove (tx1 , tx) from the graph +-- if tx has no other incoming edges then +-- insert tx into S +-- +-- if graph has edges then +-- return error (graph has at least one cycle) +-- else +-- return L (a topologically sorted order) + +-- check that all IDs in all requiredTxs groups correspond to Txs in the given zone +chkRqTx : List Tx → Tx → Set +chkRqTx tb tx = ∀[ txrid ∈ tx .Tx.body .TxBody.requiredTxs ] Any (txrid ≡_) ( getIDs tb ) + +-- check for duplicates in two sets +noDups : ℙ Tx → ℙ Tx → Set +noDups tb tb' = ∀[ tx ∈ tb ] ∀[ tx' ∈ tb' ] ¬ tx ≡ tx' + +-- apply top. sort/cycle detection to graph generated from all transactions in the zone, with forward +-- edges between transactions spending each other's outputs within the zone, +-- and backwards edges between transactions spending each other's requests within the zone +chkLinear : List Tx → Set +chkLinear tb = topSortTxs (mkAllEdges tb tb) (mkAllEdges tb tb) (nodesWithNoIncomingEdge tb (mkAllEdges tb tb)) [] ≡ just [] + +-- sum up the fees (adjusted by collateralPercentage) of transactions in a list +sumCol : List Tx → ℕ → Coin +sumCol tb cp = foldr (λ { tx c → c + tx .Tx.body .TxBody.txfee * cp }) 0 tb + +\end{code} +\caption{Functions used for zone validation} +\label{fig:functions:zone} +\end{figure*} + +\begin{figure*}[h] +\begin{code}[hide] +data +\end{code} +\begin{code} + _⊢_⇀⦇_,ZONE⦈_ : LEnv → LState → List Tx → LState → Set +\end{code} +\begin{code}[hide] + where +\end{code} +\caption{The type of the ZONE transition system} +\end{figure*} + +\begin{code}[hide] +private variable + Γ : LEnv + utxo utxo' : UTxO + fees fees' : Coin + deposits deposits' : Deposits + donations donations' : Coin + govSt govSt' : GovState + certState certState' : CertState + tb lsV : List Tx + tx : Tx +\end{code} + +\begin{figure*}[h] +\begin{code} + ZONE-V : + Γ ⊢ ⟦ ⟦ (utxo , ∅) , fees , deposits , donations ⟧ᵘᵘ , govSt , certState ⟧ˡˡ ⇀⦇ tb ,LEDGERS⦈ + ⟦ ⟦ (utxo' , ∅) , fees' , deposits' , donations' ⟧ᵘᵘ , govSt' , certState' ⟧ˡˡ + ∙ All (chkRqTx tb) (fromList tb) + ∙ chkLinear tb + ∙ All chkIsValid (fromList tb) + ∙ ((coin (balance (utxo ∣ tx .Tx.body .TxBody.collateral)) * 100) + ≥ᵇ sumCol (lsV ++ [ tx ]) (Γ .LEnv.pparams .PParams.collateralPercentage)) ≡ true + ──────────────────────────────── + Γ ⊢ ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , certState ⟧ˡ ⇀⦇ tb ,ZONE⦈ ⟦ ⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ , govSt' , certState' ⟧ˡ + ZONE-N : + Γ ⊢ ⟦ ⟦ (utxo , ∅) , fees , deposits , donations ⟧ᵘᵘ , govSt , certState ⟧ˡˡ ⇀⦇ (lsV ++ [ tx ]) ,LEDGERS⦈ _ + ∙ tx .Tx.isValid ≡ false + ∙ All chkIsValid (fromList lsV) + ∙ ((coin (balance (utxo ∣ tx .Tx.body .TxBody.collateral)) * 100) + ≥ᵇ sumCol (lsV ++ [ tx ]) (Γ .LEnv.pparams .PParams.collateralPercentage)) ≡ true + ──────────────────────────────── + Γ ⊢ ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , certState ⟧ˡ ⇀⦇ tb ,ZONE⦈ + ⟦ ⟦ utxo ∣ (tx .Tx.body .TxBody.collateral) ᶜ + , fees + cbalance (utxo ∣ tx .Tx.body .TxBody.collateral) + , deposits , donations ⟧ᵘ + , govSt + , certState ⟧ˡ +\end{code} +\caption{ZONE transition system} +\end{figure*} +\begin{code}[hide] +-- TODO fix this +-- unquoteDecl ZONE-V-premises = genPremises ZONE-V-premises (quote ZONE-V) +-- unquoteDecl ZONE-N-premises = genPremises ZONE-N-premises (quote ZONE-N) +-- pattern ZONE-V⋯ x y z w = ZONE (x , y , z , w) +-- unquoteDecl ZONE-premises = genPremises ZONE-premises (quote ZONE) +\end{code} +\begin{figure*}[h] +\begin{code} +_⊢_⇀⦇_,ZONES⦈_ : LEnv → LState → List (List Tx) → LState → Set +_⊢_⇀⦇_,ZONES⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,ZONE⦈_ +\end{code} +\caption{ZONES transition system} +\end{figure*} diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index 7cf206cc4..31d62ebc5 100644 --- a/src/Ledger/Utxo.lagda +++ b/src/Ledger/Utxo.lagda @@ -372,7 +372,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where open UTxOEnv Γ renaming (pparams to pp) open UTxOStateTemp s in - ∙ txins ≢ ∅ ∙ txins ⊆ dom (nutxo utxoTemp) -- TODO change this to check in spent UTxOs/FRxOs + ∙ txins ≢ ∅ ∙ txins ⊆ dom (nutxo utxoTemp) - ∙ inInterval slot txvldt ∙ feesOK pp tx (nutxo utxoTemp) ≡ true ∙ consumed pp s txb ≡ produced pp s txb ∙ coin mint ≡ 0 ∙ txsize ≤ maxTxSize pp diff --git a/src/Ledger/Zone.lagda b/src/Ledger/Zone.lagda index d3719e915..d45eb0a8d 100644 --- a/src/Ledger/Zone.lagda +++ b/src/Ledger/Zone.lagda @@ -3,9 +3,6 @@ \begin{code}[hide] {-# OPTIONS --safe #-} --- open import Data.List as L --- open import Data.List.Relation.Unary.All - open import Ledger.Transaction open import Ledger.PParams open import Ledger.Prelude @@ -24,6 +21,7 @@ open import Ledger.Utxow txs abs open import Ledger.Ledger txs abs open Tx +open TxBody \end{code} The entire state transformation of the ledger state caused by a valid @@ -35,19 +33,19 @@ defined transition systems. -- get a set of TxIds containing all IDs of transaction in given list tb getIDs : List Tx → ℙ TxId -getIDs tb = foldr (λ { tx ls → ls ∪ (singleton (tx .Tx.body .TxBody.txid)) }) ∅ tb +getIDs tb = foldr (λ { tx ls → ls ∪ (singleton (tx .body .txid)) }) ∅ tb -- make edges for a given transaction mkEdges : Tx → List Tx → List (Tx × Tx) mkEdges _ [] = [] -mkEdges tx (h ∷ tb) with ( ( tx .Tx.body .TxBody.txid ) ∈? (fromList (map proj₁ (setToList (h .Tx.body .TxBody.txins)))) ) +mkEdges tx (h ∷ tb) with ( ( tx .body .txid ) ∈? (fromList (map proj₁ (setToList (h .body .txins)))) ) ... | yes p = (tx , h) ∷ mkEdges tx tb ... | no ¬p = mkEdges tx tb -- make FR edges for a given transaction mkFREdges : Tx → List Tx → List (Tx × Tx) mkFREdges _ [] = [] -mkFREdges tx (h ∷ tb) with ( ( tx .Tx.body .TxBody.txid ) ∈? (fromList (map proj₁ (setToList (h .Tx.body .TxBody.fulfills)))) ) +mkFREdges tx (h ∷ tb) with ( ( tx .body .txid ) ∈? (fromList (map proj₁ (setToList (h .body .fulfills)))) ) ... | yes p = (h , tx) ∷ mkFREdges tx tb ... | no ¬p = mkFREdges tx tb @@ -61,7 +59,7 @@ mkAllEdges (h ∷ tb) ls = mkEdges h ls ++ mkFREdges h ls ++ mkAllEdges tb ls -- i.e. returns all ends of incoming edges hasIncEdges : Tx → List (Tx × Tx) → List Tx hasIncEdges tx [] = [] -hasIncEdges tx ((e , tx') ∷ edges) with (tx .Tx.body .TxBody.txid ≡ᵇ tx' .Tx.body .TxBody.txid) +hasIncEdges tx ((e , tx') ∷ edges) with (tx .body .txid ≡ᵇ tx' .body .txid) ... | true = e ∷ (hasIncEdges tx edges) ... | false = (hasIncEdges tx edges) @@ -75,7 +73,7 @@ nodesWithNoIncomingEdge (tx ∷ txs) edges with (hasIncEdges tx edges) -- remove the first instance of a transaction in a list removeTx : Tx → List Tx → List Tx removeTx tx [] = [] -removeTx tx (n ∷ ne) with (tx .Tx.body .TxBody.txid ≡ᵇ n .Tx.body .TxBody.txid) +removeTx tx (n ∷ ne) with (tx .body .txid ≡ᵇ n .body .txid) ... | true = ne ... | false = [ n ] ++ (removeTx tx ne) @@ -91,12 +89,13 @@ ifNoEdgeRemove tx edges s with (hasIncEdges tx edges) -- insert tx into S updateRES : Tx → List (Tx × Tx) → List Tx → ((List (Tx × Tx)) × (List Tx)) updateRES tx1 [] s = ([] , s) -updateRES tx1 ((tx , tx') ∷ em) s with (tx .Tx.body .TxBody.txid ≡ᵇ tx1 .Tx.body .TxBody.txid) +updateRES tx1 ((tx , tx') ∷ em) s with (tx .body .txid ≡ᵇ tx1 .body .txid) ... | true = (proj₁ (updateRES tx1 em (ifNoEdgeRemove tx em s)) , (ifNoEdgeRemove tx em s)) ... | false = ((tx , tx') ∷ proj₁ (updateRES tx1 em s) , s) -- topologically sorts a tx list -- arguments : tracking edges for agda termination check, remaining edges, remaining txs with no incoming edge (S), current sorted list (L) +-- returns nothing if there are remaining edges the graph, but S is empty topSortTxs : List (Tx × Tx) → List (Tx × Tx) → List Tx → List Tx → Maybe (List Tx) topSortTxs e [] s srtd = just srtd topSortTxs [] (r ∷ em) s srtd = nothing @@ -141,7 +140,7 @@ topSortTxs ((tx1 , tx2) ∷ dges) (r ∷ em) (tx ∷ rls) srtd = -- check that all IDs in all requiredTxs groups correspond to Txs in the given zone chkRqTx : List Tx → Tx → Set -chkRqTx tb tx = ∀[ txrid ∈ tx .Tx.body .TxBody.requiredTxs ] Any (txrid ≡_) ( getIDs tb ) +chkRqTx tb tx = ∀[ txrid ∈ tx .body .requiredTxs ] Any (txrid ≡_) ( getIDs tb ) -- check for duplicates in two sets noDups : ℙ Tx → ℙ Tx → Set @@ -155,7 +154,7 @@ chkLinear tb = topSortTxs (mkAllEdges tb tb) (mkAllEdges tb tb) (nodesWithNoInco -- sum up the fees (adjusted by collateralPercentage) of transactions in a list sumCol : List Tx → ℕ → Coin -sumCol tb cp = foldr (λ { tx c → c + tx .Tx.body .TxBody.txfee * cp }) 0 tb +sumCol tb cp = foldr (λ { tx c → c + tx .body .txfee * cp }) 0 tb \end{code} \caption{Functions used for zone validation} @@ -196,20 +195,20 @@ private variable ∙ All (chkRqTx tb) (fromList tb) ∙ chkLinear tb ∙ All chkIsValid (fromList tb) - ∙ ((coin (balance (utxo ∣ tx .Tx.body .TxBody.collateral)) * 100) + ∙ ((coin (balance (utxo ∣ tx .body .collateral)) * 100) ≥ᵇ sumCol (lsV ++ [ tx ]) (Γ .LEnv.pparams .PParams.collateralPercentage)) ≡ true ──────────────────────────────── Γ ⊢ ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , certState ⟧ˡ ⇀⦇ tb ,ZONE⦈ ⟦ ⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ , govSt' , certState' ⟧ˡ ZONE-N : Γ ⊢ ⟦ ⟦ (utxo , ∅) , fees , deposits , donations ⟧ᵘᵘ , govSt , certState ⟧ˡˡ ⇀⦇ (lsV ++ [ tx ]) ,LEDGERS⦈ _ - ∙ tx .Tx.isValid ≡ false + ∙ tx .isValid ≡ false ∙ All chkIsValid (fromList lsV) - ∙ ((coin (balance (utxo ∣ tx .Tx.body .TxBody.collateral)) * 100) + ∙ ((coin (balance (utxo ∣ tx .body .collateral)) * 100) ≥ᵇ sumCol (lsV ++ [ tx ]) (Γ .LEnv.pparams .PParams.collateralPercentage)) ≡ true ──────────────────────────────── Γ ⊢ ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , certState ⟧ˡ ⇀⦇ tb ,ZONE⦈ - ⟦ ⟦ utxo ∣ (tx .Tx.body .TxBody.collateral) ᶜ - , fees + cbalance (utxo ∣ tx .Tx.body .TxBody.collateral) + ⟦ ⟦ utxo ∣ (tx .body .collateral) ᶜ + , fees + cbalance (utxo ∣ tx .body .collateral) , deposits , donations ⟧ᵘ , govSt , certState ⟧ˡ