[SamMausberg]

Summary

Every documentation page now says only what its code, tests or records under evidence/ support. About eighty sentences across the docs, CONTRIBUTING.md, SECURITY.md and the example, tool, benchmark and demo READMEs claimed more than that: a proof where there is a Lean model or a test, "never" or "every" where a test covers some cases, a speedup with no record, a count that has drifted, or a rule the code does not have. Each now states the claim at the strength its evidence carries, and names that evidence. Prose is otherwise unchanged; the voice pass comes in later pull requests, one page or two at a time.

Motivation

The design report's documentation findings named five claims beyond their evidence: a failed guard stopping a program inside a GPU kernel (devices.md, internals.md, numerics.md), "every candidate the checker accepts is correct" (tools.md) and "an accepted plan needs no test to be correct" (agents.md) for a plan rule with no Lean model, language.md's "leaving a guard out never changes what a program does", examples.md's 10x and 85x with no record, and concurrency.md's "proved in Lean" for a device store that Lean does not cover. It asked for the rest to be found. Five read-only audits went through every page against the compiler, the runtime, the tests and evidence/, and every finding below was checked again before it was changed. The owner asked for this directly; no roadmap issue covers it.

Changes

• docs (language, memory, abstractions, library): the claims listed under Evidence, plus modelled spelled modeled as the repository mostly spells it (110 to 19), and one definition of a guard used on every page that defines one ("a check the compiler writes before an operation that could fail at run time"), with "traps" and "aborts" used one way.
• docs (concurrency, devices, numerics): the guard path on a GPU, plans, device compact, the lane pool, the tensor-core tests' real tolerance, and the GH200 runs where a sentence said a thing ran once or only on the RTX 5070 Ti.
• docs (tools, agents, internals, verification, examples, guide, index): the claims under Evidence; the capability matrix data (docs/project/capability_matrix.json) for one count, regenerated by tools/release/capability_matrix.py.
• README.md: one count, "two parallel regions" to three, in the Compute Sanitizer sentence. Nothing else in the README changes.
• CONTRIBUTING.md: the seven things AGENTS.md requires of a language change, where it listed two; the GPU rule as AGENTS.md now states it; what make native and make lean do and do not do; auto-merge set by the author.
• SECURITY.md: GitHub's private vulnerability reporting is not turned on for this repository (gh api repos/SamMausberg/cairn/private-vulnerability-reporting gives {"enabled":false}), so the page no longer offers it.
• examples/README.md, tools/README.md, bench//README.md, demos//README.md: the claims under Evidence.
• std (src/cairn/std/draw.cairn, sort.cairn): two module comments, which make docs turns into docs/std/draw.md and docs/std/sort.md. The code is unchanged.

Behaviour and compatibility

none: documentation and two comments. No program is accepted, refused, emitted or printed differently. One heading is renamed, the guide's "9. Lanes are race free by construction" to "9. Lanes cannot race"; nothing linked to it, and test_tour.py finds its twelve programs.

Testing

On this branch merged with main at 4d495bf, on the aarch64 GH200 host, with no device run:

make lint                      # ruff format, ruff check, mypy (165 files), cairn fmt: clean
python -m pytest -q -n 4 tests/language/test_docs_examples.py tests/language/test_tour.py \
  tests/tooling/test_repository.py tests/tooling/test_documented_names.py tests/tooling/test_capability_matrix.py \
  tests/language/test_std_api.py tests/tooling/test_tools.py        # 378 passed

Before the merge the same branch ran the tests that read any page it changes: those above plus test_std, test_projects, test_wordfreq, test_layouts, test_expressiveness, test_review_agent_and_device_layer, test_review_tools, test_ai_bench, test_ai_eval, test_std_system, test_focused, test_release, test_language and test_github_files: 838 passed, 1 skipped. The findings were checked with cairn check, cairn validate, cairn emit, cairn run and demos/repair/run.py on this host; the programs are in the session's scratch directory. The fast suite was not run, since no code changed.

Evidence and claims

Withdrawn or narrowed, each with what backs the new wording:

