Getting started

c-earchin (v0.3.3) 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 canonical Chelis property metadata (chelis_role and property_* fields), with no new Deep tag required. 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.

Translating a Kiro requirements.md

c-earchin also accepts Kiro-style requirements.md files, where EARS keywords are bolded in markdown. A .md extension triggers Kiro parsing automatically, or you can force it with --dialect kiro.

The references/kiro_example/ directory contains a runnable demo. Translate it the same way:

c-earchin translate references/kiro_example/requirements.md \
  --output references/kiro_example/requirements.dp \
  --spans references/kiro_example/requirements.spans.json \
  --strict

The output is identical in structure to an .ears translation: callable bool witness definitions with full provenance spans pointing back to the markdown lines. chelis prove picks up the witnesses by their canonical property metadata, exactly as with .ears input.

For the accepted markdown subset and detailed behavior, see the Kiro dialect.