Metadata-Version: 2.4
Name: rslc
Version: 0.3.0
Requires-Dist: pytest==9.0.3 ; extra == 'dev'
Provides-Extra: dev
License-File: LICENSE
License-File: THIRD_PARTY_LICENSES.txt
License-File: third-party/rust/COPYRIGHT-library.html
Summary: Correctness-by-construction compiler for Rating Specification Language
Author: EffectiveAI
License-Expression: LicenseRef-Proprietary
Requires-Python: >=3.12
Description-Content-Type: text/markdown; charset=UTF-8; variant=GFM

# rslc

`rslc` is the correctness-by-construction compiler for Rating Specification
Language. It is a standalone distribution and does not depend on
`effectiveai-tools`.

The bounded structured frontend for native Python authoring is specified in
[D-0127](docs/decisions/D-0127-structured-native-authoring.md). It constructs
syntax nodes directly and shares the text frontend's semantic checker and
native runtime. See the [Relativities example](../../../docs/relativities/native-authoring.md)
for the supported first slice and its limits.

## Module orientation

| Path                      | Role                                                                              |
| ------------------------- | --------------------------------------------------------------------------------- |
| `crates/rslc-core/`       | Lexer/parser, CST, elaborator, typed Core IR, numeric kernel, reference evaluator |
| `crates/rslc-backends/`   | Python emitter and table CSV loader                                               |
| `crates/rslc-py/`         | PyO3 bindings                                                                     |
| `python/rslc/`            | CLI / Python API; `std` symlink for editable installs                             |
| `std/`                    | RSL stdlib (wheel-bundled at `rslc/std` via build.rs + maturin include)           |
| `lean/`                   | Lean 4 numeric/eval model and extracted conformance vectors                       |
| `docs/decisions/`         | Binding design decisions cited by stable ID                                       |
| `docs/field-guide.md`     | Implementation surprises (worker-owned)                                           |
| `docs/rating-outcomes.md` | Opt-in public rating outcomes and liveness diagnostics                            |
| `corpus/`                 | Gitignored production fixtures (SHA-256 pinned via `corpus/MANIFEST.json`)        |

`rslc` is the standalone compiler CLI. Effective agent sandboxes expose the
same five commands through the registered `rsl` toolkit, which delegates
directly to this parser and these handlers.

`rslc` owns source-to-artifact work only. Published-release operations use
`raters list|show|download|rate|deploy|rollback` in an Effective session or the
matching `effective raters` commands from a host shell:

```text
RSL source -> rslc export -> bundle -> raters deploy -> raters rate/download
```

## Strict rater publication contract

`rslc check` requires the source entry point to declare its RSL version, the
four catalog fields rendered by `/raters`, and an explicit public rating
outcome contract:

```rsl
spec {
    rsl: "0.3",
    carrier: "Acme Insurance",
    state: CA,
    product: "Homeowners",
    effective_date: 2026-08-28,
}

RatingOutcomes = {
    written_premium: Policy.written_premium,
}
```

`rsl` names the RSL version the source is written for (D-0120). It is the
first field; `rslc fmt` prints it there. A missing or older version fails
`rslc check` (`E-RSL-VERSION-MISSING`, `E-RSL-VERSION-OLD`); a newer version
stops every command with `E-RSL-VERSION-NEWER`, which asks for a newer `rslc`.
`rslc fmt <dir> --migrate` runs the language steps newer than the declaration
and then declares the compiler's version. The bundle manifest records
`rsl_version`. Each required `spec` value must be non-empty. The catalog remains an open map,
so raters may carry additional metadata such as `version`. `product` is the
customer-facing rater label. The compiler rejects the retired `name` field.
Artifact inspection remains independent of source compilation. The strict
check guarantees a deployable rater can populate the list page.

## Public rating outcomes

An RSL declares its explicit public outcome contract with a non-empty top-level
`RatingOutcomes` block:

```rsl
RatingOutcomes = {
    written_premium: Policy.written_premium,
    technical_premium: Policy.technical_premium,
}
```

Each name is stable public metadata. Each target must resolve to a distinct,
computed attribute whose type is `Premium`, `Num`, `Rate`, `Factor`, `Pct`,
`Bool`, or an enum. At least one outcome must be a `Premium` (D-0098); a
`Bool` or enum outcome publishes a fact, such as a disclosure flag, next to
the premium. Multiple premiums are valid. Historical sources without the block remain parseable and
inspectable, but do not pass strict `rslc check`. See
[rating outcomes](docs/rating-outcomes.md) for validation, the
`E-ORPHAN-COMPUTED` error (RSL 0.4), and the catalog/4 field.

An RSL 0.4 `Rater.rate()` evaluates only what the declared outcomes demand,
one map cell at a time (D-0113): admission first, then each outcome's
calculation. Calculations are total (D-0114), so this changes the work, never
the result. `rate_detailed()` runs the same evaluation and reports what it
computed; values and cells that nothing demanded are omitted. An RSL 0.3
source keeps the eager schedule, so a `reject` inside any calculation still
fires.

## Sources and citations

A Source has a closed schema (D-0106):

```rsl
Sources = {
    manual: Source = {
        artifact: artifact("019f819b-1674-7046-bc54-6f18cb149d6d"),
        kind: pdf
    }
}
```

`[cite: source:region]` is the only citation spelling. It can follow a table,
constant, step, attribute, input, or `reject(...)`. The region must match the
Source's kind: `p33` or `pp20-24` (pdf), `'Sheet'!A2:AQH2` (xlsx), `row 12` or
`rows 12-20` (csv), and `anchor "fragment"` (html). The compiler checks the
region syntax and never opens the artifact.

Provenance is never a runtime value. `Source`-typed values, enums of artifact
IDs, `_source*`/`__cite`/`source_part`/`source_*page*` CSV columns,
`*_verified`-style Bool inputs that gate a `reject` or that nothing reads, and
`*_complete`/`acknowledge_*` Bool inputs that gate a `reject` fail with
`E-PROVENANCE-RUNTIME`. A table can
name one of its declared citations per row in an optional `cite` CSV column.

`rslc fmt path/to/rater.rsl --migrate` applies the mechanical rewrites: page
spellings, the two Source fields where the mapping is mechanical (other
Source fields move to a comment above the Source; a Source with no artifact ID
stays as written), `__cite` to `cite`, legacy artifact cite cells
(`[^a:<uuid>:p.N]`, `[label](/artifacts/<uuid>?page=N)`) to the one Source
with that artifact, and deletion of unread
`*_source`/`*_fidelity` fields and provenance CSV columns. It reports what
still needs an agent.

