Skip to content

Commit b8fdf63

Browse files
bwbushbwbush
authored
Merge pull request #745 from input-output-hk/bwbush/fm-crypto
Formal specification of Leios cryptography
2 parents 8dbd491 + 635071f commit b8fdf63

20 files changed

+1966
-1
lines changed

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,17 +4,33 @@ on:
44
pull_request:
55
paths:
66
- "analysis/markov/**"
7+
- "post-cip/formal-crypto/lean/**"
78
push:
89
branches:
910
- main
1011
paths:
1112
- "analysis/markov/**"
13+
- "post-cip/formal-crypto/lean/**"
1214

1315
jobs:
14-
build:
16+
17+
markov-simulator:
18+
if: true
1519
runs-on: ubuntu-latest
1620
steps:
1721
- uses: actions/checkout@v4
1822
- uses: leanprover/lean-action@v1
1923
with:
2024
lake-package-directory: analysis/markov
25+
use-github-cache: true
26+
27+
leioscrypto-spec:
28+
if: false # Turn off because the `proofwidgets` dependency fails to build due to an `npm` dependency.
29+
runs-on: ubuntu-latest
30+
steps:
31+
- uses: actions/checkout@v4
32+
- uses: leanprover/lean-action@v1
33+
with:
34+
lake-package-directory: post-cip/formal-crypto/lean
35+
use-mathlib-cache: false
36+
use-github-cache: false

