32. Restriction rule in force🔗

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

rule

Rules.OneOrder.Offers.ruleInForce
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant) : Option Rules.OneOrder.Offers.Restriction
Rules.OneOrder.Offers.ruleInForce
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant) :
  Option Rules.OneOrder.Offers.Restriction

EARS: When a change or cancellation is asked for at an instant, the system shall take as the rule in force the rule for that action and the journey's current stage with the latest effective date not after that instant.

Story: As a seller, I want to know which change or cancel rule applies at any moment of the journey, so that I can tell the customer what a change costs and what a cancellation returns.

Acceptance criteria:

ONE-503.1: When a rule is in force for an action at an instant, the system shall take it from the rules for that action and for the stage the journey is in at that instant.
ONE-503.2: When a rule is in force at an instant, the system shall take one whose effective date is not after that instant.
ONE-503.3: When rules for an action and the current stage have started, and have not expired where expiration dates end rules, the system shall take as the rule in force one with the latest effective date among them.
ONE-503.4: Where expiration dates end rules, the system shall not take a rule as in force at or after its expiration date.
ONE-503.5: While a journey is in a stage for which an action has rules, the system shall have a rule in force for that action.

Whether a rule's expiration date ends it is a reading of the guide (ExpiryReading).

32.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-503.1	Proven	Rule over journey, Rule in force belongs to the current stage
ONE-503.2	Proven	Rule over journey, Rule in force has started
ONE-503.3	Proven	Latest started rule is in force, Rule over journey
ONE-503.4	Proven	Expiry readings, Expired rules are not in force
ONE-503.5	Open	No rule in force, Every stage with rules has a rule in force

32.2. Guarantees🔗

32.2.1. Rule in force belongs to the current stage🔗

guarantee

Rules.OneOrder.Offers.ruleInForce_stage
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant) (r : Rules.OneOrder.Offers.Restriction)
  (h : Rules.OneOrder.Offers.ruleInForce e rules j a now = some r) :
  r ∈ rules ∧ r.action = a ∧ r.stage = j.stageAt now
Rules.OneOrder.Offers.ruleInForce_stage
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j a now =
      some r) :
  r ∈ rules ∧
    r.action = a ∧ r.stage = j.stageAt now

The rule in force for an action at an instant is one of the rules for that action and for the stage the journey is in at that instant.

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

Checks acceptance criteria ONE-503.1.

32.2.2. Rule in force has started🔗

guarantee

Rules.OneOrder.Offers.ruleInForce_started
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant) (r : Rules.OneOrder.Offers.Restriction)
  (h : Rules.OneOrder.Offers.ruleInForce e rules j a now = some r) :
  r.effective ≤ now
Rules.OneOrder.Offers.ruleInForce_started
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j a now =
      some r) :
  r.effective ≤ now

The rule in force at an instant has started by that instant.

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

Checks acceptance criteria ONE-503.2.

32.2.3. Latest started rule is in force🔗

guarantee

Rules.OneOrder.Offers.ruleInForce_latest
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (h :
    ∃ r' ∈ rules,
      r'.action = a ∧
        r'.stage = j.stageAt now ∧
          Rules.OneOrder.Offers.Restriction.live e now r' = true) :
  ∃ r,
    Rules.OneOrder.Offers.ruleInForce e rules j a now = some r ∧
      Rules.OneOrder.Offers.Restriction.live e now r = true ∧
        ∀ r' ∈ rules,
          r'.action = a →
            r'.stage = j.stageAt now →
              Rules.OneOrder.Offers.Restriction.live e now r' = true →
                r'.effective ≤ r.effective
Rules.OneOrder.Offers.ruleInForce_latest
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (h :
    ∃ r' ∈ rules,
      r'.action = a ∧
        r'.stage = j.stageAt now ∧
          Rules.OneOrder.Offers.Restriction.live
              e now r' =
            true) :
  ∃ r,
    Rules.OneOrder.Offers.ruleInForce e
          rules j a now =
        some r ∧
      Rules.OneOrder.Offers.Restriction.live
            e now r =
          true ∧
        ∀ r' ∈ rules,
          r'.action = a →
            r'.stage = j.stageAt now →
              Rules.OneOrder.Offers.Restriction.live
                    e now r' =
                  true →
                r'.effective ≤ r.effective

When at least one rule for an action and the current stage is live (it has started and, under the reading that expiration dates end rules, has not expired), a rule is in force. It is one of those live rules, and none of them starts later than it.

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

Checks acceptance criteria ONE-503.3.

32.2.4. Expired rules are not in force🔗

guarantee

Rules.OneOrder.Offers.ruleInForce_not_expired
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant) (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce
        Rules.OneOrder.Offers.ExpiryReading.ends rules j a now =
      some r)
  (t : Rules.Core.Instant) : r.expires = some t → now < t
