Tighten cross-program interface examples

- Split mapping/storage interface examples into two files so the
  interface lives with its owning program and call sites are clearly
  cross-program.
- Drop blow-by-blow list of frontend passes in libraries.md in favor
  of "semantic validation".

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: mohammadfawaz

documentation/language/06_libraries.md

@@ -183,7 +183,7 @@ Explicit disambiguation using absolute paths (similar to Rust's `crate::foo::…
 
 ## Building a Library
 
-Running `leo build` inside a library package parses the library sources and runs the full frontend pipeline — name validation, global-item collection, path resolution, interface checks, type checking, and static analysis — on the library itself. Type errors, unknown identifiers, interface-cycle errors, and the like are reported at the library package, instead of surfacing only when a downstream program consumes it.
+Running `leo build` inside a library package parses the library sources and runs semantic validation on the library itself. Type errors, unknown identifiers, interface-cycle errors, and the like are reported at the library package, instead of surfacing only when a downstream program consumes it.
 
 ```bash
 cd math_utils

documentation/language/programs_in_practice/interfaces.md

@@ -204,11 +204,33 @@ Interface@(target[, network])::mapping.get_or_use(key, default)
 
 These reads are only valid inside a `final fn` or a `final {}` block — they lower to the AVM `get.dynamic`, `contains.dynamic`, and `get.or_use.dynamic` instructions. Dynamic *writes* are not supported.
 
-```leo
+`bank.aleo` declares the `Bank` interface and implements it:
+
+```leo title="bank/src/main.leo"
 interface Bank {
     mapping balances: address => u64;
 }
 
+program bank.aleo: Bank {
+    mapping balances: address => u64;
+
+    fn deposit(user: address, amount: u64) -> Final {
+        return final { do_deposit(user, amount); };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+
+final fn do_deposit(user: address, amount: u64) {
+    let prev: u64 = Mapping::get_or_use(balances, user, 0u64);
+    Mapping::set(balances, user, prev + amount);
+}
+```
+
+A second program imports `bank.aleo` and reads its mapping through the interface. Since the read is cross-program, the interface name is qualified with `bank.aleo::`:
+
+```leo title="checker/src/main.leo"
 import bank.aleo;
 
 program checker.aleo {
@@ -229,7 +251,7 @@ final fn do_read(target: field, user: address) {
 }
 ```
 
-When the interface is in scope without a program qualifier (for example, self-reading from the program that declares it), the leading `program.aleo::` segment can be omitted: `Bank@(target)::balances.get(key)`.
+When the reader is inside the same program that declares the interface, drop the program qualifier — `Bank@(target)::balances.get(key)` rather than `bank.aleo::Bank@(target)::balances.get(key)`.
 
 ### Dynamic Storage Reads
 
@@ -243,12 +265,33 @@ Interface@(target[, network])::vector.len()         // u32
 
 Singleton storage is read by naming the variable directly (no trailing `.op(...)`). Vector storage supports `.get(index)` (out-of-bounds reads return `none`) and `.len()` (no arguments). Storage writes through the dynamic interface are not supported — use a dynamic call to an entry function that performs the write.
 
-```leo
+`logger.aleo` declares the `Logger` interface and implements it:
+
+```leo title="logger/src/main.leo"
 interface Logger {
     storage counter: u64;
     storage entries: [u64];
 }
 
+program logger.aleo: Logger {
+    storage counter: u64;
+    storage entries: [u64];
+
+    fn bump(val: u64) -> Final {
+        return final {
+            counter = counter.unwrap_or(0u64) + 1u64;
+            entries.push(val);
+        };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+```
+
+A second program imports `logger.aleo` and reads its storage variables through the interface. Since the read is cross-program, the interface name is qualified with `logger.aleo::`:
+
+```leo title="reader/src/main.leo"
 import logger.aleo;
 
 program reader.aleo {