A failed `rslc check`, `rslc eval` or `rslc export` on a rater that declares
an older RSL, or no RSL version, prints one `N-LEGACY-RSL` note before the
diagnostics (`notes` in `--json`). The note names the migration path:
`rslc fmt <dir> --migrate`, then the remaining diagnostics.
`python/rslc/legacy.py` owns the note.

## Exact numerics (D-0109)

Every runtime number is an exact rational. `+`, `-`, `*`, `/` and `avg` are
exact, and no operation rounds implicitly. Only `round(x, scale, mode)` and
`root(x, n, scale, mode)` narrow a value. The mode is required:

```rsl
step premium [cite: manual:p12] {
    base_premium: Premium = round(self.base_rate * self.factor, 0, half_up)
}
```

The modes are `half_up` (ties away from zero, the former R-0001 rule),
`half_down`, `half_even`, `up`, `down`, `ceiling` and `floor`. `scale` is an
integer and can be negative (`-3` rounds to thousands). `pow(x, n)` takes an
integer `n`; `root` is the only fractional power.

A declared input `precision` (`int` or a power of ten such as `0.01`) is an
admission contract: an input off its grid fails before rating. Strict
`rslc check` also requires every numeric input to declare a precision and a
range (`E-INPUT-DOMAIN`) and every rating outcome to pass through an
explicit `round` in an attribute that cites the filed rounding rule
(`E-OUTCOME-ROUND`). `precision: exact` admits any finite decimal inside a
required range, for caller values that no filing gives a scale for.

A stepwise fold rounds after every step, as filings state it:
`product(self.operators as o by o.operator_number, o.factor, round_each: (4, half_up))`.
The key orders the fold and must be unique within the list that the fold
reads; admission rejects a repeated key in that list (`E-INPUT-FOLD-KEY`).

In a source that declares `rsl: "0.4"`, a selector (`find`, `argmax`,
`argmin`, `topn`) breaks a remaining tie by its list's `keyed by` key
(D-0123): numbers and dates by value, enum members by declaration order,
codes by UTF-8 bytes. A filed priority goes first,
`argmax(self.drivers as d, d.factor, then [cite: manual:p43]: d.rank)`, and
`find` returns the first match in key order, so the order of the request
never decides a rating (`E-SELECT-TIE` over an unkeyed list). A computed
attribute declared with a precision type (`Premium = Num {precision: 0.01}`)
must be proven on that grid, usually by an explicit `round`
(`E-COMPUTED-RANGE`).

`rslc.debug.migrate_numerics(path, write=True)` rewrites the
removed `round(x, 0.01)` form to
`round(x, 2, half_up)` and `round(pow(x, 1 / n), 0.01)` to
`root(x, n, 2, half_up)`. It flags, and leaves unchanged, sites that need a
decision from the filing.

## Entity input constraints

A record refinement over the record's own scalar inputs (RSL 0.4,
`R = { … } where P`; in RSL 0.3 a `requires {}` block) is an exact entity
constraint (D-0105, D-0114) when the exact plan represents it; an RSL 0.4
rule it cannot represent (`if`, a date difference, rounding) is a dynamic
refinement that only admission decides. The parser rejects the removed
`requires exact {}` spelling with a diagnostic that names the rewrite;
`rslc fmt --migrate` deletes `exact`. Every numeric input referenced by such a
constraint needs an authored or inherited grid: `precision: int`,
`precision: 1`, or a positive base-ten quantum such as `precision: 0.01`.
Numeric bounds may be absent or open. Authored endpoints are converted exactly;
each omitted side uses `±2^50` grid units at that scale. Date bounds may also be
absent or open; omitted sides use the calendar envelope `0001-01-01` through
`9999-12-31`.
The grid scale is bounded to 15 decimal places, and scaled units are bounded to
`±2^50`, so every shipped backend uses the same exact unit projection.

Large exact finite numeric domains belong in captured source data rather than
giant RSL membership literals. Declare a direct numeric alias such as
`CensusBlockGroup = Num {precision: int, values: Csv}` and provide
`enums/CensusBlockGroup.csv` with a `value` column. A scalar input whose type is
that alias implicitly carries the exact ordered membership constraint. The
compiler rejects missing, malformed, off-grid, duplicate, wrapped, indexed, or
computed uses. The CSV is captured in bundle provenance; rating never reads it.

The exact percentage form is `selected_limit <= 70% of coverage_limit`, where
`70%` is exactly `7/10`. Ordinary `Pct` semantics remain fractional, so `0.70`
means 70 percent. Exact constraints allow Boolean and closed-enum values,
dates, memberships and comparisons, addition and subtraction, static integer
multiplication, exact percentage ratios, and `and`/`or`/`not`. They reject
bare fractional factors, division, dynamic multiplication, computed
attributes, `Code` values, relations, collections, lookups, and folds. Rewrite
`0.70 * x` as `70% of x`.

## Refinements, record unions and admission (D-0114, RSL 0.4)

A source that declares `rsl: "0.4"` states every input constraint as a
refinement, `T where P [code: "…", message: "…", cite: source:region]`, and
every alternative input shape as a union of named record types. Admission
parses a `rate()` payload against these types. It is the only place where a
rating can fail: it either builds the instance graph that rating reads, or it
refuses the request with every violation it finds.

```rsl
spec { rsl: "0.4", … }

Types = {
    Score = Num {precision: int} where self in [200, 999]
        [code: "SCORE_OUT_OF_RANGE", message: "Score is outside the filed range.", cite: manual:p17]
}
Entities = {
    Policy = {
        inputs {
            term: Num {precision: int} where self in [1, 12],
            credit: ScoreAvailable | NoInsuranceScore | NotOrdered,
            drivers: List(Driver) [children]
                where len(self) in [1, 4] [code: "DRIVER_COUNT", message: "One to four drivers."]
                where unique(self as d, d.number),
            home: Home,
            garage: Option(Garage)
        },
        step rating {
            credit_factor: Num = match self.credit {
                ScoreAvailable(s) => if s.policy_adapted_credit >= 700 then 0.9 else 1.1,
                NoInsuranceScore(n) => 1.15,
                NotOrdered => 1.2
            }
        }
    } where self.term in [6, _] [code: "TERM_TOO_SHORT", message: "…", cite: manual:p4],
    ScoreAvailable = { inputs { policy_adapted_credit: Score } },
    NoInsuranceScore = { inputs { named_insured_age: Num {precision: int} where self in [16, 120] } },
    NotOrdered = {}
}
```

