# MiFID II Transaction Reporting Classifier

## Technical Walkthrough

### Architecture

The `ReportingEngine` implements a **priority-based decision cascade** — a deterministic state machine where the first matching rule terminates evaluation.

```
┌─────────────────────────────────────────────────────────────────────┐
│                     ReportingEngine.classify(trade)                 │
├─────────────────────────────────────────────────────────────────────┤
│                                                                     │
│  ┌─────────────────────────────────────────────────────────────┐   │
│  │ Priority 1: is_eea_exchange(venue)?                         │   │
│  │             LSE, XPAR, XETR, XAMS ∈ EEA_EXCHANGES           │   │
│  └──────────────────────┬──────────────────────────────────────┘   │
│                         │ Yes → REPORTABLE                         │
│                         │ No ↓                                     │
│  ┌─────────────────────────────────────────────────────────────┐   │
│  │ Priority 2: instrument_region = EEA                         │   │
│  │             AND has_eea_counterparty(trade)?                │   │
│  └──────────────────────┬──────────────────────────────────────┘   │
│                         │ Yes → REPORTABLE                         │
│                         │ No ↓                                     │
│  ┌─────────────────────────────────────────────────────────────┐   │
│  │ Priority 3: venue = OTC                                     │   │
│  │             AND has_eea_counterparty(trade)?                │   │
│  └──────────────────────┬──────────────────────────────────────┘   │
│                         │ Yes → REPORTABLE                         │
│                         │ No ↓                                     │
│  ┌─────────────────────────────────────────────────────────────┐   │
│  │ Priority 4: Default                                         │   │
│  └──────────────────────┬──────────────────────────────────────┘   │
│                         │ → NOT REPORTABLE                         │
│                         ↓                                          │
└─────────────────────────────────────────────────────────────────────┘
```

### Data Model

```python
@dataclass(frozen=True)
class Trade:
    instrument_name: str                    # e.g., "BMW AG"
    instrument_region: Region               # EEA | US | APAC | OTHER
    venue: Venue                            # LSE | XPAR | XETR | NYSE | OTC | ...
    buyer_loc: CounterpartyLocation         # EEA | NON_EEA
    seller_loc: CounterpartyLocation        # EEA | NON_EEA
```

### The Invariants

#### Jurisdiction Safety (Verified)

**Mathematical Definition:**

$$\forall t \in \text{Trade}: \left( t.\text{venue} = \text{OTC} \land t.\text{buyer\_loc} = \text{NON\_EEA} \land t.\text{seller\_loc} = \text{NON\_EEA} \right) \implies \neg\text{is\_reportable}(t)$$

**Plain English:** An OTC trade between two non-European entities should never be reportable to ESMA, regardless of what financial instrument they are trading.

**IML Encoding:**

```ocaml
verify (fun t -> 
  (t.venue = OTC && t.buyer_loc = NON_EEA && t.seller_loc = NON_EEA) 
  ==> (is_reportable t = false)
)
```

**Status:** ✅ **PROVED** by ImandraX

---

### The Bug: What Went Wrong

#### Original (Buggy) Logic

```python
def is_reportable(trade: Trade) -> bool:
    # Priority 1: EEA Exchange
    if is_eea_exchange(trade.venue):
        return True
    
    # Priority 2: EEA Instrument - THE BUG
    if trade.instrument_region == Region.EEA:
        return True  # ← No counterparty check!
    
    # Priority 3: OTC with EEA Counterparty
    if trade.venue == Venue.OTC and has_eea_counterparty(trade):
        return True
    
    return False
```

**The Flaw:** Priority 2 checked `instrument_region == EEA` without verifying that at least one counterparty was an EEA entity. This caused jurisdictional overreach.

#### The Counterexample (Found by CodeLogician)

```ocaml
let t = {
  instrument_region = EEA;     (* Airbus, BMW, Siemens, etc. *)
  venue = OTC;                 (* Bilateral trade *)
  buyer_loc = NON_EEA;         (* US hedge fund *)
  seller_loc = NON_EEA         (* Singapore bank *)
}
(* Result: is_reportable(t) = true  ← WRONG! *)
```

**Business Translation:** A US hedge fund buying Airbus shares OTC from a Singapore bank would be incorrectly flagged for ESMA reporting. Neither party is European; neither has any MiFID II obligation.

#### The Fix

```python
# Priority 2: EEA Instrument - FIXED
if trade.instrument_region == Region.EEA and has_eea_counterparty(trade):
    return True  # ← Now requires EEA counterparty nexus
```

**The "Traded on a Trading Venue" (ToTV) nexus** under MiFID II requires an EEA Investment Firm to trigger the reporting obligation. The instrument's origin alone is insufficient.

---

### Region Decomposition

CodeLogician decomposed `is_reportable` into **8 distinct symbolic regions**:

| Region | Constraints | Output | Correctness |
|--------|-------------|--------|-------------|
| R1 | `venue = LSE` | `true` | ✅ EEA Exchange |
| R2 | `venue = XETR` | `true` | ✅ EEA Exchange |
| R3 | `venue = XPAR` | `true` | ✅ EEA Exchange |
| R4 | `instrument_region = EEA ∧ venue = NYSE ∧ has_eea_counterparty` | `true` | ✅ ToTV nexus |
| R5 | `instrument_region = EEA ∧ venue = OTC ∧ has_eea_counterparty` | `true` | ✅ ToTV nexus |
| R6 | `venue = OTC ∧ buyer_loc = EEA_CP ∧ ¬EEA_instrument` | `true` | ✅ OTC with EEA party |
| R7 | `venue = OTC ∧ buyer_loc ≠ EEA_CP ∧ seller_loc = EEA_CP ∧ ¬EEA_instrument` | `true` | ✅ OTC with EEA party |
| R8 | `venue = NYSE ∧ ¬EEA_instrument ∧ ¬has_eea_counterparty` | `false` | ✅ No EEA nexus |

**Key Insight:** Regions R4 and R5 now correctly require `has_eea_counterparty` in addition to `instrument_region = EEA`.

---

### Edge Cases Handled

| Scenario | Expected | Actual | Notes |
|----------|----------|--------|-------|
| EEA exchange, all Non-EEA parties | REPORTABLE | REPORTABLE | Venue takes precedence |
| OTC, EEA instrument, Non-EEA parties | NOT REPORTABLE | NOT REPORTABLE | **Fixed bug** |
| OTC, US instrument, one EEA party | REPORTABLE | REPORTABLE | EEA counterparty nexus |
| NYSE, EEA instrument, EEA buyer | REPORTABLE | REPORTABLE | ToTV with EEA firm |
| NYSE, US instrument, Non-EEA parties | NOT REPORTABLE | NOT REPORTABLE | No EEA nexus |

---

### Formal Verification Summary

| Metric | Value |
|--------|-------|
| **Formalization Status** | TRANSPARENT (fully executable) |
| **Invariants Verified** | 1 (Jurisdiction Safety) |
| **Counterexamples Found** | 1 (in original buggy code) |
| **Proof Status** | PROVED (after fix) |
| **Regions Decomposed** | 8 |

---

*Model verified with Imandra CodeLogician v2024*