Dada Formal Model

This book documents the formal model for the Dada programming language. The model is implemented in Rust using formality-core and defines Dada’s type system, including its permission-based ownership model.

The code examples in this book are executable tests – they are compiled and checked as part of the build. When you see a Dada program in this book, it has been verified by the model.

Throughout the book, we will also reference the formal rules from the model’s source code using anchors like ClassDecl.

Classes

Dada programs are made up of class declarations. Each class has a name, fields, and methods. Here is a simple class Point with two Int fields:

crate::assert_ok!(
    {
        class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn test(given self) -> Int {
                let p = new Point(22, 44);
                p.x.give;
            }
        }
    }
);

The Main class is special only by convention – the model checks all methods in all classes. Each method has a receiver (self) with a permission (here, given, which we’ll explain later) and a body that is type-checked against the declared return type.

New instances are created with new Point(22, 44), providing values for each field in declaration order. Fields are accessed with dot notation (p.x).

Class predicates

Classes come in three flavors, determined by a class predicate:

Int is a built-in shared class type – since shared classes are always shared, Int values can be freely copied. Most user-defined classes use the default class predicate, which gives them unique ownership by default.

We will return to class predicates as we explore the permission system.

Grammar

The grammar for class declarations in the model looks like this:

#[term($?class_predicate class $name $binder)]
pub struct ClassDecl {
    pub name: ValueId,
    pub class_predicate: ClassPredicate,
    pub binder: Binder<ClassDeclBoundData>,
}

#[term($:where $,predicates { $*fields $*methods $?drop_body })]
pub struct ClassDeclBoundData {
    pub predicates: Vec<Predicate>,
    pub fields: Vec<FieldDecl>,
    pub methods: Vec<MethodDecl>,
    pub drop_body: DropBody,
}
/// Optional drop body for a class. When present, the statements are executed
/// when an owned handle to the class is dropped. Default is an empty block
/// (no drop body), which is semantically equivalent to `drop { }`.
#[term(drop $block)]
#[derive(Default)]
pub struct DropBody {
    pub block: Block,
}

The #[term(...)] attributes define the parsing grammar using formality-core conventions: $? is an optional element, $* means zero-or-more, $, means comma-separated, and $:where means the keyword where appears only if the list is non-empty. Binder introduces generic parameters that are in scope for the bound data.

Each field has a name and a type, and can optionally be declared atomic (which affects variance – more on this later):

#[term($?atomic $name : $ty ;)]
pub struct FieldDecl {
    pub atomic: Atomic,
    pub name: FieldId,
    pub ty: Ty,
}

#[term]
#[derive(Default)]
pub enum Atomic {
    #[default]
    #[grammar(nonatomic)]
    No,

    #[grammar(atomic)]
    Yes,
}

A simple function

We’re going to walk through how the type checker handles a very simple program, step by step. Here is the complete program:

crate::assert_ok!(
    {
        class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn test(given self) -> Int {
                let p = new Point(22, 44);
                0;
            }
        }
    }
);

Nothing very exciting happens here – we create a Point and then return 0. But working through this example introduces the basic machinery that everything else builds on: the environment, places, types, and – most importantly – how the type checker is structured as a set of judgment functions with inference rules.

Grammar declarations

The formal model represents programs using Rust structs annotated with #[term], a macro from formality-core. Each #[term] struct defines both the abstract syntax and a textual grammar (the $-prefixed patterns).

A class declaration contains a name, an optional class predicate, and a binder wrapping the fields and methods:

#[term($?class_predicate class $name $binder)]
pub struct ClassDecl {
    pub name: ValueId,
    pub class_predicate: ClassPredicate,
    pub binder: Binder<ClassDeclBoundData>,
}

#[term($:where $,predicates { $*fields $*methods $?drop_body })]
pub struct ClassDeclBoundData {
    pub predicates: Vec<Predicate>,
    pub fields: Vec<FieldDecl>,
    pub methods: Vec<MethodDecl>,
    pub drop_body: DropBody,
}
/// Optional drop body for a class. When present, the statements are executed
/// when an owned handle to the class is dropped. Default is an empty block
/// (no drop body), which is semantically equivalent to `drop { }`.
#[term(drop $block)]
#[derive(Default)]
pub struct DropBody {
    pub block: Block,
}

A field declaration is a name and a type:

#[term($?atomic $name : $ty ;)]
pub struct FieldDecl {
    pub atomic: Atomic,
    pub name: FieldId,
    pub ty: Ty,
}

A method declaration contains a name and a binder wrapping the receiver (this), parameters, return type, predicates, and body:

#[term(fn $name $binder)]
pub struct MethodDecl {
    pub name: MethodId,
    pub binder: Binder<MethodDeclBoundData>,
}

// FIXME: need to guard `$inputs` by a comma and output by `->`, using customized parse
#[term(($this $,inputs) -> $output $:where $,predicates $body)]
#[customize(parse)]
pub struct MethodDeclBoundData {
    pub this: ThisDecl,
    pub inputs: Vec<LocalVariableDecl>,
    pub output: Ty,
    pub predicates: Vec<Predicate>,
    pub body: MethodBody,
}

The environment

The type checker’s job is to walk through each statement in a method body and track what it knows about each variable. This information is stored in the environment (Env), which maps variables to their types:

#[derive(Clone, Ord, Eq, PartialEq, PartialOrd, Hash)]
pub struct Env {
    program: Arc<Program>,
    universe: Universe,
    in_scope_vars: Vec<Variable>,
    local_variables: Map<Var, Ty>,
    assumptions: Set<Predicate>,
    fresh: usize,
}

The key field for now is local_variables, which maps each variable to its type. (We’ll explain the other fields as they become relevant.)

Judgments and inference rules

The type system is defined as a collection of judgment functions. Each judgment function is defined with the judgment_fn! macro and contains one or more inference rules. An inference rule has premises above a horizontal line and a conclusion below it. The conclusion holds when all the premises are satisfied.

For example, an inference rule with the conclusion check_program(program) => () means “the program type-checks successfully.” The premises above the line specify what must be true for that conclusion to hold.

How type checking begins

Type checking begins with the check_program judgment, which checks that every declaration in the program is well-formed:

(for_all(decl in program.decls.clone())
    (check_decl(program, decl) => ()))
----------------------- ("check_program")
(check_program(program) => ())

The sole premise uses for_all to require that check_decl succeeds for each declaration. In our example, the program has two declarations (Point and Main), so the premise is satisfied when both classes check successfully.

For each class, check_class checks the fields and then each method. Let’s look at the rule for check_method:

(let MethodDecl { name: _, binder } = decl)
(let (env, vars, MethodDeclBoundData { this, inputs, output, predicates, body }) =
    env.open_universally(binder))

(let env = env.add_assumptions(
    vars.iter()
        .flat_map(|v| vec![VarianceKind::Relative.apply(v), VarianceKind::Atomic.apply(v)])
        .collect::<Vec<_>>(),
))

(check_predicates(env, predicates) => ())
(let env = env.add_assumptions(predicates))

(let ThisDecl { perm: this_perm } = &this)
(let this_ty = Ty::apply_perm(this_perm, class_ty))
(let env = env.push_local_variable(This, this_ty)?)

(let env = env.push_local_variable_decls(inputs)?)

(for_all(input in inputs)
    (let LocalVariableDecl { name: _, ty } = input)
    (check_type(env, ty) => ()))

(check_type(env, output) => ())

(check_body(env, output, body) => ())
----------------------------------- ("check_method")
(check_method(class_ty, env, decl) => ())

For our example, the method declaration for test specifies given self, so the premises compute the type given Main and push it into the environment as self. If there were other parameters, they’d be pushed too. Once the environment is ready, the final premise invokes the check_body judgment:

(let live_after = LivePlaces::default())
(can_type_expr_as(env, live_after, block, output) => ())
----------------------------------- ("block")
(check_body(env, output, MethodBody::Block(block)) => ())

The “block” rule applies to our example (the “trusted” rule handles built-in methods with no body). Its premises initialize live_after to the empty set – nothing is live after the method body returns – and then require that can_type_expr_as succeeds, checking that the body can be typed as the declared return type (Int).

Typing a block

The body of a method is a block expression, so type_expr dispatches to type_block:

(type_statements(env, live_after, statements) => (env, ty))
----------------------------------- ("place")
(type_block(env, live_after, Block { statements }) => (env, ty))

A block is a sequence of statements, so this delegates to type_statements, which walks through statements one at a time:

(let live = live_after.before(statements))
(type_statement(env, live, statement) => (env, ty))
(type_statements_with_final_ty(env, live_after, statements, ty) => (env, ty))
----------------------------------- ("cons")
(type_statements_with_final_ty(env, live_after, Cons(statement, statements), _ty) => (env, ty))

The type of the last statement becomes the type of the block.

Notice the first premise: live_after.before(&statements). Every judgment in the type system carries a live_after parameter – the set of variables that are live (i.e., used later in the program). In this chapter, nothing interesting happens with liveness because we never use our variables again. We’ll explain liveness in detail in the Giving chapter, where it determines whether a value is moved or copied.

Typing let p = new Point(22, 44)

The let statement is handled by this rule:

(type_expr(env, live_after.clone().overwritten(id), &**expr) => (env, ty)) // [1]
(let env = env.push_local_variable(id, ty)?)
(let env = env.with_in_flight_stored_to(id))
----------------------------------- ("let")
(type_statement(env, live_after, Statement::Let(id, Ascription::NoTy, expr)) => (env, Ty::unit()))

The rule has three premises:

• type_expr(env, live_after.overwritten(&id), ...) => (env, ty) – Type the right-hand side expression (new Point(22, 44)) and produce its type ty. The live_after.overwritten(&id) removes p from the live set, since p doesn’t exist yet while the RHS is being evaluated.

• env.push_local_variable(&id, ty) – Add p to the environment with the type produced by the first premise.

• env.with_in_flight_stored_to(&id) – Record that the result of the expression is now stored in p. (We’ll explain “in-flight” values in a later chapter – for now, just think of it as “the result of the expression flows into the variable”.)

Typing new Point(22, 44)

The new expression is typed by the following rule:

(let class_decl = env.program().class_named(class_name)?)

(let ClassDeclBoundData { predicates, fields, methods: _, drop_body: _ } = class_decl.binder.instantiate_with(parameters)?)

(if fields.len() == exprs.len())

(let this_ty = NamedTy::new(class_name, parameters))
(prove_predicates(env, predicates) => ())

(let (env, temp_var) = env.push_fresh_variable(this_ty))

(type_field_exprs_as(env, live_after, temp_var, exprs, fields) => env)

(let env = env.with_place_in_flight(temp_var))
(let env = env.pop_fresh_variable(temp_var))
----------------------------------- ("new")
(type_expr(env, live_after, Expr::New(class_name, parameters, exprs)) => (env, this_ty))

The premises require:

1. Looking up the class Point to find its fields: x: Int, y: Int.
2. Checking that the argument count matches the field count (2 = 2).
3. Creating a temporary variable to represent the object under construction.
4. Invoking type_field_exprs_as to type each argument against the corresponding field type – 22 against Int, 44 against Int. Both succeed via the integer typing rule:

----------------------------------- ("constant")
(type_expr(env, _live_after, Expr::Integer(_)) => (env, Ty::int()))

The “constant” rule has no premises – the conclusion type_expr(env, _, Expr::Integer(_)) => (env, Ty::int()) holds unconditionally. Any integer literal has type Int.

The conclusion of the “new” rule gives us the type Point.

After the let

After typing let p = new Point(22, 44), the environment becomes:

Typing the return expression 0

The final statement in the block is 0 – an expression statement. It is typed by this rule:

(type_expr(env, live_after, expr) => (env, ty))
(let (env, temp) = env.push_fresh_variable_with_in_flight(ty))
(env_permits_access(env, live_after, Access::Drop, temp) => env)
(parameter_permits_access(env, ty, Access::Drop, temp) => env)
(let env = env.pop_fresh_variable(temp))
----------------------------------- ("expr")
(type_statement(env, live_after, Statement::Expr(expr)) => (env, ty))

The first premise types the expression 0, yielding type Int (by the “constant” rule shown above). The remaining premises check that both the environment and the type permit dropping the temporary value. For Int, dropping is trivially permitted.

The type of the last statement (Int) becomes the type of the block. Back in check_body, the can_type_expr_as premise checks this against the declared return type Int – subtyping succeeds, and the method type-checks successfully.

What about p?

You may have noticed that we never use p. We create a Point, bind it to p, and then ignore it. The type checker is fine with this – p is never referenced after the let, so it’s not in the live set and the type checker simply ignores it.

In the next chapter, we’ll see what happens when variables are live – and how liveness determines whether a value is moved or copied.

Giving

In the previous chapter, we walked through a program that created a value and ignored it. Now we’ll see what happens when you actually use a value – and how the type checker decides whether that’s allowed.

Place expressions

In Dada, values are accessed through place expressions like d.give. A place expression combines a place (a variable, possibly with field projections) and an access mode (what you want to do with the value):

#[term($place . $access)]
pub struct PlaceExpr {
    pub place: Place,
    pub access: Access,
}

A place is a variable with zero or more field projections:

#[term($var $*projections)]
pub struct Place {
    pub var: Var,
    pub projections: Vec<Projection>,
}

A projection is a field access:

#[term]
pub enum Projection {
    #[grammar(. $v0 $!)]
    #[cast]
    Field(FieldId),

    #[grammar([ $v0 ] $!)]
    Index(usize),
}

The access mode determines what kind of access is being performed:

#[term]
#[derive(Copy, Default)]
pub enum Access {
    #[default]
    #[grammar(ref)]
    Rf,

    #[grammar(give)]
    Gv,

    #[grammar(mut)]
    Mt,

    #[grammar(drop)]
    Drop,
}

We’ll start with give, which is the most fundamental.

Giving a value

If you are familiar with Rust, give is analogous to a move. When you give a value, you transfer ownership of it. The following program creates a Data value and gives it away as the return value:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) -> Data {
                let d = new Data();
                d.give;
            }
        }
    }
);

The give place rule

A place expression like d.give is typed by this rule:

(access_permitted(env, live_after, Access::Gv, place) => env)
(let ty = env.place_ty(place)?)
(move_place(env, live_after, place, ty) => env)
----------------------------------- ("give place")
(type_expr(env, live_after, PlaceExpr { access: Access::Gv, place }) => (env, ty))

The rule has three premises:

• access_permitted(env, ..., Access::Gv, &place) => env – Check that giving this place is permitted. This verifies that no other live variable holds a conflicting borrow or lien on the place. (In this simple example, nothing does.) The judgment returns an updated environment.

• env.place_ty(&place) – Look up the type of d in the environment: Data.

• move_place(&env, &live_after, &place, &ty) => env – Decide whether to move or copy the value, returning an updated environment that reflects the result. This is where liveness matters.

Liveness

In the previous chapter, we mentioned that every judgment carries a live_after parameter – the set of places that are used later in the program. Nothing interesting happened with liveness there because we never used our variables again. Now it becomes central.

How liveness is computed

Recall the type_statements_with_final_ty rule that walks through a block’s statements. Its first premise is live_after.before(&statements), which computes what’s live before the current statement by scanning forward through the remaining statements:

flowchart LR
    subgraph block ["{ s_0 ; s_1 ; s_2 }"]
        s0["s_0"] --> s1["s_1"] --> s2["s_2"]
    end
    block --> after
    after["... more code ..."]
    after -. "live_after = L<br/>(vars used by ...)" .-> block
    s2 -. "L(s_2) = <br> L ∪ vars used by s_2" .-> s1
    s1 -. "L(s_1) = <br> L(s_2) ∪ vars used by s_1" .-> s0

live_after captures what the code after the block needs. But a block isn’t atomic – it has internal structure. So when processing s_0, the type checker extends live_after by scanning forward through the remaining statements [s_1, s_2] and collecting every place they reference. This tells each judgment which places are still needed and which are free to be moved.

The move_place judgment

The move_place judgment uses liveness to decide whether giving a place moves or copies its value:

move_place(env: Env, live_after: LivePlaces, place: Place, ty: Ty,) => Env

Notice the return type: move_place takes an Env and returns an updated Env. Many judgments in the type system work this way – they thread the environment through, and the returned environment reflects any changes (like marking a place as moved).

The judgment has two rules. Which one applies depends on whether the place is live.

The “give” rule applies when the place is not live afterward – no later code needs this place, so the value can be moved. Its premise env.with_place_in_flight(&place) produces a new environment where the place is marked as moved:

(if !live_after.is_live(place))
(let env = env.with_place_in_flight(place))
----------------------------------- ("give")
(move_place(env, live_after, place, _ty) => env)

The “copy” rule applies when the place is still live – later code will use it, so the value must stay. Its premise requires prove_is_copy, which succeeds for types like Int or shared class types. If the type isn’t copyable, this premise fails and the type check fails:

(if live_after.is_live(place))!
(prove_is_copy(env, ty) => ())
----------------------------------- ("copy")
(move_place(env, _live_after, _place, ty) => env)

Applying it to d.give

In our example:

let d = new Data();
d.give;

When the type checker reaches d.give, live_after is {} – nothing comes after the method returns. So d is not live, the “give” rule applies, and the returned environment has d marked as in-flight (moved).

Giving a value twice is an error