| Form                              | Meaning                                                                       |
| --------------------------------- | ----------------------------------------------------------------------------- |
| `x: T where P`                    | a field refinement; `self` is the field's value (an `Option`'s present value) |
| `xs: List(X) where P`             | a list refinement; `self` is the list (`len(self)`, `unique(self as x, x.k)`) |
| `R = { … } where P`               | a record refinement; `self.f` reads the record's inputs and its descendants'  |
| `Name = T where P`                | a refined type alias; every field of type `Name` inherits the clause          |
| `credit: A \| B`                  | a union of record types; the payload is `{"tag": "A", …A's fields}`           |
| `x: R`, `x: Option(R)`            | exactly one child record, at most one (`null` or absent)                      |
| `x in [a, b]`, `(a, b]`, `[a, _]` | interval membership (D-0117), also in calculations                            |

`P` is any total `Bool` expression over the refined value and its
descendants' inputs, in the calculation language: arithmetic and division,
dates (`diff_years`), rounding (`floor`, `round`), `min`/`max`, `if`,
`match` (on an `Option` child record too), folds and queries over the
value's own lists, constants and `lookup!` (D-0114). Admission evaluates it
with the calculation evaluator, so a lookup, a division or a fold in a
refinement carries the same D-0110 obligations as in a calculation
(`E-KEY-RANGE`, `E-LOOKUP-GAP`, `E-DIV-ZERO`, …), proved from the facts
admission has checked before it runs. It never reads an ancestor, a sibling
(through a `Ref`) or a calculation (`E-REFINE-UPWARD`): a rule that relates
a child to its ancestor is written on the ancestor over its children,
`Policy = { … } where all(self.drivers as d, d.points <= self.term)`. A bound
has one spelling, `self in [a, b]` (`E-REFINE-CANONICAL` teaches the rewrite
of `self >= a`). A refinement on a calculation's type is a proof obligation
(`E-COMPUTED-RANGE`), only `self in [a, b]`, with no annotation. Numeric
precision stays part of the type (`{precision: 0.01}`); a range is a
refinement. A union arm record holds inputs and refinements only; it is read
only by an exhaustive `match` that names every arm by type (`E-UNION-USE`,
no `_`).

The compiler sorts the conjuncts of each clause. Static ones (a value
interval, a number set, an enum member set, a Bool value, a list length
bound, and a record clause over the record's own scalar inputs, D-0115) are
D-0110 facts; the interval and the length bound are also JSON Schema
keywords (`minimum`, `maximum`, `minItems`, `maxItems`). Every other conjunct
is dynamic: admission checks it and the schema lists its clause under
`x-rsl-refinements` with its code and message. Admission checks every
clause before any calculation runs, so what a dynamic clause implies
(`exists(self as d, d.rated = 1)` makes the matching `filter` non-empty) is
a fact in the record's calculations too, and a union arm's clauses are
facts on that arm (D-0115). The same facts decide `match` exhaustion in a
calculation (`E-MATCH`, D-0050).

A violated clause with a code is a business violation; any business
violation makes the refusal a `BusinessRejection`, otherwise it is
`InvalidInputs`. Uncoded clauses take a code derived from the first failing
conjunct: `INPUT-RANGE`, `INPUT-ENUM` (a number set), `INPUT-LEN`,
`INPUT-UNIQUE`, `INPUT-REFINEMENT`. Shape and type errors are always
`InvalidInputs`: `INPUT-TYPE`, `INPUT-VARIANT`, `INPUT-PRECISION`,
`INPUT-ENUM`, `INPUT-PATTERN`. Both exceptions carry `violations` and
`refusal_json`, the canonical bytes that the Rust engine
(`rslc.debug.admit_debug`) also writes:

```json
{
  "error": "BusinessRejection",
  "truncated": false,
  "violations": [
    {
      "cite": null,
      "code": "DRIVER_COUNT",
      "constraint": "drivers: where len(self) in [1, 4]",
      "message": "One to four drivers.",
      "path": "Policy.drivers",
      "value": 0
    }
  ]
}
```

The order is fixed (D-0121). First the JSON shape and field types, walking
the payload in declaration order (a union's `tag` before its fields, unknown
keys after the declared ones in code-point order); an enum member, a Code
pattern and a precision grid are part of a field's type. Then refinements, in
a post-order walk of the value tree: every child value is checked before its
parent; a record's fields run in declaration order (a list's elements before
the list's clauses, a union's chosen arm with its record refinements), and
the record's own refinements run last. A value's clauses stop at the first
that fails, and a clause runs only when every value it reads passed its own
checks. A refusal reports at most 256 violations; its JSON stays under
60,000 bytes (strings in a violation keep 128 code points, a value keeps 32
nodes), so it fits the hosted worker's 64 KiB row.

A source declaring RSL 0.3 still compiles with `requires {}` and `range`
metadata (`OLDEST_READABLE_RSL`); `rslc fmt <dir> --migrate` rewrites both
(the RSL 0.4 step, pass `constraints`) and declares `rsl: "0.4"`. In an RSL
0.4 source they are `E-REQUIRES-REMOVED` and `E-RANGE-REMOVED`, and RSL 0.4
syntax in an older source is `E-RSL-SYNTAX`.

`rslc inputs sample` covers every union arm and generates one instance per
entity; rows that admission refuses are skipped. `--invalid` (with
`--representation rate`) breaks one admission form per row and records the
refusal.

## Records and maps (RSL 0.4, D-0121)

A source that declares `rsl: "0.4"` writes records instead of entities and
maps over enums instead of axes. A source that declares `"0.3"` keeps its
entities and axes and rates exactly as before.

```rsl
Types = {
    Coverage = { BI, PD, COLL, COMP },
    Liability = Coverage where self in {@Coverage.BI, @Coverage.PD},
}

Records = {
    Policy = {
        inputs { zone: Zone, dwelling: Dwelling, vehicles: List(Vehicle) }
        step totals [cite: manual:p9] {
            total: Premium = sum(self.vehicles as v, v.total),
        }
    },
    Dwelling = { inputs { cov_a: Money } },
    Vehicle = {
        inputs { symbol: Symbol }
        step rating [cite: manual:p4] {
            base[c: Coverage]: Rate = lookup!(BaseRates, Policy.zone, self.symbol).rate[c],
            ilf[c: Liability]: Factor = lookup!(Ilf, self.symbol).factor[c],
            premium[c: Coverage]: Premium =
                if c in Liability then round(self.base[c] * self.ilf[c], 2, half_up)
                else self.base[c],
            multi_car: Factor = if index(self) = 0 then 1 else 0.9,
            total: Premium = round(sum(Coverage as c, self.premium[c]) * self.multi_car, 2, half_up),
        }
    },
}
```

- A field typed `R`, `Option(R)` or `List(R)` holds records; the record types
  form one tree with one root (`E-RECORD-ROOT`), each type at one field
  position (`E-RECORD-POSITION`) and none containing itself
  (`E-RECORD-RECURSIVE`). A calculation reads the enclosing record of type
  `A` as `A.x` (`E-ANCESTOR-READ` when `A` does not enclose it).
  `index(self)` and `index(v)` give a record's position in its list, as sent.
