Invoking agents via CLI
CodeLogician includes an agentic formalizer that can autonomously formalize source code into IML.
Running codelogician agent FILE will invoke CodeLogician's agentic formalizer ...
... and return the IML model produced and a json of the agent's state.
Options
By default, the agent will try to generate verification goals and decomposition requests. This can be disabled with
codelogician agent --no-artifacts FILESave the IML model and agent's state to files with names of your choosing by provding MODELFILE and OUTFILE.
codelogician agent FILE [MODELFILE] [OUTFILE]Evaluation via CLI
Region Decomposition
To perform region decomposition, a [@@decomp ...] annotation must be attached to the definition of the function of interest.
In the below example, we added
[@@decomp top ()]after the older_price and match_price functions.
IML
type order_type =
| Market
| Limit
| Quote
type order = {
order_id : int;
order_type : order_type;
order_qty : int;
order_price : real;
order_time : int;
}
type fill_price = real option
let older_price (o1 : order) (o2 : order) : real =
if o1.order_time > o2.order_time then
o2.order_price
else
o1.order_price
[@@decomp top ()]
type order_book = {
buys : order list;
sells : order list;
}
let best_buy (ob : order_book) : order option =
List.nth 0 ob.buys
let best_sell (ob : order_book) : order option =
List.nth 0 ob.sells
let next_buy (ob : order_book) : order option =
List.nth 1 ob.buys
let next_sell (ob : order_book) : order option =
List.nth 1 ob.sells
(_ Helper to access Option content safely or return default _)
let get_price (o : order option) : real option =
match o with
| Some x -> Some x.order_price
| None -> None
(_ Comparison operators for real numbers _)
let (<.) x y = Real.(x < y)
let (>.) x y = Real.(x > y)
let match_price (ob : order_book) (ref_price : real) : fill_price =
let bb = best_buy ob in
let bs = best_sell ob in
match bb, bs with
| Some bb, Some bs ->
let bb_type = bb.order_type in
let bs_type = bs.order_type in
if (bb_type = Limit && bs_type = Limit) || (bb_type = Quote && bs_type = Quote) then
Some (older_price bb bs)
else if bb_type = Market && bs_type = Market then
if bb.order_qty <> bs.order_qty then
None
else
let b_bid =
match next_buy ob with
| Some nb -> if nb.order_type <> Market then Some nb.order_price else None
| None -> None
in
let b_ask =
match next_sell ob with
| Some ns -> if ns.order_type <> Market then Some ns.order_price else None
| None -> None
in
match b_bid, b_ask with
| None, None -> Some ref_price
| None, Some ask -> Some (if ask <. ref_price then ask else ref_price)
| Some bid, None -> Some (if bid >. ref_price then bid else ref_price)
| Some bid, Some ask ->
if bid >. ref_price then Some bid
else if ask <. ref_price then Some ask
else Some ref_price
else if bb_type = Market && bs_type = Limit then
Some bs.order_price
else if bb_type = Limit && bs_type = Market then
Some bb.order_price
else if bb_type = Quote && bs_type = Limit then
if bb.order_time > bs.order_time then
(* incoming quote *)
if bb.order_qty < bs.order_qty then
Some bs.order_price
else if bb.order_qty = bs.order_qty then
match next_sell ob with
| Some ns -> Some ns.order_price
| None -> Some bb.order_price
else
None
else
(* existing quote's price used *)
Some bb.order_price
else if bb_type = Quote && bs_type = Market then
if bb.order_time > bs.order_time then
(* incoming quote *)
let next_sell_limit = next_sell ob in
if bb.order_qty < bs.order_qty then
Some bs.order_price
else if bb.order_qty = bs.order_qty then
match next_sell_limit with
| Some ns -> Some ns.order_price
| None -> Some bb.order_price
else
None
else
Some bb.order_price
else if bb_type = Limit && bs_type = Quote then
if bb.order_time > bs.order_time then
(* incoming quote *)
if bs.order_qty < bb.order_qty then
Some bb.order_price
else if bs.order_qty = bb.order_qty then
match next_buy ob with
| Some nb -> Some nb.order_price
| None -> Some bs.order_price
else
None
else
Some bs.order_price
else if bb_type = Market && bs_type = Quote then
if bb.order_time > bs.order_time then
(* incoming quote *)
if bs.order_qty < bb.order_qty then
Some bs.order_price
else if bb.order_qty = bs.order_qty then
match next_buy ob with
| Some nb -> Some nb.order_price
| None -> Some bs.order_price
else
None
else
Some bs.order_price
else
None
| \_ -> None
[@@decomp top ()]
Begin the region decomposition with
codelogician eval check-decomp MODELFILE
Learn more about region decomposition here.
Verification Goals
Use [@@verify ...] annotations to express verification goals.
We'll use the UBS Dark Pool example to demonstrate.
The IML file has two verification goals for properties that we want to hold true.
IML
type order_side = Buy | Sell | SellShort
type order_peg = Near | Mid | Far | NoPeg
type order_type =
| Market
| Limit
| Pegged
| PeggedCI
| LimitCI
| FirmUpPegged
| FirmUpLimit
let is*ci (ot : order_type) : bool =
match ot with
| PeggedCI | LimitCI -> true
| * -> false
let is*limit_type (ot : order_type) : bool =
match ot with
| Limit | LimitCI | FirmUpLimit -> true
| * -> false
let is*pegged_type (ot : order_type) : bool =
match ot with
| Pegged | PeggedCI | FirmUpPegged -> true
| * -> false
type market_data = {
nbb: real;
nbo: real;
l_up: real;
l_down: real
}
let mid_point (mkt: market_data) : real =
(mkt.nbb +. mkt.nbo) /. 2.0
let valid_market_data (mkt: market_data) : bool =
mkt.l_down >. 0.0 &&
mkt.nbb >. mkt.l_down &&
mkt.nbo >. mkt.nbb &&
mkt.l_up >. mkt.nbo
type order = {
id: int;
peg: order_peg;
client_id: int;
order_type: order_type;
qty: int;
min_qty: int;
leaves_qty: int;
price: real;
time: int
}
let valid_order (o: order) : bool =
o.leaves_qty <= o.qty &&
o.time >= 0 &&
o.price >. 0.0 &&
o.qty > 0 &&
o.leaves_qty >= 0
let less*aggressive (side: order_side) (lim_price: real) (far_price: real) : real =
if lim_price <. 0.0 then
far_price
else
match side with
| Buy -> min_r lim_price far_price
| * -> max_r lim_price far_price
let priority*price (side: order_side) (o: order) (mkt: market_data) : real =
match o.order_type with
| Limit | LimitCI | FirmUpLimit ->
(match side with
| Buy -> less_aggressive Buy o.price mkt.nbo
| * -> less*aggressive Sell o.price mkt.nbb)
| Market ->
(match side with
| Buy -> mkt.nbo
| * -> mkt.nbb)
| _ -> (* Pegged types *)
match o.peg with
| Far ->
less_aggressive side o.price
(match side with
| Buy -> mkt.nbo
| _ -> mkt.nbb)
| Mid ->
less*aggressive side o.price (mid_point mkt)
| Near ->
less_aggressive side o.price
(match side with
| Buy -> mkt.nbb
| * -> mkt.nbo)
| NoPeg -> o.price
let order_higher_ranked (side: order_side) (o1: order) (o2: order) (market: market_data) : bool =
let p_price1 = priority_price side o1 market in
let p_price2 = priority_price side o2 market in
let price*comparison =
match side with
| Buy -> p_price1 -. p_price2
| * -> p_price2 -. p_price1
in
if price*comparison >. 0.0 then
true
else if price_comparison <. 0.0 then
false
else
(* Same price level - apply additional rules \_)
if is_ci o1.order_type && is_ci o2.order_type then
o1.leaves_qty > o2.leaves_qty
else if o1.time <> o2.time then
o1.time < o2.time
else if not (is_ci o1.order_type) && is_ci o2.order_type then
true
else if is_ci o1.order_type && not (is_ci o2.order_type) then
false
else
o1.leaves_qty > o2.leaves_qty
let rank_transitivity (side: order_side) (o1: order) (o2: order) (o3: order) (market: market_data) : bool =
if order_higher_ranked side o1 o2 market && order_higher_ranked side o2 o3 market then
order_higher_ranked side o1 o3 market
else
true
verify (fun side o1 o2 o3 market -> if order_higher_ranked side o1 o2 market && order_higher_ranked side o2 o3 market then order_higher_ranked side o1 o3 market else true)
verify (fun side o1 o2 o3 market -> (valid_order o1 && valid_order o2 && valid_order o3 && valid_market_data market) ==> rank_transitivity side o1 o2 o3 market)
Perform verification with
codelogician eval check-vg MODELFILE
The results show that ImandraX was able to find counterexamples to the verification goals.