Generate code for GH-514

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,11 @@
+# Description
+
+<!-- Add your description here, if it fixes a particular issue please provide a
+[link](https://docs.github.com/en/issues/tracking-your-work-with-issues/linking-a-pull-request-to-an-issue#linking-a-pull-request-to-an-issue-using-a-keyword=)
+to the issue. -->
+
+# Checklist
+
+- [ ] Commit sequence broadly makes sense and commits have useful messages
+- [ ] Code is formatted according to [CONTRIBUTING.md](https://github.com/input-output-hk/formal-ledger-specifications/blob/master/CONTRIBUTING.md)
+- [ ] Self-reviewed the diff

.github/workflows/build.yml

@@ -0,0 +1,118 @@
+name: Formal Ledger Specs
+on:
+  push:
+    branches:
+    - master
+  pull_request:
+    branches:
+    - master
+
+permissions:
+  contents: write
+
+env:
+  MAlonzo_branch: ${{ github.event.pull_request.head.ref }}-MAlonzo
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: MAlonzo-code
+
+      - name: Create branch ${{ env.MAlonzo_branch }} for generated code
+        if: github.event_name == 'pull_request' && github.event.action == 'opened'
+        run: |
+          git checkout -b ${{ env.MAlonzo_branch }} origin/MAlonzo-code
+          git push origin ${{ env.MAlonzo_branch }}
+
+      - uses: actions/checkout@v4
+
+      - uses: cachix/install-nix-action@v20
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          extra_nix_config: |
+            trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+            substituters = https://cache.iog.io https://cache.nixos.org/
+
+      - name: Build formalLedger
+        id: formalLedger
+        run: |
+          mkdir -p outputs
+          nix-build -A formalLedger -j1 -o outputs/formalLedger
+          rsync -r --include={'**/*.time'} outputs/formalLedger*/* docs/
+
+      - name: Build ledger
+        id: ledger
+        run: |
+          nix-build -A ledger -j1 -o outputs/ledger
+          rsync -r --exclude={'**/nix-support','**/lib'} outputs/ledger*/* docs/
+
+      - name: Build midnight
+        id: midnight
+        run: |
+          nix-build -A midnight -j1 -o outputs/midnight
+          rsync -r --exclude={'**/nix-support','**/lib'} outputs/midnight*/* docs/
+
+      - name: Upload PDF artifacts
+        if: github.event_name == 'pull_request'
+        uses: actions/upload-artifact@v4
+        with:
+          name: PDF specs
+          path: docs/pdfs/*.pdf
+
+      - name: Upload typechecking times
+        if: github.event_name == 'pull_request'
+        uses: actions/upload-artifact@v4
+        with:
+          name: Typechecking durations
+          path: docs/*.time
+
+      - name: Generate main website
+        if: github.ref == 'refs/heads/master'
+        run: |
+          echo "** Generated PDF files:"; find -L docs/ -name '*.pdf'
+          echo "** Generated HTML files:"; find -L docs/ -name '*.html'
+          echo "** Generated Haskell files:"; find -L docs/ -name '*.hs'
+          OUT_DIR=../docs/ make staticWebsite
+
+      - name: Configure git
+        run: |
+          git config user.name 'github-actions[bot]'
+          git config user.email 'github-actions[bot]@users.noreply.github.com'
+
+      - name: Add files
+        if: github.ref == 'refs/heads/master'
+        run: |
+            git add -f docs/
+            git commit -m "Updated for ${{ github.sha }}"
+
+      - name: Push to gh-pages
+        if: github.ref == 'refs/heads/master'
+        uses: ad-m/[email protected]
+        with:
+            github_token: ${{ secrets.GITHUB_TOKEN }}
+            branch: gh-pages
+            force: true
+            directory: .
+
+      - name: Commit generated code at ${{ env.MAlonzo_branch }}
+        if: github.ref != 'refs/heads/master'
+        run: |
+            nix-build -A ledger.hsSrc -j1 -o outputs/MAlonzo
+            git stash push
+            git fetch origin ${{ env.MAlonzo_branch }} --depth 1
+            git checkout ${{ env.MAlonzo_branch }}
+            rsync -r --exclude={'**/nix-support','**/lib'} outputs/MAlonzo/haskell/Ledger/* generated/
+            git add -f generated && git commit -m "Generate code for ${{ github.sha }}" || echo "Everything is up-to-date."
+
+      - name: Push ${{ env.MAlonzo_branch }}
+        if: github.ref != 'refs/heads/master'
+        uses: ad-m/[email protected]
+        with:
+            github_token: ${{ secrets.GITHUB_TOKEN }}
+            branch: ${{ env.MAlonzo_branch }}
+            force: false
+            directory: .

.github/workflows/pr_merged.yml

@@ -0,0 +1,53 @@
+name: Formal Ledger Specs - PR Merged
+on:
+  pull_request:
+    branches:
+      - master
+    types:
+      - closed
+
+permissions:
+  contents: write
+
+env:
+  MAlonzo_branch: ${{ github.event.pull_request.head.ref }}-MAlonzo
+
+jobs:
+  pr-merged:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: MAlonzo-code
+      - name: Merge ${{ env.MAlonzo_branch }} into MAlonzo-code
+        if: github.event.pull_request.merged
+        run: |
+          git config user.name 'github-actions[bot]'
+          git config user.email 'github-actions[bot]@users.noreply.github.com'
+          # GitHub Actions fetches shallow copies of remote branches
+          # which might not be ideal when rebasing, hence use `--unshallow`.
+          git fetch --unshallow origin ${{ env.MAlonzo_branch }}
+          git checkout ${{ env.MAlonzo_branch }}
+          # During `git rebase` 'ours' and 'theirs' are flipped
+          # so what we do here is that we keep the changes from ${{ env.MAlonzo_branch }}.
+          git rebase -X theirs origin/MAlonzo-code
+          git checkout MAlonzo-code
+          git merge --squash ${{ env.MAlonzo_branch }}
+          git commit -m "Generate code for GH-${{ github.event.pull_request.number }}" || echo "Everything is up-to-date."
+
+      - name: Push MAlonzo-code
+        if: github.event.pull_request.merged
+        uses: ad-m/[email protected]
+        with:
+            github_token: ${{ secrets.GITHUB_TOKEN }}
+            branch: MAlonzo-code
+            force: false
+            directory: .
+
+      - name: Delete ${{ env.MAlonzo_branch }} branch
+        if: github.event.pull_request.merged
+        uses: dawidd6/action-delete-branch@v3
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          branches: ${{ env.MAlonzo_branch }}

CHANGELOG.md

@@ -0,0 +1,43 @@
+# Changelog
+
+## Conway spec
+
+### WIP
+
+- Rename `ccTermLimit` to `ccMaxTermLength`
+- Add `Vote` and `Propose` script purposes
+- Well-formed parameter updates can't be empty
+- Add reward withdrawal restriction
+- Add `pvCanFollow` check to `GOV` STS
+- Fix treasury withdrawals
+- Add `policy` field to `GovProposal`
+- Add `Voter` type and use it for `ScriptPurpose`
+- Add `minFeeRefScriptCoinsPerByte` protocol parameter
+- Add security-relevant parameters
+- Require reference inputs to be disjoint from regular inputs
+- Fix CC expiration not being considered for `ccMinSize` check
+- Replace `allEnactable` with `hasParent` in `GOV`
+- Add `curTreasury` field to transactions
+- Compute the voting stake distribution
+- Add deposit amount to `dereg` certificate
+
+### V0.9
+
+- Add proposal deposits
+- Add proposal policy (which would become the guardrails script)
+- Cold keys are now cold credentials
+- Fix: governance actions were removed immediately, now delayed by one epoch
+- Increment DRep activity in epochs where there was no GA to vote on
+- Only allow votes for GAs that actually apply
+- CC rejects every proposal when below `minCCSize`
+- Fix that `RATIFY` wasn't total
+- Properly implement treasury withdrawals
+- Remove unused hot credentials at the epoch boundary
+- Implement proper vote counting for SPOs
+- Fix some protocol parameter names
+- Check that `NewCommittee` actions are sensible when they are proposed
+- Fix: treasury withdrawals were included in the wrong map
+
+### V0.8
+
+First draft

CODE-OF-CONDUCT.md

@@ -0,0 +1 @@
+See the code of conduct in the [Cardano engineering handbook](https://github.com/input-output-hk/cardano-engineering-handbook/blob/main/CODE-OF-CONDUCT.md).

CODEOWNERS

@@ -0,0 +1 @@
+. @whatisRT

CONTRIBUTING.md

@@ -0,0 +1,113 @@
+# Contributing to the formal ledger specifications
+
+## Style guidelines
+
+We are currently aspiring to follow the [Agda standard library style guide][] as much as reasonable. Since some of our code will be rendered into a PDF, the formatting of the PDF takes priority over formatting of the code, so deviations are to be expected.
+
+We also have a separate style guide for formatting the PDF: [PDF style guide](PDF-style-guide.md).
+
+## Setup with emacs
+
+We use Agda version 2.6.4 and various dependencies. You can install the correct version of Agda and the dependencies using `nix-env -iA agda -f .`, but this is a global install which you may not want if you also have other Agda projects.
+
+To install Agda locally and use that install with emacs, you can do the following:
+
+-  Build `agda` and `agda-mode` binaries by invoking the following: `nix-build -A agdaWithDeps -o ~/IOHK/ledger-agda`. You can replace `~/IOHK/ledger-agda` with whatever path you like, just make sure to replace it in `my/agda-versions` below as well.
+
+   *Note*. You need not have built/installed Agda prior to invoking this `nix-build` command (though it's okay if you have).
+
+   *Note*. To instruct the `Makefile` to use this local Agda binary, invoke it like so: `AGDA=~/IOHK/ledger-agda make -C src/`
+
+-  Put the following into your init file (highlight and `M-x eval-region` to load it without restarting emacs).
+
+   ```
+   ;; Defines a function `my/switch-agda' that switches between different
+   ;; `agda' executables defined in `my/agda-versions'. The first entry of
+   ;; `my/agda-versions' is assumed to be the default Agda.
+   ;;
+   ;; If there are two entries in `my/agda-versions', `my/switch-agda' toggles
+   ;; between the two. If there are more entries, it will ask which one
+   ;; to choose.
+
+   (setq my/agda-versions `(("Agda"        "2.6.3" "agda")
+                            ("Ledger Agda" "2.6.4" "~/IOHK/ledger-agda/bin/agda")))
+
+   (setq my/selected-agda (caar my/agda-versions))
+
+   (defun my/switch-agda (name version path)
+     (interactive
+      (cond ((> (length my/agda-versions) 2)
+             (assoc (completing-read "Agda" my/agda-versions '(lambda (x) 't) 't) my/agda-versions))
+            ((= (length my/agda-versions) 2)
+             (car (seq-filter '(lambda (x) (not (string= my/selected-agda (car x)))) my/agda-versions)))
+            (t (error "my/agda-versions needs to have at least two elements!"))))
+     (message "Selecting %s, version %s" name version)
+     (setq my/selected-agda   name
+           agda2-version      version
+           agda2-program-name path)
+     (agda2-restart))
+
+   (with-eval-after-load 'agda2-mode (define-key agda2-mode-map (kbd "C-c C-x C-t") 'my/switch-agda))
+   ```
+
+   *Note*. This assumes that your regular install of Agda is in your path with the name `agda` and version `2.6.3`, otherwise you'll have to edit `my/agda-versions`.
+
+   You can then use `M-x my/toggle-ledger-agda`, or `C-c C-x C-t`, to switch between your regular install of Agda and the locally installed version.
+
+   There are other options as well, but this should work with all kinds of custom emacs setups or distributions (assuming there isn't already some other stuff going on with your Agda setup).
+
+
+## Setup with nix-shell
+
+`nix-shell` provides Agda complete with the correct dependencies. So you should be able to run your preferred editor within `nix-shell` and it should see the required `agda` executable.
+
+## Building the PDF quickly
+
+The Makefile can be used to build the PDF without having to build everything else. Either run `make` from within `nix-shell`, or use
+```
+nix-shell --command 'make docs'
+```
+to run `make` without launching an interactive shell.
+
+This combines well with the ability to invoke the TeX backend of Agda within Emacs,
+which is much faster when you have already loaded an Agda file/interface.
+
+## Building other artifacts
+
+Apart from the PDF specification, the `Makefile` can be used to also generate the following:
+- `make html`: generate HTML under `dist/html/`
+- `make hs`: generate Haskell code under `dist/MAlonzo/`
+- `make hsTest`: run the Haskell tests of each Agda formalisation
+- `make staticWebsite`: gather all resources above in a central webpage `dist/index.html`
+
+If you only want to command to affect a single project, prefix with `<project>.`, e.g.
+```
+$ make ledger.html
+$ make midnight.hs
+```
+
+## Updating nixpkgs
+
+To update the default nixpkgs used to build the derivations, run
+```
+niv update nixpkgs -r <revision>
+```
+
+or
+```
+niv update nixpkgs -v <version>
+```
+
+For example:
+```
+niv update nixpkgs -r 4e329926df7ee5fa49929a83d31ee7d541f8b45c
+niv update nixpkgs -v 21.11.337905.902d91def1e
+```
+
+## Maintainer
+
+This repository is maintained by @WhatisRT.
+
+
+[Agda]: https://wiki.portal.chalmers.se/agda/pmwiki.php
+[Agda standard library style guide]: https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md