27. Recording changes to an order🔗

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

rule

Rules.OneOrder.Creation.recordChanges
  (r : Rules.OneOrder.Creation.OrderRecord)
  (g : Rules.OneOrder.Creation.ChangeGroup) :
  Rules.OneOrder.Creation.OrderRecord
Rules.OneOrder.Creation.recordChanges
  (r :
    Rules.OneOrder.Creation.OrderRecord)
  (g :
    Rules.OneOrder.Creation.ChangeGroup) :
  Rules.OneOrder.Creation.OrderRecord

EARS: When the airline applies a group of changes to an order, the system shall raise the order's version by one and record the group in the order's history.

Story: As a seller, I want each version of an order to stand for one set of changes, so that I can rebuild any version from the order's history.

Acceptance criteria:

ONE-404.1: When an order is created, the system shall give it version 1 and a history with no change groups.
ONE-404.2: When the airline applies a group of changes to an order, the system shall apply the group to the order and raise its version by one.
ONE-404.3: The system shall keep an order's version one more than the number of change groups applied since it was created.
ONE-404.4: When a seller asks for an order's history, the system shall return the order at version 1 and each later change group once, labelled with the version it produced.
ONE-404.5: When a seller applies the change groups of an order's history to the order at version 1 in the order listed, the system shall give the order as it is now.

The history is listed oldest first or newest first, as the reading of the sources says (HistoryListing, orderHistory).

27.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-404.1	Proven	New orders start at version 1, Versions of trip
ONE-404.2	Proven	Each change group raises the version by one, Versions of trip
ONE-404.3	Proven	Order version, Versions of trip
ONE-404.4	Proven	The history lists each change group once, Versions of trip
ONE-404.5	Open	Newest first history, History rebuilds every version

27.2. Guarantees🔗

27.2.1. New orders start at version 1🔗

guarantee

Rules.OneOrder.Creation.create_version_one (o : Rules.OneOrder.Order)
  (l : Rules.OneOrder.Creation.HistoryListing) :
  (Rules.OneOrder.Creation.OrderRecord.create o).version = 1 ∧
    (Rules.OneOrder.Creation.OrderRecord.create o).groups = [] ∧
      (Rules.OneOrder.Creation.orderHistory l
              (Rules.OneOrder.Creation.OrderRecord.create o)).initial =
          o ∧
        (Rules.OneOrder.Creation.orderHistory l
              (Rules.OneOrder.Creation.OrderRecord.create o)).entries =
          []
Rules.OneOrder.Creation.create_version_one
  (o : Rules.OneOrder.Order)
  (l :
    Rules.OneOrder.Creation.HistoryListing) :
  (Rules.OneOrder.Creation.OrderRecord.create
          o).version =
      1 ∧
    (Rules.OneOrder.Creation.OrderRecord.create
            o).groups =
        [] ∧
      (Rules.OneOrder.Creation.orderHistory
              l
              (Rules.OneOrder.Creation.OrderRecord.create
                o)).initial =
          o ∧
        (Rules.OneOrder.Creation.orderHistory
              l
              (Rules.OneOrder.Creation.OrderRecord.create
                o)).entries =
          []

A new order is at version 1, with no change groups and an empty history under both readings.

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

Checks acceptance criteria ONE-404.1.

27.2.2. Each change group raises the version by one🔗

guarantee

Rules.OneOrder.Creation.record_raises_version
  (r : Rules.OneOrder.Creation.OrderRecord)
  (g : Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.recordChanges r g).current =
      Rules.OneOrder.Creation.applyGroup r.current g ∧
    (Rules.OneOrder.Creation.recordChanges r g).groups =
        r.groups ++ [g] ∧
      (Rules.OneOrder.Creation.recordChanges r g).version =
        r.version + 1
Rules.OneOrder.Creation.record_raises_version
  (r :
    Rules.OneOrder.Creation.OrderRecord)
  (g :
    Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.recordChanges r
          g).current =
      Rules.OneOrder.Creation.applyGroup
        r.current g ∧
    (Rules.OneOrder.Creation.recordChanges
            r g).groups =
        r.groups ++ [g] ∧
      (Rules.OneOrder.Creation.recordChanges
            r g).version =
        r.version + 1

Applying a group of changes applies it to the order, records it and raises the version by one.

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

Checks acceptance criteria ONE-404.2.

27.2.3. Order version🔗

guarantee

Rules.OneOrder.Creation.version_counts_groups (o : Rules.OneOrder.Order)
  (gs : List Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.OrderRecord.after o gs).version =
      gs.length + 1 ∧
    (Rules.OneOrder.Creation.OrderRecord.after o gs).groups = gs
Rules.OneOrder.Creation.version_counts_groups
  (o : Rules.OneOrder.Order)
  (gs :
    List
      Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.OrderRecord.after
          o gs).version =
      gs.length + 1 ∧
    (Rules.OneOrder.Creation.OrderRecord.after
          o gs).groups =
      gs

After any number of change groups, an order's version is one more than their number, and its history holds exactly those groups.

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

Checks acceptance criteria ONE-404.3.

