verify_aml_flag raises Z3Exception on NaN/Infinity amounts through the UCP payment stack; negative amounts never flag

[rahuldass19]

Summary

ComplianceGuard.verify_aml_flag — the AML control — has two failure modes on adversarial numeric input, both CONFIRMED BY EXECUTION:

1. Crash instead of verdict: NaN or Infinity amounts raise an unhandled z3types.Z3Exception: parser error out of the guard. The exception propagates through UCPIntegration.verify_payment_token with no try/except — so a sanctioned-country, KYC-less payment with a NaN amount raises instead of returning BLOCKED/PENDING_REVIEW. Whether the transaction then proceeds is decided by whatever upstream except the integrator happens to have. An AML control must return a conservative verdict, never raise.
2. Negative amounts never flag: verify_aml_flag(amount=-1_000_000, country_code="US", llm_flagged=False) → compliant=True. amount >= threshold passes for any negative value; sign is never validated.

Location

• qwed_finance/compliance_guard.py:96-101 → :123 — s.add(amt == amount) with a non-finite float crashes Z3's RealVal
• qwed_finance/compliance_guard.py:96 — should_flag = amount >= threshold or is_high_risk (no sign check)
• qwed_finance/integrations/ucp.py:134-143 — calls the guard unguarded; exception escapes verify_payment_token

Evidence (CONFIRMED BY EXECUTION, v2.1.0 @ 26d6dd0)

verify_aml_flag(amount=float("nan"), country_code="KP", llm_flagged=False)
  → z3types.Z3Exception (unhandled)
UCPIntegration().verify_payment_token({"amount": float("nan"),
  "customer_country":"KP","kyc_verified":False}) → same exception
verify_aml_flag(amount=-1_000_000, country_code="US", ...) → compliant=True

Impact

The failure mode of an AML/sanctions gate on hostile input is delegated to caller error-handling. A swallowed exception upstream = unflagged transaction. The negative-amount gap additionally lets any negative-amount path bypass flagging outright.

Fix

1. Finite-check at entry: non-finite amount → BLOCKED/compliant=False verdict (never reach the solver).
2. Wrap the Z3 section with a fail-closed fallback (the non-Z3 _verify_aml_fallback already exists — route to it on solver failure).
3. Decide negative-amount policy explicitly: flag on abs(amount) >= threshold, or reject negatives as invalid input.
4. Same finite-guard for UCPIntegration.verify_payment_token before the amount checks (NaN currently also slips past amount > max / amount <= 0 comparisons since both are False for NaN).