Document cross-package submodule access and library frontend passes

- Layout: explain program.aleo::submodule::item for structs, consts,
  helper fns, and interface references in program headers; helpers
  reached through this path are inlined into the caller's bytecode.
- Interfaces: document Interface@(target)::mapping.{get,contains,
  get_or_use}(...) and Interface@(target)::storage[.get(i)|.len()]
  dynamic-read forms, valid only in final context.
- Libraries: note that `leo build` on a library package now runs the
  full frontend pipeline, so errors surface at the library itself.

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

Author: mohammadfawaz

documentation/language/01_layout.md

@@ -165,6 +165,85 @@ fn increment(x: field) -> field {
 }
 ```
 
+### Accessing Submodules of Imported Programs
+
+When an imported program organizes its source across submodules, you can reach any `struct`, `const`, or helper `fn` from those submodules using an extended locator path:
+
+```
+program.aleo::submodule::item
+```
+
+For example, suppose `provider.aleo` has a submodule `colors` that defines a `Color` struct, a `MAX_CH` constant, and a `blend` helper:
+
+```leo title="provider/src/colors.leo"
+const MAX_CH: u32 = 255u32;
+
+struct Color {
+    r: u32,
+    g: u32,
+    b: u32,
+}
+
+fn blend(a: Color, b: Color) -> Color {
+    return Color {
+        r: (a.r + b.r) / 2u32,
+        g: (a.g + b.g) / 2u32,
+        b: (a.b + b.b) / 2u32,
+    };
+}
+```
+
+```leo title="provider/src/main.leo"
+program provider.aleo {
+    fn sum_channels(c: colors::Color) -> u32 {
+        return c.r + c.g + c.b;
+    }
+
+    fn mix_colors(a: colors::Color, b: colors::Color) -> colors::Color {
+        return colors::blend(a, b);
+    }
+
+    @noupgrade
+    constructor() {}
+}
+```
+
+A program that imports `provider.aleo` can reach the submodule struct, constant, and helper through the extended path, and can also call `provider.aleo`'s top-level entry functions:
+
+```leo title="consumer/src/main.leo"
+import provider.aleo;
+
+program consumer.aleo {
+    // Struct and const from the submodule.
+    fn make_white() -> provider.aleo::colors::Color {
+        return provider.aleo::colors::Color {
+            r: provider.aleo::colors::MAX_CH,
+            g: provider.aleo::colors::MAX_CH,
+            b: provider.aleo::colors::MAX_CH,
+        };
+    }
+
+    // Top-level entry function from the provider.
+    fn mix(a: provider.aleo::colors::Color, b: provider.aleo::colors::Color) -> provider.aleo::colors::Color {
+        return provider.aleo::mix_colors(a, b);
+    }
+
+    // Submodule helper called directly — inlined into consumer's bytecode.
+    fn average(a: provider.aleo::colors::Color, b: provider.aleo::colors::Color) -> provider.aleo::colors::Color {
+        return provider.aleo::colors::blend(a, b);
+    }
+
+    @noupgrade
+    constructor() {}
+}
+```
+
+Helper `fn`s reached through `program.aleo::submodule::name(...)` are inlined directly into the caller's bytecode; they are not separate on-chain calls and do not appear in the provider's ABI. Only top-level entry functions declared inside `program provider.aleo { ... }` remain part of its on-chain interface.
+
+Submodule paths can be arbitrarily deep — `program.aleo::a::b::item` is valid if `program.aleo` has a nested submodule `a/b.leo`. The same extended path syntax applies to library submodules (see [Leo Libraries](./06_libraries.md#submodules)).
+
+`interface` definitions may also be referenced through the same path syntax — both library submodules (`program my_app.aleo: my_lib::interfaces::Adder { ... }`) and imported program submodules (`program my_app.aleo: other_prog.aleo::interfaces::Adder { ... }`) work in a program header.
+
 <!--
 
 ## The Tests

documentation/language/06_libraries.md

@@ -181,6 +181,26 @@ When a library dependency and a local submodule share the same name, paths begin
 Explicit disambiguation using absolute paths (similar to Rust's `crate::foo::…` for local modules) is planned for a future release.
 :::
 
+## 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.
+
+```bash
+cd math_utils
+leo build
+```
+
+```
+       Leo 🔨 Building library 'math_utils'
+       Leo ✅ Validated 'math_utils'.
+```
+
+No bytecode is produced — libraries are inlined at the point of use and have no on-chain footprint — but any frontend errors are reported with spans pointing into the library's own source files.
+
+:::note
+When a program that depends on a library is built, library sources are compiled holistically with the program — any errors in the library still surface, but as part of the consuming program's build. Running `leo build` inside the library package itself validates it in isolation, so problems are caught at the source before any consumer tries to use it.
+:::
+
 ## Testing
 
 `leo test` works on library packages directly — no wrapper program is required. Place test files in the `tests/` directory and call library functions using the `library_name::item` path syntax.

documentation/language/programs_in_practice/interfaces.md

@@ -188,6 +188,93 @@ return TokenStandard@(target, network)::transfer_public(to, amount);
 The only valid network identifier currently is `aleo`.
 :::
 
+### Dynamic Mapping Reads
+
+An interface that declares a `mapping` can also be used to read that mapping on a runtime-determined program. The syntax mirrors dynamic calls, but with a mapping name in place of a method name and a trailing read operation:
+
+```
+Interface@(target[, network])::mapping.get(key)
+Interface@(target[, network])::mapping.contains(key)
+Interface@(target[, network])::mapping.get_or_use(key, default)
+```
+
+- `.get(key)` returns the mapped value; the transition fails at runtime if `key` is not present.
+- `.contains(key)` returns a `bool`.
+- `.get_or_use(key, default)` returns the mapped value, or `default` if `key` is absent.
+
+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
+interface Bank {
+    mapping balances: address => u64;
+}
+
+import bank.aleo;
+
+program checker.aleo {
+    mapping snapshot: address => u64;
+
+    fn read_balance(target: field, user: address) -> Final {
+        return final { do_read(target, user); };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+
+final fn do_read(target: field, user: address) {
+    let present: bool = bank.aleo::Bank@(target)::balances.contains(user);
+    let val: u64 = bank.aleo::Bank@(target)::balances.get_or_use(user, 0u64);
+    Mapping::set(snapshot, user, present ? val : 0u64);
+}
+```
+
+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)`.
+
+### Dynamic Storage Reads
+
+Interfaces that declare [`storage`](../02_structure.md#storage) variables support dynamic reads with the same pattern. Storage reads always return an `Option<T>`:
+
+```
+Interface@(target[, network])::singleton            // Option<T>
+Interface@(target[, network])::vector.get(index)    // Option<T>
+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
+interface Logger {
+    storage counter: u64;
+    storage entries: [u64];
+}
+
+import logger.aleo;
+
+program reader.aleo {
+    mapping latest: u32 => u64;
+
+    fn snapshot(target: field, i: u32) -> Final {
+        return final { do_snapshot(target, i); };
+    }
+
+    @noupgrade
+    constructor() {}
+}
+
+final fn do_snapshot(target: field, i: u32) {
+    let n: u32 = logger.aleo::Logger@(target)::entries.len();
+    let entry: u64? = logger.aleo::Logger@(target)::entries.get(i);
+    let current: u64? = logger.aleo::Logger@(target)::counter;
+    let stored: u64 = i < n ? entry.unwrap() : current.unwrap_or(0u64);
+    Mapping::set(latest, i, stored);
+}
+```
+
+:::note
+Dynamic mapping reads are a type-checked alternative to the [`_dynamic_get`, `_dynamic_contains`, and `_dynamic_get_or_use`](./intrinsics.md) intrinsics. The interface form checks that the named mapping exists on the interface and that keys, values, and defaults have matching types; the intrinsics accept arbitrary runtime identifiers and leave that responsibility to the caller. Prefer the interface form whenever an interface is available.
+:::
+
 ## Dynamic Records
 
 A `dyn record` is a record whose field structure is not known at compile time. It retains all the ownership and privacy properties of a regular record: