Skip to content

Commit

Permalink
simplify and describe the subtyping rules
Browse files Browse the repository at this point in the history 
The previous rules permitted cases that I did not
understand. These rules are less permissive but
make some intuitive sense to me. They also seem
to accept all the test cases.
  • Loading branch information
@nikomatsakis
nikomatsakis committed Jan 18, 2025
1 parent b90e34e commit fe9cb60
Show file tree
Hide file tree
Showing 7 changed files with 99 additions and 103 deletions.
27 changes: 16 additions & 11 deletions src/type_system/lien_chains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,24 @@ cast_impl!(TyChain);
/// A *lien chain* indicates the "history" of the liens on a given object.
/// For example `shared[x] leased[y]` means that the object was leased from `y`
/// and then the leased value was shared from `x`.
/// See also [`TyChain`][]s, which represent the combination of a [`LienChain`][]
/// applied to a type (e.g., `shared[x] leased[y] String`).
///
/// Due to subtyping, lien chains may be *incomplete*, in which they are
/// missing some elements in the middle. e.g. `shared(x) leased(y) my` is a
/// subchain of `shared(x) my`. Inuitively, this is ok because the type of `x`
/// still holds the lease on `y`.
/// An empty lien chain is special -- it represents a fully owned value (`my`, in surface syntax).
/// For non-empty lien chains, the lien has special signifiance because it impacts the
/// layout of the value the lien chain is attached to. A `leased[p]` lien chain, in particular,
/// will always create a pointer value, whereas other liens are passed by value.
///
/// Lien chains are computed by the `ty_chains` and `lien_chains`
/// judgments.
/// The *extension* of a lien chain is the lien chain excluding its first lien.
/// Unlike the full lien chain, the extension has no impact on the layout of the value
/// (for example, a `our leased[p] String` is still passed by value, even though
/// its lien chain has an extension of `leased[p]`).
///
/// Lien chains are computed by the [`lien_chains`][] judgment.
/// This judgment fills in "gaps" that users may leave in the surface syntax.
/// For example, supposed that `p: leased[q] String`
/// and the user writes `shared[p] String`. That will be elabored by by [`lien_chains`][]
/// to a [`LienChain`][] like `shared[q] leased[p]`.
#[derive(Clone, PartialOrd, Ord, PartialEq, Eq, Hash)]
pub struct LienChain {
pub vec: Vec<Lien>,
Expand Down Expand Up @@ -135,11 +145,6 @@ impl LienChain {
) -> (Self, LienChain) {
self.apply_lien(env, Lien::Leased(place.upcast()), pending)
}

/// True if this chain is non-empty (and thus does not necessarily represent unique ownership).
pub fn is_not_my(&self) -> bool {
!self.vec.is_empty()
}
}