‎post-cip/formal-crypto/ReadMe.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
# Non-normative formal specifications for Leios sortition, votes, and certificates
2+
3+
The folder [lean/](./lean/) contains the non-normative specification in Lean4.
4+
5+
The normative specification is resides in the Leios CIP and related documents:
6+
7+
- [CIP-0164](https://github.com/cardano-foundation/CIPs/blob/master/CIP-0164/README.md)
8+
- [BLS certificates for Leios](../../crypto-benchmarks.rs/Specification.md)
9+
- [Determining a quorum in weighted Fait Accompli with local sortition](../../weighted-fait-accompli.md)
10+
11+
There also exists [a prototype benchmarking implementation in Rust](../../crypto-benchmarks.rs/).
12+
13+

‎post-cip/formal-crypto/lean/.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
.lake/

‎post-cip/formal-crypto/lean/ReadMe.md‎

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
# Non-normative formal specification for Leios sortition, votes, and certificates in Lean4
2+
3+
See [the read-me in the parent folder](../ReadMe.md) for context and further references.
4+
5+
6+
## Status
7+
8+
This formal specification is a **non-normative** attempt to disambiguate and clarify concepts and relationships in [the original normative specifications](../ReadMe.md).
9+
10+
Future potential development:
11+
12+
- [ ] Refactor constraint structure for improved clarity.
13+
- [ ] Add hyperlinks to normative specifications.
14+
- [ ] Simplify proofs.
15+
- [ ] Separate lemmas from larger proofs.
16+
- [ ] Minimize use of `simp`, `omega`, and `aesop` tactics in proofs.
17+
- [ ] Translate into Agda.
18+
19+
20+
## Type relationships
21+
22+
```mermaid
23+
classDiagram
24+
%% --- Core Election Structures ---
25+
class Election {
26+
+Epoch epoch
27+
+Slot slot
28+
+ElectionId electionId
29+
+BlockHash ebHash
30+
}
31+
32+
class Epoch {
33+
+LeiosParameters protocol
34+
+Registry registry
35+
+Nat number
36+
+StakeDistribution stakes
37+
+SlotRange slot_range
38+
+PraosNonce nonce
39+
+FaitAccompli fa
40+
}
41+
42+
class LeiosParameters {
43+
+Rat τ
44+
+Nat n
45+
}
46+
47+
class FaitAccompli {
48+
+StakeDistribution stakes
49+
+Nat seats
50+
+Rat ρStar
51+
+Nat n₁
52+
+Nat n₂
53+
}
54+
55+
%% --- Identity and Stakes ---
56+
class StakeDistribution {
57+
+List~PoolKeyHash, Coin~ pools
58+
}
59+
60+
class Registry {
61+
%% Registry is defined as List Registration
62+
+List~Registration~ entries
63+
}
64+
65+
class Registration {
66+
+Pool pool
67+
+Nat issueCounter
68+
+ColdKeySignature signature
69+
}
70+
71+
class Pool {
72+
+PoolKeyHash poolId
73+
+PublicKey mvk
74+
+ProofOfPossession μ
75+
}
76+
77+
%% --- Certificates and Votes ---
78+
class Certificate {
79+
+ElectionId electionId
80+
+BlockHash ebHash
81+
+List~PoolIndex~ persistentVotes
82+
+List~PoolKeyHash, Signature~ nonpersistentVotes
83+
+Option~Signature~ σ_tilde_eid
84+
+Signature σ_tilde_m
85+
}
86+
87+
class Vote {
88+
<<Inductive>>
89+
+PersistentVote(ElectionId, PoolIndex, BlockHash, Signature)
90+
+NonpersistentVote(ElectionId, PoolKeyHash, Signature, BlockHash, Signature)
91+
}
92+
93+
class Eligible {
94+
<<Inductive>>
95+
+IsPersistent(Proof)
96+
+IsNonpersistent(Proof)
97+
+NotEligible
98+
}
99+
100+
%% --- Relationships ---
101+
Election *-- Epoch
102+
Epoch *-- LeiosParameters
103+
Epoch *-- Registry
104+
Epoch *-- StakeDistribution
105+
Epoch *-- FaitAccompli
106+
107+
%% FaitAccompli references the same stake distribution
108+
FaitAccompli --> StakeDistribution
109+
110+
Registry o-- Registration
111+
Registration *-- Pool
112+
113+
%% Conceptual Links
114+
Certificate --> Election : validates
115+
Certificate ..> Vote : aggregates (conceptual)
116+
117+
Vote --> Election : targets
118+
Eligible --> Election : predicate on
119+
```
120+
121+
122+
## Conventions for constraints
123+
124+
- `WellFormed` constraints ensure that values have basic internal consistency.
125+
- `Valid` constraints ensure that values are consistent with their context.
126+
- `Authentic` constraints ensure that values are cryptographically verified.
127+
- `Checked` constraints simply ensure `WellFormed ∧ Valid ∧ Authentic`.
128+
129+
130+
## Source
131+
132+
- [BLS.lean](./src/Leioscrypto/BLS.lean): primitive BLS types, functions, and axioms.
133+
- [Certificate.lean](./src/Leioscrypto/Certificate.lean): certificates.
134+
- [Contexts.lean](./src/Leioscrypto/Contexts.lean): protocol parameters, epochs, and elections.
135+
- [FaitAccompli.lean](./src/Leioscrypto/FaitAccompli.lean): Fait Accompli sortition.
136+
- [LocalSortition.lean](./src/Leioscrypto/LocalSortition.lean): local sortition.
137+
- [Registration.lean](./src/Leioscrypto/Registration.lean): key registration.
138+
- [StakeDistribution.lean](./src/Leioscrypto/StakeDistribution.lean): stake distribution.
139+
- [Types.lean](./src/Leioscrypto/Types.lean): basic types.
140+
- [Util.lean](./src/Leioscrypto/Util.lean): miscellaneous functions and theorems.
141+
- [Vote.lean](./src/Leioscrypto/Vote.lean): votes.
142+
143+
144+
## Type-checking and testing the specification
145+
146+
A [Nix shell derivation](./shell.nix) is provided for type-checking the specification and executing its test suite.
147+
148+
```bash
149+
nix-shell
150+
lake build
151+
lake test
152+
```

‎post-cip/formal-crypto/lean/lake-manifest.json‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover/doc-gen4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "",
8+
"rev": "0ece4c27ae1abbd0b70df729e09d8b9c06351b80",
9+
"name": "«doc-gen4»",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.25.0",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/argumentcomputer/LSpec",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
19+
"name": "LSpec",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
22+
"inherited": false,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/mathlib4",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "",
28+
"rev": "1ccd71f89cbbd82ae7d097723ce1722ca7b01c33",
29+
"name": "mathlib",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "v4.25.0",
32+
"inherited": false,
33+
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/leanprover/lean4-cli",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0",
39+
"name": "Cli",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "",
48+
"rev": "1829aec18f0e8a661dd5acf5d659d636979ba4f2",
49+
"name": "UnicodeBasic",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "main",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/dupuisf/BibtexQuery",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "",
58+
"rev": "29a4b34f8caa7c95934ab4494d8866fde1850c0b",
59+
"name": "BibtexQuery",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "master",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/acmepjz/md4lean",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "",
68+
"rev": "44da417da3705ede62b5c39382ddd2261ec3933e",
69+
"name": "MD4Lean",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "main",
72+
"inherited": true,
73+
"configFile": "lakefile.lean"},
74+
{"url": "https://github.com/leanprover-community/plausible",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3",
79+
"name": "plausible",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
89+
"name": "LeanSearchClient",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"},
94+
{"url": "https://github.com/leanprover-community/import-graph",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "leanprover-community",
98+
"rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb",
99+
"name": "importGraph",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"},
104+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
105+
"type": "git",
106+
"subDir": null,
107+
"scope": "leanprover-community",
108+
"rev": "e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d",
109+
"name": "proofwidgets",
110+
"manifestFile": "lake-manifest.json",
111+
"inputRev": "v0.0.79",
112+
"inherited": true,
113+
"configFile": "lakefile.lean"},
114+
{"url": "https://github.com/leanprover-community/aesop",
115+
"type": "git",
116+
"subDir": null,
117+
"scope": "",
118+
"rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349",
119+
"name": "aesop",
120+
"manifestFile": "lake-manifest.json",
121+
"inputRev": "v4.25.0",
122+
"inherited": false,
123+
"configFile": "lakefile.toml"},
124+
{"url": "https://github.com/leanprover-community/quote4",
125+
"type": "git",
126+
"subDir": null,
127+
"scope": "leanprover-community",
128+
"rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f",
129+
"name": "Qq",
130+
"manifestFile": "lake-manifest.json",
131+
"inputRev": "master",
132+
"inherited": true,
133+
"configFile": "lakefile.toml"},
134+
{"url": "https://github.com/leanprover-community/batteries",
135+
"type": "git",
136+
"subDir": null,
137+
"scope": "leanprover-community",
138+
"rev": "5c78955e8375f872c085514cb521216bac1bda17",
139+
"name": "batteries",
140+
"manifestFile": "lake-manifest.json",
141+
"inputRev": "main",
142+
"inherited": true,
143+
"configFile": "lakefile.toml"}],
144+
"name": "leioscrypto",
145+
"lakeDir": ".lake"}

