unsafe-deep-dive: replace may_overflow with a real safety precondition

src/SUMMARY.md

@@ -572,7 +572,7 @@ SPDX-License-Identifier: CC-BY-4.0
     - [Sometimes useful](unsafe-deep-dive/introduction/characteristics-of-unsafe-rust/sometimes-useful.md)
   - [Responsibility shift](unsafe-deep-dive/introduction/responsibility-shift.md)
   - [Stronger development workflow required](unsafe-deep-dive/introduction/impact-on-workflow.md)
-  - [Example: may_overflow](unsafe-deep-dive/introduction/may_overflow.md)
+  - [Example: a safety precondition](unsafe-deep-dive/introduction/may_overflow.md)
 - [Safety Preconditions](unsafe-deep-dive/safety-preconditions.md)
   - [Common Preconditions](unsafe-deep-dive/safety-preconditions/common-preconditions.md)
     - [Getter example](unsafe-deep-dive/safety-preconditions/getter.md)

src/unsafe-deep-dive/introduction/may_overflow.md

@@ -7,53 +7,51 @@ Copyright 2026 Google LLC
 SPDX-License-Identifier: CC-BY-4.0
 -->
 
-# Example: may_overflow function
+# Example: a safety precondition
 
-```rust,should_panic,editable
+```rust,editable
 # // Copyright 2026 Google LLC
 # // SPDX-License-Identifier: Apache-2.0
 #
-/// Adds 2^31 - 1 to negative numbers.
-unsafe fn may_overflow(a: i32) -> i32 {
-    a + i32::MAX
+/// Returns the element at `index` without bounds checking.
+///
+/// # Safety
+///
+/// The caller must guarantee that `index < slice.len()`.
+unsafe fn element_at(slice: &[i32], index: usize) -> i32 {
+    unsafe { *slice.get_unchecked(index) }
 }
 
 fn main() {
-    let x = unsafe { may_overflow(123) };
-    println!("{x}");
+    let numbers = [10, 20, 30];
+    // Safety: `1` is a valid index into `numbers`.
+    let value = unsafe { element_at(&numbers, 1) };
+    println!("{value}");
 }
 ```
 
 <details>
 
-“The `unsafe` keyword may have a subtly different meaning than what some people
-assume.”
+“`slice.get_unchecked(index)` returns the element at `index` without the bounds
+check that `slice[index]` performs. It is faster, but it is only sound when
+`index < slice.len()`.”
 
-“The code author believes that the code is correct. In principle, the code is
-safe.”
+“The compiler cannot verify that every caller respects this rule, so
+`element_at` is declared `unsafe` and states the rule in its `# Safety` section.
+Callers acknowledge that responsibility by wrapping the call in an `unsafe`
+block.”
 
-“In this toy example, the `may_overflow` function is only intended to be called
-with negative numbers.
+“Inside `element_at`, the call to `get_unchecked` is wrapped in its own `unsafe`
+block, because the body of an `unsafe fn` is a safe context — the inner block is
+what marks the unsafe operation.”
 
-Ask learners if they can explain why `may_overflow` requires the unsafe keyword.
+Ask the learners what happens if a caller passes an out-of-bounds index. The
+skipped check makes the access undefined behavior, so the safety precondition
+would be violated. The `unsafe` keyword is what shifts responsibility for
+upholding the precondition from the compiler to the programmer.
 
-“In case you’re unsure what the problem is, let’s pause briefly to explain. An
-`i32` only has 31 bits available for positive numbers. When an operation
-produces a result that requires more than 31 bits, then the program is put into
-an invalid state. And it’s not just a numerical problem. Compilers optimize code
-on the basis that invalid states are impossible. This causes code paths to be
-deleted, producing erratic runtime behavior while also introducing security
-vulnerabilities.
-
-Compile and run the code, producing a panic. Then run the example in the
-playground to run under `--release` mode to trigger UB.
-
-“This code can be used correctly, however, improper usage is highly dangerous.”
-
-“And it's impossible for the compiler to verify that the usage is correct.”
-
-This is what we mean when we say that the `unsafe` keyword marks the location
-where responsibility for memory safety shifts from the compiler to the
-programmer.
+“Note that integer overflow does not need this treatment: in Rust it is well
+defined (debug builds panic, release builds wrap), so it is never undefined
+behavior and never requires `unsafe`.”
 
 </details>