Getting started

c-earchin is a Chelis shell package rooted at CEarchin. This chapter walks through one translation from an EARS file to a runnable Deep witness file with provenance.

Building the package

A release build produces the consumable artifacts:

chelis reef build .

A private release install pulls a published tag from the org:

GITHUB_TOKEN=$(gh auth token) chelis reef install --from-github Chelis-Lang/c-earchin

A first translation

The finance options demo under references/finance_options/ is the shortest path to seeing the whole bridge work. It ships an EARS source file, the generated Deep, the span manifest, and captured chelis prove output for both a passing and a failing run.

The EARS source is plain structured English a desk or risk reviewer can read:

FIN-001  The option pricer shall produce non-negative call prices.
FIN-002  WHEN market data arrives, the implied-volatility surface shall be within tolerance.
FIN-003  WHILE the exchange is open, the portfolio delta shall be at most the limit.
FIN-004  IF an order breaches the position limit, THEN the order gateway shall reject the order.
FIN-005  WHERE same-day settlement is enabled, the settlement clock shall be bounded by the window.
FIN-006  WHILE the exchange is open, WHEN a quote changes, IF the quote is firm, THEN the call price curve shall be monotone-increasing.

Translate it into Deep plus spans:

c-earchin translate references/finance_options/options_rules.ears \
  --output references/finance_options/options_rules.dp \
  --spans references/finance_options/options_rules.spans.json \
  --strict

The --strict flag means the translation fails if any requirement response has no matching vocabulary predicate, so a clean run is a guarantee that every line became a real property witness. See verification scope for what strict mode requires.

Proving the result

The generated Deep is self-contained for the vocabulary predicates, so the property run is direct:

chelis prove references/finance_options/options_rules.dp \
  --spans references/finance_options/options_rules.spans.json \
  --json

chelis prove discovers the witnesses by scanning their property metadata. Each requirement runs as one property.

Reading a failure

The demo also includes options_rules_fail.dp, the same generated Deep with FIN-003 mutated so its witness is false. Running the failing file resolves the broken witness through the span manifest back to the EARS line:

property: req_FIN_001 -- 100/100 passed
property: req_FIN_002 -- 100/100 passed
property failure: req_FIN_003
  --> references/finance_options/options_rules.ears:3:1 FIN-003
  | WHILE the exchange is open, the portfolio delta shall be at most the limit.
property: req_FIN_004 -- 100/100 passed
property: req_FIN_005 -- 100/100 passed
property: req_FIN_006 -- 100/100 passed
5 passed, 1 failed, 0 unsupported, 0 errors

The failure names the requirement id, the file and line, and the original requirement text. The machine-readable form carries the same facts under source.requirement as {id, file, line, text}. How that resolution works is covered in provenance.

The EARS line format

A plain .ears source is one requirement per logical entry. Each requirement starts with an id, then at least two spaces, then the requirement text:

ID  text

Blank lines separate requirements, lines starting with # are comments, and an indented line continues the requirement above it. The requirement text must contain shall, and the clause before shall must name a system that begins with the.