-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathNova.lean
More file actions
72 lines (56 loc) · 2.28 KB
/
Nova.lean
File metadata and controls
72 lines (56 loc) · 2.28 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
/-
Nova Protocol Formal Model
Models protocol/nova/nova.go -- linear blockchain consensus mode.
Nova wraps Ray (linear decision engine) and provides blockchain semantics.
It is the simplest consensus mode: blocks form a chain, decided sequentially.
Maps to:
- nova.go: Nova struct wrapping ray.Driver
- nova.go: Config{SampleSize, Alpha, Beta, RoundTO, GenesisHash}
- nova.go: NewNova, Start, Stop, Status
Nova delegates all consensus logic to Ray, which delegates voting to Wave.
The composition: Nova -> Ray -> Wave -> Prism (sampling)
Properties:
- Chain property: decided blocks form a valid chain (parent links)
- Genesis: genesis block is always the first decided block
- Height monotonicity: block heights are strictly increasing
-/
import Mathlib.Data.Nat.Defs
import Mathlib.Tactic
namespace Protocol.Nova
/-- Block in linear chain -/
structure Block where
id : Nat
parentId : Nat
height : Nat
/-- Nova chain state -/
structure NovaState where
chain : List Block
lastHeight : Nat
/-- Genesis state -/
def genesis (genesisBlock : Block) (hg : genesisBlock.height = 0) : NovaState :=
{ chain := [genesisBlock], lastHeight := 0 }
/-- Append block to chain -/
def appendBlock (s : NovaState) (b : Block)
(hparent : b.parentId = (s.chain.head?.map Block.id).getD 0)
(hheight : b.height = s.lastHeight + 1) : NovaState :=
{ chain := b :: s.chain, lastHeight := b.height }
/-- Height is strictly increasing -/
theorem height_increases (s : NovaState) (b : Block)
(hparent : b.parentId = (s.chain.head?.map Block.id).getD 0)
(hheight : b.height = s.lastHeight + 1) :
(appendBlock s b hparent hheight).lastHeight > s.lastHeight := by
simp [appendBlock, hheight]
omega
/-- Chain grows on append -/
theorem chain_grows (s : NovaState) (b : Block)
(hp : b.parentId = (s.chain.head?.map Block.id).getD 0)
(hh : b.height = s.lastHeight + 1) :
(appendBlock s b hp hh).chain.length = s.chain.length + 1 := by
simp [appendBlock, List.length_cons]
/-- Genesis has height 0 -/
theorem genesis_height (b : Block) (hg : b.height = 0) :
(genesis b hg).lastHeight = 0 := rfl
/-- Genesis chain has exactly one block -/
theorem genesis_single (b : Block) (hg : b.height = 0) :
(genesis b hg).chain.length = 1 := rfl
end Protocol.Nova