Rules.OneOrder.Offers.ruleInForce_not_expired
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce
        Rules.OneOrder.Offers.ExpiryReading.ends
        rules j a now =
      some r)
  (t : Rules.Core.Instant) :
  r.expires = some t → now < t

Under the reading that expiration dates end rules, the rule in force at an instant has not reached its expiration date.

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

Checks acceptance criteria ONE-503.4.

32.2.5. Every stage with rules has a rule in force🔗

guarantee

Rules.OneOrder.Offers.ruleInForce_covers_stage
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (h : ∃ r ∈ rules, r.action = a ∧ r.stage = j.stageAt now) :
  (Rules.OneOrder.Offers.ruleInForce e rules j a now).isSome = true
Rules.OneOrder.Offers.ruleInForce_covers_stage
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (a : Rules.OneOrder.Offers.Action)
  (now : Rules.Core.Instant)
  (h :
    ∃ r ∈ rules,
      r.action = a ∧
        r.stage = j.stageAt now) :
  (Rules.OneOrder.Offers.ruleInForce e
        rules j a now).isSome =
    true

While a journey is in a stage for which an action has rules, a rule is in force for that action.

Open question for the business. A rule starts at its effective date, and the guide does not say what applies in a stage before its first rule starts, or, when expiration dates end rules, in a gap before the next rule starts. A journey paid before its first rule for the stage before departure starts has no rule in force, under both readings; under the reading that expiration dates end rules, a rule whose effective and expiration dates are equal is never in force. The example noRuleInForce shows both. What applies to a change or cancellation when no rule of the stage is in force?

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

Checks acceptance criteria ONE-503.5.

32.3. Examples🔗

32.3.1. Rule over journey🔗

example

Rules.OneOrder.Offers.ruleOverJourney :
  List Rules.OneOrder.Offers.InForceRow
Rules.OneOrder.Offers.ruleOverJourney :
  List Rules.OneOrder.Offers.InForceRow

Given the journey paid on 1 January and departing on 1 February, with the flight change rules: free before payment, 30.00 EUR after payment, 60.00 EUR from 20 January, and no change from 24 January.

When the rule in force for a flight change is read on 1 January at 08:00, 10 January, 22 January, 24 January at 12:00 and 3 February.

Then the rules in force are the free change before payment, the 30.00 EUR rule, the 60.00 EUR rule, the rule that forbids changes, and the rule after departure. On 24 January at noon the flight is just under eight days away, and the rule described as seven days before departure is already in force.

What Lean computed:

Time	Stage	Rule
2019-01-01 08:00 UTC	before payment	FLT-0
2019-01-10 00:00 UTC	before departure	FLT-1
2019-01-22 00:00 UTC	before departure	FLT-2
2019-01-24 12:00 UTC	before departure	FLT-3
2019-02-03 00:00 UTC	after departure	FLT-4

Checks acceptance criteria ONE-503.1, ONE-503.2, ONE-503.3.

32.3.2. Expiry readings🔗

example

Rules.OneOrder.Offers.expiryReadings :
  List Rules.OneOrder.Offers.ReadingRow
Rules.OneOrder.Offers.expiryReadings :
  List Rules.OneOrder.Offers.ReadingRow

Given the journey paid on 1 January, with a flight change rule that starts on 1 January and expires on 10 January, and another that starts on 15 January.

When the rule in force is read on 5, 12 and 16 January under each reading of the guide.

Then on 5 and 16 January both readings agree. On 12 January the first rule is in force when expiration dates change nothing, and no rule is in force when they end rules.

What Lean computed:

Case	Ignored	Ends
5 January	EXP-1	EXP-1
12 January	EXP-1	none
16 January	EXP-2	EXP-2

Checks acceptance criteria ONE-503.4.

32.3.3. No rule in force🔗

example

Rules.OneOrder.Offers.noRuleInForce :
  List Rules.OneOrder.Offers.ReadingRow
Rules.OneOrder.Offers.noRuleInForce :
  List Rules.OneOrder.Offers.ReadingRow

Given two journeys. In the first, paid at 10:00 on 1 January, the only flight change rule before departure starts on 2 January. In the second, the only name change rule before departure starts and expires at 00:00 on 20 January; one of the guide's examples gives a rule equal effective and expiration dates.

When the rule in force is read at 18:00 on 1 January in the first, and at 12:00 on 20 January in the second.

Then the first has no rule in force under either reading, although the stage has a rule. The second has its rule in force when expiration dates change nothing, and none when they end rules: that rule is never in force.

What Lean computed:

Case	Ignored	Ends
before the stage's first rule starts	none	none
rule that expires as it starts	SAME-1	none

Checks acceptance criteria ONE-503.5.

32.4. Open question🔗

The guarantee Every stage with rules has a rule in force is open: the example No rule in force shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.