Fix links in Rewards module; migrate Transaction

build-tools/static/md/mkdocs/includes/links.md

@@ -1,6 +1,7 @@
 [Agda documentation]: https://agda.readthedocs.io/en/
 [Agda record types]: https://agda.readthedocs.io/en/stable/language/record-types.html
 [Agda Wiki]: https://wiki.portal.chalmers.se/agda/pmwiki.php
+[Amount of Rewards to be Paid Out]: Ledger.Conway.Specification.Rewards.md#sec:amount-of-rewards-to-be-paid-out
 [Auxiliary DELEG transition system]: Ledger.Conway.Specification.Certs.md#auxiliary-deleg-transition-system
 [Auxiliary GOVCERT transition system]: Ledger.Conway.Specification.Certs.md#auxiliary-govcert-transition-system
 [Auxiliary POOL transition system]: Ledger.Conway.Specification.Certs.md#auxiliary-pool-transition-system
@@ -37,10 +38,12 @@
 [RATIFY]: Ledger.Conway.Specification.Ratify.md#the-ratify-transition-system
 [(Re)introduction to Cardano]: https://developers.cardano.org/docs/operate-a-stake-pool/introduction-to-cardano/
 [repourl]: https://github.com/IntersectMBO/formal-ledger-specifications
+[Rewards Motivation]: Ledger.Conway.Specification.Rewards.md#sec:rewards-motivation
 [scriptsCost]: Ledger.Conway.Specification.Fees.md#scriptsCost
 [SNAP]: Ledger.Conway.Specification.Rewards.md#sec:snap-transition-system
-[Type signature of the GOV transition relation]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
 [Time handling on Cardano]: https://docs.cardano.org/about-cardano/explore-more/time
+[Timing of Rewards Payout]: Ledger.Conway.Specification.Rewards.md#sec:timing-of-rewards-payout
+[Type signature of the GOV transition relation]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
 [UTXO]: Ledger.Conway.Specification.Utxo.md#sec:utxo-inference-rule
 [UTXOS]: Ledger.Conway.Specification.Utxo.md#sec:utxos-rule
 [UTXOW]: Ledger.Conway.Specification.Utxow.md#utxow-inference-rules

src/Ledger/Conway/Specification/Rewards.lagda.md

@@ -1,12 +1,13 @@
 # Rewards {#sec:rewards}
 
-This section is part of the [Ledger.Conway.Specification.Rewards][] module of the
-[formal ledger specification][], where we define how rewards for stake pools and
-their delegators are calculated and paid out. This calculation has two main aspects.
+In this section we define how rewards for stake pools and their delegators
+are calculated and paid out. This calculation has two main aspects.
 
-1.  The *amount* of rewards to be paid out. This is defined in the section [Amount of Rewards to be Paid Out][].
+1.  The *amount* of rewards to be paid out. This is defined in the section
+    [Amount of Rewards to be Paid Out][].
 
-2.  The *time* when rewards are paid out. This is defined in the section [Timing of Rewards Payout][].
+2.  The *time* when rewards are paid out. This is defined in the section
+    [Timing of Rewards Payout][].
 
 
 <!--
@@ -39,7 +40,6 @@ open import Ledger.Conway.Specification.Utxo txs abs
 -->
 
 ## Rewards Motivation {#sec:rewards-motivation}
-[Rewards Motivation]: #sec:rewards-motivation
 
 In order to operate, any blockchain needs to attract parties that are
 willing to spend computational and network resources on processing