27.2.4. The history lists each change group once🔗

guarantee

Rules.OneOrder.Creation.history_lists_each_group
  (l : Rules.OneOrder.Creation.HistoryListing)
  (o : Rules.OneOrder.Order)
  (gs : List Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.orderHistory l
          (Rules.OneOrder.Creation.OrderRecord.after o gs)).initial =
      o ∧
    (Rules.OneOrder.Creation.orderHistory l
            (Rules.OneOrder.Creation.OrderRecord.after o
              gs)).entries.Perm
      (List.mapIdx (fun k g ↦ { version := k + 2, group := g }) gs)
Rules.OneOrder.Creation.history_lists_each_group
  (l :
    Rules.OneOrder.Creation.HistoryListing)
  (o : Rules.OneOrder.Order)
  (gs :
    List
      Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.orderHistory l
          (Rules.OneOrder.Creation.OrderRecord.after
            o gs)).initial =
      o ∧
    (Rules.OneOrder.Creation.orderHistory
            l
            (Rules.OneOrder.Creation.OrderRecord.after
              o gs)).entries.Perm
      (List.mapIdx
        (fun k g ↦
          { version := k + 2,
            group := g })
        gs)

An order's history, under both readings, holds the order at version 1 and each change group once, labelled with the version it produced: the first group applied with version 2, the next with version 3, and so on.

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

Checks acceptance criteria ONE-404.4.

27.2.5. History rebuilds every version🔗

guarantee

Rules.OneOrder.Creation.history_rebuilds_current
  (l : Rules.OneOrder.Creation.HistoryListing)
  (o : Rules.OneOrder.Order)
  (gs : List Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.orderHistory l
        (Rules.OneOrder.Creation.OrderRecord.after o gs)).rebuild =
    (Rules.OneOrder.Creation.OrderRecord.after o gs).current
Rules.OneOrder.Creation.history_rebuilds_current
  (l :
    Rules.OneOrder.Creation.HistoryListing)
  (o : Rules.OneOrder.Order)
  (gs :
    List
      Rules.OneOrder.Creation.ChangeGroup) :
  (Rules.OneOrder.Creation.orderHistory l
        (Rules.OneOrder.Creation.OrderRecord.after
          o gs)).rebuild =
    (Rules.OneOrder.Creation.OrderRecord.after
        o gs).current

Applying the change groups of an order's history to the order at version 1, in the order listed, gives the order as it is now, under both readings.

Open question for the business. The guide lists change groups oldest first, each raising the version by one, while the capability page for order history lists them newest first and says each lowers the version. Applied newest first, a group that removes an item runs before the group that added it, and the item comes back. The example newestFirstHistory shows it. In which order does the history list its change groups, and does a history requested from version v include the group that produced v?

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

Checks acceptance criteria ONE-404.5.

27.3. Examples🔗

27.3.1. Versions of trip🔗

example

Rules.OneOrder.Creation.versionsOfTrip :
  Rules.OneOrder.Creation.VersionedOrder
Rules.OneOrder.Creation.versionsOfTrip :
  Rules.OneOrder.Creation.VersionedOrder

Given the trip order as created, with a flight and a seat.

When the airline adds a bag, then cancels the seat, in two change groups.

Then the order is at version 1 when created, 2 after the bag and 3 after the seat. Its history holds the two groups, labelled 2 and 3, listed oldest first or newest first as the reading says.

What Lean computed:

Versions: see the table below.
Oldest first: 2, 3
Newest first: 3, 2

Versions:

Version	Items	Active items	Groups in history
1	ITEM-FLT, ITEM-SEAT	ITEM-FLT, ITEM-SEAT	0
2	ITEM-FLT, ITEM-SEAT, ITEM-BAG	ITEM-FLT, ITEM-SEAT, ITEM-BAG	1
3	ITEM-FLT, ITEM-SEAT, ITEM-BAG	ITEM-FLT, ITEM-BAG	2

Checks acceptance criteria ONE-404.1, ONE-404.2, ONE-404.3, ONE-404.4.

27.3.2. Newest first history🔗

example

Rules.OneOrder.Creation.newestFirstHistory :
  Rules.OneOrder.Creation.RebuildCase
Rules.OneOrder.Creation.newestFirstHistory :
  Rules.OneOrder.Creation.RebuildCase

Given the trip order, to which the airline added a bag at version 2 and from which it removed the bag at version 3.

When a seller asks for the order's history and applies its change groups to the order at version 1, in the order listed.

Then listed oldest first, the rebuilt order is the order as it is now, with a flight and a seat. Listed newest first, the removal runs before the bag was added, and the bag comes back.

What Lean computed:

Current: ITEM-FLT, ITEM-SEAT
Rebuilds: see the table below.

Rebuilds:

Listing	Rebuilt	Matches current
oldest first	ITEM-FLT, ITEM-SEAT	yes
newest first	ITEM-FLT, ITEM-SEAT, ITEM-BAG	no

Checks acceptance criteria ONE-404.5.

27.4. Open question🔗

The guarantee History rebuilds every version is open: the example Newest first history shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.