7. Order status🔗

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

rule

Rules.OneOrder.orderStatuses (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) : List Rules.OneOrder.OrderStatus
Rules.OneOrder.orderStatuses
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  List Rules.OneOrder.OrderStatus

EARS: The system shall mark an order opened while any of its services holds value, and closed once all its items are closed or cancelled and all its services are delivered or removed.

Story: As an airline, I want an order's status worked out from its items and services, so that an order is closed only when nothing in it holds value.

Acceptance criteria:

ONE-003.1: While at least one service of an order holds value, the system shall mark the order opened.
ONE-003.2: When every item of an order is closed or cancelled and every service is delivered or removed, the system shall mark the order closed.
ONE-003.3: The system shall never mark an order both opened and closed.
ONE-003.4: The system shall give every order that has a service either the status opened or the status closed.

The result lists every status whose condition holds.

7.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-003.1	Proven	Opened orders are those holding value, Accept family offer
ONE-003.2	Proven	Delivered order, Closed orders as the guide defines them
ONE-003.3	Proven	Orders are never both opened and closed
ONE-003.4	Open	Expired service, Every order is opened or closed

7.2. Guarantees🔗

7.2.1. Opened orders are those holding value🔗

guarantee

Rules.OneOrder.order_opened_iff (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  Rules.OneOrder.OrderStatus.opened ∈ Rules.OneOrder.orderStatuses v o ↔
    ∃ i ∈ o.items,
      ∃ s ∈ i.services, Rules.OneOrder.Service.holdsValue v s = true
Rules.OneOrder.order_opened_iff
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  Rules.OneOrder.OrderStatus.opened ∈
      Rules.OneOrder.orderStatuses v o ↔
    ∃ i ∈ o.items,
      ∃ s ∈ i.services,
        Rules.OneOrder.Service.holdsValue
            v s =
          true

An order is marked opened exactly when at least one of its services holds value.

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

Checks acceptance criteria ONE-003.1.

7.2.2. Closed orders as the guide defines them🔗

guarantee

Rules.OneOrder.order_closed_iff (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  Rules.OneOrder.OrderStatus.closed ∈ Rules.OneOrder.orderStatuses v o ↔
    (∀ i ∈ o.items,
        i.isClosed = true ∨
          Rules.OneOrder.OrderItem.isCancelled v i = true) ∧
      ∀ i ∈ o.items,
        ∀ s ∈ i.services,
          s.delivery = Rules.OneOrder.DeliveryStatus.delivered ∨
            s.delivery = Rules.OneOrder.DeliveryStatus.removed
Rules.OneOrder.order_closed_iff
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  Rules.OneOrder.OrderStatus.closed ∈
      Rules.OneOrder.orderStatuses v o ↔
    (∀ i ∈ o.items,
        i.isClosed = true ∨
          Rules.OneOrder.OrderItem.isCancelled
              v i =
            true) ∧
      ∀ i ∈ o.items,
        ∀ s ∈ i.services,
          s.delivery =
              Rules.OneOrder.DeliveryStatus.delivered ∨
            s.delivery =
              Rules.OneOrder.DeliveryStatus.removed

An order is marked closed exactly when every item is closed or cancelled and every service is delivered or removed.

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

Checks acceptance criteria ONE-003.2.

7.2.3. Orders are never both opened and closed🔗

guarantee

Rules.OneOrder.opened_closed_exclusive (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  ¬(Rules.OneOrder.Order.isOpened v o = true ∧
      Rules.OneOrder.Order.isClosed v o = true)
Rules.OneOrder.opened_closed_exclusive
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order) :
  ¬(Rules.OneOrder.Order.isOpened v o =
        true ∧
      Rules.OneOrder.Order.isClosed v o =
        true)

An order is never both opened and closed, under every reading of the guide.

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

Checks acceptance criteria ONE-003.3.

7.2.4. Every order is opened or closed🔗

guarantee

Rules.OneOrder.order_opened_or_closed (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (h : (o.items.any fun x ↦ decide (x.services ≠ [])) = true) :
  Rules.OneOrder.orderStatuses v o ≠ []
Rules.OneOrder.order_opened_or_closed
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (h :
    (o.items.any fun x ↦
        decide (x.services ≠ [])) =
      true) :
  Rules.OneOrder.orderStatuses v o ≠ []

Every order with at least one service is opened or closed.

Open question for the business. The guide closes an order only when every service is delivered or removed, and keeps it opened only while a service holds value. It does not say whether an expired, not claimed or failed service holds value. Under a reading where an expired service holds none, an order whose only service expired is neither opened nor closed. The example expiredService shows it. Does an expired service hold value, and should an order with one be closed?

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

Checks acceptance criteria ONE-003.4.

7.3. Examples🔗

7.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.

7.3.2. Delivered order🔗

example

Rules.OneOrder.deliveredOrder : Rules.OneOrder.OrderStatuses
Rules.OneOrder.deliveredOrder :
  Rules.OneOrder.OrderStatuses

Given an order whose one item holds a delivered flight and a removed bag.

When the order's status is worked out.

Then it is closed under both readings.

What Lean computed:

Cautious: closed
Strict: closed

Checks acceptance criteria ONE-003.2.

7.3.3. Expired service🔗

example

Rules.OneOrder.expiredService : Rules.OneOrder.OrderStatuses
Rules.OneOrder.expiredService :
  Rules.OneOrder.OrderStatuses

Given an order whose one flight service expired because the customer did not claim it in time.

When the order's status is worked out.

Then under the cautious reading it stays opened, because the expired service holds value. Under the strict reading it is neither opened nor closed: no service holds value, and the expired service is neither delivered nor removed.

What Lean computed:

Cautious: opened
Strict: none

Checks acceptance criteria ONE-003.4.

7.4. Open question🔗

The guarantee Every order is opened or closed is open: the example Expired service shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.