Marketplace Form
The Marketplace form defines a decentralized marketplace with five state fields — listing_price (Nat per ID), listing_seller (Address per ID), active (Bool per ID), fee_rate (Nat), and fee_recipient (Address) — and proves the fee cap invariant fee_rate <= 1000 at compile time, bounding marketplace fees to a maximum of 10% (1000 basis points). The compiler performs bounds analysis across all transitions to verify that fee_rate never exceeds this threshold, guaranteeing that the fee calculation fee = price * fee_rate / 10000 is bounded by price / 10 for every purchase. The proven invariant is erased from WASM output, producing zero-overhead verified marketplace contracts deployable to CosmWasm, Near, Stylus, and Polkadot.
form Marketplace { state { listing_price : Nat per ID listing_seller : Address per ID active : Bool per ID fee_rate : Nat fee_recipient : Address } invariant fee_cap : fee_rate <= 1000 transition list(id, price) { require price > 0 require !active[id] listing_price[id] = price listing_seller[id] = msg.sender active[id] = true } -- fee_cap: list does not modify fee_rate, invariant trivially preserved transition buy(id) { require active[id] let fee = listing_price[id] * fee_rate / 10000 let payout = listing_price[id] - fee send(listing_seller[id], payout) send(fee_recipient, fee) active[id] = false } -- fee_cap: fee_rate <= 1000 => fee <= price * 1000 / 10000 = price / 10 -- buy does not modify fee_rate, invariant trivially preserved }
State Fields
listing_price : Nat per ID — maps each listing ID to its asking price. Set by the seller during the list transition.
listing_seller : Address per ID — maps each listing ID to the seller's address. Recorded as msg.sender when the listing is created.
active : Bool per ID — maps each listing ID to its active status. True when listed, false after purchase. Prevents double-purchase and listing overwrites.
fee_rate : Nat — the marketplace fee rate in basis points (out of 10000). Invariant-bounded to at most 1000 (10%).
fee_recipient : Address — the address that receives marketplace fees on each purchase.
Invariant: Fee Cap
The fee cap invariant fee_rate <= 1000 bounds the marketplace fee to a maximum of 10%. The compiler proves this through bounds analysis:
List: Does not modify fee_rate. The invariant is trivially preserved — no write means no violation possible.
Buy: Does not modify fee_rate. The invariant is trivially preserved. Additionally, the fee calculation fee = listing_price * fee_rate / 10000 is bounded: since fee_rate <= 1000, fee <= price * 1000 / 10000 = price / 10. The compiler derives this upper bound algebraically.
Initialization: The initial state must satisfy fee_rate <= 1000. The compiler checks this at deploy time. Since no transition writes to fee_rate, the bound holds for all subsequent states.
Transitions
list(id, price) — creates a new listing. Requires price > 0 (no zero-price listings) and !active[id] (no overwriting existing active listings). Records the seller and price, then activates the listing.
buy(id) — purchases a listed item. Requires active[id]. Computes the fee as price * fee_rate / 10000, sends the payout (price minus fee) to the seller and the fee to the fee_recipient, then deactivates the listing. The fee is provably bounded by price / 10 due to the fee cap invariant.
Frequently Asked Questions
- What invariants does a Marketplace form prove?
- The Marketplace form proves the fee cap invariant: fee_rate <= 1000, bounding marketplace fees to a maximum of 10% (1000 basis points out of 10000). The compiler verifies that no transition can set fee_rate above this threshold, ensuring that the fee calculation in the buy transition is always bounded by price / 10. Buyers and sellers are protected from excessive fee extraction by construction, not by convention.
- How does Formagine verify the fee cap invariant?
- The compiler performs bounds analysis on fee_rate across all transitions. Since neither list nor buy writes to fee_rate, and the initial state must satisfy fee_rate <= 1000 (checked at deploy time), the invariant is preserved trivially — no transition can violate a constraint on a variable it never modifies. The compiler then derives the consequence: fee = price * fee_rate / 10000 <= price * 1000 / 10000 = price / 10, bounding the fee algebraically.
- How does the Marketplace form handle listing and purchasing?
- The list transition records price and seller (msg.sender), activates the listing, and requires !active[id] to prevent overwrites. The buy transition requires active[id], splits the payment between seller (price minus fee) and fee_recipient (fee), then deactivates the listing. The active flag acts as a mutex: each listing can only be purchased once, and deactivated listings cannot be relisted without a new list call.
- What chains can the Marketplace form compile to?
- The Marketplace form compiles to optimized WASM targeting CosmWasm (Cosmos ecosystem), Near Protocol, Arbitrum Stylus (Ethereum L2), and Polkadot (ink! contracts). The same form definition produces verified marketplace contracts for all targets with identical fee cap and listing-integrity guarantees.