A fill by price-time priority, live

What an open order fills this step, min(open, max(0, meeting − ahead)): the other side's open quantity at prices the order meets, less the quantity ahead of it on its own side (a better price, or the same price arrived earlier), never below nothing and never above what it has open (lusine.finance.fill). The two folds are the game's, over its book. Below, a market of eight traders runs on your GPU as you read: each step a new order is drawn, a buy of 1 to 20 shares at a limit from 99.80 EUR to 100.04 EUR or a sell at one from 99.96 EUR to 100.20 EUR, into a book of thirty-two slots, replacing the order thirty-two steps old and cancelling what was left of it. Every open order takes what the library's fill gives it, and each bid and ask whose takes overlap on their sides' walks trade, at the library's crossing price, the resting order's limit. The buyer pays the seller, to the cent.

This page runs the program on your GPU through WebGPU, so it needs a browser with WebGPU (a recent Chrome, Edge, Safari or Firefox). Without it the program does not run and nothing is drawn below.

What it shows

• The strip above the controls is green while every check holds, and turns red for good once one fails.
• The market: the chart draws the best bid and the best ask left after each step's match, and the last trade's price, each in cents above 99.80 EUR, a step at a time. Below it, the orders placed, the trades, the shares traded, and the cash and the shares all the traders hold.
• The book: each slot's side (true a bid), limit, open quantity, arrival and trader.
• The checks: shares change hands, the shares the bids take, the shares the asks take and the trades' shares the same at every step; cash and shares kept, the eight traders and their eight twins holding 160 000 EUR and 1 600 shares in all at every step, whatever has traded; never past a limit, every trade at the limit of the order that was resting, never above the bid's limit or below the ask's; price, then time, no order taking while an order ahead of it on its side is left open; the book uncrossed, the best bid left below the best ask after every match; the continuous match, the shares traded each step the new order's quantity or the other side's open quantity at a price it meets, the less, as a match one order at a time gives; the same market again, a second book drawn from the same seed with its rows in the opposite order, its traders' cash and shares the same as the first's at every step; Harris's book, asks of 5 at 100 and 5 at 101 against a bid of 8 at 101 and a bid of 4 at 101 after it, the first bid taking 8, the second the 2 left, and both asks their 5 (Harris, Trading and Exchanges, ch. 6); by hand, the kernel given the numbers of Harris's two bids filling 8 and 2, an order with more ahead of it than meets it, or nothing meeting it, filling nothing, one before a deeper book filling whole, and one with exactly what meets it ahead of it nothing. Each is held at every step.

Every number here is computed by the program on the GPU; the page only reads the values back and draws them. The seed, the lowest limit, the cents the limits span and how far above a buy's a sell's is drawn are the program's settings, which the host may write; this page offers no control to change them yet.

The program

The book twice, Harris's book, the trades, the traders and the checks, the panels the page draws, and the one procedure, main, run each step: a new order placed, the match, the trades settled, and the checks.

// The fill's live page: a market of eight traders and a book of thirty-two orders, a new order drawn into it each step
// and matched under price-time priority by the library's fill, each crossing a trade at the library's crossing price;
// the same market again from the same seed with its book's rows in the opposite order; and Harris's book worked by
// hand, with the page's checks computed here on the GPU and shown by the panels the program declares.

namespace fill;

lusine.version version = { { number = 1 } };

// The reader's settings: the seed the orders are drawn from; the lowest limit a buy is drawn at, and the cents a limit
// spans, a buy's from 99.80 EUR to 100.04 EUR; and how far above a buy's a sell's is drawn, 16 cents, so that the
// book's two sides overlap by eight cents and hold orders that have not met.
host struct {
  integer seed = 592; integer<EUR> low = 9980 EUR_minor quantum = 1 EUR_minor; integer ticks = 25;
  integer<EUR> lift = 16 EUR_minor quantum = 1 EUR_minor;
} settings;

