Verified Air

5. Creating an order from an offer🔗

Requirement ONE-001. Of its 5 acceptance criteria, 5 are proven.

rule

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

EARS: When a customer accepts an offer, the system shall create an order with one order item for each offer item and one service for each passenger and flight segment of that item.

Story: As an airline, I want each accepted offer item to become one order item with a service for every passenger and segment, so that each service can be delivered and accounted for on its own.

Acceptance criteria:

ONE-001.1: When an offer is accepted, the system shall create exactly one order item for each offer item.
ONE-001.2: When an order item is created, the system shall give it one service for each passenger and flight segment of its offer item.
ONE-001.3: When an order is created, the system shall give its order items distinct references.
ONE-001.4: When an order is created, the system shall mark it opened.
ONE-001.5: If a customer accepts an offer at or after its expiry instant, then the system shall reject it as expired.

The checks before creating the order are the same as in the airline's rules: expiry first, then an empty offer, then items priced in another currency.

5.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-001.1	Proven	One order item per offer item, Accept family offer
ONE-001.2	Proven	One service per passenger and segment, Accept family offer
ONE-001.3	Proven	Order item IDs are unique, Accept family offer
ONE-001.4	Proven	New orders are opened, Accept family offer
ONE-001.5	Proven	Accept rejects expired, Accept family at expiry

5.2. Guarantees🔗

5.2.1. One order item per offer item🔗

guarantee

Rules.OneOrder.accept_item_per_offer_item (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h : Rules.OneOrder.accept o now orderId = Except.ok ord) :
  List.map (fun x ↦ x.fromOfferItem) ord.items =
    List.map (fun x ↦ x.id) o.items
Rules.OneOrder.accept_item_per_offer_item
  (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.accept o now orderId =
      Except.ok ord) :
  List.map (fun x ↦ x.fromOfferItem)
      ord.items =
    List.map (fun x ↦ x.id) o.items

An accepted offer becomes an order with exactly one order item for each offer item, and each order item records the offer item it came from.

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

Checks acceptance criteria ONE-001.1.

5.2.2. One service per passenger and segment🔗

guarantee

Rules.OneOrder.accept_services_per_passenger_segment
  (o : Rules.OneOrder.Offer) (now : Rules.Core.Instant)
  (orderId : String) (ord : Rules.OneOrder.Order)
  (h : Rules.OneOrder.accept o now orderId = Except.ok ord) :
  List.map
      (fun x ↦ List.map (fun s ↦ (s.passenger, s.segment)) x.services)
      ord.items =
    List.map (fun oi ↦ oi.passengers ×ˢ oi.segments) o.items
Rules.OneOrder.accept_services_per_passenger_segment
  (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.accept o now orderId =
      Except.ok ord) :
  List.map
      (fun x ↦
        List.map
          (fun s ↦
            (s.passenger, s.segment))
          x.services)
      ord.items =
    List.map
      (fun oi ↦
        oi.passengers ×ˢ oi.segments)
      o.items

Each order item gets one service for each pair of a passenger and a flight segment of its offer item: the services' passengers and segments are exactly those pairs, each once.

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

Checks acceptance criteria ONE-001.2.

5.2.3. Order item IDs are unique🔗

guarantee

Rules.OneOrder.accept_item_ids_unique (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant) (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h : Rules.OneOrder.accept o now orderId = Except.ok ord)
  (hids : (List.map (fun x ↦ x.id) o.items).Nodup) :
  (List.map (fun x ↦ x.id) ord.items).Nodup
Rules.OneOrder.accept_item_ids_unique
  (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.accept o now orderId =
      Except.ok ord)
  (hids :
    (List.map (fun x ↦ x.id)
        o.items).Nodup) :
  (List.map (fun x ↦ x.id)
      ord.items).Nodup

When the offer's item references are distinct, the order's item references are distinct too: each is the order reference, a hyphen and the offer item reference.

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

Checks acceptance criteria ONE-001.3.

5.2.4. New orders are opened🔗

guarantee

Rules.OneOrder.accept_order_opened (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Offer) (now : Rules.Core.Instant)
  (orderId : String) (ord : Rules.OneOrder.Order)
  (h : Rules.OneOrder.accept o now orderId = Except.ok ord)
  (hne : ∀ oi ∈ o.items, oi.passengers ≠ [] ∧ oi.segments ≠ []) :
  Rules.OneOrder.orderStatuses v ord =
    [Rules.OneOrder.OrderStatus.opened]
Rules.OneOrder.accept_order_opened
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (ord : Rules.OneOrder.Order)
  (h :
    Rules.OneOrder.accept o now orderId =
      Except.ok ord)
  (hne :
    ∀ oi ∈ o.items,
      oi.passengers ≠ [] ∧
        oi.segments ≠ []) :
  Rules.OneOrder.orderStatuses v ord =
    [Rules.OneOrder.OrderStatus.opened]

An order is created opened, under every reading of the guide, when every offer item has a passenger and a flight segment: its services start confirmed, and a confirmed service holds value.

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

Checks acceptance criteria ONE-001.4.

5.2.5. Accept rejects expired🔗

guarantee

Rules.OneOrder.accept_rejects_expired (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant) (orderId : String)
  (h : now ≥ o.expiresAt) :
  Rules.OneOrder.accept o now orderId =
    Except.error Rules.OfferOrder.Rejection.expired
Rules.OneOrder.accept_rejects_expired
  (o : Rules.OneOrder.Offer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (h : now ≥ o.expiresAt) :
  Rules.OneOrder.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 ONE-001.5.

5.3. Examples🔗

5.3.1. Accept family offer🔗

example

Rules.OneOrder.acceptFamilyOffer :
  Except Rules.OfferOrder.Rejection Rules.OneOrder.Accepted
Rules.OneOrder.acceptFamilyOffer :
  Except Rules.OfferOrder.Rejection
    Rules.OneOrder.Accepted

Given the family offer: a return trip for two passengers at 900.00 EUR and an outbound bag for the first passenger at 40.00 EUR, valid until 2026-10-27 12:00 UTC.

When the customer accepts it at 11:59 UTC.

Then the order has two order items, one per offer item. The trip item holds four services (two passengers on two segments) and the bag item holds one. The order is opened.

What Lean computed:

Accepted. The result:

Item refs: ORD-ONE-1-OI-1, ORD-ONE-1-OI-2
From offer items: OI-1, OI-2
Service counts: 4, 1
Order status: opened

Checks acceptance criteria ONE-001.1, ONE-001.2, ONE-001.3, ONE-001.4, ONE-003.1.

5.3.2. Accept family at expiry🔗

example

Rules.OneOrder.acceptFamilyAtExpiry :
  Except Rules.OfferOrder.Rejection Rules.OneOrder.Accepted
Rules.OneOrder.acceptFamilyAtExpiry :
  Except Rules.OfferOrder.Rejection
    Rules.OneOrder.Accepted

Given the family 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 ONE-001.5.