- `drivers: List(Driver) keyed by number` makes `number` unique in the list
  (`INPUT-KEY` at each repeat). A field `principal: Ref(Driver)` or
  `Option(Ref(Driver))` on a record below the list's owner is sent as a
  driver's `number`; admission resolves it to that driver (`INPUT-REF` when
  none has it) and `self.principal.age` reads it.
- `x[c: E]` is a map over the enum `E` or a refined enum
  `Sub = E where self in {…}`; `c` holds an `E` member. A read names its key:
  `x[c]`, `x[@E.m]` or `x[self.k]`. A key outside the map's domain is
  `E-MAP-DOMAIN`, proved under the enclosing `if k in Sub` and `match`
  guards; nothing defaults to 1.0. A map-valued column is `F[E]` and is read
  at a map binder or a member. `sum(E as c, …)`, `product`, `min`, `max`,
  `avg`, `count`, `exists` and `all` fold over an enum or a subset. A
  CSV-backed enum cannot key a map (`E-MAP-DATA-SIZED`).
- `Axes`, per-element declarations, `over` folds (`E-AXES-REMOVED`),
  `Entities`, `[children]`, `[parent]` and `EntityId` (`E-RELATION-REMOVED`)
  are removed in 0.4.
- An RSL 0.4 bundle publishes `rslc.catalog/5`: `records` with each record's
  instance path (`Policy.vehicles[]`) and container, relation fields as
  `{kind: record | option | list, record}`, and map fields as
  `{key, keys}`. The nested `rate()` payload is unchanged.

`rslc fmt <dir> --migrate` runs the `records-maps` step for RSL 0.4 on a
single-file rater: `Entities` to `Records`, parent fields deleted,
`List(EntityId(R)) [children]` to `List(R)`, `self.policy.x` to `Policy.x`,
each axis to an enum named after it, static reads to member reads, bare reads
under a binder to keyed reads, `over` folds to enum folds, `auto` columns to
named columns, and per-subset declarations to one declaration with an
`if c in {…}` chain over a generated `<Calculation>Domain` refined enum. A
read that relied on two dimensions sharing element names is reported for an
agent: merge the two enums.

## Refinement types (D-0110)

The compiler proves every partial operation before a program can run, so a
runtime error on an admissible input is a compiler defect. It infers a
non-relational fact for every value (an interval over exact rationals, a
decimal grid, a small finite set, non-zero, non-empty, `Some`, enum and
axis-element sets) from input contracts, table data, arithmetic and guards
(`if`, `match`, `and`/`or`, `else reject(…)`), `requires` constraints and the
differences that comparisons spell (D-0115).
Inference is one pass per attribute body and needs no solver.

| Obligation                                       | Code               |
| ------------------------------------------------ | ------------------ |
| lookup key inside its dimension                  | `E-KEY-RANGE`      |
| divisor non-zero                                 | `E-DIV-ZERO`       |
| `min`/`max`/`avg` collection non-empty           | `E-EMPTY-FOLD`     |
| indexed read names a defined element             | `E-AXIS-INDEX`     |
| RSL 0.4 map read names a key in the map's domain | `E-MAP-DOMAIN`     |
| `topn` limit is an `Int in 0..`                  | `E-TOPN-LIMIT`     |
| `pow` exponent whole (base non-zero if negative) | `E-POW-EXPONENT`   |
| `root` degree `>= 1` (radicand `>= 0` if even)   | `E-ROOT`           |
| declared computed `range` proven                 | `E-COMPUTED-RANGE` |
| one acyclic attribute graph over all entities    | `E-CYCLE`          |
| computed band key on the cut grid (D-0123)       | `E-KEY-HOLE`       |
| selector reads a `keyed by` list (D-0123)        | `E-SELECT-TIE`     |
| declared computed precision proven (D-0123)      | `E-COMPUTED-RANGE` |

In RSL 0.3 the only escape is `checked(x, T, reject("CODE", "message"))`, a
declared business rejection that lowers to an ordinary guard in both engines.
RSL 0.4 has no escape (see "Total calculations"): the author narrows the
inputs, writes the filed clamp, or deletes the declared range. Computed
ranges are never checked at runtime. The RSL 0.3 step of `rslc fmt --migrate`
wraps an unproven declared computed range in `checked` and deletes an
`otherwise` the facts prove dead; it lists every other obligation for an
agent. The API is `rslc_core::refine::Refinements`.

## Total calculations (D-0121, RSL 0.4)

An RSL 0.4 calculation cannot reject: admission is the only place a rating
can fail (D-0114), and a business rule that refuses a request is a coded
refinement on the inputs it reads. Three forms are removed, each an error
that names its rejection census class and the rewrite:

| Code                         | Removed form                | Rewrite                                                                                                                                          |
| ---------------------------- | --------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------ |
| `E-REJECT-REMOVED`           | `reject("CODE", "message")` | input-domain rule: a refinement on the input; cross-level: a record refinement on the ancestor; computed boundary: a total construct (D-0123); … |
| `E-OTHERWISE-REJECT-REMOVED` | `otherwise: reject(…)`      | narrow the key type to the filed rows (refined or identity enum), `unfiled` cells, or the cited filed all-other row                              |
| `E-CHECKED-REMOVED`          | `checked(x, T, reject(…))`  | narrow the inputs `x` reads, write the filed clamp, or delete the declared range                                                                 |

```text
error[E-REJECT-REMOVED]: `reject("LIMIT_HIGH", …)` in `Policy.limit_factor` was removed in RSL 0.4: a calculation cannot reject. This is an input-domain rule (rejection census class A1)
  = because: RSL 0.4 calculations are total: admission is the only place a rating can fail, so a rule that refuses a request is a refinement on the inputs it reads (D-0114, D-0121)
  = help: delete the rejecting branch and state the rule as a refinement of `Policy`: `Policy = { … } where not (self.limit > 80) [code: "LIMIT_HIGH", message: "limit above 80"]` (add `cite: <source:region>` to the annotation). …
```

The forms still lower, so `rslc fmt --migrate` can analyse them, and they
keep the program's meaning, so the other checks still run beside them. No
engine runs such a program: structural verification refuses a 0.4 program
that holds a `reject` or `otherwise: reject`, and the reference evaluator
treats one as an invalid program, never as a business rejection. RSL 0.3
sources keep all three forms and rate as before.

