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]>
81 lines
2.9 KiB
Plaintext
81 lines
2.9 KiB
Plaintext
---------------------------- MODULE MC_Quasar -------------------------
|
|
(*
|
|
* Model Checking Wrapper for Quasar Consensus Protocol
|
|
*
|
|
* Instantiates Quasar.tla with concrete constants for tractable
|
|
* model checking.
|
|
*
|
|
* Parameters: N=4, F=1
|
|
* - 4 validators, at most 1 Byzantine (3*1=3 < 4)
|
|
* - QuorumNum=2, QuorumDen=3 (2/3 quorum, standard BFT)
|
|
* Quorum check: sigWeight * 3 >= 4 * 2 = 8, so need sigWeight >= 3
|
|
* With 1 Byzantine, honest can contribute 3. Meets quorum.
|
|
* - All three layers enabled (quantum mode)
|
|
* - Two values to decide (tests conflict detection)
|
|
*
|
|
* State space analysis:
|
|
* Per validator per value per layer: 2 (signed or not)
|
|
* 3 layers * 4 validators * 2 values = 24 boolean vars
|
|
* Plus finalized[2], finalVal[2], byz(subset of 4), round
|
|
* Total: ~2^24 * 16 * bound ~ tractable with round bound 8
|
|
*
|
|
* Usage:
|
|
* TLC: java -jar tla2tools.jar -config MC_Quasar.cfg MC_Quasar
|
|
* Apalache: apalache-mc check --config=MC_Quasar.cfg MC_Quasar.tla
|
|
*)
|
|
|
|
EXTENDS Quasar, TLC
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* CONCRETE CONSTANT VALUES
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_N == 4
|
|
MC_F == 1
|
|
MC_QuorumNum == 3
|
|
MC_QuorumDen == 4
|
|
MC_EnableBLS == TRUE
|
|
MC_EnableRT == TRUE
|
|
MC_EnableMLDSA == TRUE
|
|
MC_Values == {"v1", "v2"}
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* STATE CONSTRAINT (bound exploration for TLC)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_RoundBound == 8
|
|
|
|
StateConstraint ==
|
|
round <= MC_RoundBound
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* INVARIANTS
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_TypeOK == TypeOK
|
|
MC_Safety == Safety
|
|
MC_QuantumUnforgeability == QuantumUnforgeability
|
|
MC_ByzAloneCannotReachQuorum == ByzAloneCannotReachQuorum
|
|
MC_HonestSignsAtMostOne == HonestSignsAtMostOne
|
|
MC_HonestLayerConsistency == HonestLayerConsistency
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* TEMPORAL PROPERTIES
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_FinalizedStable == [][FinalizedStableAction]_vars
|
|
|
|
\* Liveness will produce counterexamples because honest nodes may never
|
|
\* converge on a single value under pure nondeterminism. This is expected;
|
|
\* Wave/Snow pre-consensus provides probabilistic convergence.
|
|
\* Uncomment in .cfg to verify the counterexample exists:
|
|
MC_Liveness == Liveness
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SYMMETRY (reduces state space for 2+ values)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_Symmetry == Permutations(MC_Values)
|
|
|
|
=============================================================================
|