feat: @safe-gated verified resource checking + n-ary/global session runtimes#127
Merged
Conversation
…] fns
Wires the machine-checked QTT core (my_qtt::check, the faithful R5 port) into
the compiler's default check path — closing the docs/STATUS.adoc "make the
resource axis the default in checker.rs" item.
`Checker::check_function` now, for every function annotated `#[safe]`, models
it as `|params| body` and runs `qtt_bridge::check_expr` (→ verified
`my_qtt::check`). A parameter dropped or used more than once WITHIN the
resource-relevant fragment is reported as `CheckError::ResourceViolation`; a
body using constructs outside that fragment (arithmetic, records, AI exprs,
calls to globals, `return`) cannot be lowered and is skipped — unverifiable is
not unsafe. Runs by default (no flag); gated on `#[safe]` so the rest of the
language (which is not linear-by-default) is unaffected.
End-to-end via `typecheck`:
#[safe] fn id(x: Int) { x; } -> OK (x used once)
#[safe] fn drp(x: Int) { 0; } -> ResourceViolation (x dropped)
fn drp(x: Int) { 0; } -> OK (not #[safe], not enforced)
#[safe] fn add1(x: Int){ x + 1; } -> OK (arithmetic out-of-fragment, skipped)
4 new checker tests; all 153 my-lang tests green. STATUS docs updated.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
Extends the session coupling from the binary `cstep` to the remaining two
layers of the SessionPi metatheory, both nondeterministic relations:
SessionEval.v (axiom-free, in _CoqProject / CI-gated):
- gstep1 : gty -> option gty — sound (gstep1_sound) + PROGRESS (gstep1_complete:
gstep G G' -> exists G'', gstep1 G = Some G''). Commits to the head branch;
progress not determinism because gstep is nondeterministic at GBra.
- nstep1 : role_assignment -> option role_assignment — sound (nstep1_sound) +
PROGRESS (nstep1_complete). Scans for the first communicating pair
(find_recv/find_bra), parties always re-fetched via ra_get so duplicate role
entries never act on a stale party. Soundness via per-search inversion lemmas;
progress via the dual membership lemmas + ra_get_in.
For the two nondeterministic relations the honest adequacy is soundness +
progress (`step1 = None` iff stuck), not functional determinism.
Rust runtime (my_qtt::session): faithful Gty/Vty + gstep1, and
RoleAssignment/ra_get/ra_set/find_recv/find_bra/try_role/nstep1, mirroring Coq;
+5 unit tests.
Conformance: gstep1/nstep1 extracted (Extract.v); the harness gains
(gstep GTY) and (nstep RA) queries (oracle parse/show for gty + role_assignment;
generators in conformance_gen). One run.sh now drives 6 query classes:
90,000 results across 5 seeds agree (3000 cases x {check, one-step, normal-form,
cstep, gstep, nstep}).
STATUS.md: #4 row -> all three layers conformance-checked; two new
mechanised-cores rows for gstep1/nstep1.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…lures at source (#129) ## What Deals with the pre-existing CI failures **at source**, in scope order. Summary of every red and its disposition: | Failure | Root cause | Fix | |---|---|---| | `llvm-cov` "no profraw" | **My regression from #127** — `CheckError::ResourceViolation` made a `match` in `my-lsp` non-exhaustive, so `cargo --workspace` couldn't build → no tests ran → no profraw | ✅ Added the missing match arm; `cargo test --workspace --exclude my-llvm` green | | `governance / Licence consistency` | repo-root `LICENSE` had no SPDX header | ✅ Added `SPDX-License-Identifier: MPL-2.0` | | `PR (address)` / `PR (undefined)` (ClusterFuzzLite) | `.clusterfuzzlite/Containerfile` was **conflict-broken** and misnamed (the action builds from `Dockerfile`) | ✅ Clean `Dockerfile` + corrected `build.sh`; removed broken `Containerfile` | | stale merge-conflict markers | unresolved `<<<<<<<`/`=======`/`>>>>>>>` in `CONTRIBUTING.md`, `.clusterfuzzlite/{Containerfile,build.sh}` | ✅ Resolved (kept the `my-lang` side; HEAD's `my-lang-archive` is a stale name) | | `scan / Hypatia` + `Validate Hypatia Baseline` | **Upstream** — the Hypatia analyzer itself fails to compile: `undefined variable "real_subdirs"` at `lib/rules/structural_drift.ex:1019` in `hyperpolymath/standards` | ⛔ Out of my push scope — must be fixed in `standards`; nothing in my-lang triggers it | ## Honesty notes - **I mis-diagnosed `llvm-cov` earlier as "not caused by this PR."** It *was* — the "no profraw" was a downstream symptom of `my-lsp` failing to build under `--workspace`. My local `-p my-lang`/`-p my-qtt` runs never built `my-lsp`, so they missed it. This PR fixes it and I've verified the full workspace build + tests. - The ClusterFuzzLite Dockerfile/build.sh follow the documented OSS-Fuzz Rust pattern and are syntax-checked, but the full image build needs the OSS-Fuzz base image (not runnable locally) — so that one is "root cause removed, correct by inspection," not locally executed. - **Hypatia is the only remaining red and it's upstream.** Exact fix for whoever owns `standards`: bind/define `real_subdirs` before its use at `structural_drift.ex:1019` (looks like a variable that was renamed/dropped). ## Verification - `cargo test --workspace --exclude my-llvm` → all crates green (my-lsp 5, my-lang 153, my-qtt 25, …). - No conflict markers remain repo-wide; `bash -n .clusterfuzzlite/build.sh` OK; LICENSE SPDX header present. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV --- _Generated by [Claude Code](https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
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
2 participants
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.
What
Two follow-ups requested after the coupling work merged (#121):
1. Wire the verified QTT checker in as the compiler default (
#[safe]-gated)crates/my-lang/src/checker.rsnow runs the machine-checked QTT core (my_qtt::check, the faithful R5 port) by default — no flag — on every function annotated#[safe].Checker::check_qtt_safe_fnmodels the function as|params| body, lowers it viaqtt_bridge, and a parameter dropped/duplicated within the resource fragment becomesCheckError::ResourceViolation. Out-of-fragment bodies (arithmetic, records, AI exprs,return, calls to globals) can't be lowered and are skipped — unverifiable ≠ unsafe.Gated on
#[safe](per the maintainer's choice) because my-lang isn't linear-by-default — blanket enforcement would reject normal code. End-to-end viatypecheck:Closes the
docs/STATUS.adoc"make the resource axis the default in checker.rs" item. 4 new tests; all 153 my-lang tests green.2. The n-ary
nstep+ globalgstepsession runtimes (coupling #4, remaining layers)SessionEval.vadds a functional stepper for the other two layers of the SessionPi metatheory, both nondeterministic relations, proved adequate and axiom-free (CI-gated):gstep1 : gty -> option gtygstep1_sound+gstep1_complete(progress)nstep1 : role_assignment -> option role_assignmentnstep1_sound+nstep1_complete(progress)For nondeterministic relations the honest adequacy is soundness + progress (
step1 = Noneiff stuck), not functional determinism —gstep1commits to the head branch,nstep1to the first communicating pair (find_recv/find_bra, parties always re-fetched viara_getso duplicate role entries never act on a stale party).Rust runtime
my_qtt::sessiongains faithfulGty/Vty/gstep1andRoleAssignment+ the lookup/search chain +nstep1(+5 unit tests). Both are extracted and differentially conformance-tested: oneconformance/run.shnow drives 6 query classes — 90,000 results across 5 seeds agree ({check, one-step, normal-form, cstep, gstep, nstep}× 3000 × 5).Verification
coqcsuite (incl.SessionEval.v) builds; all new theoremsPrint Assumptions→ closed (axiom-free).cargo test -p my-qtt(25) +-p my-lang(153) green.conformance/run.sh90k/90k agree across 5 seeds.Scope / honesty
Refinement-by-conformance against the extracted verified steppers, not a full Rust-in-Coq proof. The
#[safe]resource check only bites where the body is in the lowerable fragment. The AI-surfaceinterpreter.rsremains a separate unverified frontend.🤖 Generated with Claude Code
https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
Generated by Claude Code