• A failed guard in a GPU kernel (devices.md "One wait, or none", internals.md "Safety and trust", numerics.md's emulation table, language.md's definition): the trap, the poisoned context and the abort at the next wait are how the runtime is built. The suite tests that path under --emulate, no test that makes a guard fail on a GPU has run since 0.8.3 (both recorded sessions skipped the three trap tests), and the one guard that failed on the GH200 was in a kernel NVVM 7.0.1 miscompiled (evidence/v1_2/gpu_gh200). The README's wording is followed. devices.md's region paragraph no longer says the process has "already aborted" when a region returns, which held runs contradict.
• Plans (tools.md, agents.md, concurrency.md): the plan rules are made so that a plan changes no result the language fixes; atomic updates follow the order lanes arrive in, which a plan can change. The suite tests planned regions against the regions as written, host plans on the host and device plans on an RTX 5070 Ti and a GH200; a fused device chain is compiled and has not run on a GPU; no Lean model covers the rules. A plan's use g selects an implementation, which could change a result, so tune takes one only once validated.
• Elided guards (language.md): a guard is left out where the checker's facts show it cannot fail, and where they are true leaving it out changes nothing. Lean proves the decision for a model of the rule; the facts' truth at each site rests on the hand-written audit and on differential runs. A local a pending defer names cannot move before the deferred call runs #167 closed the hole that made the old sentence false.
• Device compact (concurrency.md): the seventeen certificates are about the host loop; the device store at the exclusive sum of the flags has no certificate and is tested.
• Speed without a record (examples.md simulator, analytics, gpu_pipeline, the host engine's 1.2 s; tools.md's incremental build times): kept as one run's printout, labelled as having no record. The 10x and 85x are gone.
• Counts and numbers: tools.md's --generics record (172 and 84 functions are now 190 and 102), the expression-visit limit (3,200,000, E-AST-LIMIT; agents.md had 200000), the device-perf timing ranges (466 to 591 us, not 550; 338 to 348 us through cq_, against 334 to 340 us), the profile's median errors in place of "within a quarter", the Compute Sanitizer program's three regions (README and matrix), size's 5411 bytes labelled as the v0.8.0 record's, the trust table's 15,500 compiler lines plus the verifier modules it imports and a row for the build driver.
• Proofs named as tests or models: Layout.lean's spread (a model, with the compiler's evaluation tested), the lane pool's protocol (a sequentially consistent model), the lease checkers (Lean for the model, samples for places.py), a borrow's lifetime (a fragment), storage floats (the model comparison runs without sanitizers; nothing on a GPU), the math builtins' bits (clang++ and g++ tested; no device run), the tensor-core device tests (twice the bound against the reference loop, not the bound of the exact sum; the matmul app checks the bound).
• Rules the code does not have: cairn check --generics certifies a template whose instance can still be E-EFFECT-ORDER (a trait member without a ceiling on both sides of an operator); a const folds in exact arithmetic, so 0 - 1 + 1 is a u8 0; a linear record is not copyable; std.draw can trap on i64 overflow; a map Slot from another map is only a number; std.sys is not the only module that binds C symbols; the operand-order gap keep(total(c), c) (internals.md) is now named where memory.md and "Safety and trust" said there was none.
• Stale after merges: the device make targets are no longer the owner's alone (Agents may run device code on a GPU that drives no display, through the device make targets and their lock #162), cairn verify's native replay runs only where it can and otherwise leaves Z3's verdict (cairn verify keeps each path's storage for an owner the paths move, and runs every smt-equivalent verdict natively before giving it #179), the search could not reuse a check (An edit of one function's body is checked from the walk the last check kept, and a differential test holds it to a whole check #101, An edited body's check puts back the instances, layouts and implementations the walk made first there, so an edit that makes them again is not checked whole #114), the device examples and the numeric demo ran again on a GH200 (evidence/v1_2/gpu_gh200 records the suite's device tests on a GH200, and README and the capability matrix say what ran there #172), and CONTRIBUTING's GPU and language-change rules match AGENTS.md.
• Benchmark and demo READMEs: bench/gpu compares after timing and records a mismatch, bench/device records relative_error and refuses nothing, paired.py and codegen_only.py write results/native/ themselves, the suite's extra arms are listed, the repair demo's clamp fails only when hi < lo and x < lo, the implement demo's float case shrinks to n = 2048, and each demo says what its test checks.

No claim is added beyond its record.

Not changed here, for the pull requests that own them: the capability matrix's device rows and the devices.md and numerics.md sentences that name only the RTX 5070 Ti where the GH200 also ran them, which the device-record work is updating; and roadmap.md, which a later pull request brings up to date.

Found and not fixed, since they are code: E-AST-LIMIT's message and the limits rule card still say 200000 (checking.py:671, teaching.py:86); cairn check --generics misses the operand-order case above.

Performance

none

Checklist

• The title is one plain sentence saying what is now true; it becomes the squash commit's subject
• Every behaviour added has a test, and every new refusal a rejection test naming its code (no behaviour is added)
• The documentation is updated in the file that owns the subject, and its examples compile
• Generated files are current (make editors, make docs): make docs regenerated docs/std/draw.md, docs/std/sort.md and the capability matrix
• A language change carries everything AGENTS.md lists: not a language change
• No emojis, no attribution trailers, nothing unrelated to the change

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-28T19:38:35.074597Z	ccd6d9b	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ccd6d9b130

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Invoke the certificate exporter through Python

When a contributor follows this workflow after changing a Lean-modeled rule, running tools/checks/export_lean_certificates.py directly fails with Permission denied because the script is committed with mode 100644. Since make lean invokes it only with --check, that target cannot perform the required regeneration either; document python3 tools/checks/export_lean_certificates.py or make the script executable.

AGENTS.md reference: AGENTS.md:L126-L126

Useful? React with 👍 / 👎.