28. Change against a stale version🔗

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

rule

Rules.OneOrder.Creation.requestChange
  (s : Rules.OneOrder.Creation.StaleHandling)
  (r : Rules.OneOrder.Creation.OrderRecord) (seen : Option ℕ)
  (g : Rules.OneOrder.Creation.ChangeGroup) :
  Except Rules.OneOrder.Creation.VersionRejection
    Rules.OneOrder.Creation.OrderRecord
Rules.OneOrder.Creation.requestChange
  (s :
    Rules.OneOrder.Creation.StaleHandling)
  (r :
    Rules.OneOrder.Creation.OrderRecord)
  (seen : Option ℕ)
  (g :
    Rules.OneOrder.Creation.ChangeGroup) :
  Except
    Rules.OneOrder.Creation.VersionRejection
    Rules.OneOrder.Creation.OrderRecord

EARS: When a seller sends a change request, the system shall compare the order version the request carries, if any, with the order's current version before applying the change.

Story: As a seller, I want a change I make on an order I saw at an older version to be refused, so that I never overwrite a change I have not seen.

Acceptance criteria:

ONE-405.1: When a change request carries the order's current version, the system shall apply the change and raise the version by one.
ONE-405.2: When a change request carries no version, the system shall apply the change.
ONE-405.3: If a change request carries a version other than the order's current version, then the system shall reject the change.

A request without a version proceeds, as the guide says. A request with another version is handled as the reading of the guide says (StaleHandling).

28.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-405.1	Proven	Two sellers one version, Changes on the current version are applied
ONE-405.2	Proven	Changes without a version are applied, Two sellers one version
ONE-405.3	Open	Changes on a stale version are rejected, Two sellers one version

28.2. Guarantees🔗

28.2.1. Changes on the current version are applied🔗

guarantee

Rules.OneOrder.Creation.current_version_applied
  (s : Rules.OneOrder.Creation.StaleHandling)
  (r : Rules.OneOrder.Creation.OrderRecord)
  (g : Rules.OneOrder.Creation.ChangeGroup) :
  Rules.OneOrder.Creation.requestChange s r (some r.version) g =
      Except.ok (Rules.OneOrder.Creation.recordChanges r g) ∧
    (Rules.OneOrder.Creation.recordChanges r g).version = r.version + 1
Rules.OneOrder.Creation.current_version_applied
  (s :
    Rules.OneOrder.Creation.StaleHandling)
  (r :
    Rules.OneOrder.Creation.OrderRecord)
  (g :
    Rules.OneOrder.Creation.ChangeGroup) :
  Rules.OneOrder.Creation.requestChange s
        r (some r.version) g =
      Except.ok
        (Rules.OneOrder.Creation.recordChanges
          r g) ∧
    (Rules.OneOrder.Creation.recordChanges
          r g).version =
      r.version + 1

A change that carries the order's current version is applied and raises the version by one, under both readings.

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

Checks acceptance criteria ONE-405.1.

28.2.2. Changes without a version are applied🔗

guarantee

Rules.OneOrder.Creation.no_version_applied
  (s : Rules.OneOrder.Creation.StaleHandling)
  (r : Rules.OneOrder.Creation.OrderRecord)
  (g : Rules.OneOrder.Creation.ChangeGroup) :
  Rules.OneOrder.Creation.requestChange s r none g =
    Except.ok (Rules.OneOrder.Creation.recordChanges r g)
Rules.OneOrder.Creation.no_version_applied
  (s :
    Rules.OneOrder.Creation.StaleHandling)
  (r :
    Rules.OneOrder.Creation.OrderRecord)
  (g :
    Rules.OneOrder.Creation.ChangeGroup) :
  Rules.OneOrder.Creation.requestChange s
      r none g =
    Except.ok
      (Rules.OneOrder.Creation.recordChanges
        r g)

A change that carries no version is applied, under both readings.

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

Checks acceptance criteria ONE-405.2.

28.2.3. Changes on a stale version are rejected🔗

guarantee

Rules.OneOrder.Creation.stale_rejected
  (s : Rules.OneOrder.Creation.StaleHandling)
  (r : Rules.OneOrder.Creation.OrderRecord) (v : ℕ)
  (g : Rules.OneOrder.Creation.ChangeGroup) (hv : v ≠ r.version) :
  ∃ e,
    Rules.OneOrder.Creation.requestChange s r (some v) g =
      Except.error e
Rules.OneOrder.Creation.stale_rejected
  (s :
    Rules.OneOrder.Creation.StaleHandling)
  (r :
    Rules.OneOrder.Creation.OrderRecord)
  (v : ℕ)
  (g :
    Rules.OneOrder.Creation.ChangeGroup)
  (hv : v ≠ r.version) :
  ∃ e,
    Rules.OneOrder.Creation.requestChange
        s r (some v) g =
      Except.error e

A change that carries a version other than the order's current version is rejected, under both readings.

Open question for the business. The guide lets the airline return an error when the versions differ and does not require it. Under the reading where the airline applies the change anyway, a seller who saw an older version overwrites a change it never saw. The example twoSellersOneVersion shows it. Does a version mismatch always reject the change, and may a change be sent without a version?

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

Checks acceptance criteria ONE-405.3.

28.3. Examples🔗

28.3.1. Two sellers one version🔗

example

Rules.OneOrder.Creation.twoSellersOneVersion :
  List Rules.OneOrder.Creation.StaleRow
Rules.OneOrder.Creation.twoSellersOneVersion :
  List Rules.OneOrder.Creation.StaleRow

Given the trip order at version 3, which two sellers have both read.

When the first seller sends a change carrying version 3, which removes the bag. The second seller then sends a change carrying version 3, or no version.

Then the first change is applied and the order moves to version 4. The second seller's change carrying version 3 is rejected where the airline rejects stale versions, and applied over the removal its seller never saw where the airline applies it anyway. A change carrying no version is applied.

What Lean computed:

Request	Handling	Version after	Rejection
first seller sends version 3	reject	4	none
second seller sends version 3	reject	none	stale
second seller sends version 3	apply	5	none
second seller sends no version	reject	5	none

Checks acceptance criteria ONE-405.1, ONE-405.2, ONE-405.3.

28.4. Open question🔗

The guarantee Changes on a stale version are rejected is open: the example Two sellers one version shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.