SIX Swiss match-price rules

Available in the dashboard. Run speclogician demo run six-swiss to load this spec, then open it via speclogician demo dashboard six-swiss or the VS Code extension (status-bar SpecLogician / Browser button).

This is the most regulation-heavy example in the repo. It formalizes the SIX Swiss Exchange's match-price rules: given an order book with a top-of-book buy and sell, determine the fill price according to which combination of order types (Limit, Market, Quote) is present. Each rule from the regulatory document maps one-to-one to a named transition, a scenario, and a linked doc artifact.

This is the showcase for:

• One transition per behavioral case. No match_step monolith — each of the 9 fill rules is its own narrow transition.
• One doc artifact per regulatory clause. Four AddDocRef entries (§3.2 Limit×Limit, §3.3 Market×Limit, §3.4 Market×Market, §3.5 Quote tie-breaking), each linked to only the scenarios it governs.
• Variant types end-to-end. order_kind, fill_result, action_kind are all variants — the complement contains only meaningful gaps, never kind = 5.

The system

A single security trades on a single venue. Each side of the order book is a list (FIFO by time). When a match is requested:

• Look at the top-of-book on both sides.
• Classify the pair (buy.order_type, sell.order_type) — there are 9 combinations of Market/Limit/Quote.
• Apply the SIX rule for that exact combination to determine the fill price.

The challenge is that the rules differ for each combination — Limit×Limit uses the older order's price, Market×Limit uses the limit side's price, Market×Market uses surrounding-order context, and Quote tie-breaking depends on quantity equality.

Domain base

type order_kind = Market | Limit | Quote
 
type order = {
  order_id    : int;
  order_type  : order_kind;
  order_qty   : int;
  order_price : int;   (* cents *)
  order_time  : int;
}
 
type fill_result =
  | NoFill
  | Filled of int     (* fill price *)
 
type state = {
  buys      : order list;
  sells     : order list;
  ref_price : int;
  last_fill : fill_result;
}
 
type action_kind =
  | ComputeMatch
  | SubmitBuy  of order
  | SubmitSell of order
 
type action = { kind : action_kind }

Helper functions (defined alongside the base) extract the top-of-book and next-of-book on each side, and compute the older order's price:

let best_buy  (s : state) : order option = ...
let best_sell (s : state) : order option = ...
let next_buy  (s : state) : order option = ...
let next_sell (s : state) : order option = ...
 
let older_price (b : order) (sl : order) : int =
  if b.order_time > sl.order_time then sl.order_price else b.order_price

Predicates

State predicates (10)

Classify the top-of-book on each side by order type, plus the fill outcome.

Action predicates (7)

Classify which kind of order is being submitted, or whether the action is a ComputeMatch.

Transitions (10)

Each transition pattern-matches the top-of-book pair and applies its specific SIX rule. Total functions — they fall back to the unchanged state for any combination they don't handle, which lets reachability traverse them safely from any source node.

Scenarios (20)

Scenarios fall into four groups:

Initial: empty book

Submitting orders (build up book state)

Matching (the actual SIX rules)

Each match scenario is a goal — reachability must demonstrate that the rule's pre-state is achievable.

One-sided observation

Artifact linking

Each regulatory clause is linked to only the scenarios it governs:

• doc-limit-limit (§3.2) → match_limit_limit plus the submit scenarios that build a limit×limit book
• doc-market-limit (§3.3) → match_market_limit, match_limit_market, plus the submit scenarios that lead there
• doc-market-market (§3.4) → match_market_market and submit_sell_market_after_buy_market
• doc-quote (§3.5) → all match_*quote* scenarios plus the submit scenarios that build a book containing a quote
• src-impl → all 10 transitions (the executable matching engine)

This rule-by-rule linking is the reason this demo exists — opening any scenario in the dashboard shows you exactly which clause of the regulatory document it's grounded in.

Why this design

A naïve formalization would write one match_step transition with nine nested if/match clauses dispatching on the top-of-book pair. That works for the IML, but the SpecLogician model becomes weaker:

• The reachability graph has one edge class instead of nine — the per-rule story is invisible.
• A bug in the §3.4 branch is buried inside a 50-line transition; fixing it touches the same block as every other rule.
• Each clause of the regulatory doc has nothing specific to link to. You link everything to match_step or nothing.

The granular design — one transition per rule, one scenario per rule, one doc clause per rule — preserves the rule book's structure in the model itself. This is the canonical SpecLogician shape for regulation-heavy domains.

See the agent guide's Granularity discipline section for the same point made in general.

Reachability: no cycle back to empty_book

If you open this spec in the dashboard, the reachability graph fans out from empty_book through the submission scenarios into the per-rule match scenarios — and stops there. Each match_* node carries a self-loop (firing the rule from the same top-of-book pair re-computes the same fill price) but has no outgoing edge back to empty_book.

That's intentional. The matching transitions update s.last_fill to record the computed fill price but don't consume the matched orders — state.buys and state.sells stay populated. The demo focuses on price determination (the rule-by-rule mapping from top-of-book pair to fill price), not on the full order-book lifecycle. A real exchange would also pop the matched orders off both sides and the graph would cycle back to empty_book after every fill.

For the full lifecycle view — orders resting on the book, getting consumed on a match, the book cycling back to empty, plus a safety invariant against a crossed book — see Stock exchange. The two demos divide labor cleanly: six-swiss is the rule-encoding showcase, stock-exchange is the lifecycle showcase.

Running the demo

speclogician demo run six-swiss              # builds state.json
speclogician demo dashboard six-swiss        # opens it in the browser dashboard

If you already have a state file from a previous run, you can also open it directly — either via the SpecLogician status-bar button in the VS Code extension, or by pointing the standalone speclogician-dashboard binary at the demo's state.json.

The full changes.py ships in the repo at src/speclogician/demos/content/six-swiss/changes.py (~600 lines including the IML helpers) — copy it as a starting point for any regulation-heavy domain where each clause should map to its own scenario.