Static Checking​

Here is a script with two mistakes in it (a typo and a type error):

jaiscript · tower.jai
class Tower { int range = 3; }
Tower t = Tower();
t.rnage = 5;                      // a typo, caught before anything runs
int shots = "many";               // typed to typed: also a load error
output
static check failed:
<script>:3:3: error: no member 'rnage' in class 'Tower' (declared at 1:7)
    t.rnage = 5;                      // a typo, caught before anything runs
      ^
<script>:4:5: error: cannot initialize 'shots' declared 'int' with 'string'
    int shots = "many";               // typed to typed: also a load error
        ^

Nothing ran. execute() threw jai::static_check_error before the first statement, and what() listed every error in the file, compiler style, with the line and a caret. That is what every engine does out of the box: the checker is strict unless you say otherwise.

The checker is a backend-neutral pass over the AST. It runs once per unique source, at the moment the parse is cached, and that one hook covers execute(string), jaibite creation and load, hot-reload re-parses and registration changes alike. There is no second door to forget. Its contract fits in a sentence: a mismatch between two declared types is a load error; only a value that arrived through var can still fail at run time, where try/catch sees it.

jaiscript · var_runtime.jai
int range = 3;
var fromJson = "5";               // var: the checker cannot know what this holds
try {
    range = fromJson;             // loads fine; the runtime enforces the slot
} catch (e) {
    print(e);
}
print(range);
output
Cannot assign string to 'range' (declared int)
3

Both halves use the same conversion table (below), so a value the checker admits is a value the runtime converts. If you are coming from the type ladder chapter: int is enforced, auto infers then enforces, var is the opt-out. The checker simply moves the enforcement of the first two to load time wherever it can see both sides.

Check API​

C++
// compiled and run against the library
jai::check_report r = eng->check(source);                     // parse (cached) + check, without running
const jai::check_report& d = eng->last_check_diagnostics();   // the last checked execute/bite

Every load is checked. Any error-severity diagnostic makes execute(), jaibite() and jaibite_load*() throw jai::static_check_error before anything runs. A strongly-typed to strongly-typed mismatch (int x = "s", returning a string from a function declared -> int, passing an array to an int parameter, an unrelated class into a typed slot) is a load error; only a var-sourced value can still fail at run time. A region marked [[warn_mode]] reports its errors as warnings, so it loads and the runtime's own conversion errors apply unchanged there.

A small host that hands a three-line source (a bad assignment on line 2, an undeclared name on line 3) to check(), then runs a variant whose unit is a warn region, then runs the source itself:

C++
// compiled and run against the library
std::string src = "int x = 5;\nx = \"hello\";\nint y = missing + 1;\n";
jai::check_report r = eng->check(src);
std::cout << "diagnostics: " << r.diagnostics.size() << "\n";
for (const jai::check_diagnostic& d : r.diagnostics)
    std::cout << "  " << d.line << ":" << d.column << " " << d.message << "\n";

auto v = eng->execute("[[warn_mode]]; int x = 5;\nif (false) { x = \"hello\"; }\n42").as_int();
std::cout << "warn region ran: " << v << " with " << eng->last_check_diagnostics().diagnostics.size()
          << " warning(s) on record\n";

try { eng->execute(src); }
catch (const jai::static_check_error& e) { std::cout << "load refused:\n" << e.what() << "\n"; }
std::cout << "clean load: " << eng->execute("2 + 2").as_int() << "\n";

Output:

diagnostics: 2
  2:4 cannot assign 'string' to 'x' declared 'int'
  3:9 use of undeclared identifier 'missing'
warn region ran: 42 with 1 warning(s) on record
load refused:
static check failed:
<script>:2:4: error: cannot assign 'string' to 'x' declared 'int' (declared at 1:5)
    x = "hello";
       ^
<script>:3:9: error: use of undeclared identifier 'missing'
    int y = missing + 1;
            ^

clean load: 4

(The warn-region demo puts the bad assignment in an if (false) branch. The checker is flow-insensitive, so it still reports it, as a warning; the runtime never reaches it.)

