type_soundness
progresspreservation
A well-typed core term is either a value or can take a step, and each step preserves its type. That is the progress and preservation story behind type soundness.
Proofs
Trust stack
C Proof narrows the trust boundary for generated numerical code. Chelis rejects structural failures, properties bind implementations to specifications, and proof artifacts show the route, evidence, and provenance behind each result.
Foundation
Formal core
LaCaDiLE, the Lambda Calculus for Differentiable Linear Effects, is the Lean 4 model of the core language: tensors, named-dimension indexing, algebraic effects, linear types, and differentiation.
The foundation is scoped. It backs language rules and implementation/spec matching; it does not validate every generated program or decide whether every domain requirement is the right one.
dimension_safety
DimSafety.lean
Named-dimension agreement proved by the type system is not left as a primitive runtime shape check. Well-typed terms avoid primitive shape mismatch.
effect_correctness
EffectCorrectness.lean
An empty effect row means the term does not get stuck trying to perform an effect operation. Effects are part of the typed interface.
linearity_soundness
LinearitySoundness.lean
Evaluation preserves store well-formedness, so the linear resource discipline is tied to the operational model instead of an ownership convention.
ad_correctness
ADCorrectness.lean
For the supported first-order fragment, automatic differentiation is mechanized against an abstract primitive AD specification. Higher-order and closure AD are outside this theorem claim.
Guarantees
Static edge
Python and JavaScript can enforce many numerical contracts with libraries, annotations, assertions, and tests. Chelis moves selected contracts into static semantics, so violations are refused before execution when they contradict the declared program.
Dimensions
Tensor dimensions live in Chelis types. A function that promises a named dimension cannot silently combine it with a different dimension and still type-check.
Precision
Precision is declared at the boundary, such as f32 or f64, so generated code has to match the stated numerical contract instead of relying on a runtime dtype convention.
Effects
Effect rows make ambient operations visible in the type. Pure property code cannot call an undeclared effect and still pass as pure code.
Ownership
Linearity puts resource use in the typing judgement. The checker rejects ownership paths that duplicate or drop a linear value against the rules.
AD
Differentiation behavior is tied to the core calculus for the covered fragment, with coverage stated in the proof claim instead of left to a library test suite or handwritten gradient convention.
User code
Proof path
The user-code path starts with a requirement and ends with evidence. It distinguishes an SMT proof from property-based validation, and it keeps provenance attached instead of flattening every result into a pass.
Requirement
A structured rule names the function, input types, preconditions, and expected response.
Chelis property
The rule becomes a property witness with quantifiers, preconditions, source id, and role metadata.
Implementation
Chelis code supplies the function under check. The property states how the implementation must match the specification.
SMT proof
Solver-dischargeable obligations are sent to SMT. A proved result is recorded with the property, assumptions, and provenance.
Property validation
Properties outside the solver route stay explicit. Property-based validation records preconditions, sample count, validation status, and provenance. It is not relabeled as an SMT proof.
Artifact
The output records the property name, proof tier, status, source requirement, and timing reviewers can inspect.
SMT proved
intrinsic_value
A non-negative intrinsic-value property is polynomial and discharges cleanly.
SMT proved
put_call_parity_residual
An algebraic parity residual proves under the stated rate and tenor preconditions.
validated
black_scholes_call
A normal-CDF path is kept as property-based validation with explicit preconditions and sample count.
Boundary
Evidence scope
The point is auditable evidence, not a blanket correctness claim. C Proof reports what the type system rejected, what the solver proved, what validation checked, and what remains a human modeling decision.
Spec match
Properties check the implementation against the stated specification. They do not prove that the business or model requirement itself is the right requirement.
Static scope
The type system rejects declared shape, precision, effect, and ownership failures before runtime. That is separate from domain-level model review.
Solver scope
SMT evidence covers the encoded obligation and assumptions. Non-SMT results remain labeled as validation with the evidence reviewers need.
Audit trail
Reviewers can inspect source requirement provenance, property status, proof tier, validation result, and generated artifact boundary.
Review
Bring a property
We will map the requirement, Chelis property, solver route, validation route, and provenance record for a numerical kernel your team already reviews.