204 lines
9.6 KiB
Plaintext
204 lines
9.6 KiB
Plaintext
---------------------------- MODULE PoT ----------------------------
|
||
(*
|
||
Формальная спецификация Proof of Time консенсуса Монтаны.
|
||
Уровень абстракции: безопасность (Safety) и живость (Liveness)
|
||
при византийском противнике f < n/3 в частично синхронной модели.
|
||
|
||
Не моделируется (вне scope этого spec):
|
||
- Конкретные SHA-256 байты (VDF аппроксимирован монотонной функцией)
|
||
- Криптография подписей (предполагается EUF-CMA, см. 02 Криптография)
|
||
- Сетевая сериализация (предполагается канонической)
|
||
*)
|
||
|
||
EXTENDS Naturals, FiniteSets, Sequences, TLC
|
||
|
||
CONSTANTS
|
||
Operators, \* Множество всех операторов
|
||
Honest, \* Подмножество честных операторов
|
||
Byzantine, \* Подмножество византийских операторов
|
||
Accounts, \* Множество аккаунтов
|
||
MaxWindow, \* Граница model checking-а
|
||
GST \* Global Stabilization Time (окно после которого сеть синхронна)
|
||
|
||
ASSUME
|
||
/\ Honest \cup Byzantine = Operators
|
||
/\ Honest \cap Byzantine = {}
|
||
/\ Cardinality(Byzantine) * 3 < Cardinality(Operators) \* f < n/3
|
||
/\ Cardinality(Honest) >= 1
|
||
/\ MaxWindow \in Nat
|
||
/\ GST \in 0..MaxWindow
|
||
|
||
VARIABLES
|
||
window, \* Текущее окно τ₁ (длина VDF-цепи)
|
||
vdf_chain, \* Канонический VDF-выход на каждом окне: window -> hash
|
||
committed, \* Зафиксированные операции: window -> SUBSET <<account, op>>
|
||
proposed, \* Предложения операторов: <<operator, window, op>>
|
||
operator_chain, \* Локальная цепь оператора: operator -> Seq(window)
|
||
selection_winner \* Победитель лотереи окна: window -> operator
|
||
|
||
vars == <<window, vdf_chain, committed, proposed, operator_chain, selection_winner>>
|
||
|
||
----------------------------------------------------------------------
|
||
(* Определения *)
|
||
|
||
\* Один шаг на личность за окно: аккаунт может иметь не более одной операции
|
||
\* в каждом окне (anti-Sybil на уровне аккаунта)
|
||
OneStepPerWindow(w, a) ==
|
||
Cardinality({op \in committed[w] : op[1] = a}) <= 1
|
||
|
||
\* Каноническое продвижение VDF: window+1 = SHA-256^D от window
|
||
\* Здесь абстракция: vdf_chain[w+1] зависит детерминированно от vdf_chain[w]
|
||
VDFCanonical(w) ==
|
||
IF w = 0 THEN TRUE
|
||
ELSE vdf_chain[w] # vdf_chain[w-1] \* Каждое окно даёт новый выход
|
||
|
||
\* Network synchronous after GST
|
||
SynchronousAfter(w) == w >= GST
|
||
|
||
----------------------------------------------------------------------
|
||
(* Initial state *)
|
||
|
||
Init ==
|
||
/\ window = 0
|
||
/\ vdf_chain = [w \in {0} |-> 0] \* Genesis seed = 0
|
||
/\ committed = [w \in {0} |-> {}]
|
||
/\ proposed = {}
|
||
/\ operator_chain = [o \in Operators |-> <<>>]
|
||
/\ selection_winner = [w \in {} |-> CHOOSE o \in Operators : TRUE]
|
||
|
||
----------------------------------------------------------------------
|
||
(* Действия *)
|
||
|
||
\* Действие: оператор крутит VDF и продвигает окно
|
||
AdvanceWindow ==
|
||
/\ window < MaxWindow
|
||
/\ window' = window + 1
|
||
/\ vdf_chain' = vdf_chain @@ (window+1 :> window+1) \* Абстракция SHA-256^D
|
||
/\ committed' = committed @@ (window+1 :> {})
|
||
/\ UNCHANGED <<proposed, operator_chain, selection_winner>>
|
||
|
||
\* Действие: честный оператор предлагает операцию
|
||
HonestPropose(o, a, op_data) ==
|
||
/\ o \in Honest
|
||
/\ window > 0
|
||
/\ a \in Accounts
|
||
/\ \A p \in proposed : ~(p[1] = o /\ p[2] = window /\ p[3][1] = a)
|
||
\* Честный оператор не предлагает дублирующую операцию для аккаунта в текущем окне
|
||
/\ proposed' = proposed \cup {<<o, window, <<a, op_data>>>>}
|
||
/\ operator_chain' = [operator_chain EXCEPT ![o] = Append(@, window)]
|
||
/\ UNCHANGED <<window, vdf_chain, committed, selection_winner>>
|
||
|
||
\* Действие: византийский оператор может предложить ЛЮБУЮ операцию
|
||
\* (включая дубликаты, конфликтующие, в любом окне)
|
||
ByzantinePropose(o, a, op_data, w) ==
|
||
/\ o \in Byzantine
|
||
/\ w \in DOMAIN vdf_chain
|
||
/\ a \in Accounts
|
||
/\ proposed' = proposed \cup {<<o, w, <<a, op_data>>>>}
|
||
/\ UNCHANGED <<window, vdf_chain, committed, operator_chain, selection_winner>>
|
||
|
||
\* Лотерея: выбор победителя окна детерминированно из VDF-выхода
|
||
\* Абстракция: победитель — оператор, чей хеш-id ближе всех к vdf_chain[window]
|
||
LotterySelect ==
|
||
/\ window > 0
|
||
/\ window \notin DOMAIN selection_winner
|
||
/\ \E o \in Operators :
|
||
/\ selection_winner' = selection_winner @@ (window :> o)
|
||
/\ UNCHANGED <<window, vdf_chain, committed, proposed, operator_chain>>
|
||
|
||
\* Коммит: победитель окна включает свой набор операций в канон
|
||
\* Безопасность: один шаг на личность сохраняется
|
||
WinnerCommit ==
|
||
/\ window > 0
|
||
/\ window \in DOMAIN selection_winner
|
||
/\ LET winner == selection_winner[window]
|
||
winner_proposals == {p \in proposed : p[1] = winner /\ p[2] = window}
|
||
by_account == { p[3] : p \in winner_proposals }
|
||
IN
|
||
/\ \* Один шаг на личность: для каждого аккаунта максимум одна операция
|
||
\A a \in Accounts :
|
||
Cardinality({op \in by_account : op[1] = a}) <= 1
|
||
/\ committed' = [committed EXCEPT ![window] = by_account]
|
||
/\ UNCHANGED <<window, vdf_chain, proposed, operator_chain, selection_winner>>
|
||
|
||
\* Полный шаг состояния
|
||
Next ==
|
||
\/ AdvanceWindow
|
||
\/ \E o \in Operators, a \in Accounts, op_data \in {1,2,3} :
|
||
HonestPropose(o, a, op_data)
|
||
\/ \E o \in Byzantine, a \in Accounts, op_data \in {1,2,3}, w \in 0..window :
|
||
ByzantinePropose(o, a, op_data, w)
|
||
\/ LotterySelect
|
||
\/ WinnerCommit
|
||
|
||
Spec == Init /\ [][Next]_vars /\ WF_vars(AdvanceWindow) /\ WF_vars(LotterySelect) /\ WF_vars(WinnerCommit)
|
||
|
||
----------------------------------------------------------------------
|
||
(* Инварианты безопасности *)
|
||
|
||
\* S1 — Safety: невозможность форков
|
||
\* Для любого окна w и любого аккаунта a:
|
||
\* количество зафиксированных операций аккаунта a в окне w не больше 1.
|
||
NoDoubleSpendInWindow ==
|
||
\A w \in DOMAIN committed :
|
||
\A a \in Accounts :
|
||
Cardinality({op \in committed[w] : op[1] = a}) <= 1
|
||
|
||
\* S2 — VDF канонический: каждое окно даёт новый выход
|
||
VDFMonotone ==
|
||
\A w \in DOMAIN vdf_chain :
|
||
VDFCanonical(w)
|
||
|
||
\* S3 — Только победитель лотереи коммитит в окне
|
||
OnlyWinnerCommits ==
|
||
\A w \in DOMAIN committed :
|
||
committed[w] # {} =>
|
||
/\ w \in DOMAIN selection_winner
|
||
/\ \A op \in committed[w] :
|
||
\E p \in proposed :
|
||
/\ p[1] = selection_winner[w]
|
||
/\ p[2] = w
|
||
/\ p[3] = op
|
||
|
||
\* S4 — VDF цепь монотонна (длина растёт)
|
||
WindowMonotone == window' >= window
|
||
|
||
----------------------------------------------------------------------
|
||
(* Свойства живости (Liveness) *)
|
||
|
||
\* L1 — После GST: каждая операция честного оператора в конце концов коммитится
|
||
\* (упрощённо — модель не различает корректность операции от её принятия)
|
||
EventuallyCommitted(o, a, op_data) ==
|
||
[](
|
||
(window >= GST /\ o \in Honest /\ \E w \in DOMAIN vdf_chain : <<o, w, <<a, op_data>>>> \in proposed)
|
||
=> <>(\E w \in DOMAIN committed : <<a, op_data>> \in committed[w])
|
||
)
|
||
|
||
\* L2 — Окно бесконечно продвигается (если хотя бы один честный оператор активен)
|
||
WindowProgresses ==
|
||
[](\E h \in Honest : TRUE) => []<>(window' > window)
|
||
|
||
----------------------------------------------------------------------
|
||
(* Дополнительные допущения и аксиомы *)
|
||
|
||
THEOREM Safety == Spec => []NoDoubleSpendInWindow
|
||
THEOREM VDFCorrect == Spec => []VDFMonotone
|
||
THEOREM CommitProvenance == Spec => []OnlyWinnerCommits
|
||
THEOREM ChainProgress == Spec => []WindowMonotone
|
||
|
||
(*
|
||
Доказательства этих теорем выполняются через:
|
||
1. TLAPS (TLA+ Proof System) — формально верифицируемые
|
||
2. TLC model checking при малых N (см. PoT.cfg)
|
||
|
||
Текущая модель верифицирует Safety при:
|
||
- |Operators| = 4 (3 honest, 1 Byzantine)
|
||
- |Accounts| = 3
|
||
- MaxWindow = 10
|
||
|
||
Полная формальная верификация на больших N требует
|
||
разбора по индукции с инвариантами — открытый вопрос.
|
||
*)
|
||
|
||
============================================================================
|