1(* Phantom type for currency safety *)
2type usd
3type eur
4type gbp
5
6type 'currency price = {
7  cents : int64;  (* Store as cents to avoid floating-point *)
8}
9
10let usd cents = { cents }
11let eur cents = { cents }
12let gbp cents = { cents }
13
14(* Convert dollars to cents *)
15let usd_of_float (dollars : float) : usd price =
16  { cents = Int64.of_float (dollars *. 100.0) }
17
18let eur_of_float (euros : float) : eur price =
19  { cents = Int64.of_float (euros *. 100.0) }
20
21(* Currency-safe operations *)
22let add_price : 'c price -> 'c price -> 'c price =
23  fun p1 p2 -> { cents = Int64.add p1.cents p2.cents }
24
25let sub_price : 'c price -> 'c price -> 'c price =
26  fun p1 p2 -> { cents = Int64.sub p1.cents p2.cents }
27
28let mul_price : 'c price -> int64 -> 'c price =
29  fun p factor -> { cents = Int64.mul p.cents factor }
30
31(* This compiles *)
32let total_usd = 
33  add_price (usd_of_float 100.0) (usd_of_float 50.0)
34
35(* This doesn't compile - prevents currency mixing! *)
36(* let invalid = add_price (usd_of_float 100.0) (eur_of_float 50.0) *)
37

1(* Order quantity must be positive *)
2module Quantity : sig
3  type t = private int64
4  val create : int64 -> t option
5  val to_int64 : t -> int64
6  val ( + ) : t -> t -> t
7  val ( - ) : t -> t option  (* Can result in negative, so option *)
8end = struct
9  type t = int64
10  
11  let create n = 
12    if n > 0L then Some n else None
13  
14  let to_int64 t = t
15  
16  let ( + ) = Int64.add
17  
18  let ( - ) a b =
19    let result = Int64.sub a b in
20    if result > 0L then Some result else None
21end
22
23(* Percentage between 0 and 100 *)
24module Percentage : sig
25  type t = private float
26  val create : float -> t option
27  val to_float : t -> float
28  val to_basis_points : t -> int
29end = struct
30  type t = float
31  
32  let create f =
33    if f >= 0.0 && f <= 100.0 then Some f else None
34  
35  let to_float t = t
36  
37  let to_basis_points t = int_of_float (t *. 100.0)
38end
39
40(* Usage *)
41let calculate_fee (amount : usd price) (rate : Percentage.t) : usd price =
42  let rate_float = Percentage.to_float rate /. 100.0 in
43  let fee_cents = Int64.of_float (Int64.to_float amount.cents *. rate_float) in
44  { cents = fee_cents }
45
46(* This prevents invalid states at compile time *)
47match Quantity.create 100L with
48| Some qty -> Printf.printf "Valid quantity: %Ld\n" (Quantity.to_int64 qty)
49| None -> Printf.printf "Invalid quantity\n"
50
51match Percentage.create 150.0 with
52| Some _ -> Printf.printf "Valid percentage\n"
53| None -> Printf.printf "Invalid percentage (> 100)\n"  (* This path taken *)
54

1(* Order states with associated data *)
2type pending = { submitted_at : float }
3type accepted = { order_id : string; accepted_at : float }
4type filled = { order_id : string; fill_price : int64; filled_at : float }
5type rejected = { reason : string; rejected_at : float }
6
7(* GADT encoding state machine *)
8type _ order_state =
9  | Pending : pending -> pending order_state
10  | Accepted : accepted -> accepted order_state
11  | Filled : filled -> filled order_state
12  | Rejected : rejected -> rejected order_state
13
14type 'state order = {
15  account_id : string;
16  symbol : string;
17  quantity : Quantity.t;
18  state : 'state order_state;
19}
20
21(* Only accepted orders can be filled *)
22let fill_order 
23    (order : accepted order) 
24    (fill_price : int64) 
25  : filled order =
26  match order.state with
27  | Accepted acc ->
28      { order with 
29        state = Filled {
30          order_id = acc.order_id;
31          fill_price;
32          filled_at = Unix.gettimeofday ();
33        }
34      }
35
36(* Only accepted or filled orders have order_id *)
37let get_order_id : type s. s order -> string option = fun order ->
38  match order.state with
39  | Pending _ -> None
40  | Rejected _ -> None
41  | Accepted acc -> Some acc.order_id
42  | Filled f -> Some f.order_id
43
44(* This won't compile - can't fill a pending order! *)
45(* let fill_pending (order : pending order) = fill_order order 150_00L *)
46

