2. Accepting an offer🔗

Requirement OO-001. Of its 5 acceptance criteria, 2 are proven and 3 are checked by examples only.

rule

Rules.OfferOrder.accept (o : Rules.OfferOrder.Offer)
  (now : Rules.Core.Instant) (orderId : String) :
  Except Rules.OfferOrder.Rejection Rules.OfferOrder.Order
Rules.OfferOrder.accept
  (o : Rules.OfferOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String) :
  Except Rules.OfferOrder.Rejection
    Rules.OfferOrder.Order

EARS: When a customer accepts an offer, the system shall create an order only if the offer has not expired and contains at least one item.

Story: As a customer, I want to accept an offer I was shown, so that I get an order for exactly those services at the offered price.

Acceptance criteria:

OO-001.1: If a customer accepts an offer at or after its expiry instant, then the system shall reject it as expired.
OO-001.2: If a customer accepts an unexpired offer that has no items, then the system shall reject it as empty.
OO-001.3: If a customer accepts an unexpired offer with an item priced in a currency other than the offer's, then the system shall reject it for mixed currencies.
OO-001.4: When a customer accepts an unexpired offer with at least one item and every item priced in the offer's currency, the system shall create an order.
OO-001.5: When an order is created from an offer, the system shall price the order at the sum of the offer's item prices.

The checks run in order: expiry first, then an empty offer, then items priced in a currency other than the offer's. The order's price is the sum of the item prices, in the offer's currency.

2.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
OO-001.1	Proven	Expired offers are rejected, Accept at expiry
OO-001.2	Example only	Accept empty offer
OO-001.3	Example only	Accept mixed currency
OO-001.4	Example only	Accept before expiry
OO-001.5	Proven	Accept before expiry, Order price is the sum of the items

2.2. Guarantees🔗

2.2.1. Expired offers are rejected🔗

guarantee

Rules.OfferOrder.accept_rejects_expired (o : Rules.OfferOrder.Offer)
  (now : Rules.Core.Instant) (orderId : String)
  (h : now ≥ o.expiresAt) :
  Rules.OfferOrder.accept o now orderId =
    Except.error Rules.OfferOrder.Rejection.expired
Rules.OfferOrder.accept_rejects_expired
  (o : Rules.OfferOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (h : now ≥ o.expiresAt) :
  Rules.OfferOrder.accept o now orderId =
    Except.error
      Rules.OfferOrder.Rejection.expired

An offer accepted at or after its expiry instant is always rejected as expired.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria OO-001.1.

2.2.2. Order price is the sum of the items🔗

guarantee

Rules.OfferOrder.accept_price_eq_sum (o : Rules.OfferOrder.Offer)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OfferOrder.Order)
  (h : Rules.OfferOrder.accept o now orderId = Except.ok ord) :
  ord.price.amount = (List.map (fun x ↦ x.price.amount) o.items).sum
Rules.OfferOrder.accept_price_eq_sum
  (o : Rules.OfferOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OfferOrder.Order)
  (h :
    Rules.OfferOrder.accept o now
        orderId =
      Except.ok ord) :
  ord.price.amount =
    (List.map (fun x ↦ x.price.amount)
        o.items).sum

When an offer is accepted, the order's price is exactly the sum of the offer's item prices: nothing is added or dropped.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria OO-001.5.

2.3. Examples🔗

2.3.1. Accept at expiry🔗

example

Rules.OfferOrder.acceptAtExpiry :
  Except Rules.OfferOrder.Rejection Rules.OfferOrder.Order
Rules.OfferOrder.acceptAtExpiry :
  Except Rules.OfferOrder.Rejection
    Rules.OfferOrder.Order

Given the sample offer, valid until 2026-10-27 12:00 UTC.

When the customer accepts it at 12:00 UTC, the expiry instant.

Then the offer is rejected as expired.

What Lean computed:

Rejected: expired.

Checks acceptance criteria OO-001.1.

2.3.2. Accept empty offer🔗

example

Rules.OfferOrder.acceptEmptyOffer :
  Except Rules.OfferOrder.Rejection Rules.OfferOrder.Order
Rules.OfferOrder.acceptEmptyOffer :
  Except Rules.OfferOrder.Rejection
    Rules.OfferOrder.Order

Given the sample offer with no items.

When the customer accepts it at 11:59 UTC, before expiry.

Then the offer is rejected as empty.

What Lean computed:

Rejected: empty offer.

Checks acceptance criteria OO-001.2.

2.3.3. Accept mixed currency🔗

example

Rules.OfferOrder.acceptMixedCurrency :
  Except Rules.OfferOrder.Rejection Rules.OfferOrder.Order
Rules.OfferOrder.acceptMixedCurrency :
  Except Rules.OfferOrder.Rejection
    Rules.OfferOrder.Order

Given the sample offer, priced in USD, with the bag priced at 40.00 EUR instead.

When the customer accepts it at 11:59 UTC, before expiry.

Then the offer is rejected for mixed currencies.

What Lean computed:

Rejected: mixed currency.

Checks acceptance criteria OO-001.3.

2.3.4. Accept before expiry🔗

example

Rules.OfferOrder.acceptBeforeExpiry :
  Except Rules.OfferOrder.Rejection Rules.OfferOrder.Order
Rules.OfferOrder.acceptBeforeExpiry :
  Except Rules.OfferOrder.Rejection
    Rules.OfferOrder.Order

Given the sample offer: a flight at 200.00 USD and a bag at 45.00 USD, valid until 2026-10-27 12:00 UTC.

When the customer accepts it at 11:59 UTC, one minute before expiry.

Then an order is created with both items, priced at 245.00 USD.

What Lean computed:

Accepted. The result:

Id: ORD-1
From offer: OFF-1
Items: see the table below.
Price: 245.00 USD
Created at: 2026-10-27 11:59 UTC

Items:

Id	From offer item	Price	Delivery
ORD-1-OI-1	OI-1	200.00 USD	ready
ORD-1-OI-2	OI-2	45.00 USD	ready

Checks acceptance criteria OO-001.4, OO-001.5.