53. Total of a clearing🔗

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

rule

Rules.OneOrder.Accounting.clearingTotal
  (dest : Rules.OneOrder.Accounting.ClearingTo)
  (lines : List Rules.OneOrder.Accounting.ClearingLine) : ℤ
Rules.OneOrder.Accounting.clearingTotal
  (dest :
    Rules.OneOrder.Accounting.ClearingTo)
  (lines :
    List
      Rules.OneOrder.Accounting.ClearingLine) :
  ℤ

EARS: When the Clearance Manager sends a clearing, the system shall make its total, and the bank transfer for it, the amounts settled less the amounts clawed back.

Story: As a settlement payee, I want each clearing's total to match the bank transfer I receive, so that I can reconcile the transfer clearance by clearance.

Acceptance criteria:

ONE-806.1: When the Clearance Manager sends a clearing to a settlement payee, the system shall make its total the amounts settled for clearances marked Fully Settled, Partially Settled or Final Settlement, less the amounts clawed back.
ONE-806.2: When the Clearance Manager sends a clearing to a remittance payer, the system shall list its EasyPay clearances and leave them out of the total.
ONE-806.3: The system shall never make the total of a clearing to a settlement payee negative.

The bank transfer is the total; the model does not separate the two.

53.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-806.1	Proven	Sample clearing total, Clearing total
ONE-806.2	Proven	Payer clearing with easy pay, EasyPay out of a remittance payer's clearing
ONE-806.3	Open	Clearing totals are never negative, Clawback exceeds due

53.2. Guarantees🔗

53.2.1. Clearing total🔗

guarantee

Rules.OneOrder.Accounting.payee_clearing_total
  (lines : List Rules.OneOrder.Accounting.ClearingLine) :
  Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.settlementPayee lines =
    (List.map
          (fun l ↦
            if l.status.countsSettled = true then ↑l.settled else 0)
          lines).sum -
      (List.map (fun l ↦ ↑l.clawedBack) lines).sum
Rules.OneOrder.Accounting.payee_clearing_total
  (lines :
    List
      Rules.OneOrder.Accounting.ClearingLine) :
  Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.settlementPayee
      lines =
    (List.map
          (fun l ↦
            if
                l.status.countsSettled =
                  true then
              ↑l.settled
            else 0)
          lines).sum -
      (List.map (fun l ↦ ↑l.clawedBack)
          lines).sum

The total of a clearing to a settlement payee is the amounts settled for clearances marked Fully Settled, Partially Settled or Final Settlement, less the amounts clawed back.

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

Checks acceptance criteria ONE-806.1.

53.2.2. EasyPay out of a remittance payer's clearing🔗

guarantee

Rules.OneOrder.Accounting.payer_clearing_leaves_out_easyPay
  (l : Rules.OneOrder.Accounting.ClearingLine)
  (lines : List Rules.OneOrder.Accounting.ClearingLine)
  (hm : l.method = Rules.OneOrder.Accounting.ClearanceMethod.easyPay) :
  Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.remittancePayer
      (l :: lines) =
    Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.remittancePayer lines
Rules.OneOrder.Accounting.payer_clearing_leaves_out_easyPay
  (l :
    Rules.OneOrder.Accounting.ClearingLine)
  (lines :
    List
      Rules.OneOrder.Accounting.ClearingLine)
  (hm :
    l.method =
      Rules.OneOrder.Accounting.ClearanceMethod.easyPay) :
  Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.remittancePayer
      (l :: lines) =
    Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.remittancePayer
      lines

An EasyPay clearance listed in a clearing to a remittance payer adds nothing to its total.

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

Checks acceptance criteria ONE-806.2.

53.2.3. Clearing totals are never negative🔗

guarantee

Rules.OneOrder.Accounting.payee_clearing_nonneg
  (lines : List Rules.OneOrder.Accounting.ClearingLine) :
  0 ≤
    Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.settlementPayee lines
Rules.OneOrder.Accounting.payee_clearing_nonneg
  (lines :
    List
      Rules.OneOrder.Accounting.ClearingLine) :
  0 ≤
    Rules.OneOrder.Accounting.clearingTotal
      Rules.OneOrder.Accounting.ClearingTo.settlementPayee
      lines

The total of a clearing to a settlement payee is never negative.

Open question for the business. A payee whose clawbacks in a clearing exceed what it is due in that clearing gets a negative total, which a bank transfer to the payee cannot carry. The example clawbackExceedsDue shows it: a payee due 200.00 with 300.00 clawed back has a total of minus 100.00. Does the payee then become a remittance payer, or is the clawback carried forward to a later clearing?

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

Checks acceptance criteria ONE-806.3.

53.3. Examples🔗

53.3.1. Sample clearing total🔗

example

Rules.OneOrder.Accounting.sampleClearingTotal : ℤ
Rules.OneOrder.Accounting.sampleClearingTotal :
  ℤ

Given a clearing to a settlement payee listing two clearances: one Partially Settled with 250.00 EUR settled in this clearing, and one Fully Settled for 200.00 EUR. These are the figures of the source's sample clearing.

When the clearing total is worked out.

Then it is 450.00 EUR.

What Lean computed:

45000

Checks acceptance criteria ONE-806.1.

53.3.2. Payer clearing with easy pay🔗

example

Rules.OneOrder.Accounting.payerClearingWithEasyPay : ℤ
Rules.OneOrder.Accounting.payerClearingWithEasyPay :
  ℤ

Given a clearing to a remittance payer listing a settlement plan clearance of 100.00 EUR and an EasyPay clearance of 50.00 EUR, both Fully Settled.

When the clearing total is worked out.

Then it is 100.00 EUR: the EasyPay clearance is listed and left out, since the EasyPay provider pays it.

What Lean computed:

10000

Checks acceptance criteria ONE-806.2.

53.3.3. Clawback exceeds due🔗

example

Rules.OneOrder.Accounting.clawbackExceedsDue : ℤ
Rules.OneOrder.Accounting.clawbackExceedsDue :
  ℤ

Given a clearing to a settlement payee that is due 200.00 EUR on one clearance and has 300.00 EUR clawed back on another.

When the clearing total is worked out.

Then it is minus 100.00 EUR, which a bank transfer to the payee cannot carry.

What Lean computed:

-10000

Checks acceptance criteria ONE-806.3.

53.4. Open question🔗

The guarantee Clearing totals are never negative is open: the example Clawback exceeds due shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.