50. Accepting a clearance🔗

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

rule

Rules.OneOrder.Accounting.submit
  (r : Rules.OneOrder.Accounting.RepeatReading)
  (accepted : List Rules.OneOrder.Accounting.Clearance)
  (c : Rules.OneOrder.Accounting.Clearance) :
  Except Rules.OneOrder.Accounting.ClearanceRejection
    (List Rules.OneOrder.Accounting.Clearance)
Rules.OneOrder.Accounting.submit
  (r :
    Rules.OneOrder.Accounting.RepeatReading)
  (accepted :
    List
      Rules.OneOrder.Accounting.Clearance)
  (c :
    Rules.OneOrder.Accounting.Clearance) :
  Except
    Rules.OneOrder.Accounting.ClearanceRejection
    (List
      Rules.OneOrder.Accounting.Clearance)

EARS: When the ORA sends a clearance, the system shall accept it unless it repeats a clearance already accepted, and record only accepted clearances.

Story: As an airline, I want the Clearance Manager to accept each payment's clearance once, so that no payment is settled twice.

Acceptance criteria:

ONE-803.1: If a clearance repeats the clearance ID of one already accepted, then the system shall reject it.
ONE-803.2: If a clearance not signed by both parties repeats the order ID and payment ID of one already accepted, then the system shall reject it.
ONE-803.3: When the Clearance Manager accepts a clearance, the system shall add it to the accepted clearances and change none of the others.
ONE-803.4: The system shall accept at most one clearance for each pair of order ID and payment ID.

A payment split across two payment methods has a transaction per method, each with its own payment ID, and so two clearances. Whether a signed clearance is checked for a repeated order and payment is a reading of the sources (RepeatReading). The result is the accepted clearances afterwards, or the reason for the rejection.

50.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-803.1	Proven	Repeated clearances, Repeated clearance ID
ONE-803.2	Proven	Repeated clearances, Repeated payment without signatures
ONE-803.3	Proven	Split payment cleared, Accepted clearances recorded
ONE-803.4	Open	Signed twice, One clearance per payment commitment

50.2. Guarantees🔗

50.2.1. Repeated clearance ID🔗

guarantee

Rules.OneOrder.Accounting.repeated_id_rejected
  (r : Rules.OneOrder.Accounting.RepeatReading)
  (acc : List Rules.OneOrder.Accounting.Clearance)
  (c : Rules.OneOrder.Accounting.Clearance)
  (h : ∃ a ∈ acc, a.id = c.id) :
  Rules.OneOrder.Accounting.submit r acc c =
    Except.error Rules.OneOrder.Accounting.ClearanceRejection.repeatedId
Rules.OneOrder.Accounting.repeated_id_rejected
  (r :
    Rules.OneOrder.Accounting.RepeatReading)
  (acc :
    List
      Rules.OneOrder.Accounting.Clearance)
  (c :
    Rules.OneOrder.Accounting.Clearance)
  (h : ∃ a ∈ acc, a.id = c.id) :
  Rules.OneOrder.Accounting.submit r acc
      c =
    Except.error
      Rules.OneOrder.Accounting.ClearanceRejection.repeatedId

A clearance whose clearance ID is already accepted is rejected, under every reading.

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

Checks acceptance criteria ONE-803.1.

50.2.2. Repeated payment without signatures🔗

guarantee

Rules.OneOrder.Accounting.repeated_unsigned_rejected
  (r : Rules.OneOrder.Accounting.RepeatReading)
  (acc : List Rules.OneOrder.Accounting.Clearance)
  (c : Rules.OneOrder.Accounting.Clearance) (hs : c.signed = false)
  (h : ∃ a ∈ acc, a.commitment = c.commitment) :
  ∃ e, Rules.OneOrder.Accounting.submit r acc c = Except.error e
Rules.OneOrder.Accounting.repeated_unsigned_rejected
  (r :
    Rules.OneOrder.Accounting.RepeatReading)
  (acc :
    List
      Rules.OneOrder.Accounting.Clearance)
  (c :
    Rules.OneOrder.Accounting.Clearance)
  (hs : c.signed = false)
  (h :
    ∃ a ∈ acc,
      a.commitment = c.commitment) :
  ∃ e,
    Rules.OneOrder.Accounting.submit r acc
        c =
      Except.error e

A clearance not signed by both parties whose order ID and payment ID are already accepted is rejected, under every reading.

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

Checks acceptance criteria ONE-803.2.

50.2.3. Accepted clearances recorded🔗