The `rejects` pass of `rslc fmt --migrate` (the RSL 0.4 step) rewrites only
what provably changes no rated value: it deletes every site the refinement
facts over the bundle's tables prove dead (census D), and lifts `if <rule on
the record's own inputs> then reject("C", "m") else e`, reached through `if`
branches and strict operands, to `e` plus `where not (<rule>) [code: "C",
message: "m"]` (census A1, B/A4, A2). Deadness is proved in RSL 0.4 meaning:
the proof assumes no other removed form (a reject is an unknown value, a
table that keeps `otherwise: reject` has unknown outputs) and drops a
declared computed range that the facts do not prove. A lifted rule refuses
the same requests at admission, with its code among the violations; when
several rules fail, the first violation can differ from the reject RSL 0.3
reached first. Every other site stays, and the strict check lists it with
its class and rewrite. The classifier is `rslc_core::reject_sites`.

## Quality rules (D-0124)

RSL has no warnings. Every quality rule is an error that teaches its
canonical rewrite: `rslc check` prints the rule and the rewrite under the
error, and `--json` adds `because`, `help` and `applicability` (`machine`,
`placeholders` or `manual`) to the diagnostic.

The rules apply to a source that declares `rsl: "0.4"` (the version
`rslc fmt --migrate` targets). A source that declares `rsl: "0.3"` compiles
as before until it is migrated.

| Code                                              | Rule                                                                              |
| ------------------------------------------------- | --------------------------------------------------------------------------------- |
| `E-HOIST`                                         | a child's computed value that reads only ancestor data is defined on the ancestor |
| `E-ORPHAN-COMPUTED`                               | every computed attribute reaches a declared rating outcome                        |
| `E-DERIVABLE-INPUT`                               | an input that must equal a function of other inputs is computed instead           |
| `E-TABLE-UNUSED`                                  | every table and every output column is read by a lookup                           |
| `E-TABLE-UNUSED-DIM`, `E-TABLE-SINGLE-MEMBER-KEY` | every dimension changes an output                                                 |
| `E-TABLE-DUPLICATE`                               | one output column is not a copy of another table's                                |
| `E-TABLE-CONSTANT-COLUMN`                         | a column with one value is a constant                                             |
| `E-TABLE-FORMULA`                                 | a column that is `a * key + b` over 32 or more keys is a formula                  |
| `E-IF-AS-TABLE`, `E-ENUM-NUMERIC`                 | a classification of a number is a band dimension and a table                      |
| `E-PROVENANCE-COMMENT`                            | evidence lives in `[cite: …]`, not in comments                                    |
| `E-PROVENANCE`                                    | tables, constants and rounding steps cite their source, or carry `[reason: "…"]`  |

A program whose only errors are quality rules still runs every semantic
check, and `rslc check` reports its strict-check and table errors in the
same run. See D-0124 for the exact rules and the retired invariants.

## Static cost (D-0125)

`rslc check` computes the work of one `rate()` as a polynomial in list sizes,
with no solver: attribute evaluations, axis cells, table lookups and fold
iterations, where `|Policy.drivers|` is the longest such list in one
instance. It prints one line per rating outcome; `--json` reports `cost`
(the whole `rate()`, each outcome, the 20 costliest computed attributes,
and every super-linear fold), and the catalog carries each outcome's cost. Branches
cost their most expensive arm, so lookups and iterations are upper bounds;
attribute evaluations and axis cells are exact for the generated runtime when
every list of one relation has the same length.

A fold that walks one list once per element of that same list makes the
work quadratic. When the walk does not depend on the repeated element,
`E-QUADRATIC` names the rewrite: compute it once on the ancestor (or in its
own attribute) and read it. The rule applies to sources that declare
`rsl: "0.4"`; the cost report applies to every version. A walk that depends
on the repeated element (a rank) is reported in `cost.superlinear` only; a
declared list bound will discharge it once lists carry bounds. The catalog
`cost` is outside the bundle identity.

## Dimension types

A `Types` entry can declare a table key dimension (D-0107):

```rsl
Types = {
    AgeBand = IntBands(..<16, 16, 18, 25, 85..),
    AmountBand = DecimalBands(scale: 2, unit: USD; ..<100.00, 100.00, 1000.00..),
    BiLimit = IntValues(25000, 50000, 100000),
    Zip = Code(pattern: "[0-9]{5}")
}
```

