Getting started

Install Chelis with the installation guide, then create a project:

chelis reef init demo --module-prefix Demo --output demo
cd demo

Declare the dependency

Edit the generated reef.toml. The compiler pin must match this package's reef.toml; Reef rejects a project whose pin differs. Add Economoist under [dependencies]:

schema = "3"
[package]
name = "demo"
version = "0.1.0"
compiler = "=0.22.1"
module_prefix = "Demo"
additional_sources = []
resolver = "2"

[dependencies]
economoist = { version = "0.2.22" }

Install the release into your local Reef registry. This downloads the public release assets and needs no GitHub token:

chelis reef install --from-github chelis-lang/economoist@v0.2.22

The install command downloads the release assets. chelis reef build then resolves the dependency from the registry and records its version and archive hashes in reef.lock. Economoist's own dependency, chelis-std, ships with the compiler. To let chelis reef build discover a missing package instead, set GITHUB_TOKEN or authenticate with gh auth login first. The Reef guide covers lockfiles and reef setup.

A first program

Replace src/main.ch:

module Demo.Main
import Economoist.Growth (gordon_pv, gordon_pv_checked)
price = gordon_pv(2.0f32, 0.1f32, 0.05f32)
checked = gordon_pv_checked(1.0f32, 0.03f32, 0.08f32)

Then format, check, and evaluate it:

chelis fmt --inplace src/main.ch
chelis check src/main.ch
chelis eval --file src/main.ch
chelis reef build

chelis check reports "score": 1 with an empty errors list. The evaluator prints:

price = 40.0
checked = None

A dividend of 2 discounted at 10% with 5% growth is worth 2 / 0.05 = 40. The second call has the required return below the growth rate, so the checked function refuses it, returning None instead of Some(value). Every numeric argument and result in Economoist is f32; write literals with the f32 suffix, as above, so they match.

The library has three modules:

Module	Import	Page
Economoist.Markov	make_dist, advance, next_mass, make_dist3, advance3, mass3_next, eps	Markov transitions
Economoist.Bellman	bellman_state0, bellman_state1, bellman_state0_n3, bellman_state1_n3, bellman_state2_n3, fmax, fmax3, fabs	Bellman operator
Economoist.Growth	gordon_pv, gordon_pv_checked, gordon_pv_strict, gordon_pv_strict_checked, gordon_pv_negated	Gordon present value

Check a property against the library

chelis prove checks a @property in your own project against the imported functions, so you can confirm a stated result or test a claim of your own. This file states Gordon positivity twice, once outside the model's domain (g > r) and once inside it (r > g):

module Demo.Main
import Economoist.Growth (gordon_pv)
@property gordon_positive_wrong forall(d: f32, r: f32, g: f32) where d > 0.0, g > r:
  (gordon_pv(d, r, g) > 0.0)
@property gordon_positive_control forall(d: f32, r: f32, g: f32) where d > 0.0, r > g:
  (gordon_pv(d, r, g) > 0.0)

chelis prove src/main.ch --tier smt-only checks the real-arithmetic claim and prints:

property failure: gordon_positive_wrong
  --> src/main.ch
property: gordon_positive_control -- proven_modulo_real_arithmetic (proved over the reals; machine arithmetic unchecked)
1 passed, 1 failed, 0 unsupported, 0 errors

and exits with status 1 because one property failed. The cvc5 SMT solver proves the control over real arithmetic; rounded f32 execution remains unchecked. The default proof tier also tests machine arithmetic, where a positive value can underflow to zero. With --json, the failed property's record carries the counterexample {"d":1.0,"g":0.0,"r":-1.0}, which is d = 1, r = -1, g = 0 and gives a present value of -1. Its machine_arithmetic field reports confirmed: the witness rounded to f32 also refutes the claim. The counterexamples page lists the other false claims of this kind and the guard each one is missing.