Coupling step 2: my-lang surface → verified QTT core (surface engine + ast bridge)#117
Merged
Merged
Conversation
…core (coupling step 2a) The bridge from a named surface to the de Bruijn core the verified check consumes, so the resource axis can be enforced on real programs. SExpr/STy = the resource-relevant fragment of my-lang's ast::Expr/ast::Type (var, λ-with- quantity, app, both products, sums, let, echo); elaborate resolves names to de Bruijn against a Scope (innermost last, matching Tctx); check_surface runs the machine-checked usage-walk on the elaborated term. 6 tests green: a linear binder DROPPED at the named surface is rejected by the verified algorithm (linear_drop_rejected), the same body under ω is accepted (omega_dup_ok), nested binders resolve to correct indices (scope_resolution), linear let, and unbound-name elaboration errors. Quantities are explicit on SExpr binders, so the ast lowering (step 2b) can default them today and thread real linearity syntax later with no engine change.
…core (coupling step 2b)
my-qtt now sits in my-lang's dependency graph — the proofs' own usage-walk is
in the compiler. qtt_bridge lowers the resource-relevant fragment of the
running compiler's ast::Expr/ast::Type (var, λ, application, let/block, literal)
onto my_qtt::surface, and check_expr runs the machine-checked check on it.
Honest scope: opaque base types -> Unit; -> and tuples map structurally;
out-of-fragment constructs (binary/unary/match/record/AI/try/restrict) return
BridgeError::Unsupported (no silent passes). Quantity default = One (linear),
since Param has no quantity syntax yet and the Coq check is exact-usage — so
the bridge ENFORCES 'use each binder exactly once' on the real AST: a real
|x| x is accepted, a real |x| { 0 } (drops x) is rejected by the verified walk.
Surface quantity syntax (small follow-on) activates real per-binder quantities
with no engine change.
6 tests green over real ast::Expr nodes. With step 2a (the engine), item 1
(coupling step 2) is complete: proofs -> implementation is wired and enforcing.
hyperpolymath
marked this pull request as ready for review
June 18, 2026 06:12
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.
Summary
Coupling step 2 — the bridge from the my-lang surface to the verified QTT core, so the machine-checked usage-walk runs on real programs. Follows PR #116 (which landed
my-qtt, the faithful Rust port of the Coq R5/R5bcheck).2a ·
my-qtt::surface— named-variable elaboration engineThe named surface → de Bruijn
Tmpass the verifiedcheckconsumes.SExpr/STyare the resource-relevant fragment ofast::Expr/ast::Type;elaborateresolves names to de Bruijn against aScope(innermost last, matchingTctx);check_surfaceruns the machine-checked walk. 6 tests — a linear binder dropped at the named surface is rejected by the verified algorithm; the same body underωis accepted; nested binders resolve to correct indices.2b ·
my-lang::qtt_bridge— lower the realast::Exprmy-qttnow sits in my-lang's dependency graph — the proofs' own algorithm is in the compiler.qtt_bridgelowers the resource-relevant fragment of the running compiler'sast::Expr/ast::Typeontomy_qtt::surface, andcheck_exprruns the verifiedcheckon it. 6 tests over realast::Exprnodes — a real|x| xis accepted, a real|x| { 0 }(dropsx) is rejected.Honest scope: opaque base types →
Unit;->/tuples map structurally; out-of-fragment constructs (binary/unary/match/record/AI/…) returnUnsupported(no silent passes). The Coqcheckis exact-usage andParamhas no quantity syntax yet, so the bridge applies the linear default (One) — it enforces "use each binder once" on the real AST. Surface quantity syntax (a small parser+AST follow-on) activates real per-binder quantities with no engine change.Test plan
cargo test -p my-qtt→ 13 passed (engine + the original R5/R5b oracle tests)cargo test -p my-lang qtt_bridge→ 6 passed (realast::Expr)Refs
proofs/STATUS.md§"Implementation ⇄ spec coupling"🤖 Generated with Claude Code
Generated by Claude Code