Repository navigation
v0.18.7
[0.18.7] - 2026-09-13
Added
-
Add an internal compiler evidence mode for auditing native Python bindings, recording exact constructor owners, instantiated types, calls and control flow.
-
Native binding compiler evidence now records exact tuple-struct and enum constructor function exposures, including callback arguments, stored values, promoted static tables, reification casts and constant initializers. Its versioned decoder requires the exact occurrence envelope and rejects older incomplete native evidence; collection alone grants no binding authority.
-
chelis build --target hipand--target metallower first-classcount
([05-OP-29]) to a dedicated device kernel over the exactBool8carrier, and a
host program whose tensor helper containscountemits that helper as its own
device translation unit instead of a C body. Both targets previously rejected
countwith a chelis#1291 receipt. The Metal hardware gate records a pass on
Apple Silicon; the HIP hardware gate remains a documented manual gate, so
chelis#1291 stays open. See
#1307. -
The opt-in
chelis-ir/lowering-tracefeature records gradient call-site
specialization, argument and splice maps, caller snapshots, and packed results
for downstream validation tooling. The feature remains disabled by default and
does not change ordinary compiler output or language behavior. -
OpenSpec document changes land by pushing a branch. A push touching
openspec/**startsopenspec-autoland, which classifies the pushed commit
with default-branch code, opens an internal pull request when every changed
path is an OpenSpec document, waits for the required checks on that exact
commit, and merges it. Normative capability specifications are included.
Anything outside the document set is refused and follows the ordinary review
path. Inside Devenv,openspec-submitremains an optional local helper that
validates before you push. See
#1653. -
Add IR evaluator APIs for preparing strict-root and selected-plan inputs through
a fallible provider before execution. Existing evaluator signatures and input
selection remain unchanged. This is a prerequisite for, not a fix to,
#1956. -
chelis prove --tier beacon-onlyand the Tide prove tool can dispatch self-contained scalar network bounds to Beacon, retaining real-arithmetic qualification, search bounds, unknown reasons and split trees. Search and caller wall budgets are explicit; float execution is not covered. -
Add tested rustdoc graph and structural carrier-verification infrastructure for
numeric wire-surface discovery, including private/imported helpers, generic
closure and fail-closed unsupported codec handling. Live wire formats and census
activation remain part of the subsequent migration. -
Added a fail-closed internal adapter for the future #1288 zero-exception capacity receipt. It cannot issue a receipt until the primary, stdlib, wire, and final PyO3 binding gates run on one committed source tree, and retains each nested Cargo/libtest execution's framework outputs beside its supplied fresh receipt. The required stdlib selection includes symbolic generic constructors and imported boolean companions.
-
Release notes can be authored as per-PR Markdown fragments, assembled into a
versioned changelog section, and published verbatim with the GitHub Release.
Required PR checks reject missing or invalid fragments and direct changelog edits
outside release assembly. See
#1251 and the
fragment contract. -
Add the default-off
chelis-compiler-api/emission-observerfeature for immutable
observations of the actual ownership-verified payload selected for code generation.
Ordinary compiler output and behavior are unchanged; observations are not certificates. -
Add an opt-in ownership-checked C backend entry for closed fixed-control dropout execution plans, with saved-mask replay and unchanged tensor ABI. Ordinary source-build and host-helper admission remain separate work.
-
The default-off native Random observer now carries bounded, ownership-verified
host source-site and linked call associations, with exact helper-local/full
source IDs. Unsupported source shapes remain explicitly uncertified; ordinary
generated headers, public entry ABIs and default emission are unchanged. -
Add a non-default compiler feature for translation-unit-private observation of
actual generated-C Random state, including nested saved frames, fixed-control
forward/replay identities, and copied continuation counters. Public headers,
ordinary artifacts, runtime behavior, and default features remain unchanged. -
The opt-in native emission observer now exposes the initial host-lowering snapshot
alongside the selected verified payload, so consumers can inspect scalar losses
pruned from tuple-gradient artifacts. Ordinary compilation and wire output are
unchanged; the additional snapshot is not a certificate or an emitted function. -
Add the pre-Phase-4C prerequisite runner framework with exact child-command
identities and execution-receipt validation. It fails when prerequisites,
per-test outcomes, or required negative and mutation evidence are absent.
The complete prerequisite set and required CI activation remain outstanding
under #1296. -
C fixed-control lowering retains checked Resource requirements as value-free
source cuts, exposed through opt-in full-spine observations. The existing target
validator still decides compatibility. Resource-only programs and the evaluator
keep their prior lanes; existing random-only Rust carriers, wire formats, C ABI,
and shell interfaces are unchanged. -
Add an opt-in compiler API that pairs actual selected helper lowering/AD observations with the final successful C artifact. Normal compilation, existing observer layouts and shell/wire interfaces are unchanged; the observations are not correctness certificates.
-
Retain draw-free seed controls and an independent source occurrence census in
fixed-control evaluation plans, and expose opt-in execution-bearing snapshots
at actual AD calls. Compiled backend support and public wire formats are unchanged.
Changed
-
BREAKING: Compiler execution JSON advances to version 3 and WireDag JSON to version 9.
Scalar and tensor carriers preserve exact integers and IEEE floating-point bits,
including signed zero and NaN payloads. Numeric parameters, extents, references
and report fields enforce their owning domains on encoding and decoding.
Readers reject missing, older and future versions; regenerate saved wire
documents with the current compiler. The wire census now requires executed
final authority for every discovered numeric leaf and retains no legacy cohort. -
BREAKING: Python evaluation uses execution wire v3's exact numeric carriers. Floating-point
values preserve their IEEE bits, including signed zero and NaN payloads; numeric
scalar results retain their NumPy dtype, withml_dtypes.bfloat16forbf16.
Tensor results retain the declared dtype and exact element values. Old execution
versions and malformed carriers are rejected. Part of
#1288. -
BREAKING: Compiled-context worker handoffs use the same versioned, integrity-checked
envelope as the disk cache. Workers reject unversioned payloads, incompatible
formats or compiler builds, and corrupted payloads before reconstructing the
checked context. Regenerate previously saved worker handoffs with the current
compiler. -
BREAKING: The reserved
normalizebuiltin is removed. An undeclared call reports an
unbound variable; define an ordinary function with an explicit normalization
formula, as inexamples/explicit_normalization.ch.Builtin and canonical RISC semantic identities now have an exhaustive normative
atom registry and an executable closure oracle. See
#1299. -
BREAKING: Deep AST annotations use dedicated types for compiler-owned metadata and a
separate extension map. Rust API consumers must migrate fromMetaMap.entries
toMetadataand its typed accessors. Parsing, deserialization, and typed
construction reject malformed annotation values and duplicate keys, including
custom andspan_*keys; preserved macro-source arguments remain raw syntax
data. See #1604. -
BREAKING:
chelis check <dir>emits one typed envelope,{"files": [...], "errors": [...]}, with both members always present, and it never exits 1. Three behaviours change for a directory target. An empty directory now fails with anempty_corpuserror and exit 2; it used to pass. That includes a directory whose only sources sit undertarget/or a dot-directory, and the message counts those. A directory the walk cannot read no longer discards the whole run. Every readable file keeps its report, the unreadable directory is onedirectory_walk_error, and the command exits 2; it used to exit 1 with nothing on stdout. A populated directory's document now carrieserrors, which it used to omit.The walk shared by
chelis check <dir>andchelis test <dir>also changes. Each file and directory is visited once, by canonical path, so a file reached through several links is checked or run once. A dot-named ortargetlink is skipped by its name before it is resolved, so it no longer aborts the walk when its target cannot be read. A link that cannot be resolved is still an entry when it has a source name. Forcheck, any other unresolvable link is adirectory_walk_errorrather than an abort.chelis teststill stops at a walk failure. Specified inspec/04-type-system.md§ Directory mode, [04-FIT-19] to [04-FIT-25]. See #1678. -
BREAKING: HIP generated programs use opaque device owners, immutable checked metadata,
and 64-bit kernel geometry specialized to the program's checked ranks. Reshape
and BLAS operand preparation materialize logical input order into storage
accounted by the shared planner. Direct verified HIP codegen callers run
prepare_dag_for_codegenbefore ownership lowering; unprepared BLAS borrows
fail the storage-plan precondition.
HIP builds require matching official hipBLAS 3+ headers and libraries. -
BREAKING: checker/CLI:
chelis check's error objects change shape in
four ways (chelis#886). The report's error objects are now produced by
serializing one typed carrier instead of four hand-writtenformat!
templates.suggestionsis emitted when non-empty, for effect diagnostics
as well as check ones;span_offsetbecomesspan, a tagged carrier that
is{"span":"range","offset":N,"len":M}when the producer measured an
extent and{"span":"point","offset":N}when it held only a coordinate
(chelis#1395); and member order placessuggestionsbetweenseverity
andspan.kind,message,severity,expected,gotandspan_idare
unchanged in spelling, presence rule and position.spec/04-type-system.md
§6.4 states the transport contract as [04-FIT-11] through [04-FIT-17].
A consumer that readsspan_offsetfrom the check report must move to
span.offset, which is a sibling key in both variants and so needs no
matching; readinglenrequires matching thespandiscriminator. The
untagged shape is
hard-rejected by the consumer type rather than silently accepted. No
in-repo consumer readspan_offset;chelis-lspreads the carrier and
renders a point as a caret-position range. -
BREAKING: checker/CLI: nominal type applications now enforce parameter
kinds and concrete dimensions (chelis#1247, chelis#1258). Declaration
headers acquire checker-ownedType/Dimensionkinds by a deterministic
fixed point, so integer arguments reject at ordinary type parameters and
constrain dimension parameters instead of becoming fresh wildcards.
Column[3]now rejects a two-element constructor with
DimensionMismatch;Option[3]rejects withTypeMismatch. Surf emits a
structurald-litfor the integer argument, restoringdeep/surfand
migrate surfround trips, while aliases, records, matches, eval, generated
C,chelis check, andchelis testpreserve the same checked extent.
Structured inferred JSON wraps nominal dimensions as
{kind:"dimension", dim:{...}}without changing existing type-argument
objects. Serialized compiler state changes accordingly: compiled-context
cache v12 → v13, stdlib cache v8 → v9, library cache v5 → v6,
and Reef prepared-graph cache v2 → v3; stale entries rebuild
automatically. -
BREAKING: Producer AST extensions are opaque data: compiler passes preserve their contents
without expanding macros, renaming references, inferring effects, or interpreting
nested annotation-like keys. Compiler-owned annotations retain their dedicated
types and validation. Deep-to-Surf conversion rejects extensions it cannot preserve.
Property discovery requires canonical property annotations;c_earchin_roleis
producer data. The Rust extension API and serialized extension format change;
regenerate older AST caches. Part of #908. -
The runtime-extent class oracle demands
RUNTIME EXTENT ORACLE: PASSfrom
phase B rather than reporting rows short of exit, and--phase finalnow
reaches its row report instead of refusing on the withdrawn phase C. Every
recorded row of both phases is at an exit state, the nightly extended-validation
workflow runs that one completion command, and the acceptance runner over the
extent-claim fixtures runs as an ordinary test. See
#1277.The example census in
issue_1739_diagonal_runtime_boundderives its corpus
from the examples directory instead of a hand-written count, and records the
two examples the C capability gate refuses under
#1192. The shipped-example
roster stays inparity.rs, where the Phase 3 faithful-observation oracle
freezes its definition. See
#1787. -
Restrict shared durable cache publication to its two concrete library and
standard-library context payloads. Their payload formats advance to library
version 12 and standard-library version 16 under versioned cache keys; older
entries miss before payload decoding. Compiled contexts use their separate
version-18 envelope for both disk caches and worker handoffs. -
Native binding verification records raw constructor function values, including
casts and const/static initializers. The owner verifier requires this evidence
and rejects guarded constructors passed as callbacks or constructed inside
closures; a private tagged enum alone does not establish validated ownership. -
Bind native Python registration evidence to the actual compiled class objects,
descriptor kinds and exact Rust implementations. The collector rejects missing,
replaced or reclassified exports; this evidence alone grants no numeric authority. -
The primary numeric-capacity census now requires every discovered C and
standard-library row to have exact final authority. Its retired grandfather,
permanent-disposition, successor-override, and integer-plumbing admission paths
no longer authorize public surface. See
#1288. -
The compiler wire verifier checks exact source-location and scoped-reference
roles, ties them to accepted and rejected admission executions, and rejects
numeric leaves without a unique carrier or operation classification. An outer
metadata tag does not authorize arbitrary numeric payloads. -
Specify exact dtype-tagged IEEE wire bits, fixed-dtype report JSON numbers,
scoped wire references, and validated Python tensor metadata and DLPack
admission. The contract defines one atomic execution-v3/WireDag-v9 migration;
the running codecs and versions remain unchanged until its implementation. -
The capacity-census liveness check rejects legacy wire dispositions and requires
the version 2 final-authority baseline shape. Wire coverage records the publication
graph and execution witnesses required by the live verifier. -
Bind wire axis parameters and handled random seeds to their exact numeric
operation authorities. Name the existing movement and indexed-tensor contracts
in the numbered specification, and invalidate codec evidence when its operation
authority changes. These registrations are part of the atomic wire migration;
they do not authorize unrelated numeric fields or retire other legacy cohorts. -
Cover exact random wire parameter dtypes, finite domains, complete seed
encodings and owning input constraints. Preserve the scalar Bool activation
emitted by gradient lowering for UniformLike while keeping Dropout unary.
Bind standalone cache compile fixtures
to their exact driver inventory and retain normal compiled-source coverage for
the historical producer. -
Replace the
conv2dbuiltin withconv, using explicit per-axis int64
strides and(low, high)padding pairs for any positive spatial rank.
Static convolution lowering now contracts the complete window matrix in
the specified order; zero-sized contractions retain their RISC graph.Generalize the normative
to_listcontract to nested Lists at every
positive tensor rank andtensor_scanto fixed-shape tensor state.
Their runtime implementations still have rank-one/scalar restrictions,
recorded as implementation gaps in the dtype plan.Require an explicit same-dtype epsilon for
layer_norm, including its
adjoint. Correct standard lowering recipes to insert axes explicitly and
select embeddings and masked values withgatherandwhere.Run host
matmulthrough the typed rank-generic lowering and preserve a
tensor boundary for nested host operands in generated C. Batched attention
and broadcast matrix calls now execute in both lanes.Preserve canonical contraction trees during C selection instead of implicitly
substituting vendor GEMM, including generated convolution and hosted matmul.
Remove derived BLAS helper/wrapper shortcuts before binding C ownership.
Ordinary sum now uses the canonical adjacent-pair tree in evaluation and
generated C, preserving odd tails, signed zero, and checked integer overflow. -
Refresh the guard-artifact assessment with the implemented guard slices, assign
two replacement expand controls to standing pull-request CI, and select an
exact change-owned integration guarantee with measured package expansion
without expanding the developer--fastgate or weakening nightly coverage. -
Host lowering now derives each definition's kernel decision from a
HostLoweringSessionbound to the program
it describes, replacing thread-local caches keyed on the program's address and gated on a flag that an entry
point had to arm. Forgetting to establish one is now a compile error rather than a silent full recomputation.
The callee summary probe also moved to last among the host-lane predicates, so a definition whose declared
result cannot be a kernel pays none. On a thirteen-definition fan-out chain, per-definition summary builds go
from 78 to 12 where the chain returns tensors and from 398,574 to 0 where it returns scalars. End-to-end
interpreter speed is unchanged: the arming call that recovered it shipped separately, and this change replaces
that call with the structure rather than adding a further speedup. -
The Metal
countkernel's fixed-rank device-cap rejection now cites chelis#1844, the live tracker of that Metal residual, instead of chelis#1345, which #1828 resolved for the Python carrier and closed. -
Runtime-representation Phase 0 now freezes its reviewed foundation rows and all
44 mutation identities, implementations, expected failures, and commands.
Release reproducers, hardware probes, counts, and ordinary configuration remain
live-derived, so those changes do not require a freeze move. Regeneration also
rejects reactivation of an identity already retired from active debt. -
Runtime-representation Phase 1 and Phase 2 now treat reviewed test identities as
deletion-blocking floors: newly selected tests execute and are reported, while
missing, renamed, ignored, unexecuted, or failing required tests still block. -
Retire the redundant hand-maintained
expandspelling inventories in favor of
checker-owned behavioral controls that directly reject rank-raising and
non-unit-axisexpandrecipes, pin obsolete shape-taking calls to the owning
arity diagnostic, and retain focused source-dispatch parity forexpand/insert. -
The closed-vocabulary architecture guard now keeps positive typed-consumer
evidence at crate granularity through extension-selected Rust and C-family
token projections, excluding comment and literal payloads while preserving
active include operands. It scans known raw bypasses as active token patterns
across the relevant production source trees and published runtime/device
headers, including device-specific header suffixes. -
Trial wording-independent identities for production unsupported diagnostics,
preserve typed lowering spans, align the nonliteral-window rejection across
build targets, and generate the reviewed softmax wording snapshot from one
canonical reviewed row through tier-0 regeneration. -
Derive the unimplemented-rejection issue manifest from exact production source
citations, rejecting missing, stale, dynamic, or malformed issue authority
before generated Rust membership is accepted. Production source discovery now
uses every repository-local Cargo workspace package, one cfg(test=false)
parser view shared with the direct-construction boundary, and an independent
rustc dep-info closure. Required production-target features are derived from
Cargo metadata, and every exact target identity must emit non-test dep-info.
Every Rust or Cargo manifest edit retriggers live issue validation. The
dedicated liveness job owns fresh source and compiler evidence; ordinary
script-unit tests use injected evidence instead of repeating the full Cargo
derivation four times. -
Run the full source-derived standing rejection-issue manifest against GitHub
daily and on manual dispatch frommain. Any non-success result, including a
cancelled or skipped canary job, opens or updates onenightly-failure
tracking issue. A constant concurrency group prevents report scripts from
overlapping without cancelling the running workflow; bursts may coalesce to
the newest pending dispatch rather than run FIFO. Failure consolidates
exact-title duplicates and the next successful run closes every match. This is
the standing liveness canary only, not the broader loud-unsupported Phase 4
nightly matrix. -
Generate exact host views and dynamic device descriptors from the shared ABI schema. Validate native tensor boundaries through checked metadata owners and reject compiled artifact ABI 1 before metadata or library loading. HIP artifacts carry a separate device-owner implementation with checked strided copies, device-bound lifetime, and matching source/header staging. Native calls preserve named dimension equality while keeping wildcard axes independent, and DLPack exports validate actual device synchronization before capsule construction.
Construct native output owners directly in execution loops, preserving each returned host reference and interning device handles through explicit map entries. Rejected output batches release both previously adopted tensors and remaining raw owners.
Retain current execution evidence for the 37 native boundary cases, including exact test lifecycles, the Cargo-built runtime archive, and snapshots of all generated and foreign fixture artifacts. Snapshotting preserves the original model-owned temporary directory lifetimes. Device fixtures remain simulated SDK and foreign ABI evidence.
-
The Python capacity census now checks return types and reachable aliases and
containers for final registrations. Nine source, path, name, dtype-vocabulary,
and opaque-handle methods retire their legacy exceptions; eight numeric JSON
and tensor methods retain their existing migration gates. Source-only JSON
results retain their concrete Rust types until Python string conversion, with
unchanged Python result formats.
Callable discovery binds the actual PyO3 registration, Rust implementation,
source span, and live descriptor kind. Renamed functions, methods and properties
cannot inherit a same-named helper's authority; unsupported registration forms
fail closed. Source JSON authority cannot admit unrelated sibling text results.The runtime representation source census includes the source-result adapter
while preserving the existing foundation and active debt. -
Bound PR test compilation to all default-feature unit targets and 17 reviewed integration targets; preserve exhaustive nightly coverage and publish selection/build timing receipts.
-
Run the exhaustive Linux workspace and broad phase oracles in daily or manually dispatched extended validation, preserving their full acceptance commands while removing them from the PR critical path.
-
Run Mac workspace, Clippy, ABI/Metal smoke, and Darwin SMT validation nightly or on manual dispatch; preserve release validation and keep ordinary PR and main-push CI on Linux.
-
Move compiled Python census and bundle tests to explicit nightly owners, remove duplicate Linux census execution, halve real bundle regenerations, and retain test/subprocess timing diagnostics.
-
Specify Hull's axis-preserving unit-axis broadcast repair, including input
validation and matching checker/generator obligations. This is a reference-model
contract and changes no Chelis behavior, compiler format or shell pin. -
Specify Hull's independent first-order f32 directional-reference kernel and
its numerical acceptance boundary. No compiler behavior or shell pin changes. -
Specify Hull's positional single-axis sum repair, including checked axis removal,
coordinate-wise balanced evaluation and campaign obligations. This is a reference
model contract; no Chelis language, runtime, compiler output or shell pin changes. -
Specify the bounded repair of Hull's release-pinned scalar observation decoder
for dtype-tagged rank-zero f32 payloads, with version, rank and cardinality
guards. This changes no compiler behavior, wire format or shell pin. -
ReLU now retains its dedicated [05-OP-43] identity and adjoint
(chelis#1313). Reverse-mode AD returns the complete incoming cotangent
only where0 < x, and exact positive zero at both signed zeros and NaN;
directmax_elem/min_elemkeep their first-operand tie rule. Eval and the
C backend implement exact f16/bf16/f32/f64 stored-bit selection, HIP does so
through all-width kernels, and Metal admits f32/f16/bf16 while retaining its
target-wide f64 rejection. WireDag v7 carriesReluandReluAdjointas
distinct validated identities. -
Deep nominal arguments now use the recursive type grammar at ordinary
.dpingress (chelis#1125, part of chelis#731).chelis surfand
chelis validate --deepreject a rank spread such asRows[..r]instead of
accepting ad-rankbelowt-adt. Concrete dimension arguments remain
valid, and rank spreads remain valid in tensor-axis slots.
Fixed
-
BREAKING:
list_dirrejects directory names that cannot be represented as UTF-8 instead of replacing invalid bytes. Both execution lanes report the first invalid entry in host-name order with a reversible escaped diagnostic; valid names and their ordering are preserved. -
BREAKING: Preserve
printanddebugoutput preceding an evaluation failure, including Reef-context evaluation. Text mode emits the transcript on stdout before the diagnostic;eval --jsonkeeps stdout empty on failure and emits the transcript on stderr. RustCompilerErrornow carries atranscriptfield, which direct constructors must initialize. -
BREAKING: Generic comparisons and arithmetic now reject a scalar beside a tensor, including casts to bounded dtype parameters. Diagnostics name the no-broadcasting rule and an explicit-shape replacement. Programs relying on implicit broadcasting must construct the matching tensor shape with
scalar_to_tensorandinsert; scalar/scalar and matching tensor/tensor operations retain their behavior. See #1621. -
BREAKING: Concrete-dtype comparisons between a scalar and a tensor now fail at check
time with the[05-OP-36]rule and an explicit-shape suggestion, instead of
implicitly broadcasting the scalar. This applies tocmplt,lt,eq,
neq,gt,gte, andlte; scalar/scalar and matching tensor/tensor
comparisons remain accepted. Give both operands the same explicit shape.The generic-binder escape remains #1621,
and the symbolic-size replacement still has a C-lane gap tracked in
#1619. See
#1624. -
BREAKING: Generic functions with separate signatures retain their checked element dtype when constructing tensors from computed Lists, including empty Lists. This restores evaluation of the published arange and linspace constructors without a payload-derived dtype fallback.
The RustRuntimeValue::Closurevariant gainschecked_signature; callers constructing that variant must supply the checked function type (orNonewhen no checked type is available). -
BREAKING:
chelis check <dir>andchelis test <dir>now follow symbolic links. Both
used to skip every symlink while walking a directory, so a symlinked source
file, or a symlinked directory of them, was never checked or run -- with a
successful exit and no warning. A type error or a failing test could be
hidden just by putting it behind a link. A directory that previously passed
can now fail, because code it silently skipped is checked and run.Following links handles three cases it introduces. A link that loops back to
a directory already being walked is skipped. A dangling link named like a
source (.ch, or.dpforcheck) is collected rather than skipped:check
reports it as an unreadable file, exactly as naming it directly would, and
testreports it as a failing file. A dangling link to anything else,
including one named like a dot-entry, is ignored.A link to a source directory is followed wherever it points, including out of
the directory named on the command line. A link that fails to resolve for any
other reason -- a link to a directory that cannot be read, a self-referencing
link, or a link through a file -- stopschelis test, which skipped every
link before.chelis checkreports it and carries on; the entry that follows
in this release describes its envelope. See
#1678. -
BREAKING: C builds encode source stems such as
simple-shapeinto distinct valid C module symbols, consistently in generated source and headers, while retaining the source spelling in artifact filenames.
Generated symbols also change for stems that are C keywords,main, start with an underscore, or start with the reservedchelis_file_escape prefix; external callers should use the generated header. Other ASCII identifier stems keep their symbols. -
BREAKING: The checker retains authored dimension-binder identity through compatible named
axes and generic helper calls, including aliases and trusted serialized checker
contexts. Bodies that give such a polymorphic result a false concrete dimension
now reject instead of losing the binder constraint through the axis name. This
addresses the bounded checker hole in
#1875; it does not introduce
global equality between separately named values or change School's public APIs.Rust embeddings must regenerate stored checker contexts: direct
TypeEnvserde
now uses format 1 with a mandatory private dimension-label summary. Dependency,
stdlib and compiled-context payload versions are 15, 19 and 21 respectively.
Source-free snapshots remain a faithful transport from a trusted checker
producer; structural decoding does not prove an adversarial summary complete.Compiled-context named-query checking also enters the lowerer. Its separate
bounded helper-result repair is tracked by
#1889; checker snapshot
transport alone does not establish native-C or worker/disk query compatibility.
This change does not claim all of #1875 or downstream School closure. -
BREAKING: Reef imports now honor module export lists within a package as well as across
packages. Qualified references and selective imports can no longer reach a sibling
module's unexported definitions; local private helpers remain usable inside their
declaring module. Export the intended cross-module binding before adopting this
compiler.Std.Tokenizernow explicitly exports its existingTokenizertype and
constructor for its consumers. No syntax, runtime ABI, global default or shell pin
changes accompany this repair. -
BREAKING:
chelis provepreserves opaque producer obligations through deep alias chains
and record wrappers. Cyclic proof types converge, and traversal resource
exhaustion reports an error instead of silently removing obligations.The
chelis-prove::obligationshelperscollect_declared_returns,
collect_type_aliases,collect_record_fields, andtype_containsare removed;
callers should usecollect_obligationsto retain collection errors. -
BREAKING:
chelis checknow reports a failure that occurs before the checker runs
through the same JSON report as every other failure, instead of writing a
message to stderr and leaving stdout empty. An unreadable or non-UTF-8 file,
a style-gate rejection and a preparation failure all emit a report whose
errorsarray names the problem, so a consumer can no longer confuse "no
diagnostics" with "the diagnostics were not transported". A style-gate
rejection reports one diagnostic per issue, soerrorshas one entry per
formatting or lint problem rather than a single entry holding the joined
terminal text.These paths now exit
2rather than1, matching every other non-empty
error list, and directory mode exits2rather than1when a file in the
walk fails for one of these reasons. Exit1no longer means "the tool could
not run": the exit status is a function of theerrorsarray alone. The
directory walk failing to enumerate a directory at all still exits1with
no output, which chelis#1678 owns.The human message is still written to stderr on every one of these paths, and
is now also written where a read failure previously reported silently: an
unreadable or non-UTF-8.dp, a missing file, and a read failure inside a
reef package all emitted a report with empty stderr before. The
directory-mode summary lineone or more files failed to checkis gone,
replaced by the per-file diagnostics now carried in each entry's report.One machine-facing message changed for failures that already reached the
report: a missing file, a dangling symlink and a symlink loop now report
failed to read <path>: <errno>where they reported
failed to canonicalize <path>: <errno>, and an unreadable.dpgains the
errno it previously omitted. The diagnostickindand the reportscoreare
unchanged.chelis buildstill saysfailed to canonicalize, so the two
subcommands word the same condition differently. See
#886. -
chelis surfrejects call-first pipe stages whose rewrite would produce a
zero-argument call or leave their parameter unbound. Valid call-first stages
retain their existing spelling and behavior. -
A
shape(...)read that reaches anexpandorinsertsize through a record field (shape(inputs.features, 0i32)) or through a pipe (x |> shape(cast(0, int32)) |> cast(int64)) is now an admissible runtime extent. Both spellings check, and both execute on the evaluator and the C backend in the direct, local-alias,let-bound and piped forms the receipts cover, sochelis lint --fix'sprefer-pipe-operatorrewrite no longer turns a building program into a rejected one. Where the record base is also rebound by an inner binder, the compiler keeps that base's projections where they are and the program needs the prologue-local rewrite it needed before, which the C backend asks for by name rather than miscompiling (chelis#1266, chelis#569). -
Document the historical
cast_truncWireDag addition in the schema migration history and pin the current serialized operation vocabulary to its schema version. -
Check literal and resolved named extent claims against computed size carriers in Eval and generated C for live expand and reshape operations. Mismatches now report the extent Domain trap before reshape's downstream size error.
-
Serialize the wire and Python binding capacity verifiers that intentionally share
their nested rustdoc Cargo target, preventing CI-only lease contention without
weakening the target ownership guard. -
Keep the shared check-report document producer and compact layout while validating report numbers, counter relationships, and typed inferred-signature references through the exact wire carriers.
-
Preserve typed compiler results through Python string conversion for
check_json,compile_json,desugar_json, andeval_json, and validate eval tensor bindings through an exact extraction type before either evaluation route. Bind their capacity authority to compiled conversion ownership, live PyO3 registration, current wire codecs, and executed positive and negative controls, retiring their four binding-census exceptions. Native tensor and DLPack binding remediation remains separate. -
Python's compiled-artifact loader validates the manifest's required ABI version
before decoding metadata, inspecting source files, or loading a shared library.
The writer and loader use the shared compiler API schema so the manifest and its
numeric metadata participate in wire discovery. Missing, duplicate, malformed,
and unsupported versions fail explicitly; valid ABI version 1 metadata retains
its existing JSON representation. Part of
#1288. -
Reject Deep floating literals whose exponents overflow binary64 at lexical
ingress, before checking, evaluation, validation, or decompilation can consume
them. Finite source values, including signed zero, retain their exact lexical
bits. Runtime IEEE infinity and NaN transport remains supported. -
Keep the no-default-feature property runner and diagnostic privacy mutation oracle aligned with exact tensor extents and validated diagnostic severity.
-
Install Python binding dependencies before CI script tests execute the native wire consumer, include native test failure details in the wire verifier's diagnostics, and allow the complete wire verifier to finish within a bounded macOS CI job budget.
-
Updated CLI, Python, and cache regression fixtures for the exact numeric wire formats, retaining bit-level scalar checks, diagnostic member-order checks, and previous-version cache rejection. Runtime-extent observation fixtures preserve their existing values, traps, and pending contracts while adopting f64 report-number encoding.
-
Preserve the exact binary64 bits of source floats and report scores when decoding their emitted JSON decimals, including values that previously drifted by one bit.
-
Register the standalone wire-analysis driver's exact source and existing Clippy verifier owner in configuration coverage, rejecting missing owners and additional unowned sources.
-
Compiler wire dimensions and literal runtime extents use a validated int64
carrier. Decoding rejects negative, oversized, and non-integer extents even
outside a complete DAG. Window sizes and vocabulary extents retain their
operation-specific positivity checks, and valid JSON values keep their existing
representation. Part of #1288. -
Check fixed JSON-number adapters at each source, report, count, and extent field
that owns their numeric domain. Reusing one in an unrelated field or generic
wrapper fails discovery, even when the underlying numeric declaration is already
present in the census. Transparent type aliases preserve the field check. -
Update the diagnostic-checkpoint and pipeline-artifact compile-fail fixture lockfiles for the shared numeric codec's schema dependency, so locked checks reach their intended compiler diagnostics.
-
Discover compiler wire types through all public serialization exports, including
imported definitions, aliases, private fields, and concrete generic instances.
Retain explicit ownership of binary-cache candidates and bind the defining crate
artifacts to actual codec execution. Missing imports, unresolved generic exports,
and unsupported serializer shapes fail the discovery check.
The verifier also checks the compiled Python crate for binding-local serialized
type definitions, so a private manifest copy requires shared-schema ownership. -
Fixed #1288's Python wire verification on Linux by binding the direct compiler driver to its pinned sysroot libraries, preparing its owned Cargo target safely, and checking the ratified WireDag v9 identity.
-
The numeric surface census now resolves stdlib imports, aliases and recursive
generic types through compiler declaration APIs, rejecting unresolved types
instead of silently dropping numeric capacity. Existing registered stdlib
identities are preserved. -
Use the Rust module's exact test names for the capacity oracle's standard-library controls, preserving all twelve selected tests and their positive, negative, and mutation obligations.
-
A named extent check is now derived only from a signature someone wrote. A kernel the compiler synthesizes over several top-level bindings takes its parameters from those bindings, and two of them naming an axis the same way is a coincidence; reading it as an assertion made a correct program trap
Domainat run time. -
chelis build --target hipagain accepts a signature that repeats a dimension binder, such as an ordinarymatmulhelper. The retained interface witness carries an entry obligation rather than a runtime shape read, so the host prologue discharges it; a shape read a device node actually consumes is still refused under [05-SHAPE-1]. -
A declared result dimension that claims a named extent is now checked when the program runs, on both the interpreter and the compiled C lane, and traps
Domainnaming the two disagreeing parameters and their axes. A cross-tensor read under a named claim, a foreign claim over a same-tensor read, and a dimension binder repeated across parameters that the body never reads all ran silently before. -
expandandinsertnow accept a size that is checked integer arithmetic over
a runtime value, such asinsert(b, 0, mul(shape(x, 0), 2i64)). The compiled
lanes previously refused to lower such a size whilechelis evalexecuted or
crashed on it. The extent is now ordinary integer dataflow that every lane
executes, and a literal or named claim over the axis is checked at execution
and trapsDomainon mismatch. Arithmetic whose operands carry no shape source
at all, such asadd(k, 1i64)over a bare scalar parameter, is still rejected
at check with its existing diagnostic. -
A declared result dimension over a runtime-bound
shrinkis kept as a claim and
checked at run time, for the outermost activation: an exported def, a top-level
value binding, or an inlined root. A function declaring-> tensor[2, f32]
whose body shrinks to a different extent previously returned that other extent
and exited zero on both the evaluator and the compiled lane; it now raises
numeric trap: domain in shrink at int64at theshrink, before the result is
allocated, with the claimed and observed extents on an accompanying line. A
literal claim survives a call from inside another def's body; a
parameter-bound named one does not yet, and
#1800 tracks that. An
extent an operation computes can now be a member of a runtime extent equality
class and be guarded there;shrinkis the operation admitted, andpadwith
non-zero padding andstridewith a non-unit step are unchanged. The context
line accompanying a local extent trap now names the operation instead of an
internal node number, on every lane. See
#1397. -
A top-level definition whose result type carries a runtime extent now runs. A
nullarydefreturningtensor[*, f32]was dropped from the root manifest, so
chelis evalprinted nothing and warned that the input contained only
declarations, andchelis buildemitted noint main(, producing an
object-only program that exited 0. Both lanes now execute it and size the
output from the realized extent. This also unmasks the vectorized case: a
vmapover a function whose shrink bound is read from the mapped tensor's own
shape executes with its exact values. A root whose result keeps an unresolved
type, dim or rank variable is still refused, because an uninstantiated
variable has no value or ABI. See
#1397 and
#1378. -
Reject host casts whose target dtype remains unresolved after specialization instead of silently using the operand dtype. Recursive generic casts and published
arange/linspacecalls retain evaluator/C parity at their concrete integer and float widths. -
copy,cast,cast_truncand the ten csv routes no longer reject an operand
whose type is merely unresolved at the moment the call is checked. Each now
suspends its decision on the operand's type variable and settles it when that
variable is bound, running the same decision function as the immediate path, so
the verdict depends on the program rather than on the order inference reached
it. The suspended call's result is not generalized by an enclosingletuntil
the decision settles, so binding it to a name cannot detach it from the call
that produces it. An operand that is never resolved is still rejected.
round_toand the six shape-computing routes (gather,scatter,
scatter_replace,diagonal,traceandconcat) still reject an unresolved
operand. See #1489. -
gather,scatter,scatter_replaceandtraceno longer reject an operand
whose type is merely unresolved at the moment the call is checked. Each now
suspends its whole decision on the operand's type variable and settles it when
that variable is bound. The axis is normalized against the operand's settled
rank, so a negative axis on a deferred operand means the same axis it means on
a resolved one, andscatter's updates-shape equation and mode check are
replayed at the binding rather than dropped. An operand that is never resolved
is still rejected.concatanddiagonalstill reject an unresolved operand:
they compute a new extent from the operand's dims, and deferring them admitted
programs whose declared result shape was false. See
#1489. -
Preserve distinct root identities for aliased scalar and tensor values, avoiding
internal root-count mismatches. Function aliases remain callable entries, and
nullary aliases retain their callable identity in argument and local-binding
positions. Calls through aliases expose their concrete results in eval and C builds. -
The dtype-admissibility checks now run against the operand a call actually receives. A builtin whose operand was still an unresolved type variable when its route ran skipped those checks forever, so
sqrt,and,add,mean,softmax,uniform_like, the integer binary operators and the shifts each accepted a program they reject when the same operand is written out directly. The call is suspended on the deferred shape ledger instead and validated once the operand binds, with the diagnostic a resolved operand gives. Two consequences worth knowing. An operand that never binds stays accepted, because these routes do not require a shape, so a genuinely generic definition is unaffected. And an empty tensor literal under a shape- and dtype-preserving route is now validated against the dtype its declaration implies:def f() -> tensor[3, int32] = sqrt(to_tensor([]))was accepted and is now rejected. Under a reducing route the literal's dtype is still unchecked, which is chelis#1805. -
A builtin whose operand was still an unresolved type variable when its checker route ran published a result it never derived and skipped its own validation forever, so
permute,shrink,stride,pad, thereduce_windowgroup,reshapeand roughly fortyapp_postcollection, host and string routes accepted invalid calls over a lambda parameter, a pipe stage or any value bound after the call. The operand did not have to be the first one:whereaccepted mismatched branch shapes,indexa non-integer index, andpermutea non-int32 axis, each while the tensor operand was already settled. Such a call is now suspended on the deferred shape ledger and its own rule runs again once the operand binds, so the late-bound call is rejected with the same diagnostic the resolved call gives. Whether an operand that never binds is an error now depends on the route: one that needs a shape (permute,shrink,stride,pad, thereduce_windowgroup,reshape) is rejected at the declaration boundary, so a lambda that is written but never applied is newly refused, while a collection, host or string route accepts it silently, because a polymorphic definition legitimately callslenordict_ofover a value that acquires its constructor only at a call site. -
Allow tensor casts to bounded
Float,Int, andNumericdtype parameters,
preserving shape and using each call's actual target dtype in the evaluator
and direct compiled calls, including targets selected by scalar arguments or result type constraints. -
Preserve output written before compiled runtime traps when stdout or stderr is buffered, including Linux pipes and redirected files.
-
Shape-derived singleton broadcasts execute on the C backend. Anonymous output
axes use the broadcast size and the correct kept-axis sources for outputs
without explicit named dimensions; literal result claims remain intact.
Previously C could guard the size-source tensor against the operand's extent
of one or refuse a folded shape read. See
#1619. -
Queue local and full gate runs in ticket-registration order so new runs cannot
overtake waiting gates. Report queue positions and recover abandoned tickets after
cancellation or process death. Active worktrees need the updated gate to participate
in the queue. -
Capacity planning uses exact, domain-preserving keys without the legacy
saturating normalizer. Finite dimension evaluation rejects overflowing products
in both debug and release builds. See #1629. -
Host tensor allocation, repurpose, copying, and indexed movement now consume
privately checked shape, count, byte-size, and offset metadata. Invalid sizes
fail before allocation or access in debug and release builds, and negative
padding widths reportDomain. See #1631. -
Preserve generic value-root calls' concrete argument dtypes and tensor extents in evaluation and generated C, including scalar constructors and Bool tensor results.
-
Empty and nested-empty List-to-tensor evaluation preserves the checked scalar element dtype, including bool, instead of substituting f32. Nonempty leaves validate against that dtype, and unobserved inner extents require explicit shape evidence.
Eval rejects an unconstrainedto_tensor([])rather than choosing a dtype; give the empty List an explicit element type. -
Generated C now releases unused owned function parameters at their verified
entry cleanup point, including constant-gradient inputs. Caller-owned inputs
remain borrowed and valid after the call; callers should not add compensating
releases. See #1684. -
Generated C now releases temporary boxed tensor owners after assembling a
multi-output helper result, fixing leaked output references from multi-input
gradients. Returned tuples and acquired fields keep their existing ownership
contract; callers should use normal releases, not compensating extra releases.
See #1685. -
Keep capacity-census codec graph identities stable when comments move unchanged implementations, while retaining current source and artifact proof.
-
Preserve integer literal widths when lowering host function bodies. Nullary
calls, parameterized constant returns, and local literal bindings now keep
matching ownership schemas and compile without an explicit literal cast.
Marked integer-source float literals also finalize directly at their declared
float width instead of retaining the unconverted integer. -
Preserve completed
printanddebugoutput before an evaluator timeout's forced exit, using the same text/JSON channels as cooperative failures. A normal completion disarms the watchdog and claims output once. -
diagonalover an axis pair with one symbolic and one literal extent no longer admits a
declared result extent the runtime can never produce.[05-OP-33]takes the smaller selected
extent, so the literal axis is an upper bound: a declared extent strictly greater than it is
now aDimensionMismatchat check time, on both thedef/sigroute and a block-scoped
ascription. A declaration at or below the bound stays accepted and is checked at run time: a
host-lane function whose return expression is a direct builtin application and whose declared
tensor result carries a literal extent now trapsDomainon disagreement, identically on
chelis evaland the C backend, instead of silently returning a differently shaped tensor. -
Run chelis-prove integration-test SMT solves in dedicated child processes, preserving real solver verdicts while containing crashes and hangs during parallel tests.
-
Scalar
gradresults retain their scalar dtype through evaluation, including tuple, List, and ADT cotangent leaves. Checked scalar-gradient comparisons and property fuzzing now execute without a spurious scalar/tensor mismatch; genuine rank-zero tensors remain tensors. -
The runtime-extent class oracle (
scripts/runtime_extent_oracle.py) runs again. Its
per-target expected test receipts moved out of hand-maintained Python tuples into the
reviewed manifestscripts/runtime_extent_oracle_targets.json, which two independent
readers enforce: the oracle builds its cargo commands from the same rows it checks, and
a new--fasttripwire parses each named source and fails the pre-push gate when a
rename, an unregistered new test, or a new#[ignore]moves a row's real inventory.
Renaming a selected test previously broke the oracle silently for everyone who did not
run it. See #1742. -
Fix bounded tensor casts whose target dtype is constrained only by the result type, preserving independent dtype instantiations in generated C.
-
Explicit multi-parameter
grad(..., wrt=(...))results preserve the written target order, including mixed scalar/tensor and structured cotangents. Existing nonzero fusedvmap(grad(...))results also preserve that order; missing zero-gradient groups in that fused path remain tracked by #1975. Default gradient order is unchanged. See #1753. -
Concrete tensor-returning dropout helpers retain source-static rate arguments
through evaluator calls, including encoded Reef library contexts. Local helpers
also use the existing fixed-control C plan. Runtime-rate public C entries,
generic evaluator helpers, and compiled-in-context C plan transport remain
unsupported. Part of #1764. -
Generic fixed-rate dropout helpers now evaluate through the checked execution
plan, preserving concrete float dtypes, gradient replay, and the following
random draw. This fixes the evaluator'sunknown runtime name dropouterror
for source-static casts such ascast(0.5, p).
Effecting scalar data arguments are evaluated once, preserving the handled
random stream through subsequent helper calls. -
Specialize fixed dropout rates through typed helper parameters, generic dtype casts, and gradient captures in source-owned IR evaluation plans. Ordinary host evaluation keeps its existing precise rejection until it can transport these plans; compiled dropout support is unchanged.
-
Compiler APIs reject Resource regions incompatible with the selected C or HIP
target before exposing generated artifacts or emission observations. Selected
entries check reachable helpers without imposing unused helpers' device
requirements. Public request, wire, and generated ABI layouts are unchanged. -
Declared literal result guards follow host block tails, bindings, and callee results, preserving local effect order.
-
gradagain differentiates a stack of runtime-sized windows. A reshape whose
target extent is computed at run time names that extent after the scalar node
that produces it, so two reshapes sized from one scalar agree on the extent.
concatover such rows stays on its differentiable padding cascade instead of
falling back to the host-runtime lane, where the reduction that followed it
collapsed to rank zero and the backward graph could not be built. -
The staged host-source partition now declines a body that reaches a runtime-shaped
to_tensor, allowing the existing host path to evaluate it. This restores the Shoals symbolic column-reshape and vmap program on eval and generated C without weakening the staged input ownership check (chelis#1779). -
A
def main() = f(...)root whose inferred result dimension restates the callee's own dimension binder no longer emits a secondclaimed = Nextent guard ahead of the named one. The guard that runs names both disagreeing parameter axes, which is whatspec/04-type-system.mdsection 4.7 asks a runtime extent diagnostic to convey. A literal claim is declined only when a named claim already makes the same comparison against an extent the lowered graph fixes; an extent an exported kernel's parameter promises keeps its own guard. -
Host tuple functions check repeated dimension binders at entry, with the same load-trap diagnostic as tensor kernels.
-
Two roots merged into one emitted C function no longer share one declaration of a dimension binder each of their signatures spells. Every scope after the first declares its own identity from its own input, so the second root sizes its work from the tensor it was given rather than from the first root's extent (chelis#1788).
-
Keep generated C host Random state local to each public invocation, preserving nested seed restoration and existing Uniform sample bits across private helper calls. Reentrant and concurrent calls no longer overwrite each other's seed or ordinal; public function and tensor ABIs are unchanged.
-
chelis evalreports ashrinkwhose runtime end runs past the operand's
extent asspec/05-risc-primitives.md§2.4.1's overshoot error, in the same
words and with the same exit status as the compiled lane:Domain: shrink bounds outside input extentfollowed by thenumeric trap: domain in shrink at int64line. Previously the evaluator panicked and exited 101 when the declared
result claimed the span's arithmetic width or claimed nothing, and reported a
mismatch against a claim that was not the defect when it claimed something
else. See #1797. -
A declared result dimension whose axis passes through an extent an operation
computes is now guarded at that operation on both host lanes, instead of
returning the computed extent at exit zero (chelis#1798). A named result claim
consumed inside another function's body is guarded through its resolved binder
(chelis#1800), and a declared literal over a non-zeropadnow reports the
claim rather than the movement plan's generic target mismatch (part of
chelis#1837). -
A call whose result extent is decided only at run time no longer leaves the
callee's dimension variable unresolved. A dimension variable an application's
instantiation mints, that unifies with a runtime extent*and that no
argument of that application binds to a literal or named dimension, now
denotes that runtime extent. A nullary root reached through such a call used to
generalize the variable instead, which left the root with no ABI and dropped it
from both lanes in silence:chelis eval --filewarned that the input held
only declarations, andchelis build --target cemitted no entry point. Both
lanes now execute the root, and a claim the call refutes traps as
spec/04-type-system.md§4.7 requires. See
chelis#1801. -
Accept explicit negative
i64seed literals in Surf and Deep, preserving their signed 64-bit seed bits through evaluation and compiled C. Runtime, cast, and other computed seed expressions remain rejected. -
The operand-dtype policy now rejects inadmissible instantiations of a precision-generic helper when its argument is a tensor literal, a call with a concrete declared result, a parameter or value binding resolved in lexical order, or a tuple projection from a concretely typed parameter. This covers
meanreturning an integer quotient throughg[p]and bool arithmetic through the same argument forms. Declared dtype-family bounds are checked at the definition, and a precision that binds one application later is checked on replay. Function-value calls, polymorphic call chains, local-lambda transport and ADT-field arguments retain tracked gaps under chelis#1805, #1940 and #1941. -
gradwith a tensor-typed singlewrt, over a function whose declared extent disagrees with its operands, now traps with the same rendering as the undifferentiated call on both the interpreter and C lanes, instead of returning zeros and exiting zero (chelis#1821). The otherwrtkinds the spec admits still differ between the lanes and are tracked: a multi-targetwrt(chelis#1920), an aggregate-typedwrt(chelis#1924) and a float primwrt(chelis#1934). -
An
expandwhose kept axis carries a signature dimension binder now builds and runs on the C target with the size argument's extent on the expanded axis, instead of failing ownership lowering or, with no consumer, trapping at run time while the interpreter returned the right answer (chelis#1822). -
Fixed-control
dropoutnow reaches ordinary C source, API, and CLI builds
without losing its source execution plan (part of
#1764 and
#1192). An opaque host carrier
binds concrete generic-helper graphs to their private forward/replay metadata
through ownership verification. Direct entries keep the public four-argument
ABI; host helpers use the existing invocation-local RNG frame. Runtime controls
and GPU targets remain typed rejections. -
chelis evalno longer re-derives the kernel-lane decision for every imported definition it applies. The interpreter now holds the host-lowering memo for the whole evaluation, so a program that calls into a recursive library such asStd.Io.Jsonruns in seconds again instead of expanding that library's call graph as a tree per definition (chelis#1829). -
A shape-computed route whose operand is still an unresolved type variable now
ties its result to the shape it computes once the operand binds, whatever the
operand's provenance. Amatch-destructured tuple element, a field read on an
unresolved record target, and a deferredcopygate's result previously let a
false declared result shape check with no errors. A reducing route over an
operand no declaration can determine, such asmean(to_tensor([]), 0i32), is
now rejected at the declaration boundary instead of failing only at evaluation. -
A declared result extent that the body refutes once a call is inlined is now rejected at lowering, before the program runs (
chelis checkstill accepts it; chelis#526 owns the checker view), instead of executing with the undeclared shape, trapping for a comparison that could never hold, or failing an internal IR invariant on the C lane.chelis evalandchelis buildreport the same diagnostic and exit 1. The rule covers a literal claim, a named claim whose declaring argument is itself fixed, an axis an operation leaves unchanged, and activations reached through a pipe or avmap. A claim on an axis the lowered graph does not fix, areshapeor a shape-read-sizedexpandamong them, keeps its existing runtime guard (chelis#1837, chelis#1930). -
Emit minimum-int64 host constants, including literal Random seeds, as portable
INT64_MINinstead of an out-of-range positive decimal token under unary minus.
This restores strict C compilation without changing values, seed streams,
ordinary literal spellings, language admission, or public interfaces (#1859). -
The backend capacity census now preprocesses the HIP published-header closure
against the committed Phase-0 SDK stubs under a fixed, closed include universe,
fails if include attribution escapes it, and selects every recursively
discovered HIP support header before row extraction rather than filtering rows
by basename. Metal remains unenrolled while its recursively discovered
published header set exports no ABI, with shared lexical parsing and an
executable tripwire for the first public declaration in any nested or root.h. -
Remove the stale regular-CI target for the retired
expandspelling inventory
so pull requests can execute the remaining reviewed integration selection. -
HIP narrow-float build rejections now point to the operation-limited target
contract inspec/04-type-system.md§1.1.3 without repeating a drifting
capability list. The contract names the shipped exact-bitRealize, dedicated
ReLU, tensor transport, and hipBLAS matmul surfaces. -
Fixed-control C dropout entries compile from bare Surf and Deep programs as
they do beside unrelated host declarations, retaining the sealed source plan.
The new standalone admission requires a closed inferred Random effect row;
an inherited-Random bare entry remains unsupported.
Runtime-rate and unsupported device entries still reject. Correct the stale
C admission guards and nonliteral-window diagnostic expectation (#1872, #1865). -
C callable compilation in Reef contexts now preserves source-fixed dropout plans
through imported helpers, including decoded contexts, saved-mask input gradients
and subsequent draws. Existing entry selection and runtime-control rejection
remain in force. See #1876. -
Generic helper results now retain a caller-established named axis while
lowering, so direct and aliased calls can be reduced by that axis correctly
(Part of #1889). -
Fixed evaluator closure setup incorrectly equating independent wildcard tensor
axes or arguments. Functions acceptingtensor[*, *, f32]now accept nonsquare
and empty shapes; genuine repeated named-dimension constraints remain enforced. -
Preserve evaluator execution of annotated softmax helpers over tensor concat
when runtime concat extents come directly from inputs, lexical aliases, or
helper forwarding. Static-width concat kernels remain eligible. Forced tensor-DAG
concat now rejects unsupported construction instead of fabricating a scalar input.
Computed dynamic concat and C host/tensor partitioning remain outside this repair.
Shared acyclic helper admission reuses identical resolved contexts without
conflating different argument facts or caching cycle-truncated traversals. -
Preserve caller argument values when an earlier helper parameter has the same
name as a later argument. Renaming helper parameters no longer changes the
covered direct tensor calls' results. See #1915. -
The capacity-census relocation fixture now imports an exported transparent
alias while keeping its underlying declaration private, matching module export
rules. Numeric/boolean and direct-private-import controls remain covered without
changing the census classifier, frozen inventory, or test roster. See
#1919. -
Fatal tensor-helper diagnostics raised directly during a helper-summary probe
now return through the existing error channel after probe cleanup, instead of
unwinding out ofevalor silently exiting the CLI with status 101. This changes
diagnostic transport, not insert/concat support or the existing deferral of errors
already returned by nested probes. See #1922. -
A pipe stage is now typed and lowered as the application it denotes, so every rule that reads an application's arguments applies in pipe position: a materializable
expandsize orsumaxis downstream of a bare-nameto_tensorstage checks clean and runs on both lanes instead of being rejected at the declaration boundary (chelis#1923), the same shape reached through a callee builds on the C target instead of failing shape-source resolution at lowering (chelis#1791 half A), and a genuinely sourcelessexpandorinsertsize is rejected at check in pipe position with the same diagnostic the direct spelling carries (chelis#1791 half B).chelis lint --fixtherefore no longer turns a building program into a rejected one by rewriting a call into a pipe. Two public surfaces change:chelis deep --annotateshows the folded application rather than apipenode, and thechelis checkscore of any program containing a pipe shifts, because the score is a ratio over node counts and the fold replaces apipeplus its synthesized stage lambda with oneapp. No diagnostic text moves, and a clean program still scores 1.chelis deepandchelis surfstill print the pipe. -
Preserve lazy captured-initializer errors when evaluating host
gradandvmaptransforms. Prepare inputs using the existing execution selection before running the same lowered graph or plan; retain capture precedence and the existing vmap capture-rank refusal. This does not change declaration memoization or resolve all global-capture issues in #1956. -
Preserve selected zero cotangents, their caller shapes, and forward checks in fused
vmap(grad(...))IR/evaluator lowering without treating unresolved callable values as constants. Native multi-result export remains outside this repair. -
The Deep validator now accepts the explicit
*wildcard as the sole child of
d-name, matching compiler-emitted Deep while continuing to reject wildcards
in other child roles. See #1982. -
Keep ordinary
shapevalue reads scalar undervmap, shift the queried axis, and broadcast the result through existing consumer/root expansion. This also preserves valid nested shape claims when gradient forward work remains live. -
Runtime extent declarations now come from each axis's extent source rather than from a search for an input whose type carries a matching dimension name. A kept output axis over a movement operation's runtime extent builds and runs on the C lane instead of aborting with an internal compiler error (#665), a name with no resolvable extent source is a typed receipt rather than a panic, and the evaluator no longer rejects a merged kernel in which two independent signatures happen to spell a binder the same way (#1566).
-
chelis checkbuilds its report document by serializing one typed value,
chelis_compiler_api::schema::CheckResult, instead of the twoformat!
templates that previously assembled it beside a type describing the same
shape.inferred_signaturesbecomes a member of that type rather than a JSON
string spliced between two literal keys. The emitted bytes are unchanged,
verified against the prior binary across 6324chelis checkinvocations over
1581 files. Failures that short-circuit before the checker still emit the
report; failures that bypass it entirely, such as an unreadable file or a
style-gate rejection, remain outside it and are tracked by
#886. See
#1672. -
chelis check's per-file path can no longer fail without producing a report.
The functions that check one file return the report directly instead of a
Result, so a failure has nowhere to propagate to and must be carried as a
diagnostic. The visible change ischelis check --show-inferredon a program
whose inferred signatures cannot be built -- for example one with a negative
dimension extent, itself a checker defect tracked by
#1768. On a single file
it previously exited1with nothing on stdout; it now emits a report whose
errorsarray names the problem, prints the same message to stderr, and
exits2. In directory mode such a file previously produced
{"file":...,"error":"..."}in place of a report and the run ended with
one or more files failed to checkand exit1; it now contributes a report
like any other file and the run exits2. A measured report that falls
outside its own numeric domain is likewise reported rather than propagated.
See #886. -
Generated C BLAS submissions validate matrix shapes, batch indices, vendor dimensions, and conversion scratch capacities through checked runtime metadata. Reduced-float scratch uses runtime tensor storage. Canonical contraction selection is unchanged.
-
Generated C tensor literals validate their complete shape, dtype and stored element count before allocation or reuse, and preserve every stored dtype through tagged writes.
-
Generated C canonical JSON object ordering allocates its index scratch through the checked runtime tensor owner and releases it after ordering, including for empty objects.
-
Generated C movement loops use checked immutable geometry plans without per-element coordinate scratch, and local insertion extent failures retain the insert diagnostic identity.
-
Generated C reductions and Count now validate result shapes, reduction domains, indices, and scratch sizes through checked runtime metadata before allocation or access. Sum preserves its canonical adjacent-pair tree and explicit accumulator width.
-
Generated C reads checked shape metadata without runtime-rank stack arrays and allocates host results through checked input shape and explicit output representation.
-
Generated C sparse kernels and host helper loops validate exact shapes and project checked indices before allocation or access. Scatter copies use checked byte counts, preserving empty domains, exact stored values, and duplicate-update order.
-
Generated C window reductions and gradients validate complete window geometry and result/cotangent shapes before storage submission, and use checked int64 index projections instead of coordinate scratch arrays.
-
Make the runtime representation Phase 1 gate require frozen test selection and current framework execution receipts for checked host/C metadata and exact storage capacity, with mandatory production mutations and explicit manual-test exclusions.
-
Generated C validates elementwise input shapes through checked runtime metadata
before allocating or repurposing output storage. Shared elementwise, fused, cast,
and realization loops use exact scalar or identity index projections, including
empty and dynamic-rank domains; scalar fused inputs no longer enter flat-read
optimized paths for multi-element outputs. The runtime exposes two tagged-shape
and tensor-domain validation operations for generated callers. -
Generated C permutation and expansion now validate target metadata before allocation and use checked runtime coordinates. Movement preserves exact stored values across all tensor dtypes, including int64 values above 2^53, and rejects invalid or overflowing metadata.
-
Large generated scalar functions avoid repeated tree copying during parsing and
desugaring. Block lookahead shares immutable tokens while retaining its own cursor,
and Deep normalization visits children directly instead of cloning their entire
subtrees first. Binding boundaries, metadata and the normalized representation
remain the same. -
Generated C padding, shrinking, and striding validate complete shapes and coordinate arithmetic before allocation or access, preserving exact dtype bits and rejecting overflowing metadata.
-
Generated C reshape now validates target metadata through the checked runtime
before allocation or copying. Valid empty shapes such as
[INT64_MAX, INT64_MAX, 0]no longer overflow an intermediate product, and invalid
counts, strides, or byte sizes fail before access. Generated tensor snapshots
consume checked strides and logical byte counts. The C runtime also exposes
metadata observation, reshape validation, and an owned reshape operation that
preserves exact stored bits for every supported dtype. Part of
#889 and
#893. -
Computed reshape result claims and broadcast unit preconditions survive inlined
calls, aliases and discarded results. Explicit checked extents retain the required
witness independently of result metadata, so mismatches report a Domain failure
before shape-dependent allocation or element access.Computed remainder targets retain result claims on Eval and C, including HIP host-C entry selection. Signed remainder preserves exact minimum-integer behavior and DivZero diagnostics.
Host scalar reshape targets retain checked claims through a shared staged plan,
including list-derived sizes, scalar conditionals, tuple captures, scalar/tensor
views, native lists, host literals and aliased helper calls. Stages
preserve eager evaluation, handled Random streams and imported definitions. -
Fixed-control source evaluation now applies dropout at every active float dtype,
validates its same-dtype rate before drawing, and preserves accepted empty and
dead-value draws. First-order input gradients replay the actual forward mask
without advancing the ambient stream; nested seed handlers preserve parent
state on errors. Ordinary, prepared, and contextual evaluator paths share this
execution plan, including checked reshape claims whose sizes are produced by
host expressions. Staged execution preserves earlier draws on a guard failure
and retains forward keys for replay across stage boundaries.
Legacy Dag-only APIs and wire/cache formats are unchanged;
runtime-rate AD, random vmap, higher-order AD, general UniformLike numerics, and
compiled dropout remain outside this bounded repair of
#1295. -
Type environment snapshots share immutable signature bodies, reducing allocation during checking of modules with many wide function signatures while preserving lexical isolation and serialized environments.
-
Tensor helpers check runtime extent claims in declared parameter order. Exported
calls and top-level bindings now report the same first failing parameter as
inlined calls when multiple claims fail. Part of #1277. -
Share immutable resolved function bodies across IR scope snapshots, avoiding repeated deep copies when lowering many scalar helpers (chelis#2005).
-
Tier B no longer reports cvc5 counterexamples produced by an
out-of-domainsqrtvalue (chelis#1475). Every exact square-root argument
must first be proved non-negative from independent, sqrt-free total
preconditions. Unsafe or unproved arguments fall through to Tier C instead
of adding a domain assumption, while guarded and algebraically non-negative
arguments retain SMT discharge. Domain authorization and the main query
share the caller's timeout instead of each consuming a full timeout. -
Declared tensor result extents survive function checking and inlining. The
literal claim in a shape-derivedinsertkeeps its argument witness and
required Domain failure, including nested calls and discarded results.
WireDag v8 carries the witness, its invocation dependencies and provenance;
older wire and compiler-cache versions are rejected or missed. Part of
#1277; resolves the public
#1377 reproduction. -
Generated C checks simultaneous local reshape extent claims in declaration
order, including when the output reverses the claimed axes. Eval and C now
report the same first failing claim for that case. Part of
#1277. -
Avoid copying the unvisited let body at each binding during macro expansion of large scalar blocks. Expansion preserves the existing metadata, lexical blockers and malformed-form behavior.