feat(checker): enforce the verified QTT resource discipline on #[safe] 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

Author: claude

crates/my-lang/src/checker.rs

@@ -109,6 +109,13 @@ pub enum CheckError {
         line: usize,
         column: usize,
     },
+
+    #[error("`@safe` function `{name}` violates the verified linear resource discipline (a parameter is dropped or used more than once) at line {line}, column {column}")]
+    ResourceViolation {
+        name: String,
+        line: usize,
+        column: usize,
+    },
 }
 
 /// Maximum AST nesting depth the type checker will recurse through before
@@ -614,10 +621,56 @@ impl Checker {
         // Check function body
         self.check_block(&f.body);
 
+        // `@safe`: enforce the machine-checked QTT resource discipline (runs by
+        // default — no flag — for every `@safe`-annotated function).
+        if f.modifiers.contains(&FnModifier::Safe) {
+            self.check_qtt_safe_fn(f);
+        }
+
         self.current_return_type = None;
         self.symbols.exit_scope();
     }
 
+    /// Resource-check a `@safe` function with the verified QTT core
+    /// (`my_qtt::check`, the faithful R5 port reached via [`crate::qtt_bridge`]).
+    ///
+    /// The function is modelled as a lambda over its parameters — each treated
+    /// **linearly** (`DEFAULT_Q = One`, the strictest reading) — and the
+    /// machine-checked usage-walk runs on it. A parameter dropped or used more
+    /// than once *within the resource-relevant fragment* is reported as a
+    /// [`CheckError::ResourceViolation`]. A body that uses constructs OUTSIDE
+    /// that fragment (arithmetic, records, AI expressions, calls to globals, …)
+    /// cannot be lowered and is **skipped** — unverifiable is not unsafe, and
+    /// name/type resolution of those parts is the main checker's job. So
+    /// `@safe` means "the proof core has checked this function's resource
+    /// discipline wherever it is expressible", enforced by default.
+    fn check_qtt_safe_fn(&mut self, f: &FnDecl) {
+        use crate::qtt_bridge::{check_expr, BridgeCheckError};
+        use my_qtt::surface::CheckError as QttError;
+
+        // model the @safe function as `|params| body`
+        let lam = Expr::Lambda {
+            params: f.params.clone(),
+            body: LambdaBody::Block(f.body.clone()),
+            span: f.span,
+        };
+        match check_expr(&lam) {
+            // resource-safe, or outside the verifiable fragment (skip), or a
+            // free name the main resolver already diagnoses (skip).
+            Ok(_)
+            | Err(BridgeCheckError::Bridge(_))
+            | Err(BridgeCheckError::Check(QttError::Elab(_))) => {}
+            // lowered fully, but the verified walk rejected the usage discipline.
+            Err(BridgeCheckError::Check(QttError::Untypable)) => {
+                self.errors.push(CheckError::ResourceViolation {
+                    name: f.name.name.clone(),
+                    line: f.span.line,
+                    column: f.span.column,
+                });
+            }
+        }
+    }
+
     fn check_struct(&mut self, s: &StructDecl) {
         // Check that field types are valid
         for field in &s.fields {
@@ -1827,4 +1880,45 @@ mod tests {
         let errors = result.unwrap_err();
         assert!(errors.iter().any(|e| matches!(e, CheckError::NonBoolCondition { .. })));
     }
+
+    // ---- `@safe` functions are resource-checked by the verified QTT core ----
+
+    /// A `#[safe]` function whose parameter is used exactly once passes the
+    /// machine-checked linear discipline.
+    #[test]
+    fn qtt_safe_linear_param_ok() {
+        let result = check_source("#[safe]\nfn id(x: Int) { x; }");
+        assert!(result.is_ok(), "expected ok, got {:?}", result);
+    }
+
+    /// A `#[safe]` function that DROPS its linear parameter is rejected by the
+    /// verified usage-walk — the resource axis is now enforced in the compiler.
+    #[test]
+    fn qtt_safe_dropped_param_rejected() {
+        let result = check_source("#[safe]\nfn drp(x: Int) { 0; }");
+        assert!(result.is_err(), "expected ResourceViolation, got Ok");
+        let errors = result.unwrap_err();
+        assert!(
+            errors.iter().any(|e| matches!(e, CheckError::ResourceViolation { .. })),
+            "expected ResourceViolation, got {:?}",
+            errors
+        );
+    }
+
+    /// The SAME body without `#[safe]` is accepted — the discipline is opt-in
+    /// per function (gated on the modifier), so nothing else changes.
+    #[test]
+    fn non_safe_dropped_param_ok() {
+        let result = check_source("fn drp(x: Int) { 0; }");
+        assert!(result.is_ok(), "non-@safe fn must not be resource-checked, got {:?}", result);
+    }
+
+    /// A `#[safe]` body that uses constructs OUTSIDE the resource fragment
+    /// (here, arithmetic) cannot be lowered and is skipped — unverifiable is
+    /// not unsafe, so no false rejection.
+    #[test]
+    fn qtt_safe_out_of_fragment_skipped() {
+        let result = check_source("#[safe]\nfn add1(x: Int) { x + 1; }");
+        assert!(result.is_ok(), "out-of-fragment @safe body should be skipped, got {:?}", result);
+    }
 }

docs/STATUS.adoc

@@ -45,7 +45,7 @@ the Idris twin's `preservation` (#108) is now DISCHARGED (total, hole-free;
 [cols="4,1,3",options="header"]
 |===
 | Item | Status | Note
-| Make the resource axis the *default* in `crates/my-lang/src/checker.rs` | `[ ]` | the QTT bridge is opt-in (`qtt_bridge::check_expr`) today
+| Make the resource axis the *default* in `crates/my-lang/src/checker.rs` | `[x]` | DONE — the verified QTT core runs by default (no flag) on every `#[safe]` function: `Checker::check_qtt_safe_fn` lowers it via `qtt_bridge` and a dropped/duplicated binder in the resource fragment is a `CheckError::ResourceViolation`; out-of-fragment bodies skip (unverifiable ≠ unsafe). Gated on `#[safe]` so non-linear code is unaffected.
 | Surface *quantity syntax* so the bridge enforces real per-binder linearity | `[ ]` | `Param` has no quantity field; bridge defaults to `One`
 | `wasm32` via the existing LLVM backend (`TargetSpec::wasm32` + `wasm-ld`) | `[ ]` | fastest target leg; backend already emits objects
 | `RISC-V` (`riscv64gc-unknown-linux-gnu`) via LLVM | `[ ]` | near-free once `wasm32` target wiring exists

proofs/STATUS.md

@@ -122,7 +122,7 @@ verified against the crate sources + the conformance harness.)
 
 | Obligation | Status | Note |
 |------------|--------|------|