// An order: its slot in the book, its side, its limit, when it arrived, its quantity and how much of it has filled, its
// trader, and this step's match: what is open, what it takes, and where its take starts on its side's walk; and, for
// the checks and the book's panel, the orders ahead of it left open where it took, and its limit in euros.
struct order {
  integer slot; bool buy; integer<EUR> price quantum = 1 EUR_minor; integer arrival; integer quantity; integer filled;
  integer trader; integer open; integer take; integer start; integer blocked; float<EUR> limit;
};

// The book: thirty-two slots, a new order each step in the slot after the last, which cancels what was left of the
// order it replaces; and the same book again, its rows in the opposite order, drawn from the same seed.
table<order> orders(capacity = 32) = {
  { slot = 0 }, { slot = 1 }, { slot = 2 }, { slot = 3 }, { slot = 4 }, { slot = 5 }, { slot = 6 }, { slot = 7 },
  { slot = 8 }, { slot = 9 }, { slot = 10 }, { slot = 11 }, { slot = 12 }, { slot = 13 }, { slot = 14 },
  { slot = 15 }, { slot = 16 }, { slot = 17 }, { slot = 18 }, { slot = 19 }, { slot = 20 }, { slot = 21 },
  { slot = 22 }, { slot = 23 }, { slot = 24 }, { slot = 25 }, { slot = 26 }, { slot = 27 }, { slot = 28 },
  { slot = 29 }, { slot = 30 }, { slot = 31 },
};
table<order> again(capacity = 32) = {
  { slot = 31 }, { slot = 30 }, { slot = 29 }, { slot = 28 }, { slot = 27 }, { slot = 26 }, { slot = 25 },
  { slot = 24 }, { slot = 23 }, { slot = 22 }, { slot = 21 }, { slot = 20 }, { slot = 19 }, { slot = 18 },
  { slot = 17 }, { slot = 16 }, { slot = 15 }, { slot = 14 }, { slot = 13 }, { slot = 12 }, { slot = 11 },
  { slot = 10 }, { slot = 9 }, { slot = 8 }, { slot = 7 }, { slot = 6 }, { slot = 5 }, { slot = 4 }, { slot = 3 },
  { slot = 2 }, { slot = 1 }, { slot = 0 },
};

// Harris's book: asks of 5 at 100 and 5 at 101 and a bid of 8 at 101, then a bid of 4 at 101 arriving after it.
host table<order> harris(capacity = 4) = {
  { slot = 0, buy = false, price = 10000 EUR_minor, arrival = 1, quantity = 5 },
  { slot = 1, buy = false, price = 10100 EUR_minor, arrival = 2, quantity = 5 },
  { slot = 2, buy = true, price = 10100 EUR_minor, arrival = 3, quantity = 8 },
  { slot = 3, buy = true, price = 10100 EUR_minor, arrival = 4, quantity = 4 },
};

// The kernel's cases by hand, each its open quantity, what meets it, what is ahead of it, and what it fills: Harris's
// two bids, 8 and then 2; an order with more ahead of it than meets it, and one with nothing meeting it, nothing; one
// before a deeper book, whole; and one with exactly what meets it ahead of it, nothing.
struct case { integer open; integer meeting; integer ahead; integer want; integer got; };
host table<case> cases(capacity = 6) = {
  { open = 8, meeting = 10, ahead = 0, want = 8 }, { open = 4, meeting = 10, ahead = 8, want = 2 },
  { open = 5, meeting = 3, ahead = 7, want = 0 }, { open = 5, meeting = 0, ahead = 0, want = 0 },
  { open = 5, meeting = 100, ahead = 20, want = 5 }, { open = 5, meeting = 7, ahead = 7, want = 0 },
};

// A trade: who bought and who sold, at what price and how many, and the two orders' limits and arrivals.
struct trade {
  integer buyer; integer seller; integer<EUR> price quantum = 1 EUR_minor; integer quantity;
  integer<EUR> bid quantum = 1 EUR_minor; integer<EUR> ask quantum = 1 EUR_minor; integer bid_arrival;
  integer ask_arrival;
};
table<trade> trades(capacity = 64, keep = 1 step);
table<trade> trades_again(capacity = 64, keep = 1 step);

