Skip to content
chelis docs
Get started

Opaque types with declared invariants

@opaque keeps a type's construction and representation inside its defining module. Other modules can use exported values and functions, but cannot build or inspect the representation themselves. An optional @invariant states a condition that values produced for callers should satisfy. chelis check checks that the declaration is well formed; it does not evaluate the condition. chelis prove checks eligible exported functions that return the type.

Declare the type and its producers

Section titled “Declare the type and its producers”

Save the following module as opaque_invariants.ch to check its declarations and properties. It defines a probability in the unit interval and exports the type so another module can name it, while keeping construction and field access restricted to Stats.Opaque:

module Stats.Opaque
export (Probability, probability, scale, combine, prob_value)
@opaque
@invariant(p) ((p.value >= 0.0) && (p.value <= 1.0))
type Probability =
  | Probability { value: f32 }
def probability(x: f32) -> Option[Probability] = if ((x >= 0.0) && (x <= 1.0)) then Some(Probability { value: x }) else None
def scale(p: Probability, factor: Probability) -> Probability = Probability { value: (p.value * factor.value) }
def combine(p: Probability, q: Probability) -> Probability = Probability { value: (p.value * q.value) }
def prob_value(p: Probability) -> f32 = p.value
@property prob_value_in_unit_interval forall(p: Probability):
  ((prob_value(p) >= 0.0) && (prob_value(p) <= 1.0))

Keep the type's constructors and invariant in its defining module. Include Probability in the export list when other modules need to name it in their signatures.

The invariant's binder, p, has the representation type. A declared invariant requires a named module and a single record-shaped variant. Its predicate can use field projections, literals, arithmetic, comparisons, boolean operators such as &&, if, selected math functions, sum over a fixed-shape tensor field, and in-module zero-argument constant definitions. General function calls, match, lambdas, and effects are not allowed in the predicate. The type-system specification gives the full value and predicate rules.

probability returns Some only for accepted inputs. scale and combine return a new Probability from existing values. Their checks may assume that opaque inputs received from callers satisfy the invariant, and must establish it for their returned values. prob_value returns an f32, so it is not an opaque-value producer. The @property is a separate check about values of the type.

Check and prove

Section titled “Check and prove”
Terminal window
chelis check opaque_invariants.ch
chelis eval --file opaque_invariants.ch --json
chelis prove --capabilities
chelis prove opaque_invariants.ch --json

chelis check verifies the types and declaration form; it does not certify that producer functions preserve the invariant. Use chelis prove to check the property and eligible producer obligations.

Before relying on an SMT result, check chelis prove --capabilities and confirm both obligation_engine_available and smt_available are true. If the obligation engine is unavailable, a successful property run does not verify producer obligations. See Checking Properties for proof options and result qualifications.

For the SMT-enabled binary, the example has one property and three producer obligations. These are selected fields, not complete output records or a literal transcript:

{"kind":"property","name":"prob_value_in_unit_interval","status":"passed","proof_tier":"fuzz"}
{"kind":"obligation","name":"invariant:Probability:probability","status":"passed","proof_tier":"smt","composite_verdict":"proven_modulo_real_arithmetic","arith_model":"real"}
{"kind":"obligation","name":"invariant:Probability:scale","status":"passed","proof_tier":"smt","composite_verdict":"proven_modulo_real_arithmetic","arith_model":"real"}
{"kind":"obligation","name":"invariant:Probability:combine","status":"passed","proof_tier":"smt","composite_verdict":"proven_modulo_real_arithmetic","arith_model":"real"}
{"kind":"summary","total":4,"passed":4,"failed":0,"unsupported":0,"errors":0,"obligations":3}

A "fuzz" result means sampled values passed; it is validation over those samples, not a proof for all inputs. An "smt" result proves the stated goal using real-number arithmetic. "arith_model":"real" and "composite_verdict":"proven_modulo_real_arithmetic" disclose that it does not certify IEEE floating-point execution. Read "proof_tier" and "composite_verdict" alongside "status" before relying on a passed record.

If you replace the exported probability definition with one that omits the upper guard, the producer obligation fails. For example, x = 2.0 meets the lower guard but returns a value above the declared bound:

def probability(x: f32) -> Option[Probability] = if (x >= 0.0) then Some(Probability { value: x }) else None

With SMT enabled, the prover reports a counterexample and exits with a failure. The exact value is solver output; use the record's "counterexample" field rather than expect 2.0 specifically. Exported return types are read from the checker, including inferred returns. A return container that the prover cannot inspect produces an error instead of being silently skipped.

Use the type from another module

Section titled “Use the type from another module”

In a Reef package with module_prefix = "Stats", put the defining module in src/opaque.ch and this consumer in src/pricing.ch. Import both the public type and the functions:

module Stats.Pricing
import Stats.Opaque (Probability, probability, scale, prob_value)
def adjusted(x: f32, factor: Probability) -> f32 =
  match probability(x) with {
    | Some(p) => prob_value(scale(p, factor))
    | None => 0.0
  }

Exporting Probability allows the annotation. It does not allow a caller to construct Probability { value: x }, read p.value, update the record, or match its constructor. chelis check reports OpaqueTypeViolation for those operations outside Stats.Opaque; the diagnostic names the type, its defining module, and exported producer signatures. The following src/forge.ch consumer is rejected:

module Stats.Forge
import Stats.Opaque (Probability)
def forge(x: f32) -> Probability = Probability { value: x }

Tensor fields and proof boundaries

Section titled “Tensor fields and proof boundaries”

examples/opaque_invariants_simplex.ch defines a fixed-size weight vector whose sum lies within a tolerance of one. Its make_simplex producer passes by validated sampling even in an SMT-enabled build: the record has "proof_tier":"fuzz" and no "arith_model". Its property checks that valid Simplex values can be generated; it is not a proof that every possible input produces a valid sum. A tolerance band is practical for floating sums, while exact equality can starve sampled generation.

Opacity does not add bounds to downstream arithmetic. chelis check does not infer from a Probability value that a later calculation lies in an interval. Only return values produced across the module boundary receive the producer obligations described here. If the defining module passes a raw opaque value, or a function able to produce one, outward as a call argument, that path needs module review; the opaque-escape-site lint identifies such calls.

Opacity also does not hide data in tooling output. When evaluation prints an opaque value as a root, it shows the constructor and fields. Sampling counterexamples can show them too.