Step 5 Proofs & Guarantees
System Invariants & State Machine
The 34 automated proofs implemented in scripts/verify-constraints.ts guaranteeing that the database rejects invalid states.
State MachinePASS
paid -> cancelled is illegal
constraint: orders_illegal_status_transition
sqlstate: 23514
State MachinePASS
rejected order is terminal
constraint: orders_illegal_status_transition
sqlstate: 23514
State MachinePASS
buyer cannot accept own order
constraint: orders_illegal_status_transition
sqlstate: 23514
State MachinePASS
seller cannot confirm delivery
constraint: orders_illegal_status_transition
sqlstate: 23514
State MachinePASS
unauthorized actor cannot transition
constraint: orders_actor_not_authorized
sqlstate: 42501
MoneyPASS
minor units never negative
constraint: minor_units_non_negative
sqlstate: 23514
MoneyPASS
order total equals subtotal + tax + shipping
constraint: orders_total_identity
sqlstate: 23514
MoneyPASS
line total equals price x quantity
constraint: order_items_line_total_identity
sqlstate: 23514
MoneyPASS
payment amount matches order total
constraint: payments_amount_matches_order_total
sqlstate: 23514
MoneyPASS
one live payment per order
constraint: payments_single_live_per_order
sqlstate: 23505
OwnershipPASS
single seller per order
constraint: order_items_single_seller_per_order
sqlstate: 23514
OwnershipPASS
seller profile requires seller role
constraint: seller_profiles_role_must_be_seller
sqlstate: 23514
ReviewsPASS
review requires delivered order
constraint: reviews_order_must_be_completed
sqlstate: 23514
ReviewsPASS
one review per order per author
constraint: reviews_one_per_order_per_author
sqlstate: 23505
UniquenessPASS
email case-insensitive unique
constraint: users_email_lower_key
sqlstate: 23505
UniquenessPASS
checkout retries idempotent per buyer
constraint: orders_buyer_idempotency_key
sqlstate: 23505
ImmutabilityPASS
paid orders frozen
constraint: order_items_immutable_after_payment
sqlstate: 42501