How REF's three layers — cryptographic, consensus, and economic — compose through explicit contracts. What each layer assumes, what it guarantees, how it degrades, and where the composition risks lie.
Click each layer to expand its full assume-guarantee contract, including the specific degradation modes when assumptions are violated.
A-CRYPTO: Discrete log hardness over BN254. Poseidon collision
resistance (128-bit). Ed25519 SUF-CMA unforgeability.
A-PTAU: Hermez Powers-of-Tau ceremony secure (≥1 of 1,088
contributors honest).
A-MERCHANT: Merchants faithfully attest to real purchases.
P-AUTH: Every review bound to a verified purchase.
P-UNIQ: One purchase → one review (nullifier uniqueness).
P-INTEG: Tokens immutable after issuance.
P-PRIV: No PII in proofs or tokens. (v1: partial — att_hash public.)
Unforgeable tokens with sound ZK proofs. Domain-separated commitments that prevent cross-protocol replay. Binding from attestation through token to nullifier — the purchase-to-review chain.
A-CRYPTO broken: Soundness failure — fake proofs accepted. Detection: none
at protocol level (catastrophic). Mitigation: algorithm agility via versioned domain tags.
A-PTAU compromised: Adversary can forge proofs for any statement. Mitigation:
Phase 2 transition to PLONKish universal setup (no per-circuit trust).
A-MERCHANT dishonest: Phantom attestations. Mitigation: economic (merchant bonds),
not cryptographic. See ATK-3 in THREAT_MODEL.md.
A-BFT: f < ⌊c/3⌋ Byzantine validators per committee.
A-NET: Partial synchrony — messages eventually delivered after
GST (Global Stabilization Time).
Crypto layer sound: Tokens reaching consensus are unforgeable
(P-AUTH, P-UNIQ hold from below).
G-SAFETY: No conflicting QCs for the same sequence number.
G-LIVENESS: Valid submissions eventually finalized (after GST).
G-FINALITY: QC is unforgeable proof of consensus agreement.
G-ATOMICITY: Nullifier-spend and review-publish are a single atomic transition.
Finalized verification decisions. Immutable nullifier set. Atomic state transitions that cannot be partially applied. The "double-spend prevention" guarantee that underpins economic deterrence.
A-BFT violated (≥ ⌈c/3⌉ Byzantine): Conflicting QCs may be produced.
Detection: any observer holding two QCs for the same (view, seq) with different digests
has cryptographic slashing evidence. Degradation: slashing of offending validators;
committee re-election.
A-NET violated (permanent partition): Liveness degrades — finalization
stalls. Safety is preserved (no timing assumption for safety). Detection: validators
that cannot reach ≥ 2f+1 peers for > 64Δ enter safe-degrade mode.
Dominance condition: α·C₀·Nγ > k holds
(verified: 500 MC runs, 100% hold, 652× min margin).
Consensus safety: No conflicting QCs (G-SAFETY from above).
Crypto soundness: Tokens unforgeable — fraud requires real purchases,
not proof forgery (P-AUTH from above).
P-IC: Honesty is the dominant strategy for all actors.
Marginal cost of fraud exceeds marginal reward at v=0.
P-IR: Participation is individually rational.
(Market-justified via FTC Rule 465 penalties, not formally proven.)
G-DETERRENCE: Fraud is economically irrational at any scale.
End-to-end trustworthiness. The compound guarantee: reviews are cryptographically bound, consensus-finalized, and economically defended. The three layers compose to make fake reviews both impossible to forge and unprofitable to attempt.
Dominance condition fails (α·C₀·Nγ ≤ k): Fraud becomes
profitable. Detection: runtime dominance guard checks on parameter updates —
changes that would violate the guard are rejected. Degradation: automatic parameter
adjustment or operator alert.
Consensus safety fails: Economic model loses its foundation — adversary
can double-spend without paying. This cascading failure is why consensus layer integrity
is load-bearing.
Four cryptographic properties are enforced by mathematics. Two economic properties are enforced by mechanism design. Each has a defined verification artifact and status.
This is REF's top-level assurance claim. It is a structured argument, not a formal theorem in the proof-theoretic sense. Each conjunct is backed by a specific verification artifact.
Two conjuncts are not at full strength: P-PRIV is partial in v1
(att_hash is a public input, enabling linkage by observers with merchant records),
and P-IR is market-justified rather than formally proven. The compound
claim holds at full strength only when both are resolved — P-PRIV via v2 Merkle membership,
P-IR via formal game-theoretic treatment.
The critical question is whether the three layers compose cleanly. We have identified one specific composition risk that is documented but not formally resolved.
If the economic layer reveals information about merchant behavior (e.g., bond amounts correlating with fraud suspicion levels), this could leak information that degrades the privacy guarantee (P-PRIV) provided by the crypto layer.
The specific vector: An observer who can see both the merchant's bond tier and the public token stream can infer the merchant's risk profile — even though the cryptographic layer guarantees no PII leaks through proofs or tokens. The information doesn't leak through crypto; it leaks around crypto via the economic layer's observable parameters.
Status: This cross-layer leakage is acknowledged in the threat model. Formal resolution requires either: (a) making bond amounts uniform across merchants (eliminating the correlation vector but weakening risk-proportional deterrence), or (b) proving that the leaked information is insufficient for practical de-anonymization (a quantitative information flow analysis). Neither has been completed.
In assume-guarantee reasoning, each layer's guarantees must hold independently of what other layers reveal. If the economic layer's observable behavior leaks information that the crypto layer promised to hide, the composition is not clean — the privacy guarantee depends on the economic layer's information profile, creating a circular dependency.
This is not a flaw in the architecture — it is an inherent tension between risk-proportional economic deterrence and privacy. Formally characterizing this tension (e.g., via differential privacy budgets or quantitative information flow) is the next research step.
The token lifecycle spec (EV-009) proves purchase-to-review binding. The consensus spec (EV-008) proves agreement and finality. The connection is that consensus assumes tokens are valid — and the crypto layer guarantees they are. This link is documented in THREAT_MODEL.md §6.3 as an explicit contract.
The economic model (EV-012) proves honesty dominance given that consensus prevents double-spending. If consensus safety fails, the cost function's base assumption breaks — an adversary who can double-spend has zero marginal cost. The dominance condition α·C₀·Nγ > k implicitly requires G-SAFETY from the consensus layer.
The assume-guarantee contracts are documented and structured (THREAT_MODEL.md §6), but the composition itself is not machine-checked. There is no Coq/Isabelle proof that crypto guarantees + consensus guarantees + economic guarantees compose to the compound trustworthiness claim. The composition argument is currently maintained through human-authored traceability. Formally verifying composition is a Phase 2 objective requiring EasyCrypt or a similar tool.