55. Billing by service providers🔗

Requirement ONE-808. Of its 4 acceptance criteria, 4 are proven.

rule

Rules.OneOrder.Accounting.acceptBill
  (c : Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services : List Rules.OneOrder.Accounting.ProvidedService)
  (billed : List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill) : Bool
Rules.OneOrder.Accounting.acceptBill
  (c :
    Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services :
    List
      Rules.OneOrder.Accounting.ProvidedService)
  (billed :
    List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill) :
  Bool

EARS: If a service provider bills the ORA for a service before it has been delivered or consumed, then the system shall refuse the bill unless a bilateral agreement allows earlier billing.

Story: As an airline, I want providers to bill me only for what they have delivered, so that I never pay a provider for a service the customer did not receive.

Acceptance criteria:

ONE-808.1: If a service provider bills for a service that has not been delivered or consumed, then the system shall refuse the bill unless a bilateral agreement with that provider allows earlier billing.
ONE-808.2: If a service provider bills for a service another provider delivers, then the system shall refuse the bill.
ONE-808.3: The system shall keep the total billed for each service within its settlement value, and at zero while it has not been delivered or consumed unless a bilateral agreement allows earlier billing.
ONE-808.4: When a provider bills for a delivered service within what is left of its settlement value, the system shall accept the bill.

The bills are checked against the services' delivery statuses when they arrive. Which statuses count as delivered or consumed is a reading of the sources (ConsumptionReading). The result says whether the bill is accepted.

55.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-808.1	Proven	Billing after delivery, Partner seat bills
ONE-808.2	Proven	Bills from the delivering provider only, Other provider bill
ONE-808.3	Proven	Partner seat bills, Billing limited to delivered services
ONE-808.4	Proven	Partner seat bills, Bills for delivered services accepted

55.2. Guarantees🔗

55.2.1. Billing after delivery🔗

guarantee

Rules.OneOrder.Accounting.bill_refused_unless_consumed
  (c : Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services : List Rules.OneOrder.Accounting.ProvidedService)
  (billed : List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill)
  (s : Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find? (fun x ↦ x.service.id == b.serviceId) services = some s)
  (hc : c.consumed s.service.delivery = false)
  (ha : agreement b.provider = false) :
  Rules.OneOrder.Accounting.acceptBill c agreement services billed b =
    false
Rules.OneOrder.Accounting.bill_refused_unless_consumed
  (c :
    Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services :
    List
      Rules.OneOrder.Accounting.ProvidedService)
  (billed :
    List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill)
  (s :
    Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find?
        (fun x ↦
          x.service.id == b.serviceId)
        services =
      some s)
  (hc :
    c.consumed s.service.delivery = false)
  (ha : agreement b.provider = false) :
  Rules.OneOrder.Accounting.acceptBill c
      agreement services billed b =
    false

A bill for a service that is not delivered or consumed is refused unless the provider has a bilateral agreement, under every reading.

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

Checks acceptance criteria ONE-808.1.

55.2.2. Bills from the delivering provider only🔗

guarantee

Rules.OneOrder.Accounting.bill_refused_other_provider
  (c : Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services : List Rules.OneOrder.Accounting.ProvidedService)
  (billed : List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill)
  (s : Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find? (fun x ↦ x.service.id == b.serviceId) services = some s)
  (hp : s.provider ≠ b.provider) :
  Rules.OneOrder.Accounting.acceptBill c agreement services billed b =
    false
Rules.OneOrder.Accounting.bill_refused_other_provider
  (c :
    Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services :
    List
      Rules.OneOrder.Accounting.ProvidedService)
  (billed :
    List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill)
  (s :
    Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find?
        (fun x ↦
          x.service.id == b.serviceId)
        services =
      some s)
  (hp : s.provider ≠ b.provider) :
  Rules.OneOrder.Accounting.acceptBill c
      agreement services billed b =
    false

A bill from a provider that does not deliver the service is refused, under every reading.

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

Checks acceptance criteria ONE-808.2.

55.2.3. Billing limited to delivered services🔗

guarantee