-| Rust affine checker refines Coq `check` / `aff_type_dec` (R5/R5b) | **conformance-checked** | **CLOSED by differential conformance 2026-06-21.** The verified Coq `check` (R5) is extracted to OCaml (`proofs/verification/coq/solo-core/Extract.v`, `Separate Extraction check`) and used as an independent ORACLE; the Rust port `crates/my-qtt` is the implementation under test. `conformance/run.sh` generates a random corpus of `(ctx, tm)` queries (`crates/my-qtt/src/bin/conformance_gen.rs`), runs BOTH the extracted verified `check` (`conformance/oracle.ml`) and `my_qtt::check`, and asserts byte-identical results — same accept/reject, same synthesized type, same usage vector — including echo (`MkEcho`/`Weaken`/`TEcho`) terms. **25 000 random terms across 5 seeds agree** (≈13% accept / 87% reject, so both branches are exercised). `my_qtt::aff_check` mirrors the Coq `aff_type_iff` (`check … = Some(a,D0) ∧ ule D0 budget`) and carries the R5/R5b reflexivity oracle tests. SCOPE/honesty: this is differential refinement-by-conformance against the *extracted verified algorithm*, NOT a full Rust-in-Coq refinement proof; and the *main* `crates/my-lang/src/checker.rs` (1830 LOC, Hindley) still does not yet CALL the verified core (`my_qtt` is wired via `qtt_bridge` but opt-in) — making it the default checker is the separate `docs/STATUS.adoc` intend "make the resource axis the default in `checker.rs`". |
+| Rust affine checker refines Coq `check` / `aff_type_dec` (R5/R5b) | **conformance-checked** | **CLOSED by differential conformance 2026-06-21.** The verified Coq `check` (R5) is extracted to OCaml (`proofs/verification/coq/solo-core/Extract.v`, `Separate Extraction check`) and used as an independent ORACLE; the Rust port `crates/my-qtt` is the implementation under test. `conformance/run.sh` generates a random corpus of `(ctx, tm)` queries (`crates/my-qtt/src/bin/conformance_gen.rs`), runs BOTH the extracted verified `check` (`conformance/oracle.ml`) and `my_qtt::check`, and asserts byte-identical results — same accept/reject, same synthesized type, same usage vector — including echo (`MkEcho`/`Weaken`/`TEcho`) terms. **25 000 random terms across 5 seeds agree** (≈13% accept / 87% reject, so both branches are exercised). `my_qtt::aff_check` mirrors the Coq `aff_type_iff` (`check … = Some(a,D0) ∧ ule D0 budget`) and carries the R5/R5b reflexivity oracle tests. SCOPE/honesty: this is differential refinement-by-conformance against the *extracted verified algorithm*, NOT a full Rust-in-Coq refinement proof; and the *main* `crates/my-lang/src/checker.rs` (Hindley) now CALLS the verified core by default for `#[safe]` functions (`Checker::check_qtt_safe_fn` → `qtt_bridge` → `my_qtt::check`; a dropped/duplicated binder in the resource fragment is a `CheckError::ResourceViolation`, out-of-fragment bodies skip). So the resource axis is enforced-by-default where opted in via `#[safe]` (the `docs/STATUS.adoc` "make the resource axis the default" item — DONE); whole-program linear-by-default is intentionally NOT the design (my-lang is not a linear language). |
 | Evaluator refines Coq `step` (solo core) | **conformance-checked** | **CLOSED 2026-06-21.** The reference semantics is the `step` RELATION (not extractable), so `Eval.v` adds a FUNCTIONAL `step1 : tm -> option tm` and proves it both ways vs the relation — `step1_sound : step1 t = Some t' -> step t t'` and `step1_complete : step t t' -> step1 t = Some t'` — real `Qed`, **axiom-free** (`Print Assumptions` closed), machine-checked in CI (`Eval.v` is in `_CoqProject`). `step1` is extracted alongside `check` (Extract.v) and the Rust port `my_qtt::step1` (faithful `shift`/`subst_at`/`subst0`/`subst2`/`is_value`/`step1`) is differentially conformance-tested against it: `conformance/run.sh` compares **one-step** results AND **iterated normal forms** (cap 64) over a random + closed-redex corpus. **45 000 results across 5 seeds agree** (3000 terms × {check, one-step, normal-form}); the normal-form pass cross-checks the Rust substitution against Coq's extracted `subst`. SCOPE/honesty: this couples an evaluator over the SHARED solo `tm` (the same approach as the checker), exactly mirroring `step`; the separate AI-surface `interpreter.rs` (richer term language, runtime no-ops for `Restrict`/`Ref`/`RefMut`) is NOT what is coupled here and remains an independent, unverified frontend. |
 | Echo modality wired into surface + checker | **conformance-checked** (verified-core surface) | **2026-06-21.** Echo is wired end-to-end through the VERIFIED core: the `my_qtt::surface` fragment has echo intro (`SExpr::Echo` / `STy::Echo`) and the `weaken` elimination (`SExpr::Weaken`), `elaborate` lowers them to `Tm::MkEcho`/`Tm::Weaken`, and the machine-checked `check` consumes them — so the `linear ⊑ affine` discipline (`EchoLinear`) is enforced from a surface term by the proof. Pinned by `surface.rs` tests: intro types correctly, a LINEAR echo `weaken`s to AFFINE, weakening an AFFINE echo is REJECTED (the one-way *no-section* fact), and witness linearity is threaded (an echo whose witness drops a linear binder is rejected). Echo terms are also in the random differential-conformance corpus (#1/#2), so `my_qtt`'s echo handling matches the extracted Coq `check`/`step1`. SCOPE/honesty: this closes echo on the verified-core-facing surface; the *conventional compiler* (`crates/my-lang` `ast::Expr`/parser) still has no echo SYNTAX (so `qtt_bridge` cannot yet lower a compiler-AST echo — that needs a type-annotated echo grammar, a frontend follow-on like the `Param` quantity syntax). `types.rs` `EchoMode` is no longer inert at the verified boundary; it is in the conventional frontend. |
 | Session runtime refining `cstep` (binary fused config) | **conformance-checked** (binary fragment) | **2026-06-21.** `SessionEval.v` adds a functional `cstep1 : config -> option config` for the binary fused `(νc)(P∣Q)` form and proves it SOUND + COMPLETE vs the `cstep` RELATION (`cstep1_sound`/`cstep1_complete`), real `Qed`, **axiom-free**, in `_CoqProject` (CI-gated). `cstep1` is extracted (Extract.v) and the Rust session runtime `my_qtt::session` (faithful `val`/`party`/`pbranch`/`config` + `vlift`/`vsubst`/`psubst_party`/`open_party`/`pget`/`cstep1`) is differentially conformance-tested against it (`conformance/run.sh`, `(cstep CONFIG)` queries) — **15 000 session steps across 5 seeds agree** (the comm + select redexes and the stuck/None cases). SCOPE/honesty: this couples the BINARY fused config (S1.1b/S1.2 fragment); the n-ary located `nstep` and global `gstep` are NOT yet given executable runtimes (a larger follow-on), and the AI-surface `interpreter.rs` (`Go`/`Await` collapse to sequential) is a separate unverified frontend. |