25. Creating one order from several offers🔗

Requirement ONE-402. Of its 5 acceptance criteria, 1 is proven and 4 are open.

rule

Rules.OneOrder.Creation.createOrder
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String) :
  Except Rules.OneOrder.Creation.CreateRejection Rules.OneOrder.Order
Rules.OneOrder.Creation.createOrder
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String) :
  Except
    Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Order

EARS: When a seller sends a create request with selections from one or more offers, the system shall check each selection and create one order from them, or reject the request.

Story: As a customer, I want a trip I chose as a whole to be ordered as a whole, so that I never hold half of it.

Acceptance criteria:

ONE-402.1: When a create request is accepted, the system shall create one order item for each item selected from each offer and none for the items left out.
ONE-402.2: When an order is created from offers priced in one currency, the system shall make the order's total price the sum of the prices of the selected items.
ONE-402.3: If any offer named in a create request has expired at the instant of the request, then the system shall reject the whole request and create no order.
ONE-402.4: If a create request selects no item from any offer, then the system shall reject it.
ONE-402.5: When an order is created, the system shall be able to state its total price in a single currency.

Each selection is checked as orderItemsFor says. What happens when one is rejected depends on the reading of the sources (MultiOfferHandling, pickItems). The order's total is the sum of its item prices when they share a currency (Rules.OneOrder.Change.orderPrice), since the guide no longer stores a total on the order.

25.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
ONE-402.1	Open	Order items match the selection, One offer expired, Trip without bag
ONE-402.2	Open	One offer expired, Trip without bag, Order price is the sum of the selected items
ONE-402.3	Open	One offer expired, Atomic order creation
ONE-402.4	Proven	Requests that select nothing are rejected, Nothing selected
ONE-402.5	Open	Order total from item prices, Two currencies

25.2. Guarantees🔗

25.2.1. Order items match the selection🔗

guarantee

Rules.OneOrder.Creation.create_items_match_selection
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.Creation.createOrder m offers req now orderId =
      Except.ok ord) :
  ord.items =
    List.flatMap
      (fun s ↦
        List.map
          (Rules.OneOrder.toOrderItem
            (Rules.OneOrder.Creation.itemPrefix orderId s.offer))
          (Rules.OneOrder.Creation.selectedFrom offers s))
      req
Rules.OneOrder.Creation.create_items_match_selection
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.Creation.createOrder m
        offers req now orderId =
      Except.ok ord) :
  ord.items =
    List.flatMap
      (fun s ↦
        List.map
          (Rules.OneOrder.toOrderItem
            (Rules.OneOrder.Creation.itemPrefix
              orderId s.offer))
          (Rules.OneOrder.Creation.selectedFrom
            offers s))
      req

An accepted request becomes an order whose items are, for each selection in turn, the items it selects from its offer and no others, under both readings.

Open question for the business. The sources allow one request to select from several offers and do not say what happens when one of them is rejected. Under the reading where the selections that pass go ahead, the items selected from a rejected offer are left out of the order. The example oneOfferExpired shows it: the return flight selected from an expired offer has no order item. Does a rejected offer reject the whole request, or do the offers that pass go ahead?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-402.1.

25.2.2. Order price is the sum of the selected items🔗

guarantee

Rules.OneOrder.Creation.create_price_eq_sum
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order) (c : Rules.Core.Currency)
  (h :
    Rules.OneOrder.Creation.createOrder m offers req now orderId =
      Except.ok ord)
  (hc :
    ∀ s ∈ req,
      ∀ o ∈ offers, o.offer.id = s.offer → o.offer.currency = c) :
  Rules.OneOrder.Change.orderPrice ord c =
    some
      {
        amount :=
          (List.map (fun x ↦ x.price.amount)
              (List.flatMap
                (Rules.OneOrder.Creation.selectedFrom offers) req)).sum,
        currency := c }
