From c30a055eaf0d9fb40dfdf0049927a8628470328c Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Fri, 20 Sep 2024 18:16:05 +0200 Subject: [PATCH] Add WIP simple Leios spec (#12) * Add WIP simple Leios spec * Added formal spec to Nix shell and CI (#13) * Added agda and dependencies to Nix developement shell. * Added Nix derivation for Leios spec. * Updated logbook. * Added caching of nix store, fixes #14. --------- Co-authored-by: Brian W Bush Co-authored-by: Brian W Bush --- .github/workflows/ci.yaml | 59 +++++ .gitignore | 1 + Logbook.md | 29 +++ flake.lock | 93 ++++---- flake.nix | 5 +- formal-spec/CategoricalCrypto.agda | 332 ++++++++++++++++++++++++++++ formal-spec/Leios/Network.agda | 71 ++++++ formal-spec/Leios/SimpleSpec.agda | 338 +++++++++++++++++++++++++++++ formal-spec/leios-spec.agda-lib | 8 + nix/agda.nix | 108 +++++++++ nix/outputs.nix | 9 +- nix/shell.nix | 57 +++-- 12 files changed, 1047 insertions(+), 63 deletions(-) create mode 100644 formal-spec/CategoricalCrypto.agda create mode 100644 formal-spec/Leios/Network.agda create mode 100644 formal-spec/Leios/SimpleSpec.agda create mode 100644 formal-spec/leios-spec.agda-lib create mode 100644 nix/agda.nix diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 7eb06e4..0bf2f2e 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -13,12 +13,52 @@ on: - main jobs: + typecheck: + name: Typecheck specification + runs-on: ubuntu-22.04 + steps: + - name: 📥 Checkout repository + uses: actions/checkout@v4 + - name: 💾 Cache Nix store + uses: actions/cache@v3.0.8 + id: nix-cache + with: + path: /tmp/nixcache + key: ${{ runner.os }}-nix-typecheck-${{ hashFiles('flake.lock') }} + restore-keys: ${{ runner.os }}-nix-typecheck- + - name: 🛠️ Install Nix + uses: cachix/install-nix-action@v21 + with: + nix_path: nixpkgs=channel:nixos-unstable + install_url: https://releases.nixos.org/nix/nix-2.10.3/install + extra_nix_config: | + allowed-uris = ${{ env.ALLOWED_URIS }} + trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }} + substituters = ${{ env.SUBSTITUTERS }} + experimental-features = nix-command flakes + - name: 💾➤ Import Nix store cache + if: "steps.nix-cache.outputs.cache-hit == 'true'" + run: "nix-store --import < /tmp/nixcache" + - name: 🏗️ Build specification + run: | + nix build --show-trace --accept-flake-config .#leiosSpec + - name: ➤💾 Export Nix store cache + if: "steps.nix-cache.outputs.cache-hit != 'true'" + run: "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > /tmp/nixcache" + compile: name: Build libraries runs-on: ubuntu-22.04 steps: - name: 📥 Checkout repository uses: actions/checkout@v4 + - name: 💾 Cache Nix store + uses: actions/cache@v3.0.8 + id: nix-cache + with: + path: /tmp/nixcache + key: ${{ runner.os }}-nix-compile-${{ hashFiles('flake.lock') }} + restore-keys: ${{ runner.os }}-nix-compile- - name: 🛠️ Install Nix uses: cachix/install-nix-action@v21 with: @@ -29,12 +69,18 @@ jobs: trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }} substituters = ${{ env.SUBSTITUTERS }} experimental-features = nix-command flakes + - name: 💾➤ Import Nix store cache + if: "steps.nix-cache.outputs.cache-hit == 'true'" + run: "nix-store --import < /tmp/nixcache" - name: 🏗️ Build `exe:leios` run: | nix build --show-trace --accept-flake-config .#leios - name: 🏗️ Build `exe:ouroboros-net-vis` run: | nix build --show-trace --accept-flake-config .#ouroboros-net-vis + - name: ➤💾 Export Nix store cache + if: "steps.nix-cache.outputs.cache-hit != 'true'" + run: "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > /tmp/nixcache" tests: if: true @@ -43,6 +89,13 @@ jobs: steps: - name: 📥 Checkout repository uses: actions/checkout@v4 + - name: 💾 Cache Nix store + uses: actions/cache@v3.0.8 + id: nix-cache + with: + path: /tmp/nixcache + key: ${{ runner.os }}-nix-tests-${{ hashFiles('flake.lock') }} + restore-keys: ${{ runner.os }}-nix-tests- - name: 🛠️ Install Nix uses: cachix/install-nix-action@v21 with: @@ -53,9 +106,15 @@ jobs: trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }} substituters = ${{ env.SUBSTITUTERS }} experimental-features = nix-command flakes + - name: 💾➤ Import Nix store cache + if: "steps.nix-cache.outputs.cache-hit == 'true'" + run: "nix-store --import < /tmp/nixcache" - name: 🔬 Test with `leios-sim-test` run: | nix run --accept-flake-config .#leios-sim-test + - name: ➤💾 Export Nix store cache + if: "steps.nix-cache.outputs.cache-hit != 'true'" + run: "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > /tmp/nixcache" build-docusaurus: runs-on: ubuntu-22.04 diff --git a/.gitignore b/.gitignore index 65350d7..7f660a6 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ dist-newstyle/ \#* .\#* .pre-commit-config.yaml +_build \ No newline at end of file diff --git a/Logbook.md b/Logbook.md index 6c5ee78..62ba5f1 100644 --- a/Logbook.md +++ b/Logbook.md @@ -1,3 +1,5 @@ +# Leios logbook + ## 2024-09-20 ### Team meeting @@ -64,6 +66,33 @@ - Live version of `leios-sim` at https://leios-simulation.cardano-scaling.org/index.html - Run `simulation` locally via [instructions below](#running-ouroborous-net-viz-in-the-browser) +## 2024-08-30 + +### Nix and CI support for Leios specification + +The Nix flake now builds the Leios specification and the libraries upon which it depends. The type checking of the spec is now added to the CI. + +```console +$ nix develop + +Welcome to Ouroboros Leios! + +Locations of Agda libraries: + /nix/store/1yxiwwy44xxxgzdmvyjizq53w9cfinkn-standard-library-2.0/standard-library.agda-lib + /nix/store/ppsczpm7l2gx1zd3cx2brv49069krzzh-agda-stdlib-classes-2.0/standard-library-classes.agda-lib + /nix/store/gkci6kgv4v9qw2rh5gc0s26g53b253jy-agda-stdlib-meta-2.0/standard-library-meta.agda-lib + /nix/store/2gk6rvsplxww4i8dnflxbd319lfxdcvv-formal-ledger-1d77a35a/formal-ledger.agda-lib + +Run 'emacs' to edit .agda files. + + +Type 'info' to see what's inside this shell. + +$ cd formal-spec + +$ emacs Leios/SimpleSpec.agda +``` + ## 2024-07-26 ### Running `ouroborous-net-viz` in the browser diff --git a/flake.lock b/flake.lock index 7536de2..81f3cfd 100644 --- a/flake.lock +++ b/flake.lock @@ -3,11 +3,11 @@ "CHaP": { "flake": false, "locked": { - "lastModified": 1720157709, - "narHash": "sha256-9GZS2x9ZcaMncOAdVtHi+bXIi3amdOOgGCFjRZuO9sw=", + "lastModified": 1724604182, + "narHash": "sha256-gQmj2hHwEvS29Gf+juG95T7Qt5LfzDJKzdPajcuHZgs=", "owner": "input-output-hk", "repo": "cardano-haskell-packages", - "rev": "2bfd58f7293b0c66eafeab9b905ba5e680aeab41", + "rev": "3a25be01c845e86092e514403882ac74141ac3da", "type": "github" }, "original": { @@ -279,11 +279,11 @@ "hackage": { "flake": false, "locked": { - "lastModified": 1720139837, - "narHash": "sha256-sHzBEROaMR3fpBcajRh44FiaQf8F5+frPfgUMmslUkQ=", + "lastModified": 1724632371, + "narHash": "sha256-8MKEmQeJ4ft4PEcU85sCr+DqTc7wpLLV3Wt8jC9PZ+Q=", "owner": "input-output-hk", "repo": "hackage.nix", - "rev": "b7a8cc3e5e94cd79ac8b52e46f85b4279e4d6c33", + "rev": "28717c62d061f1936eb96b4c5814b7df0c31fa0d", "type": "github" }, "original": { @@ -330,16 +330,17 @@ "nixpkgs-2211": "nixpkgs-2211", "nixpkgs-2305": "nixpkgs-2305", "nixpkgs-2311": "nixpkgs-2311", + "nixpkgs-2405": "nixpkgs-2405", "nixpkgs-unstable": "nixpkgs-unstable", "old-ghc-nix": "old-ghc-nix", "stackage": "stackage" }, "locked": { - "lastModified": 1720140618, - "narHash": "sha256-NUOHsXOoB+JBopuQpTTfn0zGfbfg49i3f5VlQIU0ATQ=", + "lastModified": 1724633441, + "narHash": "sha256-jPVqNPQabeEIGUxyCMyOmer3JwSdHdleGGLwydrPvf0=", "owner": "input-output-hk", "repo": "haskell.nix", - "rev": "eb6200ccc683803154f8d8226a12f26857275f2e", + "rev": "00ca0e2522e2ec124bf4ed5285685e524fbe38ee", "type": "github" }, "original": { @@ -578,11 +579,11 @@ "sphinxcontrib-haddock": "sphinxcontrib-haddock" }, "locked": { - "lastModified": 1720207747, - "narHash": "sha256-ISZAoaeRMrTYmhkH96w2Ua/5SsVY+ja2MpW0ZKkHbWo=", + "lastModified": 1724699322, + "narHash": "sha256-H+d9HhoKZ7yItB4DqWxTEN+P5xtBnrNTYi3hXMakjzI=", "owner": "input-output-hk", "repo": "iogx", - "rev": "a6ad5dc3a956cb17b0cbee308d5b1788eb42f431", + "rev": "9720ba9bcaf738f65fbc530e427caea7bcc0d7d1", "type": "github" }, "original": { @@ -602,11 +603,11 @@ "sodium": "sodium" }, "locked": { - "lastModified": 1719443312, - "narHash": "sha256-JNDuUSmV/o5ck1CfnBtX8GJE/Pli4zYE73LZZ7u0E2Q=", + "lastModified": 1721825987, + "narHash": "sha256-PPcma4tjozwXJAWf+YtHUQUulmxwulVlwSQzKItx/n8=", "owner": "input-output-hk", "repo": "iohk-nix", - "rev": "b4025c38b609c6fb99762e2a6201e4e3488a39d3", + "rev": "eb61f2c14e1f610ec59117ad40f8690cddbf80cb", "type": "github" }, "original": { @@ -675,11 +676,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1712990762, - "narHash": "sha256-hO9W3w7NcnYeX8u8cleHiSpK2YJo7ecarFTUlbybl7k=", + "lastModified": 1720642556, + "narHash": "sha256-qsnqk13UmREKmRT7c8hEnz26X3GFFyIQrqx4EaRc1Is=", "owner": "nlewo", "repo": "nix2container", - "rev": "20aad300c925639d5d6cbe30013c8357ce9f2a2e", + "rev": "3853e5caf9ad24103b13aa6e0e8bcebb47649fe4", "type": "github" }, "original": { @@ -786,11 +787,11 @@ }, "nixpkgs-2305": { "locked": { - "lastModified": 1701362232, - "narHash": "sha256-GVdzxL0lhEadqs3hfRLuj+L1OJFGiL/L7gCcelgBlsw=", + "lastModified": 1705033721, + "narHash": "sha256-K5eJHmL1/kev6WuqyqqbS1cdNnSidIZ3jeqJ7GbrYnQ=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "d2332963662edffacfddfad59ff4f709dde80ffe", + "rev": "a1982c92d8980a0114372973cbdfe0a307f1bdea", "type": "github" }, "original": { @@ -802,11 +803,11 @@ }, "nixpkgs-2311": { "locked": { - "lastModified": 1701386440, - "narHash": "sha256-xI0uQ9E7JbmEy/v8kR9ZQan6389rHug+zOtZeZFiDJk=", + "lastModified": 1719957072, + "narHash": "sha256-gvFhEf5nszouwLAkT9nWsDzocUTqLWHuL++dvNjMp9I=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "293822e55ec1872f715a66d0eda9e592dc14419f", + "rev": "7144d6241f02d171d25fba3edeaf15e0f2592105", "type": "github" }, "original": { @@ -816,6 +817,22 @@ "type": "github" } }, + "nixpkgs-2405": { + "locked": { + "lastModified": 1720122915, + "narHash": "sha256-Nby8WWxj0elBu1xuRaUcRjPi/rU3xVbkAt2kj4QwX2U=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "835cf2d3f37989c5db6585a28de967a667a75fb1", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-24.05-darwin", + "repo": "nixpkgs", + "type": "github" + } + }, "nixpkgs-regression": { "locked": { "lastModified": 1643052045, @@ -850,33 +867,33 @@ }, "nixpkgs-stable_2": { "locked": { - "lastModified": 1718811006, - "narHash": "sha256-0Y8IrGhRmBmT7HHXlxxepg2t8j1X90++qRN3lukGaIk=", + "lastModified": 1720386169, + "narHash": "sha256-NGKVY4PjzwAa4upkGtAMz1npHGoRzWotlSnVlqI40mo=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "03d771e513ce90147b65fe922d87d3a0356fc125", + "rev": "194846768975b7ad2c4988bdb82572c00222c0d7", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixos-23.11", + "ref": "nixos-24.05", "repo": "nixpkgs", "type": "github" } }, "nixpkgs-unstable": { "locked": { - "lastModified": 1694822471, - "narHash": "sha256-6fSDCj++lZVMZlyqOe9SIOL8tYSBz1bI8acwovRwoX8=", + "lastModified": 1720181791, + "narHash": "sha256-i4vJL12/AdyuQuviMMd1Hk2tsGt02hDNhA0Zj1m16N8=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "47585496bcb13fb72e4a90daeea2f434e2501998", + "rev": "4284c2b73c8bce4b46a6adf23e16d9e2ec8da4bb", "type": "github" }, "original": { "owner": "NixOS", + "ref": "nixpkgs-unstable", "repo": "nixpkgs", - "rev": "47585496bcb13fb72e4a90daeea2f434e2501998", "type": "github" } }, @@ -936,11 +953,11 @@ "nixpkgs-stable": "nixpkgs-stable_2" }, "locked": { - "lastModified": 1719259945, - "narHash": "sha256-F1h+XIsGKT9TkGO3omxDLEb/9jOOsI6NnzsXFsZhry4=", + "lastModified": 1724440431, + "narHash": "sha256-9etXEOUtzeMgqg1u0wp+EdwG7RpmrAZ2yX516bMj2aE=", "owner": "cachix", "repo": "pre-commit-hooks.nix", - "rev": "0ff4381bbb8f7a52ca4a851660fc7a437a4c6e07", + "rev": "c8a54057aae480c56e28ef3e14e4960628ac495b", "type": "github" }, "original": { @@ -1007,11 +1024,11 @@ "stackage": { "flake": false, "locked": { - "lastModified": 1720138986, - "narHash": "sha256-+A0QV5ttTNRhlLD/o2l8VjVYE6Xk3X+I2r9b9mlrgw8=", + "lastModified": 1724631220, + "narHash": "sha256-aXkNOrKlGKFO4BfPMo28Br0+A5arKJYCZvbAyj0d3Yk=", "owner": "input-output-hk", "repo": "stackage.nix", - "rev": "0cfa5e0a9804966c8feb8227d57149348ff79f2c", + "rev": "73edb7f9d4b83b19246ab92592e0e7699faddcd9", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 9bfdc66..fbc2c3f 100644 --- a/flake.nix +++ b/flake.nix @@ -6,10 +6,6 @@ inputs = { iogx = { url = "github:input-output-hk/iogx"; - # inputs.hackage.follows = "hackage"; - # inputs.CHaP.follows = "CHaP"; - # inputs.haskell-nix.follows = "haskell-nix"; - # inputs.nixpkgs.follows = "nixpkgs"; }; # nixpkgs.follows = "haskell-nix/nixpkgs"; @@ -28,6 +24,7 @@ # url = "github:input-output-hk/haskell.nix"; # inputs.hackage.follows = "hackage"; # }; + }; diff --git a/formal-spec/CategoricalCrypto.agda b/formal-spec/CategoricalCrypto.agda new file mode 100644 index 0000000..40c68b2 --- /dev/null +++ b/formal-spec/CategoricalCrypto.agda @@ -0,0 +1,332 @@ +module CategoricalCrypto where + +open import Prelude hiding (id; _∘_; _⊗_; lookup; Dec) + +-------------------------------------------------------------------------------- +-- Channels, which form the objects + +record Channel : Set₁ where + field P : Set + rcvType sndType : P → Set + +infixr 9 _⊗_ + +I : Channel +I .Channel.P = ⊥ + +_ᵀ : Channel → Channel +_ᵀ c = let open Channel c in λ where .P → P ; .rcvType → sndType ; .sndType → rcvType + +_⊗_ : Channel → Channel → Channel +c₁ ⊗ c₂ = let open Channel c₁ renaming (P to P₁; rcvType to rcvType₁; sndType to sndType₁) + open Channel c₂ renaming (P to P₂; rcvType to rcvType₂; sndType to sndType₂) + open Channel + in λ where + .P → P₁ ⊎ P₂ + .rcvType (inj₁ a) → rcvType₁ a + .rcvType (inj₂ b) → rcvType₂ b + .sndType (inj₁ a) → sndType₁ a + .sndType (inj₂ b) → sndType₂ b + +snd₁ : ∀ {A B} → ∃ (Channel.sndType A) → ∃ (Channel.sndType (A ⊗ B)) +snd₁ (p , m) = inj₁ p , m + +snd₂ : ∀ {A B} → ∃ (Channel.sndType B) → ∃ (Channel.sndType (A ⊗ B)) +snd₂ (p , m) = inj₂ p , m + +-- being lazy here, this should be an iso instead +postulate + ⊗-assoc : ∀ {A B C} → (A ⊗ B) ⊗ C ≡ A ⊗ (B ⊗ C) + +-------------------------------------------------------------------------------- +-- Machines, which form the morphisms + +record Machine (A B : Channel) : Set₁ where + constructor MkMachine + open Channel (A ⊗ B ᵀ) public + + field State : Set + stepRel : ∃ rcvType → State → State × Maybe (∃ sndType) → Set + +module _ {A B} (let open Channel (A ⊗ B ᵀ)) where + MkMachine' : ∀ {State} → (∃ rcvType → State → State × Maybe (∃ sndType) → Set) → Machine A B + MkMachine' = MkMachine _ + + StatelessMachine : (∃ rcvType → Maybe (∃ sndType) → Set) → Machine A B + StatelessMachine R = MkMachine ⊤ (λ i _ (_ , o) → R i o) + + FunctionMachine : (∃ rcvType → Maybe (∃ sndType)) → Machine A B + FunctionMachine f = StatelessMachine (λ i o → f i ≡ o) + +id : ∀ {A} → Machine A A +id .Machine.State = ⊤ +id .Machine.stepRel (inj₁ a , m) _ (_ , m') = m' ≡ just (inj₂ a , m) +id .Machine.stepRel (inj₂ a , m) _ (_ , m') = m' ≡ just (inj₁ a , m) + +module Tensor {A B C D} (M₁ : Machine A B) (M₂ : Machine C D) where + open Machine M₁ renaming (State to State₁; stepRel to stepRel₁) + open Machine M₂ renaming (State to State₂; stepRel to stepRel₂) + + State = State₁ × State₂ + + AllCs = (A ⊗ B ᵀ) ⊗ (C ⊗ D ᵀ) + + data CompRel : ∃ (Channel.rcvType AllCs) → State → State × Maybe (∃ (Channel.sndType AllCs)) → Set where + Step₁ : ∀ {p m m' s s' s₂} → stepRel₁ (p , m) s (s' , m') + → CompRel (inj₁ p , m) (s , s₂) ((s' , s₂) , (snd₁ <$> m')) + + Step₂ : ∀ {p m m' s s' s₁} → stepRel₂ (p , m) s (s' , m') + → CompRel (inj₂ p , m) (s₁ , s) ((s₁ , s') , (snd₂ <$> m')) + + + _⊗'_ : Machine (A ⊗ C) (B ⊗ D) + _⊗'_ = λ where + .Machine.State → State + .Machine.stepRel m s (s' , m') → CompRel + (case m of λ where + (inj₁ (inj₁ p) , m) → (inj₁ (inj₁ p) , m) + (inj₁ (inj₂ p) , m) → (inj₂ (inj₁ p) , m) + (inj₂ (inj₁ p) , m) → (inj₁ (inj₂ p) , m) + (inj₂ (inj₂ p) , m) → (inj₂ (inj₂ p) , m)) + s + (s' , ((λ where + (inj₁ (inj₁ p) , m) → (inj₁ (inj₁ p) , m) + (inj₁ (inj₂ p) , m) → (inj₂ (inj₁ p) , m) + (inj₂ (inj₁ p) , m) → (inj₁ (inj₂ p) , m) + (inj₂ (inj₂ p) , m) → (inj₂ (inj₂ p) , m)) <$> m')) + +open Tensor using (_⊗'_) public + +_⊗ˡ_ : ∀ {A B} → (C : Channel) → Machine A B → Machine (C ⊗ A) (C ⊗ B) +C ⊗ˡ M = id ⊗' M + +_⊗ʳ_ : ∀ {A B} → Machine A B → (C : Channel) → Machine (A ⊗ C) (B ⊗ C) +M ⊗ʳ C = M ⊗' id + +module Comp {A B C} (M₁ : Machine B C) (M₂ : Machine A B) where + open Machine M₁ renaming (State to State₁; stepRel to stepRel₁) + open Machine M₂ renaming (State to State₂; stepRel to stepRel₂) + + State = State₁ × State₂ + + AllCs = (A ⊗ B ᵀ) ⊗ (B ⊗ C ᵀ) + + data CompRel : ∃ (Channel.rcvType AllCs) → State → State × Maybe (∃ (Channel.sndType AllCs)) → Set where + Step₁ : ∀ {p m m' s s' s₂} → stepRel₁ (p , m) s (s' , m') + → CompRel (inj₂ p , m) (s , s₂) ((s' , s₂) , (snd₂ <$> m')) + + Step₂ : ∀ {p m m' s s' s₁} → stepRel₂ (p , m) s (s' , m') + → CompRel (inj₁ p , m) (s₁ , s) ((s₁ , s') , (snd₁ <$> m')) + + Multi₁ : ∀ {p m m' m'' s s' s''} + → CompRel m s (s' , just ((inj₂ (inj₁ p) , m'))) + → CompRel (inj₁ (inj₂ p) , m') s' (s'' , m'') + → CompRel m s (s'' , m'') + + Multi₂ : ∀ {p m m' m'' s s' s''} + → CompRel m s (s' , just (inj₁ (inj₂ p) , m')) + → CompRel (inj₂ (inj₁ p) , m') s' (s'' , m'') + → CompRel m s (s'' , m'') + + infixr 9 _∘_ + + _∘_ : Machine A C + _∘_ = λ where + .Machine.State → State + .Machine.stepRel m s (s' , m') → + CompRel + (case m of λ where (inj₁ x , m) → inj₁ (inj₁ x) , m ; (inj₂ y , m) → inj₂ (inj₂ y) , m) + s (s' , ((λ where (inj₁ x , m) → inj₁ (inj₁ x) , m ; (inj₂ y , m) → inj₂ (inj₂ y) , m) <$> m')) + +open Comp using (_∘_) public + +-------------------------------------------------------------------------------- +-- Environment model + +ℰ-Out : Channel +ℰ-Out .Channel.P = ⊤ +ℰ-Out .Channel.sndType _ = Bool +ℰ-Out .Channel.rcvType _ = ⊥ + +-- Presheaf on the category of channels & machines +-- we just take machines that output a boolean +-- for now, not on the Kleisli construction +ℰ : Channel → Set₁ +ℰ C = Machine C ℰ-Out + +map-ℰ : ∀ {A B} → Machine A B → ℰ B → ℰ A +map-ℰ M E = E ∘ M + +-------------------------------------------------------------------------------- +-- UC relations + +-- perfect equivalence +_≈ℰ_ : ∀ {A B} → Machine A B → Machine A B → Set₁ +_≈ℰ_ {B = B} M M' = (E : ℰ B) → map-ℰ M E ≡ map-ℰ M' E + +_≤UC_ : ∀ {A B E E''} → Machine A (B ⊗ E) → Machine A (B ⊗ E'') → Set₁ +_≤UC_ {B = B} {E} R I = ∀ E' (A : Machine E E') → ∃[ S ] ((B ⊗ˡ A) ∘ R) ≈ℰ ((B ⊗ˡ S) ∘ I) + +-- equivalent to _≤UC_ by "completeness of the dummy adversary" +_≤'UC_ : ∀ {A B E} → Machine A (B ⊗ E) → Machine A (B ⊗ E) → Set₁ +_≤'UC_ {B = B} R I = ∃[ S ] R ≈ℰ (B ⊗ˡ S ∘ I) + + +-------------------------------------------------------------------------------- +-- Example functionalities + +module LeakyChannel (M : Set) where + -- authenticated, non-lossy, leaks all messages + + open Channel + + A B E : Channel + + -- can receive messages from Alice (in reverse) + A .P = ⊤ + A .sndType _ = M + A .rcvType _ = ⊥ + + -- can send messages to Bob (in reverse) + B .P = ⊤ + B .sndType _ = ⊥ + B .rcvType _ = M + + -- upon request, can send next message to Eve (in reverse) + E .P = ⊤ + E .sndType _ = ⊤ + E .rcvType _ = M + + open Machine hiding (rcvType; sndType) + + data R : ∃ (rcvType (I ⊗ (A ⊗ B ⊗ E) ᵀ)) + → List M + → List M × Maybe (∃ (sndType (I ⊗ (A ⊗ B ⊗ E) ᵀ))) → Set where + + Send : ∀ {m s} → R (inj₂ (inj₁ _) , m) s (s ∷ʳ m , just (inj₂ (inj₂ (inj₁ _)) , m)) + Req : ∀ {m s} → R (inj₂ (inj₂ (inj₂ _)) , _) (m ∷ s) (s , just (inj₂ (inj₂ (inj₂ _)) , m)) + + Functionality : Machine I (A ⊗ B ⊗ E) + Functionality .State = List M -- queue of messages + Functionality .stepRel = R + + + +module SecureChannel (M : Set) where + -- authenticated, non-lossy, leaks only message length + + open Channel + + A B E : Channel + + -- can receive messages from Alice (in reverse) + A .P = ⊤ + A .sndType _ = M + A .rcvType _ = ⊥ + + -- can send messages to Bob (in reverse) + B .P = ⊤ + B .sndType _ = ⊥ + B .rcvType _ = M + + -- upon request, can send length of the next message to Eve (in reverse) + E .P = ⊤ + E .sndType _ = ⊤ + E .rcvType _ = ℕ + + module _ (msgLen : M → ℕ) where + + open Machine hiding (rcvType; sndType) + + data R : ∃ (rcvType (I ⊗ (A ⊗ B ⊗ E) ᵀ)) + → List M + → List M × Maybe (∃ (sndType (I ⊗ (A ⊗ B ⊗ E) ᵀ))) → Set where + Send : ∀ {m s} → R (inj₂ (inj₁ _) , m) s (s ∷ʳ m , just (inj₂ (inj₂ (inj₁ _)) , m)) + Req : ∀ {m s} → R (inj₂ (inj₂ (inj₂ _)) , _) (m ∷ s) (s , just (inj₂ (inj₂ (inj₂ _)) , msgLen m)) + + Functionality : Machine I (A ⊗ B ⊗ E) + Functionality .State = List M -- queue of messages + Functionality .stepRel = R + + Functionality' : Machine I ((A ⊗ B) ⊗ E) + Functionality' = subst (Machine I) (sym ⊗-assoc) Functionality + + + +module Encryption (PlainText CipherText PubKey PrivKey : Set) + ⦃ _ : DecEq CipherText ⦄ ⦃ _ : DecEq PubKey ⦄ + (genCT : ℕ → CipherText) (getPubKey : PrivKey → PubKey) where + open Channel + open Machine hiding (rcvType; sndType) + + C : Channel + C .P = ⊤ + C .sndType _ = PlainText × PubKey ⊎ CipherText × PrivKey + C .rcvType _ = CipherText ⊎ Maybe PlainText + + S : Set + S = List (PubKey × PlainText × CipherText) + + lookup : {A : Set} → List A → (A → Bool) → Maybe A + lookup [] f = nothing + lookup (x ∷ l) f with f x + ... | true = just x + ... | false = lookup l f + + lookupPlainText : S → CipherText × PubKey → Maybe PlainText + lookupPlainText s (c , k) = proj₁ <$> (proj₂ <$> lookup s λ where (k' , _ , c') → ¿ k ≡ k' × c ≡ c' ¿ᵇ) + + data R : ∃ (rcvType (I ⊗ (C ᵀ))) → S → S × Maybe (∃ (sndType (I ⊗ (C ᵀ)))) → Set where + Enc : ∀ {p k s} → let c = genCT (length s) + in R (inj₂ tt , inj₁ (p , k)) s ((k , p , c) ∷ s , just (inj₂ tt , inj₁ c)) + Dec : ∀ {c k s} → let p = lookupPlainText s (c , getPubKey k) + in R (inj₂ tt , inj₂ (c , k)) s (s , just (inj₂ tt , inj₂ p)) + + Functionality : Machine I C + Functionality .State = S + Functionality .stepRel = R + +module EncryptionShim (PlainText CipherText PubKey PrivKey : Set) + ⦃ _ : DecEq CipherText ⦄ ⦃ _ : DecEq PubKey ⦄ + (genCT : ℕ → CipherText) (getPubKey : PrivKey → PubKey) + (pubKey : PubKey) (privKey : PrivKey) where + open Channel + open Machine hiding (rcvType; sndType) + + module L = LeakyChannel CipherText + module S = SecureChannel PlainText + module E = Encryption PlainText CipherText PubKey PrivKey genCT getPubKey + + data R : ∃ (rcvType ((L.A ⊗ L.B ⊗ L.E) ⊗ ((S.A ⊗ S.B ⊗ S.E) ᵀ))) + → E.Functionality .State + → E.Functionality .State × Maybe (∃ (sndType ((L.A ⊗ L.B ⊗ L.E) ⊗ ((S.A ⊗ S.B ⊗ S.E) ᵀ)))) + → Set where + EncSend : ∀ {m m' s s'} + → E.R (inj₂ _ , inj₁ (m , pubKey)) s (s' , just (inj₂ _ , inj₁ m')) + → R (inj₂ (inj₁ _) , m) s (s' , just (inj₁ (inj₁ _) , m')) + DecRcv : ∀ {m m' s s'} + → E.R (inj₂ _ , inj₂ (m , privKey)) s (s' , just (inj₂ _ , inj₂ (just m'))) + → R (inj₁ (inj₂ (inj₁ _)) , m) s (s' , just (inj₂ (inj₂ (inj₁ _)) , m')) + + Functionality : Machine (L.A ⊗ L.B ⊗ L.E) (S.A ⊗ S.B ⊗ S.E) + Functionality .State = E.Functionality .State + Functionality .stepRel = R + +module SecureFromAuthenticated (PlainText CipherText PubKey PrivKey : Set) + ⦃ _ : DecEq CipherText ⦄ ⦃ _ : DecEq PubKey ⦄ + (genCT : ℕ → CipherText) (getPubKey : PrivKey → PubKey) + (pubKey : PubKey) (privKey : PrivKey) + (msgLength : PlainText → ℕ) where + + module L = LeakyChannel CipherText + module S = SecureChannel PlainText + module SH = EncryptionShim PlainText CipherText PubKey PrivKey genCT getPubKey pubKey privKey + + Functionality : Machine I (S.A ⊗ S.B ⊗ S.E) + Functionality = SH.Functionality ∘ L.Functionality + + Functionality' : Machine I ((S.A ⊗ S.B) ⊗ S.E) + Functionality' = subst (Machine I) (sym ⊗-assoc) Functionality + + -- F≤Secure : Functionality' ≤'UC S.Functionality' msgLength + -- F≤Secure = {!!} diff --git a/formal-spec/Leios/Network.agda b/formal-spec/Leios/Network.agda new file mode 100644 index 0000000..a6fdddf --- /dev/null +++ b/formal-spec/Leios/Network.agda @@ -0,0 +1,71 @@ +module Leios.Network where + +open import Prelude hiding (_∘_; _⊗_) +open import Ledger.Prelude using (ℙ_; _∈_; _∪_; ❴_❵; _∉_) +open import CategoricalCrypto + +record Abstract : Set₁ where + field Header Body ID : Set + match : Header → Body → Set + msgID : Header → ID + +module Broadcast (M Peer : Set) where + open Channel + + C : Channel + C .P = Peer + C .rcvType _ = Peer × M + C .sndType _ = M + + postulate Functionality : Machine I C + + Single : Channel + Single .P = ⊤ + Single .rcvType _ = Peer × M + Single .sndType _ = M + + postulate SingleFunctionality : Machine I Single + + -- connectWithBroadcast : ∀ {A} → (Peer → Machine Single A) → Machine I A + -- connectWithBroadcast = {!!} + +module HeaderDiffusion (a : Abstract) (Peer : Set) (self : Peer) where + open Channel + open Abstract a + module B = Broadcast Header Peer + + data Port : Set where + Send : Port -- we want to send a header + Forward : Port -- we want to forward a header + + C : Channel + C .P = Port + C .sndType _ = Header + C .rcvType Forward = Header + C .rcvType Send = ⊥ + + data Input : Set where + S : Header → Input + F : Header → Input + R : Peer → Header → Input + + data Output : Set where + Verify : Header → Output + + private variable + h : Header + s : ℙ ID + + data Step : ∃ (rcvType (B.Single ⊗ C ᵀ)) → ℙ ID → ℙ ID × Maybe (∃ (sndType (B.Single ⊗ C ᵀ))) → Set where + Init : Step (inj₂ Send , h) s (s ∪ ❴ msgID h ❵ , just (inj₁ _ , h)) + Receive1 : ∀ {p} → Step (inj₁ _ , p , h) s (s , just (inj₂ Forward , h)) + Receive2 : msgID h ∉ s → Step (inj₂ Forward , h) s (s ∪ ❴ msgID h ❵ , just (inj₁ _ , h)) + Receive2' : msgID h ∈ s → Step (inj₂ Forward , h) s (s , nothing) + + step : ∃ (rcvType (B.Single ⊗ C ᵀ)) → ∃ (sndType (B.Single ⊗ C ᵀ)) + step (inj₁ _ , _ , h) = (inj₂ Forward , h) + step (inj₂ Forward , h) = (inj₁ _ , h) + step (inj₂ Send , h) = (inj₁ _ , h) + + Functionality : Machine I C + Functionality = MkMachine' Step ∘ B.SingleFunctionality diff --git a/formal-spec/Leios/SimpleSpec.agda b/formal-spec/Leios/SimpleSpec.agda new file mode 100644 index 0000000..c9f350f --- /dev/null +++ b/formal-spec/Leios/SimpleSpec.agda @@ -0,0 +1,338 @@ +{-# OPTIONS --allow-unsolved-metas #-} + +module Leios.SimpleSpec where + +open import Ledger.Prelude +open import Data.List using (upTo) + +fromTo : ℕ → ℕ → List ℕ +fromTo m n = map (_+ m) (upTo (n ∸ m)) + +-- High level structure: + + +-- (simple) Leios +-- / | +-- +-------------------------------------+ | +-- | Header Diffusion Body Diffusion | | +-- +-------------------------------------+ Base Protocol +-- \ / +-- Network + + +record FFDAbstract : Type₁ where + field Header Body ID : Type + match : Header → Body → Type + msgID : Header → ID + +module FFD (a : FFDAbstract) (let open FFDAbstract a) where + + data Input : Type where + Send : Header → Maybe Body → Input + Fetch : Input + + data Output : Type where + SendRes : Output + FetchRes : List (Header ⊎ Body) → Output + + record Functionality : Type₁ where + field State : Type + stepRel : Input → State → State × Output → Type + +record LeiosAbstract : Type₁ where + field Tx : Type + PoolID : Type + BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer + ⦃ DecEq-Hash ⦄ : DecEq Hash + Vote : Type + vote : Hash → Vote + sign : PrivKey → Hash → Sig + ⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash + L Λ μ : ℕ + ⦃ NonZero-L ⦄ : NonZero L + +module Leios (a : LeiosAbstract) (let open LeiosAbstract a) (id : PoolID) (pKey : PrivKey) where + + OSig : Bool → Type + OSig true = Sig + OSig false = ⊤ + + IBRef = Hash + EBRef = Hash + + slice : (L : ℕ) → ⦃ NonZero L ⦄ → ℕ → ℕ → ℙ ℕ + slice L s x = fromList (fromTo s' (s' + (L ∸ 1))) + where s' = ((s / L) ∸ x) * L -- equivalent to the formula in the paper + + -- IsBlock typeclass (could do a closed-world approach instead) + -- Q: should votes have an instance of this class? + record IsBlock (B : Type) : Type where + field slotNumber : B → ℕ + producerID : B → PoolID + lotteryPf : B → VrfPf + + infix 4 _∈ᴮ_ + + _∈ᴮ_ : B → ℙ ℕ → Type + b ∈ᴮ X = slotNumber b ∈ X + + open IsBlock ⦃...⦄ public + + record IBHeaderOSig (b : Bool) : Type where + field slotNumber : ℕ + producerID : PoolID + lotteryPf : VrfPf + bodyHash : Hash + signature : OSig b + + instance + IsBlock-IBHeaderOSig : ∀ {b} → IsBlock (IBHeaderOSig b) + IsBlock-IBHeaderOSig = record { IBHeaderOSig } + + IBHeader = IBHeaderOSig true + PreIBHeader = IBHeaderOSig false + + instance postulate Hashable-PreIBHeader : Hashable PreIBHeader Hash + + mkIBHeader : ℕ → PoolID → VrfPf → List Tx → IBHeader + mkIBHeader slot id π txs = record { signature = sign pKey (hash h) ; IBHeaderOSig h } + where + h : IBHeaderOSig false + h = record { slotNumber = slot + ; producerID = id + ; lotteryPf = π + ; bodyHash = hash txs + ; signature = _ + } + + record IBBody : Type where + field txs : List Tx + + record InputBlock : Type where + field header : IBHeader + body : IBBody + + open IBHeaderOSig header public + + instance + Hashable-IBBody : Hashable IBBody Hash + Hashable-IBBody .hash b = hash (b .IBBody.txs) + + IsBlock-InputBlock : IsBlock InputBlock + IsBlock-InputBlock = record { InputBlock } + + record EndorserBlockOSig (b : Bool) : Type where + field slotNumber : ℕ + producerID : PoolID + lotteryPf : VrfPf + ibRefs : List IBRef + ebRefs : List EBRef + signature : OSig b + + EndorserBlock = EndorserBlockOSig true + PreEndorserBlock = EndorserBlockOSig false + + instance + postulate Hashable-PreEndorserBlock : Hashable PreEndorserBlock Hash + + Hashable-EndorserBlock : Hashable EndorserBlock Hash + Hashable-EndorserBlock .hash b = hash {T = PreEndorserBlock} + record { EndorserBlockOSig b hiding (signature) ; signature = _ } + + IsBlock-EndorserBlockOSig : ∀ {b} → IsBlock (EndorserBlockOSig b) + IsBlock-EndorserBlockOSig {b} = record { EndorserBlockOSig } + + mkEB : ℕ → PoolID → VrfPf → List IBRef → List EBRef → EndorserBlock + mkEB slot id π LI LE = record { signature = sign pKey (hash b) ; EndorserBlockOSig b } + where + b : PreEndorserBlock + b = record { slotNumber = slot + ; producerID = id + ; lotteryPf = π + ; ibRefs = LI + ; ebRefs = LE + ; signature = _ + } + + postulate getIBRef : InputBlock → IBRef -- I assume these two are just the regular hashes? + getEBRef : EndorserBlock → EBRef + + -- TODO + -- record ebValid (eb : EndorserBlock) : Type where + -- field lotteryPfValid : {!!} + -- signatureValid : {!!} + -- ibRefsValid : {!!} + -- ebRefsValid : {!!} + + module GenFFD where + data Header : Type where + ibHeader : IBHeader → Header + ebHeader : EndorserBlock → Header + vHeader : List Vote → Header + + data Body : Type where + ibBody : IBBody → Body + + ID : Type + ID = ℕ × PoolID + + match : Header → Body → Type + match (ibHeader h) (ibBody b) = bodyHash ≡ hash b + where open IBHeaderOSig h; open IBBody b + match _ _ = ⊥ + + -- can we express uniqueness wrt pipelines as a property? + msgID : Header → ID + msgID (ibHeader h) = (slotNumber h , producerID h) + msgID (ebHeader h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper + msgID (vHeader h) = {!!} + + ffdAbstract : FFDAbstract + ffdAbstract = record { GenFFD } + + module BaseFunctionality where + postulate StakeDistr Cert : Type + + data Input : Type₁ where + INIT : (EndorserBlock × Cert → Type) → Input + SUBMIT : EndorserBlock ⊎ List Tx → Input -- maybe we have both + + data Output : Type where + STAKE : StakeDistr → Output + + postulate State : Type + _⇀⟦_⟧_ : State → Input → State × Output → Type + + module _ (FFD : FFD.Functionality ffdAbstract) where + module FFD' = FFD.Functionality FFD using (State) renaming (stepRel to _⇀⟦_⟧_) + module B = BaseFunctionality + + postulate VTy FTCHTy : Type + initSlot : VTy → ℕ + initFFDState : FFD'.State + + data LeiosInput : Type where + INIT : VTy → LeiosInput + SLOT : LeiosInput + FTCH-LDG : LeiosInput + + data LeiosOutput : Type where + FTCH-LDG : FTCHTy → LeiosOutput + EMPTY : LeiosOutput + + record LeiosState : Type where + field V : VTy + SD : B.StakeDistr + FFDState : FFD'.State + Ledger : List Tx + MemPool : List Tx + IBs : List InputBlock + EBs : List EndorserBlock + Vs : List (List Vote) + slot : ℕ + + initLeiosState : VTy → B.StakeDistr → LeiosState + initLeiosState V SD = record + { V = V + ; SD = SD + ; FFDState = initFFDState + ; Ledger = [] + ; MemPool = [] + ; IBs = [] + ; EBs = [] + ; Vs = [] + ; slot = initSlot V + } + + postulate canProduceIB : ℕ → VrfPf → Type + canProduceEB : ℕ → VrfPf → Type + canProduceV1 : ℕ → Type + canProduceV2 : ℕ → Type + + -- some predicates about EBs + module _ (s : LeiosState) (eb : EndorserBlock) where + open EndorserBlockOSig eb + open LeiosState s + + postulate isVote1Certified : Type -- Q: what's the threshold? (pg 7, (5)) + + vote2Eligible : Type + vote2Eligible = length ebRefs ≥ lengthˢ candidateEBs / 2 -- should this be `>`? + × fromList ebRefs ⊆ candidateEBs + where candidateEBs : ℙ Hash + candidateEBs = mapˢ getEBRef $ filterˢ (_∈ᴮ slice L slot (μ + 3)) (fromList EBs) + + allIBRefsKnown : Type + allIBRefsKnown = ∀[ ref ∈ fromList ibRefs ] ref ∈ˡ map getIBRef IBs + + postulate instance isVote1Certified? : ∀ {s eb} → isVote1Certified s eb ⁇ + + private variable s : LeiosState + ffds' : FFD'.State + π : VrfPf + + open LeiosState using (FFDState; MemPool) + + data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutput → Type where + Init : ∀ {V bs bs' SD} → + ∙ {!!} -- create & register the IB/EB lottery and voting keys with key reg + ∙ bs B.⇀⟦ B.INIT {!V_chkCerts!} ⟧ (bs' , B.STAKE SD) + ──────────────────────────────── + nothing ⇀⟦ INIT V ⟧ (initLeiosState V SD , EMPTY) + + -- fix: we need to do Slot before every other SLOT transition + Slot : ∀ {msgs} → let ffds = s .FFDState + l = {!!} -- construct ledger l + in + ∙ FFD.Fetch FFD'.⇀⟦ ffds ⟧ (ffds' , FFD.FetchRes msgs) + ──────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' ; Ledger = l } , EMPTY) + + Ftch : ∀ {l} → + ──────────────────────────────── + just s ⇀⟦ FTCH-LDG ⟧ (s , FTCH-LDG l) + + -- TODO: Base chain + + IB-Role : let open LeiosState s + txs = s .MemPool + ffds = s .FFDState + b = GenFFD.ibBody (record { txs = txs }) + h = GenFFD.ibHeader (mkIBHeader slot id π txs) + in + ∙ canProduceIB slot π + ∙ FFD.Send h (just b) FFD'.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ──────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) + + EB-Role : let open LeiosState s + LI = map getIBRef $ setToList $ filterˢ (_∈ᴮ slice L slot (Λ + 1)) (fromList IBs) + LE = map getEBRef $ setToList $ filterˢ (isVote1Certified s) $ + filterˢ (_∈ᴮ slice L slot (μ + 2)) (fromList EBs) + h = mkEB slot id π LI LE + ffds = s .FFDState + in + ∙ canProduceEB slot π + ∙ FFD.Send (GenFFD.ebHeader h) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ──────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) + + V1-Role : let open LeiosState s + EBs' = filterˢ (allIBRefsKnown s) $ filterˢ (_∈ᴮ slice L slot (μ + 1)) (fromList EBs) + votes = map (vote ∘ hash) (setToList EBs') + ffds = s .FFDState + in + ∙ canProduceV1 slot + ∙ FFD.Send (GenFFD.vHeader votes) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ──────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) + + V2-Role : let open LeiosState s + EBs' = filterˢ (vote2Eligible s) $ filterˢ (_∈ᴮ slice L slot 1) (fromList EBs) + votes = map (vote ∘ hash) (setToList EBs') + ffds = s .FFDState + in + ∙ canProduceV2 slot + ∙ FFD.Send (GenFFD.vHeader votes) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ──────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) diff --git a/formal-spec/leios-spec.agda-lib b/formal-spec/leios-spec.agda-lib new file mode 100644 index 0000000..a6d38ad --- /dev/null +++ b/formal-spec/leios-spec.agda-lib @@ -0,0 +1,8 @@ +name: leios-spec +depend: + standard-library + standard-library-classes + standard-library-meta + formal-ledger +include: + . diff --git a/nix/agda.nix b/nix/agda.nix new file mode 100644 index 0000000..abb9b51 --- /dev/null +++ b/nix/agda.nix @@ -0,0 +1,108 @@ +{ pkgs, lib, inputs, ... }: + +let + + locales = { + LANG = "en_US.UTF-8"; + LC_ALL = "en_US.UTF-8"; + LOCALE_ARCHIVE = if pkgs.system == "x86_64-linux" + then "${pkgs.glibcLocales}/lib/locale/locale-archive" + else ""; + }; + + customAgda = pkgs; + + agdaStdlib = customAgda.agdaPackages.standard-library; + + agdaStdlibClasses = customAgda.agdaPackages.mkDerivation { + inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; + pname = "agda-stdlib-classes"; + version = "2.0"; + src = pkgs.fetchFromGitHub { + repo = "agda-stdlib-classes"; + owner = "omelkonian"; + rev = "v2.0"; + sha256 = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E="; + }; + meta = { }; + libraryFile = "agda-stdlib-classes.agda-lib"; + everythingFile = "Classes.agda"; + buildInputs = [ agdaStdlib ]; + }; + + agdaStdlibMeta = customAgda.agdaPackages.mkDerivation { + inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; + pname = "agda-stdlib-meta"; + version = "2.0"; + src = pkgs.fetchFromGitHub { + repo = "stdlib-meta"; + owner = "input-output-hk"; + rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314"; + sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM="; + }; + meta = { }; + libraryFile = "agda-stdlib-meta.agda-lib"; + everythingFile = "Main.agda"; + buildInputs = [ agdaStdlib agdaStdlibClasses ]; + }; + + formalLedger = customAgda.agdaPackages.mkDerivation { + inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; + pname = "formal-ledger"; + version = "1d77a35a"; + src = pkgs.fetchFromGitHub { + repo = "formal-ledger-specifications"; + owner = "IntersectMBO"; + rev = "1d77a35ab1820c123790e5138d85325d33787e86"; + sha256 = "0d15aysxdmn31aj982gr63d40q606dqvq0k4y4rwa9kpmjgadjaq"; + }; + meta = { }; + preConfigure = '' + cat << EOI > formal-ledger.agda-lib + name: formal-ledger + depend: + standard-library + standard-library-classes + standard-library-meta + include: src + EOI + mv src/Everything.agda . + ''; + libraryFile = "formal-ledger.agda-lib"; + everythingFile = "Everything.agda"; + buildInputs = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ]; + }; + + leiosSpec = customAgda.agdaPackages.mkDerivation { + inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; + pname = "leios-spec"; + name = "leios-spec"; # FIXME: Why is this entry needed? + src = ../formal-spec; + meta = { }; + preConfigure = '' + cat << EOI > Everything.agda + module Everything where + import CategoricalCrypto + import Leios.Network + import Leios.SimpleSpec + EOI + ls + ''; + libraryFile = "formal-spec/leios-spec.agda-lib"; + everythingFile = "Everything.agda"; + buildInputs = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta formalLedger ]; + }; + + agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; ghc = pkgs.ghc; }; + +in +{ + inherit agdaStdlib agdaStdlibClasses agdaStdlibMeta formalLedger ; + agdaWithDeps = agdaWithPkgs [ + agdaStdlib + agdaStdlibClasses + agdaStdlibMeta + formalLedger + ]; + leiosSpec = leiosSpec; +} diff --git a/nix/outputs.nix b/nix/outputs.nix index 48c87c8..c4cdbb5 100644 --- a/nix/outputs.nix +++ b/nix/outputs.nix @@ -3,12 +3,13 @@ let project = repoRoot.nix.project; + agda = import ./agda.nix {inherit pkgs lib inputs;}; in [ - ( - # Docs for project.flake: https://github.com/input-output-hk/iogx/blob/main/doc/api.md#mkhaskellprojectoutflake - project.flake - ) + (project.flake) + { + packages.leiosSpec = agda.leiosSpec; + } ] diff --git a/nix/shell.nix b/nix/shell.nix index 1adf23c..aaeacbe 100644 --- a/nix/shell.nix +++ b/nix/shell.nix @@ -8,29 +8,40 @@ # project. cabalProject: +let + + agda = import ./agda.nix {inherit pkgs lib inputs;}; + emacsWithPackages = pkgs.emacs.pkgs.withPackages (epkgs: [ epkgs.agda2-mode pkgs.mononoki ]); + +in + { name = "nix-shell"; - # prompt = null; + packages = [ + agda.agdaWithDeps + emacsWithPackages + ]; - # welcomeMessage = null; + # Agda environment variables. + env.AGDA_STDLIB = "${agda.agdaStdlib}/standard-library.agda-lib"; + env.AGDA_STDLIB_CLASSES = "${agda.agdaStdlibClasses}/standard-library-classes.agda-lib"; + env.AGDA_STDLIB_META = "${agda.agdaStdlibMeta}/standard-library-meta.agda-lib"; + env.FORMAL_LEDGER_LIB = "${agda.formalLedger}/formal-ledger.agda-lib"; - # packages = []; +# prompt = "[ouroboros-leios]$ "; - # scripts = { - # foo = { - # description = ""; - # group = "general"; - # enabled = true; - # exec = '' - # echo "Hello, World!" - # ''; - # }; - # }; + welcomeMessage = '' + Welcome to Ouroboros Leios! - # env = { - # KEY = "VALUE"; - # }; + Locations of Agda libraries: + ${agda.agdaStdlib}/standard-library.agda-lib + ${agda.agdaStdlibClasses}/standard-library-classes.agda-lib + ${agda.agdaStdlibMeta}/standard-library-meta.agda-lib + ${agda.formalLedger}/formal-ledger.agda-lib + + Run 'emacs' to edit .agda files. + ''; # shellHook = ""; @@ -52,6 +63,17 @@ cabalProject: # purs-tidy = null; }; + # scripts = { + # foo = { + # description = ""; + # group = "general"; + # enabled = true; + # exec = '' + # echo "Hello, World!" + # ''; + # }; + # }; + # preCommit = { # cabal-fmt.enable = false; # cabal-fmt.extraOptions = ""; @@ -74,5 +96,6 @@ cabalProject: # purs-tidy.enable = false; # purs-tidy.extraOptions = ""; # }; + } - \ No newline at end of file +