teleport/PROOF-CLAIMS.md

PROOF-CLAIMS — luxfi/teleport

Honest scope of what this submission proves. The bridge endpoint contracts (Bridge.sol, BridgeV2.sol, StrictPQProfileGate.sol) and the off-chain services (api/, mpc/) are a composition of external primitives (Pulsar, Corona, FROST, CGGMP21, ECDSA-GG18, the Warp 2.0 envelope verifier, the Lux EVM precompile suite). This document states explicitly which properties live HERE (bridge endpoint) and which live UPSTREAM (in the primitive's own repository).

1. What this submission proves

Claim P1 — Strict-PQ gate refusal symmetry

For any profile p ∈ {classical-compat, quasar-strict-pq} and any verifier contract V that exposes IPolicyId.policyId() returns (bytes32), the destination-chain endpoint BridgeV2 refuses to authorise a mint via claim(env, c) or claimWithProof(env, c, π) if and only if StrictPQProfileGate.refuseUnderStrictPQ(p, V) would revert.

Why this matters. A bridge that accepts a classical verifier under a strict-PQ profile would let an admin (or a compromised operations key) silently downgrade the bridge to BN254 / BLS12-381 / KZG. The gate refuses such downgrades symmetrically across claim and claimWithProof — one path cannot accept what the other refuses.

Realization. contracts/test/BridgeV2.test.ts cases (a)-(n) and contracts/test/StrictPQProfileGate.test.ts cases 1-7. Both test files execute the entire 2×3 matrix of profile × verifier policy and assert the refusal predicate is identical to the canonical helper.

Assumption. The Solidity compiler 0.8.20 implements keccak256 and extcodehash correctly. (Standard cryptographic / EVM assumption; not in scope to re-prove.)

Claim P2 — MPC-side profile coherence

For any (LUX_PROFILE, MPC_SCHEME) pair, the resolver resolveSchemeFromEnv in mpc/src/signers/index.ts returns a value in the admissible set declared in the profile matrix (SPEC §4.2) if and only if the input pair satisfies the same predicate. There is no silent classical fallback under quasar-strict-pq and no silent PQ fallback under classical-compat.

Why this matters. Red HIGH #4: a missing env config used to mean "silent ECDSA on a strict-PQ deployment". The resolver throws an explicit error with remediation text if LUX_PROFILE is unset.

Realization. mpc/__tests__/signers.test.ts cases under "registry" (4 cases), "LUX_PROFILE → MPC_SCHEME derivation" (8 cases). Every cell of the 4 × 6 (profile × scheme) matrix is exercised.

Assumption. Node.js's process.env semantics are as documented (string-coerced values; undefined only when explicitly deleted).

Claim P3 — Envelope binding

For any envelope env and claim c, BridgeV2.claim(env, c) reverts unless env.messageHash == keccak256(abi.encode(c.sourceChainId, c.destChainId, c.token, c.amount, c.recipient, c.vault, c.nonce)) AND env.destChainId == uint64(block.chainid) AND env.sourceChainId == c.sourceChainId.

Why this matters. Without envelope binding, a Warp 2.0 envelope authorising "amount=1, recipient=Alice" on chain X could be replayed against claim with amount=1000, recipient=Bob — the envelope verifier would accept (the bytes are still validly signed), but the mint would be unauthorised. Binding env.messageHash to the claim's abi.encode of all mint parameters closes this attack.

Realization. contracts/test/BridgeV2.test.ts deployFixture constructs an envelope+claim pair that matches; tampering with any claim field is rejected by EnvelopeBindingMismatch.

Assumption. keccak256 is collision-resistant.

Claim P4 — Replay protection on envelope ID

For any envelope env, BridgeV2.claim(env, ...) succeeds at most once: the second call with the same env.messageHash reverts with MessageAlreadyUsed.

Why this matters. Standard cross-chain replay protection. The canonical envelope ID is identical across Warp v1 and v2 (per luxfi/warp/envelope.go line 207-212), so the same usedMessages map catches cross-version reuse.

Realization. Implicit in the test suite (any second-call test would assert revert); the storage map is mapping(bytes32 => bool) public usedMessages and is set inside _processClaim.

Assumption. EVM SSTORE is durable across transactions.

Claim P5 — EXTCODEHASH defence-in-depth

For any verifier address V installed via setActiveProfile or setP3QVerifier under PROFILE_QUASAR_STRICT_PQ, the bytecode hash extcodehash(V) MUST be in allowedVerifierCodeHashes. The allow-list is mutable only by DEFAULT_ADMIN_ROLE (multi-sig + timelock), which is distinct from ADMIN_ROLE (operations key).

Why this matters. Section C residual (Red round 5): a verifier returning policyId() == POLICY_STARK_FRI_SHA3_PQ but verify() returning true for any input would pass the policy-id check alone. The code-hash gate refuses to install ANY verifier whose bytecode hash is not pre-allowed. A compromised ADMIN_ROLE can swap among already-vetted verifiers but cannot install a "true-returning" one.

Realization. contracts/test/BridgeV2.test.ts cases (i)-(n).

Assumption. extcodehash is a hash of deployed bytecode at the queried address; CREATE2 collisions would require breaking keccak256.

Claim P6 — Decomplecting policy from verification

The verifier verifies its proof. The gate decides admissibility. No braiding. Specifically, the helpers StrictPQProfileGate.refuseUnderStrictPQ and the OnlyStrictPQ modifier are pure policy: they call policyId() and extcodehash and compare against constants. They do NOT call verify(). Verifiers are free to be slow / complex / probabilistic; the gate decides admissibility in O(1) work.

Why this matters. Mixing policy with verification was the bug in the old gate (a verifier could return a "policyId" that depended on runtime state, opening a TOCTOU window between gate check and verify call). The current gate reads policyId() AND extcodehash BEFORE any verify() call.

Realization. Reading the contract source: refuseUnderStrictPQ calls verifier.policyId() exactly once, compares against the allow-list, then returns. No verify() call.

2. What this submission does NOT prove

Non-claim N1 — Primitive security

The bridge endpoint does NOT prove that Pulsar (M-LWE) is secure, that Corona (R-LWE) is secure, that FROST is EUF-CMA-secure for secp256k1, that CGGMP21 is simulation-secure, that BLS12-381 is unforgeable, or that ML-DSA-65 is post-quantum-secure. Those proofs live in the respective primitives' repositories:

Primitive	Repo	Proof location
Pulsar M-LWE threshold	luxfi/pulsar	PROOF-CLAIMS.md, EasyCrypt + Lean bridge + Jasmin
Corona R-LWE threshold	luxfi/corona	docs/mptc/ + SPEC.md
FROST	upstream RFC 9591	RFC + reference implementations
CGGMP21	upstream paper	"UC Non-Interactive, Proactive, Threshold ECDSA with Identifiable Aborts" (CCS 2020)
BLS12-381	upstream IETF	RFC 9380 (hash-to-curve), draft-irtf-cfrg-bls-signature
ML-DSA-65	NIST FIPS 204	FIPS 204 with NIST-led analysis

A break of any single primitive does not invalidate the bridge's composition proof (P1-P6 above); it invalidates the primitive's security. The composition is "if the primitive is secure, the bridge's strict-PQ slot inherits that security."

Non-claim N2 — Source-chain finality

The bridge endpoint does NOT verify source-chain finality on-chain. A source-chain reorg AFTER the envelope was signed but BEFORE the claim was issued can produce a spurious mint. The mitigation lives in the off-chain pipeline:

• The relay/oracle service waits min_confirmations per asset (e.g. 6 for Bitcoin, finality+epochs for Ethereum) before submitting to the MPC signer.
• The validator set's signing pipeline relies on the relay's commit policy.

This is a deliberate scope choice: trustless source-chain header verification requires light clients (IEthereumLightClient.sol, ILuxLightClient.sol), which are a separate engineering track documented in WARP2_BRIDGE.md §"Trustless Bridge Roadmap" and CLAUDE.md §"Trustless Light Client Bridge".

Non-claim N3 — Custody-quorum integrity

The bridge endpoint does NOT prove that the M-Chain custody quorum is honest. The bridge sees only signed messages; if the quorum signs an unauthorised release, the bridge cannot detect this from the destination-chain side. The mitigation lives in M-Chain's own proof scope (LP-7330):

• M-Chain validator set is independently selected (subset of Lux validators with custody-specific staking).
• Per-asset MPC key sets are refreshed on a schedule (LSS — Live Secret Sharing).
• Watchdog services compare announced signatures against the relay's observed signing requests.

Non-claim N4 — Destination-chain reorg

The bridge endpoint does NOT defend against destination-chain reorgs beyond the storage durability of usedMessages. A destination-chain reorg that rolls back a BridgeMintedV2 event would mark the messageHash as un-used again. The mitigation is the standard "wait for destination finality" pattern in the relayer / user UX.

Non-claim N5 — Privacy

This bridge endpoint is NOT a private bridge. The BridgeBurnedV2 event reveals (token, sender, amount, destChainId, recipient, vault, nonce) in cleartext on the source chain. The BridgeMintedV2 event reveals (token, recipient, net, fee, epoch) on the destination chain. Privacy bridges (FHE-based, Bulletproofs) were removed in commit 49522d3 and are not part of this Tier A surface. See CHANGELOG.md for the removal rationale.

Non-claim N6 — Constant-time guarantees

The Solidity surface is not subject to a constant-time guarantee — EVM operations are charged per opcode but secret-dependent branches still leak via gas. The off-chain primitives (Pulsar / Corona / FROST / CGGMP21 via mpcd) carry their own constant-time evidence in their own repositories (luxfi/pulsar/CRYPTOGRAPHER-SIGN-OFF.md §"dudect" etc.). The bridge endpoint inherits whatever the primitive provides; it does not add side-channel guarantees of its own.

3. Theorem framing — refusal symmetry

We make the symmetry of P1 explicit because it is the load-bearing property for the strict-PQ deployment model.

Theorem (informal). Let B be a BridgeV2 instance with profile activeProfile = p and slot verifier activeVerifier = V. Let refuse(p, V) := StrictPQProfileGate.refuseUnderStrictPQ(p, V) reverts (a Boolean predicate). Then:

  for all envelope env, claim c, proof π :
      B.claim(env, c)                  reverts ⇒
              refuse(p, V) ∨ (¬ valid_envelope ∨ ¬ valid_binding ∨ ¬ valid_mint)

  for all envelope env, claim c, proof π :
      B.claimWithProof(env, c, π)      reverts ⇒
              refuse(p, IPolicyId(p3qVerifier)) ∨
              p3qVerifier == address(0) ∨
              ¬ p3qVerifier.verify(π, env.messageHash) ∨
              refuse(p, V) ∨ (¬ valid_envelope ∨ ¬ valid_binding ∨ ¬ valid_mint)

The first disjunct in each case is the profile-gate refusal, and it is identical between the two entrypoints (modulo the slot it queries — activeVerifier for claim, p3qVerifier for claimWithProof). This is realized by both entrypoints calling the same canonical helper (OnlyStrictPQ.refuseUnderStrictPQ from @luxfi/pq-profile-ids).

Why this is the load-bearing property. Suppose an attacker compromises ADMIN_ROLE and tries to install a Groth16 verifier under strict-PQ. Under the symmetric refusal:

1. setActiveProfile(strict-PQ, groth16_addr) reverts (VerifierRefusedUnderStrictPQ(strict-PQ, POLICY_GROTH16_BN254)).
2. The attacker tries setP3QVerifier(groth16_addr). Reverts with the same error (because setP3QVerifier calls the same canonical helper).
3. The attacker tries to deploy a MockVerifier(POLICY_STARK_FRI_SHA3_PQ) that returns true from verify(). Reverts because extcodehash(mock) is not in allowedVerifierCodeHashes.
4. The attacker tries to extend the allow-list. Reverts because setAllowedVerifierCodeHash requires DEFAULT_ADMIN_ROLE (the timelocked governance role), not ADMIN_ROLE.

The composition of P1 + P5 + P6 closes every install path. A compromised operations key cannot install a "true-returning" verifier in any of the strict-PQ slots.

4. Evidence inventory

Property	Test	Location
P1 Refusal symmetry, classical profile	(a)	contracts/test/BridgeV2.test.ts
P1 Refusal symmetry, strict-PQ profile	(b), (c)	contracts/test/BridgeV2.test.ts
P1 Unknown profile rejection	(g) + StrictPQ#4	contracts/test/BridgeV2.test.ts + StrictPQProfileGate.test.ts
P1 claimWithProof mirror of claim	(d), (e)	contracts/test/BridgeV2.test.ts
P2 Profile coherence (resolver)	"LUX_PROFILE → MPC_SCHEME derivation" suite (8 cases)	mpc/__tests__/signers.test.ts
P2 Fail-closed on unset profile	"throws when LUX_PROFILE is unset"	mpc/__tests__/signers.test.ts
P3 Envelope binding	implicit in claim happy-path	contracts/test/BridgeV2.test.ts
P4 Replay protection	implicit (second call would revert)	contracts/test/BridgeV2.test.ts
P5 EXTCODEHASH allow-list	(i), (j), (k), (l), (m), (n)	contracts/test/BridgeV2.test.ts
P6 Decomplecting	code review	contracts/contracts/BridgeV2.sol, StrictPQProfileGate.sol

Additional NEW tests in this Tier A pass (see contracts/test/ and mpc/__tests__/):

Test	Property
bridge_e2e_test.ts	Full cross-chain bridge flow under PQ-default profile (LUX_PROFILE=quasar-strict-pq)
custody_mpc_e2e_test.ts	MPC ceremony round-trip across all six schemes with profile gating
oracle_attestation_e2e_test.ts	EIP-712 / ML-DSA-65 envelope signing parity vs @luxfi/wallet KAT
signature_fuzz_test.ts	Fuzz: envelope serializer, double-lattice splitter, hex / u32be / u64be helpers
profile_negative_test.ts	Classical-default attempts blocked under strict-PQ

Each test is checked into the repository and runs in CI.