Once a value has been given away, it is gone. Trying to use it again is an error:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self) -> Data {
                let d = new Data();
                d.give;
                d.give;
            }
        }
    },
    expect_test::expect![[r#"
        the rule "give" at (expressions.rs) failed because
          condition evaluted to false: `!live_after.is_live(place)`
            live_after = LivePlaces { accessed: {d}, traversed: {} }
            place = d"#]]
);

This time, when we process the first d.give, the remaining statement is the second d.give, which references d. So d is live, and the “copy” rule fires instead. But Data is a class (not a shared class), so it doesn’t satisfy prove_is_copy – the type check fails.

This is the same principle as Rust’s move semantics – after a move, the original binding is no longer valid.

Giving a field

You can give individual fields from a class instance. After giving a field, that specific field is no longer available, but other fields remain accessible:

crate::assert_ok!(
    {
        class Data { }

        class Pair {
            a: Data;
            b: Data;
        }

        class Main {
            fn test(given self) -> Data {
                let p = new Pair(new Data(), new Data());
                p.a.give;
                p.b.give;
            }
        }
    }
);

When processing p.a.give, the live set includes p.b (because the next statement references it), but p.a is not live – nothing after this point uses p.a. So the “give” rule fires for p.a.

Then when processing p.b.give, nothing is live afterward, so the “give” rule fires again for p.b.

Giving a field and then the whole value is an error

If you give away a field, the whole value is now incomplete, so you can’t give the whole thing:

crate::assert_err!(
    {
        class Data { }

        class Pair {
            a: Data;
            b: Data;
        }

        class Main {
            fn test(given self) -> Pair {
                let p = new Pair(new Data(), new Data());
                p.a.give;
                p.give;
            }
        }
    },
    expect_test::expect![[r#"
        the rule "give" at (expressions.rs) failed because
          condition evaluted to false: `!live_after.is_live(place)`
            live_after = LivePlaces { accessed: {p}, traversed: {} }
            place = p . a"#]]
);

When processing p.a.give, the next statement is p.give, which references p. Since p.a overlaps with p, the liveness check is_live(p.a) returns true – p.a is live because p (which includes p.a) will be used. The “copy” rule fires, Data isn’t copyable, and the check fails.

Conversely, if you give the whole value, you can’t access its fields afterward:

crate::assert_err!(
    {
        class Data { }

        class Pair {
            a: Data;
            b: Data;
        }

        class Main {
            fn test(given self) -> Data {
                let p = new Pair(new Data(), new Data());
                p.give;
                p.a.give;
            }
        }
    },
    expect_test::expect![[r#"
        the rule "give" at (expressions.rs) failed because
          condition evaluted to false: `!live_after.is_live(place)`
            live_after = LivePlaces { accessed: {p . a}, traversed: {} }
            place = p"#]]
);

Here, when processing p.give, the next statement references p.a. Since p is a prefix of p.a, is_live(p) returns true. Same result: the “copy” rule fires, Pair isn’t copyable, failure.

Shared classes are copyable

Unlike regular class instances, shared class values are always shared and can be given multiple times. Int is a built-in shared class, so this works fine:

crate::assert_ok!(
    {
        class Main {
            fn test(given self) -> Int {
                let x = 22;
                x.give;
                x.give;
            }
        }
    }
);

When processing the first x.give, the second x.give references x, so x is live. The “copy” rule fires – but this time Int is a shared class type, so prove_is_copy succeeds, and the value is copied rather than moved.

Sharing

In the previous chapter, we saw that giving a non-copyable value moves it – after a give, the original is gone. We also saw that shared class types like Int are copyable and can be given multiple times. But what about regular classes? What if you want to use a value in multiple places without giving up ownership?

That’s what sharing is for.

Sharing a value

The .share operator converts a value from unique (given) ownership to shared ownership. Once shared, a value can be freely copied:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) -> shared Data {
                let d = new Data();
                let s = d.give.share;
                s.give;
                s.give;
            }
        }
    }
);

Compare this with the giving a value twice example from the previous chapter, which failed. The difference is .share – it transforms the Data value so that subsequent gives copy rather than move.

The share expr rule

The type checker handles .share with this rule:

(type_expr(env, live_after, &**expr) => (env, ty))
(prove_is_shareable(env, ty) => ())
----------------------------------- ("share expr")
(type_expr(env, live_after, Expr::Share(expr)) => (env, Ty::apply_perm(Perm::Shared, ty)))

The rule has two premises:

• type_expr(env, ..., &*expr) => (env, ty) – Type-check the inner expression, producing a type ty.

• prove_is_shareable(&env, &ty) => () – Verify that the type is allowed to be shared. Not all types can be shared – given classes cannot.

If both premises succeed, the result type is shared ty – the original type wrapped with the shared permission.

Shareability and class predicates

Whether a type can be shared depends on its class predicate. Classes come in three flavors:

#[term]
#[derive(Copy, Default)]
pub enum ClassPredicate {
    /// `Given` classes are permitted to have destructors (FIXME: we don't model those right now).
    /// A `Given` class cannot be shared and, since they have a destructor, we cannot drop them
    /// from borrow chains (i.e., `mut[guard] mut[data]` cannot be converted to `mut[data]`
    /// even if `guard` is not live since, in fact, the variable *will* be used again by the dtor).
    #[grammar(given)]
    Given,

    /// `Share` classes are the default. They indicate classes that, while unique by default,
    /// can be shared with `.give.share` to create a `shared Class` that is copyable around.
    #[default]
    Share,

    /// `Shared` classes are value types that are always considered shared
    /// and hence can be copied freely. However, their fields
    /// cannot be individually mutated as a result.
    #[grammar(shared)]
    Shared,
}

The prove_is_shareable judgment delegates to the general predicate-proving machinery:

(prove_predicate(env, Predicate::share(a)) => ())
---------------------------- ("is")
(prove_is_shareable(env, a) => ())

For a regular class like Data, the Share predicate is satisfied by default, so .share succeeds.

Shared values are copyable

Once a value is shared, the move_place judgment from the giving chapter treats it differently. Recall that move_place has two rules – “give” (move) and “copy”. The “copy” rule requires prove_is_copy:

(if live_after.is_live(place))!
(prove_is_copy(env, ty) => ())
----------------------------------- ("copy")
(move_place(env, _live_after, _place, ty) => env)

A shared Data type satisfies prove_is_copy because the shared permission is a copy permission. So when you write s.give on a shared value, the “copy” rule fires and the value is copied rather than moved.

This is why the example above works – both s.give expressions copy the shared value.

Shared classes are always shared

In the previous chapter, we saw that Int values can be given multiple times. That’s because Int is a shared class type – it has the Shared class predicate, which means it is always shared and copyable without needing an explicit .share:

crate::assert_ok!(
    {
        shared class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn test(given self) -> Point {
                let p = new Point(22, 44);
                p.give;
                p.give;
            }
        }
    }
);

Shared classes are always copyable, but their fields cannot be individually mutated. Regular classes are mutable by default but require .share to become copyable.

Given classes cannot be shared

Given classes cannot be shared. Attempting to share a given class is an error:

crate::assert_err!(
    {
        given class Resource { }

        class Main {
            fn test(given self) -> shared Resource {
                let r = new Resource();
                r.give.share;
            }
        }
    },
    expect_test::expect![[r#"
        the rule "share class" at (predicates.rs) failed because
          pattern `true` did not match value `false`"#]]
);

The prove_is_shareable premise fails because Resource has the Given predicate, which does not satisfy share(Resource).

Sharing is idempotent

Sharing an already-shared value is fine – it’s a no-op:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) -> shared Data {
                let d = new Data();
                d.give.share.share;
            }
        }
    }
);

The inner .share produces shared Data. The outer .share checks prove_is_shareable on shared Data, which succeeds because a shared permission is always shareable. The result is still shared Data – applying shared to an already-shared type normalizes to the same type.

Borrowing with ref

In the previous chapter, we saw how give transfers ownership of a value. But sometimes you want to use a value without giving it away. That’s what ref is for – it creates a shared reference that lets you read the value while the original stays put.

A simple borrow

Here’s a program that creates a Foo value, borrows it with ref, and then uses both the original and the borrow:

crate::assert_ok!(
    {
        class Data { }

        class Foo {
            i: Data;
        }

        class Main {
            fn test(given self) {
                let foo = new Foo(new Data());
                let bar = foo.ref;
                let i = foo.i.ref;
                bar.give;
                ();
            }
        }
    }
);

This works! After foo.ref, we can still access foo.i – reading through a shared reference doesn’t prevent further reads. Let’s walk through how the type checker handles this.

Typing foo.ref

When the type checker sees foo.ref, it matches the ref|mut place rule:

[rule ref|mut place not found in type_expr]

The rule has three premises:

• access_permitted(env, ..., Access::Rf, &place) => env – Check that borrowing foo is permitted. This consults the liens on all live variables to verify that no conflicting access is active.

• env.place_ty(&place) – Look up the type of foo: Foo.

• access_ty(&env, Access::Rf, &place, ty_place) => ty – Compute the result type by wrapping the place’s typ with a ref permission.

The access_ty judgment for ref works like this:

(let perm = Perm::rf(set![place]))
----------------------------------- ("ref")
(access_ty(_env, Access::Rf, place, ty) => Ty::apply_perm(perm, ty.strip_perm()))

It creates the permission ref[foo] and applies it to the place’s type (with the outermost permission stripped). So foo.ref has type ref[foo] Foo.

Notice that the permission carries the place it was borrowed from. This is the key idea: ref[foo] means “a shared reference that borrows from foo.” The type system uses this to restrict what you can do with foo while the reference is alive.

How access control works

The interesting premise is access_permitted. How does the type checker decide whether an access is allowed?

When we reach foo.i.ref (the third line of the block), the environment looks like this:

The type checker needs to confirm that accessing foo.i with ref is compatible with all live variables. The key judgment is env_permits_access:

(let live_var_tys: Vec<Ty> = live_after.vars().iter().map(|var| env.var_ty(var).unwrap()).cloned().collect())
(parameters_permit_access(env, live_var_tys, access, place) => env)
(accessed_place_permits_access(env, live_after, access, place) => env)
-------------------------------- ("env_permits_access")
(env_permits_access(env, live_after, access, place) => env)

It collects the types of all live variables and checks that each one permits the access. In our example, bar is live (used later by bar.give), so its type ref[foo] Foo is checked.

Liens

To check whether bar’s type permits accessing foo.i, the type checker first extracts the liens from the type. Liens are the borrowing constraints embedded in a type:

#[term]
pub enum Lien {
    Rf(Place),
    Mt(Place),
}

A Lien::Rf(place) means “a read-only borrow of place.” A Lien::Mt(place) means “a mutable borrow of place.”

The liens judgment extracts liens from permissions:

----------------------------------- ("perm-shared")
(liens(_env, Perm::Shared) => ())

For Perm::Rf(places), it creates a Lien::Rf for each place. So ref[foo] Foo yields the lien Lien::Rf(foo).

The ref'd rule

Once the liens are extracted, each lien is checked against the access. For a Lien::Rf, the ref'd rule delegates to ref_place_permits_access:

(ref_place_permits_access(place, access, accessed_place) => ())
-------------------------------- ("ref'd")
(lien_permit_access(env, Lien::Rf(place), access, accessed_place) => env)

The rules for what a ref lien permits are:

ref_place_permits_access(shared_place: Place, access: Access, accessed_place: Place,) => ()

Three rules:

• share-share: A ref lien permits any ref or share access to any place – reading is always compatible with reading.

• share-mutation: A ref lien permits mut or drop access only to places disjoint from the borrowed place. You can mutate something unrelated, but not the borrowed data.

• share-give: A ref lien permits give access only to places that are disjoint from or a prefix of the borrowed place. (Giving away the prefix cancels the borrow.)

Applying it to our example

When checking foo.i.ref against the lien Lien::Rf(foo):

• The access is ref (Access::Rf)
• The share-share rule fires – ref is always compatible with ref
• Access is permitted

That’s why the program works.

Mutation through a ref is an error

A ref creates a read-only borrow. If you try to mutably borrow a field while a ref is active, the type checker rejects it:

crate::assert_err!(
    {
        class Data { }

        class Foo {
            i: Data;
        }

        class Main {
            fn test(given self) {
                let foo = new Foo(new Data());
                let bar = foo.ref;
                let i = foo.i.mut;
                bar.give;
                ();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "share-mutation" at (accesses.rs) failed because
          condition evaluted to false: `place_disjoint_from(accessed_place, shared_place)`
            accessed_place = foo . i
            shared_place = foo"#]]
);

Here the access is mut (Access::Mt), so the share-mutation rule applies. It requires foo.i to be disjoint from the borrowed place foo. But foo.i is a sub-place of foo – not disjoint – so the check fails.

This is the fundamental guarantee of shared references: while a ref to foo exists, you cannot mutate foo or any of its fields.

Giving a field away while ref’d is an error

Similarly, you can’t give away a field of a ref’d value:

crate::assert_err!(
    {
        class Data { }

        class Foo {
            i: Data;
        }

        class Main {
            fn test(given self) {
                let foo = new Foo(new Data());
                let bar = foo.ref;
                let i = foo.i.give;
                bar.give;
                ();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "share-give" at (accesses.rs) failed because
          condition evaluted to false: `place_disjoint_from_or_prefix_of(accessed_place, shared_place)`
            accessed_place = foo . i
            shared_place = foo"#]]
);

The share-give rule requires the accessed place to be disjoint from or a prefix of the borrowed place. foo.i is neither disjoint from nor a prefix of foo (it’s a suffix), so the check fails.

Why the “prefix” exception? Giving away foo itself would cancel the borrow – the reference can’t outlive what it borrows. But giving away foo.i would leave foo in a partially-moved state while bar still refers to it.

Liveness cancels restrictions

Liens only matter while the borrowing variable is live – that is, while later code might use it. Once the borrower dies, its restrictions vanish:

crate::assert_ok!(
    {
        class Data { }

        class Foo {
            i: Data;
        }

        class Main {
            fn test(given self) {
                let foo = new Foo(new Data());
                let bar = foo.mut;
                let i = foo.i.ref;
                ();
            }
        }
    }
);

Wait – bar is a mutable borrow of foo, and we’re taking a ref of foo.i! Normally a mut lien blocks all access (even reads) to the borrowed place and its sub-places. But bar is never used after the let i = ... line.

When the type checker reaches foo.i.ref, it collects the types of all live variables. Since bar is not live (nothing references it afterward), its type mut[foo] Foo is not in the checked set. No liens, no restrictions, access is permitted.

This is analogous to Rust’s non-lexical lifetimes (NLL) – borrows end when the reference is last used, not when it goes out of scope.

Mutable borrows are more restrictive

For comparison, here’s how mut liens differ from ref liens. A mut lien blocks all access (even reads) to overlapping places:

mut_place_permits_access(leased_place: Place, access: Access, accessed_place: Place,) => ()

• lease-mutation: A mut lien permits share, ref, mut, or drop access only to places disjoint from the leased place. No reads, no shares, no further borrows of the leased data.

• lease-give: A mut lien permits give access only to places that are disjoint from or a prefix of the leased place.

That’s why this fails:

crate::assert_err!(
    {
        class Data { }

        class Foo {
            i: Data;
        }

        class Main {
            fn test(given self) {
                let foo = new Foo(new Data());
                let bar = foo.mut;
                let i = foo.i.ref;
                bar.give;
                ();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "lease-mutation" at (accesses.rs) failed because
          condition evaluted to false: `place_disjoint_from(accessed_place, leased_place)`
            accessed_place = foo . i
            leased_place = foo"#]]
);

bar is live (used by bar.give), so its Lien::Mt(foo) is active. The lease-mutation rule requires foo.i to be disjoint from foo – it isn’t, so the access is rejected.

Disjoint access is fine

Both ref and mut liens permit access to disjoint places. Borrowing foo doesn’t prevent you from touching unrelated data:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let foo = new Data();
                let other = new Data();
                let bar = foo.ref;
                other.give;
                bar.give;
                ();
            }
        }
    }
);

bar borrows foo, creating the lien Lien::Rf(foo). When we give other, the share-give check asks: is other disjoint from foo? Yes – they’re different variables. Access is permitted.

Transitive restrictions

Liens compose transitively. If you borrow from a borrow, the original restrictions still apply:

crate::assert_err!(
    {
        class Data { }

        class Foo {
            i: Data;
        }

        class Main {
            fn test(given self) {
                let p = new Foo(new Data());
                let q = p.mut;
                let r = q.ref;
                let i = p.i.ref;
                r.give;
                ();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "lease-mutation" at (accesses.rs) failed because
          condition evaluted to false: `place_disjoint_from(accessed_place, leased_place)`
            accessed_place = p . i
            leased_place = p"#]]
);

Here q has type mut[p] Foo and r has type ref[q] Foo. When we try p.i.ref, the type checker checks r’s type. The liens of ref[q] Foo include Lien::Rf(q) – but also the liens from looking up q’s type mut[p] Foo, which yields Lien::Mt(p).

So even though r only directly references q, the chain of borrows transitively propagates the restriction back to p. The lease-mutation rule blocks p.i.ref because p.i is not disjoint from p.

Note that q itself is dead here (nothing uses q after let r). But the type of r still records the transitive dependency on p, and r is live.

Summary

The access control system enforces these constraints through three mechanisms:

1. Liens extracted from the types of live variables
2. Disjointness checks that determine whether two places overlap
3. Liveness that automatically cancels restrictions when the borrower is no longer used

Subtyping

In the previous chapters, we saw how types carry permissions and how borrowing creates new permission types like ref[place]. But we glossed over an important question: what happens when a value’s type doesn’t exactly match what’s expected?

That’s where subtyping comes in. Subtyping lets one type stand in for another when the substitution is safe.

A motivating example

Here’s a simple function that creates a Data value and returns it:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) -> Data {
                let d: given Data = new Data();
                d.give;
            }
        }
    }
);

The annotation let d: given Data makes the permission explicit, but the return type is just Data – no permission written. These match because given is the default permission. When you write Data without a permission, the type checker treats it as given Data. So both sides are given Data, and subtyping is trivially satisfied.

But what about less trivial cases? Consider a function that borrows a value and returns the reference:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) -> ref[d] Data {
                d.ref;
            }
        }
    }
);

