mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
ac9676a47a
The formal/lean library (53 files — a separate formalization from lean/) had ~110 type-check errors across 38 files and had never had its Mathlib oleans built. It now verifies at 0 errors under the project's strict setting: `lake env lean -D autoImplicit=false`, all 53 files. Fixed the same families as the sibling lean/ tree (the content is diverged, so each was repaired directly): - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE/Verkle): omega needs in-scope structure invariants; Nat-division bounds; noncomputable over opaque verifiers; Fin n index → Nat; deriving Inhabited. - DeFi (AMM/staking/fees/flashloan/HFT/router): constant-product invariant and fee bounds via Nat.div_mul_le_self / Nat.div_le_of_le_mul; dead tactics. - Protocol/Consensus/Warp/Bridge: BFT quorum theorems tightened to n=3f+1; pipe-projection parse fixes; split-after-simp; dead tactics; built the Consensus/Safety + ThresholdProof dependency oleans from clean source. - Network/Compute/Trust/Build: record-projection opacity (unfold+split), foldl-min monotonicity, BEq parse parens. - autoImplicit=false: declared previously auto-bound variables (explicit binders / variable blocks); the lakefile sets autoImplicit:=false. Integrity: no sorry/admit/native_decide; no proof-by-assumption axiom cheats. Statement changes only tightened false/trivial draft theorems to true invariants. Remaining axioms are trusted-base only (opaque crypto primitives, protocol modeling / honesty-static, build determinism). Co-authored-by: Hanzo Dev <[email protected]>
88 lines
2.8 KiB
Lean4
88 lines
2.8 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 s' : DestState) (msg : WarpMessage)
|
||
(h : processMessage s msg = some s') :
|
||
s.processedNonces ⊆ s'.processedNonces := by
|
||
unfold processMessage at h
|
||
split at h
|
||
· exact absurd h (by simp)
|
||
· split at h
|
||
· exact absurd h (by simp)
|
||
· rw [Option.some.injEq] at h
|
||
rw [← h]
|
||
exact Finset.subset_union_left
|
||
|
||
end Warp.Delivery
|