// The traders, eight in the market and their eight twins in the market again, each with 10 000 EUR and 100 shares, and,
// for the check, its twin's cash and shares.
struct trader {
  integer number; integer<EUR> cash quantum = 1 EUR_minor; integer shares; integer<EUR> twin_cash quantum = 1 EUR_minor;
  integer twin_shares;
};
table<trader> traders(capacity = 16) = {
  { number = 0, cash = 10000 EUR, shares = 100 }, { number = 1, cash = 10000 EUR, shares = 100 },
  { number = 2, cash = 10000 EUR, shares = 100 }, { number = 3, cash = 10000 EUR, shares = 100 },
  { number = 4, cash = 10000 EUR, shares = 100 }, { number = 5, cash = 10000 EUR, shares = 100 },
  { number = 6, cash = 10000 EUR, shares = 100 }, { number = 7, cash = 10000 EUR, shares = 100 },
  { number = 8, cash = 10000 EUR, shares = 100 }, { number = 9, cash = 10000 EUR, shares = 100 },
  { number = 10, cash = 10000 EUR, shares = 100 }, { number = 11, cash = 10000 EUR, shares = 100 },
  { number = 12, cash = 10000 EUR, shares = 100 }, { number = 13, cash = 10000 EUR, shares = 100 },
  { number = 14, cash = 10000 EUR, shares = 100 }, { number = 15, cash = 10000 EUR, shares = 100 },
};

// The market: the step; the new order's quantity and what the book's other side has open at a price it meets, before
// the match; the shares traded this step and in all; the touch after the match and the last trade's price, and, for the
// chart, each in cents above the lowest limit, kept until there is one; the cash and the shares all the traders hold,
// and the cash in euros.
struct {
  integer step; integer wanted; integer traded; integer volume; integer trades;
  integer<EUR> bid quantum = 1 EUR_minor; integer<EUR> ask quantum = 1 EUR_minor;
  integer<EUR> last quantum = 1 EUR_minor;
  integer best_bid; integer best_ask; integer last_price;
  integer<EUR> cash quantum = 1 EUR_minor; integer shares; float<EUR> held;
} market;

// The checks: the shares each side takes equal and equal to the trades', and the traders' cash and shares in all as
// they began; every trade at the resting order's limit, never above the bid's or below the ask's; no order taking while
// an order ahead of it on its side is left open; the book uncrossed after the match, its best bid below its best ask;
// the new order filling what a continuous match gives it, its quantity or the other side's open quantity at a price it
// meets, the less; the market again, its rows in the opposite order, its traders' cash and shares the same at every
// step; and Harris's book and the kernel's limits worked by hand.
struct {
  bool shares = true; bool cash = true; bool limits = true; bool priority = true; bool uncrossed = true;
  bool continuous = true; bool again = true; bool harris = true; bool by_hand = true;
} checks;

// A strip of lamps the page draws, lit green while every check holds and red once one fails.
struct lamp { vector<float, 4> colour; };
lattice<lamp, 2> lamps(spacing = 1 m, boundary = wall);

vector<float, 4> lamp_colour(bool holds)
{
  return holds ? vector<float, 4>(0.15, 0.6, 0.3, 1.0) : vector<float, 4>(0.75, 0.15, 0.15, 1.0);
}

// A draw of this step's order: a word from the seed, the step and the stream's name.
integer drawn(integer seed, integer step, bits key, integer below)
{
  return integer(lusine.error.draw(seed = bits(seed), step = bits(step), key, index = bits(0)) >> 8) % below;
}

