mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
2d7e2a6309
The lean/ library (112 files) had ~110 type-check errors across 52 files (the
prior "green" status was a grep artifact). It now verifies at 0 errors under
the project's strict setting: `lake env lean -D autoImplicit=false`, all 112
files.
Fixed:
- Quasar/Consensus: replaced `by native_decide` with `by decide` (kernel-checked
rather than compiler-trusted).
- Vault/KeyIsolation, Bridge/{YieldVault,OmnichainRouter,FillIntegrity},
Storage/{ZapDB,Replicate}: PRF/string-encoding lemmas, division-bound vault
accounting, renamed/removed deprecated List lemmas, noncomputable.
- Crypto (Pulsar/Magnetar/Corona/CGGMP21/MLKEM/FROST/FHE/P3Q): missing local
dependency oleans compiled in dependency order; theorem→noncomputable def for
Type-valued re-exports; deriving Inhabited for opaque artifact types; dead
Mathlib imports removed.
- DeFi (AMM/staking/fees/flashloan/HFT/router) + Protocol + GPU + Warp + Trust +
Compute + Network + Build: Nat-division/AMM-invariant proofs via
Nat.div_le_of_le_mul / Nat.div_mul_le_self; omega in-scope invariants;
record-projection opacity; dead tactics; stale Nat.Basic import → Nat.Defs;
BFT quorum theorems tightened to n=3f+1.
Integrity: no sorry/admit/native_decide remaining (verified); no
proof-by-assumption axiom cheats. Statement changes only tightened false draft
theorems to true invariants. Remaining axioms are trusted-base only (opaque
crypto groups/pairings, RLWE/MLWE/MSIS hardness, FIPS 203/204/205 correctness,
VSS/Paillier, protocol modeling).
Co-authored-by: Hanzo Dev <[email protected]>
84 lines
2.7 KiB
Lean4
84 lines
2.7 KiB
Lean4
/-
|
||
Warp Cross-Chain Exactly-Once Delivery
|
||
|
||
Models the Warp messaging protocol used for cross-chain communication.
|
||
|
||
Warp messages carry BLS aggregate signatures from source chain validators.
|
||
The destination chain verifies the aggregate signature against the known
|
||
validator set before processing.
|
||
|
||
Maps to:
|
||
- src/precompiles/warp/: Warp precompile at 0x0200...0005
|
||
- treasury/Vault.sol: usedNonces mapping for replay protection
|
||
- treasury/Collect.sol: version monotonicity for settings
|
||
|
||
Properties:
|
||
- Authenticity: only messages signed by source validators are accepted
|
||
- No replay: each message processed at most once (nonce tracking)
|
||
- No loss: valid messages eventually delivered (under liveness assumption)
|
||
- Combined: exactly-once delivery
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Data.Finset.Basic
|
||
import Mathlib.Tactic
|
||
|
||
namespace Warp.Delivery
|
||
|
||
/-- Chain identifier -/
|
||
abbrev ChainId := Nat
|
||
|
||
/-- Warp message -/
|
||
structure WarpMessage where
|
||
sourceChain : ChainId
|
||
destChain : ChainId
|
||
nonce : Nat
|
||
payload : Nat -- hash of payload
|
||
sigValid : Bool -- BLS aggregate signature valid
|
||
|
||
/-- Destination chain state for Warp processing -/
|
||
structure DestState where
|
||
processedNonces : Finset Nat -- nonces already processed
|
||
lastProcessed : Nat -- monotonic counter
|
||
|
||
/-- Process a Warp message -/
|
||
def processMessage (s : DestState) (msg : WarpMessage) : Option DestState :=
|
||
if ¬msg.sigValid then none -- reject invalid signature
|
||
else if msg.nonce ∈ s.processedNonces then none -- reject replay
|
||
else some {
|
||
processedNonces := s.processedNonces ∪ {msg.nonce}
|
||
lastProcessed := max s.lastProcessed msg.nonce
|
||
}
|
||
|
||
/-- No replay: a processed nonce is never accepted again -/
|
||
theorem no_replay (s : DestState) (msg : WarpMessage)
|
||
(hmem : msg.nonce ∈ s.processedNonces) :
|
||
processMessage s msg = none := by
|
||
simp [processMessage]
|
||
intro _
|
||
exact hmem
|
||
|
||
/-- Authenticity: only valid signatures are processed -/
|
||
theorem authenticity (s : DestState) (msg : WarpMessage)
|
||
(hinv : msg.sigValid = false) :
|
||
processMessage s msg = none := by
|
||
simp [processMessage, hinv]
|
||
|
||
/-- Valid messages succeed on first attempt -/
|
||
theorem valid_message_succeeds (s : DestState) (msg : WarpMessage)
|
||
(hsig : msg.sigValid = true)
|
||
(hfresh : msg.nonce ∉ s.processedNonces) :
|
||
∃ s', processMessage s msg = some s' := by
|
||
simp [processMessage, hsig, hfresh]
|
||
|
||
/-- Processed nonces grow monotonically -/
|
||
theorem nonces_monotone (s : DestState) (msg : WarpMessage) (s' : DestState)
|
||
(h : processMessage s msg = some s') :
|
||
s.processedNonces ⊆ s'.processedNonces := by
|
||
simp [processMessage] at h
|
||
obtain ⟨_, _, h2⟩ := h
|
||
subst h2
|
||
exact Finset.subset_union_left
|
||
|
||
end Warp.Delivery
|