A check_diagnostic carries severity, line, column, message, related_line/related_column (the declaration a bad store violates). A check_report holds the vector plus capped (the 100-diagnostic cap was hit), has_errors(), error_count() and format(source, name), which renders the listing above. Errors gate the load; warning severity never gates. The shadowing warnings described in the classes chapter are the everyday example.

One conversion table​

One table, run at load by the checker and at run time by every typed slot: declarations, assignment, by-value parameters, returns, instance and static field stores, and the container element boundary.

targetacceptsnotes
intint, float (truncates), bool, an object with to_int()string/char/null/containers = error
floatfloat, int, bool, an object with to_float()
boolanythingtruthy conversion
stringanythingto_string conversion; objects use their own to_string() when they define one
charchar, an object with to_char()char c = 65 is an error at load and at run time; cast<char>(65) is the spelling
array / maparray / mapthe checker rejects a literal element, a push or an element store it can see (cannot push into 'array<int>': expected 'int', got 'string'); map keys, var-sourced values and untyped containers meet the runtime element boundary, which runs on every path: an element store says Cannot assign 'string' to element of type 'int', a push Cannot push 'string' to array<int>, a whole container or literal Cannot store string in array<int>, a map key Cannot use 'int' as a key of type 'string'
object Cnull (a typed null); the same class; derived to base; a shared_ptr<C or derived> handle; a converting constructor C(src) through exactly one one-parameter constructor that takes src directly; on plain assignment, a user operator= of C (or an in-script base) that accepts srcan unrelated class with no viable one-argument constructor or operator= = error; array/map/function into an object = error; a registered ancestor's operator= is lenient
shared_ptr<C> / weak_ptr<C>null, a handle or an instance of C or a subclassnull stores a typed null on every path; an unrelated class or a primitive is an error
functiona callable or nulla number, string or container is an error
referencescompatible storage onlysee References
varanything, foreverthe opt-out. A var-typed expression makes everything downstream unknown, and unknown never errors
auto + initializerinferred, then enforced as that typea null initializer leaves it dynamic. Null carries no type; the runtime locks at the first non-null store
auto without initializerdynamic (unchecked)the runtime locks at the first store; the checker cannot see branch order, so it opts out

Two things the table does not do. It never chains: TA -> TB -> TC or x.to_int() -> C(int) is not implicit. And it never hides a thrown conversion: a converting constructor or to_X() that throws surfaces its own error. Each run-time rejection names its slot: Cannot initialize 'x' (declared int) with string for declarations, Cannot assign string to 'x' (declared int) for =, Cannot assign string to field 'f' of C (declared int) and ... to static 's' of C ... for fields, Cannot pass string to parameter 'n' of 'fib' (declared int), Cannot return string from 'f' (declared -> int), Cannot convert S to C (no suitable single-argument constructor) for a class-target parameter or return. The type spelled is the value's own (string, null, array, a class name), never a var tag.

Two rules worth calling out:

  • Compound assignment follows C++. A typed x op= rhs behaves as x = T(x op rhs), so int x; x += 2.5 is fine (it truncates) and x += "s" is an error. var targets keep their dynamic result.
  • Typed fields are real, statics included. Field initializers, member stores (obj.field = v, a bare field = v inside a method, inherited fields) and static stores on every spelling (C::s, a bare s inside the class, the compound forms) all check against the declared type, and the runtime enforces the same table on the same spellings.
jaiscript · statics.jai
class Counter {
    static int total = 0;
    void bump() { total += 1; }
}
Counter c = Counter();
c.bump();
Counter::total += 10;
print(Counter::total);
// Counter::total = "many";   -> error: cannot assign 'string' to field 'total' declared 'int'
output
11

What gets checked​

Calls​

A call is checked when the callee resolves statically. Same-script functions, constructors and methods get arity (defaults counted) plus per-argument assignability through the table above. A string parameter therefore accepts anything. Overloads error only when no overload matches. A reference parameter binds only compatible storage (References).