1(* why3ml *)
2module RiskCalculation
3  use int.Int
4  use real.Real
5  use real.FromInt
6  
7  (* Verify position value calculation *)
8  let calculate_position_value (price : int) (quantity : int) : int
9    requires { price > 0 }
10    requires { quantity >= 0 }
11    ensures { result = price * quantity }
12    ensures { result >= 0 }
13  =
14    price * quantity
15  
16  (* Verify portfolio value is sum of positions *)
17  let rec calculate_portfolio_value (positions : list (int * int)) : int
18    variant { positions }
19    ensures { result >= 0 }
20  =
21    match positions with
22    | Nil -> 0
23    | Cons (price, qty) rest ->
24        let pos_value = calculate_position_value price qty in
25        pos_value + calculate_portfolio_value rest
26    end
27  
28  (* Verify risk limit check *)
29  let check_risk_limit (position_value : int) (limit : int) : bool
30    requires { position_value >= 0 }
31    requires { limit > 0 }
32    ensures { result = true <-> position_value <= limit }
33  =
34    position_value <= limit
35  
36  (* Prove that if individual positions are within limit,
37     portfolio is within total limit *)
38  let lemma positions_under_limit (positions : list (int * int)) (limit : int)
39    requires { forall price qty. mem (price, qty) positions -> 
40               calculate_position_value price qty <= limit }
41    ensures { calculate_portfolio_value positions <= 
42              length positions * limit }
43  = ()
44end
45

1(* Order book invariants *)
2module OrderBook
3  use int.Int
4  use list.List
5  use list.Append
6  
7  type order = {
8    id : int;
9    price : int;
10    quantity : int;
11  }
12  
13  (* Bids sorted descending by price *)
14  predicate sorted_bids (bids : list order) =
15    forall i j. 0 <= i < j < length bids ->
16      nth i bids.price >= nth j bids.price
17  
18  (* Asks sorted ascending by price *)
19  predicate sorted_asks (asks : list order) =
20    forall i j. 0 <= i < j < length asks ->
21      nth i asks.price <= nth j asks.price
22  
23  (* Best bid is higher than best ask = crossed book = match opportunity *)
24  predicate can_match (bids : list order) (asks : list order) =
25    match bids, asks with
26    | Cons bid _, Cons ask _ -> bid.price >= ask.price
27    | _, _ -> false
28    end
29  
30  (* Match orders and verify invariants maintained *)
31  let match_orders (bids : list order) (asks : list order)
32    requires { sorted_bids bids }
33    requires { sorted_asks asks }
34    requires { can_match bids asks }
35    ensures { let (new_bids, new_asks, _) = result in
36              sorted_bids new_bids /\ sorted_asks new_asks }
37  =
38    match bids, asks with
39    | Cons bid rest_bids, Cons ask rest_asks ->
40        if bid.price >= ask.price then
41          let match_qty = min bid.quantity ask.quantity in
42          let execution_price = ask.price in  (* Price-time priority *)
43          
44          (* Update or remove orders based on quantities *)
45          let new_bids = 
46            if bid.quantity > match_qty then
47              Cons {bid with quantity = bid.quantity - match_qty} rest_bids
48            else rest_bids
49          in
50          let new_asks =
51            if ask.quantity > match_qty then
52              Cons {ask with quantity = ask.quantity - match_qty} rest_asks
53            else rest_asks
54          in
55          (new_bids, new_asks, Some (execution_price, match_qty))
56        else
57          (bids, asks, None)
58    | _, _ -> (bids, asks, None)
59    end
60end
61

1open QCheck
2
3(* Properties of order matching *)
4let test_order_matching =
5  Test.make 
6    ~name:"order matching preserves total quantity"
7    (pair (list (pair small_nat small_nat)) (list (pair small_nat small_nat)))
8    (fun (bids, asks) ->
9      let total_bid_qty = List.fold_left (fun acc (_, qty) -> acc + qty) 0 bids in
10      let total_ask_qty = List.fold_left (fun acc (_, qty) -> acc + qty) 0 asks in
11      
12      let (new_bids, new_asks, matches) = match_orders bids asks in
13      
14      let new_bid_qty = List.fold_left (fun acc (_, qty) -> acc + qty) 0 new_bids in
15      let new_ask_qty = List.fold_left (fun acc (_, qty) -> acc + qty) 0 new_asks in
16      let matched_qty = List.fold_left (fun acc (_, qty) -> acc + qty) 0 matches in
17      
18      (* Quantity is conserved *)
19      total_bid_qty = new_bid_qty + matched_qty &&
20      total_ask_qty = new_ask_qty + matched_qty
21    )
22
23(* Properties of currency conversions *)
24let test_currency_conversion =
25  Test.make
26    ~name:"currency conversion roundtrip"
27    (triple (float_range 0.0 10000.0) (float_range 0.01 100.0) (float_range 0.01 100.0))
28    (fun (amount, rate1, rate2) ->
29      let usd = usd_of_float amount in
30      let eur = convert_currency usd rate1 in
31      let back_to_usd = convert_currency eur rate2 in
32      
33      (* Allow small floating point error *)
34      let expected = Int64.of_float (amount *. rate1 *. rate2 *. 100.0) in
35      abs (Int64.to_float back_to_usd.cents -. Int64.to_float expected) < 1.0
36    )
37
38let () =
39  QCheck_runner.run_tests [
40    test_order_matching;
41    test_currency_conversion;
42  ]
43

