proof(coupling): close impl⇄spec couplings #1–#4 by differential conformance; #5 by-design#121
Merged
Merged
Conversation
…ntial conformance The verified Coq `check` (R5) is extracted to OCaml and used as an independent oracle against the Rust port `my_qtt::check`; a random corpus harness asserts byte-identical results (accept/reject, synthesized type, usage vector), including echo terms. 25,000 terms across 5 seeds agree. - proofs/verification/coq/solo-core/Extract.v: `Separate Extraction check` (native-int nat), not in _CoqProject so `make` ignores it. - conformance/oracle.ml: S-expression reader over the extracted verified `check`; canonical result printer. - crates/my-qtt/src/bin/conformance_gen.rs: deterministic random corpus + Rust `my_qtt::check` results, canonical printers byte-matching the oracle. - conformance/run.sh: extract -> compile oracle -> generate -> diff (PASS/FAIL). - conformance/README.adoc: method + scope/honesty. - proofs/STATUS.md: coupling #1 -> conformance-checked; new "conformance-checked" vocabulary entry; section intro updated (method = differential conformance against the extracted verified artifact). Scope: refinement-by-conformance against the extracted verified algorithm, not a full Rust-in-Coq refinement proof; wiring my-qtt in as the DEFAULT checker (today opt-in via qtt_bridge) remains the separate docs/STATUS.adoc intend. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
…tep1 + conformance
The reference operational semantics is the `step` RELATION (not extractable),
so close the interpreter coupling in two moves:
1. Eval.v (new, in _CoqProject so CI machine-checks it): a functional
`step1 : tm -> option tm` proved SOUND and COMPLETE vs the `step` relation
(`step1_sound`, `step1_complete`), real Qed, axiom-free (Print Assumptions
closed). The executable mirror of `step`.
2. Differential conformance: `step1` is extracted to OCaml (Extract.v) and the
Rust port `my_qtt::step1` (faithful shift/subst_at/subst0/subst2/is_value/
step1, mirroring Coq) is compared against it by conformance/run.sh — one
step AND iterated to normal form (cap 64), the latter cross-checking the
Rust substitution against Coq's extracted subst. 45,000 results across 5
seeds agree (3000 terms x {check, one-step, normal-form}).
Details:
- crates/my-qtt/src/lib.rs: add the evaluator + 6 redex unit tests.
- crates/my-qtt/src/bin/conformance_gen.rs: emit (s tm) one-step and
(nf closed-redex) queries + Rust results; closed redex-rich generator.
- conformance/oracle.ml: show_tm printer, (s)/(nf) queries, open Eval.
- conformance/run.sh: dependency-sort all extracted modules (robust to
PeanoNat etc.); report both couplings.
- proofs/STATUS.md: coupling #2 -> conformance-checked; new mechanised-cores
row for Eval.v step1_sound/complete; section intro updated.
Scope: couples an evaluator over the SHARED solo `tm` (same approach as the
checker), mirroring `step`; the AI-surface interpreter.rs is a separate
unverified frontend and is not what is coupled here.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
…cker Echo is wired end-to-end through the VERIFIED machinery: the my_qtt::surface fragment already carries 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. Add surface tests pinning the full `EchoLinear` discipline from a surface term: - echo intro types correctly (-> Ty::Echo); - a LINEAR echo weakens to an AFFINE one; - weakening an AFFINE echo is REJECTED (one-way; the no-section fact); - witness linearity is threaded (an echo dropping a linear binder is rejected). Echo terms are also in the random differential-conformance corpus (#1/#2), so my_qtt's echo handling is checked against the extracted Coq check/step1. Scope: closes echo on the verified-core-facing surface; the conventional compiler (crates/my-lang ast::Expr/parser) still lacks echo SYNTAX (a type-annotated echo grammar is a frontend follow-on, like Param quantity syntax), so qtt_bridge cannot yet lower a compiler-AST echo. STATUS #3 updated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
…y-design Coupling #4 (session runtime refines Coq `cstep`), binary fused config: - SessionEval.v (new, in _CoqProject): functional `cstep1 : config -> option config` proved SOUND + COMPLETE vs the `cstep` relation (cstep1_sound, cstep1_complete), real Qed, axiom-free. - crates/my-qtt/src/session.rs (new): faithful Rust port — val/party/pbranch/ config + vlift/vsubst/psubst_party/open_party/pget/cstep1, mirroring Coq + 4 unit tests (comm step, select step, missing-label stuck, ended normal). - cstep1 extracted (Extract.v); the harness gains (cstep CONFIG) queries (oracle.ml session parse/show; conformance_gen random config generator). One run.sh now drives all couplings: 60,000 results across 5 seeds agree (3000 cases x {check, one-step, normal-form, session-step}). Coupling #5 (concrete `me` surface): reclassified from "absent" to "by-design — not a gap". Me is an agent-generated runtime PROJECTION over Solo/Duet/Ensemble, not a static dialect (the static attempts were retired/ sidelined). The elaboration coupling that matters — M1 `me_wt_sound` — is already machine-checked over the abstract Coq `me_tm`. Building a static `me` grammar would contradict the architecture, so it is intentionally not built. STATUS.md: #4 -> conformance-checked (binary fragment); #5 -> by-design; new mechanised-cores row for SessionEval cstep1; section header + intro updated (#1–#4 closed, #5 by-design). Honest scope: n-ary nstep/gstep runtimes are a larger follow-on; the AI-surface interpreter.rs is separate. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
… + coeUsage The Idris `preservation` merged in #120 did not actually compile on a clean checkout: `Substitution.idr` was committed WITHOUT `subst2Lemma` and `coeUsage` (they existed transiently in the working tree during the session but were lost from the commit), while `Soundness.preservation` calls both. #120's `Idris2 solo-core` CI never completed before merge, so the broken build landed unverified; PR #121 is the first run to fully exercise it. Fix: - Substitution.idr: re-add `coeUsage` (usage-equality coercion, public export) and `subst2Lemma` (two-variable LetPair substitution) after `substLemma0` — the exact, previously-green definitions the header comment already documents. - Soundness.idr: route `preservation`'s four coercions through the module's existing private `coeUse` (same signature) instead of the cross-module name. Verified clean: `rm -rf build && idris2 --build solo-core.ipkg` exits 0 (8/8); `:total` confirms preservation, affinePreservation, subst2Lemma, coeUsage all total; no holes / postulates / believe_me / assert_total. This repairs the broken state on main; the solo core is now genuinely HOLE-FREE on a clean build. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
hyperpolymath
marked this pull request as ready for review
June 21, 2026 11:24
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
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
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).check(R5)stepcstep(binary)mesurfaceMethod
The verified Coq functions are extracted to OCaml (
Extract.v,Separate Extraction) and used as independent oracles; the Rust ports incrates/my-qttare 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(vsstep), axiom-free, in CI.SessionEval.v—cstep1+cstep1_sound/cstep1_complete(vscstep), 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
Eval.v,SessionEval.v;Extract.v(extraction-only, not in suite).conformance/{oracle.ml,run.sh,README.adoc},crates/my-qtt/src/bin/conformance_gen.rs.crates/my-qtt/src/{lib.rs (evaluator),session.rs (new),surface.rs (echo tests)}.proofs/STATUS.md: rows Type-checker OOM (16-32 GB allocation) on deeply-nested str_concat / format chains #1–ci(antipattern): broaden TS allowlist (cli, mod.ts, lsp-server, *vscode*, deno-*) #5 + newconformance-checkedvocabulary + 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-arynstep/gstepruntimes are a larger follow-on. These are explicitly labelled, not hidden.Requires
coqc8.18,ocamlfind+ocamlc,cargo(all in the proof CI image).🤖 Generated with Claude Code
https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV
Generated by Claude Code