diff --git a/.gitignore b/.gitignore
index c45c8ebf9f..d3f7b8c041 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
+*.agdai
 /book
 /target
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index c3786707fa..3cf1c8f833 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -135,6 +135,7 @@
     - [Grammar summary](grammar.md)
     - [Syntax index](syntax-index.md)
     - [Macro follow-set ambiguity formal specification](macro-ambiguity.md)
+    - [Formal scoping model](scoping-model.lagda.md)
     - [Influences](influences.md)
     - [Test summary](test-summary.md)
     - [Glossary](glossary.md)
diff --git a/src/destructors.md b/src/destructors.md
index 73b4d65948..9c4b55046a 100644
--- a/src/destructors.md
+++ b/src/destructors.md
@@ -375,11 +375,8 @@ r[destructors.scope.lifetime-extension]
 > [!NOTE]
 > The exact rules for temporary lifetime extension are subject to change. This is describing the current behavior only.
 
-r[destructors.scope.lifetime-extension.let]
-The temporary scopes for expressions in `let` statements are sometimes
-*extended* to the scope of the block containing the `let` statement. This is
-done when the usual temporary scope would be too small, based on certain
-syntactic rules. For example:
+r[destructors.scope.lifetime-extension.intro]
+The temporary scopes for expressions are sometimes *extended*. This is done when the usual temporary scope would be too small, based on certain syntactic rules. For example:
 
 ```rust
 let x = &mut 0;
@@ -388,21 +385,35 @@ let x = &mut 0;
 println!("{}", x);
 ```
 
-r[destructors.scope.lifetime-extension.static]
-Lifetime extension also applies to `static` and `const` items, where it
-makes temporaries live until the end of the program. For example:
+r[destructors.scope.lifetime-extension.sub-expressions]
+A *place base context* is an expression context that is one of the following:
+
+- The operand of a [dereference][dereference expression], [field][field expression], or [tuple indexing expression].
+- The indexed expression of an [indexing expression].
+- The operand of a [borrow expression] in a place base context.
+
+The *projected expression* of an expression in a place base context is its closest ancestor that is not in a place base context.
+
+The temporary scope of an expression in a place base context is defined to be the temporary scope of its projected expression.
 
 ```rust
-const C: &Vec<i32> = &Vec::new();
-// Usually this would be a dangling reference as the `Vec` would only
-// exist inside the initializer expression of `C`, but instead the
-// borrow gets lifetime-extended so it effectively has `'static` lifetime.
-println!("{:?}", C);
+# use core::sync::atomic::{AtomicU64, Ordering::Relaxed};
+# static X: AtomicU64 = AtomicU64::new(0);
+# struct PrintOnDrop(&'static str);
+# impl Drop for PrintOnDrop {
+#     fn drop(&mut self) {
+#         X.fetch_add(1, Relaxed);
+#         println!("{}", self.0);
+#     }
+# }
+let x = &(0, PrintOnDrop("tuple 1 dropped")).0;
+let ref y = (0, PrintOnDrop("tuple 2 dropped")).0;
+// Though only its first field is borrowed, the temporary for the entire tuple
+// lives to the end of the block in both cases.
+println!("{x}, {y}");
+# assert_eq!(0, X.load(Relaxed));
 ```
 
-r[destructors.scope.lifetime-extension.sub-expressions]
-If a [borrow], [dereference][dereference expression], [field][field expression], or [tuple indexing expression] has an extended temporary scope, then so does its operand. If an [indexing expression] has an extended temporary scope, then the indexed expression also has an extended temporary scope.
-
 r[destructors.scope.lifetime-extension.patterns]
 #### Extending based on patterns
 
@@ -445,7 +456,7 @@ So `ref x`, `V(ref x)` and `[ref x, y]` are all extending patterns, but `x`, `&r
 
 r[destructors.scope.lifetime-extension.patterns.let]
 If the pattern in a `let` statement is an extending pattern then the temporary