// A slot keeps its order unless this step's new order goes in it: a buy or a sell, a buy's limit from the lowest to the
// cents it spans above it and a sell's the lift higher, for 1 to 20 shares, of one of the eight traders (the twins'
// numbers eight on).
(bool, integer<EUR>, integer, integer, integer, integer) placed(integer slot, bool buy, integer<EUR> price,
                                                                integer arrival, integer quantity, integer filled,
                                                                integer trader, integer seed, integer step,
                                                                integer<EUR> low, integer ticks, integer<EUR> lift,
                                                                integer twin)
{
  if (slot != step % 32) return (buy, price, arrival, quantity, filled, trader);
  let buying = drawn(seed, step, key = fnv1a("side"), below = 2) == 0;
  let above = drawn(seed, step, key = fnv1a("price"), below = ticks) * 1 EUR_minor;
  return (buying, low + (buying ? 0 EUR_minor : lift) + above, step,
          1 + drawn(seed, step, key = fnv1a("quantity"), below = 20), 0,
          drawn(seed, step, key = fnv1a("trader"), below = 8) + twin);
}

integer open_of(integer quantity, integer filled) { return quantity - filled; }

// The other side's open quantity at a price this order meets: the asks at or under a bid's limit, the bids at or over
// an ask's.
integer meeting(bool buy, integer<EUR> price, table<bool> buys, table<integer<EUR>> prices, table<integer> opens)
{
  let b = buy;
  let p = price;
  return sum(opens) where opens > 0 && buys != b && (b ? prices <= p : prices >= p);
}

// The open quantity ahead of this order on its own side: a better price, or the same price arrived earlier.
integer ahead(bool buy, integer<EUR> price, integer arrival, table<bool> buys, table<integer<EUR>> prices,
              table<integer> arrivals, table<integer> opens)
{
  let b = buy;
  let p = price;
  let a = arrival;
  return sum(opens) where opens > 0 && buys == b && ((b ? prices > p : prices < p) || (prices == p && arrivals < a));
}

// What this order takes: the library's fill, given the two folds.
integer taking(integer open, bool buy, integer<EUR> price, integer arrival, table<bool> buys,
               table<integer<EUR>> prices, table<integer> arrivals, table<integer> opens)
{
  return lusine.finance.fill(open, meeting = meeting(buy, price, buys, prices, opens),
                             ahead = ahead(buy, price, arrival, buys, prices, arrivals, opens));
}

// Where this order's take starts on its side's walk: what the orders ahead of it took.
integer starting(bool buy, integer<EUR> price, integer arrival, table<bool> buys, table<integer<EUR>> prices,
                 table<integer> arrivals, table<integer> opens, table<integer> takes)
{
  let b = buy;
  let p = price;
  let a = arrival;
  return sum(takes) where opens > 0 && buys == b && ((b ? prices > p : prices < p) || (prices == p && arrivals < a));
}

// The shares a bid's take and an ask's share on the walk: the overlap of their intervals.
integer overlap(integer bid_start, integer bid_take, integer ask_start, integer ask_take)
{
  let from = bid_start > ask_start ? bid_start : ask_start;
  let to = bid_start + bid_take < ask_start + ask_take ? bid_start + bid_take : ask_start + ask_take;
  return to > from ? to - from : 0;
}

bool crossed(order b, order s)
{
  return b.buy && !s.buy && overlap(bid_start = b.start, bid_take = b.take, ask_start = s.start, ask_take = s.take) > 0;
}

// The trade of a crossing, at the library's crossing price.
trade traded(order b, order s)
{
  return trade {
    buyer = b.trader, seller = s.trader,
    price = lusine.finance.crossing_price(bid = b.price, bid_arrival = b.arrival, ask = s.price,
                                          ask_arrival = s.arrival),
    quantity = overlap(bid_start = b.start, bid_take = b.take, ask_start = s.start, ask_take = s.take),
    bid = b.price, ask = s.price, bid_arrival = b.arrival, ask_arrival = s.arrival
  };
}

// A trader's cash and shares after this step's trades: paid for what it sold, paying for what it bought.
integer<EUR> paid(integer number, integer<EUR> cash, table<integer> buyers, table<integer> sellers,
                  table<integer<EUR>> prices, table<integer> quantities)
{
  let n = number;
  return cash + (sum(prices * quantities) where sellers == n) - (sum(prices * quantities) where buyers == n);
}

integer bought(integer number, integer shares, table<integer> buyers, table<integer> sellers, table<integer> quantities)
{
  let n = number;
  return shares + (sum(quantities) where buyers == n) - (sum(quantities) where sellers == n);
}

