51. Clearance status🔗

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

rule

Rules.OneOrder.Accounting.settleStep
  (r : Rules.OneOrder.Accounting.SettlementReading)
  (c : Rules.OneOrder.Accounting.SettlementRecord) :
  Rules.OneOrder.Accounting.SettlementEvent →
    Option Rules.OneOrder.Accounting.SettlementRecord
Rules.OneOrder.Accounting.settleStep
  (r :
    Rules.OneOrder.Accounting.SettlementReading)
  (c :
    Rules.OneOrder.Accounting.SettlementRecord) :
  Rules.OneOrder.Accounting.SettlementEvent →
    Option
      Rules.OneOrder.Accounting.SettlementRecord

EARS: When the ORA cancels a clearance or the Clearance Manager settles, claws back or writes off money on it, the system shall move the clearance's status and amounts as the clearance statuses describe.

Story: As an airline, I want each clearance's status to say how much of it is settled, so that I can match every clearing to what I am owed.

Acceptance criteria:

ONE-804.1: When the ORA cancels an Accepted clearance, the system shall mark it Cancelled and refuse every clearing for it afterwards.
ONE-804.2: When a clearing pays all that is unsettled on a clearance, the system shall mark it Fully Settled if it was Accepted and Final Settlement otherwise.
ONE-804.3: When a clearing pays part of what is unsettled on a clearance, the system shall mark it Partially Settled and settle no more than the amount still unsettled.
ONE-804.4: When the Clearance Manager writes off a clearance, the system shall remove exactly the amount still unsettled.
ONE-804.5: The system shall keep the amounts settled on a clearance, less those clawed back, plus the amount unsettled and the amount written off, equal to its agreed amount.

A clearing that pays nothing toward an Accepted clearance marks it Not Settled. Whether a clawed-back clearance can be settled again, and whether Final Settlement can be clawed back, are a reading of the sources (SettlementReading). The EasyPay statuses Funds Collected and Funds Partially Collected are not modelled. The result is the record afterwards, or none when the event is refused.

51.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-804.1	Proven	Cancelling an accepted clearance, Cancelled before clearing
ONE-804.2	Proven	Settling a clearance in full, Settled in two clearings, Settled in one clearing
ONE-804.3	Proven	Settled in two clearings, Settling a clearance in part
ONE-804.4	Proven	Remainder written off, Writing off a clearance
ONE-804.5	Open	Clawed back then collected, Settled and unsettled clearance amounts

51.2. Guarantees🔗

51.2.1. Cancelling an accepted clearance🔗

guarantee

Rules.OneOrder.Accounting.cancel_marks_cancelled
  (r : Rules.OneOrder.Accounting.SettlementReading)
  (c : Rules.OneOrder.Accounting.SettlementRecord)
  (hs : c.status = Rules.OneOrder.Accounting.ClearanceStatus.accepted) :
  Rules.OneOrder.Accounting.settleStep r c
        Rules.OneOrder.Accounting.SettlementEvent.cancel =
      some
        { status := Rules.OneOrder.Accounting.ClearanceStatus.cancelled,
          agreed := c.agreed, settled := c.settled,
          clawedBack := c.clawedBack, unsettled := c.unsettled,
          writtenOff := c.writtenOff } ∧
    ∀ (e : Rules.OneOrder.Accounting.SettlementEvent),
      Rules.OneOrder.Accounting.settleStep r
          {
            status :=
              Rules.OneOrder.Accounting.ClearanceStatus.cancelled,
            agreed := c.agreed, settled := c.settled,
            clawedBack := c.clawedBack, unsettled := c.unsettled,
            writtenOff := c.writtenOff }
          e =
        none
