[wildcard] Replace graph-based borrow checking with Compile-Time Affine Capability Tokens

Aperta
  • Qualcosa non va?
#175 1 commento 0 reazioni 0 assegnatari Vedi su GitHub

I maintainer di solito rispondono entro 1 giorno

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
5/5
Tempo stimato
Più di una settimana
Idoneità per principianti
8/100
Tipo di issue
Funzionalità
Chiarezza
Da chiarire
Stato di attività
Attiva
Stack tecnologico
go, rust
Ambito
compilers

Direzione di ricerca

This is a design proposal, not a code change. Start by reading hy-check/src/loans.rs and hy-check/src/alias.rs, then the soundness issues it cites (#27, #82, #137, #138). Done would be a written set of token transition rules checked against those issues, and the proposal's own falsification gate decides whether it survives.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

duplicate wildcard
The idea, in a paragraph

Currently, Hybrid maintains a complex, reactive graph of aliases (record_alias, record_may_share), mutable loan windows (LoanTarget::MapSlot, LoanTarget::Handle), and freeze states across lexical statements to approximate Rust-like borrow checking over Go semantics. As evidenced by recent soundness waves (#27, #82, #137, #138), this graph approach suffers from combinatorial edge holes whenever bindings cross closure captures, inner-scope rebinds, or interprocedural returns.

Instead of tracking pointers and mutable borrows via ambient graph state, replace the entire loan/alias engine with Affine Capability Tokens (Cap[T]) threaded through the typing environment. Accessing mutable state or transferring across concurrency boundaries requires consuming or splitting an unforgeable capability token. Borrowing is syntactically a scoped token split; moving is a linear consumption. The entire mutable state in st.loans, st.aliases, and st.shares can be replaced with a single forward O(N) token-balance verification pass.

Which assumption it breaks
  • Directly answers Solicitation Prompt 2: "Replace the borrow-checker machinery. Capability tokens, linear-type encodings inside Go's type system, runtime-enforced ownership — anything that deletes the alias/loan/freeze analysis rather than extending it."
  • Kills the sacred cow that Hybrid needs an ad-hoc Rust-like borrow graph engine (loans.rs, alias.rs, graph-based freeze tracking) to guarantee data-race freedom.
  • Kills statement-level retroactive loan patching in favor of compositional type-level capabilities.
Why this is a breakthrough, not an increment

Feature bounties are trapped in a cycle of adding defensive patches to loans.rs and alias.rs (interprocedural windows, map-slot re-assignments, closure-local aliasing, field projections). Each fix deepens coupling and increases compilation complexity.

Capability tokens invert the paradigm: the compiler stops asking "where might an alias have leaked in the AST?" and instead asks "does the current expression hold an active capability token to perform this mutation or transfer?". By treating capabilities as affine resources:

  1. Data races and use-after-free are structurally impossible by construction—there is no graph to bypass.
  2. In the emitted Go code, capability tokens are zero-cost phantom types (type Cap[T] struct{}) completely erased by gc / Go compiler.
How we would know it works (or doesn't)

Falsifiable Milestones:

  • M1 ($250 milestone): Theoretical typing rules & soundness stress-test
    Formulate the 3 core token transition rules: Mint (allocation), Split/Borrow (disjoint read permissions), and Consume (move / task spawn). Verify these rules against the 10 landmark soundness issues in Hybrid's history (#27, #37, #69, #72, #82, #117, #137, #138, #141, #143).
    Falsification gate: If any of these 10 soundness hazards can be expressed without causing a token imbalance under the formal rules, the proposal fails immediately at M1.

  • M2 ($250 milestone): Corpus validation & usability limit analysis
    Implement a prototype token-balance pass and run it against all 42 corpus fixtures in the test suite.
    Evaluation criteria: Must maintain 100% rejection on reject fixtures and 100% acceptance on valid fixtures.
    Published learning: If common Go idioms (e.g. temporary field projection or re-entrant map access) require excessive syntax friction that cannot be automatically inferred by the compiler, the post-mortem will document exactly where affine capabilities reach their usability ceiling in a Go-adjacent language.

Cost honesty (optional but powerful)
  • Deletions: Deletes hy-check/src/loans.rs (~1,000 lines) and simplifies hy-check/src/alias.rs.
  • Compiler architecture: Replaces complex retroactive graph traversals with a single forward capability ledger pass.
  • Migration & UX: End users write idiomatic Hybrid code (& and move); the compiler infers capability lifetimes under the hood, requiring explicit capability syntax only for advanced zero-copy concurrency patterns.
Track terms
  • I understand no prototype is required and failure-with-knowledge is a valid, paid outcome
  • I understand all outcomes (including declines and failures) are published in MOONSHOT.md
Lingua principale
Rust
Stelle
4
Fork
18
Merge medio
1g 7h
PR unite (30g)
199

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di limitlessprojects/Go-Hybrid

Tutte le issue di limitlessprojects/Go-Hybrid

Issue simili

Altre issue su Rust

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.