R-Share

Each business books capacity over an interval: a room for three nights, a seat at a show, a bike for an hour, a car for a day, a machine for an operating window. Each is paid before use and settled after. The unit, the interval, and the policy change; the flow is booking, escrow, settlement.

Most rental software rebuilds that flow per vertical, inside one operator’s database with a payment integration beside it. That gives the operator the record and the funds, and makes every new vertical a new booking engine. Most on-chain projects have repeated the vertical product rather than the shared flow.

R-Share is one set of concurrent booking, escrow, and settlement contracts that every vertical reuses by changing kind, attrs, slot IDs, terms, and at most one pure Remedy branch. No vertical adds a booking arm.

The listing has two units and six nightly slots. A guest booking both rooms for the full stay asks for all six; the allocator writes all six in one commit or writes none. No partial hold is possible.

The booking carries terms, hold, escrow, confirm, check-in, check-out, settle. Each booking has its own state cell, ticket projection, operation map, and a bond holding the escrow purse. Cancellation, no-show, deposit claims, disputes, and arbitration are on the same path, and settlement runs through R-Cash. The core is four primitives: capacity, interval, escrow, and policy. Calendar, identity, support, insurance, telemetry, and regulation are the fork’s product.

Each rung adds a real-world constraint: whether listing to unit to slot to booking still fits. A new rung changes kind, attrs, slot IDs, and at most one pure Remedy branch. It does not change the booking machine, escrow, settlement buckets, or authority model. A rung that needs a new booking arm means the primitive set is wrong.

Holiday letting is the reference path: a two-room house, three nights, one deposit, one cancellation policy, followed from terms to settlement. Robotics-as-a-service is the furthest case: machine windows, operators, certification, session evidence, and SLAs. The shared path is implemented; the RaaS-specific evidence and safety pieces are design. In the table, “pass” means a recorded suite or arm; “mapping only” means the use case rides the shared path without its own suite.

The allocator uses the tuple space — the shared pool of messages Rholang processes take from and put back — to arbitrate, with no lock and no global cell. A booking takes all requested slots in one commit or none.

Lean proves that after a successful acquire, every active reservation containing a requested slot belongs to the acquiring booking. It also proves that an acquire either refuses and leaves the state unchanged, or appends exactly one reservation. The proof is over the model, not a Rholang refinement.

The client shows how to use the contracts; it is not the product. The repository ships the contracts, a Rust SDK, a CLI, a WASM wallet, and a React reference client. There is no backend server, indexer, or off-chain database. The chain is the backend.

The campaign covers the same surface from three directions: a CLI journey (quote, book, held-slot refusal, replay, wrong-terms refusal, manual accept and cancel, one-signature refusal, two-signature pause and resume), browser journeys for guest, provider, and admin-multisig, and seven real settlement scenarios over a closed balance set with a negative control for untracked escrow.

Fork it: keep the AGPL notices, copy the contracts, harness, tools, crates, and web app, and change the kind, the attrs, the slot IDs, the terms, and at most one pure Remedy branch. The off-chain parts are yours. R-Share is the settlement core; R-Cash is the payment rail; neither is a marketplace.

On 3 November 2026, a fresh devnet built from Rholo e2d073d with R-Cash 49b441d recorded 16 passing suites, covering root, payments, lifecycle, claims, pricing, booking, pause, allocator, admin, events, provider, listing, and conservation. Claim coverage is 20 of 30 cells; four claim classes run across five kinds.

The allocator suite checks atomic multi-slot acquisition, token-gated confirm and release, pause gates, expiry takeover, and no slot-capability leak. Conservation covers seven settlement scenarios with a closed balance set and a negative control. Lean records 37 axiom audits, 21 vectors, 33 rules, 29 arms, and 13 core arms proved-model; these are internal checks, not a security audit.