Host (C++) functions are checked through engine::host_function_signatures: arity across overloads (variadic accepts anything) and only per-argument certainties: a known primitive with no builtin conversion to a primitive parameter, like square("s"). Numeric to numeric is fine; object and script_value parameters accept anything. One boundary difference to remember: the C++ side has no numeric-to-string conversion, unlike a script string slot. Callables held in variables (lambdas, cross-execute function values) are unchecked. A bound static method (Gate::twice()) is held to the arity of its binding; a second static_method of the same name replaces the first, and a binding of unknown arity accepts anything.

Returns​

A returned value must be assignable to the declared return type; a value from a void function is an error; a bare return; or a path that falls off the end is an error when the result holds no null (a primitive, a string, a reference) and a warning for a class, handle or container result. The walk runs at load and adds nothing to a call. Coroutines are exempt (calling one yields a handle typed as coroutine_handle; yield and return types are not checked).

jaiscript · required_returns.jai
class Box { int v = 1; }
int sign(int a) { if (a > 0) { return 1; } }    // falls off the end
int none() { return; }                           // bare return from an int function
Box maybe(int a) { if (a > 0) { return Box(); } }  // a class result may be null: a warning
output
static check failed:
<script>:2:5: error: 'sign' declared to return 'int' may reach the end of its body without returning
    int sign(int a) { if (a > 0) { return 1; } }    // falls off the end
        ^
<script>:3:14: error: 'none' declared to return 'int' returns no value here (declared at 3:5)
    int none() { return; }                           // bare return from an int function
                 ^
<script>:4:5: warning: 'maybe' declared to return 'Box' may reach the end of its body without returning (returns null)
    Box maybe(int a) { if (a > 0) { return Box(); } }  // a class result may be null: a warning
        ^

The listing carries every diagnostic, warnings included: the errors fail the load and the warning for maybe rides along. last_check_diagnostics() holds the same entries. In a [[warn_mode]] region such a function loads and runs as written.

The run-time half matters when the value came through var: the conversion is part of the return statement itself, C++ style. A try around the return inside the callee catches the failure, and when nothing catches it the callee is the top frame of the stack trace with the call site below it:

jaiscript · return_site.jai
int half(var v) {
    try {
        return v;                 // the conversion happens here, inside half
    } catch (e) {
        print("caught in half: " + e);
        return -1;
    }
}
print(half(10));
print(half("ten"));
output
10
caught in half: Cannot return string from 'half' (declared -> int)
-1

Identifiers​

An undeclared identifier is an error. A name counts as declared if it is in scope, a member of the current class (inherited included; inside a method or a [this] lambda, also a member of a class derived from it), a program-scope declaration of the unit (top level or a namespace body, two-pass, so a function reads a global declared below it), one of the host's per-call instance variables, a top-level name of any unit in the program (Programs), an extern declaration (escape hatches), or anything on the engine's registration surface (globals, functions, classes, template types, namespaces), which is visible because checking happens at execute time. A local, parameter or loop variable is declared only in its own scope, and a field or method only to its class: print(hp) at the top level is undeclared even when a class declares hp.

Only a unit that uses a dynamic-path import(expr)/include(expr) drops undeclared identifiers to warning severity: such a file can define anything. A literal import path never hides a name, wherever the import stands (a function body or a block included): its module joins the program instead.

References​

A reference binds compatible storage and never converts: the exact primitive kind (an int& takes an int, not a float), the class or a subclass, the same concrete container or handle type. The checker holds parameters, reference declarations, reference range-for variables and reference returns to that rule; an argument whose element type it cannot know stays lenient, and the runtime makes the same verdict there:

jaiscript · references.jai
void bump(int& r) { r += 1; }
float speed = 1.5;
bump(speed);                      // an int& never binds a float
array<int> ids = [1, 2];
for (float& v : ids) { v = 0; }
output
static check failed:
<script>:3:11: error: argument 1 of 'bump': cannot bind 'float' to 'r' declared 'int&' (declared at 1:6)
    bump(speed);                      // an int& never binds a float
              ^
<script>:5:1: error: cannot bind 'int' to 'v' declared 'float&'
    for (float& v : ids) { v = 0; }
    ^

A store through a reference runs the referenced variable's own table at run time (int& r = x; r = "s" raises like x = "s"); the checker leaves those stores to the runtime.

Members​