The expression d.ref creates a reference with type ref[d] Data. The return type is also ref[d] Data – an exact match. But internally, the type checker needs to verify that the permission ref[d] on the expression’s type is compatible with the permission ref[d] on the return type. That verification happens through permission reduction – a process we’ll explain in this chapter.

When subtyping happens

Subtyping is invoked through the type_expr_as judgment, which checks that an expression’s type is a subtype of some expected type: ok

(type_expr(env, live_after, expr) => (env, ty))
(sub(env, live_after, ty, as_ty) => ())
-------------------------------- ("type_expr_as")
(type_expr_as(env, live_after, expr, as_ty) => env)

The judgment first computes the expression’s type with type_expr, then calls sub to verify it’s a subtype of the expected type.

This happens in three situations:

• Return types – the body of a method is checked against the declared return type.
• Let bindings with type annotations – let x: T = expr checks that the expression’s type is a subtype of T.
• Method arguments and field initialization – each argument’s type must be a subtype of the declared parameter type.

Type subtyping: same class required

Dada has no class hierarchy – there’s no equivalent of Java’s extends or Rust’s trait objects. Subtyping only works between types with the same class name. The difference is always in the permissions.

The sub judgment handles this through the “sub-classes” rule:

(if let Ty::NamedTy(NamedTy { name: name_a, parameters: parameters_a }) = ty_a)
(if let Ty::NamedTy(NamedTy { name: name_b, parameters: parameters_b }) = ty_b)
(if name_a == name_b)!
(sub_perms(env, live_after, perm_a, perm_b) => ())
(let variances = env.variances(name_a)?)
(if parameters_a.len() == variances.len())
(if parameters_b.len() == variances.len())
(for_all(triple in izip!(variances, parameters_a, parameters_b))
    (let (v, pa, pb) = triple)
    (sub_generic_parameter(env, live_after, v, perm_a, pa, perm_b, pb) => ()))
------------------------------- ("sub-classes")
(sub(env, live_after, PermTy(perm_a, ty_a), PermTy(perm_b, ty_b)) => ())

The rule requires matching class names and then delegates to sub_perms for the permission comparison.

Different classes are incompatible

If the class names don’t match, subtyping fails:

crate::assert_err!(
    {
        class Foo { }
        class Bar { }

        class Main {
            fn test(given self) {
                let f = new Foo();
                let b: Bar = f.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Foo { } class Bar { } class Main { fn test (given self) -> () { let f = new Foo () ; let b : Bar = f . give ; () ; } } }`"]
);

There is no rule that can prove Foo <: Bar – the “sub-classes” rule requires name_a == name_b, and Foo and Bar are different names.

Reduced permissions

The sub_perms judgment doesn’t compare permissions directly. Instead, it first reduces each permission into a canonical form called a RedPerm, then compares the reduced forms.

Why not compare permissions directly? Because permissions as written in source code have structure – composition, place sets, liveness dependencies – that makes direct comparison impractical. Reduction normalizes all of this into a uniform representation.

What is a RedPerm?

A RedPerm is a set of RedChains. Each RedChain is a sequence of RedLinks. Links are the atomic building blocks of reduced permissions:

Notice the live/dead distinction: ref[d] reduces to Rfl(d) if d is still used later in the program, and Rfd(d) if it isn’t. The same for mut[d] → Mtl(d) or Mtd(d). This distinction matters for permission comparison – dead permissions can be cancelled or promoted, as we’ll see in the Liveness and cancellation chapter.

Reducing simple permissions

The simplest reductions are direct translations:

• given → one chain: [] (the empty chain). No links – just ownership. This is the identity permission.

• shared → one chain: [Shared]. A single link indicating shared ownership.

• ref[d] (where d is live) → one chain: [Rfl(d)]. A single reference link.

• mut[d] (where d is live) → one chain: [Mtl(d)]. A single mutable lease link.

Multi-place permissions become multiple chains

When a permission mentions multiple places, it produces one chain per place. This is why RedPerm is a set of chains:

• ref[d1, d2] → two chains: { [Rfl(d1)], [Rfl(d2)] }.

The set representation means that ref[d1, d2] describes a permission that could be borrowing from d1 or d2 (or both). For the subtype to hold, every chain in the subtype’s RedPerm must be matched by some chain in the supertype’s RedPerm.

Composition: how permissions combine

Permissions combine when you access a field through a borrowed or leased value. If r has type ref[d] Outer and Outer has a field i: Inner, then r.i has type ref[d] Inner – the ref[d] permission wraps the field’s type.

Internally, this creates a composed permission: Perm::Apply(ref[d], given) – the outer ref[d] applied to the field’s given permission. How does reduction handle this?

The append_chain rule

When reducing a composed permission P Q, the type checker reduces P and Q separately, then appends the chains using append_chain.

The rule has two cases:

• If the right-hand chain is copy (Shared, Rfl, etc.): the left-hand side is discarded. Copy permissions absorb anything applied to them.

• If the right-hand chain is NOT copy (given, Mtl, etc.): the chains are concatenated into a longer chain.

Example: ref[d] applied to given

Consider accessing a field through a reference:

crate::assert_ok!(
    {
        class Inner { }

        class Outer {
            i: Inner;
        }

        class Main {
            fn test(given self, d: given Outer) -> ref[d] Inner {
                let r: ref[d] Outer = d.ref;
                r.i.give;
            }
        }
    }
);

The expression r.i has type ref[d] Inner – but internally, the field i has type Inner (which is given Inner), and accessing it through r: ref[d] Outer composes them.

Reduction of the composed permission:

• ref[d] → [Rfl(d)]
• given → [] (empty chain, not copy)
• Append: [Rfl(d)] ++ [] = [Rfl(d)]

The given disappears. Since the empty chain represents identity, appending it to anything is a no-op. This is why ref[d] given Inner and ref[d] Inner are equivalent – given is the identity permission.

Example: ref[w] applied to shared (copy absorbs)

Now consider a field whose type is a shared class:

crate::assert_ok!(
    {
        shared class Point {
            x: Int;
            y: Int;
        }

        class Wrapper {
            p: Point;
        }

        class Main {
            fn test(given self, w: given Wrapper) -> Point {
                let r: ref[w] Wrapper = w.ref;
                r.p.give;
            }
        }
    }
);

The field p has type Point, which is a shared class. Accessing r.p through r: ref[w] Wrapper composes ref[w] with shared (the permission of Point).

Reduction:

• ref[w] → [Rfl(w)]
• shared → [Shared] (copy!)
• Append: [Rfl(w)] ++ [Shared] → [Shared]

The ref[w] is discarded. Because shared is a copy permission, the append_chain rule drops the left-hand side entirely. The result is just [Shared] – plain shared ownership.

This makes intuitive sense: if the field is already shared (freely copyable), borrowing from its container doesn’t restrict anything. You just get a shared copy.

That’s why r.p.give has type Point (i.e., shared Point) even though we accessed it through a reference – the ref[w] was absorbed by the shared.

Example: ref[p] applied to mut[d]

Now consider borrowing from a mutable lease:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d: given Data = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] mut[d] Data = p.ref;
                ();
            }
        }
    }
);

The expression p.ref has type ref[p] Data, and p has type mut[d] Data. If we were to access a field of this value, the composed permission would be Apply(ref[p], mut[d]).

Reduction:

• ref[p] → [Rfl(p)]
• mut[d] → [Mtl(d)] (not copy!)
• Append: [Rfl(p)] ++ [Mtl(d)] = [Rfl(p), Mtl(d)]

This is a genuine two-link chain. The mut[d] is not copy, so it doesn’t absorb – the chain records both links. This chain means “a reference to p, which is itself a mutable lease from d.”

Whether this chain can match some target permission depends on liveness and cancellation rules – if p is dead, the Rfl(p) link can potentially be resolved. That’s covered in the Liveness and cancellation chapter.

How comparison works

The sub_perms judgment ties it all together:

(red_perm(env, live_after, perm_a) => red_perm_a)
(red_perm(env, live_after, perm_b) => red_perm_b)
(for_all(red_chain_a in red_perm_a.chains.clone())
    (red_chain_sub_perm(env, red_chain_a, red_perm_b) => ()))
--- ("sub_red_perms")
(sub_perms(env, live_after, perm_a, perm_b) => ())

1. Reduce both permissions to RedPerms
2. For every chain in the subtype’s RedPerm, find a matching chain in the supertype’s RedPerm

“Matching” means red_chain_sub_chain – a judgment with rules for each kind of link comparison. The Subtypes and subpermissions chapter walks through these rules in detail:

• Place ordering – ref[d.f] <: ref[d] because sub-places are more specific.
• Copy permissions – shared <: ref[d] because shared ownership is stronger than borrowing.
• Liveness and cancellation – dead links can be dropped or promoted during comparison.

Shared classes and permission distribution

Shared classes get a special subtyping rule. Because a shared class’s direct fields must already be shared (copy) types, the outer permission only matters insofar as it affects the type parameters.

Consider Int – a shared class with no type parameters:

crate::assert_ok!(
    {
        class Main {
            fn test(given self) -> Int {
                let x: ref[self] Int = 0;
                x.give;
            }
        }
    }
);

ref[self] Int <: Int – a borrow of an Int is just an Int.

This works in both directions:

crate::assert_ok!(
    {
        class Main {
            fn test(given self) -> Int {
                let x: Int = 0;
                let y: ref[self] Int = x.give;
                y.give;
            }
        }
    }
);

Int <: ref[self] Int also holds.

The “sub-shared-classes” rule

The rule that makes this work is:

(if let Ty::NamedTy(NamedTy { name: name_a, parameters: parameters_a }) = ty_a)
(if let Ty::NamedTy(NamedTy { name: name_b, parameters: parameters_b }) = ty_b)
(if name_a == name_b)
(if let true = env.is_shared_ty(name_a)?)!
(if parameters_a.len() == parameters_b.len())
(for_all(pair in parameters_a.iter().zip(parameters_b))
    (let (pa, pb) = pair)
    (sub(env, live_after, perm_a.apply_to_parameter(pa), perm_b.apply_to_parameter(pb)) => ()))
------------------------------- ("sub-shared-classes")
(sub(env, live_after, PermTy(perm_a, ty_a), PermTy(perm_b, ty_b)) => ())

For shared classes, the rule distributes the outer permission into the type parameters. To check A SharedClass[B] <: X SharedClass[Y], it checks A B <: X Y for each parameter pair.

The key insight: when a shared class has zero type parameters (like Int), there’s nothing to distribute into. The for_all over parameters is vacuously true – so the subtyping holds regardless of what permissions A and X are. The outer permission is irrelevant because there are no type parameters for it to affect.

Shared classes with copy parameters

The same rule extends to shared classes with parameters, as long as those parameters are copy types:

crate::assert_ok!(
    {
        shared class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn test(given self) -> Point {
                let p: shared Point = new Point(1, 2);
                p.give;
            }
        }
    }
);

shared Point <: Point works because the rule distributes: it checks shared Int <: given Int for each parameter. Since Int is itself a shared class with no parameters, that check is vacuously true.

Non-copy parameters block erasure

But if a shared class wraps a non-copy type, the outer permission matters – it distributes into the type parameter and changes the meaning:

crate::assert_err!(
    {
        shared class Box[ty T] {
            value: T;
        }

        class Data { }

        class Main {
            fn test(given self, d: given Data) -> Box[Data] {
                let b: ref[d] Box[Data] = new Box[Data](new Data());
                b.give;
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: shared class Box [ty] { value : ^ty0_0 ; } class Data { } class Main { fn test (given self d : given Data) -> Box[Data] { let b : ref [d] Box[Data] = new Box [Data] (new Data ()) ; b . give ; } } }`"]
);

ref[d] Box[Data] </: Box[Data] fails because the rule distributes: it needs ref[d] Data <: Data. But Data is a regular class (not a shared class), so ref[d] cannot be erased. A borrowed Data is genuinely different from an owned Data.

Summary

Subtyping in Dada operates on permissions, not class hierarchies. Two types are related by subtyping only when they name the same class, and the key question is whether one permission can stand in for another.

The process:

1. Decompose each type into permission + base type
2. Reduce each permission to a RedPerm (a set of RedChains)
3. Compare chain by chain – every chain in the subtype must match some chain in the supertype

Composition flattens through append_chain: copy permissions absorb anything applied to them, while non-copy permissions concatenate into longer chains.

Shared classes get special treatment: permissions distribute into type parameters, and classes with no parameters (like Int) make the permission check vacuous.

Subtypes and subpermissions

In the previous chapter, we saw how subtyping works: the type checker reduces permissions to RedPerms (sets of RedChains) and then compares them chain by chain.

This chapter dives into the red_chain_sub_chain judgment – the rules that determine whether one chain can stand in for another.

The topics:

• Place ordering – how sub-places and place sets create a partial order on permissions.
• Copy permissions – the three copy permissions (shared, ref[d], shared mut[d]), how they relate, and how they compose.
• Liveness and cancellation – how dead links are resolved during comparison.

Place ordering

Permissions in Dada carry places – they record where a borrow or lease comes from. These places create a natural ordering on permissions: more specific places are subtypes of less specific ones.

There are two dimensions to this ordering: sub-places (field projections) and place sets (multiple sources).

Sub-place ordering

A borrow from a field is more specific than a borrow from the whole object. If you borrow d.left, that’s a tighter restriction than borrowing all of d:

crate::assert_ok!(
    {
        class Data {
            left: given Data;
            right: given Data;
        }

        class Main {
            fn test(given self, d: given Data) {
                let r: ref[d] Data = d.left.ref;
                ();
            }
        }
    }
);

The expression d.left.ref has type ref[d.left] Data, but the annotation on r expects ref[d] Data. This works because d is a prefix of d.left – a reference that borrows from d.left certainly borrows from somewhere within d.

The same principle applies to mutable leases:

crate::assert_ok!(
    {
        class Data {
            left: given Data;
            right: given Data;
        }

        class Main {
            fn test(given self, d: given Data) {
                let r: mut[d] Data = d.left.mut;
                ();
            }
        }
    }
);

mut[d.left] <: mut[d] – a lease of a field is a subtype of a lease of the parent.

The reverse fails

Going the other direction doesn’t work. A borrow from all of d can’t promise it only borrows from d.left:

crate::assert_err!(
    {
        class Data {
            left: given Data;
            right: given Data;
        }

        class Main {
            fn test(given self, d: given Data) {
                let r: ref[d.left] Data = d.ref;
                ();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "(ref::P) vs (ref::P)" at (redperms.rs) failed because
          condition evaluted to false: `place_b.is_prefix_of(place_a)`
            place_b = d . left
            place_a = d"#]]
);

ref[d] </: ref[d.left] – d.left is not a prefix of d, so the prefix check fails.

The rule

The chain comparison rule that handles sub-places is:

(if place_b.is_prefix_of(place_a))
(red_chain_sub_chain(env, tail_a, tail_b) => ())
--- ("(ref::P) vs (ref::P)")
(red_chain_sub_chain(
    env,
    Head(RedLink::Rfl(place_a) | RedLink::Rfd(place_a), Tail(tail_a)),
    Head(RedLink::Rfl(place_b) | RedLink::Rfd(place_b), Tail(tail_b)),
) => ())

It requires place_b.is_prefix_of(&place_a) – the supertype’s place must be a prefix of (or equal to) the subtype’s place. There’s an analogous rule for mut:

(if place_b.is_prefix_of(place_a))
(red_chain_sub_chain(env, tail_a, tail_b) => ())
--- ("(mut::P) vs (mut::P)")
(red_chain_sub_chain(
    env,
    Head(RedLink::Mtl(place_a) | RedLink::Mtd(place_a), Tail(tail_a)),
    Head(RedLink::Mtl(place_b) | RedLink::Mtd(place_b), Tail(tail_b)),
) => ())

Place sets

Permissions can mention multiple places. ref[d1, d2] means “a reference that may borrow from d1 or d2” – which means both d1 and d2 must be kept unmodified.

A permission that restricts fewer places is a subtype of one that restricts more:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self, d1: given Data, d2: given Data) {
                let r: ref[d1, d2] Data = d1.ref;
                ();
            }
        }
    }
);

ref[d1] <: ref[d1, d2] – the subtype restricts d1; the supertype restricts both d1 and d2. The supertype is more restrictive, so it’s safe to use the subtype in its place.

This might feel backwards at first, but think about it from the caller’s perspective: if you hold a ref[d1, d2] Data, you know not to modify d1 or d2. If the actual value only borrows from d1, that’s fine – you’re being extra careful by also avoiding modifications to d2.

Dropping a source fails

The reverse doesn’t work – you can’t narrow a multi-source reference to a single source:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self, d1: given Data, d2: given Data) {
                let r: ref[d1, d2] Data = d1.ref;
                let s: ref[d1] Data = r.give;
                ();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "(ref::P) vs (ref::P)" at (redperms.rs) failed because
          condition evaluted to false: `place_b.is_prefix_of(place_a)`
            place_b = d1
            place_a = d2"#]]
);

ref[d1, d2] </: ref[d1] – the value might borrow from d2, and the target type doesn’t protect d2 from modification.

How place sets work in the rules

Internally, a permission like ref[d1, d2] is represented as a RedPerm with multiple chains – one chain Rfl(d1) and another chain Rfl(d2). For the subtype to hold, every chain in the subtype must match some chain in the supertype.

When checking ref[d1] <: ref[d1, d2]: the subtype has one chain Rfl(d1). The supertype has two chains: Rfl(d1) and Rfl(d2). The single chain matches Rfl(d1) in the supertype. Done.

When checking ref[d1, d2] <: ref[d1]: the subtype has two chains: Rfl(d1) and Rfl(d2). Rfl(d1) matches, but Rfl(d2) has no match in the supertype. The check fails.

