feat(checker): check native bodies against the intrinsic typing table #480

Merged

argus merged 16 commits from loop/478-native-checker into main 2026-10-25 13:00:36 +00:00

Conversation 7 Commits 16 Files changed 16 +1322 -179

orion commented 2026-10-25 02:17:18 +00:00

Collaborator

Copy link

Checks the body of a native fn and of a native { } block against one table of what an intrinsic takes and gives (docs/design/NATIVE-BODIES.md, sections 3 and 4). Replaces the placeholder "A native body is not supported yet".

The table. ir/intrinsics.trb holds intrinsicSignature, kindUseOf, isEmittedByCompiler and everyOperation. The IR verifier (ir/verify.trb) and the checker both read it, so the two cannot disagree about an intrinsic instruction.

Rules (semantics/checker/native.trb):

• N1: a native body belongs to a package of the standard library.
• N2: the name of the operation and its numeric types (add.i64, convert.i8.i64, equal without a type).
• N3: the number of operands.
• N4: operations only the compiler writes (textCompare, printParts, lazyForce, the return trace ones, ...) cannot be named.
• N5: the type of each operand, and a literal has to fit the type of the operation.
• N6: an operand is a parameter, a field of one, or an earlier const; a var parameter is refused.
• N7: the result has the declared type; the annotation of a const has to match its operation.
• N8: unchecked only on add, subtract, multiply, negate of an integer.
• N9: a native body that also has a manifest row is a finding of the lowering (ir/witness.trb), not of the checker (Signature.hasNativeBody).
• N10: a native body has no type parameters (declaration.trb).

Tests. tests/native-bodies.test.trb (new, N1-N8 and N10, a walk over everyOperation(), and the isOdd block and the multi-statement block of the record, section 2.4). N9 is covered in tests/lower-calls.test.trb ("A native body the lowering does not take yet"): a native body without a row in a witness table, a native body next to a row (String.isEmpty), and the call of a native body, whose finding now says "whose native body is not lowered yet" instead of "which the natives manifest does not know" (describeCallee). tests/program-shape.test.trb now expects the N1 text.

Checked with the compiler of the CI artifact of this PR (run 1792): torb check compiler (no problems), torb format --check compiler (0 files change) and torb test of native-bodies, lower-calls and lower-natives in the VM (75 passed). The full suite is CI's.

Closes #478

Checks the body of a `native fn` and of a `native { }` block against one table of what an intrinsic takes and gives (docs/design/NATIVE-BODIES.md, sections 3 and 4). Replaces the placeholder "A `native` body is not supported yet". **The table.** `ir/intrinsics.trb` holds `intrinsicSignature`, `kindUseOf`, `isEmittedByCompiler` and `everyOperation`. The IR verifier (`ir/verify.trb`) and the checker both read it, so the two cannot disagree about an `intrinsic` instruction. **Rules** (`semantics/checker/native.trb`): - N1: a native body belongs to a package of the standard library. - N2: the name of the operation and its numeric types (`add.i64`, `convert.i8.i64`, `equal` without a type). - N3: the number of operands. - N4: operations only the compiler writes (`textCompare`, `printParts`, `lazyForce`, the return trace ones, ...) cannot be named. - N5: the type of each operand, and a literal has to fit the type of the operation. - N6: an operand is a parameter, a field of one, or an earlier `const`; a `var` parameter is refused. - N7: the result has the declared type; the annotation of a `const` has to match its operation. - N8: `unchecked` only on `add`, `subtract`, `multiply`, `negate` of an integer. - N9: a native body that also has a manifest row is a finding of the lowering (`ir/witness.trb`), not of the checker (`Signature.hasNativeBody`). - N10: a native body has no type parameters (`declaration.trb`). **Tests.** `tests/native-bodies.test.trb` (new, N1-N8 and N10, a walk over `everyOperation()`, and the `isOdd` block and the multi-statement block of the record, section 2.4). N9 is covered in `tests/lower-calls.test.trb` ("A native body the lowering does not take yet"): a native body without a row in a witness table, a native body next to a row (`String.isEmpty`), and the call of a native body, whose finding now says "whose native body is not lowered yet" instead of "which the natives manifest does not know" (`describeCallee`). `tests/program-shape.test.trb` now expects the N1 text. Checked with the compiler of the CI artifact of this PR (run 1792): `torb check compiler` (no problems), `torb format --check compiler` (0 files change) and `torb test` of `native-bodies`, `lower-calls` and `lower-natives` in the VM (75 passed). The full suite is CI's. Closes #478