@@ -88,8 +88,7 @@ number of stake pools that attract most of the stake. For more details
 about the design and rationale of the rewards and delegation system, see
 [Team18](#shelley-delegation-design).
 
-## Amount of Rewards to be Paid Out {#sec:rewards-amount}
-[Amount of Rewards to be Paid Out]: #sec:rewards-amount
+## Amount of Rewards to be Paid Out {#sec:amount-of-rewards-to-be-paid-out}
 
 ### Precision of Arithmetic Operations {#sec:precision-rewards}
 
@@ -646,11 +645,11 @@ opaque
         mapWithKey (λ c rewardBalance → utxoBalance c + rewardBalance) activeRewards
 ```
 
-## Timing of Rewards Payout {#sec:rewards-time}
+## Timing of Rewards Payout {#sec:timing-of-rewards-payout}
 
-### Rewards Calculation Timeline {#sec:rewards-timeline}
+### Rewards Calculation Timeline {#sec:rewards-calculation-timeline}
 
-As described in the [Rewards Motivation](#sec:rewards-motivation) section, the probability of
+As described in the [Rewards Motivation][] section, the probability of
 producing a block depends on the stake delegated to the block producer.  However, the
 stake distribution changes over time, as funds are transferred between parties.  This
 raises the question: What is the point in time from which we take the stake

src/Ledger/Conway/Specification/Transaction.lagda → src/Ledger/Conway/Specification/Transaction.lagda.md

@@ -1,11 +1,15 @@
-\section{Transactions}
-\label{sec:transactions}
-\modulenote{\ConwayModule{Transaction}}, where we define transactions.
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Transaction.lagda
+---
 
- A transaction consists of a transaction body, a collection of witnesses and some optional auxiliary
-data.
+# Transactions {#sec:transactions}
 
-\begin{code}[hide]
+A transaction consists of a transaction body, a collection of witnesses
+and some optional auxiliary data.
+
+<!--
+```agda
 {-# OPTIONS --safe #-}
 --------------------------------------------------------------------------------
 -- NOTE: Everything in this module is part of TransactionStructure
@@ -31,45 +35,49 @@ open import Relation.Nullary.Decidable using (⌊_⌋)
 data Tag : Type where
   Spend Mint Cert Rewrd Vote Propose : Tag
 unquoteDecl DecEq-Tag = derive-DecEq ((quote Tag , DecEq-Tag) ∷ [])
+```
+-->
+
+Here are some key components of the transaction body.
+
++  `txIns`{.AgdaField} denotes a set of transaction inputs; each input consists of a
+   transaction id and an index that points to a unique output from a previous transaction.
+
++  `txOuts`{.AgdaField} denotes an indexed collection of transaction outputs; each output
+   consists of an address and a coin value.
+
++  `txFee`{.AgdaField} denotes a transaction fee to be added to the fee pot.
+
++  `txId`{.AgdaField} denotes the hash of the serialized form of the
+   transaction---the form in which the transaction is included in a block.
+
+In addition to these, the Conway era introduces some new fields to the transaction body.
+
++  `txGovVotes`{.AgdaField} denotes the list of votes for governance actions.
+
++  `txGovProposals`{.AgdaField} denotes the list of governance proposals.
+
++  `txDonation`{.AgdaField} denotes the amount of `Coin`{.AgdaFunction} to donate to
+   treasury, e.g., to return funds to the treasury after a governance action.
+
++  `currentTreasury`{.AgdaField} denotes the current value of the treasury; this serves
+   as a precondition to executing Plutus scripts that access the value of the treasury.
+
+
+## Transaction Types
 
-\end{code}
-
-\begin{NoConway}
-Some key ingredients in the transaction body are:
-\begin{itemize}
-  \item A set \txIns{} of transaction inputs, each of which identifies an output from
-    a previous transaction.  A transaction input consists of a transaction id and an
-    index to uniquely identify the output.
-  \item An indexed collection \txOuts{} of transaction outputs.
-    The \TxOut{} type is an address paired with a coin value.
-  \item A transaction fee. This value will be added to the fee pot.
-  \item The hash \txid{} of the serialized form of the
-    transaction that was included in the block.
-\end{itemize}
-\end{NoConway}
-\begin{Conway}
-Ingredients of the transaction body introduced in the Conway era are the following:
-\begin{itemize}
-  \item \txvote{}, the list of votes for goverance actions;
-  \item \txprop{}, the list of governance proposals;
-  \item \txDonation{}, amount of \Coin{} to donate to treasury, e.g., to return money
-    to the treasury after a governance action;
-  \item \currentTreasury{}, the current value of the treasury. This field serves as a
-    precondition to executing Plutus scripts that access the value of the treasury.
-\end{itemize}
-\end{Conway}
-
-\begin{figure*}[ht]
-\begin{code}[hide]
+```agda
 record TransactionStructure : Type₁ where
   field
-\end{code}
-\emph{Abstract types}
-\begin{code}
+```
+
+*Abstract types*
+```agda
     Ix TxId AuxiliaryData : Type
+```
 
-\end{code}
-\begin{code}[hide]
+<!--
+```agda
     ⦃ DecEq-Ix   ⦄ : DecEq Ix
     ⦃ DecEq-TxId ⦄ : DecEq TxId
     adHashingScheme : isHashableSet AuxiliaryData
@@ -114,26 +122,29 @@ record TransactionStructure : Type₁ where
   open GovActions hiding (Vote; yes; no; abstain) public
 
   open import Ledger.Conway.Specification.Certs govStructure
-\end{code}
-\begin{NoConway}
-\emph{Derived types}
-\begin{code}
+```
+-->
+
+*Derived types*
+```agda
   TxIn               = TxId × Ix
   TxOut              = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script
   UTxO               = TxIn ⇀ TxOut
   RdmrPtr            = Tag × Ix
   ProposedPPUpdates  = KeyHash ⇀ PParamsUpdate
   Update             = ProposedPPUpdates × Epoch
-\end{code}
-\begin{code}[hide]
+```
+
+<!--
+```agda
   record HasUTxO {a} (A : Type a) : Type a where
     field UTxOOf : A → UTxO
   open HasUTxO ⦃...⦄ public
-\end{code}
-\end{NoConway}
-\emph{Transaction types}
-\begin{AgdaMultiCode}
-\begin{code}
+```
+-->
+
+*Transaction types*
+```agda
   record TxBody : Type where
     field
       txIns                : ℙ TxIn
@@ -155,8 +166,10 @@ record TransactionStructure : Type₁ where
       reqSignerHashes      : ℙ KeyHash
       scriptIntegrityHash  : Maybe ScriptHash
       -- txup              : Maybe Update   -- deprecated; leave for now
-\end{code}
-\begin{code}[hide]
+```
+
+<!--
+```agda
   record HasTxBody {a} (A : Type a) : Type a where
     field TxBodyOf : A → TxBody
   open HasTxBody  ⦃...⦄ public
@@ -176,10 +189,11 @@ record TransactionStructure : Type₁ where
   instance
     HasDonations-TxBody : HasDonations TxBody
     HasDonations-TxBody .DonationsOf = TxBody.txDonation
-\end{code}
+```
+-->
+
 
-\begin{NoConway}
-\begin{code}
+```agda
   record TxWitnesses : Type where
     field
       vkSigs   : VKey ⇀ Sig
@@ -197,8 +211,10 @@ record TransactionStructure : Type₁ where
       txsize   : ℕ
       isValid  : Bool
       txAD     : Maybe AuxiliaryData
-\end{code}
-\begin{code}[hide]
+```
+
+<!--
+```agda
   instance
     HasTxBody-Tx : HasTxBody Tx
     HasTxBody-Tx .TxBodyOf = Tx.body
@@ -223,17 +239,14 @@ record TransactionStructure : Type₁ where
 
     HasDonations-Tx : HasDonations Tx
     HasDonations-Tx .DonationsOf = DonationsOf ∘ TxBodyOf
-\end{code}
-\end{NoConway}
-\end{AgdaMultiCode}
-\caption{Transactions and related types}
-\label{fig:defs:transactions}
-\end{figure*}
-
-\begin{NoConway}
-\begin{figure*}[ht]
-\begin{AgdaMultiCode}
-\begin{code}
+```
+-->
+
+
+## Transaction Functions
+
+
+```agda
   getValue : TxOut → Value
   getValue (_ , v , _) = v
 
@@ -266,15 +279,13 @@ record TransactionStructure : Type₁ where
   lookupScriptHash : ScriptHash → Tx → UTxO → Maybe Script
   lookupScriptHash sh tx utxo = lookupᵐ? m sh
     where m = setToMap (mapˢ < hash , id > (txscripts tx utxo))
-\end{code}
-\end{AgdaMultiCode}
-\caption{Functions related to transactions}
-\label{fig:defs:transaction-funs}
-\end{figure*}
-\end{NoConway}
-
-\begin{code}[hide]
+```
+
+<!--
+```agda
   instance
     HasCoin-TxOut : HasCoin TxOut
     HasCoin-TxOut .getCoin = coin ∘ proj₁ ∘ proj₂
-\end{code}
+```
+-->
+