Combining both dimensions

Sub-places and place sets compose naturally. Here’s a case that uses both:

crate::assert_ok!(
    {
        class Data {
            left: given Data;
            right: given Data;
        }

        class Main {
            fn test(given self, d: given Data) {
                let r: ref[d.left, d.right] Data = d.left.ref;
                let s: ref[d] Data = r.give;
                ();
            }
        }
    }
);

ref[d.left, d.right] <: ref[d] – both d.left and d.right are sub-places of d, so both chains satisfy the prefix check.

The same holds for leases:

crate::assert_ok!(
    {
        class Data {
            left: given Data;
            right: given Data;
        }

        class Main {
            fn test(given self, d: given Data) {
                let r: mut[d.left, d.right] Data = d.left.mut;
                let s: mut[d] Data = r.give;
                ();
            }
        }
    }
);

mut[d.left, d.right] <: mut[d] works by the same logic.

Copy permissions

Some permissions are copy – values with copy permissions can be freely duplicated. There are three copy permissions in Dada, and understanding how they relate to each other is key to understanding permission comparison.

The three copy permissions

shared – owned and copy. A shared value can be duplicated freely and lives as long as any copy exists. It places no restrictions on the environment.

ref[d] – borrowed and copy. A reference can be duplicated freely, but it borrows from the place d. While the reference exists, d cannot be modified.

shared mut[d] – a composed permission. This is the result of sharing a lease: you take a mutable lease mut[d] and share it with .share. The result is copy (because the outer shared makes it so), but it still restricts d (because the underlying lease is active).

How they relate

These three form a subtyping chain:

shared  <:  ref[d]  <:  shared mut[d]

Each step adds more restrictions while remaining copy.

shared <: ref[d]

A shared value can stand in wherever a reference is expected. If the caller expects a borrowed reference from d, giving them an owned shared copy is safe – they get what they need (read access), and the extra restriction on d (not modifying it while the reference exists) is harmlessly conservative:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let s: shared Data = new Data().share;
                let r: ref[d] Data = s.give;
                ();
            }
        }
    }
);

The value s has type shared Data. The target r expects ref[d] Data. Since shared <: ref[d], this works.

ref[d] is NOT <: shared

The reverse doesn’t hold – a borrow can’t become ownership:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let r: ref[d] Data = d.ref;
                let s: shared Data = r.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self d : given Data) -> () { let r : ref [d] Data = d . ref ; let s : shared Data = r . give ; () ; } } }`"]
);

ref[d] </: shared – the reference depends on d being alive. A shared value makes no such assumption. If we allowed this, the “shared” value could outlive d.

shared <: shared mut[d]

A shared value can also stand in for a shared lease. The shared lease restricts d; a shared value doesn’t need d at all, so the restriction is harmlessly extra:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let s: shared Data = new Data().share;
                let r: shared mut[d] Data = s.give;
                ();
            }
        }
    }
);

ref[d] <: shared mut[d]

A reference can stand in for a shared lease from the same place:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let r: ref[d] Data = d.ref;
                let sm: shared mut[d] Data = r.give;
                ();
            }
        }
    }
);

Both ref[d] and shared mut[d] are copy and both restrict d. The difference is what they say about the object – ref[d] guarantees the object won’t be mutated through this reference, while shared mut[d] allows the possibility that another mut[d] holder could mutate the object. Since the reference provides a stronger guarantee, it’s a subtype.

The chain comparison rule for this is:

(if place_b.is_prefix_of(place_a))
(red_chain_sub_chain(env, tail_a, tail_b) => ())
--- ("(ref::P) vs (shared::mut::P)")
(red_chain_sub_chain(
    env,
    Head(RedLink::Rfl(place_a) | RedLink::Rfd(place_a), Tail(tail_a)),
    Head(RedLink::Shared, Head(RedLink::Mtl(place_b) | RedLink::Mtd(place_b), Tail(tail_b))),
) => ())

shared mut[d] is NOT <: ref[d]

The reverse fails:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let p: mut[d] Data = d.mut;
                let sm: shared mut[d] Data = p.ref;
                let r: ref[d] Data = sm.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self d : given Data) -> () { let p : mut [d] Data = d . mut ; let sm : shared mut [d] Data = p . ref ; let r : ref [d] Data = sm . give ; () ; } } }`"]
);

shared mut[d] </: ref[d] – a shared lease can coexist with mutation of the object, while a reference cannot. Treating a shared lease as a reference would falsely promise immutability.

How composition works

Permissions compose with Perm::Apply – written as P Q in the grammar, meaning “apply permission P to something with permission Q.” The result depends on whether the inner permission is copy.

Copy absorbs: ref[p] shared == shared

When you borrow from something that’s already shared, the borrow is redundant – you just get shared:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d: shared Data = new Data().share;
                let r = d.ref;
                let s: shared Data = r.give;
                ();
            }
        }
    }
);

The expression d.ref has type ref[d] shared Data. But d has type shared Data, so the composed permission ref[d] shared reduces to just shared – borrowing from shared gives you shared.

Internally, this is the append_chain rule: when the right-hand side of a composition is copy, the left-hand side is discarded. The permission of the thing you’re borrowing from is what matters, not the act of borrowing.

Non-copy composes: ref[p] mut[d]

When the inner permission is NOT copy, composition creates a genuine chain. Borrowing from something leased gives you a borrow-of-a-lease:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d: given Data = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] mut[d] Data = p.ref;
                ();
            }
        }
    }
);

Here p.ref creates ref[p] mut[d] Data – a chain of two links. The permission records that you borrowed from p, which itself was leased from d.

What happens when you want to use this value depends on whether p is still alive – the Liveness and cancellation chapter explains how dead links are resolved during comparison.

mut[d] is not copy

It’s worth noting what’s NOT in the copy family. A mutable lease mut[d] is NOT copy – it provides exclusive mutable access, which can’t be duplicated:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let p: mut[d] Data = d.mut;
                let q: ref[d] Data = p.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self d : given Data) -> () { let p : mut [d] Data = d . mut ; let q : ref [d] Data = p . give ; () ; } } }`"]
);

mut[d] </: ref[d] – a lease grants exclusive mutation rights, while a reference only grants shared read access. These are incomparable: neither is a subtype of the other.

Similarly, given (unique ownership) is not comparable to any of the copy permissions:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self, d: given Data) {
                let s: shared Data = d.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self d : given Data) -> () { let s : shared Data = d . give ; () ; } } }`"]
);

given </: shared – unique ownership and shared ownership represent fundamentally different memory models.

The full permission landscape

Here’s how all the permissions relate:

The copy permissions (shared, ref[d], shared mut[d]) form a chain within this landscape. The non-copy permissions (given, mut[d]) are incomparable with the copy permissions.

Summary

The copy permissions form a hierarchy:

Subtyping: shared <: ref[d] <: shared mut[d].

Composition: applying a permission to something copy just gives you the copy permission back. Applying a permission to something non-copy creates a genuine chain that requires further analysis to resolve.

The non-copy permissions (given, mut[d]) sit outside this hierarchy – they are incomparable with the copy permissions.

Liveness and cancellation

In the previous sub-chapters, we saw how permissions are compared structurally – place ordering and the copy permission hierarchy. But those rules assume all borrowed places are still alive.

What happens when a borrowed place is dead – no longer used by later code?

Dead links in a RedChain can be cancelled or promoted, which enables subtyping relationships that wouldn’t hold for live links. This is Dada’s equivalent of Rust’s non-lexical lifetimes (NLL) – borrows end when the reference is last used, not when it goes out of scope.

A motivating example: re-borrowing

Consider a function that re-borrows a lease:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: mut[p] Data = p.mut;
                let r: mut[d] Data = q.give;
                ();
            }
        }
    }
);

Here’s what happens step by step:

1. d is created with type given Data
2. p: mut[d] Data – a mutable lease of d
3. q: mut[p] Data – a mutable lease of p (a re-borrow)
4. r: mut[d] Data – we want q.give to have type mut[d] Data

The expression q.give has type mut[p] Data. But r expects mut[d] Data. How can mut[p] mut[d] become mut[d]?

When we reduce mut[p], the permission for q.give, we get the chain [Mtd(p)] – p is dead because q.give is the last expression, and p is never used again. Chain expansion follows p’s type (mut[d] Data), appending Mtl(d) to get [Mtd(p), Mtl(d)].

The target mut[d] reduces to [Mtl(d)].

Comparing [Mtd(p), Mtl(d)] vs [Mtl(d)]: the cancellation rule fires – since p is dead, the Mtd(p) link is dropped, and comparison continues with the tail [Mtl(d)] vs [Mtl(d)], which succeeds.

But not when the place is live

If p is still used after the assignment, cancellation is blocked:

crate::assert_err!(
    {
        class Data {
            fn read[perm P](P self) { (); }
        }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: mut[p] Data = p.mut;
                let r: mut[d] Data = q.give;
                p.give.read[mut[d]]();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "(mut::P) vs (mut::P)" at (redperms.rs) failed because
          condition evaluted to false: `place_b.is_prefix_of(place_a)`
            place_b = d
            place_a = p"#]]
);

Here p appears in p.give.read[...]() after q.give, so p is live at the point where q.give is evaluated. The chain becomes [Mtl(p), Mtl(d)] (live, not dead) – and there is no rule to cancel a live Mtl link. The assignment to r: mut[d] Data fails.

The two cancellation operations

Dead links are resolved by two rules in red_chain_sub_chain:

Cancellation: dropping a dead mut link

(let ty_dead = env.place_ty(place_dead)?)
(prove_is_shareable(env, ty_dead) => ())
(prove_is_mut(env, tail_a) => ())
(red_chain_sub_chain(env, tail_a, red_chain_b) => ())
--- ("(mut-dead::P) vs Q ~~> (P) vs Q")
(red_chain_sub_chain(env, Head(RedLink::Mtd(place_dead), Tail(tail_a)), red_chain_b) => ())

When the chain starts with Mtd(place) (a dead mutable lease), the rule drops it and continues comparing the tail against the target.

Three conditions must hold:

1. The place must be dead (encoded by the Mtd variant)
2. The type of the dead place must be shareable – prove_is_shareable(env.place_ty(place_dead))
3. The tail must be mut-based – prove_is_mut(tail_a)

The shareable check ensures it’s safe to silently release the lease. The tail check ensures we’re cancelling a lien on top of another lease, not an owned permission.

Promotion: converting a dead ref to shared

(let ty_dead = env.place_ty(place_dead)?)
(prove_is_shareable(env, ty_dead) => ())
(prove_is_mut(env, tail_a) => ())
(red_chain_sub_chain(env, Head(RedLink::Shared, Tail(tail_a)), red_chain_b) => ())
--- ("(ref-dead::P) vs Q ~~> (shared::P) vs Q")
(red_chain_sub_chain(env, Head(RedLink::Rfd(place_dead), Tail(tail_a)), red_chain_b) => ())

When the chain starts with Rfd(place) (a dead reference), the rule replaces it with Shared and continues comparing.

This reflects the fact that once the borrowed place is dead, the reference effectively becomes shared – no one can invalidate it through the original place anymore.

Here’s an example of promotion in action:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] Data = p.ref;
                let r: shared mut[d] Data = q.give;
                ();
            }
        }
    }
);

The expression q.give has type ref[p] mut[d] Data. The target r expects shared mut[d] Data. Since p is dead, the chain [Rfd(p), Mtl(d)] promotes Rfd(p) to Shared, giving [Shared, Mtl(d)] which matches shared mut[d].

If p were still live, promotion wouldn’t happen:

crate::assert_err!(
    {
        class Data {
            fn read[perm P](P self) { (); }
        }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] Data = p.ref;
                let r: shared mut[d] Data = q.give;
                p.give.read[mut[d]]();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "(ref::P) vs (shared::mut::P)" at (redperms.rs) failed because
          condition evaluted to false: `place_b.is_prefix_of(place_a)`
            place_b = d
            place_a = p"#]]
);

With p live, the chain is [Rfl(p), Mtl(d)] – the Rfl variant has no promotion rule, and the comparison fails.

A practical pattern: re-borrowing in functions

Liveness-based cancellation enables a common pattern – re-borrowing inside a function and returning the result:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn reborrow(given self, d: mut[self] Data) -> mut[self] Data {
                let p: mut[d] Data = d.mut;
                p.give;
            }
        }
    }
);

The parameter d: mut[self] Data is a mutable lease from self. Inside the function, d.mut creates mut[d] Data – a re-borrow. When we return p.give, its type is mut[d] Data. The return type expects mut[self] Data.

Since d is dead at the return point (it’s a parameter that’s not used after p.give), the Mtd(d) link cancels, and the chain collapses to mut[self].

Without liveness-based cancellation, re-borrowing would be useless – you could never return a value that was transiently borrowed through a local.

What cancellation cannot do

Not all dead links can be resolved. There are important limits on when cancellation and promotion apply.

Shared-to-leased conversion is blocked

Cancellation can resolve links within a permission chain, but it cannot change the nature of a permission from shared (copy) to leased (exclusive):

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] mut[d] Data = p.ref;
                let r: mut[d] Data = q.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self) -> () { let d = new Data () ; let p : mut [d] Data = d . mut ; let q : ref [p] mut [d] Data = p . ref ; let r : mut [d] Data = q . give ; () ; } } }`"]
);

The expression q.give has type ref[p] mut[d] Data. Even though p is dead, the chain [Rfd(p), Mtl(d)] cannot become [Mtl(d)].

Why? Promotion converts Rfd(p) to Shared, giving [Shared, Mtl(d)] – a shared lease. But mut[d] reduces to [Mtl(d)] – an exclusive lease. shared mut[d] is not a subtype of mut[d].

This reflects a real safety invariant: a reference (even a dead one) was shared – multiple copies may exist. You can’t recover exclusive access from something that was shared.

Multi-place permissions: all places must be dead

When a permission mentions multiple places, like ref[p, q], reduction produces one chain per place. For cancellation to resolve all of them, every place must be dead:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: ref[d] Data = d.ref;
                let q: ref[d] Data = d.ref;
                let r: ref[p, q] ref[d] Data = p.ref;
                let s: ref[d] Data = r.give;
                ();
            }
        }
    }
);

Both p and q are dead at the point of r.give, so both Rfd(p) and Rfd(q) chains can be resolved.

But if even one place is still live:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: ref[d] Data = d.ref;
                let q: ref[d] Data = d.ref;
                let r: ref[p, q] ref[d] Data = p.ref;
                let s: ref[d] Data = r.give;
                q.give;
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self) -> () { let d = new Data () ; let p : ref [d] Data = d . ref ; let q : ref [d] Data = d . ref ; let r : ref [p, q] ref [d] Data = p . ref ; let s : ref [d] Data = r . give ; q . give ; } } }`"]
);

Here q is used after r.give (in q.give), so q is live at the point where r.give is evaluated. The chain Rfl(q) (live, not dead) has no cancellation rule, and the comparison fails – even though p is dead and its chain could be resolved.

How liveness is computed

Liveness is computed backwards through the program. Starting from the end of the function body (where nothing is live), the analysis walks statements in reverse, tracking which places are accessed or traversed.

A place is live if:

• It or any overlapping place is accessed later, or
• It is a prefix of a place that gets assigned to later

A place is dead if it is not live – no future code reads from it or any of its sub-places.

This backward analysis means liveness depends on what comes after a given point in the program. The same variable can be live at one point and dead at another.

The type system threads LivePlaces through the checking process: when sub_perms is called, it receives the set of places that are live after the current expression. This is what determines whether a ref[d] or mut[d] reduces to the live variant (Rfl/Mtl) or the dead variant (Rfd/Mtd).

Summary

Key constraints:

• Only dead links can be cancelled or promoted
• The dead place’s type must be shareable
• The tail of the chain must be mut-based
• Shared-to-leased conversion is never possible
• Multi-place permissions require all places to be dead
• Liveness is computed backwards from end of function

Running a program

The previous chapters showed how the type checker verifies that a program is well-formed. But checking types is only half the story – we also want to run programs. The interpreter takes a type-checked program and evaluates it, producing a result.

Here is a simple program that creates a Point and returns it:

