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]>
63 lines
2.1 KiB
INI
63 lines
2.1 KiB
INI
\* MC_Quasar.cfg -- TLC / Apalache model checking configuration
|
|
\*
|
|
\* Run with TLC:
|
|
\* java -jar tla2tools.jar -config MC_Quasar.cfg MC_Quasar
|
|
\*
|
|
\* Run with Apalache:
|
|
\* apalache-mc check --config=MC_Quasar.cfg MC_Quasar.tla
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SPECIFICATION
|
|
\* --------------------------------------------------------------------------
|
|
|
|
SPECIFICATION Spec
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* CONSTANTS
|
|
\* --------------------------------------------------------------------------
|
|
|
|
CONSTANTS
|
|
N <- MC_N
|
|
F <- MC_F
|
|
QuorumNum <- MC_QuorumNum
|
|
QuorumDen <- MC_QuorumDen
|
|
EnableBLS <- MC_EnableBLS
|
|
EnableRT <- MC_EnableRT
|
|
EnableMLDSA <- MC_EnableMLDSA
|
|
Values <- MC_Values
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* STATE CONSTRAINT (bounds state space for tractable checking)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
CONSTRAINT StateConstraint
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* INVARIANTS (checked at every reachable state)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
INVARIANT MC_TypeOK
|
|
INVARIANT MC_Safety
|
|
INVARIANT MC_QuantumUnforgeability
|
|
INVARIANT MC_ByzAloneCannotReachQuorum
|
|
INVARIANT MC_HonestSignsAtMostOne
|
|
INVARIANT MC_HonestLayerConsistency
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* TEMPORAL PROPERTIES
|
|
\* --------------------------------------------------------------------------
|
|
|
|
\* Finalized decisions never change (action property)
|
|
PROPERTY MC_FinalizedStable
|
|
|
|
\* Liveness: will produce counterexample under nondeterminism (expected).
|
|
\* Uncomment to verify counterexample exists:
|
|
\*
|
|
\* PROPERTY MC_Liveness
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SYMMETRY (reduces state space when Values has 2+ elements)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
\* SYMMETRY MC_Symmetry
|