On a receiver whose class is fully known (an in-script hierarchy the checker can resolve, or an engine-registered class with its properties and statics), an unknown field or method is an error, on reads and on writes (the runtime raises the same mistake at the store, Cannot assign to 'x': A has no such member). A member that only a subtype declares is an error on a receiver whose static class is certain, exactly as in C++:

jaiscript · subtype_member.jai
class Unit { int hp = 10; }
class Archer : Unit { int arrows = 20; }

shared_ptr<Unit> u = new Archer();
print(u.arrows);                  // error: Unit has no 'arrows'
output
static check failed:
<script>:5:9: error: no member 'arrows' in class 'Unit' (declared at 1:7)
    print(u.arrows);                  // error: Unit has no 'arrows'
            ^

The two fixes are the two you would reach for in C++: a cast, or a receiver that opts out of typing.

jaiscript · subtype_member_fixed.jai
class Unit { int hp = 10; }
class Archer : Unit { int arrows = 20; }

shared_ptr<Unit> u = new Archer();
print(cast<Archer&>(u).arrows);   // the spelled fix: a reference, no copy
cast<Archer&>(u).arrows = 19;
print(cast<shared_ptr<Archer>>(u).arrows);
var any = u;                      // or opt the receiver out entirely
print(any.arrows);
output
20
19
19

The finer rules, each the same on both backends:

  • Accessors. A member that a user _get_x/_set_x declares (anywhere in the chain) is known, and takes the accessor's declared type when that declaration is unambiguous: one parameterless, non-coroutine int _get_hp() makes char c = obj.hp an error; one by-value void _set_hp(int) makes obj.hp = "s" the error cannot assign 'string' to property 'hp' declared 'int'. Two overloads, a var/auto getter, a getter with parameters, a reference or untyped setter parameter, or an accessor that lives only on a registered ancestor all leave the member unknown: lenient. Inside the class a bare x keeps the backing field's declared type, a global of the same name included: a bare name in a method resolves locals, then members, then globals, the order the run time takes, so the member is checked and ::x names the global.
  • Statics are typed like instance fields on every spelling (C::s, a bare s inside the class, the compound forms).
  • Enum values are checked for existence: Direction.zzz is no value 'zzz' in enum 'Direction'.
  • Lenient by design: builtin container/string/map methods, subscripts, namespaces at every depth, and the handle builtins a shared_ptr answers (use_count, cpp_ref_count, unique, same_as, reset). A class method of the same name wins first. Any ancestor the checker cannot resolve opens the whole class: silence.

Casts​

cast<T>(e) types as a certain T; cast<T&>(e) as T for member lookup only (it is a reference, never a store proof); cast<shared_ptr<T>>(e) as the handle. Primitive targets type as the primitive. The operand is the explicit typed boundary and is never checked against T. The verdict belongs to the runtime, whose Cannot cast 'X' to 'T' is catchable. A T that names no class is an error (unknown type in cast: 'Nope').

One warning lives here, because it catches a real slip. A value-form class cast of a handle or a reference copies the instance, and that is rarely what you meant:

jaiscript · cast_copy.jai
class P { int t = 1; }
shared_ptr<P> h = new P();
P copy = cast<P>(h);              // warning: this copies
copy.t = 2;
print(h.t);
print(copy.t);
output
1
2

The warning never gates. The script runs under strict and prints 1 then 2, which is the copy doing exactly what a copy does. The diagnostic waits in last_check_diagnostics() (the runner prints it under --warnings):

diagnostic
cast_copy.jai:3:10: warning: cast<P>(h) copies the instance - use cast<P&>(h) to alias it or cast<shared_ptr<P>>(h) to share it (declared at 2:15)
    P copy = cast<P>(h);              // warning: this copies
             ^

cast<T&>, cast<shared_ptr<T>>, primitive targets and var operands stay silent. The cast itself is covered in the type ladder.

Namespaces, and recovery​

math::<fn>(...) is typed by its kernel's result (int for itrunc/ifloor/wrap_*, float for the transcendental and interpolation families, operand-typed for math::abs/math::min/math::max/math::clamp); arity there is the kernel's run-time error. A user namespace path a::b::c is lenient at every depth.

