Static Checking
Here is a script with two mistakes in it (a typo and a type error):
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 errorstatic 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.
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);Cannot assign string to 'range' (declared int)
3Both 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
// 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/biteEvery 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:
// 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.
| target | accepts | notes |
|---|---|---|
int | int, float (truncates), bool, an object with to_int() | string/char/null/containers = error |
float | float, int, bool, an object with to_float() | |
bool | anything | truthy conversion |
string | anything | to_string conversion; objects use their own to_string() when they define one |
char | char, an object with to_char() | char c = 65 is an error at load and at run time; cast<char>(65) is the spelling |
array / map | array / map | the 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 C | null (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 src | an 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 subclass | null stores a typed null on every path; an unrelated class or a primitive is an error |
function | a callable or null | a number, string or container is an error |
| references | compatible storage only | see References |
var | anything, forever | the opt-out. A var-typed expression makes everything downstream unknown, and unknown never errors |
auto + initializer | inferred, then enforced as that type | a null initializer leaves it dynamic. Null carries no type; the runtime locks at the first non-null store |
auto without initializer | dynamic (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= rhsbehaves asx = T(x op rhs), soint x; x += 2.5is fine (it truncates) andx += "s"is an error.vartargets keep their dynamic result. - Typed fields are real, statics included. Field initializers, member stores
(
obj.field = v, a barefield = vinside a method, inherited fields) and static stores on every spelling (C::s, a baresinside the class, the compound forms) all check against the declared type, and the runtime enforces the same table on the same spellings.
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'11What 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).
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 warningstatic 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:
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"));10
caught in half: Cannot return string from 'half' (declared -> int)
-1Identifiers
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:
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; }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++:
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'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.
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);20
19
19The finer rules, each the same on both backends:
- Accessors. A member that a user
_get_x/_set_xdeclares (anywhere in the chain) is known, and takes the accessor's declared type when that declaration is unambiguous: one parameterless, non-coroutineint _get_hp()makeschar c = obj.hpan error; one by-valuevoid _set_hp(int)makesobj.hp = "s"the errorcannot assign 'string' to property 'hp' declared 'int'. Two overloads, avar/autogetter, 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 barexkeeps 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::xnames the global. - Statics are typed like instance fields on every spelling (
C::s, a baresinside the class, the compound forms). - Enum values are checked for existence:
Direction.zzzisno value 'zzz' in enum 'Direction'. - Lenient by design: builtin container/string/map methods, subscripts, namespaces at every
depth, and the handle builtins a
shared_ptranswers (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:
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);1
2The 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):
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:
import "rules.jai"; // rules.jai reads G, which state.jai declares
import "state.jai"; // order does not matter: names cross units
print(damage(3));int damage(int hits) { return hits * G.power; }class World { int power = 7; }
World G = World();21A 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:
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):
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); }'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:
// 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:
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);Cannot assign string to 'x' (declared int)
6A 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:
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);Cannot assign string to 'x' (declared int)
Cannot assign array to 'x' (declared int)
7A 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:
[[warn_mode]]; // first declaration of the file: the whole unit is warn
int x = 5;
try { x = "s"; } catch (e) { print(e); }
print(x);Cannot assign string to 'x' (declared int)
5Inside 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 design | why |
|---|---|
var anywhere, and everything computed from it; auto without an initializer; a null initializer | no 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 properties | no 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 depth | such 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 inlast_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).externfor 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.