fix unsoundness: refactor to unflattened chains

we no longer expand `shared[p]` when creating
a reduced term but instead do it on cancellation
only

src/type_system.rs

@@ -11,8 +11,8 @@ mod classes;
 mod env;
 mod expressions;
 mod in_flight;
-mod liens;
 mod liveness;
+mod local_liens;
 mod methods;
 mod places;
 mod predicates;

src/type_system/accesses.rs

@@ -2,7 +2,12 @@ use formality_core::{judgment_fn, Cons};
 
 use crate::{
     grammar::{Access, FieldDecl, Parameter, Place, Ty},
-    type_system::{env::Env, liens::liens, liveness::LivePlaces, quantifiers::fold},
+    type_system::{
+        env::Env,
+        liveness::LivePlaces,
+        local_liens::{local_liens, LocalLien},
+        quantifiers::fold,
+    },
 };
 
 use super::red_terms::Lien;
@@ -104,9 +109,9 @@ judgment_fn! {
         debug(parameter, access, place, env)
 
         (
-            (liens(&env, p) => liens_p)
+            (local_liens(&env, p) => liens_p)
             (fold(&env, liens_p, &|env, lien| {
-                lien_permit_access(env, lien, access, &place)
+                local_lien_permit_access(env, lien, access, &place)
             }) => env)
             -------------------------------- ("parameter")
             (parameter_permits_access(env, p, access, place) => env)
@@ -115,29 +120,24 @@ judgment_fn! {
 }
 
 judgment_fn! {
-    fn lien_permit_access(
+    fn local_lien_permit_access(
         env: Env,
-        lien: Lien,
+        lien: LocalLien,
         access: Access,
         accessed_place: Place,
     ) => Env {
         debug(lien, access, accessed_place, env)
 
-        (
-            -------------------------------- ("our-or-var")
-            (lien_permit_access(env, Lien::Our | Lien::Variable(_), _access, _accessed_place) => env)
-        )
-
         (
             (shared_place_permits_access(place, access, accessed_place) => ())
             -------------------------------- ("shared")
-            (lien_permit_access(env, Lien::Shared(place), access, accessed_place) => &env)
+            (local_lien_permit_access(env, LocalLien::Shared(place), access, accessed_place) => &env)
         )
 
         (
             (leased_place_permits_access(place, access, accessed_place) => ())
             -------------------------------- ("leased")
-            (lien_permit_access(env, Lien::Leased(place), access, accessed_place) => &env)
+            (local_lien_permit_access(env, LocalLien::Leased(place), access, accessed_place) => &env)
         )
     }
 }

src/type_system/local_liens.rs

@@ -0,0 +1,119 @@
+use formality_core::{judgment_fn, set, term, Set};
+
+use crate::{
+    grammar::{NamedTy, Parameter, Place},
+    type_system::{
+        env::Env,
+        quantifiers::union,
+        red_terms::{red_term, Chain, Lien, RedPerm, RedTerm, RedTy},
+    },
+};
+
+/// A lien on some data local to the current function.
+/// This is a subset of the full [`Lien`] type that only
+/// contains those variants relative to borrow checking.
+#[term]
+pub enum LocalLien {
+    Shared(Place),
+    Leased(Place),
+}
+
+judgment_fn! {
+    pub fn local_liens(
+        env: Env,
+        a: Parameter,
+    ) => Set<LocalLien> {
+        debug(a, env)
+
+        (
+            (red_term(&env, a) => RedTerm { red_perm, red_ty })
+            (local_liens_from_red_perm(&env, red_perm) => liens_1)
+            (local_liens_from_red_ty(&env, &red_ty) => liens_2)
+            ----------------------------------- ("my")
+            (local_liens(env, a) => (&liens_1, liens_2))
+        )
+    }
+}
+
+judgment_fn! {
+    fn local_liens_from_red_ty(
+        env: Env,
+        a: RedTy,
+    ) => Set<LocalLien> {
+        debug(a, env)
+
+        (
+            ----------------------------------- ("none")
+            (local_liens_from_red_ty(_env, RedTy::None) => ())
+        )
+
+        (
+            ----------------------------------- ("var")
+            (local_liens_from_red_ty(_env, RedTy::Var(_var)) => ())
+        )
+
+        (
+            (union(parameters, &|parameter| local_liens(&env, parameter)) => liens)
+            ----------------------------------- ("named")
+            (local_liens_from_red_ty(_env, RedTy::NamedTy(NamedTy { name: _, parameters })) => liens)
+        )
+    }
+}
+
+judgment_fn! {
+    fn local_liens_from_red_perm(
+        env: Env,
+        a: RedPerm,
+    ) => Set<LocalLien> {
+        debug(a, env)
+
+        (
+            (union(chains, &|chain| local_liens_from_chain(&env, chain)) => liens)
+            ----------------------------------- ("none")
+            (local_liens_from_red_perm(_env, RedPerm { chains }) => liens)
+        )
+    }
+}
+
+judgment_fn! {
+    fn local_liens_from_chain(
+        env: Env,
+        a: Chain,
+    ) => Set<LocalLien> {
+        debug(a, env)
+
+        (
+            (union(liens, &|lien| local_liens_from_lien(&env, lien)) => liens_out)
+            ----------------------------------- ("none")
+            (local_liens_from_chain(_env, Chain { liens }) => liens_out)
+        )
+    }
+}
+
+judgment_fn! {
+    fn local_liens_from_lien(
+        env: Env,
+        a: Lien,
+    ) => Set<LocalLien> {
+        debug(a, env)
+
+        (
+            ----------------------------------- ("none")
+            (local_liens_from_lien(_env, Lien::Our | Lien::Variable(_)) => ())
+        )
+
+        (
+            (let place_ty = env.place_ty(&place)?)
+            (local_liens(&env, place_ty) => liens)
+            ----------------------------------- ("shared")
+            (local_liens_from_lien(_env, Lien::Shared(place)) => set![LocalLien::shared(&place), ..liens])
+        )
+
+        (
+            (let place_ty = env.place_ty(&place)?)
+            (local_liens(&env, place_ty) => liens)
+            ----------------------------------- ("leased")
+            (local_liens_from_lien(_env, Lien::Leased(place)) => set![LocalLien::leased(&place), ..liens])
+        )
+    }
+}

src/type_system/predicates.rs

@@ -84,6 +84,21 @@ judgment_fn! {
     }
 }
 
+judgment_fn! {
+    pub fn prove_is_lent(
+        env: Env,
+        a: Parameter,
+    ) => () {
+        debug(a, env)
+
+        (
+            (prove_predicate(env, Predicate::lent(a)) => ())
+            ---------------------------- ("is-lent")
+            (prove_is_lent(env, a) => ())
+        )
+    }
+}
+
 pub fn prove_is_move_if_some(
     env: impl Upcast<Env>,
     a: impl Upcast<Option<Parameter>>,

src/type_system/red_terms.rs

@@ -141,6 +141,23 @@ impl Chain {
         }
     }
 
+    /// Creates a new chain `our self`.
+    pub fn copied(&self, env: &Env) -> Chain {
+        Chain::our().concat(env, self)
+    }
+
+    /// Create a new chain of custody from a shared or leased permission.
+    /// This either uses the chain of the shared/leased place (`other`),
+    /// if that is copy, or else uses `self`.
+    fn under(&self, env: &Env, other: impl Upcast<Chain>) -> Chain {
+        let other: Chain = other.upcast();
+        if other.is_copy(env) {
+            other
+        } else {
+            self.clone()
+        }
+    }
+
     /// Create a new chain of custody `(self other)`.
     pub fn concat(&self, env: &Env, other: impl Upcast<Chain>) -> Chain {
         let other: Chain = other.upcast();
@@ -153,14 +170,14 @@ impl Chain {
         }
     }
 
-    pub fn concat_perm(&self, env: &Env, other: impl Upcast<RedPerm>) -> Fallible<RedPerm> {
+    fn concat_perm(&self, env: &Env, other: impl Upcast<RedPerm>) -> Fallible<RedPerm> {
         let RedPerm { chains } = other.upcast();
         Ok(RedPerm {
             chains: chains.into_iter().map(|c| self.concat(&env, c)).collect(),
         })
     }
 
-    pub fn concat_term(&self, env: &Env, other: impl Upcast<RedTerm>) -> Fallible<RedTerm> {
+    fn concat_term(&self, env: &Env, other: impl Upcast<RedTerm>) -> Fallible<RedTerm> {
         let RedTerm { red_perm, red_ty } = other.upcast();
         Ok(RedTerm {
             red_perm: self.concat_perm(&env, red_perm)?,
@@ -220,6 +237,14 @@ pub enum Lien {
 
 cast_impl!(Lien);
 impl Lien {
+    pub fn shared(place: impl Upcast<Place>) -> Lien {
+        Lien::Shared(place.upcast())
+    }
+
+    pub fn leased(place: impl Upcast<Place>) -> Lien {
+        Lien::Leased(place.upcast())
+    }
+
     pub fn is_copy(&self, env: &Env) -> bool {
         match self {
             Lien::Our | Lien::Shared(_) => true,
@@ -355,15 +380,15 @@ judgment_fn! {
             (let place_ty = env.place_ty(&place)?)
             (chain_of_custody(&env, place_ty) => chain)
             ----------------------------------- ("shared")
-            (chain_of_custody(env, Perm::Shared(places)) => Chain::shared(&place).concat(&env, chain))
+            (chain_of_custody(env, Perm::Shared(places)) => Chain::shared(&place).under(&env, chain))
         )
 
         (
             (&places => place)
             (let place_ty = env.place_ty(&place)?)
             (chain_of_custody(&env, place_ty) => chain)
             ----------------------------------- ("leased")
-            (chain_of_custody(env, Perm::Leased(places)) => Chain::leased(&place).concat(&env, chain))
+            (chain_of_custody(env, Perm::Leased(places)) => Chain::leased(&place).under(&env, chain))
         )
 
         (