Reference previous specifications & other material #659

williamdemeo · 2025-01-30T05:08:31Z

Description

This addresses #341.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

This addresses #341.

…r-material

include links to the Agda module for each section

williamdemeo · 2025-02-07T04:58:46Z

src/Ledger/GovernanceActions.lagda

-actionWellFormed _                  = ⊤
+actionWellFormed (ChangePParams x)  =  ppdWellFormed x
+actionWellFormed (TreasuryWdrl x)   =  ∀[ a ∈ dom x ] RwdAddr.net a ≡ NetworkId
+                                       × ∃[ v ∈ range x ] ¬ (v ≡ 0)


This PR is not aimed at making the code look nicer, but the small change here is more readable (and I won't remember to make a separate PR for it later).

williamdemeo · 2025-02-07T04:59:44Z

src/Ledger/Introduction.lagda

@@ -35,7 +38,7 @@ explanations may be missing or wrong.

 \begin{NoConway}
 \begin{center}
-Repository: \url{https://github.com/IntersectMBO/formal-ledger-specifications}
+Repository: \url{\repourl}


in case the repo url changes in future (again)

src/Ledger/Introduction.lagda

src/Ledger/Address.lagda

src/Ledger/PParams.lagda

williamdemeo · 2025-02-07T05:27:15Z

src/latex/Notation.tex

-
-module Ledger.Notation where
-\end{code}
-


It seems there's no reason for this to be an Agda module.

williamdemeo · 2025-02-07T05:29:28Z

src/latex/agda-latex-macros.sty

+%%       then we can just use, e.g., \LedgerURL{Chain} instead of requiring a special \LedgerChain macro.
+%%       Unfortunatley, I get a strange LaTeX error when I try the above.
+%%       (Maybe make this an issue later; not urgent enough to do now.)
+\newcommand{\LedgerLedger}{\href{https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Ledger.lagda}{\AgdaModule{Ledger.Ledger}}\xspace}


Making module names links to the module in our repo will make it easier for readers to find the source if they wish.

williamdemeo · 2025-02-07T05:34:31Z

Besides the changes I comment on above, changes to the references.bib file include pulling in refs from the bib files of previous eras, alphabetizing the file, and changing entry names so they share a common pattern.

src/Ledger/Address.lagda

carlostome · 2025-02-07T09:40:18Z

src/Ledger/Epoch.lagda

-system. Currently, this contains some logic that is handled by
-POOLREAP in the Shelley specification, since POOLREAP is not implemented here.
+system.  Currently, this contains some logic that is handled by
+POOLREAP in the Shelley specification~(\cite[Sec.~11.6]{shelley-ledger-spec}),


Not really a comment for this review, more like a rambling.

If we are going to continue using latex, it may make sense to switch to biblatex for citations (together with cleveref) so this would be written as:

POOLREAP in \textcite[\sectionname~11.6]{shelley-ledger-spec} ...

where

\NewDocumentCommand{\sectionname}{}{Section} \crefname{section}{\sectionname}{\sectionname{}s}

so "Section" is render uniformly across the document.

Nice. I like it.

Thanks for making a ticket (#681) for this (so I'll save such improvements for a later PR specifically aimed at addressing #681).

carlostome · 2025-02-07T09:42:05Z

src/Ledger/Introduction.lagda

@@ -35,7 +38,7 @@ explanations may be missing or wrong.

 \begin{NoConway}
 \begin{center}
-Repository: \url{https://github.com/IntersectMBO/formal-ledger-specifications}
+Repository: \url{\repourl}


src/Ledger/Introduction.lagda

carlostome · 2025-02-07T09:43:19Z

src/Ledger/Introduction.lagda

+\href{https://github.com/IntersectMBO/formal-ledger-specifications/issues}%
+     {open an issue} in
+\href{https://github.com/IntersectMBO/formal-ledger-specifications}%
+     {our GitHub repository} with the `notation' label.


Use \repourl here?

carlostome · 2025-02-07T09:44:23Z

src/Ledger/PParams.lagda

+there is no \SecurityGroup, but there is the concept of security-relevant
+protocol parameters~\cite{cip1694}.  The difference between these notions
+is only social, so we implement security-relevant protocol parameters as
+a group.


Is strange to use both \href to refer to a CIP and a citation. We should unify this.

Yeah, I'm not sure a link is necessary when there's a citation right next to it.

I don't think it's strange. I think it's nicer to have occurrences of "CIP-1694" link to the CIP, but also include the more conventional reference. Sometimes you want to navigate directly to the CIP from the page you're reading and sometimes you just want to look the bib metadata. These serve two different purposes.

But I do think it's a good idea to have a latex macro named \cip1694 to make it easier to be consistent whenever we refer to \cip1694.

Since TeX doesn't allow numbers in macro names, I've used the "leet speak" equivalents, so, for example, \citeIGgA in a tex or agda source file will be typeset as CIP-1694 with a hyperlink to the CIP.

I'm not particularly fond of leet speak, so if you have a better suggestion for naming the macros, please propose it.

I'd suggest in any case to use a command that gets as parameter the CIP not a command per CIP. For example,

\ExplSyntaxOn \NewDocumentCommand\hrefCIP{m}{% \clist_if_in:nnTF {0069,1694} {#1} {% \href{https://github.com/cardano-foundation/CIPs/tree/master/CIP-#1}{CIP-#1}% }{% \PackageError{agda-latex-macros}{CIP-#1~undefined.}{} }% } \ExplSyntaxOff

(It checks whether the arguments is in the list and gives an error otherwise)
It can be used as \hrefCIP{0069}, for instance.

carlostome · 2025-02-07T09:46:48Z

src/Ledger/Utxo.lagda

@@ -160,6 +160,9 @@ the state of the previous era at the transition into the Conway era.
 Alternatively, we can effectively treat the old handling of deposits
 as an erratum in the Shelley specification, which we fix by implementing
 the new deposits logic in older eras and then replaying the chain.
+(The handling of deposits in the Shelley era is discussed
+in~\cite[Sec.~8]{shelley-ledger-spec}
+and~\cite[Sec.~B.2]{shelley-delegation-design}.)


Another rambling. Using biblatex this would be:

\texcites[Sec.~8]{shelley-ledger-spec}[App.~B.2]{shelley-delegation-design}

Good note for the PR that addresses #681.

carlostome · 2025-02-07T09:48:08Z

src/latex/references.bib

You seem to have forgotten to change some references.

See https://github.com/IntersectMBO/formal-ledger-specifications/actions/runs/13193782129/job/36831348367?pr=659#step:4:12485

We should maybe agree on a standard for naming references.
I personally like the one used by dblp.

Great idea! I like dblp too. For reference, here's the bib entry for our paper about the spec.

WhatisRT

Just a few comments/typos here and there, but I think I agree with everything @carlostome said

src/Ledger/Introduction.lagda

WhatisRT · 2025-02-07T12:54:42Z

src/Ledger/PParams.lagda

+there is no \SecurityGroup, but there is the concept of security-relevant
+protocol parameters~\cite{cip1694}.  The difference between these notions
+is only social, so we implement security-relevant protocol parameters as
+a group.


Yeah, I'm not sure a link is necessary when there's a citation right next to it.

src/Ledger/Utxow.lagda

WhatisRT · 2025-02-07T13:01:35Z

src/Ledger/Utxow.lagda

 In original spec, however, the right-hand side (\txdatsHashes) could never
 contain \nothing, hence the left-hand side (\inputHashes) could never
 contain \nothing.
-
+% TODO: Say what "original spec" refers to?


I feel like we can just remove the word 'original'. It's just the Alonzo spec.

Okay, I'll remove the word "original" in front of "Alonzo." But in the next sentence, the word "original" is ambiguous. It says, "In the original spec, however,..." so presumably that's a reference to Shelley...?

In line 224, 'original spec' also refers to Alonzo. Shelley didn't have this line.

Okay, thanks. In that case, the "however" connective doesn't make sense. I'll rewrite the sentence.

Co-authored-by: Andre Knispel <[email protected]>

Reference previous specifications & other material

61d03e8

This addresses #341.

williamdemeo linked an issue Jan 30, 2025 that may be closed by this pull request

Reference previous specifications & other material #341

Open

add more refs

cfe8698

williamdemeo self-assigned this Jan 30, 2025

williamdemeo added 4 commits February 4, 2025 07:25

improvements

67db52e

Merge branch 'master' into 341-reference-previous-specifications-othe…

9394138

…r-material

Merge branch 'master' into 341-reference-previous-specifications-othe…

d76686e

…r-material

add more reference

11f495d

include links to the Agda module for each section

williamdemeo commented Feb 7, 2025

View reviewed changes

src/Ledger/Introduction.lagda Outdated Show resolved Hide resolved

williamdemeo commented Feb 7, 2025

View reviewed changes

src/Ledger/Address.lagda Outdated Show resolved Hide resolved

williamdemeo commented Feb 7, 2025

View reviewed changes

src/Ledger/PParams.lagda Show resolved Hide resolved

improvements

c93843c

williamdemeo force-pushed the 341-reference-previous-specifications-other-material branch from 6fa0196 to c93843c Compare February 7, 2025 05:24

williamdemeo commented Feb 7, 2025

View reviewed changes

williamdemeo marked this pull request as ready for review February 7, 2025 05:34

williamdemeo requested a review from carlostome February 7, 2025 05:35

carlostome reviewed Feb 7, 2025

View reviewed changes

WhatisRT reviewed Feb 7, 2025

View reviewed changes

williamdemeo and others added 5 commits February 7, 2025 13:37

address some of the PR change requests

ad1db20

Update src/Ledger/Introduction.lagda

798ef23

Co-authored-by: Andre Knispel <[email protected]>

Update src/Ledger/Utxow.lagda

a917f35

Co-authored-by: Andre Knispel <[email protected]>

address remaining change requests

24e6db8

add macros for consistent reference to cips

8213914

williamdemeo requested a review from carlostome February 7, 2025 23:33

carlostome added 2 commits February 10, 2025 15:00

Replace \Ledger* commands by a parameterised command \LedgerModule

d06d5eb

Remove comment and extra line

f123365

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Reference previous specifications & other material #659

Reference previous specifications & other material #659

williamdemeo commented Jan 30, 2025 •

edited

Loading

williamdemeo Feb 7, 2025 •

edited

Loading

williamdemeo Feb 7, 2025 •

edited

Loading

carlostome Feb 7, 2025

williamdemeo Feb 7, 2025

williamdemeo Feb 7, 2025

williamdemeo commented Feb 7, 2025

carlostome Feb 7, 2025

williamdemeo Feb 7, 2025

williamdemeo Feb 7, 2025

carlostome Feb 7, 2025

carlostome Feb 7, 2025

carlostome Feb 7, 2025

WhatisRT Feb 7, 2025

williamdemeo Feb 7, 2025 •

edited

Loading

williamdemeo Feb 7, 2025

carlostome Feb 10, 2025 •

edited

Loading

carlostome Feb 7, 2025

williamdemeo Feb 7, 2025

carlostome Feb 7, 2025

carlostome Feb 7, 2025 •

edited

Loading

williamdemeo Feb 7, 2025

WhatisRT left a comment

WhatisRT Feb 7, 2025

WhatisRT Feb 7, 2025

williamdemeo Feb 7, 2025

WhatisRT Feb 10, 2025

williamdemeo Feb 10, 2025

Reference previous specifications & other material #659

Are you sure you want to change the base?

Reference previous specifications & other material #659

Conversation

williamdemeo commented Jan 30, 2025 • edited Loading

Description

Checklist

williamdemeo Feb 7, 2025 • edited Loading

Choose a reason for hiding this comment

williamdemeo Feb 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

williamdemeo commented Feb 7, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

williamdemeo Feb 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

carlostome Feb 10, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

carlostome Feb 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

WhatisRT left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

williamdemeo commented Jan 30, 2025 •

edited

Loading

williamdemeo Feb 7, 2025 •

edited

Loading

williamdemeo Feb 7, 2025 •

edited

Loading

williamdemeo Feb 7, 2025 •

edited

Loading

carlostome Feb 10, 2025 •

edited

Loading

carlostome Feb 7, 2025 •

edited

Loading