Repository navigation
Implement the settled/roaming memory model - #177
Conversation
Syntax: a `^` token, `^T` as a type atom beside `&T`, and `x ^T Type` for an inline type parameter that takes an owner. Six new conflict states, all in the existing `<` declared-operator family; the ledger and census record them. Semantics: `Ty.Roaming` beside `Ty.Reference` (was `Ty.Guest`). `^` only on a local, a parameter or a return type, only on a reference type; a bare reference-typed result or abort type is an error, as is a marker on `this`. A new `states.ml` decides whether a place is settled, roaming, borrowed, contingent or fresh, and the analyses read it: a move takes only a roaming symbol, a field of one (leaving the root partly spent), a verb result or a case form; a reference is minted only from a settled place, through struct fields and `ArrayRef` elements, and a declared subscript is followed to its projection; a bare reference-type parameter and `this` are borrows; a `^T` parameter is scoped to the body's top block. `guests.ml` and `owners.ml` become `references.ml` and `scopes.ml`, and diagnostics use the owner / reference / scope vocabulary. A wrong-kind type argument is reported at its origin (generics.md §3.6). `@primitives$ArrayRef<T, n>` with its literal constructor, `fill`, and subscript. `@primitives$String` is a value type, `print` borrows its text and `push` takes `^T`, which closes the old `print` divergence. Lowering and runtime: a reference is the settled owner's address, so the anchor pool, backpointers, forwarders and floating are gone (anchor.c is removed) and a reference-type instance is its members alone. A `^T` argument is moved into the callee and held in its body's arena; a borrow is passed by address. Every overwrite is in place, writing into each boxed member's existing block, and a block relocates only when its owner escapes. `ArrayRef` lowers as `Array` does, with `fill` a counted loop. Fixtures and goldens are rewritten in the new model (`hosts` and `guests` become `owners` and `settled`), with new codegen, runtime and reject cases for in-place overwrites observed through references, `ArrayRef`, takes, partial spending and the type-level rules. Design docs describe the new model and record a reference as a 64-bit address rather than a segmented offset. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
A type parameter's introduction carries the passing mode (spec generics.md §3.2): `x &T Type` takes a reference, inferred from the place it is minted from. `&` marks only a reference type, so a value type that fills an `&T` written over a type parameter, on a field or a verb's parameter, is a wrong-kind argument reported at its origin (generics.md §3.6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
|
Important Review skippedToo many files! This PR contains 118 files, which is 18 over the limit of 100. To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch. Upgrade to a paid plan to raise the limit. This review couldn't start because sufficient usage credits or metered capacity aren't available. Add credits or update usage-based reviews in the billing tab, then retry. ⚙️ Run configuration
⛔ Files ignored due to path filters (9)
📒 Files selected for processing (118)
You can disable this status message by setting the
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request implements the new memory model for the Zane language, transitioning from 'guests' and 'hosts' to 'references' and 'owners' (both settled and roaming). This includes representing references as native 64-bit addresses, performing overwrites in-place, and removing the runtime anchor pool. It also adds support for ArrayRef and ArrayRef.fill. The review feedback identifies a compilation error in lib/cgt/lower.ml where Stat.assign is called but is not defined in the codebase, suggesting the use of Stat.Assign instead.
TheLazyCat00
left a comment
TheLazyCat00
left a comment
There was a problem hiding this comment.
I would hold this PR until the four P1 findings below are fixed. I reproduced five new-model regressions at 3015da2bf15d46926ec1d791523268ca9103ac96: a function calling-convention mismatch, an overlapping borrow/take in one call, incorrect spawn move classification, an abort that consumes a borrow, and missing result-mode validation after generic instantiation.
The inline comments include the reproductions and observed behavior. Their common prelude is:
package probe;
alias Int = @primitives$Int
alias Unit = @primitives$Unit
alias String = @primitives$String
type Packet = #struct { text String; }
Packet(text String) => init{text;}
I built through TST, CGT and LLVM, and executed the native programs. The function-mode reproduction crashes; the borrow/take and borrowed-abort reproductions lose the caller's text. The existing parser, semantics, codegen, runtime and object-file suites pass. Local validation used OCaml 4.14.1 and LLVM 19.1.1, with a temporary compatibility replacement for the OCaml 5 Filename.temp_dir call in the executable-build helper; no semantic, lowering or runtime code was changed for testing. The OCaml Domain unit suite and Lean proof were not run locally.
I also checked the following problems against base 14e70c53e72ec95ecd653e7d00d2680a155cb1b0. They already exist there, so I am separating them from the new regressions:
- Abort lowering uses the expression type instead of the declared abort destination. A legal
Int?&Packet fail(p &Wrap) { abort p.child; }returns a taken owning record where the handler expects a pointer. Readinge.textcrashes on both base and head. - Scope checking of abort does not compare the aborted value with the caller's scope.
Int?&Packet fail() { p Packet(String("es") + String("caped\n")); abort &p; }is accepted despite returning a reference to a drained local. - Handler binder provenance is never populated from the call's abort value/arguments. A legal abort of a holder carrying an
&Packetto a caller's inner local can therefore be unpacked by its handler into an outer&Packetbinding. The checker accepts the escaping reference, and the dynamic-string reproduction prints nothing after the inner scope drains. This also occurs on base.
Those inherited gaps still need attention for the stated abort/lifetime guarantees. The new non-escaping borrow semantics make the fourth inline finding a new caller-visible regression even though the missing abort-store dispatch itself is older.
The existing review's claim that Stat.assign is undefined is a false positive: it is defined in lib/cgt/nodes.ml, and the compiler builds.
- A function argument matches a parameter only at the passing modes it was written with, once inference fills the parameter: `Int[Packet]` no longer fills `Int[^T]` with a reference type, nor `Int[Int]` an `Int[&T]`. - An argument lent to a borrow stays lent for the whole call, so a later argument may not take the same place. - Spawn safety reads the new modes: a `^T` argument or a `^T` local's initializer moves the owner, and a bare reference-type argument borrows it. - An abort is a store, like a return: the move, reference-source and scope checks see it at the declared abort type, lowering hands it on at that type, and a handler's binder names what the call's arguments name. - A bare type parameter as a result or abort type is rejected once an instance fills it with a reference type, including inside function types. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
|
/gemini review |
There was a problem hiding this comment.
Code Review
This pull request updates the memory model by replacing 'guests' and 'hosts' with 'references' (&T) and 'roaming owners' (^T). This change involves parser updates to support the caret (^) marker, AST modifications, and a major rewrite of the static analysis passes (introducing references.ml, states.ml, and scopes.ml). The C runtime is also simplified by removing anchors and backpointers, and implementing in-place overwrites. The review identified several critical omissions where the newly introduced Ty.Roaming type variant is not handled, specifically in scopes.ml's place function (which fails to check declared block scopes, allowing dangling references), verb_signatures.ml's home function, and type_decls.ml's concept_in and is_reference functions.
|
@codex review |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1558f40819
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
2 participants
Brings the compiler from spec b0675d6 up to zane-lang/spec#212, zane-lang/spec#214 and zane-lang/spec#216, plus the follow-ups in the spec PR on the branch of the same name.
Language
^T(roaming owner). It is written on locals, parameters, return types and abort types.^Ttakes the owner, and&Ttakes a reference.thisis always a borrow.x ^T Type,x &T Type.^Tverb result or a case form moves. Moving a field leaves its root partly spent until the field is refilled. A^Tparameter's scope is the body's top block.ArrayRefelements. A declared subscript is followed to the place its body projects.&T.@primitives$ArrayRef<T, n>, with a literal constructor,.fill(n, lambda)and element access.@primitives$Stringis now a value type.printborrows its text, which closes the oldprintdivergence.pushtakes^T.states.mldecides whether a place is settled, roaming or borrowed.moves.mlis rewritten.guests.mlis renamedreferences.mlandowners.mlis renamedscopes.ml, and diagnostics use the new vocabulary.Runtime and lowering
runtime/anchor.c. A reference is a raw pointer.docs/design/lowering.md§9.^Targument is passed by value and held in the callee's top arena.Grammar
CARETtoken,^Ttype atoms, and^/&before an inline introduction.docs/ambiguity/proof-obligations.mdis updated.Tests
just testpasses: compiler, grammar, ambiguity tools and grammar generation.just check-file-sizeswarns only thatlib/cgt/lower.mlis 1519 lines.just verify-grammar(Lean) was not run locally, becauselakeis not installed in the environment.hostsandguestsare renamed toownersandsettled, and rewritten.arrayrefs.referencesnow covers a generic&T Typeholder that sees an in-place overwrite..outis all "yes".marks.znfor marker placement, result modes, overloads by mode, and wrong-kind^/&arguments.🤖 Generated with Claude Code
https://claude.ai/code/session_01ArFxFkp985vTC6aHAAxp82
Generated by Claude Code