Rules.OneOrder.Accounting.cancel_marks_cancelled
  (r :
    Rules.OneOrder.Accounting.SettlementReading)
  (c :
    Rules.OneOrder.Accounting.SettlementRecord)
  (hs :
    c.status =
      Rules.OneOrder.Accounting.ClearanceStatus.accepted) :
  Rules.OneOrder.Accounting.settleStep r c
        Rules.OneOrder.Accounting.SettlementEvent.cancel =
      some
        {
          status :=
            Rules.OneOrder.Accounting.ClearanceStatus.cancelled,
          agreed := c.agreed,
          settled := c.settled,
          clawedBack := c.clawedBack,
          unsettled := c.unsettled,
          writtenOff := c.writtenOff } ∧
    ∀
      (e :
        Rules.OneOrder.Accounting.SettlementEvent),
      Rules.OneOrder.Accounting.settleStep
          r
          {
            status :=
              Rules.OneOrder.Accounting.ClearanceStatus.cancelled,
            agreed := c.agreed,
            settled := c.settled,
            clawedBack := c.clawedBack,
            unsettled := c.unsettled,
            writtenOff := c.writtenOff }
          e =
        none

The ORA's cancellation marks an accepted clearance Cancelled, and every later event for it is refused, under every reading.

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

Checks acceptance criteria ONE-804.1.

51.2.2. Settling a clearance in full🔗

guarantee

Rules.OneOrder.Accounting.settle_all
  (r : Rules.OneOrder.Accounting.SettlementReading)
  (c : Rules.OneOrder.Accounting.SettlementRecord) (x : ℕ)
  (hs :
    Rules.OneOrder.Accounting.ClearanceStatus.settleable r c.status =
      true)
  (hx : c.unsettled ≤ x) :
  ∃ c',
    Rules.OneOrder.Accounting.settleStep r c
          (Rules.OneOrder.Accounting.SettlementEvent.settle x) =
        some c' ∧
      (c'.status =
          if
              c.status =
                Rules.OneOrder.Accounting.ClearanceStatus.accepted then
            Rules.OneOrder.Accounting.ClearanceStatus.fullySettled
          else
            Rules.OneOrder.Accounting.ClearanceStatus.finalSettlement) ∧
        c'.settled = c.settled + c.unsettled ∧ c'.unsettled = 0
Rules.OneOrder.Accounting.settle_all
  (r :
    Rules.OneOrder.Accounting.SettlementReading)
  (c :
    Rules.OneOrder.Accounting.SettlementRecord)
  (x : ℕ)
  (hs :
    Rules.OneOrder.Accounting.ClearanceStatus.settleable
        r c.status =
      true)
  (hx : c.unsettled ≤ x) :
  ∃ c',
    Rules.OneOrder.Accounting.settleStep r
          c
          (Rules.OneOrder.Accounting.SettlementEvent.settle
            x) =
        some c' ∧
      (c'.status =
          if
              c.status =
                Rules.OneOrder.Accounting.ClearanceStatus.accepted then
            Rules.OneOrder.Accounting.ClearanceStatus.fullySettled
          else
            Rules.OneOrder.Accounting.ClearanceStatus.finalSettlement) ∧
        c'.settled =
            c.settled + c.unsettled ∧
          c'.unsettled = 0

A clearing that pays all that is unsettled marks the clearance Fully Settled if it was Accepted and Final Settlement otherwise, and leaves nothing unsettled, under every reading.

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

Checks acceptance criteria ONE-804.2.

51.2.3. Settling a clearance in part🔗

guarantee

