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 })]
pub struct ClassDeclBoundData {
    pub predicates: Vec<Predicate>,
    pub fields: Vec<FieldDecl>,
    pub methods: Vec<MethodDecl>,
}

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 })]
pub struct ClassDeclBoundData {
    pub predicates: Vec<Predicate>,
    pub fields: Vec<FieldDecl>,
    pub methods: Vec<MethodDecl>,
}

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: _ } = 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 p = new Point (22, 44) ;
        Output: Trace:   p = Point { x: 22, y: 44 }
        Output: Trace:   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 this boxed value has been moved or dropped.
    /// Safe to skip during cleanup, no refcount to decrement.
    Dropped,

    /// 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: Map<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,
}

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 x = 10 ;
        Output: Trace:   x = 10
        Output: Trace:   let y = 20 ;
        Output: Trace:   y = 20
        Output: Trace:   x . give + 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 adder = new Adder (3, 4) ;
        Output: Trace:   adder = Adder { a: 3, b: 4 }
        Output: Trace:   adder . give . sum () ;
        Output: Trace:   enter Adder.sum
        Output: Trace:     self . a . give + 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 d = new Data (42) ;
        Output: Trace:   d = Data { x: 42 }
        Output: Trace:   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 d = new Data (42) ;
        Output: Trace:   d = Data { x: 42 }
        Output: Trace:   let s = d . give . share ;
        Output: Trace:   s = shared Data { x: 42 }
        Output: Trace:   let x1 = s . give ;
        Output: Trace:   x1 = shared Data { x: 42 }
        Output: Trace:   let x2 = s . give ;
        Output: Trace:   x2 = shared Data { x: 42 }
        Output: Trace:   print(x1 . give) ;
        Output: shared Data { x: 42 }
        Output: Trace:   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 d = new Data (42) ;
        Output: Trace:   d = Data { x: 42 }
        Output: Trace:   print(d . ref) ;
        Output: ref [d] Data { x: 42 }
        Output: Trace:   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 d = new Data (42) ;
        Output: Trace:   d = Data { x: 42 }
        Output: Trace:   let s = d . give . share ;
        Output: Trace:   s = shared Data { x: 42 }
        Output: Trace:   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 o = new Outer (new Inner (1)) ;
        Output: Trace:   o = Outer { inner: Inner { x: 1 } }
        Output: Trace:   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 d = new Data (42) ;
        Output: Trace:   d = Data { x: 42 }
        Output: Trace:   let r = d . ref ;
        Output: Trace:   r = ref [d] Data { x: 42 }
        Output: Trace:   r . drop ;
        Output: Trace:   r . give ;
        Output: Trace: exit Main.main => ref [d] Data { x: 42 }
        Result: Ok: ref [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 1 { result = 42; } else { result = 0; };
                result.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let result = 0 ;
        Output: Trace:   result = 0
        Output: Trace:   if 1 { result = 42 ; } else { result = 0 ; } ;
        Output: Trace:   result = 42 ;
        Output: Trace:   result = 42
        Output: Trace:   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 0 { result = 42; } else { result = 99; };
                result.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let result = 0 ;
        Output: Trace:   result = 0
        Output: Trace:   if 0 { result = 42 ; } else { result = 99 ; } ;
        Output: Trace:   result = 99 ;
        Output: Trace:   result = 99
        Output: Trace:   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).share;
                array_set[Int](a.give, 0, 10);
                array_set[Int](a.give, 1, 20);
                array_set[Int](a.give, 2, 30);
                print(array_give[Int](a.give, 0));
                print(array_give[Int](a.give, 1));
                array_give[Int](a.give, 2);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Int](3) . share ;
        Output: Trace:   a = shared Array { flag: Shared, rc: 1, ⚡, ⚡, ⚡ }
        Output: Trace:   array_set [Int](a . give , 0 , 10) ;
        Output: Trace:   array_set [Int](a . give , 1 , 20) ;
        Output: Trace:   array_set [Int](a . give , 2 , 30) ;
        Output: Trace:   print(array_give [Int](a . give , 0)) ;
        Output: 10
        Output: Trace:   print(array_give [Int](a . give , 1)) ;
        Output: 20
        Output: Trace:   array_give [Int](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).share;
                array_set[Int](a.give, 0, 42);
                let x = array_give[Int](a.give, 0);
                let y = array_give[Int](a.give, 0);
                print(x.give);
                y.give;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Int](1) . share ;
        Output: Trace:   a = shared Array { flag: Shared, rc: 1, ⚡ }
        Output: Trace:   array_set [Int](a . give , 0 , 42) ;
        Output: Trace:   let x = array_give [Int](a . give , 0) ;
        Output: Trace:   x = 42
        Output: Trace:   let y = array_give [Int](a . give , 0) ;
        Output: Trace:   y = 42
        Output: Trace:   print(x . give) ;
        Output: 42
        Output: Trace:   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).share;
                array_set[Data](a.give, 0, new Data(42));
                let x = array_give[Data](a.give, 0);
                print(x.give);
                // Element still available — shared, no move.
                array_give[Data](a.give, 0);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Data](1) . share ;
        Output: Trace:   a = shared Array { flag: Shared, rc: 1, Data { x: ⚡ } }
        Output: Trace:   array_set [Data](a . give , 0 , new Data (42)) ;
        Output: Trace:   let x = array_give [Data](a . give , 0) ;
        Output: Trace:   x = shared Data { x: 42 }
        Output: Trace:   print(x . give) ;
        Output: shared Data { x: 42 }
        Output: Trace:   array_give [Data](a . give , 0) ;
        Output: Trace: exit Main.main => shared Data { x: 42 }
        Result: Ok: shared Data { x: 42 }
        Alloc 0x13: [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).share;
                array_set[Data](a.give, 0, new Data(42));
                array_set[Data](a.give, 1, new Data(99));
                print(array_give[Data](a.give, 0));
                array_give[Data](a.give, 1);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Data](2) . share ;
        Output: Trace:   a = shared Array { flag: Shared, rc: 1, Data { x: ⚡ }, Data { x: ⚡ } }
        Output: Trace:   array_set [Data](a . give , 0 , new Data (42)) ;
        Output: Trace:   array_set [Data](a . give , 1 , new Data (99)) ;
        Output: Trace:   print(array_give [Data](a . give , 0)) ;
        Output: shared Data { x: 42 }
        Output: Trace:   array_give [Data](a . give , 1) ;
        Output: Trace: exit Main.main => shared Data { x: 99 }
        Result: Ok: shared 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).share;
                array_set[Int](a.give, 0, 10);
                array_set[Int](a.give, 1, 20);
                let b = a.give;
                a.drop;
                print(array_give[Int](b.give, 0));
                array_give[Int](b.give, 1);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Int](2) . share ;
        Output: Trace:   a = shared Array { flag: Shared, rc: 1, ⚡, ⚡ }
        Output: Trace:   array_set [Int](a . give , 0 , 10) ;
        Output: Trace:   array_set [Int](a . give , 1 , 20) ;
        Output: Trace:   let b = a . give ;
        Output: Trace:   b = shared Array { flag: Shared, rc: 2, 10, 20 }
        Output: Trace:   a . drop ;
        Output: Trace:   print(array_give [Int](b . give , 0)) ;
        Output: 10
        Output: Trace:   array_give [Int](b . give , 1) ;
        Output: Trace: exit Main.main => 20
        Result: Ok: 20
        Alloc 0x17: [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_set[Int](a.ref, 0, 10);
                array_set[Int](a.ref, 1, 20);
                let b = a.give;
                array_give[Int](b.give, 0);
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Int](2) ;
        Output: Trace:   a = Array { flag: Given, rc: 1, ⚡, ⚡ }
        Output: Trace:   array_set [Int](a . ref , 0 , 10) ;
        Output: Trace:   array_set [Int](a . ref , 1 , 20) ;
        Output: Trace:   let b = a . give ;
        Output: Trace:   b = Array { flag: Given, rc: 1, 10, 20 }
        Output: Trace:   array_give [Int](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).share;
                array_set[Data](a.give, 0, new Data(1));
                array_set[Data](a.give, 1, new Data(2));
                a.drop;
                0;
            }
        }
    },
    expect_test::expect![[r#"
        Output: Trace: enter Main.main
        Output: Trace:   let a = array_new [Data](2) . share ;
        Output: Trace:   a = shared Array { flag: Shared, rc: 1, Data { x: ⚡ }, Data { x: ⚡ } }
        Output: Trace:   array_set [Data](a . give , 0 , new Data (1)) ;
        Output: Trace:   array_set [Data](a . give , 1 , new Data (2)) ;
        Output: Trace:   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

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.