impl Lien {
Expand Down
71 changes: 25 additions & 46 deletions src/type_system/subtypes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ use crate::{
env::Env,
is_::{lien_chain_is_copy, lien_chain_is_leased, lien_chain_is_owned},
lien_chains::{lien_chains, ty_chains, Lien, LienChain, My, Our, TyChain},
lien_set::lien_set_from_chain,
liveness::LivePlaces,
predicates::prove_predicate,
quantifiers::{fold, fold_zipped},
Expand Down Expand Up @@ -228,14 +227,24 @@ judgment_fn! {
(sub_lien_chains(env, _live_after, My(), b) => &env)
)

// Our is a subchain of everything that is copy.
//
// It has full permissions but it is not layout compatible with leased.

(
(lien_chain_is_copy(&env, &b) => ())
--------------------------- ("our-copy")
(sub_lien_chains(env, _live_after, Our(), b) => &env)
)

// If the start of `a` is *covered* by the start of `b`
// (covered = gives a superset of permissions)
// and all permissions from the subchains are also covered,
// then `a` is a subpermission of `b`.

(
(lien_covered_by(&env, lien_a, lien_b) => ())
(lien_chain_covered_by(&env, &chain_a, &chain_b) => env)
(extension_covered_by(&env, &chain_a, &chain_b) => env)
--------------------------- ("matched starts")
(sub_lien_chains(env, _live_after, Cons(lien_a, chain_a), Cons(lien_b, chain_b)) => &env)
)
Expand Down Expand Up @@ -265,35 +274,26 @@ judgment_fn! {
}

judgment_fn! {
/// A lien chain `a` is *covered by* a lien chain `b` if, when applied to some data in place `p`,
///
/// 1. `a` gives a superset of `b`'s permissions to `p`
/// 2. `a` gives a superset of `b`'s permissions to other places
///
/// This is analogous to [`lien_covered_by`][].
///
/// Examples:
///
/// * `shared[p.q]` is covered by `shared[p]` because
/// sharing `p` also shares all extensions of `p`.
/// * `our` is covered by `shared[p]` because `our`
/// restricts nothing.
/// * `leased[q]` is NOT covered by `shared[q]`; it meets condition (1)
/// but not condition (2), since `leased[q]` gives no access to `q`
/// but `shared[q]` gives read access to `q`.
fn lien_chain_covered_by(
/// We say that an extension `a` is *covered* by an extension `b` if they have
/// the same length and each lien in the extension covers the corresponding lien
/// in the other extension.
fn extension_covered_by(
env: Env,
a: LienChain,
b: LienChain,
) => Env {
debug(a, b, env)

(
(lien_set_from_chain(&env, &chain_a) => lien_set_a)
(lien_set_from_chain(&env, &chain_b) => lien_set_b)
(lien_set_covered_by(&env, &lien_set_a, &lien_set_b) => ())
--------------------------- ("chain-chain")
(lien_chain_covered_by(env, chain_a, chain_b) => &env)
------------------------------- ("my-*")
(extension_covered_by(env, My(), My()) => &env)
)

(
(lien_covered_by(&env, lien_a, lien_b) => ())
(extension_covered_by(&env, &chain_a, &chain_b) => env)
------------------------------- ("lien-lien")
(extension_covered_by(env, Cons(lien_a, chain_a), Cons(lien_b, chain_b)) => env)
)
}
}
Expand Down Expand Up @@ -325,28 +325,6 @@ judgment_fn! {
}
}

judgment_fn! {
fn lien_chain_strictly_covered_by(
env: Env,
a: LienChain,
b: LienChain,
) => () {
debug(a, b, env)

(
------------------------------- ("my-my")
(lien_chain_strictly_covered_by(_env, My(), My()) => ())
)

(
(lien_covered_by(&env, lien_a, lien_b) => ())
(lien_chain_strictly_covered_by(&env, &chain_a, &chain_b) => ())
------------------------------- ("lien-lien")
(lien_chain_strictly_covered_by(env, Cons(lien_a, chain_a), Cons(lien_b, chain_b)) => ())
)
}
}

judgment_fn! {
/// A lien `a` is *covered by* a lien `b` if, when applied to some data in place `p`,
///
Expand All @@ -371,6 +349,7 @@ judgment_fn! {
) => () {
debug(a, b, env)

// Our is covered by itself.
(
------------------------------- ("our-our")
(lien_covered_by(_env, Lien::Our, Lien::Our) => ())
Expand Down
38 changes: 21 additions & 17 deletions src/type_system/tests/subtyping.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,15 @@ fn give_from_our_Data_to_any_P() {
the rule "is_copy" failed at step #1 (src/file.rs:LL:CC) because
judgment `lien_chain_is_copy { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "var" failed at step #0 (src/file.rs:LL:CC) because
cyclic proof attempt: `prove_predicate { predicate: copy(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
cyclic proof attempt: `prove_predicate { predicate: copy(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`
the rule "our-copy" failed at step #0 (src/file.rs:LL:CC) because
judgment `lien_chain_is_copy { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "var" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_predicate { predicate: copy(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "shared" failed at step #0 (src/file.rs:LL:CC) because
judgment `is_copy { a: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "is_copy" failed at step #1 (src/file.rs:LL:CC) because
cyclic proof attempt: `lien_chain_is_copy { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
}

/// `our` is not a subtype of arbitrary P.
Expand Down Expand Up @@ -179,7 +187,15 @@ fn give_from_our_Data_to_leased_P() {
the rule "is_copy" failed at step #1 (src/file.rs:LL:CC) because
judgment `lien_chain_is_copy { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "var" failed at step #0 (src/file.rs:LL:CC) because
cyclic proof attempt: `prove_predicate { predicate: copy(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
cyclic proof attempt: `prove_predicate { predicate: copy(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`
the rule "our-copy" failed at step #0 (src/file.rs:LL:CC) because
judgment `lien_chain_is_copy { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "var" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_predicate { predicate: copy(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "shared" failed at step #0 (src/file.rs:LL:CC) because
judgment `is_copy { a: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "is_copy" failed at step #1 (src/file.rs:LL:CC) because
cyclic proof attempt: `lien_chain_is_copy { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d: our Data}, assumptions: {leased(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
}

#[test]
Expand Down Expand Up @@ -710,17 +726,9 @@ fn shared_pair1_leased_pair2_to_shared_pair1() {
the rule "cancel shared" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_lien_chains { a: our leased[pair2], b: shared[pair1], live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "matched starts" failed at step #1 (src/file.rs:LL:CC) because
judgment `lien_chain_covered_by { a: leased[pair2], b: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "chain-chain" failed at step #2 (src/file.rs:LL:CC) because
judgment `lien_set_covered_by { a: {leased[pair2]}, b: {}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
expression evaluated to an empty collection: `&b_s`
judgment had no applicable rules: `extension_covered_by { a: leased[pair2], b: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }`
the rule "matched starts" failed at step #1 (src/file.rs:LL:CC) because
judgment `lien_chain_covered_by { a: leased[pair2], b: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "chain-chain" failed at step #2 (src/file.rs:LL:CC) because
judgment `lien_set_covered_by { a: {leased[pair2]}, b: {}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
expression evaluated to an empty collection: `&b_s`"#]]);
judgment had no applicable rules: `extension_covered_by { a: leased[pair2], b: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared [pair1] leased [pair2] Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }`"#]]);
}
#[test]
#[allow(non_snake_case)]
Expand Down Expand Up @@ -761,11 +769,7 @@ fn our_leased_to_our() {
the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_lien_chains { a: our leased[pair], b: our, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased [pair] Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "matched starts" failed at step #1 (src/file.rs:LL:CC) because
judgment `lien_chain_covered_by { a: leased[pair], b: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased [pair] Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "chain-chain" failed at step #2 (src/file.rs:LL:CC) because
judgment `lien_set_covered_by { a: {leased[pair]}, b: {}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased [pair] Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
expression evaluated to an empty collection: `&b_s`"#]]);
judgment had no applicable rules: `extension_covered_by { a: leased[pair], b: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased [pair] Data, pair: Pair}, assumptions: {}, fresh: 0 } }`"#]]);
}

#[test]
Expand Down
Loading

0 comments on commit fe9cb60

Please sign in to comment.