// A twin's cash and shares, eight numbers on.
integer<EUR> twin_cash(integer number, table<integer> numbers, table<integer<EUR>> cashes)
{
  let n = number + 8;
  return sum(cashes) where numbers == n;
}

integer twin_shares(integer number, table<integer> numbers, table<integer> shareses)
{
  let n = number + 8;
  return sum(shareses) where numbers == n;
}

// The orders still open with a better price on their side, or the same price arrived earlier, where this one took.
integer blocking(integer take, bool buy, integer<EUR> price, integer arrival, table<bool> buys,
                 table<integer<EUR>> prices, table<integer> arrivals, table<integer> opens)
{
  if (take == 0) return 0;
  let b = buy;
  let p = price;
  let a = arrival;
  return count(opens) where opens > 0 && buys == b && ((b ? prices > p : prices < p) || (prices == p && arrivals < a));
}

// The new order's quantity, and the other side's open quantity at a price it meets: the less is what a continuous match
// fills.
integer wanting(table<integer> arrivals, table<integer> quantities, table<bool> buys, table<integer<EUR>> prices,
                table<integer> opens, integer step)
{
  let s = step;
  let q = sum(quantities) where arrivals == s;
  let b = any(buys) where arrivals == s && buys;
  let p = sum(prices) where arrivals == s;
  let m = sum(opens) where opens > 0 && arrivals != s && buys != b && (b ? prices <= p : prices >= p);
  return q < m ? q : m;
}

integer<EUR> touch_bid(table<bool> buys, table<integer<EUR>> prices, table<integer> opens)
{
  let p = max(prices) where buys && opens > 0;
  return p > 0 EUR_minor ? p : 0 EUR_minor;
}

integer<EUR> touch_ask(table<bool> buys, table<integer<EUR>> prices, table<integer> opens)
{
  let p = min(prices) where !buys && opens > 0;
  return p > 0 EUR_minor ? p : 0 EUR_minor;
}

// The last trade's price this step, or the last before it: an incoming bid walks up the asks, so its last trade is its
// highest; an incoming ask walks down the bids, so its last is its lowest.
integer<EUR> last_of(integer<EUR> last, table<integer<EUR>> prices, table<integer> bid_arrivals, integer step)
{
  let s = step;
  let highest = max(prices) where bid_arrivals == s;
  let lowest = min(prices) where bid_arrivals != s;
  if (highest > 0 EUR_minor) return highest;
  if (lowest > 0 EUR_minor) return lowest;
  return last;
}

// Every trade at the resting order's limit, the one that did not arrive this step, within the two limits.
bool at_limits(table<integer<EUR>> prices, table<integer<EUR>> bids, table<integer<EUR>> asks,
               table<integer> bid_arrivals, table<integer> ask_arrivals, integer step)
{
  let s = step;
  let wrong = count(prices) where prices > bids || prices < asks
                               || (bid_arrivals == s ? prices != asks : prices != bids);
  return wrong == 0;
}

integer taken(table<bool> buys, table<integer> takes, bool buy)
{
  let b = buy;
  return sum(takes) where buys == b;
}

bool harris_holds(table<integer> slots, table<integer> takes)
{
  let wrong = count(takes) where (slots == 0 && takes != 5) || (slots == 1 && takes != 5)
                              || (slots == 2 && takes != 8) || (slots == 3 && takes != 2);
  return wrong == 0;
}

integer wrong(table<integer> got, table<integer> want) { return count(got) where got != want; }

