Repository navigation
The checker records trait evidence; the debug VM checks each method call against it - #153
Merged
Merged
Conversation
For every trait predicate a use owes, the checker now notes what solved it: the impl of the trait for the type's head with the evidence of what the impl's header asks; a bound of an enclosing definition, by a where clause or taken into its scheme (reached through supertraits as steps from the bound); the type's structure; or an impl the runtime provides for a builtin type (the Error of a builtin module's error enum). When the module's types are final it writes the evidence (crate::evidence) on the AST: Expr::ev on each use of a definition with bounds and on each call through a trait, and TraitImpl::supers, the evidence that an impl's type has its trait's supertraits, from the impl's header. A bound is named by the span of its definition's body (or a let's value), the way the compiler names the function it compiles, so the evidence of a body names exactly the definition it is in. Nothing changes for someone writing silt: dispatch is as before. The walk over an expression's children is one helper now (resolve::each_child_mut), which each_expr_mut and the evidence pass share.
The compiler keeps the evidence, in a debug build only, in a side table of each function (FnEvidence: the definition it is, how it numbers its bounds, and the evidence each instruction passes on, by the offset past it), and Globals keep each impl's supertrait evidence. No instruction changes: disassembly and every output are as before. The debug VM follows the evidence beside the values as dictionaries would be passed (vm::evidence): a closure carries the evidence its body sees (VmClosure::ev), a load of a definition with bounds binds the level of its bounds, a closure made in a body sees the body's, a method the VM finds gets the level its call gives it. At each CallMethod it checks that the impl it found is the one the evidence names (or none, for structural evidence; the type's registry row, for an impl the runtime provides; for a written Error impl that leaves message out, the builtin trait's default the VM supplies); where a call through a trait is compiled, that the selected impl is the evidence's. A disagreement is a type_confusion error, which fails a golden case and is a finding of the oracle; SILT_EVIDENCE=report writes disagreements to stderr and goes on, and SILT_EVIDENCE=report=<file> appends them and a line for each call checked to the file. Evidence the VM cannot work out is not checked. The run loop changes by one line at GetGlobal, GetLocal, GetUpvalue and MakeClosure, and call_method by two. VmClosure has a constructor, VmClosure::new. Release builds keep and check nothing.
rendro
added this pull request to stack #154
October 24, 2026 05:11
An impl's method may restate in its `where` a bound the trait declares
for the method or the impl's header asks, or a supertrait of one. Its
body numbered its bounds as it is checked with them: the header's, the
trait's, then the restated ones, then (for the impl for every tuple or
function) the trait of `self`. A call passes the evidence of the
header's and the trait's only, so a restated bound, or `self`'s trait
after one, named a bound the call never passed: a valid program
stopped in a debug build ("evidence: the call of 'greet' in 'Int.both'
... the checker named Impl"), or the call went unchecked.
One layout now, the header's predicates, then the bounds the trait
declares for the method, then `self`'s trait: the body's bounds
(method_body_bounds) and what every use of the method passes on
(method_site, for a call through the trait on a known type and for
`Type.method`). A restated bound is the declared or header bound it
restates, or a supertrait step from one.
Golden cases: a bound restated as a supertrait of the declared one, as
a supertrait of a header bound, and the impls for every tuple and every
function restating the declared bound; each fails in a debug build
before this change.
…'s where clauses - Polymorphic recursion (each call at a deeper type, Box of Box of ...) copied the evidence tree at every call in a debug build: quadratic in time and memory (n=3000: 4.0 s and 316 MB, base 0.08 s; n=10000 ran out of 2 GB). The evidence of an impl's header is shared now (Arc<[Ground]>): passing it on costs the same at any depth (n=10000: 0.14 s, 44 MB). - A default method that uses a `where` clause the trait declares on its parameter (`trait Pr(a) where a: Greet`, `Greet.greet(Pr.item(self))`) had no evidence for it. The clause is a bound of the default, after its own; each impl records the evidence that its trait arguments meet the clauses (ImplEvidence::wheres, beside the supertraits), and a call of the default passes it on. - The check's message names the types and traits (from the impls the program compiles and the builtin types), not their ids. - With SILT_EVIDENCE=report, a call in a body the runtime runs (a Display impl run by println, a json.Encode impl run by json.stringify), which no call of silt's passed evidence to, is counted apart: unchecked-by-runtime. - A comment at the hooks of the run loop names the instructions that load a callable and so need one. Golden cases: polymorphic recursion 10,000 deep, and a default method using a trait parameter's where clause (its evidence locked by a unit test: it was missing before, not failing).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Lane E, PR 2 of 2 (wave 2). Stacked on #148. No visible change.
The first stage of compile-time trait resolution. The checker now records evidence for every trait predicate it solves. In debug builds the VM checks that each method call is answered by the impl that evidence names. Dispatch is unchanged.
Impl(trait, head, trait args, [evidence for the header's predicates]);Param(i): the i-th bound of the enclosing function or impl;Super(evidence, path);Structural(trait);Native(trait, type): an impl the runtime provides for a builtin type.wherethe trait declares on its parameter, for default methods), then self's trait for an impl for every tuple or function. A bound an impl's method restates is the bound it restates, or a supertrait step from it; it gets no entry of its own. Each impl records the evidence that its trait arguments meet the trait'swhereclauses and supertraits.silt checktime unchanged (0.22–0.26 s on a 3,000-function bounded file), memory about +1%. The compiler copies the evidence into a per-function side table in debug builds only;Instr,FunctionandVmClosureare unchanged in release, and the disassembly is unchanged. An impl's header evidence is shared, so passing it on is O(1) per call (polymorphic recursion 10,000 levels deep: 0.14 s, 44 MB in debug).run.rs: a load hook shared by GetGlobal, GetLocal and GetUpvalue, MakeClosure, andcall_method. A comment there lists the instructions that load a callable and so need a hook.SILT_EVIDENCE=reportlists disagreements instead, for sweeps.Sweep, distinct call sites:
Unchecked, counted and never failing:
println,json.Encodebyjson.stringify,json.Decodebyjson.parseand postgres rows (0 in goldens and oracle; the class exists);The static check compares two checker outputs (the select pass and the evidence); it does not check the runtime receiver. That waits for stage 3, where dictionaries make the static path the dynamic one.
Disagreement classes the sweep and verification found, all fixed here, none a soundness hole:
Erroron builtin error enums is answered by the runtime's registry row, so it is nowNativeevidence.Error.messageleft out of a written impl is answered by the default the VM supplies. It is accepted only in exactly that case.Golden cases (lang/traits/), each failing, missing or out of memory before this PR:
evidence__a_restated_bound_is_a_supertrait_of_the_declared_oneevidence__a_restated_bound_is_a_supertrait_of_a_header_boundevidence__an_impl_for_every_tuple_or_function_restates_a_boundevidence__polymorphic_recursion_at_ever_deeper_typesevidence__a_default_method_uses_a_where_clause_on_a_trait_parameterTests: 6 checker unit tests and 4 VM check tests. The whole suite passes with the check failing on any disagreement, 2619/2619, plus doc tests; clippy (debug and release profile, with and without all features), fmt, rustdoc, no-default-features check.