-scope of the initializer expression is extended.
+scope of the initializer expression is extended to the scope of the block containing the `let` statement.
 
 ```rust
 # fn temp() {}
@@ -473,37 +484,99 @@ let &ref x = &*&temp(); // OK
 r[destructors.scope.lifetime-extension.exprs]
 #### Extending based on expressions
 
+r[destructors.scope.lifetime-extension.exprs.borrows]
+The [temporary scope] of the operand of a [borrow expression] outside of a [place base context][destructors.scope.lifetime-extension.sub-expressions] is the *borrow scope* of the operand expression, defined below.
+
+r[destructors.scope.lifetime-extension.exprs.super-macros]
+The [scope][temporary scope] of each [super temporary] of a [super macro call] expression is the borrow scope of the super macro call expression.
+
 r[destructors.scope.lifetime-extension.exprs.extending]
-For a let statement with an initializer, an *extending expression* is an
-expression which is one of the following:
+The borrow scope of an expression is defined in terms of *extending expressions* and their *extending parents*. An extending expression is an expression which is one of the following:
 
-* The initializer expression.
-* The operand of an extending [borrow] expression.
-* The [super operands] of an extending [super macro call] expression.
-* The operand(s) of an extending [array][array expression], [cast][cast
+* The operand of a [borrow expression], the extending parent of which is the borrow expression.
+* The [super operands] of a [super macro call] expression, the extending parent of which is the macro call expression.
+* The operand(s) of an [array][array expression], [cast][cast
   expression], [braced struct][struct expression], or [tuple][tuple expression]
-  expression.
-* The arguments to an extending [tuple struct] or [tuple enum variant] constructor expression.
-* The final expression of an extending [block expression] except for an [async block expression].
-* The final expression of an extending [`if`] expression's consequent, `else if`, or `else` block.
-* An arm expression of an extending [`match`] expression.
+  expression, the extending parent of which is the array, cast, braced struct, or tuple expression.
+* The arguments to a [tuple struct] or [tuple enum variant] constructor expression, the extending parent of which is the constructor expression.
+* The final expression of a plain [block expression] or [`unsafe` block expression], the extending parent of which is the block expression.
+* The final expression of an [`if`] expression's consequent, `else if`, or `else` block, the extending parent of which is the `if` expression.
+* An arm expression of a [`match`] expression, the extending parent of which is the `match` expression.
 
 > [!NOTE]
 > The desugaring of a [destructuring assignment] makes its assigned value operand (the RHS) an extending expression within a newly-introduced block. For details, see [expr.assign.destructure.tmp-ext].
 
-So the borrow expressions in `&mut 0`, `(&1, &mut 2)`, and `Some(&mut 3)`
+> [!NOTE]
+> `rustc` does not treat [array repeat operands] of [array] expressions as extending expressions. Whether it should is an open question.
+>
+> For details, see [Rust issue #146092](https://github.com/rust-lang/rust/issues/146092).
+
+So the borrow expressions in `{ &mut 0 }`, `(&1, &mut 2)`, and `Some(&mut 3)`
 are all extending expressions. The borrows in `&0 + &1` and `f(&mut 0)` are not.
 
-r[destructors.scope.lifetime-extension.exprs.borrows]
-The operand of an extending [borrow] expression has its [temporary scope] [extended].
+r[destructors.scope.lifetime-extension.exprs.parent]
+The borrow scope of an extending expression is the borrow scope of its extending parent.
 
-r[destructors.scope.lifetime-extension.exprs.super-macros]
-The [super temporaries] of an extending [super macro call] expression have their [scopes][temporary scopes] [extended].
+r[destructors.scope.lifetime-extension.exprs.let]
+The borrow scope of the initializer expression of a `let` statement is the scope of the block containing the `let` statement.
 
-> [!NOTE]
-> `rustc` does not treat [array repeat operands] of extending [array] expressions as extending expressions. Whether it should is an open question.
+> [!EXAMPLE]
+> In this example, the temporary value holding the result of `temp()` is extended to the end of the block in which `x` is declared:
 >
-> For details, see [Rust issue #146092](https://github.com/rust-lang/rust/issues/146092).
+> ```rust,edition2024
+> # fn temp() {}
+> let x = { &temp() };
+> println!("{x:?}");
+> ```
+>
+> `temp()` is the operand of a borrow expression, so its temporary scope is its borrow scope.
+> To determine its borrow scope, look outward:
+>
+> * Since borrow expressions' operands are extending, the borrow scope of `temp()` is the borrow scope of its extending parent, the borrow expression.
+> * `&temp()` is the final expression of a plain block. Since the final expressions of plain blocks are extending, the extended temporary scope of `&temp()` is the borrow scope of its extending parent, the block expression.
+> * `{ &temp() }` is the initializer expression of a `let` statement, so its borrow scope is the scope of the block containg that `let` statement.
+>
+> If not for temporary lifetime extension, the result of `temp()` would be dropped after evaluating the tail expression of the block `{ &temp() }` ([destructors.scope.temporary.enclosing]).
+
+r[destructors.scope.lifetime-extension.exprs.static]
+The borrow scope of the body expression of a [static][static item] or [constant item], and of the final expression of a [const block expression], is the entire program. This prevents destructors from being run.
+
+```rust
+# #[derive(Debug)] struct PanicOnDrop;
+# impl Drop for PanicOnDrop { fn drop(&mut self) { panic!() } }
+# impl PanicOnDrop { const fn new() -> PanicOnDrop { PanicOnDrop } }
+const C: &PanicOnDrop = &PanicOnDrop::new();
+// Usually this would be a dangling reference as the result of
+// `PanicOnDrop::new()` would only exist inside the initializer expression of
+// `C`, but instead the borrow gets lifetime-extended so it effectively has
+// a `'static` lifetime and its destructor is never run.
+println!("{:?}", C);
+// `const` blocks may likewise extend temporaries to the end of the program:
+// the result of `PanicOnDrop::new()` is not dropped.
+println!("{:?}", const { &PanicOnDrop::new() });
+```
+
+r[destructors.scope.lifetime-extension.exprs.other]
+The borrow scope of any other expression is its non-extended temporary scope, as defined by [destructors.scope.temporary.enclosing].
+
+> [!EXAMPLE]
+> In this example, the temporary value holding the result of `temp()` is extended to the end of the statement:
+>
+> ```rust,edition2024
+> # fn temp() {}
+> # fn use_temp(_: &()) {}
+> use_temp({ &temp() });
+> ```
+>
+> `temp()` is the operand of a borrow expression, so its temporary scope is its borrow scope.
+> To determine its borrow scope, look outward:
+>
+> * Since borrow expressions' operands are extending, the borrow scope of `temp()` is the borrow scope of its extending parent, the borrow expression.
+> * `&temp()` is the final expression of a plain block. Since the final expressions of plain blocks are extending, the borrow scope of `&temp()` is the borrow scope of its extending parent, the block expression.
+> * `{ &temp() }` is the argument of a call expression, which is not extending. Since no other cases apply, its borrow scope is its temporary scope.
+> * Per [destructors.scope.temporary.enclosing], the temporary scope of `{ &temp() }`, and thus the borrow scope of `temp()`, is the scope of the statement.
+>
+> If not for temporary lifetime extension, the result of `temp()` would be dropped after evaluating the tail expression of the block `{ &temp() }` ([destructors.scope.temporary.enclosing]).
 
 #### Examples
 
@@ -606,22 +679,6 @@ let x = 'a: { break 'a &temp() }; // ERROR
 # x;
 ```
 
