Verified Air

4. Accepting a refund🔗

Requirement OO-003. Of its 2 acceptance criteria, 1 is open and 1 is not checked yet.

🔗rule
Rules.OfferOrder.acceptRefund (p : Rules.OfferOrder.Payment)
  (r : Rules.OfferOrder.Refund) : Bool
Rules.OfferOrder.acceptRefund
  (p : Rules.OfferOrder.Payment)
  (r : Rules.OfferOrder.Refund) : Bool

EARS: When a refund is requested against a payment, the system shall accept it only if the refund amount does not exceed that payment's amount.

Story: As a customer service agent, I want each refund checked against the payment it is made against, so that a customer is never refunded more than they paid.

Acceptance criteria:

  • OO-003.1: When a refund is requested against a payment, the system shall accept it only if it names that payment and its amount does not exceed the payment's amount.

  • OO-003.2: The system shall not refund more against an order than was paid for it.

The check looks at this one refund and this one payment; it does not look at refunds already made against the same payment.

4.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

OO-003.1

Not checked

nothing yet

OO-003.2

Open

Double refund, Refunds never exceed payments

4.2. Try it🔗

Choose the inputs and see what the rule decides.

Try the rule

Loading the rule...

The answer comes from the Rust function accept_refund, compiled to WebAssembly and running in your browser. Lean proves that this function computes what the model computes, for every input (Verify/RustRules.lean). The few lines that pass your choices to it are not part of the proof.

The rule checks each refund on its own. The total of the accepted refunds is added up by this page.

4.3. Guarantees🔗

4.3.1. Refunds never exceed payments🔗

🔗guarantee
Rules.OfferOrder.refunds_le_payments
  (ps : List Rules.OfferOrder.Payment)
  (rs : List Rules.OfferOrder.Refund) (orderId : String)
  (hids : (List.map (fun x ↦ x.id) ps).Nodup)
  (hacc :
    ∀ r ∈ rs, ∃ p ∈ ps, Rules.OfferOrder.acceptRefund p r = true) :
  Rules.OfferOrder.totalRefunded ps rs orderId ≤
    Rules.OfferOrder.totalPaid ps orderId
Rules.OfferOrder.refunds_le_payments
  (ps : List Rules.OfferOrder.Payment)
  (rs : List Rules.OfferOrder.Refund)
  (orderId : String)
  (hids :
    (List.map (fun x ↦ x.id) ps).Nodup)
  (hacc :
    ∀ r ∈ rs,
      ∃ p ∈ ps,
        Rules.OfferOrder.acceptRefund p
            r =
          true) :
  Rules.OfferOrder.totalRefunded ps rs
      orderId ≤
    Rules.OfferOrder.totalPaid ps orderId

Refunds against an order never exceed what was paid for it, provided each refund was accepted against one of the order's payments.

Open question for the Offer/Order team. This does not hold as the rule is written: acceptRefund checks each refund against its payment alone, so two refunds of 60.00 USD against one payment of 100.00 USD are each accepted and together return 120.00 USD. The counterexample is the doubleRefund case. Does the rule mean the limit applies per refund, cumulatively per payment, or cumulatively per order? And is a refund above the amount paid ever allowed, for example as a goodwill credit?

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

Checks acceptance criteria OO-003.2.

4.4. Examples🔗

4.4.1. Double refund🔗

🔗example
Rules.OfferOrder.doubleRefund : Rules.OfferOrder.DoubleRefund
Rules.OfferOrder.doubleRefund :
  Rules.OfferOrder.DoubleRefund

Given one payment of 100.00 USD against order ORD-1.

When two refunds of 60.00 USD each are requested against that payment.

Then each refund is accepted, and together they return 120.00 USD, more than was paid. This is the counterexample for refunds_le_payments.

What Lean computed:

  • First accepted: yes

  • Second accepted: yes

  • Total refunded: 120.00 USD

Checks acceptance criteria OO-003.2.

4.5. Open question🔗

The guarantee Refunds never exceed payments is open: the example Double refund shows the rule as written breaking it. Open Questions sets out the question for the team.