mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
54c7e9ac87
TLC had never verified anything: every MC config assigned constants with `=` (TLC model-value) instead of `<-` (operator substitution), so e.g. N became the symbol "MC_N" and the spec's `ASSUME N \in Nat` was false → TLC bailed before checking. MC_Quasar's quorum was also set to exactly 2/3, violating the strict `quorum > 2/3` BFT assumption. Fixed both; all 13 MC specs now run. Result — 13/13 model-check clean, and checking surfaced real bugs (not just config): - Teleport: ConservationOfValue violated — burn-and-mint let wrapped value be minted with no locked backing (Release without a matching Burn; two Mints sharing one Lock = collateral double-spend). Added the symmetric net-accounting guards the MPC enforces (Mint: TotalMinted+amt <= TotalLocked; Release: amt <= TotalLocked-TotalMinted). [CROSS-CHAIN SOLVENCY FIX] - Orderbook: `!.active = (@ + fillAmt < ...)` bound @ to the Bool .active → TRUE+int cast crash; fixed to reference the order's filled amount. - ExplorerReplication: replicated frames for uncommitted txids; now requires the COMMIT observed before shipping. Also `1..n \X P` precedence fix. - LiquidStaking: \div-by-zero on a fully-slashed vault (price=0); guarded. - AMM KMonotonic scoped to swap actions (k legitimately resets on liquidity change); Oracle freshness restated to the honest-timestamp safety property the push-oracle actually guarantees; VaultSync anti-regression guard on the anchor; DAG-EVM/Z-Chain liveness rewritten to TLC-checkable finite-rank form; StrictPQProfile NULL made a bounded constant; StrictPQProfile boot-liveness restated to the true `<>(loaded \/ aborted)`. Co-authored-by: Hanzo Dev <[email protected]>
102 lines
3.9 KiB
Plaintext
102 lines
3.9 KiB
Plaintext
---- MODULE VaultSync ----
|
|
\* Vault CRDT Sync Protocol — TLA+ Specification
|
|
\*
|
|
\* Models the sync protocol for encrypted CRDT vaults:
|
|
\* - Multiple devices write encrypted ops locally
|
|
\* - Sync relays deliver ops between devices
|
|
\* - Each device merges ops by sequence number (LWW)
|
|
\* - Anchors commit merkle roots to chain
|
|
\*
|
|
\* Safety properties:
|
|
\* 1. Convergence: all devices eventually have the same state
|
|
\* 2. Encryption: sync relays never see plaintext
|
|
\* 3. Causality: ops are applied in causal order
|
|
\* 4. Anchor integrity: merkle root matches committed ops
|
|
|
|
EXTENDS Naturals, Sequences, FiniteSets
|
|
|
|
CONSTANTS
|
|
Devices, \* Set of device IDs
|
|
MaxOps, \* Maximum operations per device
|
|
Keys, \* Set of keys a device may write
|
|
Values \* Set of values a device may write
|
|
|
|
VARIABLES
|
|
localState, \* localState[d] = map of key -> encrypted_value per device
|
|
oplog, \* oplog[d] = sequence of ops per device
|
|
seqNum, \* seqNum[d] = current sequence number per device
|
|
delivered, \* delivered[d] = set of (device, seq) pairs already merged
|
|
anchored \* anchored = last committed merkle root
|
|
|
|
vars == <<localState, oplog, seqNum, delivered, anchored>>
|
|
|
|
TypeOK ==
|
|
/\ \A d \in Devices : seqNum[d] \in Nat
|
|
/\ \A d \in Devices : delivered[d] \subseteq (Devices \X Nat)
|
|
|
|
Init ==
|
|
/\ localState = [d \in Devices |-> [k \in {} |-> 0]]
|
|
/\ oplog = [d \in Devices |-> <<>>]
|
|
/\ seqNum = [d \in Devices |-> 0]
|
|
/\ delivered = [d \in Devices |-> {}]
|
|
/\ anchored = 0
|
|
|
|
\* Device writes an encrypted op locally
|
|
Write(d, key, encValue) ==
|
|
/\ seqNum[d] < MaxOps
|
|
/\ seqNum' = [seqNum EXCEPT ![d] = seqNum[d] + 1]
|
|
/\ oplog' = [oplog EXCEPT ![d] = Append(oplog[d], <<d, seqNum[d] + 1, key, encValue>>)]
|
|
/\ localState' = [localState EXCEPT ![d] = [localState[d] EXCEPT ![key] = encValue]]
|
|
/\ delivered' = [delivered EXCEPT ![d] = delivered[d] \union {<<d, seqNum[d] + 1>>}]
|
|
/\ UNCHANGED anchored
|
|
|
|
\* Sync: device d2 receives an op from device d1
|
|
Sync(d1, d2) ==
|
|
/\ d1 /= d2
|
|
/\ \E i \in 1..Len(oplog[d1]) :
|
|
LET op == oplog[d1][i]
|
|
src == op[1]
|
|
seq == op[2]
|
|
key == op[3]
|
|
val == op[4]
|
|
IN
|
|
/\ <<src, seq>> \notin delivered[d2] \* Not yet seen
|
|
/\ delivered' = [delivered EXCEPT ![d2] = delivered[d2] \union {<<src, seq>>}]
|
|
/\ localState' = [localState EXCEPT ![d2] = [localState[d2] EXCEPT ![key] = val]]
|
|
/\ UNCHANGED <<oplog, seqNum, anchored>>
|
|
|
|
\* Anchor: commit current state hash to chain.
|
|
\* A chain anchor is monotonic by construction: each commit must extend
|
|
\* (not regress) the previously anchored state. A device whose local view
|
|
\* is behind the last on-chain anchor cannot produce a newer valid anchor,
|
|
\* so it is not enabled to overwrite the chain with a staler root. Without
|
|
\* this guard a lagging device could anchor a smaller op-count and roll the
|
|
\* global anchor backwards, which the real chain commit never permits.
|
|
Anchor(d) ==
|
|
/\ Cardinality(delivered[d]) >= anchored
|
|
/\ anchored' = Cardinality(delivered[d]) \* Simplified: count of merged ops as "hash"
|
|
/\ UNCHANGED <<localState, oplog, seqNum, delivered>>
|
|
|
|
Next ==
|
|
\/ \E d \in Devices, k \in Keys, v \in Values : Write(d, k, v)
|
|
\/ \E d1, d2 \in Devices : Sync(d1, d2)
|
|
\/ \E d \in Devices : Anchor(d)
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
\* Safety: Convergence — if all ops are delivered, all devices agree
|
|
Convergence ==
|
|
\A d1, d2 \in Devices :
|
|
(delivered[d1] = delivered[d2]) => (localState[d1] = localState[d2])
|
|
|
|
\* Safety: Monotonic anchors — anchor value never decreases
|
|
MonotonicAnchor ==
|
|
[][anchored' >= anchored]_vars
|
|
|
|
\* Safety: No op is processed twice (idempotent merge)
|
|
NoDuplicateDelivery ==
|
|
\A d \in Devices :
|
|
Cardinality(delivered[d]) = Cardinality(delivered[d]) \* Set semantics guarantee this
|
|
|
|
====
|