output table<lusine.widget> panels = {
  lusine.series { { panel = "the market", chart = "cents above 99.80 EUR", quantity = market.best_bid, steps = 200,
                    label = "best bid" } },
  lusine.series { { panel = "the market", chart = "cents above 99.80 EUR", quantity = market.best_ask, steps = 200,
                    label = "best ask" } },
  lusine.series { { panel = "the market", chart = "cents above 99.80 EUR", quantity = market.last_price, steps = 200,
                    label = "last trade" } },
  lusine.value { { panel = "the market", quantity = market.step, label = "orders placed" } },
  lusine.value { { panel = "the market", quantity = market.trades, label = "trades" } },
  lusine.value { { panel = "the market", quantity = market.volume, label = "shares traded" } },
  lusine.value { { panel = "the market", quantity = market.held, label = "cash held" } },
  lusine.value { { panel = "the market", quantity = market.shares, label = "shares held" } },
  lusine.column { { panel = "the book", table = "the book", quantity = orders.buy } },
  lusine.column { { panel = "the book", table = "the book", quantity = orders.limit } },
  lusine.column { { panel = "the book", table = "the book", quantity = orders.open } },
  lusine.column { { panel = "the book", table = "the book", quantity = orders.arrival } },
  lusine.column { { panel = "the book", table = "the book", quantity = orders.trader } },
  lusine.value { { panel = "the checks", quantity = checks.shares, label = "shares change hands" } },
  lusine.value { { panel = "the checks", quantity = checks.cash, label = "cash and shares kept" } },
  lusine.value { { panel = "the checks", quantity = checks.limits, label = "never past a limit" } },
  lusine.value { { panel = "the checks", quantity = checks.priority, label = "price, then time" } },
  lusine.value { { panel = "the checks", quantity = checks.uncrossed, label = "the book uncrossed" } },
  lusine.value { { panel = "the checks", quantity = checks.continuous, label = "the continuous match" } },
  lusine.value { { panel = "the checks", quantity = checks.again, label = "the same market again" } },
  lusine.value { { panel = "the checks", quantity = checks.harris, label = "Harris's book" } },
  lusine.value { { panel = "the checks", quantity = checks.by_hand, label = "by hand" } },
};