An erroring expression assumes its declared or expected type afterwards, so one bad line produces one diagnostic rather than a cascade; identical (line, column, message) triples are deduplicated; the listing caps at 100 with report.capped set.

Programs: checking across imports​

A game is rarely one file. Here rules.jai reads a global that state.jai declares, and the entry point imports them in the "wrong" order:

jaiscript · main.jai
import "rules.jai";               // rules.jai reads G, which state.jai declares
import "state.jai";               // order does not matter: names cross units
print(damage(3));
jaiscript · rules.jai
int damage(int hits) { return hits * G.power; }
jaiscript · state.jai
class World { int power = 7; }
World G = World();
output
21

A unit whose import/include statements carry literal paths (at any depth) is the root of a program. Before anything runs, the engine gathers the program's closure: every unit those paths reach, resolved exactly as the runtime resolves them (the importing file's folder, then the include paths, then the working directory), recursively, each file once (cycles are fine). It then hands the union of every unit's top-level names to the checker: functions, variables, classes, enums and their values, namespaces and their members. The root and every closure unit are then checked against that union, so a function in one file may use a global or class another file declares, whatever the import order.

Class models cross units too. Every top-level class of every unit is modeled as if it were declared in the unit being checked, so a subclass whose parent lives in another file resolves inherited fields and methods bare, through this, and on typed receivers (down a chain that may end in a registered C++ class), and a typed mismatch against a cross-unit member is the same error the same-unit case reports. A parent found nowhere (a dynamic-path import, an extern name used as a base) opens its subclass: bare names in that class's methods type as unknown and are never undeclared.

Under strict, an error anywhere in the program fails the root's execute() before any unit runs. what() lists the root's diagnostics first, then each erroring unit's own listing, formatted against that unit's source and named by its resolved path. Drop state.jai from the program above and you get:

output
static check failed:
.../rules.jai:1:38: error: use of undeclared identifier 'G'
    int damage(int hits) { return hits * G.power; }
                                         ^

The automatic disk cache gives the same answer: a leaf's checked-clean stamp holds only where the names it resolved outside itself mean what they meant when it was checked, so the program without state.jai checks rules.jai again even after the full program cached it (see jaibite, "The stamp holds for the context the file was checked in").

In the report eng->check() and last_check_diagnostics() return, closure diagnostics follow the root's with line and column 0 and the path-qualified location leading the message (the snippet belongs to another source, so none is printed).

The union is the engine's program-name memory: it lives for the engine's lifetime and rides every later check, so a leaf re-parsed on its own after a hot edit still knows the names of the program it belongs to. The memory is a superset by construction: a name it admits is never a false error, only a typo the checker cannot catch. A unit the closure cannot resolve, read or parse contributes no names and is skipped; the runtime reports it when the unit executes. Names the program never declares (a host global bound after load, a value injected at run time) are outside the closure by definition, which is what extern is for.

Escape hatches​

Two spellings tell the checker about what it cannot see, or should not gate on, without loosening anything else.

extern​

extern declares a name that exists outside the program (a host global bound after load, a function the running instance registers, a value injected at run time):

jaiscript · externs.jai
class Game { int hp = 100; }
extern function spawn_on_network;  // a callable of unknown signature: calls are unchecked
extern shared_ptr<Game> G;         // typed: G.hp is checked against Game
extern config;                     // untyped: var, reads and stores are dynamic

int report() { return G.hp; }      // checks; runs only if the host bound G
try { spawn_on_network(1, 2); } catch (e) { print(e); }
try { print(report()); } catch (e) { print(e); }
output
'spawn_on_network' is declared extern but never defined
'G' is declared extern but never defined (an 'inline' declaration creates it)

An extern name counts as declared, and a program's closure carries it to every unit like any top-level name. The typed form gives the name that certain type: member checks, assignment checks and proofs flow exactly as for a declared variable (G.mana above would be the load error no member 'mana' in class 'Game'). At run time an extern declares nothing: the name resolves when it is used (a declaration in any unit, the host's add_global or a host function defines it), and a use while nothing defines it raises the catchable text the output shows: nobody bound G or spawn_on_network in that run. inline T name; (the C++17 inline variable) is the spelling that creates the variable when no unit has: one variable shared by every unit that declares it, the first to run creating it with its initializer or its type's default. It is also the right spelling for a shared leaf that calls into a module only some programs import: the leaf declares the names it reaches for, and in a program that imports the module too the declaration is inert.