1(* ppx_invariant adds automatic invariant checking *)
2type account = {
3  id : string;
4  balance : int64; [@invariant Int64.(>=) 0L]  (* Balance never negative *)
5  positions : (string * int64) list;
6} [@@deriving invariant]
7
8let debit_account account amount =
9  let new_balance = Int64.sub account.balance amount in
10  { account with balance = new_balance }
11  (* Automatically checks: new_balance >= 0L *)
12
13(* This raises Invariant_violation at runtime *)
14let () =
15  let acc = { id = "ACC001"; balance = 100L; positions = [] } in
16  let _ = debit_account acc 150L in  (* Violates invariant! *)
17  ()
18

1open Effect
2open Effect.Deep
3
4(* Define database effect *)
5type _ Effect.t +=
6  | Query : string -> string list Effect.t
7  | Execute : string -> unit Effect.t
8
9(* Transaction effect *)
10type _ Effect.t +=
11  | Begin_transaction : unit Effect.t
12  | Commit : unit Effect.t
13  | Rollback : unit Effect.t
14
15(* Safe transaction wrapper *)
16let with_transaction f =
17  match_with f ()
18  {
19    retc = (fun result ->
20      perform Commit;
21      result
22    );
23    exnc = (fun exn ->
24      perform Rollback;
25      raise exn
26    );
27    effc = (fun (type a) (eff : a Effect.t) ->
28      match eff with
29      | Begin_transaction -> Some (fun (k : (a, _) continuation) ->
30          (* Start transaction *)
31          continue k ()
32        )
33      | _ -> None
34    )
35  }
36
37(* Example usage *)
38let transfer_money from_acc to_acc amount =
39  with_transaction (fun () ->
40    perform Begin_transaction;
41    
42    (* Debit source account *)
43    let query = Printf.sprintf "UPDATE accounts SET balance = balance - %Ld WHERE id = '%s'" amount from_acc in
44    perform (Execute query);
45    
46    (* Credit destination account *)
47    let query = Printf.sprintf "UPDATE accounts SET balance = balance + %Ld WHERE id = '%s'" amount to_acc in
48    perform (Execute query);
49    
50    (* Automatically commits on success, rolls back on exception *)
51  )
52

1(* Public interface enforces safe usage *)
2module type POSITION = sig
3  type t
4  
5  val create : symbol:string -> quantity:int64 -> price:int64 -> t option
6  val symbol : t -> string
7  val quantity : t -> int64
8  val update_price : t -> int64 -> t
9  val close : t -> int64  (* Returns P&L, consumes position *)
10end
11
12(* Implementation with invariants *)
13module Position : POSITION = struct
14  type t = {
15    symbol : string;
16    quantity : int64;
17    average_price : int64;
18  }
19  
20  let create ~symbol ~quantity ~price =
21    if quantity > 0L && price > 0L then
22      Some { symbol; quantity; average_price = price }
23    else
24      None
25  
26  let symbol t = t.symbol
27  let quantity t = t.quantity
28  
29  let update_price t new_price =
30    if new_price > 0L then
31      { t with average_price = new_price }
32    else
33      t
34  
35  let close t =
36    (* Calculate P&L *)
37    Int64.mul t.quantity t.average_price
38end
39
40(* Users can't construct invalid positions *)
41match Position.create ~symbol:"AAPL" ~quantity:100L ~price:150_00L with
42| Some pos -> 
43    let pnl = Position.close pos in
44    Printf.printf "Closed position, P&L: %Ld\n" pnl
45| None -> 
46    Printf.printf "Invalid position parameters\n"
47