Rules.OneOrder.Creation.create_price_eq_sum
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (c : Rules.Core.Currency)
  (h :
    Rules.OneOrder.Creation.createOrder m
        offers req now orderId =
      Except.ok ord)
  (hc :
    ∀ s ∈ req,
      ∀ o ∈ offers,
        o.offer.id = s.offer →
          o.offer.currency = c) :
  Rules.OneOrder.Change.orderPrice ord c =
    some
      {
        amount :=
          (List.map
              (fun x ↦ x.price.amount)
              (List.flatMap
                (Rules.OneOrder.Creation.selectedFrom
                  offers)
                req)).sum,
        currency := c }

An order created from offers priced in one currency has a total in that currency, the sum of the prices of the selected items, under both readings.

Open question for the business. Under the reading where the selections that pass go ahead, the items selected from a rejected offer are left out, and the order costs less than the items selected. The example oneOfferExpired shows it: the selected items cost 780.00 EUR and the order 400.00 EUR. Does a rejected offer reject the whole request, or do the offers that pass go ahead?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-402.2.

25.2.3. Atomic order creation🔗

guarantee

Rules.OneOrder.Creation.create_rejects_expired
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (s : Rules.OneOrder.Creation.Selection) (hs : s ∈ req)
  (o : Rules.OneOrder.Creation.MarkedOffer)
  (ho : List.find? (fun x ↦ x.offer.id == s.offer) offers = some o)
  (hexp : now ≥ o.offer.expiresAt) :
  ∃ e,
    Rules.OneOrder.Creation.createOrder m offers req now orderId =
      Except.error e
Rules.OneOrder.Creation.create_rejects_expired
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (s : Rules.OneOrder.Creation.Selection)
  (hs : s ∈ req)
  (o :
    Rules.OneOrder.Creation.MarkedOffer)
  (ho :
    List.find?
        (fun x ↦ x.offer.id == s.offer)
        offers =
      some o)
  (hexp : now ≥ o.offer.expiresAt) :
  ∃ e,
    Rules.OneOrder.Creation.createOrder m
        offers req now orderId =
      Except.error e

A request that names an offer which has expired at the instant of the request is rejected as a whole, under both readings: no order is created.

Open question for the business. The sources allow one request to select from several offers and do not say what happens when one of them has expired or fails its checks. Under the reading where the selections that pass go ahead, an order is created from the valid offer alone, and the customer holds half of a trip chosen as a whole. The example oneOfferExpired shows it. Does a rejected offer reject the whole request, or do the offers that pass go ahead?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-402.3.

25.2.4. Requests that select nothing are rejected🔗

guarantee

Rules.OneOrder.Creation.create_rejects_empty
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (hempty :
    ∀ s ∈ req, Rules.OneOrder.Creation.selectedFrom offers s = []) :
  ∃ e,
    Rules.OneOrder.Creation.createOrder m offers req now orderId =
      Except.error e
Rules.OneOrder.Creation.create_rejects_empty
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (hempty :
    ∀ s ∈ req,
      Rules.OneOrder.Creation.selectedFrom
          offers s =
        []) :
  ∃ e,
    Rules.OneOrder.Creation.createOrder m
        offers req now orderId =
      Except.error e

A request that selects no item from any offer is rejected, under both readings.

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

Checks acceptance criteria ONE-402.4.

25.2.5. Order total from item prices🔗

guarantee

Rules.OneOrder.Creation.create_single_currency
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.Creation.createOrder m offers req now orderId =
      Except.ok ord) :
  ∃ c, (Rules.OneOrder.Change.orderPrice ord c).isSome = true
Rules.OneOrder.Creation.create_single_currency
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.Creation.createOrder m
        offers req now orderId =
      Except.ok ord) :
  ∃ c,
    (Rules.OneOrder.Change.orderPrice ord
          c).isSome =
      true

Every order created has a total price in a single currency, under both readings.

Open question for the business. Each offer is checked for its own currency, and a request may select from offers priced in different currencies. The order then holds items in two currencies, and its item prices have no sum. The example twoCurrencies shows it: a flight priced in EUR and a hotel transfer priced in USD go into one order that has no total. May one order hold items priced in more than one currency, and if so, what is its total?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-402.5.