From the host, defining an extern is the ordinary registration, made before or after the script loads:

C++
// compiled and run against the library
eng->execute("extern int G; print(G + 1);");
// throws jai::script_exception: "'G' is declared extern but never defined (an 'inline' declaration creates it)"
eng->add_global("G", eng->make_value(int64_t{41}));
eng->execute("extern int G; print(G + 1);");                  // 42
eng->add_function("spawn_wave", [](jai::script_int n) { return n * 2; });
eng->execute("extern function spawn_wave; print(spawn_wave(3));");   // 6

[[warn_mode]] and [[strict_mode]]​

These set the checker's mode for a region of one unit. They compose and innermost wins; outside every region the unit is strict. An attribute leads one of three positions.

One statement. Before any statement (top level, in a function or lambda body, in a loop body, in a bare block), it covers that statement's own subtree, then the mode reverts:

jaiscript · warn_statement.jai
int x = 5;
try {
    x = 6;                        // checked as usual
    [[warn_mode]] x = "s";        // this one statement is lenient: loads, raises at run time
} catch (e) {
    print(e);
}
print(x);
output
Cannot assign string to 'x' (declared int)
6

A nested function or lambda body is a new scope that keeps the enclosing mode: [[warn_mode]] self.spawn_on_network([](){ x = 5; }); accepts self, the member and the call, but x = 5 inside the lambda is still checked.

A whole block. As the first statement of a block (a function, method or lambda body, an if/while/for body, a bare { }), it covers the whole block, nested bodies included:

jaiscript · warn_block.jai
int x = 5;
{
    [[warn_mode]]                 // first statement of a block: the whole block is lenient
    try { x = "s"; } catch (e) { print(e); }
    try { x = [1, 2]; } catch (e) { print(e); }
    x = 7;
}
print(x);
output
Cannot assign string to 'x' (declared int)
Cannot assign array to 'x' (declared int)
7

A whole unit. As the first declaration of a file (a leading comment is fine, the trailing ; optional) it sets the unit's mode. The checker still runs there, but reports every error it finds as a warning:

jaiscript · legacy.jai
[[warn_mode]];                    // first declaration of the file: the whole unit is warn
int x = 5;
try { x = "s"; } catch (e) { print(e); }
print(x);
output
Cannot assign string to 'x' (declared int)
5

Inside a warn region every error-severity diagnostic is reported as a warning (still collected, still in last_check_diagnostics() and eng->check()), and an undeclared identifier is accepted as unknown: an undeclared callee is assumed callable with an unknown result, so nothing downstream is proven from it. [[strict_mode]] inside a warn region re-arms strict there: its errors gate the load.

The runtime never changes: both backends treat an attribute as nothing, and a warn region's type mistakes raise at run time exactly as they would without the checker. Every output above is the runtime's ordinary error. A unit's mode says nothing about the units it imports, and a [[warn_mode]] leaf never fails its program. warn_mode and strict_mode are the only attribute names; [[bogus]] is a parse error, and [[ in expression position still opens a nested array literal.

What still fails at run time (the precision map)​

Everywhere the static story is uncertain, the checker goes silent by design. This is the whole list; a mistake in any of these spots is a run-time error, never a load error:

lenient by designwhy
var anywhere, and everything computed from it; auto without an initializer; a null initializerno declared type to check against; auto locks at a store the checker cannot order
stores through a reference (T& declarations, auto& loop variables, by-reference parameters)the referenced variable's table runs at run time; binding the reference and member lookup through it are still checked
container elements the checker cannot type: map keys, elements of untyped containers and var receivers, subscripts, builtin container/string method results (literal elements, pushes and element stores into a declared array<T> or map<K,V> are checked)the runtime element boundary is the check
engine globals (typed off the value tag; a later retag is invisible), host-object conversions, callables held in variables, host functions beyond arity and primitive certainties, binder (C++) methods reached through a script chain, binder propertiesno static signature in view
dynamic-path import(expr)/include(expr) units (undeclared identifiers drop to warnings), untyped extern names, a parent found nowhere, namespaces at every depthsuch a unit or name can define anything
accessor-bearing members whose declaration is ambiguous (two getter/setter overloads, var/auto/coroutine/parameterized getters, reference or untyped setter parameters, an accessor on a registered-only ancestor)no single declaration to trust
coroutines: yield and return types, and what a handle's next() returns (the handle itself is typed: next and done are its only members)the checker does not model what a coroutine yields
mixed-branch ternaries, this/super as values, hot-reload redefinitions (receivers that carry the old shape are open), extended classes and everything passed to extend(...)the shape is decided at run time

For proofs (below) the lenient set is wider still: every row here, cross-unit classes until their unit has run, and every accessor-bearing member, typed or not.

The false-positive contract​

A program that runs clean and does not genuinely violate declared types must produce zero error diagnostics. The precision map above is the implementation of that promise: wherever the checker cannot be certain, it says nothing. The promise is enforced mechanically: a standing gate feeds the checker 200 differential-fuzzer-generated programs, and any program that executes cleanly must check clean.

This is what makes strict-by-default livable on a real codebase: the checker can only reject scripts that were already broken.

Proofs: the same walk, put to work​

The walk that produces diagnostics also stamps proofs on the AST: annotations saying "the conversion this store, argument or return would run is the identity", and the static class of a binary's operands. The VM's compiler reads them to choose its typed lowerings and what it may inline; every lane they select keeps a total runtime guard, and a guard miss runs the ordinary code byte for byte. Certainty is the complement of the precision map, so the false-positive contract doubles as the proof-soundness contract.

What that means for you: nothing. There is no program whose value, printed output, error text or type_of differs between engine::type_proofs(true) (the default) and type_proofs(false); toggling it off strips cached stamps at their next execute. engine::last_proof_stats() counts the stamps of the most recent pass for tests. Proofs are never serialized into a bite (a loaded bite re-derives them), and a hot reload that changes a class's shape re-stamps the entries that read it at their next execute (Hot Reload).

jaibite stamping​

A bite is checked at creation: an error makes jaibite() throw there, exactly like execute(), and the report rides the bite (bite.checked_clean(), bite.check_diagnostics()). save() stamps a checked-clean bit in the header; on load the stamp is trusted only when the registration fingerprint matches the saving engine's, otherwise the bite is re-checked against the loading engine's surface (an error throws at load). A bite is checked once. Registrations after that do not re-trigger; re-create the bite to re-check. Proofs are independent of the stamp: they re-derive at creation, load and execute. Details in the jaibite chapter.

Cost​

One AST walk per unique source per registration epoch, cached beside the parse; the proof pass rides it. The walk re-runs only when the registration surface moves (add_function/add_global/add_class/register_template_type, a script class's first definition or a non-identical redefinition) or the proof switch flips. Executes with per-call host instance variables check fresh per call, without touching the cached stamps. Walk cost is parse-order: the same tree, no allocation-heavy state. A .jaibite cache stamped checked-clean skips the diagnostics walk on load. New source text (a hot reload) is a new cache entry and a fresh check.

Migrating a loosely typed codebase​

Every load is strict; a codebase mid-migration opts down, at the narrowest scope that still lets it load:

  • [[warn_mode]]; at the top of each legacy file while you port. Its diagnostics keep accumulating in last_check_diagnostics() as warnings, so the to-do list writes itself.
  • [[warn_mode]] before one statement or block for the handful of lines that read a field the checker cannot see. A migration hook reading a removed field is the classic case (Hot Reload).
  • extern for the names your host injects at run time; the typed form keeps them checked.

Re-arm with [[strict_mode]] inside a warn region as files come clean, and drop the attribute when the file is clean. eng->check(src) is the batch entry point. A build step can walk every script and fail on has_errors() without executing anything; it throws jai::parse_error only when the source does not parse. Prototype scripts that live on var are never flagged, so the ladder stays incremental: declare a type where you want enforcement, and the checker follows the declaration.