A band column cell holds the band's lower cut or `..`; the key selects its
band by binary search. A value-set cell holds one listed value; the key
matches by membership. A Code cell holds one code; the key matches by exact
identity. A value-set type can type an input (admission enforces membership),
and a `Code` type can type inputs and attributes (admission enforces the
pattern; both engines run the compiler's Thompson NFA, so matching is linear).

A band dimension's number kind is the precision its bands are filed at. In a
source that declares `rsl: "0.4"`, a computed key must be on that grid: write the filed rounding,
`round(score, 0, half_up)`, in a cited step. When the filing defines the bands
over the unrounded value (interpolation segments, "up to and including x"),
declare it: `IntBands(key: unrounded; 10, 15, 20..)`. Otherwise a key between
two filed values would land in a band by the spelling alone (`E-KEY-HOLE`,
D-0123). `otherwise: reject(…)` does not cover a computed key outside the
bands: an open band or a filed `otherwise` row does.
Excel and model-JSON export reject programs that declare dimensions.

## Tables

RSL has one table form (D-0108):

```rsl
Tables = {
    DriverClass [cite: manual:p22] :
        table dims (age: AgeBand, marital: MaritalStatus) -> {
            factor: Factor[coverage]
        }
        columns: { age: "age_band" }

    ZipFactor [cite: manual:p40] :
        table dims (zip: Zip) -> { factor: Factor }
        otherwise: reject("ZIP_UNRATED", "zip is not in the filed list")
}
```

Every key cell is exact: no `_`, no ranges, no sets. Rows are unique and
their order has no meaning. `otherwise: { … }` or (RSL 0.3 only)
`otherwise: reject("CODE", "message")` covers every key tuple that no row
names; RSL 0.4 removes the rejecting form (`E-OTHERWISE-REJECT-REMOVED`).

`rslc check` runs one linear checker on every table. It packs each row into
one mixed-radix key and reports repeated keys (`E-LOOKUP-OVERLAP`). It has
no budget or cache. Entity `requires` constraints do not take part.
`E-TABLE-UNUSED-DIM` and the other table quality rules are RSL 0.4 errors
(see "Quality rules"). Runtime lookup in Rust and generated Python is the
same packed key and one hash probe.

Totality depends on the declared language (D-0120):

- **RSL 0.3** (D-0108): every tuple of the dims has a row or `otherwise`; the
  checker compares the distinct-key count with the product of the dimension
  sizes (`E-LOOKUP-GAP` on the table, with the smallest missing tuple) and
  reports an `otherwise` that covers nothing (`E-OTHERWISE-DEAD`). A `Code`
  dim needs `otherwise`, because its domain is open.
- **RSL 0.4** (`spec { rsl: "0.4", … }`, D-0122): an output cell `unfiled`
  marks a cell the filing leaves blank; a row whose outputs are all
  `unfiled` is absent (not indexed, not stored in SQLite), and a row with
  only some is `E-TABLE-COL` (split the table per output). Totality is an
  obligation of each `lookup!` call site: the key tuples the site's keys can
  take, by their inferred facts (narrowed and sibling enums, guards,
  `requires`, ranges, mapping-table outputs), must all have a filed row, or
  the table needs `otherwise` (`E-LOOKUP-GAP` at the lookup, with the
  smallest absent tuple and the rewrites). An `otherwise: reject(…)` (itself
  `E-OTHERWISE-REJECT-REMOVED`) that no call site needs is also
  `E-OTHERWISE-DEAD`. `otherwise [cite: source:region]:
{ … }` is the filed all-other row and must cite it.

`match: specific`, `match: range` with its boundary modes, `NumRange` pairs,
`[type: …]` column annotations and `_` wildcard cells are removed
(`E-TABLE-MODE`, `E-TABLE-COL`, `E-TABLE-WILDCARD`). The bundle-level
migration rewrites legacy tables and their CSVs in place:

```python
import rslc.debug
report = rslc.debug.migrate_tables("path/to/rater.rsl", write=True)
```

It reuses the D-0107 `migrate_dimensions` planner for `NumRange` pairs. It is
idempotent, and it reports each table it cannot rewrite, with a reason for an
agent. See D-0108 for the exact passes.

### No extern tables

RSL has no extern tables (D-0111). `[extern: …]`, bare `[extern]`,
`implementation:`, `path:`, `sqlite_table:` and `reject:` on a table fail
with `E-EXTERN-REMOVED`. A large identifier lookup is an ordinary table with a
`Code` key and `otherwise`, with its rows in `tables/<Name>.csv`. The compiler
checks every row at build time and stores a large table as SQLite in the
bundle; no authoring action is needed. The `externs` pass of
`rslc fmt --migrate` converts a CSV or SQLite extern. A `Text` key whose
codes have no simple pattern (`3+`, `<=50%`) becomes an enum in
`enums/<Type>.csv` whose external values are the codes.

## No Text type (D-0112)

RSL has no `Text` type. Declaring it in any position is `E-TEXT-REMOVED`: an
identifier is a `Code(pattern: "…")` type and a closed set of labels is an
enum. The `text` pass of `rslc fmt --migrate` deletes each `Text` input that
no rule or scenario reads, and each `Text` alias that nothing else names. A
`#` comment records each deleted declaration in its place. Reads come from the
elaborated program, so a name in a string or comment is not a read. The pass
lists every other `Text` for an agent. Admission is strict, so a caller that still
sends a deleted input is rejected once the migrated rater is deployed.

## Large tables in the bundle

Storage is a bundle concern, not an authoring choice (D-0111). The canonical
CSV stays the source of truth: `rslc check` checks it and the Rust evaluator
reads it. At export, a table with at least 100,000 CSV cells (data rows ×
header columns) is also written as `tables/<Name>.sqlite`, which the
generated Python reads; the bundle keeps the CSV as a source file that rating
never reads. The file is one `WITHOUT ROWID` table
keyed by the lookup key tuple (a `Code` key as its text, every other key as
its dimension coordinate), with each output as its exact CSV text. The
compiler writes the SQLite format itself, so the same source gives the same
bytes on every machine.

The manifest entry declares `format: "rslc.sqlite-table/1"`, the row count,
and the path and hash of the canonical CSV it came from. The manifest
identity check re-derives the file from that CSV. `Rater.load()` copies the
file into a private snapshot while hashing it, opens the snapshot read-only,
checks its layout and row count, and on Linux unlinks it at once. Each lookup is one
primary-key query; the generated Python needs only the standard library.
A table that the index cannot represent exactly stays CSV, and export reports
it in `csv_fallbacks` (see D-0111).

## What you have when this lands

Each claim is present-tense. A claim without a passing proof command does not
belong here.

**You have a compiler-backed language, not a grammar plus accidents.** Binding
semantics live in `docs/decisions/` (numeric model, Core IR, formula subset,
eval schedule), the Lean 4 theorems under `lean/`, and the closed Core IR ADTs
in `rslc-core`. A separate prose `docs/spec/` document is not checked in yet
(see status table). Every construct exercised by the golden corpus parses
equivalently to the recorded Lark oracle, elaborates, and evaluates — or is
rejected with a spanned diagnostic.

Proof: `pytest tests/golden/` — zero parse divergence vs. committed recorded
trees (in-repo) / `corpus/PARSE-GOLDENS.json` hashes (optional corpus);
IR / elaborator cite decision IDs. The recorded trees are frozen output of
the retired legacy Lark parser (see `tests/golden/test_parse_equivalence.py`).

**You have a compiler whose acceptance is a guarantee.** Elaborating a rater
(via the `rslc.debug` APIs `program_json` / `compile_debug`, or `rslc export`)
either fails with a
spanned diagnostic — source span, explanation, the invariant ID it violated —
or succeeds, and success _means_ something: every reference resolves, every
lookup is total, every type checks against a closed ADT that cannot represent
an illegal state, every aggregation has a pinned order, every `nl` stub is a
tracked typed hole. There is no "compiles but crashes on a real applicant."

Proof: `cargo test -p rslc-core` — every obligation has accept + reject cases;
all 4 corpus raters elaborate clean.

**You have machine-checked mathematics under the money path.** The rounding and
evaluation semantics aren't documented intentions — they're Lean 4 theorems
(determinism, totality, idempotence, monotonicity and within-one-increment
correctness for all seven rounding modes, `half_up` equal to the former
half-away rule, integer nth-root bounds, exact-semantics fold invariance) that
a proof checker verifies on every CI run, with zero `sorry`. Lean extracts the
adversarial cases (ties for every mode and sign, negative scales,
non-terminating rationals, roots) as exact conformance vectors that the Rust
kernel, the Rust evaluator and the generated Python runtime must reproduce
exactly.

Proof: `lake build` + `lean/scripts/regen_conformance.sh` (idempotent vs
`conformance/`) + `cargo test -p rslc-core conformance`.

**You have two execution paths that are checked to be the same rater.** The
Rust reference evaluator owns the semantics. One IR projects to a coupled,
zero-dependency Python artifact with explicit `Rater.load()`, exact
`rater.evaluate()`, and ergonomic nested `rater.rate()` (D-0090/D-0091); this
generated Python bundle is the production artifact. The reference evaluator and generated Python are compared on
every returned tagged value, with exact rational values. Authored business
rejections must also agree. This is bounded differential evidence, not a proof
of business correctness or complete axis-lane coverage. RSLC has no Excel
backend (D-0104).

Run `pytest tests/differential/` for the committed synthetic corpus, generated
cases with independent checkpoints, and tests of the comparison harness itself.
Every declared case must execute. Preparation errors, missing outputs, and
engine failures fail the campaign. See [compiler testing](docs/compiler-testing.md)
for private fleet runs and the precise comparison contract.

**You have the insurance domain knowledge as a living, compounding registry.**
Every one of the ~30 legacy `rsl_ast` checks has an explicit disposition
(ported / subsumed by the type system / dropped with rationale) — the dimension
analysis, the domain-coverage family, the table-extraction forensics all survive
as first-class invariants with stable citable IDs, severities, and named
profiles selectable at compile time. Adding a learned rule is a
one-registration-point, visitor-API, template-documented change with a mandatory
mutant kill — the mechanism by which the language grows as agents learn.
`rslc_core::invariants::explain` documents each `I-NNNN` for library and
compiler development use; it is not a public CLI verb.

Proof: `cargo test -p rslc-core registry_completeness` — CI fails on any legacy
check without a disposition or any invariant without a killing mutant; see
`docs/invariants.md` and `invariants::disposition::LEGACY_DISPOSITIONS`.

**You have native scenario execution.** A scenario `.rsl` (optionally
`import`ing a rater) elaborates and runs without the legacy toolkit:
instance graph bootstrap (empty `[children]` → `[]`), evaluate targets,
assertions, instance provenance, and hole-blocked attrs for mid-build agents.
CLI: `rslc eval path.rsl`; use `--partial` only for incomplete authoring
inspection.
Bundle helper: `PreparedRater(bundle_dir)`; bound invariant checks use
`PreparedRater.check_invariants()`.

`emit_python(source_path, allow_holes=False, bundle_dir=None)` is an in-place
complete-bundle export (D-0091). It loads the existing exact-case
CSVs, rejects rows wider than their headers, validates and proves D-0054
totality, then writes `rater.py` and `rater-manifest.json` beside the
source bundle, plus `tables/<Name>.sqlite` for each large table (D-0111).
CSV tables are never copied or rewritten. `bundle_dir` defaults to
the source parent. The bundle ID binds the compiled program, ordered exact
tables, root/imported RSL, and CSV-backed enum sources. `Rater.load()` checks
containment and raw hashes for every listed source and table, parses tables
once, and privately owns them; reused `rate()` / `evaluate()` calls perform no
hashing. A large table is written once as indexed SQLite and read per lookup
from a verified private snapshot (D-0111).

Proof: `rslc.run_scenario` on MGT `combined-sample-scenario.rsl` →
`_premium=11052` (legacy oracle); `pytest tests/differential/`.

**You have calibrated invariant profiles.** `build` keeps holes informational;
`verify` treats unresolved holes and bare referenced `[skip]` as Obligations
while I-16/I-4 ignore collection/`__coll_*` folds — so accepted Farmowners is
Obligation-clean under verify (D-0034).

Proof: `Registry::check(..., ProfileName::Verify)` on mgt-ca-farmowners.
Mutation replay is supplemental evidence and remains under oracle revision.

Mutation and differential runs provide supplemental evidence. Committed
reproducer and summary artifacts are historical and unavailable private corpus
rows are reported as skips; conformance remains the acceptance gate.

**You have speed that changes what's affordable.** Published benchmarks vs. the
old toolchain — compile time and batch evaluation throughput — with
order-of-magnitude wins on compile/MGT eval and no-regression batch eval
in the historical persistent-evaluation samples (D-0030); rerun benchmarks for
the current `PreparedRater.eval_batch` implementation. Exact rational
arithmetic (D-0109) costs about 1.1–1.7× per evaluated row against binary64 in
the Rust evaluator; see `docs/benchmarks.md`.

Proof: `../../.venv/bin/python tests/benchmarks/run.py --corpus corpus/` →
`tests/benchmarks/reports/benchmark-summary.json` + `docs/benchmarks.md`
(D-0029 / D-0030).

**You have a product, not a prototype.** `pip install` of the wheel from a clean
environment gives you the `rslc` CLI (`export` to python/bundle;
`--version`) and the checked Python API (`PreparedRater`,
emitters, and input/scenario helpers) on any machine with nothing else
installed — including the RSL stdlib under `rslc/std` (so `import "std/…"`
resolves without the source checkout). Raw program/table inspection hooks are
available explicitly under `rslc.debug`. Path-filtered CI jobs
cover rust / lean / wheel smoke when `effectiveai-tools/raters/rslc` changes.
Differential, mutation, and benchmarks remain local corpus-gated pytest.

Proof: fresh-venv wheel install + CLI/API smoke (the `rslc-wheel` CI job
runs exactly this), including `tests/test_bundled_std.py`.

## CLI

The public command surface is deliberately small:

```bash
rslc check path/to/rater.rsl
rslc check path/to/rater.rsl --allow-incomplete
rslc eval path/to/scenario.rsl
rslc eval path/to/scenario.rsl --partial
rslc export path/to/rater.rsl --format python
rslc export path/to/rater.rsl --format bundle --out path/to/rater.zip
rslc fmt path/to/rater.rsl
rslc fmt path/to/rater.rsl --check
rslc fmt path/to/rater.rsl --migrate
rslc inputs sample path/to/rater.rsl --n 100 --seed 7
rslc inputs validate path/to/rater.rsl input.json
```

Commands print concise human-readable output by default. Pass `--json` to emit
exactly one JSON value on stdout. Failed checks, evaluations, input validation,
and format checks return a nonzero status. `check` is strict by default;
`--allow-incomplete` only softens unresolved authoring holes.

`check` reports each diagnostic at `file:line:column` in the file that
contributed it, including imported files. In `--json` output, each located
diagnostic has a `location` object: `file`, one-based `line`, `column`,
`end_line`, and `end_column` (byte columns), and `start` and `end` (byte
offsets in that file). `span` indexes the merged import buffer, which differs
from every input file; use `location` to find the source.

## One spelling per concept

Each concept has one source spelling (D-0105). The parser rejects a removed
spelling with a diagnostic that names the canonical form:

| Removed                     | Canonical                              |
| --------------------------- | -------------------------------------- |
| `--` and `//` comments      | `#`                                    |
| `×` and `÷`                 | `*` and `/`                            |
| `Int`, `Integer`, `Decimal` | `Num`                                  |
| `Percent`                   | `Pct`                                  |
| `Str`, `String`             | `Text`, then `E-TEXT-REMOVED` (D-0112) |
| `requires exact {}`         | `requires {}`                          |
| `Option(Num {…})`           | `Option(Num) {…}`                      |

These are the `spelling` stage of `rslc fmt --migrate` (see "Migrating a
rater bundle to RSL 0.3"). The source passes live in
`rslc_core::syntax::migrate::PASSES`; each pass is independent and
idempotent, and the strict parser rejects every finding of every pass.

## Migrating a rater bundle

One command runs every migration step newer than the bundle's declared RSL
over a whole rater bundle: the entry source (`rater.rsl` or `batch.rsl`),
every local import, `tables/*.csv` and `enums/`.

```bash
rslc fmt path/to/rater-dir --migrate --json          # writes the bundle
rslc fmt path/to/rater-dir --migrate --check --json  # plans, writes nothing
```

A path to any source inside the bundle selects the same bundle. The passes
run in this order (`rslc.migrate_bundle.PASSES`); each is mechanical and
idempotent:

| Pass          | Decision | Rewrites                                                          |
| ------------- | -------- | ----------------------------------------------------------------- |
| `spelling`    | D-0105   | removed spellings (every later pass parses strictly)              |
| `numerics`    | D-0109   | `round(x, 0.01)` and `round(pow(x, 1 / n), …)`                    |
| `citations`   | D-0106   | page spellings, closed Sources, `__cite`, runtime provenance      |
| `dimensions`  | D-0107   | sentinel tails, degenerate values, `NumRange` bands               |
| `tables`      | D-0108   | `match:` tables to `table dims` with `otherwise`                  |
| `externs`     | D-0111   | CSV or SQLite extern tables to `Code`-key tables with `otherwise` |
| `text`        | D-0112   | unread `Text` inputs deleted                                      |
| `refinements` | D-0110   | unproven computed ranges to `checked`, dead `otherwise` deleted   |
| `constraints` | D-0114   | RSL 0.4: `requires` and `range` to refinements                    |
| `rejects`     | D-0121   | RSL 0.4: dead rejections deleted, input-only guards lifted        |

Then every source is formatted and the bundle is strictly checked. The run
uses a private copy of the bundle; files are copied back only when it
finishes, and never with `--check`. The JSON report holds `passes` (one
summary per pass), `files` (changed paths, relative to the bundle), `agent`,
`check_ok` and `complete`. `agent` lists every
item that still needs an agent, as
`{pass, code, file, line, column, message}`: strict-check errors located in
their source file (1-based line and character column), tables that the
`tables` pass left in a removed form with its reason, externs the `externs`
pass could not convert (or whose callers must now send a string code), and
numerics sites that need a decision. `complete` is true when `agent` is empty and the check
passes. The exit status is 1 only when the run stops (an unparsable entry) or
when `--check` finds a change.

The per-pass entry points (`rslc.debug.migrate_numerics`,
`migrate_dimensions` and `migrate_tables`) remain for debugging one pass.

## Generate input-contract cases

Use the rater's `.rsl` source file:

```bash
rslc inputs sample path/to/rater.rsl --n 100 --seed 7 --json-lines samples.jsonl
rslc inputs sample path/to/rater.rsl --n 100 --seed 7 --representation rate
rslc inputs validate path/to/rater.rsl input.json --json
```

The compiler proves that each input contract has a constructive witness.
Generation covers constraint literals, field bounds, Boolean and enum members,
and then seeded interior values. It emits exactly `n` distinct rows or a
structured `insufficient_distinct_samples` error. The same generator version,
contract hash, seed, and row index produce the same row.

Sampling does not load rating tables or execute the rater. A positive row
satisfies required Core inputs, entity graph rules, field domains, and every
top-level `requires` rule. Deliberate business rejection is a valid result for
such an input, not an input-contract failure. Optional inputs are omitted.

The default `evaluator` representation keeps named instance graphs for
`evaluate()`. The opt-in `rate` representation emits
`rslc.rate-inputs.batch/1` and `rslc.rate-inputs.row/1` envelopes whose `input`
is the nested public `Rater.rate()` payload. It nests child instances, removes
relation fields, and converts enum source names to external values. Negative
samples cannot use this representation because malformed instance graphs do
not have a lossless nested payload form.

For evaluator representation, stdout is one `rslc.inputs.batch/1` JSON object.
`--json-lines OUT` also writes only `rslc.inputs.row/1` records to `OUT`. Each
row keeps the named instance graph under `input`. `generation` records the
generator version, seed, row index, coverage target, program identity, and
contract hash. Bundle provenance uses an adjacent `rater-manifest.json` for the
bundle ID and program fingerprint when available. Sampling does not depend on
the rest of the bundle format.

Sampling always compiles the current source. `rslc export --format python`
writes `rater.py` and `rater-manifest.json` beside the source, so an edit to
the source or its tables after an export leaves them stale. Sampling ignores a
stale manifest: one that is intact but records other source, table, extern, or
Core program bytes, or a table or extern file that is gone. The program identity is then `core_ir`. Export again to record
manifest provenance. A manifest that is forged, malformed, or from an older
manifest format still fails sampling.

Validation checks any named graph without loading rating tables or running the
rater. Deliberate negative generation remains available through the Python API
for compiler testing, but is not an agent-facing CLI operation.

## Generated Python result selection

`Rater.rate(payload)` evaluates and returns declared `RatingOutcomes` at their
canonical nested paths (D-0113). `Rater.rate_detailed(payload)` runs the same
evaluation and returns every value it computed (only the read cells of an
indexed attribute) for calculation inspection. The corresponding schemas are
`output_schema` and `detailed_output_schema`. A source without outcome
declarations must use the detailed method, which then evaluates everything.
`evaluate()` returns the same trace as a flat wire map. Existing
immutable bundles need rebuilding and releasing to adopt the new default.

## Development

```bash
cargo fmt --check
cargo clippy --locked --workspace --all-targets -- -D warnings
cargo test --locked --workspace

cd lean
lake build
# optional: bash lean/scripts/regen_conformance.sh  # must be byte-identical

python -m pip install -e '.[dev]'   # or: maturin develop --release -m crates/rslc-py/Cargo.toml
pytest tests/
rslc --version
rslc check path/to/rater.rsl
rslc export path/to/rater.rsl --format python
rslc eval path/to/combined-sample-scenario.rsl
rslc eval path/to/holey.rsl --partial
```

The design contract is that the typed Core IR owns semantics. The Rust
reference evaluator and generated Python must agree bit-for-bit.

See `docs/decisions/` for binding design decisions and `docs/field-guide.md`
for durable operational notes. The production facade contract is documented
next to the facade itself in
`effectiveai-tools/src/toolkit/toolkits/rsl/facade.md`.