Rules.OneOrder.Accounting.settle_part
  (r : Rules.OneOrder.Accounting.SettlementReading)
  (c c' : Rules.OneOrder.Accounting.SettlementRecord) (x : ℕ)
  (h :
    Rules.OneOrder.Accounting.settleStep r c
        (Rules.OneOrder.Accounting.SettlementEvent.settle x) =
      some c') :
  c'.settled ≤ c.settled + c.unsettled ∧
    (0 < x →
      x < c.unsettled →
        c'.status =
            Rules.OneOrder.Accounting.ClearanceStatus.partiallySettled ∧
          c'.settled = c.settled + x)
Rules.OneOrder.Accounting.settle_part
  (r :
    Rules.OneOrder.Accounting.SettlementReading)
  (c c' :
    Rules.OneOrder.Accounting.SettlementRecord)
  (x : ℕ)
  (h :
    Rules.OneOrder.Accounting.settleStep r
        c
        (Rules.OneOrder.Accounting.SettlementEvent.settle
          x) =
      some c') :
  c'.settled ≤ c.settled + c.unsettled ∧
    (0 < x →
      x < c.unsettled →
        c'.status =
            Rules.OneOrder.Accounting.ClearanceStatus.partiallySettled ∧
          c'.settled = c.settled + x)

A clearing that pays part of what is unsettled marks the clearance Partially Settled and settles what it pays. No clearing settles more than the amount still unsettled. Both hold under every reading.

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

Checks acceptance criteria ONE-804.3.

51.2.4. Writing off a clearance🔗

guarantee

Rules.OneOrder.Accounting.write_off_removes_unsettled
  (r : Rules.OneOrder.Accounting.SettlementReading)
  (c c' : Rules.OneOrder.Accounting.SettlementRecord)
  (h :
    Rules.OneOrder.Accounting.settleStep r c
        Rules.OneOrder.Accounting.SettlementEvent.writeOff =
      some c') :
  c'.status = Rules.OneOrder.Accounting.ClearanceStatus.writtenOff ∧
    c'.writtenOff = c.writtenOff + c.unsettled ∧
      c'.unsettled = 0 ∧
        c'.settled = c.settled ∧ c'.clawedBack = c.clawedBack
Rules.OneOrder.Accounting.write_off_removes_unsettled
  (r :
    Rules.OneOrder.Accounting.SettlementReading)
  (c c' :
    Rules.OneOrder.Accounting.SettlementRecord)
  (h :
    Rules.OneOrder.Accounting.settleStep r
        c
        Rules.OneOrder.Accounting.SettlementEvent.writeOff =
      some c') :
  c'.status =
      Rules.OneOrder.Accounting.ClearanceStatus.writtenOff ∧
    c'.writtenOff =
        c.writtenOff + c.unsettled ∧
      c'.unsettled = 0 ∧
        c'.settled = c.settled ∧
          c'.clawedBack = c.clawedBack

Writing off a clearance removes exactly the amount still unsettled and changes nothing settled, under every reading.

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

Checks acceptance criteria ONE-804.4.

51.2.5. Settled and unsettled clearance amounts🔗

guarantee

Rules.OneOrder.Accounting.clearance_amounts_accounted
  (r : Rules.OneOrder.Accounting.SettlementReading) (agreed : ℕ)
  (es : List Rules.OneOrder.Accounting.SettlementEvent) :
  (Rules.OneOrder.Accounting.settleRun r
      (Rules.OneOrder.Accounting.SettlementRecord.new agreed)
      es).Accounted
Rules.OneOrder.Accounting.clearance_amounts_accounted
  (r :
    Rules.OneOrder.Accounting.SettlementReading)
  (agreed : ℕ)
  (es :
    List
      Rules.OneOrder.Accounting.SettlementEvent) :
  (Rules.OneOrder.Accounting.settleRun r
      (Rules.OneOrder.Accounting.SettlementRecord.new
        agreed)
      es).Accounted

Every part of a clearance's agreed amount stays settled and kept, still unsettled, or written off, whatever happens to it.

Open question for the business. Under a reading where a clawed-back amount does not count as unsettled again, a clawback takes money back from the payee without adding it to what is owed, so that part of the agreed amount is neither settled, unsettled nor written off. The example clawedBackThenCollected shows it: a 300.00 clearance settled in full and then clawed back by 100.00 keeps 200.00 settled, with nothing unsettled. Does a clawed-back amount count as unsettled again, and can a later clearing settle it?

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

Checks acceptance criteria ONE-804.5.

51.3. Examples🔗

51.3.1. Cancelled before clearing🔗

example

Rules.OneOrder.Accounting.cancelledBeforeClearing :
  Rules.OneOrder.Accounting.SettlementTrace
Rules.OneOrder.Accounting.cancelledBeforeClearing :
  Rules.OneOrder.Accounting.SettlementTrace

Given an accepted clearance of 300.00 EUR.

When the ORA cancels it, and a clearing then tries to pay it.

Then the clearance is Cancelled and stays Cancelled, with nothing settled.

What Lean computed:

Statuses: cancelled, cancelled
Settled: 0
Clawed back: 0
Unsettled: 30000
Written off: 0
Accounted for: 30000

Checks acceptance criteria ONE-804.1.

51.3.2. Settled in one clearing🔗

example

Rules.OneOrder.Accounting.settledInOneClearing :
  Rules.OneOrder.Accounting.SettlementTrace
Rules.OneOrder.Accounting.settledInOneClearing :
  Rules.OneOrder.Accounting.SettlementTrace

Given an accepted clearance of 300.00 EUR.

When the next clearing pays all of it.

Then the clearance is Fully Settled, with 300.00 EUR settled and nothing unsettled.

What Lean computed:

Statuses: fully settled
Settled: 30000
Clawed back: 0
Unsettled: 0
Written off: 0
Accounted for: 30000

Checks acceptance criteria ONE-804.2.

51.3.3. Settled in two clearings🔗

example

Rules.OneOrder.Accounting.settledInTwoClearings :
  Rules.OneOrder.Accounting.SettlementTrace
Rules.OneOrder.Accounting.settledInTwoClearings :
  Rules.OneOrder.Accounting.SettlementTrace

Given an accepted clearance of 300.00 EUR.

When a clearing pays 250.00 EUR toward it and a later clearing pays the remaining 50.00 EUR. The first clearing is the source's sample, which shows 250.00 EUR settled and 50.00 EUR unsettled.

Then the clearance is Partially Settled with 50.00 EUR unsettled, and then Final Settlement.

What Lean computed:

Statuses: partially settled, final settlement
Settled: 30000
Clawed back: 0
Unsettled: 0
Written off: 0
Accounted for: 30000

Checks acceptance criteria ONE-804.2, ONE-804.3.

51.3.4. Remainder written off🔗

example

Rules.OneOrder.Accounting.remainderWrittenOff :
  Rules.OneOrder.Accounting.SettlementTrace
Rules.OneOrder.Accounting.remainderWrittenOff :
  Rules.OneOrder.Accounting.SettlementTrace

Given an accepted clearance of 300.00 EUR, of which a clearing paid 250.00 EUR.

When the Clearance Manager cannot collect the rest and writes it off.

Then the clearance is Written Off, with the 50.00 EUR that was unsettled written off.

What Lean computed:

Statuses: partially settled, written off
Settled: 25000
Clawed back: 0
Unsettled: 0
Written off: 5000
Accounted for: 30000

Checks acceptance criteria ONE-804.4.

51.3.5. Clawed back then collected🔗

example

Rules.OneOrder.Accounting.clawedBackThenCollected :
  Rules.OneOrder.Accounting.ClawbackTraces
Rules.OneOrder.Accounting.clawedBackThenCollected :
  Rules.OneOrder.Accounting.ClawbackTraces

Given a clearance of 300.00 EUR settled in full in its first clearing.

When the Clearance Manager claws back 100.00 EUR from the payee, collects the funds, and a later clearing pays 100.00 EUR.

Then where a clawed-back amount counts as unsettled again, the clearance goes to Clawed Back and then Final Settlement, and all 300.00 EUR is accounted for. Where it does not, the later clearing is refused: the clearance stays Clawed Back with 300.00 EUR settled, 100.00 EUR clawed back and nothing unsettled, so 100.00 EUR of the agreed amount is accounted for nowhere.

What Lean computed:

Reopens: statuses fully settled, clawed back, final settlement, settled 40000, clawed back 10000, unsettled 0, written off 0, accounted for 30000
Does not reopen: statuses fully settled, clawed back, clawed back, settled 30000, clawed back 10000, unsettled 0, written off 0, accounted for 20000

Checks acceptance criteria ONE-804.5.

51.4. Open question🔗

The guarantee Settled and unsettled clearance amounts is open: the example Clawed back then collected shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.