Rules.OneOrder.Accounting.billed_within_value
  (c : Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services : List Rules.OneOrder.Accounting.ProvidedService)
  (bs : List Rules.OneOrder.Accounting.Bill)
  (s : Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find? (fun x ↦ x.service.id == s.service.id) services =
      some s) :
  Rules.OneOrder.Accounting.billedFor
      (Rules.OneOrder.Accounting.billAll c agreement services [] bs)
      s.service.id ≤
    if
        (c.consumed s.service.delivery || agreement s.provider) =
          true then
      s.settlementValue
    else 0
Rules.OneOrder.Accounting.billed_within_value
  (c :
    Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services :
    List
      Rules.OneOrder.Accounting.ProvidedService)
  (bs :
    List Rules.OneOrder.Accounting.Bill)
  (s :
    Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find?
        (fun x ↦
          x.service.id == s.service.id)
        services =
      some s) :
  Rules.OneOrder.Accounting.billedFor
      (Rules.OneOrder.Accounting.billAll c
        agreement services [] bs)
      s.service.id ≤
    if
        (c.consumed s.service.delivery ||
            agreement s.provider) =
          true then
      s.settlementValue
    else 0

Whatever bills providers send, the total billed for a service stays within its settlement value, and at zero while it is not delivered or consumed unless its provider has a bilateral agreement, under every reading.

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

Checks acceptance criteria ONE-808.3.

55.2.4. Bills for delivered services accepted🔗

guarantee

Rules.OneOrder.Accounting.delivered_bill_accepted
  (c : Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services : List Rules.OneOrder.Accounting.ProvidedService)
  (billed : List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill)
  (s : Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find? (fun x ↦ x.service.id == b.serviceId) services = some s)
  (hd : s.service.delivery = Rules.OneOrder.DeliveryStatus.delivered)
  (hp : s.provider = b.provider)
  (hle :
    Rules.OneOrder.Accounting.billedFor billed b.serviceId + b.amount ≤
      s.settlementValue) :
  Rules.OneOrder.Accounting.acceptBill c agreement services billed b =
    true
Rules.OneOrder.Accounting.delivered_bill_accepted
  (c :
    Rules.OneOrder.Accounting.ConsumptionReading)
  (agreement : String → Bool)
  (services :
    List
      Rules.OneOrder.Accounting.ProvidedService)
  (billed :
    List Rules.OneOrder.Accounting.Bill)
  (b : Rules.OneOrder.Accounting.Bill)
  (s :
    Rules.OneOrder.Accounting.ProvidedService)
  (hs :
    List.find?
        (fun x ↦
          x.service.id == b.serviceId)
        services =
      some s)
  (hd :
    s.service.delivery =
      Rules.OneOrder.DeliveryStatus.delivered)
  (hp : s.provider = b.provider)
  (hle :
    Rules.OneOrder.Accounting.billedFor
          billed b.serviceId +
        b.amount ≤
      s.settlementValue) :
  Rules.OneOrder.Accounting.acceptBill c
      agreement services billed b =
    true

A bill for a delivered service within what is left of its settlement value is accepted, under every reading.

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

Checks acceptance criteria ONE-808.4.

55.3. Examples🔗

55.3.1. Partner seat bills🔗

example

Rules.OneOrder.Accounting.partnerSeatBills :
  List Rules.OneOrder.Accounting.BillCase
Rules.OneOrder.Accounting.partnerSeatBills :
  List Rules.OneOrder.Accounting.BillCase

Given partner P's seat, with a settlement value of 120.00 EUR.

When P bills the ORA 120.00 EUR for it: after the passenger flew; after a no-show; before the flight; before the flight under a bilateral agreement; and again after the passenger flew and P already billed for it.

Then the bill after the flight is accepted under both readings, and the bill before the flight only with the agreement. The no-show bill is accepted only where NOT CLAIMED counts as consumed. The second bill is refused: it would exceed the settlement value.

What Lean computed:

Case	Delivered only	No show counts
flown	yes	yes
no-show	no	yes
before the flight	no	no
before the flight, with an agreement	yes	yes
flown, billed twice	no	no

Checks acceptance criteria ONE-808.1, ONE-808.3, ONE-808.4.

55.3.2. Other provider bill🔗

example

Rules.OneOrder.Accounting.otherProviderBill : Bool
Rules.OneOrder.Accounting.otherProviderBill :
  Bool

Given partner P's seat after the passenger flew.

When airline Q, which does not deliver the seat, bills the ORA for it.

Then the bill is refused under both readings.

What Lean computed:

Checks acceptance criteria ONE-808.2.