ci(antipattern): allowlist legit TS bridge/adapter paths#4
Merged
Conversation
hyperpolymath
added a commit
that referenced
this pull request
Jun 21, 2026
…ormance; #5 by-design (#121) ## What Closes the **implementation ⇄ spec coupling** obligations (`proofs/STATUS.md` §"Implementation ⇄ spec coupling") — making "the soundness lives in the compiler" literally true, by **differential conformance against the Coq-extracted verified artifacts** (the honest, reproducible alternative to an infeasible full Rust-in-Coq refinement proof). | # | Coupling | Status | |---|----------|--------| | 1 | Rust checker refines Coq `check` (R5) | ✅ conformance-checked | | 2 | Rust evaluator refines Coq `step` | ✅ conformance-checked | | 3 | Echo modality wired surface → verified checker | ✅ conformance-checked (verified-core surface) | | 4 | Rust session runtime refines Coq `cstep` (binary) | ✅ conformance-checked | | 5 | Concrete `me` surface | ✅ by-design — not a gap | ## Method The verified Coq functions are extracted to OCaml (`Extract.v`, `Separate Extraction`) and used as **independent oracles**; the Rust ports in `crates/my-qtt` are the implementations under test. One harness (`conformance/run.sh`) generates a random corpus and asserts byte-identical results. Where the spec is a *relation* (`step`, `cstep`), a functional mirror is first **proved sound + complete** vs the relation, then conformance-tested: - **`Eval.v`** — `step1` + `step1_sound`/`step1_complete` (vs `step`), axiom-free, in CI. - **`SessionEval.v`** — `cstep1` + `cstep1_sound`/`cstep1_complete` (vs `cstep`), axiom-free, in CI. **60,000 results across 5 seeds agree** (3000 cases × {check, one-step, normal-form, session-step}); the normal-form pass cross-checks the Rust substitution against Coq's extracted `subst`, and echo terms (#3) ride in the corpus. ## Files - Coq (new, CI-gated): `Eval.v`, `SessionEval.v`; `Extract.v` (extraction-only, not in suite). - Harness: `conformance/{oracle.ml,run.sh,README.adoc}`, `crates/my-qtt/src/bin/conformance_gen.rs`. - Rust verified-core: `crates/my-qtt/src/{lib.rs (evaluator),session.rs (new),surface.rs (echo tests)}`. - `proofs/STATUS.md`: rows #1–#5 + new `conformance-checked` vocabulary + two mechanised-cores rows. ## Scope / honesty (carried in STATUS.md) Refinement-by-conformance against the *extracted verified algorithm*, not a full Rust-in-Coq proof. The *main* `checker.rs` (Hindley) still doesn't call the verified core by default; echo lacks conventional-compiler *syntax*; the n-ary `nstep`/`gstep` runtimes are a larger follow-on. These are explicitly labelled, not hidden. Requires `coqc` 8.18, `ocamlfind`+`ocamlc`, `cargo` (all in the proof CI image). 🤖 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>
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…untimes (#127) ## 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.rs` now 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_fn` models the function as `|params| body`, lowers it via `qtt_bridge`, and a parameter dropped/duplicated *within the resource fragment* becomes `CheckError::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 via `typecheck`: ``` #[safe] fn id(x: Int) { x; } -> OK #[safe] fn drp(x: Int) { 0; } -> ResourceViolation (x dropped) fn drp(x: Int) { 0; } -> OK (not #[safe]) #[safe] fn add1(x: Int){ x + 1; } -> OK (arithmetic out-of-fragment, skipped) ``` 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` + global `gstep` session runtimes (coupling #4, remaining layers) `SessionEval.v` adds a functional stepper for the other two layers of the SessionPi metatheory, both **nondeterministic** relations, proved adequate and **axiom-free** (CI-gated): | Stepper | Layer | Theorems | |---------|-------|----------| | `gstep1 : gty -> option gty` | global type | `gstep1_sound` + `gstep1_complete` (progress) | | `nstep1 : role_assignment -> option role_assignment` | n-ary located | `nstep1_sound` + `nstep1_complete` (progress) | For nondeterministic relations the honest adequacy is **soundness + progress** (`step1 = None` iff stuck), not functional determinism — `gstep1` commits to the head branch, `nstep1` to 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). Rust runtime `my_qtt::session` gains faithful `Gty`/`Vty`/`gstep1` and `RoleAssignment` + the lookup/search chain + `nstep1` (+5 unit tests). Both are extracted and differentially conformance-tested: one `conformance/run.sh` now drives **6 query classes** — **90,000 results across 5 seeds agree** (`{check, one-step, normal-form, cstep, gstep, nstep}` × 3000 × 5). ## Verification - `coqc` suite (incl. `SessionEval.v`) builds; all new theorems `Print Assumptions` → closed (axiom-free). - `cargo test -p my-qtt` (25) + `-p my-lang` (153) green. - `conformance/run.sh` 90k/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-surface `interpreter.rs` remains a separate unverified frontend. 🤖 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
1 participant
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.
Same fleet-wide patch as stapeln#24 / rsr-template-repo#30. Broadens TS exclusion list (bindings/, tests/, test/, scripts/, mcp-adapter/, vscode/).