guarantee

Rules.OneOrder.Accounting.accepted_recorded
  (r : Rules.OneOrder.Accounting.RepeatReading)
  (acc acc' : List Rules.OneOrder.Accounting.Clearance)
  (c : Rules.OneOrder.Accounting.Clearance)
  (h : Rules.OneOrder.Accounting.submit r acc c = Except.ok acc') :
  acc' = acc ++ [c]
Rules.OneOrder.Accounting.accepted_recorded
  (r :
    Rules.OneOrder.Accounting.RepeatReading)
  (acc acc' :
    List
      Rules.OneOrder.Accounting.Clearance)
  (c :
    Rules.OneOrder.Accounting.Clearance)
  (h :
    Rules.OneOrder.Accounting.submit r acc
        c =
      Except.ok acc') :
  acc' = acc ++ [c]

An accepted clearance is added after those accepted before, which stay as they were, under every reading.

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

Checks acceptance criteria ONE-803.3.

50.2.4. One clearance per payment commitment🔗

guarantee

Rules.OneOrder.Accounting.one_clearance_per_payment
  (r : Rules.OneOrder.Accounting.RepeatReading)
  (cs : List Rules.OneOrder.Accounting.Clearance) :
  (List.map (fun x ↦ x.commitment)
      (Rules.OneOrder.Accounting.submitAll r [] cs)).Nodup
Rules.OneOrder.Accounting.one_clearance_per_payment
  (r :
    Rules.OneOrder.Accounting.RepeatReading)
  (cs :
    List
      Rules.OneOrder.Accounting.Clearance) :
  (List.map (fun x ↦ x.commitment)
      (Rules.OneOrder.Accounting.submitAll
        r [] cs)).Nodup

Every pair of an order ID and a payment ID has at most one accepted clearance, whatever clearances the ORA sends.

Open question for the business. The Clearance Manager checks clearance data signed by both parties only for a repeated clearance ID. Two signed clearances for one payment with different clearance IDs are both accepted. The example signedTwice shows it. May one payment have two signed clearances with different clearance IDs?

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

Checks acceptance criteria ONE-803.4.

50.3. Examples🔗

50.3.1. Repeated clearances🔗

example

Rules.OneOrder.Accounting.repeatedClearances :
  List Rules.OneOrder.Accounting.Decision
Rules.OneOrder.Accounting.repeatedClearances :
  List Rules.OneOrder.Accounting.Decision

Given an accepted clearance CLR-1 for order ORD-ACC-1 and payment PAY-1, not signed by both parties.

When the ORA sends CLR-1 again, and then an unsigned clearance CLR-3 for the same order and payment.

Then the Clearance Manager rejects the first as a repeated clearance ID and the second as a repeated payment.

What Lean computed:

Clearance	Outcome
CLR-1	ok
CLR-1	error repeated id
CLR-3	error repeated payment

Checks acceptance criteria ONE-803.1, ONE-803.2.

50.3.2. Split payment cleared🔗

example

Rules.OneOrder.Accounting.splitPaymentCleared :
  List Rules.OneOrder.Accounting.Decision
Rules.OneOrder.Accounting.splitPaymentCleared :
  List Rules.OneOrder.Accounting.Decision

Given a payment of 410.00 EUR split across two payment methods: 300.00 EUR through a settlement plan and 110.00 EUR through EasyPay, each with its own payment ID.

When the ORA sends a clearance for each.

Then the Clearance Manager accepts both, and each is recorded after the clearances accepted before.

What Lean computed:

Clearance	Outcome
CLR-1	ok
CLR-2	ok

Checks acceptance criteria ONE-803.3.

50.3.3. Signed twice🔗

example

Rules.OneOrder.Accounting.signedTwice :
  Rules.OneOrder.Accounting.AcceptedUnderReadings
Rules.OneOrder.Accounting.signedTwice :
  Rules.OneOrder.Accounting.AcceptedUnderReadings

Given two clearances for order ORD-ACC-1 and payment PAY-1, both signed by both parties, with clearance IDs CLR-1 and CLR-2.

When the ORA sends both.

Then when signed clearances are checked only for a repeated ID, both are accepted and the payment can be settled twice. When they are also checked for a repeated payment, only CLR-1 is accepted.

What Lean computed:

Id only: CLR-1, CLR-2
Id and payment: CLR-1

Checks acceptance criteria ONE-803.4.

50.4. Open question🔗

The guarantee One clearance per payment commitment is open: the example Signed twice shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.