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. It constructs syntax nodes directly and shares the text frontend's semantic checker and native runtime. See the Relativities example 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:

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:

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:

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 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):

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:

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.

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:

{
  "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.

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

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):

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):

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:

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 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 importing 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:

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/.

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:

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

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.