26. Repeated create requests🔗

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

rule

Rules.OneOrder.Creation.createOnce
  (h : Rules.OneOrder.Creation.RepeatHandling)
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (book : List Rules.OneOrder.Creation.CreatedOrder)
  (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 × List Rules.OneOrder.Creation.CreatedOrder)
Rules.OneOrder.Creation.createOnce
  (h :
    Rules.OneOrder.Creation.RepeatHandling)
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (book :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (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 ×
      List
        Rules.OneOrder.Creation.CreatedOrder)

EARS: When a seller sends a create request, the system shall create the order and record the offers it came from, unless an offer it names has already produced an order.

Story: As a seller, I want a request I send again after a timeout to give me the order I already have, so that the customer is not booked twice.

Acceptance criteria:

ONE-403.1: When a create request that names no offer with an order is accepted, the system shall record the new order against every offer it names.
ONE-403.2: Where the airline returns the existing order for a repeated request, the system shall answer a request that names an offer which already produced an order with a recorded order from one of its offers, and record no new order.
ONE-403.3: Where the airline rejects repeated requests, the system shall reject a request that names an offer which already produced an order.
ONE-403.4: The system shall create at most one order from each offer.

A request that names an offer with an order is handled as the reading of the guide says (RepeatHandling). A new order is created as createOrder says, under its own reading. When it names offers from more than one recorded order, the first recorded order is the existing one.

26.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-403.1	Proven	New orders are recorded against their offers, Repeated request
ONE-403.2	Proven	Repeated request, Repeated requests get the existing order
ONE-403.3	Proven	Repeated requests can be rejected, Repeated request
ONE-403.4	Open	Repeated request, One order per offer

26.2. Guarantees🔗

26.2.1. New orders are recorded against their offers🔗

guarantee

Rules.OneOrder.Creation.create_once_records
  (hd : Rules.OneOrder.Creation.RepeatHandling)
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (book : List Rules.OneOrder.Creation.CreatedOrder)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order)
  (book' : List Rules.OneOrder.Creation.CreatedOrder)
  (hfresh :
    ∀ e ∈ book,
      Rules.OneOrder.Creation.CreatedOrder.fromAny req e = false)
  (h :
    Rules.OneOrder.Creation.createOnce hd m book offers req now
        orderId =
      Except.ok (ord, book')) :
  Rules.OneOrder.Creation.createOrder m offers req now orderId =
      Except.ok ord ∧
    book' =
      book ++
        [{ offers := List.map (fun x ↦ x.offer) req, order := ord }]
Rules.OneOrder.Creation.create_once_records
  (hd :
    Rules.OneOrder.Creation.RepeatHandling)
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (book :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (book' :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (hfresh :
    ∀ e ∈ book,
      Rules.OneOrder.Creation.CreatedOrder.fromAny
          req e =
        false)
  (h :
    Rules.OneOrder.Creation.createOnce hd
        m book offers req now orderId =
      Except.ok (ord, book')) :
  Rules.OneOrder.Creation.createOrder m
        offers req now orderId =
      Except.ok ord ∧
    book' =
      book ++
        [{
            offers :=
              List.map (fun x ↦ x.offer)
                req,
            order := ord }]

A request that names no offer with an order gets the order createOrder creates, recorded against every offer it names, under every reading of both parameters.

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

Checks acceptance criteria ONE-403.1.

26.2.2. Repeated requests get the existing order🔗

guarantee

Rules.OneOrder.Creation.repeat_returns_existing
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (book : List Rules.OneOrder.Creation.CreatedOrder)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (hused :
    ∃ e ∈ book,
      Rules.OneOrder.Creation.CreatedOrder.fromAny req e = true) :
  ∃ e ∈ book,
    Rules.OneOrder.Creation.CreatedOrder.fromAny req e = true ∧
      Rules.OneOrder.Creation.createOnce
          Rules.OneOrder.Creation.RepeatHandling.returnExisting m book
          offers req now orderId =
        Except.ok (e.order, book)
Rules.OneOrder.Creation.repeat_returns_existing
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (book :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (hused :
    ∃ e ∈ book,
      Rules.OneOrder.Creation.CreatedOrder.fromAny
          req e =
        true) :
  ∃ e ∈ book,
    Rules.OneOrder.Creation.CreatedOrder.fromAny
          req e =
        true ∧
      Rules.OneOrder.Creation.createOnce
          Rules.OneOrder.Creation.RepeatHandling.returnExisting
          m book offers req now orderId =
        Except.ok (e.order, book)

Where the airline returns the existing order, a request that names an offer with an order is answered with an order recorded for one of the offers it names, and nothing new is recorded.

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

Checks acceptance criteria ONE-403.2.

26.2.3. Repeated requests can be rejected🔗

guarantee

Rules.OneOrder.Creation.repeat_rejected
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (book : List Rules.OneOrder.Creation.CreatedOrder)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (hused :
    ∃ e ∈ book,
      Rules.OneOrder.Creation.CreatedOrder.fromAny req e = true) :
  ∃ r,
    Rules.OneOrder.Creation.createOnce
        Rules.OneOrder.Creation.RepeatHandling.reject m book offers req
        now orderId =
      Except.error r
Rules.OneOrder.Creation.repeat_rejected
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (book :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (hused :
    ∃ e ∈ book,
      Rules.OneOrder.Creation.CreatedOrder.fromAny
          req e =
        true) :
  ∃ r,
    Rules.OneOrder.Creation.createOnce
        Rules.OneOrder.Creation.RepeatHandling.reject
        m book offers req now orderId =
      Except.error r

Where the airline rejects repeated requests, a request that names an offer with an order is rejected.

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

Checks acceptance criteria ONE-403.3.

26.2.4. One order per offer🔗

guarantee

Rules.OneOrder.Creation.once_per_offer
  (hd : Rules.OneOrder.Creation.RepeatHandling)
  (m : Rules.OneOrder.Creation.MultiOfferHandling)
  (book : List Rules.OneOrder.Creation.CreatedOrder)
  (offers : List Rules.OneOrder.Creation.MarkedOffer)
  (req : List Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order)
  (book' : List Rules.OneOrder.Creation.CreatedOrder)
  (hbook : Rules.OneOrder.Creation.OncePerOffer book)
  (h :
    Rules.OneOrder.Creation.createOnce hd m book offers req now
        orderId =
      Except.ok (ord, book')) :
  Rules.OneOrder.Creation.OncePerOffer book'
Rules.OneOrder.Creation.once_per_offer
  (hd :
    Rules.OneOrder.Creation.RepeatHandling)
  (m :
    Rules.OneOrder.Creation.MultiOfferHandling)
  (book :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (offers :
    List
      Rules.OneOrder.Creation.MarkedOffer)
  (req :
    List
      Rules.OneOrder.Creation.Selection)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (book' :
    List
      Rules.OneOrder.Creation.CreatedOrder)
  (hbook :
    Rules.OneOrder.Creation.OncePerOffer
      book)
  (h :
    Rules.OneOrder.Creation.createOnce hd
        m book offers req now orderId =
      Except.ok (ord, book')) :
  Rules.OneOrder.Creation.OncePerOffer
    book'

No offer ever produces two orders: once an offer appears in a recorded order, no request adds another order for it.

Open question for the business. The sources do not say that creating an order uses up its offer. Under the reading where the airline creates another order for a repeated request, a request sent again after a timeout gives the customer a second order from the same offer. The example repeatedRequest shows it. Does creating an order use up its offer, and how does the airline recognize a request it has already answered?

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

Checks acceptance criteria ONE-403.4.

26.3. Examples🔗

26.3.1. Repeated request🔗

example

Rules.OneOrder.Creation.repeatedRequest :
  List Rules.OneOrder.Creation.RepeatRow
Rules.OneOrder.Creation.repeatedRequest :
  List Rules.OneOrder.Creation.RepeatRow

Given the trip offer, and no order created from it yet.

When a seller sends a create request for the flight, the request times out at the seller, and the seller sends it again.

Then the first request creates order ORD-5 and records it against the trip offer. The repeated request is answered with ORD-5 where the airline returns the existing order, and rejected where it rejects repeated requests. Where the airline creates another order, the seller gets ORD-6 and the trip offer has produced two orders.

What Lean computed:

Request	Handling	Answer	Rejection	Orders from offer
first request	reject	ORD-5	none	1
same request again	return existing	ORD-5	none	1
same request again	reject	none	offer used ORD-5	1
same request again	create again	ORD-6	none	2

Checks acceptance criteria ONE-403.1, ONE-403.2, ONE-403.3, ONE-403.4.

26.4. Open question🔗

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