crate::assert_interpret!(
    {
        class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn main(given self) -> Point {
                let p = new Point(22, 44);
                p.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_p = new Point (22, 44) ;
        Output: Trace:   _1_p = Point { x: 22, y: 44 }
        Output: Trace:   _1_p . give ;
        Output: Trace: exit Main.main => Point { x: 22, y: 44 }
        Result: Ok: Point { x: 22, y: 44 }
        Alloc 0x06: [Int(22), Int(44)]"#]]
);

The interpreter starts by creating a Main() instance and calling its main method. The method creates a Point, gives it away as the return value, and the interpreter displays the result: Point { flag: Given, x: 22, y: 44 }. The flag: Given tells us this is a uniquely owned value.

The memory model

The interpreter models memory as a collection of allocations. Each allocation is a flat array of words – there are no pointers between fields, no type tags in memory, and no named field maps. This mirrors how a real machine represents values.

An Alloc is a flat vector of words:

/// A flat array of words representing a value in memory.
#[derive(Debug, Clone, PartialEq, Eq)]
struct Alloc {
    data: Vec<Word>,
}

Each word is one of:

/// A single word of memory.
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum Word {
    Int(i64),
    Flags(Flags),
    Pointer(Pointer),
    MutRef(Pointer),
    RefCount(i64),
    Capacity(usize),
    Uninitialized,
}

• Int(n) – an integer value.
• Flags(f) – a permission flag for unique objects.
• Uninitialized – the slot has been moved or cleared.

The Flags enum tracks the permission state of a unique object:

/// Permission flag for unique objects.
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum Flags {
    /// Indicates that the data here is fully owned.
    Given,

    /// Indicates that the data here has shared ownership.
    Shared,

    /// Indicates that the data here is a borrowed reference.
    Borrowed,
}

• Given – the value is uniquely owned.
• Shared – the value has been shared (copyable).
• Borrowed – the value is a read-only reference copy.
• Uninitialized – the value has been moved away.

A Pointer identifies a position within an allocation:

/// Identifies a position within an allocation.
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
struct Pointer {
    index: usize,
    offset: usize,
}

Object layout

Unique classes (regular class and given class) are laid out with a flags word followed by their fields:

+-------------------+
| Flags(Given)      |   <- flags word
| field 0 words...  |
| field 1 words...  |
| ...               |
+-------------------+

Shared classes (shared class) have no flags word – they are always copyable, so no permission tracking is needed:

+-------------------+
| field 0 words...  |
| field 1 words...  |
| ...               |
+-------------------+

An Int is a single word [Int(n)]. A unit value () is an empty allocation (zero words).

Types flow through evaluation, not memory

The interpreter does not store type information in allocations. Memory is just words – the type exists in the evaluator’s head. A TypedValue pairs a pointer with the type needed to interpret it:

/// A pointer paired with the type needed to interpret the words.
/// For boxed types (e.g., arrays, mut-refs), this will be a pointer to a pointer.
/// For inline objects, this will be a pointer to the object data.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ObjectValue {
    pointer: Pointer,
    ty: Ty,
}

The stack frame maps variables to TypedValues, so we always know both where a value lives and what type it is:

pub struct StackFrame {
    env: Env,
    variables: Vec<(Var, Pointer)>,
}

The interpreter and stack frames

The interpreter holds a reference to the program, a type system environment (used to check whether types are copyable), and the collection of allocations:

pub struct Interpreter<'a> {
    program: &'a Program,
    allocs: Vec<Alloc>,
    output: String,
    indent: usize,
    /// Monotonically increasing counter for alpha-renaming method bodies.
    /// Each method invocation gets a unique ID so renamed variables
    /// (e.g., `_1_self`, `_2_self`) never collide, even across sequential
    /// calls at the same stack depth.
    next_call_id: usize,
}

Each method call creates a StackFrame that maps variable names to typed value pointers.

Walking through evaluation

Let’s trace through the example above step by step.

Entry point

The interpreter begins by instantiating Main() – a unique class with no fields, so its allocation is just a flags word – then calling main on it. The stack frame for main starts with self bound to the Main allocation:

allocs: [ [Flags(Given)] ]
stack:  { self -> (alloc 0, Main) }

let p = new Point(22, 44)

The new expression evaluates each field argument (creating temporary allocations for each integer), then builds a flat allocation for the Point:

allocs: [ [Flags(Given)],     <- Main (alloc 0)
          [Int(22)],           <- temp for 22 (alloc 1)
          [Int(44)],           <- temp for 44 (alloc 2)
          [Flags(Given), Int(22), Int(44)] ]  <- Point (alloc 3)
stack:  { self -> (alloc 0, Main), p -> (alloc 3, Point) }

Alloc 3 holds a Point with its flags word at offset 0, x at offset 1, and y at offset 2. To access p.x, the interpreter uses the type Point to compute that field x starts at offset 1.

p.give

The give access mode copies the words to a new allocation and marks the source’s flags as Uninitialized. Since p is the last statement, this is the return value:

allocs: [ ...,
          [Flags(Uninitialized), Int(22), Int(44)],  <- alloc 3 (moved)
          [Flags(Given), Int(22), Int(44)] ]          <- alloc 4 (copy)

The method returns alloc 4 – a fresh Point with copied words. Displayed: Point { flag: Given, x: 22, y: 44 }.

Arithmetic

The interpreter supports integer arithmetic:

crate::assert_interpret!(
    {
        class Main {
            fn main(given self) -> Int {
                let x = 10;
                let y = 20;
                x.give + y.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_x = 10 ;
        Output: Trace:   _1_x = 10
        Output: Trace:   let _1_y = 20 ;
        Output: Trace:   _1_y = 20
        Output: Trace:   _1_x . give + _1_y . give ;
        Output: Trace: exit Main.main => 30
        Result: Ok: 30
        Alloc 0x08: [Int(30)]"#]]
);

Method calls

Methods can call other methods on objects they receive. The interpreter uses the receiver’s type (not the memory contents) to resolve which class and method to call, creates a new stack frame, and evaluates the body:

crate::assert_interpret!(
    {
        class Adder {
            a: Int;
            b: Int;

            fn sum(given self) -> Int {
                self.a.give + self.b.give;
            }
        }

        class Main {
            fn main(given self) -> Int {
                let adder = new Adder(3, 4);
                adder.give.sum();
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_adder = new Adder (3, 4) ;
        Output: Trace:   _1_adder = Adder { a: 3, b: 4 }
        Output: Trace:   _1_adder . give . sum () ;
        Output: Trace:   enter Adder.sum
        Output: Trace:     _2_self . a . give + _2_self . b . give ;
        Output: Trace:   exit Adder.sum => 7
        Output: Trace: exit Main.main => 7
        Result: Ok: 7
        Alloc 0x0a: [Int(7)]"#]]
);

When the interpreter encounters adder.give.sum(), it first evaluates the receiver adder.give – copying the Adder’s words to a new allocation. Then it uses the type Adder to look up sum, creates a stack frame with self bound to the copied adder, and evaluates the body.

Access modes at runtime

The type checker verifies that access modes are used correctly. The interpreter executes them – but the behavior depends on the flags of the source value. Each place operation begins by reading the source’s flags word (if the type has one) and dispatching on it.

If a place expression traverses through a field whose object has Uninitialized flags, the interpreter faults immediately. Similarly, applying any place operation directly to an Uninitialized value is a fault. The type checker prevents these cases in well-typed programs, but faulting at runtime makes it possible to fuzz the type checker for soundness bugs.

Give

give copies the value’s words to a new allocation. What happens next depends on the source’s flags:

Giving a Given value transfers ownership – the source becomes dead:

crate::assert_interpret!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let d = new Data(42);
                d.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_d = new Data (42) ;
        Output: Trace:   _1_d = Data { x: 42 }
        Output: Trace:   _1_d . give ;
        Output: Trace: exit Main.main => Data { x: 42 }
        Result: Ok: Data { x: 42 }
        Alloc 0x05: [Int(42)]"#]]
);

Giving a Shared value produces a shared copy – and since shared values are copyable, the source remains usable:

crate::assert_interpret_only!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let d = new Data(42);
                let s = d.give.share;
                let x1 = s.give;
                let x2 = s.give;
                print(x1.give);
                x2.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_d = new Data (42) ;
        Output: Trace:   _1_d = Data { x: 42 }
        Output: Trace:   let _1_s = _1_d . give . share ;
        Output: Trace:   _1_s = shared Data { x: 42 }
        Output: Trace:   let _1_x1 = _1_s . give ;
        Output: Trace:   _1_x1 = shared Data { x: 42 }
        Output: Trace:   let _1_x2 = _1_s . give ;
        Output: Trace:   _1_x2 = shared Data { x: 42 }
        Output: Trace:   print(_1_x1 . give) ;
        Output: ----->   shared Data { x: 42 }
        Output: Trace:   _1_x2 . give ;
        Output: Trace: exit Main.main => shared Data { x: 42 }
        Result: Ok: shared Data { x: 42 }
        Alloc 0x0d: [Int(42)]"#]]
);

Ref

ref creates a read-only copy. The behavior depends on the source’s flags:

A ref from a Given source creates a Borrowed copy while leaving the original intact:

crate::assert_interpret!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let d = new Data(42);
                print(d.ref);
                d.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_d = new Data (42) ;
        Output: Trace:   _1_d = Data { x: 42 }
        Output: Trace:   print(_1_d . ref) ;
        Output: ----->   ref [_1_d] Data { x: 42 }
        Output: Trace:   _1_d . give ;
        Output: Trace: exit Main.main => Data { x: 42 }
        Result: Ok: Data { x: 42 }
        Alloc 0x07: [Int(42)]"#]]
);

A ref from a Shared source stays Shared – shared permission is “stickier” than borrowed:

crate::assert_interpret_only!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let d = new Data(42);
                let s = d.give.share;
                s.ref;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_d = new Data (42) ;
        Output: Trace:   _1_d = Data { x: 42 }
        Output: Trace:   let _1_s = _1_d . give . share ;
        Output: Trace:   _1_s = shared Data { x: 42 }
        Output: Trace:   _1_s . ref ;
        Output: Trace: exit Main.main => shared Data { x: 42 }
        Result: Ok: shared Data { x: 42 }
        Alloc 0x07: [Int(42)]"#]]
);

Share

share is a value operation, not a place operation. To share a place, you first give it and then share the result: d.give.share.

The share operation converts a value from unique to shared ownership in place. If the flags are Given, it sets them to Shared and recursively applies the share operation to nested class fields. If already Shared or Borrowed, it’s a no-op:

crate::assert_interpret_only!(
    {
        class Inner { x: Int; }
        class Outer { inner: Inner; }
        class Main {
            fn main(given self) -> Outer {
                let o = new Outer(new Inner(1));
                o.give.share;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_o = new Outer (new Inner (1)) ;
        Output: Trace:   _1_o = Outer { inner: Inner { x: 1 } }
        Output: Trace:   _1_o . give . share ;
        Output: Trace: exit Main.main => shared Outer { inner: Inner { x: 1 } }
        Result: Ok: shared Outer { inner: Inner { x: 1 } }
        Alloc 0x06: [Int(1)]"#]]
);

The share operation is recursive – when sharing an Outer, its Given inner field is also set to Shared.

Drop

drop releases ownership of a value. The behavior depends on the source’s flags:

Dropping a Given value recursively uninitializes it and its fields. Dropping a Borrowed value is a no-op – you can continue using the borrow afterward:

crate::assert_interpret_only!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let d = new Data(42);
                let r = d.ref;
                r.drop;
                r.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_d = new Data (42) ;
        Output: Trace:   _1_d = Data { x: 42 }
        Output: Trace:   let _1_r = _1_d . ref ;
        Output: Trace:   _1_r = ref [_1_d] Data { x: 42 }
        Output: Trace:   _1_r . drop ;
        Output: Trace:   _1_r . give ;
        Output: Trace: exit Main.main => ref [_1_d] Data { x: 42 }
        Result: Ok: ref [_1_d] Data { x: 42 }
        Alloc 0x08: [Int(42)]"#]]
);

Mut

mut creates a mutable reference. It is not yet implemented in the interpreter.

Conditionals

The if expression evaluates a condition and executes one of two branches. The interpreter treats 0 as false and any other integer as true. Since if returns unit, we use assignment to communicate a result out:

crate::assert_interpret!(
    {
        class Main {
            fn main(given self) -> Int {
                let result = 0;
                if true { result = 42; } else { result = 0; };
                result.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_result = 0 ;
        Output: Trace:   _1_result = 0
        Output: Trace:   if true { _1_result = 42 ; } else { _1_result = 0 ; } ;
        Output: Trace:   _1_result = 42 ;
        Output: Trace:   _1_result = 42
        Output: Trace:   _1_result . give ;
        Output: Trace: exit Main.main => 42
        Result: Ok: 42
        Alloc 0x08: [Int(42)]"#]]
);

crate::assert_interpret!(
    {
        class Main {
            fn main(given self) -> Int {
                let result = 0;
                if false { result = 42; } else { result = 99; };
                result.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_result = 0 ;
        Output: Trace:   _1_result = 0
        Output: Trace:   if false { _1_result = 42 ; } else { _1_result = 99 ; } ;
        Output: Trace:   _1_result = 99 ;
        Output: Trace:   _1_result = 99
        Output: Trace:   _1_result . give ;
        Output: Trace: exit Main.main => 99
        Result: Ok: 99
        Alloc 0x08: [Int(99)]"#]]
);

Arrays

Array[T] is the single heap-allocation primitive in Dada. Higher-level types like Vec, String, and Box are all built on top of arrays. An array is a fixed-capacity, refcounted block of memory that holds elements of type T.

Array layout

An Array[T] value is two words – a flags word and a pointer to the backing allocation:

Array[T] value (2 words):
+-------------------+
| Flags(Given)      |   <- ownership flag
| Pointer(alloc)    |   <- points to backing allocation
+-------------------+

Backing allocation:
+-------------------+
| RefCount(1)       |   <- reference count
| Capacity(n)       |   <- number of element slots
| element 0 words   |   <- size_of(T) words per element
| element 1 words   |
| ...               |
+-------------------+

Each element slot is size_of(T) words. Elements of unique classes (like Data) start with a flags word, while copy types (like Int) have no flags:

Array[Data] backing (capacity 2):
+-------------------+
| RefCount(1)       |
| Capacity(2)       |
| Flags(Given)      |   <- element 0 flags
| Int(42)           |   <- element 0 field x
| Flags(Given)      |   <- element 1 flags
| Int(99)           |   <- element 1 field x
+-------------------+

Array[Int] backing (capacity 3):
+-------------------+
| RefCount(1)       |
| Capacity(3)       |
| Int(10)           |   <- element 0
| Int(20)           |   <- element 1
| Int(30)           |   <- element 2
+-------------------+

Creating and accessing arrays

Five operations work with arrays:

• array_new[T](n) – allocate a new array with capacity n. All element slots start uninitialized.
• array_set[T](a, i, v) – write value v into slot i. The slot must be uninitialized.
• array_give[T](a, i) – read the element at slot i. Behavior depends on the element type (see below).
• array_drop[T](a, i) – drop the element at slot i, marking it uninitialized.
• array_capacity[T](a) – return the array’s capacity as an Int.

Here’s a simple example that creates, fills, and reads an Array[Int]:

crate::assert_interpret_only!(
    {
        class Main {
            fn main(given self) -> Int {
                let a = array_new[Int](3);
                array_write[Int, mut[a]](a.mut, 0, 10);
                array_write[Int, mut[a]](a.mut, 1, 20);
                array_write[Int, mut[a]](a.mut, 2, 30);
                print(array_give[Int, given, ref[a]](a.ref, 0));
                print(array_give[Int, given, ref[a]](a.ref, 1));
                array_give[Int, given, given](a.give, 2);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Int](3) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, ⚡, ⚡, ⚡ }
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 0 , 10) ;
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 1 , 20) ;
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 2 , 30) ;
        Output: Trace:   print(array_give [Int, given, ref [_1_a]](_1_a . ref , 0)) ;
        Output: ----->   10
        Output: Trace:   print(array_give [Int, given, ref [_1_a]](_1_a . ref , 1)) ;
        Output: ----->   20
        Output: Trace:   array_give [Int, given, given](_1_a . give , 2) ;
        Output: Trace: exit Main.main => 30
        Result: Ok: 30
        Alloc 0x1c: [Int(30)]"#]]
);

The array is created with array_new[Int](3) (capacity 3), then shared so it can be passed to multiple operations. Each array_set writes a value into a slot, and array_give reads elements back out.

Copy elements vs. move elements

array_give behaves differently depending on whether the element type is a copy type:

Int elements are copy types – giving an Int element copies it without disturbing the source. You can read the same slot multiple times:

crate::assert_interpret_only!(
    {
        class Main {
            fn main(given self) -> Int {
                let a = array_new[Int](1);
                array_write[Int, mut[a]](a.mut, 0, 42);
                let x = array_give[Int, given, ref[a]](a.ref, 0);
                let y = array_give[Int, given, ref[a]](a.ref, 0);
                print(x.give);
                y.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Int](1) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, ⚡ }
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 0 , 42) ;
        Output: Trace:   let _1_x = array_give [Int, given, ref [_1_a]](_1_a . ref , 0) ;
        Output: Trace:   _1_x = 42
        Output: Trace:   let _1_y = array_give [Int, given, ref [_1_a]](_1_a . ref , 0) ;
        Output: Trace:   _1_y = 42
        Output: Trace:   print(_1_x . give) ;
        Output: ----->   42
        Output: Trace:   _1_y . give ;
        Output: Trace: exit Main.main => 42
        Result: Ok: 42
        Alloc 0x14: [Int(42)]"#]]
);

The array’s own flags propagate to element access. When a shared array’s elements are accessed via array_give, the shared context overrides the element’s runtime flags – even though class elements have Flags(Given) at rest, accessing them through a shared array uses shared semantics (copy + share_op, no move). This means you can read the same slot multiple times:

// Shared array: class elements are accessed with shared semantics —
// giving an element produces a shared copy, element remains available.
crate::assert_interpret_only!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let a = array_new[Data](1);
                array_write[Data, mut[a]](a.mut, 0, new Data(42));
                let s = a.give.share;
                let x = array_give[Data, shared, ref[s]](s.ref, 0);
                print(x.give);
                // Element still available — shared, no move.
                array_give[Data, shared, shared](s.give, 0);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Data](1) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, Data { x: ⚡ } }
        Output: Trace:   array_write [Data, mut [_1_a]](_1_a . mut , 0 , new Data (42)) ;
        Output: Trace:   let _1_s = _1_a . give . share ;
        Output: Trace:   _1_s = shared Array { flag: Shared, rc: 1, Data { x: 42 } }
        Output: Trace:   let _1_x = array_give [Data, shared, ref [_1_s]](_1_s . ref , 0) ;
        Output: Trace:   _1_x = shared Data { x: 42 }
        Output: Trace:   print(_1_x . give) ;
        Output: ----->   shared Data { x: 42 }
        Output: Trace:   array_give [Data, shared, shared](_1_s . give , 0) ;
        Output: Trace: exit Main.main => shared Data { x: 42 }
        Result: Ok: shared Data { x: 42 }
        Alloc 0x15: [Int(42)]"#]]
);

This is the same effective-flags principle as place traversal: accessing a field through a shared path gives shared semantics, regardless of the field’s runtime flags.

Here’s an example with Data elements in a shared array – each element can be read multiple times without moving:

crate::assert_interpret_only!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Data {
                let a = array_new[Data](2);
                array_write[Data, mut[a]](a.mut, 0, new Data(42));
                array_write[Data, mut[a]](a.mut, 1, new Data(99));
                print(array_give[Data, given, ref[a]](a.ref, 0));
                array_give[Data, given, given](a.give, 1);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Data](2) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, Data { x: ⚡ }, Data { x: ⚡ } }
        Output: Trace:   array_write [Data, mut [_1_a]](_1_a . mut , 0 , new Data (42)) ;
        Output: Trace:   array_write [Data, mut [_1_a]](_1_a . mut , 1 , new Data (99)) ;
        Output: Trace:   print(array_give [Data, given, ref [_1_a]](_1_a . ref , 0)) ;
        Output: ----->   Data { x: 42 }
        Output: Trace:   array_give [Data, given, given](_1_a . give , 1) ;
        Output: Trace: exit Main.main => Data { x: 99 }
        Result: Ok: Data { x: 99 }
        Alloc 0x16: [Int(99)]"#]]
);

Sharing and reference counting

A freshly created array has Flags(Given) – it is uniquely owned. Sharing converts it to Flags(Shared), and from that point on, giving the array to another variable increments the refcount rather than moving:

crate::assert_interpret_only!(
    {
        class Main {
            fn main(given self) -> Int {
                let a = array_new[Int](2);
                array_write[Int, mut[a]](a.mut, 0, 10);
                array_write[Int, mut[a]](a.mut, 1, 20);
                let s = a.give.share;
                let b = s.give;
                s.drop;
                print(array_give[Int, given, ref[b]](b.ref, 0));
                array_give[Int, given, shared](b.give, 1);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Int](2) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, ⚡, ⚡ }
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 0 , 10) ;
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 1 , 20) ;
        Output: Trace:   let _1_s = _1_a . give . share ;
        Output: Trace:   _1_s = shared Array { flag: Shared, rc: 1, 10, 20 }
        Output: Trace:   let _1_b = _1_s . give ;
        Output: Trace:   _1_b = shared Array { flag: Shared, rc: 2, 10, 20 }
        Output: Trace:   _1_s . drop ;
        Output: Trace:   print(array_give [Int, given, ref [_1_b]](_1_b . ref , 0)) ;
        Output: ----->   10
        Output: Trace:   array_give [Int, given, shared](_1_b . give , 1) ;
        Output: Trace: exit Main.main => 20
        Result: Ok: 20
        Alloc 0x19: [Int(20)]"#]]
);

After let b = a.give, both a and b point to the same backing allocation (refcount is now 2). Dropping a decrements the refcount to 1, but b still works because the allocation is alive.

The key distinction is between convert_to_shared and share_op:

• convert_to_shared is an in-place ownership change (Called by .share). It flips the flags from Given to Shared. The refcount stays at 1 – one reference is still one reference.
• share_op is duplication accounting (called when copying a Shared value via .give or .ref). It increments the refcount because one reference has become two.

Given arrays

Without sharing, an array is uniquely owned. Giving it transfers ownership, and the source becomes uninitialized:

crate::assert_interpret_only!(
    {
        class Main {
            fn main(given self) -> Int {
                let a = array_new[Int](2);
                array_write[Int, mut[a]](a.mut, 0, 10);
                array_write[Int, mut[a]](a.mut, 1, 20);
                let b = a.give;
                array_give[Int, given, given](b.give, 0);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Int](2) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, ⚡, ⚡ }
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 0 , 10) ;
        Output: Trace:   array_write [Int, mut [_1_a]](_1_a . mut , 1 , 20) ;
        Output: Trace:   let _1_b = _1_a . give ;
        Output: Trace:   _1_b = Array { flag: Given, rc: 1, 10, 20 }
        Output: Trace:   array_give [Int, given, given](_1_b . give , 0) ;
        Output: Trace: exit Main.main => 10
        Result: Ok: 10
        Alloc 0x12: [Int(10)]"#]]
);

The array is Given, so let b = a.give moves it. After the move, a is dead – any access would fault.

Dropping arrays

Dropping an array decrements the refcount. When the refcount reaches zero, the interpreter walks all element slots and recursively drops any initialized elements, then frees the backing allocation:

crate::assert_interpret_only!(
    {
        class Data { x: Int; }
        class Main {
            fn main(given self) -> Int {
                let a = array_new[Data](2);
                array_write[Data, mut[a]](a.mut, 0, new Data(1));
                array_write[Data, mut[a]](a.mut, 1, new Data(2));
                a.drop;
                0;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let _1_a = array_new [Data](2) ;
        Output: Trace:   _1_a = Array { flag: Given, rc: 1, Data { x: ⚡ }, Data { x: ⚡ } }
        Output: Trace:   array_write [Data, mut [_1_a]](_1_a . mut , 0 , new Data (1)) ;
        Output: Trace:   array_write [Data, mut [_1_a]](_1_a . mut , 1 , new Data (2)) ;
        Output: Trace:   _1_a . drop ;
        Output: Trace:   0 ;
        Output: Trace: exit Main.main => 0
        Result: Ok: 0
        Alloc 0x11: [Int(0)]"#]]
);

Both Data elements are recursively dropped (their flags are set to Uninitialized, fields are cleaned up), then the backing allocation is overwritten with Uninitialized words. The heap snapshot shows only the result Int – no leaked array memory.

Work in progress

Vec and array design

We are working our way towards the following design which will cover a “partially initialize” array type called Vec (the full Vec in the standard library would be expected to support more features, but this is enough for now). I’m also assuming all indices are in-bounds and a few other details.

Goal: Vector class

class Vec[type T] {
    data: Array[T]
    len: Int
    
    fn push[perm P](P self, value: given T) where P is mut {
        array_write[T, mut[self.data]](self.data.mut, self.len.give, value.give)
        self.len = self.len.give + 1
    }
    
    fn get[perm P](P self, index: Int) -> given_from[self] T {
        let data: given_from[self.data] Array[T] = self.data.give # P=given: moves data out, self not-whole, Vec.drop won't run.
                                                               # P=ref/shared: copies, self stays whole, Vec.drop runs but is
                                                               # harmless (is_last_ref guards cleanup, array_drop is no-op).
        let len: Int = self.len.give
        array_drop[T, given_from[self], ref[data]](data.ref, 0, index.give)
        array_drop[T, given_from[self], ref[data]](data.ref, index.give + 1, len.give)
        array_give[T, given_from[self], ref[data]](data.ref, index.give)
    }
    
    fn iter[perm P](P self) -> Iterator[P, T] {
        new Iterator[P, T](self.give, 0)
    }

    drop {
        if is_last_ref[ref[self.data]](self.data.ref) {
            array_drop[T, given, ref[self]](self.data.ref, 0, self.len.give)
        } else {}
    }
}

class Iterator[perm P, type T] {
    vec: P Vec[T]
    start: Int
    
    fn next[perm I](I self) -> P T
    where
        I is mut,
    {
        let index = self.start.give
        self.start = self.start.give + 1
        array_give[T, P, ref[self.vec.data]](self.vec.data.ref, index.give)
    }
    
    drop {
        let data = self.vec.data.give # subtle: disables vec dtor
        let start = self.start.give
        let len = self.vec.len.give
        
        # free the elements not yet iterated over:
        array_drop[T, P, ref[data]](data.ref, start.give, len.give)
    }
}

Key points

boxed classes

A boxed class indicates a class whose memory is stored in the heap. Boxed classes permit recursion, internal mutation with mutexes etc, and cheaper data movement. Currently the only boxed class is the built-in Array, but we expect to change this later.

A boxed-class is represented as a pointer along with flags that, in the real thing, will be stored in the low-bits of the pointer:

• dropped – the value has been moved or dropped
• given – sole ownership
• shared – shared ownership (refcount > 1)
• ref – a borrow (no ownership)

Note that a mut ref is different and always stored as a pointer to the object data, independent of whether it refers to a boxed class or a regular class.

Boxed class layout is:

• [ref-count, fields...]

Dropping a owned boxed class decrements the ref-count and, if it is zero, drops the fields.

Array[T] type semantics

The Array[T] is a special boxed class that carries inline data:

• [ref-count, capacity, elements...]

Dropping a owned array decrements the ref-count and, if it is zero, frees the array. IT DOES NOT DROP THE ELEMENTS, users are expected to drop those elements themselves. This is because array elements may not be initialized at all times.

Arrays support the following intrinsic, unsafe operations

• array_new[type T](capacity: Int) -> given Array[T], returns a fresh owned uninitialized array. No permission parameter — always returns given.

• array_capacity[type T, perm A](array: A Array[T]) -> Int where A is ref, returns capacity of an array

• array_write[type T, perm A](array: A Array[T], index: Int, value: given T) where A is mut, writes the value to the given index; any previous value is ignored

• array_drop[type T, perm P, perm A](array: A Array[T], from: Int, to: Int) where A is ref, drops elements from from..to (exclusive) in a way that depends on the permission P. If from >= to, this is a no-op.

  • If P is given (i.e., prove_is_given(P) — the permission alone, not P T), then the value is dropped.
  • Else this is a no-op.
  • Note: the dispatch checks P, not P T. Even if T is a copy type (e.g., a shared class), P = given means “I own these elements, clean them up.” This is needed to avoid leaks: a shared class with boxed fields (e.g., shared class Wrapper { data: Array[Int] }) still needs its boxed fields’ refcounts decremented.

• array_give[type T, perm P, perm A](array: A Array[T], index: Int) -> P T where A is ref, reads and returns the element at index. The behavior is determined by composing P with the element’s runtime flags — not by classifying the static type P T. The interpreter translates P into an owner_operms (given→Given, mut→MutRef, shared→Shared, ref→Borrowed), then calls object_value_to_data on the element with type T and that owner_operms. For boxed elements, the runtime Flags word is read and composed via with_projection_flags: runtime Shared always wins (producing a shared copy with rc++), runtime Given passes through the owner_operms. The result type is P T. The four effective behaviors:

  • Given + runtime Given: the value is moved and the source is uninitialized.
  • MutRef + runtime Given: a mutable reference to the element’s fields is created. For boxed types, this dereferences through the [Flags, Pointer] wrapper to point at the object data. For flat (non-boxed) types, the MutRef points directly into the array allocation at the element’s offset.
  • Shared (either from P or runtime Shared override): the element’s words are copied out, and then any boxed fields within the copy are transitioned to shared (flags set to Shared, refcount incremented). Flat (non-boxed) fields are just copied — there is no refcount to touch.
  • Borrowed + runtime Given: the element’s words are copied out, and then any boxed fields within the copy have their flags set to Borrowed. Flat fields are just copied.

  Subtyping note: Because shared ≤ ref, a shared value can be stored in a slot typed ref[x] T. When array_give accesses such an element with P = ref, the runtime Shared flags override the static Borrowed owner_operms, correctly producing a shared copy (rc++) instead of a borrow. This avoids a refcount leak that would occur if the static type alone determined the operation. The earlier P is shared ↔ A is shared assertion was invalidated by this scenario and has been removed.

Implementation note: array_give_element calls perm_to_operms(P) to translate the permission into ObjectPerms, then delegates to the standard object_value_to_data (with the element’s raw type T, not P T) followed by give_place. This reuses the existing place access operations (give_place for given/shared, mut_place for mut, ref_place for ref) without any array-specific dispatch logic. No separate object_value_to_data_from_ty is needed — the same object_value_to_data used for normal place resolution handles array elements correctly when given the right owner_operms.

The semantics of drop and give are setup to support a “poly-permission” operation like Vec.get above. The array_drop calls in get are no-ops when P is not given, but they are present so that a single function body works correctly across all permissions — in the given case, they actually destroy the elements we don’t want.

Note that the return type given_from[self] T in Vec.get is effectively equivalent to P — given_from[place] picks up the permission of the place, so given_from[self] where self: P Vec[T] becomes P T. It is written as given_from[self] because it conveys the intent more clearly: “you get whatever permission you had on self.”

“drop” sections – defining custom destructors

A drop section in a class is a special optional section. The type of self in the drop body depends on the class predicate:

• given class → self: given Class[...] (sole ownership)
• class (default, i.e. share) → self: ref Class[...]
• shared class → self: ref Class[...]

When a drop body executes, self is treated as not whole even though all its fields are initialized. This means the whole-place drop logic will drop each field individually rather than dropping self as a unit (which would recursively invoke the drop body again). There is no special “post-drop-body field cleanup” step — the individual field drops are a consequence of the existing whole-place rules applied to a self that is never whole.

Partial moves and field access: Moving a field out of a struct makes the struct not-whole, but other initialized fields remain accessible. Reading a field of a partially-moved struct is legal as long as that specific field has not been moved. The whole-place rules only govern dropping, not reading. The type checker already supports this — liveness is tracked at the place level (e.g., self.vec.data and self.vec.len are independent places), so moving one field doesn’t invalidate sibling fields. No new type-checker feature is needed for the Iterator.drop pattern (self.vec.data.give then self.vec.len.give).

Places always require an access mode: A bare place (e.g., x, self.len) is never valid as an expression. Every use of a place as a value must go through an access mode: .give, .ref, .mut, or .drop. This applies to local variables, function parameters, and field accesses alike. For example, self.len.give (not self.len), index.give (not index).

is_last_ref primitive

is_last_ref[perm A](value: A T) -> Bool is a built-in intrinsic expression (like array_new, etc.). It accepts any ref value — e.g., is_last_ref[ref[self.data]](self.data.ref). It returns a Bool — a new built-in type that needs to be added to TypeName alongside Int. For boxed types (currently only arrays), it returns true if the refcount is 1 (i.e., this is the last owned handle). For non-boxed types, it always returns false — there is no refcount to check, and the caller cannot assume sole ownership. Under a garbage collector, is_last_ref always returns false — elements are collected independently.

Note: if/else already exists as Expr::If.

Executing “drop”

The drop for a class is executed whenever any owned handle to an instance of that class is dropped — not just the last reference. The type of self depends on the class predicate: given class gets self: given Class[...], while class (default) and shared class get self: ref Class[...]. For the non-given cases, ref is the lowest common denominator: shared is a subpermission of ref, so self: ref Class is valid for any owned handle to a share/shared class.

For classes like Vec that manage owned resources, the drop body uses is_last_ref to conditionally clean up only when this is the final handle:

drop {
    if is_last_ref[ref[self.data]](self.data.ref) {
        array_drop[T, given, ref[self]](self.data.ref, 0, self.len.give)
    } else {}
}

When is_last_ref is false (other handles remain, or under GC), the drop body skips element cleanup — another handle will do it, or the GC will collect the elements independently.

Dropping local variables

When a function/block terminates, it drops all values found in “whole” places. A whole value is a value where no part has been moved.

Definition: accessible place. An accessible place is either

• a local variable X
• a field P.F where P is an accessible place of type class and F is a field
• a field P[i] where P is an accessible place of type tuple and i is a tuple index

Note that elements of arrays are not accessible places.

Definition: whole place. An accessible place P is a whole place if

• P and all accessible places that extend P are initialized
  • This is the one place in the interpreter that we “branch” on uninitialized data. The compiler would be expected to track this statically or with extra flags on the stack as needed.

Example. Consider this function

class Vec[type T] {
    data: Array[T]
    index: Int
    
    fn example(given self) {
        # point A
        let data = self.data.give
        # point B
    }
    
    drop {
      # ...
    }
}

For the function example, the accessible places are self, self.data, and self.index.

At point A, self is a whole place. If the function were to return at point A, then self would be dropped. This would cause the drop code to execute, since we are dropping a Vec.

At point B, self.data has been moved, and hence self is not a whole place. self would not be dropped and hence its drop code would not run. self.index is a whole accessible place and would be dropped (but dropping an Int is a no-op).

FAQ

Q: Why does Vec.get call array_drop on all elements except the one being returned? Isn’t that wasteful for ref/shared?

The function body is polymorphic over P. When P is given, those array_drop calls actually destroy the elements we don’t want (we’re consuming the vec). When P is ref or shared, the array_drop calls are no-ops. The alternative would be separate implementations per permission, but one body that works for all permissions is simpler and correct.

Q: What does given_from[self] mean as a return type?

given_from[place] picks up the permission of the place. So given_from[self] where self: P Vec[T] is effectively P T. It’s written as given_from[self] rather than P because it conveys intent more clearly: “you get whatever permission you had on self.”

Q: How does the drop body avoid infinite recursion? If self is whole at the end of the drop body, wouldn’t whole-place dropping invoke the drop body again?

In a drop body, self is treated as not whole even though all its fields are initialized. This means the whole-place logic drops each field individually rather than dropping self as a unit. No special mechanism — just the existing whole-place rules applied to a self that is never whole.

Q: Why doesn’t Iterator.drop use is_last_ref, like Vec.drop does?

Because the poly-permission P already handles all cases correctly. Vec.drop needs is_last_ref because it runs on every handle drop (shared handles each trigger the drop body), so it must guard element cleanup to avoid double-free. Iterator.drop doesn’t have this problem: its array_drop[T, P, ...] dispatches on the permission the iterator was created with. When P = given, the iterator owns the elements and array_drop drops them. When P = shared or P = ref, array_drop is a no-op — the iterator doesn’t own the elements. No runtime guard is needed because the static permission already encodes ownership.

Q: In Iterator.drop, moving self.vec.data out disables Vec.drop. But what about the array backing itself?

The local data is whole at end of scope, so it gets dropped normally: refcount decremented, backing freed if zero. Any elements not covered by the array_drop(data.ref, start, len) call (i.e., elements before start that were already iterated and consumed) are already gone — they were moved out by next(). So the cleanup is complete: array_drop handles un-iterated elements, and dropping data frees the backing.

Q: When P = shared, doesn’t array_drop being a no-op cause leaks in Iterator.drop?

No. When P = shared, the iterator doesn’t own the vec — self.vec is shared Vec[T]. So self.vec.data.give produces a shared copy of the array (incrementing its refcount), not a move. self.vec stays whole, the array_drop call is a no-op, and the shared data copy just gets its refcount decremented at end of scope. Vec.drop runs on every handle being dropped, but the is_last_ref check means element cleanup only happens when the final handle is dropped. The “disables vec dtor” comment in Iterator.drop is only operative in the P = given case.

Q: What does array_drop with P = given actually do to each element? Shallow uninitialize, or full recursive drop?

Full recursive drop. If the element’s class has a drop { } section, that body runs (and then fields are individually dropped via the not-whole self rule). If it has no drop { } section, it behaves as if it had an empty drop {} — fields are individually dropped directly. This recurses all the way down through nested classes.

Q: What does .give do on a borrowed or shared value?

.give always gives the full permissions you have on a value. If you have given, it moves. If you have shared, it produces a shared copy (rc++). If you have ref, it produces a ref copy. You can always .give a value — it’s not restricted to owned data. This is why self.vec.data.give in Iterator.drop works for all permissions P: when P = given it moves the array out (disabling Vec.drop), when P = shared it produces a shared copy, when P = ref it produces a ref copy. In the non-given cases, self.vec remains whole, but the dtor is harmless — dropping a shared handle runs the drop body, but is_last_ref guards ensure cleanup only happens on the final owned handle. Dropping a ref handle is a no-op (borrows don’t own anything).

Q: In Vec.get with P = given, who frees the array backing allocation?

The local data holds the array after self.data.give. At end of scope, data is whole, so it gets dropped: refcount decremented, backing freed. The built-in array drop handles the backing allocation. The elements in the array are the user’s responsibility — that’s what the array_drop and array_give calls in the method body handle.

Q: What is .share in array.give.share? Is it an access mode?

No. .share is an expression-level operation (Expr::Share), not a place access mode. It operates on values, not places — that’s why we write array.give.share: first .give converts the place to a value, then .share converts that value from given to shared ownership. The access modes (.give, .ref, .mut, .drop) operate on places; .share is a separate expression form already in the grammar.

Q: Can drop bodies access class-level generic parameters?

Yes. Drop bodies have access to the class’s generic parameters (e.g., P and T in Iterator[perm P, type T]), just like any method on the class. This is why Iterator.drop can pass P to array_drop.

Q: How can array intrinsics bypass normal permission rules? Aren’t some of these operations obviously unsound?

Yes — array operations are unsafe intrinsics that deliberately violate the permission rules safe code must follow. Specific examples:

• array_drop[T, given, ref[a]](a.ref, 0, 3) — drops and uninitializes element slots through only a ref to the array. Normal safe code cannot modify memory through ref.
• array_give[Data, mut[a], ref[a]](a.ref, 0) — produces a mut[a] Data (a mutable reference to an element) through only a ref to the array. Normal safe code cannot obtain mut access through ref. The returned mut ref is a pointer directly at the object data for the element.
• array_write[T, mut[a]](a.mut, 0, value) — overwrites an element slot without dropping the previous value. Normal safe code would drop the old value first.

The A is ref / A is mut constraints are the minimum the type system enforces on the caller, but the operations themselves bypass normal permission rules internally. Soundness is the caller’s responsibility — e.g., Vec must ensure it never hands out two mut refs to the same element, never reads an uninitialized slot, etc. A full “unsafe effects” system to describe and constrain what unsafe operations can do is future work.

Q: How does the interpreter compute element offsets in arrays?

The interpreter already has size_of(env, ty) which returns the number of words a type occupies. Array element access computes ARRAY_ELEMENTS_OFFSET + index * element_size. This is internal interpreter machinery — user code (like Vec) just passes integer indices to array intrinsics and the interpreter handles offset calculation.

Q: What happens when array_drop is called with from >= to (empty or inverted range)?

It’s a no-op. This naturally arises in Vec.get when index == len - 1, producing array_drop(..., index + 1, len) where from == to.

Q: How does the interpreter decide which array_give/array_drop behavior to use?

For array_give, the interpreter translates P into owner_operms via perm_to_operms, then calls object_value_to_data on the element with its raw type T and that owner_operms. For boxed elements, the runtime Flags word is composed with owner_operms via with_projection_flags — runtime Shared always wins, runtime Given passes through. This means the runtime state can override the static permission: a shared value in a ref-typed slot correctly produces a shared copy, not a borrow. For flat types (no runtime flags), the type classification determines operms. The result is then passed to give_place, which dispatches on the final operms. For array_drop, the interpreter checks just P via prove_is_given(P) — if the permission is given, elements are dropped regardless of T.

Q: Why does array_drop dispatch on just P while array_give uses runtime flags?

array_give uses runtime flags (via object_value_to_data) because the operation on a boxed element must respect the element’s actual ownership state. A shared value stored in a ref-typed slot (valid via subtyping shared ≤ ref) must produce a shared copy (rc++), not a borrow — otherwise the refcount increment would never be undone and the refcount would leak. The runtime flags capture the true ownership state that the static type may have lost.

array_drop checks just P because the question is different: “should I clean up these elements?” If P = given, the caller owns the elements and must clean them up — even if T is a copy type like a shared class. A shared class with boxed fields (e.g., shared class Wrapper { data: Array[Int] }) still needs its boxed fields’ refcounts decremented.

Q: In Vec.get with P = given, the array has uninitialized trailing slots (capacity > len). Is that a problem when the array is dropped?

No. Dropping the array just decrements the refcount, and when it hits zero, the entire backing allocation is scrubbed (all words set to Word::Uninitialized). This does not inspect or iterate over element contents — it’s a bulk uninitialize of the raw memory. Trailing uninitialized slots are harmless; they get overwritten with the same Word::Uninitialized value they already had.

Random notes to check on

• given_from[a.b] Foo – can this be contracted to given_from[a]? Only when the field b is declared with given permission (or no permission prefix). The Mv expansion rule in redperms.rs replaces given_from[place] with the permission of place. So given_from[a.b] reduces to the permission of a.b, which composes the permission of a with the declared permission of field b. If a: mut[x] Foo and b: shared Bar, then a.b has permission shared (mut applied to shared = shared), so given_from[a.b] ≠ given_from[a] (which would be mut[x]). The existing reduction rules handle this correctly — no special case needed.

Implementation plan

Implementation follows a TDD approach: write or update tests first to express intent, then implement until they pass. Each phase produces a working, all-tests-passing state. Tests that don’t yet match intent are fixed in the phase where the feature that enables correct behavior lands.

Agent workflow: Complete ONE phase at a time. After each phase, commit the work, run cargo test --all --all-targets to confirm 100% of tests pass (0 failures, 0 ignored unless pre-existing), and stop. Do not begin the next phase. A human must review the completed phase and explicitly approve before the next phase begins. This is a hard rule — never do more than one phase without human-in-the-loop review. Each phase should be a separate commit (or small series of commits).

Phase 1: Standalone renames and syntax ✅

No semantic changes. Clears the deck so subsequent code matches the doc’s notation.

• Rename array_set → array_write — pure rename across grammar, interpreter, type system, and all tests. Current array_set already has “ignore previous value” semantics.
• Rename given_from → given — skipped. The parser prefix ambiguity between given and given_from[...] is unresolved and not worth the risk. Keeping given_from[places] as-is.
• Remove Flags::Dropped — replaced all uses of Flags::Dropped with Word::Uninitialized. Removed Dropped from the Flags enum. Added try_read_flags() helper that returns Option<Flags> (None for uninitialized, Some(flags) for live values). Callers now check for Word::Uninitialized before calling expect_flags(). Error messages are “access of uninitialized value” uniformly. Note: and_drop_fields still silently skips uninitialized boxed values rather than erroring — this is needed because the interpreter’s end-of-scope cleanup drops ALL variables unconditionally without checking wholeness. Phase 4’s whole-place checks will allow this to become an error.
• Scrub entire array backing on refcount zero — when an array’s refcount reaches 0, all words in the backing allocation (header + elements) are set to Word::Uninitialized. Freed arrays now disappear completely from heap snapshots. Updated 44 test snapshots.
• param is pred syntax — flipped both Predicate::Parameter and Predicate::Variance grammar from #[grammar($v0($v1))] to #[grammar($v1 is $v0)]. All predicates now use consistent param is pred syntax (e.g., P is mut, T is relative, T is atomic). Added is to KEYWORDS. Updated all test programs and where clauses. Class predicates (given class, shared class) are unchanged.

Phase 2: Permission parameter plumbing ✅

Add P and A parameters to array ops. Loosen access requirements. Keep current behavior — all existing call sites pass P = given (or equivalent).

• Add P, A parameters to array_give — array_give[T, P, A](array, index). No grammar annotation change needed — $[v0] already parses a Vec<Parameter> as a comma-separated list inside brackets. The interpreter/type-checker code that destructures the parameter list changes from expecting 1 element to expecting 3. Interpreter: extract P and A from parameters but dispatch only on P=given (move, current behavior). Type system: accept 3 type parameters, check array expression against A Array[T], return P T.
• Add P, A parameters to array_drop — array_drop[T, P, A](array, index). Same as above — no grammar annotation change for the bracket params. Keep single-index for now. Interpreter: extract P, dispatch only on P=given (drop, current behavior). Type system: check array expression against A Array[T] (no mut requirement — loosened from current mut).
• Add A parameter to array_write — array_write[T, A](array, index, value). Same — no grammar annotation change. Type system: require A is mut via prove_is_mut(A), check array expression against A Array[T].
• Add A parameter to array_capacity — array_capacity[T, A](array). Same — no grammar annotation change. Type system: check array expression against A Array[T] (accepts any perm).

TDD notes: Update all existing test call sites from array_give[T](...) to array_give[T, given, ref[a]](...) etc. Tests should pass with identical behavior since P=given matches current semantics. Key tests to watch:

• array_give_given_class_moves_out — should keep move semantics with explicit P = given
• array_drop_element, array_drop_class_element — should keep drop semantics with P = given
• array_capacity_given, array_capacity_shared, array_capacity_ref — should all work with A is ref

Phase 3: Poly-permission semantics

Implement dispatch on P for array_give and array_drop. Add range semantics to array_drop.

• array_give dispatches on P + runtime flags — The interpreter translates P into owner_operms via perm_to_operms(P), then calls the standard object_value_to_data on the element with its raw type T and that owner_operms. For boxed elements, the runtime Flags word is composed with owner_operms via with_projection_flags — runtime Shared always overrides to Shared, runtime Given passes through the owner_operms. This correctly handles subtyping: a shared value stored in a ref-typed slot produces a shared copy (rc++), not a leaked borrow. The result is passed to give_place which dispatches on the final operms. The earlier object_value_to_data_from_ty (which derived operms from the static type, ignoring runtime flags) was deleted. The P is shared ↔ A is shared assertion was invalidated by the subtyping scenario and removed.
• array_drop dispatches on P — given → actually drop each element in range, else → no-op. Dispatch uses prove_is_given(P) (the permission alone, not P T). Even copy types like shared class are dropped when P=given — needed to avoid leaking refcounts on boxed fields inside shared classes.
• array_drop range semantics — changed grammar from (array, index) to (array, from, to), drops elements in from..to range (exclusive) in forward order. from >= to is a no-op. All existing single-index array_drop(a, i) calls rewritten to array_drop(a, i, i + 1). Updated type system, interpreter, liveness, and all tests.

TDD notes — tests written and passing:

• array_give_p_mut — array_give[Data, mut[a], ref[a]](a.ref, 0) returns a mut[a] Data ✅

• array_give_p_shared — array_give[Array[Int], shared, ref[outer]](outer.ref, 0) returns a shared copy, rc incremented ✅

• array_give_p_ref — array_give[Array[Int], ref[outer], ref[outer]](outer.ref, 0) returns a borrowed copy ✅

• array_drop_p_shared_is_noop — array_drop[Data, shared, ref[a]](a.ref, 0, 1) does nothing, element still accessible ✅

• array_drop_p_given_range — array_drop[Data, given, ref[a]](a.ref, 0, 3) drops elements 0, 1, 2 ✅

• array_give_p_given_int_is_copy — giving an Int element with P=given copies without uninitializing ✅

• array_drop_empty_range_is_noop — array_drop with from >= to is a no-op ✅

• array_drop_shared_class_element_is_noop — shared class (Pt) elements: array_drop[Pt, given, ...] is a no-op since given Pt is copy ✅

• array_give_ref_of_shared_is_shared — P = ref[shared_place] where the place is shared. The type system normalizes ref[shared_place] to shared before substitution, so P arrives as shared and the shared branch fires. This tests that a ref to a shared place correctly resolves to shared semantics.

class Data {}

fn head[perm P](array: P Array[Data]) -> P Data
where
    P is ref,
{
    array_give[Data, P, ref[array]](array.ref, 0)
}

fn main() {
    let array: given Array[Data] = array_new[Data](1)
    array_write[Data, mut[array]](array.mut, 0, new Data())
    let shared_array = array.give.share
    let elem0 = head[ref[shared_array]](shared_array.ref)
    # elem0 should be `shared Data`, not `ref Data`
}

Phase 3.5: Test rewrite

Rewrite existing tests to use the new array op signatures and express their intended semantics now that poly-permission and range ops are available.

• Restore shared-array test intent — shared_array_give_class_is_shared_copy already used P = shared explicitly after Phase 3. Verified refcount lifecycle. No change needed.

• Fix ref-array test intent — ref_array_give_int_element, ref_array_give_class_element updated to use P = ref[a] explicitly. ref_array_of_shared_arrays updated to use element type shared Array[Int] (matching test name) with P = ref[outer]. Key behavioral changes: ref_array_give_class_element now correctly shows d = ref [a] Data (borrowed copy, element stays initialized); ref_array_of_shared_arrays correctly shows got = shared Array { ... } (shared copy via runtime flags).

• Runtime-vs-static mismatch test — array_give_ref_of_runtime_shared_element: stores a shared array into a ref[dummy] Array[Int]-typed slot, gives with P = ref[outer]. Demonstrates that runtime Shared flags override static ref operms, producing a shared copy (rc++) instead of a borrowed copy (which would leak the refcount). This test motivated the deletion of object_value_to_data_from_ty and the switch to runtime-flag-based dispatch.

• Verify “freed” test snapshots — refcount_reaches_zero_frees_allocation and shared_array_all_refs_dropped_frees: backing allocations absent from heap ✅. nested_array_all_refs_freed: inner array backing (Alloc 0x03) correctly remains — arrays don’t drop their elements, so the inner array handle is scrubbed without being properly dropped. Updated comment to document this as expected leak behavior.

• Intentional leak tests — tests that deliberately skip array_drop on some or all elements, then drop the array. Uses Array[Array[Int]] so inner arrays are boxed with separate heap allocations that survive the outer’s scrub. Flat element types (like class Data { x: Int }) are stored inline and don’t produce separate allocations to leak.

  • array_leak_all_elements — create array of 2 inner arrays, drop outer without dropping elements. Both inner backing allocations remain as orphans.
  • array_leak_some_elements — drop element 0 of a 2-element array, skip element 1, drop outer. Element 1’s backing allocation remains.

TDD notes: This phase produces no new features — only test corrections that reflect the capabilities added in Phase 3 (poly-permission dispatch, range semantics). Do NOT add tests for Phase 4 features (drop sections, is_last_ref) or adjust snapshots to account for them. All tests should pass before and after, but the snapshots change to reflect correct behavior enabled by Phase 3. Use UPDATE_EXPECT=1 after verifying each test’s intent is right.

Phase 4: Drop sections

Grammar, type checking, and interpreter support for drop { ... } blocks and whole-place drop semantics.

4a: Grammar ✅

• drop { ... } in ClassDecl — added DropBody enum (None | Block(Vec<Statement>)) with Default derive to ClassDeclBoundData. Grammar: drop { stmts } after methods. Updated all destructuring sites. Added 3 parser tests.

4b: Type checker ✅

• Type-check drop body — added check_drop_body judgment to classes.rs. For given class: type-checks with self: given Class[...]. For class (share) and shared class: introduces a universal perm variable P with P is copy assumed, then type-checks with self: P Class[...]. This means the drop body can read fields (via .ref or .give which copies) but cannot mutate or move fields. Added open_universal_perm_var() helper to Env. Tests: drop_body_prints_field, given_class_drop_body_can_move, share_class_drop_body_cannot_move_field, share_class_drop_body_cannot_mut_field, shared_class_drop_body_ref_self, empty_drop_body, drop_body_accesses_class_generics.
• Array elements are not accessible places — confirmed the type checker already rejects array[i].give because Projection::Index is for tuples only. Added test array_index_not_accessible_place. Note: formality-core parses kind keywords as ty and perm (not type and perm), so generic class tests must use [ty T] not [type T].

4c: Interpreter ✅

• Bool type and operators — added Bool to TypeName (shared class, always copyable, 1 word, Word::Int representation). Added true/false as Expr variants with KEYWORDS. Added BinaryOp enum (Add, Sub, Ge, Le, Eq, Ne) with a single Expr::BinaryOp(lhs, op, rhs) variant. Type rules grouped into “arithmetic” (Int→Int) and “comparison” (Int→Bool). Changed Expr::If condition from Int to Bool. Updated 5 existing tests. Note: bare > and < omitted due to parser prefix ambiguity with >=/<= in formality-core; the restricted set is sufficient.
• is_last_ref intrinsic — added is_last_ref[perm A](value: A T) -> Bool as Expr::IsLastRef. Type system accepts any value, returns Bool. Interpreter: for boxed types returns refcount == 1, for non-boxed types returns false.
• Execute drop body — drop_value checks if value is an owned class with a non-empty drop body. Only runs for owned handles (given/shared), not borrowed. Only runs if value is “whole” (all fields initialized via is_value_whole). Drop body runs BEFORE field-by-field cleanup. self type: given class → self: given Class[...], else → self: ref[magic] Class[...] using synthetic Var::Magic. Fixed drop_place for flat types to route through drop_value so drop body fires on explicit .drop. Added Access::Drop type rule.
• Whole-place drop — implemented as is_value_whole check inside drop_value rather than as a separate end-of-scope mechanism. For flat types, checks all words for Uninitialized. For boxed types, checks flags word. Partially-moved classes: drop body is skipped, but traverse_value + and_drop_fields still cleans up each field individually (uninitialized fields are skipped by try_read_flags returning None). This simpler approach works because and_drop_fields already handles uninitialized boxed fields gracefully.
• Array elements are not accessible places — already implemented (find_object_fields returns empty vec for arrays).

Tests written and passing:

• class_with_drop_body — drop body runs on scope exit ✅
• drop_body_runs_on_give — drop body runs on explicit .drop ✅
• drop_body_runs_on_every_shared_handle — two shared copies produce two drop runs ✅
• is_last_ref_true_when_sole_owner — boxed object with refcount 1 ✅
• is_last_ref_false_when_shared — shared array with refcount 2 ✅
• drop_body_with_is_last_ref — Vec-like conditional cleanup pattern ✅
• bool_true_false_literals — true/false display correctly ✅
• comparison_operators — all 6 comparisons work ✅
• subtraction — basic subtraction ✅
• partially_moved_class_drops_remaining_fields — drop body skipped, remaining fields cleaned ✅
• partial_move_then_read_other_field — Iterator.drop pattern works ✅
• drop_body_accesses_class_generics — full Vec+Item pattern with nested drops ✅

TDD notes — tests to write before implementing:

• class_with_drop_body — simple class with drop { print(self.x) }, verify drop body runs on scope exit
• drop_body_self_not_whole — class with drop body that moves one field; verify remaining fields are individually dropped, no infinite recursion
• partially_moved_class_drops_fields — move one field out of a class, verify remaining fields drop at scope exit but the class drop body does NOT run (self not whole)
• partial_move_then_read_other_field — move one field out of a struct, then read a different field with .give. Verify the read succeeds. This is the pattern Iterator.drop relies on (self.vec.data.give then self.vec.len.give). Already works in the interpreter (field projection is pure pointer arithmetic, no wholeness check), but worth an explicit test.
• vec_drop_cleans_elements — Vec class with drop { array_drop[T, given, ref[self]](self.data.ref, 0, self.len.give) }, verify elements are dropped when vec goes out of scope
• shared_class_drop_gets_ref_self — shared class with drop body, verify self: ref Class
• drop_runs_on_every_handle — shared class with drop body, create two shared handles, verify drop body runs twice (once per handle drop)
• is_last_ref_true_when_sole_owner — boxed object with one handle, is_last_ref returns true
• is_last_ref_false_when_shared — boxed object with two handles, is_last_ref returns false on first drop, true on second

Phase 5: Integration — Vec as a test program ✅

Write the full Vec and Iterator from the design doc as a test program that exercises the entire stack.

• Vec push and get — replaced the old vector_push_and_get test (was ignored, used outdated syntax). Fresh test vec_push_and_get_given uses the target signatures from the design doc. Also vec_push_increments_len for basic push. All pass end-to-end.
• Vec iter and next — vec_iter_and_next tests consuming iteration: creates Vec, pushes 3 items, creates iterator, calls next() once. Iterator.drop cleans up remaining elements (prints 20, 30). Verified elements moved out and cleanup correct.
• Shared Vec access — shared_vec_get with P = shared: elements are shared copies, array_drop is no-op, Vec.drop with is_last_ref only cleans up on final handle.
• Ref Vec access — ref_vec_get with P = ref[v]: elements are borrows, Vec remains intact.
• Vec drop lifecycle — vec_drop_cleans_all_elements: push 3 items, let Vec go out of scope. Drop body runs, is_last_ref true, all elements cleaned (prints 100, 200, 300). Heap is clean.

Implementation notes — interpreter fixes required:

Three interpreter bugs were found and fixed to make the Vec tests work:

1. call_method double-wrapped this_ty: The method’s this_decl.perm was applied on top of the receiver’s type, which already carried the correct permission from the access mode. E.g., v.mut.push[mut[v]]() produced receiver type mut[v] Vec[T], but call_method added another mut[v] on top → mut[v] mut[v] Vec[T]. Fixed by using this.ty directly.

2. is_mut_ref_type used prove_is_mut which failed on out-of-scope places: Inside a method, prove_is_mut(env, mut[v] Vec[T]) tries to resolve place v in the method’s env, but v is from the calling scope. Changed to structural pattern matching: matches!(ty, Ty::ApplyPerm(Perm::Mt(_), inner)) && !is_copy_type(inner). The !is_copy_type guard is needed because mut[x] Int is NOT stored as a MutRef — copy types are always inline.

3. give_place with MutRef operms on copy types: When accessing self.start.give through a mut ref (Iterator.next), the operms were MutRef but the field type was Int (copy). give_place blindly created a MutRef, but Int fields are stored inline, not through MutRef pointers. Fixed: if the type is copy, produce a ref copy instead of a MutRef.

Snapshot improvement: array_give_p_mut snapshot now correctly displays Data { x: 42 } instead of <unexpected: Int(42)> — the structural is_mut_ref_type correctly identifies and dereferences MutRef types during display.

Call site syntax: Method calls require the receiver to use an access mode: v.mut.push[mut[v]](...), v.give.get[given](...), v.ref.get[ref[v]](...). This matches the language rule that places always require an access mode.

Future work

• Reunify is_mut_ref_type with prove_is_mut — The interpreter’s is_mut_ref_type uses structural pattern matching (Ty::ApplyPerm(Perm::Mt(_), inner) where inner is not copy) instead of the type system’s prove_is_mut judgment. This divergence exists because prove_is_mut on Perm::Mt(places) resolves each place’s type via env.place_ty(place), but inside a method body the places (e.g., v in mut[v]) refer to the calling context and are not in the method’s env. Possible fixes: (a) enrich the method env with calling-context information, (b) add a simpler “structural” rule to prove_mut_predicate that recognizes Perm::Mt(_) as always mut without checking places, or (c) propagate where-clause assumptions into the interpreter’s env. Each has trade-offs — this should be revisited when the interpreter and type system are more integrated.

• Move Vec tests to assert_interpret! — Most Vec tests currently use assert_interpret_only! (interpreter-only, no type checking) because the type checker doesn’t yet support the permission patterns Vec uses (generic perm P self, given_from[self] return types, where-clause dispatch). As the type checker gains support for these features, migrate tests to assert_interpret! (type-check AND execute). Only keep assert_interpret_only! for tests that specifically exercise unsafe/UB patterns.

• Design unsafe effects — array operations are currently “magic” intrinsics that bypass normal permission rules (e.g., array_drop uninitializes element slots through A is ref). A proper unsafe effects system would describe and constrain what unsafe operations can do. Not needed for the current Vec milestone, but important for the broader language design.

Unsafe code

Levels of classes

• give class (can be given)
• share class (can be shared, the default)
• shared class (already shared)

Memory representation of values

We have two classes of values

• unique – these are give classes, share classes, and shared classes that have a type parameter which is unique
• shared – these are shared classes, integers, flags, characters (when we add those)

Unsafe primitives

There is a built-in type

• Array[T] – stores a ref count, a length, and N elements of type T (elements are initially uninitialized)

Array[T] is a share class and offers the following built-in operations (special expressions):

• ArrayNew[T](length: uint) -> Array[T], allocates an array of the given length
• ArrayCapacity[T](array: Array[T]) -> uint, returns the capacity that the array was created with
• ArrayGive[T](array: Array[T], index) -> given[array] T, gets an element from the array
• ArrayDrop[T](array: ref Array[T], index), drops an element from the array (recursively drops the element, marks slot uninitialized)
• ArraySet[T](array: Array[T], index, value: given T), initializes an element from the array for first time

Type sizes

size_of[T]() is a built-in expression that returns the number of Words needed to store a value of type T. It takes a single type parameter and no arguments. It type-checks to Int.

The interpreter evaluates size_of[T]() as:

• Int → 1
• Tuple(0) (i.e., ()) → 0
• A class → 1 (for the flags word if unique, 0 if shared) + sum of size_of for each field’s type
• Other (including Array[T] once added) → 1

The real system has more complex layout rules obviously.

Unique values

Unique values are 4-aligned and begin with a flags field:

+--------------+
| flags        |
| ...fields... |
+--------------+

Shared values

Shared values are just stored as a sequence of fields. No flags are needed because they are always copied out.

Representing in the interpreter

We will have a Alloc struct like

struct Alloc {
    data: Vec<Word>
}

enum Word {
    Int(isize),
    Array(Pointer),
    MutRef(Pointer),
    Flags(Flags),
    Uninitialized,
}

struct Pointer {
    index: usize,
    offset: usize,
}

enum Flags {
    // Indicates that the value is uninitialized
    Uninitialized,

    // Unique ownership
    Given,

    // Shared ownership
    Shared,

    // Copied fields from value stored elsewhere, either `ref` or `shared mut`
    Borrowed,
}

All values, including arrays, use the same Alloc struct. An Array[T] allocation stores the ref count and length as the first two words, followed by the elements:

+------------------+
| Int(refcount)    |
| Int(length)      |
| element 0        |   \
| ...              |    > each element is size_of[T]() words
| element N-1      |   /
+------------------+

Place operations

There are four operations on places:

• place.give
• place.ref
• place.mut
• place.drop

Each begins by evaluating the place which results in a Perm and a Pointer:

• the Perm represents the most restrictive we have passed through. If at any point we access an uninitialized flags the interpreter faults.
• the Pointer identifiers the location in memory that the place is stored

The Perm can be one of

enum Perm {
    Given,
    Shared,
    Borrowed,
    Mut,
}

The operations then proceed as follows:

• give examines the Flags
  • Given => copy the fields to the destination and then mark the Flags as Uninitialized
  • Shared => copy the fields to the destination, set the flags to Shared, and then apply the share operation to them (see below)
  • Borrowed => copy the fields to the destination, set the flags to Borrowed
  • Mut => create a MutRef with the pointer
• ref examines the Flags
  • Shared => copy the fields to the destination, set the flags to Shared, and then apply the share operation to them (see below)
  • Given | Borrowed | Mut => copy the fields to the destination, set the flags to Borrowed
• mut examines the Flags
  • Shared | Borrowed => fault
  • Given | Mut => create a MutRef value
• drop examines the Flags
  • Given => drop fields recursively
  • Shared => apply “drop shared” operation (see below)
  • Borrowed | Mut => no-op

The “drop shared” operation

When dropping a shared value, we visit its fields and check their type:

• for a give|share class, we recursively apply drop shared to its fields
• for an Array[T], decrement the ref count; if it reaches zero, recursively drop all initialized elements and free the array
• for a borrowed class | mut-ref, no-op
• for int | flags, ignore

The “share operation” (duplication accounting)

When a shared value is duplicated (by place.give or place.ref on a Shared value), we apply share_op to the copy to account for the new references:

• for a given|shared class, we recursively apply share op to its fields
• for an Array[T], inc the ref count
• for a borrowed class | mut-ref, no-op
• for int | flags, ignore

Converting to shared (in-place)

When value.share converts a value from Given to Shared, we apply convert_to_shared to recursively flip flags:

• for a given|shared class, flip flags Given→Shared, then recurse into fields
• for an Array[T], flip flags Given→Shared (no refcount change — no duplication)
• for a borrowed class | mut-ref, no-op
• for int | flags, ignore

Value operations

There is one operation on values:

• value.share

This operates on a value that has already been copied to a destination. It converts the value from unique to shared ownership:

• If the flags are Given, set them to Shared and apply the share operation to the fields
• If the flags are Shared or Borrowed, no-op (already shared or borrowed)

Array reference counting

Arrays are share class types. The ref count (stored at offset 0 of the array allocation) tracks how many live references exist.

Two share-related operations

There are two distinct operations that involve sharing:

1. convert_to_shared — in-place conversion from Given to Shared ownership. Called by Expr::Share (i.e., value.share). Recursively flips flags from Given→Shared on nested class fields. For arrays: just flips the value’s flags, no refcount change. No duplication occurs.

2. share_op — duplication accounting. Called when a Shared value is copied (by place.give or place.ref on a Shared value). For arrays: increments the refcount. For classes: recurses into fields to account for nested duplications.

The distinction matters because Expr::Share converts in place (one reference → one reference, no refcount change), while place.give on Shared duplicates the value (one reference → two references, refcount must increase).

Lifecycle

1. ArrayNew — allocates [Int(1), Int(length), elements...]. Refcount starts at 1.
2. value.share — flips flags Given→Shared via convert_to_shared. Refcount stays 1.
3. place.give on Shared — copies the value, calls share_op which increments refcount. Each additional copy adds 1.
4. drop (Given or Shared) — decrements refcount. If zero: recursively drop all initialized elements, then free the array allocation.

Implementation plan

Approach: doc-driven, test-driven

Each step follows the same rhythm:

1. Write/update mdbook chapter describing the feature or change
2. Write tests (interpreter tests using assert_interpret!, type system tests using assert_ok!/assert_err!) that express the expected behavior
3. Implement until the tests pass

The mdbook chapters to write/update:

• md/interpreter.md (existing) — describes the Alloc/Word/Pointer/Flags/TypedValue memory model, with word-level walkthrough and access mode table.
• md/wip/unsafe.md (this doc) — eventually becomes a real chapter covering Array[T], size_of, and the unsafe primitives.

Step 1: Remove PointerOps ✅

Removed TypeName::Pointer and all 6 PointerOps expression variants. Compiles and existing tests pass.

Step 2: Add size_of[T]() ✅

Added Expr::SizeOf(Vec<Parameter>) with #[grammar(size_of $[v0] ( ))]. Type-checks to Int. Interpreter computes word count: 1 for Int, flags + fields for classes, 0 for unit. 6 interpreter tests.

Step 3: Restructure interpreter memory model ✅

Replaced Value/ValueData/ObjectData/ObjectFlag with flat word-based memory:

• Alloc { data: Vec<Word> } — flat word arrays, no type tags in memory
• Word { Int, Flags, Uninitialized } — individual memory words
• Flags { Uninitialized, Given, Shared, Borrowed } — permission flags for unique objects
• Pointer { index, offset } — position within an allocation
• TypedValue { pointer, ty } — types flow through evaluation, not stored on allocations

Object layout: [Flags, field0_words..., field1_words...] for unique classes, [field0_words...] for shared classes (no flags word). Field access uses type-driven offset computation. Display: flag: Given (was Owned), flag: Borrowed (was Ref), shared classes omit flag entirely.

Step 4: Implement place operations (give/ref/mut/drop) ✅

Implemented flags-dependent place operations (give/ref/drop) dispatching on Given/Shared/Borrowed/Uninitialized. Added UB faulting — interpreter bails on all undefined behavior to enable fuzzing the type checker for soundness. Removed Access::Sh — share is now exclusively a value operation (Expr::Share), users write d.give.share. Added prove_is_shareable check to Expr::Share typing rule. Mut is stubbed (bail on use).

Step 4b: Doc/code review cleanup ✅

Reviewed interpreter.md + unsafe.md against the implementation. Fixed share_op ordering (flag flip before recurse) and break/return control flow (introduced Outcome enum, anyhow::Error reserved for UB faults). Remaining items tracked in WIP.md.

Step 5: Add Array[T] to grammar and implement operations

• Doc: expand md/wip/unsafe.md into a proper chapter — motivating example (building a simple Vec), then walk through ArrayNew/Initialize/Get/Drop.
• Tests first: write interpreter tests — create array, initialize elements, read them back, drop elements. Test out-of-bounds faults. Test uninitialized read faults.
• Add TypeName::Array (with one type parameter T)
• Add 5 Array expression variants: ArrayNew[T](expr), ArrayCapacity[T](expr), ArrayGive[T](expr, expr), ArrayDrop[T](expr, expr), ArraySet[T](expr, expr, expr)
• Add Array keyword entries
• Add type-checking rules for all 5 operations
• Add match arms in type system (env.rs, liveness.rs, places.rs, types.rs)
• Interpreter implementation:
  • ArrayNew[T](length) — allocate [Int(1), Int(length), Uninitialized...]
  • ArrayCapacity[T](array) — read length word
  • ArraySet[T](array, index, value) — write element at computed offset
  • ArrayGive[T](array, index) — read element via give semantics
  • ArrayDrop[T](array, index) — recursively drop element, mark slot uninitialized
• Goal: arrays work end-to-end

Step 6: Implement reference counting for arrays

• Doc: add section to array chapter on sharing and ref counting — walk through what happens when an array is shared, how ref count increments/decrements, when elements get dropped.
• Tests first: write interpreter tests — shared array survives after original dropped, array freed when last reference dropped, elements recursively dropped on array free.
• Share operation increments array ref count
• Drop-shared decrements ref count, frees when zero
• Goal: array ref counting works correctly

FAQ

Why not have a specialized ArrayAlloc instead of using generic Alloc?

We use a single Alloc type for all allocations, with arrays storing their ref count and length as the first two words by convention. A specialized ArrayAlloc would be more type-safe in the interpreter, but we expect to add more ref-counted allocation kinds in the future (e.g., a Box-like type that carries just a ref count + value). Keeping one uniform allocation pool with layout-by-convention is simpler and more extensible than adding a new allocation variant for each kind.