void main()
{
  market.step = market.step + 1;
  (orders.buy, orders.price, orders.arrival, orders.quantity, orders.filled, orders.trader)
    = placed(orders.slot, orders.buy, orders.price, orders.arrival, orders.quantity, orders.filled, orders.trader,
             settings.seed, step = market.step, settings.low, settings.ticks, settings.lift, twin = 0);
  (again.buy, again.price, again.arrival, again.quantity, again.filled, again.trader)
    = placed(again.slot, again.buy, again.price, again.arrival, again.quantity, again.filled, again.trader,
             settings.seed, step = market.step, settings.low, settings.ticks, settings.lift, twin = 8);
  orders.open = open_of(orders.quantity, orders.filled);
  again.open = open_of(again.quantity, again.filled);
  harris.open = open_of(harris.quantity, harris.filled);
  market.wanted = wanting(arrivals = orders.arrival, quantities = orders.quantity, buys = orders.buy,
                          prices = orders.price, opens = orders.open, step = market.step);

  // The match: what each order takes, where its take starts, and a trade for each bid and ask whose takes overlap.
  orders.take = taking(orders.open, orders.buy, orders.price, orders.arrival, buys = orders.buy,
                       prices = orders.price, arrivals = orders.arrival, opens = orders.open);
  again.take = taking(again.open, again.buy, again.price, again.arrival, buys = again.buy, prices = again.price,
                      arrivals = again.arrival, opens = again.open);
  harris.take = taking(harris.open, harris.buy, harris.price, harris.arrival, buys = harris.buy,
                       prices = harris.price, arrivals = harris.arrival, opens = harris.open);
  orders.start = starting(orders.buy, orders.price, orders.arrival, buys = orders.buy, prices = orders.price,
                          arrivals = orders.arrival, opens = orders.open, takes = orders.take);
  again.start = starting(again.buy, again.price, again.arrival, buys = again.buy, prices = again.price,
                         arrivals = again.arrival, opens = again.open, takes = again.take);
  insert into trades select traded(b, s) from orders b join orders s on b.buy != s.buy where crossed(b, s);
  insert into trades_again select traded(b, s) from again b join again s on b.buy != s.buy where crossed(b, s);

  // The trades settled: each buyer pays the price for the shares, each seller is paid it.
  traders.cash = paid(traders.number, traders.cash, buyers = trades.buyer, sellers = trades.seller,
                      prices = trades.price, quantities = trades.quantity);
  traders.cash = paid(traders.number, traders.cash, buyers = trades_again.buyer, sellers = trades_again.seller,
                      prices = trades_again.price, quantities = trades_again.quantity);
  traders.shares = bought(traders.number, traders.shares, buyers = trades.buyer, sellers = trades.seller,
                          quantities = trades.quantity);
  traders.shares = bought(traders.number, traders.shares, buyers = trades_again.buyer, sellers = trades_again.seller,
                          quantities = trades_again.quantity);
  orders.filled = orders.filled + orders.take;
  again.filled = again.filled + again.take;
  orders.open = open_of(orders.quantity, orders.filled);
  again.open = open_of(again.quantity, again.filled);

  // What the panels read.
  market.traded = sum(trades.quantity);
  market.volume = market.volume + market.traded;
  market.trades = market.trades + count(trades.quantity);
  market.bid = touch_bid(buys = orders.buy, prices = orders.price, opens = orders.open);
  market.ask = touch_ask(buys = orders.buy, prices = orders.price, opens = orders.open);
  market.last = last_of(market.last, prices = trades.price, bid_arrivals = trades.bid_arrival, step = market.step);
  market.best_bid = market.bid > 0 EUR_minor ? (market.bid - settings.low) / 1 EUR_minor : market.best_bid;
  market.best_ask = market.ask > 0 EUR_minor ? (market.ask - settings.low) / 1 EUR_minor : market.best_ask;
  market.last_price = market.last > 0 EUR_minor ? (market.last - settings.low) / 1 EUR_minor : market.last_price;
  orders.limit = float(orders.price);
  market.cash = sum(traders.cash);
  market.held = float(market.cash);
  market.shares = sum(traders.shares);
  traders.twin_cash = twin_cash(traders.number, numbers = traders.number, cashes = traders.cash);
  traders.twin_shares = twin_shares(traders.number, numbers = traders.number, shareses = traders.shares);
  orders.blocked = blocking(orders.take, orders.buy, orders.price, orders.arrival, buys = orders.buy,
                            prices = orders.price, arrivals = orders.arrival, opens = orders.open);

  checks.shares = checks.shares
                  && taken(buys = orders.buy, takes = orders.take, buy = true) == market.traded
                  && taken(buys = orders.buy, takes = orders.take, buy = false) == market.traded
                  && taken(buys = again.buy, takes = again.take, buy = true) == sum(trades_again.quantity);
  checks.cash = checks.cash && market.cash == 160000 EUR && market.shares == 1600;
  checks.limits = checks.limits
                  && at_limits(prices = trades.price, bids = trades.bid, asks = trades.ask,
                               bid_arrivals = trades.bid_arrival, ask_arrivals = trades.ask_arrival,
                               step = market.step)
                  && at_limits(prices = trades_again.price, bids = trades_again.bid, asks = trades_again.ask,
                               bid_arrivals = trades_again.bid_arrival, ask_arrivals = trades_again.ask_arrival,
                               step = market.step);
  checks.priority = checks.priority && sum(orders.blocked) == 0;
  checks.uncrossed = checks.uncrossed && (market.bid == 0 EUR_minor || market.ask == 0 EUR_minor
                                          || market.bid < market.ask);
  checks.continuous = checks.continuous && market.traded == market.wanted;
  checks.again = checks.again
                 && (count(traders.number) where traders.number < 8
                     && (traders.cash != traders.twin_cash || traders.shares != traders.twin_shares)) == 0;
  checks.harris = checks.harris && harris_holds(slots = harris.slot, takes = harris.take);
  cases.got = lusine.finance.fill(cases.open, cases.meeting, cases.ahead);
  checks.by_hand = checks.by_hand && wrong(got = cases.got, want = cases.want) == 0;
  lamps.colour = lamp_colour(holds = checks.shares && checks.cash && checks.limits && checks.priority
                                     && checks.uncrossed && checks.continuous && checks.again && checks.harris
                                     && checks.by_hand);
}

The kernel's other proof (two hundred random queues against the continuous match order by order) is on its proof page.