-```rust,edition2024,compile_fail,E0716
-# use core::pin::pin;
-# fn temp() {}
-// The argument to `pin!` is only an extending expression if the call
-// is an extending expression. Since it's not, the inner block is not
-// an extending expression, so the temporaries in its trailing
-// expression are dropped immediately.
-pin!({ &temp() }); // ERROR
-```
-
-```rust,edition2024,compile_fail,E0716
-# fn temp() {}
-// As above.
-format_args!("{:?}", { &temp() }); // ERROR
-```
-
 r[destructors.forget]
 ## Not running destructors
 
@@ -647,6 +704,7 @@ There is one additional case to be aware of: when a panic reaches a [non-unwindi
 [Assignment]: expressions/operator-expr.md#assignment-expressions
 [binding modes]: patterns.md#binding-modes
 [closure]: types/closure.md
+[constant item]: items/constant-items.md
 [destructors]: destructors.md
 [destructuring assignment]: expr.assign.destructure
 [expression]: expressions.md
@@ -660,6 +718,7 @@ There is one additional case to be aware of: when a panic reaches a [non-unwindi
 [promoted]: destructors.md#constant-promotion
 [scrutinee]: glossary.md#scrutinee
 [statement]: statements.md
+[static item]: items/static-items.md
 [temporary]: expressions.md#temporaries
 [unwinding]: panic.md#unwinding
 [variable]: variables.md
@@ -681,10 +740,10 @@ There is one additional case to be aware of: when a panic reaches a [non-unwindi
 
 [array expression]: expressions/array-expr.md#array-expressions
 [array repeat operands]: expr.array.repeat-operand
-[async block expression]: expr.block.async
 [block expression]: expressions/block-expr.md
-[borrow]: expr.operator.borrow
+[borrow expression]: expr.operator.borrow
 [cast expression]: expressions/operator-expr.md#type-cast-expressions
+[const block expression]: expr.block.const
 [dereference expression]: expressions/operator-expr.md#the-dereference-operator
 [extended]: destructors.scope.lifetime-extension
 [field expression]: expressions/field-expr.md
@@ -692,11 +751,11 @@ There is one additional case to be aware of: when a panic reaches a [non-unwindi
 [struct expression]: expressions/struct-expr.md
 [super macro call]: expr.super-macros
 [super operands]: expr.super-macros
-[super temporaries]: expr.super-macros
+[super temporary]: expr.super-macros
 [temporary scope]: destructors.scope.temporary
-[temporary scopes]: destructors.scope.temporary
 [tuple expression]: expressions/tuple-expr.md#tuple-expressions
 [tuple indexing expression]: expressions/tuple-expr.md#tuple-indexing-expressions
+[`unsafe` block expression]: expr.block.unsafe
 
 [`for`]: expressions/loop-expr.md#iterator-loops
 [`if let`]: expressions/if-expr.md#if-let-patterns
diff --git a/src/expressions.md b/src/expressions.md
index 9abc51ae59..353993dc5f 100644
--- a/src/expressions.md
+++ b/src/expressions.md
@@ -262,7 +262,7 @@ r[expr.super-macros.intro]
 Certain built-in macros may create [temporaries] whose [scopes][temporary scopes] may be [extended]. These temporaries are *super temporaries* and these macros are *super macros*. [Invocations][macro invocations] of these macros are *super macro call expressions*. Arguments to these macros may be *super operands*.
 
 > [!NOTE]
-> When a super macro call expression is an [extending expression], its super operands are [extending expressions] and the [scopes][temporary scopes] of the super temporaries are [extended]. See [destructors.scope.lifetime-extension.exprs].
+> The super operands of a super macro call are [extending expressions] and the [scopes][temporary scopes] of the super temporaries are [extended]. See [destructors.scope.lifetime-extension.exprs].
 
 r[expr.super-macros.format_args]
 #### `format_args!`
@@ -272,10 +272,11 @@ Except for the format string argument, all arguments passed to [`format_args!`]
 
 ```rust,edition2024
 # fn temp() -> String { String::from("") }
-// Due to the call being an extending expression and the argument
-// being a super operand, the inner block is an extending expression,
-// so the scope of the temporary created in its trailing expression
-// is extended.
+// Due to the argument being a super operand, the inner block is an
+// extending expression, so the scope of the temporary created in its
+// trailing expression is extended to the extended scope of the call.
+// Since the call is the initializer of a `let` statement, this
+// extends it to the end of the surrounding block.
 let _ = format_args!("{}", { &temp() }); // OK
 ```
 
@@ -406,7 +407,6 @@ They are never allowed before:
 [destructors]:          destructors.md
 [drop scope]:           destructors.md#drop-scopes
 [extended]:             destructors.scope.lifetime-extension
-[extending expression]: destructors.scope.lifetime-extension.exprs
 [extending expressions]: destructors.scope.lifetime-extension.exprs
 [field]:                expressions/field-expr.md
 [functional update]:    expressions/struct-expr.md#functional-update-syntax
diff --git a/src/expressions/operator-expr.md b/src/expressions/operator-expr.md
index 735d9cea3a..6a4d87467b 100644
--- a/src/expressions/operator-expr.md
+++ b/src/expressions/operator-expr.md
@@ -900,9 +900,9 @@ r[expr.assign.destructure.tmp-scopes]
 
 r[expr.assign.destructure.tmp-ext]
 > [!NOTE]
-> Due to the desugaring, the assigned value operand (the RHS) of a destructuring assignment is an [extending expression] within a newly-introduced block.
+> Due to the desugaring, the assigned value operand (the RHS) of a destructuring assignment is the initializer expression of a `let` statement within a newly-introduced block.
 >
-> Below, because the [temporary scope] is extended to the end of this introduced block, the assignment is allowed.
+> Below, because the [temporary scope] is [extended] to the end of this introduced block, the assignment is allowed.
 >
 > ```rust
 > # fn temp() {}
@@ -1089,7 +1089,7 @@ As with normal assignment expressions, compound assignment expressions always pr
 [dropping]: ../destructors.md
 [eval order test]: https://github.com/rust-lang/rust/blob/1.58.0/src/test/ui/expr/compound-assignment/eval-order.rs
 [explicit discriminants]: ../items/enumerations.md#explicit-discriminants
-[extending expression]: destructors.scope.lifetime-extension.exprs
+[extended]: destructors.scope.lifetime-extension.exprs
 [field-less enums]: ../items/enumerations.md#field-less-enum
 [grouped expression]: grouped-expr.md
 [literal expression]: literal-expr.md#integer-literal-expressions
diff --git a/src/scoping-model.lagda.md b/src/scoping-model.lagda.md
new file mode 100644
index 0000000000..4bf66e781a
--- /dev/null
+++ b/src/scoping-model.lagda.md
@@ -0,0 +1,430 @@
+# Appendix: Formal scoping model
+
+This appendix presents a formal model of temporary scoping rules in Rust. It compares the current stable behavior with that of [Rust PR #146098] / [Reference PR #2051], and it compares different formalizations of *borrow scopes* and *extended subexpressions*.
+
+The model is written in [Agda](https://github.com/agda/agda), a dependently typed functional programming language. This chapter is executable [literate Agda].
+
+```agda
+module scoping-model (FnCtxt ConstCtxt : Set) where
+
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (ℕ)
+open import Function using (_|>_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+```
+
+## Reading guide
+
+> [!NOTE]
+> For readers familiar with Rust but new to Agda, here is a brief guide to the notation used in this model.
+>
+> - `data ... where`: Similar to a Rust `enum`. Each line in the `where` block is a variant (constructor).
+> - `record`: Similar to a Rust `struct`.
+> - `{...}`: Implicit arguments. Agda infers these, similar to generic type inference or lifetime elision in Rust.
+> - `_▷_`: Underscores in names indicate where arguments go (infix operators). `_▷_` is an infix constructor.
+> - `refl`: Stands for "reflexivity"; used to prove that two values are equal.
+> - Pattern matching: Definitions are often spread across multiple equations, similar to a `match` expression at the function level.
+
+## Common definitions
+
+### Syntax and contexts
+
+To focus on scoping, this appendix models a simplified abstract syntax tree (AST).
+
+- `Array` (`⟦…,●,…⟧`) represents all *extending expressions* (structs, tuples, arrays).
+- `Indexing` (`●⟦…⟧`) represents all *place base contexts* (derefs, fields, indexes).
+
+The *context* of a syntax-tree node uniquely identifies where in the source it appears. This is defined inductively.
+
+```agda
+data NodeKind : Set where
+  Stmt : NodeKind
+  Expr : NodeKind
+  FnDecl : NodeKind
+  ConstDecl : NodeKind
+  Toplevel : NodeKind
+
+-- Patterns are either extending patterns (like `ref x`) or not.
+data Pat : Set where
+  pat-ext : Pat
+  pat-non : Pat
+
+-- Each sub-node is the child of a particular kind of parent node.
+data _SubnodeOf_ : NodeKind → NodeKind → Set where
+  -- A function.
+  node-fn : (fn : FnCtxt) → FnDecl SubnodeOf Toplevel
+  -- A constant.
+  node-const : (const : ConstCtxt) → ConstDecl SubnodeOf Toplevel
+  -- The nᵗʰ statement in a block:
+  ⦃…●…⦄ : (n : ℕ) → Stmt SubnodeOf Expr
+  -- The body expression of a function:
+  |…|● : Expr SubnodeOf FnDecl
+  -- The body expression of a constant item:
+  const…=●⨾ : Expr SubnodeOf ConstDecl
+  -- The initializer expression of a `let` statement:
+  let…=●⨾ : (pat : Pat) → Expr SubnodeOf Stmt
+  -- The expression of an expression statement:
+  ●⨾ : Expr SubnodeOf Stmt
+  -- The tail expression of a block:
+  ⦃…⨾●⦄ : Expr SubnodeOf Expr
+  -- The nᵗʰ argument expression to a call:
+  …⦅…,●,…⦆ : (n : ℕ) → Expr SubnodeOf Expr
+  -- The nᵗʰ operand expression to an array constructor:
+  ⟦…,●,…⟧ : (n : ℕ) → Expr SubnodeOf Expr
+  -- The indexed array operand of an indexing operator expression:
+  ●⟦…⟧ : Expr SubnodeOf Expr
+  -- The operand of a borrow expression:
+  &● : Expr SubnodeOf Expr
+
+infixl 5 _▷_
+
+data Context : NodeKind → Set where
+  ctxt-top : Context Toplevel
+  _▷_ : ∀ {k₁ k₂} → Context k₁ → k₂ SubnodeOf k₁ → Context k₂
+```
+
+This formulation allows constructs like `const X: &T = f(&●);` to be represented as a chain of contexts:
+
+```agda
+exampleContext : ConstCtxt → Context Expr
+exampleContext const =
+  ctxt-top ▷ node-const const ▷ const…=●⨾ ▷ …⦅…,●,…⦆ 0 ▷ &●
+```
+
+Helpers can also be defined to navigate the AST, such as finding the block containing a statement:
+
+```agda
+blockOf : Context Stmt → Context Expr
+blockOf (e-block ▷ ⦃…●…⦄ _) = e-block
+```
+
+### Scopes
+
+A *scope* is the syntactic context in which a temporary or variable lives. When execution leaves that context, the value is dropped.
+
+> [!NOTE]
+> In `rustc`, scopes are more granular (e.g., individual statements have remainder scopes). This model simplifies this by associating scopes directly with AST nodes.
+
+```agda
+record Scope : Set where
+  constructor scope
+  field
+    {kind} : NodeKind
+    ctxt : Context kind
+```
+
+#### Scope hierarchy
+
+Scopes form a hierarchy. The `Hierarchy` module defines the ancestry relation, where `_≻_` is the parent relation and `_≻*_` is the reflexive transitive closure (ancestor relation).
+
+```agda
+module Hierarchy where
+  open import Relation.Binary.Construct.Closure.ReflexiveTransitive
+    using (Star)
+
+  data _≻_ : Scope → Scope → Set where
+    parent≻child : ∀ x {k} (n : k SubnodeOf Scope.kind x) →
+      x ≻ scope (Scope.ctxt x ▷ n)
+
+  _≻*_ : Scope → Scope → Set
+  _≻*_ = Star _≻_
+```
+
+## The enclosing temporary scope
+
+The temporary scope of non-extended temporaries is the closest ancestor temporary scope boundary, as defined by [destructors.scope.temporary.enclosing].
+
+```agda
+enclosingTempScope : Context Expr → Scope
+-- Body expressions are temporary scope boundaries.
+enclosingTempScope e-body@(_ ▷ |…|●) = scope e-body
+enclosingTempScope e-body@(_ ▷ const…=●⨾) = scope e-body
+-- Statements are temporary scope boundaries.
+enclosingTempScope (s-let ▷ let…=●⨾ _) = scope s-let
+enclosingTempScope (s-expr ▷ ●⨾) = scope s-expr
+-- Block tails are temporary scope boundaries
+enclosingTempScope e-tail@(_ ▷ ⦃…⨾●⦄) = scope e-tail
+-- Our other contexts are not temporary scope boundaries.
+enclosingTempScope (e-call ▷ …⦅…,●,…⦆ _) = enclosingTempScope e-call
+enclosingTempScope (e-array ▷ ⟦…,●,…⟧ _) = enclosingTempScope e-array
+enclosingTempScope (e-indexing ▷ ●⟦…⟧) = enclosingTempScope e-indexing
+enclosingTempScope (e-ref ▷ &●) = enclosingTempScope e-ref
+```
+
+## Stable Rust
+
+First, an auxiliary definition is required: *extending contexts* correspond to [destructors.scope.lifetime-extension.exprs.extending].
+
+The operand of an extending borrow expression has an extended temporary scope. The `extendingScope` function determines if a context is extending, and if so, what scope it extends a borrowed temporary to.
+
+```agda
+extendingScope : Context Expr → Maybe Scope
+-- `let` statements extend temporaries to the end of the block.
+extendingScope (s-let ▷ let…=●⨾ _) = just (scope (blockOf s-let))
+-- Constant items extend temporaries to the end of the program.
+extendingScope (_ ▷ const…=●⨾) = just (scope ctxt-top)
+-- Block tails, array expression operands, and borrow expression
+-- operands are extending if their parents are, and extend to the same
+-- scope.
+extendingScope (e-block ▷ ⦃…⨾●⦄) = extendingScope e-block
+extendingScope (e-array ▷ ⟦…,●,…⟧ _) = extendingScope e-array
+extendingScope (e-ref ▷ &●) = extendingScope e-ref
+-- These expressions aren't extending.
+extendingScope (_ ▷ |…|●) = nothing
+extendingScope (_ ▷ ●⨾) = nothing
+extendingScope (_ ▷ …⦅…,●,…⦆ _) = nothing
+extendingScope (_ ▷ ●⟦…⟧) = nothing
+```
+
+There is another consideration in the definition of temporary scopes: [destructors.scope.lifetime-extension.sub-expressions], also known as *the subexpressions rule*.
+
+This is interpreted as defining a grammar of *subexpression contexts*. The temporary scope of a subexpression context is the same as its parent's temporary scope.
+
+```agda
+tempScope-stable : Context Expr → Scope
+-- `let ref x = ●;` has an extended temporary scope.
+tempScope-stable (s-let ▷ let…=●⨾ pat-ext) = scope (blockOf s-let)
+-- The subexpressions rule: `●⟦…⟧` has the same temporary scope as
+-- its parent, and `&●` does as well in "subexpression contexts".
+tempScope-stable (e-indexing ▷ ●⟦…⟧) = tempScope-stable e-indexing
+tempScope-stable (e-ref@(_ ▷ ●⟦…⟧) ▷ &●) = tempScope-stable e-ref
+tempScope-stable (e-inner-ref@(_ ▷ &●) ▷ &●) =
+  tempScope-stable e-inner-ref
+-- The scope of `&●` in other contexts depends on whether its parent
+-- is extending. If so, its temporary scope is extended by
+-- `extendingScope`.  Otherwise, its temporary scope is its enclosing
+-- temporary scope.
+{-# CATCHALL #-}
+tempScope-stable e-operand@(e-ref ▷ &●) with extendingScope e-ref
+… | just x-extended = x-extended
+… | nothing = enclosingTempScope e-operand
+-- Our other contexts don't have extended temporary scopes.  Their
+-- temporary scopes are their enclosing temporary scopes.
+{-# CATCHALL #-}
+tempScope-stable e-other = enclosingTempScope e-other
+```
+
+### Alternate formulation: expanded subexpressions rule
+
+The subexpressions rule can be reinterpreted as applying more broadly and uniformly: the temporary scope of `e ▷ &●` for non-extending `e` is the temporary scope of `e`.
+
+```agda
+tempScope-stable′ : Context Expr → Scope
+-- `let ref x = ●;` has an extended temporary scope.
+tempScope-stable′ (s-let ▷ let…=●⨾ pat-ext) = scope (blockOf s-let)
+-- `●[…]` has the same temporary scope as its parent, per the sub-expr
+-- rule.
+tempScope-stable′ (e-indexing ▷ ●⟦…⟧) = tempScope-stable′ e-indexing
+-- The scope of `&●` depends on whether the borrow is extending.  If
+-- it's extending, its temporary scope is extended by
+-- `extendingScope`.  Otherwise, its temporary scope is the same as
+-- its parent's, per the expanded subexpressions rule.
+tempScope-stable′ (e-ref ▷ &●) with extendingScope e-ref
+… | just x-extended = x-extended
+… | nothing = tempScope-stable′ e-ref
+-- Our other contexts don't have extended temporary scopes.  Their
+-- temporary scopes are their enclosing temporary scopes.
+{-# CATCHALL #-}
+tempScope-stable′ e-other = enclosingTempScope e-other
+```
+
+This is equivalent to the definition of `tempScope-stable` above: `∀ e → tempScope-stable e ≡ tempScope-stable′ e`.
+
+#### Proof
+
+**Lemma**: If `e` is an extending context (`extendingScope e ≡ just x`), then `tempScope-stable (e ▷ &●)` is `x`. This requires induction because `tempScope-stable` recurses on `&●` chains.
+
+I.e., "if a context `e` extends its temporaries to scope `x`, then the temporary scope of a borrow in that context is `x`".
+
+```agda
+lemma-extending : ∀ e {x}
+  → (extendingScope e ≡ just x) → (tempScope-stable (e ▷ &●) ≡ x)
+lemma-extending (e ▷ ⦃…⨾●⦄) p rewrite p = refl
+lemma-extending (e ▷ ⟦…,●,…⟧ n) p rewrite p = refl
+lemma-extending (e ▷ &●) p = lemma-extending e p
+lemma-extending (s ▷ let…=●⨾ pat) refl = refl
+lemma-extending (c ▷ const…=●⨾) refl = refl
+lemma-extending (fn ▷ |…|●) ()
+lemma-extending (s ▷ ●⨾) ()
+lemma-extending (e ▷ …⦅…,●,…⦆ n) ()
+lemma-extending (e ▷ ●⟦…⟧) ()
+```
+
+Proof that `tempScope-stable` and `tempScope-stable′` are equivalent.
+
+```agda
+proof-tempScope-equiv :
+  ∀ e → tempScope-stable e ≡ tempScope-stable′ e
+proof-tempScope-equiv (e ▷ |…|●) = refl
+proof-tempScope-equiv (e ▷ const…=●⨾) = refl
+proof-tempScope-equiv (e ▷ let…=●⨾ pat-ext) = refl
+proof-tempScope-equiv (e ▷ let…=●⨾ pat-non) = refl
+proof-tempScope-equiv (e ▷ ●⨾) = refl
+proof-tempScope-equiv (e ▷ ⦃…⨾●⦄) = refl
+proof-tempScope-equiv (e ▷ …⦅…,●,…⦆ n) = refl
+proof-tempScope-equiv (e ▷ ⟦…,●,…⟧ n) = refl
+proof-tempScope-equiv (e ▷ ●⟦…⟧) = proof-tempScope-equiv e
+proof-tempScope-equiv ((e ▷ ●⟦…⟧) ▷ &●) = proof-tempScope-equiv e
+proof-tempScope-equiv ((e ▷ &●) ▷ &●)
+  -- Adding the recursive call to the with-abstraction is done as
+  -- otherwise Agda's termination checker will fail to validate this
+  -- as terminating.  See:
+  --
+  -- - <https://agda.readthedocs.io/en/stable/language/with-abstraction.html#termination-checking>
+  with proof-tempScope-equiv (e ▷ &●) | extendingScope e in eq
+… | _ | just _ = lemma-extending e eq
+… | rec | nothing = rec
+proof-tempScope-equiv ((_ ▷ |…|●) ▷ &●) = refl
+proof-tempScope-equiv ((_ ▷ const…=●⨾) ▷ &●) = refl
+proof-tempScope-equiv ((_ ▷ let…=●⨾ _) ▷ &●) = refl
+proof-tempScope-equiv ((_ ▷ ●⨾) ▷ &●) = refl
+proof-tempScope-equiv ((e ▷ ⦃…⨾●⦄) ▷ &●) with extendingScope e
+… | just _ = refl
+… | nothing = refl
+proof-tempScope-equiv ((_ ▷ …⦅…,●,…⦆ _) ▷ &●) = refl
+proof-tempScope-equiv ((e ▷ ⟦…,●,…⟧ _) ▷ &●) with extendingScope e
+… | just _ = refl
+… | nothing = refl
+```
+
+## Compiler PR #146098
+
+For [Rust PR #146098], the partial definition of extending expressions (`extendingScope`) is replaced with a total function that determines the scope of borrow expressions' operands in any non-subexpression context. This is what was called the "extended scope" in [Reference PR #2051].
+
+`refScope-146098 e` is the scope of `e ▷ &●` when `e` is not a subexpression context.
+
+```agda
+refScope-146098 : Context Expr → Scope
+-- `let x = &●;` has an extended temporary scope.
+refScope-146098 (s-let ▷ let…=●⨾ _) = scope (blockOf s-let)
+-- `const … = &●;` has an extended temporary scope.
+refScope-146098 (_ ▷ const…=●⨾) = scope ctxt-top
+-- Extending subexpressions preserve `&●`'s temporary scope.
+refScope-146098 (e-block ▷ ⦃…⨾●⦄) = refScope-146098 e-block
+refScope-146098 (e-array ▷ ⟦…,●,…⟧ _) = refScope-146098 e-array
+refScope-146098 (e-ref-outer ▷ &●) = refScope-146098 e-ref-outer
+-- In other contexts, the temp scope of `&●` is the enclosing temp
+-- scope.
+{-# CATCHALL #-}
+refScope-146098 e-other = enclosingTempScope e-other
+```
+
+Temporary scoping with this new rule can then be defined analogously to the definition for stable Rust:
+
+```agda
+tempScope-146098 : Context Expr → Scope
+-- `let ref x = ●;` has an extended temporary scope.
+tempScope-146098 (s-let ▷ let…=●⨾ pat-ext) = scope (blockOf s-let)
+-- The subexpressions rule: `●⟦…⟧` has the same temporary scope as
+-- its parent, and `&●` does as well in "subexpression contexts".
+tempScope-146098 (e-indexing ▷ ●⟦…⟧) = tempScope-146098 e-indexing
+tempScope-146098 (e-ref@(_ ▷ ●⟦…⟧) ▷ &●) = tempScope-146098 e-ref
+tempScope-146098 (e-inner-ref@(_ ▷ &●) ▷ &●) = tempScope-146098 e-inner-ref
+-- The scope of `&●` in other contexts is given by `refScope-146098`.
+{-# CATCHALL #-}
+tempScope-146098 (e-ref ▷ &●) = refScope-146098 e-ref
+-- Our other contexts don't have extended temporary scopes.
+-- Their temporary scopes are their enclosing temporary scopes.
+{-# CATCHALL #-}
+tempScope-146098 e-other = enclosingTempScope e-other
+```
+
+This still splits temporary scoping into two steps: first, apply the subexpressions rule; second, if you end up in an `&●` you take the `refScope-146098`, and otherwise you take the `enclosingTempScope`. The separation is important: it means [Rust PR #146098] only extends temporaries past statement/`const` boundaries when stable Rust does.
+
+## The expanded subexpressions rule
+
+In [this commit to the Reference PR](https://github.com/rust-lang/reference/pull/2051/commits/6536b3be7957261bfe91567af8737454b6c34d40), an alternative interpretation of the subexpressions rule is considered: that the temporary scope of `&●` in a non-extending context is the temporary scope of its parent. This is achieved by defining `tempScope-refPr` and `refScope-refPr` through mutual recursion:
+
+```agda
+tempScope-refPr : Context Expr → Scope
+refScope-refPr : Context Expr → Scope
+
+-- `let ref x = ●;` has an extended temporary scope.
+tempScope-refPr (s-let ▷ let…=●⨾ pat-ext) = scope (blockOf s-let)
+-- `●[…]` has the same temporary scope as its parent, per the expanded
+-- subexpressions rule.
+tempScope-refPr (e-indexing ▷ ●⟦…⟧) = tempScope-refPr e-indexing
+-- The temporary scope of `&●` is given by `refScope-refPr`.
+tempScope-refPr (e-ref ▷ &●) = refScope-refPr e-ref
+-- Our other contexts don't have extended temporary scopes.  Their
+-- temporary scopes are their enclosing temporary scopes.
+{-# CATCHALL #-}
+tempScope-refPr e-other = enclosingTempScope e-other
+
+-- `let x = &●;` has an extended temporary scope.
+refScope-refPr (s-let ▷ let…=●⨾ _) = scope (blockOf s-let)
+-- `const … = &●;` has an extended temporary scope.
+refScope-refPr (_ ▷ const…=●⨾) = scope ctxt-top
+-- Extending subexpressions preserve `&●`'s temporary scope.
+refScope-refPr (e-block ▷ ⦃…⨾●⦄) = refScope-refPr e-block
+refScope-refPr (e-array ▷ ⟦…,●,…⟧ _) = refScope-refPr e-array
+refScope-refPr (e-ref-outer ▷ &●) = refScope-refPr e-ref-outer
+-- `&●` outside of an extending subexpression has the same temporary
+-- scope as its parent, per the expanded subexpressions rule.
+{-# CATCHALL #-}
+refScope-refPr e-ref-other = tempScope-refPr e-ref-other
+```
+
+Similar to stable Rust, the scoping rules for `e ▷ &●` no longer depend on whether `e` is a subexpression context. This does however mean that it allows more programs than [Rust PR #146098] does by extending some temporaries past statement boundaries. Consider the expression context `let x = &[&●][0];`:
+
+```agda
+let＿=&⟦&●⟧⟦0⟧⨾ : Context Stmt → Context Expr
+let＿=&⟦&●⟧⟦0⟧⨾ s = s ▷ let…=●⨾ pat-non ▷ &● ▷ ●⟦…⟧ ▷ ⟦…,●,…⟧ 0 ▷ &●
+```
+
+In stable Rust and under [Rust PR #146098], the context's temporary scope is not extended, meaning any later use of `x` would result in a borrow-checking error:
+
+```agda
+scope-let＿=&⟦&●⟧⟦0⟧⨾-stable : ∀ s-let →
+  tempScope-stable (s-let |> let＿=&⟦&●⟧⟦0⟧⨾) ≡ scope s-let
+scope-let＿=&⟦&●⟧⟦0⟧⨾-stable _ = refl
+
+scope-let＿=&⟦&●⟧⟦0⟧⨾-146098 : ∀ s-let →
+  tempScope-146098 (s-let |> let＿=&⟦&●⟧⟦0⟧⨾) ≡ scope s-let
+scope-let＿=&⟦&●⟧⟦0⟧⨾-146098 _ = refl
+```
+
+However, with the expanded subexpressions rule, this is extended to the end of the block:
+
+```agda
+scope-let＿=&⟦&●⟧⟦0⟧⨾-refPr : ∀ s-let →
+  tempScope-refPr (s-let |> let＿=&⟦&●⟧⟦0⟧⨾) ≡ scope (blockOf s-let)
+scope-let＿=&⟦&●⟧⟦0⟧⨾-refPr _ = refl
+```
+
+## Alternate formulation: single function
+
+These rules can also be expressed using a single function:
+
+```agda
+tempScope-refPr′ : Context Expr → Scope
+-- `let ref x = ●;` and `let _ = &●;` have extended temporary scopes.
+tempScope-refPr′ (s-let ▷ let…=●⨾ pat-ext) = scope (blockOf s-let)
+tempScope-refPr′ (s-let ▷ let…=●⨾ _ ▷ &●) = scope (blockOf s-let)
+-- `const … = &●;` has an extended temporary scope.
+tempScope-refPr′ (_ ▷ const…=●⨾ ▷ &●) = scope ctxt-top
+-- `●[…]` has the same temporary scope as its parent, per the expanded
+-- subexpressions rule.
+tempScope-refPr′ (e-indexing ▷ ●⟦…⟧) = tempScope-refPr′ e-indexing
+-- Extending subexpressions preserve `&●`'s temporary scope.
+tempScope-refPr′ (e-block ▷ ⦃…⨾●⦄ ▷ &●) =
+  tempScope-refPr′ (e-block ▷ &●)
+tempScope-refPr′ (e-array ▷ ⟦…,●,…⟧ _ ▷ &●) =
+  tempScope-refPr′ (e-array ▷ &●)
+tempScope-refPr′ (e-ref-outer ▷ &● ▷ &●) =
+  tempScope-refPr′ (e-ref-outer ▷ &●)
+-- `&●` outside of an extending subexpression has the same temporary
+-- scope as its parent, per the expanded subexpressions rule.
+{-# CATCHALL #-}
+tempScope-refPr′ (e-ref-other ▷ &●) = tempScope-refPr′ e-ref-other
+-- Our other contexts don't have extended temporary scopes.
+-- Their temporary scopes are their enclosing temporary scopes.
+{-# CATCHALL #-}
+tempScope-refPr′ e-other = enclosingTempScope e-other
+```
+
+This offers a more visual interpretation of extending subexpressions: to find the temporary scope of `&●` within an extending subexpression, imagine moving the `&●` up as though it was in its parent's place. `tempScope-146098` can also be expressed in this way, but it still requires two function definitions or some extra bit of state to encode whether the subexpressions rule has been applied already.
+
+[literate Agda]: https://agda.readthedocs.io/en/latest/tools/literate-programming.html
+[Reference PR #2051]: https://github.com/rust-lang/reference/pull/2051
+[Rust PR #146098]: https://github.com/rust-lang/rust/pull/146098