‎post-cip/formal-crypto/lean/lakefile.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
import Lake
2+
3+
open Lake DSL
4+
5+
abbrev linter : Array LeanOption := #[
6+
⟨`linter.longLine, true⟩,
7+
-- (`linter.style.multiGoal, true),
8+
-- (`linter.textBased.trailingWhitespace, true),
9+
-- (`linter.defLemma, true),
10+
⟨`linter.missingEnd, true⟩,
11+
⟨`linter.setOption, true⟩
12+
]
13+
14+
package «leioscrypto» where
15+
version := StdVer.mk (SemVerCore.mk 0 1 0) ""
16+
testDriver := "leioscrypto_test"
17+
leanOptions := #[
18+
-- pretty-prints `fun a ↦ b`
19+
⟨`pp.unicode.fun, true⟩,
20+
-- disables automatic implicit arguments
21+
⟨`autoImplicit, false⟩,
22+
-- suppresses the checkBinderAnnotations error/warning
23+
⟨`checkBinderAnnotations, false⟩,
24+
] ++ linter.map fun s ↦ { s with name := `weak ++ s.name }
25+
moreServerOptions := #[
26+
⟨`trace.debug, true⟩,
27+
]
28+
29+
lean_lib «Leioscrypto» where
30+
srcDir := "src"
31+
32+
@[default_target]
33+
lean_exe «leioscrypto_test» where
34+
root := `LeioscryptoTest
35+
srcDir := "src"
36+
37+
require mathlib from git
38+
"https://github.com/leanprover-community/mathlib4" @ "v4.25.0"
39+
40+
require LSpec from git
41+
"https://github.com/argumentcomputer/LSpec" @ "b05e6b83798bce0887eb5001cb10fdcbe675dde3"
42+
43+
require «doc-gen4» from git
44+
"https://github.com/leanprover/doc-gen4" @ "v4.25.0"

‎post-cip/formal-crypto/lean/lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.25.0

0 commit comments

Comments
 (0)