-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathQuasar.lean
More file actions
95 lines (77 loc) · 2.92 KB
/
Quasar.lean
File metadata and controls
95 lines (77 loc) · 2.92 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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
/-
Quasar Protocol Formal Model
Models protocol/quasar/ -- BLS+Ringtail hybrid quantum consensus.
Quasar is the finality engine. It collects blocks from all chains
and produces quantum-final aggregate blocks with dual signatures:
- BLS (classical, fast): 96-byte aggregated signatures
- Ringtail (post-quantum, larger): ~4KB lattice-based threshold signatures
Maps to:
- quasar/bls.go: BLS signature aggregation (quorum = 2f+1)
- quasar/core.go: Quasar struct, chain buffers, quantum finality
- quasar/engine.go: Engine implementation
- quasar/horizon.go: Event horizon (pending blocks)
Properties:
- BLS aggregation correctness: agg_verify(agg_sig, agg_pk, msg) iff all individual sigs valid
- Quorum threshold: 2f+1 signatures required for finality
- Dual signature: quantum block has both BLS and Ringtail sigs
- Epoch monotonicity: quantum height only increases
-/
import Mathlib.Data.Nat.Defs
import Mathlib.Tactic
namespace Protocol.Quasar
/-- Signature types -/
structure BLSSig where
bytes : List UInt8
valid : Bool
structure RingtailSig where
bytes : List UInt8
valid : Bool
/-- Quasar signature = BLS + Ringtail (models quasar.QuasarSig) -/
structure QuasarSig where
bls : BLSSig
ringtail : RingtailSig
/-- Quantum block (models quasar.QuantumBlock) -/
structure QuantumBlock where
height : Nat
sourceBlocks : List Nat -- block hashes
signature : QuasarSig
/-- Quasar state -/
structure QuasarState where
quantumHeight : Nat
finalized : List QuantumBlock
/-- BLS aggregation: aggregate of valid sigs is valid -/
axiom bls_aggregation_sound :
∀ (sigs : List BLSSig),
(∀ s ∈ sigs, s.valid = true) →
sigs ≠ [] →
-- Aggregated signature is valid (bilinear pairing property)
∃ (agg : BLSSig), agg.valid = true
/-- Quantum height is monotonically increasing -/
def addBlock (s : QuasarState) (b : QuantumBlock)
(h : b.height > s.quantumHeight) : QuasarState :=
{ quantumHeight := b.height
, finalized := b :: s.finalized }
theorem height_monotone (s : QuasarState) (b : QuantumBlock)
(h : b.height > s.quantumHeight) :
(addBlock s b h).quantumHeight > s.quantumHeight := by
simp [addBlock]
exact h
/-- Quorum intersection for BLS signatures:
Two quorums of 2f+1 from n=3f+1 validators share f+1 members.
At least one shared member is honest. -/
theorem bls_quorum_intersection
(n f : Nat) (hf : 3 * f < n)
(q1 q2 : Nat)
(hq1 : q1 ≥ 2 * f + 1) (hq2 : q2 ≥ 2 * f + 1) :
q1 + q2 > n := by
omega
/-- Dual signature validity: both components must be valid -/
def isValidQuantumSig (qs : QuasarSig) : Bool :=
qs.bls.valid && qs.ringtail.valid
/-- A finalized block has both BLS and Ringtail valid -/
theorem quantum_finality_requires_both
(qs : QuasarSig) (h : isValidQuantumSig qs = true) :
qs.bls.valid = true ∧ qs.ringtail.valid = true := by
simp [isValidQuantumSig] at h
exact h
end Protocol.Quasar