25.3. Examples🔗

25.3.1. One offer expired🔗

example

Rules.OneOrder.Creation.oneOfferExpired :
  List Rules.OneOrder.Creation.MultiOfferRow
Rules.OneOrder.Creation.oneOfferExpired :
  List
    Rules.OneOrder.Creation.MultiOfferRow

Given the trip offer, valid until 12:00 UTC, and a return flight offer that expired at 11:00 UTC.

When a seller sends one create request at 11:30 UTC for the outbound flight at 400.00 EUR from the first offer and the return flight at 380.00 EUR from the second.

Then where a rejected offer rejects the whole request, the request is rejected because the return offer has expired, and no order is created. Where the offers that pass go ahead, an order is created for the outbound flight alone: the return flight the seller selected has no order item, and the order costs 400.00 EUR against 780.00 EUR selected.

What Lean computed:

Handling	Selected items cost	Order items	Order total	Rejection
whole request	780.00 EUR	none	none	expired OFF-B
passing offers	780.00 EUR	ORD-2-OFF-A-OI-FLT	400.00 EUR	none

Checks acceptance criteria ONE-402.1, ONE-402.2, ONE-402.3.

25.3.2. Trip without bag🔗

example

Rules.OneOrder.Creation.tripWithoutBag :
  Except Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.CreatedSummary
Rules.OneOrder.Creation.tripWithoutBag :
  Except
    Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.CreatedSummary

Given the trip offer: a flight at 400.00 EUR, a bag at 40.00 EUR and a seat at 25.00 EUR, valid until 12:00 UTC.

When a seller sends a create request at 11:30 UTC for the flight and the seat, leaving out the bag.

Then the order holds two items, the flight and the seat, and no bag. Its total is 425.00 EUR, the price of the flight and the seat.

What Lean computed:

Accepted. The result:

Item refs: ORD-1-OFF-A-OI-FLT, ORD-1-OFF-A-OI-SEAT
From offer items: OI-FLT, OI-SEAT
Total: 425.00 EUR

Checks acceptance criteria ONE-402.1, ONE-402.2.

25.3.3. Nothing selected🔗

example

Rules.OneOrder.Creation.nothingSelected :
  Except Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.CreatedSummary
Rules.OneOrder.Creation.nothingSelected :
  Except
    Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.CreatedSummary

Given the a la carte offer, which marks no item mandatory.

When a seller sends a create request that selects nothing from it.

Then the request is rejected, since the order would hold no item.

What Lean computed:

Rejected: no items.

Checks acceptance criteria ONE-402.4.

25.3.4. Two currencies🔗

example

Rules.OneOrder.Creation.twoCurrencies :
  Except Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.TotalsCase
Rules.OneOrder.Creation.twoCurrencies :
  Except
    Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.TotalsCase

Given the trip offer, priced in euros, and a hotel transfer offer at 60.00 USD, priced in US dollars. Both are valid until 12:00 UTC.

When a seller sends one create request at 11:30 UTC for the flight and the transfer.

Then the order is created with a flight at 400.00 EUR and a transfer at 60.00 USD. It has no total in any currency.

What Lean computed:

Accepted. The result:

Items: see the table below.
Totals: see the table below.

Items:

Item	Price
ORD-4-OFF-A-OI-FLT	400.00 EUR
ORD-4-OFF-D-OI-TRF	60.00 USD

Totals:

Currency	Total
EUR	none
USD	none
GBP	none

Checks acceptance criteria ONE-402.5.

25.4. Open question🔗

The guarantee Order items match the selection is open: the example One offer expired, Trip without bag shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

25.5. Open question🔗

The guarantee Order price is the sum of the selected items is open: the example One offer expired, Trip without bag shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

25.6. Open question🔗

The guarantee Atomic order creation is open: the example One offer expired shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

25.7. Open question🔗

The guarantee Order total from item prices is open: the example Two currencies shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.