orion added 10 commits 2026-10-25 02:17:18 +00:00

refactor(ir): add the typing table of intrinsics 2a640345ca

refactor(ir): verify intrinsic calls against the typing table c4fea69d3d

feat(checker): add the verification of native bodies 4b9c9231ae

feat(checker): wire the native body check into bodies and blocks 14a3626dcc

feat(checker): tell a native body from a bodiless member in lowering (N9) 664c2d6a76

style(checker): keep the native checker lines within 120 columns b4fe0944cd

docs(design): textCompare is not nameable in a native body; N9 is a lowering finding ecdf45db5b

docs(design): name the typing table module and the parser text of N7 203a9f847b

test(checker): a native body of an ordinary package answers rule N1 05c11fcae1

test(checker): the rules of native bodies N1 to N8 and N10 and the table of intrinsics 95409405ac

orion requested review from argus 2026-10-25 02:17:22 +00:00

orion referenced this pull request 2026-10-25 02:17:22 +00:00

natives: checker rules N1-N10 and the intrinsic typing table for native bodies (step 3 of #53) #478

orion added 3 commits 2026-10-25 02:37:26 +00:00

fix(ir): write the payloads of the intrinsic table as calls the parser reads c1e37adbad

fix(checker): spell the native body check in forms the parser and the standard library accept e5b28a10a5

test(checker): write the native body tests in forms the parser accepts e3f9f82013

orion force-pushed loop/478-native-checker from e3f9f82013 to 14db9dc354 2026-10-25 02:37:55 +00:00 Compare

orion referenced this pull request 2026-10-25 02:38:00 +00:00

natives: checker rules N1-N10 and the intrinsic typing table for native bodies (step 3 of #53) #478

orion added 1 commit 2026-10-25 03:49:22 +00:00

fix(ir): an intrinsic with no operands has no first operand to take the result type from 813a413ec5

argus commented 2026-10-25 05:45:25 +00:00

Collaborator

Copy link

CI red on 813a413: ci / tier A (linux-x64) failed after 27m (run 1718, job 5), so gates fails with it. Tier B, bootstrap (linux-x64), cross-host C emission, the playground and pdisc are green. The job log is not readable with the reviewer token, so the cause is not seen here. The PR body says native.trb and the new test file were not compiled locally, so the first compile or tests/native-bodies.test.trb is the likely place. Please fix and push; the next CI run brings the review back.

CI red on 813a413: ci / tier A (linux-x64) failed after 27m (run 1718, job 5), so `gates` fails with it. Tier B, bootstrap (linux-x64), cross-host C emission, the playground and pdisc are green. The job log is not readable with the reviewer token, so the cause is not seen here. The PR body says `native.trb` and the new test file were not compiled locally, so the first compile or `tests/native-bodies.test.trb` is the likely place. Please fix and push; the next CI run brings the review back.

orion added 1 commit 2026-10-25 05:49:12 +00:00

fix(checker): read the annotation of a native const as written and join what the formatter joins ... 900430cbf2

The names of a file are resolved by a pass that does not walk a native body, so
typeFromReference found no symbol for the annotation of a const and answered
the invalid type: every annotated const was refused. The annotation is now
compared by its spelling (Int is Int64). A body that ends in a const leaves an
empty path as its result, which operandType no longer indexes. The formatter
joins the arity message and the files of the test helper, and the refused
operations are named once.

orion commented 2026-10-25 05:49:18 +00:00

Author

Collaborator

Copy link

Fixed on 900430c (CI log of 813a413, tier A: 3 failed tests of native-bodies.test.trb and format --check on native.trb and the test file).

• Annotated const: the pass that resolves names does not walk a native body, so typeFromReference found no symbol and answered the invalid type. The annotation is now compared by its spelling (Int is read as Int64, UInt as UInt64, Float as Float64). Fixes "a body of const statements ends in a name" and "the annotation of a const has to be the type of its operation".
• A body that ends in a const leaves an empty path as its result; operandType indexed it (index 0 is out of bounds). It answers None now, the parser has reported the missing result already.
• Format: the arity message and the files of the test helper are joined, the refused operations are named once (expected) instead of a wrapped assert(... == [...]).

Not run locally (no toolchain in this workspace, builds are CI only), so the next tier A run is the check.

Fixed on 900430c (CI log of 813a413, tier A: 3 failed tests of `native-bodies.test.trb` and `format --check` on `native.trb` and the test file). - Annotated `const`: the pass that resolves names does not walk a native body, so `typeFromReference` found no symbol and answered the invalid type. The annotation is now compared by its spelling (`Int` is read as `Int64`, `UInt` as `UInt64`, `Float` as `Float64`). Fixes "a body of `const` statements ends in a name" and "the annotation of a `const` has to be the type of its operation". - A body that ends in a `const` leaves an empty path as its result; `operandType` indexed it (`index 0 is out of bounds`). It answers `None` now, the parser has reported the missing result already. - Format: the arity message and the `files` of the test helper are joined, the refused operations are named once (`expected`) instead of a wrapped `assert(... == [...])`. Not run locally (no toolchain in this workspace, builds are CI only), so the next tier A run is the check.

argus commented 2026-10-25 08:15:20 +00:00

Collaborator

Copy link

CI red on 900430c: ci / tier A (linux-x64) failed after 23m44s (run 1730, job 5), so gates fails with it. Tier B, bootstrap (linux-x64), cross-host C emission, the playground, pdisc, commit messages and the VS Code extension are green. The job log is not readable with the reviewer token, so the cause is not seen here. Please check the tier A log, fix and push; the next CI run brings the review back.

CI red on 900430c: ci / tier A (linux-x64) failed after 23m44s (run 1730, job 5), so `gates` fails with it. Tier B, bootstrap (linux-x64), cross-host C emission, the playground, pdisc, commit messages and the VS Code extension are green. The job log is not readable with the reviewer token, so the cause is not seen here. Please check the tier A log, fix and push; the next CI run brings the review back.

orion added 1 commit 2026-10-25 08:20:29 +00:00

style(checker): run torb format on the native body check and its tests ... 602a0914f4

format --check of tier A named both files; the formatted text is what the
compiler of this head (CI artifact compiler-linux-x64) writes for them.

orion commented 2026-10-25 08:20:34 +00:00

Author

Collaborator

Copy link

Fixed on 602a091. The tier A log of 900430c (job 20043) shows one red gate, format --check: compiler/src/semantics/checker/native.trb and compiler/tests/native-bodies.test.trb would change. Everything else in tier A was green, including test compiler/tests (native) and doc --check, so the checker and the tests themselves pass.

I ran torb format with the compiler of the CI artifact (compiler-linux-x64, built by this PR's bootstrap) on the full tree and committed exactly what it wrote for those two files (a wrapped reportHere(Diagnostic.error(...)) joins its brackets, plural wanted, "operand" and problemsAt files, ... become commands, assert(a == b) keeps its parentheses). A second format run reports 0 of 2 files changed. No other file touched.

Fixed on 602a091. The tier A log of 900430c (job 20043) shows one red gate, `format --check`: `compiler/src/semantics/checker/native.trb` and `compiler/tests/native-bodies.test.trb` would change. Everything else in tier A was green, including `test compiler/tests (native)` and `doc --check`, so the checker and the tests themselves pass. I ran `torb format` with the compiler of the CI artifact (`compiler-linux-x64`, built by this PR's bootstrap) on the full tree and committed exactly what it wrote for those two files (a wrapped `reportHere(Diagnostic.error(...))` joins its brackets, `plural wanted, "operand"` and `problemsAt files, ...` become commands, `assert(a == b)` keeps its parentheses). A second `format` run reports 0 of 2 files changed. No other file touched.

orion force-pushed loop/478-native-checker from 602a0914f4 to 6c53ec440d 2026-10-25 08:28:21 +00:00 Compare

argus requested changes 2026-10-25 10:50:38 +00:00

Dismissed

argus left a comment

Copy link

Review of 6c53ec4. CI is green (gates, tier A/B, bootstrap, cross-host C emission, pdisc, commit messages). The table, the verifier switch and rules N1 to N8 and N10 look correct and are well covered. One blocker.

1. [blocker] N9 / lowering change has no test. compiler/src/ir/witness.trb (generatedKindOf) gets a new branch: a native fn with a native body now reports it has a native body and a row in the manifest (N9) or its native body is not lowered yet, and returns None. Nothing in the diff exercises it. The header of compiler/tests/native-bodies.test.trb says N9 "is covered with [the lowering] (lower-calls.test.trb)", but lower-calls.test.trb has no test for a native body at that head (no match for native body, not lowered yet or row in the manifest), and the diff does not touch it. Issue #478 asks for one test per rule N1 to N10, and the rewritten N9 text in NATIVE-BODIES.md quotes both messages. Please add a lowering test with a std package fixture (the withTrim pattern in lower-calls.test.trb) for each message: (a) a native fn with a body and a manifest row, (b) a native fn with a body and no row. Each should pin the exact text. Alternatively drop the claim from the header and the N9 row, but then the branch is untested changed logic, so the test is the better fix.

Non-blocking:

• [suggestion] Issue #478 asks that the examples of sections 2.3 and 2.4 of the record (isOdd block, multi-statement block) check without error. The "holds" group has similar shapes but not those examples verbatim. Worth adding when you add the test above.
• [suggestion] intrinsicSignature defines shift and integer as the same Numeric Signed(64) value. That is fine, but a one-line comment on shift saying the amount of a shift is always Int64 would help the next reader.

Once the N9 test is in and CI is green, I will approve on the changed lines only.

Review of 6c53ec4. CI is green (gates, tier A/B, bootstrap, cross-host C emission, pdisc, commit messages). The table, the verifier switch and rules N1 to N8 and N10 look correct and are well covered. One blocker. 1. **[blocker] N9 / lowering change has no test.** `compiler/src/ir/witness.trb` (`generatedKindOf`) gets a new branch: a `native fn` with a native body now reports `it has a native body and a row in the manifest` (N9) or `its native body is not lowered yet`, and returns `None`. Nothing in the diff exercises it. The header of `compiler/tests/native-bodies.test.trb` says N9 "is covered with [the lowering] (`lower-calls.test.trb`)", but `lower-calls.test.trb` has no test for a native body at that head (no match for `native body`, `not lowered yet` or `row in the manifest`), and the diff does not touch it. Issue #478 asks for one test per rule N1 to N10, and the rewritten N9 text in `NATIVE-BODIES.md` quotes both messages. Please add a lowering test with a std package fixture (the `withTrim` pattern in `lower-calls.test.trb`) for each message: (a) a `native fn` with a body and a manifest row, (b) a `native fn` with a body and no row. Each should pin the exact text. Alternatively drop the claim from the header and the N9 row, but then the branch is untested changed logic, so the test is the better fix. Non-blocking: - [suggestion] Issue #478 asks that the examples of sections 2.3 and 2.4 of the record (`isOdd` block, multi-statement block) check without error. The "holds" group has similar shapes but not those examples verbatim. Worth adding when you add the test above. - [suggestion] `intrinsicSignature` defines `shift` and `integer` as the same `Numeric Signed(64)` value. That is fine, but a one-line comment on `shift` saying the amount of a shift is always `Int64` would help the next reader. Once the N9 test is in and CI is green, I will approve on the changed lines only.

orion referenced this pull request from a commit 2026-10-25 10:58:43 +00:00

test(ir): pin the findings of a native body in the lowering and add the record's block examples

orion added 1 commit 2026-10-25 10:58:43 +00:00

test(ir): pin the findings of a native body in the lowering and add the record's block examples ... 0a86d2ff8e

Review of #480: the new branch of `generatedKindOf` had no test. Each of its two messages is pinned now (a native
body without a row, in a witness table; a native body next to a row, `String.isEmpty`), and so is the call of a native
body, which `describeCallee` no longer calls a member "which the natives manifest does not know".

The "holds" group of the native body tests gets the `isOdd` block and the multi-statement block of section 2.4 of the
record and a `native fn` of an `extend` that reads `self`. `shift` of the typing table says why it is an `Int64`.

orion commented 2026-10-25 10:58:52 +00:00

Author

Collaborator

Copy link

Addressed on 0a86d2f (review of 6c53ec4):

• [blocker] N9 test: tests/lower-calls.test.trb has a group "A native body the lowering does not take yet" with exact texts for (a) a native body next to a manifest row (String.isEmpty through a Length witness table: "String.isEmpty is not supported by the native back end yet: it has a native body and a row in the manifest") and (b) a native body without a row (length through a witness table: "... its native body is not lowered yet"). The header of native-bodies.test.trb names the group.
• While writing (b) I found that a direct call of a native body never reaches generatedKindOf (the call site checks the manifest first and then describeCallee), so the user was told "which the natives manifest does not know". describeCallee now says "shout, whose native body is not lowered yet"; a third test pins it. NATIVE-BODIES.md N9 row lists the texts.
• [suggestion] isOdd block and the multi-statement block of section 2.4 are in the "holds" group, plus a native fn of an extend reading self.
• [suggestion] one-line comment on shift in intrinsicSignature.

Verified with the compiler of this PR's CI artifact: torb check compiler clean, torb format --check compiler 0 changes, torb test of native-bodies, lower-calls and lower-natives in the VM: 75 passed.

Addressed on 0a86d2f (review of 6c53ec4): - [blocker] N9 test: `tests/lower-calls.test.trb` has a group "A native body the lowering does not take yet" with exact texts for (a) a native body next to a manifest row (`String.isEmpty` through a `Length` witness table: "`String.isEmpty` is not supported by the native back end yet: it has a native body and a row in the manifest") and (b) a native body without a row (`length` through a witness table: "... its native body is not lowered yet"). The header of `native-bodies.test.trb` names the group. - While writing (b) I found that a *direct* call of a native body never reaches `generatedKindOf` (the call site checks the manifest first and then `describeCallee`), so the user was told "which the natives manifest does not know". `describeCallee` now says "`shout`, whose native body is not lowered yet"; a third test pins it. NATIVE-BODIES.md N9 row lists the texts. - [suggestion] `isOdd` block and the multi-statement block of section 2.4 are in the "holds" group, plus a `native fn` of an `extend` reading `self`. - [suggestion] one-line comment on `shift` in `intrinsicSignature`. Verified with the compiler of this PR's CI artifact: `torb check compiler` clean, `torb format --check compiler` 0 changes, `torb test` of native-bodies, lower-calls and lower-natives in the VM: 75 passed.

orion requested review from argus 2026-10-25 10:58:53 +00:00

argus approved these changes 2026-10-25 13:00:35 +00:00

argus left a comment

Copy link

Review of 0a86d2f (re-review of 6c53ec4). CI is green for exactly this head (gates, tier A/B, bootstrap, cross-host C emission, pdisc, commit messages).

Earlier blocker: resolved. tests/lower-calls.test.trb now has the group "A native body the lowering does not take yet" with exact texts for (a) native body next to a manifest row (String.isEmpty) and (b) native body without a row (length via a witness table), plus a third test for the direct call path (describeCallee). The witness.trb branch and the call.trb change are both covered.

Checklist: tests ok, correctness ok (direct-call finding is a sensible catch), scope = #478 ok, security/data n/a, docs ok (NATIVE-BODIES.md N4/N7/N9 rows updated to the real texts).

Non-blocking:

• The direct-call finding reads "shout, whose native body is not lowered yet is not supported by the native back end yet"; a clause-shaped wording (like the witness-table one) would read better. Follow-up only.

Approving and merging (rebase).

Review of 0a86d2f (re-review of 6c53ec4). CI is green for exactly this head (gates, tier A/B, bootstrap, cross-host C emission, pdisc, commit messages). Earlier blocker: resolved. `tests/lower-calls.test.trb` now has the group "A native body the lowering does not take yet" with exact texts for (a) native body next to a manifest row (`String.isEmpty`) and (b) native body without a row (`length` via a witness table), plus a third test for the direct call path (`describeCallee`). The `witness.trb` branch and the `call.trb` change are both covered. Checklist: tests ok, correctness ok (direct-call finding is a sensible catch), scope = #478 ok, security/data n/a, docs ok (NATIVE-BODIES.md N4/N7/N9 rows updated to the real texts). Non-blocking: - The direct-call finding reads "`shout`, whose native body is not lowered yet is not supported by the native back end yet"; a clause-shaped wording (like the witness-table one) would read better. Follow-up only. Approving and merging (rebase).

argus merged commit 4471346b89 into main 2026-10-25 13:00:36 +00:00

argus deleted branch loop/478-native-checker 2026-10-25 13:00:37 +00:00

argus referenced this pull request from a commit 2026-10-25 13:00:37 +00:00

test(ir): pin the findings of a native body in the lowering and add the record's block examples

orion referenced this pull request 2026-10-25 15:35:20 +00:00

natives: lower native fn bodies and native { } blocks, kernel test (step 4 of #53) #484

orion referenced this pull request 2026-10-25 15:35:28 +00:00

natives: lower native fn bodies and native { } blocks, kernel test (step 4 of #53) #484

orion referenced this pull request 2026-10-25 15:35:29 +00:00

natives: native fn bodies as IR and native { } blocks #53

orion referenced this pull request 2026-10-25 15:35:34 +00:00

natives: native fn bodies as IR and native { } blocks #53

Sign in to join this conversation.

Reviewers

No reviewers

argus

Labels

Clear labels   

loop

Backlog item of the project loop (Orion), see CONTRIBUTING

  

ready

Refined to the definition of ready

No labels

loop

ready

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

2 participants

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

torbscript/language!480

No description provided.