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]>
90 lines
3.3 KiB
Plaintext
90 lines
3.3 KiB
Plaintext
---------------------------- MODULE MC_Teleport ------------------------------
|
|
(*
|
|
* Model Checking Wrapper for Teleport Bridge Protocol
|
|
*
|
|
* Instantiates Teleport.tla with concrete constants for tractable
|
|
* model checking.
|
|
*
|
|
* Parameters:
|
|
* - 2 chains: {"src", "dst"}
|
|
* - 2 tokens: {"LUX", "USDC"}
|
|
* - MaxAmount = 3 (amounts 0..3)
|
|
* - MaxNonce = 4 (nonces 1..4)
|
|
* - 3 signers: {"s1", "s2", "s3"}
|
|
*
|
|
* State space analysis:
|
|
* Per chain per token: locked(4) * minted(4) * backing(4) = 64
|
|
* 2 chains * 2 tokens: 64^4 = 16,777,216 balance states
|
|
* Nonces per chain: 2^4 = 16 subsets
|
|
* Pause per chain: 2^2 = 4
|
|
* Total: ~16M * 256 * 4 = ~16B (large but tractable with constraints)
|
|
* With state constraint (max 8 actions): explored in minutes.
|
|
*
|
|
* Usage:
|
|
* TLC: java -jar tla2tools.jar -config MC_Teleport.cfg MC_Teleport
|
|
* Apalache: apalache-mc check --config=MC_Teleport.cfg MC_Teleport.tla
|
|
*)
|
|
|
|
EXTENDS Teleport, TLC
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* CONCRETE CONSTANT VALUES
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_Chains == {"src", "dst"}
|
|
\* Single token. Every Teleport invariant (ConservationOfValue,
|
|
\* BackingInvariant, ExitGuarantee, NonNegativeBalances, NoncesFinite) is
|
|
\* of the form \A c \in Chains, t \in Tokens : P(c,t) with no term coupling
|
|
\* two distinct tokens -- tokens are independent ledgers. Checking one
|
|
\* token therefore verifies the identical logical content as many tokens,
|
|
\* while keeping the state space exhaustively checkable. (Two tokens
|
|
\* multiplied locked*minted*backing per cell into the tens of millions of
|
|
\* states; with the conservation violations fixed, search no longer
|
|
\* short-circuits, so that breadth must be fully explored.)
|
|
MC_Tokens == {"LUX"}
|
|
MC_MaxAmount == 3
|
|
MC_MaxNonce == 4
|
|
MC_Signers == {"s1", "s2", "s3"}
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* STATE CONSTRAINT (bound exploration for TLC)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
(*
|
|
* Limit the total number of processed nonces across all chains.
|
|
* This bounds state space without cutting reachable invariant violations.
|
|
*)
|
|
MC_MaxTotalNonces == 6
|
|
|
|
TotalNonceCount ==
|
|
SumOver([c \in MC_Chains |-> Cardinality(nonces[c])], MC_Chains)
|
|
|
|
StateConstraint ==
|
|
TotalNonceCount <= MC_MaxTotalNonces
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SYMMETRY (for TLC performance)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_ChainSymmetry == Permutations(MC_Chains)
|
|
MC_TokenSymmetry == Permutations(MC_Tokens)
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* INVARIANTS
|
|
\* --------------------------------------------------------------------------
|
|
|
|
MC_TypeOK == TypeOK
|
|
MC_BackingInvariant == BackingInvariant
|
|
MC_NonceInvariant == NonceInvariant
|
|
MC_ExitGuarantee == ExitGuarantee
|
|
MC_NonNegativeBalances == NonNegativeBalances
|
|
MC_NoncesFinite == NoncesFinite
|
|
|
|
(*
|
|
* ConservationOfValue: Mint now requires a corresponding Lock on a
|
|
* source chain, so this invariant is checkable by TLC.
|
|
*)
|
|
MC_ConservationOfValue == ConservationOfValue
|
|
|
|
=============================================================================
|